PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-flugpl.opb
MD5SUM	f7c404708fc3042fadfc18ab8efeb9a5
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	14745600
Optimality of the best value was proved	NO
Number of terms in the objective function	265
Biggest coefficient in the objective function	48318382080
Number of bits for the biggest coefficient in the objective function	36
Sum of the numbers in the objective function	103103023008
Number of bits of the sum of numbers in the objective function	37
Biggest number in a constraint	80530636800
Number of bits of the biggest number in a constraint	37
Biggest sum of numbers in a constraint	162146381673
Number of bits of the biggest sum of numbers	38
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	21.6227
Number of variables	265
Total number of constraints	29
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	29
Minimum length of a constraint	5
Maximum length of a constraint	65
Trace number 16454

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        636720 kB
Buffers:         33616 kB
Cached:         342664 kB
SwapCached:        440 kB
Active:          95716 kB
Inactive:       282672 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        636468 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            13976 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 07:43:51 (client local time) WITH STATUS 143 IN 1215.1 SECONDS
stats: 13373 7 1215.1 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-flugpl.opb
c reading problem 
c [nbvar=265]
c [nbconstr=29]
c time 0.751
c #vars     265
c #clauses  36
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=18802685
c Current CPU time (ms) : 13.056
c starts	: 3
c conflicts	: 371
c decisions	: 815
c propagations	: 2715
c inspects	: 19817
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 371
c root simplifications	: 16
c 
c CURRENT OPTIMUM=18581501
c Current CPU time (ms) : 13.541
c starts	: 4
c conflicts	: 375
c decisions	: 953
c propagations	: 2942
c inspects	: 20858
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 375
c root simplifications	: 18
c 
c CURRENT OPTIMUM=18319357
c Current CPU time (ms) : 14.034
c starts	: 5
c conflicts	: 375
c decisions	: 1083
c propagations	: 3142
c inspects	: 21532
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 375
c root simplifications	: 19
c 
c CURRENT OPTIMUM=18286589
c Current CPU time (ms) : 14.615
c starts	: 6
c conflicts	: 375
c decisions	: 1207
c propagations	: 3342
c inspects	: 22295
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 375
c root simplifications	: 20
c 
c CURRENT OPTIMUM=18270205
c Current CPU time (ms) : 15.218
c starts	: 7
c conflicts	: 375
c decisions	: 1329
c propagations	: 3542
c inspects	: 23143
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 375
c root simplifications	: 21
c 
c CURRENT OPTIMUM=18262013
c Current CPU time (ms) : 15.922
c starts	: 8
c conflicts	: 375
c decisions	: 1448
c propagations	: 3742
c inspects	: 24076
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 375
c root simplifications	: 22
c 
c CURRENT OPTIMUM=18262012
c Current CPU time (ms) : 17.144
c starts	: 9
c conflicts	: 376
c decisions	: 1596
c propagations	: 3978
c inspects	: 25231
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 376
c root simplifications	: 23
c 
c CURRENT OPTIMUM=18036765
c Current CPU time (ms) : 19.704
c starts	: 10
c conflicts	: 412
c decisions	: 1911
c propagations	: 4641
c inspects	: 31151
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 412
c root simplifications	: 28
c 
c CURRENT OPTIMUM=17795101
c Current CPU time (ms) : 20.418
c starts	: 11
c conflicts	: 416
c decisions	: 2046
c propagations	: 4849
c inspects	: 32422
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 416
c root simplifications	: 30
c 
c CURRENT OPTIMUM=17270813
c Current CPU time (ms) : 21.164
c starts	: 12
c conflicts	: 420
c decisions	: 2172
c propagations	: 5034
c inspects	: 33857
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 420
c root simplifications	: 31
c 
c CURRENT OPTIMUM=17008669
c Current CPU time (ms) : 22.119
c starts	: 13
c conflicts	: 428
c decisions	: 2301
c propagations	: 5250
c inspects	: 35787
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 33
c 
c CURRENT OPTIMUM=16779293
c Current CPU time (ms) : 22.843
c starts	: 14
c conflicts	: 428
c decisions	: 2418
c propagations	: 5412
c inspects	: 36773
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 34
c 
c CURRENT OPTIMUM=16762909
c Current CPU time (ms) : 23.624
c starts	: 15
c conflicts	: 428
c decisions	: 2528
c propagations	: 5574
c inspects	: 37818
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 35
c 
c CURRENT OPTIMUM=16754717
c Current CPU time (ms) : 24.427
c starts	: 16
c conflicts	: 428
c decisions	: 2635
c propagations	: 5736
c inspects	: 38922
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 36
c 
c CURRENT OPTIMUM=16754716
c Current CPU time (ms) : 25.278
c starts	: 17
c conflicts	: 428
c decisions	: 2728
c propagations	: 5898
c inspects	: 40073
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 37
c 
c CURRENT OPTIMUM=16754715
c Current CPU time (ms) : 26.181
c starts	: 18
c conflicts	: 428
c decisions	: 2821
c propagations	: 6060
c inspects	: 41283
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 38
c 
c CURRENT OPTIMUM=16754714
c Current CPU time (ms) : 27.12
c starts	: 19
c conflicts	: 428
c decisions	: 2913
c propagations	: 6222
c inspects	: 42535
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 39
c 
c CURRENT OPTIMUM=16754713
c Current CPU time (ms) : 28.128
c starts	: 20
c conflicts	: 428
c decisions	: 3006
c propagations	: 6384
c inspects	: 43863
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 40
c 
c CURRENT OPTIMUM=16754712
c Current CPU time (ms) : 29.174
c starts	: 21
c conflicts	: 428
c decisions	: 3098
c propagations	: 6546
c inspects	: 45231
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 41
c 
c CURRENT OPTIMUM=16754711
c Current CPU time (ms) : 30.336
c starts	: 22
c conflicts	: 428
c decisions	: 3190
c propagations	: 6708
c inspects	: 46657
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 42
c 
c CURRENT OPTIMUM=16754710
c Current CPU time (ms) : 31.464
c starts	: 23
c conflicts	: 428
c decisions	: 3281
c propagations	: 6870
c inspects	: 48121
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 43
c 
c CURRENT OPTIMUM=16754709
c Current CPU time (ms) : 32.713
c starts	: 24
c conflicts	: 428
c decisions	: 3374
c propagations	: 7032
c inspects	: 49685
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 44
c 
c CURRENT OPTIMUM=16754708
c Current CPU time (ms) : 33.952
c starts	: 25
c conflicts	: 428
c decisions	: 3466
c propagations	: 7194
c inspects	: 51285
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 45
c 
c CURRENT OPTIMUM=16754707
c Current CPU time (ms) : 35.269
c starts	: 26
c conflicts	: 428
c decisions	: 3558
c propagations	: 7356
c inspects	: 52943
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 46
c 
c CURRENT OPTIMUM=16754706
c Current CPU time (ms) : 36.584
c starts	: 27
c conflicts	: 428
c decisions	: 3649
c propagations	: 7518
c inspects	: 54635
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 47
c 
c CURRENT OPTIMUM=16754705
c Current CPU time (ms) : 37.995
c starts	: 28
c conflicts	: 428
c decisions	: 3741
c propagations	: 7680
c inspects	: 56409
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 48
c 
c CURRENT OPTIMUM=16754704
c Current CPU time (ms) : 39.412
c starts	: 29
c conflicts	: 428
c decisions	: 3832
c propagations	: 7842
c inspects	: 58215
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 49
c 
c CURRENT OPTIMUM=16754703
c Current CPU time (ms) : 40.916
c starts	: 30
c conflicts	: 428
c decisions	: 3923
c propagations	: 8004
c inspects	: 60078
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 50
c 
c CURRENT OPTIMUM=16754702
c Current CPU time (ms) : 42.43
c starts	: 31
c conflicts	: 428
c decisions	: 4013
c propagations	: 8166
c inspects	: 61970
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 51
c 
c CURRENT OPTIMUM=16754701
c Current CPU time (ms) : 44.043
c starts	: 32
c conflicts	: 428
c decisions	: 4106
c propagations	: 8328
c inspects	: 64006
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 52
c 
c CURRENT OPTIMUM=16754700
c Current CPU time (ms) : 45.7
c starts	: 33
c conflicts	: 428
c decisions	: 4198
c propagations	: 8490
c inspects	: 66070
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 53
c 
c CURRENT OPTIMUM=16754699
c Current CPU time (ms) : 47.399
c starts	: 34
c conflicts	: 428
c decisions	: 4290
c propagations	: 8652
c inspects	: 68192
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 54
c 
c CURRENT OPTIMUM=16754698
c Current CPU time (ms) : 49.109
c starts	: 35
c conflicts	: 428
c decisions	: 4381
c propagations	: 8814
c inspects	: 70340
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 55
c 
c CURRENT OPTIMUM=16754697
c Current CPU time (ms) : 50.907
c starts	: 36
c conflicts	: 428
c decisions	: 4473
c propagations	: 8976
c inspects	: 72578
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 56
c 
c CURRENT OPTIMUM=16754696
c Current CPU time (ms) : 52.75
c starts	: 37
c conflicts	: 428
c decisions	: 4564
c propagations	: 9138
c inspects	: 74840
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 57
c 
c CURRENT OPTIMUM=16754695
c Current CPU time (ms) : 54.601
c starts	: 38
c conflicts	: 428
c decisions	: 4655
c propagations	: 9300
c inspects	: 77159
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 58
c 
c CURRENT OPTIMUM=16754694
c Current CPU time (ms) : 56.469
c starts	: 39
c conflicts	: 428
c decisions	: 4745
c propagations	: 9462
c inspects	: 79499
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 59
c 
c CURRENT OPTIMUM=16754693
c Current CPU time (ms) : 58.463
c starts	: 40
c conflicts	: 428
c decisions	: 4837
c propagations	: 9624
c inspects	: 81969
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 60
c 
c CURRENT OPTIMUM=16754692
c Current CPU time (ms) : 60.478
c starts	: 41
c conflicts	: 428
c decisions	: 4928
c propagations	: 9786
c inspects	: 84459
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 61
c 
c CURRENT OPTIMUM=16754691
c Current CPU time (ms) : 62.55
c starts	: 42
c conflicts	: 428
c decisions	: 5019
c propagations	: 9948
c inspects	: 87006
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 62
c 
c CURRENT OPTIMUM=16754690
c Current CPU time (ms) : 64.604
c starts	: 43
c conflicts	: 428
c decisions	: 5109
c propagations	: 10110
c inspects	: 89570
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 63
c 
c CURRENT OPTIMUM=16754689
c Current CPU time (ms) : 66.754
c starts	: 44
c conflicts	: 428
c decisions	: 5200
c propagations	: 10272
c inspects	: 92231
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 64
c 
c CURRENT OPTIMUM=16754688
c Current CPU time (ms) : 68.909
c starts	: 45
c conflicts	: 428
c decisions	: 5290
c propagations	: 10434
c inspects	: 94907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 65
c 
c CURRENT OPTIMUM=16754687
c Current CPU time (ms) : 71.108
c starts	: 46
c conflicts	: 428
c decisions	: 5380
c propagations	: 10596
c inspects	: 97639
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 66
c 
c CURRENT OPTIMUM=16754686
c Current CPU time (ms) : 73.308
c starts	: 47
c conflicts	: 428
c decisions	: 5469
c propagations	: 10758
c inspects	: 100383
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 67
c 
c CURRENT OPTIMUM=16754685
c Current CPU time (ms) : 75.721
c starts	: 48
c conflicts	: 428
c decisions	: 5562
c propagations	: 10920
c inspects	: 103363
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 68
c 
c CURRENT OPTIMUM=16754684
c Current CPU time (ms) : 78.162
c starts	: 49
c conflicts	: 428
c decisions	: 5654
c propagations	: 11082
c inspects	: 106355
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 69
c 
c CURRENT OPTIMUM=16754683
c Current CPU time (ms) : 80.637
c starts	: 50
c conflicts	: 428
c decisions	: 5746
c propagations	: 11244
c inspects	: 109405
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 70
c 
c CURRENT OPTIMUM=16754682
c Current CPU time (ms) : 83.11
c starts	: 51
c conflicts	: 428
c decisions	: 5837
c propagations	: 11406
c inspects	: 112465
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 71
c 
c CURRENT OPTIMUM=16754681
c Current CPU time (ms) : 85.681
c starts	: 52
c conflicts	: 428
c decisions	: 5929
c propagations	: 11568
c inspects	: 115631
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 72
c 
c CURRENT OPTIMUM=16754680
c Current CPU time (ms) : 88.263
c starts	: 53
c conflicts	: 428
c decisions	: 6020
c propagations	: 11730
c inspects	: 118805
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 73
c 
c CURRENT OPTIMUM=16754679
c Current CPU time (ms) : 90.906
c starts	: 54
c conflicts	: 428
c decisions	: 6111
c propagations	: 11892
c inspects	: 122036
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 74
c 
c CURRENT OPTIMUM=16754678
c Current CPU time (ms) : 93.582
c starts	: 55
c conflicts	: 428
c decisions	: 6201
c propagations	: 12054
c inspects	: 125272
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 75
c 
c CURRENT OPTIMUM=16754677
c Current CPU time (ms) : 96.38
c starts	: 56
c conflicts	: 428
c decisions	: 6293
c propagations	: 12216
c inspects	: 128670
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 76
c 
c CURRENT OPTIMUM=16754676
c Current CPU time (ms) : 99.17
c starts	: 57
c conflicts	: 428
c decisions	: 6384
c propagations	: 12378
c inspects	: 132072
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 77
c 
c CURRENT OPTIMUM=16754675
c Current CPU time (ms) : 101.997
c starts	: 58
c conflicts	: 428
c decisions	: 6475
c propagations	: 12540
c inspects	: 135531
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 78
c 
c CURRENT OPTIMUM=16754674
c Current CPU time (ms) : 104.835
c starts	: 59
c conflicts	: 428
c decisions	: 6565
c propagations	: 12702
c inspects	: 138991
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 79
c 
c CURRENT OPTIMUM=16754673
c Current CPU time (ms) : 107.773
c starts	: 60
c conflicts	: 428
c decisions	: 6656
c propagations	: 12864
c inspects	: 142564
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 80
c 
c CURRENT OPTIMUM=16754672
c Current CPU time (ms) : 110.704
c starts	: 61
c conflicts	: 428
c decisions	: 6746
c propagations	: 13026
c inspects	: 146136
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 81
c 
c CURRENT OPTIMUM=16754671
c Current CPU time (ms) : 113.677
c starts	: 62
c conflicts	: 428
c decisions	: 6836
c propagations	: 13188
c inspects	: 149764
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 82
c 
c CURRENT OPTIMUM=16754670
c Current CPU time (ms) : 116.637
c starts	: 63
c conflicts	: 428
c decisions	: 6925
c propagations	: 13350
c inspects	: 153388
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 83
c 
c CURRENT OPTIMUM=16754669
c Current CPU time (ms) : 119.802
c starts	: 64
c conflicts	: 428
c decisions	: 7017
c propagations	: 13512
c inspects	: 157250
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 84
c 
c CURRENT OPTIMUM=16754668
c Current CPU time (ms) : 122.966
c starts	: 65
c conflicts	: 428
c decisions	: 7108
c propagations	: 13674
c inspects	: 161108
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 85
c 
c CURRENT OPTIMUM=16754667
c Current CPU time (ms) : 126.18
c starts	: 66
c conflicts	: 428
c decisions	: 7199
c propagations	: 13836
c inspects	: 165023
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 86
c 
c CURRENT OPTIMUM=16754666
c Current CPU time (ms) : 129.402
c starts	: 67
c conflicts	: 428
c decisions	: 7289
c propagations	: 13998
c inspects	: 168931
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 87
c 
c CURRENT OPTIMUM=16754665
c Current CPU time (ms) : 132.723
c starts	: 68
c conflicts	: 428
c decisions	: 7380
c propagations	: 14160
c inspects	: 172960
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 88
c 
c CURRENT OPTIMUM=16754664
c Current CPU time (ms) : 136.037
c starts	: 69
c conflicts	: 428
c decisions	: 7470
c propagations	: 14322
c inspects	: 176980
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 89
c 
c CURRENT OPTIMUM=16754663
c Current CPU time (ms) : 139.371
c starts	: 70
c conflicts	: 428
c decisions	: 7560
c propagations	: 14484
c inspects	: 181056
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 90
c 
c CURRENT OPTIMUM=16754662
c Current CPU time (ms) : 142.727
c starts	: 71
c conflicts	: 428
c decisions	: 7649
c propagations	: 14646
c inspects	: 185120
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 91
c 
c CURRENT OPTIMUM=16754661
c Current CPU time (ms) : 146.237
c starts	: 72
c conflicts	: 428
c decisions	: 7740
c propagations	: 14808
c inspects	: 189377
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 92
c 
c CURRENT OPTIMUM=16754660
c Current CPU time (ms) : 149.734
c starts	: 73
c conflicts	: 428
c decisions	: 7830
c propagations	: 14970
c inspects	: 193621
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 93
c 
c CURRENT OPTIMUM=16754659
c Current CPU time (ms) : 153.283
c starts	: 74
c conflicts	: 428
c decisions	: 7920
c propagations	: 15132
c inspects	: 197921
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 94
c 
c CURRENT OPTIMUM=16754658
c Current CPU time (ms) : 156.813
c starts	: 75
c conflicts	: 428
c decisions	: 8009
c propagations	: 15294
c inspects	: 202205
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 95
c 
c CURRENT OPTIMUM=16754657
c Current CPU time (ms) : 160.459
c starts	: 76
c conflicts	: 428
c decisions	: 8099
c propagations	: 15456
c inspects	: 206617
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 96
c 
c CURRENT OPTIMUM=16754656
c Current CPU time (ms) : 164.097
c starts	: 77
c conflicts	: 428
c decisions	: 8188
c propagations	: 15618
c inspects	: 211011
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 97
c 
c CURRENT OPTIMUM=16754655
c Current CPU time (ms) : 167.766
c starts	: 78
c conflicts	: 428
c decisions	: 8277
c propagations	: 15780
c inspects	: 215460
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 98
c 
c CURRENT OPTIMUM=16754654
c Current CPU time (ms) : 171.436
c starts	: 79
c conflicts	: 428
c decisions	: 8365
c propagations	: 15942
c inspects	: 219888
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 99
c 
c CURRENT OPTIMUM=16754653
c Current CPU time (ms) : 175.454
c starts	: 80
c conflicts	: 428
c decisions	: 8458
c propagations	: 16104
c inspects	: 224756
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 100
c 
c CURRENT OPTIMUM=16754652
c Current CPU time (ms) : 179.468
c starts	: 81
c conflicts	: 428
c decisions	: 8550
c propagations	: 16266
c inspects	: 229604
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 101
c 
c CURRENT OPTIMUM=16754651
c Current CPU time (ms) : 183.542
c starts	: 82
c conflicts	: 428
c decisions	: 8642
c propagations	: 16428
c inspects	: 234510
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 102
c 
c CURRENT OPTIMUM=16754650
c Current CPU time (ms) : 187.599
c starts	: 83
c conflicts	: 428
c decisions	: 8733
c propagations	: 16590
c inspects	: 239394
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 103
c 
c CURRENT OPTIMUM=16754649
c Current CPU time (ms) : 191.771
c starts	: 84
c conflicts	: 428
c decisions	: 8825
c propagations	: 16752
c inspects	: 244416
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 104
c 
c CURRENT OPTIMUM=16754648
c Current CPU time (ms) : 195.91
c starts	: 85
c conflicts	: 428
c decisions	: 8916
c propagations	: 16914
c inspects	: 249414
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 105
c 
c CURRENT OPTIMUM=16754647
c Current CPU time (ms) : 200.11
c starts	: 86
c conflicts	: 428
c decisions	: 9007
c propagations	: 17076
c inspects	: 254469
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 106
c 
c CURRENT OPTIMUM=16754646
c Current CPU time (ms) : 204.276
c starts	: 87
c conflicts	: 428
c decisions	: 9097
c propagations	: 17238
c inspects	: 259497
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 107
c 
c CURRENT OPTIMUM=16754645
c Current CPU time (ms) : 208.631
c starts	: 88
c conflicts	: 428
c decisions	: 9189
c propagations	: 17400
c inspects	: 264751
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 108
c 
c CURRENT OPTIMUM=16754644
c Current CPU time (ms) : 212.975
c starts	: 89
c conflicts	: 428
c decisions	: 9280
c propagations	: 17562
c inspects	: 269977
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 109
c 
c CURRENT OPTIMUM=16754643
c Current CPU time (ms) : 217.354
c starts	: 90
c conflicts	: 428
c decisions	: 9371
c propagations	: 17724
c inspects	: 275260
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 110
c 
c CURRENT OPTIMUM=16754642
c Current CPU time (ms) : 221.734
c starts	: 91
c conflicts	: 428
c decisions	: 9461
c propagations	: 17886
c inspects	: 280512
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 111
c 
c CURRENT OPTIMUM=16754641
c Current CPU time (ms) : 226.214
c starts	: 92
c conflicts	: 428
c decisions	: 9552
c propagations	: 18048
c inspects	: 285909
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 112
c 
c CURRENT OPTIMUM=16754640
c Current CPU time (ms) : 230.658
c starts	: 93
c conflicts	: 428
c decisions	: 9642
c propagations	: 18210
c inspects	: 291273
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 113
c 
c CURRENT OPTIMUM=16754639
c Current CPU time (ms) : 235.188
c starts	: 94
c conflicts	: 428
c decisions	: 9732
c propagations	: 18372
c inspects	: 296693
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 114
c 
c CURRENT OPTIMUM=16754638
c Current CPU time (ms) : 239.688
c starts	: 95
c conflicts	: 428
c decisions	: 9821
c propagations	: 18534
c inspects	: 302077
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 115
c 
c CURRENT OPTIMUM=16754637
c Current CPU time (ms) : 244.442
c starts	: 96
c conflicts	: 428
c decisions	: 9913
c propagations	: 18696
c inspects	: 307795
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 116
c 
c CURRENT OPTIMUM=16754636
c Current CPU time (ms) : 249.188
c starts	: 97
c conflicts	: 428
c decisions	: 10004
c propagations	: 18858
c inspects	: 313477
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 117
c 
c CURRENT OPTIMUM=16754635
c Current CPU time (ms) : 253.972
c starts	: 98
c conflicts	: 428
c decisions	: 10095
c propagations	: 19020
c inspects	: 319216
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 118
c 
c CURRENT OPTIMUM=16754634
c Current CPU time (ms) : 258.739
c starts	: 99
c conflicts	: 428
c decisions	: 10185
c propagations	: 19182
c inspects	: 324916
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 119
c 
c CURRENT OPTIMUM=16754633
c Current CPU time (ms) : 263.643
c starts	: 100
c conflicts	: 428
c decisions	: 10276
c propagations	: 19344
c inspects	: 330769
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 120
c 
c CURRENT OPTIMUM=16754632
c Current CPU time (ms) : 268.509
c starts	: 101
c conflicts	: 428
c decisions	: 10366
c propagations	: 19506
c inspects	: 336581
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 121
c 
c CURRENT OPTIMUM=16754631
c Current CPU time (ms) : 273.427
c starts	: 102
c conflicts	: 428
c decisions	: 10456
c propagations	: 19668
c inspects	: 342449
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 122
c 
c CURRENT OPTIMUM=16754630
c Current CPU time (ms) : 278.317
c starts	: 103
c conflicts	: 428
c decisions	: 10545
c propagations	: 19830
c inspects	: 348273
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 123
c 
c CURRENT OPTIMUM=16754629
c Current CPU time (ms) : 283.41
c starts	: 104
c conflicts	: 428
c decisions	: 10636
c propagations	: 19992
c inspects	: 354354
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 124
c 
c CURRENT OPTIMUM=16754628
c Current CPU time (ms) : 288.462
c starts	: 105
c conflicts	: 428
c decisions	: 10726
c propagations	: 20154
c inspects	: 360390
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 125
c 
c CURRENT OPTIMUM=16754627
c Current CPU time (ms) : 293.553
c starts	: 106
c conflicts	: 428
c decisions	: 10816
c propagations	: 20316
c inspects	: 366482
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 126
c 
c CURRENT OPTIMUM=16754626
c Current CPU time (ms) : 298.617
c starts	: 107
c conflicts	: 428
c decisions	: 10905
c propagations	: 20478
c inspects	: 372526
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 127
c 
c CURRENT OPTIMUM=16754625
c Current CPU time (ms) : 303.812
c starts	: 108
c conflicts	: 428
c decisions	: 10995
c propagations	: 20640
c inspects	: 378730
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 128
c 
c CURRENT OPTIMUM=16754624
c Current CPU time (ms) : 308.98
c starts	: 109
c conflicts	: 428
c decisions	: 11084
c propagations	: 20802
c inspects	: 384884
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 129
c 
c CURRENT OPTIMUM=16754623
c Current CPU time (ms) : 314.21
c starts	: 110
c conflicts	: 428
c decisions	: 11173
c propagations	: 20964
c inspects	: 391093
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 130
c 
c CURRENT OPTIMUM=16754622
c Current CPU time (ms) : 319.364
c starts	: 111
c conflicts	: 428
c decisions	: 11261
c propagations	: 21126
c inspects	: 397249
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 131
c 
c CURRENT OPTIMUM=16754621
c Current CPU time (ms) : 324.944
c starts	: 112
c conflicts	: 428
c decisions	: 11353
c propagations	: 21288
c inspects	: 403895
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 132
c 
c CURRENT OPTIMUM=16754620
c Current CPU time (ms) : 330.483
c starts	: 113
c conflicts	: 428
c decisions	: 11444
c propagations	: 21450
c inspects	: 410489
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 133
c 
c CURRENT OPTIMUM=16754619
c Current CPU time (ms) : 336.056
c starts	: 114
c conflicts	: 428
c decisions	: 11535
c propagations	: 21612
c inspects	: 417140
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 134
c 
c CURRENT OPTIMUM=16754618
c Current CPU time (ms) : 341.583
c starts	: 115
c conflicts	: 428
c decisions	: 11625
c propagations	: 21774
c inspects	: 423736
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 135
c 
c CURRENT OPTIMUM=16754617
c Current CPU time (ms) : 347.235
c starts	: 116
c conflicts	: 428
c decisions	: 11716
c propagations	: 21936
c inspects	: 430501
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 136
c 
c CURRENT OPTIMUM=16754616
c Current CPU time (ms) : 352.864
c starts	: 117
c conflicts	: 428
c decisions	: 11806
c propagations	: 22098
c inspects	: 437209
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 137
c 
c CURRENT OPTIMUM=16754615
c Current CPU time (ms) : 358.533
c starts	: 118
c conflicts	: 428
c decisions	: 11896
c propagations	: 22260
c inspects	: 443973
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 138
c 
c CURRENT OPTIMUM=16754614
c Current CPU time (ms) : 364.147
c starts	: 119
c conflicts	: 428
c decisions	: 11985
c propagations	: 22422
c inspects	: 450677
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 139
c 
c CURRENT OPTIMUM=16754613
c Current CPU time (ms) : 370.013
c starts	: 120
c conflicts	: 428
c decisions	: 12076
c propagations	: 22584
c inspects	: 457670
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 140
c 
c CURRENT OPTIMUM=16754612
c Current CPU time (ms) : 375.828
c starts	: 121
c conflicts	: 428
c decisions	: 12166
c propagations	: 22746
c inspects	: 464602
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 141
c 
c CURRENT OPTIMUM=16754611
c Current CPU time (ms) : 381.698
c starts	: 122
c conflicts	: 428
c decisions	: 12256
c propagations	: 22908
c inspects	: 471590
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 142
c 
c CURRENT OPTIMUM=16754610
c Current CPU time (ms) : 387.501
c starts	: 123
c conflicts	: 428
c decisions	: 12345
c propagations	: 23070
c inspects	: 478514
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 143
c 
c CURRENT OPTIMUM=16754609
c Current CPU time (ms) : 393.459
c starts	: 124
c conflicts	: 428
c decisions	: 12435
c propagations	: 23232
c inspects	: 485614
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 144
c 
c CURRENT OPTIMUM=16754608
c Current CPU time (ms) : 399.357
c starts	: 125
c conflicts	: 428
c decisions	: 12524
c propagations	: 23394
c inspects	: 492648
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 145
c 
c CURRENT OPTIMUM=16754607
c Current CPU time (ms) : 405.314
c starts	: 126
c conflicts	: 428
c decisions	: 12613
c propagations	: 23556
c inspects	: 499737
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 146
c 
c CURRENT OPTIMUM=16754606
c Current CPU time (ms) : 411.22
c starts	: 127
c conflicts	: 428
c decisions	: 12701
c propagations	: 23718
c inspects	: 506757
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 147
c 
c CURRENT OPTIMUM=16754605
c Current CPU time (ms) : 417.475
c starts	: 128
c conflicts	: 428
c decisions	: 12792
c propagations	: 23880
c inspects	: 514206
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 148
c 
c CURRENT OPTIMUM=16754604
c Current CPU time (ms) : 423.686
c starts	: 129
c conflicts	: 428
c decisions	: 12882
c propagations	: 24042
c inspects	: 521586
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 149
c 
c CURRENT OPTIMUM=16754603
c Current CPU time (ms) : 429.934
c starts	: 130
c conflicts	: 428
c decisions	: 12972
c propagations	: 24204
c inspects	: 529022
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 150
c 
c CURRENT OPTIMUM=16754602
c Current CPU time (ms) : 436.121
c starts	: 131
c conflicts	: 428
c decisions	: 13061
c propagations	: 24366
c inspects	: 536386
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 151
c 
c CURRENT OPTIMUM=16754601
c Current CPU time (ms) : 442.465
c starts	: 132
c conflicts	: 428
c decisions	: 13151
c propagations	: 24528
c inspects	: 543934
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 152
c 
c CURRENT OPTIMUM=16754600
c Current CPU time (ms) : 448.755
c starts	: 133
c conflicts	: 428
c decisions	: 13240
c propagations	: 24690
c inspects	: 551408
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 153
c 
c CURRENT OPTIMUM=16754599
c Current CPU time (ms) : 455.091
c starts	: 134
c conflicts	: 428
c decisions	: 13329
c propagations	: 24852
c inspects	: 558937
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 154
c 
c CURRENT OPTIMUM=16754598
c Current CPU time (ms) : 461.379
c starts	: 135
c conflicts	: 428
c decisions	: 13417
c propagations	: 25014
c inspects	: 566389
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 155
c 
c CURRENT OPTIMUM=16754597
c Current CPU time (ms) : 467.921
c starts	: 136
c conflicts	: 428
c decisions	: 13507
c propagations	: 25176
c inspects	: 574161
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 156
c 
c CURRENT OPTIMUM=16754596
c Current CPU time (ms) : 474.391
c starts	: 137
c conflicts	: 428
c decisions	: 13596
c propagations	: 25338
c inspects	: 581855
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 157
c 
c CURRENT OPTIMUM=16754595
c Current CPU time (ms) : 480.922
c starts	: 138
c conflicts	: 428
c decisions	: 13685
c propagations	: 25500
c inspects	: 589604
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 158
c 
c CURRENT OPTIMUM=16754594
c Current CPU time (ms) : 487.381
c starts	: 139
c conflicts	: 428
c decisions	: 13773
c propagations	: 25662
c inspects	: 597272
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 159
c 
c CURRENT OPTIMUM=16754593
c Current CPU time (ms) : 493.987
c starts	: 140
c conflicts	: 428
c decisions	: 13862
c propagations	: 25824
c inspects	: 605131
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 160
c 
c CURRENT OPTIMUM=16754592
c Current CPU time (ms) : 500.525
c starts	: 141
c conflicts	: 428
c decisions	: 13950
c propagations	: 25986
c inspects	: 612907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 161
c 
c CURRENT OPTIMUM=16754591
c Current CPU time (ms) : 507.124
c starts	: 142
c conflicts	: 428
c decisions	: 14038
c propagations	: 26148
c inspects	: 620737
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 162
c 
c CURRENT OPTIMUM=16754590
c Current CPU time (ms) : 513.652
c starts	: 143
c conflicts	: 428
c decisions	: 14125
c propagations	: 26310
c inspects	: 628481
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 163
c 
c CURRENT OPTIMUM=16754589
c Current CPU time (ms) : 520.927
c starts	: 144
c conflicts	: 428
c decisions	: 14218
c propagations	: 26472
c inspects	: 637125
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 164
c 
c CURRENT OPTIMUM=16754588
c Current CPU time (ms) : 528.145
c starts	: 145
c conflicts	: 428
c decisions	: 14310
c propagations	: 26634
c inspects	: 645685
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 165
c 
c CURRENT OPTIMUM=16754587
c Current CPU time (ms) : 535.396
c starts	: 146
c conflicts	: 428
c decisions	: 14402
c propagations	: 26796
c inspects	: 654303
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 166
c 
c CURRENT OPTIMUM=16754586
c Current CPU time (ms) : 542.593
c starts	: 147
c conflicts	: 428
c decisions	: 14493
c propagations	: 26958
c inspects	: 662835
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 167
c 
c CURRENT OPTIMUM=16754585
c Current CPU time (ms) : 549.952
c starts	: 148
c conflicts	: 428
c decisions	: 14585
c propagations	: 27120
c inspects	: 671569
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 168
c 
c CURRENT OPTIMUM=16754584
c Current CPU time (ms) : 557.244
c starts	: 149
c conflicts	: 428
c decisions	: 14676
c propagations	: 27282
c inspects	: 680215
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 169
c 
c CURRENT OPTIMUM=16754583
c Current CPU time (ms) : 564.585
c starts	: 150
c conflicts	: 428
c decisions	: 14767
c propagations	: 27444
c inspects	: 688918
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 170
c 
c CURRENT OPTIMUM=16754582
c Current CPU time (ms) : 571.86
c starts	: 151
c conflicts	: 428
c decisions	: 14857
c propagations	: 27606
c inspects	: 697530
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 171
c 
c CURRENT OPTIMUM=16754581
c Current CPU time (ms) : 579.421
c starts	: 152
c conflicts	: 428
c decisions	: 14949
c propagations	: 27768
c inspects	: 706496
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 172
c 
c CURRENT OPTIMUM=16754580
c Current CPU time (ms) : 586.893
c starts	: 153
c conflicts	: 428
c decisions	: 15040
c propagations	: 27930
c inspects	: 715370
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 173
c 
c CURRENT OPTIMUM=16754579
c Current CPU time (ms) : 594.448
c starts	: 154
c conflicts	: 428
c decisions	: 15131
c propagations	: 28092
c inspects	: 724301
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 174
c 
c CURRENT OPTIMUM=16754578
c Current CPU time (ms) : 601.928
c starts	: 155
c conflicts	: 428
c decisions	: 15221
c propagations	: 28254
c inspects	: 733137
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 175
c 
c CURRENT OPTIMUM=16754577
c Current CPU time (ms) : 609.556
c starts	: 156
c conflicts	: 428
c decisions	: 15312
c propagations	: 28416
c inspects	: 742182
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 176
c 
c CURRENT OPTIMUM=16754576
c Current CPU time (ms) : 617.116
c starts	: 157
c conflicts	: 428
c decisions	: 15402
c propagations	: 28578
c inspects	: 751130
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 177
c 
c CURRENT OPTIMUM=16754575
c Current CPU time (ms) : 624.726
c starts	: 158
c conflicts	: 428
c decisions	: 15492
c propagations	: 28740
c inspects	: 760134
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 178
c 
c CURRENT OPTIMUM=16754574
c Current CPU time (ms) : 632.254
c starts	: 159
c conflicts	: 428
c decisions	: 15581
c propagations	: 28902
c inspects	: 769038
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 179
c 
c CURRENT OPTIMUM=16754573
c Current CPU time (ms) : 640.225
c starts	: 160
c conflicts	: 428
c decisions	: 15673
c propagations	: 29064
c inspects	: 778468
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 180
c 
c CURRENT OPTIMUM=16754572
c Current CPU time (ms) : 648.112
c starts	: 161
c conflicts	: 428
c decisions	: 15764
c propagations	: 29226
c inspects	: 787798
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 181
c 
c CURRENT OPTIMUM=16754571
c Current CPU time (ms) : 656.048
c starts	: 162
c conflicts	: 428
c decisions	: 15855
c propagations	: 29388
c inspects	: 797185
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 182
c 
c CURRENT OPTIMUM=16754570
c Current CPU time (ms) : 663.893
c starts	: 163
c conflicts	: 428
c decisions	: 15945
c propagations	: 29550
c inspects	: 806469
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 183
c 
c CURRENT OPTIMUM=16754569
c Current CPU time (ms) : 671.919
c starts	: 164
c conflicts	: 428
c decisions	: 16036
c propagations	: 29712
c inspects	: 815970
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 184
c 
c CURRENT OPTIMUM=16754568
c Current CPU time (ms) : 679.851
c starts	: 165
c conflicts	: 428
c decisions	: 16126
c propagations	: 29874
c inspects	: 825366
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 185
c 
c CURRENT OPTIMUM=16754567
c Current CPU time (ms) : 687.854
c starts	: 166
c conflicts	: 428
c decisions	: 16216
c propagations	: 30036
c inspects	: 834818
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 186
c 
c CURRENT OPTIMUM=16754566
c Current CPU time (ms) : 695.756
c starts	: 167
c conflicts	: 428
c decisions	: 16305
c propagations	: 30198
c inspects	: 844162
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 187
c 
c CURRENT OPTIMUM=16754565
c Current CPU time (ms) : 703.986
c starts	: 168
c conflicts	: 428
c decisions	: 16396
c propagations	: 30360
c inspects	: 853891
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 188
c 
c CURRENT OPTIMUM=16754564
c Current CPU time (ms) : 712.114
c starts	: 169
c conflicts	: 428
c decisions	: 16486
c propagations	: 30522
c inspects	: 863511
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 189
c 
c CURRENT OPTIMUM=16754563
c Current CPU time (ms) : 720.28
c starts	: 170
c conflicts	: 428
c decisions	: 16576
c propagations	: 30684
c inspects	: 873187
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 190
c 
c CURRENT OPTIMUM=16754562
c Current CPU time (ms) : 728.373
c starts	: 171
c conflicts	: 428
c decisions	: 16665
c propagations	: 30846
c inspects	: 882751
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 191
c 
c CURRENT OPTIMUM=16754561
c Current CPU time (ms) : 736.653
c starts	: 172
c conflicts	: 428
c decisions	: 16755
c propagations	: 31008
c inspects	: 892539
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 192
c 
c CURRENT OPTIMUM=16754560
c Current CPU time (ms) : 744.839
c starts	: 173
c conflicts	: 428
c decisions	: 16844
c propagations	: 31170
c inspects	: 902213
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 193
c 
c CURRENT OPTIMUM=16754559
c Current CPU time (ms) : 753.091
c starts	: 174
c conflicts	: 428
c decisions	: 16933
c propagations	: 31332
c inspects	: 911942
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 194
c 
c CURRENT OPTIMUM=16754558
c Current CPU time (ms) : 761.237
c starts	: 175
c conflicts	: 428
c decisions	: 17021
c propagations	: 31494
c inspects	: 921554
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 195
c 
c CURRENT OPTIMUM=16754557
c Current CPU time (ms) : 769.993
c starts	: 176
c conflicts	: 428
c decisions	: 17113
c propagations	: 31656
c inspects	: 931912
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 196
c 
c CURRENT OPTIMUM=16754556
c Current CPU time (ms) : 778.661
c starts	: 177
c conflicts	: 428
c decisions	: 17204
c propagations	: 31818
c inspects	: 942154
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 197
c 
c CURRENT OPTIMUM=16754555
c Current CPU time (ms) : 787.38
c starts	: 178
c conflicts	: 428
c decisions	: 17295
c propagations	: 31980
c inspects	: 952453
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 198
c 
c CURRENT OPTIMUM=16754554
c Current CPU time (ms) : 796.014
c starts	: 179
c conflicts	: 428
c decisions	: 17385
c propagations	: 32142
c inspects	: 962633
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 199
c 
c CURRENT OPTIMUM=16754553
c Current CPU time (ms) : 804.829
c starts	: 180
c conflicts	: 428
c decisions	: 17476
c propagations	: 32304
c inspects	: 973046
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 200
c 
c CURRENT OPTIMUM=16754552
c Current CPU time (ms) : 813.545
c starts	: 181
c conflicts	: 428
c decisions	: 17566
c propagations	: 32466
c inspects	: 983338
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 201
c 
c CURRENT OPTIMUM=16754551
c Current CPU time (ms) : 822.312
c starts	: 182
c conflicts	: 428
c decisions	: 17656
c propagations	: 32628
c inspects	: 993686
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 202
c 
c CURRENT OPTIMUM=16754550
c Current CPU time (ms) : 830.963
c starts	: 183
c conflicts	: 428
c decisions	: 17745
c propagations	: 32790
c inspects	: 1003910
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 203
c 
c CURRENT OPTIMUM=16754549
c Current CPU time (ms) : 839.981
c starts	: 184
c conflicts	: 428
c decisions	: 17836
c propagations	: 32952
c inspects	: 1014551
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 204
c 
c CURRENT OPTIMUM=16754548
c Current CPU time (ms) : 848.884
c starts	: 185
c conflicts	: 428
c decisions	: 17926
c propagations	: 33114
c inspects	: 1025067
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 205
c 
c CURRENT OPTIMUM=16754547
c Current CPU time (ms) : 857.832
c starts	: 186
c conflicts	: 428
c decisions	: 18016
c propagations	: 33276
c inspects	: 1035639
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 206
c 
c CURRENT OPTIMUM=16754546
c Current CPU time (ms) : 866.686
c starts	: 187
c conflicts	: 428
c decisions	: 18105
c propagations	: 33438
c inspects	: 1046083
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 207
c 
c CURRENT OPTIMUM=16754545
c Current CPU time (ms) : 875.75
c starts	: 188
c conflicts	: 428
c decisions	: 18195
c propagations	: 33600
c inspects	: 1056767
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 208
c 
c CURRENT OPTIMUM=16754544
c Current CPU time (ms) : 884.692
c starts	: 189
c conflicts	: 428
c decisions	: 18284
c propagations	: 33762
c inspects	: 1067321
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 209
c 
c CURRENT OPTIMUM=16754543
c Current CPU time (ms) : 893.683
c starts	: 190
c conflicts	: 428
c decisions	: 18373
c propagations	: 33924
c inspects	: 1077930
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 210
c 
c CURRENT OPTIMUM=16754542
c Current CPU time (ms) : 902.578
c starts	: 191
c conflicts	: 428
c decisions	: 18461
c propagations	: 34086
c inspects	: 1088406
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 211
c 
c CURRENT OPTIMUM=16754541
c Current CPU time (ms) : 911.997
c starts	: 192
c conflicts	: 428
c decisions	: 18552
c propagations	: 34248
c inspects	: 1099503
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 212
c 
c CURRENT OPTIMUM=16754540
c Current CPU time (ms) : 921.292
c starts	: 193
c conflicts	: 428
c decisions	: 18642
c propagations	: 34410
c inspects	: 1110467
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 213
c 
c CURRENT OPTIMUM=16754539
c Current CPU time (ms) : 930.651
c starts	: 194
c conflicts	: 428
c decisions	: 18732
c propagations	: 34572
c inspects	: 1121487
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 214
c 
c CURRENT OPTIMUM=16754538
c Current CPU time (ms) : 939.926
c starts	: 195
c conflicts	: 428
c decisions	: 18821
c propagations	: 34734
c inspects	: 1132371
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 215
c 
c CURRENT OPTIMUM=16754537
c Current CPU time (ms) : 949.449
c starts	: 196
c conflicts	: 428
c decisions	: 18911
c propagations	: 34896
c inspects	: 1143503
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 216
c 
c CURRENT OPTIMUM=16754536
c Current CPU time (ms) : 958.845
c starts	: 197
c conflicts	: 428
c decisions	: 19000
c propagations	: 35058
c inspects	: 1154497
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 217
c 
c CURRENT OPTIMUM=16754535
c Current CPU time (ms) : 968.266
c starts	: 198
c conflicts	: 428
c decisions	: 19089
c propagations	: 35220
c inspects	: 1165546
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 218
c 
c CURRENT OPTIMUM=16754534
c Current CPU time (ms) : 977.535
c starts	: 199
c conflicts	: 428
c decisions	: 19177
c propagations	: 35382
c inspects	: 1176454
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 219
c 
c CURRENT OPTIMUM=16754533
c Current CPU time (ms) : 987.16
c starts	: 200
c conflicts	: 428
c decisions	: 19267
c propagations	: 35544
c inspects	: 1187810
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 220
c 
c CURRENT OPTIMUM=16754532
c Current CPU time (ms) : 996.688
c starts	: 201
c conflicts	: 428
c decisions	: 19356
c propagations	: 35706
c inspects	: 1199024
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 221
c 
c CURRENT OPTIMUM=16754531
c Current CPU time (ms) : 1006.269
c starts	: 202
c conflicts	: 428
c decisions	: 19445
c propagations	: 35868
c inspects	: 1210293
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 222
c 
c CURRENT OPTIMUM=16754530
c Current CPU time (ms) : 1015.714
c starts	: 203
c conflicts	: 428
c decisions	: 19533
c propagations	: 36030
c inspects	: 1221417
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 223
c 
c CURRENT OPTIMUM=16754529
c Current CPU time (ms) : 1025.386
c starts	: 204
c conflicts	: 428
c decisions	: 19622
c propagations	: 36192
c inspects	: 1232796
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 224
c 
c CURRENT OPTIMUM=16754528
c Current CPU time (ms) : 1034.922
c starts	: 205
c conflicts	: 428
c decisions	: 19710
c propagations	: 36354
c inspects	: 1244028
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 225
c 
c CURRENT OPTIMUM=16754527
c Current CPU time (ms) : 1044.527
c starts	: 206
c conflicts	: 428
c decisions	: 19798
c propagations	: 36516
c inspects	: 1255314
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 226
c 
c CURRENT OPTIMUM=16754526
c Current CPU time (ms) : 1053.993
c starts	: 207
c conflicts	: 428
c decisions	: 19885
c propagations	: 36678
c inspects	: 1266450
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 227
c 
c CURRENT OPTIMUM=16754525
c Current CPU time (ms) : 1064.356
c starts	: 208
c conflicts	: 428
c decisions	: 19977
c propagations	: 36840
c inspects	: 1278664
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 228
c 
c CURRENT OPTIMUM=16754524
c Current CPU time (ms) : 1074.589
c starts	: 209
c conflicts	: 428
c decisions	: 20068
c propagations	: 37002
c inspects	: 1290730
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 229
c 
c CURRENT OPTIMUM=16754523
c Current CPU time (ms) : 1084.878
c starts	: 210
c conflicts	: 428
c decisions	: 20159
c propagations	: 37164
c inspects	: 1302853
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 230
c 
c CURRENT OPTIMUM=16754522
c Current CPU time (ms) : 1095.056
c starts	: 211
c conflicts	: 428
c decisions	: 20249
c propagations	: 37326
c inspects	: 1314825
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 231
c 
c CURRENT OPTIMUM=16754521
c Current CPU time (ms) : 1105.447
c starts	: 212
c conflicts	: 428
c decisions	: 20340
c propagations	: 37488
c inspects	: 1327062
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 232
c 
c CURRENT OPTIMUM=16754520
c Current CPU time (ms) : 1115.714
c starts	: 213
c conflicts	: 428
c decisions	: 20430
c propagations	: 37650
c inspects	: 1339146
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 233
c 
c CURRENT OPTIMUM=16754519
c Current CPU time (ms) : 1126.047
c starts	: 214
c conflicts	: 428
c decisions	: 20520
c propagations	: 37812
c inspects	: 1351286
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 234
c 
c CURRENT OPTIMUM=16754518
c Current CPU time (ms) : 1136.242
c starts	: 215
c conflicts	: 428
c decisions	: 20609
c propagations	: 37974
c inspects	: 1363270
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 235
c 
c CURRENT OPTIMUM=16754517
c Current CPU time (ms) : 1146.834
c starts	: 216
c conflicts	: 428
c decisions	: 20700
c propagations	: 38136
c inspects	: 1375735
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 236
c 
c CURRENT OPTIMUM=16754516
c Current CPU time (ms) : 1157.319
c starts	: 217
c conflicts	: 428
c decisions	: 20790
c propagations	: 38298
c inspects	: 1388043
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 237
c 
c CURRENT OPTIMUM=16754515
c Current CPU time (ms) : 1167.826
c starts	: 218
c conflicts	: 428
c decisions	: 20880
c propagations	: 38460
c inspects	: 1400407
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 238
c 
c CURRENT OPTIMUM=16754514
c Current CPU time (ms) : 1178.214
c starts	: 219
c conflicts	: 428
c decisions	: 20969
c propagations	: 38622
c inspects	: 1412611
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 239
c 
c CURRENT OPTIMUM=16754513
c Current CPU time (ms) : 1188.841
c starts	: 220
c conflicts	: 428
c decisions	: 21059
c propagations	: 38784
c inspects	: 1425087
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 240
c 
c CURRENT OPTIMUM=16754512
c Current CPU time (ms) : 1199.337
c starts	: 221
c conflicts	: 428
c decisions	: 21148
c propagations	: 38946
c inspects	: 1437401
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 241
c 
c CURRENT OPTIMUM=16754511
c Current CPU time (ms) : 1209.897
c starts	: 222
c conflicts	: 428
c decisions	: 21237
c propagations	: 39108
c inspects	: 1449770
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 242
#### 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.84 0.88 2/54 1178
Raw data (stat): 1178 (runsolver) R 1177 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485026158 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.94 0.88 0.89 4/64 1188
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 15583 0 1 0 595 35 0 0 25 0 11 0 485026158 870342656 19567 4294967295 134512640 134569956 3221224400 3221214656 1130917749 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212486 19568 13073 16 0 212470 0
vsize: 849944
[startup+20.0025 s]
Raw data (loadavg): 1.17 0.93 0.91 2/64 1195
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18100 3 1 0 1415 41 0 0 25 0 11 0 485026158 870256640 22895 4294967295 134512640 134569956 3221224400 3221214896 1131185518 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212465 22895 13073 16 0 212449 0
vsize: 849860
[startup+30.0038 s]
Raw data (loadavg): 1.15 0.93 0.91 2/64 1207
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18101 3 1 0 2387 42 0 0 24 0 11 0 485026158 870256640 22914 4294967295 134512640 134569956 3221224400 3221214896 1131184533 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212465 22914 13073 16 0 212449 0
vsize: 849860
[startup+40.0036 s]
Raw data (loadavg): 1.20 0.95 0.91 2/64 1214
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 3348 43 0 0 25 0 11 0 485026158 872353792 23693 4294967295 134512640 134569956 3221224400 3221214776 1131175675 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 23693 13073 16 0 212961 0
vsize: 851908
[startup+50.0039 s]
Raw data (loadavg): 1.17 0.95 0.91 2/64 1221
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 4318 43 1 0 25 0 11 0 485026158 872353792 23723 4294967295 134512640 134569956 3221224400 3221214776 1131175649 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 23723 13073 16 0 212961 0
vsize: 851908
[startup+60.0041 s]
Raw data (loadavg): 1.14 0.95 0.91 2/64 1226
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 5298 44 1 0 25 0 11 0 485026158 872353792 23797 4294967295 134512640 134569956 3221224400 3221214776 1131176965 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 23797 13073 16 0 212961 0
vsize: 851908
[startup+70.0081 s]
Raw data (loadavg): 1.12 0.95 0.91 2/64 1231
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 6283 44 1 0 25 0 11 0 485026158 872353792 23873 4294967295 134512640 134569956 3221224400 3221214776 1131176187 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 212977 23873 13073 16 0 212961 0
vsize: 851908
[startup+80.0093 s]
Raw data (loadavg): 1.10 0.95 0.91 2/64 1235
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 7270 44 2 0 25 0 11 0 485026158 872353792 23912 4294967295 134512640 134569956 3221224400 3221214776 1131176229 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 23912 13073 16 0 212961 0
vsize: 851908
[startup+90.0098 s]
Raw data (loadavg): 1.08 0.95 0.91 2/64 1239
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 8255 45 2 0 25 0 11 0 485026158 872353792 23969 4294967295 134512640 134569956 3221224400 3221214872 1131184920 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 23969 13073 16 0 212961 0
vsize: 851908
[startup+100.01 s]
Raw data (loadavg): 1.07 0.96 0.91 2/64 1243
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 9240 45 2 0 25 0 11 0 485026158 872353792 24013 4294967295 134512640 134569956 3221224400 3221214776 1131176011 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24013 13073 16 0 212961 0
vsize: 851908
[startup+110.011 s]
Raw data (loadavg): 1.06 0.96 0.91 2/64 1246
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 10226 45 2 0 25 0 11 0 485026158 872353792 24079 4294967295 134512640 134569956 3221224400 3221214872 1131185581 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24079 13073 16 0 212961 0
vsize: 851908
[startup+120.011 s]
Raw data (loadavg): 1.05 0.96 0.91 2/64 1249
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 11215 45 2 0 25 0 11 0 485026158 872353792 24145 4294967295 134512640 134569956 3221224400 3221214776 1131176931 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24145 13073 16 0 212961 0
vsize: 851908
[startup+130.012 s]
Raw data (loadavg): 1.04 0.96 0.91 2/64 1252
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 12203 46 2 1 25 0 11 0 485026158 872353792 24209 4294967295 134512640 134569956 3221224400 3221214816 1131154128 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24209 13073 16 0 212961 0
vsize: 851908
[startup+140.012 s]
Raw data (loadavg): 1.03 0.96 0.91 2/64 1255
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 13192 46 3 1 25 0 11 0 485026158 872353792 24240 4294967295 134512640 134569956 3221224400 3221214752 1131425261 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24240 13073 16 0 212961 0
vsize: 851908
[startup+150.013 s]
Raw data (loadavg): 1.03 0.96 0.91 2/64 1258
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 14181 46 3 1 25 0 11 0 485026158 872353792 24298 4294967295 134512640 134569956 3221224400 3221214776 1131176038 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24298 13073 16 0 212961 0
vsize: 851908
[startup+160.014 s]
Raw data (loadavg): 1.02 0.96 0.91 2/64 1262
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 15170 46 3 1 25 0 11 0 485026158 872353792 24344 4294967295 134512640 134569956 3221224400 3221214816 1131154208 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24344 13073 16 0 212961 0
vsize: 851908
[startup+170.014 s]
Raw data (loadavg): 1.02 0.96 0.91 2/64 1266
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 16160 46 3 1 25 0 11 0 485026158 872353792 24384 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24384 13073 16 0 212961 0
vsize: 851908
[startup+180.015 s]
Raw data (loadavg): 1.02 0.96 0.91 2/64 1268
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 17149 47 3 1 25 0 11 0 485026158 872353792 24432 4294967295 134512640 134569956 3221224400 3221214776 1131176117 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24432 13073 16 0 212961 0
vsize: 851908
[startup+190.016 s]
Raw data (loadavg): 1.01 0.96 0.91 3/64 1271
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 18138 47 3 1 25 0 11 0 485026158 872353792 24479 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24479 13073 16 0 212961 0
vsize: 851908
[startup+200.016 s]
Raw data (loadavg): 1.01 0.97 0.91 2/64 1273
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 19129 47 3 1 25 0 11 0 485026158 872353792 24516 4294967295 134512640 134569956 3221224400 3221214816 1131451272 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24516 13073 16 0 212961 0
vsize: 851908
[startup+210.017 s]
Raw data (loadavg): 1.01 0.97 0.91 2/64 1276
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 20119 47 3 1 25 0 11 0 485026158 872353792 24557 4294967295 134512640 134569956 3221224400 3221214868 1131210632 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24557 13073 16 0 212961 0
vsize: 851908
[startup+220.018 s]
Raw data (loadavg): 1.01 0.97 0.91 2/64 1278
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 21108 48 3 1 25 0 11 0 485026158 872353792 24604 4294967295 134512640 134569956 3221224400 3221214776 1131176080 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24604 13073 16 0 212961 0
vsize: 851908
[startup+230.019 s]
Raw data (loadavg): 1.01 0.97 0.91 2/64 1280
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 22098 48 3 1 25 0 11 0 485026158 872353792 24640 4294967295 134512640 134569956 3221224400 3221214776 1131175937 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24640 13073 16 0 212961 0
vsize: 851908
[startup+240.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1282
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 23089 48 3 1 25 0 11 0 485026158 872353792 24674 4294967295 134512640 134569956 3221224400 3221214816 1131154045 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24674 13073 16 0 212961 0
vsize: 851908
[startup+250.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1285
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 24079 49 3 1 25 0 11 0 485026158 872353792 24713 4294967295 134512640 134569956 3221224400 3221214776 1131176539 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24713 13073 16 0 212961 0
vsize: 851908
[startup+260.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1288
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 25067 49 4 1 24 0 11 0 485026158 872353792 24758 4294967295 134512640 134569956 3221224400 3221214776 1131175969 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24758 13073 16 0 212961 0
vsize: 851908
[startup+270.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1290
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 26054 49 4 1 25 0 11 0 485026158 872353792 24797 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24797 13073 16 0 212961 0
vsize: 851908
[startup+280.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1292
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 27040 49 4 1 25 0 11 0 485026158 872353792 24842 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24842 13073 16 0 212961 0
vsize: 851908
[startup+290.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1294
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 28029 49 4 1 25 0 11 0 485026158 872353792 24912 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24912 13073 16 0 212961 0
vsize: 851908
[startup+300.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1296
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 29021 49 4 1 25 0 11 0 485026158 872353792 24946 4294967295 134512640 134569956 3221224400 3221214776 1131175645 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24946 13073 16 0 212961 0
vsize: 851908
[startup+310.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1298
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 30010 49 4 1 25 0 11 0 485026158 872353792 24993 4294967295 134512640 134569956 3221224400 3221214776 1131175749 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 24993 13073 16 0 212961 0
vsize: 851908
[startup+320.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1300
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 30999 50 4 1 25 0 11 0 485026158 872353792 25038 4294967295 134512640 134569956 3221224400 3221214848 1131210553 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25038 13073 16 0 212961 0
vsize: 851908
[startup+330.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1301
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 31988 50 4 1 25 0 11 0 485026158 872353792 25099 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25099 13073 16 0 212961 0
vsize: 851908
[startup+340.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1303
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 32978 50 4 1 25 0 11 0 485026158 872353792 25144 4294967295 134512640 134569956 3221224400 3221214776 1131175667 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25144 13073 16 0 212961 0
vsize: 851908
[startup+350.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1305
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 33968 50 4 1 25 0 11 0 485026158 872353792 25181 4294967295 134512640 134569956 3221224400 3221214776 1131176141 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25181 13073 16 0 212961 0
vsize: 851908
[startup+360.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1307
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 34957 51 4 2 25 0 11 0 485026158 872353792 25228 4294967295 134512640 134569956 3221224400 3221214872 1131185533 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25228 13073 16 0 212961 0
vsize: 851908
[startup+370.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1308
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 35945 51 4 2 25 0 11 0 485026158 872353792 25257 4294967295 134512640 134569956 3221224400 3221214816 1131154073 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25257 13073 16 0 212961 0
vsize: 851908
[startup+380.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1310
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 36935 51 4 2 25 0 11 0 485026158 872353792 25319 4294967295 134512640 134569956 3221224400 3221214776 1131176343 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25319 13073 16 0 212961 0
vsize: 851908
[startup+390.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1312
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 37924 51 4 2 25 0 11 0 485026158 872353792 25379 4294967295 134512640 134569956 3221224400 3221214776 1131176205 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25379 13073 16 0 212961 0
vsize: 851908
[startup+400.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1314
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 38913 52 4 2 25 0 11 0 485026158 872353792 25417 4294967295 134512640 134569956 3221224400 3221214776 1131175948 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25417 13073 16 0 212961 0
vsize: 851908
[startup+410.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1315
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 39903 52 5 2 25 0 11 0 485026158 872353792 25470 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25470 13073 16 0 212961 0
vsize: 851908
[startup+420.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1318
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 40893 52 5 2 25 0 11 0 485026158 872353792 25508 4294967295 134512640 134569956 3221224400 3221214776 1131176205 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25508 13073 16 0 212961 0
vsize: 851908
[startup+430.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1319
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 41882 52 5 2 25 0 11 0 485026158 872353792 25566 4294967295 134512640 134569956 3221224400 3221214776 1131176925 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25566 13073 16 0 212961 0
vsize: 851908
[startup+440.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1321
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 42871 52 5 2 25 0 11 0 485026158 872353792 25607 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25607 13073 16 0 212961 0
vsize: 851908
[startup+450.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1323
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 43861 52 5 2 25 0 11 0 485026158 872353792 25658 4294967295 134512640 134569956 3221224400 3221214776 1131175649 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25658 13073 16 0 212961 0
vsize: 851908
[startup+460.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1324
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 44850 53 5 2 25 0 11 0 485026158 872353792 25692 4294967295 134512640 134569956 3221224400 3221214776 1131175649 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25692 13073 16 0 212961 0
vsize: 851908
[startup+470.061 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1326
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 45841 53 5 2 25 0 11 0 485026158 872353792 25744 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25744 13073 16 0 212961 0
vsize: 851908
[startup+480.061 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1327
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 46831 53 5 2 25 0 11 0 485026158 872353792 25780 4294967295 134512640 134569956 3221224400 3221214776 1131175667 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25780 13073 16 0 212961 0
vsize: 851908
[startup+490.061 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1329
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 47820 53 5 2 25 0 11 0 485026158 872353792 25832 4294967295 134512640 134569956 3221224400 3221214872 1131184910 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25832 13073 16 0 212961 0
vsize: 851908
[startup+500.062 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1330
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 48809 54 5 2 25 0 11 0 485026158 872353792 25863 4294967295 134512640 134569956 3221224400 3221214776 1131175959 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25863 13073 16 0 212961 0
vsize: 851908
[startup+510.062 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1332
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 49800 54 5 2 25 0 11 0 485026158 872353792 25916 4294967295 134512640 134569956 3221224400 3221214776 1131176289 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25916 13073 16 0 212961 0
vsize: 851908
[startup+520.062 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1333
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 50790 54 5 2 25 0 11 0 485026158 872353792 25947 4294967295 134512640 134569956 3221224400 3221214776 1131176011 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 25947 13073 16 0 212961 0
vsize: 851908
[startup+530.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1335
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 51779 54 5 2 25 0 11 0 485026158 872353792 26001 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26001 13073 16 0 212961 0
vsize: 851908
[startup+540.064 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1336
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 52769 54 5 2 25 0 11 0 485026158 872353792 26032 4294967295 134512640 134569956 3221224400 3221214776 1131176944 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26032 13073 16 0 212961 0
vsize: 851908
[startup+550.064 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1337
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 53759 54 5 2 25 0 11 0 485026158 872353792 26086 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26086 13073 16 0 212961 0
vsize: 851908
[startup+560.065 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1339
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 54750 54 5 2 25 0 11 0 485026158 872353792 26115 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26115 13073 16 0 212961 0
vsize: 851908
[startup+570.065 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1340
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 55739 55 6 2 25 0 11 0 485026158 872353792 26149 4294967295 134512640 134569956 3221224400 3221214776 1131175961 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26149 13073 16 0 212961 0
vsize: 851908
[startup+580.065 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1341
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 56729 55 6 2 25 0 11 0 485026158 872353792 26205 4294967295 134512640 134569956 3221224400 3221214832 1131425344 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26205 13073 16 0 212961 0
vsize: 851908
[startup+590.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1343
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 57720 55 6 2 25 0 11 0 485026158 872353792 26238 4294967295 134512640 134569956 3221224400 3221214776 1131177004 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26238 13073 16 0 212961 0
vsize: 851908
[startup+600.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1344
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 58709 55 6 2 25 0 11 0 485026158 872353792 26277 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26277 13073 16 0 212961 0
vsize: 851908
[startup+610.067 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1345
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 59700 55 6 2 25 0 11 0 485026158 872353792 26316 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26316 13073 16 0 212961 0
vsize: 851908
[startup+620.067 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1347
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 60690 56 6 2 25 0 11 0 485026158 872353792 26355 4294967295 134512640 134569956 3221224400 3221214776 1131176291 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26355 13073 16 0 212961 0
vsize: 851908
[startup+630.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1348
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 61680 56 6 2 25 0 11 0 485026158 872353792 26395 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26395 13073 16 0 212961 0
vsize: 851908
[startup+640.067 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 1349
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 62670 57 6 2 25 0 11 0 485026158 872353792 26436 4294967295 134512640 134569956 3221224400 3221214776 1131175724 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26436 13073 16 0 212961 0
vsize: 851908
[startup+650.068 s]
Raw data (loadavg): 1.22 1.02 0.93 2/64 1351
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 63660 57 6 2 25 0 11 0 485026158 872353792 26468 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26468 13073 16 0 212961 0
vsize: 851908
[startup+660.068 s]
Raw data (loadavg): 1.19 1.02 0.93 2/64 1352
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 64651 57 6 2 25 0 11 0 485026158 872353792 26507 4294967295 134512640 134569956 3221224400 3221214776 1131176106 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26507 13073 16 0 212961 0
vsize: 851908
[startup+670.068 s]
Raw data (loadavg): 1.16 1.02 0.93 2/64 1353
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 65642 57 6 2 25 0 11 0 485026158 872353792 26548 4294967295 134512640 134569956 3221224400 3221214872 1131184927 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26548 13073 16 0 212961 0
vsize: 851908
[startup+680.068 s]
Raw data (loadavg): 1.13 1.02 0.93 2/64 1354
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 66632 57 6 2 25 0 11 0 485026158 872353792 26583 4294967295 134512640 134569956 3221224400 3221214776 1131176361 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26583 13073 16 0 212961 0
vsize: 851908
[startup+690.068 s]
Raw data (loadavg): 1.11 1.02 0.93 2/64 1356
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 67622 58 6 2 25 0 11 0 485026158 872353792 26612 4294967295 134512640 134569956 3221224400 3221214872 1131184709 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26612 13073 16 0 212961 0
vsize: 851908
[startup+700.068 s]
Raw data (loadavg): 1.09 1.02 0.93 2/64 1357
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 68612 58 6 3 25 0 11 0 485026158 872353792 26651 4294967295 134512640 134569956 3221224400 3221214816 1131154045 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26651 13073 16 0 212961 0
vsize: 851908
[startup+710.07 s]
Raw data (loadavg): 1.08 1.01 0.93 2/64 1358
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 69604 58 7 3 25 0 11 0 485026158 872353792 26683 4294967295 134512640 134569956 3221224400 3221214776 1131175656 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26683 13073 16 0 212961 0
vsize: 851908
[startup+720.07 s]
Raw data (loadavg): 1.07 1.01 0.93 2/64 1359
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 70594 58 7 3 25 0 11 0 485026158 872353792 26723 4294967295 134512640 134569956 3221224400 3221214776 1131176011 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26723 13073 16 0 212961 0
vsize: 851908
[startup+730.07 s]
Raw data (loadavg): 1.06 1.01 0.93 2/64 1362
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 71583 59 7 3 25 0 11 0 485026158 872353792 26753 4294967295 134512640 134569956 3221224400 3221214816 1131154073 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26753 13073 16 0 212961 0
vsize: 851908
[startup+740.07 s]
Raw data (loadavg): 1.05 1.01 0.93 2/64 1363
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 72573 59 7 3 25 0 11 0 485026158 872353792 26792 4294967295 134512640 134569956 3221224400 3221214776 1131176061 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26792 13073 16 0 212961 0
vsize: 851908
[startup+750.07 s]
Raw data (loadavg): 1.04 1.01 0.93 2/64 1364
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 73564 59 7 3 25 0 11 0 485026158 872353792 26829 4294967295 134512640 134569956 3221224400 3221214872 1131184882 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26829 13073 16 0 212961 0
vsize: 851908
[startup+760.071 s]
Raw data (loadavg): 1.03 1.01 0.93 2/64 1365
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 74554 59 7 3 25 0 11 0 485026158 872353792 26870 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26870 13073 16 0 212961 0
vsize: 851908
[startup+770.072 s]
Raw data (loadavg): 1.03 1.01 0.93 2/64 1366
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 75545 60 7 3 25 0 11 0 485026158 872353792 26900 4294967295 134512640 134569956 3221224400 3221214776 1131175653 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26900 13073 16 0 212961 0
vsize: 851908
[startup+780.072 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 1368
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 76535 60 7 3 25 0 11 0 485026158 872353792 26935 4294967295 134512640 134569956 3221224400 3221214776 1131176381 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26935 13073 16 0 212961 0
vsize: 851908
[startup+790.072 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 1369
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 77525 60 7 3 25 0 11 0 485026158 872353792 26971 4294967295 134512640 134569956 3221224400 3221214816 1131154073 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 26971 13073 16 0 212961 0
vsize: 851908
[startup+800.072 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 1370
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 78516 60 7 3 17 0 11 0 485026158 872353792 27002 4294967295 134512640 134569956 3221224400 3221214776 1131175653 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27002 13073 16 0 212961 0
vsize: 851908
[startup+810.072 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 1371
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 79507 60 7 3 25 0 11 0 485026158 872353792 27043 4294967295 134512640 134569956 3221224400 3221214776 1131176551 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27043 13073 16 0 212961 0
vsize: 851908
[startup+820.073 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 1372
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 80498 60 7 3 25 0 11 0 485026158 872353792 27071 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27071 13073 16 0 212961 0
vsize: 851908
[startup+830.074 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 1373
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 81488 61 7 3 25 0 11 0 485026158 872353792 27101 4294967295 134512640 134569956 3221224400 3221214816 1131154065 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27101 13073 16 0 212961 0
vsize: 851908
[startup+840.074 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 1374
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 82479 61 7 3 25 0 11 0 485026158 872353792 27138 4294967295 134512640 134569956 3221224400 3221214776 1131176002 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27138 13073 16 0 212961 0
vsize: 851908
[startup+850.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1376
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 83469 61 7 3 25 0 11 0 485026158 872353792 27172 4294967295 134512640 134569956 3221224400 3221214872 1131185653 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27172 13073 16 0 212961 0
vsize: 851908
[startup+860.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1377
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 84460 61 7 3 25 0 11 0 485026158 872353792 27200 4294967295 134512640 134569956 3221224400 3221214872 1131185493 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27200 13073 16 0 212961 0
vsize: 851908
[startup+870.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1378
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 85451 62 7 3 25 0 11 0 485026158 872353792 27229 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27229 13073 16 0 212961 0
vsize: 851908
[startup+880.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1379
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 86441 62 7 3 25 0 11 0 485026158 872353792 27260 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27260 13073 16 0 212961 0
vsize: 851908
[startup+890.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1380
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 87431 62 7 3 25 0 11 0 485026158 872353792 27301 4294967295 134512640 134569956 3221224400 3221214776 1131176466 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27301 13073 16 0 212961 0
vsize: 851908
[startup+900.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1381
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 88421 62 7 3 25 0 11 0 485026158 872353792 27329 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27329 13073 16 0 212961 0
vsize: 851908
[startup+910.078 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1382
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 89411 63 7 3 25 0 11 0 485026158 872353792 27369 4294967295 134512640 134569956 3221224400 3221214872 1131184728 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27369 13073 16 0 212961 0
vsize: 851908
[startup+920.078 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1383
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 90400 63 7 3 25 0 11 0 485026158 872353792 27402 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27402 13073 16 0 212961 0
vsize: 851908
[startup+930.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1384
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 91390 63 8 3 25 0 11 0 485026158 872353792 27431 4294967295 134512640 134569956 3221224400 3221214816 1131154258 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27431 13073 16 0 212961 0
vsize: 851908
[startup+940.078 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1385
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 92377 63 8 3 25 0 11 0 485026158 872353792 27473 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27473 13073 16 0 212961 0
vsize: 851908
[startup+950.079 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1386
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 93360 63 8 3 25 0 11 0 485026158 872353792 27522 4294967295 134512640 134569956 3221224400 3221214832 1131425356 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27522 13073 16 0 212961 0
vsize: 851908
[startup+960.079 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1388
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 94342 64 8 3 24 0 11 0 485026158 872353792 27565 4294967295 134512640 134569956 3221224400 3221214816 1131154073 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27565 13073 16 0 212961 0
vsize: 851908
[startup+970.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1389
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 95329 64 8 3 25 0 11 0 485026158 872353792 27648 4294967295 134512640 134569956 3221224400 3221214868 1131210528 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27648 13073 16 0 212961 0
vsize: 851908
[startup+980.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1390
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 96319 64 8 3 25 0 11 0 485026158 872353792 27691 4294967295 134512640 134569956 3221224400 3221214776 1131175669 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27691 13073 16 0 212961 0
vsize: 851908
[startup+990.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1391
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 97309 64 8 3 25 0 11 0 485026158 872353792 27719 4294967295 134512640 134569956 3221224400 3221214816 1131154206 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27719 13073 16 0 212961 0
vsize: 851908
[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1392
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 98299 64 8 3 25 0 11 0 485026158 872353792 27748 4294967295 134512640 134569956 3221224400 3221214816 1131154065 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27748 13073 16 0 212961 0
vsize: 851908
[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1393
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 99289 64 8 3 25 0 11 0 485026158 872353792 27777 4294967295 134512640 134569956 3221224400 3221214776 1131176498 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27777 13073 16 0 212961 0
vsize: 851908
[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1394
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 100280 64 8 3 25 0 11 0 485026158 872353792 27817 4294967295 134512640 134569956 3221224400 3221214776 1131175667 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27817 13073 16 0 212961 0
vsize: 851908
[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1395
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 101270 64 8 3 25 0 11 0 485026158 872353792 27847 4294967295 134512640 134569956 3221224400 3221214872 1131184533 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27847 13073 16 0 212961 0
vsize: 851908
[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1396
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 102261 64 8 3 25 0 11 0 485026158 872353792 27876 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27876 13073 16 0 212961 0
vsize: 851908
[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1397
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 103251 65 8 3 25 0 11 0 485026158 872353792 27906 4294967295 134512640 134569956 3221224400 3221214776 1131175653 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27906 13073 16 0 212961 0
vsize: 851908
[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1398
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 104241 65 8 3 25 0 11 0 485026158 872353792 27935 4294967295 134512640 134569956 3221224400 3221214816 1131154204 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27935 13073 16 0 212961 0
vsize: 851908
[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1399
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 105231 65 8 3 25 0 11 0 485026158 872353792 27964 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27964 13073 16 0 212961 0
vsize: 851908
[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1400
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 106221 65 8 3 25 0 11 0 485026158 872353792 27992 4294967295 134512640 134569956 3221224400 3221214872 1131185466 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 27992 13073 16 0 212961 0
vsize: 851908
[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1401
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 107213 65 8 3 25 0 11 0 485026158 872353792 28020 4294967295 134512640 134569956 3221224400 3221214816 1131154163 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28020 13073 16 0 212961 0
vsize: 851908
[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1402
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 108203 66 8 3 25 0 11 0 485026158 872353792 28049 4294967295 134512640 134569956 3221224400 3221214776 1131175649 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28049 13073 16 0 212961 0
vsize: 851908
[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1403
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 109193 66 8 3 25 0 11 0 485026158 872353792 28077 4294967295 134512640 134569956 3221224400 3221214776 1131176110 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28077 13073 16 0 212961 0
vsize: 851908
[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1404
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 110183 66 8 3 25 0 11 0 485026158 872353792 28105 4294967295 134512640 134569956 3221224400 3221214776 1131176306 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28105 13073 16 0 212961 0
vsize: 851908
[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1405
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 111172 66 8 3 25 0 11 0 485026158 872353792 28133 4294967295 134512640 134569956 3221224400 3221214872 1131185485 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28133 13073 16 0 212961 0
vsize: 851908
[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1406
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 112161 66 8 3 25 0 11 0 485026158 872353792 28161 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28161 13073 16 0 212961 0
vsize: 851908
[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1407
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 113151 67 8 3 25 0 11 0 485026158 872353792 28211 4294967295 134512640 134569956 3221224400 3221214816 1131154048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28211 13073 16 0 212961 0
vsize: 851908
[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1408
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 114140 67 9 3 25 0 11 0 485026158 872353792 28263 4294967295 134512640 134569956 3221224400 3221214776 1131176057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28263 13073 16 0 212961 0
vsize: 851908
[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1409
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 115129 67 9 3 25 0 11 0 485026158 872353792 28291 4294967295 134512640 134569956 3221224400 3221214776 1131175653 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28291 13073 16 0 212961 0
vsize: 851908
[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1410
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 116118 67 9 3 25 0 11 0 485026158 872353792 28343 4294967295 134512640 134569956 3221224400 3221214776 1131176539 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28343 13073 16 0 212961 0
vsize: 851908
[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1411
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 117106 67 9 3 24 0 11 0 485026158 872353792 28401 4294967295 134512640 134569956 3221224400 3221214872 1131184737 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28401 13073 16 0 212961 0
vsize: 851908
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1412
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 118094 67 9 3 25 0 11 0 485026158 872353792 28429 4294967295 134512640 134569956 3221224400 3221214816 1131154065 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28429 13073 16 0 212961 0
vsize: 851908
[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1412
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 119081 67 9 3 25 0 11 0 485026158 872353792 28481 4294967295 134512640 134569956 3221224400 3221214776 1131175683 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28481 13073 16 0 212961 0
vsize: 851908
[startup+1220.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 1413
Raw data (stat): 1178 (java) R 1177 29151 29150 0 -1 0 18105 3 1 0 120069 67 9 3 25 0 11 0 485026158 872353792 28575 4294967295 134512640 134569956 3221224400 3221214776 1131176533 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212977 28575 13073 16 0 212961 0
vsize: 851908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1220.17 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 1415
Raw data (stat): 1178 (java) Z 1177 29151 29150 0 -1 1036 18105 5728 1 0 120071 67 1337 32 25 0 1 0 485026158 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): 1220.17
CPU time (s): 1215.1
CPU user time (s): 1214.09
CPU system time (s): 1.00385
CPU usage (%): 99.5842
Max. virtual memory (Kb): 851908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####