PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core4872-1529.opb
MD5SUM	7eea141e02c7a2753145fd63f1e9087d
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	24865
Biggest coefficient in the objective function	52428800000000000
Number of bits for the biggest coefficient in the objective function	56
Sum of the numbers in the objective function	226690477012582900
Number of bits of the sum of numbers in the objective function	58
Biggest number in a constraint	1280000000000000000000
Number of bits of the biggest number in a constraint	71
Biggest sum of numbers in a constraint	1280226690477012549632
Number of bits of the biggest sum of numbers	71
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	41.1118
Number of variables	24865
Total number of constraints	29520
Number of constraints which are clauses	4872
Number of constraints which are cardinality constraints (but not clauses)	24647
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	24865
Trace number 14427

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-20 23:48:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20068 boxname=wulflinc19 idbench=1544 idsolver=9 numberseed=0
MD5SUM SOLVER: daf345f6fbf228671abfac48013b9cac  /oldhome/oroussel/solvers/sat4jPseudo.jar
MD5SUM BENCH:  7eea141e02c7a2753145fd63f1e9087d  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-core4872-1529.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudo.jar /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-core4872-1529.opb
IDLAUNCH: 20068
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        613064 kB
Buffers:         34560 kB
Cached:         353060 kB
SwapCached:        660 kB
Active:         105440 kB
Inactive:       284416 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        612812 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            26092 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 00:08:58 (client local time) WITH STATUS 1 IN 1225.69 SECONDS
stats: 20068 7 1225.69 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-core4872-1529.opb
c reading problem 
c [nbvar=24865]
c [nbconstr=29520]
c time 195.409
c #vars     24865
c #clauses  4875
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=817168384
c Current CPU time (ms) : 210.15
c starts	: 1
c conflicts	: 0
c decisions	: 23529
c propagations	: 24865
c inspects	: 38731
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 1
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 210.643
c starts	: 2
c conflicts	: 0
c decisions	: 47058
c propagations	: 49679
c inspects	: 42153
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 2
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 211.343
c starts	: 3
c conflicts	: 0
c decisions	: 70587
c propagations	: 74493
c inspects	: 44969
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 3
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 211.821
c starts	: 4
c conflicts	: 0
c decisions	: 94116
c propagations	: 99307
c inspects	: 47774
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 4
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 212.312
c starts	: 5
c conflicts	: 0
c decisions	: 117645
c propagations	: 124121
c inspects	: 50590
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 5
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 212.798
c starts	: 6
c conflicts	: 0
c decisions	: 141174
c propagations	: 148935
c inspects	: 53406
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 6
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 213.673
c starts	: 7
c conflicts	: 0
c decisions	: 164703
c propagations	: 173749
c inspects	: 56211
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 7
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 214.165
c starts	: 8
c conflicts	: 0
c decisions	: 188232
c propagations	: 198563
c inspects	: 59027
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 8
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 214.673
c starts	: 9
c conflicts	: 0
c decisions	: 211761
c propagations	: 223377
c inspects	: 61843
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 9
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 215.169
c starts	: 10
c conflicts	: 0
c decisions	: 235290
c propagations	: 248191
c inspects	: 64659
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 10
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 216.098
c starts	: 11
c conflicts	: 0
c decisions	: 258819
c propagations	: 273005
c inspects	: 67475
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 11
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 216.603
c starts	: 12
c conflicts	: 0
c decisions	: 282348
c propagations	: 297819
c inspects	: 70280
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 12
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 217.112
c starts	: 13
c conflicts	: 0
c decisions	: 305877
c propagations	: 322633
c inspects	: 73096
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 13
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 218.008
c starts	: 14
c conflicts	: 0
c decisions	: 329406
c propagations	: 347447
c inspects	: 75912
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 14
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 218.525
c starts	: 15
c conflicts	: 0
c decisions	: 352935
c propagations	: 372261
c inspects	: 78728
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 15
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 219.046
c starts	: 16
c conflicts	: 0
c decisions	: 376464
c propagations	: 397075
c inspects	: 81544
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 16
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 219.594
c starts	: 17
c conflicts	: 0
c decisions	: 399993
c propagations	: 421889
c inspects	: 84360
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 17
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 220.594
c starts	: 18
c conflicts	: 0
c decisions	: 423522
c propagations	: 446703
c inspects	: 87176
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 18
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 221.128
c starts	: 19
c conflicts	: 0
c decisions	: 447051
c propagations	: 471517
c inspects	: 89992
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 19
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 221.662
c starts	: 20
c conflicts	: 0
c decisions	: 470580
c propagations	: 496331
c inspects	: 92796
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 20
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 222.199
c starts	: 21
c conflicts	: 0
c decisions	: 494109
c propagations	: 521145
c inspects	: 95612
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 21
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 223.051
c starts	: 22
c conflicts	: 0
c decisions	: 517638
c propagations	: 545959
c inspects	: 98417
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 22
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 223.595
c starts	: 23
c conflicts	: 0
c decisions	: 541167
c propagations	: 570773
c inspects	: 101223
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 23
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 224.143
c starts	: 24
c conflicts	: 0
c decisions	: 564696
c propagations	: 595587
c inspects	: 104039
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 24
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 224.7
c starts	: 25
c conflicts	: 0
c decisions	: 588225
c propagations	: 620401
c inspects	: 106855
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 25
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 225.683
c starts	: 26
c conflicts	: 0
c decisions	: 611754
c propagations	: 645215
c inspects	: 109671
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 26
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 226.245
c starts	: 27
c conflicts	: 0
c decisions	: 635283
c propagations	: 670029
c inspects	: 112475
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 27
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 226.809
c starts	: 28
c conflicts	: 0
c decisions	: 658812
c propagations	: 694843
c inspects	: 115291
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 28
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 227.807
c starts	: 29
c conflicts	: 0
c decisions	: 682341
c propagations	: 719657
c inspects	: 118107
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 29
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 228.38
c starts	: 30
c conflicts	: 0
c decisions	: 705870
c propagations	: 744471
c inspects	: 120923
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 30
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 228.96
c starts	: 31
c conflicts	: 0
c decisions	: 729399
c propagations	: 769285
c inspects	: 123739
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 31
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 229.541
c starts	: 32
c conflicts	: 0
c decisions	: 752928
c propagations	: 794099
c inspects	: 126555
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 32
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 230.642
c starts	: 33
c conflicts	: 0
c decisions	: 776457
c propagations	: 818913
c inspects	: 129371
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 33
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 231.23
c starts	: 34
c conflicts	: 0
c decisions	: 799986
c propagations	: 843727
c inspects	: 132187
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 34
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 231.82
c starts	: 35
c conflicts	: 0
c decisions	: 823515
c propagations	: 868541
c inspects	: 134992
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 35
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 232.415
c starts	: 36
c conflicts	: 0
c decisions	: 847044
c propagations	: 893355
c inspects	: 137808
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 36
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 233.311
c starts	: 37
c conflicts	: 0
c decisions	: 870573
c propagations	: 918169
c inspects	: 140617
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 37
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 233.912
c starts	: 38
c conflicts	: 0
c decisions	: 894102
c propagations	: 942983
c inspects	: 143422
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 38
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 234.517
c starts	: 39
c conflicts	: 0
c decisions	: 917631
c propagations	: 967797
c inspects	: 146238
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 39
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 235.55
c starts	: 40
c conflicts	: 0
c decisions	: 941160
c propagations	: 992611
c inspects	: 149054
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 40
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 236.166
c starts	: 41
c conflicts	: 0
c decisions	: 964689
c propagations	: 1017425
c inspects	: 151870
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 41
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 236.785
c starts	: 42
c conflicts	: 0
c decisions	: 988218
c propagations	: 1042239
c inspects	: 154679
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 42
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 237.407
c starts	: 43
c conflicts	: 0
c decisions	: 1011747
c propagations	: 1067053
c inspects	: 157495
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 43
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 238.463
c starts	: 44
c conflicts	: 0
c decisions	: 1035276
c propagations	: 1091867
c inspects	: 160300
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 44
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 239.091
c starts	: 45
c conflicts	: 0
c decisions	: 1058805
c propagations	: 1116681
c inspects	: 163105
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 45
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 239.724
c starts	: 46
c conflicts	: 0
c decisions	: 1082334
c propagations	: 1141495
c inspects	: 165921
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 46
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 240.359
c starts	: 47
c conflicts	: 0
c decisions	: 1105863
c propagations	: 1166309
c inspects	: 168733
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 47
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 241.373
c starts	: 48
c conflicts	: 0
c decisions	: 1129392
c propagations	: 1191123
c inspects	: 171549
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 48
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 242.019
c starts	: 49
c conflicts	: 0
c decisions	: 1152921
c propagations	: 1215937
c inspects	: 174365
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 49
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 242.673
c starts	: 50
c conflicts	: 0
c decisions	: 1176450
c propagations	: 1240751
c inspects	: 177181
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 50
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 243.323
c starts	: 51
c conflicts	: 0
c decisions	: 1199979
c propagations	: 1265565
c inspects	: 179997
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 51
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 244.418
c starts	: 52
c conflicts	: 0
c decisions	: 1223508
c propagations	: 1290379
c inspects	: 182813
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 52
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 245.076
c starts	: 53
c conflicts	: 0
c decisions	: 1247037
c propagations	: 1315193
c inspects	: 185629
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 53
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 245.739
c starts	: 54
c conflicts	: 0
c decisions	: 1270566
c propagations	: 1340007
c inspects	: 188445
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 54
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 246.804
c starts	: 55
c conflicts	: 0
c decisions	: 1294095
c propagations	: 1364821
c inspects	: 191250
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 55
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 247.475
c starts	: 56
c conflicts	: 0
c decisions	: 1317624
c propagations	: 1389635
c inspects	: 194066
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 56
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 248.148
c starts	: 57
c conflicts	: 0
c decisions	: 1341153
c propagations	: 1414449
c inspects	: 196882
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 57
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 248.827
c starts	: 58
c conflicts	: 0
c decisions	: 1364682
c propagations	: 1439263
c inspects	: 199698
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 58
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 249.953
c starts	: 59
c conflicts	: 0
c decisions	: 1388211
c propagations	: 1464077
c inspects	: 202503
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 59
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 250.642
c starts	: 60
c conflicts	: 0
c decisions	: 1411740
c propagations	: 1488891
c inspects	: 205319
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 60
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 251.331
c starts	: 61
c conflicts	: 0
c decisions	: 1435269
c propagations	: 1513705
c inspects	: 208135
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 61
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 252.021
c starts	: 62
c conflicts	: 0
c decisions	: 1458798
c propagations	: 1538519
c inspects	: 210935
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 62
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 253.084
c starts	: 63
c conflicts	: 0
c decisions	: 1482327
c propagations	: 1563333
c inspects	: 213751
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 63
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 253.775
c starts	: 64
c conflicts	: 0
c decisions	: 1505856
c propagations	: 1588147
c inspects	: 216567
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 64
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 254.572
c starts	: 65
c conflicts	: 0
c decisions	: 1529385
c propagations	: 1612961
c inspects	: 219379
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 65
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 255.743
c starts	: 66
c conflicts	: 0
c decisions	: 1552914
c propagations	: 1637775
c inspects	: 222195
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 66
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 256.452
c starts	: 67
c conflicts	: 0
c decisions	: 1576443
c propagations	: 1662589
c inspects	: 225000
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 67
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 257.17
c starts	: 68
c conflicts	: 0
c decisions	: 1599972
c propagations	: 1687403
c inspects	: 227816
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 68
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 257.888
c starts	: 69
c conflicts	: 0
c decisions	: 1623501
c propagations	: 1712217
c inspects	: 230632
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 69
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 258.998
c starts	: 70
c conflicts	: 0
c decisions	: 1647030
c propagations	: 1737031
c inspects	: 233448
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 70
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 259.726
c starts	: 71
c conflicts	: 0
c decisions	: 1670559
c propagations	: 1761845
c inspects	: 236253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 71
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 260.457
c starts	: 72
c conflicts	: 0
c decisions	: 1694088
c propagations	: 1786659
c inspects	: 239058
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 72
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 261.606
c starts	: 73
c conflicts	: 0
c decisions	: 1717617
c propagations	: 1811473
c inspects	: 241863
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 73
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 262.346
c starts	: 74
c conflicts	: 0
c decisions	: 1741146
c propagations	: 1836287
c inspects	: 244668
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 74
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 263.089
c starts	: 75
c conflicts	: 0
c decisions	: 1764675
c propagations	: 1861101
c inspects	: 247484
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 75
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 263.833
c starts	: 76
c conflicts	: 0
c decisions	: 1788204
c propagations	: 1885915
c inspects	: 250289
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 76
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 265.03
c starts	: 77
c conflicts	: 0
c decisions	: 1811733
c propagations	: 1910729
c inspects	: 253105
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 77
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 265.783
c starts	: 78
c conflicts	: 0
c decisions	: 1835262
c propagations	: 1935543
c inspects	: 255921
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 78
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 266.539
c starts	: 79
c conflicts	: 0
c decisions	: 1858791
c propagations	: 1960357
c inspects	: 258726
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 79
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 267.297
c starts	: 80
c conflicts	: 0
c decisions	: 1882320
c propagations	: 1985171
c inspects	: 261531
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 80
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 268.425
c starts	: 81
c conflicts	: 0
c decisions	: 1905849
c propagations	: 2009985
c inspects	: 264347
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 81
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 269.199
c starts	: 82
c conflicts	: 0
c decisions	: 1929378
c propagations	: 2034799
c inspects	: 267163
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 82
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 269.973
c starts	: 83
c conflicts	: 0
c decisions	: 1952907
c propagations	: 2059613
c inspects	: 269972
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 83
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 270.748
c starts	: 84
c conflicts	: 0
c decisions	: 1976436
c propagations	: 2084427
c inspects	: 272788
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 84
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 271.949
c starts	: 85
c conflicts	: 0
c decisions	: 1999965
c propagations	: 2109241
c inspects	: 275604
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 85
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 272.731
c starts	: 86
c conflicts	: 0
c decisions	: 2023494
c propagations	: 2134055
c inspects	: 278420
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 86
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 273.517
c starts	: 87
c conflicts	: 0
c decisions	: 2047023
c propagations	: 2158869
c inspects	: 281236
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 87
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 274.733
c starts	: 88
c conflicts	: 0
c decisions	: 2070552
c propagations	: 2183683
c inspects	: 284052
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 88
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 275.528
c starts	: 89
c conflicts	: 0
c decisions	: 2094081
c propagations	: 2208497
c inspects	: 286868
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 89
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 276.324
c starts	: 90
c conflicts	: 0
c decisions	: 2117610
c propagations	: 2233311
c inspects	: 289674
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 90
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 277.124
c starts	: 91
c conflicts	: 0
c decisions	: 2141139
c propagations	: 2258125
c inspects	: 292490
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 91
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 278.378
c starts	: 92
c conflicts	: 0
c decisions	: 2164668
c propagations	: 2282939
c inspects	: 295306
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 92
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 279.187
c starts	: 93
c conflicts	: 0
c decisions	: 2188197
c propagations	: 2307753
c inspects	: 298112
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 93
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 279.993
c starts	: 94
c conflicts	: 0
c decisions	: 2211726
c propagations	: 2332567
c inspects	: 300911
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 94
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 280.804
c starts	: 95
c conflicts	: 0
c decisions	: 2235255
c propagations	: 2357381
c inspects	: 303727
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 95
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 281.988
c starts	: 96
c conflicts	: 0
c decisions	: 2258784
c propagations	: 2382195
c inspects	: 306543
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 96
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 282.816
c starts	: 97
c conflicts	: 0
c decisions	: 2282313
c propagations	: 2407009
c inspects	: 309359
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 97
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 283.658
c starts	: 98
c conflicts	: 0
c decisions	: 2305842
c propagations	: 2431823
c inspects	: 312164
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 98
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 284.489
c starts	: 99
c conflicts	: 0
c decisions	: 2329371
c propagations	: 2456637
c inspects	: 314980
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 99
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 285.79
c starts	: 100
c conflicts	: 0
c decisions	: 2352900
c propagations	: 2481451
c inspects	: 317796
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 100
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 286.631
c starts	: 101
c conflicts	: 0
c decisions	: 2376429
c propagations	: 2506265
c inspects	: 320612
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 101
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 287.474
c starts	: 102
c conflicts	: 0
c decisions	: 2399958
c propagations	: 2531079
c inspects	: 323428
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 102
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 288.692
c starts	: 103
c conflicts	: 0
c decisions	: 2423487
c propagations	: 2555893
c inspects	: 326244
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 103
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 289.542
c starts	: 104
c conflicts	: 0
c decisions	: 2447016
c propagations	: 2580707
c inspects	: 329060
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 104
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 290.406
c starts	: 105
c conflicts	: 0
c decisions	: 2470545
c propagations	: 2605521
c inspects	: 331876
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 105
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 291.261
c starts	: 106
c conflicts	: 0
c decisions	: 2494074
c propagations	: 2630335
c inspects	: 334680
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 106
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 292.526
c starts	: 107
c conflicts	: 0
c decisions	: 2517603
c propagations	: 2655149
c inspects	: 337496
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 107
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 293.392
c starts	: 108
c conflicts	: 0
c decisions	: 2541132
c propagations	: 2679963
c inspects	: 340312
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 108
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 294.262
c starts	: 109
c conflicts	: 0
c decisions	: 2564661
c propagations	: 2704777
c inspects	: 343128
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 109
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 295.132
c starts	: 110
c conflicts	: 0
c decisions	: 2588190
c propagations	: 2729591
c inspects	: 345925
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 110
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 296.418
c starts	: 111
c conflicts	: 0
c decisions	: 2611719
c propagations	: 2754405
c inspects	: 348730
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 111
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 297.298
c starts	: 112
c conflicts	: 0
c decisions	: 2635248
c propagations	: 2779219
c inspects	: 351546
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 112
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 298.188
c starts	: 113
c conflicts	: 0
c decisions	: 2658777
c propagations	: 2804033
c inspects	: 354350
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 113
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 299.501
c starts	: 114
c conflicts	: 0
c decisions	: 2682306
c propagations	: 2828847
c inspects	: 357190
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 114
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 300.389
c starts	: 115
c conflicts	: 0
c decisions	: 2705835
c propagations	: 2853661
c inspects	: 359995
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 115
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 301.285
c starts	: 116
c conflicts	: 0
c decisions	: 2729364
c propagations	: 2878475
c inspects	: 362811
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 116
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 302.183
c starts	: 117
c conflicts	: 0
c decisions	: 2752893
c propagations	: 2903289
c inspects	: 365627
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 117
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 303.523
c starts	: 118
c conflicts	: 0
c decisions	: 2776422
c propagations	: 2928103
c inspects	: 368443
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 118
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 304.428
c starts	: 119
c conflicts	: 0
c decisions	: 2799951
c propagations	: 2952917
c inspects	: 371249
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 119
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 305.338
c starts	: 120
c conflicts	: 0
c decisions	: 2823480
c propagations	: 2977731
c inspects	: 374065
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 120
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 306.253
c starts	: 121
c conflicts	: 0
c decisions	: 2847009
c propagations	: 3002545
c inspects	: 376881
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 121
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 307.552
c starts	: 122
c conflicts	: 0
c decisions	: 2870538
c propagations	: 3027359
c inspects	: 379681
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 122
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 308.474
c starts	: 123
c conflicts	: 0
c decisions	: 2894067
c propagations	: 3052173
c inspects	: 382497
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 123
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 309.398
c starts	: 124
c conflicts	: 0
c decisions	: 2917596
c propagations	: 3076987
c inspects	: 385313
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 124
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 310.326
c starts	: 125
c conflicts	: 0
c decisions	: 2941125
c propagations	: 3101801
c inspects	: 388129
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 125
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 311.67
c starts	: 126
c conflicts	: 0
c decisions	: 2964654
c propagations	: 3126615
c inspects	: 390945
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 126
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 312.596
c starts	: 127
c conflicts	: 0
c decisions	: 2988183
c propagations	: 3151429
c inspects	: 393761
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 127
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 313.524
c starts	: 128
c conflicts	: 0
c decisions	: 3011712
c propagations	: 3176243
c inspects	: 396577
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 128
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 315.048
c starts	: 129
c conflicts	: 0
c decisions	: 3035241
c propagations	: 3201057
c inspects	: 399383
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 129
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 315.997
c starts	: 130
c conflicts	: 0
c decisions	: 3058770
c propagations	: 3225871
c inspects	: 402187
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 130
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 317.446
c starts	: 131
c conflicts	: 0
c decisions	: 3082299
c propagations	: 3250685
c inspects	: 405003
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 131
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 318.403
c starts	: 132
c conflicts	: 0
c decisions	: 3105828
c propagations	: 3275499
c inspects	: 407819
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 132
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 319.362
c starts	: 133
c conflicts	: 0
c decisions	: 3129357
c propagations	: 3300313
c inspects	: 410624
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 133
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 320.644
c starts	: 134
c conflicts	: 0
c decisions	: 3152886
c propagations	: 3325127
c inspects	: 413440
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 134
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 321.612
c starts	: 135
c conflicts	: 0
c decisions	: 3176415
c propagations	: 3349941
c inspects	: 416256
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 135
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 322.58
c starts	: 136
c conflicts	: 0
c decisions	: 3199944
c propagations	: 3374755
c inspects	: 419062
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 136
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 323.556
c starts	: 137
c conflicts	: 0
c decisions	: 3223473
c propagations	: 3399569
c inspects	: 421878
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 137
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 324.962
c starts	: 138
c conflicts	: 0
c decisions	: 3247002
c propagations	: 3424383
c inspects	: 424683
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 138
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 325.947
c starts	: 139
c conflicts	: 0
c decisions	: 3270531
c propagations	: 3449197
c inspects	: 427499
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 139
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 326.933
c starts	: 140
c conflicts	: 0
c decisions	: 3294060
c propagations	: 3474011
c inspects	: 430315
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 140
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 327.921
c starts	: 141
c conflicts	: 0
c decisions	: 3317589
c propagations	: 3498825
c inspects	: 433131
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 141
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 329.307
c starts	: 142
c conflicts	: 0
c decisions	: 3341118
c propagations	: 3523639
c inspects	: 435947
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 142
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 330.305
c starts	: 143
c conflicts	: 0
c decisions	: 3364647
c propagations	: 3548453
c inspects	: 438763
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 143
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 331.31
c starts	: 144
c conflicts	: 0
c decisions	: 3388176
c propagations	: 3573267
c inspects	: 441568
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 144
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 332.321
c starts	: 145
c conflicts	: 0
c decisions	: 3411705
c propagations	: 3598081
c inspects	: 444384
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 145
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 333.753
c starts	: 146
c conflicts	: 0
c decisions	: 3435234
c propagations	: 3622895
c inspects	: 447197
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 146
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 334.767
c starts	: 147
c conflicts	: 0
c decisions	: 3458763
c propagations	: 3647709
c inspects	: 450013
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 147
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 335.78
c starts	: 148
c conflicts	: 0
c decisions	: 3482292
c propagations	: 3672523
c inspects	: 452818
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 148
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 337.262
c starts	: 149
c conflicts	: 0
c decisions	: 3505821
c propagations	: 3697337
c inspects	: 455634
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 149
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 338.283
c starts	: 150
c conflicts	: 0
c decisions	: 3529350
c propagations	: 3722151
c inspects	: 458450
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 150
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 339.309
c starts	: 151
c conflicts	: 0
c decisions	: 3552879
c propagations	: 3746965
c inspects	: 461266
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 151
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 340.337
c starts	: 152
c conflicts	: 0
c decisions	: 3576408
c propagations	: 3771779
c inspects	: 464082
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 152
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 341.735
c starts	: 153
c conflicts	: 0
c decisions	: 3599937
c propagations	: 3796593
c inspects	: 466898
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 153
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 342.771
c starts	: 154
c conflicts	: 0
c decisions	: 3623466
c propagations	: 3821407
c inspects	: 469699
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 154
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 343.81
c starts	: 155
c conflicts	: 0
c decisions	: 3646995
c propagations	: 3846221
c inspects	: 472504
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 155
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 344.855
c starts	: 156
c conflicts	: 0
c decisions	: 3670524
c propagations	: 3871035
c inspects	: 475320
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 156
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 346.318
c starts	: 157
c conflicts	: 0
c decisions	: 3694053
c propagations	: 3895849
c inspects	: 478136
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 157
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 347.373
c starts	: 158
c conflicts	: 0
c decisions	: 3717582
c propagations	: 3920663
c inspects	: 480952
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 158
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 348.427
c starts	: 159
c conflicts	: 0
c decisions	: 3741111
c propagations	: 3945477
c inspects	: 483749
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 159
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 349.914
c starts	: 160
c conflicts	: 0
c decisions	: 3764640
c propagations	: 3970291
c inspects	: 486554
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 160
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 350.986
c starts	: 161
c conflicts	: 0
c decisions	: 3788169
c propagations	: 3995105
c inspects	: 489370
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 161
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 352.056
c starts	: 162
c conflicts	: 0
c decisions	: 3811698
c propagations	: 4019919
c inspects	: 492178
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 162
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 353.126
c starts	: 163
c conflicts	: 0
c decisions	: 3835227
c propagations	: 4044733
c inspects	: 494979
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 163
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 354.609
c starts	: 164
c conflicts	: 0
c decisions	: 3858756
c propagations	: 4069547
c inspects	: 497795
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 164
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 355.675
c starts	: 165
c conflicts	: 0
c decisions	: 3882285
c propagations	: 4094361
c inspects	: 500611
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 165
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 356.745
c starts	: 166
c conflicts	: 0
c decisions	: 3905814
c propagations	: 4119175
c inspects	: 503427
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 166
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 357.822
c starts	: 167
c conflicts	: 0
c decisions	: 3929343
c propagations	: 4143989
c inspects	: 506232
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 167
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 359.316
c starts	: 168
c conflicts	: 0
c decisions	: 3952872
c propagations	: 4168803
c inspects	: 509037
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 168
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 360.411
c starts	: 169
c conflicts	: 0
c decisions	: 3976401
c propagations	: 4193617
c inspects	: 511842
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 169
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 361.506
c starts	: 170
c conflicts	: 0
c decisions	: 3999930
c propagations	: 4218431
c inspects	: 514646
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 170
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 363.031
c starts	: 171
c conflicts	: 0
c decisions	: 4023459
c propagations	: 4243245
c inspects	: 517462
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 171
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 364.13
c starts	: 172
c conflicts	: 0
c decisions	: 4046988
c propagations	: 4268059
c inspects	: 520267
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 172
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 365.224
c starts	: 173
c conflicts	: 0
c decisions	: 4070517
c propagations	: 4292873
c inspects	: 523083
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 173
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 366.323
c starts	: 174
c conflicts	: 0
c decisions	: 4094046
c propagations	: 4317687
c inspects	: 525899
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 174
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 367.863
c starts	: 175
c conflicts	: 0
c decisions	: 4117575
c propagations	: 4342501
c inspects	: 528715
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 175
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 368.982
c starts	: 176
c conflicts	: 0
c decisions	: 4141104
c propagations	: 4367315
c inspects	: 531531
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 176
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 370.098
c starts	: 177
c conflicts	: 0
c decisions	: 4164633
c propagations	: 4392129
c inspects	: 534347
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 177
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 371.21
c starts	: 178
c conflicts	: 0
c decisions	: 4188162
c propagations	: 4416943
c inspects	: 537163
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 178
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 372.728
c starts	: 179
c conflicts	: 0
c decisions	: 4211691
c propagations	: 4441757
c inspects	: 539979
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 179
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 373.865
c starts	: 180
c conflicts	: 0
c decisions	: 4235220
c propagations	: 4466571
c inspects	: 542795
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 180
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 375.003
c starts	: 181
c conflicts	: 0
c decisions	: 4258749
c propagations	: 4491385
c inspects	: 545611
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 181
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 376.551
c starts	: 182
c conflicts	: 0
c decisions	: 4282278
c propagations	: 4516199
c inspects	: 548427
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 182
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 377.7
c starts	: 183
c conflicts	: 0
c decisions	: 4305807
c propagations	: 4541013
c inspects	: 551243
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 183
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 378.848
c starts	: 184
c conflicts	: 0
c decisions	: 4329336
c propagations	: 4565827
c inspects	: 554048
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 184
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 380.003
c starts	: 185
c conflicts	: 0
c decisions	: 4352865
c propagations	: 4590641
c inspects	: 556864
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 185
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 381.593
c starts	: 186
c conflicts	: 0
c decisions	: 4376394
c propagations	: 4615455
c inspects	: 559662
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 186
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 382.759
c starts	: 187
c conflicts	: 0
c decisions	: 4399923
c propagations	: 4640269
c inspects	: 562478
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 187
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 383.922
c starts	: 188
c conflicts	: 0
c decisions	: 4423452
c propagations	: 4665083
c inspects	: 565294
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 188
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 385.08
c starts	: 189
c conflicts	: 0
c decisions	: 4446981
c propagations	: 4689897
c inspects	: 568110
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 189
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 386.632
c starts	: 190
c conflicts	: 0
c decisions	: 4470510
c propagations	: 4714711
c inspects	: 570926
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 190
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 387.805
c starts	: 191
c conflicts	: 0
c decisions	: 4494039
c propagations	: 4739525
c inspects	: 573729
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 191
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 388.988
c starts	: 192
c conflicts	: 0
c decisions	: 4517568
c propagations	: 4764339
c inspects	: 576545
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 192
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 390.598
c starts	: 193
c conflicts	: 0
c decisions	: 4541097
c propagations	: 4789153
c inspects	: 579342
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 193
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 391.815
c starts	: 194
c conflicts	: 0
c decisions	: 4564626
c propagations	: 4813967
c inspects	: 582158
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 194
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 393.007
c starts	: 195
c conflicts	: 0
c decisions	: 4588155
c propagations	: 4838781
c inspects	: 584974
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 195
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 394.203
c starts	: 196
c conflicts	: 0
c decisions	: 4611684
c propagations	: 4863595
c inspects	: 587790
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 196
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 395.824
c starts	: 197
c conflicts	: 0
c decisions	: 4635213
c propagations	: 4888409
c inspects	: 590589
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 197
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 397.027
c starts	: 198
c conflicts	: 0
c decisions	: 4658742
c propagations	: 4913223
c inspects	: 593405
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 198
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 398.233
c starts	: 199
c conflicts	: 0
c decisions	: 4682271
c propagations	: 4938037
c inspects	: 596209
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 199
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 399.445
c starts	: 200
c conflicts	: 0
c decisions	: 4705800
c propagations	: 4962851
c inspects	: 599013
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 200
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 401.027
c starts	: 201
c conflicts	: 0
c decisions	: 4729329
c propagations	: 4987665
c inspects	: 601829
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 201
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 402.243
c starts	: 202
c conflicts	: 0
c decisions	: 4752858
c propagations	: 5012479
c inspects	: 604632
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 202
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 403.466
c starts	: 203
c conflicts	: 0
c decisions	: 4776387
c propagations	: 5037293
c inspects	: 607448
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 203
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 405.161
c starts	: 204
c conflicts	: 0
c decisions	: 4799916
c propagations	: 5062107
c inspects	: 610256
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 204
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 406.388
c starts	: 205
c conflicts	: 0
c decisions	: 4823445
c propagations	: 5086921
c inspects	: 613061
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 205
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 407.619
c starts	: 206
c conflicts	: 0
c decisions	: 4846974
c propagations	: 5111735
c inspects	: 615877
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 206
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 408.855
c starts	: 207
c conflicts	: 0
c decisions	: 4870503
c propagations	: 5136549
c inspects	: 618693
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 207
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 410.455
c starts	: 208
c conflicts	: 0
c decisions	: 4894032
c propagations	: 5161363
c inspects	: 621509
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 208
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 411.699
c starts	: 209
c conflicts	: 0
c decisions	: 4917561
c propagations	: 5186177
c inspects	: 624325
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 209
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 412.947
c starts	: 210
c conflicts	: 0
c decisions	: 4941090
c propagations	: 5210991
c inspects	: 627130
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 210
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 414.197
c starts	: 211
c conflicts	: 0
c decisions	: 4964619
c propagations	: 5235805
c inspects	: 629946
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 211
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 415.871
c starts	: 212
c conflicts	: 0
c decisions	: 4988148
c propagations	: 5260619
c inspects	: 632762
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 212
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 417.129
c starts	: 213
c conflicts	: 0
c decisions	: 5011677
c propagations	: 5285433
c inspects	: 635578
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 213
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 418.391
c starts	: 214
c conflicts	: 0
c decisions	: 5035206
c propagations	: 5310247
c inspects	: 638394
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 214
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 420.116
c starts	: 215
c conflicts	: 0
c decisions	: 5058735
c propagations	: 5335061
c inspects	: 641199
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 215
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 421.386
c starts	: 216
c conflicts	: 0
c decisions	: 5082264
c propagations	: 5359875
c inspects	: 644015
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 216
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 422.661
c starts	: 217
c conflicts	: 0
c decisions	: 5105793
c propagations	: 5384689
c inspects	: 646820
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 217
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 423.934
c starts	: 218
c conflicts	: 0
c decisions	: 5129322
c propagations	: 5409503
c inspects	: 649625
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 218
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 425.583
c starts	: 219
c conflicts	: 0
c decisions	: 5152851
c propagations	: 5434317
c inspects	: 652441
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 219
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 426.867
c starts	: 220
c conflicts	: 0
c decisions	: 5176380
c propagations	: 5459131
c inspects	: 655257
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 220
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 428.155
c starts	: 221
c conflicts	: 0
c decisions	: 5199909
c propagations	: 5483945
c inspects	: 658073
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 221
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 429.446
c starts	: 222
c conflicts	: 0
c decisions	: 5223438
c propagations	: 5508759
c inspects	: 660889
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 222
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 431.174
c starts	: 223
c conflicts	: 0
c decisions	: 5246967
c propagations	: 5533573
c inspects	: 663705
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 223
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 432.474
c starts	: 224
c conflicts	: 0
c decisions	: 5270496
c propagations	: 5558387
c inspects	: 666521
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 224
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 433.78
c starts	: 225
c conflicts	: 0
c decisions	: 5294025
c propagations	: 5583201
c inspects	: 669326
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 225
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 435.542
c starts	: 226
c conflicts	: 0
c decisions	: 5317554
c propagations	: 5608015
c inspects	: 672142
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 226
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 436.852
c starts	: 227
c conflicts	: 0
c decisions	: 5341083
c propagations	: 5632829
c inspects	: 674940
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 227
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 438.169
c starts	: 228
c conflicts	: 0
c decisions	: 5364612
c propagations	: 5657643
c inspects	: 677756
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 228
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 439.487
c starts	: 229
c conflicts	: 0
c decisions	: 5388141
c propagations	: 5682457
c inspects	: 680572
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 229
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 441.197
c starts	: 230
c conflicts	: 0
c decisions	: 5411670
c propagations	: 5707271
c inspects	: 683388
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 230
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 442.524
c starts	: 231
c conflicts	: 0
c decisions	: 5435199
c propagations	: 5732085
c inspects	: 686204
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 231
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 443.85
c starts	: 232
c conflicts	: 0
c decisions	: 5458728
c propagations	: 5756899
c inspects	: 689001
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 232
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 445.182
c starts	: 233
c conflicts	: 0
c decisions	: 5482257
c propagations	: 5781713
c inspects	: 691806
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 233
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 446.95
c starts	: 234
c conflicts	: 0
c decisions	: 5505786
c propagations	: 5806527
c inspects	: 694622
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 234
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 448.29
c starts	: 235
c conflicts	: 0
c decisions	: 5529315
c propagations	: 5831341
c inspects	: 697438
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 235
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 449.636
c starts	: 236
c conflicts	: 0
c decisions	: 5552844
c propagations	: 5856155
c inspects	: 700254
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 236
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 451.413
c starts	: 237
c conflicts	: 0
c decisions	: 5576373
c propagations	: 5880969
c inspects	: 703059
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 237
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 452.751
c starts	: 238
c conflicts	: 0
c decisions	: 5599902
c propagations	: 5905783
c inspects	: 705875
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 238
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 454.107
c starts	: 239
c conflicts	: 0
c decisions	: 5623431
c propagations	: 5930597
c inspects	: 708691
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 239
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 455.465
c starts	: 240
c conflicts	: 0
c decisions	: 5646960
c propagations	: 5955411
c inspects	: 711507
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 240
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 457.218
c starts	: 241
c conflicts	: 0
c decisions	: 5670489
c propagations	: 5980225
c inspects	: 714323
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 241
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 458.584
c starts	: 242
c conflicts	: 0
c decisions	: 5694018
c propagations	: 6005039
c inspects	: 717128
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 242
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 459.955
c starts	: 243
c conflicts	: 0
c decisions	: 5717547
c propagations	: 6029853
c inspects	: 719944
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 243
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 461.751
c starts	: 244
c conflicts	: 0
c decisions	: 5741076
c propagations	: 6054667
c inspects	: 722760
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 244
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 463.13
c starts	: 245
c conflicts	: 0
c decisions	: 5764605
c propagations	: 6079481
c inspects	: 725576
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 245
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 464.52
c starts	: 246
c conflicts	: 0
c decisions	: 5788134
c propagations	: 6104295
c inspects	: 728392
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 246
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 465.909
c starts	: 247
c conflicts	: 0
c decisions	: 5811663
c propagations	: 6129109
c inspects	: 731201
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 247
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 467.711
c starts	: 248
c conflicts	: 0
c decisions	: 5835192
c propagations	: 6153923
c inspects	: 734007
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 248
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 469.087
c starts	: 249
c conflicts	: 0
c decisions	: 5858721
c propagations	: 6178737
c inspects	: 736823
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 249
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 470.471
c starts	: 250
c conflicts	: 0
c decisions	: 5882250
c propagations	: 6203551
c inspects	: 739639
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 250
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 471.871
c starts	: 251
c conflicts	: 0
c decisions	: 5905779
c propagations	: 6228365
c inspects	: 742455
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 251
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 473.684
c starts	: 252
c conflicts	: 0
c decisions	: 5929308
c propagations	: 6253179
c inspects	: 745271
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 252
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 475.077
c starts	: 253
c conflicts	: 0
c decisions	: 5952837
c propagations	: 6277993
c inspects	: 748076
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 253
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 476.474
c starts	: 254
c conflicts	: 0
c decisions	: 5976366
c propagations	: 6302807
c inspects	: 750892
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 254
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 478.309
c starts	: 255
c conflicts	: 0
c decisions	: 5999895
c propagations	: 6327621
c inspects	: 753708
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 255
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 479.714
c starts	: 256
c conflicts	: 0
c decisions	: 6023424
c propagations	: 6352435
c inspects	: 756524
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 256
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 482.406
c starts	: 257
c conflicts	: 0
c decisions	: 6046953
c propagations	: 6377249
c inspects	: 759340
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 257
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 483.826
c starts	: 258
c conflicts	: 0
c decisions	: 6070482
c propagations	: 6402063
c inspects	: 762156
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 258
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 485.256
c starts	: 259
c conflicts	: 0
c decisions	: 6094011
c propagations	: 6426877
c inspects	: 764972
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 259
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 486.691
c starts	: 260
c conflicts	: 0
c decisions	: 6117540
c propagations	: 6451691
c inspects	: 767788
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 260
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 503.793
c starts	: 261
c conflicts	: 0
c decisions	: 6141069
c propagations	: 6476505
c inspects	: 770593
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 261
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 505.222
c starts	: 262
c conflicts	: 0
c decisions	: 6164598
c propagations	: 6501319
c inspects	: 773409
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 262
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 506.656
c starts	: 263
c conflicts	: 0
c decisions	: 6188127
c propagations	: 6526133
c inspects	: 776215
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 263
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 520.982
c starts	: 264
c conflicts	: 0
c decisions	: 6211656
c propagations	: 6550947
c inspects	: 779031
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 264
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 522.422
c starts	: 265
c conflicts	: 0
c decisions	: 6235185
c propagations	: 6575761
c inspects	: 781837
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 265
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 523.867
c starts	: 266
c conflicts	: 0
c decisions	: 6258714
c propagations	: 6600575
c inspects	: 784653
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 266
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 525.318
c starts	: 267
c conflicts	: 0
c decisions	: 6282243
c propagations	: 6625389
c inspects	: 787458
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 267
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 539.851
c starts	: 268
c conflicts	: 0
c decisions	: 6305772
c propagations	: 6650203
c inspects	: 790274
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 268
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 541.313
c starts	: 269
c conflicts	: 0
c decisions	: 6329301
c propagations	: 6675017
c inspects	: 793079
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 269
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 542.772
c starts	: 270
c conflicts	: 0
c decisions	: 6352830
c propagations	: 6699831
c inspects	: 795895
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 270
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 544.244
c starts	: 271
c conflicts	: 0
c decisions	: 6376359
c propagations	: 6724645
c inspects	: 798711
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 271
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 564.902
c starts	: 272
c conflicts	: 0
c decisions	: 6399888
c propagations	: 6749459
c inspects	: 801527
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 272
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 566.37
c starts	: 273
c conflicts	: 0
c decisions	: 6423417
c propagations	: 6774273
c inspects	: 804343
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 273
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 567.846
c starts	: 274
c conflicts	: 0
c decisions	: 6446946
c propagations	: 6799087
c inspects	: 807159
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 274
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 569.548
c starts	: 275
c conflicts	: 0
c decisions	: 6470475
c propagations	: 6823901
c inspects	: 809965
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 275
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 571.026
c starts	: 276
c conflicts	: 0
c decisions	: 6494004
c propagations	: 6848715
c inspects	: 812770
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 276
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 572.51
c starts	: 277
c conflicts	: 0
c decisions	: 6517533
c propagations	: 6873529
c inspects	: 815586
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 277
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 574.013
c starts	: 278
c conflicts	: 0
c decisions	: 6541062
c propagations	: 6898343
c inspects	: 818402
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 278
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 575.889
c starts	: 279
c conflicts	: 0
c decisions	: 6564591
c propagations	: 6923157
c inspects	: 821218
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 279
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 577.384
c starts	: 280
c conflicts	: 0
c decisions	: 6588120
c propagations	: 6947971
c inspects	: 824034
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 280
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 578.882
c starts	: 281
c conflicts	: 0
c decisions	: 6611649
c propagations	: 6972785
c inspects	: 826850
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 281
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 580.387
c starts	: 282
c conflicts	: 0
c decisions	: 6635178
c propagations	: 6997599
c inspects	: 829655
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 282
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 595.687
c starts	: 283
c conflicts	: 0
c decisions	: 6658707
c propagations	: 7022413
c inspects	: 832471
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 283
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 597.201
c starts	: 284
c conflicts	: 0
c decisions	: 6682236
c propagations	: 7047227
c inspects	: 835276
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 284
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 598.713
c starts	: 285
c conflicts	: 0
c decisions	: 6705765
c propagations	: 7072041
c inspects	: 838092
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 285
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 614.07
c starts	: 286
c conflicts	: 0
c decisions	: 6729294
c propagations	: 7096855
c inspects	: 840898
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 286
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 615.596
c starts	: 287
c conflicts	: 0
c decisions	: 6752823
c propagations	: 7121669
c inspects	: 843702
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 287
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 617.133
c starts	: 288
c conflicts	: 0
c decisions	: 6776352
c propagations	: 7146483
c inspects	: 846518
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 288
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 618.667
c starts	: 289
c conflicts	: 0
c decisions	: 6799881
c propagations	: 7171297
c inspects	: 849334
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 289
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 634.269
c starts	: 290
c conflicts	: 0
c decisions	: 6823410
c propagations	: 7196111
c inspects	: 852150
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 290
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 635.801
c starts	: 291
c conflicts	: 0
c decisions	: 6846939
c propagations	: 7220925
c inspects	: 854955
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 291
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 637.342
c starts	: 292
c conflicts	: 0
c decisions	: 6870468
c propagations	: 7245739
c inspects	: 857771
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 292
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 656.361
c starts	: 293
c conflicts	: 0
c decisions	: 6893997
c propagations	: 7270553
c inspects	: 860587
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 293
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 657.913
c starts	: 294
c conflicts	: 0
c decisions	: 6917526
c propagations	: 7295367
c inspects	: 863403
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 294
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 659.463
c starts	: 295
c conflicts	: 0
c decisions	: 6941055
c propagations	: 7320181
c inspects	: 866219
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 295
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 661.016
c starts	: 296
c conflicts	: 0
c decisions	: 6964584
c propagations	: 7344995
c inspects	: 869035
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 296
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 676.947
c starts	: 297
c conflicts	: 0
c decisions	: 6988113
c propagations	: 7369809
c inspects	: 871851
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 297
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 678.506
c starts	: 298
c conflicts	: 0
c decisions	: 7011642
c propagations	: 7394623
c inspects	: 874667
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 298
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 680.072
c starts	: 299
c conflicts	: 0
c decisions	: 7035171
c propagations	: 7419437
c inspects	: 877483
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 299
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 681.65
c starts	: 300
c conflicts	: 0
c decisions	: 7058700
c propagations	: 7444251
c inspects	: 880299
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 300
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 697.834
c starts	: 301
c conflicts	: 0
c decisions	: 7082229
c propagations	: 7469065
c inspects	: 883107
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 301
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 699.417
c starts	: 302
c conflicts	: 0
c decisions	: 7105758
c propagations	: 7493879
c inspects	: 885923
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 302
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 700.995
c starts	: 303
c conflicts	: 0
c decisions	: 7129287
c propagations	: 7518693
c inspects	: 888739
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 303
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 717.309
c starts	: 304
c conflicts	: 0
c decisions	: 7152816
c propagations	: 7543507
c inspects	: 891555
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 304
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 718.898
c starts	: 305
c conflicts	: 0
c decisions	: 7176345
c propagations	: 7568321
c inspects	: 894368
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 305
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 720.496
c starts	: 306
c conflicts	: 0
c decisions	: 7199874
c propagations	: 7593135
c inspects	: 897184
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 306
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 722.102
c starts	: 307
c conflicts	: 0
c decisions	: 7223403
c propagations	: 7617949
c inspects	: 900000
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 307
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 744.317
c starts	: 308
c conflicts	: 0
c decisions	: 7246932
c propagations	: 7642763
c inspects	: 902816
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 308
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 745.92
c starts	: 309
c conflicts	: 0
c decisions	: 7270461
c propagations	: 7667577
c inspects	: 905632
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 309
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 747.533
c starts	: 310
c conflicts	: 0
c decisions	: 7293990
c propagations	: 7692391
c inspects	: 908448
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 310
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 764.181
c starts	: 311
c conflicts	: 0
c decisions	: 7317519
c propagations	: 7717205
c inspects	: 911264
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 311
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 765.804
c starts	: 312
c conflicts	: 0
c decisions	: 7341048
c propagations	: 7742019
c inspects	: 914080
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 312
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 767.435
c starts	: 313
c conflicts	: 0
c decisions	: 7364577
c propagations	: 7766833
c inspects	: 916896
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 313
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 769.068
c starts	: 314
c conflicts	: 0
c decisions	: 7388106
c propagations	: 7791647
c inspects	: 919712
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 314
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 786.682
c starts	: 315
c conflicts	: 0
c decisions	: 7411635
c propagations	: 7816461
c inspects	: 922528
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 315
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 788.312
c starts	: 316
c conflicts	: 0
c decisions	: 7435164
c propagations	: 7841275
c inspects	: 925344
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 316
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 789.952
c starts	: 317
c conflicts	: 0
c decisions	: 7458693
c propagations	: 7866089
c inspects	: 928160
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 317
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 791.818
c starts	: 318
c conflicts	: 0
c decisions	: 7482222
c propagations	: 7890903
c inspects	: 930976
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 318
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 809.525
c starts	: 319
c conflicts	: 0
c decisions	: 7505751
c propagations	: 7915717
c inspects	: 933792
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 319
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 811.172
c starts	: 320
c conflicts	: 0
c decisions	: 7529280
c propagations	: 7940531
c inspects	: 936608
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 320
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 812.821
c starts	: 321
c conflicts	: 0
c decisions	: 7552809
c propagations	: 7965345
c inspects	: 939424
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 321
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 831.111
c starts	: 322
c conflicts	: 0
c decisions	: 7576338
c propagations	: 7990159
c inspects	: 942240
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 322
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 832.781
c starts	: 323
c conflicts	: 0
c decisions	: 7599867
c propagations	: 8014973
c inspects	: 945056
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 323
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 834.452
c starts	: 324
c conflicts	: 0
c decisions	: 7623396
c propagations	: 8039787
c inspects	: 947861
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 324
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 852.707
c starts	: 325
c conflicts	: 0
c decisions	: 7646925
c propagations	: 8064601
c inspects	: 950677
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 325
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 854.373
c starts	: 326
c conflicts	: 0
c decisions	: 7670454
c propagations	: 8089415
c inspects	: 953493
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 326
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 856.448
c starts	: 327
c conflicts	: 0
c decisions	: 7693983
c propagations	: 8114229
c inspects	: 956309
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 327
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 874.221
c starts	: 328
c conflicts	: 0
c decisions	: 7717512
c propagations	: 8139043
c inspects	: 959125
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 328
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 875.894
c starts	: 329
c conflicts	: 0
c decisions	: 7741041
c propagations	: 8163857
c inspects	: 961924
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 329
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 894.257
c starts	: 330
c conflicts	: 0
c decisions	: 7764570
c propagations	: 8188671
c inspects	: 964740
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 330
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 895.941
c starts	: 331
c conflicts	: 0
c decisions	: 7788099
c propagations	: 8213485
c inspects	: 967556
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 331
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 917.967
c starts	: 332
c conflicts	: 0
c decisions	: 7811628
c propagations	: 8238299
c inspects	: 970372
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 332
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 919.663
c starts	: 333
c conflicts	: 0
c decisions	: 7835157
c propagations	: 8263113
c inspects	: 973188
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 333
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 938.168
c starts	: 334
c conflicts	: 0
c decisions	: 7858686
c propagations	: 8287927
c inspects	: 975985
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 334
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 940.154
c starts	: 335
c conflicts	: 0
c decisions	: 7882215
c propagations	: 8312741
c inspects	: 978791
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 335
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 958.428
c starts	: 336
c conflicts	: 0
c decisions	: 7905744
c propagations	: 8337555
c inspects	: 981607
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 336
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 976.694
c starts	: 337
c conflicts	: 0
c decisions	: 7929273
c propagations	: 8362369
c inspects	: 984412
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 337
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 978.723
c starts	: 338
c conflicts	: 0
c decisions	: 7952802
c propagations	: 8387183
c inspects	: 987228
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 338
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 1000.573
c starts	: 339
c conflicts	: 0
c decisions	: 7976331
c propagations	: 8411997
c inspects	: 990044
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 339
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 1019.298
c starts	: 340
c conflicts	: 0
c decisions	: 7999860
c propagations	: 8436811
c inspects	: 992860
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 340
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 1037.95
c starts	: 341
c conflicts	: 0
c decisions	: 8023389
c propagations	: 8461625
c inspects	: 995676
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 341
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 1056.697
c starts	: 342
c conflicts	: 0
c decisions	: 8046918
c propagations	: 8486439
c inspects	: 998492
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 342
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 1079.267
c starts	: 343
c conflicts	: 0
c decisions	: 8070447
c propagations	: 8511253
c inspects	: 1001297
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 343
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 1098.454
c starts	: 344
c conflicts	: 0
c decisions	: 8093976
c propagations	: 8536067
c inspects	: 1004094
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 344
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 1133.964
c starts	: 345
c conflicts	: 0
c decisions	: 8117505
c propagations	: 8560881
c inspects	: 1006910
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 345
c 
c CURRENT OPTIMUM=817168384
c Current CPU time (ms) : 1169.689
c starts	: 346
c conflicts	: 0
c decisions	: 8141034
c propagations	: 8585695
c inspects	: 1009726
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 346
c 
c CURRENT OPTIMUM=817168384
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.97 0.91 2/55 16517
Raw data (stat): 16517 (runsolver) R 16516 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540516320 1052672 99 4294967295 134512640 135381576 3221224416 3221219664 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.97 0.91 2/64 16526
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 888 39 0 0 25 0 10 0 540516320 854220800 19227 4294967295 134512640 134569956 3221224400 3221214744 1131184513 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208550 19227 13073 16 0 208534 0
vsize: 834200
[startup+19.9997 s]
Raw data (loadavg): 0.94 0.97 0.91 2/64 16526
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 1776 40 0 0 25 0 10 0 540516320 854220800 19785 4294967295 134512640 134569956 3221224400 3221214820 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208550 19785 13073 16 0 208534 0
vsize: 834200
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.97 0.91 2/64 16526
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 2673 40 0 0 25 0 10 0 540516320 854220800 20224 4294967295 134512640 134569956 3221224400 3221214716 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 20224 13073 16 0 208534 0
vsize: 834200
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.97 0.91 2/64 16526
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 3602 41 0 0 25 0 10 0 540516320 854220800 20454 4294967295 134512640 134569956 3221224400 3221214272 1077558376 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 20454 13073 16 0 208534 0
vsize: 834200
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.97 0.91 2/64 16526
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 4529 41 0 0 25 0 10 0 540516320 854220800 20577 4294967295 134512640 134569956 3221224400 3221214288 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208550 20577 13073 16 0 208534 0
vsize: 834200
[startup+60.009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/64 16526
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 5457 41 0 0 25 0 10 0 540516320 854220800 20696 4294967295 134512640 134569956 3221224400 3221214820 1080204163 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 20696 13073 16 0 208534 0
vsize: 834200
[startup+70.0158 s]
Raw data (loadavg): 0.97 0.97 0.91 2/64 16526
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 6399 42 0 0 25 0 10 0 540516320 854220800 20902 4294967295 134512640 134569956 3221224400 3221214700 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 20902 13073 16 0 208534 0
vsize: 834200
[startup+80.0165 s]
Raw data (loadavg): 0.98 0.97 0.91 2/64 16526
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 17986 0 1 0 7344 42 0 0 25 0 10 0 540516320 854220800 20979 4294967295 134512640 134569956 3221224400 3221213392 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 20979 13073 16 0 208534 0
vsize: 834200
[startup+90.0169 s]
Raw data (loadavg): 0.98 0.97 0.91 2/64 16528
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 8291 43 0 0 25 0 10 0 540516320 854220800 21053 4294967295 134512640 134569956 3221224400 3221214796 1080204031 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 21053 13073 16 0 208534 0
vsize: 834200
[startup+100.017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/64 16528
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 9237 43 0 0 25 0 10 0 540516320 854220800 21122 4294967295 134512640 134569956 3221224400 3221214796 1080204031 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 21122 13073 16 0 208534 0
vsize: 834200
[startup+110.018 s]
Raw data (loadavg): 0.98 0.97 0.91 2/64 16528
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 17986 0 1 0 10185 44 0 0 25 0 10 0 540516320 854220800 21185 4294967295 134512640 134569956 3221224400 3221213512 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 21185 13073 16 0 208534 0
vsize: 834200
[startup+120.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 16528
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 11133 44 0 0 25 0 10 0 540516320 854220800 21246 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 21246 13073 16 0 208534 0
vsize: 834200
[startup+130.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 16528
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 12080 44 0 0 25 0 10 0 540516320 854220800 21304 4294967295 134512640 134569956 3221224400 3221214796 1080204031 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 21304 13073 16 0 208534 0
vsize: 834200
[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 16528
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 13027 45 0 0 25 0 10 0 540516320 854220800 21360 4294967295 134512640 134569956 3221224400 3221214256 1077558376 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 21360 13073 16 0 208534 0
vsize: 834200
[startup+150.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 16528
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 13976 45 0 0 25 0 10 0 540516320 854220800 21412 4294967295 134512640 134569956 3221224400 3221214700 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 21412 13073 16 0 208534 0
vsize: 834200
[startup+160.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 16528
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17986 0 1 0 14921 45 0 0 25 0 10 0 540516320 854220800 21463 4294967295 134512640 134569956 3221224400 3221214700 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208550 21463 13073 16 0 208534 0
vsize: 834200
[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.91 4/64 16528
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17990 0 1 0 15801 46 0 0 25 0 10 0 540516320 856977408 22129 4294967295 134512640 134569956 3221224400 3221213828 1130883346 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209223 22129 13073 16 0 209207 0
vsize: 836892
[startup+180.022 s]
Raw data (loadavg): 1.14 1.00 0.93 2/64 16528
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17991 0 1 0 16764 47 0 0 25 0 10 0 540516320 855736320 21871 4294967295 134512640 134569956 3221224400 3221214440 1131274560 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208920 21871 13073 16 0 208904 0
vsize: 835680
[startup+190.021 s]
Raw data (loadavg): 1.12 1.00 0.93 2/64 16528
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 17991 0 1 0 17751 48 0 0 25 0 10 0 540516320 855736320 22401 4294967295 134512640 134569956 3221224400 3221214640 1131277158 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208920 22401 13073 16 0 208904 0
vsize: 835680
[startup+200.022 s]
Raw data (loadavg): 1.10 1.00 0.93 2/65 16529
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18022 0 1 0 18675 51 0 0 25 0 11 0 540516320 857612288 26579 4294967295 134512640 134569956 3221224400 3221214688 1131407529 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209378 26579 13073 16 0 209362 0
vsize: 837512
[startup+210.022 s]
Raw data (loadavg): 1.08 1.00 0.93 2/65 16529
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18022 0 1 0 19655 51 0 0 25 0 11 0 540516320 857018368 26469 4294967295 134512640 134569956 3221224400 3221214728 1131443162 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 26469 13073 16 0 209217 0
vsize: 836932
[startup+220.022 s]
Raw data (loadavg): 1.07 1.00 0.93 2/64 16545
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18024 4 1 0 20494 52 0 0 25 0 10 0 540516320 857018368 31846 4294967295 134512640 134569956 3221224400 3221215024 1131251072 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 31846 13073 16 0 209217 0
vsize: 836932
[startup+230.022 s]
Raw data (loadavg): 1.06 1.00 0.93 2/64 16560
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18024 4 1 0 21328 53 0 0 25 0 10 0 540516320 857018368 39057 4294967295 134512640 134569956 3221224400 3221214880 1131276118 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 39057 13073 16 0 209217 0
vsize: 836932
[startup+240.022 s]
Raw data (loadavg): 1.05 1.00 0.93 2/65 16574
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18024 4 1 0 22164 53 1 0 25 0 11 0 540516320 857018368 46988 4294967295 134512640 134569956 3221224400 3221214680 1131407384 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 46988 13073 16 0 209217 0
vsize: 836932
[startup+250.027 s]
Raw data (loadavg): 1.04 1.00 0.93 2/64 16587
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18024 4 1 0 23036 54 1 0 25 0 10 0 540516320 857018368 51868 4294967295 134512640 134569956 3221224400 3221213488 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 51868 13073 16 0 209217 0
vsize: 836932
[startup+260.028 s]
Raw data (loadavg): 1.03 1.00 0.93 2/65 16599
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18024 4 1 0 23873 55 1 1 25 0 11 0 540516320 857018368 60864 4294967295 134512640 134569956 3221224400 3221214768 1131441468 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 60864 13073 16 0 209217 0
vsize: 836932
[startup+270.027 s]
Raw data (loadavg): 1.03 1.00 0.93 2/65 16611
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18024 4 1 0 24747 56 2 1 25 0 11 0 540516320 857018368 65581 4294967295 134512640 134569956 3221224400 3221214816 1131423729 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 65581 13073 16 0 209217 0
vsize: 836932
[startup+280.028 s]
Raw data (loadavg): 1.02 1.00 0.93 2/65 16622
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18024 4 1 0 25615 56 2 1 25 0 11 0 540516320 857018368 70569 4294967295 134512640 134569956 3221224400 3221214816 1131424532 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 70569 13073 16 0 209217 0
vsize: 836932
[startup+290.028 s]
Raw data (loadavg): 1.02 1.00 0.93 2/64 16632
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18024 4 1 0 26492 57 2 1 24 0 10 0 540516320 857018368 75677 4294967295 134512640 134569956 3221224400 3221214840 1131370450 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 75677 13073 16 0 209217 0
vsize: 836932
[startup+300.028 s]
Raw data (loadavg): 1.02 1.00 0.93 2/64 16642
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18024 4 1 0 27370 58 3 1 25 0 10 0 540516320 857018368 80272 4294967295 134512640 134569956 3221224400 3221213528 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 80272 13073 16 0 209217 0
vsize: 836932
[startup+310.033 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 16652
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18025 4 1 0 28285 58 3 2 25 0 10 0 540516320 857018368 83332 4294967295 134512640 134569956 3221224400 3221214608 1131331718 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 83332 13073 16 0 209217 0
vsize: 836932
[startup+320.033 s]
Raw data (loadavg): 1.01 1.00 0.93 2/65 16662
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18025 4 1 0 29154 59 3 2 25 0 11 0 540516320 857018368 94081 4294967295 134512640 134569956 3221224400 3221214816 1131423731 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 94081 13073 16 0 209217 0
vsize: 836932
[startup+330.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/65 16671
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18025 4 1 0 30037 60 3 2 25 0 11 0 540516320 857018368 97964 4294967295 134512640 134569956 3221224400 3221214816 1131423860 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 97964 13073 16 0 209217 0
vsize: 836932
[startup+340.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/65 16680
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18025 4 1 0 30947 61 3 2 25 0 11 0 540516320 857018368 101359 4294967295 134512640 134569956 3221224400 3221214816 1131423835 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 101359 13073 16 0 209217 0
vsize: 836932
[startup+350.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16688
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18025 4 1 0 31867 61 4 2 25 0 10 0 540516320 857018368 104166 4294967295 134512640 134569956 3221224400 3221213488 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 104166 13073 16 0 209217 0
vsize: 836932
[startup+360.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16697
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18025 4 1 0 32742 62 4 2 17 0 11 0 540516320 857018368 108834 4294967295 134512640 134569956 3221224400 3221214816 1131424509 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 108834 13073 16 0 209217 0
vsize: 836932
[startup+370.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16705
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 33653 63 4 2 25 0 11 0 540516320 857018368 112069 4294967295 134512640 134569956 3221224400 3221214816 1131424628 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 112069 13073 16 0 209217 0
vsize: 836932
[startup+380.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16713
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 34572 64 4 3 25 0 11 0 540516320 857018368 115083 4294967295 134512640 134569956 3221224400 3221214816 1131423763 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 115083 13073 16 0 209217 0
vsize: 836932
[startup+390.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16723
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 35487 65 4 3 25 0 11 0 540516320 857018368 118119 4294967295 134512640 134569956 3221224400 3221214816 1131423729 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 118119 13073 16 0 209217 0
vsize: 836932
[startup+400.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16730
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 36401 65 5 3 25 0 10 0 540516320 857018368 121942 4294967295 134512640 134569956 3221224400 3221214688 1131331718 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 121942 13073 16 0 209217 0
vsize: 836932
[startup+410.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16738
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 37316 65 5 3 25 0 11 0 540516320 857018368 125533 4294967295 134512640 134569956 3221224400 3221214816 1131424554 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 125533 13073 16 0 209217 0
vsize: 836932
[startup+420.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16745
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 38239 65 5 3 25 0 11 0 540516320 857018368 128317 4294967295 134512640 134569956 3221224400 3221214956 1131366176 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 128317 13073 16 0 209217 0
vsize: 836932
[startup+430.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16752
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 39155 66 5 3 25 0 10 0 540516320 857018368 131353 4294967295 134512640 134569956 3221224400 3221214528 1131332154 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 131353 13073 16 0 209217 0
vsize: 836932
[startup+440.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16759
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 40065 66 5 3 25 0 10 0 540516320 857018368 134659 4294967295 134512640 134569956 3221224400 3221214768 1131331674 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 134659 13073 16 0 209217 0
vsize: 836932
[startup+450.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16766
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 40983 66 5 3 25 0 11 0 540516320 857018368 137554 4294967295 134512640 134569956 3221224400 3221214752 1131306803 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 137554 13073 16 0 209217 0
vsize: 836932
[startup+460.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16773
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 41900 67 5 3 25 0 11 0 540516320 857018368 140590 4294967295 134512640 134569956 3221224400 3221214816 1131424554 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 140590 13073 16 0 209217 0
vsize: 836932
[startup+470.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16780
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 42814 67 6 3 25 0 11 0 540516320 857018368 143718 4294967295 134512640 134569956 3221224400 3221214816 1131423645 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 143718 13073 16 0 209217 0
vsize: 836932
[startup+480.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16786
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 43729 68 6 3 25 0 11 0 540516320 857018368 146790 4294967295 134512640 134569956 3221224400 3221214680 1131407705 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 146790 13073 16 0 209217 0
vsize: 836932
[startup+490.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16791
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 44481 68 6 3 25 0 11 0 540516320 857018368 160681 4294967295 134512640 134569956 3221224400 3221213368 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160681 13073 16 0 209217 0
vsize: 836932
[startup+500.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16791
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 44481 68 6 3 25 0 11 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221213368 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+510.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16794
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 44930 69 6 3 25 0 10 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221213488 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+520.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16794
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 44930 69 6 3 25 0 10 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221213488 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+530.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16798
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 45498 69 6 3 25 0 10 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221213552 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+540.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16798
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 45498 69 6 3 25 0 10 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221213552 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+550.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16802
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 46069 69 6 4 25 0 11 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221213280 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+560.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16802
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 46069 69 6 4 25 0 11 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221213280 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+570.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16805
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 46532 70 6 4 25 0 10 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+580.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16812
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 47490 70 6 4 20 0 11 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221214816 1131423725 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+590.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16813
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 47668 70 6 4 25 0 11 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221213464 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+600.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16816
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 48110 71 6 4 25 0 11 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221214816 1131424522 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+610.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16816
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 48174 71 6 4 25 0 10 0 540516320 857018368 160682 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160682 13073 16 0 209217 0
vsize: 836932
[startup+620.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16820
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 48726 71 6 4 25 0 11 0 540516320 857018368 160757 4294967295 134512640 134569956 3221224400 3221214816 1131424576 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160757 13073 16 0 209217 0
vsize: 836932
[startup+630.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16820
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 48772 71 6 4 25 0 11 0 540516320 857018368 160757 4294967295 134512640 134569956 3221224400 3221213384 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 160757 13073 16 0 209217 0
vsize: 836932
[startup+640.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16823
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 49255 72 6 4 25 0 10 0 540516320 857018368 162426 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 162426 13073 16 0 209217 0
vsize: 836932
[startup+650.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16823
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 49255 72 6 4 25 0 10 0 540516320 857018368 162428 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 162428 13073 16 0 209217 0
vsize: 836932
[startup+660.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16825
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 49570 72 6 4 25 0 10 0 540516320 857018368 163490 4294967295 134512640 134569956 3221224400 3221214208 1131331735 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 163490 13073 16 0 209217 0
vsize: 836932
[startup+670.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16827
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 49860 72 6 4 25 0 11 0 540516320 857018368 163490 4294967295 134512640 134569956 3221224400 3221213664 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 163490 13073 16 0 209217 0
vsize: 836932
[startup+680.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16829
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 50132 72 6 4 25 0 11 0 540516320 857018368 165060 4294967295 134512640 134569956 3221224400 3221214816 1131423700 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 165060 13073 16 0 209217 0
vsize: 836932
[startup+690.059 s]
Raw data (loadavg): 1.08 1.02 0.93 3/68 16870
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 50450 72 7 4 25 0 11 0 540516320 857018368 165060 4294967295 134512640 134569956 3221224400 3221213224 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 165060 13073 16 0 209217 0
vsize: 836932
[startup+700.065 s]
Raw data (loadavg): 1.07 1.02 0.93 2/64 16887
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 50672 73 7 4 25 0 10 0 540516320 857018368 166826 4294967295 134512640 134569956 3221224400 3221213728 1131331271 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 166826 13073 16 0 209217 0
vsize: 836932
[startup+710.064 s]
Raw data (loadavg): 1.06 1.01 0.93 2/64 16889
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 50969 73 7 4 25 0 10 0 540516320 857018368 166826 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 166826 13073 16 0 209217 0
vsize: 836932
[startup+720.065 s]
Raw data (loadavg): 1.05 1.01 0.93 2/65 16891
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 51200 73 7 4 25 0 11 0 540516320 857018368 168622 4294967295 134512640 134569956 3221224400 3221214816 1131424509 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 168622 13073 16 0 209217 0
vsize: 836932
[startup+730.065 s]
Raw data (loadavg): 1.04 1.01 0.93 2/65 16893
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 51593 73 7 5 25 0 11 0 540516320 857018368 168622 4294967295 134512640 134569956 3221224400 3221213280 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 168622 13073 16 0 209217 0
vsize: 836932
[startup+740.065 s]
Raw data (loadavg): 1.03 1.01 0.93 2/65 16893
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 51593 73 7 5 25 0 11 0 540516320 857018368 168623 4294967295 134512640 134569956 3221224400 3221213280 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 168623 13073 16 0 209217 0
vsize: 836932
[startup+750.066 s]
Raw data (loadavg): 1.03 1.01 0.93 2/64 16896
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 52097 73 7 5 25 0 10 0 540516320 857018368 169342 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 169342 13073 16 0 209217 0
vsize: 836932
[startup+760.067 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 16898
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 52097 73 7 5 25 0 10 0 540516320 857018368 169344 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 169344 13073 16 0 209217 0
vsize: 836932
[startup+770.066 s]
Raw data (loadavg): 1.02 1.01 0.93 2/65 16902
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 52632 73 7 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214816 1131423669 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+780.066 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 16902
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 52820 73 7 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213544 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+790.066 s]
Raw data (loadavg): 1.01 1.01 0.93 2/65 16904
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 53106 74 7 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214816 1131424509 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+800.067 s]
Raw data (loadavg): 1.01 1.01 0.93 2/65 16906
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 53550 74 7 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213408 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+810.067 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 16906
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 53572 74 7 5 18 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214880 1131299018 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+820.067 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 16909
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 54152 75 7 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213624 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+830.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16909
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 54152 75 7 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213624 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+840.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16912
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 54753 75 7 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213720 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+850.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16912
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 54753 75 7 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213720 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+860.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16915
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 55324 75 7 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213408 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+870.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16915
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 55324 75 7 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213408 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+880.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16917
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 55769 75 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213624 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+890.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16917
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 55769 75 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213624 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+900.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16919
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 56191 76 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213488 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+910.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16919
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 56191 76 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213488 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+920.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16920
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 56355 76 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214848 1131480585 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+930.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16921
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 56623 76 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213688 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+940.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16922
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 56770 76 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214816 1131424509 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+950.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16923
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 57049 76 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213408 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+960.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16924
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 57182 76 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214816 1131424516 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+970.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16924
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 57303 76 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213528 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+980.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16926
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 57587 76 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214816 1131423677 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+990.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16928
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 57707 76 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213408 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16930
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 57707 76 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213408 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16931
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 57993 76 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213832 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16932
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 58029 76 8 5 20 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214816 1131423825 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1030.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16932
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 58254 76 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213488 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16933
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 58421 76 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213808 1073940437 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16933
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 58518 76 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213552 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16934
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 58793 77 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213496 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16934
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 58793 77 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213496 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16935
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 58852 77 8 5 21 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214816 1131423763 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16935
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 59059 77 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213512 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16936
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 59236 77 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214816 1131424509 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16936
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 59298 77 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213512 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16936
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 59397 77 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213520 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16936
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 59397 77 8 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213520 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16937
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 59646 77 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213384 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16937
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 59646 77 8 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213384 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1160.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16937
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 59732 77 9 5 24 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1170.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16937
Raw data (stat): 16517 (java) R 16516 22929 22928 0 -1 0 18026 4 1 0 59742 77 9 5 17 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221214312 1079300757 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 16938
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 59980 77 9 5 25 0 11 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213512 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1190.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16938
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 60073 77 9 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16938
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 60073 77 9 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16938
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 60073 77 9 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1220.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 16938
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 60073 77 9 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 836932
[startup+1222.52 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 16938
Raw data (stat): 16517 (java) S 16516 22929 22928 0 -1 0 18026 4 1 0 60073 77 9 5 25 0 10 0 540516320 857018368 170961 4294967295 134512640 134569956 3221224400 3221213624 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209233 170961 13073 16 0 209217 0
vsize: 0

Child status: 1
Real time (s): 1222.52
CPU time (s): 1225.69
CPU user time (s): 1221.51
CPU system time (s): 4.18036
CPU usage (%): 100.259
Max. virtual memory (Kb): 837512
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####