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/miplib/normalized-mps-v2-20-10-flugpl.opb
MD5SUM	7b40a76c609224f38c1798eb54355221
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.8077
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 17052

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        536216 kB
Buffers:         31892 kB
Cached:         436264 kB
SwapCached:         24 kB
Active:         153428 kB
Inactive:       317384 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        535964 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            21976 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 09:53:41 (client local time) WITH STATUS 143 IN 1215.03 SECONDS
stats: 11865 7 1215.03 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-flugpl.opb
c reading problem 
c [nbvar=265]
c [nbconstr=29]
c time 0.746
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) : 12.942
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.452
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) : 13.947
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.521
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.139
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.856
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.15
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.773
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.478
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.207
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.145
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.858
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.629
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.418
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.255
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.145
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.074
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.068
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.096
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.241
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.339
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.549
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.788
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.107
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.42
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.812
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.21
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.692
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.197
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) : 43.79
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.422
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.1
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) : 48.785
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.558
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.35
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.186
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.029
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) : 57.999
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) : 59.987
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.033
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.058
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.178
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.306
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) : 70.482
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) : 72.662
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.045
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) : 77.453
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) : 79.893
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) : 82.344
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) : 84.879
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) : 87.423
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.029
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) : 92.668
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) : 95.446
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) : 98.207
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.003
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) : 103.814
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) : 106.723
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) : 109.624
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) : 112.563
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) : 115.491
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) : 118.622
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) : 121.752
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) : 124.936
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) : 128.13
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) : 131.418
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) : 134.696
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) : 137.998
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) : 141.318
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) : 144.79
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) : 148.257
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) : 151.769
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) : 155.261
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) : 158.867
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) : 162.466
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) : 166.097
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) : 169.726
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) : 173.701
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) : 177.674
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) : 181.707
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) : 185.72
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) : 189.846
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) : 193.94
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) : 198.093
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) : 202.215
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) : 206.523
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) : 210.821
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) : 215.151
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) : 219.485
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) : 223.916
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) : 228.312
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) : 232.793
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) : 237.244
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) : 241.942
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) : 246.637
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) : 251.37
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) : 256.088
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) : 260.937
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) : 265.748
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) : 270.622
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) : 275.47
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) : 280.524
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) : 285.533
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) : 290.583
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) : 295.604
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) : 300.753
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) : 305.88
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) : 311.065
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) : 316.175
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) : 321.713
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) : 327.21
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) : 332.738
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) : 338.223
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) : 343.827
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) : 349.409
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) : 355.035
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) : 360.602
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) : 366.429
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) : 372.197
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) : 378.019
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) : 383.773
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) : 389.691
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) : 395.539
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) : 401.453
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) : 407.313
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) : 413.514
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) : 419.674
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) : 425.88
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) : 432.016
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) : 438.31
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) : 444.551
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) : 450.838
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) : 457.076
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) : 463.573
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) : 469.988
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) : 476.463
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) : 482.855
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) : 489.388
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) : 495.855
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) : 502.387
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) : 508.843
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) : 516.037
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) : 523.179
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) : 530.353
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) : 537.474
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) : 544.754
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) : 551.97
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) : 559.271
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) : 566.576
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) : 574.175
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) : 581.675
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) : 589.255
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) : 596.766
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) : 604.433
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) : 612.03
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) : 619.674
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) : 627.239
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) : 635.246
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) : 643.165
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) : 651.138
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) : 659.019
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) : 667.079
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) : 675.048
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) : 683.077
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) : 691.009
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) : 699.269
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) : 707.431
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) : 715.627
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) : 723.749
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) : 732.067
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) : 740.287
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) : 748.555
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) : 756.738
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) : 765.529
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) : 774.229
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) : 782.986
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) : 791.651
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) : 800.501
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) : 809.253
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) : 818.054
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) : 826.737
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) : 835.794
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) : 844.729
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) : 853.715
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) : 862.605
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) : 871.702
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) : 880.681
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) : 889.707
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) : 898.632
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) : 908.081
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) : 917.408
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) : 926.801
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) : 936.113
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) : 945.66
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) : 955.09
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) : 964.545
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) : 973.85
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) : 983.512
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) : 993.074
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) : 1002.692
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) : 1012.175
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) : 1021.874
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) : 1031.448
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) : 1041.09
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) : 1050.586
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) : 1060.992
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) : 1071.263
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) : 1081.595
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) : 1091.81
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) : 1102.242
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) : 1112.554
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) : 1122.919
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) : 1133.16
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) : 1143.779
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) : 1154.304
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) : 1164.852
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) : 1175.249
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) : 1185.89
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) : 1196.392
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) : 1206.961
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
c 
c CURRENT OPTIMUM=16754510
c Current CPU time (ms) : 1217.382
c starts	: 223
c conflicts	: 428
c decisions	: 21325
c propagations	: 39270
c inspects	: 1461974
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 2
c learned clauses	: 428
c root simplifications	: 243
#### 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.85 0.97 0.93 1/54 30739
Raw data (stat): 30739 (runsolver) R 30738 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544028499 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+9.99996 s]
Raw data (loadavg): 1.18 1.03 0.95 4/64 30749
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 12012 0 1 0 534 26 0 0 25 0 11 0 544028499 871874560 16527 4294967295 134512640 134569956 3221224400 3221214776 1131167708 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212860 16529 13073 16 0 212844 0
vsize: 851440
[startup+20.0012 s]
Raw data (loadavg): 1.38 1.08 0.97 2/64 30756
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18125 4 1 0 1410 39 0 0 25 0 11 0 544028499 869781504 22696 4294967295 134512640 134569956 3221224400 3221214840 1131157440 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 212349 22696 13073 16 0 212333 0
vsize: 849396
[startup+30.0019 s]
Raw data (loadavg): 1.32 1.08 0.97 2/64 30768
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 2382 40 0 0 24 0 11 0 544028499 869781504 22806 4294967295 134512640 134569956 3221224400 3221214840 1131157440 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 212349 22806 13073 16 0 212333 0
vsize: 849396
[startup+40.001 s]
Raw data (loadavg): 1.35 1.09 0.97 2/64 30776
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 3348 41 1 0 25 0 11 0 544028499 867639296 22551 4294967295 134512640 134569956 3221224400 3221214776 1131167682 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 22551 13073 16 0 211810 0
vsize: 847304
[startup+50.0023 s]
Raw data (loadavg): 1.29 1.09 0.97 2/64 30782
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 4316 41 1 0 25 0 11 0 544028499 867639296 22702 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 22702 13073 16 0 211810 0
vsize: 847304
[startup+60.003 s]
Raw data (loadavg): 1.25 1.08 0.97 2/64 30787
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 5299 42 1 0 25 0 11 0 544028499 867639296 22767 4294967295 134512640 134569956 3221224400 3221214816 1131157443 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 22767 13073 16 0 211810 0
vsize: 847304
[startup+70.0032 s]
Raw data (loadavg): 1.21 1.08 0.97 2/64 30792
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 6285 42 1 0 25 0 11 0 544028499 867639296 22839 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 22839 13073 16 0 211810 0
vsize: 847304
[startup+80.0045 s]
Raw data (loadavg): 1.18 1.08 0.97 2/64 30796
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 7270 42 1 0 25 0 11 0 544028499 867639296 22879 4294967295 134512640 134569956 3221224400 3221214872 1131175617 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 22879 13073 16 0 211810 0
vsize: 847304
[startup+90.0045 s]
Raw data (loadavg): 1.15 1.08 0.97 2/64 30800
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 8256 42 1 0 24 0 11 0 544028499 867639296 22876 4294967295 134512640 134569956 3221224400 3221214776 1131166894 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 22876 13073 16 0 211810 0
vsize: 847304
[startup+100.004 s]
Raw data (loadavg): 1.12 1.07 0.97 2/64 30804
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 9241 43 1 0 25 0 11 0 544028499 867639296 22917 4294967295 134512640 134569956 3221224400 3221214872 1131175874 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 22917 13073 16 0 211810 0
vsize: 847304
[startup+110.008 s]
Raw data (loadavg): 1.11 1.07 0.97 2/64 30807
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 10227 43 2 0 25 0 11 0 544028499 867639296 22985 4294967295 134512640 134569956 3221224400 3221214776 1131166780 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 22985 13073 16 0 211810 0
vsize: 847304
[startup+120.014 s]
Raw data (loadavg): 1.09 1.07 0.97 2/64 30811
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 11215 43 2 0 25 0 11 0 544028499 867639296 23060 4294967295 134512640 134569956 3221224400 3221214816 1131157586 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23060 13073 16 0 211810 0
vsize: 847304
[startup+130.015 s]
Raw data (loadavg): 1.07 1.06 0.97 2/64 30814
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 12204 43 2 0 25 0 11 0 544028499 867639296 23112 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23112 13073 16 0 211810 0
vsize: 847304
[startup+140.015 s]
Raw data (loadavg): 1.06 1.06 0.97 2/64 30817
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 13192 43 2 0 25 0 11 0 544028499 867639296 23145 4294967295 134512640 134569956 3221224400 3221214776 1131167393 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23145 13073 16 0 211810 0
vsize: 847304
[startup+150.016 s]
Raw data (loadavg): 1.05 1.06 0.97 2/64 30820
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 14180 44 2 1 25 0 11 0 544028499 867639296 23215 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23215 13073 16 0 211810 0
vsize: 847304
[startup+160.016 s]
Raw data (loadavg): 1.04 1.06 0.97 2/64 30823
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 15169 44 2 1 25 0 11 0 544028499 867639296 23255 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23255 13073 16 0 211810 0
vsize: 847304
[startup+170.017 s]
Raw data (loadavg): 1.04 1.05 0.97 2/64 30825
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 16159 44 3 1 25 0 11 0 544028499 867639296 23300 4294967295 134512640 134569956 3221224400 3221214816 1131157457 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23300 13073 16 0 211810 0
vsize: 847304
[startup+180.018 s]
Raw data (loadavg): 1.03 1.05 0.97 2/64 30828
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 17148 45 3 1 25 0 11 0 544028499 867639296 23349 4294967295 134512640 134569956 3221224400 3221214776 1131167069 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23349 13073 16 0 211810 0
vsize: 847304
[startup+190.018 s]
Raw data (loadavg): 1.03 1.05 0.97 2/64 30830
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 18138 45 3 1 25 0 11 0 544028499 867639296 23394 4294967295 134512640 134569956 3221224400 3221214848 1131208826 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23394 13073 16 0 211810 0
vsize: 847304
[startup+200.018 s]
Raw data (loadavg): 1.02 1.05 0.97 2/64 30833
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 19128 45 3 1 25 0 11 0 544028499 867639296 23429 4294967295 134512640 134569956 3221224400 3221214776 1131166497 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23429 13073 16 0 211810 0
vsize: 847304
[startup+210.019 s]
Raw data (loadavg): 1.02 1.05 0.97 2/64 30835
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 20118 45 3 1 25 0 11 0 544028499 867639296 23475 4294967295 134512640 134569956 3221224400 3221214816 1131157618 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23475 13073 16 0 211810 0
vsize: 847304
[startup+220.02 s]
Raw data (loadavg): 1.01 1.04 0.97 2/64 30837
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 21108 45 3 1 25 0 11 0 544028499 867639296 23510 4294967295 134512640 134569956 3221224400 3221214776 1131166497 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23510 13073 16 0 211810 0
vsize: 847304
[startup+230.02 s]
Raw data (loadavg): 1.01 1.04 0.97 2/64 30840
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 22098 46 3 1 25 0 11 0 544028499 867639296 23549 4294967295 134512640 134569956 3221224400 3221214816 1131157473 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23549 13073 16 0 211810 0
vsize: 847304
[startup+240.02 s]
Raw data (loadavg): 1.01 1.04 0.97 2/64 30842
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 23088 46 3 1 25 0 11 0 544028499 867639296 23591 4294967295 134512640 134569956 3221224400 3221214776 1131167804 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23591 13073 16 0 211810 0
vsize: 847304
[startup+250.02 s]
Raw data (loadavg): 1.01 1.04 0.97 2/64 30844
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 24077 46 3 1 25 0 11 0 544028499 867639296 23627 4294967295 134512640 134569956 3221224400 3221214776 1131166537 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23627 13073 16 0 211810 0
vsize: 847304
[startup+260.02 s]
Raw data (loadavg): 1.01 1.04 0.97 2/64 30846
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 25065 46 3 1 25 0 11 0 544028499 867639296 23671 4294967295 134512640 134569956 3221224400 3221214872 1131175617 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23671 13073 16 0 211810 0
vsize: 847304
[startup+270.021 s]
Raw data (loadavg): 1.00 1.03 0.97 2/64 30848
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 26050 46 3 1 24 0 11 0 544028499 867639296 23712 4294967295 134512640 134569956 3221224400 3221214776 1131166826 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23712 13073 16 0 211810 0
vsize: 847304
[startup+280.021 s]
Raw data (loadavg): 1.00 1.03 0.97 2/64 30850
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 27038 47 4 1 25 0 11 0 544028499 867639296 23760 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23760 13073 16 0 211810 0
vsize: 847304
[startup+290.022 s]
Raw data (loadavg): 1.00 1.03 0.97 2/64 30852
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 28027 47 4 1 25 0 11 0 544028499 867639296 23832 4294967295 134512640 134569956 3221224400 3221214816 1131157457 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23832 13073 16 0 211810 0
vsize: 847304
[startup+300.022 s]
Raw data (loadavg): 1.00 1.03 0.97 2/64 30854
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 29016 47 4 1 25 0 11 0 544028499 867639296 23863 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23863 13073 16 0 211810 0
vsize: 847304
[startup+310.023 s]
Raw data (loadavg): 1.00 1.03 0.97 2/64 30856
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 30004 48 4 1 25 0 11 0 544028499 867639296 23911 4294967295 134512640 134569956 3221224400 3221214776 1131167379 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23911 13073 16 0 211810 0
vsize: 847304
[startup+320.024 s]
Raw data (loadavg): 1.00 1.03 0.97 2/64 30858
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 30993 48 4 1 25 0 11 0 544028499 867639296 23969 4294967295 134512640 134569956 3221224400 3221214776 1131166863 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 23969 13073 16 0 211810 0
vsize: 847304
[startup+330.025 s]
Raw data (loadavg): 1.00 1.03 0.97 2/64 30860
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 31982 48 4 1 25 0 11 0 544028499 867639296 24012 4294967295 134512640 134569956 3221224400 3221214776 1131167776 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24012 13073 16 0 211810 0
vsize: 847304
[startup+340.025 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30862
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 32972 48 4 1 25 0 11 0 544028499 867639296 24056 4294967295 134512640 134569956 3221224400 3221214776 1131166493 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24056 13073 16 0 211810 0
vsize: 847304
[startup+350.025 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30863
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 33961 48 4 1 25 0 11 0 544028499 867639296 24101 4294967295 134512640 134569956 3221224400 3221214816 1131157461 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24101 13073 16 0 211810 0
vsize: 847304
[startup+360.026 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30865
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18126 4 1 0 34950 48 4 1 25 0 11 0 544028499 867639296 24144 4294967295 134512640 134569956 3221224400 3221214776 1131166851 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24144 13073 16 0 211810 0
vsize: 847304
[startup+370.027 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30867
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 35939 49 4 1 25 0 11 0 544028499 867639296 24171 4294967295 134512640 134569956 3221224400 3221214776 1131166925 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24171 13073 16 0 211810 0
vsize: 847304
[startup+380.027 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30869
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 36927 49 4 2 25 0 11 0 544028499 867639296 24254 4294967295 134512640 134569956 3221224400 3221214776 1131167839 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24254 13073 16 0 211810 0
vsize: 847304
[startup+390.027 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30870
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 37917 49 4 2 25 0 11 0 544028499 867639296 24294 4294967295 134512640 134569956 3221224400 3221214776 1131166518 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24294 13073 16 0 211810 0
vsize: 847304
[startup+400.028 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30872
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 38907 49 5 2 25 0 11 0 544028499 867639296 24334 4294967295 134512640 134569956 3221224400 3221214816 1131157465 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24334 13073 16 0 211810 0
vsize: 847304
[startup+410.028 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30874
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 39895 50 5 2 25 0 11 0 544028499 867639296 24384 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24384 13073 16 0 211810 0
vsize: 847304
[startup+420.029 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30875
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 40884 50 5 2 25 0 11 0 544028499 867639296 24441 4294967295 134512640 134569956 3221224400 3221214776 1131167320 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24441 13073 16 0 211810 0
vsize: 847304
[startup+430.029 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30877
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 41874 50 5 2 25 0 11 0 544028499 867639296 24483 4294967295 134512640 134569956 3221224400 3221214816 1131157465 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24483 13073 16 0 211810 0
vsize: 847304
[startup+440.029 s]
Raw data (loadavg): 1.00 1.02 0.97 2/64 30879
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 42863 50 5 2 25 0 11 0 544028499 867639296 24534 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24534 13073 16 0 211810 0
vsize: 847304
[startup+450.03 s]
Raw data (loadavg): 1.00 1.01 0.97 2/64 30880
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 43852 51 5 2 25 0 11 0 544028499 867639296 24570 4294967295 134512640 134569956 3221224400 3221214868 1131166483 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24570 13073 16 0 211810 0
vsize: 847304
[startup+460.03 s]
Raw data (loadavg): 1.00 1.01 0.97 2/64 30882
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 44841 51 5 2 25 0 11 0 544028499 867639296 24623 4294967295 134512640 134569956 3221224400 3221214776 1131166863 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24623 13073 16 0 211810 0
vsize: 847304
[startup+470.031 s]
Raw data (loadavg): 1.00 1.01 0.97 2/64 30883
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 45831 51 5 2 25 0 11 0 544028499 867639296 24661 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24661 13073 16 0 211810 0
vsize: 847304
[startup+480.032 s]
Raw data (loadavg): 1.00 1.01 0.97 2/64 30885
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 46821 51 5 2 25 0 11 0 544028499 867639296 24707 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24707 13073 16 0 211810 0
vsize: 847304
[startup+490.032 s]
Raw data (loadavg): 1.00 1.01 0.97 2/64 30886
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 47810 52 5 2 25 0 11 0 544028499 867639296 24744 4294967295 134512640 134569956 3221224400 3221214832 1131479381 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24744 13073 16 0 211810 0
vsize: 847304
[startup+500.033 s]
Raw data (loadavg): 1.00 1.01 0.97 2/64 30888
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 48799 52 5 2 25 0 11 0 544028499 867639296 24790 4294967295 134512640 134569956 3221224400 3221214776 1131166493 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24790 13073 16 0 211810 0
vsize: 847304
[startup+510.033 s]
Raw data (loadavg): 1.00 1.01 0.97 2/64 30890
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 49789 52 5 2 25 0 11 0 544028499 867639296 24834 4294967295 134512640 134569956 3221224400 3221214776 1131167393 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24834 13073 16 0 211810 0
vsize: 847304
[startup+520.033 s]
Raw data (loadavg): 1.00 1.01 0.97 2/64 30891
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 50778 52 5 2 25 0 11 0 544028499 867639296 24875 4294967295 134512640 134569956 3221224400 3221214816 1131157473 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24875 13073 16 0 211810 0
vsize: 847304
[startup+530.034 s]
Raw data (loadavg): 1.00 1.01 0.97 2/64 30892
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 51768 52 5 2 25 0 11 0 544028499 867639296 24920 4294967295 134512640 134569956 3221224400 3221214680 1131487445 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24920 13073 16 0 211810 0
vsize: 847304
[startup+540.033 s]
Raw data (loadavg): 1.00 1.01 0.97 2/64 30894
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 52758 53 5 2 25 0 11 0 544028499 867639296 24959 4294967295 134512640 134569956 3221224400 3221214776 1131167069 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24959 13073 16 0 211810 0
vsize: 847304
[startup+550.034 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30895
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 53748 53 5 2 25 0 11 0 544028499 867639296 24996 4294967295 134512640 134569956 3221224400 3221214872 1131175832 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211826 24996 13073 16 0 211810 0
vsize: 847304
[startup+560.035 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30897
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 54737 53 5 2 25 0 11 0 544028499 867639296 25047 4294967295 134512640 134569956 3221224400 3221214776 1131167002 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25047 13073 16 0 211810 0
vsize: 847304
[startup+570.036 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30898
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 55726 54 6 2 25 0 11 0 544028499 867639296 25077 4294967295 134512640 134569956 3221224400 3221214776 1131167085 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25077 13073 16 0 211810 0
vsize: 847304
[startup+580.036 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30899
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 56715 54 6 2 25 0 11 0 544028499 867639296 25124 4294967295 134512640 134569956 3221224400 3221214776 1131167864 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25124 13073 16 0 211810 0
vsize: 847304
[startup+590.036 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30901
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 57704 55 6 2 25 0 11 0 544028499 867639296 25163 4294967295 134512640 134569956 3221224400 3221214776 1131167761 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25163 13073 16 0 211810 0
vsize: 847304
[startup+600.037 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30902
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 58693 55 6 2 25 0 11 0 544028499 867639296 25197 4294967295 134512640 134569956 3221224400 3221214816 1131157539 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25197 13073 16 0 211810 0
vsize: 847304
[startup+610.037 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30903
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 59682 56 6 2 25 0 11 0 544028499 867639296 25241 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25241 13073 16 0 211810 0
vsize: 847304
[startup+620.038 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30904
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 60672 56 6 2 25 0 11 0 544028499 867639296 25282 4294967295 134512640 134569956 3221224400 3221214872 1131175856 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25282 13073 16 0 211810 0
vsize: 847304
[startup+630.039 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30906
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 61660 56 6 2 25 0 11 0 544028499 867639296 25314 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25314 13073 16 0 211810 0
vsize: 847304
[startup+640.039 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30907
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 62649 57 6 2 25 0 11 0 544028499 867639296 25353 4294967295 134512640 134569956 3221224400 3221214776 1131166831 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25353 13073 16 0 211810 0
vsize: 847304
[startup+650.04 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30908
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 63639 57 6 2 25 0 11 0 544028499 867639296 25394 4294967295 134512640 134569956 3221224400 3221214776 1131167344 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25394 13073 16 0 211810 0
vsize: 847304
[startup+660.041 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30910
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 64628 58 6 2 25 0 11 0 544028499 867639296 25427 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25427 13073 16 0 211810 0
vsize: 847304
[startup+670.041 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30911
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 65618 58 6 2 25 0 11 0 544028499 867639296 25463 4294967295 134512640 134569956 3221224400 3221214776 1131166929 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25463 13073 16 0 211810 0
vsize: 847304
[startup+680.042 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30912
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 66608 58 6 3 25 0 11 0 544028499 867639296 25497 4294967295 134512640 134569956 3221224400 3221214776 1131166501 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25497 13073 16 0 211810 0
vsize: 847304
[startup+690.042 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30913
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 67598 58 6 3 25 0 11 0 544028499 867639296 25540 4294967295 134512640 134569956 3221224400 3221214816 1131157569 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25540 13073 16 0 211810 0
vsize: 847304
[startup+700.043 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30915
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 68589 59 6 3 25 0 11 0 544028499 867639296 25571 4294967295 134512640 134569956 3221224400 3221214776 1131167038 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25571 13073 16 0 211810 0
vsize: 847304
[startup+710.043 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30916
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 69579 59 6 3 25 0 11 0 544028499 867639296 25606 4294967295 134512640 134569956 3221224400 3221214872 1131175712 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25606 13073 16 0 211810 0
vsize: 847304
[startup+720.043 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30917
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 70569 60 6 3 25 0 11 0 544028499 867639296 25642 4294967295 134512640 134569956 3221224400 3221214776 1131167315 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25642 13073 16 0 211810 0
vsize: 847304
[startup+730.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30918
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 71560 60 6 3 25 0 11 0 544028499 867639296 25670 4294967295 134512640 134569956 3221224400 3221214776 1131166863 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25670 13073 16 0 211810 0
vsize: 847304
[startup+740.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30919
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 72549 60 6 3 25 0 11 0 544028499 867639296 25711 4294967295 134512640 134569956 3221224400 3221214816 1131157461 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25711 13073 16 0 211810 0
vsize: 847304
[startup+750.045 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30921
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 73539 61 6 3 25 0 11 0 544028499 867639296 25746 4294967295 134512640 134569956 3221224400 3221214776 1131167426 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25746 13073 16 0 211810 0
vsize: 847304
[startup+760.045 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30922
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 74529 61 6 3 25 0 11 0 544028499 867639296 25786 4294967295 134512640 134569956 3221224400 3221214776 1131167069 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25786 13073 16 0 211810 0
vsize: 847304
[startup+770.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30923
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 75518 62 6 3 25 0 11 0 544028499 867639296 25817 4294967295 134512640 134569956 3221224400 3221214816 1131157623 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25817 13073 16 0 211810 0
vsize: 847304
[startup+780.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30924
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 76509 62 6 3 25 0 11 0 544028499 867639296 25846 4294967295 134512640 134569956 3221224400 3221214848 1131208811 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25846 13073 16 0 211810 0
vsize: 847304
[startup+790.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30925
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 77499 63 6 3 25 0 11 0 544028499 867639296 25889 4294967295 134512640 134569956 3221224400 3221214816 1131157676 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25889 13073 16 0 211810 0
vsize: 847304
[startup+800.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30926
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 78489 63 6 3 25 0 11 0 544028499 867639296 25919 4294967295 134512640 134569956 3221224400 3221214776 1131167079 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25919 13073 16 0 211810 0
vsize: 847304
[startup+810.048 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30928
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 79479 64 6 3 25 0 11 0 544028499 867639296 25959 4294967295 134512640 134569956 3221224400 3221214776 1131167168 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25959 13073 16 0 211810 0
vsize: 847304
[startup+820.048 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30929
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 80470 65 6 3 25 0 11 0 544028499 867639296 25987 4294967295 134512640 134569956 3221224400 3221214776 1131167030 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 25987 13073 16 0 211810 0
vsize: 847304
[startup+830.048 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30930
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 81460 65 6 3 25 0 11 0 544028499 867639296 26017 4294967295 134512640 134569956 3221224400 3221214872 1131175433 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26017 13073 16 0 211810 0
vsize: 847304
[startup+840.049 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30931
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 82451 65 7 3 25 0 11 0 544028499 867639296 26048 4294967295 134512640 134569956 3221224400 3221214776 1131167105 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26048 13073 16 0 211810 0
vsize: 847304
[startup+850.049 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30932
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 83441 66 7 3 25 0 11 0 544028499 867639296 26090 4294967295 134512640 134569956 3221224400 3221214776 1131166865 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26090 13073 16 0 211810 0
vsize: 847304
[startup+860.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30933
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 84431 66 7 3 25 0 11 0 544028499 867639296 26119 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26119 13073 16 0 211810 0
vsize: 847304
[startup+870.058 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30934
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 85423 67 7 3 25 0 11 0 544028499 867639296 26149 4294967295 134512640 134569956 3221224400 3221214872 1131175874 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26149 13073 16 0 211810 0
vsize: 847304
[startup+880.058 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30935
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 86413 67 7 3 25 0 11 0 544028499 867639296 26184 4294967295 134512640 134569956 3221224400 3221214776 1131166811 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26184 13073 16 0 211810 0
vsize: 847304
[startup+890.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30936
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 87403 67 7 3 25 0 11 0 544028499 867639296 26216 4294967295 134512640 134569956 3221224400 3221214848 1131208811 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26216 13073 16 0 211810 0
vsize: 847304
[startup+900.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30938
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 88392 68 7 3 25 0 11 0 544028499 867639296 26248 4294967295 134512640 134569956 3221224400 3221214776 1131167085 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26248 13073 16 0 211810 0
vsize: 847304
[startup+910.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30939
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 89382 68 7 4 25 0 11 0 544028499 867639296 26281 4294967295 134512640 134569956 3221224400 3221214872 1131175445 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26281 13073 16 0 211810 0
vsize: 847304
[startup+920.061 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30940
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 90372 69 7 4 25 0 11 0 544028499 867639296 26310 4294967295 134512640 134569956 3221224400 3221214776 1131166565 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26310 13073 16 0 211810 0
vsize: 847304
[startup+930.062 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30941
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 91359 69 7 4 25 0 11 0 544028499 867639296 26346 4294967295 134512640 134569956 3221224400 3221214776 1131167783 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26346 13073 16 0 211810 0
vsize: 847304
[startup+940.062 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30942
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 92344 70 7 4 25 0 11 0 544028499 867639296 26379 4294967295 134512640 134569956 3221224400 3221214816 1131157465 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26379 13073 16 0 211810 0
vsize: 847304
[startup+950.063 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30943
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 93328 70 7 4 25 0 11 0 544028499 867639296 26428 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26428 13073 16 0 211810 0
vsize: 847304
[startup+960.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30944
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 94312 70 7 4 25 0 11 0 544028499 867639296 26473 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26473 13073 16 0 211810 0
vsize: 847304
[startup+970.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30945
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 95300 71 7 4 25 0 11 0 544028499 867639296 26575 4294967295 134512640 134569956 3221224400 3221214776 1131166571 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26575 13073 16 0 211810 0
vsize: 847304
[startup+980.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30946
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 96290 71 7 4 25 0 11 0 544028499 867639296 26615 4294967295 134512640 134569956 3221224400 3221214776 1131167143 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26615 13073 16 0 211810 0
vsize: 847304
[startup+990.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30947
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 97280 72 7 4 25 0 11 0 544028499 867639296 26644 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26644 13073 16 0 211810 0
vsize: 847304
[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30948
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 98270 72 7 4 25 0 11 0 544028499 867639296 26672 4294967295 134512640 134569956 3221224400 3221214776 1131167414 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26672 13073 16 0 211810 0
vsize: 847304
[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30949
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 99259 72 7 4 25 0 11 0 544028499 867639296 26708 4294967295 134512640 134569956 3221224400 3221214776 1131166863 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26708 13073 16 0 211810 0
vsize: 847304
[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30950
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 100250 73 7 4 25 0 11 0 544028499 867639296 26740 4294967295 134512640 134569956 3221224400 3221214776 1131166848 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26740 13073 16 0 211810 0
vsize: 847304
[startup+1030.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30951
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 101240 73 7 4 25 0 11 0 544028499 867639296 26775 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26775 13073 16 0 211810 0
vsize: 847304
[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30952
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 102230 73 7 4 25 0 11 0 544028499 867639296 26804 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26804 13073 16 0 211810 0
vsize: 847304
[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30953
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 103221 73 7 4 25 0 11 0 544028499 867639296 26835 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26835 13073 16 0 211810 0
vsize: 847304
[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30954
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 104211 74 7 4 25 0 11 0 544028499 867639296 26864 4294967295 134512640 134569956 3221224400 3221214816 1131157451 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26864 13073 16 0 211810 0
vsize: 847304
[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30955
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 105201 74 7 4 25 0 11 0 544028499 867639296 26892 4294967295 134512640 134569956 3221224400 3221214776 1131166571 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26892 13073 16 0 211810 0
vsize: 847304
[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30956
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 106192 74 7 4 25 0 11 0 544028499 867639296 26920 4294967295 134512640 134569956 3221224400 3221214816 1131157490 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26920 13073 16 0 211810 0
vsize: 847304
[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30957
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 107182 75 7 4 25 0 11 0 544028499 867639296 26948 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26948 13073 16 0 211810 0
vsize: 847304
[startup+1100.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30958
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 108172 75 7 4 25 0 11 0 544028499 867639296 26977 4294967295 134512640 134569956 3221224400 3221214776 1131166591 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 26977 13073 16 0 211810 0
vsize: 847304
[startup+1110.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30959
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 109161 76 7 4 25 0 11 0 544028499 867639296 27005 4294967295 134512640 134569956 3221224400 3221214776 1131166518 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27005 13073 16 0 211810 0
vsize: 847304
[startup+1120.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30960
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 110150 77 7 4 25 0 11 0 544028499 867639296 27033 4294967295 134512640 134569956 3221224400 3221214776 1131166579 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27033 13073 16 0 211810 0
vsize: 847304
[startup+1130.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30961
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 111140 77 7 4 25 0 11 0 544028499 867639296 27043 4294967295 134512640 134569956 3221224400 3221214816 1131579402 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27043 13073 16 0 211810 0
vsize: 847304
[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30962
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 112128 77 7 4 25 0 11 0 544028499 867639296 27096 4294967295 134512640 134569956 3221224400 3221214868 1131166476 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27096 13073 16 0 211810 0
vsize: 847304
[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30963
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 113117 78 8 4 25 0 11 0 544028499 867639296 27119 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27119 13073 16 0 211810 0
vsize: 847304
[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30964
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 114106 78 8 4 25 0 11 0 544028499 867639296 27171 4294967295 134512640 134569956 3221224400 3221214776 1131166571 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27171 13073 16 0 211810 0
vsize: 847304
[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30965
Raw data (stat): 30739 (java) S 30738 26298 26297 0 -1 0 18127 4 1 0 115095 79 8 4 25 0 11 0 544028499 867639296 27200 4294967295 134512640 134569956 3221224400 3221213480 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27200 13073 16 0 211810 0
vsize: 847304
[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30966
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 116084 79 8 4 25 0 11 0 544028499 867639296 27251 4294967295 134512640 134569956 3221224400 3221214816 1131157623 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27251 13073 16 0 211810 0
vsize: 847304
[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30967
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 117072 80 8 4 19 0 11 0 544028499 867639296 27309 4294967295 134512640 134569956 3221224400 3221214776 1131166568 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27309 13073 16 0 211810 0
vsize: 847304
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30968
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 118058 80 8 4 25 0 11 0 544028499 867639296 27337 4294967295 134512640 134569956 3221224400 3221214776 1131166913 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27337 13073 16 0 211810 0
vsize: 847304
[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30969
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 119044 80 8 4 25 0 11 0 544028499 867639296 27389 4294967295 134512640 134569956 3221224400 3221214816 1131157440 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27389 13073 16 0 211810 0
vsize: 847304
[startup+1220.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/64 30970
Raw data (stat): 30739 (java) R 30738 26298 26297 0 -1 0 18127 4 1 0 120033 81 8 4 25 0 11 0 544028499 867639296 27502 4294967295 134512640 134569956 3221224400 3221214872 1131175771 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211826 27502 13073 16 0 211810 0
vsize: 847304
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1220.19 s]
Raw data (loadavg): 1.00 1.00 0.97 1/54 30972
Raw data (stat): 30739 (java) Z 30738 26298 26297 0 -1 1036 18127 5755 1 0 120038 81 1349 34 25 0 1 0 544028499 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.19
CPU time (s): 1215.03
CPU user time (s): 1213.88
CPU system time (s): 1.15482
CPU usage (%): 99.5772
Max. virtual memory (Kb): 851440
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####