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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-grow22.opb
MD5SUM252426e4d147311f236e947ac8e9f53d
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 1958
Biggest coefficient in the objective function 3758096384
Number of bits for the biggest coefficient in the objective function 32
Sum of the numbers in the objective function 234612588283
Number of bits of the sum of numbers in the objective function 38
Biggest number in a constraint 878188741787648
Number of bits of the biggest number in a constraint 50
Biggest sum of numbers in a constraint 4550739094651140
Number of bits of the biggest sum of numbers53
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1264.78
Number of variables25124
Total number of constraints1320
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1320
Minimum length of a constraint22
Maximum length of a constraint491

Trace number 17490

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 10:14:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=10916 boxname=wulflinc20 idbench=840 idsolver=9 numberseed=0
MD5SUM SOLVER: daf345f6fbf228671abfac48013b9cac  /oldhome/oroussel/solvers/sat4jPseudo.jar
MD5SUM BENCH:  252426e4d147311f236e947ac8e9f53d  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-grow22.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudo.jar /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-grow22.opb
IDLAUNCH: 10916
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        396360 kB
Buffers:         24968 kB
Cached:         588624 kB
SwapCached:        516 kB
Active:         125472 kB
Inactive:       490112 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        396108 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            17152 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 10:35:31 (client local time) WITH STATUS 143 IN 1279.22 SECONDS
stats: 10916 7 1279.22 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-grow22.opb
c reading problem 
c [nbvar=25124]
c [nbconstr=1320]
c time 185.327
c #vars     25124
c #clauses  1761
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=0
c Current CPU time (ms) : 193.821
c starts	: 1
c conflicts	: 0
c decisions	: 24332
c propagations	: 25124
c inspects	: 27638
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=-1879048192
c Current CPU time (ms) : 196.108
c starts	: 2
c conflicts	: 0
c decisions	: 48663
c propagations	: 50248
c inspects	: 30063
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=1476395008
c Current CPU time (ms) : 198.498
c starts	: 3
c conflicts	: 0
c decisions	: 72993
c propagations	: 75372
c inspects	: 32497
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=1476395008
c Current CPU time (ms) : 200.953
c starts	: 4
c conflicts	: 0
c decisions	: 97323
c propagations	: 100496
c inspects	: 34924
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=1476395008
c Current CPU time (ms) : 203.35
c starts	: 5
c conflicts	: 0
c decisions	: 121653
c propagations	: 125620
c inspects	: 37355
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=1476395008
c Current CPU time (ms) : 205.815
c starts	: 6
c conflicts	: 0
c decisions	: 145983
c propagations	: 150744
c inspects	: 39784
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=1476395008
c Current CPU time (ms) : 208.221
c starts	: 7
c conflicts	: 0
c decisions	: 170313
c propagations	: 175868
c inspects	: 42214
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=1476395008
c Current CPU time (ms) : 210.578
c starts	: 8
c conflicts	: 0
c decisions	: 194643
c propagations	: 200992
c inspects	: 44642
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=1476395008
c Current CPU time (ms) : 213.102
c starts	: 9
c conflicts	: 0
c decisions	: 218973
c propagations	: 226116
c inspects	: 47072
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=1476395008
c Current CPU time (ms) : 215.508
c starts	: 10
c conflicts	: 0
c decisions	: 243303
c propagations	: 251240
c inspects	: 49499
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=1476395008
c Current CPU time (ms) : 217.976
c starts	: 11
c conflicts	: 0
c decisions	: 267633
c propagations	: 276364
c inspects	: 51925
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=1476395008
c Current CPU time (ms) : 220.381
c starts	: 12
c conflicts	: 0
c decisions	: 291963
c propagations	: 301488
c inspects	: 54355
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=1476395008
c Current CPU time (ms) : 222.782
c starts	: 13
c conflicts	: 0
c decisions	: 316293
c propagations	: 326612
c inspects	: 56782
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=1476395008
c Current CPU time (ms) : 225.22
c starts	: 14
c conflicts	: 0
c decisions	: 340623
c propagations	: 351736
c inspects	: 59213
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=1476395008
c Current CPU time (ms) : 227.586
c starts	: 15
c conflicts	: 0
c decisions	: 364953
c propagations	: 376860
c inspects	: 61639
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=1476395008
c Current CPU time (ms) : 230.045
c starts	: 16
c conflicts	: 0
c decisions	: 389283
c propagations	: 401984
c inspects	: 64067
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=1476395008
c Current CPU time (ms) : 232.463
c starts	: 17
c conflicts	: 0
c decisions	: 413613
c propagations	: 427108
c inspects	: 66494
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=1476395008
c Current CPU time (ms) : 234.802
c starts	: 18
c conflicts	: 0
c decisions	: 437943
c propagations	: 452232
c inspects	: 68923
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=1476395008
c Current CPU time (ms) : 237.164
c starts	: 19
c conflicts	: 0
c decisions	: 462273
c propagations	: 477356
c inspects	: 71349
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=1476395008
c Current CPU time (ms) : 239.459
c starts	: 20
c conflicts	: 0
c decisions	: 486603
c propagations	: 502480
c inspects	: 73778
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=1476395008
c Current CPU time (ms) : 241.79
c starts	: 21
c conflicts	: 0
c decisions	: 510933
c propagations	: 527604
c inspects	: 76204
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=1476395008
c Current CPU time (ms) : 244.098
c starts	: 22
c conflicts	: 0
c decisions	: 535263
c propagations	: 552728
c inspects	: 78634
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=1476395008
c Current CPU time (ms) : 246.427
c starts	: 23
c conflicts	: 0
c decisions	: 559593
c propagations	: 577852
c inspects	: 81061
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=1476395008
c Current CPU time (ms) : 248.776
c starts	: 24
c conflicts	: 0
c decisions	: 583923
c propagations	: 602976
c inspects	: 83489
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=1476395008
c Current CPU time (ms) : 251.115
c starts	: 25
c conflicts	: 0
c decisions	: 608253
c propagations	: 628100
c inspects	: 85916
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=1476395008
c Current CPU time (ms) : 253.457
c starts	: 26
c conflicts	: 0
c decisions	: 632583
c propagations	: 653224
c inspects	: 88344
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=1476395008
c Current CPU time (ms) : 255.858
c starts	: 27
c conflicts	: 0
c decisions	: 656913
c propagations	: 678348
c inspects	: 90769
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=1476395008
c Current CPU time (ms) : 258.216
c starts	: 28
c conflicts	: 0
c decisions	: 681243
c propagations	: 703472
c inspects	: 93194
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=1476395008
c Current CPU time (ms) : 260.634
c starts	: 29
c conflicts	: 0
c decisions	: 705573
c propagations	: 728596
c inspects	: 95623
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=1476395008
c Current CPU time (ms) : 263.002
c starts	: 30
c conflicts	: 0
c decisions	: 729903
c propagations	: 753720
c inspects	: 98053
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=1476395008
c Current CPU time (ms) : 265.38
c starts	: 31
c conflicts	: 0
c decisions	: 754233
c propagations	: 778844
c inspects	: 100483
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=1476395008
c Current CPU time (ms) : 267.856
c starts	: 32
c conflicts	: 0
c decisions	: 778563
c propagations	: 803968
c inspects	: 102911
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=1476395008
c Current CPU time (ms) : 270.325
c starts	: 33
c conflicts	: 0
c decisions	: 802893
c propagations	: 829092
c inspects	: 105342
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=1476395008
c Current CPU time (ms) : 272.616
c starts	: 34
c conflicts	: 0
c decisions	: 827223
c propagations	: 854216
c inspects	: 107770
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=1476395008
c Current CPU time (ms) : 274.93
c starts	: 35
c conflicts	: 0
c decisions	: 851553
c propagations	: 879340
c inspects	: 110199
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=1476395008
c Current CPU time (ms) : 277.229
c starts	: 36
c conflicts	: 0
c decisions	: 875883
c propagations	: 904464
c inspects	: 112628
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=1476395008
c Current CPU time (ms) : 279.537
c starts	: 37
c conflicts	: 0
c decisions	: 900213
c propagations	: 929588
c inspects	: 115056
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=1476395008
c Current CPU time (ms) : 281.831
c starts	: 38
c conflicts	: 0
c decisions	: 924543
c propagations	: 954712
c inspects	: 117487
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=1476395008
c Current CPU time (ms) : 284.194
c starts	: 39
c conflicts	: 0
c decisions	: 948873
c propagations	: 979836
c inspects	: 119917
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=1476395008
c Current CPU time (ms) : 286.483
c starts	: 40
c conflicts	: 0
c decisions	: 973203
c propagations	: 1004960
c inspects	: 122346
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=1476395008
c Current CPU time (ms) : 288.793
c starts	: 41
c conflicts	: 0
c decisions	: 997533
c propagations	: 1030084
c inspects	: 124777
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=1476395008
c Current CPU time (ms) : 291.148
c starts	: 42
c conflicts	: 0
c decisions	: 1021863
c propagations	: 1055208
c inspects	: 127206
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=1476395008
c Current CPU time (ms) : 293.497
c starts	: 43
c conflicts	: 0
c decisions	: 1046193
c propagations	: 1080332
c inspects	: 129632
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=1476395008
c Current CPU time (ms) : 295.908
c starts	: 44
c conflicts	: 0
c decisions	: 1070523
c propagations	: 1105456
c inspects	: 132059
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=1476395008
c Current CPU time (ms) : 298.268
c starts	: 45
c conflicts	: 0
c decisions	: 1094853
c propagations	: 1130580
c inspects	: 134486
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=1476395008
c Current CPU time (ms) : 300.646
c starts	: 46
c conflicts	: 0
c decisions	: 1119183
c propagations	: 1155704
c inspects	: 136914
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=1476395008
c Current CPU time (ms) : 303.066
c starts	: 47
c conflicts	: 0
c decisions	: 1143513
c propagations	: 1180828
c inspects	: 139344
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=1476395008
c Current CPU time (ms) : 305.451
c starts	: 48
c conflicts	: 0
c decisions	: 1167843
c propagations	: 1205952
c inspects	: 141773
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=1476395008
c Current CPU time (ms) : 307.834
c starts	: 49
c conflicts	: 0
c decisions	: 1192173
c propagations	: 1231076
c inspects	: 144204
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=1476395008
c Current CPU time (ms) : 310.243
c starts	: 50
c conflicts	: 0
c decisions	: 1216503
c propagations	: 1256200
c inspects	: 146632
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=1476395008
c Current CPU time (ms) : 312.598
c starts	: 51
c conflicts	: 0
c decisions	: 1240833
c propagations	: 1281324
c inspects	: 149060
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=1476395008
c Current CPU time (ms) : 315.03
c starts	: 52
c conflicts	: 0
c decisions	: 1265163
c propagations	: 1306448
c inspects	: 151487
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=1476395008
c Current CPU time (ms) : 317.385
c starts	: 53
c conflicts	: 0
c decisions	: 1289493
c propagations	: 1331572
c inspects	: 153915
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=1476395008
c Current CPU time (ms) : 319.752
c starts	: 54
c conflicts	: 0
c decisions	: 1313823
c propagations	: 1356696
c inspects	: 156342
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=1476395008
c Current CPU time (ms) : 322.162
c starts	: 55
c conflicts	: 0
c decisions	: 1338153
c propagations	: 1381820
c inspects	: 158770
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=1476395008
c Current CPU time (ms) : 324.536
c starts	: 56
c conflicts	: 0
c decisions	: 1362483
c propagations	: 1406944
c inspects	: 161197
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=1476395008
c Current CPU time (ms) : 326.948
c starts	: 57
c conflicts	: 0
c decisions	: 1386813
c propagations	: 1432068
c inspects	: 163623
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=1476395008
c Current CPU time (ms) : 329.298
c starts	: 58
c conflicts	: 0
c decisions	: 1411143
c propagations	: 1457192
c inspects	: 166053
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=1476395008
c Current CPU time (ms) : 331.651
c starts	: 59
c conflicts	: 0
c decisions	: 1435473
c propagations	: 1482316
c inspects	: 168484
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=1476395008
c Current CPU time (ms) : 334.085
c starts	: 60
c conflicts	: 0
c decisions	: 1459803
c propagations	: 1507440
c inspects	: 170911
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=1476395008
c Current CPU time (ms) : 336.443
c starts	: 61
c conflicts	: 0
c decisions	: 1484133
c propagations	: 1532564
c inspects	: 173341
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=1476395008
c Current CPU time (ms) : 338.794
c starts	: 62
c conflicts	: 0
c decisions	: 1508463
c propagations	: 1557688
c inspects	: 175768
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=1476395008
c Current CPU time (ms) : 341.198
c starts	: 63
c conflicts	: 0
c decisions	: 1532793
c propagations	: 1582812
c inspects	: 178197
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=1476395008
c Current CPU time (ms) : 343.649
c starts	: 64
c conflicts	: 0
c decisions	: 1557123
c propagations	: 1607936
c inspects	: 180628
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=1476395008
c Current CPU time (ms) : 346.188
c starts	: 65
c conflicts	: 0
c decisions	: 1581453
c propagations	: 1633060
c inspects	: 183059
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=1476395008
c Current CPU time (ms) : 348.535
c starts	: 66
c conflicts	: 0
c decisions	: 1605783
c propagations	: 1658184
c inspects	: 185489
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=1476395008
c Current CPU time (ms) : 350.978
c starts	: 67
c conflicts	: 0
c decisions	: 1630113
c propagations	: 1683308
c inspects	: 187918
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=1476395008
c Current CPU time (ms) : 353.329
c starts	: 68
c conflicts	: 0
c decisions	: 1654443
c propagations	: 1708432
c inspects	: 190346
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=1476395008
c Current CPU time (ms) : 355.725
c starts	: 69
c conflicts	: 0
c decisions	: 1678773
c propagations	: 1733556
c inspects	: 192775
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=1476395008
c Current CPU time (ms) : 358.125
c starts	: 70
c conflicts	: 0
c decisions	: 1703103
c propagations	: 1758680
c inspects	: 195204
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=1476395008
c Current CPU time (ms) : 360.491
c starts	: 71
c conflicts	: 0
c decisions	: 1727433
c propagations	: 1783804
c inspects	: 197632
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=1476395008
c Current CPU time (ms) : 362.9
c starts	: 72
c conflicts	: 0
c decisions	: 1751763
c propagations	: 1808928
c inspects	: 200059
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=1476395008
c Current CPU time (ms) : 365.248
c starts	: 73
c conflicts	: 0
c decisions	: 1776093
c propagations	: 1834052
c inspects	: 202488
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=1476395008
c Current CPU time (ms) : 367.612
c starts	: 74
c conflicts	: 0
c decisions	: 1800423
c propagations	: 1859176
c inspects	: 204917
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=1476395008
c Current CPU time (ms) : 370.055
c starts	: 75
c conflicts	: 0
c decisions	: 1824753
c propagations	: 1884300
c inspects	: 207343
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=1476395008
c Current CPU time (ms) : 372.407
c starts	: 76
c conflicts	: 0
c decisions	: 1849083
c propagations	: 1909424
c inspects	: 209769
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=1476395008
c Current CPU time (ms) : 374.8
c starts	: 77
c conflicts	: 0
c decisions	: 1873413
c propagations	: 1934548
c inspects	: 212198
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=1476395008
c Current CPU time (ms) : 377.219
c starts	: 78
c conflicts	: 0
c decisions	: 1897743
c propagations	: 1959672
c inspects	: 214624
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=1476395008
c Current CPU time (ms) : 379.592
c starts	: 79
c conflicts	: 0
c decisions	: 1922073
c propagations	: 1984796
c inspects	: 217054
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=1476395008
c Current CPU time (ms) : 381.989
c starts	: 80
c conflicts	: 0
c decisions	: 1946403
c propagations	: 2009920
c inspects	: 219481
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=1476395008
c Current CPU time (ms) : 384.387
c starts	: 81
c conflicts	: 0
c decisions	: 1970733
c propagations	: 2035044
c inspects	: 221911
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=1476395008
c Current CPU time (ms) : 386.735
c starts	: 82
c conflicts	: 0
c decisions	: 1995063
c propagations	: 2060168
c inspects	: 224338
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=1476395008
c Current CPU time (ms) : 389.136
c starts	: 83
c conflicts	: 0
c decisions	: 2019393
c propagations	: 2085292
c inspects	: 226765
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=1476395008
c Current CPU time (ms) : 391.528
c starts	: 84
c conflicts	: 0
c decisions	: 2043723
c propagations	: 2110416
c inspects	: 229192
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=1476395008
c Current CPU time (ms) : 393.932
c starts	: 85
c conflicts	: 0
c decisions	: 2068053
c propagations	: 2135540
c inspects	: 231623
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=1476395008
c Current CPU time (ms) : 396.298
c starts	: 86
c conflicts	: 0
c decisions	: 2092383
c propagations	: 2160664
c inspects	: 234051
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=1476395008
c Current CPU time (ms) : 398.649
c starts	: 87
c conflicts	: 0
c decisions	: 2116713
c propagations	: 2185788
c inspects	: 236479
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=1476395008
c Current CPU time (ms) : 401.08
c starts	: 88
c conflicts	: 0
c decisions	: 2141043
c propagations	: 2210912
c inspects	: 238908
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=1476395008
c Current CPU time (ms) : 403.477
c starts	: 89
c conflicts	: 0
c decisions	: 2165373
c propagations	: 2236036
c inspects	: 241336
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=1476395008
c Current CPU time (ms) : 405.861
c starts	: 90
c conflicts	: 0
c decisions	: 2189703
c propagations	: 2261160
c inspects	: 243765
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=1476395008
c Current CPU time (ms) : 408.29
c starts	: 91
c conflicts	: 0
c decisions	: 2214033
c propagations	: 2286284
c inspects	: 246194
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=1476395008
c Current CPU time (ms) : 410.633
c starts	: 92
c conflicts	: 0
c decisions	: 2238363
c propagations	: 2311408
c inspects	: 248623
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=1476395008
c Current CPU time (ms) : 413.03
c starts	: 93
c conflicts	: 0
c decisions	: 2262693
c propagations	: 2336532
c inspects	: 251051
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=1476395008
c Current CPU time (ms) : 415.394
c starts	: 94
c conflicts	: 0
c decisions	: 2287023
c propagations	: 2361656
c inspects	: 253479
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=1476395008
c Current CPU time (ms) : 417.744
c starts	: 95
c conflicts	: 0
c decisions	: 2311353
c propagations	: 2386780
c inspects	: 255908
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=1476395008
c Current CPU time (ms) : 420.139
c starts	: 96
c conflicts	: 0
c decisions	: 2335683
c propagations	: 2411904
c inspects	: 258337
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=1476395008
c Current CPU time (ms) : 422.538
c starts	: 97
c conflicts	: 0
c decisions	: 2360013
c propagations	: 2437028
c inspects	: 260766
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=1476395008
c Current CPU time (ms) : 424.963
c starts	: 98
c conflicts	: 0
c decisions	: 2384343
c propagations	: 2462152
c inspects	: 263193
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=1476395008
c Current CPU time (ms) : 427.366
c starts	: 99
c conflicts	: 0
c decisions	: 2408673
c propagations	: 2487276
c inspects	: 265622
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=1476395008
c Current CPU time (ms) : 429.757
c starts	: 100
c conflicts	: 0
c decisions	: 2433003
c propagations	: 2512400
c inspects	: 268052
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=1476395008
c Current CPU time (ms) : 432.191
c starts	: 101
c conflicts	: 0
c decisions	: 2457333
c propagations	: 2537524
c inspects	: 270482
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=1476395008
c Current CPU time (ms) : 434.557
c starts	: 102
c conflicts	: 0
c decisions	: 2481663
c propagations	: 2562648
c inspects	: 272912
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=1476395008
c Current CPU time (ms) : 436.953
c starts	: 103
c conflicts	: 0
c decisions	: 2505993
c propagations	: 2587772
c inspects	: 275340
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=1476395008
c Current CPU time (ms) : 439.38
c starts	: 104
c conflicts	: 0
c decisions	: 2530323
c propagations	: 2612896
c inspects	: 277766
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=1476395008
c Current CPU time (ms) : 441.754
c starts	: 105
c conflicts	: 0
c decisions	: 2554653
c propagations	: 2638020
c inspects	: 280193
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=1476395008
c Current CPU time (ms) : 444.18
c starts	: 106
c conflicts	: 0
c decisions	: 2578983
c propagations	: 2663144
c inspects	: 282620
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=1476395008
c Current CPU time (ms) : 446.599
c starts	: 107
c conflicts	: 0
c decisions	: 2603313
c propagations	: 2688268
c inspects	: 285048
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=1476395008
c Current CPU time (ms) : 448.976
c starts	: 108
c conflicts	: 0
c decisions	: 2627643
c propagations	: 2713392
c inspects	: 287476
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=1476395008
c Current CPU time (ms) : 451.413
c starts	: 109
c conflicts	: 0
c decisions	: 2651973
c propagations	: 2738516
c inspects	: 289909
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=1476395008
c Current CPU time (ms) : 453.818
c starts	: 110
c conflicts	: 0
c decisions	: 2676303
c propagations	: 2763640
c inspects	: 292336
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=1476395008
c Current CPU time (ms) : 456.235
c starts	: 111
c conflicts	: 0
c decisions	: 2700633
c propagations	: 2788764
c inspects	: 294764
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=1476395008
c Current CPU time (ms) : 458.613
c starts	: 112
c conflicts	: 0
c decisions	: 2724963
c propagations	: 2813888
c inspects	: 297193
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=1476395008
c Current CPU time (ms) : 460.98
c starts	: 113
c conflicts	: 0
c decisions	: 2749293
c propagations	: 2839012
c inspects	: 299622
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=1476395008
c Current CPU time (ms) : 463.377
c starts	: 114
c conflicts	: 0
c decisions	: 2773623
c propagations	: 2864136
c inspects	: 302051
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=1476395008
c Current CPU time (ms) : 465.727
c starts	: 115
c conflicts	: 0
c decisions	: 2797953
c propagations	: 2889260
c inspects	: 304479
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=1476395008
c Current CPU time (ms) : 468.103
c starts	: 116
c conflicts	: 0
c decisions	: 2822283
c propagations	: 2914384
c inspects	: 306909
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=1476395008
c Current CPU time (ms) : 470.533
c starts	: 117
c conflicts	: 0
c decisions	: 2846613
c propagations	: 2939508
c inspects	: 309340
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=1476395008
c Current CPU time (ms) : 472.882
c starts	: 118
c conflicts	: 0
c decisions	: 2870943
c propagations	: 2964632
c inspects	: 311769
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=1476395008
c Current CPU time (ms) : 475.292
c starts	: 119
c conflicts	: 0
c decisions	: 2895273
c propagations	: 2989756
c inspects	: 314200
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=1476395008
c Current CPU time (ms) : 477.664
c starts	: 120
c conflicts	: 0
c decisions	: 2919603
c propagations	: 3014880
c inspects	: 316628
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=1476395008
c Current CPU time (ms) : 480.046
c starts	: 121
c conflicts	: 0
c decisions	: 2943933
c propagations	: 3040004
c inspects	: 319057
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=1476395008
c Current CPU time (ms) : 482.454
c starts	: 122
c conflicts	: 0
c decisions	: 2968263
c propagations	: 3065128
c inspects	: 321485
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=1476395008
c Current CPU time (ms) : 484.854
c starts	: 123
c conflicts	: 0
c decisions	: 2992593
c propagations	: 3090252
c inspects	: 323912
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=1476395008
c Current CPU time (ms) : 487.261
c starts	: 124
c conflicts	: 0
c decisions	: 3016923
c propagations	: 3115376
c inspects	: 326336
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=1476395008
c Current CPU time (ms) : 489.646
c starts	: 125
c conflicts	: 0
c decisions	: 3041253
c propagations	: 3140500
c inspects	: 328765
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=1476395008
c Current CPU time (ms) : 492.021
c starts	: 126
c conflicts	: 0
c decisions	: 3065583
c propagations	: 3165624
c inspects	: 331194
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=1476395008
c Current CPU time (ms) : 494.429
c starts	: 127
c conflicts	: 0
c decisions	: 3089913
c propagations	: 3190748
c inspects	: 333621
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=1476395008
c Current CPU time (ms) : 497.036
c starts	: 128
c conflicts	: 0
c decisions	: 3114243
c propagations	: 3215872
c inspects	: 336049
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=1476395008
c Current CPU time (ms) : 499.7
c starts	: 129
c conflicts	: 0
c decisions	: 3138573
c propagations	: 3240996
c inspects	: 338477
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=1476395008
c Current CPU time (ms) : 502.086
c starts	: 130
c conflicts	: 0
c decisions	: 3162903
c propagations	: 3266120
c inspects	: 340904
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=1476395008
c Current CPU time (ms) : 504.513
c starts	: 131
c conflicts	: 0
c decisions	: 3187233
c propagations	: 3291244
c inspects	: 343332
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=1476395008
c Current CPU time (ms) : 506.934
c starts	: 132
c conflicts	: 0
c decisions	: 3211563
c propagations	: 3316368
c inspects	: 345759
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=1476395008
c Current CPU time (ms) : 509.276
c starts	: 133
c conflicts	: 0
c decisions	: 3235893
c propagations	: 3341492
c inspects	: 348189
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=1476395008
c Current CPU time (ms) : 511.669
c starts	: 134
c conflicts	: 0
c decisions	: 3260223
c propagations	: 3366616
c inspects	: 350617
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=1476395008
c Current CPU time (ms) : 514.029
c starts	: 135
c conflicts	: 0
c decisions	: 3284553
c propagations	: 3391740
c inspects	: 353047
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=1476395008
c Current CPU time (ms) : 516.529
c starts	: 136
c conflicts	: 0
c decisions	: 3308883
c propagations	: 3416864
c inspects	: 355474
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=1476395008
c Current CPU time (ms) : 518.855
c starts	: 137
c conflicts	: 0
c decisions	: 3333213
c propagations	: 3441988
c inspects	: 357904
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=1476395008
c Current CPU time (ms) : 521.192
c starts	: 138
c conflicts	: 0
c decisions	: 3357543
c propagations	: 3467112
c inspects	: 360333
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=1476395008
c Current CPU time (ms) : 523.586
c starts	: 139
c conflicts	: 0
c decisions	: 3381873
c propagations	: 3492236
c inspects	: 362762
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=1476395008
c Current CPU time (ms) : 526.011
c starts	: 140
c conflicts	: 0
c decisions	: 3406203
c propagations	: 3517360
c inspects	: 365190
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=1476395008
c Current CPU time (ms) : 528.5
c starts	: 141
c conflicts	: 0
c decisions	: 3430533
c propagations	: 3542484
c inspects	: 367615
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=1476395008
c Current CPU time (ms) : 530.839
c starts	: 142
c conflicts	: 0
c decisions	: 3454863
c propagations	: 3567608
c inspects	: 370043
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=1476395008
c Current CPU time (ms) : 533.194
c starts	: 143
c conflicts	: 0
c decisions	: 3479193
c propagations	: 3592732
c inspects	: 372471
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=1476395008
c Current CPU time (ms) : 535.568
c starts	: 144
c conflicts	: 0
c decisions	: 3503523
c propagations	: 3617856
c inspects	: 374898
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=1476395008
c Current CPU time (ms) : 537.918
c starts	: 145
c conflicts	: 0
c decisions	: 3527853
c propagations	: 3642980
c inspects	: 377325
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=1476395008
c Current CPU time (ms) : 540.259
c starts	: 146
c conflicts	: 0
c decisions	: 3552183
c propagations	: 3668104
c inspects	: 379755
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=1476395008
c Current CPU time (ms) : 542.734
c starts	: 147
c conflicts	: 0
c decisions	: 3576513
c propagations	: 3693228
c inspects	: 382184
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=1476395008
c Current CPU time (ms) : 545.151
c starts	: 148
c conflicts	: 0
c decisions	: 3600843
c propagations	: 3718352
c inspects	: 384612
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=1476395008
c Current CPU time (ms) : 547.609
c starts	: 149
c conflicts	: 0
c decisions	: 3625173
c propagations	: 3743476
c inspects	: 387040
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=1476395008
c Current CPU time (ms) : 550.021
c starts	: 150
c conflicts	: 0
c decisions	: 3649503
c propagations	: 3768600
c inspects	: 389466
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=1476395008
c Current CPU time (ms) : 552.361
c starts	: 151
c conflicts	: 0
c decisions	: 3673833
c propagations	: 3793724
c inspects	: 391894
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=1476395008
c Current CPU time (ms) : 554.823
c starts	: 152
c conflicts	: 0
c decisions	: 3698163
c propagations	: 3818848
c inspects	: 394323
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=1476395008
c Current CPU time (ms) : 557.213
c starts	: 153
c conflicts	: 0
c decisions	: 3722493
c propagations	: 3843972
c inspects	: 396752
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=1476395008
c Current CPU time (ms) : 559.68
c starts	: 154
c conflicts	: 0
c decisions	: 3746823
c propagations	: 3869096
c inspects	: 399179
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=1476395008
c Current CPU time (ms) : 561.984
c starts	: 155
c conflicts	: 0
c decisions	: 3771153
c propagations	: 3894220
c inspects	: 401607
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=1476395008
c Current CPU time (ms) : 564.4
c starts	: 156
c conflicts	: 0
c decisions	: 3795483
c propagations	: 3919344
c inspects	: 404034
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=1476395008
c Current CPU time (ms) : 566.87
c starts	: 157
c conflicts	: 0
c decisions	: 3819813
c propagations	: 3944468
c inspects	: 406459
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=1476395008
c Current CPU time (ms) : 569.274
c starts	: 158
c conflicts	: 0
c decisions	: 3844143
c propagations	: 3969592
c inspects	: 408886
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=1476395008
c Current CPU time (ms) : 571.614
c starts	: 159
c conflicts	: 0
c decisions	: 3868473
c propagations	: 3994716
c inspects	: 411315
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=1476395008
c Current CPU time (ms) : 573.987
c starts	: 160
c conflicts	: 0
c decisions	: 3892803
c propagations	: 4019840
c inspects	: 413744
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=1476395008
c Current CPU time (ms) : 576.343
c starts	: 161
c conflicts	: 0
c decisions	: 3917133
c propagations	: 4044964
c inspects	: 416173
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=1476395008
c Current CPU time (ms) : 578.72
c starts	: 162
c conflicts	: 0
c decisions	: 3941463
c propagations	: 4070088
c inspects	: 418601
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=1476395008
c Current CPU time (ms) : 581.092
c starts	: 163
c conflicts	: 0
c decisions	: 3965793
c propagations	: 4095212
c inspects	: 421032
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=1476395008
c Current CPU time (ms) : 583.444
c starts	: 164
c conflicts	: 0
c decisions	: 3990123
c propagations	: 4120336
c inspects	: 423461
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=1476395008
c Current CPU time (ms) : 585.827
c starts	: 165
c conflicts	: 0
c decisions	: 4014453
c propagations	: 4145460
c inspects	: 425889
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=1476395008
c Current CPU time (ms) : 588.226
c starts	: 166
c conflicts	: 0
c decisions	: 4038783
c propagations	: 4170584
c inspects	: 428319
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=1476395008
c Current CPU time (ms) : 590.617
c starts	: 167
c conflicts	: 0
c decisions	: 4063113
c propagations	: 4195708
c inspects	: 430749
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=1476395008
c Current CPU time (ms) : 593.03
c starts	: 168
c conflicts	: 0
c decisions	: 4087443
c propagations	: 4220832
c inspects	: 433175
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=1476395008
c Current CPU time (ms) : 595.453
c starts	: 169
c conflicts	: 0
c decisions	: 4111773
c propagations	: 4245956
c inspects	: 435603
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=1476395008
c Current CPU time (ms) : 597.918
c starts	: 170
c conflicts	: 0
c decisions	: 4136103
c propagations	: 4271080
c inspects	: 438031
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=1476395008
c Current CPU time (ms) : 600.339
c starts	: 171
c conflicts	: 0
c decisions	: 4160433
c propagations	: 4296204
c inspects	: 440458
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=1476395008
c Current CPU time (ms) : 602.671
c starts	: 172
c conflicts	: 0
c decisions	: 4184763
c propagations	: 4321328
c inspects	: 442886
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=1476395008
c Current CPU time (ms) : 605.052
c starts	: 173
c conflicts	: 0
c decisions	: 4209093
c propagations	: 4346452
c inspects	: 445312
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=1476395008
c Current CPU time (ms) : 607.399
c starts	: 174
c conflicts	: 0
c decisions	: 4233423
c propagations	: 4371576
c inspects	: 447738
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=1476395008
c Current CPU time (ms) : 609.785
c starts	: 175
c conflicts	: 0
c decisions	: 4257753
c propagations	: 4396700
c inspects	: 450166
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=1476395008
c Current CPU time (ms) : 612.136
c starts	: 176
c conflicts	: 0
c decisions	: 4282083
c propagations	: 4421824
c inspects	: 452594
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=1476395008
c Current CPU time (ms) : 614.482
c starts	: 177
c conflicts	: 0
c decisions	: 4306413
c propagations	: 4446948
c inspects	: 455023
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=1476395008
c Current CPU time (ms) : 616.855
c starts	: 178
c conflicts	: 0
c decisions	: 4330743
c propagations	: 4472072
c inspects	: 457452
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=1476395008
c Current CPU time (ms) : 619.209
c starts	: 179
c conflicts	: 0
c decisions	: 4355073
c propagations	: 4497196
c inspects	: 459881
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=1476395008
c Current CPU time (ms) : 621.596
c starts	: 180
c conflicts	: 0
c decisions	: 4379403
c propagations	: 4522320
c inspects	: 462310
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=1476395008
c Current CPU time (ms) : 624.023
c starts	: 181
c conflicts	: 0
c decisions	: 4403733
c propagations	: 4547444
c inspects	: 464736
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=1476395008
c Current CPU time (ms) : 626.447
c starts	: 182
c conflicts	: 0
c decisions	: 4428063
c propagations	: 4572568
c inspects	: 467163
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=1476395008
c Current CPU time (ms) : 628.925
c starts	: 183
c conflicts	: 0
c decisions	: 4452393
c propagations	: 4597692
c inspects	: 469591
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=1476395008
c Current CPU time (ms) : 631.346
c starts	: 184
c conflicts	: 0
c decisions	: 4476723
c propagations	: 4622816
c inspects	: 472021
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=1476395008
c Current CPU time (ms) : 633.77
c starts	: 185
c conflicts	: 0
c decisions	: 4501053
c propagations	: 4647940
c inspects	: 474450
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=1476395008
c Current CPU time (ms) : 636.241
c starts	: 186
c conflicts	: 0
c decisions	: 4525383
c propagations	: 4673064
c inspects	: 476879
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=1476395008
c Current CPU time (ms) : 638.662
c starts	: 187
c conflicts	: 0
c decisions	: 4549713
c propagations	: 4698188
c inspects	: 479309
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=1476395008
c Current CPU time (ms) : 641.132
c starts	: 188
c conflicts	: 0
c decisions	: 4574043
c propagations	: 4723312
c inspects	: 481738
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=1476395008
c Current CPU time (ms) : 643.558
c starts	: 189
c conflicts	: 0
c decisions	: 4598373
c propagations	: 4748436
c inspects	: 484166
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=1476395008
c Current CPU time (ms) : 645.874
c starts	: 190
c conflicts	: 0
c decisions	: 4622703
c propagations	: 4773560
c inspects	: 486594
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=1476395008
c Current CPU time (ms) : 648.247
c starts	: 191
c conflicts	: 0
c decisions	: 4647033
c propagations	: 4798684
c inspects	: 489018
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=1476395008
c Current CPU time (ms) : 650.647
c starts	: 192
c conflicts	: 0
c decisions	: 4671363
c propagations	: 4823808
c inspects	: 491447
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=1476395008
c Current CPU time (ms) : 653.133
c starts	: 193
c conflicts	: 0
c decisions	: 4695693
c propagations	: 4848932
c inspects	: 493876
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=1476395008
c Current CPU time (ms) : 655.542
c starts	: 194
c conflicts	: 0
c decisions	: 4720023
c propagations	: 4874056
c inspects	: 496302
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=1476395008
c Current CPU time (ms) : 657.987
c starts	: 195
c conflicts	: 0
c decisions	: 4744353
c propagations	: 4899180
c inspects	: 498734
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=1476395008
c Current CPU time (ms) : 660.49
c starts	: 196
c conflicts	: 0
c decisions	: 4768683
c propagations	: 4924304
c inspects	: 501162
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=1476395008
c Current CPU time (ms) : 662.933
c starts	: 197
c conflicts	: 0
c decisions	: 4793013
c propagations	: 4949428
c inspects	: 503589
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=1476395008
c Current CPU time (ms) : 665.291
c starts	: 198
c conflicts	: 0
c decisions	: 4817343
c propagations	: 4974552
c inspects	: 506016
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=1476395008
c Current CPU time (ms) : 667.703
c starts	: 199
c conflicts	: 0
c decisions	: 4841673
c propagations	: 4999676
c inspects	: 508442
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=1476395008
c Current CPU time (ms) : 670.142
c starts	: 200
c conflicts	: 0
c decisions	: 4866003
c propagations	: 5024800
c inspects	: 510869
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=1476395008
c Current CPU time (ms) : 672.648
c starts	: 201
c conflicts	: 0
c decisions	: 4890333
c propagations	: 5049924
c inspects	: 513299
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=1476395008
c Current CPU time (ms) : 675.005
c starts	: 202
c conflicts	: 0
c decisions	: 4914663
c propagations	: 5075048
c inspects	: 515727
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=1476395008
c Current CPU time (ms) : 677.452
c starts	: 203
c conflicts	: 0
c decisions	: 4938993
c propagations	: 5100172
c inspects	: 518150
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=1476395008
c Current CPU time (ms) : 679.953
c starts	: 204
c conflicts	: 0
c decisions	: 4963323
c propagations	: 5125296
c inspects	: 520577
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=1476395008
c Current CPU time (ms) : 682.392
c starts	: 205
c conflicts	: 0
c decisions	: 4987653
c propagations	: 5150420
c inspects	: 523006
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=1476395008
c Current CPU time (ms) : 684.899
c starts	: 206
c conflicts	: 0
c decisions	: 5011983
c propagations	: 5175544
c inspects	: 525432
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=1476395008
c Current CPU time (ms) : 687.324
c starts	: 207
c conflicts	: 0
c decisions	: 5036313
c propagations	: 5200668
c inspects	: 527862
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=1476395008
c Current CPU time (ms) : 689.734
c starts	: 208
c conflicts	: 0
c decisions	: 5060643
c propagations	: 5225792
c inspects	: 530291
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=1476395008
c Current CPU time (ms) : 692.213
c starts	: 209
c conflicts	: 0
c decisions	: 5084973
c propagations	: 5250916
c inspects	: 532718
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=1476395008
c Current CPU time (ms) : 694.633
c starts	: 210
c conflicts	: 0
c decisions	: 5109303
c propagations	: 5276040
c inspects	: 535148
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=1476395008
c Current CPU time (ms) : 696.968
c starts	: 211
c conflicts	: 0
c decisions	: 5133633
c propagations	: 5301164
c inspects	: 537577
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=1476395008
c Current CPU time (ms) : 699.443
c starts	: 212
c conflicts	: 0
c decisions	: 5157963
c propagations	: 5326288
c inspects	: 540005
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=1476395008
c Current CPU time (ms) : 701.874
c starts	: 213
c conflicts	: 0
c decisions	: 5182293
c propagations	: 5351412
c inspects	: 542434
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=1476395008
c Current CPU time (ms) : 704.348
c starts	: 214
c conflicts	: 0
c decisions	: 5206623
c propagations	: 5376536
c inspects	: 544860
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=1476395008
c Current CPU time (ms) : 706.675
c starts	: 215
c conflicts	: 0
c decisions	: 5230953
c propagations	: 5401660
c inspects	: 547288
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=1476395008
c Current CPU time (ms) : 709.008
c starts	: 216
c conflicts	: 0
c decisions	: 5255283
c propagations	: 5426784
c inspects	: 549717
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=1476395008
c Current CPU time (ms) : 711.481
c starts	: 217
c conflicts	: 0
c decisions	: 5279613
c propagations	: 5451908
c inspects	: 552145
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=1476395008
c Current CPU time (ms) : 713.899
c starts	: 218
c conflicts	: 0
c decisions	: 5303943
c propagations	: 5477032
c inspects	: 554575
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=1476395008
c Current CPU time (ms) : 716.371
c starts	: 219
c conflicts	: 0
c decisions	: 5328273
c propagations	: 5502156
c inspects	: 557005
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=1476395008
c Current CPU time (ms) : 718.696
c starts	: 220
c conflicts	: 0
c decisions	: 5352603
c propagations	: 5527280
c inspects	: 559433
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=1476395008
c Current CPU time (ms) : 721.053
c starts	: 221
c conflicts	: 0
c decisions	: 5376933
c propagations	: 5552404
c inspects	: 561863
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=1476395008
c Current CPU time (ms) : 723.525
c starts	: 222
c conflicts	: 0
c decisions	: 5401263
c propagations	: 5577528
c inspects	: 564292
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=1476395008
c Current CPU time (ms) : 725.954
c starts	: 223
c conflicts	: 0
c decisions	: 5425593
c propagations	: 5602652
c inspects	: 566718
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=1476395008
c Current CPU time (ms) : 728.296
c starts	: 224
c conflicts	: 0
c decisions	: 5449923
c propagations	: 5627776
c inspects	: 569148
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=1476395008
c Current CPU time (ms) : 730.673
c starts	: 225
c conflicts	: 0
c decisions	: 5474253
c propagations	: 5652900
c inspects	: 571578
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=1476395008
c Current CPU time (ms) : 733.021
c starts	: 226
c conflicts	: 0
c decisions	: 5498583
c propagations	: 5678024
c inspects	: 574007
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=1476395008
c Current CPU time (ms) : 735.504
c starts	: 227
c conflicts	: 0
c decisions	: 5522913
c propagations	: 5703148
c inspects	: 576436
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=1476395008
c Current CPU time (ms) : 737.872
c starts	: 228
c conflicts	: 0
c decisions	: 5547243
c propagations	: 5728272
c inspects	: 578864
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=1476395008
c Current CPU time (ms) : 740.334
c starts	: 229
c conflicts	: 0
c decisions	: 5571573
c propagations	: 5753396
c inspects	: 581294
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=1476395008
c Current CPU time (ms) : 742.802
c starts	: 230
c conflicts	: 0
c decisions	: 5595903
c propagations	: 5778520
c inspects	: 583725
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=1476395008
c Current CPU time (ms) : 745.228
c starts	: 231
c conflicts	: 0
c decisions	: 5620233
c propagations	: 5803644
c inspects	: 586156
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=1476395008
c Current CPU time (ms) : 747.613
c starts	: 232
c conflicts	: 0
c decisions	: 5644563
c propagations	: 5828768
c inspects	: 588587
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=1476395008
c Current CPU time (ms) : 749.98
c starts	: 233
c conflicts	: 0
c decisions	: 5668893
c propagations	: 5853892
c inspects	: 591015
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=1476395008
c Current CPU time (ms) : 752.404
c starts	: 234
c conflicts	: 0
c decisions	: 5693223
c propagations	: 5879016
c inspects	: 593444
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=1476395008
c Current CPU time (ms) : 754.78
c starts	: 235
c conflicts	: 0
c decisions	: 5717553
c propagations	: 5904140
c inspects	: 595871
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=1476395008
c Current CPU time (ms) : 757.118
c starts	: 236
c conflicts	: 0
c decisions	: 5741883
c propagations	: 5929264
c inspects	: 598299
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=1476395008
c Current CPU time (ms) : 759.454
c starts	: 237
c conflicts	: 0
c decisions	: 5766213
c propagations	: 5954388
c inspects	: 600728
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=1476395008
c Current CPU time (ms) : 761.828
c starts	: 238
c conflicts	: 0
c decisions	: 5790543
c propagations	: 5979512
c inspects	: 603156
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=1476395008
c Current CPU time (ms) : 764.18
c starts	: 239
c conflicts	: 0
c decisions	: 5814873
c propagations	: 6004636
c inspects	: 605586
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=1476395008
c Current CPU time (ms) : 766.559
c starts	: 240
c conflicts	: 0
c decisions	: 5839203
c propagations	: 6029760
c inspects	: 608013
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=1476395008
c Current CPU time (ms) : 768.919
c starts	: 241
c conflicts	: 0
c decisions	: 5863533
c propagations	: 6054884
c inspects	: 610439
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=1476395008
c Current CPU time (ms) : 771.267
c starts	: 242
c conflicts	: 0
c decisions	: 5887863
c propagations	: 6080008
c inspects	: 612866
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=1476395008
c Current CPU time (ms) : 773.752
c starts	: 243
c conflicts	: 0
c decisions	: 5912193
c propagations	: 6105132
c inspects	: 615291
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=1476395008
c Current CPU time (ms) : 776.179
c starts	: 244
c conflicts	: 0
c decisions	: 5936523
c propagations	: 6130256
c inspects	: 617719
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=1476395008
c Current CPU time (ms) : 778.58
c starts	: 245
c conflicts	: 0
c decisions	: 5960853
c propagations	: 6155380
c inspects	: 620148
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=1476395008
c Current CPU time (ms) : 780.944
c starts	: 246
c conflicts	: 0
c decisions	: 5985183
c propagations	: 6180504
c inspects	: 622577
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=1476395008
c Current CPU time (ms) : 783.373
c starts	: 247
c conflicts	: 0
c decisions	: 6009513
c propagations	: 6205628
c inspects	: 625003
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=1476395008
c Current CPU time (ms) : 785.847
c starts	: 248
c conflicts	: 0
c decisions	: 6033843
c propagations	: 6230752
c inspects	: 627429
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=1476395008
c Current CPU time (ms) : 788.277
c starts	: 249
c conflicts	: 0
c decisions	: 6058173
c propagations	: 6255876
c inspects	: 629856
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=1476395008
c Current CPU time (ms) : 790.702
c starts	: 250
c conflicts	: 0
c decisions	: 6082503
c propagations	: 6281000
c inspects	: 632284
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=1476395008
c Current CPU time (ms) : 793.182
c starts	: 251
c conflicts	: 0
c decisions	: 6106833
c propagations	: 6306124
c inspects	: 634711
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=1476395008
c Current CPU time (ms) : 795.542
c starts	: 252
c conflicts	: 0
c decisions	: 6131163
c propagations	: 6331248
c inspects	: 637138
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=1476395008
c Current CPU time (ms) : 798.023
c starts	: 253
c conflicts	: 0
c decisions	: 6155493
c propagations	: 6356372
c inspects	: 639569
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=1476395008
c Current CPU time (ms) : 800.441
c starts	: 254
c conflicts	: 0
c decisions	: 6179823
c propagations	: 6381496
c inspects	: 641997
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=1476395008
c Current CPU time (ms) : 802.823
c starts	: 255
c conflicts	: 0
c decisions	: 6204153
c propagations	: 6406620
c inspects	: 644426
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=1476395008
c Current CPU time (ms) : 806.08
c starts	: 256
c conflicts	: 0
c decisions	: 6228483
c propagations	: 6431744
c inspects	: 646857
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=1476395008
c Current CPU time (ms) : 808.526
c starts	: 257
c conflicts	: 0
c decisions	: 6252813
c propagations	: 6456868
c inspects	: 649284
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=1476395008
c Current CPU time (ms) : 811.021
c starts	: 258
c conflicts	: 0
c decisions	: 6277143
c propagations	: 6481992
c inspects	: 651716
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=1476395008
c Current CPU time (ms) : 813.416
c starts	: 259
c conflicts	: 0
c decisions	: 6301473
c propagations	: 6507116
c inspects	: 654144
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=1476395008
c Current CPU time (ms) : 815.796
c starts	: 260
c conflicts	: 0
c decisions	: 6325803
c propagations	: 6532240
c inspects	: 656573
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=1476395008
c Current CPU time (ms) : 818.329
c starts	: 261
c conflicts	: 0
c decisions	: 6350133
c propagations	: 6557364
c inspects	: 658999
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=1476395008
c Current CPU time (ms) : 820.791
c starts	: 262
c conflicts	: 0
c decisions	: 6374463
c propagations	: 6582488
c inspects	: 661427
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=1476395008
c Current CPU time (ms) : 823.229
c starts	: 263
c conflicts	: 0
c decisions	: 6398793
c propagations	: 6607612
c inspects	: 663857
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=1476395008
c Current CPU time (ms) : 825.738
c starts	: 264
c conflicts	: 0
c decisions	: 6423123
c propagations	: 6632736
c inspects	: 666287
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=1476395008
c Current CPU time (ms) : 828.128
c starts	: 265
c conflicts	: 0
c decisions	: 6447453
c propagations	: 6657860
c inspects	: 668719
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=1476395008
c Current CPU time (ms) : 830.656
c starts	: 266
c conflicts	: 0
c decisions	: 6471783
c propagations	: 6682984
c inspects	: 671143
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=1476395008
c Current CPU time (ms) : 833.06
c starts	: 267
c conflicts	: 0
c decisions	: 6496113
c propagations	: 6708108
c inspects	: 673569
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=1476395008
c Current CPU time (ms) : 835.497
c starts	: 268
c conflicts	: 0
c decisions	: 6520443
c propagations	: 6733232
c inspects	: 675996
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=1476395008
c Current CPU time (ms) : 837.902
c starts	: 269
c conflicts	: 0
c decisions	: 6544773
c propagations	: 6758356
c inspects	: 678420
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=1476395008
c Current CPU time (ms) : 840.365
c starts	: 270
c conflicts	: 0
c decisions	: 6569103
c propagations	: 6783480
c inspects	: 680848
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=1476395008
c Current CPU time (ms) : 842.868
c starts	: 271
c conflicts	: 0
c decisions	: 6593433
c propagations	: 6808604
c inspects	: 683277
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=1476395008
c Current CPU time (ms) : 845.225
c starts	: 272
c conflicts	: 0
c decisions	: 6617763
c propagations	: 6833728
c inspects	: 685706
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=1476395008
c Current CPU time (ms) : 847.593
c starts	: 273
c conflicts	: 0
c decisions	: 6642093
c propagations	: 6858852
c inspects	: 688135
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=1476395008
c Current CPU time (ms) : 849.995
c starts	: 274
c conflicts	: 0
c decisions	: 6666423
c propagations	: 6883976
c inspects	: 690566
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=1476395008
c Current CPU time (ms) : 852.369
c starts	: 275
c conflicts	: 0
c decisions	: 6690753
c propagations	: 6909100
c inspects	: 692995
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=1476395008
c Current CPU time (ms) : 854.775
c starts	: 276
c conflicts	: 0
c decisions	: 6715083
c propagations	: 6934224
c inspects	: 695424
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=1476395008
c Current CPU time (ms) : 857.157
c starts	: 277
c conflicts	: 0
c decisions	: 6739413
c propagations	: 6959348
c inspects	: 697852
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=1476395008
c Current CPU time (ms) : 859.602
c starts	: 278
c conflicts	: 0
c decisions	: 6763743
c propagations	: 6984472
c inspects	: 700283
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=1476395008
c Current CPU time (ms) : 862.013
c starts	: 279
c conflicts	: 0
c decisions	: 6788073
c propagations	: 7009596
c inspects	: 702710
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=1476395008
c Current CPU time (ms) : 864.381
c starts	: 280
c conflicts	: 0
c decisions	: 6812403
c propagations	: 7034720
c inspects	: 705135
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=1476395008
c Current CPU time (ms) : 866.791
c starts	: 281
c conflicts	: 0
c decisions	: 6836733
c propagations	: 7059844
c inspects	: 707562
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=1476395008
c Current CPU time (ms) : 869.166
c starts	: 282
c conflicts	: 0
c decisions	: 6861063
c propagations	: 7084968
c inspects	: 709987
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=1476395008
c Current CPU time (ms) : 871.539
c starts	: 283
c conflicts	: 0
c decisions	: 6885393
c propagations	: 7110092
c inspects	: 712415
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=1476395008
c Current CPU time (ms) : 874.032
c starts	: 284
c conflicts	: 0
c decisions	: 6909723
c propagations	: 7135216
c inspects	: 714843
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=1476395008
c Current CPU time (ms) : 876.456
c starts	: 285
c conflicts	: 0
c decisions	: 6934053
c propagations	: 7160340
c inspects	: 717272
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=1476395008
c Current CPU time (ms) : 878.819
c starts	: 286
c conflicts	: 0
c decisions	: 6958383
c propagations	: 7185464
c inspects	: 719699
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=1476395008
c Current CPU time (ms) : 881.319
c starts	: 287
c conflicts	: 0
c decisions	: 6982713
c propagations	: 7210588
c inspects	: 722129
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=1476395008
c Current CPU time (ms) : 883.76
c starts	: 288
c conflicts	: 0
c decisions	: 7007043
c propagations	: 7235712
c inspects	: 724557
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=1476395008
c Current CPU time (ms) : 886.162
c starts	: 289
c conflicts	: 0
c decisions	: 7031373
c propagations	: 7260836
c inspects	: 726985
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=1476395008
c Current CPU time (ms) : 888.641
c starts	: 290
c conflicts	: 0
c decisions	: 7055703
c propagations	: 7285960
c inspects	: 729416
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=1476395008
c Current CPU time (ms) : 891.087
c starts	: 291
c conflicts	: 0
c decisions	: 7080033
c propagations	: 7311084
c inspects	: 731842
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=1476395008
c Current CPU time (ms) : 893.586
c starts	: 292
c conflicts	: 0
c decisions	: 7104363
c propagations	: 7336208
c inspects	: 734271
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=1476395008
c Current CPU time (ms) : 895.935
c starts	: 293
c conflicts	: 0
c decisions	: 7128693
c propagations	: 7361332
c inspects	: 736699
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=1476395008
c Current CPU time (ms) : 898.336
c starts	: 294
c conflicts	: 0
c decisions	: 7153023
c propagations	: 7386456
c inspects	: 739128
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=1476395008
c Current CPU time (ms) : 900.719
c starts	: 295
c conflicts	: 0
c decisions	: 7177353
c propagations	: 7411580
c inspects	: 741557
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=1476395008
c Current CPU time (ms) : 903.084
c starts	: 296
c conflicts	: 0
c decisions	: 7201683
c propagations	: 7436704
c inspects	: 743985
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=1476395008
c Current CPU time (ms) : 905.489
c starts	: 297
c conflicts	: 0
c decisions	: 7226013
c propagations	: 7461828
c inspects	: 746414
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=1476395008
c Current CPU time (ms) : 907.862
c starts	: 298
c conflicts	: 0
c decisions	: 7250343
c propagations	: 7486952
c inspects	: 748842
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=1476395008
c Current CPU time (ms) : 910.232
c starts	: 299
c conflicts	: 0
c decisions	: 7274673
c propagations	: 7512076
c inspects	: 751272
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=1476395008
c Current CPU time (ms) : 912.731
c starts	: 300
c conflicts	: 0
c decisions	: 7299003
c propagations	: 7537200
c inspects	: 753700
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=1476395008
c Current CPU time (ms) : 915.183
c starts	: 301
c conflicts	: 0
c decisions	: 7323333
c propagations	: 7562324
c inspects	: 756126
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=1476395008
c Current CPU time (ms) : 917.696
c starts	: 302
c conflicts	: 0
c decisions	: 7347663
c propagations	: 7587448
c inspects	: 758555
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=1476395008
c Current CPU time (ms) : 920.048
c starts	: 303
c conflicts	: 0
c decisions	: 7371993
c propagations	: 7612572
c inspects	: 760984
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=1476395008
c Current CPU time (ms) : 922.412
c starts	: 304
c conflicts	: 0
c decisions	: 7396323
c propagations	: 7637696
c inspects	: 763412
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=1476395008
c Current CPU time (ms) : 924.817
c starts	: 305
c conflicts	: 0
c decisions	: 7420653
c propagations	: 7662820
c inspects	: 765842
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=1476395008
c Current CPU time (ms) : 927.248
c starts	: 306
c conflicts	: 0
c decisions	: 7444983
c propagations	: 7687944
c inspects	: 768271
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=1476395008
c Current CPU time (ms) : 929.774
c starts	: 307
c conflicts	: 0
c decisions	: 7469313
c propagations	: 7713068
c inspects	: 770701
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=1476395008
c Current CPU time (ms) : 932.221
c starts	: 308
c conflicts	: 0
c decisions	: 7493643
c propagations	: 7738192
c inspects	: 773129
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=1476395008
c Current CPU time (ms) : 934.669
c starts	: 309
c conflicts	: 0
c decisions	: 7517973
c propagations	: 7763316
c inspects	: 775556
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=1476395008
c Current CPU time (ms) : 937.084
c starts	: 310
c conflicts	: 0
c decisions	: 7542303
c propagations	: 7788440
c inspects	: 777984
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=1476395008
c Current CPU time (ms) : 939.472
c starts	: 311
c conflicts	: 0
c decisions	: 7566633
c propagations	: 7813564
c inspects	: 780413
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=1476395008
c Current CPU time (ms) : 941.845
c starts	: 312
c conflicts	: 0
c decisions	: 7590963
c propagations	: 7838688
c inspects	: 782842
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=1476395008
c Current CPU time (ms) : 944.261
c starts	: 313
c conflicts	: 0
c decisions	: 7615293
c propagations	: 7863812
c inspects	: 785270
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=1476395008
c Current CPU time (ms) : 946.633
c starts	: 314
c conflicts	: 0
c decisions	: 7639623
c propagations	: 7888936
c inspects	: 787700
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=1476395008
c Current CPU time (ms) : 949.152
c starts	: 315
c conflicts	: 0
c decisions	: 7663953
c propagations	: 7914060
c inspects	: 790129
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=1476395008
c Current CPU time (ms) : 951.613
c starts	: 316
c conflicts	: 0
c decisions	: 7688283
c propagations	: 7939184
c inspects	: 792556
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=1476395008
c Current CPU time (ms) : 953.975
c starts	: 317
c conflicts	: 0
c decisions	: 7712613
c propagations	: 7964308
c inspects	: 794983
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=1476395008
c Current CPU time (ms) : 956.388
c starts	: 318
c conflicts	: 0
c decisions	: 7736943
c propagations	: 7989432
c inspects	: 797410
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=1476395008
c Current CPU time (ms) : 958.767
c starts	: 319
c conflicts	: 0
c decisions	: 7761273
c propagations	: 8014556
c inspects	: 799839
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=1476395008
c Current CPU time (ms) : 961.285
c starts	: 320
c conflicts	: 0
c decisions	: 7785603
c propagations	: 8039680
c inspects	: 802265
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=1476395008
c Current CPU time (ms) : 963.662
c starts	: 321
c conflicts	: 0
c decisions	: 7809933
c propagations	: 8064804
c inspects	: 804694
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=1476395008
c Current CPU time (ms) : 966.019
c starts	: 322
c conflicts	: 0
c decisions	: 7834263
c propagations	: 8089928
c inspects	: 807121
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=1476395008
c Current CPU time (ms) : 968.525
c starts	: 323
c conflicts	: 0
c decisions	: 7858593
c propagations	: 8115052
c inspects	: 809552
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=1476395008
c Current CPU time (ms) : 970.983
c starts	: 324
c conflicts	: 0
c decisions	: 7882923
c propagations	: 8140176
c inspects	: 811979
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=1476395008
c Current CPU time (ms) : 973.44
c starts	: 325
c conflicts	: 0
c decisions	: 7907253
c propagations	: 8165300
c inspects	: 814406
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=1476395008
c Current CPU time (ms) : 975.949
c starts	: 326
c conflicts	: 0
c decisions	: 7931583
c propagations	: 8190424
c inspects	: 816834
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=1476395008
c Current CPU time (ms) : 978.406
c starts	: 327
c conflicts	: 0
c decisions	: 7955913
c propagations	: 8215548
c inspects	: 819264
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=1476395008
c Current CPU time (ms) : 980.914
c starts	: 328
c conflicts	: 0
c decisions	: 7980243
c propagations	: 8240672
c inspects	: 821692
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=1476395008
c Current CPU time (ms) : 983.362
c starts	: 329
c conflicts	: 0
c decisions	: 8004573
c propagations	: 8265796
c inspects	: 824120
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=1476395008
c Current CPU time (ms) : 985.816
c starts	: 330
c conflicts	: 0
c decisions	: 8028903
c propagations	: 8290920
c inspects	: 826549
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=1476395008
c Current CPU time (ms) : 988.232
c starts	: 331
c conflicts	: 0
c decisions	: 8053233
c propagations	: 8316044
c inspects	: 828978
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=1476395008
c Current CPU time (ms) : 990.611
c starts	: 332
c conflicts	: 0
c decisions	: 8077563
c propagations	: 8341168
c inspects	: 831408
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=1476395008
c Current CPU time (ms) : 993.031
c starts	: 333
c conflicts	: 0
c decisions	: 8101893
c propagations	: 8366292
c inspects	: 833835
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=1476395008
c Current CPU time (ms) : 995.4
c starts	: 334
c conflicts	: 0
c decisions	: 8126223
c propagations	: 8391416
c inspects	: 836266
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=1476395008
c Current CPU time (ms) : 997.782
c starts	: 335
c conflicts	: 0
c decisions	: 8150553
c propagations	: 8416540
c inspects	: 838696
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=1476395008
c Current CPU time (ms) : 1000.179
c starts	: 336
c conflicts	: 0
c decisions	: 8174883
c propagations	: 8441664
c inspects	: 841123
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=1476395008
c Current CPU time (ms) : 1002.565
c starts	: 337
c conflicts	: 0
c decisions	: 8199213
c propagations	: 8466788
c inspects	: 843553
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=1476395008
c Current CPU time (ms) : 1005.027
c starts	: 338
c conflicts	: 0
c decisions	: 8223543
c propagations	: 8491912
c inspects	: 845980
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=1476395008
c Current CPU time (ms) : 1007.435
c starts	: 339
c conflicts	: 0
c decisions	: 8247873
c propagations	: 8517036
c inspects	: 848407
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=1476395008
c Current CPU time (ms) : 1009.816
c starts	: 340
c conflicts	: 0
c decisions	: 8272203
c propagations	: 8542160
c inspects	: 850835
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=1476395008
c Current CPU time (ms) : 1012.234
c starts	: 341
c conflicts	: 0
c decisions	: 8296533
c propagations	: 8567284
c inspects	: 853262
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=1476395008
c Current CPU time (ms) : 1014.583
c starts	: 342
c conflicts	: 0
c decisions	: 8320863
c propagations	: 8592408
c inspects	: 855689
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=1476395008
c Current CPU time (ms) : 1016.963
c starts	: 343
c conflicts	: 0
c decisions	: 8345193
c propagations	: 8617532
c inspects	: 858119
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=1476395008
c Current CPU time (ms) : 1019.371
c starts	: 344
c conflicts	: 0
c decisions	: 8369523
c propagations	: 8642656
c inspects	: 860549
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=1476395008
c Current CPU time (ms) : 1021.766
c starts	: 345
c conflicts	: 0
c decisions	: 8393853
c propagations	: 8667780
c inspects	: 862975
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=1476395008
c Current CPU time (ms) : 1024.276
c starts	: 346
c conflicts	: 0
c decisions	: 8418183
c propagations	: 8692904
c inspects	: 865404
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=1476395008
c Current CPU time (ms) : 1026.659
c starts	: 347
c conflicts	: 0
c decisions	: 8442513
c propagations	: 8718028
c inspects	: 867833
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 347
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1029.035
c starts	: 348
c conflicts	: 0
c decisions	: 8466843
c propagations	: 8743152
c inspects	: 870260
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 348
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1031.535
c starts	: 349
c conflicts	: 0
c decisions	: 8491173
c propagations	: 8768276
c inspects	: 872687
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 349
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1033.928
c starts	: 350
c conflicts	: 0
c decisions	: 8515503
c propagations	: 8793400
c inspects	: 875114
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 350
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1036.385
c starts	: 351
c conflicts	: 0
c decisions	: 8539833
c propagations	: 8818524
c inspects	: 877542
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 351
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1038.802
c starts	: 352
c conflicts	: 0
c decisions	: 8564163
c propagations	: 8843648
c inspects	: 879968
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 352
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1041.19
c starts	: 353
c conflicts	: 0
c decisions	: 8588493
c propagations	: 8868772
c inspects	: 882397
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 353
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1043.61
c starts	: 354
c conflicts	: 0
c decisions	: 8612823
c propagations	: 8893896
c inspects	: 884827
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 354
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1046.001
c starts	: 355
c conflicts	: 0
c decisions	: 8637153
c propagations	: 8919020
c inspects	: 887256
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 355
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1048.48
c starts	: 356
c conflicts	: 0
c decisions	: 8661483
c propagations	: 8944144
c inspects	: 889683
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 356
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1050.904
c starts	: 357
c conflicts	: 0
c decisions	: 8685813
c propagations	: 8969268
c inspects	: 892112
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 357
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1053.358
c starts	: 358
c conflicts	: 0
c decisions	: 8710143
c propagations	: 8994392
c inspects	: 894539
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 358
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1055.866
c starts	: 359
c conflicts	: 0
c decisions	: 8734473
c propagations	: 9019516
c inspects	: 896967
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 359
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1058.26
c starts	: 360
c conflicts	: 0
c decisions	: 8758803
c propagations	: 9044640
c inspects	: 899395
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 360
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1060.65
c starts	: 361
c conflicts	: 0
c decisions	: 8783133
c propagations	: 9069764
c inspects	: 901825
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 361
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1063.153
c starts	: 362
c conflicts	: 0
c decisions	: 8807463
c propagations	: 9094888
c inspects	: 904253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 362
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1065.616
c starts	: 363
c conflicts	: 0
c decisions	: 8831793
c propagations	: 9120012
c inspects	: 906682
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 363
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1068.075
c starts	: 364
c conflicts	: 0
c decisions	: 8856123
c propagations	: 9145136
c inspects	: 909109
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 364
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1070.593
c starts	: 365
c conflicts	: 0
c decisions	: 8880453
c propagations	: 9170260
c inspects	: 911539
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 365
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1073.037
c starts	: 366
c conflicts	: 0
c decisions	: 8904783
c propagations	: 9195384
c inspects	: 913965
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 366
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1075.461
c starts	: 367
c conflicts	: 0
c decisions	: 8929113
c propagations	: 9220508
c inspects	: 916394
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 367
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1077.921
c starts	: 368
c conflicts	: 0
c decisions	: 8953443
c propagations	: 9245632
c inspects	: 918824
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 368
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1080.389
c starts	: 369
c conflicts	: 0
c decisions	: 8977773
c propagations	: 9270756
c inspects	: 921253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 369
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1082.799
c starts	: 370
c conflicts	: 0
c decisions	: 9002103
c propagations	: 9295880
c inspects	: 923681
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 370
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1085.265
c starts	: 371
c conflicts	: 0
c decisions	: 9026433
c propagations	: 9321004
c inspects	: 926112
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 371
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1087.777
c starts	: 372
c conflicts	: 0
c decisions	: 9050763
c propagations	: 9346128
c inspects	: 928541
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 372
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1090.242
c starts	: 373
c conflicts	: 0
c decisions	: 9075093
c propagations	: 9371252
c inspects	: 930966
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 373
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1092.702
c starts	: 374
c conflicts	: 0
c decisions	: 9099423
c propagations	: 9396376
c inspects	: 933396
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 374
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1095.218
c starts	: 375
c conflicts	: 0
c decisions	: 9123753
c propagations	: 9421500
c inspects	: 935826
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 375
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1097.671
c starts	: 376
c conflicts	: 0
c decisions	: 9148083
c propagations	: 9446624
c inspects	: 938253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 376
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1100.14
c starts	: 377
c conflicts	: 0
c decisions	: 9172413
c propagations	: 9471748
c inspects	: 940682
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 377
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1102.55
c starts	: 378
c conflicts	: 0
c decisions	: 9196743
c propagations	: 9496872
c inspects	: 943108
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 378
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1104.943
c starts	: 379
c conflicts	: 0
c decisions	: 9221073
c propagations	: 9521996
c inspects	: 945537
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 379
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1107.361
c starts	: 380
c conflicts	: 0
c decisions	: 9245403
c propagations	: 9547120
c inspects	: 947965
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 380
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1109.762
c starts	: 381
c conflicts	: 0
c decisions	: 9269733
c propagations	: 9572244
c inspects	: 950393
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 381
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1112.138
c starts	: 382
c conflicts	: 0
c decisions	: 9294063
c propagations	: 9597368
c inspects	: 952819
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 382
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1114.652
c starts	: 383
c conflicts	: 0
c decisions	: 9318393
c propagations	: 9622492
c inspects	: 955249
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 383
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1117.113
c starts	: 384
c conflicts	: 0
c decisions	: 9342723
c propagations	: 9647616
c inspects	: 957677
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 384
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1119.683
c starts	: 385
c conflicts	: 0
c decisions	: 9367053
c propagations	: 9672740
c inspects	: 960106
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 385
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1122.171
c starts	: 386
c conflicts	: 0
c decisions	: 9391383
c propagations	: 9697864
c inspects	: 962533
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 386
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1124.618
c starts	: 387
c conflicts	: 0
c decisions	: 9415713
c propagations	: 9722988
c inspects	: 964962
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 387
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1127.074
c starts	: 388
c conflicts	: 0
c decisions	: 9440043
c propagations	: 9748112
c inspects	: 967388
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 388
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1129.425
c starts	: 389
c conflicts	: 0
c decisions	: 9464373
c propagations	: 9773236
c inspects	: 969816
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 389
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1131.894
c starts	: 390
c conflicts	: 0
c decisions	: 9488703
c propagations	: 9798360
c inspects	: 972244
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 390
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1134.247
c starts	: 391
c conflicts	: 0
c decisions	: 9513033
c propagations	: 9823484
c inspects	: 974673
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 391
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1136.696
c starts	: 392
c conflicts	: 0
c decisions	: 9537363
c propagations	: 9848608
c inspects	: 977101
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 392
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1139.206
c starts	: 393
c conflicts	: 0
c decisions	: 9561693
c propagations	: 9873732
c inspects	: 979527
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 393
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1141.586
c starts	: 394
c conflicts	: 0
c decisions	: 9586023
c propagations	: 9898856
c inspects	: 981954
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 394
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1144.058
c starts	: 395
c conflicts	: 0
c decisions	: 9610353
c propagations	: 9923980
c inspects	: 984378
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 395
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1146.494
c starts	: 396
c conflicts	: 0
c decisions	: 9634683
c propagations	: 9949104
c inspects	: 986806
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 396
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1148.98
c starts	: 397
c conflicts	: 0
c decisions	: 9659013
c propagations	: 9974228
c inspects	: 989235
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 397
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1151.522
c starts	: 398
c conflicts	: 0
c decisions	: 9683343
c propagations	: 9999352
c inspects	: 991662
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 398
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1153.991
c starts	: 399
c conflicts	: 0
c decisions	: 9707673
c propagations	: 10024476
c inspects	: 994089
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 399
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1156.46
c starts	: 400
c conflicts	: 0
c decisions	: 9732003
c propagations	: 10049600
c inspects	: 996519
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 400
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1158.989
c starts	: 401
c conflicts	: 0
c decisions	: 9756333
c propagations	: 10074724
c inspects	: 998945
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 401
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1161.368
c starts	: 402
c conflicts	: 0
c decisions	: 9780663
c propagations	: 10099848
c inspects	: 1001373
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 402
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1163.798
c starts	: 403
c conflicts	: 0
c decisions	: 9804993
c propagations	: 10124972
c inspects	: 1003801
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 403
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1166.263
c starts	: 404
c conflicts	: 0
c decisions	: 9829323
c propagations	: 10150096
c inspects	: 1006227
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 404
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1168.734
c starts	: 405
c conflicts	: 0
c decisions	: 9853653
c propagations	: 10175220
c inspects	: 1008658
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 405
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1171.242
c starts	: 406
c conflicts	: 0
c decisions	: 9877983
c propagations	: 10200344
c inspects	: 1011084
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 406
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1173.713
c starts	: 407
c conflicts	: 0
c decisions	: 9902313
c propagations	: 10225468
c inspects	: 1013511
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 407
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1176.185
c starts	: 408
c conflicts	: 0
c decisions	: 9926643
c propagations	: 10250592
c inspects	: 1015941
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 408
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1178.607
c starts	: 409
c conflicts	: 0
c decisions	: 9950973
c propagations	: 10275716
c inspects	: 1018368
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 409
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1180.984
c starts	: 410
c conflicts	: 0
c decisions	: 9975303
c propagations	: 10300840
c inspects	: 1020797
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 410
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1183.414
c starts	: 411
c conflicts	: 0
c decisions	: 9999633
c propagations	: 10325964
c inspects	: 1023224
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 411
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1185.814
c starts	: 412
c conflicts	: 0
c decisions	: 10023963
c propagations	: 10351088
c inspects	: 1025652
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 412
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1188.206
c starts	: 413
c conflicts	: 0
c decisions	: 10048293
c propagations	: 10376212
c inspects	: 1028081
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 413
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1190.621
c starts	: 414
c conflicts	: 0
c decisions	: 10072623
c propagations	: 10401336
c inspects	: 1030508
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 414
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1193.096
c starts	: 415
c conflicts	: 0
c decisions	: 10096953
c propagations	: 10426460
c inspects	: 1032937
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 415
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1195.619
c starts	: 416
c conflicts	: 0
c decisions	: 10121283
c propagations	: 10451584
c inspects	: 1035362
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 416
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1197.993
c starts	: 417
c conflicts	: 0
c decisions	: 10145613
c propagations	: 10476708
c inspects	: 1037792
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 417
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1200.463
c starts	: 418
c conflicts	: 0
c decisions	: 10169943
c propagations	: 10501832
c inspects	: 1040220
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 418
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1202.992
c starts	: 419
c conflicts	: 0
c decisions	: 10194273
c propagations	: 10526956
c inspects	: 1042649
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 419
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1205.371
c starts	: 420
c conflicts	: 0
c decisions	: 10218603
c propagations	: 10552080
c inspects	: 1045077
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 420
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1207.849
c starts	: 421
c conflicts	: 0
c decisions	: 10242933
c propagations	: 10577204
c inspects	: 1047505
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 421
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1210.365
c starts	: 422
c conflicts	: 0
c decisions	: 10267263
c propagations	: 10602328
c inspects	: 1049932
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 422
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1212.838
c starts	: 423
c conflicts	: 0
c decisions	: 10291593
c propagations	: 10627452
c inspects	: 1052361
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 423
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1215.36
c starts	: 424
c conflicts	: 0
c decisions	: 10315923
c propagations	: 10652576
c inspects	: 1054788
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 424
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1217.835
c starts	: 425
c conflicts	: 0
c decisions	: 10340253
c propagations	: 10677700
c inspects	: 1057218
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 425
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1220.289
c starts	: 426
c conflicts	: 0
c decisions	: 10364583
c propagations	: 10702824
c inspects	: 1059645
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 426
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1222.818
c starts	: 427
c conflicts	: 0
c decisions	: 10388913
c propagations	: 10727948
c inspects	: 1062074
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 427
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1225.203
c starts	: 428
c conflicts	: 0
c decisions	: 10413243
c propagations	: 10753072
c inspects	: 1064502
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 428
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1227.643
c starts	: 429
c conflicts	: 0
c decisions	: 10437573
c propagations	: 10778196
c inspects	: 1066933
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 429
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1230.026
c starts	: 430
c conflicts	: 0
c decisions	: 10461903
c propagations	: 10803320
c inspects	: 1069361
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 430
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1232.505
c starts	: 431
c conflicts	: 0
c decisions	: 10486233
c propagations	: 10828444
c inspects	: 1071790
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 431
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1235.028
c starts	: 432
c conflicts	: 0
c decisions	: 10510563
c propagations	: 10853568
c inspects	: 1074221
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 432
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1237.417
c starts	: 433
c conflicts	: 0
c decisions	: 10534893
c propagations	: 10878692
c inspects	: 1076650
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 433
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1239.801
c starts	: 434
c conflicts	: 0
c decisions	: 10559223
c propagations	: 10903816
c inspects	: 1079078
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 434
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1242.332
c starts	: 435
c conflicts	: 0
c decisions	: 10583553
c propagations	: 10928940
c inspects	: 1081509
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 435
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1244.802
c starts	: 436
c conflicts	: 0
c decisions	: 10607883
c propagations	: 10954064
c inspects	: 1083937
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 436
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1247.24
c starts	: 437
c conflicts	: 0
c decisions	: 10632213
c propagations	: 10979188
c inspects	: 1086366
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 437
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1249.623
c starts	: 438
c conflicts	: 0
c decisions	: 10656543
c propagations	: 11004312
c inspects	: 1088794
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 438
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1251.994
c starts	: 439
c conflicts	: 0
c decisions	: 10680873
c propagations	: 11029436
c inspects	: 1091223
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 439
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1254.399
c starts	: 440
c conflicts	: 0
c decisions	: 10705203
c propagations	: 11054560
c inspects	: 1093651
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 440
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1256.765
c starts	: 441
c conflicts	: 0
c decisions	: 10729533
c propagations	: 11079684
c inspects	: 1096078
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 441
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1259.265
c starts	: 442
c conflicts	: 0
c decisions	: 10753863
c propagations	: 11104808
c inspects	: 1098507
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 442
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1261.718
c starts	: 443
c conflicts	: 0
c decisions	: 10778193
c propagations	: 11129932
c inspects	: 1100933
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 443
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1264.074
c starts	: 444
c conflicts	: 0
c decisions	: 10802523
c propagations	: 11155056
c inspects	: 1103362
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 444
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1266.579
c starts	: 445
c conflicts	: 0
c decisions	: 10826853
c propagations	: 11180180
c inspects	: 1105791
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 445
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1269.025
c starts	: 446
c conflicts	: 0
c decisions	: 10851183
c propagations	: 11205304
c inspects	: 1108219
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 446
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1271.468
c starts	: 447
c conflicts	: 0
c decisions	: 10875513
c propagations	: 11230428
c inspects	: 1110646
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 447
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1273.969
c starts	: 448
c conflicts	: 0
c decisions	: 10899843
c propagations	: 11255552
c inspects	: 1113076
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 448
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1276.426
c starts	: 449
c conflicts	: 0
c decisions	: 10924173
c propagations	: 11280676
c inspects	: 1115504
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 449
c 
c CURRENT OPTIMUM=1476395008
c Current CPU time (ms) : 1278.926
c starts	: 450
c conflicts	: 0
c decisions	: 10948503
c propagations	: 11305800
c inspects	: 1117932
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 450
#### 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.86 0.92 2/54 5674
Raw data (stat): 5674 (runsolver) R 5673 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544274526 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 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.0002 s]
Raw data (loadavg): 0.93 0.86 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18027 0 1 0 818 42 0 0 25 0 10 0 544274526 860413952 20839 4294967295 134512640 134569956 3221224400 3221214728 1131176513 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210062 20839 13073 16 0 210046 0
vsize: 840248
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.87 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 1699 42 0 0 25 0 10 0 544274526 859627520 21248 4294967295 134512640 134569956 3221224400 3221214820 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 21248 13073 16 0 209854 0
vsize: 839480
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.87 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 2573 42 0 0 25 0 10 0 544274526 859627520 21820 4294967295 134512640 134569956 3221224400 3221214832 1131313866 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209870 21820 13073 16 0 209854 0
vsize: 839480
[startup+40.0027 s]
Raw data (loadavg): 0.95 0.87 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 3481 43 0 0 25 0 10 0 544274526 859627520 22093 4294967295 134512640 134569956 3221224400 3221214724 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 22093 13073 16 0 209854 0
vsize: 839480
[startup+50.0085 s]
Raw data (loadavg): 0.96 0.88 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 4396 44 0 0 25 0 10 0 544274526 859627520 22250 4294967295 134512640 134569956 3221224400 3221214820 1080203551 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 22250 13073 16 0 209854 0
vsize: 839480
[startup+60.0092 s]
Raw data (loadavg): 0.97 0.88 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 5309 44 0 0 24 0 10 0 544274526 859627520 22380 4294967295 134512640 134569956 3221224400 3221214280 1077558376 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 22380 13073 16 0 209854 0
vsize: 839480
[startup+70.0109 s]
Raw data (loadavg): 0.97 0.89 0.92 2/63 5683
Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18028 0 1 0 6237 44 0 0 25 0 10 0 544274526 859627520 22604 4294967295 134512640 134569956 3221224400 3221213520 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 22604 13073 16 0 209854 0
vsize: 839480
[startup+80.0117 s]
Raw data (loadavg): 0.98 0.89 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 7170 45 0 0 24 0 10 0 544274526 859627520 22712 4294967295 134512640 134569956 3221224400 3221214296 1080019622 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 22712 13073 16 0 209854 0
vsize: 839480
[startup+90.0127 s]
Raw data (loadavg): 0.98 0.89 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 8104 45 0 0 25 0 10 0 544274526 859627520 22805 4294967295 134512640 134569956 3221224400 3221214280 1077558376 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 22805 13073 16 0 209854 0
vsize: 839480
[startup+100.014 s]
Raw data (loadavg): 0.98 0.89 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 9039 46 0 0 25 0 10 0 544274526 859627520 22893 4294967295 134512640 134569956 3221224400 3221214776 1131176395 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 22893 13073 16 0 209854 0
vsize: 839480
[startup+110.014 s]
Raw data (loadavg): 0.98 0.90 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 9976 46 0 0 25 0 10 0 544274526 859627520 22975 4294967295 134512640 134569956 3221224400 3221214724 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 22975 13073 16 0 209854 0
vsize: 839480
[startup+120.014 s]
Raw data (loadavg): 0.99 0.90 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 10912 47 0 0 25 0 10 0 544274526 859627520 23053 4294967295 134512640 134569956 3221224400 3221214828 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 23053 13073 16 0 209854 0
vsize: 839480
[startup+130.014 s]
Raw data (loadavg): 0.99 0.90 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 11844 47 0 0 24 0 10 0 544274526 859627520 23130 4294967295 134512640 134569956 3221224400 3221214296 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 23130 13073 16 0 209854 0
vsize: 839480
[startup+140.015 s]
Raw data (loadavg): 0.99 0.91 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 12780 47 0 0 25 0 10 0 544274526 859627520 23202 4294967295 134512640 134569956 3221224400 3221214820 1080203551 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 23202 13073 16 0 209854 0
vsize: 839480
[startup+150.015 s]
Raw data (loadavg): 0.99 0.91 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 13716 48 0 0 25 0 10 0 544274526 859627520 23269 4294967295 134512640 134569956 3221224400 3221214724 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 23269 13073 16 0 209854 0
vsize: 839480
[startup+160.014 s]
Raw data (loadavg): 0.99 0.91 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 14642 48 0 0 25 0 10 0 544274526 859627520 23335 4294967295 134512640 134569956 3221224400 3221214296 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 23335 13073 16 0 209854 0
vsize: 839480
[startup+170.015 s]
Raw data (loadavg): 0.99 0.91 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 15534 50 0 0 25 0 10 0 544274526 859627520 23421 4294967295 134512640 134569956 3221224400 3221214296 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 23421 13073 16 0 209854 0
vsize: 839480
[startup+180.015 s]
Raw data (loadavg): 0.99 0.92 0.92 2/63 5683
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18028 0 1 0 16398 50 0 0 25 0 10 0 544274526 859627520 24044 4294967295 134512640 134569956 3221224400 3221214724 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209870 24044 13073 16 0 209854 0
vsize: 839480
[startup+190.016 s]
Raw data (loadavg): 0.99 0.92 0.92 2/64 5684
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18058 0 1 0 17267 53 0 0 25 0 11 0 544274526 860155904 30055 4294967295 134512640 134569956 3221224400 3221214776 1131394326 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209999 30055 13073 16 0 209983 0
vsize: 839996
[startup+200.016 s]
Raw data (loadavg): 0.99 0.92 0.92 2/64 5687
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 18209 54 0 0 25 0 11 0 544274526 860155904 30072 4294967295 134512640 134569956 3221224400 3221214648 1131353685 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 30072 13073 16 0 209983 0
vsize: 839996
[startup+210.017 s]
Raw data (loadavg): 1.07 0.94 0.93 2/64 5691
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 19141 54 0 0 25 0 11 0 544274526 860155904 30072 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 30072 13073 16 0 209983 0
vsize: 839996
[startup+220.017 s]
Raw data (loadavg): 1.06 0.94 0.93 2/64 5695
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 20065 55 0 0 25 0 11 0 544274526 860155904 30248 4294967295 134512640 134569956 3221224400 3221214808 1131397952 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 30248 13073 16 0 209983 0
vsize: 839996
[startup+230.018 s]
Raw data (loadavg): 1.05 0.94 0.93 2/64 5699
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 20999 56 0 0 25 0 11 0 544274526 860155904 30383 4294967295 134512640 134569956 3221224400 3221214736 1131357348 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 30383 13073 16 0 209983 0
vsize: 839996
[startup+240.019 s]
Raw data (loadavg): 1.12 0.96 0.93 2/64 5703
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 21954 56 0 0 25 0 11 0 544274526 860155904 31678 4294967295 134512640 134569956 3221224400 3221214736 1131357787 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 31678 13073 16 0 209983 0
vsize: 839996
[startup+250.019 s]
Raw data (loadavg): 1.10 0.96 0.93 2/64 5708
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 22925 57 0 0 25 0 11 0 544274526 860155904 31678 4294967295 134512640 134569956 3221224400 3221214648 1131352402 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 31678 13073 16 0 209983 0
vsize: 839996
[startup+260.019 s]
Raw data (loadavg): 1.08 0.96 0.93 2/64 5712
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 23879 57 0 0 25 0 11 0 544274526 860155904 31679 4294967295 134512640 134569956 3221224400 3221214736 1131357442 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 31679 13073 16 0 209983 0
vsize: 839996
[startup+270.032 s]
Raw data (loadavg): 1.07 0.96 0.93 2/64 5716
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 24819 58 1 0 25 0 11 0 544274526 860155904 32075 4294967295 134512640 134569956 3221224400 3221214648 1131352442 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 32075 13073 16 0 209983 0
vsize: 839996
[startup+280.032 s]
Raw data (loadavg): 1.06 0.96 0.93 2/64 5720
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 25793 59 1 0 25 0 11 0 544274526 860155904 33914 4294967295 134512640 134569956 3221224400 3221214648 1131353717 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 33914 13073 16 0 209983 0
vsize: 839996
[startup+290.033 s]
Raw data (loadavg): 1.05 0.96 0.93 2/64 5725
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 26759 59 1 0 25 0 11 0 544274526 860155904 33914 4294967295 134512640 134569956 3221224400 3221214736 1131357341 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 33914 13073 16 0 209983 0
vsize: 839996
[startup+300.042 s]
Raw data (loadavg): 1.04 0.97 0.93 2/64 5729
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 27713 60 1 0 25 0 11 0 544274526 860155904 33914 4294967295 134512640 134569956 3221224400 3221214808 1131394127 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 33914 13073 16 0 209983 0
vsize: 839996
[startup+310.041 s]
Raw data (loadavg): 1.04 0.97 0.93 2/64 5733
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 28658 61 1 0 25 0 11 0 544274526 860155904 34079 4294967295 134512640 134569956 3221224400 3221214808 1131393350 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 34079 13073 16 0 209983 0
vsize: 839996
[startup+320.041 s]
Raw data (loadavg): 1.03 0.97 0.93 2/64 5737
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 29600 61 1 0 25 0 11 0 544274526 860155904 34225 4294967295 134512640 134569956 3221224400 3221214648 1131353705 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 34225 13073 16 0 209983 0
vsize: 839996
[startup+330.147 s]
Raw data (loadavg): 1.02 0.97 0.93 2/64 5742
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 30555 62 2 0 25 0 11 0 544274526 860155904 34354 4294967295 134512640 134569956 3221224400 3221214880 1131347785 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 34354 13073 16 0 209983 0
vsize: 839996
[startup+340.147 s]
Raw data (loadavg): 1.02 0.97 0.93 2/64 5746
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 31496 62 2 0 25 0 11 0 544274526 860155904 34641 4294967295 134512640 134569956 3221224400 3221214648 1131352439 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 34641 13073 16 0 209983 0
vsize: 839996
[startup+350.147 s]
Raw data (loadavg): 1.02 0.97 0.93 2/64 5750
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 32432 63 2 0 25 0 11 0 544274526 860155904 37918 4294967295 134512640 134569956 3221224400 3221214736 1131357381 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 37918 13073 16 0 209983 0
vsize: 839996
[startup+360.147 s]
Raw data (loadavg): 1.01 0.97 0.93 2/64 5754
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 33375 63 2 0 25 0 11 0 544274526 860155904 38050 4294967295 134512640 134569956 3221224400 3221214804 1131423212 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209999 38050 13073 16 0 209983 0
vsize: 839996
[startup+370.179 s]
Raw data (loadavg): 1.01 0.97 0.93 2/64 5758
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 34323 64 2 0 25 0 11 0 544274526 860155904 38179 4294967295 134512640 134569956 3221224400 3221214736 1131357752 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 38179 13073 16 0 209983 0
vsize: 839996
[startup+380.179 s]
Raw data (loadavg): 1.01 0.97 0.93 2/64 5762
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 35267 64 2 0 25 0 11 0 544274526 860155904 38418 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 38418 13073 16 0 209983 0
vsize: 839996
[startup+390.179 s]
Raw data (loadavg): 1.01 0.97 0.93 2/64 5767
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 36213 64 3 0 25 0 11 0 544274526 860155904 38547 4294967295 134512640 134569956 3221224400 3221215032 1131407238 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 38547 13073 16 0 209983 0
vsize: 839996
[startup+400.18 s]
Raw data (loadavg): 1.01 0.97 0.93 2/64 5771
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 37160 65 3 1 25 0 11 0 544274526 860155904 38709 4294967295 134512640 134569956 3221224400 3221214648 1131352341 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 38709 13073 16 0 209983 0
vsize: 839996
[startup+410.18 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5775
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 38107 65 3 1 25 0 11 0 544274526 860155904 38872 4294967295 134512640 134569956 3221224400 3221214808 1131395207 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 38872 13073 16 0 209983 0
vsize: 839996
[startup+420.18 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5779
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 39055 66 3 1 25 0 11 0 544274526 860155904 39001 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 39001 13073 16 0 209983 0
vsize: 839996
[startup+430.18 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5783
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 39995 66 3 1 25 0 11 0 544274526 860155904 39130 4294967295 134512640 134569956 3221224400 3221214736 1131357450 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 39130 13073 16 0 209983 0
vsize: 839996
[startup+440.181 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5788
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 40933 67 4 1 25 0 11 0 544274526 860155904 39259 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 39259 13073 16 0 209983 0
vsize: 839996
[startup+450.181 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5792
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 41871 67 4 1 25 0 11 0 544274526 860155904 39421 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 39421 13073 16 0 209983 0
vsize: 839996
[startup+460.181 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5796
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 42814 67 4 1 25 0 11 0 544274526 860155904 39798 4294967295 134512640 134569956 3221224400 3221214648 1131352372 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 39798 13073 16 0 209983 0
vsize: 839996
[startup+470.182 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5800
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 43761 68 4 1 25 0 11 0 544274526 860155904 39928 4294967295 134512640 134569956 3221224400 3221214736 1131357350 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 39928 13073 16 0 209983 0
vsize: 839996
[startup+480.182 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5804
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 44709 69 4 1 25 0 11 0 544274526 860155904 40057 4294967295 134512640 134569956 3221224400 3221214648 1131352639 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 40057 13073 16 0 209983 0
vsize: 839996
[startup+490.182 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5808
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 45654 69 5 1 25 0 11 0 544274526 860155904 40192 4294967295 134512640 134569956 3221224400 3221214736 1131357350 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 40192 13073 16 0 209983 0
vsize: 839996
[startup+500.182 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5812
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 46579 70 5 1 25 0 11 0 544274526 860155904 46647 4294967295 134512640 134569956 3221224400 3221214648 1131352379 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 46647 13073 16 0 209983 0
vsize: 839996
[startup+510.183 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5817
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 47518 70 5 1 24 0 11 0 544274526 860155904 46776 4294967295 134512640 134569956 3221224400 3221214736 1131357370 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 46776 13073 16 0 209983 0
vsize: 839996
[startup+520.183 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5821
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 48458 71 5 2 25 0 11 0 544274526 860155904 46905 4294967295 134512640 134569956 3221224400 3221214808 1131394326 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 46905 13073 16 0 209983 0
vsize: 839996
[startup+530.182 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5825
Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18059 3 1 0 49400 71 5 2 25 0 11 0 544274526 860155904 47143 4294967295 134512640 134569956 3221224400 3221213480 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 47143 13073 16 0 209983 0
vsize: 839996
[startup+540.184 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5829
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 50344 72 5 2 25 0 11 0 544274526 860155904 47381 4294967295 134512640 134569956 3221224400 3221214736 1131357773 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 47381 13073 16 0 209983 0
vsize: 839996
[startup+550.185 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5833
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 51294 72 5 2 25 0 11 0 544274526 860155904 47510 4294967295 134512640 134569956 3221224400 3221214736 1131357685 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 47510 13073 16 0 209983 0
vsize: 839996
[startup+560.184 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5837
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 52240 73 6 2 25 0 11 0 544274526 860155904 47640 4294967295 134512640 134569956 3221224400 3221214648 1131352653 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 47640 13073 16 0 209983 0
vsize: 839996
[startup+570.186 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5842
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 53185 74 6 2 25 0 11 0 544274526 860155904 47770 4294967295 134512640 134569956 3221224400 3221214736 1131357801 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 47770 13073 16 0 209983 0
vsize: 839996
[startup+580.186 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5846
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 54130 74 6 2 25 0 11 0 544274526 860155904 47899 4294967295 134512640 134569956 3221224400 3221214648 1131352289 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 47899 13073 16 0 209983 0
vsize: 839996
[startup+590.187 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5850
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 55072 75 6 2 25 0 11 0 544274526 860155904 48061 4294967295 134512640 134569956 3221224400 3221214808 1131395136 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 48061 13073 16 0 209983 0
vsize: 839996
[startup+600.187 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5854
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 56020 75 6 2 25 0 11 0 544274526 860155904 48256 4294967295 134512640 134569956 3221224400 3221214648 1131353636 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 48256 13073 16 0 209983 0
vsize: 839996
[startup+610.187 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5858
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 56966 75 7 2 25 0 11 0 544274526 860155904 48385 4294967295 134512640 134569956 3221224400 3221214648 1131352579 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 48385 13073 16 0 209983 0
vsize: 839996
[startup+620.188 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5863
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 57914 76 7 2 25 0 11 0 544274526 860155904 48514 4294967295 134512640 134569956 3221224400 3221214736 1131357832 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 48514 13073 16 0 209983 0
vsize: 839996
[startup+630.188 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5867
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 58860 77 7 2 25 0 11 0 544274526 860155904 48644 4294967295 134512640 134569956 3221224400 3221214976 1131410945 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 48644 13073 16 0 209983 0
vsize: 839996
[startup+640.19 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5871
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 59805 77 7 2 25 0 11 0 544274526 860155904 48805 4294967295 134512640 134569956 3221224400 3221214808 1131393226 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 48805 13073 16 0 209983 0
vsize: 839996
[startup+650.19 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5875
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 60751 78 7 2 25 0 11 0 544274526 860155904 48934 4294967295 134512640 134569956 3221224400 3221214808 1131397843 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 48934 13073 16 0 209983 0
vsize: 839996
[startup+660.19 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5879
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 61687 78 8 2 20 0 11 0 544274526 860155904 49128 4294967295 134512640 134569956 3221224400 3221214804 1131185452 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 49128 13073 16 0 209983 0
vsize: 839996
[startup+670.191 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5883
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 62622 80 8 3 24 0 11 0 544274526 860155904 49257 4294967295 134512640 134569956 3221224400 3221214760 1131185520 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 49257 13073 16 0 209983 0
vsize: 839996
[startup+680.191 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5887
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 63563 80 8 3 25 0 11 0 544274526 860155904 49454 4294967295 134512640 134569956 3221224400 3221214808 1131393226 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 49454 13073 16 0 209983 0
vsize: 839996
[startup+690.193 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5891
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 64503 81 8 3 25 0 11 0 544274526 860155904 49945 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 49945 13073 16 0 209983 0
vsize: 839996
[startup+700.196 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5896
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 65449 81 8 3 25 0 11 0 544274526 860155904 50074 4294967295 134512640 134569956 3221224400 3221214832 1131382771 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 50074 13073 16 0 209983 0
vsize: 839996
[startup+710.196 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5900
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 66394 82 8 3 25 0 11 0 544274526 860155904 50236 4294967295 134512640 134569956 3221224400 3221214688 1131329914 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 50236 13073 16 0 209983 0
vsize: 839996
[startup+720.201 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5904
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 67341 82 9 3 25 0 11 0 544274526 860155904 50365 4294967295 134512640 134569956 3221224400 3221214736 1131357798 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 50365 13073 16 0 209983 0
vsize: 839996
[startup+730.201 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5908
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 68287 83 9 3 25 0 11 0 544274526 860155904 50494 4294967295 134512640 134569956 3221224400 3221214648 1131353232 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 50494 13073 16 0 209983 0
vsize: 839996
[startup+740.201 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5912
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 69233 84 9 3 24 0 11 0 544274526 860155904 50624 4294967295 134512640 134569956 3221224400 3221214732 1131352256 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 50624 13073 16 0 209983 0
vsize: 839996
[startup+750.207 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5916
Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18059 3 1 0 70183 84 9 4 25 0 11 0 544274526 860155904 50753 4294967295 134512640 134569956 3221224400 3221213480 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 50753 13073 16 0 209983 0
vsize: 839996
[startup+760.207 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5921
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 71132 85 9 4 25 0 11 0 544274526 860155904 50894 4294967295 134512640 134569956 3221224400 3221214832 1131382808 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 50894 13073 16 0 209983 0
vsize: 839996
[startup+770.207 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5925
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 72074 85 9 4 24 0 11 0 544274526 860155904 51055 4294967295 134512640 134569956 3221224400 3221214760 1131185475 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 51055 13073 16 0 209983 0
vsize: 839996
[startup+780.206 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5929
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 73025 86 10 4 25 0 11 0 544274526 860155904 51153 4294967295 134512640 134569956 3221224400 3221214648 1131353659 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 51153 13073 16 0 209983 0
vsize: 839996
[startup+790.208 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5933
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 73970 86 10 4 25 0 11 0 544274526 860155904 51314 4294967295 134512640 134569956 3221224400 3221214648 1131352631 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 51314 13073 16 0 209983 0
vsize: 839996
[startup+800.208 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5937
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 74917 86 10 4 25 0 11 0 544274526 860155904 51443 4294967295 134512640 134569956 3221224400 3221214736 1131357442 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209999 51443 13073 16 0 209983 0
vsize: 839996
[startup+810.208 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5941
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 75820 87 10 4 25 0 11 0 544274526 860155904 64158 4294967295 134512640 134569956 3221224400 3221214736 1131357337 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 64158 13073 16 0 209983 0
vsize: 839996
[startup+820.209 s]
Raw data (loadavg): 1.00 0.97 0.93 2/64 5945
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 76752 87 10 4 25 0 11 0 544274526 860155904 64288 4294967295 134512640 134569956 3221224400 3221214648 1131353404 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 64288 13073 16 0 209983 0
vsize: 839996
[startup+830.209 s]
Raw data (loadavg): 1.08 0.99 0.94 2/64 5949
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 77685 88 10 5 25 0 11 0 544274526 860155904 64417 4294967295 134512640 134569956 3221224400 3221214760 1131185472 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 64417 13073 16 0 209983 0
vsize: 839996
[startup+840.21 s]
Raw data (loadavg): 1.07 0.99 0.94 2/64 5953
Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18059 3 1 0 78622 89 10 5 25 0 11 0 544274526 860155904 64832 4294967295 134512640 134569956 3221224400 3221213352 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 64832 13073 16 0 209983 0
vsize: 839996
[startup+850.21 s]
Raw data (loadavg): 1.06 0.99 0.94 2/64 5957
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 79566 89 10 5 25 0 11 0 544274526 860155904 65109 4294967295 134512640 134569956 3221224400 3221214648 1131352381 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 65109 13073 16 0 209983 0
vsize: 839996
[startup+860.216 s]
Raw data (loadavg): 1.05 0.99 0.94 2/64 5961
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 80511 89 11 5 25 0 11 0 544274526 860155904 65238 4294967295 134512640 134569956 3221224400 3221214044 1077094240 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 65238 13073 16 0 209983 0
vsize: 839996
[startup+870.221 s]
Raw data (loadavg): 1.04 0.99 0.94 2/64 5966
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 81455 90 11 5 25 0 11 0 544274526 860155904 65367 4294967295 134512640 134569956 3221224400 3221214808 1131393219 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 65367 13073 16 0 209983 0
vsize: 839996
[startup+880.222 s]
Raw data (loadavg): 1.03 0.99 0.94 2/64 5970
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 82399 90 11 5 25 0 11 0 544274526 860155904 65530 4294967295 134512640 134569956 3221224400 3221214648 1131352601 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 65530 13073 16 0 209983 0
vsize: 839996
[startup+890.223 s]
Raw data (loadavg): 1.03 0.99 0.94 2/64 5974
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 83345 91 11 5 25 0 11 0 544274526 860155904 65660 4294967295 134512640 134569956 3221224400 3221214648 1131352422 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 65660 13073 16 0 209983 0
vsize: 839996
[startup+900.223 s]
Raw data (loadavg): 1.02 0.99 0.94 2/64 5978
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 84290 91 11 5 25 0 11 0 544274526 860155904 65789 4294967295 134512640 134569956 3221224400 3221214760 1131185475 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 65789 13073 16 0 209983 0
vsize: 839996
[startup+910.223 s]
Raw data (loadavg): 1.02 0.99 0.94 2/64 5982
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 85236 92 11 5 25 0 11 0 544274526 860155904 65918 4294967295 134512640 134569956 3221224400 3221214736 1131357804 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 65918 13073 16 0 209983 0
vsize: 839996
[startup+920.224 s]
Raw data (loadavg): 1.02 0.99 0.94 2/64 5986
Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18059 3 1 0 86182 92 11 5 25 0 11 0 544274526 860155904 66048 4294967295 134512640 134569956 3221224400 3221213480 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 66048 13073 16 0 209983 0
vsize: 839996
[startup+930.26 s]
Raw data (loadavg): 1.01 0.99 0.94 2/64 5990
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 87134 93 11 5 25 0 11 0 544274526 860155904 66177 4294967295 134512640 134569956 3221224400 3221214736 1131357348 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 66177 13073 16 0 209983 0
vsize: 839996
[startup+940.261 s]
Raw data (loadavg): 1.01 0.99 0.94 2/64 5995
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 88075 94 11 6 25 0 11 0 544274526 860155904 66306 4294967295 134512640 134569956 3221224400 3221214808 1131394312 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 66306 13073 16 0 209983 0
vsize: 839996
[startup+950.261 s]
Raw data (loadavg): 1.01 0.99 0.94 2/64 5999
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 89016 94 12 6 25 0 11 0 544274526 860155904 66434 4294967295 134512640 134569956 3221224400 3221214808 1131395529 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 66434 13073 16 0 209983 0
vsize: 839996
[startup+960.261 s]
Raw data (loadavg): 1.01 0.99 0.94 2/64 6003
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 89956 94 12 6 25 0 11 0 544274526 860155904 66597 4294967295 134512640 134569956 3221224400 3221214808 1131393266 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 66597 13073 16 0 209983 0
vsize: 839996
[startup+970.262 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6007
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 90898 95 12 6 25 0 11 0 544274526 860155904 66858 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 66858 13073 16 0 209983 0
vsize: 839996
[startup+980.262 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6011
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 91847 96 12 6 25 0 11 0 544274526 860155904 66987 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 66987 13073 16 0 209983 0
vsize: 839996
[startup+990.263 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6015
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 92790 97 12 6 25 0 11 0 544274526 860155904 67117 4294967295 134512640 134569956 3221224400 3221214808 1131393226 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 67117 13073 16 0 209983 0
vsize: 839996
[startup+1000.26 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6019
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 93735 97 13 7 25 0 11 0 544274526 860155904 67246 4294967295 134512640 134569956 3221224400 3221214736 1131357341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209999 67246 13073 16 0 209983 0
vsize: 839996
[startup+1010.26 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6023
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 94680 98 13 7 25 0 11 0 544274526 860155904 67374 4294967295 134512640 134569956 3221224400 3221214648 1131353363 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 67374 13073 16 0 209983 0
vsize: 839996
[startup+1020.26 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6028
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 95625 98 13 7 25 0 11 0 544274526 860155904 67503 4294967295 134512640 134569956 3221224400 3221214952 1131415243 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 67503 13073 16 0 209983 0
vsize: 839996
[startup+1030.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6032
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 96568 99 13 7 25 0 11 0 544274526 860155904 67666 4294967295 134512640 134569956 3221224400 3221214808 1131393007 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 67666 13073 16 0 209983 0
vsize: 839996
[startup+1040.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6036
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 97511 99 13 7 24 0 11 0 544274526 860155904 67794 4294967295 134512640 134569956 3221224400 3221214648 1131353659 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 67794 13073 16 0 209983 0
vsize: 839996
[startup+1050.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6040
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 98460 99 13 7 25 0 11 0 544274526 860155904 67923 4294967295 134512640 134569956 3221224400 3221214736 1131357438 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 67923 13073 16 0 209983 0
vsize: 839996
[startup+1060.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6044
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 99404 100 14 7 24 0 11 0 544274526 860155904 68052 4294967295 134512640 134569956 3221224400 3221214648 1131352617 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 68052 13073 16 0 209983 0
vsize: 839996
[startup+1070.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6048
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 100348 101 14 7 25 0 11 0 544274526 860155904 68183 4294967295 134512640 134569956 3221224400 3221214736 1131357381 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 68183 13073 16 0 209983 0
vsize: 839996
[startup+1080.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6052
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 101292 101 14 7 24 0 11 0 544274526 860155904 68311 4294967295 134512640 134569956 3221224400 3221214736 1131357716 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 68311 13073 16 0 209983 0
vsize: 839996
[startup+1090.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6056
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 102241 102 14 7 25 0 11 0 544274526 860155904 68441 4294967295 134512640 134569956 3221224400 3221214648 1131352494 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 68441 13073 16 0 209983 0
vsize: 839996
[startup+1100.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6060
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 103184 103 14 7 25 0 11 0 544274526 860155904 68570 4294967295 134512640 134569956 3221224400 3221214736 1131357728 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 68570 13073 16 0 209983 0
vsize: 839996
[startup+1110.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6064
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 104129 103 14 7 25 0 11 0 544274526 860155904 68700 4294967295 134512640 134569956 3221224400 3221214736 1131357676 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 68700 13073 16 0 209983 0
vsize: 839996
[startup+1120.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6068
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 105068 104 14 7 24 0 11 0 544274526 860155904 68929 4294967295 134512640 134569956 3221224400 3221214648 1131353644 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 68929 13073 16 0 209983 0
vsize: 839996
[startup+1130.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6073
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 106028 105 15 7 25 0 11 0 544274526 860155904 69804 4294967295 134512640 134569956 3221224400 3221214648 1131353287 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 69804 13073 16 0 209983 0
vsize: 839996
[startup+1140.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6077
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 106980 105 15 7 25 0 11 0 544274526 860155904 69804 4294967295 134512640 134569956 3221224400 3221214648 1131352381 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 69804 13073 16 0 209983 0
vsize: 839996
[startup+1150.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6081
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 107918 106 15 7 25 0 11 0 544274526 860155904 69804 4294967295 134512640 134569956 3221224400 3221214648 1131352425 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 69804 13073 16 0 209983 0
vsize: 839996
[startup+1160.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6085
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 108864 106 15 7 25 0 11 0 544274526 860155904 70367 4294967295 134512640 134569956 3221224400 3221214992 1131389937 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 70367 13073 16 0 209983 0
vsize: 839996
[startup+1170.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6089
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 109807 107 15 7 25 0 11 0 544274526 860155904 70528 4294967295 134512640 134569956 3221224400 3221214648 1131352355 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 70528 13073 16 0 209983 0
vsize: 839996
[startup+1180.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6093
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 110751 107 16 7 25 0 11 0 544274526 860155904 70657 4294967295 134512640 134569956 3221224400 3221214808 1131394312 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 70657 13073 16 0 209983 0
vsize: 839996
[startup+1190.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6097
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 111696 108 16 8 25 0 11 0 544274526 860155904 70787 4294967295 134512640 134569956 3221224400 3221214760 1131185475 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 70787 13073 16 0 209983 0
vsize: 839996
[startup+1200.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6101
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 112645 108 16 8 25 0 11 0 544274526 860155904 70916 4294967295 134512640 134569956 3221224400 3221214648 1131352631 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 70916 13073 16 0 209983 0
vsize: 839996
[startup+1210.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6105
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 113588 109 16 8 25 0 11 0 544274526 860155904 71044 4294967295 134512640 134569956 3221224400 3221214808 1131394326 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 71044 13073 16 0 209983 0
vsize: 839996
[startup+1220.27 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6109
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 114531 109 16 8 25 0 11 0 544274526 860155904 71173 4294967295 134512640 134569956 3221224400 3221214736 1131357804 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 71173 13073 16 0 209983 0
vsize: 839996
[startup+1230.28 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6113
Raw data (stat): 5674 (java) S 5673 27565 27564 0 -1 0 18059 3 1 0 115475 110 16 8 25 0 11 0 544274526 860155904 71303 4294967295 134512640 134569956 3221224400 3221213480 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 71303 13073 16 0 209983 0
vsize: 839996
[startup+1240.28 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6117
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 116424 110 16 8 25 0 11 0 544274526 860155904 71432 4294967295 134512640 134569956 3221224400 3221214808 1131394326 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209999 71432 13073 16 0 209983 0
vsize: 839996
[startup+1250.28 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6121
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 117367 111 16 8 25 0 11 0 544274526 860155904 71561 4294967295 134512640 134569956 3221224400 3221214916 1130885120 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209999 71561 13073 16 0 209983 0
vsize: 839996
[startup+1260.28 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6126
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 118309 111 17 8 25 0 11 0 544274526 860155904 71691 4294967295 134512640 134569956 3221224400 3221214648 1131352488 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209999 71691 13073 16 0 209983 0
vsize: 839996
[startup+1270.28 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6130
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 119251 111 17 8 24 0 11 0 544274526 860155904 71852 4294967295 134512640 134569956 3221224400 3221214648 1131352280 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209999 71852 13073 16 0 209983 0
vsize: 839996
[startup+1280.28 s]
Raw data (loadavg): 1.00 0.99 0.94 2/64 6134
Raw data (stat): 5674 (java) R 5673 27565 27564 0 -1 0 18059 3 1 0 120199 112 17 8 25 0 11 0 544274526 860155904 71949 4294967295 134512640 134569956 3221224400 3221214688 1131330281 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209999 71949 13073 16 0 209983 0
vsize: 839996
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1280.42 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 6135
Raw data (stat): 5674 (java) Z 5673 27565 27564 0 -1 1036 18059 52196 1 0 120199 112 7478 131 25 0 1 0 544274526 0 0 4294967295 0 0 0 0 0 0 4 3 23756 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 143
Real time (s): 1280.42
CPU time (s): 1279.22
CPU user time (s): 1276.78
CPU system time (s): 2.44163
CPU usage (%): 99.9063
Max. virtual memory (Kb): 840248
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####