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-glass4.opb
MD5SUM	7ca49051adbbebe6e2c6f68e4bc64c63
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	1253.9
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 14346

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        652080 kB
Buffers:         33944 kB
Cached:         317364 kB
SwapCached:        388 kB
Active:          90060 kB
Inactive:       263656 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        651828 kB
SwapTotal:     2097892 kB
SwapFree:      2096996 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6220 kB
Slab:            23260 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 00:00:00 (client local time) WITH STATUS 143 IN 1243.59 SECONDS
stats: 20133 7 1243.59 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-glass4.opb
c reading problem 
c [nbvar=653]
c [nbconstr=707]
c time 3.885
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) : 17.835
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.188
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) : 20.876
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) : 21.399
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.023
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) : 22.756
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) : 23.414
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) : 31.657
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) : 37.203
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) : 38.608
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) : 39.76
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) : 40.959
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) : 42.112
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) : 43.313
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) : 44.511
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) : 45.733
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) : 46.907
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) : 48.11
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) : 49.286
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) : 50.509
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) : 51.674
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) : 52.869
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) : 54.08
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) : 55.338
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) : 56.529
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) : 57.764
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) : 58.963
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) : 60.207
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) : 61.388
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) : 62.615
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) : 63.832
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) : 65.082
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) : 66.269
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) : 67.497
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) : 68.669
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) : 69.904
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) : 71.082
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) : 72.277
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) : 73.507
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) : 75.206
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) : 78.84
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) : 82.605
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) : 86.533
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) : 90.583
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) : 94.754
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) : 99.017
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) : 103.417
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) : 107.887
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) : 112.457
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) : 117.185
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) : 121.999
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) : 126.997
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) : 132.119
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) : 137.394
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) : 142.75
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) : 148.374
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) : 154.087
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) : 159.939
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) : 165.909
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) : 172.078
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) : 178.365
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) : 184.773
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) : 191.297
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) : 199.615
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) : 213.117
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) : 218.862
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) : 222.58
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) : 225.867
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) : 229.151
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) : 232.441
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) : 235.731
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) : 239.047
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) : 242.355
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) : 245.661
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) : 248.954
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) : 252.222
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) : 255.511
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) : 258.796
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) : 262.083
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) : 265.366
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) : 268.631
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) : 271.929
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) : 275.201
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) : 278.494
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) : 281.795
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) : 285.067
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) : 288.348
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) : 291.627
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) : 294.894
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) : 298.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) : 301.449
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) : 304.736
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) : 308.027
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) : 311.321
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) : 314.605
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) : 317.893
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) : 321.169
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) : 324.444
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) : 327.722
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) : 331.006
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) : 334.295
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) : 337.594
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) : 340.892
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) : 344.179
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) : 347.459
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) : 350.753
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) : 354.058
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) : 357.358
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) : 360.656
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) : 363.96
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) : 367.249
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) : 370.557
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) : 373.867
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) : 377.179
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) : 380.493
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) : 383.784
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) : 387.083
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) : 390.368
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) : 393.647
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) : 396.927
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) : 400.198
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) : 403.457
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) : 406.753
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) : 410.046
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) : 413.321
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) : 416.618
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) : 419.918
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) : 423.201
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) : 426.481
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) : 429.777
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) : 433.092
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) : 436.393
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) : 439.689
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) : 442.983
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) : 446.28
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) : 449.581
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) : 452.883
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) : 456.174
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) : 459.478
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) : 462.785
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) : 466.075
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) : 469.364
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) : 472.674
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) : 475.964
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) : 479.252
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) : 482.544
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) : 485.844
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) : 489.143
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) : 492.433
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) : 495.735
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) : 499.029
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) : 502.306
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) : 505.606
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) : 508.898
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) : 512.191
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) : 515.486
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) : 518.776
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) : 522.068
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) : 525.337
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) : 528.61
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) : 531.898
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) : 535.166
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) : 538.459
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) : 541.746
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) : 545.05
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) : 548.323
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) : 551.622
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) : 554.896
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) : 558.194
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) : 561.503
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) : 564.802
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) : 568.097
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) : 571.382
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) : 574.663
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) : 577.951
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) : 581.243
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) : 584.538
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) : 587.814
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) : 591.097
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) : 594.382
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) : 597.662
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) : 600.961
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) : 604.264
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) : 607.549
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) : 610.839
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) : 614.122
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) : 617.403
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) : 620.706
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) : 624.013
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) : 627.305
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) : 630.596
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) : 633.889
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) : 637.198
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) : 640.501
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) : 643.821
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) : 647.14
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) : 650.453
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) : 653.781
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) : 657.096
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) : 659.602
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) : 662.1
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) : 664.613
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) : 667.108
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) : 669.617
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) : 672.112
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) : 674.596
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) : 677.068
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) : 679.556
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) : 682.048
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) : 684.558
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) : 687.044
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) : 689.53
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) : 692.005
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) : 694.482
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) : 696.967
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) : 699.459
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) : 701.963
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) : 704.446
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) : 706.937
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) : 709.424
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) : 711.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) : 714.389
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) : 716.872
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) : 719.38
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) : 721.876
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) : 724.368
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) : 726.862
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) : 729.363
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) : 731.851
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) : 734.354
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) : 736.839
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) : 739.336
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) : 741.846
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) : 744.345
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) : 746.82
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) : 749.307
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) : 751.801
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) : 754.288
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) : 756.771
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) : 759.27
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) : 761.753
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) : 764.237
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) : 766.736
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) : 769.218
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) : 771.694
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) : 774.177
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) : 776.661
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) : 779.133
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) : 781.603
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) : 784.078
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) : 786.563
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) : 789.043
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) : 791.527
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) : 794.007
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) : 796.491
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) : 798.97
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) : 801.458
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) : 803.956
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) : 806.432
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) : 808.918
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) : 811.379
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) : 813.828
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) : 816.291
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) : 818.742
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) : 821.185
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) : 823.646
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) : 826.122
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) : 828.566
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) : 831.018
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) : 833.465
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) : 835.901
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) : 838.351
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) : 840.807
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) : 843.253
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) : 845.702
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) : 848.153
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) : 850.615
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) : 853.069
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) : 855.512
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) : 857.968
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) : 860.411
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) : 862.863
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) : 865.298
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) : 867.743
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) : 870.188
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) : 872.641
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) : 875.086
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) : 877.543
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) : 879.993
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) : 882.453
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) : 884.916
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) : 887.383
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) : 889.836
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) : 892.294
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) : 894.76
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) : 897.2
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) : 899.655
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) : 902.126
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) : 904.592
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) : 907.033
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) : 909.492
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) : 911.936
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) : 914.374
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) : 916.837
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) : 919.276
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) : 921.724
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) : 924.184
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) : 926.621
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) : 929.092
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) : 931.553
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) : 933.998
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) : 936.461
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) : 938.922
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) : 941.396
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) : 943.846
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) : 946.298
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) : 948.757
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) : 951.22
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) : 953.66
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) : 956.121
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) : 958.596
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) : 961.047
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) : 963.533
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) : 966.021
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) : 968.499
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) : 970.979
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) : 973.458
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) : 975.94
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) : 978.421
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) : 980.898
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) : 983.384
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) : 985.857
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) : 988.343
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) : 990.813
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) : 993.258
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) : 995.704
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) : 998.148
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) : 1000.605
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) : 1003.053
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) : 1005.506
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) : 1007.962
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) : 1010.424
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) : 1012.875
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) : 1015.321
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) : 1017.777
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) : 1020.236
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) : 1022.686
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) : 1025.14
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) : 1027.6
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) : 1030.062
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) : 1032.509
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) : 1034.963
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) : 1037.408
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) : 1039.855
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) : 1042.301
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) : 1044.743
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) : 1047.182
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) : 1049.638
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) : 1052.097
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) : 1054.561
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) : 1057.011
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) : 1059.461
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) : 1061.917
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) : 1064.371
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) : 1066.81
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) : 1069.261
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) : 1071.724
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) : 1074.177
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) : 1076.644
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) : 1079.115
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) : 1081.568
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) : 1084.046
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) : 1086.512
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) : 1088.987
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) : 1091.459
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) : 1093.932
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) : 1096.401
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) : 1098.875
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) : 1101.336
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) : 1103.806
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) : 1106.274
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) : 1108.765
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) : 1111.243
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) : 1113.713
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) : 1116.193
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) : 1118.676
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) : 1121.15
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) : 1123.625
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) : 1126.107
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) : 1128.592
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) : 1131.088
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) : 1133.57
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) : 1136.046
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) : 1138.528
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) : 1140.997
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) : 1143.485
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) : 1145.957
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) : 1148.428
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) : 1150.908
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) : 1153.394
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) : 1155.865
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) : 1158.346
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) : 1160.821
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) : 1163.298
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) : 1165.778
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) : 1168.262
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) : 1170.733
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) : 1173.216
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) : 1175.704
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) : 1178.172
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) : 1180.65
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) : 1183.127
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) : 1185.602
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) : 1188.085
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) : 1190.56
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) : 1193.034
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) : 1195.509
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) : 1197.978
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) : 1200.457
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) : 1202.937
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) : 1205.418
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
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1207.901
c starts	: 424
c conflicts	: 319
c decisions	: 151409
c propagations	: 280348
c inspects	: 1898004
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 424
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1210.374
c starts	: 425
c conflicts	: 319
c decisions	: 151762
c propagations	: 280997
c inspects	: 1902174
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 425
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1212.838
c starts	: 426
c conflicts	: 319
c decisions	: 152115
c propagations	: 281646
c inspects	: 1906344
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 426
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1215.312
c starts	: 427
c conflicts	: 319
c decisions	: 152468
c propagations	: 282295
c inspects	: 1910514
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 427
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1217.773
c starts	: 428
c conflicts	: 319
c decisions	: 152821
c propagations	: 282944
c inspects	: 1914684
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 428
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1220.236
c starts	: 429
c conflicts	: 319
c decisions	: 153174
c propagations	: 283593
c inspects	: 1918854
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 429
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1222.701
c starts	: 430
c conflicts	: 319
c decisions	: 153527
c propagations	: 284242
c inspects	: 1923024
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 430
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1225.166
c starts	: 431
c conflicts	: 319
c decisions	: 153880
c propagations	: 284891
c inspects	: 1927194
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 431
c 
c CURRENT OPTIMUM=1835776794
c Current CPU time (ms) : 1227.617
c starts	: 432
c conflicts	: 319
c decisions	: 154233
c propagations	: 285540
c inspects	: 1931364
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 319
c root simplifications	: 432
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.56 0.83 0.86 2/55 12666
Raw data (stat): 12666 (runsolver) R 12665 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540457875 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.0035 s]
Raw data (loadavg): 0.85 0.88 0.88 3/65 12676
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18080 0 1 0 517 40 0 0 25 0 11 0 540457875 860147712 20387 4294967295 134512640 134569956 3221224400 3221214840 1130917173 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209997 20387 13073 16 0 209981 0
vsize: 839988
[startup+20.0079 s]
Raw data (loadavg): 0.95 0.90 0.89 2/65 12678
Raw data (stat): 12666 (java) S 12665 20024 20023 0 -1 0 18081 3 1 0 1437 40 0 0 25 0 11 0 540457875 859844608 21252 4294967295 134512640 134569956 3221224400 3221213384 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209923 21252 13073 16 0 209907 0
vsize: 839692
[startup+30.0083 s]
Raw data (loadavg): 0.96 0.91 0.89 2/65 12683
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 2362 41 0 0 25 0 11 0 540457875 859844608 22164 4294967295 134512640 134569956 3221224400 3221214504 1131546052 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209923 22164 13073 16 0 209907 0
vsize: 839692
[startup+40.0093 s]
Raw data (loadavg): 0.96 0.91 0.89 2/65 12686
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 3328 42 0 0 25 0 11 0 540457875 865087488 23486 4294967295 134512640 134569956 3221224400 3221214584 1131181384 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211203 23486 13073 16 0 211187 0
vsize: 844812
[startup+50.0105 s]
Raw data (loadavg): 0.97 0.91 0.89 2/65 12695
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 4302 42 0 0 25 0 11 0 540457875 864038912 23205 4294967295 134512640 134569956 3221224400 3221214288 1131650742 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210947 23205 13073 16 0 210931 0
vsize: 843788
[startup+60.0101 s]
Raw data (loadavg): 0.97 0.91 0.89 2/65 12703
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 5275 43 1 0 25 0 11 0 540457875 862990336 22896 4294967295 134512640 134569956 3221224400 3221214408 1131644248 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 22896 13073 16 0 210675 0
vsize: 842764
[startup+70.018 s]
Raw data (loadavg): 0.98 0.92 0.89 2/65 12711
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 6242 44 1 0 25 0 11 0 540457875 862990336 23010 4294967295 134512640 134569956 3221224400 3221214672 1131243448 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 23010 13073 16 0 210675 0
vsize: 842764
[startup+80.0263 s]
Raw data (loadavg): 0.98 0.92 0.89 2/65 12719
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 7207 45 1 0 25 0 11 0 540457875 862990336 23155 4294967295 134512640 134569956 3221224400 3221214488 1131650864 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 23155 13073 16 0 210675 0
vsize: 842764
[startup+90.0273 s]
Raw data (loadavg): 0.98 0.92 0.89 2/65 12721
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 8162 45 1 0 25 0 11 0 540457875 862990336 23393 4294967295 134512640 134569956 3221224400 3221214768 1131345297 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 23393 13073 16 0 210675 0
vsize: 842764
[startup+100.028 s]
Raw data (loadavg): 0.98 0.92 0.90 2/65 12724
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 9133 46 2 0 25 0 11 0 540457875 862990336 23541 4294967295 134512640 134569956 3221224400 3221214720 1131644076 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 23541 13073 16 0 210675 0
vsize: 842764
[startup+110.028 s]
Raw data (loadavg): 0.99 0.92 0.90 2/65 12726
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 10114 46 2 0 25 0 11 0 540457875 862990336 23751 4294967295 134512640 134569956 3221224400 3221214672 1131243556 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 23751 13073 16 0 210675 0
vsize: 842764
[startup+120.029 s]
Raw data (loadavg): 0.99 0.93 0.90 2/65 12728
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 11100 46 2 0 25 0 11 0 540457875 862990336 23835 4294967295 134512640 134569956 3221224400 3221214672 1131244401 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 23835 13073 16 0 210675 0
vsize: 842764
[startup+130.03 s]
Raw data (loadavg): 0.99 0.93 0.90 2/65 12730
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 12088 47 2 0 25 0 11 0 540457875 862990336 23874 4294967295 134512640 134569956 3221224400 3221214672 1131243519 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 23874 13073 16 0 210675 0
vsize: 842764
[startup+140.03 s]
Raw data (loadavg): 0.99 0.93 0.90 2/65 12732
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 13075 48 2 0 24 0 11 0 540457875 862990336 23917 4294967295 134512640 134569956 3221224400 3221214672 1131243141 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 23917 13073 16 0 210675 0
vsize: 842764
[startup+150.032 s]
Raw data (loadavg): 0.99 0.93 0.90 2/65 12734
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 14064 48 2 1 25 0 11 0 540457875 862990336 23975 4294967295 134512640 134569956 3221224400 3221214440 1131648632 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 23975 13073 16 0 210675 0
vsize: 842764
[startup+160.032 s]
Raw data (loadavg): 0.99 0.93 0.90 2/65 12735
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 15053 49 2 1 25 0 11 0 540457875 862990336 24013 4294967295 134512640 134569956 3221224400 3221214672 1131243325 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24013 13073 16 0 210675 0
vsize: 842764
[startup+170.033 s]
Raw data (loadavg): 0.99 0.94 0.90 2/65 12737
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 16039 49 2 1 24 0 11 0 540457875 862990336 24053 4294967295 134512640 134569956 3221224400 3221214672 1131244355 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24053 13073 16 0 210675 0
vsize: 842764
[startup+180.034 s]
Raw data (loadavg): 0.99 0.94 0.90 2/65 12739
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 17027 49 2 1 25 0 11 0 540457875 862990336 24082 4294967295 134512640 134569956 3221224400 3221214672 1131243757 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24082 13073 16 0 210675 0
vsize: 842764
[startup+190.036 s]
Raw data (loadavg): 0.99 0.94 0.90 2/65 12740
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 18014 50 2 1 25 0 11 0 540457875 862990336 24143 4294967295 134512640 134569956 3221224400 3221214768 1131348267 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24143 13073 16 0 210675 0
vsize: 842764
[startup+200.036 s]
Raw data (loadavg): 0.99 0.94 0.91 2/65 12741
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 19004 50 2 1 25 0 11 0 540457875 862990336 24210 4294967295 134512640 134569956 3221224400 3221214672 1131244345 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24210 13073 16 0 210675 0
vsize: 842764
[startup+210.138 s]
Raw data (loadavg): 0.99 0.94 0.91 2/65 12742
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 20003 51 2 1 25 0 11 0 540457875 862990336 24243 4294967295 134512640 134569956 3221224400 3221214768 1131345186 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24243 13073 16 0 210675 0
vsize: 842764
[startup+220.139 s]
Raw data (loadavg): 0.99 0.94 0.91 2/65 12744
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 20992 51 2 1 25 0 11 0 540457875 862990336 24265 4294967295 134512640 134569956 3221224400 3221214672 1131243565 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24265 13073 16 0 210675 0
vsize: 842764
[startup+230.139 s]
Raw data (loadavg): 0.99 0.94 0.91 2/65 12747
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 21977 52 2 1 25 0 11 0 540457875 862990336 24288 4294967295 134512640 134569956 3221224400 3221214408 1085632310 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24288 13073 16 0 210675 0
vsize: 842764
[startup+240.14 s]
Raw data (loadavg): 0.99 0.95 0.91 2/65 12750
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 22961 52 2 1 25 0 11 0 540457875 862990336 24325 4294967295 134512640 134569956 3221224400 3221214632 1131648632 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24325 13073 16 0 210675 0
vsize: 842764
[startup+250.141 s]
Raw data (loadavg): 0.99 0.95 0.91 2/65 12753
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 23944 52 3 1 25 0 11 0 540457875 862990336 24375 4294967295 134512640 134569956 3221224400 3221214672 1131243437 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 24375 13073 16 0 210675 0
vsize: 842764
[startup+260.141 s]
Raw data (loadavg): 0.99 0.95 0.91 2/65 12756
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 24931 53 3 1 25 0 11 0 540457875 862990336 24456 4294967295 134512640 134569956 3221224400 3221214672 1131243148 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24456 13073 16 0 210675 0
vsize: 842764
[startup+270.143 s]
Raw data (loadavg): 0.99 0.95 0.91 2/65 12759
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 25920 53 3 1 25 0 11 0 540457875 862990336 24504 4294967295 134512640 134569956 3221224400 3221214672 1131243169 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24504 13073 16 0 210675 0
vsize: 842764
[startup+280.143 s]
Raw data (loadavg): 0.99 0.95 0.91 2/65 12762
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 26907 54 3 1 25 0 11 0 540457875 862990336 24556 4294967295 134512640 134569956 3221224400 3221214672 1131244590 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24556 13073 16 0 210675 0
vsize: 842764
[startup+290.145 s]
Raw data (loadavg): 0.99 0.95 0.91 2/65 12765
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 27895 54 3 1 25 0 11 0 540457875 862990336 24608 4294967295 134512640 134569956 3221224400 3221214672 1131244396 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24608 13073 16 0 210675 0
vsize: 842764
[startup+300.145 s]
Raw data (loadavg): 0.99 0.95 0.91 2/65 12768
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 28884 55 3 1 25 0 11 0 540457875 862990336 24654 4294967295 134512640 134569956 3221224400 3221214768 1131348240 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24654 13073 16 0 210675 0
vsize: 842764
[startup+310.145 s]
Raw data (loadavg): 0.99 0.95 0.91 2/65 12771
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 29874 55 4 1 25 0 11 0 540457875 862990336 24702 4294967295 134512640 134569956 3221224400 3221214672 1131244401 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24702 13073 16 0 210675 0
vsize: 842764
[startup+320.146 s]
Raw data (loadavg): 0.99 0.95 0.91 2/65 12774
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 30863 55 4 1 25 0 11 0 540457875 862990336 24739 4294967295 134512640 134569956 3221224400 3221214672 1131243137 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24739 13073 16 0 210675 0
vsize: 842764
[startup+330.147 s]
Raw data (loadavg): 0.99 0.95 0.91 2/65 12777
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 31851 56 4 1 25 0 11 0 540457875 862990336 24792 4294967295 134512640 134569956 3221224400 3221214672 1131243519 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24792 13073 16 0 210675 0
vsize: 842764
[startup+340.148 s]
Raw data (loadavg): 0.99 0.96 0.91 2/65 12780
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 32837 56 4 1 25 0 11 0 540457875 862990336 24848 4294967295 134512640 134569956 3221224400 3221214672 1131244460 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24848 13073 16 0 210675 0
vsize: 842764
[startup+350.149 s]
Raw data (loadavg): 0.99 0.96 0.91 2/65 12783
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 33824 56 4 1 25 0 11 0 540457875 862990336 24901 4294967295 134512640 134569956 3221224400 3221214672 1131243554 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24901 13073 16 0 210675 0
vsize: 842764
[startup+360.15 s]
Raw data (loadavg): 0.99 0.96 0.91 2/65 12786
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 34811 57 5 1 25 0 11 0 540457875 862990336 24959 4294967295 134512640 134569956 3221224400 3221214672 1131243213 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 24959 13073 16 0 210675 0
vsize: 842764
[startup+370.151 s]
Raw data (loadavg): 0.99 0.96 0.91 2/65 12789
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 35798 57 5 2 25 0 11 0 540457875 862990336 25030 4294967295 134512640 134569956 3221224400 3221214672 1131243795 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25030 13073 16 0 210675 0
vsize: 842764
[startup+380.152 s]
Raw data (loadavg): 0.99 0.96 0.91 2/65 12794
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 36785 58 5 2 25 0 11 0 540457875 862990336 25095 4294967295 134512640 134569956 3221224400 3221214672 1131243519 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25095 13073 16 0 210675 0
vsize: 842764
[startup+390.152 s]
Raw data (loadavg): 0.99 0.96 0.91 2/65 12797
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 37773 59 5 2 25 0 11 0 540457875 862990336 25158 4294967295 134512640 134569956 3221224400 3221214672 1131243446 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25158 13073 16 0 210675 0
vsize: 842764
[startup+400.154 s]
Raw data (loadavg): 0.99 0.96 0.91 2/65 12800
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 38761 60 5 2 25 0 11 0 540457875 862990336 25214 4294967295 134512640 134569956 3221224400 3221214768 1131349131 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25214 13073 16 0 210675 0
vsize: 842764
[startup+410.153 s]
Raw data (loadavg): 0.99 0.96 0.91 2/65 12803
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 39750 60 5 2 25 0 11 0 540457875 862990336 25281 4294967295 134512640 134569956 3221224400 3221214672 1131243491 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25281 13073 16 0 210675 0
vsize: 842764
[startup+420.154 s]
Raw data (loadavg): 0.99 0.96 0.91 2/65 12806
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 40737 60 5 2 24 0 11 0 540457875 862990336 25335 4294967295 134512640 134569956 3221224400 3221214672 1131243749 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25335 13073 16 0 210675 0
vsize: 842764
[startup+430.156 s]
Raw data (loadavg): 0.99 0.96 0.91 2/65 12809
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 41725 61 5 2 25 0 11 0 540457875 862990336 25373 4294967295 134512640 134569956 3221224400 3221214740 1131648656 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25373 13073 16 0 210675 0
vsize: 842764
[startup+440.156 s]
Raw data (loadavg): 0.99 0.97 0.91 2/65 12812
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 42711 62 5 2 25 0 11 0 540457875 862990336 25414 4294967295 134512640 134569956 3221224400 3221214768 1131348250 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25414 13073 16 0 210675 0
vsize: 842764
[startup+450.157 s]
Raw data (loadavg): 0.99 0.97 0.91 2/65 12815
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 43697 62 5 2 25 0 11 0 540457875 862990336 25480 4294967295 134512640 134569956 3221224400 3221214740 1131411747 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25480 13073 16 0 210675 0
vsize: 842764
[startup+460.157 s]
Raw data (loadavg): 0.99 0.97 0.91 2/65 12819
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 44684 63 6 2 25 0 11 0 540457875 862990336 25533 4294967295 134512640 134569956 3221224400 3221214600 1085679313 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25533 13073 16 0 210675 0
vsize: 842764
[startup+470.158 s]
Raw data (loadavg): 0.99 0.97 0.91 2/65 12822
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 45671 63 6 2 25 0 11 0 540457875 862990336 25674 4294967295 134512640 134569956 3221224400 3221214656 1085679762 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25674 13073 16 0 210675 0
vsize: 842764
[startup+480.157 s]
Raw data (loadavg): 0.99 0.97 0.91 2/65 12825
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 46659 64 6 2 25 0 11 0 540457875 862990336 25715 4294967295 134512640 134569956 3221224400 3221214436 1131648656 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25715 13073 16 0 210675 0
vsize: 842764
[startup+490.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/65 12828
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 47647 64 6 2 25 0 11 0 540457875 862990336 25767 4294967295 134512640 134569956 3221224400 3221214520 1131648657 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25767 13073 16 0 210675 0
vsize: 842764
[startup+500.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/65 12831
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 48635 65 6 3 25 0 11 0 540457875 862990336 25819 4294967295 134512640 134569956 3221224400 3221214728 1131181384 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25819 13073 16 0 210675 0
vsize: 842764
[startup+510.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/65 12834
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 49623 65 6 3 25 0 11 0 540457875 862990336 25877 4294967295 134512640 134569956 3221224400 3221214672 1131243141 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25877 13073 16 0 210675 0
vsize: 842764
[startup+520.163 s]
Raw data (loadavg): 1.15 1.00 0.92 2/65 12837
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 50612 66 7 3 25 0 11 0 540457875 862990336 25930 4294967295 134512640 134569956 3221224400 3221214672 1131243565 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25930 13073 16 0 210675 0
vsize: 842764
[startup+530.163 s]
Raw data (loadavg): 1.12 1.00 0.92 2/65 12840
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 51601 66 7 3 25 0 11 0 540457875 862990336 25996 4294967295 134512640 134569956 3221224400 3221214672 1131243960 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 25996 13073 16 0 210675 0
vsize: 842764
[startup+540.165 s]
Raw data (loadavg): 1.10 1.00 0.92 2/65 12843
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 52592 66 7 3 25 0 11 0 540457875 862990336 26035 4294967295 134512640 134569956 3221224400 3221214768 1131344938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26035 13073 16 0 210675 0
vsize: 842764
[startup+550.166 s]
Raw data (loadavg): 1.09 1.00 0.92 2/65 12846
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 53580 67 7 3 25 0 11 0 540457875 862990336 26066 4294967295 134512640 134569956 3221224400 3221214672 1131243596 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26066 13073 16 0 210675 0
vsize: 842764
[startup+560.166 s]
Raw data (loadavg): 1.07 1.00 0.92 2/65 12849
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 54570 68 8 3 25 0 11 0 540457875 862990336 26107 4294967295 134512640 134569956 3221224400 3221214672 1131243505 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26107 13073 16 0 210675 0
vsize: 842764
[startup+570.167 s]
Raw data (loadavg): 1.06 1.00 0.92 2/65 12852
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 55560 68 8 3 25 0 11 0 540457875 862990336 26142 4294967295 134512640 134569956 3221224400 3221214768 1131343995 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26142 13073 16 0 210675 0
vsize: 842764
[startup+580.167 s]
Raw data (loadavg): 1.05 1.00 0.92 2/65 12855
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 56549 69 8 3 25 0 11 0 540457875 862990336 26167 4294967295 134512640 134569956 3221224400 3221214672 1131243598 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26167 13073 16 0 210675 0
vsize: 842764
[startup+590.168 s]
Raw data (loadavg): 1.04 1.00 0.92 2/65 12858
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 57539 69 8 3 25 0 11 0 540457875 862990336 26211 4294967295 134512640 134569956 3221224400 3221214672 1131244401 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26211 13073 16 0 210675 0
vsize: 842764
[startup+600.168 s]
Raw data (loadavg): 1.04 1.00 0.92 2/65 12861
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 58529 70 8 3 25 0 11 0 540457875 862990336 26253 4294967295 134512640 134569956 3221224400 3221214672 1131244345 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26253 13073 16 0 210675 0
vsize: 842764
[startup+610.17 s]
Raw data (loadavg): 1.18 1.03 0.93 2/65 12864
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 59519 71 8 3 25 0 11 0 540457875 862990336 26281 4294967295 134512640 134569956 3221224400 3221214480 1131651024 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26281 13073 16 0 210675 0
vsize: 842764
[startup+620.171 s]
Raw data (loadavg): 1.16 1.03 0.93 2/65 12867
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 60508 71 8 3 25 0 11 0 540457875 862990336 26327 4294967295 134512640 134569956 3221224400 3221214672 1131244396 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26327 13073 16 0 210675 0
vsize: 842764
[startup+630.171 s]
Raw data (loadavg): 1.13 1.03 0.93 2/65 12870
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 61497 71 8 4 25 0 11 0 540457875 862990336 26356 4294967295 134512640 134569956 3221224400 3221214672 1131243569 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26356 13073 16 0 210675 0
vsize: 842764
[startup+640.173 s]
Raw data (loadavg): 1.11 1.03 0.93 2/65 12873
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 62484 72 9 4 25 0 11 0 540457875 862990336 26399 4294967295 134512640 134569956 3221224400 3221214656 1085679762 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26399 13073 16 0 210675 0
vsize: 842764
[startup+650.173 s]
Raw data (loadavg): 1.09 1.03 0.93 2/65 12876
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 63466 72 9 4 25 0 11 0 540457875 862990336 26428 4294967295 134512640 134569956 3221224400 3221214672 1131244401 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26428 13073 16 0 210675 0
vsize: 842764
[startup+660.173 s]
Raw data (loadavg): 1.08 1.03 0.93 2/65 12879
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 64445 73 9 4 24 0 11 0 540457875 862990336 26520 4294967295 134512640 134569956 3221224400 3221214672 1131243137 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26520 13073 16 0 210675 0
vsize: 842764
[startup+670.175 s]
Raw data (loadavg): 1.07 1.02 0.93 2/65 12883
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 65422 73 9 4 24 0 11 0 540457875 862990336 26634 4294967295 134512640 134569956 3221224400 3221214672 1131243614 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26634 13073 16 0 210675 0
vsize: 842764
[startup+680.175 s]
Raw data (loadavg): 1.06 1.02 0.93 2/65 12889
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 66403 74 9 4 24 0 11 0 540457875 862990336 26908 4294967295 134512640 134569956 3221224400 3221214672 1131244068 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 26908 13073 16 0 210675 0
vsize: 842764
[startup+690.176 s]
Raw data (loadavg): 1.05 1.02 0.93 2/65 12893
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 67386 75 10 4 25 0 11 0 540457875 862990336 27000 4294967295 134512640 134569956 3221224400 3221215048 1130897409 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27000 13073 16 0 210675 0
vsize: 842764
[startup+700.176 s]
Raw data (loadavg): 1.04 1.02 0.93 2/65 12898
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 68369 75 10 4 25 0 11 0 540457875 862990336 27090 4294967295 134512640 134569956 3221224400 3221214672 1131243224 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27090 13073 16 0 210675 0
vsize: 842764
[startup+710.177 s]
Raw data (loadavg): 1.03 1.02 0.93 2/65 12902
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 69351 76 10 4 25 0 11 0 540457875 862990336 27183 4294967295 134512640 134569956 3221224400 3221214672 1131244340 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27183 13073 16 0 210675 0
vsize: 842764
[startup+720.178 s]
Raw data (loadavg): 1.03 1.02 0.93 2/65 12906
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 70332 76 10 4 25 0 11 0 540457875 862990336 27246 4294967295 134512640 134569956 3221224400 3221214672 1131243565 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27246 13073 16 0 210675 0
vsize: 842764
[startup+730.179 s]
Raw data (loadavg): 1.02 1.02 0.93 2/65 12910
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 71312 77 10 4 25 0 11 0 540457875 862990336 27361 4294967295 134512640 134569956 3221224400 3221214672 1131243169 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27361 13073 16 0 210675 0
vsize: 842764
[startup+740.179 s]
Raw data (loadavg): 1.02 1.02 0.93 2/65 12914
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 72292 77 11 4 18 0 11 0 540457875 862990336 27452 4294967295 134512640 134569956 3221224400 3221214672 1131243860 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27452 13073 16 0 210675 0
vsize: 842764
[startup+750.181 s]
Raw data (loadavg): 1.02 1.02 0.93 2/65 12918
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 73272 78 11 4 25 0 11 0 540457875 862990336 27604 4294967295 134512640 134569956 3221224400 3221214764 1131244607 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27604 13073 16 0 210675 0
vsize: 842764
[startup+760.181 s]
Raw data (loadavg): 1.01 1.02 0.93 2/65 12922
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 74254 79 11 4 25 0 11 0 540457875 862990336 27696 4294967295 134512640 134569956 3221224400 3221214672 1131243137 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27696 13073 16 0 210675 0
vsize: 842764
[startup+770.181 s]
Raw data (loadavg): 1.01 1.02 0.93 2/65 12926
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 75238 79 11 4 25 0 11 0 540457875 862990336 27798 4294967295 134512640 134569956 3221224400 3221214672 1131243137 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27798 13073 16 0 210675 0
vsize: 842764
[startup+780.182 s]
Raw data (loadavg): 1.01 1.01 0.93 2/65 12930
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 76222 80 12 4 25 0 11 0 540457875 862990336 27895 4294967295 134512640 134569956 3221224400 3221214672 1131244370 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27895 13073 16 0 210675 0
vsize: 842764
[startup+790.183 s]
Raw data (loadavg): 1.01 1.01 0.93 2/65 12934
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 77208 80 12 4 25 0 11 0 540457875 862990336 27969 4294967295 134512640 134569956 3221224400 3221214764 1131244607 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 27969 13073 16 0 210675 0
vsize: 842764
[startup+800.183 s]
Raw data (loadavg): 1.00 1.01 0.93 2/65 12938
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 78195 81 12 4 25 0 11 0 540457875 862990336 28025 4294967295 134512640 134569956 3221224400 3221214672 1131243169 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 28025 13073 16 0 210675 0
vsize: 842764
[startup+810.183 s]
Raw data (loadavg): 1.00 1.01 0.93 2/65 12942
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 79181 81 12 5 25 0 11 0 540457875 862990336 28063 4294967295 134512640 134569956 3221224400 3221214672 1131243565 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210691 28063 13073 16 0 210675 0
vsize: 842764
[startup+820.184 s]
Raw data (loadavg): 1.00 1.01 0.93 2/65 12946
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 80166 82 12 5 25 0 11 0 540457875 862990336 28087 4294967295 134512640 134569956 3221224400 3221214928 1131420697 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28087 13073 16 0 210675 0
vsize: 842764
[startup+830.185 s]
Raw data (loadavg): 1.00 1.01 0.93 2/65 12950
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 81151 82 12 5 25 0 11 0 540457875 862990336 28200 4294967295 134512640 134569956 3221224400 3221214924 1130885154 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28200 13073 16 0 210675 0
vsize: 842764
[startup+840.185 s]
Raw data (loadavg): 1.00 1.01 0.93 2/65 12954
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 82139 82 13 5 25 0 11 0 540457875 862990336 28226 4294967295 134512640 134569956 3221224400 3221214672 1131244055 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28226 13073 16 0 210675 0
vsize: 842764
[startup+850.186 s]
Raw data (loadavg): 1.00 1.01 0.93 2/65 12958
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 83127 82 13 5 25 0 11 0 540457875 862990336 28263 4294967295 134512640 134569956 3221224400 3221214672 1131244586 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28263 13073 16 0 210675 0
vsize: 842764
[startup+860.186 s]
Raw data (loadavg): 1.00 1.01 0.93 2/65 12962
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 84114 83 13 5 25 0 11 0 540457875 862990336 28288 4294967295 134512640 134569956 3221224400 3221214672 1131243565 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28288 13073 16 0 210675 0
vsize: 842764
[startup+870.188 s]
Raw data (loadavg): 1.00 1.01 0.93 2/65 12966
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 85101 83 13 5 25 0 11 0 540457875 862990336 28330 4294967295 134512640 134569956 3221224400 3221214672 1131243565 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28330 13073 16 0 210675 0
vsize: 842764
[startup+880.189 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 12970
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 86088 83 13 5 25 0 11 0 540457875 862990336 28378 4294967295 134512640 134569956 3221224400 3221214672 1131243565 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28378 13073 16 0 210675 0
vsize: 842764
[startup+890.189 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 12974
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 87075 83 14 5 25 0 11 0 540457875 862990336 28414 4294967295 134512640 134569956 3221224400 3221214672 1131244420 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28414 13073 16 0 210675 0
vsize: 842764
[startup+900.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 12978
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 88061 83 14 5 25 0 11 0 540457875 862990336 28455 4294967295 134512640 134569956 3221224400 3221214768 1131343775 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28455 13073 16 0 210675 0
vsize: 842764
[startup+910.192 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 12983
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 89047 83 14 5 25 0 11 0 540457875 862990336 28515 4294967295 134512640 134569956 3221224400 3221214768 1131348280 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28515 13073 16 0 210675 0
vsize: 842764
[startup+920.193 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 12987
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 90032 84 14 5 25 0 11 0 540457875 862990336 28563 4294967295 134512640 134569956 3221224400 3221214768 1131343995 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28563 13073 16 0 210675 0
vsize: 842764
[startup+930.193 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 12991
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 91018 84 15 6 25 0 11 0 540457875 862990336 28594 4294967295 134512640 134569956 3221224400 3221214672 1131243565 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28594 13073 16 0 210675 0
vsize: 842764
[startup+940.193 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 12995
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 92003 85 15 6 25 0 11 0 540457875 862990336 28659 4294967295 134512640 134569956 3221224400 3221214768 1131344060 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28659 13073 16 0 210675 0
vsize: 842764
[startup+950.194 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 12999
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 92987 85 15 6 25 0 11 0 540457875 862990336 28710 4294967295 134512640 134569956 3221224400 3221214672 1131244059 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28710 13073 16 0 210675 0
vsize: 842764
[startup+960.195 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13003
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 93971 86 15 6 25 0 11 0 540457875 862990336 28806 4294967295 134512640 134569956 3221224400 3221214672 1131244365 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28806 13073 16 0 210675 0
vsize: 842764
[startup+970.196 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13007
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 94947 86 15 6 24 0 11 0 540457875 862990336 28877 4294967295 134512640 134569956 3221224400 3221214672 1131243860 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28877 13073 16 0 210675 0
vsize: 842764
[startup+980.196 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13013
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 95921 86 16 6 25 0 11 0 540457875 862990336 28949 4294967295 134512640 134569956 3221224400 3221214768 1131345116 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 28949 13073 16 0 210675 0
vsize: 842764
[startup+990.197 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13017
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 96898 86 16 6 25 0 11 0 540457875 862990336 29343 4294967295 134512640 134569956 3221224400 3221214672 1131243820 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29343 13073 16 0 210675 0
vsize: 842764
[startup+1000.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13021
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 97884 87 16 6 25 0 11 0 540457875 862990336 29399 4294967295 134512640 134569956 3221224400 3221214672 1131243565 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29399 13073 16 0 210675 0
vsize: 842764
[startup+1010.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13025
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 98869 87 16 6 25 0 11 0 540457875 862990336 29427 4294967295 134512640 134569956 3221224400 3221214672 1131243137 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29427 13073 16 0 210675 0
vsize: 842764
[startup+1020.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13029
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 99855 87 17 6 25 0 11 0 540457875 862990336 29489 4294967295 134512640 134569956 3221224400 3221214768 1131344060 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29489 13073 16 0 210675 0
vsize: 842764
[startup+1030.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13033
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 100840 87 17 6 25 0 11 0 540457875 862990336 29560 4294967295 134512640 134569956 3221224400 3221214672 1131243141 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29560 13073 16 0 210675 0
vsize: 842764
[startup+1040.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13037
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 101827 87 17 6 25 0 11 0 540457875 862990336 29613 4294967295 134512640 134569956 3221224400 3221214672 1131243896 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29613 13073 16 0 210675 0
vsize: 842764
[startup+1050.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13041
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 102814 88 18 6 25 0 11 0 540457875 862990336 29640 4294967295 134512640 134569956 3221224400 3221214672 1131243791 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29640 13073 16 0 210675 0
vsize: 842764
[startup+1060.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13046
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 103800 88 18 6 23 0 11 0 540457875 862990336 29680 4294967295 134512640 134569956 3221224400 3221214768 1131345072 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29680 13073 16 0 210675 0
vsize: 842764
[startup+1070.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13050
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 104786 89 18 6 25 0 11 0 540457875 862990336 29730 4294967295 134512640 134569956 3221224400 3221214764 1131244607 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29730 13073 16 0 210675 0
vsize: 842764
[startup+1080.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13054
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 105768 89 18 7 25 0 11 0 540457875 862990336 29780 4294967295 134512640 134569956 3221224400 3221214672 1131243133 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29780 13073 16 0 210675 0
vsize: 842764
[startup+1090.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13058
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 106749 89 19 7 25 0 11 0 540457875 862990336 29822 4294967295 134512640 134569956 3221224400 3221214672 1131244345 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29822 13073 16 0 210675 0
vsize: 842764
[startup+1100.22 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13062
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 107730 89 19 7 25 0 11 0 540457875 862990336 29968 4294967295 134512640 134569956 3221224400 3221214768 1131344971 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 29968 13073 16 0 210675 0
vsize: 842764
[startup+1110.22 s]
Raw data (loadavg): 1.00 1.00 0.93 2/65 13066
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 108708 89 19 7 25 0 11 0 540457875 862990336 30095 4294967295 134512640 134569956 3221224400 3221214768 1131343988 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 30095 13073 16 0 210675 0
vsize: 842764
[startup+1120.22 s]
Raw data (loadavg): 1.08 1.02 0.94 2/65 13070
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 109685 90 19 7 25 0 11 0 540457875 862990336 30225 4294967295 134512640 134569956 3221224400 3221214672 1131243141 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 30225 13073 16 0 210675 0
vsize: 842764
[startup+1130.23 s]
Raw data (loadavg): 1.07 1.02 0.94 2/65 13074
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 110661 90 19 7 25 0 11 0 540457875 862990336 30373 4294967295 134512640 134569956 3221224400 3221214768 1131343988 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 30373 13073 16 0 210675 0
vsize: 842764
[startup+1140.23 s]
Raw data (loadavg): 1.06 1.01 0.94 2/65 13078
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 111637 91 20 7 25 0 11 0 540457875 862990336 30528 4294967295 134512640 134569956 3221224400 3221214672 1131243141 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 30528 13073 16 0 210675 0
vsize: 842764
[startup+1150.23 s]
Raw data (loadavg): 1.05 1.01 0.94 2/65 13082
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 112613 91 20 7 25 0 11 0 540457875 862990336 30685 4294967295 134512640 134569956 3221224400 3221214672 1131244355 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 30685 13073 16 0 210675 0
vsize: 842764
[startup+1160.23 s]
Raw data (loadavg): 1.04 1.01 0.94 2/65 13086
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 113589 91 20 7 24 0 11 0 540457875 862990336 30875 4294967295 134512640 134569956 3221224400 3221214672 1131243169 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 30875 13073 16 0 210675 0
vsize: 842764
[startup+1170.23 s]
Raw data (loadavg): 1.03 1.01 0.94 2/65 13090
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 114566 91 20 7 25 0 11 0 540457875 862990336 31006 4294967295 134512640 134569956 3221224400 3221214928 1131420697 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 31006 13073 16 0 210675 0
vsize: 842764
[startup+1180.23 s]
Raw data (loadavg): 1.03 1.01 0.94 2/65 13094
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 115543 92 20 7 25 0 11 0 540457875 862990336 31163 4294967295 134512640 134569956 3221224400 3221214768 1131345112 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 31163 13073 16 0 210675 0
vsize: 842764
[startup+1190.23 s]
Raw data (loadavg): 1.02 1.01 0.94 2/65 13098
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 116520 92 20 7 25 0 11 0 540457875 862990336 31319 4294967295 134512640 134569956 3221224400 3221214768 1131343995 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 31319 13073 16 0 210675 0
vsize: 842764
[startup+1200.23 s]
Raw data (loadavg): 1.02 1.01 0.94 2/65 13102
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 117498 92 21 7 25 0 11 0 540457875 862990336 31476 4294967295 134512640 134569956 3221224400 3221214672 1131244396 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 31476 13073 16 0 210675 0
vsize: 842764
[startup+1210.23 s]
Raw data (loadavg): 1.02 1.01 0.94 2/65 13106
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 118477 92 21 7 25 0 11 0 540457875 862990336 31608 4294967295 134512640 134569956 3221224400 3221214672 1131244586 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 31608 13073 16 0 210675 0
vsize: 842764
[startup+1220.23 s]
Raw data (loadavg): 1.01 1.01 0.94 2/65 13110
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 119459 93 21 7 25 0 11 0 540457875 862990336 31728 4294967295 134512640 134569956 3221224400 3221214768 1131345891 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 31728 13073 16 0 210675 0
vsize: 842764
[startup+1230.23 s]
Raw data (loadavg): 1.01 1.01 0.94 2/65 13114
Raw data (stat): 12666 (java) R 12665 20024 20023 0 -1 0 18083 3 1 0 120443 93 21 8 25 0 11 0 540457875 862990336 31818 4294967295 134512640 134569956 3221224400 3221214672 1131243519 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210691 31818 13073 16 0 210675 0
vsize: 842764
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1230.36 s]
Raw data (loadavg): 1.01 1.01 0.94 1/55 13116
Raw data (stat): 12666 (java) Z 12665 20024 20023 0 -1 1036 18083 22559 1 1 120447 99 3738 73 25 0 1 0 540457875 0 0 4294967295 0 0 0 0 0 0 4 3 23756 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 143
Real time (s): 1230.35
CPU time (s): 1243.59
CPU user time (s): 1241.86
CPU system time (s): 1.72874
CPU usage (%): 101.076
Max. virtual memory (Kb): 844812
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####