PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb
MD5SUM	4f5f6e30a602f3968daa9ca41c7da043
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2058
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	9334
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1024
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	9334
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05284
Number of variables	133
Total number of constraints	126
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	56
Number of constraints which are nor clauses,nor cardinality constraints	70
Minimum length of a constraint	1
Maximum length of a constraint	81
Trace number 14631

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        697488 kB
Buffers:         26904 kB
Cached:         288208 kB
SwapCached:          0 kB
Active:          46816 kB
Inactive:       270808 kB
HighTotal:      131008 kB
HighFree:        63644 kB
LowTotal:       903652 kB
LowFree:        633844 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13956 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 00:46:31 (client local time) WITH STATUS 143 IN 1256.53 SECONDS
stats: 19717 7 1256.53 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-neos5.opb
c reading problem 
c [nbvar=133]
c [nbconstr=126]
c time 1.414
c #vars     133
c #clauses  73
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=3072
c Current CPU time (ms) : 2.006
c starts	: 1
c conflicts	: 2
c decisions	: 90
c propagations	: 155
c inspects	: 430
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 1
c 
c CURRENT OPTIMUM=3071
c Current CPU time (ms) : 2.071
c starts	: 2
c conflicts	: 2
c decisions	: 120
c propagations	: 288
c inspects	: 775
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 2
c 
c CURRENT OPTIMUM=3070
c Current CPU time (ms) : 2.144
c starts	: 3
c conflicts	: 2
c decisions	: 149
c propagations	: 421
c inspects	: 819
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 3
c 
c CURRENT OPTIMUM=3069
c Current CPU time (ms) : 2.231
c starts	: 4
c conflicts	: 2
c decisions	: 178
c propagations	: 554
c inspects	: 871
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 4
c 
c CURRENT OPTIMUM=3068
c Current CPU time (ms) : 2.297
c starts	: 5
c conflicts	: 2
c decisions	: 206
c propagations	: 687
c inspects	: 923
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 5
c 
c CURRENT OPTIMUM=3067
c Current CPU time (ms) : 2.412
c starts	: 6
c conflicts	: 2
c decisions	: 235
c propagations	: 820
c inspects	: 988
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 6
c 
c CURRENT OPTIMUM=3066
c Current CPU time (ms) : 2.488
c starts	: 7
c conflicts	: 2
c decisions	: 263
c propagations	: 953
c inspects	: 1052
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 7
c 
c CURRENT OPTIMUM=3065
c Current CPU time (ms) : 2.572
c starts	: 8
c conflicts	: 2
c decisions	: 291
c propagations	: 1086
c inspects	: 1122
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 8
c 
c CURRENT OPTIMUM=3064
c Current CPU time (ms) : 2.821
c starts	: 9
c conflicts	: 2
c decisions	: 318
c propagations	: 1219
c inspects	: 1189
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 9
c 
c CURRENT OPTIMUM=3063
c Current CPU time (ms) : 3.334
c starts	: 10
c conflicts	: 2
c decisions	: 347
c propagations	: 1352
c inspects	: 1282
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 10
c 
c CURRENT OPTIMUM=3062
c Current CPU time (ms) : 3.478
c starts	: 11
c conflicts	: 2
c decisions	: 375
c propagations	: 1485
c inspects	: 1370
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 11
c 
c CURRENT OPTIMUM=3061
c Current CPU time (ms) : 3.612
c starts	: 12
c conflicts	: 2
c decisions	: 403
c propagations	: 1618
c inspects	: 1464
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 12
c 
c CURRENT OPTIMUM=3060
c Current CPU time (ms) : 3.717
c starts	: 13
c conflicts	: 2
c decisions	: 430
c propagations	: 1751
c inspects	: 1551
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 13
c 
c CURRENT OPTIMUM=3059
c Current CPU time (ms) : 3.846
c starts	: 14
c conflicts	: 2
c decisions	: 458
c propagations	: 1884
c inspects	: 1657
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 14
c 
c CURRENT OPTIMUM=3058
c Current CPU time (ms) : 3.963
c starts	: 15
c conflicts	: 2
c decisions	: 485
c propagations	: 2017
c inspects	: 1754
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 15
c 
c CURRENT OPTIMUM=3057
c Current CPU time (ms) : 4.193
c starts	: 16
c conflicts	: 2
c decisions	: 512
c propagations	: 2150
c inspects	: 1856
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 16
c 
c CURRENT OPTIMUM=3056
c Current CPU time (ms) : 4.302
c starts	: 17
c conflicts	: 2
c decisions	: 538
c propagations	: 2283
c inspects	: 1946
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 17
c 
c CURRENT OPTIMUM=3055
c Current CPU time (ms) : 4.484
c starts	: 18
c conflicts	: 2
c decisions	: 567
c propagations	: 2416
c inspects	: 2095
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 18
c 
c CURRENT OPTIMUM=3054
c Current CPU time (ms) : 4.652
c starts	: 19
c conflicts	: 2
c decisions	: 595
c propagations	: 2549
c inspects	: 2231
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 19
c 
c CURRENT OPTIMUM=3053
c Current CPU time (ms) : 4.878
c starts	: 20
c conflicts	: 2
c decisions	: 623
c propagations	: 2682
c inspects	: 2373
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 20
c 
c CURRENT OPTIMUM=3052
c Current CPU time (ms) : 5.051
c starts	: 21
c conflicts	: 2
c decisions	: 650
c propagations	: 2815
c inspects	: 2500
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 21
c 
c CURRENT OPTIMUM=3051
c Current CPU time (ms) : 5.24
c starts	: 22
c conflicts	: 2
c decisions	: 678
c propagations	: 2948
c inspects	: 2654
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 22
c 
c CURRENT OPTIMUM=3050
c Current CPU time (ms) : 5.402
c starts	: 23
c conflicts	: 2
c decisions	: 705
c propagations	: 3081
c inspects	: 2791
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 23
c 
c CURRENT OPTIMUM=3049
c Current CPU time (ms) : 5.485
c starts	: 24
c conflicts	: 2
c decisions	: 732
c propagations	: 3214
c inspects	: 2933
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 24
c 
c CURRENT OPTIMUM=3048
c Current CPU time (ms) : 5.557
c starts	: 25
c conflicts	: 2
c decisions	: 758
c propagations	: 3347
c inspects	: 3055
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 25
c 
c CURRENT OPTIMUM=3047
c Current CPU time (ms) : 5.737
c starts	: 26
c conflicts	: 2
c decisions	: 786
c propagations	: 3480
c inspects	: 3233
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 26
c 
c CURRENT OPTIMUM=3046
c Current CPU time (ms) : 5.852
c starts	: 27
c conflicts	: 2
c decisions	: 813
c propagations	: 3613
c inspects	: 3390
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 27
c 
c CURRENT OPTIMUM=3045
c Current CPU time (ms) : 5.922
c starts	: 28
c conflicts	: 2
c decisions	: 840
c propagations	: 3746
c inspects	: 3552
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 28
c 
c CURRENT OPTIMUM=3044
c Current CPU time (ms) : 5.983
c starts	: 29
c conflicts	: 2
c decisions	: 866
c propagations	: 3879
c inspects	: 3690
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 29
c 
c CURRENT OPTIMUM=3043
c Current CPU time (ms) : 6.058
c starts	: 30
c conflicts	: 2
c decisions	: 893
c propagations	: 4012
c inspects	: 3862
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 30
c 
c CURRENT OPTIMUM=3042
c Current CPU time (ms) : 6.122
c starts	: 31
c conflicts	: 2
c decisions	: 919
c propagations	: 4145
c inspects	: 4008
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 31
c 
c CURRENT OPTIMUM=3041
c Current CPU time (ms) : 6.188
c starts	: 32
c conflicts	: 2
c decisions	: 945
c propagations	: 4278
c inspects	: 4158
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 32
c 
c CURRENT OPTIMUM=3040
c Current CPU time (ms) : 6.243
c starts	: 33
c conflicts	: 2
c decisions	: 970
c propagations	: 4411
c inspects	: 4279
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 33
c 
c CURRENT OPTIMUM=3039
c Current CPU time (ms) : 6.354
c starts	: 34
c conflicts	: 2
c decisions	: 999
c propagations	: 4544
c inspects	: 4540
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 34
c 
c CURRENT OPTIMUM=3038
c Current CPU time (ms) : 6.459
c starts	: 35
c conflicts	: 2
c decisions	: 1027
c propagations	: 4677
c inspects	: 4772
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 35
c 
c CURRENT OPTIMUM=3037
c Current CPU time (ms) : 6.56
c starts	: 36
c conflicts	: 2
c decisions	: 1055
c propagations	: 4810
c inspects	: 5010
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 36
c 
c CURRENT OPTIMUM=3036
c Current CPU time (ms) : 6.661
c starts	: 37
c conflicts	: 2
c decisions	: 1082
c propagations	: 4943
c inspects	: 5217
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 37
c 
c CURRENT OPTIMUM=3035
c Current CPU time (ms) : 6.823
c starts	: 38
c conflicts	: 2
c decisions	: 1110
c propagations	: 5076
c inspects	: 5467
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 38
c 
c CURRENT OPTIMUM=3034
c Current CPU time (ms) : 6.919
c starts	: 39
c conflicts	: 2
c decisions	: 1137
c propagations	: 5209
c inspects	: 5684
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 39
c 
c CURRENT OPTIMUM=3033
c Current CPU time (ms) : 7.045
c starts	: 40
c conflicts	: 2
c decisions	: 1164
c propagations	: 5342
c inspects	: 5906
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 40
c 
c CURRENT OPTIMUM=3032
c Current CPU time (ms) : 7.277
c starts	: 41
c conflicts	: 2
c decisions	: 1190
c propagations	: 5475
c inspects	: 6092
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 41
c 
c CURRENT OPTIMUM=3031
c Current CPU time (ms) : 7.53
c starts	: 42
c conflicts	: 2
c decisions	: 1218
c propagations	: 5608
c inspects	: 6366
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 42
c 
c CURRENT OPTIMUM=3030
c Current CPU time (ms) : 7.706
c starts	: 43
c conflicts	: 2
c decisions	: 1245
c propagations	: 5741
c inspects	: 6603
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 43
c 
c CURRENT OPTIMUM=3029
c Current CPU time (ms) : 7.824
c starts	: 44
c conflicts	: 2
c decisions	: 1272
c propagations	: 5874
c inspects	: 6845
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 44
c 
c CURRENT OPTIMUM=3028
c Current CPU time (ms) : 7.909
c starts	: 45
c conflicts	: 2
c decisions	: 1298
c propagations	: 6007
c inspects	: 7047
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 45
c 
c CURRENT OPTIMUM=3027
c Current CPU time (ms) : 8.014
c starts	: 46
c conflicts	: 2
c decisions	: 1325
c propagations	: 6140
c inspects	: 7299
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 46
c 
c CURRENT OPTIMUM=3026
c Current CPU time (ms) : 8.101
c starts	: 47
c conflicts	: 2
c decisions	: 1351
c propagations	: 6273
c inspects	: 7509
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 47
c 
c CURRENT OPTIMUM=3025
c Current CPU time (ms) : 8.193
c starts	: 48
c conflicts	: 2
c decisions	: 1377
c propagations	: 6406
c inspects	: 7723
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 48
c 
c CURRENT OPTIMUM=3024
c Current CPU time (ms) : 8.263
c starts	: 49
c conflicts	: 2
c decisions	: 1402
c propagations	: 6539
c inspects	: 7892
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 49
c 
c CURRENT OPTIMUM=3023
c Current CPU time (ms) : 8.427
c starts	: 50
c conflicts	: 2
c decisions	: 1430
c propagations	: 6672
c inspects	: 8214
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 50
c 
c CURRENT OPTIMUM=3022
c Current CPU time (ms) : 8.541
c starts	: 51
c conflicts	: 2
c decisions	: 1457
c propagations	: 6805
c inspects	: 8491
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 51
c 
c CURRENT OPTIMUM=3021
c Current CPU time (ms) : 8.657
c starts	: 52
c conflicts	: 2
c decisions	: 1484
c propagations	: 6938
c inspects	: 8773
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 52
c 
c CURRENT OPTIMUM=3020
c Current CPU time (ms) : 8.753
c starts	: 53
c conflicts	: 2
c decisions	: 1510
c propagations	: 7071
c inspects	: 9007
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 53
c 
c CURRENT OPTIMUM=3019
c Current CPU time (ms) : 8.873
c starts	: 54
c conflicts	: 2
c decisions	: 1537
c propagations	: 7204
c inspects	: 9299
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 54
c 
c CURRENT OPTIMUM=3018
c Current CPU time (ms) : 8.976
c starts	: 55
c conflicts	: 2
c decisions	: 1563
c propagations	: 7337
c inspects	: 9541
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 55
c 
c CURRENT OPTIMUM=3017
c Current CPU time (ms) : 9.076
c starts	: 56
c conflicts	: 2
c decisions	: 1589
c propagations	: 7470
c inspects	: 9787
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 56
c 
c CURRENT OPTIMUM=3016
c Current CPU time (ms) : 9.156
c starts	: 57
c conflicts	: 2
c decisions	: 1614
c propagations	: 7603
c inspects	: 9980
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 57
c 
c CURRENT OPTIMUM=3015
c Current CPU time (ms) : 9.283
c starts	: 58
c conflicts	: 2
c decisions	: 1641
c propagations	: 7736
c inspects	: 10292
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 58
c 
c CURRENT OPTIMUM=3014
c Current CPU time (ms) : 9.388
c starts	: 59
c conflicts	: 2
c decisions	: 1667
c propagations	: 7869
c inspects	: 10550
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 59
c 
c CURRENT OPTIMUM=3013
c Current CPU time (ms) : 9.526
c starts	: 60
c conflicts	: 2
c decisions	: 1693
c propagations	: 8002
c inspects	: 10812
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 60
c 
c CURRENT OPTIMUM=3012
c Current CPU time (ms) : 9.614
c starts	: 61
c conflicts	: 2
c decisions	: 1718
c propagations	: 8135
c inspects	: 11017
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 61
c 
c CURRENT OPTIMUM=3011
c Current CPU time (ms) : 9.725
c starts	: 62
c conflicts	: 2
c decisions	: 1744
c propagations	: 8268
c inspects	: 11287
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 62
c 
c CURRENT OPTIMUM=3010
c Current CPU time (ms) : 9.812
c starts	: 63
c conflicts	: 2
c decisions	: 1769
c propagations	: 8401
c inspects	: 11498
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 63
c 
c CURRENT OPTIMUM=3009
c Current CPU time (ms) : 9.901
c starts	: 64
c conflicts	: 2
c decisions	: 1794
c propagations	: 8534
c inspects	: 11712
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 64
c 
c CURRENT OPTIMUM=3008
c Current CPU time (ms) : 9.965
c starts	: 65
c conflicts	: 2
c decisions	: 1818
c propagations	: 8667
c inspects	: 11864
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 65
c 
c CURRENT OPTIMUM=3007
c Current CPU time (ms) : 10.165
c starts	: 66
c conflicts	: 2
c decisions	: 1847
c propagations	: 8800
c inspects	: 12349
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 66
c 
c CURRENT OPTIMUM=3006
c Current CPU time (ms) : 10.333
c starts	: 67
c conflicts	: 2
c decisions	: 1875
c propagations	: 8933
c inspects	: 12773
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 67
c 
c CURRENT OPTIMUM=3005
c Current CPU time (ms) : 10.536
c starts	: 68
c conflicts	: 2
c decisions	: 1903
c propagations	: 9066
c inspects	: 13203
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 68
c 
c CURRENT OPTIMUM=3004
c Current CPU time (ms) : 10.683
c starts	: 69
c conflicts	: 2
c decisions	: 1930
c propagations	: 9199
c inspects	: 13570
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 69
c 
c CURRENT OPTIMUM=3003
c Current CPU time (ms) : 10.862
c starts	: 70
c conflicts	: 2
c decisions	: 1958
c propagations	: 9332
c inspects	: 14012
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 70
c 
c CURRENT OPTIMUM=3002
c Current CPU time (ms) : 11.015
c starts	: 71
c conflicts	: 2
c decisions	: 1985
c propagations	: 9465
c inspects	: 14389
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 71
c 
c CURRENT OPTIMUM=3001
c Current CPU time (ms) : 11.17
c starts	: 72
c conflicts	: 2
c decisions	: 2012
c propagations	: 9598
c inspects	: 14771
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 72
c 
c CURRENT OPTIMUM=3000
c Current CPU time (ms) : 11.297
c starts	: 73
c conflicts	: 2
c decisions	: 2038
c propagations	: 9731
c inspects	: 15085
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 73
c 
c CURRENT OPTIMUM=2999
c Current CPU time (ms) : 11.518
c starts	: 74
c conflicts	: 2
c decisions	: 2066
c propagations	: 9864
c inspects	: 15551
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 74
c 
c CURRENT OPTIMUM=2998
c Current CPU time (ms) : 11.678
c starts	: 75
c conflicts	: 2
c decisions	: 2093
c propagations	: 9997
c inspects	: 15948
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 75
c 
c CURRENT OPTIMUM=2997
c Current CPU time (ms) : 11.854
c starts	: 76
c conflicts	: 2
c decisions	: 2120
c propagations	: 10130
c inspects	: 16350
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 76
c 
c CURRENT OPTIMUM=2996
c Current CPU time (ms) : 11.986
c starts	: 77
c conflicts	: 2
c decisions	: 2146
c propagations	: 10263
c inspects	: 16680
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 77
c 
c CURRENT OPTIMUM=2995
c Current CPU time (ms) : 12.15
c starts	: 78
c conflicts	: 2
c decisions	: 2173
c propagations	: 10396
c inspects	: 17092
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 78
c 
c CURRENT OPTIMUM=2994
c Current CPU time (ms) : 12.285
c starts	: 79
c conflicts	: 2
c decisions	: 2199
c propagations	: 10529
c inspects	: 17430
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 79
c 
c CURRENT OPTIMUM=2993
c Current CPU time (ms) : 12.456
c starts	: 80
c conflicts	: 2
c decisions	: 2225
c propagations	: 10662
c inspects	: 17772
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 80
c 
c CURRENT OPTIMUM=2992
c Current CPU time (ms) : 12.566
c starts	: 81
c conflicts	: 2
c decisions	: 2250
c propagations	: 10795
c inspects	: 18037
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 81
c 
c CURRENT OPTIMUM=2991
c Current CPU time (ms) : 12.77
c starts	: 82
c conflicts	: 2
c decisions	: 2278
c propagations	: 10928
c inspects	: 18551
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 82
c 
c CURRENT OPTIMUM=2990
c Current CPU time (ms) : 12.944
c starts	: 83
c conflicts	: 2
c decisions	: 2305
c propagations	: 11061
c inspects	: 18988
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 83
c 
c CURRENT OPTIMUM=2989
c Current CPU time (ms) : 13.121
c starts	: 84
c conflicts	: 2
c decisions	: 2332
c propagations	: 11194
c inspects	: 19430
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 84
c 
c CURRENT OPTIMUM=2988
c Current CPU time (ms) : 13.265
c starts	: 85
c conflicts	: 2
c decisions	: 2358
c propagations	: 11327
c inspects	: 19792
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 85
c 
c CURRENT OPTIMUM=2987
c Current CPU time (ms) : 13.487
c starts	: 86
c conflicts	: 2
c decisions	: 2385
c propagations	: 11460
c inspects	: 20244
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 86
c 
c CURRENT OPTIMUM=2986
c Current CPU time (ms) : 13.638
c starts	: 87
c conflicts	: 2
c decisions	: 2411
c propagations	: 11593
c inspects	: 20614
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 87
c 
c CURRENT OPTIMUM=2985
c Current CPU time (ms) : 13.789
c starts	: 88
c conflicts	: 2
c decisions	: 2437
c propagations	: 11726
c inspects	: 20988
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 88
c 
c CURRENT OPTIMUM=2984
c Current CPU time (ms) : 13.907
c starts	: 89
c conflicts	: 2
c decisions	: 2462
c propagations	: 11859
c inspects	: 21277
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 89
c 
c CURRENT OPTIMUM=2983
c Current CPU time (ms) : 14.097
c starts	: 90
c conflicts	: 2
c decisions	: 2489
c propagations	: 11992
c inspects	: 21749
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 90
c 
c CURRENT OPTIMUM=2982
c Current CPU time (ms) : 14.252
c starts	: 91
c conflicts	: 2
c decisions	: 2515
c propagations	: 12125
c inspects	: 22135
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 91
c 
c CURRENT OPTIMUM=2981
c Current CPU time (ms) : 14.446
c starts	: 92
c conflicts	: 2
c decisions	: 2541
c propagations	: 12258
c inspects	: 22525
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 92
c 
c CURRENT OPTIMUM=2980
c Current CPU time (ms) : 14.567
c starts	: 93
c conflicts	: 2
c decisions	: 2566
c propagations	: 12391
c inspects	: 22826
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 93
c 
c CURRENT OPTIMUM=2979
c Current CPU time (ms) : 14.726
c starts	: 94
c conflicts	: 2
c decisions	: 2592
c propagations	: 12524
c inspects	: 23224
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 94
c 
c CURRENT OPTIMUM=2978
c Current CPU time (ms) : 14.85
c starts	: 95
c conflicts	: 2
c decisions	: 2617
c propagations	: 12657
c inspects	: 23531
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 95
c 
c CURRENT OPTIMUM=2977
c Current CPU time (ms) : 14.974
c starts	: 96
c conflicts	: 2
c decisions	: 2642
c propagations	: 12790
c inspects	: 23841
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 96
c 
c CURRENT OPTIMUM=2976
c Current CPU time (ms) : 15.062
c starts	: 97
c conflicts	: 2
c decisions	: 2666
c propagations	: 12923
c inspects	: 24057
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 97
c 
c CURRENT OPTIMUM=2975
c Current CPU time (ms) : 15.342
c starts	: 98
c conflicts	: 2
c decisions	: 2694
c propagations	: 13056
c inspects	: 24667
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 98
c 
c CURRENT OPTIMUM=2974
c Current CPU time (ms) : 15.548
c starts	: 99
c conflicts	: 2
c decisions	: 2721
c propagations	: 13189
c inspects	: 25184
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 99
c 
c CURRENT OPTIMUM=2973
c Current CPU time (ms) : 15.756
c starts	: 100
c conflicts	: 2
c decisions	: 2748
c propagations	: 13322
c inspects	: 25706
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 100
c 
c CURRENT OPTIMUM=2972
c Current CPU time (ms) : 15.926
c starts	: 101
c conflicts	: 2
c decisions	: 2774
c propagations	: 13455
c inspects	: 26132
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 101
c 
c CURRENT OPTIMUM=2971
c Current CPU time (ms) : 16.137
c starts	: 102
c conflicts	: 2
c decisions	: 2801
c propagations	: 13588
c inspects	: 26664
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 102
c 
c CURRENT OPTIMUM=2970
c Current CPU time (ms) : 16.35
c starts	: 103
c conflicts	: 2
c decisions	: 2827
c propagations	: 13721
c inspects	: 27098
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 103
c 
c CURRENT OPTIMUM=2969
c Current CPU time (ms) : 16.525
c starts	: 104
c conflicts	: 2
c decisions	: 2853
c propagations	: 13854
c inspects	: 27536
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 104
c 
c CURRENT OPTIMUM=2968
c Current CPU time (ms) : 16.66
c starts	: 105
c conflicts	: 2
c decisions	: 2878
c propagations	: 13987
c inspects	: 27873
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 105
c 
c CURRENT OPTIMUM=2967
c Current CPU time (ms) : 16.881
c starts	: 106
c conflicts	: 2
c decisions	: 2905
c propagations	: 14120
c inspects	: 28425
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 106
c 
c CURRENT OPTIMUM=2966
c Current CPU time (ms) : 17.06
c starts	: 107
c conflicts	: 2
c decisions	: 2931
c propagations	: 14253
c inspects	: 28875
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 107
c 
c CURRENT OPTIMUM=2965
c Current CPU time (ms) : 17.282
c starts	: 108
c conflicts	: 2
c decisions	: 2957
c propagations	: 14386
c inspects	: 29329
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 108
c 
c CURRENT OPTIMUM=2964
c Current CPU time (ms) : 17.423
c starts	: 109
c conflicts	: 2
c decisions	: 2982
c propagations	: 14519
c inspects	: 29678
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 109
c 
c CURRENT OPTIMUM=2963
c Current CPU time (ms) : 17.611
c starts	: 110
c conflicts	: 2
c decisions	: 3008
c propagations	: 14652
c inspects	: 30140
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 110
c 
c CURRENT OPTIMUM=2962
c Current CPU time (ms) : 17.756
c starts	: 111
c conflicts	: 2
c decisions	: 3033
c propagations	: 14785
c inspects	: 30495
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 111
c 
c CURRENT OPTIMUM=2961
c Current CPU time (ms) : 17.903
c starts	: 112
c conflicts	: 2
c decisions	: 3058
c propagations	: 14918
c inspects	: 30853
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 112
c 
c CURRENT OPTIMUM=2960
c Current CPU time (ms) : 18.004
c starts	: 113
c conflicts	: 2
c decisions	: 3082
c propagations	: 15051
c inspects	: 31101
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 113
c 
c CURRENT OPTIMUM=2959
c Current CPU time (ms) : 18.284
c starts	: 114
c conflicts	: 2
c decisions	: 3109
c propagations	: 15184
c inspects	: 31693
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 114
c 
c CURRENT OPTIMUM=2958
c Current CPU time (ms) : 18.479
c starts	: 115
c conflicts	: 2
c decisions	: 3135
c propagations	: 15317
c inspects	: 32175
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 115
c 
c CURRENT OPTIMUM=2957
c Current CPU time (ms) : 18.674
c starts	: 116
c conflicts	: 2
c decisions	: 3161
c propagations	: 15450
c inspects	: 32661
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 116
c 
c CURRENT OPTIMUM=2956
c Current CPU time (ms) : 18.824
c starts	: 117
c conflicts	: 2
c decisions	: 3186
c propagations	: 15583
c inspects	: 33034
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 117
c 
c CURRENT OPTIMUM=2955
c Current CPU time (ms) : 19.021
c starts	: 118
c conflicts	: 2
c decisions	: 3212
c propagations	: 15716
c inspects	: 33528
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 118
c 
c CURRENT OPTIMUM=2954
c Current CPU time (ms) : 19.215
c starts	: 119
c conflicts	: 2
c decisions	: 3237
c propagations	: 15849
c inspects	: 33907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 119
c 
c CURRENT OPTIMUM=2953
c Current CPU time (ms) : 19.37
c starts	: 120
c conflicts	: 2
c decisions	: 3262
c propagations	: 15982
c inspects	: 34289
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 120
c 
c CURRENT OPTIMUM=2952
c Current CPU time (ms) : 19.477
c starts	: 121
c conflicts	: 2
c decisions	: 3286
c propagations	: 16115
c inspects	: 34553
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 121
c 
c CURRENT OPTIMUM=2951
c Current CPU time (ms) : 19.681
c starts	: 122
c conflicts	: 2
c decisions	: 3312
c propagations	: 16248
c inspects	: 35063
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 122
c 
c CURRENT OPTIMUM=2950
c Current CPU time (ms) : 19.838
c starts	: 123
c conflicts	: 2
c decisions	: 3337
c propagations	: 16381
c inspects	: 35454
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 123
c 
c CURRENT OPTIMUM=2949
c Current CPU time (ms) : 19.995
c starts	: 124
c conflicts	: 2
c decisions	: 3362
c propagations	: 16514
c inspects	: 35848
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 124
c 
c CURRENT OPTIMUM=2948
c Current CPU time (ms) : 20.105
c starts	: 125
c conflicts	: 2
c decisions	: 3386
c propagations	: 16647
c inspects	: 36120
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 125
c 
c CURRENT OPTIMUM=2947
c Current CPU time (ms) : 20.311
c starts	: 126
c conflicts	: 2
c decisions	: 3411
c propagations	: 16780
c inspects	: 36520
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 126
c 
c CURRENT OPTIMUM=2946
c Current CPU time (ms) : 20.424
c starts	: 127
c conflicts	: 2
c decisions	: 3435
c propagations	: 16913
c inspects	: 36796
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 127
c 
c CURRENT OPTIMUM=2945
c Current CPU time (ms) : 20.54
c starts	: 128
c conflicts	: 2
c decisions	: 3459
c propagations	: 17046
c inspects	: 37074
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 128
c 
c CURRENT OPTIMUM=2944
c Current CPU time (ms) : 20.602
c starts	: 129
c conflicts	: 2
c decisions	: 3482
c propagations	: 17179
c inspects	: 37225
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 129
c 
c CURRENT OPTIMUM=2943
c Current CPU time (ms) : 20.928
c starts	: 130
c conflicts	: 2
c decisions	: 3511
c propagations	: 17312
c inspects	: 38168
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 130
c 
c CURRENT OPTIMUM=2942
c Current CPU time (ms) : 21.246
c starts	: 131
c conflicts	: 2
c decisions	: 3539
c propagations	: 17445
c inspects	: 38856
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 131
c 
c CURRENT OPTIMUM=2941
c Current CPU time (ms) : 21.52
c starts	: 132
c conflicts	: 2
c decisions	: 3567
c propagations	: 17578
c inspects	: 39551
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 132
c 
c CURRENT OPTIMUM=2940
c Current CPU time (ms) : 21.75
c starts	: 133
c conflicts	: 2
c decisions	: 3594
c propagations	: 17711
c inspects	: 40122
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 133
c 
c CURRENT OPTIMUM=2939
c Current CPU time (ms) : 22.031
c starts	: 134
c conflicts	: 2
c decisions	: 3622
c propagations	: 17844
c inspects	: 40833
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 134
c 
c CURRENT OPTIMUM=2938
c Current CPU time (ms) : 22.311
c starts	: 135
c conflicts	: 2
c decisions	: 3649
c propagations	: 17977
c inspects	: 41415
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 135
c 
c CURRENT OPTIMUM=2937
c Current CPU time (ms) : 22.545
c starts	: 136
c conflicts	: 2
c decisions	: 3676
c propagations	: 18110
c inspects	: 42004
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 136
c 
c CURRENT OPTIMUM=2936
c Current CPU time (ms) : 22.729
c starts	: 137
c conflicts	: 2
c decisions	: 3702
c propagations	: 18243
c inspects	: 42468
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 137
c 
c CURRENT OPTIMUM=2935
c Current CPU time (ms) : 23.013
c starts	: 138
c conflicts	: 2
c decisions	: 3730
c propagations	: 18376
c inspects	: 43207
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 138
c 
c CURRENT OPTIMUM=2934
c Current CPU time (ms) : 23.299
c starts	: 139
c conflicts	: 2
c decisions	: 3757
c propagations	: 18509
c inspects	: 43806
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 139
c 
c CURRENT OPTIMUM=2933
c Current CPU time (ms) : 23.538
c starts	: 140
c conflicts	: 2
c decisions	: 3784
c propagations	: 18642
c inspects	: 44412
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 140
c 
c CURRENT OPTIMUM=2932
c Current CPU time (ms) : 23.729
c starts	: 141
c conflicts	: 2
c decisions	: 3810
c propagations	: 18775
c inspects	: 44893
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 141
c 
c CURRENT OPTIMUM=2931
c Current CPU time (ms) : 23.97
c starts	: 142
c conflicts	: 2
c decisions	: 3837
c propagations	: 18908
c inspects	: 45512
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 142
c 
c CURRENT OPTIMUM=2930
c Current CPU time (ms) : 24.213
c starts	: 143
c conflicts	: 2
c decisions	: 3863
c propagations	: 19041
c inspects	: 46001
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 143
c 
c CURRENT OPTIMUM=2929
c Current CPU time (ms) : 24.409
c starts	: 144
c conflicts	: 2
c decisions	: 3889
c propagations	: 19174
c inspects	: 46496
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 144
c 
c CURRENT OPTIMUM=2928
c Current CPU time (ms) : 24.556
c starts	: 145
c conflicts	: 2
c decisions	: 3914
c propagations	: 19307
c inspects	: 46865
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 145
c 
c CURRENT OPTIMUM=2927
c Current CPU time (ms) : 24.854
c starts	: 146
c conflicts	: 2
c decisions	: 3942
c propagations	: 19440
c inspects	: 47652
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 146
c 
c CURRENT OPTIMUM=2926
c Current CPU time (ms) : 25.149
c starts	: 147
c conflicts	: 2
c decisions	: 3969
c propagations	: 19573
c inspects	: 48276
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 147
c 
c CURRENT OPTIMUM=2925
c Current CPU time (ms) : 25.398
c starts	: 148
c conflicts	: 2
c decisions	: 3996
c propagations	: 19706
c inspects	: 48907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 148
c 
c CURRENT OPTIMUM=2924
c Current CPU time (ms) : 25.599
c starts	: 149
c conflicts	: 2
c decisions	: 4022
c propagations	: 19839
c inspects	: 49413
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 149
c 
c CURRENT OPTIMUM=2923
c Current CPU time (ms) : 25.85
c starts	: 150
c conflicts	: 2
c decisions	: 4049
c propagations	: 19972
c inspects	: 50057
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 150
c 
c CURRENT OPTIMUM=2922
c Current CPU time (ms) : 26.104
c starts	: 151
c conflicts	: 2
c decisions	: 4075
c propagations	: 20105
c inspects	: 50571
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 151
c 
c CURRENT OPTIMUM=2921
c Current CPU time (ms) : 26.31
c starts	: 152
c conflicts	: 2
c decisions	: 4101
c propagations	: 20238
c inspects	: 51091
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 152
c 
c CURRENT OPTIMUM=2920
c Current CPU time (ms) : 26.465
c starts	: 153
c conflicts	: 2
c decisions	: 4126
c propagations	: 20371
c inspects	: 51485
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 153
c 
c CURRENT OPTIMUM=2919
c Current CPU time (ms) : 26.724
c starts	: 154
c conflicts	: 2
c decisions	: 4153
c propagations	: 20504
c inspects	: 52152
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 154
c 
c CURRENT OPTIMUM=2918
c Current CPU time (ms) : 26.983
c starts	: 155
c conflicts	: 2
c decisions	: 4179
c propagations	: 20637
c inspects	: 52678
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 155
c 
c CURRENT OPTIMUM=2917
c Current CPU time (ms) : 27.193
c starts	: 156
c conflicts	: 2
c decisions	: 4205
c propagations	: 20770
c inspects	: 53210
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 156
c 
c CURRENT OPTIMUM=2916
c Current CPU time (ms) : 27.354
c starts	: 157
c conflicts	: 2
c decisions	: 4230
c propagations	: 20903
c inspects	: 53615
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 157
c 
c CURRENT OPTIMUM=2915
c Current CPU time (ms) : 27.568
c starts	: 158
c conflicts	: 2
c decisions	: 4256
c propagations	: 21036
c inspects	: 54157
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 158
c 
c CURRENT OPTIMUM=2914
c Current CPU time (ms) : 27.73
c starts	: 159
c conflicts	: 2
c decisions	: 4281
c propagations	: 21169
c inspects	: 54568
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 159
c 
c CURRENT OPTIMUM=2913
c Current CPU time (ms) : 27.948
c starts	: 160
c conflicts	: 2
c decisions	: 4306
c propagations	: 21302
c inspects	: 54984
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 160
c 
c CURRENT OPTIMUM=2912
c Current CPU time (ms) : 28.063
c starts	: 161
c conflicts	: 2
c decisions	: 4330
c propagations	: 21435
c inspects	: 55273
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 161
c 
c CURRENT OPTIMUM=2911
c Current CPU time (ms) : 28.38
c starts	: 162
c conflicts	: 2
c decisions	: 4358
c propagations	: 21568
c inspects	: 56140
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 162
c 
c CURRENT OPTIMUM=2910
c Current CPU time (ms) : 28.64
c starts	: 163
c conflicts	: 2
c decisions	: 4385
c propagations	: 21701
c inspects	: 56797
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 163
c 
c CURRENT OPTIMUM=2909
c Current CPU time (ms) : 28.956
c starts	: 164
c conflicts	: 2
c decisions	: 4412
c propagations	: 21834
c inspects	: 57461
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 164
c 
c CURRENT OPTIMUM=2908
c Current CPU time (ms) : 29.17
c starts	: 165
c conflicts	: 2
c decisions	: 4438
c propagations	: 21967
c inspects	: 58000
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 165
c 
c CURRENT OPTIMUM=2907
c Current CPU time (ms) : 29.438
c starts	: 166
c conflicts	: 2
c decisions	: 4465
c propagations	: 22100
c inspects	: 58677
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 166
c 
c CURRENT OPTIMUM=2906
c Current CPU time (ms) : 29.655
c starts	: 167
c conflicts	: 2
c decisions	: 4491
c propagations	: 22233
c inspects	: 59224
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 167
c 
c CURRENT OPTIMUM=2905
c Current CPU time (ms) : 29.928
c starts	: 168
c conflicts	: 2
c decisions	: 4517
c propagations	: 22366
c inspects	: 59777
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 168
c 
c CURRENT OPTIMUM=2904
c Current CPU time (ms) : 30.097
c starts	: 169
c conflicts	: 2
c decisions	: 4542
c propagations	: 22499
c inspects	: 60204
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 169
c 
c CURRENT OPTIMUM=2903
c Current CPU time (ms) : 30.371
c starts	: 170
c conflicts	: 2
c decisions	: 4569
c propagations	: 22632
c inspects	: 60904
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 170
c 
c CURRENT OPTIMUM=2902
c Current CPU time (ms) : 30.594
c starts	: 171
c conflicts	: 2
c decisions	: 4595
c propagations	: 22765
c inspects	: 61463
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 171
c 
c CURRENT OPTIMUM=2901
c Current CPU time (ms) : 30.873
c starts	: 172
c conflicts	: 2
c decisions	: 4621
c propagations	: 22898
c inspects	: 62028
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 172
c 
c CURRENT OPTIMUM=2900
c Current CPU time (ms) : 31.048
c starts	: 173
c conflicts	: 2
c decisions	: 4646
c propagations	: 23031
c inspects	: 62467
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 173
c 
c CURRENT OPTIMUM=2899
c Current CPU time (ms) : 31.281
c starts	: 174
c conflicts	: 2
c decisions	: 4672
c propagations	: 23164
c inspects	: 63043
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 174
c 
c CURRENT OPTIMUM=2898
c Current CPU time (ms) : 31.458
c starts	: 175
c conflicts	: 2
c decisions	: 4697
c propagations	: 23297
c inspects	: 63488
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 175
c 
c CURRENT OPTIMUM=2897
c Current CPU time (ms) : 31.636
c starts	: 176
c conflicts	: 2
c decisions	: 4722
c propagations	: 23430
c inspects	: 63938
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 176
c 
c CURRENT OPTIMUM=2896
c Current CPU time (ms) : 31.763
c starts	: 177
c conflicts	: 2
c decisions	: 4746
c propagations	: 23563
c inspects	: 64261
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 177
c 
c CURRENT OPTIMUM=2895
c Current CPU time (ms) : 32.103
c starts	: 178
c conflicts	: 2
c decisions	: 4773
c propagations	: 23696
c inspects	: 65000
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 178
c 
c CURRENT OPTIMUM=2894
c Current CPU time (ms) : 32.332
c starts	: 179
c conflicts	: 2
c decisions	: 4799
c propagations	: 23829
c inspects	: 65575
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 179
c 
c CURRENT OPTIMUM=2893
c Current CPU time (ms) : 32.564
c starts	: 180
c conflicts	: 2
c decisions	: 4825
c propagations	: 23962
c inspects	: 66156
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 180
c 
c CURRENT OPTIMUM=2892
c Current CPU time (ms) : 32.743
c starts	: 181
c conflicts	: 2
c decisions	: 4850
c propagations	: 24095
c inspects	: 66611
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 181
c 
c CURRENT OPTIMUM=2891
c Current CPU time (ms) : 33.036
c starts	: 182
c conflicts	: 2
c decisions	: 4876
c propagations	: 24228
c inspects	: 67203
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 182
c 
c CURRENT OPTIMUM=2890
c Current CPU time (ms) : 33.22
c starts	: 183
c conflicts	: 2
c decisions	: 4901
c propagations	: 24361
c inspects	: 67664
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 183
c 
c CURRENT OPTIMUM=2889
c Current CPU time (ms) : 33.405
c starts	: 184
c conflicts	: 2
c decisions	: 4926
c propagations	: 24494
c inspects	: 68129
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 184
c 
c CURRENT OPTIMUM=2888
c Current CPU time (ms) : 33.54
c starts	: 185
c conflicts	: 2
c decisions	: 4950
c propagations	: 24627
c inspects	: 68467
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 185
c 
c CURRENT OPTIMUM=2887
c Current CPU time (ms) : 33.836
c starts	: 186
c conflicts	: 2
c decisions	: 4976
c propagations	: 24760
c inspects	: 69077
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 186
c 
c CURRENT OPTIMUM=2886
c Current CPU time (ms) : 34.023
c starts	: 187
c conflicts	: 2
c decisions	: 5001
c propagations	: 24893
c inspects	: 69545
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 187
c 
c CURRENT OPTIMUM=2885
c Current CPU time (ms) : 34.212
c starts	: 188
c conflicts	: 2
c decisions	: 5026
c propagations	: 25026
c inspects	: 70017
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 188
c 
c CURRENT OPTIMUM=2884
c Current CPU time (ms) : 34.35
c starts	: 189
c conflicts	: 2
c decisions	: 5050
c propagations	: 25159
c inspects	: 70362
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 189
c 
c CURRENT OPTIMUM=2883
c Current CPU time (ms) : 34.541
c starts	: 190
c conflicts	: 2
c decisions	: 5075
c propagations	: 25292
c inspects	: 70843
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 190
c 
c CURRENT OPTIMUM=2882
c Current CPU time (ms) : 34.679
c starts	: 191
c conflicts	: 2
c decisions	: 5099
c propagations	: 25425
c inspects	: 71192
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 191
c 
c CURRENT OPTIMUM=2881
c Current CPU time (ms) : 34.88
c starts	: 192
c conflicts	: 2
c decisions	: 5123
c propagations	: 25558
c inspects	: 71545
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 192
c 
c CURRENT OPTIMUM=2880
c Current CPU time (ms) : 34.97
c starts	: 193
c conflicts	: 2
c decisions	: 5146
c propagations	: 25691
c inspects	: 71770
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 193
c 
c CURRENT OPTIMUM=2879
c Current CPU time (ms) : 35.309
c starts	: 194
c conflicts	: 2
c decisions	: 5174
c propagations	: 25824
c inspects	: 72765
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 194
c 
c CURRENT OPTIMUM=2878
c Current CPU time (ms) : 35.583
c starts	: 195
c conflicts	: 2
c decisions	: 5201
c propagations	: 25957
c inspects	: 73455
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 195
c 
c CURRENT OPTIMUM=2877
c Current CPU time (ms) : 35.921
c starts	: 196
c conflicts	: 2
c decisions	: 5228
c propagations	: 26090
c inspects	: 74152
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 196
c 
c CURRENT OPTIMUM=2876
c Current CPU time (ms) : 36.149
c starts	: 197
c conflicts	: 2
c decisions	: 5254
c propagations	: 26223
c inspects	: 74724
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 197
c 
c CURRENT OPTIMUM=2875
c Current CPU time (ms) : 36.431
c starts	: 198
c conflicts	: 2
c decisions	: 5281
c propagations	: 26356
c inspects	: 75434
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 198
c 
c CURRENT OPTIMUM=2874
c Current CPU time (ms) : 36.66
c starts	: 199
c conflicts	: 2
c decisions	: 5307
c propagations	: 26489
c inspects	: 76014
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 199
c 
c CURRENT OPTIMUM=2873
c Current CPU time (ms) : 36.958
c starts	: 200
c conflicts	: 2
c decisions	: 5333
c propagations	: 26622
c inspects	: 76600
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 200
c 
c CURRENT OPTIMUM=2872
c Current CPU time (ms) : 37.141
c starts	: 201
c conflicts	: 2
c decisions	: 5358
c propagations	: 26755
c inspects	: 77060
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 201
c 
c CURRENT OPTIMUM=2871
c Current CPU time (ms) : 37.427
c starts	: 202
c conflicts	: 2
c decisions	: 5385
c propagations	: 26888
c inspects	: 77793
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 202
c 
c CURRENT OPTIMUM=2870
c Current CPU time (ms) : 37.661
c starts	: 203
c conflicts	: 2
c decisions	: 5411
c propagations	: 27021
c inspects	: 78385
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 203
c 
c CURRENT OPTIMUM=2869
c Current CPU time (ms) : 37.947
c starts	: 204
c conflicts	: 2
c decisions	: 5437
c propagations	: 27154
c inspects	: 78983
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 204
c 
c CURRENT OPTIMUM=2868
c Current CPU time (ms) : 38.134
c starts	: 205
c conflicts	: 2
c decisions	: 5462
c propagations	: 27287
c inspects	: 79455
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 205
c 
c CURRENT OPTIMUM=2867
c Current CPU time (ms) : 38.375
c starts	: 206
c conflicts	: 2
c decisions	: 5488
c propagations	: 27420
c inspects	: 80064
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 206
c 
c CURRENT OPTIMUM=2866
c Current CPU time (ms) : 38.563
c starts	: 207
c conflicts	: 2
c decisions	: 5513
c propagations	: 27553
c inspects	: 80542
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 207
c 
c CURRENT OPTIMUM=2865
c Current CPU time (ms) : 38.797
c starts	: 208
c conflicts	: 2
c decisions	: 5538
c propagations	: 27686
c inspects	: 81025
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 208
c 
c CURRENT OPTIMUM=2864
c Current CPU time (ms) : 38.939
c starts	: 209
c conflicts	: 2
c decisions	: 5562
c propagations	: 27819
c inspects	: 81381
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 209
c 
c CURRENT OPTIMUM=2863
c Current CPU time (ms) : 39.234
c starts	: 210
c conflicts	: 2
c decisions	: 5589
c propagations	: 27952
c inspects	: 82153
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 210
c 
c CURRENT OPTIMUM=2862
c Current CPU time (ms) : 39.477
c starts	: 211
c conflicts	: 2
c decisions	: 5615
c propagations	: 28085
c inspects	: 82761
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 211
c 
c CURRENT OPTIMUM=2861
c Current CPU time (ms) : 39.763
c starts	: 212
c conflicts	: 2
c decisions	: 5641
c propagations	: 28218
c inspects	: 83375
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 212
c 
c CURRENT OPTIMUM=2860
c Current CPU time (ms) : 39.957
c starts	: 213
c conflicts	: 2
c decisions	: 5666
c propagations	: 28351
c inspects	: 83863
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 213
c 
c CURRENT OPTIMUM=2859
c Current CPU time (ms) : 40.204
c starts	: 214
c conflicts	: 2
c decisions	: 5692
c propagations	: 28484
c inspects	: 84488
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 214
c 
c CURRENT OPTIMUM=2858
c Current CPU time (ms) : 40.4
c starts	: 215
c conflicts	: 2
c decisions	: 5717
c propagations	: 28617
c inspects	: 84982
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 215
c 
c CURRENT OPTIMUM=2857
c Current CPU time (ms) : 40.596
c starts	: 216
c conflicts	: 2
c decisions	: 5742
c propagations	: 28750
c inspects	: 85481
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 216
c 
c CURRENT OPTIMUM=2856
c Current CPU time (ms) : 40.788
c starts	: 217
c conflicts	: 2
c decisions	: 5766
c propagations	: 28883
c inspects	: 85853
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 217
c 
c CURRENT OPTIMUM=2855
c Current CPU time (ms) : 41.039
c starts	: 218
c conflicts	: 2
c decisions	: 5792
c propagations	: 29016
c inspects	: 86497
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 218
c 
c CURRENT OPTIMUM=2854
c Current CPU time (ms) : 41.24
c starts	: 219
c conflicts	: 2
c decisions	: 5817
c propagations	: 29149
c inspects	: 86999
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 219
c 
c CURRENT OPTIMUM=2853
c Current CPU time (ms) : 41.441
c starts	: 220
c conflicts	: 2
c decisions	: 5842
c propagations	: 29282
c inspects	: 87506
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 220
c 
c CURRENT OPTIMUM=2852
c Current CPU time (ms) : 41.634
c starts	: 221
c conflicts	: 2
c decisions	: 5866
c propagations	: 29415
c inspects	: 87886
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 221
c 
c CURRENT OPTIMUM=2851
c Current CPU time (ms) : 41.838
c starts	: 222
c conflicts	: 2
c decisions	: 5891
c propagations	: 29548
c inspects	: 88402
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 222
c 
c CURRENT OPTIMUM=2850
c Current CPU time (ms) : 41.991
c starts	: 223
c conflicts	: 2
c decisions	: 5915
c propagations	: 29681
c inspects	: 88786
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 223
c 
c CURRENT OPTIMUM=2849
c Current CPU time (ms) : 42.145
c starts	: 224
c conflicts	: 2
c decisions	: 5939
c propagations	: 29814
c inspects	: 89174
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 224
c 
c CURRENT OPTIMUM=2848
c Current CPU time (ms) : 42.249
c starts	: 225
c conflicts	: 2
c decisions	: 5962
c propagations	: 29947
c inspects	: 89434
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 225
c 
c CURRENT OPTIMUM=2847
c Current CPU time (ms) : 42.554
c starts	: 226
c conflicts	: 2
c decisions	: 5989
c propagations	: 30080
c inspects	: 90269
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 226
c 
c CURRENT OPTIMUM=2846
c Current CPU time (ms) : 42.846
c starts	: 227
c conflicts	: 2
c decisions	: 6015
c propagations	: 30213
c inspects	: 90893
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 227
c 
c CURRENT OPTIMUM=2845
c Current CPU time (ms) : 43.097
c starts	: 228
c conflicts	: 2
c decisions	: 6041
c propagations	: 30346
c inspects	: 91523
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 228
c 
c CURRENT OPTIMUM=2844
c Current CPU time (ms) : 43.298
c starts	: 229
c conflicts	: 2
c decisions	: 6066
c propagations	: 30479
c inspects	: 92027
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 229
c 
c CURRENT OPTIMUM=2843
c Current CPU time (ms) : 43.599
c starts	: 230
c conflicts	: 2
c decisions	: 6092
c propagations	: 30612
c inspects	: 92668
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 230
c 
c CURRENT OPTIMUM=2842
c Current CPU time (ms) : 43.802
c starts	: 231
c conflicts	: 2
c decisions	: 6117
c propagations	: 30745
c inspects	: 93178
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 231
c 
c CURRENT OPTIMUM=2841
c Current CPU time (ms) : 44.008
c starts	: 232
c conflicts	: 2
c decisions	: 6142
c propagations	: 30878
c inspects	: 93693
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 232
c 
c CURRENT OPTIMUM=2840
c Current CPU time (ms) : 44.162
c starts	: 233
c conflicts	: 2
c decisions	: 6166
c propagations	: 31011
c inspects	: 94081
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 233
c 
c CURRENT OPTIMUM=2839
c Current CPU time (ms) : 44.418
c starts	: 234
c conflicts	: 2
c decisions	: 6192
c propagations	: 31144
c inspects	: 94741
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 234
c 
c CURRENT OPTIMUM=2838
c Current CPU time (ms) : 44.667
c starts	: 235
c conflicts	: 2
c decisions	: 6217
c propagations	: 31277
c inspects	: 95259
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 235
c 
c CURRENT OPTIMUM=2837
c Current CPU time (ms) : 44.875
c starts	: 236
c conflicts	: 2
c decisions	: 6242
c propagations	: 31410
c inspects	: 95781
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 236
c 
c CURRENT OPTIMUM=2836
c Current CPU time (ms) : 45.033
c starts	: 237
c conflicts	: 2
c decisions	: 6266
c propagations	: 31543
c inspects	: 96176
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 237
c 
c CURRENT OPTIMUM=2835
c Current CPU time (ms) : 45.244
c starts	: 238
c conflicts	: 2
c decisions	: 6291
c propagations	: 31676
c inspects	: 96707
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 238
c 
c CURRENT OPTIMUM=2834
c Current CPU time (ms) : 45.401
c starts	: 239
c conflicts	: 2
c decisions	: 6315
c propagations	: 31809
c inspects	: 97106
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 239
c 
c CURRENT OPTIMUM=2833
c Current CPU time (ms) : 45.605
c starts	: 240
c conflicts	: 2
c decisions	: 6339
c propagations	: 31942
c inspects	: 97509
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 240
c 
c CURRENT OPTIMUM=2832
c Current CPU time (ms) : 45.717
c starts	: 241
c conflicts	: 2
c decisions	: 6362
c propagations	: 32075
c inspects	: 97784
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 241
c 
c CURRENT OPTIMUM=2831
c Current CPU time (ms) : 45.984
c starts	: 242
c conflicts	: 2
c decisions	: 6388
c propagations	: 32208
c inspects	: 98474
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 242
c 
c CURRENT OPTIMUM=2830
c Current CPU time (ms) : 46.198
c starts	: 243
c conflicts	: 2
c decisions	: 6413
c propagations	: 32341
c inspects	: 98999
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 243
c 
c CURRENT OPTIMUM=2829
c Current CPU time (ms) : 46.41
c starts	: 244
c conflicts	: 2
c decisions	: 6438
c propagations	: 32474
c inspects	: 99529
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 244
c 
c CURRENT OPTIMUM=2828
c Current CPU time (ms) : 46.616
c starts	: 245
c conflicts	: 2
c decisions	: 6462
c propagations	: 32607
c inspects	: 99932
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 245
c 
c CURRENT OPTIMUM=2827
c Current CPU time (ms) : 46.83
c starts	: 246
c conflicts	: 2
c decisions	: 6487
c propagations	: 32740
c inspects	: 100471
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 246
c 
c CURRENT OPTIMUM=2826
c Current CPU time (ms) : 46.993
c starts	: 247
c conflicts	: 2
c decisions	: 6511
c propagations	: 32873
c inspects	: 100878
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 247
c 
c CURRENT OPTIMUM=2825
c Current CPU time (ms) : 47.157
c starts	: 248
c conflicts	: 2
c decisions	: 6535
c propagations	: 33006
c inspects	: 101289
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 248
c 
c CURRENT OPTIMUM=2824
c Current CPU time (ms) : 47.27
c starts	: 249
c conflicts	: 2
c decisions	: 6558
c propagations	: 33139
c inspects	: 101572
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 249
c 
c CURRENT OPTIMUM=2823
c Current CPU time (ms) : 47.529
c starts	: 250
c conflicts	: 2
c decisions	: 6583
c propagations	: 33272
c inspects	: 102126
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 250
c 
c CURRENT OPTIMUM=2822
c Current CPU time (ms) : 47.693
c starts	: 251
c conflicts	: 2
c decisions	: 6607
c propagations	: 33405
c inspects	: 102537
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 251
c 
c CURRENT OPTIMUM=2821
c Current CPU time (ms) : 47.859
c starts	: 252
c conflicts	: 2
c decisions	: 6631
c propagations	: 33538
c inspects	: 102952
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 252
c 
c CURRENT OPTIMUM=2820
c Current CPU time (ms) : 47.976
c starts	: 253
c conflicts	: 2
c decisions	: 6654
c propagations	: 33671
c inspects	: 103239
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 253
c 
c CURRENT OPTIMUM=2819
c Current CPU time (ms) : 48.143
c starts	: 254
c conflicts	: 2
c decisions	: 6678
c propagations	: 33804
c inspects	: 103660
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 254
c 
c CURRENT OPTIMUM=2818
c Current CPU time (ms) : 48.258
c starts	: 255
c conflicts	: 2
c decisions	: 6701
c propagations	: 33937
c inspects	: 103948
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 255
c 
c CURRENT OPTIMUM=2817
c Current CPU time (ms) : 48.373
c starts	: 256
c conflicts	: 2
c decisions	: 6724
c propagations	: 34070
c inspects	: 104239
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 256
c 
c CURRENT OPTIMUM=2816
c Current CPU time (ms) : 48.485
c starts	: 257
c conflicts	: 2
c decisions	: 6746
c propagations	: 34203
c inspects	: 104401
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 2
c root simplifications	: 257
c 
c CURRENT OPTIMUM=2688
c Current CPU time (ms) : 48.572
c starts	: 258
c conflicts	: 3
c decisions	: 6838
c propagations	: 34369
c inspects	: 104608
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 3
c root simplifications	: 258
c 
c CURRENT OPTIMUM=2560
c Current CPU time (ms) : 49.143
c starts	: 259
c conflicts	: 4
c decisions	: 7029
c propagations	: 34589
c inspects	: 110151
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 4
c root simplifications	: 259
c 
c CURRENT OPTIMUM=2432
c Current CPU time (ms) : 49.828
c starts	: 260
c conflicts	: 4
c decisions	: 7129
c propagations	: 34722
c inspects	: 118000
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 4
c root simplifications	: 260
c 
c CURRENT OPTIMUM=2431
c Current CPU time (ms) : 61.175
c starts	: 262
c conflicts	: 111
c decisions	: 8005
c propagations	: 36333
c inspects	: 193975
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 111
c root simplifications	: 262
c 
c CURRENT OPTIMUM=2427
c Current CPU time (ms) : 84.791
c starts	: 265
c conflicts	: 411
c decisions	: 8763
c propagations	: 38647
c inspects	: 336802
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 411
c root simplifications	: 265
c 
c CURRENT OPTIMUM=2335
c Current CPU time (ms) : 85.74
c starts	: 266
c conflicts	: 411
c decisions	: 8883
c propagations	: 38780
c inspects	: 344887
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 411
c root simplifications	: 266
c 
c CURRENT OPTIMUM=2271
c Current CPU time (ms) : 86.186
c starts	: 267
c conflicts	: 412
c decisions	: 9007
c propagations	: 38926
c inspects	: 344988
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 412
c root simplifications	: 267
c 
c CURRENT OPTIMUM=2176
c Current CPU time (ms) : 88.097
c starts	: 268
c conflicts	: 432
c decisions	: 9179
c propagations	: 39212
c inspects	: 354241
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 432
c root simplifications	: 268
c 
c CURRENT OPTIMUM=2166
c Current CPU time (ms) : 91.254
c starts	: 269
c conflicts	: 482
c decisions	: 9410
c propagations	: 39748
c inspects	: 373247
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 482
c root simplifications	: 269
c 
c CURRENT OPTIMUM=2163
c Current CPU time (ms) : 353.199
c starts	: 276
c conflicts	: 3223
c decisions	: 16927
c propagations	: 62091
c inspects	: 1268502
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 3223
c root simplifications	: 276
c 
c CURRENT OPTIMUM=2162
c Current CPU time (ms) : 373.312
c starts	: 277
c conflicts	: 3287
c decisions	: 17316
c propagations	: 63295
c inspects	: 1338746
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 3287
c root simplifications	: 277
c 
c CURRENT OPTIMUM=2158
c Current CPU time (ms) : 645.028
c starts	: 283
c conflicts	: 4642
c decisions	: 21481
c propagations	: 76159
c inspects	: 2032258
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 4642
c root simplifications	: 283
c 
c CURRENT OPTIMUM=2146
c Current CPU time (ms) : 1043.406
c starts	: 289
c conflicts	: 6230
c decisions	: 26219
c propagations	: 89791
c inspects	: 2713731
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 6230
c root simplifications	: 289
#### 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.92 0.98 0.93 2/54 20577
Raw data (stat): 20577 (runsolver) R 20576 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482531288 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 1.15 1.03 0.94 2/64 20645
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18078 8 1 0 758 47 2 0 25 0 11 0 482531288 867409920 21667 4294967295 134512640 134569956 3221224400 3221214776 1131303745 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211770 21667 13073 16 0 211754 0
vsize: 847080
[startup+20.0013 s]
Raw data (loadavg): 1.13 1.03 0.94 2/64 20706
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18078 8 1 0 1709 51 4 1 25 0 11 0 482531288 865865728 21628 4294967295 134512640 134569956 3221224400 3221214776 1131304602 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211393 21628 13073 16 0 211377 0
vsize: 845572
[startup+30.0013 s]
Raw data (loadavg): 1.11 1.03 0.94 2/64 20752
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18079 8 1 0 2655 55 5 2 25 0 11 0 482531288 864227328 21525 4294967295 134512640 134569956 3221224400 3221214776 1131310578 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 21525 13073 16 0 210977 0
vsize: 843972
[startup+40.0019 s]
Raw data (loadavg): 1.09 1.03 0.94 2/64 20797
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18080 8 1 0 3594 58 6 2 25 0 11 0 482531288 864227328 21951 4294967295 134512640 134569956 3221224400 3221214756 1131231475 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 21951 13073 16 0 210977 0
vsize: 843972
[startup+50.0019 s]
Raw data (loadavg): 1.08 1.03 0.94 2/64 20846
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18081 8 1 0 4540 60 8 3 25 0 11 0 482531288 864227328 22137 4294967295 134512640 134569956 3221224400 3221214760 1131302582 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 22137 13073 16 0 210977 0
vsize: 843972
[startup+60.003 s]
Raw data (loadavg): 1.14 1.04 0.95 3/64 20847
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 5392 60 8 3 25 0 11 0 482531288 872468480 24099 4294967295 134512640 134569956 3221224400 3221214760 1131307569 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 213005 24099 13073 16 0 212989 0
vsize: 852020
[startup+70.0036 s]
Raw data (loadavg): 1.12 1.04 0.95 2/64 20848
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 6317 61 8 3 25 0 11 0 482531288 864227328 22476 4294967295 134512640 134569956 3221224400 3221214536 1131267024 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 22476 13073 16 0 210977 0
vsize: 843972
[startup+80.0076 s]
Raw data (loadavg): 1.10 1.04 0.95 2/64 20848
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 7259 61 8 3 24 0 11 0 482531288 864227328 22702 4294967295 134512640 134569956 3221224400 3221214760 1131307569 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 22702 13073 16 0 210977 0
vsize: 843972
[startup+90.0078 s]
Raw data (loadavg): 1.09 1.04 0.95 2/64 20852
Raw data (stat): 20577 (java) S 20576 25347 25346 0 -1 0 18089 8 1 0 8217 61 8 3 25 0 11 0 482531288 864227328 22806 4294967295 134512640 134569956 3221224400 3221213504 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 22806 13073 16 0 210977 0
vsize: 843972
[startup+100.008 s]
Raw data (loadavg): 1.07 1.03 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 9170 61 8 3 25 0 11 0 482531288 864227328 23065 4294967295 134512640 134569956 3221224400 3221214152 1131633105 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 23065 13073 16 0 210977 0
vsize: 843972
[startup+110.008 s]
Raw data (loadavg): 1.06 1.03 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 10123 62 8 3 25 0 11 0 482531288 864227328 23293 4294967295 134512640 134569956 3221224400 3221214528 1131631996 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 23293 13073 16 0 210977 0
vsize: 843972
[startup+120.009 s]
Raw data (loadavg): 1.05 1.03 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 11068 62 8 3 25 0 11 0 482531288 864227328 23452 4294967295 134512640 134569956 3221224400 3221214760 1131304562 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 23452 13073 16 0 210977 0
vsize: 843972
[startup+130.009 s]
Raw data (loadavg): 1.04 1.03 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 12011 62 8 3 25 0 11 0 482531288 864227328 23634 4294967295 134512640 134569956 3221224400 3221214528 1131631975 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 23634 13073 16 0 210977 0
vsize: 843972
[startup+140.009 s]
Raw data (loadavg): 1.04 1.03 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 12970 63 8 3 25 0 11 0 482531288 864227328 23792 4294967295 134512640 134569956 3221224400 3221214648 1131425185 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 23792 13073 16 0 210977 0
vsize: 843972
[startup+150.01 s]
Raw data (loadavg): 1.03 1.03 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 13928 63 8 3 25 0 11 0 482531288 864227328 23965 4294967295 134512640 134569956 3221224400 3221214544 1131267203 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 23965 13073 16 0 210977 0
vsize: 843972
[startup+160.011 s]
Raw data (loadavg): 1.02 1.03 0.95 2/64 20853
Raw data (stat): 20577 (java) S 20576 25347 25346 0 -1 0 18089 8 1 0 14884 63 8 3 25 0 11 0 482531288 864227328 24070 4294967295 134512640 134569956 3221224400 3221213504 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 24070 13073 16 0 210977 0
vsize: 843972
[startup+170.011 s]
Raw data (loadavg): 1.02 1.02 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 15844 64 8 3 25 0 11 0 482531288 864227328 24176 4294967295 134512640 134569956 3221224400 3221214032 1131633044 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 24176 13073 16 0 210977 0
vsize: 843972
[startup+180.012 s]
Raw data (loadavg): 1.02 1.02 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 16804 64 8 3 25 0 11 0 482531288 864227328 24321 4294967295 134512640 134569956 3221224400 3221214760 1131307569 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 24321 13073 16 0 210977 0
vsize: 843972
[startup+190.013 s]
Raw data (loadavg): 1.01 1.02 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 17764 64 8 3 25 0 11 0 482531288 864227328 24405 4294967295 134512640 134569956 3221224400 3221214536 1131461872 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 24405 13073 16 0 210977 0
vsize: 843972
[startup+200.012 s]
Raw data (loadavg): 1.01 1.02 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 18711 64 8 3 25 0 11 0 482531288 864227328 24565 4294967295 134512640 134569956 3221224400 3221214240 1131645899 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 24565 13073 16 0 210977 0
vsize: 843972
[startup+210.012 s]
Raw data (loadavg): 1.01 1.02 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 19660 64 8 3 25 0 11 0 482531288 864227328 24700 4294967295 134512640 134569956 3221224400 3221214128 1131645672 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 24700 13073 16 0 210977 0
vsize: 843972
[startup+220.013 s]
Raw data (loadavg): 1.01 1.02 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 20619 65 8 3 25 0 11 0 482531288 864227328 24819 4294967295 134512640 134569956 3221224400 3221213944 1085679492 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 24819 13073 16 0 210977 0
vsize: 843972
[startup+230.012 s]
Raw data (loadavg): 1.01 1.02 0.95 3/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 21577 65 8 3 25 0 11 0 482531288 864227328 24967 4294967295 134512640 134569956 3221224400 3221213456 1073952732 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 24967 13073 16 0 210977 0
vsize: 843972
[startup+240.012 s]
Raw data (loadavg): 1.00 1.02 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 22515 65 8 3 24 0 11 0 482531288 864227328 25227 4294967295 134512640 134569956 3221224400 3221214536 1131633080 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 25227 13073 16 0 210977 0
vsize: 843972
[startup+250.013 s]
Raw data (loadavg): 1.00 1.02 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 23465 66 8 3 25 0 11 0 482531288 864227328 25346 4294967295 134512640 134569956 3221224400 3221214704 1131482169 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 25346 13073 16 0 210977 0
vsize: 843972
[startup+260.014 s]
Raw data (loadavg): 1.00 1.02 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 24415 66 8 3 25 0 11 0 482531288 864227328 25470 4294967295 134512640 134569956 3221224400 3221214784 1131435439 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 25470 13073 16 0 210977 0
vsize: 843972
[startup+270.014 s]
Raw data (loadavg): 1.00 1.02 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 25366 66 8 3 25 0 11 0 482531288 864227328 25601 4294967295 134512640 134569956 3221224400 3221214760 1131307626 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 25601 13073 16 0 210977 0
vsize: 843972
[startup+280.014 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 26307 66 8 3 25 0 11 0 482531288 864227328 25743 4294967295 134512640 134569956 3221224400 3221213896 1085679293 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 25743 13073 16 0 210977 0
vsize: 843972
[startup+290.015 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 27278 66 8 3 24 0 11 0 482531288 864227328 25853 4294967295 134512640 134569956 3221224400 3221214760 1131309536 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 25853 13073 16 0 210977 0
vsize: 843972
[startup+300.015 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 28250 66 8 3 25 0 11 0 482531288 864227328 25980 4294967295 134512640 134569956 3221224400 3221213864 1131631996 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 25980 13073 16 0 210977 0
vsize: 843972
[startup+310.015 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 29222 67 8 3 25 0 11 0 482531288 864227328 26089 4294967295 134512640 134569956 3221224400 3221214280 1085679318 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26089 13073 16 0 210977 0
vsize: 843972
[startup+320.015 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 30194 67 8 3 25 0 11 0 482531288 864227328 26170 4294967295 134512640 134569956 3221224400 3221214228 1131631744 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 26170 13073 16 0 210977 0
vsize: 843972
[startup+330.015 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 31164 67 8 3 25 0 11 0 482531288 864227328 26241 4294967295 134512640 134569956 3221224400 3221214828 1131733868 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26241 13073 16 0 210977 0
vsize: 843972
[startup+340.015 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 32133 67 8 3 25 0 11 0 482531288 864227328 26347 4294967295 134512640 134569956 3221224400 3221213772 1085679264 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26347 13073 16 0 210977 0
vsize: 843972
[startup+350.016 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 20853
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 33112 67 8 3 25 0 11 0 482531288 864227328 26431 4294967295 134512640 134569956 3221224400 3221214524 1131631392 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26431 13073 16 0 210977 0
vsize: 843972
[startup+360.017 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 20854
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 34090 68 8 3 25 0 11 0 482531288 864227328 26474 4294967295 134512640 134569956 3221224400 3221214392 1085679272 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26474 13073 16 0 210977 0
vsize: 843972
[startup+370.017 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 20854
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 35059 68 8 3 25 0 11 0 482531288 864227328 26537 4294967295 134512640 134569956 3221224400 3221214760 1131302582 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26537 13073 16 0 210977 0
vsize: 843972
[startup+380.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 36049 68 8 3 25 0 11 0 482531288 864227328 26554 4294967295 134512640 134569956 3221224400 3221213872 1131633165 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26554 13073 16 0 210977 0
vsize: 843972
[startup+390.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 37039 68 8 3 25 0 11 0 482531288 864227328 26595 4294967295 134512640 134569956 3221224400 3221214064 1085679762 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 26595 13073 16 0 210977 0
vsize: 843972
[startup+400.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 38017 69 8 3 25 0 11 0 482531288 864227328 26646 4294967295 134512640 134569956 3221224400 3221214360 1131631975 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26646 13073 16 0 210977 0
vsize: 843972
[startup+410.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 38996 69 8 3 25 0 11 0 482531288 864227328 26691 4294967295 134512640 134569956 3221224400 3221214544 1131267249 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26691 13073 16 0 210977 0
vsize: 843972
[startup+420.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 39985 69 8 3 25 0 11 0 482531288 864227328 26721 4294967295 134512640 134569956 3221224400 3221214476 1131633048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26721 13073 16 0 210977 0
vsize: 843972
[startup+430.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 40954 69 8 3 25 0 11 0 482531288 864227328 26829 4294967295 134512640 134569956 3221224400 3221214112 1085679313 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26829 13073 16 0 210977 0
vsize: 843972
[startup+440.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 41943 69 8 3 25 0 11 0 482531288 864227328 26829 4294967295 134512640 134569956 3221224400 3221214760 1131307812 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26829 13073 16 0 210977 0
vsize: 843972
[startup+450.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 42922 69 8 3 25 0 11 0 482531288 864227328 26898 4294967295 134512640 134569956 3221224400 3221214760 1131309800 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 26898 13073 16 0 210977 0
vsize: 843972
[startup+460.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 43890 69 8 3 25 0 11 0 482531288 864227328 26988 4294967295 134512640 134569956 3221224400 3221213928 1131633105 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 26988 13073 16 0 210977 0
vsize: 843972
[startup+470.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 44868 69 8 3 25 0 11 0 482531288 864227328 27027 4294967295 134512640 134569956 3221224400 3221213984 1131633080 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27027 13073 16 0 210977 0
vsize: 843972
[startup+480.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 45856 69 8 3 25 0 11 0 482531288 864227328 27077 4294967295 134512640 134569956 3221224400 3221213928 1131633080 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 27077 13073 16 0 210977 0
vsize: 843972
[startup+490.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 46836 69 8 3 25 0 11 0 482531288 864227328 27140 4294967295 134512640 134569956 3221224400 3221214760 1131310799 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27140 13073 16 0 210977 0
vsize: 843972
[startup+500.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 47793 70 8 3 25 0 11 0 482531288 864227328 27276 4294967295 134512640 134569956 3221224400 3221214456 1131627215 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27276 13073 16 0 210977 0
vsize: 843972
[startup+510.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 48760 70 8 3 25 0 11 0 482531288 864227328 27355 4294967295 134512640 134569956 3221224400 3221213916 1131631972 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 27355 13073 16 0 210977 0
vsize: 843972
[startup+520.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 49717 70 8 3 25 0 11 0 482531288 864227328 27531 4294967295 134512640 134569956 3221224400 3221214600 1131526210 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27531 13073 16 0 210977 0
vsize: 843972
[startup+530.134 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 50686 70 8 3 24 0 11 0 482531288 864227328 27587 4294967295 134512640 134569956 3221224400 3221214760 1131304422 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27587 13073 16 0 210977 0
vsize: 843972
[startup+540.141 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 51666 71 8 3 25 0 11 0 482531288 864227328 27637 4294967295 134512640 134569956 3221224400 3221214640 1131459297 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27637 13073 16 0 210977 0
vsize: 843972
[startup+550.141 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 52645 71 8 3 25 0 11 0 482531288 864227328 27667 4294967295 134512640 134569956 3221224400 3221214760 1131309756 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27667 13073 16 0 210977 0
vsize: 843972
[startup+560.142 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 53624 71 8 3 25 0 11 0 482531288 864227328 27736 4294967295 134512640 134569956 3221224400 3221213840 1085679308 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27736 13073 16 0 210977 0
vsize: 843972
[startup+570.142 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 54592 71 8 3 25 0 11 0 482531288 864227328 27828 4294967295 134512640 134569956 3221224400 3221214032 1131633052 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27828 13073 16 0 210977 0
vsize: 843972
[startup+580.142 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 55561 72 8 3 25 0 11 0 482531288 864227328 27919 4294967295 134512640 134569956 3221224400 3221214028 1131633040 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27919 13073 16 0 210977 0
vsize: 843972
[startup+590.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 56530 72 8 3 25 0 11 0 482531288 864227328 27976 4294967295 134512640 134569956 3221224400 3221213760 1131633080 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 27976 13073 16 0 210977 0
vsize: 843972
[startup+600.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 57499 72 8 3 25 0 11 0 482531288 864227328 28070 4294967295 134512640 134569956 3221224400 3221214760 1131302361 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28070 13073 16 0 210977 0
vsize: 843972
[startup+610.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 58470 73 8 3 25 0 11 0 482531288 864227328 28175 4294967295 134512640 134569956 3221224400 3221214224 1085679313 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28175 13073 16 0 210977 0
vsize: 843972
[startup+620.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 59451 73 8 3 25 0 11 0 482531288 864227328 28252 4294967295 134512640 134569956 3221224400 3221214528 1131631777 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28252 13073 16 0 210977 0
vsize: 843972
[startup+630.142 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 60432 73 8 3 25 0 11 0 482531288 864227328 28345 4294967295 134512640 134569956 3221224400 3221214080 1131631983 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28345 13073 16 0 210977 0
vsize: 843972
[startup+640.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20855
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 61432 73 8 3 25 0 11 0 482531288 864227328 28345 4294967295 134512640 134569956 3221224400 3221213760 1131633105 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28345 13073 16 0 210977 0
vsize: 843972
[startup+650.142 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 62415 73 8 3 25 0 11 0 482531288 864227328 28384 4294967295 134512640 134569956 3221224400 3221213816 1131633105 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28384 13073 16 0 210977 0
vsize: 843972
[startup+660.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 63406 74 8 3 25 0 11 0 482531288 864227328 28403 4294967295 134512640 134569956 3221224400 3221214032 1131633179 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28403 13073 16 0 210977 0
vsize: 843972
[startup+670.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 64396 74 8 3 25 0 11 0 482531288 864227328 28424 4294967295 134512640 134569956 3221224400 3221214056 1085679762 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28424 13073 16 0 210977 0
vsize: 843972
[startup+680.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 65387 74 8 3 25 0 11 0 482531288 864227328 28442 4294967295 134512640 134569956 3221224400 3221213920 1131633060 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 28442 13073 16 0 210977 0
vsize: 843972
[startup+690.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 66377 74 8 3 25 0 11 0 482531288 864227328 28459 4294967295 134512640 134569956 3221224400 3221214184 1131632008 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 28459 13073 16 0 210977 0
vsize: 843972
[startup+700.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 67357 74 8 3 25 0 11 0 482531288 864227328 28500 4294967295 134512640 134569956 3221224400 3221213832 1085632310 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28500 13073 16 0 210977 0
vsize: 843972
[startup+710.144 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 68347 74 8 3 25 0 11 0 482531288 864227328 28521 4294967295 134512640 134569956 3221224400 3221213804 1131631392 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28521 13073 16 0 210977 0
vsize: 843972
[startup+720.145 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 69326 74 8 3 25 0 11 0 482531288 864227328 28579 4294967295 134512640 134569956 3221224400 3221214832 1131248279 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28579 13073 16 0 210977 0
vsize: 843972
[startup+730.145 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 70316 74 8 3 25 0 11 0 482531288 864227328 28606 4294967295 134512640 134569956 3221224400 3221214464 1131631381 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28606 13073 16 0 210977 0
vsize: 843972
[startup+740.146 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 71305 75 8 3 25 0 11 0 482531288 864227328 28636 4294967295 134512640 134569956 3221224400 3221214080 1131631968 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28636 13073 16 0 210977 0
vsize: 843972
[startup+750.145 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 72295 75 8 3 25 0 11 0 482531288 864227328 28661 4294967295 134512640 134569956 3221224400 3221214448 1085632310 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28661 13073 16 0 210977 0
vsize: 843972
[startup+760.146 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 73263 75 8 3 25 0 11 0 482531288 864227328 28729 4294967295 134512640 134569956 3221224400 3221214312 1131632997 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28729 13073 16 0 210977 0
vsize: 843972
[startup+770.146 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 74252 75 8 3 25 0 11 0 482531288 864227328 28747 4294967295 134512640 134569956 3221224400 3221214580 1131632009 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 28747 13073 16 0 210977 0
vsize: 843972
[startup+780.145 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 75241 75 8 3 25 0 11 0 482531288 864227328 28775 4294967295 134512640 134569956 3221224400 3221214512 1131627218 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 28775 13073 16 0 210977 0
vsize: 843972
[startup+790.146 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 76220 75 8 3 25 0 11 0 482531288 864227328 28832 4294967295 134512640 134569956 3221224400 3221213888 1085679325 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28832 13073 16 0 210977 0
vsize: 843972
[startup+800.147 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 77220 76 8 3 25 0 11 0 482531288 864227328 28832 4294967295 134512640 134569956 3221224400 3221214536 1131633080 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 28832 13073 16 0 210977 0
vsize: 843972
[startup+810.147 s]
Raw data (loadavg): 1.08 1.02 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 78209 76 8 3 25 0 11 0 482531288 864227328 28851 4294967295 134512640 134569956 3221224400 3221214352 1131632002 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28851 13073 16 0 210977 0
vsize: 843972
[startup+820.147 s]
Raw data (loadavg): 1.07 1.02 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 79198 76 8 3 25 0 11 0 482531288 864227328 28867 4294967295 134512640 134569956 3221224400 3221214360 1131631975 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28867 13073 16 0 210977 0
vsize: 843972
[startup+830.146 s]
Raw data (loadavg): 1.06 1.01 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 80166 76 8 3 25 0 11 0 482531288 864227328 28931 4294967295 134512640 134569956 3221224400 3221214760 1131302666 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 28931 13073 16 0 210977 0
vsize: 843972
[startup+840.147 s]
Raw data (loadavg): 1.05 1.01 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 81143 76 8 3 25 0 11 0 482531288 864227328 29000 4294967295 134512640 134569956 3221224400 3221214408 1131632008 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29000 13073 16 0 210977 0
vsize: 843972
[startup+850.147 s]
Raw data (loadavg): 1.04 1.01 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 82132 76 8 3 25 0 11 0 482531288 864227328 29033 4294967295 134512640 134569956 3221224400 3221214312 1131633068 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29033 13073 16 0 210977 0
vsize: 843972
[startup+860.147 s]
Raw data (loadavg): 1.03 1.01 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 83132 77 8 3 25 0 11 0 482531288 864227328 29033 4294967295 134512640 134569956 3221224400 3221213984 1131633044 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29033 13073 16 0 210977 0
vsize: 843972
[startup+870.147 s]
Raw data (loadavg): 1.03 1.01 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 84110 78 8 3 25 0 11 0 482531288 864227328 29106 4294967295 134512640 134569956 3221224400 3221214536 1131266907 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29106 13073 16 0 210977 0
vsize: 843972
[startup+880.147 s]
Raw data (loadavg): 1.02 1.01 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 85088 78 8 3 25 0 11 0 482531288 864227328 29157 4294967295 134512640 134569956 3221224400 3221214416 1131631983 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29157 13073 16 0 210977 0
vsize: 843972
[startup+890.148 s]
Raw data (loadavg): 1.02 1.01 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 86056 78 8 3 25 0 11 0 482531288 864227328 29214 4294967295 134512640 134569956 3221224400 3221214128 1131631383 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 29214 13073 16 0 210977 0
vsize: 843972
[startup+900.147 s]
Raw data (loadavg): 1.02 1.01 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 87034 78 8 3 25 0 11 0 482531288 864227328 29243 4294967295 134512640 134569956 3221224400 3221214304 1131631983 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29243 13073 16 0 210977 0
vsize: 843972
[startup+910.148 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 88012 79 8 3 24 0 11 0 482531288 864227328 29341 4294967295 134512640 134569956 3221224400 3221214200 1131633080 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29341 13073 16 0 210977 0
vsize: 843972
[startup+920.149 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 88991 79 8 3 25 0 11 0 482531288 864227328 29387 4294967295 134512640 134569956 3221224400 3221214648 1131425011 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29387 13073 16 0 210977 0
vsize: 843972
[startup+930.148 s]
Raw data (loadavg): 1.01 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 89970 79 8 3 25 0 11 0 482531288 864227328 29442 4294967295 134512640 134569956 3221224400 3221214392 1085679747 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29442 13073 16 0 210977 0
vsize: 843972
[startup+940.148 s]
Raw data (loadavg): 1.01 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 90939 80 8 3 25 0 11 0 482531288 864227328 29534 4294967295 134512640 134569956 3221224400 3221214624 1131497050 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29534 13073 16 0 210977 0
vsize: 843972
[startup+950.148 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 91919 80 8 3 25 0 11 0 482531288 864227328 29587 4294967295 134512640 134569956 3221224400 3221214032 1131633080 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29587 13073 16 0 210977 0
vsize: 843972
[startup+960.149 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 92890 81 8 3 25 0 11 0 482531288 864227328 29681 4294967295 134512640 134569956 3221224400 3221214648 1131456366 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29681 13073 16 0 210977 0
vsize: 843972
[startup+970.149 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 93880 81 8 3 25 0 11 0 482531288 864227328 29697 4294967295 134512640 134569956 3221224400 3221214760 1131302259 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29697 13073 16 0 210977 0
vsize: 843972
[startup+980.149 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 94870 81 8 3 25 0 11 0 482531288 864227328 29714 4294967295 134512640 134569956 3221224400 3221214468 1131633190 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29714 13073 16 0 210977 0
vsize: 843972
[startup+990.149 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 95860 81 8 3 25 0 11 0 482531288 864227328 29745 4294967295 134512640 134569956 3221224400 3221213912 1131632008 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29745 13073 16 0 210977 0
vsize: 843972
[startup+1000.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 96850 82 8 3 25 0 11 0 482531288 864227328 29766 4294967295 134512640 134569956 3221224400 3221213632 1131632002 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29766 13073 16 0 210977 0
vsize: 843972
[startup+1010.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 97842 82 8 3 25 0 11 0 482531288 864227328 29796 4294967295 134512640 134569956 3221224400 3221213592 1131633044 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29796 13073 16 0 210977 0
vsize: 843972
[startup+1020.17 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 98832 82 8 3 25 0 11 0 482531288 864227328 29827 4294967295 134512640 134569956 3221224400 3221214188 1131631392 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29827 13073 16 0 210977 0
vsize: 843972
[startup+1030.17 s]
Raw data (loadavg): 1.07 1.02 0.96 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 99822 82 8 3 25 0 11 0 482531288 864227328 29860 4294967295 134512640 134569956 3221224400 3221214424 1131632972 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29860 13073 16 0 210977 0
vsize: 843972
[startup+1040.17 s]
Raw data (loadavg): 1.06 1.02 0.96 2/64 20856
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 100801 83 8 3 25 0 11 0 482531288 864227328 29913 4294967295 134512640 134569956 3221224400 3221214784 1131435124 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29913 13073 16 0 210977 0
vsize: 843972
[startup+1050.17 s]
Raw data (loadavg): 1.05 1.01 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 101790 83 8 3 25 0 11 0 482531288 864227328 29933 4294967295 134512640 134569956 3221224400 3221214760 1131302399 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29933 13073 16 0 210977 0
vsize: 843972
[startup+1060.28 s]
Raw data (loadavg): 1.04 1.01 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 102780 83 8 3 25 0 11 0 482531288 864227328 29985 4294967295 134512640 134569956 3221224400 3221214248 1131631781 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 29985 13073 16 0 210977 0
vsize: 843972
[startup+1070.28 s]
Raw data (loadavg): 1.04 1.01 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 103760 84 8 3 25 0 11 0 482531288 864227328 30039 4294967295 134512640 134569956 3221224400 3221214472 1131631786 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30039 13073 16 0 210977 0
vsize: 843972
[startup+1080.28 s]
Raw data (loadavg): 1.03 1.01 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 104749 84 8 3 25 0 11 0 482531288 864227328 30065 4294967295 134512640 134569956 3221224400 3221214412 1131633190 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30065 13073 16 0 210977 0
vsize: 843972
[startup+1090.28 s]
Raw data (loadavg): 1.02 1.01 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 105718 84 8 3 25 0 11 0 482531288 864227328 30140 4294967295 134512640 134569956 3221224400 3221213672 1085679526 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30140 13073 16 0 210977 0
vsize: 843972
[startup+1100.28 s]
Raw data (loadavg): 1.02 1.01 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 106708 85 8 3 25 0 11 0 482531288 864227328 30162 4294967295 134512640 134569956 3221224400 3221213952 1085632310 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30162 13073 16 0 210977 0
vsize: 843972
[startup+1110.28 s]
Raw data (loadavg): 1.02 1.01 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 107676 85 8 3 25 0 11 0 482531288 864227328 30233 4294967295 134512640 134569956 3221224400 3221213920 1131631996 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30233 13073 16 0 210977 0
vsize: 843972
[startup+1120.28 s]
Raw data (loadavg): 1.01 1.01 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 108666 85 8 3 25 0 11 0 482531288 864227328 30250 4294967295 134512640 134569956 3221224400 3221214536 1131461742 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30250 13073 16 0 210977 0
vsize: 843972
[startup+1130.28 s]
Raw data (loadavg): 1.01 1.01 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 109644 85 8 3 25 0 11 0 482531288 864227328 30296 4294967295 134512640 134569956 3221224400 3221214760 1131307812 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30296 13073 16 0 210977 0
vsize: 843972
[startup+1140.28 s]
Raw data (loadavg): 1.01 1.01 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 110622 85 8 3 25 0 11 0 482531288 864227328 30350 4294967295 134512640 134569956 3221224400 3221214352 1131631381 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30350 13073 16 0 210977 0
vsize: 843972
[startup+1150.28 s]
Raw data (loadavg): 1.01 1.00 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 111601 86 8 3 25 0 11 0 482531288 864227328 30403 4294967295 134512640 134569956 3221224400 3221214760 1131306694 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30403 13073 16 0 210977 0
vsize: 843972
[startup+1160.28 s]
Raw data (loadavg): 1.01 1.00 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 112569 86 8 3 25 0 11 0 482531288 864227328 30492 4294967295 134512640 134569956 3221224400 3221213892 1085616768 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30492 13073 16 0 210977 0
vsize: 843972
[startup+1170.28 s]
Raw data (loadavg): 1.00 1.00 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 113547 86 8 3 25 0 11 0 482531288 864227328 30562 4294967295 134512640 134569956 3221224400 3221214080 1131631996 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30562 13073 16 0 210977 0
vsize: 843972
[startup+1180.28 s]
Raw data (loadavg): 1.00 1.00 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 114537 86 8 3 25 0 11 0 482531288 864227328 30562 4294967295 134512640 134569956 3221224400 3221214520 1131631381 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30562 13073 16 0 210977 0
vsize: 843972
[startup+1190.28 s]
Raw data (loadavg): 1.00 1.00 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 115515 87 8 3 25 0 11 0 482531288 864227328 30594 4294967295 134512640 134569956 3221224400 3221214360 1131631849 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30594 13073 16 0 210977 0
vsize: 843972
[startup+1200.28 s]
Raw data (loadavg): 1.00 1.00 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 116515 87 8 3 25 0 11 0 482531288 864227328 30594 4294967295 134512640 134569956 3221224400 3221214472 1131631996 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210993 30594 13073 16 0 210977 0
vsize: 843972
[startup+1210.28 s]
Raw data (loadavg): 1.00 1.00 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 117504 87 8 3 25 0 11 0 482531288 864227328 30636 4294967295 134512640 134569956 3221224400 3221213912 1131631983 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30636 13073 16 0 210977 0
vsize: 843972
[startup+1220.28 s]
Raw data (loadavg): 1.00 1.00 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 118493 88 8 3 25 0 11 0 482531288 864227328 30678 4294967295 134512640 134569956 3221224400 3221214760 1131302586 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30678 13073 16 0 210977 0
vsize: 843972
[startup+1230.28 s]
Raw data (loadavg): 1.00 1.00 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 119481 88 8 3 25 0 11 0 482531288 864227328 30706 4294967295 134512640 134569956 3221224400 3221214760 1131307738 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30706 13073 16 0 210977 0
vsize: 843972
[startup+1240.28 s]
Raw data (loadavg): 1.00 1.00 0.96 2/64 20857
Raw data (stat): 20577 (java) R 20576 25347 25346 0 -1 0 18089 8 1 0 120459 88 8 3 25 0 11 0 482531288 864227328 30743 4294967295 134512640 134569956 3221224400 3221214232 1131627158 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210993 30743 13073 16 0 210977 0
vsize: 843972
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1240.36 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 20859
Raw data (stat): 20577 (java) Z 20576 25347 25346 0 -1 1036 18089 21480 1 0 120461 94 5041 56 25 0 1 0 482531288 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): 1240.36
CPU time (s): 1256.53
CPU user time (s): 1255.03
CPU system time (s): 1.50277
CPU usage (%): 101.304
Max. virtual memory (Kb): 852020
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####