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/miplib2003/normalized-mps-v2-20-10-glass4.opb
MD5SUM	929651d54295ccab2bd7ed98e4ab5229
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	478
Biggest coefficient in the objective function	536870912000000
Number of bits for the biggest coefficient in the objective function	49
Sum of the numbers in the objective function	1073761158741413
Number of bits of the sum of numbers in the objective function	50
Biggest number in a constraint	71583145981965762560
Number of bits of the biggest number in a constraint	66
Biggest sum of numbers in a constraint	303620978593259257856
Number of bits of the biggest sum of numbers	69
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1224.1
Number of variables	780
Total number of constraints	707
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	338
Number of constraints which are nor clauses,nor cardinality constraints	369
Minimum length of a constraint	1
Maximum length of a constraint	101
Trace number 21813

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-22 01:01:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12593 boxname=wulflinc7 idbench=969 idsolver=9 numberseed=0
MD5SUM SOLVER: daf345f6fbf228671abfac48013b9cac  /oldhome/oroussel/solvers/sat4jPseudo.jar
MD5SUM BENCH:  929651d54295ccab2bd7ed98e4ab5229  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-glass4.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudo.jar /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-glass4.opb
IDLAUNCH: 12593
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        315536 kB
Buffers:         21040 kB
Cached:         675836 kB
SwapCached:        328 kB
Active:          42304 kB
Inactive:       657140 kB
HighTotal:      131008 kB
HighFree:        40180 kB
LowTotal:       903652 kB
LowFree:        275356 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6460 kB
Slab:            13840 kB
Committed_AS:    63576 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:21:38 (client local time) WITH STATUS 143 IN 1237.28 SECONDS
stats: 12593 7 1237.28 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-glass4.opb
c reading problem 
c [nbvar=780]
c [nbconstr=707]
c time 4.145
c #vars     780
c #clauses  442
c starts	: 0
c conflicts	: 0
c decisions	: 0
c propagations	: 0
c inspects	: 0
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 0
c SATISFIABLE
c OPTIMIZING...
c 
c CURRENT OPTIMUM=159137832
c Current CPU time (ms) : 21.154
c starts	: 1
c conflicts	: 61
c decisions	: 826
c propagations	: 1845
c inspects	: 29101
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 61
c root simplifications	: 1
c 
c CURRENT OPTIMUM=-1925002907
c Current CPU time (ms) : 25.269
c starts	: 2
c conflicts	: 64
c decisions	: 1313
c propagations	: 2690
c inspects	: 46317
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 64
c root simplifications	: 2
c 
c CURRENT OPTIMUM=-328284304
c Current CPU time (ms) : 29.086
c starts	: 3
c conflicts	: 67
c decisions	: 1794
c propagations	: 3507
c inspects	: 60779
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 67
c root simplifications	: 3
c 
c CURRENT OPTIMUM=-1808326524
c Current CPU time (ms) : 33.084
c starts	: 4
c conflicts	: 73
c decisions	: 2260
c propagations	: 4312
c inspects	: 75250
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 73
c root simplifications	: 4
c 
c CURRENT OPTIMUM=-1918604031
c Current CPU time (ms) : 36.758
c starts	: 5
c conflicts	: 74
c decisions	: 2741
c propagations	: 5090
c inspects	: 88952
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 74
c root simplifications	: 5
c 
c CURRENT OPTIMUM=-1812083270
c Current CPU time (ms) : 40.29
c starts	: 6
c conflicts	: 76
c decisions	: 3187
c propagations	: 5888
c inspects	: 101973
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 76
c root simplifications	: 6
c 
c CURRENT OPTIMUM=-1735635153
c Current CPU time (ms) : 45.669
c starts	: 7
c conflicts	: 87
c decisions	: 3713
c propagations	: 6900
c inspects	: 120847
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 87
c root simplifications	: 7
c 
c CURRENT OPTIMUM=-342285166
c Current CPU time (ms) : 49.143
c starts	: 8
c conflicts	: 89
c decisions	: 4166
c propagations	: 7690
c inspects	: 135114
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 89
c root simplifications	: 8
c 
c CURRENT OPTIMUM=1880570157
c Current CPU time (ms) : 54.137
c starts	: 9
c conflicts	: 96
c decisions	: 4810
c propagations	: 8785
c inspects	: 158573
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 96
c root simplifications	: 9
c 
c CURRENT OPTIMUM=-323863097
c Current CPU time (ms) : 57.825
c starts	: 10
c conflicts	: 99
c decisions	: 5277
c propagations	: 9580
c inspects	: 173544
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 99
c root simplifications	: 10
c 
c CURRENT OPTIMUM=-1889943020
c Current CPU time (ms) : 61.768
c starts	: 11
c conflicts	: 101
c decisions	: 5701
c propagations	: 10366
c inspects	: 189873
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 101
c root simplifications	: 11
c 
c CURRENT OPTIMUM=287801073
c Current CPU time (ms) : 65.919
c starts	: 12
c conflicts	: 104
c decisions	: 6184
c propagations	: 11170
c inspects	: 206494
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 104
c root simplifications	: 12
c 
c CURRENT OPTIMUM=1359039946
c Current CPU time (ms) : 70.872
c starts	: 13
c conflicts	: 114
c decisions	: 6624
c propagations	: 12061
c inspects	: 225438
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 114
c root simplifications	: 13
c 
c CURRENT OPTIMUM=-1579299984
c Current CPU time (ms) : 76.15
c starts	: 14
c conflicts	: 125
c decisions	: 7105
c propagations	: 12984
c inspects	: 244205
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 125
c root simplifications	: 14
c 
c CURRENT OPTIMUM=-1848580828
c Current CPU time (ms) : 80.106
c starts	: 15
c conflicts	: 126
c decisions	: 7497
c propagations	: 13765
c inspects	: 260045
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 126
c root simplifications	: 15
c 
c CURRENT OPTIMUM=-1713823817
c Current CPU time (ms) : 84.474
c starts	: 16
c conflicts	: 132
c decisions	: 7903
c propagations	: 14573
c inspects	: 274819
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 132
c root simplifications	: 16
c 
c CURRENT OPTIMUM=169906953
c Current CPU time (ms) : 99.87
c starts	: 17
c conflicts	: 219
c decisions	: 8463
c propagations	: 15920
c inspects	: 311613
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 219
c root simplifications	: 17
c 
c CURRENT OPTIMUM=-401334183
c Current CPU time (ms) : 108.578
c starts	: 18
c conflicts	: 236
c decisions	: 9013
c propagations	: 17199
c inspects	: 341969
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 236
c root simplifications	: 19
c 
c CURRENT OPTIMUM=-318070949
c Current CPU time (ms) : 113.832
c starts	: 19
c conflicts	: 239
c decisions	: 9456
c propagations	: 18000
c inspects	: 361463
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 239
c root simplifications	: 20
c 
c CURRENT OPTIMUM=-263329373
c Current CPU time (ms) : 118.969
c starts	: 20
c conflicts	: 242
c decisions	: 9875
c propagations	: 18801
c inspects	: 377672
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 242
c root simplifications	: 21
c 
c CURRENT OPTIMUM=-1246652102
c Current CPU time (ms) : 125.645
c starts	: 21
c conflicts	: 247
c decisions	: 10341
c propagations	: 19795
c inspects	: 400032
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 247
c root simplifications	: 22
c 
c CURRENT OPTIMUM=222252541
c Current CPU time (ms) : 132.454
c starts	: 22
c conflicts	: 249
c decisions	: 10883
c propagations	: 20723
c inspects	: 420049
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 249
c root simplifications	: 23
c 
c CURRENT OPTIMUM=-1416745602
c Current CPU time (ms) : 145.119
c starts	: 23
c conflicts	: 263
c decisions	: 11484
c propagations	: 21978
c inspects	: 450113
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 263
c root simplifications	: 24
c 
c CURRENT OPTIMUM=-428814942
c Current CPU time (ms) : 151.098
c starts	: 24
c conflicts	: 269
c decisions	: 11953
c propagations	: 22828
c inspects	: 471832
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 269
c root simplifications	: 25
c 
c CURRENT OPTIMUM=-381547328
c Current CPU time (ms) : 157.521
c starts	: 25
c conflicts	: 273
c decisions	: 12479
c propagations	: 23821
c inspects	: 493924
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 273
c root simplifications	: 26
c 
c CURRENT OPTIMUM=-347961567
c Current CPU time (ms) : 162.646
c starts	: 26
c conflicts	: 274
c decisions	: 12944
c propagations	: 24598
c inspects	: 510023
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 274
c root simplifications	: 27
c 
c CURRENT OPTIMUM=-288435450
c Current CPU time (ms) : 167.65
c starts	: 27
c conflicts	: 275
c decisions	: 13379
c propagations	: 25375
c inspects	: 524583
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 28
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 172.584
c starts	: 28
c conflicts	: 275
c decisions	: 13825
c propagations	: 26150
c inspects	: 538578
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 29
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 177.517
c starts	: 29
c conflicts	: 275
c decisions	: 14271
c propagations	: 26925
c inspects	: 552427
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 30
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 182.425
c starts	: 30
c conflicts	: 275
c decisions	: 14717
c propagations	: 27700
c inspects	: 566274
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 31
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 187.353
c starts	: 31
c conflicts	: 275
c decisions	: 15163
c propagations	: 28475
c inspects	: 580121
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 32
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 192.262
c starts	: 32
c conflicts	: 275
c decisions	: 15609
c propagations	: 29250
c inspects	: 593968
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 33
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 197.155
c starts	: 33
c conflicts	: 275
c decisions	: 16055
c propagations	: 30025
c inspects	: 607815
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 34
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 202.062
c starts	: 34
c conflicts	: 275
c decisions	: 16501
c propagations	: 30800
c inspects	: 621662
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 35
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 206.941
c starts	: 35
c conflicts	: 275
c decisions	: 16947
c propagations	: 31575
c inspects	: 635509
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 36
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 211.839
c starts	: 36
c conflicts	: 275
c decisions	: 17393
c propagations	: 32350
c inspects	: 649356
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 37
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 216.711
c starts	: 37
c conflicts	: 275
c decisions	: 17839
c propagations	: 33125
c inspects	: 663203
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 38
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 221.598
c starts	: 38
c conflicts	: 275
c decisions	: 18285
c propagations	: 33900
c inspects	: 677050
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 39
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 226.467
c starts	: 39
c conflicts	: 275
c decisions	: 18731
c propagations	: 34675
c inspects	: 690897
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 40
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 231.359
c starts	: 40
c conflicts	: 275
c decisions	: 19177
c propagations	: 35450
c inspects	: 704744
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 41
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 236.227
c starts	: 41
c conflicts	: 275
c decisions	: 19623
c propagations	: 36225
c inspects	: 718591
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 42
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 241.115
c starts	: 42
c conflicts	: 275
c decisions	: 20069
c propagations	: 37000
c inspects	: 732438
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 43
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 245.998
c starts	: 43
c conflicts	: 275
c decisions	: 20515
c propagations	: 37775
c inspects	: 746285
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 44
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 250.886
c starts	: 44
c conflicts	: 275
c decisions	: 20961
c propagations	: 38550
c inspects	: 760132
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 45
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 255.762
c starts	: 45
c conflicts	: 275
c decisions	: 21407
c propagations	: 39325
c inspects	: 773979
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 46
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 260.654
c starts	: 46
c conflicts	: 275
c decisions	: 21853
c propagations	: 40100
c inspects	: 787826
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 47
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 265.534
c starts	: 47
c conflicts	: 275
c decisions	: 22299
c propagations	: 40875
c inspects	: 801673
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 48
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 270.414
c starts	: 48
c conflicts	: 275
c decisions	: 22745
c propagations	: 41650
c inspects	: 815520
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 49
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 275.319
c starts	: 49
c conflicts	: 275
c decisions	: 23191
c propagations	: 42425
c inspects	: 829367
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 50
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 280.208
c starts	: 50
c conflicts	: 275
c decisions	: 23637
c propagations	: 43200
c inspects	: 843214
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 51
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 285.111
c starts	: 51
c conflicts	: 275
c decisions	: 24083
c propagations	: 43975
c inspects	: 857061
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 52
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 290.004
c starts	: 52
c conflicts	: 275
c decisions	: 24529
c propagations	: 44750
c inspects	: 870908
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 53
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 294.917
c starts	: 53
c conflicts	: 275
c decisions	: 24975
c propagations	: 45525
c inspects	: 884755
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 54
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 299.807
c starts	: 54
c conflicts	: 275
c decisions	: 25421
c propagations	: 46300
c inspects	: 898602
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 55
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 304.708
c starts	: 55
c conflicts	: 275
c decisions	: 25867
c propagations	: 47075
c inspects	: 912449
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 56
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 309.604
c starts	: 56
c conflicts	: 275
c decisions	: 26313
c propagations	: 47850
c inspects	: 926296
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 57
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 314.516
c starts	: 57
c conflicts	: 275
c decisions	: 26759
c propagations	: 48625
c inspects	: 940143
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 58
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 319.407
c starts	: 58
c conflicts	: 275
c decisions	: 27205
c propagations	: 49400
c inspects	: 953990
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 59
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 324.328
c starts	: 59
c conflicts	: 275
c decisions	: 27651
c propagations	: 50175
c inspects	: 967837
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 60
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 329.223
c starts	: 60
c conflicts	: 275
c decisions	: 28097
c propagations	: 50950
c inspects	: 981684
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 61
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 334.137
c starts	: 61
c conflicts	: 275
c decisions	: 28543
c propagations	: 51725
c inspects	: 995531
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 62
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 339.042
c starts	: 62
c conflicts	: 275
c decisions	: 28989
c propagations	: 52500
c inspects	: 1009378
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 63
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 343.952
c starts	: 63
c conflicts	: 275
c decisions	: 29435
c propagations	: 53275
c inspects	: 1023225
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 64
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 348.855
c starts	: 64
c conflicts	: 275
c decisions	: 29881
c propagations	: 54050
c inspects	: 1037072
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 65
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 353.725
c starts	: 65
c conflicts	: 275
c decisions	: 30327
c propagations	: 54825
c inspects	: 1050919
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 66
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 358.607
c starts	: 66
c conflicts	: 275
c decisions	: 30773
c propagations	: 55600
c inspects	: 1064766
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 67
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 363.472
c starts	: 67
c conflicts	: 275
c decisions	: 31219
c propagations	: 56375
c inspects	: 1078613
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 68
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 368.341
c starts	: 68
c conflicts	: 275
c decisions	: 31665
c propagations	: 57150
c inspects	: 1092460
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 69
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 373.193
c starts	: 69
c conflicts	: 275
c decisions	: 32111
c propagations	: 57925
c inspects	: 1106307
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 70
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 378.055
c starts	: 70
c conflicts	: 275
c decisions	: 32557
c propagations	: 58700
c inspects	: 1120154
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 71
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 382.897
c starts	: 71
c conflicts	: 275
c decisions	: 33003
c propagations	: 59475
c inspects	: 1134001
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 72
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 387.751
c starts	: 72
c conflicts	: 275
c decisions	: 33449
c propagations	: 60250
c inspects	: 1147848
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 73
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 392.589
c starts	: 73
c conflicts	: 275
c decisions	: 33895
c propagations	: 61025
c inspects	: 1161695
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 74
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 397.445
c starts	: 74
c conflicts	: 275
c decisions	: 34341
c propagations	: 61800
c inspects	: 1175542
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 75
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 402.288
c starts	: 75
c conflicts	: 275
c decisions	: 34787
c propagations	: 62575
c inspects	: 1189389
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 76
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 407.135
c starts	: 76
c conflicts	: 275
c decisions	: 35233
c propagations	: 63350
c inspects	: 1203236
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 77
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 411.992
c starts	: 77
c conflicts	: 275
c decisions	: 35679
c propagations	: 64125
c inspects	: 1217083
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 78
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 416.829
c starts	: 78
c conflicts	: 275
c decisions	: 36125
c propagations	: 64900
c inspects	: 1230930
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 79
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 421.697
c starts	: 79
c conflicts	: 275
c decisions	: 36571
c propagations	: 65675
c inspects	: 1244777
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 80
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 426.547
c starts	: 80
c conflicts	: 275
c decisions	: 37017
c propagations	: 66450
c inspects	: 1258624
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 81
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 431.416
c starts	: 81
c conflicts	: 275
c decisions	: 37463
c propagations	: 67225
c inspects	: 1272471
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 82
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 436.267
c starts	: 82
c conflicts	: 275
c decisions	: 37909
c propagations	: 68000
c inspects	: 1286318
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 83
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 441.131
c starts	: 83
c conflicts	: 275
c decisions	: 38355
c propagations	: 68775
c inspects	: 1300165
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 84
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 445.985
c starts	: 84
c conflicts	: 275
c decisions	: 38801
c propagations	: 69550
c inspects	: 1314012
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 85
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 450.85
c starts	: 85
c conflicts	: 275
c decisions	: 39247
c propagations	: 70325
c inspects	: 1327859
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 86
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 455.704
c starts	: 86
c conflicts	: 275
c decisions	: 39693
c propagations	: 71100
c inspects	: 1341706
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 87
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 460.586
c starts	: 87
c conflicts	: 275
c decisions	: 40139
c propagations	: 71875
c inspects	: 1355553
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 88
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 465.441
c starts	: 88
c conflicts	: 275
c decisions	: 40585
c propagations	: 72650
c inspects	: 1369400
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 89
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 470.307
c starts	: 89
c conflicts	: 275
c decisions	: 41031
c propagations	: 73425
c inspects	: 1383247
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 90
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 475.157
c starts	: 90
c conflicts	: 275
c decisions	: 41477
c propagations	: 74200
c inspects	: 1397094
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 91
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 480.007
c starts	: 91
c conflicts	: 275
c decisions	: 41923
c propagations	: 74975
c inspects	: 1410941
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 92
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 484.899
c starts	: 92
c conflicts	: 275
c decisions	: 42369
c propagations	: 75750
c inspects	: 1424788
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 93
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 489.767
c starts	: 93
c conflicts	: 275
c decisions	: 42815
c propagations	: 76525
c inspects	: 1438635
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 94
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 494.655
c starts	: 94
c conflicts	: 275
c decisions	: 43261
c propagations	: 77300
c inspects	: 1452482
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 95
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 499.54
c starts	: 95
c conflicts	: 275
c decisions	: 43707
c propagations	: 78075
c inspects	: 1466329
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 96
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 504.444
c starts	: 96
c conflicts	: 275
c decisions	: 44153
c propagations	: 78850
c inspects	: 1480176
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 97
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 509.326
c starts	: 97
c conflicts	: 275
c decisions	: 44599
c propagations	: 79625
c inspects	: 1494023
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 98
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 514.23
c starts	: 98
c conflicts	: 275
c decisions	: 45045
c propagations	: 80400
c inspects	: 1507870
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 99
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 519.099
c starts	: 99
c conflicts	: 275
c decisions	: 45491
c propagations	: 81175
c inspects	: 1521717
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 100
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 523.983
c starts	: 100
c conflicts	: 275
c decisions	: 45937
c propagations	: 81950
c inspects	: 1535564
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 101
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 528.849
c starts	: 101
c conflicts	: 275
c decisions	: 46383
c propagations	: 82725
c inspects	: 1549411
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 102
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 533.724
c starts	: 102
c conflicts	: 275
c decisions	: 46829
c propagations	: 83500
c inspects	: 1563258
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 103
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 538.58
c starts	: 103
c conflicts	: 275
c decisions	: 47275
c propagations	: 84275
c inspects	: 1577105
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 104
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 543.454
c starts	: 104
c conflicts	: 275
c decisions	: 47721
c propagations	: 85050
c inspects	: 1590952
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 105
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 548.309
c starts	: 105
c conflicts	: 275
c decisions	: 48167
c propagations	: 85825
c inspects	: 1604799
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 106
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 553.166
c starts	: 106
c conflicts	: 275
c decisions	: 48613
c propagations	: 86600
c inspects	: 1618646
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 107
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 558.047
c starts	: 107
c conflicts	: 275
c decisions	: 49059
c propagations	: 87375
c inspects	: 1632493
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 108
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 562.901
c starts	: 108
c conflicts	: 275
c decisions	: 49505
c propagations	: 88150
c inspects	: 1646340
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 109
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 567.773
c starts	: 109
c conflicts	: 275
c decisions	: 49951
c propagations	: 88925
c inspects	: 1660187
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 110
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 572.621
c starts	: 110
c conflicts	: 275
c decisions	: 50397
c propagations	: 89700
c inspects	: 1674034
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 111
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 577.491
c starts	: 111
c conflicts	: 275
c decisions	: 50843
c propagations	: 90475
c inspects	: 1687881
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 112
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 581.498
c starts	: 112
c conflicts	: 275
c decisions	: 51289
c propagations	: 91250
c inspects	: 1701728
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 113
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 585.535
c starts	: 113
c conflicts	: 275
c decisions	: 51735
c propagations	: 92025
c inspects	: 1715575
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 114
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 589.556
c starts	: 114
c conflicts	: 275
c decisions	: 52181
c propagations	: 92800
c inspects	: 1729422
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 115
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 593.6
c starts	: 115
c conflicts	: 275
c decisions	: 52627
c propagations	: 93575
c inspects	: 1743269
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 116
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 597.624
c starts	: 116
c conflicts	: 275
c decisions	: 53073
c propagations	: 94350
c inspects	: 1757116
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 117
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 601.667
c starts	: 117
c conflicts	: 275
c decisions	: 53519
c propagations	: 95125
c inspects	: 1770963
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 118
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 605.694
c starts	: 118
c conflicts	: 275
c decisions	: 53965
c propagations	: 95900
c inspects	: 1784810
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 119
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 609.744
c starts	: 119
c conflicts	: 275
c decisions	: 54411
c propagations	: 96675
c inspects	: 1798657
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 120
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 613.768
c starts	: 120
c conflicts	: 275
c decisions	: 54857
c propagations	: 97450
c inspects	: 1812504
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 121
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 617.782
c starts	: 121
c conflicts	: 275
c decisions	: 55303
c propagations	: 98225
c inspects	: 1826351
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 122
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 621.813
c starts	: 122
c conflicts	: 275
c decisions	: 55749
c propagations	: 99000
c inspects	: 1840198
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 123
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 625.815
c starts	: 123
c conflicts	: 275
c decisions	: 56195
c propagations	: 99775
c inspects	: 1854045
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 124
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 629.846
c starts	: 124
c conflicts	: 275
c decisions	: 56641
c propagations	: 100550
c inspects	: 1867892
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 125
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 633.854
c starts	: 125
c conflicts	: 275
c decisions	: 57087
c propagations	: 101325
c inspects	: 1881739
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 126
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 637.878
c starts	: 126
c conflicts	: 275
c decisions	: 57533
c propagations	: 102100
c inspects	: 1895586
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 127
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 641.884
c starts	: 127
c conflicts	: 275
c decisions	: 57979
c propagations	: 102875
c inspects	: 1909433
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 128
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 645.906
c starts	: 128
c conflicts	: 275
c decisions	: 58425
c propagations	: 103650
c inspects	: 1923280
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 129
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 649.906
c starts	: 129
c conflicts	: 275
c decisions	: 58871
c propagations	: 104425
c inspects	: 1937127
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 130
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 653.927
c starts	: 130
c conflicts	: 275
c decisions	: 59317
c propagations	: 105200
c inspects	: 1950974
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 131
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 657.93
c starts	: 131
c conflicts	: 275
c decisions	: 59763
c propagations	: 105975
c inspects	: 1964821
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 132
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 661.957
c starts	: 132
c conflicts	: 275
c decisions	: 60209
c propagations	: 106750
c inspects	: 1978668
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 133
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 665.964
c starts	: 133
c conflicts	: 275
c decisions	: 60655
c propagations	: 107525
c inspects	: 1992515
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 134
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 669.993
c starts	: 134
c conflicts	: 275
c decisions	: 61101
c propagations	: 108300
c inspects	: 2006362
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 135
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 674.004
c starts	: 135
c conflicts	: 275
c decisions	: 61547
c propagations	: 109075
c inspects	: 2020209
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 136
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 678.013
c starts	: 136
c conflicts	: 275
c decisions	: 61993
c propagations	: 109850
c inspects	: 2034056
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 137
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 682.039
c starts	: 137
c conflicts	: 275
c decisions	: 62439
c propagations	: 110625
c inspects	: 2047903
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 138
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 686.048
c starts	: 138
c conflicts	: 275
c decisions	: 62885
c propagations	: 111400
c inspects	: 2061750
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 139
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 690.061
c starts	: 139
c conflicts	: 275
c decisions	: 63331
c propagations	: 112175
c inspects	: 2075597
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 140
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 694.061
c starts	: 140
c conflicts	: 275
c decisions	: 63777
c propagations	: 112950
c inspects	: 2089444
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 141
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 698.074
c starts	: 141
c conflicts	: 275
c decisions	: 64223
c propagations	: 113725
c inspects	: 2103291
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 142
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 702.08
c starts	: 142
c conflicts	: 275
c decisions	: 64669
c propagations	: 114500
c inspects	: 2117138
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 143
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 706.101
c starts	: 143
c conflicts	: 275
c decisions	: 65115
c propagations	: 115275
c inspects	: 2130985
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 144
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 710.112
c starts	: 144
c conflicts	: 275
c decisions	: 65561
c propagations	: 116050
c inspects	: 2144832
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 145
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 714.131
c starts	: 145
c conflicts	: 275
c decisions	: 66007
c propagations	: 116825
c inspects	: 2158679
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 146
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 718.135
c starts	: 146
c conflicts	: 275
c decisions	: 66453
c propagations	: 117600
c inspects	: 2172526
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 147
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 722.152
c starts	: 147
c conflicts	: 275
c decisions	: 66899
c propagations	: 118375
c inspects	: 2186373
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 148
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 726.164
c starts	: 148
c conflicts	: 275
c decisions	: 67345
c propagations	: 119150
c inspects	: 2200220
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 149
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 730.191
c starts	: 149
c conflicts	: 275
c decisions	: 67791
c propagations	: 119925
c inspects	: 2214067
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 150
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 734.207
c starts	: 150
c conflicts	: 275
c decisions	: 68237
c propagations	: 120700
c inspects	: 2227914
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 151
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 738.221
c starts	: 151
c conflicts	: 275
c decisions	: 68683
c propagations	: 121475
c inspects	: 2241761
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 152
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 742.272
c starts	: 152
c conflicts	: 275
c decisions	: 69129
c propagations	: 122250
c inspects	: 2255608
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 153
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 746.288
c starts	: 153
c conflicts	: 275
c decisions	: 69575
c propagations	: 123025
c inspects	: 2269455
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 154
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 750.327
c starts	: 154
c conflicts	: 275
c decisions	: 70021
c propagations	: 123800
c inspects	: 2283302
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 155
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 754.344
c starts	: 155
c conflicts	: 275
c decisions	: 70467
c propagations	: 124575
c inspects	: 2297149
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 156
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 758.394
c starts	: 156
c conflicts	: 275
c decisions	: 70913
c propagations	: 125350
c inspects	: 2310996
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 157
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 762.418
c starts	: 157
c conflicts	: 275
c decisions	: 71359
c propagations	: 126125
c inspects	: 2324843
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 158
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 766.451
c starts	: 158
c conflicts	: 275
c decisions	: 71805
c propagations	: 126900
c inspects	: 2338690
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 159
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 770.464
c starts	: 159
c conflicts	: 275
c decisions	: 72251
c propagations	: 127675
c inspects	: 2352537
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 160
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 774.489
c starts	: 160
c conflicts	: 275
c decisions	: 72697
c propagations	: 128450
c inspects	: 2366384
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 161
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 778.497
c starts	: 161
c conflicts	: 275
c decisions	: 73143
c propagations	: 129225
c inspects	: 2380231
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 162
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 782.525
c starts	: 162
c conflicts	: 275
c decisions	: 73589
c propagations	: 130000
c inspects	: 2394078
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 163
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 786.528
c starts	: 163
c conflicts	: 275
c decisions	: 74035
c propagations	: 130775
c inspects	: 2407925
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 164
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 790.537
c starts	: 164
c conflicts	: 275
c decisions	: 74481
c propagations	: 131550
c inspects	: 2421772
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 165
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 794.533
c starts	: 165
c conflicts	: 275
c decisions	: 74927
c propagations	: 132325
c inspects	: 2435619
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 166
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 798.528
c starts	: 166
c conflicts	: 275
c decisions	: 75373
c propagations	: 133100
c inspects	: 2449466
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 167
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 802.552
c starts	: 167
c conflicts	: 275
c decisions	: 75819
c propagations	: 133875
c inspects	: 2463313
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 168
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 806.564
c starts	: 168
c conflicts	: 275
c decisions	: 76265
c propagations	: 134650
c inspects	: 2477160
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 169
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 810.602
c starts	: 169
c conflicts	: 275
c decisions	: 76711
c propagations	: 135425
c inspects	: 2491007
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 170
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 814.621
c starts	: 170
c conflicts	: 275
c decisions	: 77157
c propagations	: 136200
c inspects	: 2504854
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 171
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 818.661
c starts	: 171
c conflicts	: 275
c decisions	: 77603
c propagations	: 136975
c inspects	: 2518701
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 172
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 822.677
c starts	: 172
c conflicts	: 275
c decisions	: 78049
c propagations	: 137750
c inspects	: 2532548
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 173
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 826.711
c starts	: 173
c conflicts	: 275
c decisions	: 78495
c propagations	: 138525
c inspects	: 2546395
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 174
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 830.734
c starts	: 174
c conflicts	: 275
c decisions	: 78941
c propagations	: 139300
c inspects	: 2560242
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 175
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 834.772
c starts	: 175
c conflicts	: 275
c decisions	: 79387
c propagations	: 140075
c inspects	: 2574089
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 176
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 838.792
c starts	: 176
c conflicts	: 275
c decisions	: 79833
c propagations	: 140850
c inspects	: 2587936
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 177
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 842.828
c starts	: 177
c conflicts	: 275
c decisions	: 80279
c propagations	: 141625
c inspects	: 2601783
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 178
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 846.853
c starts	: 178
c conflicts	: 275
c decisions	: 80725
c propagations	: 142400
c inspects	: 2615630
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 179
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 850.895
c starts	: 179
c conflicts	: 275
c decisions	: 81171
c propagations	: 143175
c inspects	: 2629477
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 180
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 854.918
c starts	: 180
c conflicts	: 275
c decisions	: 81617
c propagations	: 143950
c inspects	: 2643324
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 181
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 858.935
c starts	: 181
c conflicts	: 275
c decisions	: 82063
c propagations	: 144725
c inspects	: 2657171
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 182
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 862.972
c starts	: 182
c conflicts	: 275
c decisions	: 82509
c propagations	: 145500
c inspects	: 2671018
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 183
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 866.988
c starts	: 183
c conflicts	: 275
c decisions	: 82955
c propagations	: 146275
c inspects	: 2684865
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 184
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 871.025
c starts	: 184
c conflicts	: 275
c decisions	: 83401
c propagations	: 147050
c inspects	: 2698712
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 185
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 875.043
c starts	: 185
c conflicts	: 275
c decisions	: 83847
c propagations	: 147825
c inspects	: 2712559
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 186
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 879.076
c starts	: 186
c conflicts	: 275
c decisions	: 84293
c propagations	: 148600
c inspects	: 2726406
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 187
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 883.09
c starts	: 187
c conflicts	: 275
c decisions	: 84739
c propagations	: 149375
c inspects	: 2740253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 188
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 887.125
c starts	: 188
c conflicts	: 275
c decisions	: 85185
c propagations	: 150150
c inspects	: 2754100
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 189
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 891.148
c starts	: 189
c conflicts	: 275
c decisions	: 85631
c propagations	: 150925
c inspects	: 2767947
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 190
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 895.195
c starts	: 190
c conflicts	: 275
c decisions	: 86077
c propagations	: 151700
c inspects	: 2781794
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 191
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 899.224
c starts	: 191
c conflicts	: 275
c decisions	: 86523
c propagations	: 152475
c inspects	: 2795641
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 192
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 903.273
c starts	: 192
c conflicts	: 275
c decisions	: 86969
c propagations	: 153250
c inspects	: 2809488
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 193
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 907.322
c starts	: 193
c conflicts	: 275
c decisions	: 87415
c propagations	: 154025
c inspects	: 2823335
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 194
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 911.372
c starts	: 194
c conflicts	: 275
c decisions	: 87861
c propagations	: 154800
c inspects	: 2837182
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 195
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 915.441
c starts	: 195
c conflicts	: 275
c decisions	: 88307
c propagations	: 155575
c inspects	: 2851029
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 196
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 919.487
c starts	: 196
c conflicts	: 275
c decisions	: 88753
c propagations	: 156350
c inspects	: 2864876
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 197
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 923.55
c starts	: 197
c conflicts	: 275
c decisions	: 89199
c propagations	: 157125
c inspects	: 2878723
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 198
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 927.586
c starts	: 198
c conflicts	: 275
c decisions	: 89645
c propagations	: 157900
c inspects	: 2892570
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 199
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 931.63
c starts	: 199
c conflicts	: 275
c decisions	: 90091
c propagations	: 158675
c inspects	: 2906417
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 200
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 935.668
c starts	: 200
c conflicts	: 275
c decisions	: 90537
c propagations	: 159450
c inspects	: 2920264
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 201
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 939.727
c starts	: 201
c conflicts	: 275
c decisions	: 90983
c propagations	: 160225
c inspects	: 2934111
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 202
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 943.776
c starts	: 202
c conflicts	: 275
c decisions	: 91429
c propagations	: 161000
c inspects	: 2947958
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 203
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 947.86
c starts	: 203
c conflicts	: 275
c decisions	: 91875
c propagations	: 161775
c inspects	: 2961805
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 204
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 951.921
c starts	: 204
c conflicts	: 275
c decisions	: 92321
c propagations	: 162550
c inspects	: 2975652
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 205
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 956.0
c starts	: 205
c conflicts	: 275
c decisions	: 92767
c propagations	: 163325
c inspects	: 2989499
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 206
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 960.086
c starts	: 206
c conflicts	: 275
c decisions	: 93213
c propagations	: 164100
c inspects	: 3003346
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 207
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 964.182
c starts	: 207
c conflicts	: 275
c decisions	: 93659
c propagations	: 164875
c inspects	: 3017193
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 208
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 968.258
c starts	: 208
c conflicts	: 275
c decisions	: 94105
c propagations	: 165650
c inspects	: 3031040
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 209
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 972.355
c starts	: 209
c conflicts	: 275
c decisions	: 94551
c propagations	: 166425
c inspects	: 3044887
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 210
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 976.404
c starts	: 210
c conflicts	: 275
c decisions	: 94997
c propagations	: 167200
c inspects	: 3058734
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 211
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 980.449
c starts	: 211
c conflicts	: 275
c decisions	: 95443
c propagations	: 167975
c inspects	: 3072581
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 212
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 984.519
c starts	: 212
c conflicts	: 275
c decisions	: 95889
c propagations	: 168750
c inspects	: 3086428
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 213
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 988.568
c starts	: 213
c conflicts	: 275
c decisions	: 96335
c propagations	: 169525
c inspects	: 3100275
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 214
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 992.627
c starts	: 214
c conflicts	: 275
c decisions	: 96781
c propagations	: 170300
c inspects	: 3114122
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 215
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 996.67
c starts	: 215
c conflicts	: 275
c decisions	: 97227
c propagations	: 171075
c inspects	: 3127969
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 216
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1000.724
c starts	: 216
c conflicts	: 275
c decisions	: 97673
c propagations	: 171850
c inspects	: 3141816
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 217
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1004.76
c starts	: 217
c conflicts	: 275
c decisions	: 98119
c propagations	: 172625
c inspects	: 3155663
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 218
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1008.811
c starts	: 218
c conflicts	: 275
c decisions	: 98565
c propagations	: 173400
c inspects	: 3169510
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 219
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1012.848
c starts	: 219
c conflicts	: 275
c decisions	: 99011
c propagations	: 174175
c inspects	: 3183357
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 220
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1016.899
c starts	: 220
c conflicts	: 275
c decisions	: 99457
c propagations	: 174950
c inspects	: 3197204
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 221
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1020.933
c starts	: 221
c conflicts	: 275
c decisions	: 99903
c propagations	: 175725
c inspects	: 3211051
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 222
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1024.975
c starts	: 222
c conflicts	: 275
c decisions	: 100349
c propagations	: 176500
c inspects	: 3224898
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 223
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1029.013
c starts	: 223
c conflicts	: 275
c decisions	: 100795
c propagations	: 177275
c inspects	: 3238745
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 224
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1033.049
c starts	: 224
c conflicts	: 275
c decisions	: 101241
c propagations	: 178050
c inspects	: 3252592
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 225
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1037.116
c starts	: 225
c conflicts	: 275
c decisions	: 101687
c propagations	: 178825
c inspects	: 3266439
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 226
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1041.182
c starts	: 226
c conflicts	: 275
c decisions	: 102133
c propagations	: 179600
c inspects	: 3280286
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 227
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1045.276
c starts	: 227
c conflicts	: 275
c decisions	: 102579
c propagations	: 180375
c inspects	: 3294133
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 228
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1049.349
c starts	: 228
c conflicts	: 275
c decisions	: 103025
c propagations	: 181150
c inspects	: 3307980
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 229
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1053.446
c starts	: 229
c conflicts	: 275
c decisions	: 103471
c propagations	: 181925
c inspects	: 3321827
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 230
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1057.524
c starts	: 230
c conflicts	: 275
c decisions	: 103917
c propagations	: 182700
c inspects	: 3335674
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 231
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1061.631
c starts	: 231
c conflicts	: 275
c decisions	: 104363
c propagations	: 183475
c inspects	: 3349521
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 232
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1065.72
c starts	: 232
c conflicts	: 275
c decisions	: 104809
c propagations	: 184250
c inspects	: 3363368
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 233
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1069.804
c starts	: 233
c conflicts	: 275
c decisions	: 105255
c propagations	: 185025
c inspects	: 3377215
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 234
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1073.853
c starts	: 234
c conflicts	: 275
c decisions	: 105701
c propagations	: 185800
c inspects	: 3391062
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 235
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1077.917
c starts	: 235
c conflicts	: 275
c decisions	: 106147
c propagations	: 186575
c inspects	: 3404909
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 236
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1081.959
c starts	: 236
c conflicts	: 275
c decisions	: 106593
c propagations	: 187350
c inspects	: 3418756
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 237
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1086.026
c starts	: 237
c conflicts	: 275
c decisions	: 107039
c propagations	: 188125
c inspects	: 3432603
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 238
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1090.089
c starts	: 238
c conflicts	: 275
c decisions	: 107485
c propagations	: 188900
c inspects	: 3446450
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 239
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1094.135
c starts	: 239
c conflicts	: 275
c decisions	: 107931
c propagations	: 189675
c inspects	: 3460297
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 240
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1098.204
c starts	: 240
c conflicts	: 275
c decisions	: 108377
c propagations	: 190450
c inspects	: 3474144
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 241
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1102.251
c starts	: 241
c conflicts	: 275
c decisions	: 108823
c propagations	: 191225
c inspects	: 3487991
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 242
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1106.322
c starts	: 242
c conflicts	: 275
c decisions	: 109269
c propagations	: 192000
c inspects	: 3501838
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 243
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1110.378
c starts	: 243
c conflicts	: 275
c decisions	: 109715
c propagations	: 192775
c inspects	: 3515685
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 244
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1114.446
c starts	: 244
c conflicts	: 275
c decisions	: 110161
c propagations	: 193550
c inspects	: 3529532
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 245
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1118.489
c starts	: 245
c conflicts	: 275
c decisions	: 110607
c propagations	: 194325
c inspects	: 3543379
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 246
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1122.532
c starts	: 246
c conflicts	: 275
c decisions	: 111053
c propagations	: 195100
c inspects	: 3557226
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 247
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1126.572
c starts	: 247
c conflicts	: 275
c decisions	: 111499
c propagations	: 195875
c inspects	: 3571073
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 248
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1130.621
c starts	: 248
c conflicts	: 275
c decisions	: 111945
c propagations	: 196650
c inspects	: 3584920
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 249
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1134.657
c starts	: 249
c conflicts	: 275
c decisions	: 112391
c propagations	: 197425
c inspects	: 3598767
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 250
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1138.709
c starts	: 250
c conflicts	: 275
c decisions	: 112837
c propagations	: 198200
c inspects	: 3612614
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 251
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1142.746
c starts	: 251
c conflicts	: 275
c decisions	: 113283
c propagations	: 198975
c inspects	: 3626461
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 252
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1146.815
c starts	: 252
c conflicts	: 275
c decisions	: 113729
c propagations	: 199750
c inspects	: 3640308
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 253
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1150.868
c starts	: 253
c conflicts	: 275
c decisions	: 114175
c propagations	: 200525
c inspects	: 3654155
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 254
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1154.92
c starts	: 254
c conflicts	: 275
c decisions	: 114621
c propagations	: 201300
c inspects	: 3668002
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 255
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1159.002
c starts	: 255
c conflicts	: 275
c decisions	: 115067
c propagations	: 202075
c inspects	: 3681849
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 256
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1163.059
c starts	: 256
c conflicts	: 275
c decisions	: 115513
c propagations	: 202850
c inspects	: 3695696
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 257
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1167.139
c starts	: 257
c conflicts	: 275
c decisions	: 115959
c propagations	: 203625
c inspects	: 3709543
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 258
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1171.198
c starts	: 258
c conflicts	: 275
c decisions	: 116405
c propagations	: 204400
c inspects	: 3723390
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 259
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1175.269
c starts	: 259
c conflicts	: 275
c decisions	: 116851
c propagations	: 205175
c inspects	: 3737237
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 260
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1179.325
c starts	: 260
c conflicts	: 275
c decisions	: 117297
c propagations	: 205950
c inspects	: 3751084
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 261
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1183.396
c starts	: 261
c conflicts	: 275
c decisions	: 117743
c propagations	: 206725
c inspects	: 3764931
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 262
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1187.443
c starts	: 262
c conflicts	: 275
c decisions	: 118189
c propagations	: 207500
c inspects	: 3778778
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 263
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1191.513
c starts	: 263
c conflicts	: 275
c decisions	: 118635
c propagations	: 208275
c inspects	: 3792625
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 264
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1195.564
c starts	: 264
c conflicts	: 275
c decisions	: 119081
c propagations	: 209050
c inspects	: 3806472
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 265
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1199.636
c starts	: 265
c conflicts	: 275
c decisions	: 119527
c propagations	: 209825
c inspects	: 3820319
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 266
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1203.697
c starts	: 266
c conflicts	: 275
c decisions	: 119973
c propagations	: 210600
c inspects	: 3834166
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 267
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1207.77
c starts	: 267
c conflicts	: 275
c decisions	: 120419
c propagations	: 211375
c inspects	: 3848013
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 268
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1211.835
c starts	: 268
c conflicts	: 275
c decisions	: 120865
c propagations	: 212150
c inspects	: 3861860
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 269
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1215.892
c starts	: 269
c conflicts	: 275
c decisions	: 121311
c propagations	: 212925
c inspects	: 3875707
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 270
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1219.961
c starts	: 270
c conflicts	: 275
c decisions	: 121757
c propagations	: 213700
c inspects	: 3889554
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 271
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1224.007
c starts	: 271
c conflicts	: 275
c decisions	: 122203
c propagations	: 214475
c inspects	: 3903401
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 272
c 
c CURRENT OPTIMUM=-328006904
c Current CPU time (ms) : 1228.072
c starts	: 272
c conflicts	: 275
c decisions	: 122649
c propagations	: 215250
c inspects	: 3917248
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 275
c root simplifications	: 273
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.96 0.92 2/54 23590
Raw data (stat): 23590 (runsolver) R 23589 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491381199 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0346 s]
Raw data (loadavg): 0.94 0.97 0.93 4/64 23600
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18071 0 1 0 686 40 0 0 25 0 11 0 491381199 860446720 21187 4294967295 134512640 134569956 3221224400 3221213732 1073952732 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210070 21187 13073 16 0 210054 0
vsize: 840280
[startup+20.057 s]
Raw data (loadavg): 1.26 1.04 0.95 2/64 23602
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18110 0 1 0 1541 41 0 0 25 0 11 0 491381199 867176448 23138 4294967295 134512640 134569956 3221224400 3221214776 1131332024 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211713 23138 13073 16 0 211697 0
vsize: 846852
[startup+30.058 s]
Raw data (loadavg): 1.22 1.04 0.95 2/64 23605
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 2455 41 0 0 25 0 11 0 491381199 865878016 23082 4294967295 134512640 134569956 3221224400 3221214776 1131330974 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211396 23082 13073 16 0 211380 0
vsize: 845584
[startup+40.0588 s]
Raw data (loadavg): 1.18 1.04 0.95 2/64 23607
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 3382 41 0 0 25 0 11 0 491381199 865026048 23573 4294967295 134512640 134569956 3221224400 3221214680 1131245167 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211188 23573 13073 16 0 211172 0
vsize: 844752
[startup+50.0594 s]
Raw data (loadavg): 1.15 1.03 0.95 2/64 23609
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 4351 42 0 0 25 0 11 0 491381199 867897344 24320 4294967295 134512640 134569956 3221224400 3221214640 1131252521 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211889 24320 13073 16 0 211873 0
vsize: 847556
[startup+60.06 s]
Raw data (loadavg): 1.13 1.03 0.95 2/64 23612
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 5321 42 0 0 25 0 11 0 491381199 866783232 24163 4294967295 134512640 134569956 3221224400 3221214680 1131244973 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211617 24163 13073 16 0 211601 0
vsize: 846468
[startup+70.0643 s]
Raw data (loadavg): 1.11 1.03 0.95 2/64 23614
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 6293 43 0 0 24 0 11 0 491381199 865456128 23908 4294967295 134512640 134569956 3221224400 3221214704 1131222655 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 23908 13073 16 0 211277 0
vsize: 845172
[startup+80.0689 s]
Raw data (loadavg): 1.09 1.03 0.95 2/64 23616
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 7263 43 0 0 25 0 11 0 491381199 865456128 24006 4294967295 134512640 134569956 3221224400 3221214664 1131245022 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 24006 13073 16 0 211277 0
vsize: 845172
[startup+90.0689 s]
Raw data (loadavg): 1.08 1.03 0.95 2/64 23618
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 8234 44 0 0 25 0 11 0 491381199 865456128 24112 4294967295 134512640 134569956 3221224400 3221214664 1131244973 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 24112 13073 16 0 211277 0
vsize: 845172
[startup+100.069 s]
Raw data (loadavg): 1.07 1.03 0.95 2/64 23618
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 9201 44 0 0 25 0 11 0 491381199 865456128 24233 4294967295 134512640 134569956 3221224400 3221214664 1131244877 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 24233 13073 16 0 211277 0
vsize: 845172
[startup+110.069 s]
Raw data (loadavg): 1.06 1.03 0.95 2/64 23620
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 10152 45 0 0 25 0 11 0 491381199 865456128 24413 4294967295 134512640 134569956 3221224400 3221214664 1131244604 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 24413 13073 16 0 211277 0
vsize: 845172
[startup+120.07 s]
Raw data (loadavg): 1.05 1.02 0.95 2/64 23622
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 11120 45 1 0 25 0 11 0 491381199 865456128 24507 4294967295 134512640 134569956 3221224400 3221214760 1131331039 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 24507 13073 16 0 211277 0
vsize: 845172
[startup+130.071 s]
Raw data (loadavg): 1.04 1.02 0.95 2/64 23623
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 12085 46 1 0 25 0 11 0 491381199 865456128 24702 4294967295 134512640 134569956 3221224400 3221214264 1131694061 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 24702 13073 16 0 211277 0
vsize: 845172
[startup+140.072 s]
Raw data (loadavg): 1.03 1.02 0.95 2/64 23624
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 13059 46 1 0 25 0 11 0 491381199 865456128 24821 4294967295 134512640 134569956 3221224400 3221214760 1131330940 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 24821 13073 16 0 211277 0
vsize: 845172
[startup+150.072 s]
Raw data (loadavg): 1.03 1.02 0.95 2/64 23625
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 14034 46 1 0 25 0 11 0 491381199 865456128 24936 4294967295 134512640 134569956 3221224400 3221214664 1131245723 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 24936 13073 16 0 211277 0
vsize: 845172
[startup+160.079 s]
Raw data (loadavg): 1.02 1.02 0.95 2/64 23627
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 15007 47 1 0 25 0 11 0 491381199 865456128 25021 4294967295 134512640 134569956 3221224400 3221214664 1131244632 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 25021 13073 16 0 211277 0
vsize: 845172
[startup+170.078 s]
Raw data (loadavg): 1.02 1.02 0.95 2/64 23629
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 15979 47 1 0 25 0 11 0 491381199 865456128 25114 4294967295 134512640 134569956 3221224400 3221214664 1131245153 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 25114 13073 16 0 211277 0
vsize: 845172
[startup+180.08 s]
Raw data (loadavg): 1.02 1.02 0.95 2/64 23631
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 16954 48 1 0 25 0 11 0 491381199 865456128 25262 4294967295 134512640 134569956 3221224400 3221214664 1131244549 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 25262 13073 16 0 211277 0
vsize: 845172
[startup+190.087 s]
Raw data (loadavg): 1.01 1.02 0.95 2/64 23633
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 17933 48 1 0 25 0 11 0 491381199 865456128 25373 4294967295 134512640 134569956 3221224400 3221214664 1131244541 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 25373 13073 16 0 211277 0
vsize: 845172
[startup+200.087 s]
Raw data (loadavg): 1.01 1.02 0.95 2/64 23635
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 18913 49 1 0 25 0 11 0 491381199 865456128 25490 4294967295 134512640 134569956 3221224400 3221214544 1131787382 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 25490 13073 16 0 211277 0
vsize: 845172
[startup+210.087 s]
Raw data (loadavg): 1.01 1.02 0.95 2/64 23637
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 19896 49 1 0 25 0 11 0 491381199 865456128 25631 4294967295 134512640 134569956 3221224400 3221214664 1131245705 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 25631 13073 16 0 211277 0
vsize: 845172
[startup+220.088 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 23639
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 20880 49 1 0 25 0 11 0 491381199 865456128 25761 4294967295 134512640 134569956 3221224400 3221214664 1131245109 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 25761 13073 16 0 211277 0
vsize: 845172
[startup+230.089 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 23641
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 21866 50 1 0 25 0 11 0 491381199 865456128 25836 4294967295 134512640 134569956 3221224400 3221214664 1131244545 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 25836 13073 16 0 211277 0
vsize: 845172
[startup+240.089 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 23643
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 22852 50 1 0 25 0 11 0 491381199 865456128 25895 4294967295 134512640 134569956 3221224400 3221214664 1131245748 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 25895 13073 16 0 211277 0
vsize: 845172
[startup+250.089 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 23645
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 23837 51 1 0 25 0 11 0 491381199 865456128 25972 4294967295 134512640 134569956 3221224400 3221214448 1131786286 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 25972 13073 16 0 211277 0
vsize: 845172
[startup+260.09 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 23647
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 24822 51 2 0 25 0 11 0 491381199 865456128 26052 4294967295 134512640 134569956 3221224400 3221214664 1131245121 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 26052 13073 16 0 211277 0
vsize: 845172
[startup+270.09 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 23649
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 25806 51 2 0 25 0 11 0 491381199 865456128 26126 4294967295 134512640 134569956 3221224400 3221214664 1131244589 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 26126 13073 16 0 211277 0
vsize: 845172
[startup+280.091 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 23651
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 26786 52 2 0 25 0 11 0 491381199 865456128 26227 4294967295 134512640 134569956 3221224400 3221214664 1131245492 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 26227 13073 16 0 211277 0
vsize: 845172
[startup+290.092 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 23653
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 27768 53 2 0 25 0 11 0 491381199 865456128 26329 4294967295 134512640 134569956 3221224400 3221214664 1131244621 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 26329 13073 16 0 211277 0
vsize: 845172
[startup+300.092 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 23655
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 28749 53 2 0 25 0 11 0 491381199 865456128 26438 4294967295 134512640 134569956 3221224400 3221214760 1131334557 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 26438 13073 16 0 211277 0
vsize: 845172
[startup+310.093 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 23657
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 29732 53 2 0 25 0 11 0 491381199 865456128 26547 4294967295 134512640 134569956 3221224400 3221214300 1131692688 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 26547 13073 16 0 211277 0
vsize: 845172
[startup+320.093 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23661
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 30713 54 2 0 25 0 11 0 491381199 865456128 26693 4294967295 134512640 134569956 3221224400 3221214760 1131332046 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 26693 13073 16 0 211277 0
vsize: 845172
[startup+330.094 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23663
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 31694 55 2 0 25 0 11 0 491381199 865456128 26812 4294967295 134512640 134569956 3221224400 3221214448 1131789293 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 26812 13073 16 0 211277 0
vsize: 845172
[startup+340.095 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23666
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 32675 55 2 0 25 0 11 0 491381199 865456128 26868 4294967295 134512640 134569956 3221224400 3221214756 1131246015 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 26868 13073 16 0 211277 0
vsize: 845172
[startup+350.095 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23668
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 33654 56 2 0 25 0 11 0 491381199 865456128 27041 4294967295 134512640 134569956 3221224400 3221214760 1131331036 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27041 13073 16 0 211277 0
vsize: 845172
[startup+360.096 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23670
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 34637 56 2 0 25 0 11 0 491381199 865456128 27150 4294967295 134512640 134569956 3221224400 3221214664 1131245203 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27150 13073 16 0 211277 0
vsize: 845172
[startup+370.097 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23672
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 35621 56 2 0 25 0 11 0 491381199 865456128 27314 4294967295 134512640 134569956 3221224400 3221214460 1131763712 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27314 13073 16 0 211277 0
vsize: 845172
[startup+380.097 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23674
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 36606 57 2 0 25 0 11 0 491381199 865456128 27401 4294967295 134512640 134569956 3221224400 3221214664 1131244918 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27401 13073 16 0 211277 0
vsize: 845172
[startup+390.098 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23676
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 37592 57 2 0 25 0 11 0 491381199 865456128 27484 4294967295 134512640 134569956 3221224400 3221214760 1131331936 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27484 13073 16 0 211277 0
vsize: 845172
[startup+400.098 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23678
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 38579 57 2 0 25 0 11 0 491381199 865456128 27529 4294967295 134512640 134569956 3221224400 3221214756 1131246015 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27529 13073 16 0 211277 0
vsize: 845172
[startup+410.099 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23680
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 39565 58 3 1 25 0 11 0 491381199 865456128 27606 4294967295 134512640 134569956 3221224400 3221214664 1131245129 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27606 13073 16 0 211277 0
vsize: 845172
[startup+420.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23682
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 40550 58 3 1 25 0 11 0 491381199 865456128 27687 4294967295 134512640 134569956 3221224400 3221214736 1131786440 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27687 13073 16 0 211277 0
vsize: 845172
[startup+430.102 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23684
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 41535 59 3 1 25 0 11 0 491381199 865456128 27742 4294967295 134512640 134569956 3221224400 3221214664 1131244638 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27742 13073 16 0 211277 0
vsize: 845172
[startup+440.102 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23686
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 42519 60 3 1 25 0 11 0 491381199 865456128 27822 4294967295 134512640 134569956 3221224400 3221214664 1131244927 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27822 13073 16 0 211277 0
vsize: 845172
[startup+450.103 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23688
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 43503 61 3 1 25 0 11 0 491381199 865456128 27866 4294967295 134512640 134569956 3221224400 3221214744 1131788409 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27866 13073 16 0 211277 0
vsize: 845172
[startup+460.103 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23690
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 44487 61 3 1 25 0 11 0 491381199 865456128 28009 4294967295 134512640 134569956 3221224400 3221214664 1131245207 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28009 13073 16 0 211277 0
vsize: 845172
[startup+470.104 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23692
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 45469 61 3 1 25 0 11 0 491381199 865456128 28071 4294967295 134512640 134569956 3221224400 3221214760 1131330967 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28071 13073 16 0 211277 0
vsize: 845172
[startup+480.106 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23694
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 46453 62 3 1 25 0 11 0 491381199 865456128 28165 4294967295 134512640 134569956 3221224400 3221214760 1131332039 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28165 13073 16 0 211277 0
vsize: 845172
[startup+490.106 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23696
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 47435 62 4 1 25 0 11 0 491381199 865456128 28278 4294967295 134512640 134569956 3221224400 3221214760 1131334553 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28278 13073 16 0 211277 0
vsize: 845172
[startup+500.107 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23698
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 48415 62 4 1 25 0 11 0 491381199 865456128 28372 4294967295 134512640 134569956 3221224400 3221214664 1131245821 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28372 13073 16 0 211277 0
vsize: 845172
[startup+510.107 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23700
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 49392 63 4 1 25 0 11 0 491381199 865456128 28452 4294967295 134512640 134569956 3221224400 3221214464 1131694208 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28452 13073 16 0 211277 0
vsize: 845172
[startup+520.108 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23703
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 50371 64 4 1 25 0 11 0 491381199 865456128 28662 4294967295 134512640 134569956 3221224400 3221214664 1131245773 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28662 13073 16 0 211277 0
vsize: 845172
[startup+530.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23705
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 51353 64 4 1 25 0 11 0 491381199 865456128 28822 4294967295 134512640 134569956 3221224400 3221214664 1131245434 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28822 13073 16 0 211277 0
vsize: 845172
[startup+540.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23707
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 52334 64 4 1 25 0 11 0 491381199 865456128 28980 4294967295 134512640 134569956 3221224400 3221214760 1131332108 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28980 13073 16 0 211277 0
vsize: 845172
[startup+550.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23709
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 53318 65 4 1 25 0 11 0 491381199 865456128 29067 4294967295 134512640 134569956 3221224400 3221214664 1131244927 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29067 13073 16 0 211277 0
vsize: 845172
[startup+560.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23711
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 54301 65 5 1 25 0 11 0 491381199 865456128 29160 4294967295 134512640 134569956 3221224400 3221214760 1131330974 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29160 13073 16 0 211277 0
vsize: 845172
[startup+570.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23713
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 55285 66 5 1 25 0 11 0 491381199 865456128 29264 4294967295 134512640 134569956 3221224400 3221214664 1131244973 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29264 13073 16 0 211277 0
vsize: 845172
[startup+580.113 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23715
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 56267 66 5 1 25 0 11 0 491381199 865456128 29359 4294967295 134512640 134569956 3221224400 3221214664 1131244973 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29359 13073 16 0 211277 0
vsize: 845172
[startup+590.114 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23717
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 57246 66 5 1 25 0 11 0 491381199 865456128 29463 4294967295 134512640 134569956 3221224400 3221214664 1131244973 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29463 13073 16 0 211277 0
vsize: 845172
[startup+600.114 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23720
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 58222 67 5 1 25 0 11 0 491381199 865456128 29580 4294967295 134512640 134569956 3221224400 3221214664 1131244632 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29580 13073 16 0 211277 0
vsize: 845172
[startup+610.114 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23722
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 59198 67 5 1 25 0 11 0 491381199 865456128 29671 4294967295 134512640 134569956 3221224400 3221214760 1131330974 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29671 13073 16 0 211277 0
vsize: 845172
[startup+620.115 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23725
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 60175 68 5 1 25 0 11 0 491381199 865456128 29932 4294967295 134512640 134569956 3221224400 3221214664 1131245998 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29932 13073 16 0 211277 0
vsize: 845172
[startup+630.115 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23727
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 61155 68 5 1 25 0 11 0 491381199 865456128 30047 4294967295 134512640 134569956 3221224400 3221214664 1131244664 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30047 13073 16 0 211277 0
vsize: 845172
[startup+640.116 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23730
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 62135 69 5 2 25 0 11 0 491381199 865456128 30199 4294967295 134512640 134569956 3221224400 3221214664 1131245175 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30199 13073 16 0 211277 0
vsize: 845172
[startup+650.116 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23732
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 63118 69 5 2 25 0 11 0 491381199 865456128 30296 4294967295 134512640 134569956 3221224400 3221214664 1131244638 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30296 13073 16 0 211277 0
vsize: 845172
[startup+660.116 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23735
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 64098 70 5 2 24 0 11 0 491381199 865456128 30412 4294967295 134512640 134569956 3221224400 3221214664 1131244577 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30412 13073 16 0 211277 0
vsize: 845172
[startup+670.117 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23737
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 65078 70 5 2 25 0 11 0 491381199 865456128 30482 4294967295 134512640 134569956 3221224400 3221214664 1131244973 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30482 13073 16 0 211277 0
vsize: 845172
[startup+680.117 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23740
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 66058 71 6 2 25 0 11 0 491381199 865456128 30590 4294967295 134512640 134569956 3221224400 3221214664 1131245809 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30590 13073 16 0 211277 0
vsize: 845172
[startup+690.118 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23742
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 67039 72 6 2 25 0 11 0 491381199 865456128 30758 4294967295 134512640 134569956 3221224400 3221214664 1131244973 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30758 13073 16 0 211277 0
vsize: 845172
[startup+700.118 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23745
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 68022 73 6 2 25 0 11 0 491381199 865456128 30843 4294967295 134512640 134569956 3221224400 3221214760 1131330974 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30843 13073 16 0 211277 0
vsize: 845172
[startup+710.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23747
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 69004 73 6 2 25 0 11 0 491381199 865456128 30931 4294967295 134512640 134569956 3221224400 3221214664 1131244632 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30931 13073 16 0 211277 0
vsize: 845172
[startup+720.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23750
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 69985 74 6 2 25 0 11 0 491381199 865456128 30991 4294967295 134512640 134569956 3221224400 3221214664 1131244925 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30991 13073 16 0 211277 0
vsize: 845172
[startup+730.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23752
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 70966 75 6 2 25 0 11 0 491381199 865456128 31122 4294967295 134512640 134569956 3221224400 3221214760 1131332002 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 31122 13073 16 0 211277 0
vsize: 845172
[startup+740.121 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23755
Raw data (stat): 23590 (java) S 23589 22932 22931 0 -1 0 18111 3 1 0 71945 75 6 2 25 0 11 0 491381199 865456128 31193 4294967295 134512640 134569956 3221224400 3221213264 1073952481 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 31193 13073 16 0 211277 0
vsize: 845172
[startup+750.121 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23757
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 72921 76 6 2 25 0 11 0 491381199 865456128 31282 4294967295 134512640 134569956 3221224400 3221214664 1131245858 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 31282 13073 16 0 211277 0
vsize: 845172
[startup+760.121 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23760
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 73898 76 7 2 25 0 11 0 491381199 865456128 31468 4294967295 134512640 134569956 3221224400 3221214664 1131245856 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 31468 13073 16 0 211277 0
vsize: 845172
[startup+770.122 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23762
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 74877 76 7 2 25 0 11 0 491381199 865456128 31620 4294967295 134512640 134569956 3221224400 3221214664 1131245807 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 31620 13073 16 0 211277 0
vsize: 845172
[startup+780.124 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23765
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 75857 77 7 2 25 0 11 0 491381199 865456128 31663 4294967295 134512640 134569956 3221224400 3221214760 1131332002 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 31663 13073 16 0 211277 0
vsize: 845172
[startup+790.124 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23767
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 76840 77 7 2 25 0 11 0 491381199 865456128 31900 4294967295 134512640 134569956 3221224400 3221214760 1131334855 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 31900 13073 16 0 211277 0
vsize: 845172
[startup+800.125 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23770
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 77823 78 7 2 25 0 11 0 491381199 865456128 31966 4294967295 134512640 134569956 3221224400 3221214760 1131334882 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 31966 13073 16 0 211277 0
vsize: 845172
[startup+810.126 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23772
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 78804 78 7 2 25 0 11 0 491381199 865456128 31994 4294967295 134512640 134569956 3221224400 3221214760 1131332088 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 31994 13073 16 0 211277 0
vsize: 845172
[startup+820.127 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23775
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 79783 78 8 2 25 0 11 0 491381199 865456128 32106 4294967295 134512640 134569956 3221224400 3221214664 1131244601 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 32106 13073 16 0 211277 0
vsize: 845172
[startup+830.128 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23777
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 80762 78 8 2 25 0 11 0 491381199 865456128 32234 4294967295 134512640 134569956 3221224400 3221214760 1131334844 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 32234 13073 16 0 211277 0
vsize: 845172
[startup+840.128 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23780
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 81738 79 8 2 24 0 11 0 491381199 865456128 32415 4294967295 134512640 134569956 3221224400 3221214664 1131245098 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 32415 13073 16 0 211277 0
vsize: 845172
[startup+850.129 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23782
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 82716 79 8 3 25 0 11 0 491381199 865456128 32529 4294967295 134512640 134569956 3221224400 3221214664 1131244621 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 32529 13073 16 0 211277 0
vsize: 845172
[startup+860.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23785
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 83694 80 8 3 25 0 11 0 491381199 865456128 32616 4294967295 134512640 134569956 3221224400 3221214760 1131334790 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 32616 13073 16 0 211277 0
vsize: 845172
[startup+870.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23787
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 84673 80 8 3 25 0 11 0 491381199 865456128 32797 4294967295 134512640 134569956 3221224400 3221214760 1131332024 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 32797 13073 16 0 211277 0
vsize: 845172
[startup+880.131 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23790
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 85653 81 8 3 25 0 11 0 491381199 865456128 32922 4294967295 134512640 134569956 3221224400 3221214664 1131245800 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 32922 13073 16 0 211277 0
vsize: 845172
[startup+890.132 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23792
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 86632 81 8 3 25 0 11 0 491381199 865456128 33030 4294967295 134512640 134569956 3221224400 3221214664 1131244695 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 33030 13073 16 0 211277 0
vsize: 845172
[startup+900.132 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23794
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 87609 82 8 3 25 0 11 0 491381199 865456128 33178 4294967295 134512640 134569956 3221224400 3221214776 1131485148 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 33178 13073 16 0 211277 0
vsize: 845172
[startup+910.133 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23797
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 88587 83 8 3 25 0 11 0 491381199 865456128 33252 4294967295 134512640 134569956 3221224400 3221214664 1131244927 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 33252 13073 16 0 211277 0
vsize: 845172
[startup+920.133 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23799
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 89567 83 8 3 25 0 11 0 491381199 865456128 33419 4294967295 134512640 134569956 3221224400 3221214664 1131245129 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 33419 13073 16 0 211277 0
vsize: 845172
[startup+930.134 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23802
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 90548 83 9 3 25 0 11 0 491381199 865456128 33581 4294967295 134512640 134569956 3221224400 3221214664 1131244537 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 33581 13073 16 0 211277 0
vsize: 845172
[startup+940.134 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23804
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 91530 84 9 3 25 0 11 0 491381199 865456128 33644 4294967295 134512640 134569956 3221224400 3221214760 1131332039 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 33644 13073 16 0 211277 0
vsize: 845172
[startup+950.138 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23807
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 92509 84 9 3 25 0 11 0 491381199 865456128 33771 4294967295 134512640 134569956 3221224400 3221214664 1131245809 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 33771 13073 16 0 211277 0
vsize: 845172
[startup+960.139 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23809
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 93484 84 9 3 25 0 11 0 491381199 865456128 33818 4294967295 134512640 134569956 3221224400 3221214664 1131244747 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 33818 13073 16 0 211277 0
vsize: 845172
[startup+970.139 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23812
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 94456 84 9 3 25 0 11 0 491381199 865456128 33932 4294967295 134512640 134569956 3221224400 3221214760 1131330959 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 33932 13073 16 0 211277 0
vsize: 845172
[startup+980.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23814
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 95433 85 9 3 25 0 11 0 491381199 865456128 34237 4294967295 134512640 134569956 3221224400 3221214664 1131244973 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 34237 13073 16 0 211277 0
vsize: 845172
[startup+990.147 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23817
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 96414 85 9 3 25 0 11 0 491381199 865456128 34445 4294967295 134512640 134569956 3221224400 3221214760 1131335016 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 34445 13073 16 0 211277 0
vsize: 845172
[startup+1000.18 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23819
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 97398 85 9 3 25 0 11 0 491381199 865456128 34520 4294967295 134512640 134569956 3221224400 3221214760 1131332983 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 34520 13073 16 0 211277 0
vsize: 845172
[startup+1010.18 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23822
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 98381 85 9 3 25 0 11 0 491381199 865456128 34610 4294967295 134512640 134569956 3221224400 3221214664 1131245713 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 34610 13073 16 0 211277 0
vsize: 845172
[startup+1020.19 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23824
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 99365 86 9 3 25 0 11 0 491381199 865456128 34733 4294967295 134512640 134569956 3221224400 3221214664 1131244545 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 34733 13073 16 0 211277 0
vsize: 845172
[startup+1030.3 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23827
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 100360 86 9 3 25 0 11 0 491381199 865456128 34797 4294967295 134512640 134569956 3221224400 3221214760 1131330974 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 34797 13073 16 0 211277 0
vsize: 845172
[startup+1040.3 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23829
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 101341 86 10 3 25 0 11 0 491381199 865456128 34863 4294967295 134512640 134569956 3221224400 3221214664 1131244877 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 34863 13073 16 0 211277 0
vsize: 845172
[startup+1050.3 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23832
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 102315 86 10 3 25 0 11 0 491381199 865456128 34954 4294967295 134512640 134569956 3221224400 3221214768 1131317568 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 34954 13073 16 0 211277 0
vsize: 845172
[startup+1060.3 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23834
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18111 3 1 0 103287 87 10 4 25 0 11 0 491381199 865456128 35045 4294967295 134512640 134569956 3221224400 3221214664 1131245049 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 35045 13073 16 0 211277 0
vsize: 845172
[startup+1070.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23836
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 104259 87 10 4 25 0 11 0 491381199 865456128 35416 4294967295 134512640 134569956 3221224400 3221214664 1131244973 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 35416 13073 16 0 211277 0
vsize: 845172
[startup+1080.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23839
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 105239 87 10 4 25 0 11 0 491381199 865456128 35536 4294967295 134512640 134569956 3221224400 3221214760 1131331910 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 35536 13073 16 0 211277 0
vsize: 845172
[startup+1090.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23841
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 106219 87 10 4 25 0 11 0 491381199 865456128 35731 4294967295 134512640 134569956 3221224400 3221214760 1131332208 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 35731 13073 16 0 211277 0
vsize: 845172
[startup+1100.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23844
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 107199 88 10 4 25 0 11 0 491381199 865456128 35794 4294967295 134512640 134569956 3221224400 3221214760 1131334859 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 35794 13073 16 0 211277 0
vsize: 845172
[startup+1110.31 s]
Raw data (loadavg): 1.00 1.00 0.95 3/64 23846
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 108178 88 10 4 25 0 11 0 491381199 865456128 35840 4294967295 134512640 134569956 3221224400 3221214760 1131330936 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 35840 13073 16 0 211277 0
vsize: 845172
[startup+1120.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23849
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 109158 88 11 4 25 0 11 0 491381199 865456128 36106 4294967295 134512640 134569956 3221224400 3221214760 1131330974 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 36106 13073 16 0 211277 0
vsize: 845172
[startup+1130.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23851
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 110143 88 11 4 25 0 11 0 491381199 865456128 36133 4294967295 134512640 134569956 3221224400 3221214664 1131245748 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 36133 13073 16 0 211277 0
vsize: 845172
[startup+1140.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23854
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 111127 88 11 4 25 0 11 0 491381199 865456128 36242 4294967295 134512640 134569956 3221224400 3221214664 1131244582 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 36242 13073 16 0 211277 0
vsize: 845172
[startup+1150.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23856
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 112108 88 11 4 25 0 11 0 491381199 865456128 36281 4294967295 134512640 134569956 3221224400 3221214664 1131245203 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 36281 13073 16 0 211277 0
vsize: 845172
[startup+1160.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23859
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 113086 89 11 4 25 0 11 0 491381199 865456128 36393 4294967295 134512640 134569956 3221224400 3221214760 1131332178 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 36393 13073 16 0 211277 0
vsize: 845172
[startup+1170.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23861
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 114064 89 11 4 25 0 11 0 491381199 865456128 36501 4294967295 134512640 134569956 3221224400 3221214664 1131244973 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 36501 13073 16 0 211277 0
vsize: 845172
[startup+1180.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23864
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 115043 89 11 4 25 0 11 0 491381199 865456128 36619 4294967295 134512640 134569956 3221224400 3221214664 1131245828 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 36619 13073 16 0 211277 0
vsize: 845172
[startup+1190.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23866
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 116023 89 11 4 25 0 11 0 491381199 865456128 36810 4294967295 134512640 134569956 3221224400 3221214760 1131334928 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 36810 13073 16 0 211277 0
vsize: 845172
[startup+1200.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23868
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 117003 89 11 4 25 0 11 0 491381199 865456128 36903 4294967295 134512640 134569956 3221224400 3221214664 1131244644 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 36903 13073 16 0 211277 0
vsize: 845172
[startup+1210.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23871
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 117981 90 12 4 25 0 11 0 491381199 865456128 37006 4294967295 134512640 134569956 3221224400 3221214664 1131245004 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 37006 13073 16 0 211277 0
vsize: 845172
[startup+1220.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23873
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 118959 90 12 4 25 0 11 0 491381199 865456128 37131 4294967295 134512640 134569956 3221224400 3221214760 1131332002 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 37131 13073 16 0 211277 0
vsize: 845172
[startup+1230.31 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 23876
Raw data (stat): 23590 (java) R 23589 22932 22931 0 -1 0 18112 3 1 0 119940 90 12 4 25 0 11 0 491381199 865456128 37298 4294967295 134512640 134569956 3221224400 3221214664 1131245145 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 37298 13073 16 0 211277 0
vsize: 845172
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1230.4 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 23878
Raw data (stat): 23590 (java) Z 23589 22932 22931 0 -1 1036 18112 21662 1 1 119942 90 3623 72 25 0 1 0 491381199 0 0 4294967295 0 0 0 0 0 0 4 3 23756 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 143
Real time (s): 1230.4
CPU time (s): 1237.28
CPU user time (s): 1235.65
CPU system time (s): 1.62775
CPU usage (%): 100.559
Max. virtual memory (Kb): 847556
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####