PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-bg512142.opb
MD5SUM	0f3e1a19529370afcd1348994ae2c757
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	6480
Biggest coefficient in the objective function	5242880000
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	755791986840
Number of bits of the sum of numbers in the objective function	40
Biggest number in a constraint	5242880000
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	755791986840
Number of bits of the biggest sum of numbers	40
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1246.02
Number of variables	11280
Total number of constraints	1307
Number of constraints which are clauses	11
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1296
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 14509

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        792088 kB
Buffers:         11520 kB
Cached:         200052 kB
SwapCached:        520 kB
Active:          65020 kB
Inactive:       148692 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        791836 kB
SwapTotal:     2097136 kB
SwapFree:      2095824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            23176 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 00:25:57 (client local time) WITH STATUS 143 IN 1336.78 SECONDS
stats: 19938 7 1336.78 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-bg512142.opb
c reading problem 
c [nbvar=11280]
c [nbconstr=1307]
c time 42.862
c #vars     11280
c #clauses  1186
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=750878720
c Current CPU time (ms) : 48.176
c starts	: 1
c conflicts	: 0
c decisions	: 5406
c propagations	: 11280
c inspects	: 17749
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=-922648576
c Current CPU time (ms) : 52.279
c starts	: 2
c conflicts	: 0
c decisions	: 10811
c propagations	: 21874
c inspects	: 32803
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=1698791424
c Current CPU time (ms) : 55.968
c starts	: 3
c conflicts	: 0
c decisions	: 16215
c propagations	: 32468
c inspects	: 47856
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=1698791424
c Current CPU time (ms) : 59.572
c starts	: 4
c conflicts	: 0
c decisions	: 21619
c propagations	: 43062
c inspects	: 62910
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=1698791424
c Current CPU time (ms) : 63.226
c starts	: 5
c conflicts	: 0
c decisions	: 27023
c propagations	: 53656
c inspects	: 77964
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=1698791424
c Current CPU time (ms) : 66.933
c starts	: 6
c conflicts	: 0
c decisions	: 32427
c propagations	: 64250
c inspects	: 93018
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=1698791424
c Current CPU time (ms) : 70.652
c starts	: 7
c conflicts	: 0
c decisions	: 37831
c propagations	: 74844
c inspects	: 108072
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=1698791424
c Current CPU time (ms) : 74.264
c starts	: 8
c conflicts	: 0
c decisions	: 43235
c propagations	: 85438
c inspects	: 123126
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=1698791424
c Current CPU time (ms) : 77.946
c starts	: 9
c conflicts	: 0
c decisions	: 48639
c propagations	: 96032
c inspects	: 138180
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=1698791424
c Current CPU time (ms) : 81.588
c starts	: 10
c conflicts	: 0
c decisions	: 54043
c propagations	: 106626
c inspects	: 153234
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=1698791424
c Current CPU time (ms) : 85.211
c starts	: 11
c conflicts	: 0
c decisions	: 59447
c propagations	: 117220
c inspects	: 168288
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=1698791424
c Current CPU time (ms) : 88.831
c starts	: 12
c conflicts	: 0
c decisions	: 64851
c propagations	: 127814
c inspects	: 183342
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=1698791424
c Current CPU time (ms) : 92.458
c starts	: 13
c conflicts	: 0
c decisions	: 70255
c propagations	: 138408
c inspects	: 198396
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=1698791424
c Current CPU time (ms) : 96.094
c starts	: 14
c conflicts	: 0
c decisions	: 75659
c propagations	: 149002
c inspects	: 213450
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=1698791424
c Current CPU time (ms) : 99.674
c starts	: 15
c conflicts	: 0
c decisions	: 81063
c propagations	: 159596
c inspects	: 228504
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=1698791424
c Current CPU time (ms) : 103.37
c starts	: 16
c conflicts	: 0
c decisions	: 86467
c propagations	: 170190
c inspects	: 243558
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=1698791424
c Current CPU time (ms) : 107.09
c starts	: 17
c conflicts	: 0
c decisions	: 91871
c propagations	: 180784
c inspects	: 258612
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=1698791424
c Current CPU time (ms) : 110.757
c starts	: 18
c conflicts	: 0
c decisions	: 97275
c propagations	: 191378
c inspects	: 273666
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=1698791424
c Current CPU time (ms) : 114.345
c starts	: 19
c conflicts	: 0
c decisions	: 102679
c propagations	: 201972
c inspects	: 288720
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=1698791424
c Current CPU time (ms) : 117.938
c starts	: 20
c conflicts	: 0
c decisions	: 108083
c propagations	: 212566
c inspects	: 303774
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=1698791424
c Current CPU time (ms) : 121.512
c starts	: 21
c conflicts	: 0
c decisions	: 113487
c propagations	: 223160
c inspects	: 318828
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=1698791424
c Current CPU time (ms) : 125.112
c starts	: 22
c conflicts	: 0
c decisions	: 118891
c propagations	: 233754
c inspects	: 333882
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=1698791424
c Current CPU time (ms) : 128.656
c starts	: 23
c conflicts	: 0
c decisions	: 124295
c propagations	: 244348
c inspects	: 348936
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=1698791424
c Current CPU time (ms) : 132.304
c starts	: 24
c conflicts	: 0
c decisions	: 129699
c propagations	: 254942
c inspects	: 363990
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=1698791424
c Current CPU time (ms) : 135.959
c starts	: 25
c conflicts	: 0
c decisions	: 135103
c propagations	: 265536
c inspects	: 379044
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=1698791424
c Current CPU time (ms) : 139.629
c starts	: 26
c conflicts	: 0
c decisions	: 140507
c propagations	: 276130
c inspects	: 394098
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=1698791424
c Current CPU time (ms) : 143.318
c starts	: 27
c conflicts	: 0
c decisions	: 145911
c propagations	: 286724
c inspects	: 409152
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=1698791424
c Current CPU time (ms) : 146.995
c starts	: 28
c conflicts	: 0
c decisions	: 151315
c propagations	: 297318
c inspects	: 424206
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=1698791424
c Current CPU time (ms) : 150.696
c starts	: 29
c conflicts	: 0
c decisions	: 156719
c propagations	: 307912
c inspects	: 439260
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=1698791424
c Current CPU time (ms) : 154.315
c starts	: 30
c conflicts	: 0
c decisions	: 162123
c propagations	: 318506
c inspects	: 454314
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=1698791424
c Current CPU time (ms) : 158.012
c starts	: 31
c conflicts	: 0
c decisions	: 167527
c propagations	: 329100
c inspects	: 469368
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=1698791424
c Current CPU time (ms) : 161.709
c starts	: 32
c conflicts	: 0
c decisions	: 172931
c propagations	: 339694
c inspects	: 484422
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=1698791424
c Current CPU time (ms) : 165.421
c starts	: 33
c conflicts	: 0
c decisions	: 178335
c propagations	: 350288
c inspects	: 499476
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=1698791424
c Current CPU time (ms) : 169.152
c starts	: 34
c conflicts	: 0
c decisions	: 183739
c propagations	: 360882
c inspects	: 514530
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=1698791424
c Current CPU time (ms) : 172.864
c starts	: 35
c conflicts	: 0
c decisions	: 189143
c propagations	: 371476
c inspects	: 529584
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=1698791424
c Current CPU time (ms) : 176.401
c starts	: 36
c conflicts	: 0
c decisions	: 194547
c propagations	: 382070
c inspects	: 544638
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=1698791424
c Current CPU time (ms) : 179.883
c starts	: 37
c conflicts	: 0
c decisions	: 199951
c propagations	: 392664
c inspects	: 559692
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=1698791424
c Current CPU time (ms) : 183.448
c starts	: 38
c conflicts	: 0
c decisions	: 205355
c propagations	: 403258
c inspects	: 574746
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=1698791424
c Current CPU time (ms) : 187.066
c starts	: 39
c conflicts	: 0
c decisions	: 210759
c propagations	: 413852
c inspects	: 589800
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=1698791424
c Current CPU time (ms) : 190.731
c starts	: 40
c conflicts	: 0
c decisions	: 216163
c propagations	: 424446
c inspects	: 604854
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=1698791424
c Current CPU time (ms) : 194.424
c starts	: 41
c conflicts	: 0
c decisions	: 221567
c propagations	: 435040
c inspects	: 619908
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=1698791424
c Current CPU time (ms) : 198.109
c starts	: 42
c conflicts	: 0
c decisions	: 226971
c propagations	: 445634
c inspects	: 634962
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=1698791424
c Current CPU time (ms) : 201.771
c starts	: 43
c conflicts	: 0
c decisions	: 232375
c propagations	: 456228
c inspects	: 650016
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=1698791424
c Current CPU time (ms) : 205.444
c starts	: 44
c conflicts	: 0
c decisions	: 237779
c propagations	: 466822
c inspects	: 665070
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=1698791424
c Current CPU time (ms) : 209.024
c starts	: 45
c conflicts	: 0
c decisions	: 243183
c propagations	: 477416
c inspects	: 680124
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=1698791424
c Current CPU time (ms) : 212.706
c starts	: 46
c conflicts	: 0
c decisions	: 248587
c propagations	: 488010
c inspects	: 695178
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=1698791424
c Current CPU time (ms) : 216.392
c starts	: 47
c conflicts	: 0
c decisions	: 253991
c propagations	: 498604
c inspects	: 710232
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=1698791424
c Current CPU time (ms) : 220.063
c starts	: 48
c conflicts	: 0
c decisions	: 259395
c propagations	: 509198
c inspects	: 725286
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=1698791424
c Current CPU time (ms) : 223.778
c starts	: 49
c conflicts	: 0
c decisions	: 264799
c propagations	: 519792
c inspects	: 740340
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=1698791424
c Current CPU time (ms) : 227.472
c starts	: 50
c conflicts	: 0
c decisions	: 270203
c propagations	: 530386
c inspects	: 755394
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=1698791424
c Current CPU time (ms) : 231.155
c starts	: 51
c conflicts	: 0
c decisions	: 275607
c propagations	: 540980
c inspects	: 770448
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=1698791424
c Current CPU time (ms) : 234.763
c starts	: 52
c conflicts	: 0
c decisions	: 281011
c propagations	: 551574
c inspects	: 785502
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=1698791424
c Current CPU time (ms) : 238.44
c starts	: 53
c conflicts	: 0
c decisions	: 286415
c propagations	: 562168
c inspects	: 800556
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=1698791424
c Current CPU time (ms) : 242.124
c starts	: 54
c conflicts	: 0
c decisions	: 291819
c propagations	: 572762
c inspects	: 815610
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=1698791424
c Current CPU time (ms) : 245.827
c starts	: 55
c conflicts	: 0
c decisions	: 297223
c propagations	: 583356
c inspects	: 830664
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=1698791424
c Current CPU time (ms) : 249.543
c starts	: 56
c conflicts	: 0
c decisions	: 302627
c propagations	: 593950
c inspects	: 845718
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=1698791424
c Current CPU time (ms) : 253.238
c starts	: 57
c conflicts	: 0
c decisions	: 308031
c propagations	: 604544
c inspects	: 860772
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=1698791424
c Current CPU time (ms) : 256.944
c starts	: 58
c conflicts	: 0
c decisions	: 313435
c propagations	: 615138
c inspects	: 875826
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=1698791424
c Current CPU time (ms) : 260.585
c starts	: 59
c conflicts	: 0
c decisions	: 318839
c propagations	: 625732
c inspects	: 890880
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=1698791424
c Current CPU time (ms) : 264.308
c starts	: 60
c conflicts	: 0
c decisions	: 324243
c propagations	: 636326
c inspects	: 905934
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=1698791424
c Current CPU time (ms) : 268.041
c starts	: 61
c conflicts	: 0
c decisions	: 329647
c propagations	: 646920
c inspects	: 920988
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=1698791424
c Current CPU time (ms) : 271.778
c starts	: 62
c conflicts	: 0
c decisions	: 335051
c propagations	: 657514
c inspects	: 936042
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=1698791424
c Current CPU time (ms) : 275.531
c starts	: 63
c conflicts	: 0
c decisions	: 340455
c propagations	: 668108
c inspects	: 951096
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=1698791424
c Current CPU time (ms) : 279.229
c starts	: 64
c conflicts	: 0
c decisions	: 345859
c propagations	: 678702
c inspects	: 966150
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=1698791424
c Current CPU time (ms) : 282.948
c starts	: 65
c conflicts	: 0
c decisions	: 351263
c propagations	: 689296
c inspects	: 981204
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=1698791424
c Current CPU time (ms) : 286.552
c starts	: 66
c conflicts	: 0
c decisions	: 356667
c propagations	: 699890
c inspects	: 996258
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=1698791424
c Current CPU time (ms) : 290.238
c starts	: 67
c conflicts	: 0
c decisions	: 362071
c propagations	: 710484
c inspects	: 1011312
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=1698791424
c Current CPU time (ms) : 293.911
c starts	: 68
c conflicts	: 0
c decisions	: 367475
c propagations	: 721078
c inspects	: 1026366
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=1698791424
c Current CPU time (ms) : 297.657
c starts	: 69
c conflicts	: 0
c decisions	: 372879
c propagations	: 731672
c inspects	: 1041420
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=1698791424
c Current CPU time (ms) : 301.169
c starts	: 70
c conflicts	: 0
c decisions	: 378283
c propagations	: 742266
c inspects	: 1056474
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=1698791424
c Current CPU time (ms) : 304.727
c starts	: 71
c conflicts	: 0
c decisions	: 383687
c propagations	: 752860
c inspects	: 1071528
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=1698791424
c Current CPU time (ms) : 308.335
c starts	: 72
c conflicts	: 0
c decisions	: 389091
c propagations	: 763454
c inspects	: 1086582
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=1698791424
c Current CPU time (ms) : 311.991
c starts	: 73
c conflicts	: 0
c decisions	: 394495
c propagations	: 774048
c inspects	: 1101636
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=1698791424
c Current CPU time (ms) : 315.707
c starts	: 74
c conflicts	: 0
c decisions	: 399899
c propagations	: 784642
c inspects	: 1116690
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=1698791424
c Current CPU time (ms) : 319.378
c starts	: 75
c conflicts	: 0
c decisions	: 405303
c propagations	: 795236
c inspects	: 1131744
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=1698791424
c Current CPU time (ms) : 323.13
c starts	: 76
c conflicts	: 0
c decisions	: 410707
c propagations	: 805830
c inspects	: 1146798
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=1698791424
c Current CPU time (ms) : 326.872
c starts	: 77
c conflicts	: 0
c decisions	: 416111
c propagations	: 816424
c inspects	: 1161852
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=1698791424
c Current CPU time (ms) : 330.608
c starts	: 78
c conflicts	: 0
c decisions	: 421515
c propagations	: 827018
c inspects	: 1176906
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=1698791424
c Current CPU time (ms) : 334.329
c starts	: 79
c conflicts	: 0
c decisions	: 426919
c propagations	: 837612
c inspects	: 1191960
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=1698791424
c Current CPU time (ms) : 338.079
c starts	: 80
c conflicts	: 0
c decisions	: 432323
c propagations	: 848206
c inspects	: 1207014
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=1698791424
c Current CPU time (ms) : 341.854
c starts	: 81
c conflicts	: 0
c decisions	: 437727
c propagations	: 858800
c inspects	: 1222068
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=1698791424
c Current CPU time (ms) : 345.524
c starts	: 82
c conflicts	: 0
c decisions	: 443131
c propagations	: 869394
c inspects	: 1237122
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=1698791424
c Current CPU time (ms) : 349.264
c starts	: 83
c conflicts	: 0
c decisions	: 448535
c propagations	: 879988
c inspects	: 1252176
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=1698791424
c Current CPU time (ms) : 353.051
c starts	: 84
c conflicts	: 0
c decisions	: 453939
c propagations	: 890582
c inspects	: 1267230
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=1698791424
c Current CPU time (ms) : 356.793
c starts	: 85
c conflicts	: 0
c decisions	: 459343
c propagations	: 901176
c inspects	: 1282284
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=1698791424
c Current CPU time (ms) : 360.557
c starts	: 86
c conflicts	: 0
c decisions	: 464747
c propagations	: 911770
c inspects	: 1297338
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=1698791424
c Current CPU time (ms) : 364.285
c starts	: 87
c conflicts	: 0
c decisions	: 470151
c propagations	: 922364
c inspects	: 1312392
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=1698791424
c Current CPU time (ms) : 368.025
c starts	: 88
c conflicts	: 0
c decisions	: 475555
c propagations	: 932958
c inspects	: 1327446
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=1698791424
c Current CPU time (ms) : 371.765
c starts	: 89
c conflicts	: 0
c decisions	: 480959
c propagations	: 943552
c inspects	: 1342500
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=1698791424
c Current CPU time (ms) : 375.421
c starts	: 90
c conflicts	: 0
c decisions	: 486363
c propagations	: 954146
c inspects	: 1357554
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=1698791424
c Current CPU time (ms) : 379.164
c starts	: 91
c conflicts	: 0
c decisions	: 491767
c propagations	: 964740
c inspects	: 1372608
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=1698791424
c Current CPU time (ms) : 382.907
c starts	: 92
c conflicts	: 0
c decisions	: 497171
c propagations	: 975334
c inspects	: 1387662
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=1698791424
c Current CPU time (ms) : 386.671
c starts	: 93
c conflicts	: 0
c decisions	: 502575
c propagations	: 985928
c inspects	: 1402716
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=1698791424
c Current CPU time (ms) : 390.445
c starts	: 94
c conflicts	: 0
c decisions	: 507979
c propagations	: 996522
c inspects	: 1417770
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=1698791424
c Current CPU time (ms) : 394.208
c starts	: 95
c conflicts	: 0
c decisions	: 513383
c propagations	: 1007116
c inspects	: 1432824
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=1698791424
c Current CPU time (ms) : 397.97
c starts	: 96
c conflicts	: 0
c decisions	: 518787
c propagations	: 1017710
c inspects	: 1447878
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=1698791424
c Current CPU time (ms) : 401.683
c starts	: 97
c conflicts	: 0
c decisions	: 524191
c propagations	: 1028304
c inspects	: 1462932
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=1698791424
c Current CPU time (ms) : 405.439
c starts	: 98
c conflicts	: 0
c decisions	: 529595
c propagations	: 1038898
c inspects	: 1477986
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=1698791424
c Current CPU time (ms) : 409.205
c starts	: 99
c conflicts	: 0
c decisions	: 534999
c propagations	: 1049492
c inspects	: 1493040
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=1698791424
c Current CPU time (ms) : 412.95
c starts	: 100
c conflicts	: 0
c decisions	: 540403
c propagations	: 1060086
c inspects	: 1508094
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=1698791424
c Current CPU time (ms) : 416.692
c starts	: 101
c conflicts	: 0
c decisions	: 545807
c propagations	: 1070680
c inspects	: 1523148
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=1698791424
c Current CPU time (ms) : 420.433
c starts	: 102
c conflicts	: 0
c decisions	: 551211
c propagations	: 1081274
c inspects	: 1538202
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=1698791424
c Current CPU time (ms) : 424.202
c starts	: 103
c conflicts	: 0
c decisions	: 556615
c propagations	: 1091868
c inspects	: 1553256
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=1698791424
c Current CPU time (ms) : 427.89
c starts	: 104
c conflicts	: 0
c decisions	: 562019
c propagations	: 1102462
c inspects	: 1568310
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=1698791424
c Current CPU time (ms) : 431.638
c starts	: 105
c conflicts	: 0
c decisions	: 567423
c propagations	: 1113056
c inspects	: 1583364
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=1698791424
c Current CPU time (ms) : 435.405
c starts	: 106
c conflicts	: 0
c decisions	: 572827
c propagations	: 1123650
c inspects	: 1598418
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=1698791424
c Current CPU time (ms) : 439.197
c starts	: 107
c conflicts	: 0
c decisions	: 578231
c propagations	: 1134244
c inspects	: 1613472
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=1698791424
c Current CPU time (ms) : 443.012
c starts	: 108
c conflicts	: 0
c decisions	: 583635
c propagations	: 1144838
c inspects	: 1628526
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=1698791424
c Current CPU time (ms) : 446.826
c starts	: 109
c conflicts	: 0
c decisions	: 589039
c propagations	: 1155432
c inspects	: 1643580
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=1698791424
c Current CPU time (ms) : 450.634
c starts	: 110
c conflicts	: 0
c decisions	: 594443
c propagations	: 1166026
c inspects	: 1658634
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=1698791424
c Current CPU time (ms) : 454.475
c starts	: 111
c conflicts	: 0
c decisions	: 599847
c propagations	: 1176620
c inspects	: 1673688
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=1698791424
c Current CPU time (ms) : 458.181
c starts	: 112
c conflicts	: 0
c decisions	: 605251
c propagations	: 1187214
c inspects	: 1688742
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=1698791424
c Current CPU time (ms) : 461.986
c starts	: 113
c conflicts	: 0
c decisions	: 610655
c propagations	: 1197808
c inspects	: 1703796
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=1698791424
c Current CPU time (ms) : 465.801
c starts	: 114
c conflicts	: 0
c decisions	: 616059
c propagations	: 1208402
c inspects	: 1718850
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=1698791424
c Current CPU time (ms) : 469.613
c starts	: 115
c conflicts	: 0
c decisions	: 621463
c propagations	: 1218996
c inspects	: 1733904
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=1698791424
c Current CPU time (ms) : 473.424
c starts	: 116
c conflicts	: 0
c decisions	: 626867
c propagations	: 1229590
c inspects	: 1748958
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=1698791424
c Current CPU time (ms) : 477.245
c starts	: 117
c conflicts	: 0
c decisions	: 632271
c propagations	: 1240184
c inspects	: 1764012
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=1698791424
c Current CPU time (ms) : 481.073
c starts	: 118
c conflicts	: 0
c decisions	: 637675
c propagations	: 1250778
c inspects	: 1779066
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=1698791424
c Current CPU time (ms) : 484.822
c starts	: 119
c conflicts	: 0
c decisions	: 643079
c propagations	: 1261372
c inspects	: 1794120
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=1698791424
c Current CPU time (ms) : 488.649
c starts	: 120
c conflicts	: 0
c decisions	: 648483
c propagations	: 1271966
c inspects	: 1809174
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=1698791424
c Current CPU time (ms) : 492.478
c starts	: 121
c conflicts	: 0
c decisions	: 653887
c propagations	: 1282560
c inspects	: 1824228
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=1698791424
c Current CPU time (ms) : 496.292
c starts	: 122
c conflicts	: 0
c decisions	: 659291
c propagations	: 1293154
c inspects	: 1839282
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=1698791424
c Current CPU time (ms) : 500.125
c starts	: 123
c conflicts	: 0
c decisions	: 664695
c propagations	: 1303748
c inspects	: 1854336
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=1698791424
c Current CPU time (ms) : 503.926
c starts	: 124
c conflicts	: 0
c decisions	: 670099
c propagations	: 1314342
c inspects	: 1869390
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=1698791424
c Current CPU time (ms) : 507.717
c starts	: 125
c conflicts	: 0
c decisions	: 675503
c propagations	: 1324936
c inspects	: 1884444
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=1698791424
c Current CPU time (ms) : 511.435
c starts	: 126
c conflicts	: 0
c decisions	: 680907
c propagations	: 1335530
c inspects	: 1899498
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=1698791424
c Current CPU time (ms) : 515.232
c starts	: 127
c conflicts	: 0
c decisions	: 686311
c propagations	: 1346124
c inspects	: 1914552
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=1698791424
c Current CPU time (ms) : 519.022
c starts	: 128
c conflicts	: 0
c decisions	: 691715
c propagations	: 1356718
c inspects	: 1929606
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=1698791424
c Current CPU time (ms) : 522.843
c starts	: 129
c conflicts	: 0
c decisions	: 697119
c propagations	: 1367312
c inspects	: 1944660
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=1698791424
c Current CPU time (ms) : 526.589
c starts	: 130
c conflicts	: 0
c decisions	: 702523
c propagations	: 1377906
c inspects	: 1959714
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=1698791424
c Current CPU time (ms) : 530.344
c starts	: 131
c conflicts	: 0
c decisions	: 707927
c propagations	: 1388500
c inspects	: 1974768
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=1698791424
c Current CPU time (ms) : 534.097
c starts	: 132
c conflicts	: 0
c decisions	: 713331
c propagations	: 1399094
c inspects	: 1989822
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=1698791424
c Current CPU time (ms) : 537.797
c starts	: 133
c conflicts	: 0
c decisions	: 718735
c propagations	: 1409688
c inspects	: 2004876
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=1698791424
c Current CPU time (ms) : 541.59
c starts	: 134
c conflicts	: 0
c decisions	: 724139
c propagations	: 1420282
c inspects	: 2019930
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=1698791424
c Current CPU time (ms) : 545.344
c starts	: 135
c conflicts	: 0
c decisions	: 729543
c propagations	: 1430876
c inspects	: 2034984
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=1698791424
c Current CPU time (ms) : 549.091
c starts	: 136
c conflicts	: 0
c decisions	: 734947
c propagations	: 1441470
c inspects	: 2050038
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=1698791424
c Current CPU time (ms) : 553.062
c starts	: 137
c conflicts	: 0
c decisions	: 740351
c propagations	: 1452064
c inspects	: 2065092
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=1698791424
c Current CPU time (ms) : 556.831
c starts	: 138
c conflicts	: 0
c decisions	: 745755
c propagations	: 1462658
c inspects	: 2080146
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=1698791424
c Current CPU time (ms) : 560.601
c starts	: 139
c conflicts	: 0
c decisions	: 751159
c propagations	: 1473252
c inspects	: 2095200
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=1698791424
c Current CPU time (ms) : 564.414
c starts	: 140
c conflicts	: 0
c decisions	: 756563
c propagations	: 1483846
c inspects	: 2110254
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=1698791424
c Current CPU time (ms) : 568.201
c starts	: 141
c conflicts	: 0
c decisions	: 761967
c propagations	: 1494440
c inspects	: 2125308
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=1698791424
c Current CPU time (ms) : 571.909
c starts	: 142
c conflicts	: 0
c decisions	: 767371
c propagations	: 1505034
c inspects	: 2140362
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=1698791424
c Current CPU time (ms) : 575.688
c starts	: 143
c conflicts	: 0
c decisions	: 772775
c propagations	: 1515628
c inspects	: 2155416
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=1698791424
c Current CPU time (ms) : 579.452
c starts	: 144
c conflicts	: 0
c decisions	: 778179
c propagations	: 1526222
c inspects	: 2170470
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=1698791424
c Current CPU time (ms) : 583.189
c starts	: 145
c conflicts	: 0
c decisions	: 783583
c propagations	: 1536816
c inspects	: 2185524
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=1698791424
c Current CPU time (ms) : 586.954
c starts	: 146
c conflicts	: 0
c decisions	: 788987
c propagations	: 1547410
c inspects	: 2200578
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=1698791424
c Current CPU time (ms) : 590.747
c starts	: 147
c conflicts	: 0
c decisions	: 794391
c propagations	: 1558004
c inspects	: 2215632
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=1698791424
c Current CPU time (ms) : 594.497
c starts	: 148
c conflicts	: 0
c decisions	: 799795
c propagations	: 1568598
c inspects	: 2230686
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=1698791424
c Current CPU time (ms) : 598.26
c starts	: 149
c conflicts	: 0
c decisions	: 805199
c propagations	: 1579192
c inspects	: 2245740
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=1698791424
c Current CPU time (ms) : 601.935
c starts	: 150
c conflicts	: 0
c decisions	: 810603
c propagations	: 1589786
c inspects	: 2260794
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=1698791424
c Current CPU time (ms) : 605.692
c starts	: 151
c conflicts	: 0
c decisions	: 816007
c propagations	: 1600380
c inspects	: 2275848
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=1698791424
c Current CPU time (ms) : 609.448
c starts	: 152
c conflicts	: 0
c decisions	: 821411
c propagations	: 1610974
c inspects	: 2290902
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=1698791424
c Current CPU time (ms) : 613.219
c starts	: 153
c conflicts	: 0
c decisions	: 826815
c propagations	: 1621568
c inspects	: 2305956
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=1698791424
c Current CPU time (ms) : 617.023
c starts	: 154
c conflicts	: 0
c decisions	: 832219
c propagations	: 1632162
c inspects	: 2321010
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=1698791424
c Current CPU time (ms) : 620.776
c starts	: 155
c conflicts	: 0
c decisions	: 837623
c propagations	: 1642756
c inspects	: 2336064
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=1698791424
c Current CPU time (ms) : 624.546
c starts	: 156
c conflicts	: 0
c decisions	: 843027
c propagations	: 1653350
c inspects	: 2351118
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=1698791424
c Current CPU time (ms) : 628.226
c starts	: 157
c conflicts	: 0
c decisions	: 848431
c propagations	: 1663944
c inspects	: 2366172
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=1698791424
c Current CPU time (ms) : 631.995
c starts	: 158
c conflicts	: 0
c decisions	: 853835
c propagations	: 1674538
c inspects	: 2381226
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=1698791424
c Current CPU time (ms) : 635.747
c starts	: 159
c conflicts	: 0
c decisions	: 859239
c propagations	: 1685132
c inspects	: 2396280
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=1698791424
c Current CPU time (ms) : 639.513
c starts	: 160
c conflicts	: 0
c decisions	: 864643
c propagations	: 1695726
c inspects	: 2411334
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=1698791424
c Current CPU time (ms) : 643.322
c starts	: 161
c conflicts	: 0
c decisions	: 870047
c propagations	: 1706320
c inspects	: 2426388
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=1698791424
c Current CPU time (ms) : 647.139
c starts	: 162
c conflicts	: 0
c decisions	: 875451
c propagations	: 1716914
c inspects	: 2441442
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=1698791424
c Current CPU time (ms) : 650.945
c starts	: 163
c conflicts	: 0
c decisions	: 880855
c propagations	: 1727508
c inspects	: 2456496
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=1698791424
c Current CPU time (ms) : 654.661
c starts	: 164
c conflicts	: 0
c decisions	: 886259
c propagations	: 1738102
c inspects	: 2471550
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=1698791424
c Current CPU time (ms) : 658.468
c starts	: 165
c conflicts	: 0
c decisions	: 891663
c propagations	: 1748696
c inspects	: 2486604
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=1698791424
c Current CPU time (ms) : 662.307
c starts	: 166
c conflicts	: 0
c decisions	: 897067
c propagations	: 1759290
c inspects	: 2501658
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=1698791424
c Current CPU time (ms) : 666.159
c starts	: 167
c conflicts	: 0
c decisions	: 902471
c propagations	: 1769884
c inspects	: 2516712
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=1698791424
c Current CPU time (ms) : 669.928
c starts	: 168
c conflicts	: 0
c decisions	: 907875
c propagations	: 1780478
c inspects	: 2531766
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=1698791424
c Current CPU time (ms) : 673.698
c starts	: 169
c conflicts	: 0
c decisions	: 913279
c propagations	: 1791072
c inspects	: 2546820
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=1698791424
c Current CPU time (ms) : 677.473
c starts	: 170
c conflicts	: 0
c decisions	: 918683
c propagations	: 1801666
c inspects	: 2561874
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=1698791424
c Current CPU time (ms) : 681.251
c starts	: 171
c conflicts	: 0
c decisions	: 924087
c propagations	: 1812260
c inspects	: 2576928
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=1698791424
c Current CPU time (ms) : 684.926
c starts	: 172
c conflicts	: 0
c decisions	: 929491
c propagations	: 1822854
c inspects	: 2591982
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=1698791424
c Current CPU time (ms) : 688.691
c starts	: 173
c conflicts	: 0
c decisions	: 934895
c propagations	: 1833448
c inspects	: 2607036
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=1698791424
c Current CPU time (ms) : 692.453
c starts	: 174
c conflicts	: 0
c decisions	: 940299
c propagations	: 1844042
c inspects	: 2622090
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=1698791424
c Current CPU time (ms) : 696.219
c starts	: 175
c conflicts	: 0
c decisions	: 945703
c propagations	: 1854636
c inspects	: 2637144
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=1698791424
c Current CPU time (ms) : 700.003
c starts	: 176
c conflicts	: 0
c decisions	: 951107
c propagations	: 1865230
c inspects	: 2652198
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=1698791424
c Current CPU time (ms) : 703.793
c starts	: 177
c conflicts	: 0
c decisions	: 956511
c propagations	: 1875824
c inspects	: 2667252
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=1698791424
c Current CPU time (ms) : 707.598
c starts	: 178
c conflicts	: 0
c decisions	: 961915
c propagations	: 1886418
c inspects	: 2682306
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=1698791424
c Current CPU time (ms) : 711.321
c starts	: 179
c conflicts	: 0
c decisions	: 967319
c propagations	: 1897012
c inspects	: 2697360
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=1698791424
c Current CPU time (ms) : 715.125
c starts	: 180
c conflicts	: 0
c decisions	: 972723
c propagations	: 1907606
c inspects	: 2712414
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=1698791424
c Current CPU time (ms) : 718.939
c starts	: 181
c conflicts	: 0
c decisions	: 978127
c propagations	: 1918200
c inspects	: 2727468
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=1698791424
c Current CPU time (ms) : 722.733
c starts	: 182
c conflicts	: 0
c decisions	: 983531
c propagations	: 1928794
c inspects	: 2742522
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=1698791424
c Current CPU time (ms) : 726.53
c starts	: 183
c conflicts	: 0
c decisions	: 988935
c propagations	: 1939388
c inspects	: 2757576
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=1698791424
c Current CPU time (ms) : 730.327
c starts	: 184
c conflicts	: 0
c decisions	: 994339
c propagations	: 1949982
c inspects	: 2772630
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=1698791424
c Current CPU time (ms) : 734.144
c starts	: 185
c conflicts	: 0
c decisions	: 999743
c propagations	: 1960576
c inspects	: 2787684
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=1698791424
c Current CPU time (ms) : 737.873
c starts	: 186
c conflicts	: 0
c decisions	: 1005147
c propagations	: 1971170
c inspects	: 2802738
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=1698791424
c Current CPU time (ms) : 741.696
c starts	: 187
c conflicts	: 0
c decisions	: 1010551
c propagations	: 1981764
c inspects	: 2817792
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=1698791424
c Current CPU time (ms) : 745.507
c starts	: 188
c conflicts	: 0
c decisions	: 1015955
c propagations	: 1992358
c inspects	: 2832846
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=1698791424
c Current CPU time (ms) : 749.325
c starts	: 189
c conflicts	: 0
c decisions	: 1021359
c propagations	: 2002952
c inspects	: 2847900
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=1698791424
c Current CPU time (ms) : 753.134
c starts	: 190
c conflicts	: 0
c decisions	: 1026763
c propagations	: 2013546
c inspects	: 2862954
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=1698791424
c Current CPU time (ms) : 756.945
c starts	: 191
c conflicts	: 0
c decisions	: 1032167
c propagations	: 2024140
c inspects	: 2878008
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=1698791424
c Current CPU time (ms) : 760.756
c starts	: 192
c conflicts	: 0
c decisions	: 1037571
c propagations	: 2034734
c inspects	: 2893062
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=1698791424
c Current CPU time (ms) : 764.612
c starts	: 193
c conflicts	: 0
c decisions	: 1042975
c propagations	: 2045328
c inspects	: 2908116
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=1698791424
c Current CPU time (ms) : 768.318
c starts	: 194
c conflicts	: 0
c decisions	: 1048379
c propagations	: 2055922
c inspects	: 2923170
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=1698791424
c Current CPU time (ms) : 772.09
c starts	: 195
c conflicts	: 0
c decisions	: 1053783
c propagations	: 2066516
c inspects	: 2938224
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=1698791424
c Current CPU time (ms) : 775.839
c starts	: 196
c conflicts	: 0
c decisions	: 1059187
c propagations	: 2077110
c inspects	: 2953278
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=1698791424
c Current CPU time (ms) : 779.626
c starts	: 197
c conflicts	: 0
c decisions	: 1064591
c propagations	: 2087704
c inspects	: 2968332
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=1698791424
c Current CPU time (ms) : 783.45
c starts	: 198
c conflicts	: 0
c decisions	: 1069995
c propagations	: 2098298
c inspects	: 2983386
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=1698791424
c Current CPU time (ms) : 787.311
c starts	: 199
c conflicts	: 0
c decisions	: 1075399
c propagations	: 2108892
c inspects	: 2998440
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=1698791424
c Current CPU time (ms) : 791.087
c starts	: 200
c conflicts	: 0
c decisions	: 1080803
c propagations	: 2119486
c inspects	: 3013494
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=1698791424
c Current CPU time (ms) : 794.827
c starts	: 201
c conflicts	: 0
c decisions	: 1086207
c propagations	: 2130080
c inspects	: 3028548
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=1698791424
c Current CPU time (ms) : 798.681
c starts	: 202
c conflicts	: 0
c decisions	: 1091611
c propagations	: 2140674
c inspects	: 3043602
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=1698791424
c Current CPU time (ms) : 802.537
c starts	: 203
c conflicts	: 0
c decisions	: 1097015
c propagations	: 2151268
c inspects	: 3058656
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=1698791424
c Current CPU time (ms) : 806.394
c starts	: 204
c conflicts	: 0
c decisions	: 1102419
c propagations	: 2161862
c inspects	: 3073710
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=1698791424
c Current CPU time (ms) : 810.272
c starts	: 205
c conflicts	: 0
c decisions	: 1107823
c propagations	: 2172456
c inspects	: 3088764
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=1698791424
c Current CPU time (ms) : 814.151
c starts	: 206
c conflicts	: 0
c decisions	: 1113227
c propagations	: 2183050
c inspects	: 3103818
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=1698791424
c Current CPU time (ms) : 818.028
c starts	: 207
c conflicts	: 0
c decisions	: 1118631
c propagations	: 2193644
c inspects	: 3118872
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=1698791424
c Current CPU time (ms) : 821.907
c starts	: 208
c conflicts	: 0
c decisions	: 1124035
c propagations	: 2204238
c inspects	: 3133926
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=1698791424
c Current CPU time (ms) : 825.689
c starts	: 209
c conflicts	: 0
c decisions	: 1129439
c propagations	: 2214832
c inspects	: 3148980
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=1698791424
c Current CPU time (ms) : 829.557
c starts	: 210
c conflicts	: 0
c decisions	: 1134843
c propagations	: 2225426
c inspects	: 3164034
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=1698791424
c Current CPU time (ms) : 833.433
c starts	: 211
c conflicts	: 0
c decisions	: 1140247
c propagations	: 2236020
c inspects	: 3179088
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=1698791424
c Current CPU time (ms) : 837.329
c starts	: 212
c conflicts	: 0
c decisions	: 1145651
c propagations	: 2246614
c inspects	: 3194142
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=1698791424
c Current CPU time (ms) : 841.227
c starts	: 213
c conflicts	: 0
c decisions	: 1151055
c propagations	: 2257208
c inspects	: 3209196
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=1698791424
c Current CPU time (ms) : 845.124
c starts	: 214
c conflicts	: 0
c decisions	: 1156459
c propagations	: 2267802
c inspects	: 3224250
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=1698791424
c Current CPU time (ms) : 849.027
c starts	: 215
c conflicts	: 0
c decisions	: 1161863
c propagations	: 2278396
c inspects	: 3239304
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=1698791424
c Current CPU time (ms) : 852.837
c starts	: 216
c conflicts	: 0
c decisions	: 1167267
c propagations	: 2288990
c inspects	: 3254358
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=1698791424
c Current CPU time (ms) : 856.73
c starts	: 217
c conflicts	: 0
c decisions	: 1172671
c propagations	: 2299584
c inspects	: 3269412
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=1698791424
c Current CPU time (ms) : 860.628
c starts	: 218
c conflicts	: 0
c decisions	: 1178075
c propagations	: 2310178
c inspects	: 3284466
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=1698791424
c Current CPU time (ms) : 864.529
c starts	: 219
c conflicts	: 0
c decisions	: 1183479
c propagations	: 2320772
c inspects	: 3299520
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=1698791424
c Current CPU time (ms) : 868.438
c starts	: 220
c conflicts	: 0
c decisions	: 1188883
c propagations	: 2331366
c inspects	: 3314574
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=1698791424
c Current CPU time (ms) : 872.334
c starts	: 221
c conflicts	: 0
c decisions	: 1194287
c propagations	: 2341960
c inspects	: 3329628
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=1698791424
c Current CPU time (ms) : 876.245
c starts	: 222
c conflicts	: 0
c decisions	: 1199691
c propagations	: 2352554
c inspects	: 3344682
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=1698791424
c Current CPU time (ms) : 880.048
c starts	: 223
c conflicts	: 0
c decisions	: 1205095
c propagations	: 2363148
c inspects	: 3359736
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=1698791424
c Current CPU time (ms) : 883.944
c starts	: 224
c conflicts	: 0
c decisions	: 1210499
c propagations	: 2373742
c inspects	: 3374790
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=1698791424
c Current CPU time (ms) : 887.845
c starts	: 225
c conflicts	: 0
c decisions	: 1215903
c propagations	: 2384336
c inspects	: 3389844
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=1698791424
c Current CPU time (ms) : 891.738
c starts	: 226
c conflicts	: 0
c decisions	: 1221307
c propagations	: 2394930
c inspects	: 3404898
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=1698791424
c Current CPU time (ms) : 895.636
c starts	: 227
c conflicts	: 0
c decisions	: 1226711
c propagations	: 2405524
c inspects	: 3419952
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=1698791424
c Current CPU time (ms) : 899.558
c starts	: 228
c conflicts	: 0
c decisions	: 1232115
c propagations	: 2416118
c inspects	: 3435006
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=1698791424
c Current CPU time (ms) : 903.473
c starts	: 229
c conflicts	: 0
c decisions	: 1237519
c propagations	: 2426712
c inspects	: 3450060
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=1698791424
c Current CPU time (ms) : 907.392
c starts	: 230
c conflicts	: 0
c decisions	: 1242923
c propagations	: 2437306
c inspects	: 3465114
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=1698791424
c Current CPU time (ms) : 911.151
c starts	: 231
c conflicts	: 0
c decisions	: 1248327
c propagations	: 2447900
c inspects	: 3480168
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=1698791424
c Current CPU time (ms) : 915.025
c starts	: 232
c conflicts	: 0
c decisions	: 1253731
c propagations	: 2458494
c inspects	: 3495222
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=1698791424
c Current CPU time (ms) : 918.889
c starts	: 233
c conflicts	: 0
c decisions	: 1259135
c propagations	: 2469088
c inspects	: 3510276
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=1698791424
c Current CPU time (ms) : 922.751
c starts	: 234
c conflicts	: 0
c decisions	: 1264539
c propagations	: 2479682
c inspects	: 3525330
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=1698791424
c Current CPU time (ms) : 926.604
c starts	: 235
c conflicts	: 0
c decisions	: 1269943
c propagations	: 2490276
c inspects	: 3540384
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=1698791424
c Current CPU time (ms) : 930.487
c starts	: 236
c conflicts	: 0
c decisions	: 1275347
c propagations	: 2500870
c inspects	: 3555438
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=1698791424
c Current CPU time (ms) : 934.39
c starts	: 237
c conflicts	: 0
c decisions	: 1280751
c propagations	: 2511464
c inspects	: 3570492
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=1698791424
c Current CPU time (ms) : 938.159
c starts	: 238
c conflicts	: 0
c decisions	: 1286155
c propagations	: 2522058
c inspects	: 3585546
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=1698791424
c Current CPU time (ms) : 942.041
c starts	: 239
c conflicts	: 0
c decisions	: 1291559
c propagations	: 2532652
c inspects	: 3600600
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=1698791424
c Current CPU time (ms) : 945.93
c starts	: 240
c conflicts	: 0
c decisions	: 1296963
c propagations	: 2543246
c inspects	: 3615654
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=1698791424
c Current CPU time (ms) : 949.823
c starts	: 241
c conflicts	: 0
c decisions	: 1302367
c propagations	: 2553840
c inspects	: 3630708
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=1698791424
c Current CPU time (ms) : 953.716
c starts	: 242
c conflicts	: 0
c decisions	: 1307771
c propagations	: 2564434
c inspects	: 3645762
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=1698791424
c Current CPU time (ms) : 957.599
c starts	: 243
c conflicts	: 0
c decisions	: 1313175
c propagations	: 2575028
c inspects	: 3660816
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=1698791424
c Current CPU time (ms) : 961.495
c starts	: 244
c conflicts	: 0
c decisions	: 1318579
c propagations	: 2585622
c inspects	: 3675870
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=1698791424
c Current CPU time (ms) : 965.323
c starts	: 245
c conflicts	: 0
c decisions	: 1323983
c propagations	: 2596216
c inspects	: 3690924
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=1698791424
c Current CPU time (ms) : 969.27
c starts	: 246
c conflicts	: 0
c decisions	: 1329387
c propagations	: 2606810
c inspects	: 3705978
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=1698791424
c Current CPU time (ms) : 973.153
c starts	: 247
c conflicts	: 0
c decisions	: 1334791
c propagations	: 2617404
c inspects	: 3721032
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=1698791424
c Current CPU time (ms) : 977.05
c starts	: 248
c conflicts	: 0
c decisions	: 1340195
c propagations	: 2627998
c inspects	: 3736086
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=1698791424
c Current CPU time (ms) : 980.953
c starts	: 249
c conflicts	: 0
c decisions	: 1345599
c propagations	: 2638592
c inspects	: 3751140
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=1698791424
c Current CPU time (ms) : 984.849
c starts	: 250
c conflicts	: 0
c decisions	: 1351003
c propagations	: 2649186
c inspects	: 3766194
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=1698791424
c Current CPU time (ms) : 988.753
c starts	: 251
c conflicts	: 0
c decisions	: 1356407
c propagations	: 2659780
c inspects	: 3781248
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=1698791424
c Current CPU time (ms) : 992.653
c starts	: 252
c conflicts	: 0
c decisions	: 1361811
c propagations	: 2670374
c inspects	: 3796302
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=1698791424
c Current CPU time (ms) : 996.459
c starts	: 253
c conflicts	: 0
c decisions	: 1367215
c propagations	: 2680968
c inspects	: 3811356
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=1698791424
c Current CPU time (ms) : 1000.36
c starts	: 254
c conflicts	: 0
c decisions	: 1372619
c propagations	: 2691562
c inspects	: 3826410
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=1698791424
c Current CPU time (ms) : 1004.274
c starts	: 255
c conflicts	: 0
c decisions	: 1378023
c propagations	: 2702156
c inspects	: 3841464
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=1698791424
c Current CPU time (ms) : 1008.18
c starts	: 256
c conflicts	: 0
c decisions	: 1383427
c propagations	: 2712750
c inspects	: 3856518
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=1698791424
c Current CPU time (ms) : 1012.133
c starts	: 257
c conflicts	: 0
c decisions	: 1388831
c propagations	: 2723344
c inspects	: 3871572
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=1698791424
c Current CPU time (ms) : 1015.963
c starts	: 258
c conflicts	: 0
c decisions	: 1394235
c propagations	: 2733938
c inspects	: 3886626
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=1698791424
c Current CPU time (ms) : 1019.785
c starts	: 259
c conflicts	: 0
c decisions	: 1399639
c propagations	: 2744532
c inspects	: 3901680
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=1698791424
c Current CPU time (ms) : 1023.534
c starts	: 260
c conflicts	: 0
c decisions	: 1405043
c propagations	: 2755126
c inspects	: 3916734
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=1698791424
c Current CPU time (ms) : 1027.35
c starts	: 261
c conflicts	: 0
c decisions	: 1410447
c propagations	: 2765720
c inspects	: 3931788
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=1698791424
c Current CPU time (ms) : 1031.214
c starts	: 262
c conflicts	: 0
c decisions	: 1415851
c propagations	: 2776314
c inspects	: 3946842
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=1698791424
c Current CPU time (ms) : 1035.112
c starts	: 263
c conflicts	: 0
c decisions	: 1421255
c propagations	: 2786908
c inspects	: 3961896
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=1698791424
c Current CPU time (ms) : 1039.024
c starts	: 264
c conflicts	: 0
c decisions	: 1426659
c propagations	: 2797502
c inspects	: 3976950
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=1698791424
c Current CPU time (ms) : 1042.931
c starts	: 265
c conflicts	: 0
c decisions	: 1432063
c propagations	: 2808096
c inspects	: 3992004
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=1698791424
c Current CPU time (ms) : 1046.848
c starts	: 266
c conflicts	: 0
c decisions	: 1437467
c propagations	: 2818690
c inspects	: 4007058
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=1698791424
c Current CPU time (ms) : 1050.787
c starts	: 267
c conflicts	: 0
c decisions	: 1442871
c propagations	: 2829284
c inspects	: 4022112
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=1698791424
c Current CPU time (ms) : 1054.636
c starts	: 268
c conflicts	: 0
c decisions	: 1448275
c propagations	: 2839878
c inspects	: 4037166
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=1698791424
c Current CPU time (ms) : 1058.471
c starts	: 269
c conflicts	: 0
c decisions	: 1453679
c propagations	: 2850472
c inspects	: 4052220
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=1698791424
c Current CPU time (ms) : 1062.268
c starts	: 270
c conflicts	: 0
c decisions	: 1459083
c propagations	: 2861066
c inspects	: 4067274
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=1698791424
c Current CPU time (ms) : 1066.073
c starts	: 271
c conflicts	: 0
c decisions	: 1464487
c propagations	: 2871660
c inspects	: 4082328
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=1698791424
c Current CPU time (ms) : 1069.908
c starts	: 272
c conflicts	: 0
c decisions	: 1469891
c propagations	: 2882254
c inspects	: 4097382
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=1698791424
c Current CPU time (ms) : 1074.144
c starts	: 273
c conflicts	: 0
c decisions	: 1475295
c propagations	: 2892848
c inspects	: 4112436
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=1698791424
c Current CPU time (ms) : 1078.049
c starts	: 274
c conflicts	: 0
c decisions	: 1480699
c propagations	: 2903442
c inspects	: 4127490
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=1698791424
c Current CPU time (ms) : 1081.975
c starts	: 275
c conflicts	: 0
c decisions	: 1486103
c propagations	: 2914036
c inspects	: 4142544
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=1698791424
c Current CPU time (ms) : 1085.907
c starts	: 276
c conflicts	: 0
c decisions	: 1491507
c propagations	: 2924630
c inspects	: 4157598
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=1698791424
c Current CPU time (ms) : 1089.869
c starts	: 277
c conflicts	: 0
c decisions	: 1496911
c propagations	: 2935224
c inspects	: 4172652
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=1698791424
c Current CPU time (ms) : 1093.845
c starts	: 278
c conflicts	: 0
c decisions	: 1502315
c propagations	: 2945818
c inspects	: 4187706
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=1698791424
c Current CPU time (ms) : 1097.671
c starts	: 279
c conflicts	: 0
c decisions	: 1507719
c propagations	: 2956412
c inspects	: 4202760
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=1698791424
c Current CPU time (ms) : 1101.621
c starts	: 280
c conflicts	: 0
c decisions	: 1513123
c propagations	: 2967006
c inspects	: 4217814
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=1698791424
c Current CPU time (ms) : 1105.493
c starts	: 281
c conflicts	: 0
c decisions	: 1518527
c propagations	: 2977600
c inspects	: 4232868
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=1698791424
c Current CPU time (ms) : 1109.323
c starts	: 282
c conflicts	: 0
c decisions	: 1523931
c propagations	: 2988194
c inspects	: 4247922
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=1698791424
c Current CPU time (ms) : 1113.155
c starts	: 283
c conflicts	: 0
c decisions	: 1529335
c propagations	: 2998788
c inspects	: 4262976
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=1698791424
c Current CPU time (ms) : 1116.99
c starts	: 284
c conflicts	: 0
c decisions	: 1534739
c propagations	: 3009382
c inspects	: 4278030
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=1698791424
c Current CPU time (ms) : 1120.867
c starts	: 285
c conflicts	: 0
c decisions	: 1540143
c propagations	: 3019976
c inspects	: 4293084
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=1698791424
c Current CPU time (ms) : 1124.719
c starts	: 286
c conflicts	: 0
c decisions	: 1545547
c propagations	: 3030570
c inspects	: 4308138
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=1698791424
c Current CPU time (ms) : 1128.641
c starts	: 287
c conflicts	: 0
c decisions	: 1550951
c propagations	: 3041164
c inspects	: 4323192
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=1698791424
c Current CPU time (ms) : 1132.536
c starts	: 288
c conflicts	: 0
c decisions	: 1556355
c propagations	: 3051758
c inspects	: 4338246
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=1698791424
c Current CPU time (ms) : 1136.434
c starts	: 289
c conflicts	: 0
c decisions	: 1561759
c propagations	: 3062352
c inspects	: 4353300
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=1698791424
c Current CPU time (ms) : 1140.334
c starts	: 290
c conflicts	: 0
c decisions	: 1567163
c propagations	: 3072946
c inspects	: 4368354
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=1698791424
c Current CPU time (ms) : 1144.223
c starts	: 291
c conflicts	: 0
c decisions	: 1572567
c propagations	: 3083540
c inspects	: 4383408
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=1698791424
c Current CPU time (ms) : 1148.142
c starts	: 292
c conflicts	: 0
c decisions	: 1577971
c propagations	: 3094134
c inspects	: 4398462
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=1698791424
c Current CPU time (ms) : 1152.117
c starts	: 293
c conflicts	: 0
c decisions	: 1583375
c propagations	: 3104728
c inspects	: 4413516
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=1698791424
c Current CPU time (ms) : 1155.92
c starts	: 294
c conflicts	: 0
c decisions	: 1588779
c propagations	: 3115322
c inspects	: 4428570
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=1698791424
c Current CPU time (ms) : 1159.766
c starts	: 295
c conflicts	: 0
c decisions	: 1594183
c propagations	: 3125916
c inspects	: 4443624
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=1698791424
c Current CPU time (ms) : 1163.602
c starts	: 296
c conflicts	: 0
c decisions	: 1599587
c propagations	: 3136510
c inspects	: 4458678
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=1698791424
c Current CPU time (ms) : 1167.461
c starts	: 297
c conflicts	: 0
c decisions	: 1604991
c propagations	: 3147104
c inspects	: 4473732
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=1698791424
c Current CPU time (ms) : 1171.349
c starts	: 298
c conflicts	: 0
c decisions	: 1610395
c propagations	: 3157698
c inspects	: 4488786
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=1698791424
c Current CPU time (ms) : 1175.27
c starts	: 299
c conflicts	: 0
c decisions	: 1615799
c propagations	: 3168292
c inspects	: 4503840
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=1698791424
c Current CPU time (ms) : 1179.232
c starts	: 300
c conflicts	: 0
c decisions	: 1621203
c propagations	: 3178886
c inspects	: 4518894
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=1698791424
c Current CPU time (ms) : 1183.124
c starts	: 301
c conflicts	: 0
c decisions	: 1626607
c propagations	: 3189480
c inspects	: 4533948
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=1698791424
c Current CPU time (ms) : 1187.103
c starts	: 302
c conflicts	: 0
c decisions	: 1632011
c propagations	: 3200074
c inspects	: 4549002
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=1698791424
c Current CPU time (ms) : 1191.09
c starts	: 303
c conflicts	: 0
c decisions	: 1637415
c propagations	: 3210668
c inspects	: 4564056
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=1698791424
c Current CPU time (ms) : 1195.054
c starts	: 304
c conflicts	: 0
c decisions	: 1642819
c propagations	: 3221262
c inspects	: 4579110
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=1698791424
c Current CPU time (ms) : 1199.03
c starts	: 305
c conflicts	: 0
c decisions	: 1648223
c propagations	: 3231856
c inspects	: 4594164
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=1698791424
c Current CPU time (ms) : 1203.021
c starts	: 306
c conflicts	: 0
c decisions	: 1653627
c propagations	: 3242450
c inspects	: 4609218
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=1698791424
c Current CPU time (ms) : 1207.008
c starts	: 307
c conflicts	: 0
c decisions	: 1659031
c propagations	: 3253044
c inspects	: 4624272
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=1698791424
c Current CPU time (ms) : 1211.005
c starts	: 308
c conflicts	: 0
c decisions	: 1664435
c propagations	: 3263638
c inspects	: 4639326
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=1698791424
c Current CPU time (ms) : 1214.792
c starts	: 309
c conflicts	: 0
c decisions	: 1669839
c propagations	: 3274232
c inspects	: 4654380
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=1698791424
c Current CPU time (ms) : 1218.599
c starts	: 310
c conflicts	: 0
c decisions	: 1675243
c propagations	: 3284826
c inspects	: 4669434
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=1698791424
c Current CPU time (ms) : 1222.41
c starts	: 311
c conflicts	: 0
c decisions	: 1680647
c propagations	: 3295420
c inspects	: 4684488
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=1698791424
c Current CPU time (ms) : 1226.259
c starts	: 312
c conflicts	: 0
c decisions	: 1686051
c propagations	: 3306014
c inspects	: 4699542
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=1698791424
c Current CPU time (ms) : 1230.16
c starts	: 313
c conflicts	: 0
c decisions	: 1691455
c propagations	: 3316608
c inspects	: 4714596
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=1698791424
c Current CPU time (ms) : 1234.086
c starts	: 314
c conflicts	: 0
c decisions	: 1696859
c propagations	: 3327202
c inspects	: 4729650
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=1698791424
c Current CPU time (ms) : 1238.056
c starts	: 315
c conflicts	: 0
c decisions	: 1702263
c propagations	: 3337796
c inspects	: 4744704
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=1698791424
c Current CPU time (ms) : 1241.964
c starts	: 316
c conflicts	: 0
c decisions	: 1707667
c propagations	: 3348390
c inspects	: 4759758
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=1698791424
c Current CPU time (ms) : 1245.93
c starts	: 317
c conflicts	: 0
c decisions	: 1713071
c propagations	: 3358984
c inspects	: 4774812
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=1698791424
c Current CPU time (ms) : 1249.887
c starts	: 318
c conflicts	: 0
c decisions	: 1718475
c propagations	: 3369578
c inspects	: 4789866
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=1698791424
c Current CPU time (ms) : 1253.839
c starts	: 319
c conflicts	: 0
c decisions	: 1723879
c propagations	: 3380172
c inspects	: 4804920
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=1698791424
c Current CPU time (ms) : 1257.807
c starts	: 320
c conflicts	: 0
c decisions	: 1729283
c propagations	: 3390766
c inspects	: 4819974
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=1698791424
c Current CPU time (ms) : 1261.774
c starts	: 321
c conflicts	: 0
c decisions	: 1734687
c propagations	: 3401360
c inspects	: 4835028
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=1698791424
c Current CPU time (ms) : 1265.724
c starts	: 322
c conflicts	: 0
c decisions	: 1740091
c propagations	: 3411954
c inspects	: 4850082
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=1698791424
c Current CPU time (ms) : 1269.709
c starts	: 323
c conflicts	: 0
c decisions	: 1745495
c propagations	: 3422548
c inspects	: 4865136
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=1698791424
c Current CPU time (ms) : 1273.609
c starts	: 324
c conflicts	: 0
c decisions	: 1750899
c propagations	: 3433142
c inspects	: 4880190
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=1698791424
c Current CPU time (ms) : 1277.583
c starts	: 325
c conflicts	: 0
c decisions	: 1756303
c propagations	: 3443736
c inspects	: 4895244
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=1698791424
c Current CPU time (ms) : 1281.548
c starts	: 326
c conflicts	: 0
c decisions	: 1761707
c propagations	: 3454330
c inspects	: 4910298
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=1698791424
c Current CPU time (ms) : 1285.515
c starts	: 327
c conflicts	: 0
c decisions	: 1767111
c propagations	: 3464924
c inspects	: 4925352
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=1698791424
c Current CPU time (ms) : 1289.466
c starts	: 328
c conflicts	: 0
c decisions	: 1772515
c propagations	: 3475518
c inspects	: 4940406
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=1698791424
c Current CPU time (ms) : 1293.426
c starts	: 329
c conflicts	: 0
c decisions	: 1777919
c propagations	: 3486112
c inspects	: 4955460
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=1698791424
c Current CPU time (ms) : 1297.389
c starts	: 330
c conflicts	: 0
c decisions	: 1783323
c propagations	: 3496706
c inspects	: 4970514
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=1698791424
c Current CPU time (ms) : 1301.274
c starts	: 331
c conflicts	: 0
c decisions	: 1788727
c propagations	: 3507300
c inspects	: 4985568
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=1698791424
c Current CPU time (ms) : 1305.278
c starts	: 332
c conflicts	: 0
c decisions	: 1794131
c propagations	: 3517894
c inspects	: 5000622
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=1698791424
c Current CPU time (ms) : 1309.338
c starts	: 333
c conflicts	: 0
c decisions	: 1799535
c propagations	: 3528488
c inspects	: 5015676
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=1698791424
c Current CPU time (ms) : 1313.22
c starts	: 334
c conflicts	: 0
c decisions	: 1804939
c propagations	: 3539082
c inspects	: 5030730
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=1698791424
c Current CPU time (ms) : 1317.073
c starts	: 335
c conflicts	: 0
c decisions	: 1810343
c propagations	: 3549676
c inspects	: 5045784
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=1698791424
c Current CPU time (ms) : 1320.929
c starts	: 336
c conflicts	: 0
c decisions	: 1815747
c propagations	: 3560270
c inspects	: 5060838
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=1698791424
c Current CPU time (ms) : 1324.814
c starts	: 337
c conflicts	: 0
c decisions	: 1821151
c propagations	: 3570864
c inspects	: 5075892
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=1698791424
c Current CPU time (ms) : 1328.739
c starts	: 338
c conflicts	: 0
c decisions	: 1826555
c propagations	: 3581458
c inspects	: 5090946
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 338
#### 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.74 0.92 0.90 2/54 25065
Raw data (stat): 25065 (runsolver) R 25064 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540611787 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.0001 s]
Raw data (loadavg): 0.78 0.92 0.90 2/63 25074
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 17972 0 1 0 875 42 0 0 25 0 10 0 540611787 853958656 19351 4294967295 134512640 134569956 3221224400 3221214700 1080204163 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208486 19351 13073 16 0 208470 0
vsize: 833944
[startup+20.0014 s]
Raw data (loadavg): 0.97 0.95 0.91 2/63 25074
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 17978 0 1 0 1693 43 0 0 25 0 10 0 540611787 857190400 21195 4294967295 134512640 134569956 3221224400 3221214740 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209275 21195 13073 16 0 209259 0
vsize: 837100
[startup+30.0013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/63 25074
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 17978 0 1 0 2551 44 0 0 25 0 10 0 540611787 857026560 21341 4294967295 134512640 134569956 3221224400 3221214836 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209235 21341 13073 16 0 209219 0
vsize: 836940
[startup+40.0011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/63 25074
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 17978 0 1 0 3408 44 0 0 25 0 10 0 540611787 857026560 21848 4294967295 134512640 134569956 3221224400 3221214312 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209235 21848 13073 16 0 209219 0
vsize: 836940
[startup+50.0017 s]
Raw data (loadavg): 0.98 0.96 0.91 2/64 25076
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 4260 45 0 0 25 0 11 0 540611787 857554944 22940 4294967295 134512640 134569956 3221224400 3221214680 1131304252 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 22940 13073 16 0 209348 0
vsize: 837456
[startup+60.0013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/64 25078
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 5158 45 0 0 25 0 11 0 540611787 857554944 23785 4294967295 134512640 134569956 3221224400 3221214624 1131303942 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 23785 13073 16 0 209348 0
vsize: 837456
[startup+70.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 25081
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 6065 46 0 0 25 0 11 0 540611787 857554944 23940 4294967295 134512640 134569956 3221224400 3221214624 1131303897 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 23940 13073 16 0 209348 0
vsize: 837456
[startup+80.0031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 25084
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 6969 46 0 0 25 0 11 0 540611787 857554944 24471 4294967295 134512640 134569956 3221224400 3221214624 1131303726 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 24471 13073 16 0 209348 0
vsize: 837456
[startup+90.0021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 25087
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 7895 46 0 0 25 0 11 0 540611787 857554944 24751 4294967295 134512640 134569956 3221224400 3221214716 1131304843 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 24751 13073 16 0 209348 0
vsize: 837456
[startup+100.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 25091
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 8810 46 0 0 25 0 11 0 540611787 857554944 25138 4294967295 134512640 134569956 3221224400 3221214624 1131304295 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 25138 13073 16 0 209348 0
vsize: 837456
[startup+110.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 25094
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 9707 46 0 0 25 0 11 0 540611787 857554944 26036 4294967295 134512640 134569956 3221224400 3221214624 1131304569 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 26036 13073 16 0 209348 0
vsize: 837456
[startup+120.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 25097
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 10641 47 1 0 25 0 11 0 540611787 857554944 26315 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 26315 13073 16 0 209348 0
vsize: 837456
[startup+130.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 25100
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 11568 47 1 0 25 0 11 0 540611787 857554944 26840 4294967295 134512640 134569956 3221224400 3221214624 1131304644 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 26840 13073 16 0 209348 0
vsize: 837456
[startup+140.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 25102
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 12479 47 1 0 25 0 11 0 540611787 857554944 27315 4294967295 134512640 134569956 3221224400 3221214720 1131354779 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 27315 13073 16 0 209348 0
vsize: 837456
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25105
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 13389 48 1 0 21 0 11 0 540611787 857554944 27678 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 27678 13073 16 0 209348 0
vsize: 837456
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25108
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 14288 48 1 0 24 0 11 0 540611787 857554944 28117 4294967295 134512640 134569956 3221224400 3221214624 1131303357 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 28117 13073 16 0 209348 0
vsize: 837456
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25111
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 15201 48 1 0 25 0 11 0 540611787 857554944 28400 4294967295 134512640 134569956 3221224400 3221214624 1131303563 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 28400 13073 16 0 209348 0
vsize: 837456
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25113
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 16141 48 1 0 25 0 11 0 540611787 857554944 30386 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 30386 13073 16 0 209348 0
vsize: 837456
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25116
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 17075 49 1 0 24 0 11 0 540611787 857554944 30386 4294967295 134512640 134569956 3221224400 3221214624 1131303698 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 30386 13073 16 0 209348 0
vsize: 837456
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25119
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 17990 50 1 0 25 0 11 0 540611787 857554944 30729 4294967295 134512640 134569956 3221224400 3221214624 1131303397 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 30729 13073 16 0 209348 0
vsize: 837456
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25122
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 18902 50 2 0 25 0 11 0 540611787 857554944 31180 4294967295 134512640 134569956 3221224400 3221214720 1131359414 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 31180 13073 16 0 209348 0
vsize: 837456
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25124
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 19820 50 2 0 25 0 11 0 540611787 857554944 31501 4294967295 134512640 134569956 3221224400 3221214624 1131303740 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 31501 13073 16 0 209348 0
vsize: 837456
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25127
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 20722 51 2 0 17 0 11 0 540611787 857554944 32085 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 32085 13073 16 0 209348 0
vsize: 837456
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25130
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 21635 51 2 0 25 0 11 0 540611787 857554944 32386 4294967295 134512640 134569956 3221224400 3221214624 1131304012 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 32386 13073 16 0 209348 0
vsize: 837456
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25132
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 22537 51 2 0 18 0 11 0 540611787 857554944 32723 4294967295 134512640 134569956 3221224400 3221214720 1131354896 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 32723 13073 16 0 209348 0
vsize: 837456
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25135
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 23445 51 2 0 20 0 11 0 540611787 857554944 33046 4294967295 134512640 134569956 3221224400 3221214720 1131355812 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 33046 13073 16 0 209348 0
vsize: 837456
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25138
Raw data (stat): 25065 (java) S 25064 3260 3259 0 -1 0 18012 4 1 0 24346 51 2 0 22 0 11 0 540611787 857554944 33327 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 33327 13073 16 0 209348 0
vsize: 837456
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25141
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 25245 52 2 0 22 0 11 0 540611787 857554944 33778 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 33778 13073 16 0 209348 0
vsize: 837456
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25143
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 26158 52 2 0 24 0 11 0 540611787 857554944 34269 4294967295 134512640 134569956 3221224400 3221214624 1131304826 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 34269 13073 16 0 209348 0
vsize: 837456
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25146
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 27080 52 2 1 25 0 11 0 540611787 857554944 37099 4294967295 134512640 134569956 3221224400 3221214624 1131303740 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 37099 13073 16 0 209348 0
vsize: 837456
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25149
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 28033 53 2 1 25 0 11 0 540611787 857554944 37099 4294967295 134512640 134569956 3221224400 3221214624 1131304024 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 37099 13073 16 0 209348 0
vsize: 837456
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 25151
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 28959 53 2 1 25 0 10 0 540611787 857554944 37246 4294967295 134512640 134569956 3221224400 3221214640 1131288506 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 37246 13073 16 0 209348 0
vsize: 837456
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25154
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 29865 54 3 1 18 0 11 0 540611787 857554944 37755 4294967295 134512640 134569956 3221224400 3221214624 1131303942 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 37755 13073 16 0 209348 0
vsize: 837456
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25157
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 30783 54 3 1 25 0 11 0 540611787 857554944 37996 4294967295 134512640 134569956 3221224400 3221214624 1131303740 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 37996 13073 16 0 209348 0
vsize: 837456
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25160
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 31697 55 3 1 25 0 11 0 540611787 857554944 38364 4294967295 134512640 134569956 3221224400 3221214624 1131303458 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 38364 13073 16 0 209348 0
vsize: 837456
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25162
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 32598 55 3 1 25 0 11 0 540611787 857554944 39007 4294967295 134512640 134569956 3221224400 3221214624 1131303397 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 39007 13073 16 0 209348 0
vsize: 837456
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25165
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 33515 56 3 1 25 0 11 0 540611787 857554944 39362 4294967295 134512640 134569956 3221224400 3221214624 1131304008 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 39362 13073 16 0 209348 0
vsize: 837456
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25168
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 34434 56 3 1 25 0 11 0 540611787 857554944 39755 4294967295 134512640 134569956 3221224400 3221214624 1131303778 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 39755 13073 16 0 209348 0
vsize: 837456
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25170
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 35337 57 3 1 25 0 11 0 540611787 857554944 40135 4294967295 134512640 134569956 3221224400 3221214624 1131303397 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 40135 13073 16 0 209348 0
vsize: 837456
[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25173
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 36248 57 3 1 19 0 11 0 540611787 857554944 40407 4294967295 134512640 134569956 3221224400 3221214720 1131359480 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 40407 13073 16 0 209348 0
vsize: 837456
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25176
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 37159 58 3 1 25 0 11 0 540611787 857554944 41219 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 41219 13073 16 0 209348 0
vsize: 837456
[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25178
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 38069 58 3 1 24 0 11 0 540611787 857554944 41595 4294967295 134512640 134569956 3221224400 3221214624 1131303361 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 41595 13073 16 0 209348 0
vsize: 837456
[startup+430.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25181
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 38982 59 4 1 25 0 11 0 540611787 857554944 42016 4294967295 134512640 134569956 3221224400 3221214624 1131304668 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 42016 13073 16 0 209348 0
vsize: 837456
[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25184
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 39893 60 4 1 25 0 11 0 540611787 857554944 42206 4294967295 134512640 134569956 3221224400 3221214624 1131303974 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 42206 13073 16 0 209348 0
vsize: 837456
[startup+450.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25186
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 40793 60 4 1 25 0 11 0 540611787 857554944 42537 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 42537 13073 16 0 209348 0
vsize: 837456
[startup+460.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25189
Raw data (stat): 25065 (java) S 25064 3260 3259 0 -1 0 18012 4 1 0 41690 61 4 1 25 0 11 0 540611787 857554944 42846 4294967295 134512640 134569956 3221224400 3221213328 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 42846 13073 16 0 209348 0
vsize: 837456
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25191
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 42589 61 4 2 25 0 11 0 540611787 857554944 43194 4294967295 134512640 134569956 3221224400 3221214624 1131303698 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 43194 13073 16 0 209348 0
vsize: 837456
[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25194
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 43490 62 4 2 25 0 11 0 540611787 857554944 43443 4294967295 134512640 134569956 3221224400 3221214624 1131303796 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 43443 13073 16 0 209348 0
vsize: 837456
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25197
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 44389 62 4 2 25 0 11 0 540611787 857554944 43769 4294967295 134512640 134569956 3221224400 3221214624 1131303740 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 43769 13073 16 0 209348 0
vsize: 837456
[startup+500.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25199
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 45290 63 5 2 25 0 11 0 540611787 857554944 44223 4294967295 134512640 134569956 3221224400 3221214884 1131379939 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 44223 13073 16 0 209348 0
vsize: 837456
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25202
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 46198 64 5 2 25 0 11 0 540611787 857554944 44458 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 44458 13073 16 0 209348 0
vsize: 837456
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25205
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 47109 64 5 2 25 0 11 0 540611787 857554944 44869 4294967295 134512640 134569956 3221224400 3221214624 1131303397 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 44869 13073 16 0 209348 0
vsize: 837456
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25207
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 48016 65 5 2 25 0 11 0 540611787 857554944 45428 4294967295 134512640 134569956 3221224400 3221214624 1131303575 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 45428 13073 16 0 209348 0
vsize: 837456
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25210
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 48931 66 5 2 25 0 11 0 540611787 857554944 45869 4294967295 134512640 134569956 3221224400 3221214624 1131303581 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 45869 13073 16 0 209348 0
vsize: 837456
[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25214
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 49853 67 5 3 24 0 11 0 540611787 857554944 46407 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 46407 13073 16 0 209348 0
vsize: 837456
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25221
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 50755 67 6 3 25 0 11 0 540611787 857554944 49606 4294967295 134512640 134569956 3221224400 3221214624 1131303740 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 49606 13073 16 0 209348 0
vsize: 837456
[startup+570.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25224
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 51670 68 6 3 17 0 11 0 540611787 857554944 50090 4294967295 134512640 134569956 3221224400 3221214624 1131303668 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 50090 13073 16 0 209348 0
vsize: 837456
[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25226
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 52590 68 6 3 25 0 11 0 540611787 857554944 50636 4294967295 134512640 134569956 3221224400 3221214576 1131320259 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 50636 13073 16 0 209348 0
vsize: 837456
[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25229
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 53504 68 6 3 25 0 11 0 540611787 857554944 50938 4294967295 134512640 134569956 3221224400 3221214624 1131304252 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 50938 13073 16 0 209348 0
vsize: 837456
[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25232
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 54411 68 6 3 24 0 11 0 540611787 857554944 51400 4294967295 134512640 134569956 3221224400 3221214920 1131216793 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 51400 13073 16 0 209348 0
vsize: 837456
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25234
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 55327 69 6 3 25 0 11 0 540611787 857554944 51780 4294967295 134512640 134569956 3221224400 3221214776 1131385554 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 51780 13073 16 0 209348 0
vsize: 837456
[startup+620.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25237
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 56237 69 6 3 25 0 11 0 540611787 857554944 52309 4294967295 134512640 134569956 3221224400 3221214624 1131303357 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 52309 13073 16 0 209348 0
vsize: 837456
[startup+630.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25240
Raw data (stat): 25065 (java) S 25064 3260 3259 0 -1 0 18012 4 1 0 57148 69 7 3 25 0 11 0 540611787 857554944 52582 4294967295 134512640 134569956 3221224400 3221213328 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 52582 13073 16 0 209348 0
vsize: 837456
[startup+640.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25242
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 58062 69 7 3 25 0 11 0 540611787 857554944 52988 4294967295 134512640 134569956 3221224400 3221214720 1131356670 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 52988 13073 16 0 209348 0
vsize: 837456
[startup+650.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25245
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 58964 70 7 3 25 0 11 0 540611787 857554944 53401 4294967295 134512640 134569956 3221224400 3221214624 1131303897 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 53401 13073 16 0 209348 0
vsize: 837456
[startup+660.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25248
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 59871 70 7 3 25 0 11 0 540611787 857554944 53604 4294967295 134512640 134569956 3221224400 3221214720 1131355765 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 53604 13073 16 0 209348 0
vsize: 837456
[startup+670.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25250
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 60775 70 7 3 25 0 11 0 540611787 857554944 54273 4294967295 134512640 134569956 3221224400 3221214624 1131303397 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 54273 13073 16 0 209348 0
vsize: 837456
[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25257
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 61683 70 7 3 24 0 11 0 540611787 857554944 54698 4294967295 134512640 134569956 3221224400 3221214624 1131303361 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 54698 13073 16 0 209348 0
vsize: 837456
[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25260
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 62602 71 7 3 25 0 11 0 540611787 857554944 55141 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 55141 13073 16 0 209348 0
vsize: 837456
[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25262
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 63520 71 7 4 25 0 11 0 540611787 857554944 55519 4294967295 134512640 134569956 3221224400 3221214624 1131303740 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 55519 13073 16 0 209348 0
vsize: 837456
[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25265
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 64430 71 7 4 25 0 11 0 540611787 857554944 55827 4294967295 134512640 134569956 3221224400 3221214624 1131303372 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 55827 13073 16 0 209348 0
vsize: 837456
[startup+720.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25268
Raw data (stat): 25065 (java) S 25064 3260 3259 0 -1 0 18012 4 1 0 65334 71 7 4 19 0 11 0 540611787 857554944 56312 4294967295 134512640 134569956 3221224400 3221213328 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 56312 13073 16 0 209348 0
vsize: 837456
[startup+730.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 25270
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 66242 71 7 4 25 0 11 0 540611787 857554944 56681 4294967295 134512640 134569956 3221224400 3221214720 1131356676 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 56681 13073 16 0 209348 0
vsize: 837456
[startup+740.057 s]
Raw data (loadavg): 1.06 0.99 0.91 2/64 25273
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 67148 71 8 4 25 0 11 0 540611787 857554944 57011 4294967295 134512640 134569956 3221224400 3221214664 1131344289 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 57011 13073 16 0 209348 0
vsize: 837456
[startup+750.058 s]
Raw data (loadavg): 1.05 0.99 0.91 2/64 25276
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 68059 72 8 4 25 0 11 0 540611787 857554944 57398 4294967295 134512640 134569956 3221224400 3221214760 1131328467 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 57398 13073 16 0 209348 0
vsize: 837456
[startup+760.057 s]
Raw data (loadavg): 1.04 0.99 0.91 2/64 25278
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18012 4 1 0 68966 72 8 4 25 0 11 0 540611787 857554944 57717 4294967295 134512640 134569956 3221224400 3221214624 1131303357 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 57717 13073 16 0 209348 0
vsize: 837456
[startup+770.058 s]
Raw data (loadavg): 1.04 0.99 0.91 2/64 25281
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 69876 73 8 4 25 0 11 0 540611787 857554944 58431 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 58431 13073 16 0 209348 0
vsize: 837456
[startup+780.07 s]
Raw data (loadavg): 1.03 0.99 0.91 2/64 25283
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 70792 73 8 4 25 0 11 0 540611787 857554944 58954 4294967295 134512640 134569956 3221224400 3221214624 1131303740 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 58954 13073 16 0 209348 0
vsize: 837456
[startup+790.069 s]
Raw data (loadavg): 1.03 0.99 0.91 2/64 25286
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 71700 73 8 4 25 0 11 0 540611787 857554944 59595 4294967295 134512640 134569956 3221224400 3221214624 1131303546 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 59595 13073 16 0 209348 0
vsize: 837456
[startup+800.08 s]
Raw data (loadavg): 1.02 0.99 0.91 2/64 25289
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 72616 73 9 4 25 0 11 0 540611787 857554944 59702 4294967295 134512640 134569956 3221224400 3221214624 1131303538 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 59702 13073 16 0 209348 0
vsize: 837456
[startup+810.08 s]
Raw data (loadavg): 1.02 0.99 0.91 2/64 25291
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 73527 73 9 4 25 0 11 0 540611787 857554944 60032 4294967295 134512640 134569956 3221224400 3221214624 1131303796 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 60032 13073 16 0 209348 0
vsize: 837456
[startup+820.08 s]
Raw data (loadavg): 1.01 0.99 0.91 2/64 25294
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 74433 74 9 4 25 0 11 0 540611787 857554944 60401 4294967295 134512640 134569956 3221224400 3221214624 1131303517 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 60401 13073 16 0 209348 0
vsize: 837456
[startup+830.088 s]
Raw data (loadavg): 1.01 0.99 0.91 2/64 25296
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 75341 74 9 4 25 0 11 0 540611787 857554944 60720 4294967295 134512640 134569956 3221224400 3221214720 1131356690 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 60720 13073 16 0 209348 0
vsize: 837456
[startup+840.088 s]
Raw data (loadavg): 1.01 0.99 0.91 2/64 25299
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 76244 75 9 4 25 0 11 0 540611787 857554944 61148 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 61148 13073 16 0 209348 0
vsize: 837456
[startup+850.093 s]
Raw data (loadavg): 1.01 0.99 0.91 2/64 25302
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 77148 76 9 4 25 0 11 0 540611787 857554944 61361 4294967295 134512640 134569956 3221224400 3221214624 1131303397 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 61361 13073 16 0 209348 0
vsize: 837456
[startup+860.093 s]
Raw data (loadavg): 1.01 0.99 0.91 2/64 25304
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 78048 76 9 4 25 0 11 0 540611787 857554944 61679 4294967295 134512640 134569956 3221224400 3221214624 1131304068 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 61679 13073 16 0 209348 0
vsize: 837456
[startup+870.093 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25307
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 78950 77 9 4 17 0 11 0 540611787 857554944 61952 4294967295 134512640 134569956 3221224400 3221214624 1131303563 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 61952 13073 16 0 209348 0
vsize: 837456
[startup+880.095 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25309
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 79852 77 9 4 18 0 11 0 540611787 857554944 62271 4294967295 134512640 134569956 3221224400 3221214716 1131304843 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 62271 13073 16 0 209348 0
vsize: 837456
[startup+890.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25312
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 80752 77 9 4 16 0 11 0 540611787 857554944 62589 4294967295 134512640 134569956 3221224400 3221214624 1131303372 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 62589 13073 16 0 209348 0
vsize: 837456
[startup+900.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25314
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 81653 78 9 4 17 0 11 0 540611787 857554944 62771 4294967295 134512640 134569956 3221224400 3221214624 1131303663 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 62771 13073 16 0 209348 0
vsize: 837456
[startup+910.103 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25317
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 82545 78 10 4 16 0 11 0 540611787 857554944 63206 4294967295 134512640 134569956 3221224400 3221214624 1131303528 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 63206 13073 16 0 209348 0
vsize: 837456
[startup+920.109 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25320
Raw data (stat): 25065 (java) S 25064 3260 3259 0 -1 0 18013 4 1 0 83451 79 10 4 25 0 11 0 540611787 857554944 63419 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 63419 13073 16 0 209348 0
vsize: 837456
[startup+930.113 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25322
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 84347 79 10 4 16 0 11 0 540611787 857554944 63655 4294967295 134512640 134569956 3221224400 3221214624 1131304026 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 63655 13073 16 0 209348 0
vsize: 837456
[startup+940.117 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25325
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 85245 79 10 4 16 0 11 0 540611787 857554944 64222 4294967295 134512640 134569956 3221224400 3221214720 1131354672 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 64222 13073 16 0 209348 0
vsize: 837456
[startup+950.117 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25327
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 86154 80 10 4 17 0 11 0 540611787 857554944 64435 4294967295 134512640 134569956 3221224400 3221214624 1131304826 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 64435 13073 16 0 209348 0
vsize: 837456
[startup+960.117 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25330
Raw data (stat): 25065 (java) S 25064 3260 3259 0 -1 0 18013 4 1 0 87060 80 10 4 22 0 11 0 540611787 857554944 64750 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 64750 13073 16 0 209348 0
vsize: 837456
[startup+970.118 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25333
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 87968 81 10 5 25 0 11 0 540611787 857554944 65119 4294967295 134512640 134569956 3221224400 3221214760 1131329267 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 65119 13073 16 0 209348 0
vsize: 837456
[startup+980.119 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25335
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 88874 81 10 5 25 0 11 0 540611787 857554944 65511 4294967295 134512640 134569956 3221224400 3221214624 1131303409 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 65511 13073 16 0 209348 0
vsize: 837456
[startup+990.119 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25338
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 89783 82 10 5 25 0 11 0 540611787 857554944 65832 4294967295 134512640 134569956 3221224400 3221214624 1131304274 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 65832 13073 16 0 209348 0
vsize: 837456
[startup+1000.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25340
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 90691 82 10 5 25 0 11 0 540611787 857554944 66262 4294967295 134512640 134569956 3221224400 3221214624 1131303497 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 66262 13073 16 0 209348 0
vsize: 837456
[startup+1010.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25343
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 91595 83 10 5 25 0 11 0 540611787 857554944 66477 4294967295 134512640 134569956 3221224400 3221214624 1131304041 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 66477 13073 16 0 209348 0
vsize: 837456
[startup+1020.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25345
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 92515 83 11 5 25 0 11 0 540611787 857554944 67361 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 67361 13073 16 0 209348 0
vsize: 837456
[startup+1030.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25348
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 93442 83 11 5 25 0 11 0 540611787 857554944 67722 4294967295 134512640 134569956 3221224400 3221214624 1131303441 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 67722 13073 16 0 209348 0
vsize: 837456
[startup+1040.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25351
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 94352 84 11 5 25 0 11 0 540611787 857554944 68078 4294967295 134512640 134569956 3221224400 3221214640 1131216793 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 68078 13073 16 0 209348 0
vsize: 837456
[startup+1050.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25353
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 95258 84 11 5 25 0 11 0 540611787 857554944 68399 4294967295 134512640 134569956 3221224400 3221214624 1131303698 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 68399 13073 16 0 209348 0
vsize: 837456
[startup+1060.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25356
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 96171 85 11 5 25 0 11 0 540611787 857554944 69232 4294967295 134512640 134569956 3221224400 3221214624 1131304068 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 69232 13073 16 0 209348 0
vsize: 837456
[startup+1070.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25358
Raw data (stat): 25065 (java) S 25064 3260 3259 0 -1 0 18013 4 1 0 97105 85 11 5 25 0 11 0 540611787 857554944 69675 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 69675 13073 16 0 209348 0
vsize: 837456
[startup+1080.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25361
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 98002 86 11 5 25 0 11 0 540611787 857554944 75493 4294967295 134512640 134569956 3221224400 3221214720 1131354695 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 75493 13073 16 0 209348 0
vsize: 837456
[startup+1090.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25363
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 98906 87 11 5 25 0 11 0 540611787 857554944 75850 4294967295 134512640 134569956 3221224400 3221214624 1131303789 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 75850 13073 16 0 209348 0
vsize: 837456
[startup+1100.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25366
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 99806 87 11 5 25 0 11 0 540611787 857554944 76275 4294967295 134512640 134569956 3221224400 3221214624 1131303796 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 76275 13073 16 0 209348 0
vsize: 837456
[startup+1110.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25369
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 100729 87 11 5 25 0 11 0 540611787 857554944 76927 4294967295 134512640 134569956 3221224400 3221214760 1131328475 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 76927 13073 16 0 209348 0
vsize: 837456
[startup+1120.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25371
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 101656 88 12 5 25 0 11 0 540611787 857554944 77262 4294967295 134512640 134569956 3221224400 3221214624 1131303456 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 77262 13073 16 0 209348 0
vsize: 837456
[startup+1130.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25374
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 102565 89 12 5 25 0 11 0 540611787 857554944 77757 4294967295 134512640 134569956 3221224400 3221214624 1131303897 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 77757 13073 16 0 209348 0
vsize: 837456
[startup+1140.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25376
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 103481 89 12 6 25 0 11 0 540611787 857554944 78076 4294967295 134512640 134569956 3221224400 3221214720 1131354766 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 78076 13073 16 0 209348 0
vsize: 837456
[startup+1150.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25379
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 104393 89 12 6 25 0 11 0 540611787 857554944 78279 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 78279 13073 16 0 209348 0
vsize: 837456
[startup+1160.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25381
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 105312 90 12 6 25 0 11 0 540611787 857554944 79107 4294967295 134512640 134569956 3221224400 3221214624 1131304826 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 79107 13073 16 0 209348 0
vsize: 837456
[startup+1170.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25384
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 106239 90 12 6 25 0 11 0 540611787 857554944 79406 4294967295 134512640 134569956 3221224400 3221214624 1131303390 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 79406 13073 16 0 209348 0
vsize: 837456
[startup+1180.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25387
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 107148 90 12 6 25 0 11 0 540611787 857554944 79756 4294967295 134512640 134569956 3221224400 3221214716 1131304843 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 79756 13073 16 0 209348 0
vsize: 837456
[startup+1190.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25389
Raw data (stat): 25065 (java) S 25064 3260 3259 0 -1 0 18013 4 1 0 108045 91 12 6 25 0 11 0 540611787 857554944 80073 4294967295 134512640 134569956 3221224400 3221213328 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 80073 13073 16 0 209348 0
vsize: 837456
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25392
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 108953 91 12 6 25 0 11 0 540611787 857554944 80286 4294967295 134512640 134569956 3221224400 3221214720 1131355812 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 80286 13073 16 0 209348 0
vsize: 837456
[startup+1210.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25394
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 109846 91 12 6 25 0 11 0 540611787 857554944 80937 4294967295 134512640 134569956 3221224400 3221214624 1131303357 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 80937 13073 16 0 209348 0
vsize: 837456
[startup+1220.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25397
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 110778 92 13 6 25 0 11 0 540611787 857554944 81751 4294967295 134512640 134569956 3221224400 3221214720 1131355787 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 81751 13073 16 0 209348 0
vsize: 837456
[startup+1230.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25399
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 111709 92 13 6 25 0 11 0 540611787 857554944 81751 4294967295 134512640 134569956 3221224400 3221214720 1131360563 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 81751 13073 16 0 209348 0
vsize: 837456
[startup+1240.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25402
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 112615 93 13 6 25 0 11 0 540611787 857554944 81988 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 81988 13073 16 0 209348 0
vsize: 837456
[startup+1250.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25404
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 113518 94 13 6 25 0 11 0 540611787 857554944 82470 4294967295 134512640 134569956 3221224400 3221214624 1131304299 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 82470 13073 16 0 209348 0
vsize: 837456
[startup+1260.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25407
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 114431 94 13 6 25 0 11 0 540611787 857554944 82682 4294967295 134512640 134569956 3221224400 3221214624 1131304024 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 82682 13073 16 0 209348 0
vsize: 837456
[startup+1270.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25409
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 115338 94 13 6 25 0 11 0 540611787 857554944 82991 4294967295 134512640 134569956 3221224400 3221214624 1131303781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 82991 13073 16 0 209348 0
vsize: 837456
[startup+1280.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25412
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 116235 95 14 6 25 0 11 0 540611787 857554944 83560 4294967295 134512640 134569956 3221224400 3221214624 1131303357 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 83560 13073 16 0 209348 0
vsize: 837456
[startup+1290.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25415
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 117141 95 14 6 25 0 11 0 540611787 857554944 83773 4294967295 134512640 134569956 3221224400 3221214760 1131329289 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209364 83773 13073 16 0 209348 0
vsize: 837456
[startup+1300.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25417
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 118045 96 14 6 24 0 11 0 540611787 857554944 84069 4294967295 134512640 134569956 3221224400 3221214624 1131303372 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 84069 13073 16 0 209348 0
vsize: 837456
[startup+1310.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25420
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 118950 97 14 6 25 0 11 0 540611787 857554944 84744 4294967295 134512640 134569956 3221224400 3221214760 1131328464 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 84744 13073 16 0 209348 0
vsize: 837456
[startup+1320.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25422
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 119879 97 14 6 25 0 11 0 540611787 857554944 85385 4294967295 134512640 134569956 3221224400 3221214720 1131356775 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 85385 13073 16 0 209348 0
vsize: 837456
[startup+1330.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/64 25425
Raw data (stat): 25065 (java) R 25064 3260 3259 0 -1 0 18013 4 1 0 120804 97 14 6 25 0 11 0 540611787 857554944 85578 4294967295 134512640 134569956 3221224400 3221214624 1131303778 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209364 85578 13073 16 0 209348 0
vsize: 837456
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1330.31 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 25426
Raw data (stat): 25065 (java) Z 25064 3260 3259 0 -1 1036 18013 69650 1 0 120805 113 12599 159 25 0 1 0 540611787 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): 1330.31
CPU time (s): 1336.78
CPU user time (s): 1334.06
CPU system time (s): 2.72758
CPU usage (%): 100.486
Max. virtual memory (Kb): 837456
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####