PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-net12.opb
MD5SUM	1e83ed64f0fd862e44095daf089e38c2
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	351
Biggest coefficient in the objective function	524288000000
Number of bits for the biggest coefficient in the objective function	39
Sum of the numbers in the objective function	1048594922917
Number of bits of the sum of numbers in the objective function	40
Biggest number in a constraint	1075200000000000000
Number of bits of the biggest number in a constraint	60
Biggest sum of numbers in a constraint	2440670651161677657
Number of bits of the biggest sum of numbers	62
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1256.38
Number of variables	653
Total number of constraints	707
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	338
Number of constraints which are nor clauses,nor cardinality constraints	369
Minimum length of a constraint	1
Maximum length of a constraint	75
Trace number 14342

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        695848 kB
Buffers:         31464 kB
Cached:         273076 kB
SwapCached:        508 kB
Active:          31268 kB
Inactive:       275528 kB
HighTotal:      131008 kB
HighFree:        16772 kB
LowTotal:       903652 kB
LowFree:        679076 kB
SwapTotal:     2097892 kB
SwapFree:      2096708 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5932 kB
Slab:            26196 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 23:59:44 (client local time) WITH STATUS 143 IN 1243.51 SECONDS
stats: 20146 7 1243.51 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-net12.opb
c reading problem 
c [nbvar=653]
c [nbconstr=707]
c time 3.944
c #vars     653
c #clauses  442
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=616175339
c Current CPU time (ms) : 18.463
c starts	: 2
c conflicts	: 130
c decisions	: 1121
c propagations	: 3118
c inspects	: 30537
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 130
c root simplifications	: 2
c 
c CURRENT OPTIMUM=606726375
c Current CPU time (ms) : 19.821
c starts	: 3
c conflicts	: 145
c decisions	: 1603
c propagations	: 4084
c inspects	: 41459
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 145
c root simplifications	: 3
c 
c CURRENT OPTIMUM=548085060
c Current CPU time (ms) : 21.544
c starts	: 4
c conflicts	: 159
c decisions	: 2076
c propagations	: 5040
c inspects	: 52444
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 159
c root simplifications	: 4
c 
c CURRENT OPTIMUM=548001948
c Current CPU time (ms) : 22.068
c starts	: 5
c conflicts	: 159
c decisions	: 2447
c propagations	: 5689
c inspects	: 60964
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 159
c root simplifications	: 5
c 
c CURRENT OPTIMUM=547551388
c Current CPU time (ms) : 22.698
c starts	: 6
c conflicts	: 163
c decisions	: 2818
c propagations	: 6354
c inspects	: 63903
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 163
c root simplifications	: 6
c 
c CURRENT OPTIMUM=547311173
c Current CPU time (ms) : 23.449
c starts	: 7
c conflicts	: 167
c decisions	: 3174
c propagations	: 7041
c inspects	: 68859
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 167
c root simplifications	: 7
c 
c CURRENT OPTIMUM=545835156
c Current CPU time (ms) : 24.119
c starts	: 8
c conflicts	: 170
c decisions	: 3590
c propagations	: 7795
c inspects	: 76173
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 170
c root simplifications	: 8
c 
c CURRENT OPTIMUM=488352973
c Current CPU time (ms) : 32.472
c starts	: 10
c conflicts	: 279
c decisions	: 4337
c propagations	: 9658
c inspects	: 102982
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 279
c root simplifications	: 10
c 
c CURRENT OPTIMUM=482974933
c Current CPU time (ms) : 38.102
c starts	: 11
c conflicts	: 296
c decisions	: 5002
c propagations	: 11030
c inspects	: 123564
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 11
c 
c CURRENT OPTIMUM=422433580
c Current CPU time (ms) : 39.548
c starts	: 12
c conflicts	: 296
c decisions	: 5362
c propagations	: 11679
c inspects	: 134251
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 12
c 
c CURRENT OPTIMUM=358433580
c Current CPU time (ms) : 40.718
c starts	: 13
c conflicts	: 296
c decisions	: 5723
c propagations	: 12328
c inspects	: 136743
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 13
c 
c CURRENT OPTIMUM=294433580
c Current CPU time (ms) : 41.937
c starts	: 14
c conflicts	: 296
c decisions	: 6083
c propagations	: 12977
c inspects	: 139217
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 14
c 
c CURRENT OPTIMUM=230433580
c Current CPU time (ms) : 43.11
c starts	: 15
c conflicts	: 296
c decisions	: 6443
c propagations	: 13626
c inspects	: 141695
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 15
c 
c CURRENT OPTIMUM=166433580
c Current CPU time (ms) : 44.331
c starts	: 16
c conflicts	: 296
c decisions	: 6802
c propagations	: 14275
c inspects	: 144169
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 16
c 
c CURRENT OPTIMUM=102433580
c Current CPU time (ms) : 45.533
c starts	: 17
c conflicts	: 296
c decisions	: 7163
c propagations	: 14924
c inspects	: 146669
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 17
c 
c CURRENT OPTIMUM=38433580
c Current CPU time (ms) : 46.769
c starts	: 18
c conflicts	: 296
c decisions	: 7523
c propagations	: 15573
c inspects	: 149157
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 18
c 
c CURRENT OPTIMUM=-25566420
c Current CPU time (ms) : 47.965
c starts	: 19
c conflicts	: 296
c decisions	: 7883
c propagations	: 16222
c inspects	: 151650
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 19
c 
c CURRENT OPTIMUM=-89566420
c Current CPU time (ms) : 49.198
c starts	: 20
c conflicts	: 296
c decisions	: 8242
c propagations	: 16871
c inspects	: 154135
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 20
c 
c CURRENT OPTIMUM=-153566420
c Current CPU time (ms) : 50.39
c starts	: 21
c conflicts	: 296
c decisions	: 8602
c propagations	: 17520
c inspects	: 156636
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 21
c 
c CURRENT OPTIMUM=-217566420
c Current CPU time (ms) : 51.629
c starts	: 22
c conflicts	: 296
c decisions	: 8961
c propagations	: 18169
c inspects	: 159127
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 22
c 
c CURRENT OPTIMUM=-281566420
c Current CPU time (ms) : 52.808
c starts	: 23
c conflicts	: 296
c decisions	: 9320
c propagations	: 18818
c inspects	: 161621
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 23
c 
c CURRENT OPTIMUM=-345566420
c Current CPU time (ms) : 54.028
c starts	: 24
c conflicts	: 296
c decisions	: 9678
c propagations	: 19467
c inspects	: 164103
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 24
c 
c CURRENT OPTIMUM=-409566420
c Current CPU time (ms) : 55.248
c starts	: 25
c conflicts	: 296
c decisions	: 10039
c propagations	: 20116
c inspects	: 166642
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 25
c 
c CURRENT OPTIMUM=-473566420
c Current CPU time (ms) : 56.518
c starts	: 26
c conflicts	: 296
c decisions	: 10399
c propagations	: 20765
c inspects	: 169162
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 26
c 
c CURRENT OPTIMUM=-537566420
c Current CPU time (ms) : 57.744
c starts	: 27
c conflicts	: 296
c decisions	: 10759
c propagations	: 21414
c inspects	: 171686
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 27
c 
c CURRENT OPTIMUM=-601566420
c Current CPU time (ms) : 59.007
c starts	: 28
c conflicts	: 296
c decisions	: 11118
c propagations	: 22063
c inspects	: 174195
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 28
c 
c CURRENT OPTIMUM=-665566420
c Current CPU time (ms) : 60.212
c starts	: 29
c conflicts	: 296
c decisions	: 11478
c propagations	: 22712
c inspects	: 176727
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 29
c 
c CURRENT OPTIMUM=-729566420
c Current CPU time (ms) : 61.477
c starts	: 30
c conflicts	: 296
c decisions	: 11837
c propagations	: 23361
c inspects	: 179242
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 30
c 
c CURRENT OPTIMUM=-793566420
c Current CPU time (ms) : 62.677
c starts	: 31
c conflicts	: 296
c decisions	: 12196
c propagations	: 24010
c inspects	: 181760
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 31
c 
c CURRENT OPTIMUM=-857566420
c Current CPU time (ms) : 63.918
c starts	: 32
c conflicts	: 296
c decisions	: 12554
c propagations	: 24659
c inspects	: 184258
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 32
c 
c CURRENT OPTIMUM=-921566420
c Current CPU time (ms) : 65.149
c starts	: 33
c conflicts	: 296
c decisions	: 12914
c propagations	: 25308
c inspects	: 186806
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 33
c 
c CURRENT OPTIMUM=-985566420
c Current CPU time (ms) : 66.418
c starts	: 34
c conflicts	: 296
c decisions	: 13273
c propagations	: 25957
c inspects	: 189333
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 34
c 
c CURRENT OPTIMUM=-1049566420
c Current CPU time (ms) : 67.623
c starts	: 35
c conflicts	: 296
c decisions	: 13632
c propagations	: 26606
c inspects	: 191863
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 35
c 
c CURRENT OPTIMUM=-1113566420
c Current CPU time (ms) : 68.87
c starts	: 36
c conflicts	: 296
c decisions	: 13990
c propagations	: 27255
c inspects	: 194369
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 36
c 
c CURRENT OPTIMUM=-1177566420
c Current CPU time (ms) : 70.069
c starts	: 37
c conflicts	: 296
c decisions	: 14349
c propagations	: 27904
c inspects	: 196905
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 37
c 
c CURRENT OPTIMUM=-1241566420
c Current CPU time (ms) : 71.331
c starts	: 38
c conflicts	: 296
c decisions	: 14707
c propagations	: 28553
c inspects	: 199415
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 38
c 
c CURRENT OPTIMUM=-1305566420
c Current CPU time (ms) : 72.515
c starts	: 39
c conflicts	: 296
c decisions	: 15065
c propagations	: 29202
c inspects	: 201927
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 39
c 
c CURRENT OPTIMUM=-1369566420
c Current CPU time (ms) : 73.729
c starts	: 40
c conflicts	: 296
c decisions	: 15422
c propagations	: 29851
c inspects	: 204410
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 40
c 
c CURRENT OPTIMUM=-1433566420
c Current CPU time (ms) : 74.974
c starts	: 41
c conflicts	: 296
c decisions	: 15781
c propagations	: 30500
c inspects	: 207030
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 41
c 
c CURRENT OPTIMUM=-1497566420
c Current CPU time (ms) : 76.696
c starts	: 42
c conflicts	: 296
c decisions	: 16139
c propagations	: 31149
c inspects	: 209967
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 42
c 
c CURRENT OPTIMUM=-1561566420
c Current CPU time (ms) : 80.382
c starts	: 43
c conflicts	: 296
c decisions	: 16494
c propagations	: 31798
c inspects	: 214781
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 43
c 
c CURRENT OPTIMUM=-1625566420
c Current CPU time (ms) : 84.211
c starts	: 44
c conflicts	: 296
c decisions	: 16848
c propagations	: 32447
c inspects	: 219694
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 44
c 
c CURRENT OPTIMUM=-1689566420
c Current CPU time (ms) : 88.188
c starts	: 45
c conflicts	: 296
c decisions	: 17203
c propagations	: 33096
c inspects	: 224790
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 45
c 
c CURRENT OPTIMUM=-1753566420
c Current CPU time (ms) : 92.303
c starts	: 46
c conflicts	: 296
c decisions	: 17557
c propagations	: 33745
c inspects	: 229991
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 46
c 
c CURRENT OPTIMUM=-1817566420
c Current CPU time (ms) : 96.545
c starts	: 47
c conflicts	: 296
c decisions	: 17910
c propagations	: 34394
c inspects	: 235338
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 47
c 
c CURRENT OPTIMUM=-1881566420
c Current CPU time (ms) : 100.877
c starts	: 48
c conflicts	: 296
c decisions	: 18262
c propagations	: 35043
c inspects	: 240799
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 48
c 
c CURRENT OPTIMUM=-1913566420
c Current CPU time (ms) : 105.357
c starts	: 49
c conflicts	: 296
c decisions	: 18612
c propagations	: 35692
c inspects	: 246383
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 49
c 
c CURRENT OPTIMUM=-1929566420
c Current CPU time (ms) : 109.908
c starts	: 50
c conflicts	: 296
c decisions	: 18960
c propagations	: 36341
c inspects	: 252082
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 50
c 
c CURRENT OPTIMUM=-1930566420
c Current CPU time (ms) : 114.559
c starts	: 51
c conflicts	: 296
c decisions	: 19306
c propagations	: 36990
c inspects	: 257893
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 51
c 
c CURRENT OPTIMUM=-1931566420
c Current CPU time (ms) : 119.372
c starts	: 52
c conflicts	: 296
c decisions	: 19652
c propagations	: 37639
c inspects	: 263842
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 52
c 
c CURRENT OPTIMUM=-1932566420
c Current CPU time (ms) : 124.261
c starts	: 53
c conflicts	: 296
c decisions	: 19997
c propagations	: 38288
c inspects	: 269892
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 53
c 
c CURRENT OPTIMUM=-1933566420
c Current CPU time (ms) : 129.362
c starts	: 54
c conflicts	: 296
c decisions	: 20343
c propagations	: 38937
c inspects	: 276122
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 54
c 
c CURRENT OPTIMUM=-1934566420
c Current CPU time (ms) : 134.572
c starts	: 55
c conflicts	: 296
c decisions	: 20688
c propagations	: 39586
c inspects	: 282451
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 55
c 
c CURRENT OPTIMUM=-1935566420
c Current CPU time (ms) : 139.886
c starts	: 56
c conflicts	: 296
c decisions	: 21032
c propagations	: 40235
c inspects	: 288920
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 56
c 
c CURRENT OPTIMUM=-1936566420
c Current CPU time (ms) : 145.259
c starts	: 57
c conflicts	: 296
c decisions	: 21375
c propagations	: 40884
c inspects	: 295494
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 57
c 
c CURRENT OPTIMUM=-1937566420
c Current CPU time (ms) : 150.897
c starts	: 58
c conflicts	: 296
c decisions	: 21720
c propagations	: 41533
c inspects	: 302286
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 58
c 
c CURRENT OPTIMUM=-1938566420
c Current CPU time (ms) : 156.621
c starts	: 59
c conflicts	: 296
c decisions	: 22064
c propagations	: 42182
c inspects	: 309174
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 59
c 
c CURRENT OPTIMUM=-1939566420
c Current CPU time (ms) : 162.482
c starts	: 60
c conflicts	: 296
c decisions	: 22408
c propagations	: 42831
c inspects	: 316202
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 60
c 
c CURRENT OPTIMUM=-1940566420
c Current CPU time (ms) : 168.473
c starts	: 61
c conflicts	: 296
c decisions	: 22751
c propagations	: 43480
c inspects	: 323331
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 61
c 
c CURRENT OPTIMUM=-1941566420
c Current CPU time (ms) : 174.648
c starts	: 62
c conflicts	: 296
c decisions	: 23095
c propagations	: 44129
c inspects	: 330638
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 62
c 
c CURRENT OPTIMUM=-1942566420
c Current CPU time (ms) : 180.966
c starts	: 63
c conflicts	: 296
c decisions	: 23438
c propagations	: 44778
c inspects	: 338044
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 63
c 
c CURRENT OPTIMUM=-1943566420
c Current CPU time (ms) : 187.4
c starts	: 64
c conflicts	: 296
c decisions	: 23780
c propagations	: 45427
c inspects	: 345589
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 64
c 
c CURRENT OPTIMUM=-1944566420
c Current CPU time (ms) : 193.959
c starts	: 65
c conflicts	: 296
c decisions	: 24121
c propagations	: 46076
c inspects	: 353229
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 296
c root simplifications	: 65
c 
c CURRENT OPTIMUM=-1944566422
c Current CPU time (ms) : 202.317
c starts	: 66
c conflicts	: 297
c decisions	: 24543
c propagations	: 46879
c inspects	: 363235
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 297
c root simplifications	: 66
c 
c CURRENT OPTIMUM=-1944611024
c Current CPU time (ms) : 215.867
c starts	: 67
c conflicts	: 309
c decisions	: 25208
c propagations	: 48185
c inspects	: 384245
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 309
c root simplifications	: 67
c 
c CURRENT OPTIMUM=1831740968
c Current CPU time (ms) : 221.647
c starts	: 68
c conflicts	: 319
c decisions	: 25741
c propagations	: 49304
c inspects	: 404351
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 68
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 225.416
c starts	: 69
c conflicts	: 319
c decisions	: 26094
c propagations	: 49953
c inspects	: 417646
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 69
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 228.757
c starts	: 70
c conflicts	: 319
c decisions	: 26447
c propagations	: 50602
c inspects	: 421824
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 70
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 232.088
c starts	: 71
c conflicts	: 319
c decisions	: 26800
c propagations	: 51251
c inspects	: 425994
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 71
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 235.433
c starts	: 72
c conflicts	: 319
c decisions	: 27153
c propagations	: 51900
c inspects	: 430164
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 72
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 238.773
c starts	: 73
c conflicts	: 319
c decisions	: 27506
c propagations	: 52549
c inspects	: 434334
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 73
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 242.134
c starts	: 74
c conflicts	: 319
c decisions	: 27859
c propagations	: 53198
c inspects	: 438504
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 74
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 245.489
c starts	: 75
c conflicts	: 319
c decisions	: 28212
c propagations	: 53847
c inspects	: 442674
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 75
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 248.848
c starts	: 76
c conflicts	: 319
c decisions	: 28565
c propagations	: 54496
c inspects	: 446844
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 76
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 252.178
c starts	: 77
c conflicts	: 319
c decisions	: 28918
c propagations	: 55145
c inspects	: 451014
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 77
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 255.504
c starts	: 78
c conflicts	: 319
c decisions	: 29271
c propagations	: 55794
c inspects	: 455184
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 78
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 258.839
c starts	: 79
c conflicts	: 319
c decisions	: 29624
c propagations	: 56443
c inspects	: 459354
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 79
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 262.171
c starts	: 80
c conflicts	: 319
c decisions	: 29977
c propagations	: 57092
c inspects	: 463524
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 80
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 265.496
c starts	: 81
c conflicts	: 319
c decisions	: 30330
c propagations	: 57741
c inspects	: 467694
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 81
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 268.827
c starts	: 82
c conflicts	: 319
c decisions	: 30683
c propagations	: 58390
c inspects	: 471864
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 82
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 272.147
c starts	: 83
c conflicts	: 319
c decisions	: 31036
c propagations	: 59039
c inspects	: 476034
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 83
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 275.494
c starts	: 84
c conflicts	: 319
c decisions	: 31389
c propagations	: 59688
c inspects	: 480204
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 84
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 278.817
c starts	: 85
c conflicts	: 319
c decisions	: 31742
c propagations	: 60337
c inspects	: 484374
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 85
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 282.159
c starts	: 86
c conflicts	: 319
c decisions	: 32095
c propagations	: 60986
c inspects	: 488544
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 86
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 285.51
c starts	: 87
c conflicts	: 319
c decisions	: 32448
c propagations	: 61635
c inspects	: 492714
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 87
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 288.839
c starts	: 88
c conflicts	: 319
c decisions	: 32801
c propagations	: 62284
c inspects	: 496884
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 88
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 292.176
c starts	: 89
c conflicts	: 319
c decisions	: 33154
c propagations	: 62933
c inspects	: 501054
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 89
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 295.511
c starts	: 90
c conflicts	: 319
c decisions	: 33507
c propagations	: 63582
c inspects	: 505224
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 90
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 298.838
c starts	: 91
c conflicts	: 319
c decisions	: 33860
c propagations	: 64231
c inspects	: 509394
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 91
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 302.158
c starts	: 92
c conflicts	: 319
c decisions	: 34213
c propagations	: 64880
c inspects	: 513564
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 92
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 305.499
c starts	: 93
c conflicts	: 319
c decisions	: 34566
c propagations	: 65529
c inspects	: 517734
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 93
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 308.83
c starts	: 94
c conflicts	: 319
c decisions	: 34919
c propagations	: 66178
c inspects	: 521904
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 94
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 312.174
c starts	: 95
c conflicts	: 319
c decisions	: 35272
c propagations	: 66827
c inspects	: 526074
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 95
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 315.507
c starts	: 96
c conflicts	: 319
c decisions	: 35625
c propagations	: 67476
c inspects	: 530244
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 96
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 318.837
c starts	: 97
c conflicts	: 319
c decisions	: 35978
c propagations	: 68125
c inspects	: 534414
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 97
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 322.17
c starts	: 98
c conflicts	: 319
c decisions	: 36331
c propagations	: 68774
c inspects	: 538584
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 98
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 325.491
c starts	: 99
c conflicts	: 319
c decisions	: 36684
c propagations	: 69423
c inspects	: 542754
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 99
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 328.819
c starts	: 100
c conflicts	: 319
c decisions	: 37037
c propagations	: 70072
c inspects	: 546924
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 100
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 332.141
c starts	: 101
c conflicts	: 319
c decisions	: 37390
c propagations	: 70721
c inspects	: 551094
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 101
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 335.484
c starts	: 102
c conflicts	: 319
c decisions	: 37743
c propagations	: 71370
c inspects	: 555264
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 102
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 338.812
c starts	: 103
c conflicts	: 319
c decisions	: 38096
c propagations	: 72019
c inspects	: 559434
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 103
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 342.16
c starts	: 104
c conflicts	: 319
c decisions	: 38449
c propagations	: 72668
c inspects	: 563604
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 104
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 345.521
c starts	: 105
c conflicts	: 319
c decisions	: 38802
c propagations	: 73317
c inspects	: 567774
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 105
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 348.855
c starts	: 106
c conflicts	: 319
c decisions	: 39155
c propagations	: 73966
c inspects	: 571944
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 106
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 352.181
c starts	: 107
c conflicts	: 319
c decisions	: 39508
c propagations	: 74615
c inspects	: 576114
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 107
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 355.517
c starts	: 108
c conflicts	: 319
c decisions	: 39861
c propagations	: 75264
c inspects	: 580284
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 108
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 358.858
c starts	: 109
c conflicts	: 319
c decisions	: 40214
c propagations	: 75913
c inspects	: 584454
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 109
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 362.211
c starts	: 110
c conflicts	: 319
c decisions	: 40567
c propagations	: 76562
c inspects	: 588624
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 110
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 365.554
c starts	: 111
c conflicts	: 319
c decisions	: 40920
c propagations	: 77211
c inspects	: 592794
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 111
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 368.905
c starts	: 112
c conflicts	: 319
c decisions	: 41273
c propagations	: 77860
c inspects	: 596964
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 112
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 372.243
c starts	: 113
c conflicts	: 319
c decisions	: 41626
c propagations	: 78509
c inspects	: 601134
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 113
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 375.596
c starts	: 114
c conflicts	: 319
c decisions	: 41979
c propagations	: 79158
c inspects	: 605304
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 114
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 378.957
c starts	: 115
c conflicts	: 319
c decisions	: 42332
c propagations	: 79807
c inspects	: 609474
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 115
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 382.32
c starts	: 116
c conflicts	: 319
c decisions	: 42685
c propagations	: 80456
c inspects	: 613644
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 116
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 385.685
c starts	: 117
c conflicts	: 319
c decisions	: 43038
c propagations	: 81105
c inspects	: 617814
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 117
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 389.018
c starts	: 118
c conflicts	: 319
c decisions	: 43391
c propagations	: 81754
c inspects	: 621984
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 118
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 392.366
c starts	: 119
c conflicts	: 319
c decisions	: 43744
c propagations	: 82403
c inspects	: 626154
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 119
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 395.694
c starts	: 120
c conflicts	: 319
c decisions	: 44097
c propagations	: 83052
c inspects	: 630324
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 120
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 399.019
c starts	: 121
c conflicts	: 319
c decisions	: 44450
c propagations	: 83701
c inspects	: 634494
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 121
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 402.358
c starts	: 122
c conflicts	: 319
c decisions	: 44803
c propagations	: 84350
c inspects	: 638664
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 122
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 405.693
c starts	: 123
c conflicts	: 319
c decisions	: 45156
c propagations	: 84999
c inspects	: 642834
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 123
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 409.017
c starts	: 124
c conflicts	: 319
c decisions	: 45509
c propagations	: 85648
c inspects	: 647004
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 124
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 412.369
c starts	: 125
c conflicts	: 319
c decisions	: 45862
c propagations	: 86297
c inspects	: 651174
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 125
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 415.707
c starts	: 126
c conflicts	: 319
c decisions	: 46215
c propagations	: 86946
c inspects	: 655344
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 126
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 419.041
c starts	: 127
c conflicts	: 319
c decisions	: 46568
c propagations	: 87595
c inspects	: 659514
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 127
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 422.388
c starts	: 128
c conflicts	: 319
c decisions	: 46921
c propagations	: 88244
c inspects	: 663684
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 128
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 425.724
c starts	: 129
c conflicts	: 319
c decisions	: 47274
c propagations	: 88893
c inspects	: 667854
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 129
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 429.052
c starts	: 130
c conflicts	: 319
c decisions	: 47627
c propagations	: 89542
c inspects	: 672024
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 130
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 432.376
c starts	: 131
c conflicts	: 319
c decisions	: 47980
c propagations	: 90191
c inspects	: 676194
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 131
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 435.718
c starts	: 132
c conflicts	: 319
c decisions	: 48333
c propagations	: 90840
c inspects	: 680364
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 132
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 439.08
c starts	: 133
c conflicts	: 319
c decisions	: 48686
c propagations	: 91489
c inspects	: 684534
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 133
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 442.413
c starts	: 134
c conflicts	: 319
c decisions	: 49039
c propagations	: 92138
c inspects	: 688704
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 134
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 445.769
c starts	: 135
c conflicts	: 319
c decisions	: 49392
c propagations	: 92787
c inspects	: 692874
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 135
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 449.108
c starts	: 136
c conflicts	: 319
c decisions	: 49745
c propagations	: 93436
c inspects	: 697044
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 136
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 452.456
c starts	: 137
c conflicts	: 319
c decisions	: 50098
c propagations	: 94085
c inspects	: 701214
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 137
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 455.8
c starts	: 138
c conflicts	: 319
c decisions	: 50451
c propagations	: 94734
c inspects	: 705384
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 138
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 459.151
c starts	: 139
c conflicts	: 319
c decisions	: 50804
c propagations	: 95383
c inspects	: 709554
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 139
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 462.489
c starts	: 140
c conflicts	: 319
c decisions	: 51157
c propagations	: 96032
c inspects	: 713724
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 140
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 465.84
c starts	: 141
c conflicts	: 319
c decisions	: 51510
c propagations	: 96681
c inspects	: 717894
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 141
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 469.192
c starts	: 142
c conflicts	: 319
c decisions	: 51863
c propagations	: 97330
c inspects	: 722064
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 142
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 472.531
c starts	: 143
c conflicts	: 319
c decisions	: 52216
c propagations	: 97979
c inspects	: 726234
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 143
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 475.863
c starts	: 144
c conflicts	: 319
c decisions	: 52569
c propagations	: 98628
c inspects	: 730404
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 144
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 479.22
c starts	: 145
c conflicts	: 319
c decisions	: 52922
c propagations	: 99277
c inspects	: 734574
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 145
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 482.56
c starts	: 146
c conflicts	: 319
c decisions	: 53275
c propagations	: 99926
c inspects	: 738744
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 146
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 485.893
c starts	: 147
c conflicts	: 319
c decisions	: 53628
c propagations	: 100575
c inspects	: 742914
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 147
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 489.231
c starts	: 148
c conflicts	: 319
c decisions	: 53981
c propagations	: 101224
c inspects	: 747084
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 148
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 492.576
c starts	: 149
c conflicts	: 319
c decisions	: 54334
c propagations	: 101873
c inspects	: 751254
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 149
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 495.926
c starts	: 150
c conflicts	: 319
c decisions	: 54687
c propagations	: 102522
c inspects	: 755424
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 150
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 499.261
c starts	: 151
c conflicts	: 319
c decisions	: 55040
c propagations	: 103171
c inspects	: 759594
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 151
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 502.621
c starts	: 152
c conflicts	: 319
c decisions	: 55393
c propagations	: 103820
c inspects	: 763764
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 152
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 505.961
c starts	: 153
c conflicts	: 319
c decisions	: 55746
c propagations	: 104469
c inspects	: 767934
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 153
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 509.281
c starts	: 154
c conflicts	: 319
c decisions	: 56099
c propagations	: 105118
c inspects	: 772104
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 154
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 512.625
c starts	: 155
c conflicts	: 319
c decisions	: 56452
c propagations	: 105767
c inspects	: 776274
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 155
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 515.96
c starts	: 156
c conflicts	: 319
c decisions	: 56805
c propagations	: 106416
c inspects	: 780444
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 156
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 519.299
c starts	: 157
c conflicts	: 319
c decisions	: 57158
c propagations	: 107065
c inspects	: 784614
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 157
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 522.641
c starts	: 158
c conflicts	: 319
c decisions	: 57511
c propagations	: 107714
c inspects	: 788784
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 158
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 525.981
c starts	: 159
c conflicts	: 319
c decisions	: 57864
c propagations	: 108363
c inspects	: 792954
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 159
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 529.321
c starts	: 160
c conflicts	: 319
c decisions	: 58217
c propagations	: 109012
c inspects	: 797124
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 160
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 532.63
c starts	: 161
c conflicts	: 319
c decisions	: 58570
c propagations	: 109661
c inspects	: 801294
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 161
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 535.967
c starts	: 162
c conflicts	: 319
c decisions	: 58923
c propagations	: 110310
c inspects	: 805464
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 162
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 539.288
c starts	: 163
c conflicts	: 319
c decisions	: 59276
c propagations	: 110959
c inspects	: 809634
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 163
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 542.608
c starts	: 164
c conflicts	: 319
c decisions	: 59629
c propagations	: 111608
c inspects	: 813804
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 164
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 545.937
c starts	: 165
c conflicts	: 319
c decisions	: 59982
c propagations	: 112257
c inspects	: 817974
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 165
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 549.261
c starts	: 166
c conflicts	: 319
c decisions	: 60335
c propagations	: 112906
c inspects	: 822144
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 166
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 552.603
c starts	: 167
c conflicts	: 319
c decisions	: 60688
c propagations	: 113555
c inspects	: 826314
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 167
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 555.924
c starts	: 168
c conflicts	: 319
c decisions	: 61041
c propagations	: 114204
c inspects	: 830484
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 168
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 559.258
c starts	: 169
c conflicts	: 319
c decisions	: 61394
c propagations	: 114853
c inspects	: 834654
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 169
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 562.588
c starts	: 170
c conflicts	: 319
c decisions	: 61747
c propagations	: 115502
c inspects	: 838824
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 170
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 565.922
c starts	: 171
c conflicts	: 319
c decisions	: 62100
c propagations	: 116151
c inspects	: 842994
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 171
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 569.275
c starts	: 172
c conflicts	: 319
c decisions	: 62453
c propagations	: 116800
c inspects	: 847164
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 172
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 572.625
c starts	: 173
c conflicts	: 319
c decisions	: 62806
c propagations	: 117449
c inspects	: 851334
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 173
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 575.97
c starts	: 174
c conflicts	: 319
c decisions	: 63159
c propagations	: 118098
c inspects	: 855504
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 174
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 579.303
c starts	: 175
c conflicts	: 319
c decisions	: 63512
c propagations	: 118747
c inspects	: 859674
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 175
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 582.63
c starts	: 176
c conflicts	: 319
c decisions	: 63865
c propagations	: 119396
c inspects	: 863844
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 176
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 585.958
c starts	: 177
c conflicts	: 319
c decisions	: 64218
c propagations	: 120045
c inspects	: 868014
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 177
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 589.3
c starts	: 178
c conflicts	: 319
c decisions	: 64571
c propagations	: 120694
c inspects	: 872184
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 178
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 592.644
c starts	: 179
c conflicts	: 319
c decisions	: 64924
c propagations	: 121343
c inspects	: 876354
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 179
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 595.97
c starts	: 180
c conflicts	: 319
c decisions	: 65277
c propagations	: 121992
c inspects	: 880524
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 180
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 599.301
c starts	: 181
c conflicts	: 319
c decisions	: 65630
c propagations	: 122641
c inspects	: 884694
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 181
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 602.633
c starts	: 182
c conflicts	: 319
c decisions	: 65983
c propagations	: 123290
c inspects	: 888864
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 182
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 605.955
c starts	: 183
c conflicts	: 319
c decisions	: 66336
c propagations	: 123939
c inspects	: 893034
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 183
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 609.303
c starts	: 184
c conflicts	: 319
c decisions	: 66689
c propagations	: 124588
c inspects	: 897204
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 184
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 612.654
c starts	: 185
c conflicts	: 319
c decisions	: 67042
c propagations	: 125237
c inspects	: 901374
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 185
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 615.984
c starts	: 186
c conflicts	: 319
c decisions	: 67395
c propagations	: 125886
c inspects	: 905544
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 186
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 619.317
c starts	: 187
c conflicts	: 319
c decisions	: 67748
c propagations	: 126535
c inspects	: 909714
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 187
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 622.648
c starts	: 188
c conflicts	: 319
c decisions	: 68101
c propagations	: 127184
c inspects	: 913884
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 188
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 625.976
c starts	: 189
c conflicts	: 319
c decisions	: 68454
c propagations	: 127833
c inspects	: 918054
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 189
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 629.327
c starts	: 190
c conflicts	: 319
c decisions	: 68807
c propagations	: 128482
c inspects	: 922224
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 190
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 632.682
c starts	: 191
c conflicts	: 319
c decisions	: 69160
c propagations	: 129131
c inspects	: 926394
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 191
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 636.02
c starts	: 192
c conflicts	: 319
c decisions	: 69513
c propagations	: 129780
c inspects	: 930564
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 192
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 639.355
c starts	: 193
c conflicts	: 319
c decisions	: 69866
c propagations	: 130429
c inspects	: 934734
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 193
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 642.702
c starts	: 194
c conflicts	: 319
c decisions	: 70219
c propagations	: 131078
c inspects	: 938904
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 194
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 646.061
c starts	: 195
c conflicts	: 319
c decisions	: 70572
c propagations	: 131727
c inspects	: 943074
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 195
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 649.413
c starts	: 196
c conflicts	: 319
c decisions	: 70925
c propagations	: 132376
c inspects	: 947244
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 196
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 652.772
c starts	: 197
c conflicts	: 319
c decisions	: 71278
c propagations	: 133025
c inspects	: 951414
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 197
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 656.138
c starts	: 198
c conflicts	: 319
c decisions	: 71631
c propagations	: 133674
c inspects	: 955584
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 198
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 659.515
c starts	: 199
c conflicts	: 319
c decisions	: 71984
c propagations	: 134323
c inspects	: 959754
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 199
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 662.892
c starts	: 200
c conflicts	: 319
c decisions	: 72337
c propagations	: 134972
c inspects	: 963924
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 200
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 666.254
c starts	: 201
c conflicts	: 319
c decisions	: 72690
c propagations	: 135621
c inspects	: 968094
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 201
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 668.797
c starts	: 202
c conflicts	: 319
c decisions	: 73043
c propagations	: 136270
c inspects	: 972264
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 202
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 671.333
c starts	: 203
c conflicts	: 319
c decisions	: 73396
c propagations	: 136919
c inspects	: 976434
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 203
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 673.884
c starts	: 204
c conflicts	: 319
c decisions	: 73749
c propagations	: 137568
c inspects	: 980604
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 204
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 676.421
c starts	: 205
c conflicts	: 319
c decisions	: 74102
c propagations	: 138217
c inspects	: 984774
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 205
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 678.956
c starts	: 206
c conflicts	: 319
c decisions	: 74455
c propagations	: 138866
c inspects	: 988944
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 206
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 681.492
c starts	: 207
c conflicts	: 319
c decisions	: 74808
c propagations	: 139515
c inspects	: 993114
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 207
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 684.016
c starts	: 208
c conflicts	: 319
c decisions	: 75161
c propagations	: 140164
c inspects	: 997284
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 208
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 686.542
c starts	: 209
c conflicts	: 319
c decisions	: 75514
c propagations	: 140813
c inspects	: 1001454
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 209
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 689.061
c starts	: 210
c conflicts	: 319
c decisions	: 75867
c propagations	: 141462
c inspects	: 1005624
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 210
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 691.593
c starts	: 211
c conflicts	: 319
c decisions	: 76220
c propagations	: 142111
c inspects	: 1009794
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 211
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 694.143
c starts	: 212
c conflicts	: 319
c decisions	: 76573
c propagations	: 142760
c inspects	: 1013964
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 212
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 696.667
c starts	: 213
c conflicts	: 319
c decisions	: 76926
c propagations	: 143409
c inspects	: 1018134
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 213
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 699.202
c starts	: 214
c conflicts	: 319
c decisions	: 77279
c propagations	: 144058
c inspects	: 1022304
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 214
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 701.716
c starts	: 215
c conflicts	: 319
c decisions	: 77632
c propagations	: 144707
c inspects	: 1026474
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 215
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 704.23
c starts	: 216
c conflicts	: 319
c decisions	: 77985
c propagations	: 145356
c inspects	: 1030644
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 216
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 706.74
c starts	: 217
c conflicts	: 319
c decisions	: 78338
c propagations	: 146005
c inspects	: 1034814
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 217
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 709.273
c starts	: 218
c conflicts	: 319
c decisions	: 78691
c propagations	: 146654
c inspects	: 1038984
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 218
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 711.813
c starts	: 219
c conflicts	: 319
c decisions	: 79044
c propagations	: 147303
c inspects	: 1043154
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 219
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 714.334
c starts	: 220
c conflicts	: 319
c decisions	: 79397
c propagations	: 147952
c inspects	: 1047324
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 220
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 716.863
c starts	: 221
c conflicts	: 319
c decisions	: 79750
c propagations	: 148601
c inspects	: 1051494
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 221
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 719.39
c starts	: 222
c conflicts	: 319
c decisions	: 80103
c propagations	: 149250
c inspects	: 1055664
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 222
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 721.902
c starts	: 223
c conflicts	: 319
c decisions	: 80456
c propagations	: 149899
c inspects	: 1059834
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 223
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 724.428
c starts	: 224
c conflicts	: 319
c decisions	: 80809
c propagations	: 150548
c inspects	: 1064004
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 224
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 726.951
c starts	: 225
c conflicts	: 319
c decisions	: 81162
c propagations	: 151197
c inspects	: 1068174
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 225
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 729.512
c starts	: 226
c conflicts	: 319
c decisions	: 81515
c propagations	: 151846
c inspects	: 1072344
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 226
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 732.043
c starts	: 227
c conflicts	: 319
c decisions	: 81868
c propagations	: 152495
c inspects	: 1076514
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 227
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 734.574
c starts	: 228
c conflicts	: 319
c decisions	: 82221
c propagations	: 153144
c inspects	: 1080684
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 228
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 737.107
c starts	: 229
c conflicts	: 319
c decisions	: 82574
c propagations	: 153793
c inspects	: 1084854
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 229
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 739.65
c starts	: 230
c conflicts	: 319
c decisions	: 82927
c propagations	: 154442
c inspects	: 1089024
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 230
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 742.174
c starts	: 231
c conflicts	: 319
c decisions	: 83280
c propagations	: 155091
c inspects	: 1093194
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 231
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 744.715
c starts	: 232
c conflicts	: 319
c decisions	: 83633
c propagations	: 155740
c inspects	: 1097364
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 232
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 747.239
c starts	: 233
c conflicts	: 319
c decisions	: 83986
c propagations	: 156389
c inspects	: 1101534
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 233
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 749.764
c starts	: 234
c conflicts	: 319
c decisions	: 84339
c propagations	: 157038
c inspects	: 1105704
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 234
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 752.316
c starts	: 235
c conflicts	: 319
c decisions	: 84692
c propagations	: 157687
c inspects	: 1109874
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 235
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 754.858
c starts	: 236
c conflicts	: 319
c decisions	: 85045
c propagations	: 158336
c inspects	: 1114044
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 236
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 757.368
c starts	: 237
c conflicts	: 319
c decisions	: 85398
c propagations	: 158985
c inspects	: 1118214
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 237
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 759.895
c starts	: 238
c conflicts	: 319
c decisions	: 85751
c propagations	: 159634
c inspects	: 1122384
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 238
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 762.425
c starts	: 239
c conflicts	: 319
c decisions	: 86104
c propagations	: 160283
c inspects	: 1126554
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 239
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 764.94
c starts	: 240
c conflicts	: 319
c decisions	: 86457
c propagations	: 160932
c inspects	: 1130724
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 240
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 767.458
c starts	: 241
c conflicts	: 319
c decisions	: 86810
c propagations	: 161581
c inspects	: 1134894
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 241
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 769.996
c starts	: 242
c conflicts	: 319
c decisions	: 87163
c propagations	: 162230
c inspects	: 1139064
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 242
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 772.505
c starts	: 243
c conflicts	: 319
c decisions	: 87516
c propagations	: 162879
c inspects	: 1143234
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 243
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 775.002
c starts	: 244
c conflicts	: 319
c decisions	: 87869
c propagations	: 163528
c inspects	: 1147404
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 244
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 777.546
c starts	: 245
c conflicts	: 319
c decisions	: 88222
c propagations	: 164177
c inspects	: 1151574
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 245
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 780.064
c starts	: 246
c conflicts	: 319
c decisions	: 88575
c propagations	: 164826
c inspects	: 1155744
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 246
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 782.577
c starts	: 247
c conflicts	: 319
c decisions	: 88928
c propagations	: 165475
c inspects	: 1159914
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 247
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 785.098
c starts	: 248
c conflicts	: 319
c decisions	: 89281
c propagations	: 166124
c inspects	: 1164084
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 248
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 787.625
c starts	: 249
c conflicts	: 319
c decisions	: 89634
c propagations	: 166773
c inspects	: 1168254
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 249
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 790.134
c starts	: 250
c conflicts	: 319
c decisions	: 89987
c propagations	: 167422
c inspects	: 1172424
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 250
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 792.637
c starts	: 251
c conflicts	: 319
c decisions	: 90340
c propagations	: 168071
c inspects	: 1176594
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 251
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 795.15
c starts	: 252
c conflicts	: 319
c decisions	: 90693
c propagations	: 168720
c inspects	: 1180764
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 252
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 797.66
c starts	: 253
c conflicts	: 319
c decisions	: 91046
c propagations	: 169369
c inspects	: 1184934
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 253
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 800.179
c starts	: 254
c conflicts	: 319
c decisions	: 91399
c propagations	: 170018
c inspects	: 1189104
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 254
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 802.706
c starts	: 255
c conflicts	: 319
c decisions	: 91752
c propagations	: 170667
c inspects	: 1193274
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 255
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 805.225
c starts	: 256
c conflicts	: 319
c decisions	: 92105
c propagations	: 171316
c inspects	: 1197444
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 256
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 807.75
c starts	: 257
c conflicts	: 319
c decisions	: 92458
c propagations	: 171965
c inspects	: 1201614
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 257
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 810.265
c starts	: 258
c conflicts	: 319
c decisions	: 92811
c propagations	: 172614
c inspects	: 1205784
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 258
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 812.789
c starts	: 259
c conflicts	: 319
c decisions	: 93164
c propagations	: 173263
c inspects	: 1209954
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 259
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 815.325
c starts	: 260
c conflicts	: 319
c decisions	: 93517
c propagations	: 173912
c inspects	: 1214124
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 260
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 817.837
c starts	: 261
c conflicts	: 319
c decisions	: 93870
c propagations	: 174561
c inspects	: 1218294
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 261
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 820.361
c starts	: 262
c conflicts	: 319
c decisions	: 94223
c propagations	: 175210
c inspects	: 1222464
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 262
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 822.88
c starts	: 263
c conflicts	: 319
c decisions	: 94576
c propagations	: 175859
c inspects	: 1226634
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 263
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 825.409
c starts	: 264
c conflicts	: 319
c decisions	: 94929
c propagations	: 176508
c inspects	: 1230804
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 264
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 827.951
c starts	: 265
c conflicts	: 319
c decisions	: 95282
c propagations	: 177157
c inspects	: 1234974
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 265
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 830.478
c starts	: 266
c conflicts	: 319
c decisions	: 95635
c propagations	: 177806
c inspects	: 1239144
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 266
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 832.987
c starts	: 267
c conflicts	: 319
c decisions	: 95988
c propagations	: 178455
c inspects	: 1243314
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 267
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 835.52
c starts	: 268
c conflicts	: 319
c decisions	: 96341
c propagations	: 179104
c inspects	: 1247484
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 268
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 838.061
c starts	: 269
c conflicts	: 319
c decisions	: 96694
c propagations	: 179753
c inspects	: 1251654
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 269
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 840.573
c starts	: 270
c conflicts	: 319
c decisions	: 97047
c propagations	: 180402
c inspects	: 1255824
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 270
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 843.088
c starts	: 271
c conflicts	: 319
c decisions	: 97400
c propagations	: 181051
c inspects	: 1259994
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 271
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 845.602
c starts	: 272
c conflicts	: 319
c decisions	: 97753
c propagations	: 181700
c inspects	: 1264164
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 272
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 848.103
c starts	: 273
c conflicts	: 319
c decisions	: 98106
c propagations	: 182349
c inspects	: 1268334
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 273
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 850.619
c starts	: 274
c conflicts	: 319
c decisions	: 98459
c propagations	: 182998
c inspects	: 1272504
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 274
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 853.136
c starts	: 275
c conflicts	: 319
c decisions	: 98812
c propagations	: 183647
c inspects	: 1276674
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 275
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 855.652
c starts	: 276
c conflicts	: 319
c decisions	: 99165
c propagations	: 184296
c inspects	: 1280844
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 276
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 858.17
c starts	: 277
c conflicts	: 319
c decisions	: 99518
c propagations	: 184945
c inspects	: 1285014
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 277
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 860.68
c starts	: 278
c conflicts	: 319
c decisions	: 99871
c propagations	: 185594
c inspects	: 1289184
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 278
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 863.216
c starts	: 279
c conflicts	: 319
c decisions	: 100224
c propagations	: 186243
c inspects	: 1293354
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 279
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 865.738
c starts	: 280
c conflicts	: 319
c decisions	: 100577
c propagations	: 186892
c inspects	: 1297524
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 280
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 868.253
c starts	: 281
c conflicts	: 319
c decisions	: 100930
c propagations	: 187541
c inspects	: 1301694
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 281
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 870.779
c starts	: 282
c conflicts	: 319
c decisions	: 101283
c propagations	: 188190
c inspects	: 1305864
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 282
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 873.29
c starts	: 283
c conflicts	: 319
c decisions	: 101636
c propagations	: 188839
c inspects	: 1310034
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 283
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 875.81
c starts	: 284
c conflicts	: 319
c decisions	: 101989
c propagations	: 189488
c inspects	: 1314204
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 284
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 878.314
c starts	: 285
c conflicts	: 319
c decisions	: 102342
c propagations	: 190137
c inspects	: 1318374
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 285
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 880.828
c starts	: 286
c conflicts	: 319
c decisions	: 102695
c propagations	: 190786
c inspects	: 1322544
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 286
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 883.341
c starts	: 287
c conflicts	: 319
c decisions	: 103048
c propagations	: 191435
c inspects	: 1326714
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 287
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 885.864
c starts	: 288
c conflicts	: 319
c decisions	: 103401
c propagations	: 192084
c inspects	: 1330884
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 288
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 888.377
c starts	: 289
c conflicts	: 319
c decisions	: 103754
c propagations	: 192733
c inspects	: 1335054
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 289
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 890.902
c starts	: 290
c conflicts	: 319
c decisions	: 104107
c propagations	: 193382
c inspects	: 1339224
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 290
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 893.422
c starts	: 291
c conflicts	: 319
c decisions	: 104460
c propagations	: 194031
c inspects	: 1343394
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 291
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 895.939
c starts	: 292
c conflicts	: 319
c decisions	: 104813
c propagations	: 194680
c inspects	: 1347564
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 292
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 898.475
c starts	: 293
c conflicts	: 319
c decisions	: 105166
c propagations	: 195329
c inspects	: 1351734
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 293
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 901.008
c starts	: 294
c conflicts	: 319
c decisions	: 105519
c propagations	: 195978
c inspects	: 1355904
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 294
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 903.533
c starts	: 295
c conflicts	: 319
c decisions	: 105872
c propagations	: 196627
c inspects	: 1360074
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 295
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 906.06
c starts	: 296
c conflicts	: 319
c decisions	: 106225
c propagations	: 197276
c inspects	: 1364244
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 296
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 908.594
c starts	: 297
c conflicts	: 319
c decisions	: 106578
c propagations	: 197925
c inspects	: 1368414
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 297
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 911.096
c starts	: 298
c conflicts	: 319
c decisions	: 106931
c propagations	: 198574
c inspects	: 1372584
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 298
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 913.619
c starts	: 299
c conflicts	: 319
c decisions	: 107284
c propagations	: 199223
c inspects	: 1376754
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 299
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 916.153
c starts	: 300
c conflicts	: 319
c decisions	: 107637
c propagations	: 199872
c inspects	: 1380924
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 300
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 918.688
c starts	: 301
c conflicts	: 319
c decisions	: 107990
c propagations	: 200521
c inspects	: 1385094
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 301
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 921.196
c starts	: 302
c conflicts	: 319
c decisions	: 108343
c propagations	: 201170
c inspects	: 1389264
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 302
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 923.725
c starts	: 303
c conflicts	: 319
c decisions	: 108696
c propagations	: 201819
c inspects	: 1393434
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 303
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 926.236
c starts	: 304
c conflicts	: 319
c decisions	: 109049
c propagations	: 202468
c inspects	: 1397604
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 304
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 928.741
c starts	: 305
c conflicts	: 319
c decisions	: 109402
c propagations	: 203117
c inspects	: 1401774
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 305
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 931.268
c starts	: 306
c conflicts	: 319
c decisions	: 109755
c propagations	: 203766
c inspects	: 1405944
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 306
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 933.771
c starts	: 307
c conflicts	: 319
c decisions	: 110108
c propagations	: 204415
c inspects	: 1410114
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 307
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 936.286
c starts	: 308
c conflicts	: 319
c decisions	: 110461
c propagations	: 205064
c inspects	: 1414284
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 308
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 938.816
c starts	: 309
c conflicts	: 319
c decisions	: 110814
c propagations	: 205713
c inspects	: 1418454
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 309
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 941.319
c starts	: 310
c conflicts	: 319
c decisions	: 111167
c propagations	: 206362
c inspects	: 1422624
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 310
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 943.848
c starts	: 311
c conflicts	: 319
c decisions	: 111520
c propagations	: 207011
c inspects	: 1426794
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 311
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 946.375
c starts	: 312
c conflicts	: 319
c decisions	: 111873
c propagations	: 207660
c inspects	: 1430964
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 312
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 948.886
c starts	: 313
c conflicts	: 319
c decisions	: 112226
c propagations	: 208309
c inspects	: 1435134
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 313
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 951.423
c starts	: 314
c conflicts	: 319
c decisions	: 112579
c propagations	: 208958
c inspects	: 1439304
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 314
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 953.951
c starts	: 315
c conflicts	: 319
c decisions	: 112932
c propagations	: 209607
c inspects	: 1443474
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 315
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 956.496
c starts	: 316
c conflicts	: 319
c decisions	: 113285
c propagations	: 210256
c inspects	: 1447644
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 316
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 959.014
c starts	: 317
c conflicts	: 319
c decisions	: 113638
c propagations	: 210905
c inspects	: 1451814
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 317
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 961.535
c starts	: 318
c conflicts	: 319
c decisions	: 113991
c propagations	: 211554
c inspects	: 1455984
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 318
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 964.064
c starts	: 319
c conflicts	: 319
c decisions	: 114344
c propagations	: 212203
c inspects	: 1460154
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 319
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 966.594
c starts	: 320
c conflicts	: 319
c decisions	: 114697
c propagations	: 212852
c inspects	: 1464324
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 320
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 969.097
c starts	: 321
c conflicts	: 319
c decisions	: 115050
c propagations	: 213501
c inspects	: 1468494
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 321
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 971.621
c starts	: 322
c conflicts	: 319
c decisions	: 115403
c propagations	: 214150
c inspects	: 1472664
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 322
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 974.169
c starts	: 323
c conflicts	: 319
c decisions	: 115756
c propagations	: 214799
c inspects	: 1476834
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 323
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 976.666
c starts	: 324
c conflicts	: 319
c decisions	: 116109
c propagations	: 215448
c inspects	: 1481004
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 324
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 979.214
c starts	: 325
c conflicts	: 319
c decisions	: 116462
c propagations	: 216097
c inspects	: 1485174
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 325
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 981.776
c starts	: 326
c conflicts	: 319
c decisions	: 116815
c propagations	: 216746
c inspects	: 1489344
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 326
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 984.322
c starts	: 327
c conflicts	: 319
c decisions	: 117168
c propagations	: 217395
c inspects	: 1493514
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 327
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 986.87
c starts	: 328
c conflicts	: 319
c decisions	: 117521
c propagations	: 218044
c inspects	: 1497684
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 328
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 989.422
c starts	: 329
c conflicts	: 319
c decisions	: 117874
c propagations	: 218693
c inspects	: 1501854
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 329
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 991.972
c starts	: 330
c conflicts	: 319
c decisions	: 118227
c propagations	: 219342
c inspects	: 1506024
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 330
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 994.519
c starts	: 331
c conflicts	: 319
c decisions	: 118580
c propagations	: 219991
c inspects	: 1510194
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 331
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 997.062
c starts	: 332
c conflicts	: 319
c decisions	: 118933
c propagations	: 220640
c inspects	: 1514364
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 332
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 999.613
c starts	: 333
c conflicts	: 319
c decisions	: 119286
c propagations	: 221289
c inspects	: 1518534
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 333
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1002.154
c starts	: 334
c conflicts	: 319
c decisions	: 119639
c propagations	: 221938
c inspects	: 1522704
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 334
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1004.703
c starts	: 335
c conflicts	: 319
c decisions	: 119992
c propagations	: 222587
c inspects	: 1526874
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 335
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1007.232
c starts	: 336
c conflicts	: 319
c decisions	: 120345
c propagations	: 223236
c inspects	: 1531044
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 336
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1009.746
c starts	: 337
c conflicts	: 319
c decisions	: 120698
c propagations	: 223885
c inspects	: 1535214
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 337
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1012.26
c starts	: 338
c conflicts	: 319
c decisions	: 121051
c propagations	: 224534
c inspects	: 1539384
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 338
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1014.769
c starts	: 339
c conflicts	: 319
c decisions	: 121404
c propagations	: 225183
c inspects	: 1543554
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 339
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1017.295
c starts	: 340
c conflicts	: 319
c decisions	: 121757
c propagations	: 225832
c inspects	: 1547724
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 340
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1019.808
c starts	: 341
c conflicts	: 319
c decisions	: 122110
c propagations	: 226481
c inspects	: 1551894
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 341
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1022.328
c starts	: 342
c conflicts	: 319
c decisions	: 122463
c propagations	: 227130
c inspects	: 1556064
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 342
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1024.853
c starts	: 343
c conflicts	: 319
c decisions	: 122816
c propagations	: 227779
c inspects	: 1560234
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 343
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1027.384
c starts	: 344
c conflicts	: 319
c decisions	: 123169
c propagations	: 228428
c inspects	: 1564404
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 344
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1029.905
c starts	: 345
c conflicts	: 319
c decisions	: 123522
c propagations	: 229077
c inspects	: 1568574
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 345
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1032.417
c starts	: 346
c conflicts	: 319
c decisions	: 123875
c propagations	: 229726
c inspects	: 1572744
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 346
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1034.945
c starts	: 347
c conflicts	: 319
c decisions	: 124228
c propagations	: 230375
c inspects	: 1576914
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 347
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1037.475
c starts	: 348
c conflicts	: 319
c decisions	: 124581
c propagations	: 231024
c inspects	: 1581084
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 348
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1039.992
c starts	: 349
c conflicts	: 319
c decisions	: 124934
c propagations	: 231673
c inspects	: 1585254
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 349
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1042.516
c starts	: 350
c conflicts	: 319
c decisions	: 125287
c propagations	: 232322
c inspects	: 1589424
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 350
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1045.044
c starts	: 351
c conflicts	: 319
c decisions	: 125640
c propagations	: 232971
c inspects	: 1593594
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 351
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1047.576
c starts	: 352
c conflicts	: 319
c decisions	: 125993
c propagations	: 233620
c inspects	: 1597764
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 352
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1050.09
c starts	: 353
c conflicts	: 319
c decisions	: 126346
c propagations	: 234269
c inspects	: 1601934
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 353
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1052.613
c starts	: 354
c conflicts	: 319
c decisions	: 126699
c propagations	: 234918
c inspects	: 1606104
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 354
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1055.127
c starts	: 355
c conflicts	: 319
c decisions	: 127052
c propagations	: 235567
c inspects	: 1610274
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 355
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1057.641
c starts	: 356
c conflicts	: 319
c decisions	: 127405
c propagations	: 236216
c inspects	: 1614444
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 356
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1060.157
c starts	: 357
c conflicts	: 319
c decisions	: 127758
c propagations	: 236865
c inspects	: 1618614
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 357
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1062.666
c starts	: 358
c conflicts	: 319
c decisions	: 128111
c propagations	: 237514
c inspects	: 1622784
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 358
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1065.171
c starts	: 359
c conflicts	: 319
c decisions	: 128464
c propagations	: 238163
c inspects	: 1626954
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 359
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1067.694
c starts	: 360
c conflicts	: 319
c decisions	: 128817
c propagations	: 238812
c inspects	: 1631124
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 360
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1070.221
c starts	: 361
c conflicts	: 319
c decisions	: 129170
c propagations	: 239461
c inspects	: 1635294
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 361
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1072.755
c starts	: 362
c conflicts	: 319
c decisions	: 129523
c propagations	: 240110
c inspects	: 1639464
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 362
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1075.274
c starts	: 363
c conflicts	: 319
c decisions	: 129876
c propagations	: 240759
c inspects	: 1643634
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 363
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1077.792
c starts	: 364
c conflicts	: 319
c decisions	: 130229
c propagations	: 241408
c inspects	: 1647804
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 364
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1080.315
c starts	: 365
c conflicts	: 319
c decisions	: 130582
c propagations	: 242057
c inspects	: 1651974
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 365
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1082.839
c starts	: 366
c conflicts	: 319
c decisions	: 130935
c propagations	: 242706
c inspects	: 1656144
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 366
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1085.353
c starts	: 367
c conflicts	: 319
c decisions	: 131288
c propagations	: 243355
c inspects	: 1660314
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 367
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1087.877
c starts	: 368
c conflicts	: 319
c decisions	: 131641
c propagations	: 244004
c inspects	: 1664484
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 368
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1090.41
c starts	: 369
c conflicts	: 319
c decisions	: 131994
c propagations	: 244653
c inspects	: 1668654
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 369
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1092.929
c starts	: 370
c conflicts	: 319
c decisions	: 132347
c propagations	: 245302
c inspects	: 1672824
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 370
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1095.467
c starts	: 371
c conflicts	: 319
c decisions	: 132700
c propagations	: 245951
c inspects	: 1676994
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 371
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1098.008
c starts	: 372
c conflicts	: 319
c decisions	: 133053
c propagations	: 246600
c inspects	: 1681164
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 372
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1100.531
c starts	: 373
c conflicts	: 319
c decisions	: 133406
c propagations	: 247249
c inspects	: 1685334
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 373
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1103.083
c starts	: 374
c conflicts	: 319
c decisions	: 133759
c propagations	: 247898
c inspects	: 1689504
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 374
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1105.614
c starts	: 375
c conflicts	: 319
c decisions	: 134112
c propagations	: 248547
c inspects	: 1693674
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 375
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1108.162
c starts	: 376
c conflicts	: 319
c decisions	: 134465
c propagations	: 249196
c inspects	: 1697844
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 376
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1110.703
c starts	: 377
c conflicts	: 319
c decisions	: 134818
c propagations	: 249845
c inspects	: 1702014
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 377
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1113.247
c starts	: 378
c conflicts	: 319
c decisions	: 135171
c propagations	: 250494
c inspects	: 1706184
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 378
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1115.782
c starts	: 379
c conflicts	: 319
c decisions	: 135524
c propagations	: 251143
c inspects	: 1710354
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 379
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1118.325
c starts	: 380
c conflicts	: 319
c decisions	: 135877
c propagations	: 251792
c inspects	: 1714524
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 380
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1120.842
c starts	: 381
c conflicts	: 319
c decisions	: 136230
c propagations	: 252441
c inspects	: 1718694
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 381
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1123.383
c starts	: 382
c conflicts	: 319
c decisions	: 136583
c propagations	: 253090
c inspects	: 1722864
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 382
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1125.921
c starts	: 383
c conflicts	: 319
c decisions	: 136936
c propagations	: 253739
c inspects	: 1727034
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 383
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1128.476
c starts	: 384
c conflicts	: 319
c decisions	: 137289
c propagations	: 254388
c inspects	: 1731204
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 384
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1131.013
c starts	: 385
c conflicts	: 319
c decisions	: 137642
c propagations	: 255037
c inspects	: 1735374
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 385
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1133.55
c starts	: 386
c conflicts	: 319
c decisions	: 137995
c propagations	: 255686
c inspects	: 1739544
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 386
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1136.1
c starts	: 387
c conflicts	: 319
c decisions	: 138348
c propagations	: 256335
c inspects	: 1743714
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 387
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1138.654
c starts	: 388
c conflicts	: 319
c decisions	: 138701
c propagations	: 256984
c inspects	: 1747884
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 388
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1141.198
c starts	: 389
c conflicts	: 319
c decisions	: 139054
c propagations	: 257633
c inspects	: 1752054
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 389
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1143.742
c starts	: 390
c conflicts	: 319
c decisions	: 139407
c propagations	: 258282
c inspects	: 1756224
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 390
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1146.294
c starts	: 391
c conflicts	: 319
c decisions	: 139760
c propagations	: 258931
c inspects	: 1760394
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 391
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1148.845
c starts	: 392
c conflicts	: 319
c decisions	: 140113
c propagations	: 259580
c inspects	: 1764564
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 392
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1151.405
c starts	: 393
c conflicts	: 319
c decisions	: 140466
c propagations	: 260229
c inspects	: 1768734
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 393
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1153.957
c starts	: 394
c conflicts	: 319
c decisions	: 140819
c propagations	: 260878
c inspects	: 1772904
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 394
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1156.504
c starts	: 395
c conflicts	: 319
c decisions	: 141172
c propagations	: 261527
c inspects	: 1777074
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 395
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1159.056
c starts	: 396
c conflicts	: 319
c decisions	: 141525
c propagations	: 262176
c inspects	: 1781244
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 396
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1161.594
c starts	: 397
c conflicts	: 319
c decisions	: 141878
c propagations	: 262825
c inspects	: 1785414
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 397
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1164.156
c starts	: 398
c conflicts	: 319
c decisions	: 142231
c propagations	: 263474
c inspects	: 1789584
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 398
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1166.692
c starts	: 399
c conflicts	: 319
c decisions	: 142584
c propagations	: 264123
c inspects	: 1793754
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 399
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1169.233
c starts	: 400
c conflicts	: 319
c decisions	: 142937
c propagations	: 264772
c inspects	: 1797924
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 400
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1171.781
c starts	: 401
c conflicts	: 319
c decisions	: 143290
c propagations	: 265421
c inspects	: 1802094
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 401
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1174.34
c starts	: 402
c conflicts	: 319
c decisions	: 143643
c propagations	: 266070
c inspects	: 1806264
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 402
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1176.876
c starts	: 403
c conflicts	: 319
c decisions	: 143996
c propagations	: 266719
c inspects	: 1810434
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 403
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1179.429
c starts	: 404
c conflicts	: 319
c decisions	: 144349
c propagations	: 267368
c inspects	: 1814604
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 404
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1181.969
c starts	: 405
c conflicts	: 319
c decisions	: 144702
c propagations	: 268017
c inspects	: 1818774
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 405
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1184.513
c starts	: 406
c conflicts	: 319
c decisions	: 145055
c propagations	: 268666
c inspects	: 1822944
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 406
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1187.065
c starts	: 407
c conflicts	: 319
c decisions	: 145408
c propagations	: 269315
c inspects	: 1827114
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 407
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1189.617
c starts	: 408
c conflicts	: 319
c decisions	: 145761
c propagations	: 269964
c inspects	: 1831284
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 408
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1192.156
c starts	: 409
c conflicts	: 319
c decisions	: 146114
c propagations	: 270613
c inspects	: 1835454
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 409
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1194.708
c starts	: 410
c conflicts	: 319
c decisions	: 146467
c propagations	: 271262
c inspects	: 1839624
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 410
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1197.266
c starts	: 411
c conflicts	: 319
c decisions	: 146820
c propagations	: 271911
c inspects	: 1843794
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 411
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1199.802
c starts	: 412
c conflicts	: 319
c decisions	: 147173
c propagations	: 272560
c inspects	: 1847964
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 412
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1202.349
c starts	: 413
c conflicts	: 319
c decisions	: 147526
c propagations	: 273209
c inspects	: 1852134
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 413
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1204.894
c starts	: 414
c conflicts	: 319
c decisions	: 147879
c propagations	: 273858
c inspects	: 1856304
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 414
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1207.432
c starts	: 415
c conflicts	: 319
c decisions	: 148232
c propagations	: 274507
c inspects	: 1860474
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 415
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1209.979
c starts	: 416
c conflicts	: 319
c decisions	: 148585
c propagations	: 275156
c inspects	: 1864644
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 416
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1212.515
c starts	: 417
c conflicts	: 319
c decisions	: 148938
c propagations	: 275805
c inspects	: 1868814
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 417
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1215.051
c starts	: 418
c conflicts	: 319
c decisions	: 149291
c propagations	: 276454
c inspects	: 1872984
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 418
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1217.598
c starts	: 419
c conflicts	: 319
c decisions	: 149644
c propagations	: 277103
c inspects	: 1877154
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 419
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1220.137
c starts	: 420
c conflicts	: 319
c decisions	: 149997
c propagations	: 277752
c inspects	: 1881324
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 420
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1222.686
c starts	: 421
c conflicts	: 319
c decisions	: 150350
c propagations	: 278401
c inspects	: 1885494
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 421
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1225.237
c starts	: 422
c conflicts	: 319
c decisions	: 150703
c propagations	: 279050
c inspects	: 1889664
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 422
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1227.788
c starts	: 423
c conflicts	: 319
c decisions	: 151056
c propagations	: 279699
c inspects	: 1893834
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 423
#### 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.77 0.91 0.90 2/54 21250
Raw data (stat): 21250 (runsolver) R 21249 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540461606 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 1.04 0.96 0.92 4/64 21260
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18076 0 1 0 499 42 0 0 25 0 11 0 540461606 861630464 20642 4294967295 134512640 134569956 3221224400 3221213396 1073952732 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210359 20642 13073 16 0 210343 0
vsize: 841436
[startup+20.0023 s]
Raw data (loadavg): 1.03 0.96 0.92 2/64 21261
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18077 4 1 0 1416 42 0 0 25 0 11 0 540461606 860119040 21451 4294967295 134512640 134569956 3221224400 3221214680 1131616418 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209990 21451 13073 16 0 209974 0
vsize: 839960
[startup+30.0025 s]
Raw data (loadavg): 1.02 0.97 0.92 2/64 21267
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18079 4 1 0 2346 43 0 0 25 0 11 0 540461606 860119040 21899 4294967295 134512640 134569956 3221224400 3221214488 1131289987 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209990 21899 13073 16 0 209974 0
vsize: 839960
[startup+40.0029 s]
Raw data (loadavg): 1.02 0.97 0.92 3/64 21269
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18079 4 1 0 3300 43 0 0 25 0 11 0 540461606 866025472 23441 4294967295 134512640 134569956 3221224400 3221214768 1131339952 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211432 23441 13073 16 0 211416 0
vsize: 845728
[startup+50.0031 s]
Raw data (loadavg): 1.02 0.97 0.92 2/64 21278
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 4273 44 0 0 25 0 11 0 540461606 865361920 23540 4294967295 134512640 134569956 3221224400 3221214672 1131243096 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211270 23540 13073 16 0 211254 0
vsize: 845080
[startup+60.0027 s]
Raw data (loadavg): 1.09 0.99 0.92 2/64 21286
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 5245 45 1 0 25 0 11 0 540461606 862216192 22724 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 22724 13073 16 0 210486 0
vsize: 842008
[startup+70.004 s]
Raw data (loadavg): 1.08 0.99 0.92 2/64 21294
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 6216 45 1 0 25 0 11 0 540461606 862216192 22810 4294967295 134512640 134569956 3221224400 3221214488 1131641904 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 22810 13073 16 0 210486 0
vsize: 842008
[startup+80.0046 s]
Raw data (loadavg): 1.07 0.99 0.92 2/64 21300
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 7177 46 1 0 25 0 11 0 540461606 862216192 22959 4294967295 134512640 134569956 3221224400 3221214624 1131403890 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 22959 13073 16 0 210486 0
vsize: 842008
[startup+90.0039 s]
Raw data (loadavg): 1.06 0.99 0.92 2/64 21303
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 8132 46 1 0 25 0 11 0 540461606 862216192 23198 4294967295 134512640 134569956 3221224400 3221214768 1131341224 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 23198 13073 16 0 210486 0
vsize: 842008
[startup+100.005 s]
Raw data (loadavg): 1.05 0.99 0.92 2/64 21305
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 9098 46 1 0 25 0 11 0 540461606 862216192 23348 4294967295 134512640 134569956 3221224400 3221214768 1131339759 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 23348 13073 16 0 210486 0
vsize: 842008
[startup+110.005 s]
Raw data (loadavg): 1.04 0.99 0.92 2/64 21307
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 10075 47 1 0 24 0 11 0 540461606 862216192 23570 4294967295 134512640 134569956 3221224400 3221214768 1131341967 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 23570 13073 16 0 210486 0
vsize: 842008
[startup+120.006 s]
Raw data (loadavg): 1.03 0.99 0.92 2/64 21309
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 11061 48 2 0 24 0 11 0 540461606 862216192 23657 4294967295 134512640 134569956 3221224400 3221214712 1085632281 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 23657 13073 16 0 210486 0
vsize: 842008
[startup+130.006 s]
Raw data (loadavg): 1.03 0.99 0.92 2/64 21311
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 12048 48 2 0 25 0 11 0 540461606 862216192 23694 4294967295 134512640 134569956 3221224400 3221214720 1131551888 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 23694 13073 16 0 210486 0
vsize: 842008
[startup+140.006 s]
Raw data (loadavg): 1.02 0.99 0.92 2/64 21313
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 13036 48 2 0 25 0 11 0 540461606 862216192 23729 4294967295 134512640 134569956 3221224400 3221214672 1131242465 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 23729 13073 16 0 210486 0
vsize: 842008
[startup+150.007 s]
Raw data (loadavg): 1.02 0.99 0.92 2/64 21315
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 14024 48 2 1 25 0 11 0 540461606 862216192 23794 4294967295 134512640 134569956 3221224400 3221214768 1131339959 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 23794 13073 16 0 210486 0
vsize: 842008
[startup+160.008 s]
Raw data (loadavg): 1.02 0.99 0.92 2/64 21317
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 15013 49 2 1 25 0 11 0 540461606 862216192 23832 4294967295 134512640 134569956 3221224400 3221214768 1131344198 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 23832 13073 16 0 210486 0
vsize: 842008
[startup+170.008 s]
Raw data (loadavg): 1.01 0.99 0.92 2/64 21319
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 16000 49 2 1 24 0 11 0 540461606 862216192 23873 4294967295 134512640 134569956 3221224400 3221214672 1131242281 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 23873 13073 16 0 210486 0
vsize: 842008
[startup+180.008 s]
Raw data (loadavg): 1.01 0.99 0.92 2/64 21320
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 16989 49 2 1 25 0 11 0 540461606 862216192 23898 4294967295 134512640 134569956 3221224400 3221214928 1131224921 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 23898 13073 16 0 210486 0
vsize: 842008
[startup+190.008 s]
Raw data (loadavg): 1.01 0.99 0.92 2/64 21322
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 17976 49 2 1 25 0 11 0 540461606 862216192 23931 4294967295 134512640 134569956 3221224400 3221214768 1131344127 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 23931 13073 16 0 210486 0
vsize: 842008
[startup+200.009 s]
Raw data (loadavg): 1.01 0.99 0.92 2/64 21323
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 18965 49 2 1 25 0 11 0 540461606 862216192 24033 4294967295 134512640 134569956 3221224400 3221214672 1131242330 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 24033 13073 16 0 210486 0
vsize: 842008
[startup+210.009 s]
Raw data (loadavg): 1.00 0.99 0.92 2/64 21324
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 19954 49 2 1 25 0 11 0 540461606 862216192 24059 4294967295 134512640 134569956 3221224400 3221214520 1131638968 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 24059 13073 16 0 210486 0
vsize: 842008
[startup+220.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/64 21325
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 20943 49 2 1 24 0 11 0 540461606 862216192 24091 4294967295 134512640 134569956 3221224400 3221214672 1131242262 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 24091 13073 16 0 210486 0
vsize: 842008
[startup+230.011 s]
Raw data (loadavg): 1.08 1.00 0.93 2/64 21328
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 21929 50 2 1 25 0 11 0 540461606 862216192 24112 4294967295 134512640 134569956 3221224400 3221214912 1131650574 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24112 13073 16 0 210486 0
vsize: 842008
[startup+240.01 s]
Raw data (loadavg): 1.07 1.00 0.93 2/64 21331
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 22912 50 3 1 25 0 11 0 540461606 862216192 24142 4294967295 134512640 134569956 3221224400 3221214768 1131344174 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 24142 13073 16 0 210486 0
vsize: 842008
[startup+250.012 s]
Raw data (loadavg): 1.06 1.00 0.93 2/64 21334
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 23894 51 3 1 25 0 11 0 540461606 862216192 24182 4294967295 134512640 134569956 3221224400 3221214672 1131243096 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 24182 13073 16 0 210486 0
vsize: 842008
[startup+260.012 s]
Raw data (loadavg): 1.05 1.00 0.93 2/64 21337
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 24878 51 3 1 25 0 11 0 540461606 862216192 24269 4294967295 134512640 134569956 3221224400 3221214568 1131404028 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24269 13073 16 0 210486 0
vsize: 842008
[startup+270.013 s]
Raw data (loadavg): 1.04 1.00 0.93 2/64 21340
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 25866 52 3 1 25 0 11 0 540461606 862216192 24311 4294967295 134512640 134569956 3221224400 3221214672 1131241991 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24311 13073 16 0 210486 0
vsize: 842008
[startup+280.014 s]
Raw data (loadavg): 1.03 1.00 0.93 2/64 21343
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 26853 53 3 2 25 0 11 0 540461606 862216192 24367 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24367 13073 16 0 210486 0
vsize: 842008
[startup+290.014 s]
Raw data (loadavg): 1.03 1.00 0.93 2/64 21346
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 27841 53 3 2 25 0 11 0 540461606 862216192 24413 4294967295 134512640 134569956 3221224400 3221214672 1131241857 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24413 13073 16 0 210486 0
vsize: 842008
[startup+300.015 s]
Raw data (loadavg): 1.02 1.00 0.93 2/64 21349
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 28830 53 3 2 25 0 11 0 540461606 862216192 24463 4294967295 134512640 134569956 3221224400 3221214672 1131242189 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24463 13073 16 0 210486 0
vsize: 842008
[startup+310.016 s]
Raw data (loadavg): 1.02 1.00 0.93 2/64 21352
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 29818 53 3 2 25 0 11 0 540461606 862216192 24509 4294967295 134512640 134569956 3221224400 3221214764 1131241836 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24509 13073 16 0 210486 0
vsize: 842008
[startup+320.017 s]
Raw data (loadavg): 1.02 1.00 0.93 2/64 21355
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 30807 54 3 2 25 0 11 0 540461606 862216192 24558 4294967295 134512640 134569956 3221224400 3221214792 1131403986 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24558 13073 16 0 210486 0
vsize: 842008
[startup+330.017 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 21358
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 31795 54 4 2 25 0 11 0 540461606 862216192 24593 4294967295 134512640 134569956 3221224400 3221214744 1131638897 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24593 13073 16 0 210486 0
vsize: 842008
[startup+340.018 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 21361
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 32783 55 4 2 25 0 11 0 540461606 862216192 24650 4294967295 134512640 134569956 3221224400 3221214672 1131241853 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24650 13073 16 0 210486 0
vsize: 842008
[startup+350.018 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 21364
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 33770 55 4 2 25 0 11 0 540461606 862216192 24693 4294967295 134512640 134569956 3221224400 3221214672 1131242300 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24693 13073 16 0 210486 0
vsize: 842008
[startup+360.018 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 21367
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 34757 56 4 2 25 0 11 0 540461606 862216192 24744 4294967295 134512640 134569956 3221224400 3221214404 1085679260 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24744 13073 16 0 210486 0
vsize: 842008
[startup+370.019 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 21370
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 35744 56 4 2 25 0 11 0 540461606 862216192 24809 4294967295 134512640 134569956 3221224400 3221214688 1131638924 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24809 13073 16 0 210486 0
vsize: 842008
[startup+380.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21373
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 36730 57 4 2 25 0 11 0 540461606 862216192 24885 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24885 13073 16 0 210486 0
vsize: 842008
[startup+390.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21376
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 37717 57 4 2 25 0 11 0 540461606 862216192 24945 4294967295 134512640 134569956 3221224400 3221214672 1131241868 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 24945 13073 16 0 210486 0
vsize: 842008
[startup+400.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21379
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 38705 58 4 2 25 0 11 0 540461606 862216192 25015 4294967295 134512640 134569956 3221224400 3221214672 1131242433 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25015 13073 16 0 210486 0
vsize: 842008
[startup+410.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21382
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 39693 58 5 2 25 0 11 0 540461606 862216192 25079 4294967295 134512640 134569956 3221224400 3221214672 1131243091 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25079 13073 16 0 210486 0
vsize: 842008
[startup+420.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21385
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 40682 59 5 3 25 0 11 0 540461606 862216192 25135 4294967295 134512640 134569956 3221224400 3221214768 1131339768 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25135 13073 16 0 210486 0
vsize: 842008
[startup+430.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21388
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 41670 59 5 3 25 0 11 0 540461606 862216192 25172 4294967295 134512640 134569956 3221224400 3221214484 1131639712 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25172 13073 16 0 210486 0
vsize: 842008
[startup+440.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21391
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 42657 60 5 3 25 0 11 0 540461606 862216192 25225 4294967295 134512640 134569956 3221224400 3221214628 1085632316 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 25225 13073 16 0 210486 0
vsize: 842008
[startup+450.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21394
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 43643 60 6 3 25 0 11 0 540461606 862216192 25268 4294967295 134512640 134569956 3221224400 3221214632 1131638940 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25268 13073 16 0 210486 0
vsize: 842008
[startup+460.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21397
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 44629 61 6 3 25 0 11 0 540461606 862216192 25326 4294967295 134512640 134569956 3221224400 3221214488 1085679287 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25326 13073 16 0 210486 0
vsize: 842008
[startup+470.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21400
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 45614 61 6 3 25 0 11 0 540461606 862216192 25382 4294967295 134512640 134569956 3221224400 3221214488 1131641924 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25382 13073 16 0 210486 0
vsize: 842008
[startup+480.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21403
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 46602 62 6 3 25 0 11 0 540461606 862216192 25515 4294967295 134512640 134569956 3221224400 3221214560 1131661845 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25515 13073 16 0 210486 0
vsize: 842008
[startup+490.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21406
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 47590 62 6 3 25 0 11 0 540461606 862216192 25568 4294967295 134512640 134569956 3221224400 3221214564 1131404004 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25568 13073 16 0 210486 0
vsize: 842008
[startup+500.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21409
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 48577 63 6 3 25 0 11 0 540461606 862216192 25609 4294967295 134512640 134569956 3221224400 3221214488 1131641590 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25609 13073 16 0 210486 0
vsize: 842008
[startup+510.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21412
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 49565 63 7 3 25 0 11 0 540461606 862216192 25673 4294967295 134512640 134569956 3221224400 3221214436 1131638992 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25673 13073 16 0 210486 0
vsize: 842008
[startup+520.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21415
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 50554 64 7 3 25 0 11 0 540461606 862216192 25719 4294967295 134512640 134569956 3221224400 3221214488 1131642016 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25719 13073 16 0 210486 0
vsize: 842008
[startup+530.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21418
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 51543 64 7 3 25 0 11 0 540461606 862216192 25787 4294967295 134512640 134569956 3221224400 3221214600 1085679284 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25787 13073 16 0 210486 0
vsize: 842008
[startup+540.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21421
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 52533 64 7 3 25 0 11 0 540461606 862216192 25837 4294967295 134512640 134569956 3221224400 3221214560 1131639701 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25837 13073 16 0 210486 0
vsize: 842008
[startup+550.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21424
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 53522 65 8 3 25 0 11 0 540461606 862216192 25869 4294967295 134512640 134569956 3221224400 3221214736 1131404048 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25869 13073 16 0 210486 0
vsize: 842008
[startup+560.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21427
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 54511 66 8 3 25 0 11 0 540461606 862216192 25899 4294967295 134512640 134569956 3221224400 3221214744 1131639050 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25899 13073 16 0 210486 0
vsize: 842008
[startup+570.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21430
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 55501 66 8 3 25 0 11 0 540461606 862216192 25947 4294967295 134512640 134569956 3221224400 3221214792 1131404007 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25947 13073 16 0 210486 0
vsize: 842008
[startup+580.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21433
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 56491 66 8 3 25 0 11 0 540461606 862216192 25977 4294967295 134512640 134569956 3221224400 3221214352 1085679313 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 25977 13073 16 0 210486 0
vsize: 842008
[startup+590.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21436
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 57480 67 8 3 25 0 11 0 540461606 862216192 26015 4294967295 134512640 134569956 3221224400 3221214440 1131639067 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26015 13073 16 0 210486 0
vsize: 842008
[startup+600.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21439
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 58469 67 9 4 25 0 11 0 540461606 862216192 26045 4294967295 134512640 134569956 3221224400 3221214564 1131639078 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26045 13073 16 0 210486 0
vsize: 842008
[startup+610.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21442
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 59459 69 9 4 25 0 11 0 540461606 862216192 26095 4294967295 134512640 134569956 3221224400 3221214832 1131634508 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26095 13073 16 0 210486 0
vsize: 842008
[startup+620.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21445
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 60449 69 9 4 25 0 11 0 540461606 862216192 26127 4294967295 134512640 134569956 3221224400 3221214436 1131638987 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26127 13073 16 0 210486 0
vsize: 842008
[startup+630.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21448
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 61438 69 9 4 25 0 11 0 540461606 862216192 26155 4294967295 134512640 134569956 3221224400 3221214488 1131642023 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26155 13073 16 0 210486 0
vsize: 842008
[startup+640.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21451
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 62427 69 9 4 25 0 11 0 540461606 862216192 26184 4294967295 134512640 134569956 3221224400 3221214808 1131318874 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26184 13073 16 0 210486 0
vsize: 842008
[startup+650.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21453
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 63414 70 9 4 25 0 11 0 540461606 862216192 26227 4294967295 134512640 134569956 3221224400 3221214488 1131641731 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26227 13073 16 0 210486 0
vsize: 842008
[startup+660.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21456
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 64396 70 10 4 25 0 11 0 540461606 862216192 26256 4294967295 134512640 134569956 3221224400 3221214768 1131341839 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26256 13073 16 0 210486 0
vsize: 842008
[startup+670.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21460
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 65376 70 10 4 25 0 11 0 540461606 862216192 26348 4294967295 134512640 134569956 3221224400 3221214672 1131243071 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26348 13073 16 0 210486 0
vsize: 842008
[startup+680.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21464
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 66352 71 10 4 25 0 11 0 540461606 862216192 26462 4294967295 134512640 134569956 3221224400 3221214768 1131339959 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26462 13073 16 0 210486 0
vsize: 842008
[startup+690.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21468
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 67333 71 10 4 25 0 11 0 540461606 862216192 26736 4294967295 134512640 134569956 3221224400 3221214672 1131241889 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26736 13073 16 0 210486 0
vsize: 842008
[startup+700.057 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21472
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 68316 71 10 4 25 0 11 0 540461606 862216192 26828 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26828 13073 16 0 210486 0
vsize: 842008
[startup+710.057 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21476
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 69298 72 11 4 25 0 11 0 540461606 862216192 26918 4294967295 134512640 134569956 3221224400 3221214672 1131242057 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 26918 13073 16 0 210486 0
vsize: 842008
[startup+720.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21480
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 70279 72 11 4 25 0 11 0 540461606 862216192 27011 4294967295 134512640 134569956 3221224400 3221214808 1131318864 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27011 13073 16 0 210486 0
vsize: 842008
[startup+730.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21483
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 71262 73 11 5 25 0 11 0 540461606 862216192 27074 4294967295 134512640 134569956 3221224400 3221214672 1131242449 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27074 13073 16 0 210486 0
vsize: 842008
[startup+740.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21487
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18081 4 1 0 72241 73 11 5 25 0 11 0 540461606 862216192 27189 4294967295 134512640 134569956 3221224400 3221214672 1131242740 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27189 13073 16 0 210486 0
vsize: 842008
[startup+750.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21491
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 73220 73 11 5 25 0 11 0 540461606 862216192 27281 4294967295 134512640 134569956 3221224400 3221214768 1131344228 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27281 13073 16 0 210486 0
vsize: 842008
[startup+760.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21495
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 74200 74 12 5 25 0 11 0 540461606 862216192 27433 4294967295 134512640 134569956 3221224400 3221214672 1131241861 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27433 13073 16 0 210486 0
vsize: 842008
[startup+770.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21499
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 75181 75 12 5 25 0 11 0 540461606 862216192 27525 4294967295 134512640 134569956 3221224400 3221214672 1131241889 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27525 13073 16 0 210486 0
vsize: 842008
[startup+780.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21503
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 76164 76 12 5 25 0 11 0 540461606 862216192 27627 4294967295 134512640 134569956 3221224400 3221214672 1131241865 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27627 13073 16 0 210486 0
vsize: 842008
[startup+790.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21507
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 77148 76 12 5 25 0 11 0 540461606 862216192 27718 4294967295 134512640 134569956 3221224400 3221214672 1131241853 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27718 13073 16 0 210486 0
vsize: 842008
[startup+800.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21511
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 78133 77 13 5 23 0 11 0 540461606 862216192 27798 4294967295 134512640 134569956 3221224400 3221214768 1131344153 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27798 13073 16 0 210486 0
vsize: 842008
[startup+810.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21515
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 79121 77 13 5 25 0 11 0 540461606 862216192 27843 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27843 13073 16 0 210486 0
vsize: 842008
[startup+820.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21519
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 80107 78 13 5 25 0 11 0 540461606 862216192 27880 4294967295 134512640 134569956 3221224400 3221214672 1131242231 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27880 13073 16 0 210486 0
vsize: 842008
[startup+830.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21523
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 81092 79 13 5 25 0 11 0 540461606 862216192 27910 4294967295 134512640 134569956 3221224400 3221214672 1131243038 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 27910 13073 16 0 210486 0
vsize: 842008
[startup+840.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21527
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 82077 79 13 5 25 0 11 0 540461606 862216192 28006 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28006 13073 16 0 210486 0
vsize: 842008
[startup+850.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21531
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 83065 80 13 6 25 0 11 0 540461606 862216192 28047 4294967295 134512640 134569956 3221224400 3221214672 1131241861 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28047 13073 16 0 210486 0
vsize: 842008
[startup+860.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21535
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 84052 81 14 6 25 0 11 0 540461606 862216192 28087 4294967295 134512640 134569956 3221224400 3221214672 1131243091 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28087 13073 16 0 210486 0
vsize: 842008
[startup+870.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21539
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 85038 82 14 6 25 0 11 0 540461606 862216192 28111 4294967295 134512640 134569956 3221224400 3221214672 1131241931 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28111 13073 16 0 210486 0
vsize: 842008
[startup+880.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21543
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 86024 83 14 6 25 0 11 0 540461606 862216192 28141 4294967295 134512640 134569956 3221224400 3221214768 1131340024 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28141 13073 16 0 210486 0
vsize: 842008
[startup+890.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21547
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 87010 84 14 6 24 0 11 0 540461606 862216192 28198 4294967295 134512640 134569956 3221224400 3221214768 1131341055 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28198 13073 16 0 210486 0
vsize: 842008
[startup+900.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21551
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 87998 84 14 6 25 0 11 0 540461606 862216192 28228 4294967295 134512640 134569956 3221224400 3221214672 1131241879 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28228 13073 16 0 210486 0
vsize: 842008
[startup+910.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21555
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 88984 85 14 6 25 0 11 0 540461606 862216192 28266 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 28266 13073 16 0 210486 0
vsize: 842008
[startup+920.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21559
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 89970 85 14 6 25 0 11 0 540461606 862216192 28321 4294967295 134512640 134569956 3221224400 3221214672 1131242469 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28321 13073 16 0 210486 0
vsize: 842008
[startup+930.078 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21563
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 90955 86 15 6 25 0 11 0 540461606 862216192 28369 4294967295 134512640 134569956 3221224400 3221214672 1131242461 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28369 13073 16 0 210486 0
vsize: 842008
[startup+940.079 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21567
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 91941 87 15 6 25 0 11 0 540461606 862216192 28410 4294967295 134512640 134569956 3221224400 3221214672 1131243021 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28410 13073 16 0 210486 0
vsize: 842008
[startup+950.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21571
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 92926 87 15 6 25 0 11 0 540461606 862216192 28465 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28465 13073 16 0 210486 0
vsize: 842008
[startup+960.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21575
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 93910 88 15 7 25 0 11 0 540461606 862216192 28519 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28519 13073 16 0 210486 0
vsize: 842008
[startup+970.081 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21579
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 94893 89 16 7 25 0 11 0 540461606 862216192 28575 4294967295 134512640 134569956 3221224400 3221214768 1131341108 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28575 13073 16 0 210486 0
vsize: 842008
[startup+980.085 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21583
Raw data (stat): 21250 (java) S 21249 28546 28545 0 -1 0 18082 4 1 0 95876 90 16 7 25 0 11 0 540461606 862216192 28671 4294967295 134512640 134569956 3221224400 3221213416 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28671 13073 16 0 210486 0
vsize: 842008
[startup+990.085 s]
Raw data (loadavg): 1.00 1.00 0.93 2/63 21586
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 96852 90 16 7 25 0 10 0 540461606 862216192 28733 4294967295 134512640 134569956 3221224400 3221214040 1131301725 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28733 13073 16 0 210486 0
vsize: 842008
[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21590
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 97827 90 16 7 25 0 11 0 540461606 862216192 28787 4294967295 134512640 134569956 3221224400 3221214672 1131241857 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 28787 13073 16 0 210486 0
vsize: 842008
[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21594
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 98806 90 17 7 25 0 11 0 540461606 862216192 29181 4294967295 134512640 134569956 3221224400 3221214672 1131241857 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29181 13073 16 0 210486 0
vsize: 842008
[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21598
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 99791 91 17 7 25 0 11 0 540461606 862216192 29234 4294967295 134512640 134569956 3221224400 3221214768 1131339624 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29234 13073 16 0 210486 0
vsize: 842008
[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21602
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 100775 92 17 7 25 0 11 0 540461606 862216192 29277 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29277 13073 16 0 210486 0
vsize: 842008
[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21606
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 101760 92 17 7 24 0 11 0 540461606 862216192 29338 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29338 13073 16 0 210486 0
vsize: 842008
[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21610
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 102747 92 17 7 25 0 11 0 540461606 862216192 29407 4294967295 134512640 134569956 3221224400 3221214768 1131339944 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29407 13073 16 0 210486 0
vsize: 842008
[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21614
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 103734 93 17 7 25 0 11 0 540461606 862216192 29449 4294967295 134512640 134569956 3221224400 3221214768 1131341843 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29449 13073 16 0 210486 0
vsize: 842008
[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21618
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 104721 93 18 7 25 0 11 0 540461606 862216192 29480 4294967295 134512640 134569956 3221224400 3221214768 1131339959 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29480 13073 16 0 210486 0
vsize: 842008
[startup+1080.1 s]
Raw data (loadavg): 1.07 1.02 0.93 2/64 21622
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 105706 95 18 7 25 0 11 0 540461606 862216192 29515 4294967295 134512640 134569956 3221224400 3221214764 1131622627 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29515 13073 16 0 210486 0
vsize: 842008
[startup+1090.1 s]
Raw data (loadavg): 1.06 1.02 0.93 2/64 21626
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 106690 95 18 7 25 0 11 0 540461606 862216192 29568 4294967295 134512640 134569956 3221224400 3221214768 1131341088 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29568 13073 16 0 210486 0
vsize: 842008
[startup+1100.1 s]
Raw data (loadavg): 1.05 1.01 0.93 2/64 21630
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 107672 96 18 8 25 0 11 0 540461606 862216192 29622 4294967295 134512640 134569956 3221224400 3221214672 1131241868 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29622 13073 16 0 210486 0
vsize: 842008
[startup+1110.1 s]
Raw data (loadavg): 1.04 1.01 0.93 2/64 21634
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 108651 97 18 8 24 0 11 0 540461606 862216192 29667 4294967295 134512640 134569956 3221224400 3221214768 1131344153 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 29667 13073 16 0 210486 0
vsize: 842008
[startup+1120.1 s]
Raw data (loadavg): 1.04 1.01 0.93 2/64 21638
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 109632 97 18 8 25 0 11 0 540461606 862216192 29797 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 29797 13073 16 0 210486 0
vsize: 842008
[startup+1130.1 s]
Raw data (loadavg): 1.03 1.01 0.93 2/64 21642
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 110609 98 18 8 25 0 11 0 540461606 862216192 29925 4294967295 134512640 134569956 3221224400 3221214672 1131242179 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210502 29925 13073 16 0 210486 0
vsize: 842008
[startup+1140.1 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 21646
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 111586 98 18 8 25 0 11 0 540461606 862216192 30055 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 30055 13073 16 0 210486 0
vsize: 842008
[startup+1150.11 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 21650
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 112560 99 19 8 25 0 11 0 540461606 862216192 30203 4294967295 134512640 134569956 3221224400 3221214768 1131339959 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 30203 13073 16 0 210486 0
vsize: 842008
[startup+1160.11 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 21654
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 113534 99 19 8 24 0 11 0 540461606 862216192 30358 4294967295 134512640 134569956 3221224400 3221214672 1131242277 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 30358 13073 16 0 210486 0
vsize: 842008
[startup+1170.11 s]
Raw data (loadavg): 1.01 1.01 0.93 2/64 21658
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 114512 100 19 8 25 0 11 0 540461606 862216192 30466 4294967295 134512640 134569956 3221224400 3221214768 1131344198 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 30466 13073 16 0 210486 0
vsize: 842008
[startup+1180.11 s]
Raw data (loadavg): 1.01 1.01 0.93 2/64 21662
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 115489 101 19 8 25 0 11 0 540461606 862216192 30652 4294967295 134512640 134569956 3221224400 3221214808 1131318899 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 30652 13073 16 0 210486 0
vsize: 842008
[startup+1190.11 s]
Raw data (loadavg): 1.01 1.01 0.93 2/64 21665
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 116465 102 19 8 25 0 11 0 540461606 862216192 30770 4294967295 134512640 134569956 3221224400 3221214768 1131339952 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 30770 13073 16 0 210486 0
vsize: 842008
[startup+1200.11 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 21669
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 117442 102 20 8 25 0 11 0 540461606 862216192 30915 4294967295 134512640 134569956 3221224400 3221214672 1131241889 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 30915 13073 16 0 210486 0
vsize: 842008
[startup+1210.11 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 21673
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 118419 103 20 8 25 0 11 0 540461606 862216192 31083 4294967295 134512640 134569956 3221224400 3221214768 1131344077 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 31083 13073 16 0 210486 0
vsize: 842008
[startup+1220.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21677
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 119396 104 20 8 25 0 11 0 540461606 862216192 31234 4294967295 134512640 134569956 3221224400 3221214768 1131339952 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 31234 13073 16 0 210486 0
vsize: 842008
[startup+1230.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 21681
Raw data (stat): 21250 (java) R 21249 28546 28545 0 -1 0 18082 4 1 0 120374 104 20 9 25 0 11 0 540461606 862216192 31372 4294967295 134512640 134569956 3221224400 3221214768 1131340024 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210502 31372 13073 16 0 210486 0
vsize: 842008
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1230.22 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 21683
Raw data (stat): 21250 (java) Z 21249 28546 28545 0 -1 1036 18082 21711 1 1 120379 110 3788 73 25 0 1 0 540461606 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): 1230.22
CPU time (s): 1243.51
CPU user time (s): 1241.68
CPU system time (s): 1.83472
CPU usage (%): 101.08
Max. virtual memory (Kb): 845728
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####