PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-bell5.opb
MD5SUM	e2343a1c48cef657bed9677a2fcc9921
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	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 numbers	60
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1231.56
Number of variables	1704
Total number of constraints	149
Number of constraints which are clauses	15
Number of constraints which are cardinality constraints (but not clauses)	30
Number of constraints which are nor clauses,nor cardinality constraints	104
Minimum length of a constraint	1
Maximum length of a constraint	135
Trace number 17108

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 09:41:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11735 boxname=wulflinc30 idbench=903 idsolver=9 numberseed=0
MD5SUM SOLVER: daf345f6fbf228671abfac48013b9cac  /oldhome/oroussel/solvers/sat4jPseudo.jar
MD5SUM BENCH:  e2343a1c48cef657bed9677a2fcc9921  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-bell5.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudo.jar /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-bell5.opb
IDLAUNCH: 11735
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        794836 kB
Buffers:         14976 kB
Cached:         196028 kB
SwapCached:          0 kB
Active:          43208 kB
Inactive:       170620 kB
HighTotal:      131008 kB
HighFree:        31696 kB
LowTotal:       903652 kB
LowFree:        763140 kB
SwapTotal:     2097892 kB
SwapFree:      2097824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            20156 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 10:02:57 (client local time) WITH STATUS 143 IN 1272.47 SECONDS
stats: 11735 7 1272.47 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-bell5.opb
c reading problem 
c [nbvar=1704]
c [nbconstr=149]
c time 3.014
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.214
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.18
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.104
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.49
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.569
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.519
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) : 58.966
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.494
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.101
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.662
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.255
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.812
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.372
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.959
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.518
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) : 86.067
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.668
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.237
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.805
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.411
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.979
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.552
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) : 104.158
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.727
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) : 109.303
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.919
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.506
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) : 117.086
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.709
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) : 122.285
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.86
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) : 127.477
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) : 130.053
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.63
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) : 135.252
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.825
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) : 140.401
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) : 143.015
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) : 145.591
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) : 148.164
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.785
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) : 153.367
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.943
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) : 158.571
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) : 161.153
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) : 163.74
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) : 166.372
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.965
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) : 171.562
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) : 174.202
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) : 176.795
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) : 179.38
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) : 182.004
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) : 184.59
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) : 187.175
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) : 189.807
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) : 192.39
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) : 194.974
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) : 197.614
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) : 200.194
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) : 202.777
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) : 205.393
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) : 207.969
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) : 210.547
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) : 213.157
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) : 215.732
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) : 218.324
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) : 220.963
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) : 223.564
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) : 226.159
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) : 228.809
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) : 231.417
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) : 234.018
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) : 236.667
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) : 239.276
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) : 241.886
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) : 244.537
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) : 247.145
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) : 249.754
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) : 252.421
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) : 255.049
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) : 257.714
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) : 260.338
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) : 262.954
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) : 265.624
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) : 268.251
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) : 270.872
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) : 273.54
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) : 276.169
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) : 278.804
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) : 281.485
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) : 284.128
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) : 286.763
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) : 289.439
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) : 291.507
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) : 293.57
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) : 295.673
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) : 297.739
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) : 299.796
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) : 301.901
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) : 303.974
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) : 306.04
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) : 308.147
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) : 310.214
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) : 312.274
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) : 314.379
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) : 316.435
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) : 318.498
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) : 320.603
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) : 322.664
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) : 324.722
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) : 326.812
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) : 328.862
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) : 330.914
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) : 333.013
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) : 335.072
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) : 337.13
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) : 339.228
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) : 341.291
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) : 343.354
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) : 345.441
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) : 347.503
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) : 349.55
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) : 351.637
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) : 353.691
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) : 355.741
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) : 357.828
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) : 359.881
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) : 361.936
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) : 364.024
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) : 366.078
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) : 368.139
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) : 370.229
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) : 372.284
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) : 374.337
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) : 376.434
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) : 378.487
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) : 380.548
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) : 382.646
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) : 384.706
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) : 386.766
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) : 388.87
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) : 390.927
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) : 393.024
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) : 395.081
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) : 397.14
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) : 399.238
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) : 401.287
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) : 403.353
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) : 405.449
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) : 407.507
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) : 409.582
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) : 411.714
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) : 413.809
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) : 415.889
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) : 418.016
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) : 420.102
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) : 422.19
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) : 424.314
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) : 426.403
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) : 428.495
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) : 430.635
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) : 432.72
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) : 434.805
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) : 436.939
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) : 439.018
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) : 441.085
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) : 443.191
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) : 445.258
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) : 447.308
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) : 449.408
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) : 451.48
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) : 453.545
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) : 455.649
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) : 457.713
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) : 459.781
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) : 461.887
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) : 463.953
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) : 466.019
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) : 468.131
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) : 470.2
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) : 472.27
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) : 474.391
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) : 476.47
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) : 478.546
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) : 480.675
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) : 482.749
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) : 484.873
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) : 486.939
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) : 489.031
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) : 491.181
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) : 493.293
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) : 495.387
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) : 497.554
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) : 499.662
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) : 501.761
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) : 503.918
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) : 506.021
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) : 508.123
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) : 510.273
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) : 512.369
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) : 514.469
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) : 516.616
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) : 518.716
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) : 520.802
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) : 522.921
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) : 525.001
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) : 527.08
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) : 529.2
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) : 531.284
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) : 533.36
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) : 535.493
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) : 537.576
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) : 539.668
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) : 541.797
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) : 543.879
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) : 545.961
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) : 548.091
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) : 550.175
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) : 552.245
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) : 554.372
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) : 556.449
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) : 558.531
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) : 560.648
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) : 562.739
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) : 564.869
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) : 566.964
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) : 569.042
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) : 571.169
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) : 573.252
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) : 575.324
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) : 577.452
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) : 579.545
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) : 581.625
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) : 583.742
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) : 585.833
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) : 587.919
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) : 590.047
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) : 592.134
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) : 594.214
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) : 596.333
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) : 598.415
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) : 600.494
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) : 602.607
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) : 604.695
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) : 606.778
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) : 608.903
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) : 610.983
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) : 613.067
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) : 615.188
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) : 617.274
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) : 619.356
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) : 621.476
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) : 623.557
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) : 625.635
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) : 627.761
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) : 629.844
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) : 631.933
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) : 634.064
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) : 636.148
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) : 638.234
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) : 640.355
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) : 642.438
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) : 644.564
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) : 646.647
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) : 648.737
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) : 650.871
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) : 652.953
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) : 655.036
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) : 657.169
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) : 659.266
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) : 661.357
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) : 663.491
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) : 665.582
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) : 667.67
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) : 669.803
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) : 671.9
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) : 673.998
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) : 676.13
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) : 678.217
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) : 680.309
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) : 682.436
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) : 684.524
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) : 686.621
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) : 688.741
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) : 690.837
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) : 692.932
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) : 695.064
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) : 697.158
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) : 699.249
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) : 701.37
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) : 703.457
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) : 705.536
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) : 707.669
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) : 709.763
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) : 711.979
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) : 714.063
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) : 716.155
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) : 718.211
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) : 720.261
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) : 722.31
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) : 724.386
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) : 726.452
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) : 728.522
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) : 730.632
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) : 732.714
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) : 734.81
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) : 736.927
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) : 739.017
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) : 741.108
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) : 743.245
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) : 745.35
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) : 747.451
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) : 749.584
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) : 751.674
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) : 753.77
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) : 755.916
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) : 758.013
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) : 760.117
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) : 762.259
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) : 764.352
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) : 766.49
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) : 768.592
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) : 770.692
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) : 772.847
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) : 774.953
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) : 777.061
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) : 779.208
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) : 781.315
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) : 783.426
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) : 785.569
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) : 787.681
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) : 789.784
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) : 791.934
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) : 794.05
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) : 796.157
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) : 798.305
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) : 800.41
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) : 802.507
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) : 804.647
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) : 806.74
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) : 808.814
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) : 810.92
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) : 812.997
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) : 815.076
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) : 817.195
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) : 819.276
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) : 821.357
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) : 823.477
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) : 825.552
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) : 827.673
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) : 829.76
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) : 831.843
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) : 833.963
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) : 836.052
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) : 838.132
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) : 840.249
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) : 842.338
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) : 844.415
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) : 846.537
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) : 848.62
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) : 850.708
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) : 852.832
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) : 854.923
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) : 857.011
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) : 859.146
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) : 861.237
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) : 863.335
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) : 865.479
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) : 867.566
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) : 869.657
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) : 871.786
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) : 873.878
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) : 875.975
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) : 878.118
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) : 880.22
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) : 882.368
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) : 884.466
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) : 886.566
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) : 888.723
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) : 890.836
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) : 892.945
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) : 895.135
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) : 897.278
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) : 899.42
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) : 901.624
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) : 903.773
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) : 905.913
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) : 908.137
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) : 910.288
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) : 912.442
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) : 914.651
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) : 916.797
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) : 918.934
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) : 921.136
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) : 923.273
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) : 925.4
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) : 927.571
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) : 929.677
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) : 931.851
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) : 933.977
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) : 936.112
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) : 938.253
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) : 940.363
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) : 942.469
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) : 944.605
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) : 946.707
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) : 948.8
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) : 950.938
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) : 953.034
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) : 955.133
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) : 957.284
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) : 959.381
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) : 961.471
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) : 963.608
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) : 965.718
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) : 967.836
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) : 970.002
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) : 972.126
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) : 974.254
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) : 976.417
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) : 978.543
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) : 980.712
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) : 982.85
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) : 984.981
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) : 987.157
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) : 989.289
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) : 991.42
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) : 993.594
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) : 995.724
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) : 997.857
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) : 1000.028
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) : 1002.16
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) : 1004.285
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) : 1006.461
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) : 1008.594
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) : 1010.718
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) : 1012.89
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) : 1015.018
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) : 1017.141
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) : 1019.301
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) : 1021.421
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) : 1023.548
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) : 1025.723
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) : 1027.849
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) : 1030.024
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) : 1032.16
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) : 1034.288
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) : 1036.477
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) : 1038.628
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) : 1040.769
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) : 1042.95
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) : 1045.081
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) : 1047.216
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) : 1049.395
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) : 1051.539
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) : 1053.683
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) : 1055.86
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) : 1057.996
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) : 1060.13
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) : 1062.307
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) : 1064.444
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) : 1066.576
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) : 1068.763
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) : 1070.894
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) : 1073.074
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) : 1075.222
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) : 1077.359
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) : 1079.549
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) : 1081.694
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) : 1083.835
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) : 1086.018
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) : 1088.169
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) : 1090.286
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) : 1092.514
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) : 1094.628
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) : 1096.762
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) : 1098.945
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) : 1101.083
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) : 1103.217
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) : 1105.398
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) : 1107.541
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) : 1109.673
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) : 1111.854
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) : 1113.991
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) : 1116.167
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) : 1118.294
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) : 1120.426
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) : 1122.6
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) : 1124.737
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) : 1126.866
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) : 1129.039
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) : 1131.178
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) : 1133.309
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) : 1135.477
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) : 1137.6
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) : 1139.729
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) : 1141.901
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) : 1144.036
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) : 1146.157
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) : 1148.332
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) : 1150.462
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) : 1152.596
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) : 1154.762
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) : 1156.907
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) : 1159.102
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) : 1161.248
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) : 1163.392
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) : 1165.57
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) : 1167.728
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) : 1169.87
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) : 1172.056
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) : 1174.214
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) : 1176.359
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) : 1178.543
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) : 1180.69
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) : 1182.842
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) : 1185.03
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) : 1187.177
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) : 1189.324
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) : 1191.502
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) : 1193.655
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) : 1195.792
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) : 1197.98
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) : 1200.113
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) : 1202.292
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) : 1204.439
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) : 1206.584
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) : 1208.77
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) : 1210.918
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) : 1213.061
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) : 1215.24
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) : 1217.386
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) : 1219.533
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) : 1221.712
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) : 1223.847
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) : 1225.99
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) : 1228.173
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) : 1230.318
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) : 1232.459
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) : 1234.642
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) : 1236.78
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) : 1238.927
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) : 1241.113
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) : 1243.262
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) : 1245.438
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) : 1247.593
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) : 1249.746
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) : 1251.944
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) : 1254.101
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) : 1256.265
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) : 1258.476
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
#### 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.80 0.91 0.90 2/54 17894
Raw data (stat): 17894 (runsolver) R 17893 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544078853 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.98 0.95 0.91 3/64 17905
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18053 3 1 0 714 45 0 0 25 0 11 0 544078853 857174016 19932 4294967295 134512640 134569956 3221224400 3221214752 1131275999 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209271 19932 13073 16 0 209255 0
vsize: 837084
[startup+20.001 s]
Raw data (loadavg): 1.14 0.98 0.92 3/64 17905
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18055 3 1 0 1634 46 0 0 25 0 11 0 544078853 861818880 21056 4294967295 134512640 134569956 3221224400 3221214716 1130917326 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210405 21056 13073 16 0 210389 0
vsize: 841620
[startup+30.0017 s]
Raw data (loadavg): 1.12 0.98 0.92 2/64 17905
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18055 3 1 0 2588 46 0 0 25 0 11 0 544078853 860860416 21053 4294967295 134512640 134569956 3221224400 3221214680 1131227597 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210171 21053 13073 16 0 210155 0
vsize: 840684
[startup+40.0021 s]
Raw data (loadavg): 1.10 0.98 0.92 2/64 17907
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 3533 46 0 0 25 0 11 0 544078853 859766784 21036 4294967295 134512640 134569956 3221224400 3221214720 1131276284 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209904 21036 13073 16 0 209888 0
vsize: 839616
[startup+50.0034 s]
Raw data (loadavg): 1.08 0.98 0.92 2/64 17909
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 4481 46 0 0 25 0 11 0 544078853 865189888 22703 4294967295 134512640 134569956 3221224400 3221214616 1131589121 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211228 22703 13073 16 0 211212 0
vsize: 844912
[startup+60.0032 s]
Raw data (loadavg): 1.07 0.98 0.92 2/64 17911
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 5453 46 0 0 25 0 11 0 544078853 865189888 22750 4294967295 134512640 134569956 3221224400 3221214720 1131278959 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211228 22750 13073 16 0 211212 0
vsize: 844912
[startup+70.0035 s]
Raw data (loadavg): 1.06 0.98 0.92 2/64 17913
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 6423 47 0 0 25 0 11 0 544078853 865189888 22802 4294967295 134512640 134569956 3221224400 3221214624 1131227749 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211228 22802 13073 16 0 211212 0
vsize: 844912
[startup+80.004 s]
Raw data (loadavg): 1.05 0.98 0.92 2/64 17917
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 7392 47 0 0 25 0 11 0 544078853 865189888 22965 4294967295 134512640 134569956 3221224400 3221214624 1131227077 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211228 22965 13073 16 0 211212 0
vsize: 844912
[startup+90.0036 s]
Raw data (loadavg): 1.04 0.98 0.92 2/64 17921
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 8361 47 0 0 25 0 11 0 544078853 865189888 23036 4294967295 134512640 134569956 3221224400 3221214624 1131227759 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211228 23036 13073 16 0 211212 0
vsize: 844912
[startup+100.005 s]
Raw data (loadavg): 1.03 0.98 0.92 2/64 17925
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 9326 48 0 0 25 0 11 0 544078853 861855744 22335 4294967295 134512640 134569956 3221224400 3221214720 1131277308 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 22335 13073 16 0 210398 0
vsize: 841656
[startup+110.006 s]
Raw data (loadavg): 1.03 0.98 0.92 2/64 17929
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 10287 48 0 0 25 0 11 0 544078853 861855744 22445 4294967295 134512640 134569956 3221224400 3221214624 1131227505 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 22445 13073 16 0 210398 0
vsize: 841656
[startup+120.006 s]
Raw data (loadavg): 1.02 0.98 0.92 2/64 17932
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 11249 49 0 0 25 0 11 0 544078853 861855744 22581 4294967295 134512640 134569956 3221224400 3221214568 1131562954 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 22581 13073 16 0 210398 0
vsize: 841656
[startup+130.006 s]
Raw data (loadavg): 1.02 0.98 0.92 2/64 17936
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 12211 49 1 0 25 0 11 0 544078853 861855744 22731 4294967295 134512640 134569956 3221224400 3221214728 1131589936 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 22731 13073 16 0 210398 0
vsize: 841656
[startup+140.006 s]
Raw data (loadavg): 1.02 0.98 0.92 2/64 17940
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 13170 49 1 0 24 0 11 0 544078853 861855744 22878 4294967295 134512640 134569956 3221224400 3221214676 1131562960 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 22878 13073 16 0 210398 0
vsize: 841656
[startup+150.011 s]
Raw data (loadavg): 1.01 0.98 0.92 2/64 17944
Raw data (stat): 17894 (java) S 17893 11931 11930 0 -1 0 18056 3 1 0 14135 49 1 0 25 0 11 0 544078853 861855744 23022 4294967295 134512640 134569956 3221224400 3221213264 1073952481 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 23022 13073 16 0 210398 0
vsize: 841656
[startup+160.012 s]
Raw data (loadavg): 1.01 0.98 0.92 2/64 17948
Raw data (stat): 17894 (java) S 17893 11931 11930 0 -1 0 18056 3 1 0 15100 49 2 0 25 0 11 0 544078853 861855744 23150 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 23150 13073 16 0 210398 0
vsize: 841656
[startup+170.012 s]
Raw data (loadavg): 1.01 0.98 0.92 2/64 17952
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 16059 49 2 0 25 0 11 0 544078853 861855744 23293 4294967295 134512640 134569956 3221224400 3221214720 1131276319 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 23293 13073 16 0 210398 0
vsize: 841656
[startup+180.013 s]
Raw data (loadavg): 1.01 0.98 0.92 2/64 17955
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 17016 50 2 0 25 0 11 0 544078853 861855744 23427 4294967295 134512640 134569956 3221224400 3221214624 1131227811 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 23427 13073 16 0 210398 0
vsize: 841656
[startup+190.013 s]
Raw data (loadavg): 1.01 0.98 0.92 2/64 17959
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 17974 50 2 0 25 0 11 0 544078853 861855744 23575 4294967295 134512640 134569956 3221224400 3221214616 1131590936 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 23575 13073 16 0 210398 0
vsize: 841656
[startup+200.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 17963
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 18935 51 2 0 25 0 11 0 544078853 861855744 23855 4294967295 134512640 134569956 3221224400 3221214720 1131276284 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 23855 13073 16 0 210398 0
vsize: 841656
[startup+210.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 17967
Raw data (stat): 17894 (java) S 17893 11931 11930 0 -1 0 18056 3 1 0 19896 51 3 0 25 0 11 0 544078853 861855744 24001 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 24001 13073 16 0 210398 0
vsize: 841656
[startup+220.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 17971
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 20861 51 3 0 25 0 11 0 544078853 861855744 24138 4294967295 134512640 134569956 3221224400 3221214624 1131227759 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 24138 13073 16 0 210398 0
vsize: 841656
[startup+230.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 17975
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 21826 52 3 0 25 0 11 0 544078853 861855744 24271 4294967295 134512640 134569956 3221224400 3221214624 1131227117 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 24271 13073 16 0 210398 0
vsize: 841656
[startup+240.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 17979
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 22791 52 3 0 25 0 11 0 544078853 861855744 24395 4294967295 134512640 134569956 3221224400 3221214624 1131227749 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 24395 13073 16 0 210398 0
vsize: 841656
[startup+250.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 17982
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 23758 53 3 1 25 0 11 0 544078853 861855744 24504 4294967295 134512640 134569956 3221224400 3221214624 1131228467 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 24504 13073 16 0 210398 0
vsize: 841656
[startup+260.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 17986
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 24719 53 3 1 25 0 11 0 544078853 861855744 24628 4294967295 134512640 134569956 3221224400 3221214624 1131227749 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 24628 13073 16 0 210398 0
vsize: 841656
[startup+270.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 17990
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 25677 54 3 1 25 0 11 0 544078853 861855744 24772 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 24772 13073 16 0 210398 0
vsize: 841656
[startup+280.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 17994
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 26635 54 3 1 25 0 11 0 544078853 861855744 24940 4294967295 134512640 134569956 3221224400 3221214624 1131227105 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 24940 13073 16 0 210398 0
vsize: 841656
[startup+290.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 17997
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 27592 55 3 1 25 0 11 0 544078853 861855744 25312 4294967295 134512640 134569956 3221224400 3221214568 1131562908 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 25312 13073 16 0 210398 0
vsize: 841656
[startup+300.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18002
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 28541 55 4 1 25 0 11 0 544078853 861855744 25501 4294967295 134512640 134569956 3221224400 3221214720 1131276284 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 25501 13073 16 0 210398 0
vsize: 841656
[startup+310.022 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18007
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 29488 56 4 1 25 0 11 0 544078853 861855744 25671 4294967295 134512640 134569956 3221224400 3221214624 1131227069 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 25671 13073 16 0 210398 0
vsize: 841656
[startup+320.022 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18012
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 30438 56 4 1 25 0 11 0 544078853 861855744 25867 4294967295 134512640 134569956 3221224400 3221214624 1131227541 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 25867 13073 16 0 210398 0
vsize: 841656
[startup+330.022 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18017
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 31386 57 4 1 24 0 11 0 544078853 861855744 26063 4294967295 134512640 134569956 3221224400 3221214720 1131277322 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 26063 13073 16 0 210398 0
vsize: 841656
[startup+340.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18022
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 32339 58 4 1 25 0 11 0 544078853 861855744 26273 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 26273 13073 16 0 210398 0
vsize: 841656
[startup+350.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18026
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 33293 59 5 1 25 0 11 0 544078853 861855744 26474 4294967295 134512640 134569956 3221224400 3221214624 1131227865 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 26474 13073 16 0 210398 0
vsize: 841656
[startup+360.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18031
Raw data (stat): 17894 (java) S 17893 11931 11930 0 -1 0 18056 3 1 0 34250 59 5 2 25 0 11 0 544078853 861855744 26663 4294967295 134512640 134569956 3221224400 3221213328 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 26663 13073 16 0 210398 0
vsize: 841656
[startup+370.026 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18036
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 35204 60 5 2 25 0 11 0 544078853 861855744 26795 4294967295 134512640 134569956 3221224400 3221214624 1131228043 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 26795 13073 16 0 210398 0
vsize: 841656
[startup+380.026 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18041
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 36160 61 5 2 25 0 11 0 544078853 861855744 26916 4294967295 134512640 134569956 3221224400 3221214864 1131469188 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 26916 13073 16 0 210398 0
vsize: 841656
[startup+390.027 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18046
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 37116 62 6 2 25 0 11 0 544078853 861855744 27062 4294967295 134512640 134569956 3221224400 3221214720 1131277372 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 27062 13073 16 0 210398 0
vsize: 841656
[startup+400.028 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18051
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 38069 62 6 2 25 0 11 0 544078853 861855744 27232 4294967295 134512640 134569956 3221224400 3221214720 1131279073 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 27232 13073 16 0 210398 0
vsize: 841656
[startup+410.028 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18055
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 39026 63 6 2 25 0 11 0 544078853 861855744 27376 4294967295 134512640 134569956 3221224400 3221214720 1131279036 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 27376 13073 16 0 210398 0
vsize: 841656
[startup+420.028 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18060
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 39970 63 6 2 25 0 11 0 544078853 861855744 27721 4294967295 134512640 134569956 3221224400 3221214624 1131228093 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 27721 13073 16 0 210398 0
vsize: 841656
[startup+430.029 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18065
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 40914 64 7 2 25 0 11 0 544078853 861855744 27924 4294967295 134512640 134569956 3221224400 3221214624 1131228492 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 27924 13073 16 0 210398 0
vsize: 841656
[startup+440.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18070
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 41859 64 7 2 25 0 11 0 544078853 861855744 28492 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 28492 13073 16 0 210398 0
vsize: 841656
[startup+450.031 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18074
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 42811 65 7 2 25 0 11 0 544078853 861855744 28638 4294967295 134512640 134569956 3221224400 3221214624 1131227632 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 28638 13073 16 0 210398 0
vsize: 841656
[startup+460.032 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18079
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 43767 65 7 3 25 0 11 0 544078853 861855744 28817 4294967295 134512640 134569956 3221224400 3221214624 1131227553 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 28817 13073 16 0 210398 0
vsize: 841656
[startup+470.031 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18084
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 44722 66 7 3 25 0 11 0 544078853 861855744 28986 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 28986 13073 16 0 210398 0
vsize: 841656
[startup+480.032 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18089
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 45676 66 7 3 25 0 11 0 544078853 861855744 29090 4294967295 134512640 134569956 3221224400 3221214624 1131227105 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 29090 13073 16 0 210398 0
vsize: 841656
[startup+490.033 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18094
Raw data (stat): 17894 (java) S 17893 11931 11930 0 -1 0 18056 3 1 0 46620 67 8 3 25 0 11 0 544078853 861855744 29266 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 29266 13073 16 0 210398 0
vsize: 841656
[startup+500.034 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18098
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 47558 68 8 3 25 0 11 0 544078853 861855744 29447 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 29447 13073 16 0 210398 0
vsize: 841656
[startup+510.035 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18103
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 48497 68 8 3 24 0 11 0 544078853 861855744 29649 4294967295 134512640 134569956 3221224400 3221214624 1131227073 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 29649 13073 16 0 210398 0
vsize: 841656
[startup+520.035 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18108
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 49441 69 8 3 25 0 11 0 544078853 861855744 29966 4294967295 134512640 134569956 3221224400 3221214720 1131277322 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 29966 13073 16 0 210398 0
vsize: 841656
[startup+530.035 s]
Raw data (loadavg): 1.00 0.98 0.92 3/64 18113
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 50393 69 9 3 25 0 11 0 544078853 861855744 30146 4294967295 134512640 134569956 3221224400 3221214624 1131227825 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 30146 13073 16 0 210398 0
vsize: 841656
[startup+540.035 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18117
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 51345 70 9 3 25 0 11 0 544078853 861855744 30301 4294967295 134512640 134569956 3221224400 3221214624 1131227865 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 30301 13073 16 0 210398 0
vsize: 841656
[startup+550.036 s]
Raw data (loadavg): 1.00 0.98 0.92 2/64 18122
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 52296 71 9 3 25 0 11 0 544078853 861855744 30515 4294967295 134512640 134569956 3221224400 3221214624 1131227105 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 30515 13073 16 0 210398 0
vsize: 841656
[startup+560.037 s]
Raw data (loadavg): 1.08 1.00 0.93 2/64 18127
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 53249 71 9 3 25 0 11 0 544078853 861855744 30694 4294967295 134512640 134569956 3221224400 3221214624 1131227073 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 30694 13073 16 0 210398 0
vsize: 841656
[startup+570.038 s]
Raw data (loadavg): 1.07 1.00 0.93 2/64 18132
Raw data (stat): 17894 (java) S 17893 11931 11930 0 -1 0 18056 3 1 0 54199 72 9 4 25 0 11 0 544078853 861855744 30927 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 30927 13073 16 0 210398 0
vsize: 841656
[startup+580.038 s]
Raw data (loadavg): 1.06 1.00 0.93 2/64 18136
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 55152 73 10 4 25 0 11 0 544078853 861855744 31075 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 31075 13073 16 0 210398 0
vsize: 841656
[startup+590.039 s]
Raw data (loadavg): 1.05 1.00 0.93 2/64 18141
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 56104 73 10 4 25 0 11 0 544078853 861855744 31250 4294967295 134512640 134569956 3221224400 3221214624 1131228464 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 31250 13073 16 0 210398 0
vsize: 841656
[startup+600.04 s]
Raw data (loadavg): 1.04 1.00 0.93 2/64 18146
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 57060 74 10 4 25 0 11 0 544078853 861855744 31466 4294967295 134512640 134569956 3221224400 3221214624 1131227110 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 31466 13073 16 0 210398 0
vsize: 841656
[startup+610.041 s]
Raw data (loadavg): 1.03 1.00 0.93 2/64 18151
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 58016 75 10 4 25 0 11 0 544078853 861855744 31644 4294967295 134512640 134569956 3221224400 3221214624 1131227481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 31644 13073 16 0 210398 0
vsize: 841656
[startup+620.042 s]
Raw data (loadavg): 1.03 1.00 0.93 2/64 18156
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 58973 76 10 4 25 0 11 0 544078853 861855744 31751 4294967295 134512640 134569956 3221224400 3221214760 1131458637 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 31751 13073 16 0 210398 0
vsize: 841656
[startup+630.043 s]
Raw data (loadavg): 1.02 1.00 0.93 2/64 18160
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 59926 76 11 4 24 0 11 0 544078853 861855744 31881 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 31881 13073 16 0 210398 0
vsize: 841656
[startup+640.043 s]
Raw data (loadavg): 1.02 1.00 0.93 2/64 18165
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 60882 77 11 4 25 0 11 0 544078853 861855744 32062 4294967295 134512640 134569956 3221224400 3221214624 1131227723 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 32062 13073 16 0 210398 0
vsize: 841656
[startup+650.044 s]
Raw data (loadavg): 1.02 1.00 0.93 2/64 18170
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 61839 78 11 4 25 0 11 0 544078853 861855744 32154 4294967295 134512640 134569956 3221224400 3221214720 1131278972 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 32154 13073 16 0 210398 0
vsize: 841656
[startup+660.045 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 18175
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 62795 78 12 4 25 0 11 0 544078853 861855744 32274 4294967295 134512640 134569956 3221224400 3221214624 1131227601 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 32274 13073 16 0 210398 0
vsize: 841656
[startup+670.044 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 18179
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 63749 79 12 4 25 0 11 0 544078853 861855744 32413 4294967295 134512640 134569956 3221224400 3221214624 1131228467 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 32413 13073 16 0 210398 0
vsize: 841656
[startup+680.046 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 18184
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 64704 80 12 5 25 0 11 0 544078853 861855744 32582 4294967295 134512640 134569956 3221224400 3221214624 1131227749 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 32582 13073 16 0 210398 0
vsize: 841656
[startup+690.047 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 18189
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 65660 80 12 5 25 0 11 0 544078853 861855744 32736 4294967295 134512640 134569956 3221224400 3221214624 1131227077 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 32736 13073 16 0 210398 0
vsize: 841656
[startup+700.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18194
Raw data (stat): 17894 (java) S 17893 11931 11930 0 -1 0 18056 3 1 0 66613 81 12 5 25 0 11 0 544078853 861855744 32902 4294967295 134512640 134569956 3221224400 3221213368 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 32902 13073 16 0 210398 0
vsize: 841656
[startup+710.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18198
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 67568 81 12 5 25 0 11 0 544078853 861855744 33012 4294967295 134512640 134569956 3221224400 3221214624 1131227648 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 33012 13073 16 0 210398 0
vsize: 841656
[startup+720.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18203
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 68530 81 13 5 25 0 11 0 544078853 861855744 34699 4294967295 134512640 134569956 3221224400 3221214624 1131227073 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 34699 13073 16 0 210398 0
vsize: 841656
[startup+730.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18208
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 69505 82 13 5 25 0 11 0 544078853 861855744 34699 4294967295 134512640 134569956 3221224400 3221214624 1131227551 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 34699 13073 16 0 210398 0
vsize: 841656
[startup+740.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18213
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 70468 82 13 5 25 0 11 0 544078853 861855744 34699 4294967295 134512640 134569956 3221224400 3221214624 1131227077 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 34699 13073 16 0 210398 0
vsize: 841656
[startup+750.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18217
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 71421 83 13 5 24 0 11 0 544078853 861855744 34854 4294967295 134512640 134569956 3221224400 3221214624 1131228415 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 34854 13073 16 0 210398 0
vsize: 841656
[startup+760.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18222
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 72376 84 14 6 24 0 11 0 544078853 861855744 35023 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 35023 13073 16 0 210398 0
vsize: 841656
[startup+770.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18227
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 73330 85 14 6 25 0 11 0 544078853 861855744 35132 4294967295 134512640 134569956 3221224400 3221214624 1131228435 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 35132 13073 16 0 210398 0
vsize: 841656
[startup+780.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18232
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 74284 85 14 6 25 0 11 0 544078853 861855744 35266 4294967295 134512640 134569956 3221224400 3221214720 1131278984 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 35266 13073 16 0 210398 0
vsize: 841656
[startup+790.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18236
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 75238 86 14 6 25 0 11 0 544078853 861855744 35468 4294967295 134512640 134569956 3221224400 3221214720 1131278938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 35468 13073 16 0 210398 0
vsize: 841656
[startup+800.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18241
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 76193 87 14 6 25 0 11 0 544078853 861855744 35624 4294967295 134512640 134569956 3221224400 3221214720 1131277278 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 35624 13073 16 0 210398 0
vsize: 841656
[startup+810.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18246
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 77149 87 14 6 25 0 11 0 544078853 861855744 35789 4294967295 134512640 134569956 3221224400 3221214624 1131228464 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 35789 13073 16 0 210398 0
vsize: 841656
[startup+820.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18251
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 78106 87 15 6 25 0 11 0 544078853 861855744 35922 4294967295 134512640 134569956 3221224400 3221214720 1131278896 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 35922 13073 16 0 210398 0
vsize: 841656
[startup+830.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18255
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 79062 87 15 6 25 0 11 0 544078853 861855744 36057 4294967295 134512640 134569956 3221224400 3221214624 1131228265 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 36057 13073 16 0 210398 0
vsize: 841656
[startup+840.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18260
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 80014 88 15 6 25 0 11 0 544078853 861855744 36199 4294967295 134512640 134569956 3221224400 3221214716 1131227052 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 36199 13073 16 0 210398 0
vsize: 841656
[startup+850.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18265
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 80969 88 15 6 25 0 11 0 544078853 861855744 36357 4294967295 134512640 134569956 3221224400 3221214624 1131227303 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 36357 13073 16 0 210398 0
vsize: 841656
[startup+860.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18270
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 81922 88 15 6 25 0 11 0 544078853 861855744 36491 4294967295 134512640 134569956 3221224400 3221214624 1131227117 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 36491 13073 16 0 210398 0
vsize: 841656
[startup+870.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18274
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18056 3 1 0 82873 89 16 6 25 0 11 0 544078853 861855744 36625 4294967295 134512640 134569956 3221224400 3221214624 1131227077 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 36625 13073 16 0 210398 0
vsize: 841656
[startup+880.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18279
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 83824 89 16 6 25 0 11 0 544078853 861855744 36842 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 36842 13073 16 0 210398 0
vsize: 841656
[startup+890.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18284
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 84772 89 16 6 25 0 11 0 544078853 861855744 36985 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 36985 13073 16 0 210398 0
vsize: 841656
[startup+900.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18288
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 85707 89 16 6 25 0 11 0 544078853 861855744 37140 4294967295 134512640 134569956 3221224400 3221214720 1131275968 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 37140 13073 16 0 210398 0
vsize: 841656
[startup+910.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18293
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 86631 90 17 6 25 0 11 0 544078853 861855744 37300 4294967295 134512640 134569956 3221224400 3221214624 1131227553 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 37300 13073 16 0 210398 0
vsize: 841656
[startup+920.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18298
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 87557 90 17 6 25 0 11 0 544078853 861855744 37583 4294967295 134512640 134569956 3221224400 3221214624 1131228140 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 37583 13073 16 0 210398 0
vsize: 841656
[startup+930.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18302
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 88495 90 17 7 25 0 11 0 544078853 861855744 37995 4294967295 134512640 134569956 3221224400 3221214624 1131227553 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 37995 13073 16 0 210398 0
vsize: 841656
[startup+940.057 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18307
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 89442 91 17 7 25 0 11 0 544078853 861855744 38259 4294967295 134512640 134569956 3221224400 3221214720 1131277278 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 38259 13073 16 0 210398 0
vsize: 841656
[startup+950.057 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18312
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 90394 91 17 7 25 0 11 0 544078853 861855744 38490 4294967295 134512640 134569956 3221224400 3221214720 1131278637 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 38490 13073 16 0 210398 0
vsize: 841656
[startup+960.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18317
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 91347 92 18 7 25 0 11 0 544078853 861855744 38668 4294967295 134512640 134569956 3221224400 3221214760 1131459529 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 38668 13073 16 0 210398 0
vsize: 841656
[startup+970.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18321
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 92299 92 18 7 25 0 11 0 544078853 861855744 38845 4294967295 134512640 134569956 3221224400 3221214872 1131466993 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 38845 13073 16 0 210398 0
vsize: 841656
[startup+980.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18326
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 93251 92 18 7 25 0 11 0 544078853 861855744 39027 4294967295 134512640 134569956 3221224400 3221214624 1131227807 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 39027 13073 16 0 210398 0
vsize: 841656
[startup+990.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18331
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 94200 93 18 7 25 0 11 0 544078853 861855744 39145 4294967295 134512640 134569956 3221224400 3221214624 1131227835 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 39145 13073 16 0 210398 0
vsize: 841656
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18335
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 95146 94 19 7 25 0 11 0 544078853 861855744 39396 4294967295 134512640 134569956 3221224400 3221214720 1131278978 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 39396 13073 16 0 210398 0
vsize: 841656
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18340
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 96095 95 19 7 25 0 11 0 544078853 861855744 39576 4294967295 134512640 134569956 3221224400 3221214624 1131228464 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 39576 13073 16 0 210398 0
vsize: 841656
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18345
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 97047 95 19 7 25 0 11 0 544078853 861855744 39850 4294967295 134512640 134569956 3221224400 3221214760 1131459566 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 39850 13073 16 0 210398 0
vsize: 841656
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18349
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 97999 95 19 7 25 0 11 0 544078853 861855744 39993 4294967295 134512640 134569956 3221224400 3221214624 1131227084 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 39993 13073 16 0 210398 0
vsize: 841656
[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18354
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 98950 96 19 8 25 0 11 0 544078853 861855744 40153 4294967295 134512640 134569956 3221224400 3221214624 1131227692 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 40153 13073 16 0 210398 0
vsize: 841656
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18359
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 99901 97 19 8 25 0 11 0 544078853 861855744 40322 4294967295 134512640 134569956 3221224400 3221214760 1131458633 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 40322 13073 16 0 210398 0
vsize: 841656
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18363
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 100852 97 20 8 24 0 11 0 544078853 861855744 40525 4294967295 134512640 134569956 3221224400 3221214720 1131277248 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 40525 13073 16 0 210398 0
vsize: 841656
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18368
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 101810 98 20 8 25 0 11 0 544078853 861855744 40681 4294967295 134512640 134569956 3221224400 3221214624 1131228513 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 40681 13073 16 0 210398 0
vsize: 841656
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 18372
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 102762 99 20 8 25 0 11 0 544078853 861855744 40814 4294967295 134512640 134569956 3221224400 3221214624 1131227682 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 40814 13073 16 0 210398 0
vsize: 841656
[startup+1090.06 s]
Raw data (loadavg): 1.08 1.01 0.93 2/68 18381
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 103710 100 20 8 25 0 11 0 544078853 861855744 40969 4294967295 134512640 134569956 3221224400 3221214720 1131277322 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 40969 13073 16 0 210398 0
vsize: 841656
[startup+1100.07 s]
Raw data (loadavg): 1.14 1.03 0.94 2/64 18435
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 104657 105 20 8 25 0 11 0 544078853 861855744 41126 4294967295 134512640 134569956 3221224400 3221214624 1131227511 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210414 41126 13073 16 0 210398 0
vsize: 841656
[startup+1110.07 s]
Raw data (loadavg): 1.12 1.03 0.94 2/64 18439
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 105610 105 21 8 25 0 11 0 544078853 861855744 41351 4294967295 134512640 134569956 3221224400 3221214720 1131277349 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 41351 13073 16 0 210398 0
vsize: 841656
[startup+1120.07 s]
Raw data (loadavg): 1.10 1.03 0.94 2/64 18444
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 106565 105 21 8 25 0 11 0 544078853 861855744 41506 4294967295 134512640 134569956 3221224400 3221214720 1131277322 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 41506 13073 16 0 210398 0
vsize: 841656
[startup+1130.07 s]
Raw data (loadavg): 1.08 1.03 0.94 2/64 18449
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 107521 106 21 8 25 0 11 0 544078853 861855744 41666 4294967295 134512640 134569956 3221224400 3221214720 1131277174 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 41666 13073 16 0 210398 0
vsize: 841656
[startup+1140.07 s]
Raw data (loadavg): 1.07 1.03 0.94 2/64 18453
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 108480 106 21 9 25 0 11 0 544078853 861855744 41820 4294967295 134512640 134569956 3221224400 3221214624 1131227932 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 41820 13073 16 0 210398 0
vsize: 841656
[startup+1150.07 s]
Raw data (loadavg): 1.06 1.02 0.94 2/64 18458
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 109436 107 22 9 25 0 11 0 544078853 861855744 41926 4294967295 134512640 134569956 3221224400 3221214624 1131227785 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 41926 13073 16 0 210398 0
vsize: 841656
[startup+1160.07 s]
Raw data (loadavg): 1.05 1.02 0.94 2/64 18465
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 110391 107 22 9 25 0 11 0 544078853 861855744 42017 4294967295 134512640 134569956 3221224400 3221214720 1131277421 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 42017 13073 16 0 210398 0
vsize: 841656
[startup+1170.07 s]
Raw data (loadavg): 1.04 1.02 0.94 2/64 18469
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 111345 108 22 9 25 0 11 0 544078853 861855744 42147 4294967295 134512640 134569956 3221224400 3221214624 1131227303 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 42147 13073 16 0 210398 0
vsize: 841656
[startup+1180.07 s]
Raw data (loadavg): 1.04 1.02 0.94 2/64 18474
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 112299 108 22 9 24 0 11 0 544078853 861855744 42253 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 42253 13073 16 0 210398 0
vsize: 841656
[startup+1190.07 s]
Raw data (loadavg): 1.03 1.02 0.94 2/64 18479
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 113258 108 23 9 25 0 11 0 544078853 861855744 42486 4294967295 134512640 134569956 3221224400 3221214760 1131458748 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 42486 13073 16 0 210398 0
vsize: 841656
[startup+1200.07 s]
Raw data (loadavg): 1.02 1.02 0.94 2/64 18483
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 114214 108 23 9 25 0 11 0 544078853 861855744 42618 4294967295 134512640 134569956 3221224400 3221214720 1131279153 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 42618 13073 16 0 210398 0
vsize: 841656
[startup+1210.07 s]
Raw data (loadavg): 1.02 1.02 0.94 2/64 18488
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 115171 109 23 9 25 0 11 0 544078853 861855744 42718 4294967295 134512640 134569956 3221224400 3221214624 1131227077 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 42718 13073 16 0 210398 0
vsize: 841656
[startup+1220.07 s]
Raw data (loadavg): 1.02 1.02 0.94 2/64 18492
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 116127 109 24 9 25 0 11 0 544078853 861855744 42827 4294967295 134512640 134569956 3221224400 3221214624 1131227268 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 42827 13073 16 0 210398 0
vsize: 841656
[startup+1230.07 s]
Raw data (loadavg): 1.01 1.02 0.94 2/64 18497
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 117085 109 24 9 25 0 11 0 544078853 861855744 42994 4294967295 134512640 134569956 3221224400 3221214624 1131227553 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 42994 13073 16 0 210398 0
vsize: 841656
[startup+1240.07 s]
Raw data (loadavg): 1.01 1.02 0.94 2/64 18502
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 118042 110 24 9 25 0 11 0 544078853 861855744 43078 4294967295 134512640 134569956 3221224400 3221214624 1131228389 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 43078 13073 16 0 210398 0
vsize: 841656
[startup+1250.07 s]
Raw data (loadavg): 1.01 1.01 0.94 2/64 18506
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 118999 110 24 9 25 0 11 0 544078853 861855744 43208 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 43208 13073 16 0 210398 0
vsize: 841656
[startup+1260.07 s]
Raw data (loadavg): 1.01 1.01 0.94 2/64 18511
Raw data (stat): 17894 (java) R 17893 11931 11930 0 -1 0 18057 3 1 0 119950 110 25 9 25 0 11 0 544078853 861855744 43314 4294967295 134512640 134569956 3221224400 3221214624 1131227597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210414 43314 13073 16 0 210398 0
vsize: 841656
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1260.19 s]
Raw data (loadavg): 1.01 1.01 0.94 1/54 18513
Raw data (stat): 17894 (java) Z 17893 11931 11930 0 -1 1036 18057 31090 1 2 119953 118 7076 98 25 0 1 0 544078853 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): 1260.18
CPU time (s): 1272.47
CPU user time (s): 1270.3
CPU system time (s): 2.16767
CPU usage (%): 100.975
Max. virtual memory (Kb): 844912
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####