Some explanations

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

General information on the benchmark

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-bell5.opb
MD5SUM69f4cc43076dd783d9debfd1c0708aef
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2147483647
Optimality of the best value was proved NO
Number of terms in the objective function 1268
Biggest coefficient in the objective function 50331648000000000
Number of bits for the biggest coefficient in the objective function 56
Sum of the numbers in the objective function 888722133694353611
Number of bits of the sum of numbers in the objective function 60
Biggest number in a constraint 50331648000000000
Number of bits of the biggest number in a constraint 56
Biggest sum of numbers in a constraint 888722133694353611
Number of bits of the biggest sum of numbers60
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1234.3
Number of variables1704
Total number of constraints149
Number of constraints which are clauses15
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints104
Minimum length of a constraint1
Maximum length of a constraint135

Trace number 16493 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        698828 kB
Buffers:         25568 kB
Cached:         281940 kB
SwapCached:        464 kB
Active:          56944 kB
Inactive:       252696 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        698576 kB
SwapTotal:     2097892 kB
SwapFree:      2096700 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            20340 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 07:51:45 (client local time) WITH STATUS 143 IN 1283.99 SECONDS
stats: 13230 7 1283.99 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-bell5.opb
c reading problem 
c [nbvar=1704]
c [nbconstr=149]
c time 2.953
c #vars     1704
c #clauses  119
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=351839417
c Current CPU time (ms) : 9.808
c starts	: 1
c conflicts	: 11
c decisions	: 1188
c propagations	: 2219
c inspects	: 2141
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 11
c root simplifications	: 1
c 
c CURRENT OPTIMUM=-595524717
c Current CPU time (ms) : 34.581
c starts	: 2
c conflicts	: 80
c decisions	: 13131
c propagations	: 23517
c inspects	: 55979
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 80
c root simplifications	: 31
c 
c CURRENT OPTIMUM=-1406827629
c Current CPU time (ms) : 37.466
c starts	: 3
c conflicts	: 81
c decisions	: 14172
c propagations	: 25034
c inspects	: 59766
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 81
c root simplifications	: 32
c 
c CURRENT OPTIMUM=-1523558400
c Current CPU time (ms) : 39.822
c starts	: 4
c conflicts	: 82
c decisions	: 15363
c propagations	: 26599
c inspects	: 64959
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 82
c root simplifications	: 33
c 
c CURRENT OPTIMUM=-1984226872
c Current CPU time (ms) : 42.85
c starts	: 5
c conflicts	: 84
c decisions	: 16634
c propagations	: 28464
c inspects	: 70794
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 34
c 
c CURRENT OPTIMUM=1319387921
c Current CPU time (ms) : 54.696
c starts	: 6
c conflicts	: 93
c decisions	: 20373
c propagations	: 34869
c inspects	: 95895
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 93
c root simplifications	: 40
c 
c CURRENT OPTIMUM=-892394729
c Current CPU time (ms) : 59.099
c starts	: 7
c conflicts	: 96
c decisions	: 21532
c propagations	: 37105
c inspects	: 105210
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 96
c root simplifications	: 43
c 
c CURRENT OPTIMUM=-140725622
c Current CPU time (ms) : 65.534
c starts	: 8
c conflicts	: 100
c decisions	: 22890
c propagations	: 39969
c inspects	: 117115
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 46
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 68.112
c starts	: 9
c conflicts	: 100
c decisions	: 23764
c propagations	: 41483
c inspects	: 121958
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 47
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 70.654
c starts	: 10
c conflicts	: 100
c decisions	: 24638
c propagations	: 42997
c inspects	: 126500
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 48
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 73.22
c starts	: 11
c conflicts	: 100
c decisions	: 25512
c propagations	: 44511
c inspects	: 131042
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 49
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 75.751
c starts	: 12
c conflicts	: 100
c decisions	: 26386
c propagations	: 46025
c inspects	: 135584
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 50
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 78.279
c starts	: 13
c conflicts	: 100
c decisions	: 27260
c propagations	: 47539
c inspects	: 140126
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 51
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 80.845
c starts	: 14
c conflicts	: 100
c decisions	: 28134
c propagations	: 49053
c inspects	: 144669
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 52
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 83.378
c starts	: 15
c conflicts	: 100
c decisions	: 29008
c propagations	: 50567
c inspects	: 149212
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 53
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 85.923
c starts	: 16
c conflicts	: 100
c decisions	: 29882
c propagations	: 52081
c inspects	: 153754
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 54
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 88.509
c starts	: 17
c conflicts	: 100
c decisions	: 30756
c propagations	: 53595
c inspects	: 158297
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 55
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 91.059
c starts	: 18
c conflicts	: 100
c decisions	: 31630
c propagations	: 55109
c inspects	: 162839
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 56
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 93.597
c starts	: 19
c conflicts	: 100
c decisions	: 32504
c propagations	: 56623
c inspects	: 167381
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 57
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 96.182
c starts	: 20
c conflicts	: 100
c decisions	: 33378
c propagations	: 58137
c inspects	: 171923
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 58
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 98.742
c starts	: 21
c conflicts	: 100
c decisions	: 34252
c propagations	: 59651
c inspects	: 176465
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 59
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 101.297
c starts	: 22
c conflicts	: 100
c decisions	: 35126
c propagations	: 61165
c inspects	: 181007
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 60
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 103.886
c starts	: 23
c conflicts	: 100
c decisions	: 36000
c propagations	: 62679
c inspects	: 185549
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 61
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 106.425
c starts	: 24
c conflicts	: 100
c decisions	: 36874
c propagations	: 64193
c inspects	: 190091
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 62
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 108.965
c starts	: 25
c conflicts	: 100
c decisions	: 37748
c propagations	: 65707
c inspects	: 194633
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 63
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 111.552
c starts	: 26
c conflicts	: 100
c decisions	: 38622
c propagations	: 67221
c inspects	: 199176
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 64
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 114.098
c starts	: 27
c conflicts	: 100
c decisions	: 39496
c propagations	: 68735
c inspects	: 203718
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 65
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 116.651
c starts	: 28
c conflicts	: 100
c decisions	: 40370
c propagations	: 70249
c inspects	: 208260
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 66
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 119.243
c starts	: 29
c conflicts	: 100
c decisions	: 41244
c propagations	: 71763
c inspects	: 212802
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 67
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 121.789
c starts	: 30
c conflicts	: 100
c decisions	: 42118
c propagations	: 73277
c inspects	: 217344
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 68
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 124.337
c starts	: 31
c conflicts	: 100
c decisions	: 42992
c propagations	: 74791
c inspects	: 221886
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 69
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 126.926
c starts	: 32
c conflicts	: 100
c decisions	: 43866
c propagations	: 76305
c inspects	: 226428
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 70
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 129.479
c starts	: 33
c conflicts	: 100
c decisions	: 44740
c propagations	: 77819
c inspects	: 230970
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 71
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 132.036
c starts	: 34
c conflicts	: 100
c decisions	: 45614
c propagations	: 79333
c inspects	: 235513
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 72
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 134.629
c starts	: 35
c conflicts	: 100
c decisions	: 46488
c propagations	: 80847
c inspects	: 240055
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 73
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 137.181
c starts	: 36
c conflicts	: 100
c decisions	: 47362
c propagations	: 82361
c inspects	: 244598
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 74
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 139.737
c starts	: 37
c conflicts	: 100
c decisions	: 48236
c propagations	: 83875
c inspects	: 249141
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 75
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 142.33
c starts	: 38
c conflicts	: 100
c decisions	: 49110
c propagations	: 85389
c inspects	: 253684
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 76
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 144.882
c starts	: 39
c conflicts	: 100
c decisions	: 49984
c propagations	: 86903
c inspects	: 258226
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 77
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 147.435
c starts	: 40
c conflicts	: 100
c decisions	: 50858
c propagations	: 88417
c inspects	: 262768
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 78
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 150.026
c starts	: 41
c conflicts	: 100
c decisions	: 51732
c propagations	: 89931
c inspects	: 267310
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 79
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 152.593
c starts	: 42
c conflicts	: 100
c decisions	: 52606
c propagations	: 91445
c inspects	: 271852
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 80
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 155.144
c starts	: 43
c conflicts	: 100
c decisions	: 53480
c propagations	: 92959
c inspects	: 276394
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 81
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 157.749
c starts	: 44
c conflicts	: 100
c decisions	: 54354
c propagations	: 94473
c inspects	: 280936
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 82
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 160.31
c starts	: 45
c conflicts	: 100
c decisions	: 55228
c propagations	: 95987
c inspects	: 285479
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 83
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 162.874
c starts	: 46
c conflicts	: 100
c decisions	: 56102
c propagations	: 97501
c inspects	: 290022
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 84
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 165.483
c starts	: 47
c conflicts	: 100
c decisions	: 56976
c propagations	: 99015
c inspects	: 294564
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 85
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 168.053
c starts	: 48
c conflicts	: 100
c decisions	: 57850
c propagations	: 100529
c inspects	: 299106
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 86
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 170.622
c starts	: 49
c conflicts	: 100
c decisions	: 58724
c propagations	: 102043
c inspects	: 303649
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 87
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 173.245
c starts	: 50
c conflicts	: 100
c decisions	: 59598
c propagations	: 103557
c inspects	: 308191
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 88
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 175.819
c starts	: 51
c conflicts	: 100
c decisions	: 60472
c propagations	: 105071
c inspects	: 312733
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 89
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 178.391
c starts	: 52
c conflicts	: 100
c decisions	: 61346
c propagations	: 106585
c inspects	: 317275
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 90
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 180.998
c starts	: 53
c conflicts	: 100
c decisions	: 62220
c propagations	: 108099
c inspects	: 321817
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 91
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 183.562
c starts	: 54
c conflicts	: 100
c decisions	: 63094
c propagations	: 109613
c inspects	: 326359
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 92
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 186.128
c starts	: 55
c conflicts	: 100
c decisions	: 63968
c propagations	: 111127
c inspects	: 330901
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 93
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 188.745
c starts	: 56
c conflicts	: 100
c decisions	: 64842
c propagations	: 112641
c inspects	: 335443
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 94
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 191.308
c starts	: 57
c conflicts	: 100
c decisions	: 65716
c propagations	: 114155
c inspects	: 339985
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 95
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 193.874
c starts	: 58
c conflicts	: 100
c decisions	: 66590
c propagations	: 115669
c inspects	: 344527
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 96
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 196.48
c starts	: 59
c conflicts	: 100
c decisions	: 67464
c propagations	: 117183
c inspects	: 349069
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 97
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 199.041
c starts	: 60
c conflicts	: 100
c decisions	: 68338
c propagations	: 118697
c inspects	: 353612
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 98
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 201.611
c starts	: 61
c conflicts	: 100
c decisions	: 69212
c propagations	: 120211
c inspects	: 358154
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 99
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 204.207
c starts	: 62
c conflicts	: 100
c decisions	: 70086
c propagations	: 121725
c inspects	: 362696
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 100
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 206.762
c starts	: 63
c conflicts	: 100
c decisions	: 70960
c propagations	: 123239
c inspects	: 367239
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 101
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 209.322
c starts	: 64
c conflicts	: 100
c decisions	: 71834
c propagations	: 124753
c inspects	: 371781
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 102
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 211.913
c starts	: 65
c conflicts	: 100
c decisions	: 72708
c propagations	: 126267
c inspects	: 376323
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 103
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 214.465
c starts	: 66
c conflicts	: 100
c decisions	: 73582
c propagations	: 127781
c inspects	: 380866
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 104
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 217.023
c starts	: 67
c conflicts	: 100
c decisions	: 74456
c propagations	: 129295
c inspects	: 385408
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 105
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 219.61
c starts	: 68
c conflicts	: 100
c decisions	: 75330
c propagations	: 130809
c inspects	: 389950
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 106
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 222.162
c starts	: 69
c conflicts	: 100
c decisions	: 76204
c propagations	: 132323
c inspects	: 394493
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 107
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 224.713
c starts	: 70
c conflicts	: 100
c decisions	: 77078
c propagations	: 133837
c inspects	: 399035
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 108
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 227.307
c starts	: 71
c conflicts	: 100
c decisions	: 77952
c propagations	: 135351
c inspects	: 403578
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 109
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 229.863
c starts	: 72
c conflicts	: 100
c decisions	: 78826
c propagations	: 136865
c inspects	: 408121
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 110
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 232.414
c starts	: 73
c conflicts	: 100
c decisions	: 79700
c propagations	: 138379
c inspects	: 412663
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 111
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 235.008
c starts	: 74
c conflicts	: 100
c decisions	: 80574
c propagations	: 139893
c inspects	: 417206
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 112
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 237.562
c starts	: 75
c conflicts	: 100
c decisions	: 81448
c propagations	: 141407
c inspects	: 421748
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 113
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 240.118
c starts	: 76
c conflicts	: 100
c decisions	: 82322
c propagations	: 142921
c inspects	: 426290
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 114
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 242.713
c starts	: 77
c conflicts	: 100
c decisions	: 83196
c propagations	: 144435
c inspects	: 430832
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 115
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 245.268
c starts	: 78
c conflicts	: 100
c decisions	: 84070
c propagations	: 145949
c inspects	: 435374
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 116
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 247.826
c starts	: 79
c conflicts	: 100
c decisions	: 84944
c propagations	: 147463
c inspects	: 439916
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 117
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 250.441
c starts	: 80
c conflicts	: 100
c decisions	: 85818
c propagations	: 148977
c inspects	: 444458
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 118
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 253.013
c starts	: 81
c conflicts	: 100
c decisions	: 86692
c propagations	: 150491
c inspects	: 449000
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 119
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 255.627
c starts	: 82
c conflicts	: 100
c decisions	: 87566
c propagations	: 152005
c inspects	: 453543
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 120
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 258.196
c starts	: 83
c conflicts	: 100
c decisions	: 88440
c propagations	: 153519
c inspects	: 458085
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 121
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 260.763
c starts	: 84
c conflicts	: 100
c decisions	: 89314
c propagations	: 155033
c inspects	: 462627
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 122
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 263.382
c starts	: 85
c conflicts	: 100
c decisions	: 90188
c propagations	: 156547
c inspects	: 467169
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 123
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 265.954
c starts	: 86
c conflicts	: 100
c decisions	: 91062
c propagations	: 158061
c inspects	: 471711
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 124
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 268.526
c starts	: 87
c conflicts	: 100
c decisions	: 91936
c propagations	: 159575
c inspects	: 476253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 125
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 271.149
c starts	: 88
c conflicts	: 100
c decisions	: 92810
c propagations	: 161089
c inspects	: 480795
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 126
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 273.725
c starts	: 89
c conflicts	: 100
c decisions	: 93684
c propagations	: 162603
c inspects	: 485338
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 127
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 276.306
c starts	: 90
c conflicts	: 100
c decisions	: 94558
c propagations	: 164117
c inspects	: 489880
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 128
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 278.933
c starts	: 91
c conflicts	: 100
c decisions	: 95432
c propagations	: 165631
c inspects	: 494423
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 129
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 281.519
c starts	: 92
c conflicts	: 100
c decisions	: 96306
c propagations	: 167145
c inspects	: 498965
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 130
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 284.102
c starts	: 93
c conflicts	: 100
c decisions	: 97180
c propagations	: 168659
c inspects	: 503508
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 131
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 286.727
c starts	: 94
c conflicts	: 100
c decisions	: 98054
c propagations	: 170173
c inspects	: 508051
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 132
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 288.756
c starts	: 95
c conflicts	: 100
c decisions	: 98928
c propagations	: 171687
c inspects	: 512594
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 133
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 290.784
c starts	: 96
c conflicts	: 100
c decisions	: 99802
c propagations	: 173201
c inspects	: 517136
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 134
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 292.854
c starts	: 97
c conflicts	: 100
c decisions	: 100676
c propagations	: 174715
c inspects	: 521678
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 135
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 294.881
c starts	: 98
c conflicts	: 100
c decisions	: 101550
c propagations	: 176229
c inspects	: 526220
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 136
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 296.908
c starts	: 99
c conflicts	: 100
c decisions	: 102424
c propagations	: 177743
c inspects	: 530763
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 137
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 298.982
c starts	: 100
c conflicts	: 100
c decisions	: 103298
c propagations	: 179257
c inspects	: 535305
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 138
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 301.016
c starts	: 101
c conflicts	: 100
c decisions	: 104172
c propagations	: 180771
c inspects	: 539847
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 139
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 303.044
c starts	: 102
c conflicts	: 100
c decisions	: 105046
c propagations	: 182285
c inspects	: 544390
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 140
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 305.115
c starts	: 103
c conflicts	: 100
c decisions	: 105920
c propagations	: 183799
c inspects	: 548932
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 141
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 307.145
c starts	: 104
c conflicts	: 100
c decisions	: 106794
c propagations	: 185313
c inspects	: 553474
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 142
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 309.176
c starts	: 105
c conflicts	: 100
c decisions	: 107668
c propagations	: 186827
c inspects	: 558016
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 143
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 311.246
c starts	: 106
c conflicts	: 100
c decisions	: 108542
c propagations	: 188341
c inspects	: 562558
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 144
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 313.266
c starts	: 107
c conflicts	: 100
c decisions	: 109416
c propagations	: 189855
c inspects	: 567101
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 145
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 315.294
c starts	: 108
c conflicts	: 100
c decisions	: 110290
c propagations	: 191369
c inspects	: 571643
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 146
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 317.363
c starts	: 109
c conflicts	: 100
c decisions	: 111164
c propagations	: 192883
c inspects	: 576185
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 147
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 319.389
c starts	: 110
c conflicts	: 100
c decisions	: 112038
c propagations	: 194397
c inspects	: 580728
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 148
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 321.413
c starts	: 111
c conflicts	: 100
c decisions	: 112912
c propagations	: 195911
c inspects	: 585270
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 149
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 323.469
c starts	: 112
c conflicts	: 100
c decisions	: 113786
c propagations	: 197425
c inspects	: 589812
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 150
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 325.482
c starts	: 113
c conflicts	: 100
c decisions	: 114660
c propagations	: 198939
c inspects	: 594354
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 151
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 327.497
c starts	: 114
c conflicts	: 100
c decisions	: 115534
c propagations	: 200453
c inspects	: 598896
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 152
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 329.559
c starts	: 115
c conflicts	: 100
c decisions	: 116408
c propagations	: 201967
c inspects	: 603439
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 153
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 331.582
c starts	: 116
c conflicts	: 100
c decisions	: 117282
c propagations	: 203481
c inspects	: 607981
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 154
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 333.604
c starts	: 117
c conflicts	: 100
c decisions	: 118156
c propagations	: 204995
c inspects	: 612524
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 155
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 335.664
c starts	: 118
c conflicts	: 100
c decisions	: 119030
c propagations	: 206509
c inspects	: 617066
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 156
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 337.685
c starts	: 119
c conflicts	: 100
c decisions	: 119904
c propagations	: 208023
c inspects	: 621608
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 157
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 339.709
c starts	: 120
c conflicts	: 100
c decisions	: 120778
c propagations	: 209537
c inspects	: 626151
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 158
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 341.761
c starts	: 121
c conflicts	: 100
c decisions	: 121652
c propagations	: 211051
c inspects	: 630693
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 159
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 343.783
c starts	: 122
c conflicts	: 100
c decisions	: 122526
c propagations	: 212565
c inspects	: 635235
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 160
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 345.796
c starts	: 123
c conflicts	: 100
c decisions	: 123400
c propagations	: 214079
c inspects	: 639777
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 161
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 347.848
c starts	: 124
c conflicts	: 100
c decisions	: 124274
c propagations	: 215593
c inspects	: 644319
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 162
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 349.864
c starts	: 125
c conflicts	: 100
c decisions	: 125148
c propagations	: 217107
c inspects	: 648861
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 163
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 351.879
c starts	: 126
c conflicts	: 100
c decisions	: 126022
c propagations	: 218621
c inspects	: 653403
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 164
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 353.929
c starts	: 127
c conflicts	: 100
c decisions	: 126896
c propagations	: 220135
c inspects	: 657945
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 165
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 355.944
c starts	: 128
c conflicts	: 100
c decisions	: 127770
c propagations	: 221649
c inspects	: 662487
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 166
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 357.965
c starts	: 129
c conflicts	: 100
c decisions	: 128644
c propagations	: 223163
c inspects	: 667030
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 167
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 360.015
c starts	: 130
c conflicts	: 100
c decisions	: 129518
c propagations	: 224677
c inspects	: 671572
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 168
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 362.032
c starts	: 131
c conflicts	: 100
c decisions	: 130392
c propagations	: 226191
c inspects	: 676115
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 169
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 364.056
c starts	: 132
c conflicts	: 100
c decisions	: 131266
c propagations	: 227705
c inspects	: 680658
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 170
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 366.108
c starts	: 133
c conflicts	: 100
c decisions	: 132140
c propagations	: 229219
c inspects	: 685201
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 171
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 368.128
c starts	: 134
c conflicts	: 100
c decisions	: 133014
c propagations	: 230733
c inspects	: 689744
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 172
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 370.148
c starts	: 135
c conflicts	: 100
c decisions	: 133888
c propagations	: 232247
c inspects	: 694287
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 173
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 372.206
c starts	: 136
c conflicts	: 100
c decisions	: 134762
c propagations	: 233761
c inspects	: 698830
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 174
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 374.224
c starts	: 137
c conflicts	: 100
c decisions	: 135636
c propagations	: 235275
c inspects	: 703373
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 175
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 376.246
c starts	: 138
c conflicts	: 100
c decisions	: 136510
c propagations	: 236789
c inspects	: 707915
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 176
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 378.306
c starts	: 139
c conflicts	: 100
c decisions	: 137384
c propagations	: 238303
c inspects	: 712457
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 177
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 380.331
c starts	: 140
c conflicts	: 100
c decisions	: 138258
c propagations	: 239817
c inspects	: 716999
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 178
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 382.352
c starts	: 141
c conflicts	: 100
c decisions	: 139132
c propagations	: 241331
c inspects	: 721541
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 179
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 384.415
c starts	: 142
c conflicts	: 100
c decisions	: 140006
c propagations	: 242845
c inspects	: 726084
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 180
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 386.434
c starts	: 143
c conflicts	: 100
c decisions	: 140880
c propagations	: 244359
c inspects	: 730626
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 181
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 388.494
c starts	: 144
c conflicts	: 100
c decisions	: 141754
c propagations	: 245873
c inspects	: 735169
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 182
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 390.513
c starts	: 145
c conflicts	: 100
c decisions	: 142628
c propagations	: 247387
c inspects	: 739711
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 183
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 392.535
c starts	: 146
c conflicts	: 100
c decisions	: 143502
c propagations	: 248901
c inspects	: 744253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 184
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 394.6
c starts	: 147
c conflicts	: 100
c decisions	: 144376
c propagations	: 250415
c inspects	: 748795
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 185
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 396.61
c starts	: 148
c conflicts	: 100
c decisions	: 145250
c propagations	: 251929
c inspects	: 753338
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 186
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 398.636
c starts	: 149
c conflicts	: 100
c decisions	: 146124
c propagations	: 253443
c inspects	: 757881
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 187
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 400.698
c starts	: 150
c conflicts	: 100
c decisions	: 146998
c propagations	: 254957
c inspects	: 762423
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 188
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 402.717
c starts	: 151
c conflicts	: 100
c decisions	: 147872
c propagations	: 256471
c inspects	: 766965
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 189
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 404.754
c starts	: 152
c conflicts	: 100
c decisions	: 148746
c propagations	: 257985
c inspects	: 771508
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 190
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 406.85
c starts	: 153
c conflicts	: 100
c decisions	: 149620
c propagations	: 259499
c inspects	: 776050
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 191
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 408.907
c starts	: 154
c conflicts	: 100
c decisions	: 150494
c propagations	: 261013
c inspects	: 780592
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 192
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 410.949
c starts	: 155
c conflicts	: 100
c decisions	: 151368
c propagations	: 262527
c inspects	: 785135
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 193
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 413.043
c starts	: 156
c conflicts	: 100
c decisions	: 152242
c propagations	: 264041
c inspects	: 789677
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 194
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 415.091
c starts	: 157
c conflicts	: 100
c decisions	: 153116
c propagations	: 265555
c inspects	: 794219
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 195
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 417.143
c starts	: 158
c conflicts	: 100
c decisions	: 153990
c propagations	: 267069
c inspects	: 798761
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 196
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 419.234
c starts	: 159
c conflicts	: 100
c decisions	: 154864
c propagations	: 268583
c inspects	: 803303
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 197
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 421.296
c starts	: 160
c conflicts	: 100
c decisions	: 155738
c propagations	: 270097
c inspects	: 807845
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 198
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 423.362
c starts	: 161
c conflicts	: 100
c decisions	: 156612
c propagations	: 271611
c inspects	: 812387
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 199
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 425.48
c starts	: 162
c conflicts	: 100
c decisions	: 157486
c propagations	: 273125
c inspects	: 816930
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 200
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 427.551
c starts	: 163
c conflicts	: 100
c decisions	: 158360
c propagations	: 274639
c inspects	: 821472
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 201
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 429.619
c starts	: 164
c conflicts	: 100
c decisions	: 159234
c propagations	: 276153
c inspects	: 826014
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 202
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 431.734
c starts	: 165
c conflicts	: 100
c decisions	: 160108
c propagations	: 277667
c inspects	: 830557
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 203
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 433.793
c starts	: 166
c conflicts	: 100
c decisions	: 160982
c propagations	: 279181
c inspects	: 835100
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 204
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 435.821
c starts	: 167
c conflicts	: 100
c decisions	: 161856
c propagations	: 280695
c inspects	: 839642
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 205
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 437.896
c starts	: 168
c conflicts	: 100
c decisions	: 162730
c propagations	: 282209
c inspects	: 844184
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 206
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 439.925
c starts	: 169
c conflicts	: 100
c decisions	: 163604
c propagations	: 283723
c inspects	: 848727
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 207
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 441.955
c starts	: 170
c conflicts	: 100
c decisions	: 164478
c propagations	: 285237
c inspects	: 853269
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 208
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 444.017
c starts	: 171
c conflicts	: 100
c decisions	: 165352
c propagations	: 286751
c inspects	: 857811
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 209
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 446.05
c starts	: 172
c conflicts	: 100
c decisions	: 166226
c propagations	: 288265
c inspects	: 862353
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 210
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 448.086
c starts	: 173
c conflicts	: 100
c decisions	: 167100
c propagations	: 289779
c inspects	: 866896
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 211
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 450.153
c starts	: 174
c conflicts	: 100
c decisions	: 167974
c propagations	: 291293
c inspects	: 871439
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 212
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 452.178
c starts	: 175
c conflicts	: 100
c decisions	: 168848
c propagations	: 292807
c inspects	: 875982
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 213
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 454.219
c starts	: 176
c conflicts	: 100
c decisions	: 169722
c propagations	: 294321
c inspects	: 880525
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 214
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 456.298
c starts	: 177
c conflicts	: 100
c decisions	: 170596
c propagations	: 295835
c inspects	: 885067
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 215
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 458.324
c starts	: 178
c conflicts	: 100
c decisions	: 171470
c propagations	: 297349
c inspects	: 889609
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 216
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 460.354
c starts	: 179
c conflicts	: 100
c decisions	: 172344
c propagations	: 298863
c inspects	: 894151
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 217
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 462.428
c starts	: 180
c conflicts	: 100
c decisions	: 173218
c propagations	: 300377
c inspects	: 898693
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 218
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 464.461
c starts	: 181
c conflicts	: 100
c decisions	: 174092
c propagations	: 301891
c inspects	: 903235
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 219
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 466.494
c starts	: 182
c conflicts	: 100
c decisions	: 174966
c propagations	: 303405
c inspects	: 907777
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 220
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 468.577
c starts	: 183
c conflicts	: 100
c decisions	: 175840
c propagations	: 304919
c inspects	: 912320
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 221
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 470.621
c starts	: 184
c conflicts	: 100
c decisions	: 176714
c propagations	: 306433
c inspects	: 916863
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 222
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 472.662
c starts	: 185
c conflicts	: 100
c decisions	: 177588
c propagations	: 307947
c inspects	: 921405
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 223
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 474.749
c starts	: 186
c conflicts	: 100
c decisions	: 178462
c propagations	: 309461
c inspects	: 925947
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 224
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 476.79
c starts	: 187
c conflicts	: 100
c decisions	: 179336
c propagations	: 310975
c inspects	: 930490
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 225
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 478.88
c starts	: 188
c conflicts	: 100
c decisions	: 180210
c propagations	: 312489
c inspects	: 935033
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 226
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 480.924
c starts	: 189
c conflicts	: 100
c decisions	: 181084
c propagations	: 314003
c inspects	: 939575
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 227
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 482.978
c starts	: 190
c conflicts	: 100
c decisions	: 181958
c propagations	: 315517
c inspects	: 944117
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 228
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 485.092
c starts	: 191
c conflicts	: 100
c decisions	: 182832
c propagations	: 317031
c inspects	: 948659
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 229
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 487.159
c starts	: 192
c conflicts	: 100
c decisions	: 183706
c propagations	: 318545
c inspects	: 953202
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 230
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 489.22
c starts	: 193
c conflicts	: 100
c decisions	: 184580
c propagations	: 320059
c inspects	: 957744
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 231
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 491.348
c starts	: 194
c conflicts	: 100
c decisions	: 185454
c propagations	: 321573
c inspects	: 962287
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 232
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 493.416
c starts	: 195
c conflicts	: 100
c decisions	: 186328
c propagations	: 323087
c inspects	: 966830
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 233
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 495.481
c starts	: 196
c conflicts	: 100
c decisions	: 187202
c propagations	: 324601
c inspects	: 971372
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 234
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 497.602
c starts	: 197
c conflicts	: 100
c decisions	: 188076
c propagations	: 326115
c inspects	: 975914
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 235
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 499.668
c starts	: 198
c conflicts	: 100
c decisions	: 188950
c propagations	: 327629
c inspects	: 980456
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 236
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 501.736
c starts	: 199
c conflicts	: 100
c decisions	: 189824
c propagations	: 329143
c inspects	: 984998
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 237
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 503.861
c starts	: 200
c conflicts	: 100
c decisions	: 190698
c propagations	: 330657
c inspects	: 989541
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 238
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 505.918
c starts	: 201
c conflicts	: 100
c decisions	: 191572
c propagations	: 332171
c inspects	: 994083
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 239
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 507.981
c starts	: 202
c conflicts	: 100
c decisions	: 192446
c propagations	: 333685
c inspects	: 998625
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 240
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 510.095
c starts	: 203
c conflicts	: 100
c decisions	: 193320
c propagations	: 335199
c inspects	: 1003168
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 241
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 512.156
c starts	: 204
c conflicts	: 100
c decisions	: 194194
c propagations	: 336713
c inspects	: 1007711
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 242
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 514.211
c starts	: 205
c conflicts	: 100
c decisions	: 195068
c propagations	: 338227
c inspects	: 1012253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 243
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 516.298
c starts	: 206
c conflicts	: 100
c decisions	: 195942
c propagations	: 339741
c inspects	: 1016796
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 244
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 518.34
c starts	: 207
c conflicts	: 100
c decisions	: 196816
c propagations	: 341255
c inspects	: 1021339
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 245
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 520.387
c starts	: 208
c conflicts	: 100
c decisions	: 197690
c propagations	: 342769
c inspects	: 1025881
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 246
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 522.468
c starts	: 209
c conflicts	: 100
c decisions	: 198564
c propagations	: 344283
c inspects	: 1030423
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 247
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 524.513
c starts	: 210
c conflicts	: 100
c decisions	: 199438
c propagations	: 345797
c inspects	: 1034966
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 248
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 526.552
c starts	: 211
c conflicts	: 100
c decisions	: 200312
c propagations	: 347311
c inspects	: 1039508
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 249
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 528.648
c starts	: 212
c conflicts	: 100
c decisions	: 201186
c propagations	: 348825
c inspects	: 1044051
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 250
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 530.692
c starts	: 213
c conflicts	: 100
c decisions	: 202060
c propagations	: 350339
c inspects	: 1048593
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 251
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 532.749
c starts	: 214
c conflicts	: 100
c decisions	: 202934
c propagations	: 351853
c inspects	: 1053135
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 252
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 534.839
c starts	: 215
c conflicts	: 100
c decisions	: 203808
c propagations	: 353367
c inspects	: 1057678
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 253
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 536.888
c starts	: 216
c conflicts	: 100
c decisions	: 204682
c propagations	: 354881
c inspects	: 1062221
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 254
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 538.94
c starts	: 217
c conflicts	: 100
c decisions	: 205556
c propagations	: 356395
c inspects	: 1066763
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 255
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 541.032
c starts	: 218
c conflicts	: 100
c decisions	: 206430
c propagations	: 357909
c inspects	: 1071305
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 256
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 543.079
c starts	: 219
c conflicts	: 100
c decisions	: 207304
c propagations	: 359423
c inspects	: 1075847
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 257
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 545.119
c starts	: 220
c conflicts	: 100
c decisions	: 208178
c propagations	: 360937
c inspects	: 1080390
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 258
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 547.207
c starts	: 221
c conflicts	: 100
c decisions	: 209052
c propagations	: 362451
c inspects	: 1084932
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 259
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 549.246
c starts	: 222
c conflicts	: 100
c decisions	: 209926
c propagations	: 363965
c inspects	: 1089475
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 260
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 551.294
c starts	: 223
c conflicts	: 100
c decisions	: 210800
c propagations	: 365479
c inspects	: 1094018
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 261
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 553.375
c starts	: 224
c conflicts	: 100
c decisions	: 211674
c propagations	: 366993
c inspects	: 1098561
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 262
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 555.426
c starts	: 225
c conflicts	: 100
c decisions	: 212548
c propagations	: 368507
c inspects	: 1103103
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 263
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 557.522
c starts	: 226
c conflicts	: 100
c decisions	: 213422
c propagations	: 370021
c inspects	: 1107646
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 264
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 559.577
c starts	: 227
c conflicts	: 100
c decisions	: 214296
c propagations	: 371535
c inspects	: 1112189
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 265
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 561.619
c starts	: 228
c conflicts	: 100
c decisions	: 215170
c propagations	: 373049
c inspects	: 1116731
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 266
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 563.71
c starts	: 229
c conflicts	: 100
c decisions	: 216044
c propagations	: 374563
c inspects	: 1121274
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 267
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 565.755
c starts	: 230
c conflicts	: 100
c decisions	: 216918
c propagations	: 376077
c inspects	: 1125817
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 268
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 567.795
c starts	: 231
c conflicts	: 100
c decisions	: 217792
c propagations	: 377591
c inspects	: 1130359
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 269
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 569.885
c starts	: 232
c conflicts	: 100
c decisions	: 218666
c propagations	: 379105
c inspects	: 1134901
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 270
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 571.935
c starts	: 233
c conflicts	: 100
c decisions	: 219540
c propagations	: 380619
c inspects	: 1139443
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 271
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 573.981
c starts	: 234
c conflicts	: 100
c decisions	: 220414
c propagations	: 382133
c inspects	: 1143985
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 272
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 576.074
c starts	: 235
c conflicts	: 100
c decisions	: 221288
c propagations	: 383647
c inspects	: 1148528
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 273
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 578.126
c starts	: 236
c conflicts	: 100
c decisions	: 222162
c propagations	: 385161
c inspects	: 1153071
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 274
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 580.177
c starts	: 237
c conflicts	: 100
c decisions	: 223036
c propagations	: 386675
c inspects	: 1157613
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 275
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 582.269
c starts	: 238
c conflicts	: 100
c decisions	: 223910
c propagations	: 388189
c inspects	: 1162155
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 276
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 584.317
c starts	: 239
c conflicts	: 100
c decisions	: 224784
c propagations	: 389703
c inspects	: 1166698
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 277
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 586.362
c starts	: 240
c conflicts	: 100
c decisions	: 225658
c propagations	: 391217
c inspects	: 1171240
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 278
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 588.444
c starts	: 241
c conflicts	: 100
c decisions	: 226532
c propagations	: 392731
c inspects	: 1175782
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 279
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 590.488
c starts	: 242
c conflicts	: 100
c decisions	: 227406
c propagations	: 394245
c inspects	: 1180325
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 280
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 592.531
c starts	: 243
c conflicts	: 100
c decisions	: 228280
c propagations	: 395759
c inspects	: 1184867
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 281
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 594.61
c starts	: 244
c conflicts	: 100
c decisions	: 229154
c propagations	: 397273
c inspects	: 1189410
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 282
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 596.659
c starts	: 245
c conflicts	: 100
c decisions	: 230028
c propagations	: 398787
c inspects	: 1193952
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 283
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 598.706
c starts	: 246
c conflicts	: 100
c decisions	: 230902
c propagations	: 400301
c inspects	: 1198494
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 284
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 600.79
c starts	: 247
c conflicts	: 100
c decisions	: 231776
c propagations	: 401815
c inspects	: 1203037
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 285
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 602.83
c starts	: 248
c conflicts	: 100
c decisions	: 232650
c propagations	: 403329
c inspects	: 1207579
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 286
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 604.877
c starts	: 249
c conflicts	: 100
c decisions	: 233524
c propagations	: 404843
c inspects	: 1212121
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 287
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 606.96
c starts	: 250
c conflicts	: 100
c decisions	: 234398
c propagations	: 406357
c inspects	: 1216664
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 288
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 609.009
c starts	: 251
c conflicts	: 100
c decisions	: 235272
c propagations	: 407871
c inspects	: 1221206
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 289
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 611.053
c starts	: 252
c conflicts	: 100
c decisions	: 236146
c propagations	: 409385
c inspects	: 1225749
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 290
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 613.134
c starts	: 253
c conflicts	: 100
c decisions	: 237020
c propagations	: 410899
c inspects	: 1230291
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 291
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 615.184
c starts	: 254
c conflicts	: 100
c decisions	: 237894
c propagations	: 412413
c inspects	: 1234833
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 292
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 617.228
c starts	: 255
c conflicts	: 100
c decisions	: 238768
c propagations	: 413927
c inspects	: 1239375
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 293
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 619.317
c starts	: 256
c conflicts	: 100
c decisions	: 239642
c propagations	: 415441
c inspects	: 1243917
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 294
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 621.362
c starts	: 257
c conflicts	: 100
c decisions	: 240516
c propagations	: 416955
c inspects	: 1248460
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 295
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 623.413
c starts	: 258
c conflicts	: 100
c decisions	: 241390
c propagations	: 418469
c inspects	: 1253003
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 296
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 625.504
c starts	: 259
c conflicts	: 100
c decisions	: 242264
c propagations	: 419983
c inspects	: 1257545
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 297
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 627.551
c starts	: 260
c conflicts	: 100
c decisions	: 243138
c propagations	: 421497
c inspects	: 1262088
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 298
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 629.6
c starts	: 261
c conflicts	: 100
c decisions	: 244012
c propagations	: 423011
c inspects	: 1266630
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 299
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 631.681
c starts	: 262
c conflicts	: 100
c decisions	: 244886
c propagations	: 424525
c inspects	: 1271172
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 300
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 633.728
c starts	: 263
c conflicts	: 100
c decisions	: 245760
c propagations	: 426039
c inspects	: 1275715
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 301
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 635.816
c starts	: 264
c conflicts	: 100
c decisions	: 246634
c propagations	: 427553
c inspects	: 1280257
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 302
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 637.862
c starts	: 265
c conflicts	: 100
c decisions	: 247508
c propagations	: 429067
c inspects	: 1284799
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 303
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 639.916
c starts	: 266
c conflicts	: 100
c decisions	: 248382
c propagations	: 430581
c inspects	: 1289341
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 304
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 642.009
c starts	: 267
c conflicts	: 100
c decisions	: 249256
c propagations	: 432095
c inspects	: 1293883
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 305
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 644.059
c starts	: 268
c conflicts	: 100
c decisions	: 250130
c propagations	: 433609
c inspects	: 1298425
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 306
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 646.105
c starts	: 269
c conflicts	: 100
c decisions	: 251004
c propagations	: 435123
c inspects	: 1302967
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 307
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 648.204
c starts	: 270
c conflicts	: 100
c decisions	: 251878
c propagations	: 436637
c inspects	: 1307509
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 308
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 650.26
c starts	: 271
c conflicts	: 100
c decisions	: 252752
c propagations	: 438151
c inspects	: 1312052
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 309
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 652.317
c starts	: 272
c conflicts	: 100
c decisions	: 253626
c propagations	: 439665
c inspects	: 1316595
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 310
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 654.413
c starts	: 273
c conflicts	: 100
c decisions	: 254500
c propagations	: 441179
c inspects	: 1321137
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 311
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 656.466
c starts	: 274
c conflicts	: 100
c decisions	: 255374
c propagations	: 442693
c inspects	: 1325679
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 312
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 658.519
c starts	: 275
c conflicts	: 100
c decisions	: 256248
c propagations	: 444207
c inspects	: 1330221
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 313
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 660.614
c starts	: 276
c conflicts	: 100
c decisions	: 257122
c propagations	: 445721
c inspects	: 1334763
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 314
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 662.673
c starts	: 277
c conflicts	: 100
c decisions	: 257996
c propagations	: 447235
c inspects	: 1339305
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 315
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 664.736
c starts	: 278
c conflicts	: 100
c decisions	: 258870
c propagations	: 448749
c inspects	: 1343847
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 316
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 666.833
c starts	: 279
c conflicts	: 100
c decisions	: 259744
c propagations	: 450263
c inspects	: 1348389
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 317
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 668.881
c starts	: 280
c conflicts	: 100
c decisions	: 260618
c propagations	: 451777
c inspects	: 1352931
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 318
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 670.934
c starts	: 281
c conflicts	: 100
c decisions	: 261492
c propagations	: 453291
c inspects	: 1357474
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 319
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 673.023
c starts	: 282
c conflicts	: 100
c decisions	: 262366
c propagations	: 454805
c inspects	: 1362016
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 320
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 675.075
c starts	: 283
c conflicts	: 100
c decisions	: 263240
c propagations	: 456319
c inspects	: 1366559
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 321
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 677.136
c starts	: 284
c conflicts	: 100
c decisions	: 264114
c propagations	: 457833
c inspects	: 1371101
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 322
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 679.241
c starts	: 285
c conflicts	: 100
c decisions	: 264988
c propagations	: 459347
c inspects	: 1375644
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 323
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 681.296
c starts	: 286
c conflicts	: 100
c decisions	: 265862
c propagations	: 460861
c inspects	: 1380186
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 324
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 683.354
c starts	: 287
c conflicts	: 100
c decisions	: 266736
c propagations	: 462375
c inspects	: 1384729
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 325
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 685.448
c starts	: 288
c conflicts	: 100
c decisions	: 267610
c propagations	: 463889
c inspects	: 1389272
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 326
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 687.505
c starts	: 289
c conflicts	: 100
c decisions	: 268484
c propagations	: 465403
c inspects	: 1393815
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 327
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 689.561
c starts	: 290
c conflicts	: 100
c decisions	: 269358
c propagations	: 466917
c inspects	: 1398358
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 328
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 691.645
c starts	: 291
c conflicts	: 100
c decisions	: 270232
c propagations	: 468431
c inspects	: 1402901
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 329
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 693.696
c starts	: 292
c conflicts	: 100
c decisions	: 271106
c propagations	: 469945
c inspects	: 1407443
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 330
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 695.75
c starts	: 293
c conflicts	: 100
c decisions	: 271980
c propagations	: 471459
c inspects	: 1411985
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 331
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 697.844
c starts	: 294
c conflicts	: 100
c decisions	: 272854
c propagations	: 472973
c inspects	: 1416527
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 332
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 699.901
c starts	: 295
c conflicts	: 100
c decisions	: 273728
c propagations	: 474487
c inspects	: 1421069
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 333
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 702.086
c starts	: 296
c conflicts	: 100
c decisions	: 274602
c propagations	: 476001
c inspects	: 1425611
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 334
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 704.133
c starts	: 297
c conflicts	: 100
c decisions	: 275476
c propagations	: 477515
c inspects	: 1430153
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 335
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 706.194
c starts	: 298
c conflicts	: 100
c decisions	: 276350
c propagations	: 479029
c inspects	: 1434695
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 336
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 708.217
c starts	: 299
c conflicts	: 100
c decisions	: 277224
c propagations	: 480543
c inspects	: 1439238
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 337
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 710.229
c starts	: 300
c conflicts	: 100
c decisions	: 278098
c propagations	: 482057
c inspects	: 1443781
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 338
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 712.243
c starts	: 301
c conflicts	: 100
c decisions	: 278972
c propagations	: 483571
c inspects	: 1448324
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 339
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 714.284
c starts	: 302
c conflicts	: 100
c decisions	: 279846
c propagations	: 485085
c inspects	: 1452866
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 340
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 716.313
c starts	: 303
c conflicts	: 100
c decisions	: 280720
c propagations	: 486599
c inspects	: 1457408
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 341
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 718.343
c starts	: 304
c conflicts	: 100
c decisions	: 281594
c propagations	: 488113
c inspects	: 1461950
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 342
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 720.414
c starts	: 305
c conflicts	: 100
c decisions	: 282468
c propagations	: 489627
c inspects	: 1466493
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 343
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 722.458
c starts	: 306
c conflicts	: 100
c decisions	: 283342
c propagations	: 491141
c inspects	: 1471035
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 344
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 724.508
c starts	: 307
c conflicts	: 100
c decisions	: 284216
c propagations	: 492655
c inspects	: 1475577
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 345
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 726.6
c starts	: 308
c conflicts	: 100
c decisions	: 285090
c propagations	: 494169
c inspects	: 1480119
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 346
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 728.654
c starts	: 309
c conflicts	: 100
c decisions	: 285964
c propagations	: 495683
c inspects	: 1484661
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 347
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 730.711
c starts	: 310
c conflicts	: 100
c decisions	: 286838
c propagations	: 497197
c inspects	: 1489203
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 348
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 732.809
c starts	: 311
c conflicts	: 100
c decisions	: 287712
c propagations	: 498711
c inspects	: 1493745
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 349
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 734.874
c starts	: 312
c conflicts	: 100
c decisions	: 288586
c propagations	: 500225
c inspects	: 1498287
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 350
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 736.941
c starts	: 313
c conflicts	: 100
c decisions	: 289460
c propagations	: 501739
c inspects	: 1502829
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 351
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 739.037
c starts	: 314
c conflicts	: 100
c decisions	: 290334
c propagations	: 503253
c inspects	: 1507371
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 352
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 741.093
c starts	: 315
c conflicts	: 100
c decisions	: 291208
c propagations	: 504767
c inspects	: 1511913
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 353
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 743.153
c starts	: 316
c conflicts	: 100
c decisions	: 292082
c propagations	: 506281
c inspects	: 1516455
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 354
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 745.259
c starts	: 317
c conflicts	: 100
c decisions	: 292956
c propagations	: 507795
c inspects	: 1520997
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 355
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 747.318
c starts	: 318
c conflicts	: 100
c decisions	: 293830
c propagations	: 509309
c inspects	: 1525539
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 356
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 749.383
c starts	: 319
c conflicts	: 100
c decisions	: 294704
c propagations	: 510823
c inspects	: 1530081
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 357
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 751.488
c starts	: 320
c conflicts	: 100
c decisions	: 295578
c propagations	: 512337
c inspects	: 1534623
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 358
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 753.547
c starts	: 321
c conflicts	: 100
c decisions	: 296452
c propagations	: 513851
c inspects	: 1539165
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 359
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 755.655
c starts	: 322
c conflicts	: 100
c decisions	: 297326
c propagations	: 515365
c inspects	: 1543707
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 360
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 757.722
c starts	: 323
c conflicts	: 100
c decisions	: 298200
c propagations	: 516879
c inspects	: 1548249
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 361
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 759.784
c starts	: 324
c conflicts	: 100
c decisions	: 299074
c propagations	: 518393
c inspects	: 1552791
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 362
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 761.903
c starts	: 325
c conflicts	: 100
c decisions	: 299948
c propagations	: 519907
c inspects	: 1557333
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 363
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 763.971
c starts	: 326
c conflicts	: 100
c decisions	: 300822
c propagations	: 521421
c inspects	: 1561875
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 364
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 766.047
c starts	: 327
c conflicts	: 100
c decisions	: 301696
c propagations	: 522935
c inspects	: 1566418
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 365
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 768.168
c starts	: 328
c conflicts	: 100
c decisions	: 302570
c propagations	: 524449
c inspects	: 1570960
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 366
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 770.234
c starts	: 329
c conflicts	: 100
c decisions	: 303444
c propagations	: 525963
c inspects	: 1575503
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 367
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 772.306
c starts	: 330
c conflicts	: 100
c decisions	: 304318
c propagations	: 527477
c inspects	: 1580046
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 368
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 774.416
c starts	: 331
c conflicts	: 100
c decisions	: 305192
c propagations	: 528991
c inspects	: 1584588
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 369
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 776.492
c starts	: 332
c conflicts	: 100
c decisions	: 306066
c propagations	: 530505
c inspects	: 1589130
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 370
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 778.556
c starts	: 333
c conflicts	: 100
c decisions	: 306940
c propagations	: 532019
c inspects	: 1593672
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 371
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 780.671
c starts	: 334
c conflicts	: 100
c decisions	: 307814
c propagations	: 533533
c inspects	: 1598215
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 372
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 782.744
c starts	: 335
c conflicts	: 100
c decisions	: 308688
c propagations	: 535047
c inspects	: 1602757
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 373
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 784.816
c starts	: 336
c conflicts	: 100
c decisions	: 309562
c propagations	: 536561
c inspects	: 1607299
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 374
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 786.926
c starts	: 337
c conflicts	: 100
c decisions	: 310436
c propagations	: 538075
c inspects	: 1611841
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 375
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 788.993
c starts	: 338
c conflicts	: 100
c decisions	: 311310
c propagations	: 539589
c inspects	: 1616384
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 376
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 791.06
c starts	: 339
c conflicts	: 100
c decisions	: 312184
c propagations	: 541103
c inspects	: 1620927
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 377
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 793.164
c starts	: 340
c conflicts	: 100
c decisions	: 313058
c propagations	: 542617
c inspects	: 1625469
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 378
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 795.224
c starts	: 341
c conflicts	: 100
c decisions	: 313932
c propagations	: 544131
c inspects	: 1630011
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 379
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 797.3
c starts	: 342
c conflicts	: 100
c decisions	: 314806
c propagations	: 545645
c inspects	: 1634553
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 380
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 799.399
c starts	: 343
c conflicts	: 100
c decisions	: 315680
c propagations	: 547159
c inspects	: 1639095
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 381
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 801.469
c starts	: 344
c conflicts	: 100
c decisions	: 316554
c propagations	: 548673
c inspects	: 1643638
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 382
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 803.539
c starts	: 345
c conflicts	: 100
c decisions	: 317428
c propagations	: 550187
c inspects	: 1648181
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 383
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 805.645
c starts	: 346
c conflicts	: 100
c decisions	: 318302
c propagations	: 551701
c inspects	: 1652723
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 384
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 807.713
c starts	: 347
c conflicts	: 100
c decisions	: 319176
c propagations	: 553215
c inspects	: 1657265
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 385
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 809.782
c starts	: 348
c conflicts	: 100
c decisions	: 320050
c propagations	: 554729
c inspects	: 1661807
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 386
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 811.888
c starts	: 349
c conflicts	: 100
c decisions	: 320924
c propagations	: 556243
c inspects	: 1666350
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 387
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 813.953
c starts	: 350
c conflicts	: 100
c decisions	: 321798
c propagations	: 557757
c inspects	: 1670892
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 388
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 816.063
c starts	: 351
c conflicts	: 100
c decisions	: 322672
c propagations	: 559271
c inspects	: 1675435
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 389
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 818.137
c starts	: 352
c conflicts	: 100
c decisions	: 323546
c propagations	: 560785
c inspects	: 1679977
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 390
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 820.212
c starts	: 353
c conflicts	: 100
c decisions	: 324420
c propagations	: 562299
c inspects	: 1684519
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 391
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 822.324
c starts	: 354
c conflicts	: 100
c decisions	: 325294
c propagations	: 563813
c inspects	: 1689062
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 392
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 824.399
c starts	: 355
c conflicts	: 100
c decisions	: 326168
c propagations	: 565327
c inspects	: 1693604
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 393
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 826.47
c starts	: 356
c conflicts	: 100
c decisions	: 327042
c propagations	: 566841
c inspects	: 1698146
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 394
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 828.58
c starts	: 357
c conflicts	: 100
c decisions	: 327916
c propagations	: 568355
c inspects	: 1702689
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 395
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 830.653
c starts	: 358
c conflicts	: 100
c decisions	: 328790
c propagations	: 569869
c inspects	: 1707231
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 396
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 832.72
c starts	: 359
c conflicts	: 100
c decisions	: 329664
c propagations	: 571383
c inspects	: 1711773
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 397
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 834.833
c starts	: 360
c conflicts	: 100
c decisions	: 330538
c propagations	: 572897
c inspects	: 1716315
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 398
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 836.904
c starts	: 361
c conflicts	: 100
c decisions	: 331412
c propagations	: 574411
c inspects	: 1720858
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 399
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 838.98
c starts	: 362
c conflicts	: 100
c decisions	: 332286
c propagations	: 575925
c inspects	: 1725400
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 400
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 841.092
c starts	: 363
c conflicts	: 100
c decisions	: 333160
c propagations	: 577439
c inspects	: 1729942
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 401
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 843.171
c starts	: 364
c conflicts	: 100
c decisions	: 334034
c propagations	: 578953
c inspects	: 1734485
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 402
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 845.254
c starts	: 365
c conflicts	: 100
c decisions	: 334908
c propagations	: 580467
c inspects	: 1739027
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 403
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 847.375
c starts	: 366
c conflicts	: 100
c decisions	: 335782
c propagations	: 581981
c inspects	: 1743570
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 404
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 849.453
c starts	: 367
c conflicts	: 100
c decisions	: 336656
c propagations	: 583495
c inspects	: 1748112
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 405
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 851.533
c starts	: 368
c conflicts	: 100
c decisions	: 337530
c propagations	: 585009
c inspects	: 1752654
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 406
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 853.658
c starts	: 369
c conflicts	: 100
c decisions	: 338404
c propagations	: 586523
c inspects	: 1757196
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 407
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 855.732
c starts	: 370
c conflicts	: 100
c decisions	: 339278
c propagations	: 588037
c inspects	: 1761738
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 408
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 857.815
c starts	: 371
c conflicts	: 100
c decisions	: 340152
c propagations	: 589551
c inspects	: 1766281
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 409
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 859.935
c starts	: 372
c conflicts	: 100
c decisions	: 341026
c propagations	: 591065
c inspects	: 1770823
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 410
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 862.016
c starts	: 373
c conflicts	: 100
c decisions	: 341900
c propagations	: 592579
c inspects	: 1775365
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 411
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 864.102
c starts	: 374
c conflicts	: 100
c decisions	: 342774
c propagations	: 594093
c inspects	: 1779907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 412
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 866.236
c starts	: 375
c conflicts	: 100
c decisions	: 343648
c propagations	: 595607
c inspects	: 1784449
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 413
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 868.326
c starts	: 376
c conflicts	: 100
c decisions	: 344522
c propagations	: 597121
c inspects	: 1788991
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 414
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 870.464
c starts	: 377
c conflicts	: 100
c decisions	: 345396
c propagations	: 598635
c inspects	: 1793533
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 415
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 872.551
c starts	: 378
c conflicts	: 100
c decisions	: 346270
c propagations	: 600149
c inspects	: 1798076
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 416
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 874.642
c starts	: 379
c conflicts	: 100
c decisions	: 347144
c propagations	: 601663
c inspects	: 1802619
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 417
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 876.784
c starts	: 380
c conflicts	: 100
c decisions	: 348018
c propagations	: 603177
c inspects	: 1807161
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 418
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 878.884
c starts	: 381
c conflicts	: 100
c decisions	: 348892
c propagations	: 604691
c inspects	: 1811704
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 419
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 880.983
c starts	: 382
c conflicts	: 100
c decisions	: 349766
c propagations	: 606205
c inspects	: 1816246
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 420
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 883.154
c starts	: 383
c conflicts	: 100
c decisions	: 350640
c propagations	: 607719
c inspects	: 1820789
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 421
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 885.284
c starts	: 384
c conflicts	: 100
c decisions	: 351514
c propagations	: 609233
c inspects	: 1825331
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 422
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 887.412
c starts	: 385
c conflicts	: 100
c decisions	: 352388
c propagations	: 610747
c inspects	: 1829873
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 423
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 889.608
c starts	: 386
c conflicts	: 100
c decisions	: 353262
c propagations	: 612261
c inspects	: 1834415
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 424
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 891.743
c starts	: 387
c conflicts	: 100
c decisions	: 354136
c propagations	: 613775
c inspects	: 1838958
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 425
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 893.874
c starts	: 388
c conflicts	: 100
c decisions	: 355010
c propagations	: 615289
c inspects	: 1843501
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 426
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 896.081
c starts	: 389
c conflicts	: 100
c decisions	: 355884
c propagations	: 616803
c inspects	: 1848044
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 427
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 898.219
c starts	: 390
c conflicts	: 100
c decisions	: 356758
c propagations	: 618317
c inspects	: 1852586
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 428
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 900.361
c starts	: 391
c conflicts	: 100
c decisions	: 357632
c propagations	: 619831
c inspects	: 1857129
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 429
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 902.558
c starts	: 392
c conflicts	: 100
c decisions	: 358506
c propagations	: 621345
c inspects	: 1861671
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 430
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 904.692
c starts	: 393
c conflicts	: 100
c decisions	: 359380
c propagations	: 622859
c inspects	: 1866213
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 431
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 906.82
c starts	: 394
c conflicts	: 100
c decisions	: 360254
c propagations	: 624373
c inspects	: 1870756
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 432
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 909.011
c starts	: 395
c conflicts	: 100
c decisions	: 361128
c propagations	: 625887
c inspects	: 1875298
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 433
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 911.135
c starts	: 396
c conflicts	: 100
c decisions	: 362002
c propagations	: 627401
c inspects	: 1879840
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 434
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 913.252
c starts	: 397
c conflicts	: 100
c decisions	: 362876
c propagations	: 628915
c inspects	: 1884383
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 435
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 915.409
c starts	: 398
c conflicts	: 100
c decisions	: 363750
c propagations	: 630429
c inspects	: 1888926
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 436
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 917.506
c starts	: 399
c conflicts	: 100
c decisions	: 364624
c propagations	: 631943
c inspects	: 1893468
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 437
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 919.656
c starts	: 400
c conflicts	: 100
c decisions	: 365498
c propagations	: 633457
c inspects	: 1898010
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 438
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 921.748
c starts	: 401
c conflicts	: 100
c decisions	: 366372
c propagations	: 634971
c inspects	: 1902552
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 439
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 923.847
c starts	: 402
c conflicts	: 100
c decisions	: 367246
c propagations	: 636485
c inspects	: 1907094
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 440
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 925.978
c starts	: 403
c conflicts	: 100
c decisions	: 368120
c propagations	: 637999
c inspects	: 1911636
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 441
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 928.071
c starts	: 404
c conflicts	: 100
c decisions	: 368994
c propagations	: 639513
c inspects	: 1916178
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 442
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 930.163
c starts	: 405
c conflicts	: 100
c decisions	: 369868
c propagations	: 641027
c inspects	: 1920720
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 443
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 932.287
c starts	: 406
c conflicts	: 100
c decisions	: 370742
c propagations	: 642541
c inspects	: 1925263
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 444
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 934.377
c starts	: 407
c conflicts	: 100
c decisions	: 371616
c propagations	: 644055
c inspects	: 1929805
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 445
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 936.463
c starts	: 408
c conflicts	: 100
c decisions	: 372490
c propagations	: 645569
c inspects	: 1934348
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 446
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 938.592
c starts	: 409
c conflicts	: 100
c decisions	: 373364
c propagations	: 647083
c inspects	: 1938890
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 447
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 940.677
c starts	: 410
c conflicts	: 100
c decisions	: 374238
c propagations	: 648597
c inspects	: 1943432
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 448
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 942.766
c starts	: 411
c conflicts	: 100
c decisions	: 375112
c propagations	: 650111
c inspects	: 1947974
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 449
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 944.905
c starts	: 412
c conflicts	: 100
c decisions	: 375986
c propagations	: 651625
c inspects	: 1952517
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 450
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 946.992
c starts	: 413
c conflicts	: 100
c decisions	: 376860
c propagations	: 653139
c inspects	: 1957060
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 451
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 949.074
c starts	: 414
c conflicts	: 100
c decisions	: 377734
c propagations	: 654653
c inspects	: 1961602
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 452
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 951.198
c starts	: 415
c conflicts	: 100
c decisions	: 378608
c propagations	: 656167
c inspects	: 1966145
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 453
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 953.295
c starts	: 416
c conflicts	: 100
c decisions	: 379482
c propagations	: 657681
c inspects	: 1970687
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 454
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 955.392
c starts	: 417
c conflicts	: 100
c decisions	: 380356
c propagations	: 659195
c inspects	: 1975230
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 455
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 957.527
c starts	: 418
c conflicts	: 100
c decisions	: 381230
c propagations	: 660709
c inspects	: 1979772
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 456
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 959.623
c starts	: 419
c conflicts	: 100
c decisions	: 382104
c propagations	: 662223
c inspects	: 1984314
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 457
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 961.721
c starts	: 420
c conflicts	: 100
c decisions	: 382978
c propagations	: 663737
c inspects	: 1988857
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 458
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 963.859
c starts	: 421
c conflicts	: 100
c decisions	: 383852
c propagations	: 665251
c inspects	: 1993399
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 459
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 965.955
c starts	: 422
c conflicts	: 100
c decisions	: 384726
c propagations	: 666765
c inspects	: 1997941
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 460
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 968.09
c starts	: 423
c conflicts	: 100
c decisions	: 385600
c propagations	: 668279
c inspects	: 2002483
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 461
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 970.191
c starts	: 424
c conflicts	: 100
c decisions	: 386474
c propagations	: 669793
c inspects	: 2007025
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 462
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 972.29
c starts	: 425
c conflicts	: 100
c decisions	: 387348
c propagations	: 671307
c inspects	: 2011568
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 463
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 974.439
c starts	: 426
c conflicts	: 100
c decisions	: 388222
c propagations	: 672821
c inspects	: 2016110
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 464
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 976.536
c starts	: 427
c conflicts	: 100
c decisions	: 389096
c propagations	: 674335
c inspects	: 2020653
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 465
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 978.647
c starts	: 428
c conflicts	: 100
c decisions	: 389970
c propagations	: 675849
c inspects	: 2025196
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 466
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 980.792
c starts	: 429
c conflicts	: 100
c decisions	: 390844
c propagations	: 677363
c inspects	: 2029738
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 467
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 982.894
c starts	: 430
c conflicts	: 100
c decisions	: 391718
c propagations	: 678877
c inspects	: 2034281
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 468
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 984.999
c starts	: 431
c conflicts	: 100
c decisions	: 392592
c propagations	: 680391
c inspects	: 2038823
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 469
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 987.14
c starts	: 432
c conflicts	: 100
c decisions	: 393466
c propagations	: 681905
c inspects	: 2043365
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 470
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 989.242
c starts	: 433
c conflicts	: 100
c decisions	: 394340
c propagations	: 683419
c inspects	: 2047907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 471
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 991.344
c starts	: 434
c conflicts	: 100
c decisions	: 395214
c propagations	: 684933
c inspects	: 2052449
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 472
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 993.489
c starts	: 435
c conflicts	: 100
c decisions	: 396088
c propagations	: 686447
c inspects	: 2056992
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 473
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 995.587
c starts	: 436
c conflicts	: 100
c decisions	: 396962
c propagations	: 687961
c inspects	: 2061534
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 474
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 997.683
c starts	: 437
c conflicts	: 100
c decisions	: 397836
c propagations	: 689475
c inspects	: 2066077
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 475
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 999.821
c starts	: 438
c conflicts	: 100
c decisions	: 398710
c propagations	: 690989
c inspects	: 2070620
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 476
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1001.916
c starts	: 439
c conflicts	: 100
c decisions	: 399584
c propagations	: 692503
c inspects	: 2075162
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 477
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1004.013
c starts	: 440
c conflicts	: 100
c decisions	: 400458
c propagations	: 694017
c inspects	: 2079704
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 478
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1006.144
c starts	: 441
c conflicts	: 100
c decisions	: 401332
c propagations	: 695531
c inspects	: 2084246
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 479
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1008.23
c starts	: 442
c conflicts	: 100
c decisions	: 402206
c propagations	: 697045
c inspects	: 2088788
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 480
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1010.326
c starts	: 443
c conflicts	: 100
c decisions	: 403080
c propagations	: 698559
c inspects	: 2093331
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 481
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1012.468
c starts	: 444
c conflicts	: 100
c decisions	: 403954
c propagations	: 700073
c inspects	: 2097874
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 482
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1014.569
c starts	: 445
c conflicts	: 100
c decisions	: 404828
c propagations	: 701587
c inspects	: 2102416
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 483
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1016.715
c starts	: 446
c conflicts	: 100
c decisions	: 405702
c propagations	: 703101
c inspects	: 2106958
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 484
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1018.806
c starts	: 447
c conflicts	: 100
c decisions	: 406576
c propagations	: 704615
c inspects	: 2111500
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 485
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1020.909
c starts	: 448
c conflicts	: 100
c decisions	: 407450
c propagations	: 706129
c inspects	: 2116042
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 486
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1023.065
c starts	: 449
c conflicts	: 100
c decisions	: 408324
c propagations	: 707643
c inspects	: 2120584
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 487
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1025.17
c starts	: 450
c conflicts	: 100
c decisions	: 409198
c propagations	: 709157
c inspects	: 2125126
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 488
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1027.275
c starts	: 451
c conflicts	: 100
c decisions	: 410072
c propagations	: 710671
c inspects	: 2129668
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 489
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1029.42
c starts	: 452
c conflicts	: 100
c decisions	: 410946
c propagations	: 712185
c inspects	: 2134211
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 490
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1031.519
c starts	: 453
c conflicts	: 100
c decisions	: 411820
c propagations	: 713699
c inspects	: 2138753
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 491
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1033.619
c starts	: 454
c conflicts	: 100
c decisions	: 412694
c propagations	: 715213
c inspects	: 2143295
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 492
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1035.765
c starts	: 455
c conflicts	: 100
c decisions	: 413568
c propagations	: 716727
c inspects	: 2147837
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 493
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1037.869
c starts	: 456
c conflicts	: 100
c decisions	: 414442
c propagations	: 718241
c inspects	: 2152380
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 494
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1039.974
c starts	: 457
c conflicts	: 100
c decisions	: 415316
c propagations	: 719755
c inspects	: 2156922
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 495
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1042.113
c starts	: 458
c conflicts	: 100
c decisions	: 416190
c propagations	: 721269
c inspects	: 2161464
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 496
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1044.217
c starts	: 459
c conflicts	: 100
c decisions	: 417064
c propagations	: 722783
c inspects	: 2166007
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 497
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1046.314
c starts	: 460
c conflicts	: 100
c decisions	: 417938
c propagations	: 724297
c inspects	: 2170549
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 498
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1048.455
c starts	: 461
c conflicts	: 100
c decisions	: 418812
c propagations	: 725811
c inspects	: 2175092
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 499
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1050.547
c starts	: 462
c conflicts	: 100
c decisions	: 419686
c propagations	: 727325
c inspects	: 2179634
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 500
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1052.643
c starts	: 463
c conflicts	: 100
c decisions	: 420560
c propagations	: 728839
c inspects	: 2184177
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 501
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1054.786
c starts	: 464
c conflicts	: 100
c decisions	: 421434
c propagations	: 730353
c inspects	: 2188719
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 502
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1056.883
c starts	: 465
c conflicts	: 100
c decisions	: 422308
c propagations	: 731867
c inspects	: 2193261
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 503
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1059.028
c starts	: 466
c conflicts	: 100
c decisions	: 423182
c propagations	: 733381
c inspects	: 2197803
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 504
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1061.136
c starts	: 467
c conflicts	: 100
c decisions	: 424056
c propagations	: 734895
c inspects	: 2202346
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 505
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1063.239
c starts	: 468
c conflicts	: 100
c decisions	: 424930
c propagations	: 736409
c inspects	: 2206888
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 506
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1065.391
c starts	: 469
c conflicts	: 100
c decisions	: 425804
c propagations	: 737923
c inspects	: 2211431
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 507
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1067.496
c starts	: 470
c conflicts	: 100
c decisions	: 426678
c propagations	: 739437
c inspects	: 2215973
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 508
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1069.603
c starts	: 471
c conflicts	: 100
c decisions	: 427552
c propagations	: 740951
c inspects	: 2220516
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 509
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1071.753
c starts	: 472
c conflicts	: 100
c decisions	: 428426
c propagations	: 742465
c inspects	: 2225059
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 510
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1073.863
c starts	: 473
c conflicts	: 100
c decisions	: 429300
c propagations	: 743979
c inspects	: 2229601
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 511
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1075.962
c starts	: 474
c conflicts	: 100
c decisions	: 430174
c propagations	: 745493
c inspects	: 2234143
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 512
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1078.111
c starts	: 475
c conflicts	: 100
c decisions	: 431048
c propagations	: 747007
c inspects	: 2238686
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 513
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1080.216
c starts	: 476
c conflicts	: 100
c decisions	: 431922
c propagations	: 748521
c inspects	: 2243228
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 514
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1082.316
c starts	: 477
c conflicts	: 100
c decisions	: 432796
c propagations	: 750035
c inspects	: 2247770
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 515
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1084.465
c starts	: 478
c conflicts	: 100
c decisions	: 433670
c propagations	: 751549
c inspects	: 2252312
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 516
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1086.578
c starts	: 479
c conflicts	: 100
c decisions	: 434544
c propagations	: 753063
c inspects	: 2256855
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 517
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1088.679
c starts	: 480
c conflicts	: 100
c decisions	: 435418
c propagations	: 754577
c inspects	: 2261398
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 518
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1090.824
c starts	: 481
c conflicts	: 100
c decisions	: 436292
c propagations	: 756091
c inspects	: 2265940
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 519
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1092.933
c starts	: 482
c conflicts	: 100
c decisions	: 437166
c propagations	: 757605
c inspects	: 2270483
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 520
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1095.032
c starts	: 483
c conflicts	: 100
c decisions	: 438040
c propagations	: 759119
c inspects	: 2275026
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 521
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1097.174
c starts	: 484
c conflicts	: 100
c decisions	: 438914
c propagations	: 760633
c inspects	: 2279568
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 522
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1099.274
c starts	: 485
c conflicts	: 100
c decisions	: 439788
c propagations	: 762147
c inspects	: 2284111
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 523
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1101.417
c starts	: 486
c conflicts	: 100
c decisions	: 440662
c propagations	: 763661
c inspects	: 2288653
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 524
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1103.509
c starts	: 487
c conflicts	: 100
c decisions	: 441536
c propagations	: 765175
c inspects	: 2293195
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 525
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1105.616
c starts	: 488
c conflicts	: 100
c decisions	: 442410
c propagations	: 766689
c inspects	: 2297738
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 526
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1107.756
c starts	: 489
c conflicts	: 100
c decisions	: 443284
c propagations	: 768203
c inspects	: 2302281
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 527
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1109.862
c starts	: 490
c conflicts	: 100
c decisions	: 444158
c propagations	: 769717
c inspects	: 2306824
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 528
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1111.961
c starts	: 491
c conflicts	: 100
c decisions	: 445032
c propagations	: 771231
c inspects	: 2311366
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 529
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1114.103
c starts	: 492
c conflicts	: 100
c decisions	: 445906
c propagations	: 772745
c inspects	: 2315909
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 530
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1116.205
c starts	: 493
c conflicts	: 100
c decisions	: 446780
c propagations	: 774259
c inspects	: 2320451
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 531
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1118.308
c starts	: 494
c conflicts	: 100
c decisions	: 447654
c propagations	: 775773
c inspects	: 2324994
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 532
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1120.441
c starts	: 495
c conflicts	: 100
c decisions	: 448528
c propagations	: 777287
c inspects	: 2329536
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 533
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1122.527
c starts	: 496
c conflicts	: 100
c decisions	: 449402
c propagations	: 778801
c inspects	: 2334078
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 534
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1124.622
c starts	: 497
c conflicts	: 100
c decisions	: 450276
c propagations	: 780315
c inspects	: 2338620
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 535
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1126.76
c starts	: 498
c conflicts	: 100
c decisions	: 451150
c propagations	: 781829
c inspects	: 2343163
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 536
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1128.863
c starts	: 499
c conflicts	: 100
c decisions	: 452024
c propagations	: 783343
c inspects	: 2347706
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 537
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1130.961
c starts	: 500
c conflicts	: 100
c decisions	: 452898
c propagations	: 784857
c inspects	: 2352248
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 538
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1133.101
c starts	: 501
c conflicts	: 100
c decisions	: 453772
c propagations	: 786371
c inspects	: 2356791
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 539
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1135.2
c starts	: 502
c conflicts	: 100
c decisions	: 454646
c propagations	: 787885
c inspects	: 2361333
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 540
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1137.299
c starts	: 503
c conflicts	: 100
c decisions	: 455520
c propagations	: 789399
c inspects	: 2365875
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 541
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1139.442
c starts	: 504
c conflicts	: 100
c decisions	: 456394
c propagations	: 790913
c inspects	: 2370418
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 542
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1141.548
c starts	: 505
c conflicts	: 100
c decisions	: 457268
c propagations	: 792427
c inspects	: 2374961
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 543
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1143.709
c starts	: 506
c conflicts	: 100
c decisions	: 458142
c propagations	: 793941
c inspects	: 2379503
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 544
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1145.815
c starts	: 507
c conflicts	: 100
c decisions	: 459016
c propagations	: 795455
c inspects	: 2384046
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 545
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1147.927
c starts	: 508
c conflicts	: 100
c decisions	: 459890
c propagations	: 796969
c inspects	: 2388588
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 546
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1150.072
c starts	: 509
c conflicts	: 100
c decisions	: 460764
c propagations	: 798483
c inspects	: 2393131
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 547
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1152.191
c starts	: 510
c conflicts	: 100
c decisions	: 461638
c propagations	: 799997
c inspects	: 2397674
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 548
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1154.311
c starts	: 511
c conflicts	: 100
c decisions	: 462512
c propagations	: 801511
c inspects	: 2402217
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 549
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1156.462
c starts	: 512
c conflicts	: 100
c decisions	: 463386
c propagations	: 803025
c inspects	: 2406759
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 550
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1158.584
c starts	: 513
c conflicts	: 100
c decisions	: 464260
c propagations	: 804539
c inspects	: 2411302
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 551
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1160.694
c starts	: 514
c conflicts	: 100
c decisions	: 465134
c propagations	: 806053
c inspects	: 2415845
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 552
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1162.844
c starts	: 515
c conflicts	: 100
c decisions	: 466008
c propagations	: 807567
c inspects	: 2420388
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 553
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1164.955
c starts	: 516
c conflicts	: 100
c decisions	: 466882
c propagations	: 809081
c inspects	: 2424931
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 554
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1167.071
c starts	: 517
c conflicts	: 100
c decisions	: 467756
c propagations	: 810595
c inspects	: 2429473
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 555
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1169.221
c starts	: 518
c conflicts	: 100
c decisions	: 468630
c propagations	: 812109
c inspects	: 2434015
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 556
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1171.328
c starts	: 519
c conflicts	: 100
c decisions	: 469504
c propagations	: 813623
c inspects	: 2438557
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 557
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1173.444
c starts	: 520
c conflicts	: 100
c decisions	: 470378
c propagations	: 815137
c inspects	: 2443099
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 558
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1175.585
c starts	: 521
c conflicts	: 100
c decisions	: 471252
c propagations	: 816651
c inspects	: 2447641
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 559
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1177.702
c starts	: 522
c conflicts	: 100
c decisions	: 472126
c propagations	: 818165
c inspects	: 2452183
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 560
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1179.806
c starts	: 523
c conflicts	: 100
c decisions	: 473000
c propagations	: 819679
c inspects	: 2456725
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 561
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1181.956
c starts	: 524
c conflicts	: 100
c decisions	: 473874
c propagations	: 821193
c inspects	: 2461268
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 562
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1184.062
c starts	: 525
c conflicts	: 100
c decisions	: 474748
c propagations	: 822707
c inspects	: 2465810
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 563
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1186.211
c starts	: 526
c conflicts	: 100
c decisions	: 475622
c propagations	: 824221
c inspects	: 2470353
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 564
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1188.327
c starts	: 527
c conflicts	: 100
c decisions	: 476496
c propagations	: 825735
c inspects	: 2474896
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 565
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1190.433
c starts	: 528
c conflicts	: 100
c decisions	: 477370
c propagations	: 827249
c inspects	: 2479438
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 566
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1192.583
c starts	: 529
c conflicts	: 100
c decisions	: 478244
c propagations	: 828763
c inspects	: 2483980
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 567
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1194.692
c starts	: 530
c conflicts	: 100
c decisions	: 479118
c propagations	: 830277
c inspects	: 2488523
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 568
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1196.799
c starts	: 531
c conflicts	: 100
c decisions	: 479992
c propagations	: 831791
c inspects	: 2493065
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 569
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1198.943
c starts	: 532
c conflicts	: 100
c decisions	: 480866
c propagations	: 833305
c inspects	: 2497607
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 570
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1201.052
c starts	: 533
c conflicts	: 100
c decisions	: 481740
c propagations	: 834819
c inspects	: 2502150
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 571
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1203.163
c starts	: 534
c conflicts	: 100
c decisions	: 482614
c propagations	: 836333
c inspects	: 2506692
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 572
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1205.307
c starts	: 535
c conflicts	: 100
c decisions	: 483488
c propagations	: 837847
c inspects	: 2511234
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 573
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1207.405
c starts	: 536
c conflicts	: 100
c decisions	: 484362
c propagations	: 839361
c inspects	: 2515776
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 574
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1209.516
c starts	: 537
c conflicts	: 100
c decisions	: 485236
c propagations	: 840875
c inspects	: 2520318
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 575
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1211.666
c starts	: 538
c conflicts	: 100
c decisions	: 486110
c propagations	: 842389
c inspects	: 2524861
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 576
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1213.776
c starts	: 539
c conflicts	: 100
c decisions	: 486984
c propagations	: 843903
c inspects	: 2529403
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 577
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1215.883
c starts	: 540
c conflicts	: 100
c decisions	: 487858
c propagations	: 845417
c inspects	: 2533945
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 578
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1218.028
c starts	: 541
c conflicts	: 100
c decisions	: 488732
c propagations	: 846931
c inspects	: 2538487
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 579
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1220.133
c starts	: 542
c conflicts	: 100
c decisions	: 489606
c propagations	: 848445
c inspects	: 2543029
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 580
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1222.245
c starts	: 543
c conflicts	: 100
c decisions	: 490480
c propagations	: 849959
c inspects	: 2547572
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 581
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1224.395
c starts	: 544
c conflicts	: 100
c decisions	: 491354
c propagations	: 851473
c inspects	: 2552114
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 582
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1226.507
c starts	: 545
c conflicts	: 100
c decisions	: 492228
c propagations	: 852987
c inspects	: 2556656
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 583
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1228.65
c starts	: 546
c conflicts	: 100
c decisions	: 493102
c propagations	: 854501
c inspects	: 2561198
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 584
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1230.765
c starts	: 547
c conflicts	: 100
c decisions	: 493976
c propagations	: 856015
c inspects	: 2565741
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 585
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1232.886
c starts	: 548
c conflicts	: 100
c decisions	: 494850
c propagations	: 857529
c inspects	: 2570283
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 586
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1235.05
c starts	: 549
c conflicts	: 100
c decisions	: 495724
c propagations	: 859043
c inspects	: 2574825
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 587
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1237.172
c starts	: 550
c conflicts	: 100
c decisions	: 496598
c propagations	: 860557
c inspects	: 2579367
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 588
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1239.299
c starts	: 551
c conflicts	: 100
c decisions	: 497472
c propagations	: 862071
c inspects	: 2583909
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 589
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1241.467
c starts	: 552
c conflicts	: 100
c decisions	: 498346
c propagations	: 863585
c inspects	: 2588452
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 590
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1243.607
c starts	: 553
c conflicts	: 100
c decisions	: 499220
c propagations	: 865099
c inspects	: 2592995
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 591
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1245.731
c starts	: 554
c conflicts	: 100
c decisions	: 500094
c propagations	: 866613
c inspects	: 2597537
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 592
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1247.918
c starts	: 555
c conflicts	: 100
c decisions	: 500968
c propagations	: 868127
c inspects	: 2602080
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 593
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1250.048
c starts	: 556
c conflicts	: 100
c decisions	: 501842
c propagations	: 869641
c inspects	: 2606623
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 594
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1252.178
c starts	: 557
c conflicts	: 100
c decisions	: 502716
c propagations	: 871155
c inspects	: 2611166
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 595
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1254.347
c starts	: 558
c conflicts	: 100
c decisions	: 503590
c propagations	: 872669
c inspects	: 2615709
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 596
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1256.469
c starts	: 559
c conflicts	: 100
c decisions	: 504464
c propagations	: 874183
c inspects	: 2620251
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 597
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1258.6
c starts	: 560
c conflicts	: 100
c decisions	: 505338
c propagations	: 875697
c inspects	: 2624794
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 598
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1260.775
c starts	: 561
c conflicts	: 100
c decisions	: 506212
c propagations	: 877211
c inspects	: 2629337
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 599
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1262.897
c starts	: 562
c conflicts	: 100
c decisions	: 507086
c propagations	: 878725
c inspects	: 2633880
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 600
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1265.055
c starts	: 563
c conflicts	: 100
c decisions	: 507960
c propagations	: 880239
c inspects	: 2638423
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 601
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1267.2
c starts	: 564
c conflicts	: 100
c decisions	: 508834
c propagations	: 881753
c inspects	: 2642966
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 602
c 
c CURRENT OPTIMUM=-2113391460
c Current CPU time (ms) : 1269.326
c starts	: 565
c conflicts	: 100
c decisions	: 509708
c propagations	: 883267
c inspects	: 2647508
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 100
c root simplifications	: 603
#### 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.56 0.82 0.87 2/54 26304
Raw data (stat): 26304 (runsolver) R 26303 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543290429 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.77 0.86 0.88 2/64 26314
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18067 0 1 0 769 38 0 0 25 0 11 0 543290429 857862144 20022 4294967295 134512640 134569956 3221224400 3221214488 1131231932 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209439 20022 13073 16 0 209423 0
vsize: 837756
[startup+20.0024 s]
Raw data (loadavg): 0.89 0.88 0.88 3/64 26315
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18068 4 1 0 1679 38 0 0 25 0 11 0 543290429 862404608 21400 4294967295 134512640 134569956 3221224400 3221214712 1130917143 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210548 21400 13073 16 0 210532 0
vsize: 842192
[startup+30.003 s]
Raw data (loadavg): 0.90 0.89 0.89 2/64 26315
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 2628 39 0 0 25 0 11 0 543290429 861831168 21412 4294967295 134512640 134569956 3221224400 3221214752 1131325093 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210408 21412 13073 16 0 210392 0
vsize: 841632
[startup+40.0038 s]
Raw data (loadavg): 0.92 0.89 0.89 2/64 26317
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 3572 40 0 0 24 0 11 0 543290429 858607616 20881 4294967295 134512640 134569956 3221224400 3221214664 1131227592 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209621 20881 13073 16 0 209605 0
vsize: 838484
[startup+50.005 s]
Raw data (loadavg): 0.93 0.89 0.89 2/64 26319
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 4524 40 0 0 24 0 11 0 543290429 864899072 22623 4294967295 134512640 134569956 3221224400 3221214760 1131268207 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 22623 13073 16 0 211141 0
vsize: 844628
[startup+60.0064 s]
Raw data (loadavg): 0.94 0.89 0.89 2/64 26321
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 5495 40 0 0 25 0 11 0 543290429 864899072 22670 4294967295 134512640 134569956 3221224400 3221214664 1131227769 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 22670 13073 16 0 211141 0
vsize: 844628
[startup+70.0072 s]
Raw data (loadavg): 0.95 0.90 0.89 2/64 26323
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 6465 41 0 0 25 0 11 0 543290429 864899072 22722 4294967295 134512640 134569956 3221224400 3221214632 1131044207 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 22722 13073 16 0 211141 0
vsize: 844628
[startup+80.0077 s]
Raw data (loadavg): 0.96 0.90 0.89 2/64 26327
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 7435 41 0 0 25 0 11 0 543290429 864899072 22885 4294967295 134512640 134569956 3221224400 3221214664 1131227569 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 22885 13073 16 0 211141 0
vsize: 844628
[startup+90.0087 s]
Raw data (loadavg): 0.96 0.90 0.89 2/64 26331
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 8403 42 0 0 25 0 11 0 543290429 864899072 22956 4294967295 134512640 134569956 3221224400 3221214760 1131270375 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 22956 13073 16 0 211141 0
vsize: 844628
[startup+100.01 s]
Raw data (loadavg): 0.97 0.91 0.89 2/64 26335
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 9363 42 0 0 25 0 11 0 543290429 864899072 23043 4294967295 134512640 134569956 3221224400 3221214608 1131526236 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 23043 13073 16 0 211141 0
vsize: 844628
[startup+110.011 s]
Raw data (loadavg): 0.97 0.91 0.89 2/64 26339
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 10325 43 0 0 25 0 11 0 543290429 864899072 23147 4294967295 134512640 134569956 3221224400 3221214664 1131226817 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 23147 13073 16 0 211141 0
vsize: 844628
[startup+120.012 s]
Raw data (loadavg): 0.98 0.91 0.89 2/64 26343
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 11287 43 0 0 25 0 11 0 543290429 864899072 23288 4294967295 134512640 134569956 3221224400 3221214664 1131228110 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 23288 13073 16 0 211141 0
vsize: 844628
[startup+130.012 s]
Raw data (loadavg): 0.98 0.91 0.90 2/64 26346
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 12249 43 1 0 25 0 11 0 543290429 864899072 23440 4294967295 134512640 134569956 3221224400 3221214604 1131526288 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 23440 13073 16 0 211141 0
vsize: 844628
[startup+140.012 s]
Raw data (loadavg): 0.98 0.92 0.90 2/64 26350
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 13212 44 1 0 25 0 11 0 543290429 864899072 23580 4294967295 134512640 134569956 3221224400 3221214664 1131227295 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 23580 13073 16 0 211141 0
vsize: 844628
[startup+150.013 s]
Raw data (loadavg): 0.98 0.92 0.90 2/64 26354
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 14175 44 1 0 25 0 11 0 543290429 864899072 23745 4294967295 134512640 134569956 3221224400 3221214720 1131526264 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 23745 13073 16 0 211141 0
vsize: 844628
[startup+160.014 s]
Raw data (loadavg): 0.99 0.92 0.90 2/64 26358
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 15138 44 1 0 25 0 11 0 543290429 864899072 23873 4294967295 134512640 134569956 3221224400 3221214664 1131227225 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 23873 13073 16 0 211141 0
vsize: 844628
[startup+170.014 s]
Raw data (loadavg): 0.99 0.92 0.90 2/64 26362
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 16097 44 1 1 25 0 11 0 543290429 864899072 23996 4294967295 134512640 134569956 3221224400 3221214520 1085679313 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 23996 13073 16 0 211141 0
vsize: 844628
[startup+180.015 s]
Raw data (loadavg): 0.99 0.92 0.90 2/64 26366
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 17054 45 1 1 25 0 11 0 543290429 864899072 24138 4294967295 134512640 134569956 3221224400 3221214608 1131526156 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 24138 13073 16 0 211141 0
vsize: 844628
[startup+190.016 s]
Raw data (loadavg): 0.99 0.93 0.90 2/64 26370
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 18013 45 2 1 25 0 11 0 543290429 864899072 24295 4294967295 134512640 134569956 3221224400 3221214664 1131227200 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 24295 13073 16 0 211141 0
vsize: 844628
[startup+200.016 s]
Raw data (loadavg): 0.99 0.93 0.90 2/64 26374
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 18973 46 2 1 25 0 11 0 543290429 864899072 24575 4294967295 134512640 134569956 3221224400 3221214764 1131612769 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 24575 13073 16 0 211141 0
vsize: 844628
[startup+210.017 s]
Raw data (loadavg): 0.99 0.93 0.90 2/64 26378
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 19936 46 2 1 25 0 11 0 543290429 864899072 24725 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 24725 13073 16 0 211141 0
vsize: 844628
[startup+220.018 s]
Raw data (loadavg): 0.99 0.93 0.90 2/64 26381
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 20897 46 2 1 25 0 11 0 543290429 864899072 24863 4294967295 134512640 134569956 3221224400 3221214760 1131271186 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 24863 13073 16 0 211141 0
vsize: 844628
[startup+230.017 s]
Raw data (loadavg): 0.99 0.93 0.91 2/64 26385
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 21862 47 2 1 25 0 11 0 543290429 864899072 25000 4294967295 134512640 134569956 3221224400 3221214632 1085679735 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 25000 13073 16 0 211141 0
vsize: 844628
[startup+240.019 s]
Raw data (loadavg): 1.07 0.95 0.91 2/64 26389
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 22827 47 2 1 25 0 11 0 543290429 864899072 25125 4294967295 134512640 134569956 3221224400 3221214608 1131526289 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 25125 13073 16 0 211141 0
vsize: 844628
[startup+250.019 s]
Raw data (loadavg): 1.06 0.95 0.91 2/64 26393
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 23793 47 2 1 25 0 11 0 543290429 864899072 25230 4294967295 134512640 134569956 3221224400 3221214760 1131271116 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 25230 13073 16 0 211141 0
vsize: 844628
[startup+260.021 s]
Raw data (loadavg): 1.05 0.95 0.91 2/64 26397
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 24753 48 2 1 25 0 11 0 543290429 864899072 25358 4294967295 134512640 134569956 3221224400 3221214664 1131228110 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 25358 13073 16 0 211141 0
vsize: 844628
[startup+270.022 s]
Raw data (loadavg): 1.04 0.95 0.91 2/64 26401
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 25711 48 3 1 25 0 11 0 543290429 864899072 25497 4294967295 134512640 134569956 3221224400 3221214652 1131524384 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 25497 13073 16 0 211141 0
vsize: 844628
[startup+280.022 s]
Raw data (loadavg): 1.03 0.96 0.91 2/64 26405
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 26668 48 3 1 25 0 11 0 543290429 864899072 25680 4294967295 134512640 134569956 3221224400 3221214664 1131227467 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 25680 13073 16 0 211141 0
vsize: 844628
[startup+290.022 s]
Raw data (loadavg): 1.03 0.96 0.91 2/64 26409
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 27620 49 3 1 25 0 11 0 543290429 864899072 26062 4294967295 134512640 134569956 3221224400 3221214960 1131179161 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 26062 13073 16 0 211141 0
vsize: 844628
[startup+300.022 s]
Raw data (loadavg): 1.02 0.96 0.91 2/64 26414
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18069 4 1 0 28568 49 3 1 25 0 11 0 543290429 864899072 26228 4294967295 134512640 134569956 3221224400 3221214664 1131228057 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 26228 13073 16 0 211141 0
vsize: 844628
[startup+310.026 s]
Raw data (loadavg): 1.02 0.96 0.91 2/64 26419
Raw data (stat): 26304 (java) S 26303 27222 27221 0 -1 0 18070 4 1 0 29515 49 4 1 25 0 11 0 543290429 864899072 26433 4294967295 134512640 134569956 3221224400 3221213408 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 26433 13073 16 0 211141 0
vsize: 844628
[startup+320.027 s]
Raw data (loadavg): 1.02 0.96 0.91 2/64 26423
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 30461 50 4 1 25 0 11 0 543290429 864899072 26647 4294967295 134512640 134569956 3221224400 3221214744 1131231688 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 26647 13073 16 0 211141 0
vsize: 844628
[startup+330.031 s]
Raw data (loadavg): 1.01 0.96 0.91 2/64 26428
Raw data (stat): 26304 (java) S 26303 27222 27221 0 -1 0 18070 4 1 0 31412 50 4 1 25 0 11 0 543290429 864899072 26858 4294967295 134512640 134569956 3221224400 3221213408 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 26858 13073 16 0 211141 0
vsize: 844628
[startup+340.032 s]
Raw data (loadavg): 1.01 0.96 0.91 2/64 26433
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 32363 51 4 1 25 0 11 0 543290429 864899072 27042 4294967295 134512640 134569956 3221224400 3221214664 1131227234 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 27042 13073 16 0 211141 0
vsize: 844628
[startup+350.036 s]
Raw data (loadavg): 1.01 0.96 0.91 2/64 26438
Raw data (stat): 26304 (java) S 26303 27222 27221 0 -1 0 18070 4 1 0 33318 51 4 1 25 0 11 0 543290429 864899072 27252 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 27252 13073 16 0 211141 0
vsize: 844628
[startup+360.037 s]
Raw data (loadavg): 1.01 0.96 0.91 2/64 26443
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 34273 51 5 1 25 0 11 0 543290429 864899072 27409 4294967295 134512640 134569956 3221224400 3221214760 1131270398 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 27409 13073 16 0 211141 0
vsize: 844628
[startup+370.038 s]
Raw data (loadavg): 1.00 0.96 0.91 2/64 26448
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 35225 51 5 1 24 0 11 0 543290429 864899072 27542 4294967295 134512640 134569956 3221224400 3221214760 1131268476 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 27542 13073 16 0 211141 0
vsize: 844628
[startup+380.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 26453
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 36181 52 5 2 25 0 11 0 543290429 864899072 27708 4294967295 134512640 134569956 3221224400 3221214664 1131227426 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 27708 13073 16 0 211141 0
vsize: 844628
[startup+390.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 26458
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 37133 52 5 2 24 0 11 0 543290429 864899072 27863 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 27863 13073 16 0 211141 0
vsize: 844628
[startup+400.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/64 26463
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 38090 53 5 2 25 0 11 0 543290429 864899072 28014 4294967295 134512640 134569956 3221224400 3221214664 1131228149 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 28014 13073 16 0 211141 0
vsize: 844628
[startup+410.042 s]
Raw data (loadavg): 1.08 0.98 0.92 2/64 26468
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 39041 53 6 2 25 0 11 0 543290429 864899072 28321 4294967295 134512640 134569956 3221224400 3221214664 1131226821 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 28321 13073 16 0 211141 0
vsize: 844628
[startup+420.042 s]
Raw data (loadavg): 1.07 0.98 0.92 2/64 26473
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 39981 53 6 2 25 0 11 0 543290429 864899072 28505 4294967295 134512640 134569956 3221224400 3221214760 1131268392 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 28505 13073 16 0 211141 0
vsize: 844628
[startup+430.042 s]
Raw data (loadavg): 1.06 0.98 0.92 2/64 26477
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 40924 54 6 2 25 0 11 0 543290429 864899072 28719 4294967295 134512640 134569956 3221224400 3221214760 1131268436 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211157 28719 13073 16 0 211141 0
vsize: 844628
[startup+440.042 s]
Raw data (loadavg): 1.05 0.98 0.92 2/64 26482
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 41873 54 6 2 25 0 11 0 543290429 864899072 29262 4294967295 134512640 134569956 3221224400 3221214760 1131269553 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 29262 13073 16 0 211141 0
vsize: 844628
[startup+450.042 s]
Raw data (loadavg): 1.04 0.98 0.92 2/64 26487
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 42825 55 6 2 25 0 11 0 543290429 864899072 29466 4294967295 134512640 134569956 3221224400 3221214760 1131269526 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 29466 13073 16 0 211141 0
vsize: 844628
[startup+460.043 s]
Raw data (loadavg): 1.03 0.98 0.92 2/64 26492
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 43780 55 7 3 25 0 11 0 543290429 864899072 29576 4294967295 134512640 134569956 3221224400 3221214756 1131226796 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 29576 13073 16 0 211141 0
vsize: 844628
[startup+470.043 s]
Raw data (loadavg): 1.03 0.98 0.92 2/64 26497
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 44730 55 7 3 25 0 11 0 543290429 864899072 29753 4294967295 134512640 134569956 3221224400 3221214664 1131227586 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 29753 13073 16 0 211141 0
vsize: 844628
[startup+480.044 s]
Raw data (loadavg): 1.02 0.98 0.92 2/64 26502
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 45680 56 7 3 25 0 11 0 543290429 864899072 29897 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 29897 13073 16 0 211141 0
vsize: 844628
[startup+490.044 s]
Raw data (loadavg): 1.02 0.98 0.92 2/64 26507
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 46623 56 8 3 25 0 11 0 543290429 864899072 30056 4294967295 134512640 134569956 3221224400 3221214664 1131227280 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 30056 13073 16 0 211141 0
vsize: 844628
[startup+500.045 s]
Raw data (loadavg): 1.02 0.98 0.92 2/64 26511
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 47556 56 8 3 25 0 11 0 543290429 864899072 30242 4294967295 134512640 134569956 3221224400 3221214664 1131228164 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 30242 13073 16 0 211141 0
vsize: 844628
[startup+510.046 s]
Raw data (loadavg): 1.01 0.98 0.92 2/64 26516
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 48497 56 8 3 25 0 11 0 543290429 864899072 30475 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 30475 13073 16 0 211141 0
vsize: 844628
[startup+520.047 s]
Raw data (loadavg): 1.01 0.98 0.92 2/64 26521
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 49446 57 9 3 23 0 11 0 543290429 864899072 30790 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 30790 13073 16 0 211141 0
vsize: 844628
[startup+530.046 s]
Raw data (loadavg): 1.01 0.98 0.92 2/64 26526
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 50393 57 9 3 24 0 11 0 543290429 864899072 30983 4294967295 134512640 134569956 3221224400 3221214760 1131271163 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 30983 13073 16 0 211141 0
vsize: 844628
[startup+540.047 s]
Raw data (loadavg): 1.01 0.98 0.92 2/64 26531
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 51344 57 9 3 25 0 11 0 543290429 864899072 31140 4294967295 134512640 134569956 3221224400 3221214664 1131227493 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 31140 13073 16 0 211141 0
vsize: 844628
[startup+550.048 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26536
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 52296 58 9 3 25 0 11 0 543290429 864899072 31352 4294967295 134512640 134569956 3221224400 3221214760 1131268407 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 31352 13073 16 0 211141 0
vsize: 844628
[startup+560.049 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26540
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 53244 58 10 3 25 0 11 0 543290429 864899072 31585 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 31585 13073 16 0 211141 0
vsize: 844628
[startup+570.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26545
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 54197 58 10 3 25 0 11 0 543290429 864899072 31757 4294967295 134512640 134569956 3221224400 3221214664 1131228133 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 31757 13073 16 0 211141 0
vsize: 844628
[startup+580.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26550
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 55150 58 10 3 25 0 11 0 543290429 864899072 31882 4294967295 134512640 134569956 3221224400 3221214760 1131268400 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 31882 13073 16 0 211141 0
vsize: 844628
[startup+590.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26555
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 56101 59 11 4 25 0 11 0 543290429 864899072 32133 4294967295 134512640 134569956 3221224400 3221214760 1131270413 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 32133 13073 16 0 211141 0
vsize: 844628
[startup+600.051 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26560
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 57058 59 11 4 25 0 11 0 543290429 864899072 32278 4294967295 134512640 134569956 3221224400 3221214664 1131227493 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 32278 13073 16 0 211141 0
vsize: 844628
[startup+610.052 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26565
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 58015 59 11 4 25 0 11 0 543290429 864899072 32432 4294967295 134512640 134569956 3221224400 3221214760 1131268400 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 32432 13073 16 0 211141 0
vsize: 844628
[startup+620.053 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26570
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 58968 59 11 4 25 0 11 0 543290429 864899072 32563 4294967295 134512640 134569956 3221224400 3221214664 1131227295 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 32563 13073 16 0 211141 0
vsize: 844628
[startup+630.053 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26574
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 59924 60 11 4 25 0 11 0 543290429 864899072 32740 4294967295 134512640 134569956 3221224400 3221214664 1131226828 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 32740 13073 16 0 211141 0
vsize: 844628
[startup+640.054 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26579
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 60878 60 12 4 24 0 11 0 543290429 864899072 32857 4294967295 134512640 134569956 3221224400 3221214664 1131228226 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 32857 13073 16 0 211141 0
vsize: 844628
[startup+650.055 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26584
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 61834 60 12 4 23 0 11 0 543290429 864899072 32974 4294967295 134512640 134569956 3221224400 3221214760 1131268407 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 32974 13073 16 0 211141 0
vsize: 844628
[startup+660.056 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26589
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 62788 60 12 4 25 0 11 0 543290429 864899072 33089 4294967295 134512640 134569956 3221224400 3221214664 1131226821 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 33089 13073 16 0 211141 0
vsize: 844628
[startup+670.057 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26594
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 63739 60 12 4 24 0 11 0 543290429 864899072 33285 4294967295 134512640 134569956 3221224400 3221214760 1131270471 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 33285 13073 16 0 211141 0
vsize: 844628
[startup+680.057 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26599
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 64694 61 13 4 25 0 11 0 543290429 864899072 33439 4294967295 134512640 134569956 3221224400 3221214760 1131269526 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 33439 13073 16 0 211141 0
vsize: 844628
[startup+690.057 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26603
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 65649 61 13 4 25 0 11 0 543290429 864899072 33605 4294967295 134512640 134569956 3221224400 3221214664 1131227218 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 33605 13073 16 0 211141 0
vsize: 844628
[startup+700.058 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26608
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 66602 61 13 4 24 0 11 0 543290429 864899072 33715 4294967295 134512640 134569956 3221224400 3221214760 1131270445 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 33715 13073 16 0 211141 0
vsize: 844628
[startup+710.058 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26613
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 67564 62 13 5 25 0 11 0 543290429 864899072 35402 4294967295 134512640 134569956 3221224400 3221214760 1131269670 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 35402 13073 16 0 211141 0
vsize: 844628
[startup+720.059 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26618
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 68538 62 13 5 25 0 11 0 543290429 864899072 35402 4294967295 134512640 134569956 3221224400 3221214664 1131227022 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 35402 13073 16 0 211141 0
vsize: 844628
[startup+730.058 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26623
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 69497 63 13 5 25 0 11 0 543290429 864899072 35426 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 35426 13073 16 0 211141 0
vsize: 844628
[startup+740.059 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26628
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 70453 63 14 5 25 0 11 0 543290429 864899072 35557 4294967295 134512640 134569956 3221224400 3221214664 1131228184 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 35557 13073 16 0 211141 0
vsize: 844628
[startup+750.06 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26633
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 71408 63 14 5 25 0 11 0 543290429 864899072 35726 4294967295 134512640 134569956 3221224400 3221214800 1131474077 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 35726 13073 16 0 211141 0
vsize: 844628
[startup+760.061 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26637
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 72358 64 14 5 25 0 11 0 543290429 864899072 35835 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 35835 13073 16 0 211141 0
vsize: 844628
[startup+770.061 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26642
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 73311 64 15 5 25 0 11 0 543290429 864899072 35990 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 35990 13073 16 0 211141 0
vsize: 844628
[startup+780.061 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26647
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 74264 65 15 5 25 0 11 0 543290429 864899072 36171 4294967295 134512640 134569956 3221224400 3221214664 1131227732 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 36171 13073 16 0 211141 0
vsize: 844628
[startup+790.062 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26652
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 75219 65 15 5 25 0 11 0 543290429 864899072 36327 4294967295 134512640 134569956 3221224400 3221214664 1131227285 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 36327 13073 16 0 211141 0
vsize: 844628
[startup+800.063 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26657
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 76172 65 15 5 25 0 11 0 543290429 864899072 36514 4294967295 134512640 134569956 3221224400 3221214800 1131474928 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 36514 13073 16 0 211141 0
vsize: 844628
[startup+810.064 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26661
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 77128 65 15 6 25 0 11 0 543290429 864899072 36670 4294967295 134512640 134569956 3221224400 3221214664 1131226817 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 36670 13073 16 0 211141 0
vsize: 844628
[startup+820.065 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26666
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 78083 66 15 6 25 0 11 0 543290429 864899072 36782 4294967295 134512640 134569956 3221224400 3221214756 1131226796 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 36782 13073 16 0 211141 0
vsize: 844628
[startup+830.067 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26671
Raw data (stat): 26304 (java) S 26303 27222 27221 0 -1 0 18070 4 1 0 79039 66 16 6 25 0 11 0 543290429 864899072 36902 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 36902 13073 16 0 211141 0
vsize: 844628
[startup+840.068 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26676
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 79990 66 16 6 25 0 11 0 543290429 864899072 37060 4294967295 134512640 134569956 3221224400 3221214960 1131179161 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 37060 13073 16 0 211141 0
vsize: 844628
[startup+850.069 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26680
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 80943 67 16 6 25 0 11 0 543290429 864899072 37215 4294967295 134512640 134569956 3221224400 3221214664 1131227322 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 37215 13073 16 0 211141 0
vsize: 844628
[startup+860.07 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26685
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 81894 67 16 6 25 0 11 0 543290429 864899072 37350 4294967295 134512640 134569956 3221224400 3221214664 1131226821 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 37350 13073 16 0 211141 0
vsize: 844628
[startup+870.071 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26690
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 82844 68 17 6 25 0 11 0 543290429 864899072 37544 4294967295 134512640 134569956 3221224400 3221214664 1131226821 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 37544 13073 16 0 211141 0
vsize: 844628
[startup+880.07 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26695
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 83791 68 17 6 25 0 11 0 543290429 864899072 37712 4294967295 134512640 134569956 3221224400 3221214760 1131269526 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 37712 13073 16 0 211141 0
vsize: 844628
[startup+890.074 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26699
Raw data (stat): 26304 (java) S 26303 27222 27221 0 -1 0 18070 4 1 0 84722 68 17 6 25 0 11 0 543290429 864899072 37869 4294967295 134512640 134569956 3221224400 3221213408 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 37869 13073 16 0 211141 0
vsize: 844628
[startup+900.075 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26704
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 85646 69 17 6 25 0 11 0 543290429 864899072 38013 4294967295 134512640 134569956 3221224400 3221214960 1131179161 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 38013 13073 16 0 211141 0
vsize: 844628
[startup+910.077 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26709
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 86573 69 18 7 25 0 11 0 543290429 864899072 38285 4294967295 134512640 134569956 3221224400 3221214664 1131227892 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 38285 13073 16 0 211141 0
vsize: 844628
[startup+920.078 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26713
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 87514 69 18 7 25 0 11 0 543290429 864899072 38721 4294967295 134512640 134569956 3221224400 3221214664 1131228208 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 38721 13073 16 0 211141 0
vsize: 844628
[startup+930.077 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26718
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 88463 69 18 7 25 0 11 0 543290429 864899072 39080 4294967295 134512640 134569956 3221224400 3221214664 1131227297 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 39080 13073 16 0 211141 0
vsize: 844628
[startup+940.078 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26723
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 89410 70 18 7 24 0 11 0 543290429 864899072 39234 4294967295 134512640 134569956 3221224400 3221214664 1131227386 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 39234 13073 16 0 211141 0
vsize: 844628
[startup+950.078 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26728
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 90363 70 19 7 25 0 11 0 543290429 864899072 39439 4294967295 134512640 134569956 3221224400 3221214760 1131269431 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 39439 13073 16 0 211141 0
vsize: 844628
[startup+960.08 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26732
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 91316 70 19 7 25 0 11 0 543290429 864899072 39618 4294967295 134512640 134569956 3221224400 3221214664 1131227338 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 39618 13073 16 0 211141 0
vsize: 844628
[startup+970.081 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26737
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 92267 70 19 7 25 0 11 0 543290429 864899072 39771 4294967295 134512640 134569956 3221224400 3221214664 1131227260 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 39771 13073 16 0 211141 0
vsize: 844628
[startup+980.086 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26742
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 93216 71 19 7 25 0 11 0 543290429 864899072 39892 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 39892 13073 16 0 211141 0
vsize: 844628
[startup+990.087 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26747
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 94164 71 20 7 25 0 11 0 543290429 864899072 40119 4294967295 134512640 134569956 3221224400 3221214664 1131226828 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 40119 13073 16 0 211141 0
vsize: 844628
[startup+1000.09 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26751
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 95115 72 20 7 25 0 11 0 543290429 864899072 40369 4294967295 134512640 134569956 3221224400 3221214760 1131268177 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 40369 13073 16 0 211141 0
vsize: 844628
[startup+1010.1 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26756
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 96069 72 20 7 25 0 11 0 543290429 864899072 40579 4294967295 134512640 134569956 3221224400 3221214664 1131227386 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 40579 13073 16 0 211141 0
vsize: 844628
[startup+1020.11 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26761
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 97016 73 20 7 24 0 11 0 543290429 864899072 40737 4294967295 134512640 134569956 3221224400 3221214756 1131226796 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 40737 13073 16 0 211141 0
vsize: 844628
[startup+1030.11 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26766
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 97966 74 21 7 25 0 11 0 543290429 864899072 40876 4294967295 134512640 134569956 3221224400 3221214800 1131474134 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 40876 13073 16 0 211141 0
vsize: 844628
[startup+1040.11 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26770
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 98919 74 21 7 25 0 11 0 543290429 864899072 41114 4294967295 134512640 134569956 3221224400 3221214760 1131271234 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 41114 13073 16 0 211141 0
vsize: 844628
[startup+1050.11 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26775
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 99871 74 21 7 25 0 11 0 543290429 864899072 41341 4294967295 134512640 134569956 3221224400 3221214664 1131228211 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 41341 13073 16 0 211141 0
vsize: 844628
[startup+1060.11 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26780
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 100826 75 21 7 25 0 11 0 543290429 864899072 41426 4294967295 134512640 134569956 3221224400 3221214760 1131268407 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 41426 13073 16 0 211141 0
vsize: 844628
[startup+1070.12 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26784
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 101777 75 22 7 25 0 11 0 543290429 864899072 41606 4294967295 134512640 134569956 3221224400 3221214664 1131227521 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 41606 13073 16 0 211141 0
vsize: 844628
[startup+1080.12 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26789
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 102727 75 22 8 25 0 11 0 543290429 864899072 41761 4294967295 134512640 134569956 3221224400 3221214664 1131228257 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 41761 13073 16 0 211141 0
vsize: 844628
[startup+1090.12 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26794
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 103678 76 22 8 25 0 11 0 543290429 864899072 41966 4294967295 134512640 134569956 3221224400 3221214664 1131226849 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 41966 13073 16 0 211141 0
vsize: 844628
[startup+1100.14 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26799
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 104633 76 23 8 25 0 11 0 543290429 864899072 42144 4294967295 134512640 134569956 3221224400 3221214664 1131226830 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 42144 13073 16 0 211141 0
vsize: 844628
[startup+1110.15 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26803
Raw data (stat): 26304 (java) S 26303 27222 27221 0 -1 0 18070 4 1 0 105589 77 23 8 25 0 11 0 543290429 864899072 42251 4294967295 134512640 134569956 3221224400 3221213408 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 42251 13073 16 0 211141 0
vsize: 844628
[startup+1120.15 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26808
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 106541 77 23 8 24 0 11 0 543290429 864899072 42479 4294967295 134512640 134569956 3221224400 3221214664 1131227551 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 42479 13073 16 0 211141 0
vsize: 844628
[startup+1130.15 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26813
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 107499 78 23 8 25 0 11 0 543290429 864899072 42564 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 42564 13073 16 0 211141 0
vsize: 844628
[startup+1140.16 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26818
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 108456 78 23 9 25 0 11 0 543290429 864899072 42671 4294967295 134512640 134569956 3221224400 3221214704 1131231528 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 42671 13073 16 0 211141 0
vsize: 844628
[startup+1150.19 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26822
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 109412 78 23 9 25 0 11 0 543290429 864899072 42783 4294967295 134512640 134569956 3221224400 3221214760 1131269526 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 42783 13073 16 0 211141 0
vsize: 844628
[startup+1160.19 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26827
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 110364 79 24 9 25 0 11 0 543290429 864899072 42913 4294967295 134512640 134569956 3221224400 3221214760 1131271028 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 42913 13073 16 0 211141 0
vsize: 844628
[startup+1170.19 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26832
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 111317 79 24 9 25 0 11 0 543290429 864899072 43093 4294967295 134512640 134569956 3221224400 3221214664 1131227531 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 43093 13073 16 0 211141 0
vsize: 844628
[startup+1180.19 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26836
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 112274 79 24 9 25 0 11 0 543290429 864899072 43266 4294967295 134512640 134569956 3221224400 3221214664 1131227646 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 43266 13073 16 0 211141 0
vsize: 844628
[startup+1190.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26841
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 113230 80 24 9 25 0 11 0 543290429 864899072 43396 4294967295 134512640 134569956 3221224400 3221214664 1131227513 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 43396 13073 16 0 211141 0
vsize: 844628
[startup+1200.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26846
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 114187 80 25 9 25 0 11 0 543290429 864899072 43487 4294967295 134512640 134569956 3221224400 3221214760 1131269526 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 43487 13073 16 0 211141 0
vsize: 844628
[startup+1210.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26851
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 115143 80 25 9 25 0 11 0 543290429 864899072 43646 4294967295 134512640 134569956 3221224400 3221214800 1131474867 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 43646 13073 16 0 211141 0
vsize: 844628
[startup+1220.22 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26855
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 116102 81 25 9 25 0 11 0 543290429 864899072 43759 4294967295 134512640 134569956 3221224400 3221214664 1131226842 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 43759 13073 16 0 211141 0
vsize: 844628
[startup+1230.22 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26860
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 117058 81 25 9 25 0 11 0 543290429 864899072 43868 4294967295 134512640 134569956 3221224400 3221214664 1131227341 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 43868 13073 16 0 211141 0
vsize: 844628
[startup+1240.22 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26865
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 118011 81 26 9 25 0 11 0 543290429 864899072 43974 4294967295 134512640 134569956 3221224400 3221214664 1131227247 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 43974 13073 16 0 211141 0
vsize: 844628
[startup+1250.23 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26869
Raw data (stat): 26304 (java) S 26303 27222 27221 0 -1 0 18070 4 1 0 118958 82 26 9 25 0 11 0 543290429 864899072 44080 4294967295 134512640 134569956 3221224400 3221213408 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211157 44080 13073 16 0 211141 0
vsize: 844628
[startup+1260.23 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26874
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 119907 82 26 9 25 0 11 0 543290429 864899072 44237 4294967295 134512640 134569956 3221224400 3221214664 1131228301 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211157 44237 13073 16 0 211141 0
vsize: 844628
[startup+1270.23 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 26879
Raw data (stat): 26304 (java) R 26303 27222 27221 0 -1 0 18070 4 1 0 120861 83 26 9 25 0 11 0 543290429 864899072 44583 4294967295 134512640 134569956 3221224400 3221214760 1131268400 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211157 44583 13073 16 0 211141 0
vsize: 844628
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1270.37 s]
Raw data (loadavg): 1.00 0.98 0.92 1/54 26881
Raw data (stat): 26304 (java) Z 26303 27222 27221 0 -1 1036 18070 31951 1 0 120867 91 7338 101 25 0 1 0 543290429 0 0 4294967295 0 0 0 0 0 0 4 3 23756 3222412051 0 0 17 1 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): 1270.37
CPU time (s): 1283.99
CPU user time (s): 1282.06
CPU system time (s): 1.92571
CPU usage (%): 101.072
Max. virtual memory (Kb): 844628
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####