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-core2536-691.opb
MD5SUM	1a2d760450612ad13ad0fc356acc93dc
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	15464
Biggest coefficient in the objective function	52428800000000000
Number of bits for the biggest coefficient in the objective function	56
Sum of the numbers in the objective function	214380061511534325
Number of bits of the sum of numbers in the objective function	58
Biggest number in a constraint	1280000000000000000000
Number of bits of the biggest number in a constraint	71
Biggest sum of numbers in a constraint	1280214380061511647232
Number of bits of the biggest sum of numbers	71
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	14.8847
Number of variables	15464
Total number of constraints	17823
Number of constraints which are clauses	2536
Number of constraints which are cardinality constraints (but not clauses)	15286
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	15464
Trace number 13925

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-20 22:23:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20029 boxname=wulflinc9 idbench=1541 idsolver=9 numberseed=0
MD5SUM SOLVER: daf345f6fbf228671abfac48013b9cac  /oldhome/oroussel/solvers/sat4jPseudo.jar
MD5SUM BENCH:  1a2d760450612ad13ad0fc356acc93dc  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-core2536-691.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudo.jar /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-core2536-691.opb
IDLAUNCH: 20029
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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:        658908 kB
Buffers:         34560 kB
Cached:         317808 kB
SwapCached:          8 kB
Active:          39676 kB
Inactive:       315492 kB
HighTotal:      131008 kB
HighFree:        33152 kB
LowTotal:       903652 kB
LowFree:        625756 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            14876 kB
Committed_AS:    63580 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:35:34 (client local time) WITH STATUS 1 IN 754.614 SECONDS
stats: 20029 7 754.614 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-core2536-691.opb
c reading problem 
c [nbvar=15464]
c [nbconstr=17823]
c time 83.538
c #vars     15464
c #clauses  2539
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=1432158208
c Current CPU time (ms) : 88.237
c starts	: 1
c conflicts	: 0
c decisions	: 14814
c propagations	: 15464
c inspects	: 25903
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 1
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 88.665
c starts	: 2
c conflicts	: 0
c decisions	: 29628
c propagations	: 30923
c inspects	: 27445
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 2
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 89.012
c starts	: 3
c conflicts	: 0
c decisions	: 44442
c propagations	: 46382
c inspects	: 28836
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 3
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 89.358
c starts	: 4
c conflicts	: 0
c decisions	: 59256
c propagations	: 61841
c inspects	: 30227
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 4
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 89.98
c starts	: 5
c conflicts	: 0
c decisions	: 74070
c propagations	: 77300
c inspects	: 31618
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 5
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 90.327
c starts	: 6
c conflicts	: 0
c decisions	: 88884
c propagations	: 92759
c inspects	: 33009
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 6
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 90.673
c starts	: 7
c conflicts	: 0
c decisions	: 103698
c propagations	: 108218
c inspects	: 34400
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 7
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 91.03
c starts	: 8
c conflicts	: 0
c decisions	: 118512
c propagations	: 123677
c inspects	: 35791
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 8
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 91.387
c starts	: 9
c conflicts	: 0
c decisions	: 133326
c propagations	: 139136
c inspects	: 37182
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 9
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 92.086
c starts	: 10
c conflicts	: 0
c decisions	: 148140
c propagations	: 154595
c inspects	: 38573
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 10
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 92.439
c starts	: 11
c conflicts	: 0
c decisions	: 162954
c propagations	: 170054
c inspects	: 39964
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 11
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 92.785
c starts	: 12
c conflicts	: 0
c decisions	: 177768
c propagations	: 185513
c inspects	: 41355
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 12
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 93.146
c starts	: 13
c conflicts	: 0
c decisions	: 192582
c propagations	: 200972
c inspects	: 42746
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 13
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 93.839
c starts	: 14
c conflicts	: 0
c decisions	: 207396
c propagations	: 216431
c inspects	: 44137
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 14
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 94.207
c starts	: 15
c conflicts	: 0
c decisions	: 222210
c propagations	: 231890
c inspects	: 45528
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 15
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 94.573
c starts	: 16
c conflicts	: 0
c decisions	: 237024
c propagations	: 247349
c inspects	: 46919
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 16
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 94.958
c starts	: 17
c conflicts	: 0
c decisions	: 251838
c propagations	: 262808
c inspects	: 48310
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 17
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 95.327
c starts	: 18
c conflicts	: 0
c decisions	: 266652
c propagations	: 278267
c inspects	: 49701
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 18
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 96.011
c starts	: 19
c conflicts	: 0
c decisions	: 281466
c propagations	: 293726
c inspects	: 51092
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 19
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 96.383
c starts	: 20
c conflicts	: 0
c decisions	: 296280
c propagations	: 309185
c inspects	: 52483
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 20
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 96.753
c starts	: 21
c conflicts	: 0
c decisions	: 311094
c propagations	: 324644
c inspects	: 53874
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 21
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 97.129
c starts	: 22
c conflicts	: 0
c decisions	: 325908
c propagations	: 340103
c inspects	: 55265
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 22
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 97.839
c starts	: 23
c conflicts	: 0
c decisions	: 340722
c propagations	: 355562
c inspects	: 56656
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 23
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 98.226
c starts	: 24
c conflicts	: 0
c decisions	: 355536
c propagations	: 371021
c inspects	: 58047
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 24
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 98.568
c starts	: 25
c conflicts	: 0
c decisions	: 370350
c propagations	: 386480
c inspects	: 59385
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 25
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 98.95
c starts	: 26
c conflicts	: 0
c decisions	: 385164
c propagations	: 401939
c inspects	: 60776
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 26
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 99.338
c starts	: 27
c conflicts	: 0
c decisions	: 399978
c propagations	: 417398
c inspects	: 62167
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 27
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 100.038
c starts	: 28
c conflicts	: 0
c decisions	: 414792
c propagations	: 432857
c inspects	: 63558
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 28
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 100.387
c starts	: 29
c conflicts	: 0
c decisions	: 429606
c propagations	: 448316
c inspects	: 64866
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 29
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 100.736
c starts	: 30
c conflicts	: 0
c decisions	: 444420
c propagations	: 463775
c inspects	: 66204
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 30
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 101.126
c starts	: 31
c conflicts	: 0
c decisions	: 459234
c propagations	: 479234
c inspects	: 67595
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 31
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 101.519
c starts	: 32
c conflicts	: 0
c decisions	: 474048
c propagations	: 494693
c inspects	: 68986
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 32
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 102.324
c starts	: 33
c conflicts	: 0
c decisions	: 488862
c propagations	: 510152
c inspects	: 70377
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 33
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 102.681
c starts	: 34
c conflicts	: 0
c decisions	: 503676
c propagations	: 525611
c inspects	: 71717
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 34
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 103.077
c starts	: 35
c conflicts	: 0
c decisions	: 518490
c propagations	: 541070
c inspects	: 73108
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 35
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 103.467
c starts	: 36
c conflicts	: 0
c decisions	: 533304
c propagations	: 556529
c inspects	: 74499
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 36
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 104.144
c starts	: 37
c conflicts	: 0
c decisions	: 548118
c propagations	: 571988
c inspects	: 75890
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 37
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 104.546
c starts	: 38
c conflicts	: 0
c decisions	: 562932
c propagations	: 587447
c inspects	: 77281
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 38
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 104.952
c starts	: 39
c conflicts	: 0
c decisions	: 577746
c propagations	: 602906
c inspects	: 78672
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 39
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 105.358
c starts	: 40
c conflicts	: 0
c decisions	: 592560
c propagations	: 618365
c inspects	: 80063
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 40
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 105.727
c starts	: 41
c conflicts	: 0
c decisions	: 607374
c propagations	: 633824
c inspects	: 81403
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 41
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 106.455
c starts	: 42
c conflicts	: 0
c decisions	: 622188
c propagations	: 649283
c inspects	: 82794
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 42
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 106.866
c starts	: 43
c conflicts	: 0
c decisions	: 637002
c propagations	: 664742
c inspects	: 84185
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 43
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 107.275
c starts	: 44
c conflicts	: 0
c decisions	: 651816
c propagations	: 680201
c inspects	: 85576
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 44
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 107.688
c starts	: 45
c conflicts	: 0
c decisions	: 666630
c propagations	: 695660
c inspects	: 86967
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 45
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 108.1
c starts	: 46
c conflicts	: 0
c decisions	: 681444
c propagations	: 711119
c inspects	: 88358
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 46
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 108.84
c starts	: 47
c conflicts	: 0
c decisions	: 696258
c propagations	: 726578
c inspects	: 89749
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 47
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 109.259
c starts	: 48
c conflicts	: 0
c decisions	: 711072
c propagations	: 742037
c inspects	: 91140
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 48
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 109.678
c starts	: 49
c conflicts	: 0
c decisions	: 725886
c propagations	: 757496
c inspects	: 92531
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 49
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 110.103
c starts	: 50
c conflicts	: 0
c decisions	: 740700
c propagations	: 772955
c inspects	: 93922
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 50
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 110.865
c starts	: 51
c conflicts	: 0
c decisions	: 755514
c propagations	: 788414
c inspects	: 95313
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 51
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 111.294
c starts	: 52
c conflicts	: 0
c decisions	: 770328
c propagations	: 803873
c inspects	: 96704
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 52
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 111.718
c starts	: 53
c conflicts	: 0
c decisions	: 785142
c propagations	: 819332
c inspects	: 98095
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 53
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 112.148
c starts	: 54
c conflicts	: 0
c decisions	: 799956
c propagations	: 834791
c inspects	: 99486
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 54
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 112.581
c starts	: 55
c conflicts	: 0
c decisions	: 814770
c propagations	: 850250
c inspects	: 100877
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 55
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 113.283
c starts	: 56
c conflicts	: 0
c decisions	: 829584
c propagations	: 865709
c inspects	: 102215
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 56
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 113.719
c starts	: 57
c conflicts	: 0
c decisions	: 844398
c propagations	: 881168
c inspects	: 103606
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 57
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 114.151
c starts	: 58
c conflicts	: 0
c decisions	: 859212
c propagations	: 896627
c inspects	: 104997
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 58
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 114.584
c starts	: 59
c conflicts	: 0
c decisions	: 874026
c propagations	: 912086
c inspects	: 106388
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 59
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 115.016
c starts	: 60
c conflicts	: 0
c decisions	: 888840
c propagations	: 927545
c inspects	: 107779
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 60
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 115.77
c starts	: 61
c conflicts	: 0
c decisions	: 903654
c propagations	: 943004
c inspects	: 109170
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 61
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 116.211
c starts	: 62
c conflicts	: 0
c decisions	: 918468
c propagations	: 958463
c inspects	: 110561
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 62
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 116.65
c starts	: 63
c conflicts	: 0
c decisions	: 933282
c propagations	: 973922
c inspects	: 111952
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 63
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 117.095
c starts	: 64
c conflicts	: 0
c decisions	: 948096
c propagations	: 989381
c inspects	: 113343
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 64
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 117.97
c starts	: 65
c conflicts	: 0
c decisions	: 962910
c propagations	: 1004840
c inspects	: 114734
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 65
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 118.422
c starts	: 66
c conflicts	: 0
c decisions	: 977724
c propagations	: 1020299
c inspects	: 116125
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 66
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 118.874
c starts	: 67
c conflicts	: 0
c decisions	: 992538
c propagations	: 1035758
c inspects	: 117516
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 67
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 119.334
c starts	: 68
c conflicts	: 0
c decisions	: 1007352
c propagations	: 1051217
c inspects	: 118907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 68
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 120.042
c starts	: 69
c conflicts	: 0
c decisions	: 1022166
c propagations	: 1066676
c inspects	: 120251
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 69
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 120.501
c starts	: 70
c conflicts	: 0
c decisions	: 1036980
c propagations	: 1082135
c inspects	: 121642
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 70
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 120.96
c starts	: 71
c conflicts	: 0
c decisions	: 1051794
c propagations	: 1097594
c inspects	: 123033
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 71
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 121.415
c starts	: 72
c conflicts	: 0
c decisions	: 1066608
c propagations	: 1113053
c inspects	: 124424
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 72
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 121.88
c starts	: 73
c conflicts	: 0
c decisions	: 1081422
c propagations	: 1128512
c inspects	: 125815
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 73
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 122.639
c starts	: 74
c conflicts	: 0
c decisions	: 1096236
c propagations	: 1143971
c inspects	: 127206
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 74
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 123.107
c starts	: 75
c conflicts	: 0
c decisions	: 1111050
c propagations	: 1159430
c inspects	: 128597
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 75
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 123.582
c starts	: 76
c conflicts	: 0
c decisions	: 1125864
c propagations	: 1174889
c inspects	: 129988
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 76
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 124.052
c starts	: 77
c conflicts	: 0
c decisions	: 1140678
c propagations	: 1190348
c inspects	: 131379
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 77
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 124.523
c starts	: 78
c conflicts	: 0
c decisions	: 1155492
c propagations	: 1205807
c inspects	: 132770
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 78
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 125.312
c starts	: 79
c conflicts	: 0
c decisions	: 1170306
c propagations	: 1221266
c inspects	: 134161
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 79
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 125.789
c starts	: 80
c conflicts	: 0
c decisions	: 1185120
c propagations	: 1236725
c inspects	: 135552
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 80
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 126.262
c starts	: 81
c conflicts	: 0
c decisions	: 1199934
c propagations	: 1252184
c inspects	: 136943
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 81
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 126.741
c starts	: 82
c conflicts	: 0
c decisions	: 1214748
c propagations	: 1267643
c inspects	: 138334
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 82
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 127.519
c starts	: 83
c conflicts	: 0
c decisions	: 1229562
c propagations	: 1283102
c inspects	: 139725
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 83
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 128.003
c starts	: 84
c conflicts	: 0
c decisions	: 1244376
c propagations	: 1298561
c inspects	: 141116
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 84
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 128.481
c starts	: 85
c conflicts	: 0
c decisions	: 1259190
c propagations	: 1314020
c inspects	: 142507
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 85
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 128.968
c starts	: 86
c conflicts	: 0
c decisions	: 1274004
c propagations	: 1329479
c inspects	: 143898
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 86
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 129.457
c starts	: 87
c conflicts	: 0
c decisions	: 1288818
c propagations	: 1344938
c inspects	: 145289
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 87
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 130.245
c starts	: 88
c conflicts	: 0
c decisions	: 1303632
c propagations	: 1360397
c inspects	: 146680
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 88
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 130.74
c starts	: 89
c conflicts	: 0
c decisions	: 1318446
c propagations	: 1375856
c inspects	: 148071
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 89
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 131.192
c starts	: 90
c conflicts	: 0
c decisions	: 1333260
c propagations	: 1391315
c inspects	: 149411
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 90
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 131.69
c starts	: 91
c conflicts	: 0
c decisions	: 1348074
c propagations	: 1406774
c inspects	: 150802
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 91
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 132.502
c starts	: 92
c conflicts	: 0
c decisions	: 1362888
c propagations	: 1422233
c inspects	: 152193
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 92
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 133.006
c starts	: 93
c conflicts	: 0
c decisions	: 1377702
c propagations	: 1437692
c inspects	: 153584
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 93
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 133.508
c starts	: 94
c conflicts	: 0
c decisions	: 1392516
c propagations	: 1453151
c inspects	: 154975
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 94
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 134.008
c starts	: 95
c conflicts	: 0
c decisions	: 1407330
c propagations	: 1468610
c inspects	: 156366
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 95
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 134.515
c starts	: 96
c conflicts	: 0
c decisions	: 1422144
c propagations	: 1484069
c inspects	: 157757
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 96
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 135.324
c starts	: 97
c conflicts	: 0
c decisions	: 1436958
c propagations	: 1499528
c inspects	: 159148
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 97
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 135.837
c starts	: 98
c conflicts	: 0
c decisions	: 1451772
c propagations	: 1514987
c inspects	: 160539
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 98
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 136.346
c starts	: 99
c conflicts	: 0
c decisions	: 1466586
c propagations	: 1530446
c inspects	: 161930
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 99
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 136.857
c starts	: 100
c conflicts	: 0
c decisions	: 1481400
c propagations	: 1545905
c inspects	: 163321
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 100
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 137.677
c starts	: 101
c conflicts	: 0
c decisions	: 1496214
c propagations	: 1561364
c inspects	: 164712
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 101
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 138.189
c starts	: 102
c conflicts	: 0
c decisions	: 1511028
c propagations	: 1576823
c inspects	: 166103
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 102
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 138.708
c starts	: 103
c conflicts	: 0
c decisions	: 1525842
c propagations	: 1592282
c inspects	: 167494
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 103
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 139.227
c starts	: 104
c conflicts	: 0
c decisions	: 1540656
c propagations	: 1607741
c inspects	: 168885
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 104
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 139.746
c starts	: 105
c conflicts	: 0
c decisions	: 1555470
c propagations	: 1623200
c inspects	: 170276
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 105
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 140.582
c starts	: 106
c conflicts	: 0
c decisions	: 1570284
c propagations	: 1638659
c inspects	: 171667
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 106
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 141.106
c starts	: 107
c conflicts	: 0
c decisions	: 1585098
c propagations	: 1654118
c inspects	: 173058
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 107
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 141.628
c starts	: 108
c conflicts	: 0
c decisions	: 1599912
c propagations	: 1669577
c inspects	: 174449
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 108
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 142.155
c starts	: 109
c conflicts	: 0
c decisions	: 1614726
c propagations	: 1685036
c inspects	: 175840
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 109
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 142.681
c starts	: 110
c conflicts	: 0
c decisions	: 1629540
c propagations	: 1700495
c inspects	: 177231
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 110
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 143.472
c starts	: 111
c conflicts	: 0
c decisions	: 1644354
c propagations	: 1715954
c inspects	: 178569
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 111
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 143.965
c starts	: 112
c conflicts	: 0
c decisions	: 1659168
c propagations	: 1731413
c inspects	: 179903
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 112
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 144.501
c starts	: 113
c conflicts	: 0
c decisions	: 1673982
c propagations	: 1746872
c inspects	: 181294
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 113
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 145.04
c starts	: 114
c conflicts	: 0
c decisions	: 1688796
c propagations	: 1762331
c inspects	: 182685
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 114
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 145.578
c starts	: 115
c conflicts	: 0
c decisions	: 1703610
c propagations	: 1777790
c inspects	: 184076
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 115
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 146.447
c starts	: 116
c conflicts	: 0
c decisions	: 1718424
c propagations	: 1793249
c inspects	: 185467
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 116
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 146.985
c starts	: 117
c conflicts	: 0
c decisions	: 1733238
c propagations	: 1808708
c inspects	: 186858
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 117
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 147.527
c starts	: 118
c conflicts	: 0
c decisions	: 1748052
c propagations	: 1824167
c inspects	: 188249
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 118
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 148.071
c starts	: 119
c conflicts	: 0
c decisions	: 1762866
c propagations	: 1839626
c inspects	: 189640
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 119
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 148.928
c starts	: 120
c conflicts	: 0
c decisions	: 1777680
c propagations	: 1855085
c inspects	: 191031
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 120
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 149.477
c starts	: 121
c conflicts	: 0
c decisions	: 1792494
c propagations	: 1870544
c inspects	: 192422
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 121
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 150.024
c starts	: 122
c conflicts	: 0
c decisions	: 1807308
c propagations	: 1886003
c inspects	: 193813
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 122
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 150.574
c starts	: 123
c conflicts	: 0
c decisions	: 1822122
c propagations	: 1901462
c inspects	: 195204
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 123
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 151.126
c starts	: 124
c conflicts	: 0
c decisions	: 1836936
c propagations	: 1916921
c inspects	: 196595
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 124
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 151.987
c starts	: 125
c conflicts	: 0
c decisions	: 1851750
c propagations	: 1932380
c inspects	: 197986
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 125
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 152.505
c starts	: 126
c conflicts	: 0
c decisions	: 1866564
c propagations	: 1947839
c inspects	: 199324
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 126
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 153.062
c starts	: 127
c conflicts	: 0
c decisions	: 1881378
c propagations	: 1963298
c inspects	: 200715
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 127
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 153.617
c starts	: 128
c conflicts	: 0
c decisions	: 1896192
c propagations	: 1978757
c inspects	: 202106
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 128
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 154.608
c starts	: 129
c conflicts	: 0
c decisions	: 1911006
c propagations	: 1994216
c inspects	: 203497
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 129
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 155.171
c starts	: 130
c conflicts	: 0
c decisions	: 1925820
c propagations	: 2009675
c inspects	: 204888
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 130
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 155.736
c starts	: 131
c conflicts	: 0
c decisions	: 1940634
c propagations	: 2025134
c inspects	: 206279
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 131
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 156.67
c starts	: 132
c conflicts	: 0
c decisions	: 1955448
c propagations	: 2040593
c inspects	: 207670
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 132
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 157.243
c starts	: 133
c conflicts	: 0
c decisions	: 1970262
c propagations	: 2056052
c inspects	: 209061
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 133
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 157.812
c starts	: 134
c conflicts	: 0
c decisions	: 1985076
c propagations	: 2071511
c inspects	: 210452
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 134
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 158.385
c starts	: 135
c conflicts	: 0
c decisions	: 1999890
c propagations	: 2086970
c inspects	: 211843
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 135
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 159.218
c starts	: 136
c conflicts	: 0
c decisions	: 2014704
c propagations	: 2102429
c inspects	: 213234
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 136
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 159.797
c starts	: 137
c conflicts	: 0
c decisions	: 2029518
c propagations	: 2117888
c inspects	: 214625
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 137
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 160.374
c starts	: 138
c conflicts	: 0
c decisions	: 2044332
c propagations	: 2133347
c inspects	: 216016
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 138
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 160.954
c starts	: 139
c conflicts	: 0
c decisions	: 2059146
c propagations	: 2148806
c inspects	: 217407
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 139
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 161.538
c starts	: 140
c conflicts	: 0
c decisions	: 2073960
c propagations	: 2164265
c inspects	: 218798
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 140
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 162.465
c starts	: 141
c conflicts	: 0
c decisions	: 2088774
c propagations	: 2179724
c inspects	: 220189
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 141
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 163.05
c starts	: 142
c conflicts	: 0
c decisions	: 2103588
c propagations	: 2195183
c inspects	: 221580
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 142
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 163.636
c starts	: 143
c conflicts	: 0
c decisions	: 2118402
c propagations	: 2210642
c inspects	: 222971
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 143
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 164.221
c starts	: 144
c conflicts	: 0
c decisions	: 2133216
c propagations	: 2226101
c inspects	: 224362
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 144
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 164.804
c starts	: 145
c conflicts	: 0
c decisions	: 2148030
c propagations	: 2241560
c inspects	: 225753
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 145
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 165.711
c starts	: 146
c conflicts	: 0
c decisions	: 2162844
c propagations	: 2257019
c inspects	: 227144
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 146
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 166.307
c starts	: 147
c conflicts	: 0
c decisions	: 2177658
c propagations	: 2272478
c inspects	: 228535
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 147
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 166.9
c starts	: 148
c conflicts	: 0
c decisions	: 2192472
c propagations	: 2287937
c inspects	: 229926
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 148
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 167.498
c starts	: 149
c conflicts	: 0
c decisions	: 2207286
c propagations	: 2303396
c inspects	: 231317
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 149
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 168.385
c starts	: 150
c conflicts	: 0
c decisions	: 2222100
c propagations	: 2318855
c inspects	: 232657
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 150
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 168.985
c starts	: 151
c conflicts	: 0
c decisions	: 2236914
c propagations	: 2334314
c inspects	: 234048
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 151
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 169.586
c starts	: 152
c conflicts	: 0
c decisions	: 2251728
c propagations	: 2349773
c inspects	: 235439
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 152
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 170.195
c starts	: 153
c conflicts	: 0
c decisions	: 2266542
c propagations	: 2365232
c inspects	: 236830
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 153
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 170.763
c starts	: 154
c conflicts	: 0
c decisions	: 2281356
c propagations	: 2380691
c inspects	: 238168
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 154
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 171.68
c starts	: 155
c conflicts	: 0
c decisions	: 2296170
c propagations	: 2396150
c inspects	: 239559
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 155
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 172.291
c starts	: 156
c conflicts	: 0
c decisions	: 2310984
c propagations	: 2411609
c inspects	: 240950
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 156
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 172.899
c starts	: 157
c conflicts	: 0
c decisions	: 2325798
c propagations	: 2427068
c inspects	: 242341
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 157
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 173.511
c starts	: 158
c conflicts	: 0
c decisions	: 2340612
c propagations	: 2442527
c inspects	: 243732
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 158
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 174.127
c starts	: 159
c conflicts	: 0
c decisions	: 2355426
c propagations	: 2457986
c inspects	: 245123
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 159
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 175.112
c starts	: 160
c conflicts	: 0
c decisions	: 2370240
c propagations	: 2473445
c inspects	: 246514
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 160
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 175.734
c starts	: 161
c conflicts	: 0
c decisions	: 2385054
c propagations	: 2488904
c inspects	: 247905
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 161
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 176.354
c starts	: 162
c conflicts	: 0
c decisions	: 2399868
c propagations	: 2504363
c inspects	: 249296
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 162
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 176.977
c starts	: 163
c conflicts	: 0
c decisions	: 2414682
c propagations	: 2519822
c inspects	: 250687
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 163
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 177.928
c starts	: 164
c conflicts	: 0
c decisions	: 2429496
c propagations	: 2535281
c inspects	: 252078
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 164
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 178.518
c starts	: 165
c conflicts	: 0
c decisions	: 2444310
c propagations	: 2550740
c inspects	: 253416
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 165
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 179.145
c starts	: 166
c conflicts	: 0
c decisions	: 2459124
c propagations	: 2566199
c inspects	: 254807
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 166
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 179.773
c starts	: 167
c conflicts	: 0
c decisions	: 2473938
c propagations	: 2581658
c inspects	: 256198
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 167
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 180.401
c starts	: 168
c conflicts	: 0
c decisions	: 2488752
c propagations	: 2597117
c inspects	: 257589
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 168
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 181.333
c starts	: 169
c conflicts	: 0
c decisions	: 2503566
c propagations	: 2612576
c inspects	: 258980
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 169
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 181.971
c starts	: 170
c conflicts	: 0
c decisions	: 2518380
c propagations	: 2628035
c inspects	: 260371
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 170
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 182.606
c starts	: 171
c conflicts	: 0
c decisions	: 2533194
c propagations	: 2643494
c inspects	: 261762
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 171
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 183.245
c starts	: 172
c conflicts	: 0
c decisions	: 2548008
c propagations	: 2658953
c inspects	: 263153
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 172
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 183.845
c starts	: 173
c conflicts	: 0
c decisions	: 2562822
c propagations	: 2674412
c inspects	: 264492
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 173
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 184.812
c starts	: 174
c conflicts	: 0
c decisions	: 2577636
c propagations	: 2689871
c inspects	: 265883
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 174
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 185.456
c starts	: 175
c conflicts	: 0
c decisions	: 2592450
c propagations	: 2705330
c inspects	: 267274
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 175
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 186.098
c starts	: 176
c conflicts	: 0
c decisions	: 2607264
c propagations	: 2720789
c inspects	: 268665
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 176
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 186.745
c starts	: 177
c conflicts	: 0
c decisions	: 2622078
c propagations	: 2736248
c inspects	: 270056
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 177
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 187.688
c starts	: 178
c conflicts	: 0
c decisions	: 2636892
c propagations	: 2751707
c inspects	: 271394
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 178
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 188.304
c starts	: 179
c conflicts	: 0
c decisions	: 2651706
c propagations	: 2767166
c inspects	: 272732
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 179
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 188.952
c starts	: 180
c conflicts	: 0
c decisions	: 2666520
c propagations	: 2782625
c inspects	: 274123
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 180
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 189.607
c starts	: 181
c conflicts	: 0
c decisions	: 2681334
c propagations	: 2798084
c inspects	: 275514
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 181
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 190.261
c starts	: 182
c conflicts	: 0
c decisions	: 2696148
c propagations	: 2813543
c inspects	: 276905
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 182
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 191.237
c starts	: 183
c conflicts	: 0
c decisions	: 2710962
c propagations	: 2829002
c inspects	: 278296
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 183
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 191.899
c starts	: 184
c conflicts	: 0
c decisions	: 2725776
c propagations	: 2844461
c inspects	: 279687
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 184
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 192.56
c starts	: 185
c conflicts	: 0
c decisions	: 2740590
c propagations	: 2859920
c inspects	: 281078
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 185
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 193.224
c starts	: 186
c conflicts	: 0
c decisions	: 2755404
c propagations	: 2875379
c inspects	: 282469
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 186
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 193.889
c starts	: 187
c conflicts	: 0
c decisions	: 2770218
c propagations	: 2890838
c inspects	: 283860
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 187
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 194.864
c starts	: 188
c conflicts	: 0
c decisions	: 2785032
c propagations	: 2906297
c inspects	: 285251
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 188
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 195.532
c starts	: 189
c conflicts	: 0
c decisions	: 2799846
c propagations	: 2921756
c inspects	: 286642
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 189
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 196.202
c starts	: 190
c conflicts	: 0
c decisions	: 2814660
c propagations	: 2937215
c inspects	: 288033
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 190
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 196.842
c starts	: 191
c conflicts	: 0
c decisions	: 2829474
c propagations	: 2952674
c inspects	: 289372
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 191
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 197.474
c starts	: 192
c conflicts	: 0
c decisions	: 2844288
c propagations	: 2968133
c inspects	: 290710
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 192
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 198.48
c starts	: 193
c conflicts	: 0
c decisions	: 2859102
c propagations	: 2983592
c inspects	: 292101
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 193
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 199.172
c starts	: 194
c conflicts	: 0
c decisions	: 2873916
c propagations	: 2999051
c inspects	: 293492
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 194
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 199.845
c starts	: 195
c conflicts	: 0
c decisions	: 2888730
c propagations	: 3014510
c inspects	: 294883
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 195
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 200.525
c starts	: 196
c conflicts	: 0
c decisions	: 2903544
c propagations	: 3029969
c inspects	: 296274
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 196
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 201.537
c starts	: 197
c conflicts	: 0
c decisions	: 2918358
c propagations	: 3045428
c inspects	: 297665
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 197
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 202.22
c starts	: 198
c conflicts	: 0
c decisions	: 2933172
c propagations	: 3060887
c inspects	: 299056
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 198
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 202.903
c starts	: 199
c conflicts	: 0
c decisions	: 2947986
c propagations	: 3076346
c inspects	: 300447
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 199
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 203.59
c starts	: 200
c conflicts	: 0
c decisions	: 2962800
c propagations	: 3091805
c inspects	: 301838
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 200
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 204.278
c starts	: 201
c conflicts	: 0
c decisions	: 2977614
c propagations	: 3107264
c inspects	: 303229
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 201
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 205.29
c starts	: 202
c conflicts	: 0
c decisions	: 2992428
c propagations	: 3122723
c inspects	: 304620
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 202
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 205.984
c starts	: 203
c conflicts	: 0
c decisions	: 3007242
c propagations	: 3138182
c inspects	: 306011
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 203
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 206.677
c starts	: 204
c conflicts	: 0
c decisions	: 3022056
c propagations	: 3153641
c inspects	: 307402
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 204
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 207.385
c starts	: 205
c conflicts	: 0
c decisions	: 3036870
c propagations	: 3169100
c inspects	: 308793
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 205
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 208.371
c starts	: 206
c conflicts	: 0
c decisions	: 3051684
c propagations	: 3184559
c inspects	: 310132
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 206
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 209.071
c starts	: 207
c conflicts	: 0
c decisions	: 3066498
c propagations	: 3200018
c inspects	: 311523
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 207
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 209.773
c starts	: 208
c conflicts	: 0
c decisions	: 3081312
c propagations	: 3215477
c inspects	: 312914
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 208
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 210.471
c starts	: 209
c conflicts	: 0
c decisions	: 3096126
c propagations	: 3230936
c inspects	: 314305
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 209
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 211.174
c starts	: 210
c conflicts	: 0
c decisions	: 3110940
c propagations	: 3246395
c inspects	: 315696
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 210
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 212.183
c starts	: 211
c conflicts	: 0
c decisions	: 3125754
c propagations	: 3261854
c inspects	: 317087
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 211
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 212.889
c starts	: 212
c conflicts	: 0
c decisions	: 3140568
c propagations	: 3277313
c inspects	: 318478
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 212
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 213.598
c starts	: 213
c conflicts	: 0
c decisions	: 3155382
c propagations	: 3292772
c inspects	: 319869
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 213
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 214.306
c starts	: 214
c conflicts	: 0
c decisions	: 3170196
c propagations	: 3308231
c inspects	: 321260
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 214
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 215.017
c starts	: 215
c conflicts	: 0
c decisions	: 3185010
c propagations	: 3323690
c inspects	: 322651
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 215
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 216.046
c starts	: 216
c conflicts	: 0
c decisions	: 3199824
c propagations	: 3339149
c inspects	: 324042
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 216
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 216.765
c starts	: 217
c conflicts	: 0
c decisions	: 3214638
c propagations	: 3354608
c inspects	: 325433
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 217
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 217.484
c starts	: 218
c conflicts	: 0
c decisions	: 3229452
c propagations	: 3370067
c inspects	: 326824
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 218
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 218.199
c starts	: 219
c conflicts	: 0
c decisions	: 3244266
c propagations	: 3385526
c inspects	: 328215
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 219
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 219.217
c starts	: 220
c conflicts	: 0
c decisions	: 3259080
c propagations	: 3400985
c inspects	: 329606
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 220
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 219.945
c starts	: 221
c conflicts	: 0
c decisions	: 3273894
c propagations	: 3416444
c inspects	: 330997
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 221
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 220.672
c starts	: 222
c conflicts	: 0
c decisions	: 3288708
c propagations	: 3431903
c inspects	: 332388
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 222
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 221.398
c starts	: 223
c conflicts	: 0
c decisions	: 3303522
c propagations	: 3447362
c inspects	: 333779
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 223
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 222.124
c starts	: 224
c conflicts	: 0
c decisions	: 3318336
c propagations	: 3462821
c inspects	: 335170
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 224
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 223.159
c starts	: 225
c conflicts	: 0
c decisions	: 3333150
c propagations	: 3478280
c inspects	: 336561
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 225
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 223.896
c starts	: 226
c conflicts	: 0
c decisions	: 3347964
c propagations	: 3493739
c inspects	: 337952
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 226
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 224.63
c starts	: 227
c conflicts	: 0
c decisions	: 3362778
c propagations	: 3509198
c inspects	: 339343
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 227
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 225.367
c starts	: 228
c conflicts	: 0
c decisions	: 3377592
c propagations	: 3524657
c inspects	: 340734
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 228
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 226.436
c starts	: 229
c conflicts	: 0
c decisions	: 3392406
c propagations	: 3540116
c inspects	: 342125
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 229
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 227.177
c starts	: 230
c conflicts	: 0
c decisions	: 3407220
c propagations	: 3555575
c inspects	: 343516
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 230
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 227.918
c starts	: 231
c conflicts	: 0
c decisions	: 3422034
c propagations	: 3571034
c inspects	: 344907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 231
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 228.657
c starts	: 232
c conflicts	: 0
c decisions	: 3436848
c propagations	: 3586493
c inspects	: 346298
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 232
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 229.394
c starts	: 233
c conflicts	: 0
c decisions	: 3451662
c propagations	: 3601952
c inspects	: 347689
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 233
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 230.448
c starts	: 234
c conflicts	: 0
c decisions	: 3466476
c propagations	: 3617411
c inspects	: 349080
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 234
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 231.197
c starts	: 235
c conflicts	: 0
c decisions	: 3481290
c propagations	: 3632870
c inspects	: 350471
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 235
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 231.944
c starts	: 236
c conflicts	: 0
c decisions	: 3496104
c propagations	: 3648329
c inspects	: 351862
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 236
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 232.693
c starts	: 237
c conflicts	: 0
c decisions	: 3510918
c propagations	: 3663788
c inspects	: 353253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 237
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 233.399
c starts	: 238
c conflicts	: 0
c decisions	: 3525732
c propagations	: 3679247
c inspects	: 354591
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 238
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 234.477
c starts	: 239
c conflicts	: 0
c decisions	: 3540546
c propagations	: 3694706
c inspects	: 355982
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 239
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 235.233
c starts	: 240
c conflicts	: 0
c decisions	: 3555360
c propagations	: 3710165
c inspects	: 357373
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 240
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 235.989
c starts	: 241
c conflicts	: 0
c decisions	: 3570174
c propagations	: 3725624
c inspects	: 358764
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 241
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 236.751
c starts	: 242
c conflicts	: 0
c decisions	: 3584988
c propagations	: 3741083
c inspects	: 360155
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 242
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 237.824
c starts	: 243
c conflicts	: 0
c decisions	: 3599802
c propagations	: 3756542
c inspects	: 361546
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 243
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 238.591
c starts	: 244
c conflicts	: 0
c decisions	: 3614616
c propagations	: 3772001
c inspects	: 362937
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 244
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 239.355
c starts	: 245
c conflicts	: 0
c decisions	: 3629430
c propagations	: 3787460
c inspects	: 364328
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 245
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 240.117
c starts	: 246
c conflicts	: 0
c decisions	: 3644244
c propagations	: 3802919
c inspects	: 365719
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 246
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 240.887
c starts	: 247
c conflicts	: 0
c decisions	: 3659058
c propagations	: 3818378
c inspects	: 367110
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 247
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 241.961
c starts	: 248
c conflicts	: 0
c decisions	: 3673872
c propagations	: 3833837
c inspects	: 368501
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 248
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 242.73
c starts	: 249
c conflicts	: 0
c decisions	: 3688686
c propagations	: 3849296
c inspects	: 369892
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 249
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 243.506
c starts	: 250
c conflicts	: 0
c decisions	: 3703500
c propagations	: 3864755
c inspects	: 371283
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 250
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 244.246
c starts	: 251
c conflicts	: 0
c decisions	: 3718314
c propagations	: 3880214
c inspects	: 372621
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 251
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 244.987
c starts	: 252
c conflicts	: 0
c decisions	: 3733128
c propagations	: 3895673
c inspects	: 373961
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 252
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 246.105
c starts	: 253
c conflicts	: 0
c decisions	: 3747942
c propagations	: 3911132
c inspects	: 375352
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 253
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 246.891
c starts	: 254
c conflicts	: 0
c decisions	: 3762756
c propagations	: 3926591
c inspects	: 376743
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 254
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 247.67
c starts	: 255
c conflicts	: 0
c decisions	: 3777570
c propagations	: 3942050
c inspects	: 378134
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 255
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 248.454
c starts	: 256
c conflicts	: 0
c decisions	: 3792384
c propagations	: 3957509
c inspects	: 379525
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 256
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 249.816
c starts	: 257
c conflicts	: 0
c decisions	: 3807198
c propagations	: 3972968
c inspects	: 380916
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 257
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 250.604
c starts	: 258
c conflicts	: 0
c decisions	: 3822012
c propagations	: 3988427
c inspects	: 382307
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 258
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 251.864
c starts	: 259
c conflicts	: 0
c decisions	: 3836826
c propagations	: 4003886
c inspects	: 383698
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 259
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 252.666
c starts	: 260
c conflicts	: 0
c decisions	: 3851640
c propagations	: 4019345
c inspects	: 385089
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 260
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 253.419
c starts	: 261
c conflicts	: 0
c decisions	: 3866454
c propagations	: 4034804
c inspects	: 386427
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 261
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 254.218
c starts	: 262
c conflicts	: 0
c decisions	: 3881268
c propagations	: 4050263
c inspects	: 387818
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 262
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 254.981
c starts	: 263
c conflicts	: 0
c decisions	: 3896082
c propagations	: 4065722
c inspects	: 389162
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 263
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 255.97
c starts	: 264
c conflicts	: 0
c decisions	: 3910896
c propagations	: 4081181
c inspects	: 390500
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 264
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 256.774
c starts	: 265
c conflicts	: 0
c decisions	: 3925710
c propagations	: 4096640
c inspects	: 391891
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 265
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 257.579
c starts	: 266
c conflicts	: 0
c decisions	: 3940524
c propagations	: 4112099
c inspects	: 393282
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 266
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 258.384
c starts	: 267
c conflicts	: 0
c decisions	: 3955338
c propagations	: 4127558
c inspects	: 394673
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 267
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 259.579
c starts	: 268
c conflicts	: 0
c decisions	: 3970152
c propagations	: 4143017
c inspects	: 396064
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 268
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 260.387
c starts	: 269
c conflicts	: 0
c decisions	: 3984966
c propagations	: 4158476
c inspects	: 397455
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 269
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 261.199
c starts	: 270
c conflicts	: 0
c decisions	: 3999780
c propagations	: 4173935
c inspects	: 398846
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 270
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 262.014
c starts	: 271
c conflicts	: 0
c decisions	: 4014594
c propagations	: 4189394
c inspects	: 400237
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 271
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 262.834
c starts	: 272
c conflicts	: 0
c decisions	: 4029408
c propagations	: 4204853
c inspects	: 401628
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 272
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 263.914
c starts	: 273
c conflicts	: 0
c decisions	: 4044222
c propagations	: 4220312
c inspects	: 402966
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 273
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 264.738
c starts	: 274
c conflicts	: 0
c decisions	: 4059036
c propagations	: 4235771
c inspects	: 404357
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 274
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 265.513
c starts	: 275
c conflicts	: 0
c decisions	: 4073850
c propagations	: 4251230
c inspects	: 405685
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 275
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 266.332
c starts	: 276
c conflicts	: 0
c decisions	: 4088664
c propagations	: 4266689
c inspects	: 407076
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 276
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 267.154
c starts	: 277
c conflicts	: 0
c decisions	: 4103478
c propagations	: 4282148
c inspects	: 408467
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 277
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 268.297
c starts	: 278
c conflicts	: 0
c decisions	: 4118292
c propagations	: 4297607
c inspects	: 409858
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 278
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 269.123
c starts	: 279
c conflicts	: 0
c decisions	: 4133106
c propagations	: 4313066
c inspects	: 411249
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 279
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 269.949
c starts	: 280
c conflicts	: 0
c decisions	: 4147920
c propagations	: 4328525
c inspects	: 412640
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 280
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 270.786
c starts	: 281
c conflicts	: 0
c decisions	: 4162734
c propagations	: 4343984
c inspects	: 414031
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 281
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 271.574
c starts	: 282
c conflicts	: 0
c decisions	: 4177548
c propagations	: 4359443
c inspects	: 415341
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 282
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 272.75
c starts	: 283
c conflicts	: 0
c decisions	: 4192362
c propagations	: 4374902
c inspects	: 416732
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 283
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 273.549
c starts	: 284
c conflicts	: 0
c decisions	: 4207176
c propagations	: 4390361
c inspects	: 418071
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 284
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 274.385
c starts	: 285
c conflicts	: 0
c decisions	: 4221990
c propagations	: 4405820
c inspects	: 419462
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 285
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 275.227
c starts	: 286
c conflicts	: 0
c decisions	: 4236804
c propagations	: 4421279
c inspects	: 420853
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 286
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 276.025
c starts	: 287
c conflicts	: 0
c decisions	: 4251618
c propagations	: 4436738
c inspects	: 422192
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 287
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 277.211
c starts	: 288
c conflicts	: 0
c decisions	: 4266432
c propagations	: 4452197
c inspects	: 423583
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 288
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 278.02
c starts	: 289
c conflicts	: 0
c decisions	: 4281246
c propagations	: 4467656
c inspects	: 424921
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 289
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 278.871
c starts	: 290
c conflicts	: 0
c decisions	: 4296060
c propagations	: 4483115
c inspects	: 426312
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 290
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 279.72
c starts	: 291
c conflicts	: 0
c decisions	: 4310874
c propagations	: 4498574
c inspects	: 427703
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 291
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 280.917
c starts	: 292
c conflicts	: 0
c decisions	: 4325688
c propagations	: 4514033
c inspects	: 429094
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 292
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 281.769
c starts	: 293
c conflicts	: 0
c decisions	: 4340502
c propagations	: 4529492
c inspects	: 430485
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 293
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 282.62
c starts	: 294
c conflicts	: 0
c decisions	: 4355316
c propagations	: 4544951
c inspects	: 431876
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 294
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 283.474
c starts	: 295
c conflicts	: 0
c decisions	: 4370130
c propagations	: 4560410
c inspects	: 433267
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 295
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 284.331
c starts	: 296
c conflicts	: 0
c decisions	: 4384944
c propagations	: 4575869
c inspects	: 434658
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 296
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 285.497
c starts	: 297
c conflicts	: 0
c decisions	: 4399758
c propagations	: 4591328
c inspects	: 436049
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 297
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 286.357
c starts	: 298
c conflicts	: 0
c decisions	: 4414572
c propagations	: 4606787
c inspects	: 437440
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 298
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 287.215
c starts	: 299
c conflicts	: 0
c decisions	: 4429386
c propagations	: 4622246
c inspects	: 438831
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 299
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 288.077
c starts	: 300
c conflicts	: 0
c decisions	: 4444200
c propagations	: 4637705
c inspects	: 440222
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 300
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 289.258
c starts	: 301
c conflicts	: 0
c decisions	: 4459014
c propagations	: 4653164
c inspects	: 441613
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 301
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 290.126
c starts	: 302
c conflicts	: 0
c decisions	: 4473828
c propagations	: 4668623
c inspects	: 443004
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 302
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 290.994
c starts	: 303
c conflicts	: 0
c decisions	: 4488642
c propagations	: 4684082
c inspects	: 444395
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 303
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 291.864
c starts	: 304
c conflicts	: 0
c decisions	: 4503456
c propagations	: 4699541
c inspects	: 445786
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 304
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 292.742
c starts	: 305
c conflicts	: 0
c decisions	: 4518270
c propagations	: 4715000
c inspects	: 447177
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 305
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 293.908
c starts	: 306
c conflicts	: 0
c decisions	: 4533084
c propagations	: 4730459
c inspects	: 448524
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 306
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 294.785
c starts	: 307
c conflicts	: 0
c decisions	: 4547898
c propagations	: 4745918
c inspects	: 449915
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 307
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 295.66
c starts	: 308
c conflicts	: 0
c decisions	: 4562712
c propagations	: 4761377
c inspects	: 451306
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 308
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 296.537
c starts	: 309
c conflicts	: 0
c decisions	: 4577526
c propagations	: 4776836
c inspects	: 452697
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 309
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 297.411
c starts	: 310
c conflicts	: 0
c decisions	: 4592340
c propagations	: 4792295
c inspects	: 454088
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 310
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 298.616
c starts	: 311
c conflicts	: 0
c decisions	: 4607154
c propagations	: 4807754
c inspects	: 455479
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 311
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 299.508
c starts	: 312
c conflicts	: 0
c decisions	: 4621968
c propagations	: 4823213
c inspects	: 456870
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 312
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 300.355
c starts	: 313
c conflicts	: 0
c decisions	: 4636782
c propagations	: 4838672
c inspects	: 458208
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 313
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 301.244
c starts	: 314
c conflicts	: 0
c decisions	: 4651596
c propagations	: 4854131
c inspects	: 459599
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 314
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 302.458
c starts	: 315
c conflicts	: 0
c decisions	: 4666410
c propagations	: 4869590
c inspects	: 460990
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 315
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 303.355
c starts	: 316
c conflicts	: 0
c decisions	: 4681224
c propagations	: 4885049
c inspects	: 462381
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 316
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 304.212
c starts	: 317
c conflicts	: 0
c decisions	: 4696038
c propagations	: 4900508
c inspects	: 463719
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 317
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 305.096
c starts	: 318
c conflicts	: 0
c decisions	: 4710852
c propagations	: 4915967
c inspects	: 465110
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 318
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 305.979
c starts	: 319
c conflicts	: 0
c decisions	: 4725666
c propagations	: 4931426
c inspects	: 466501
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 319
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 307.192
c starts	: 320
c conflicts	: 0
c decisions	: 4740480
c propagations	: 4946885
c inspects	: 467892
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 320
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 308.084
c starts	: 321
c conflicts	: 0
c decisions	: 4755294
c propagations	: 4962344
c inspects	: 469283
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 321
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 308.97
c starts	: 322
c conflicts	: 0
c decisions	: 4770108
c propagations	: 4977803
c inspects	: 470674
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 322
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 309.862
c starts	: 323
c conflicts	: 0
c decisions	: 4784922
c propagations	: 4993262
c inspects	: 472065
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 323
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 310.763
c starts	: 324
c conflicts	: 0
c decisions	: 4799736
c propagations	: 5008721
c inspects	: 473456
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 324
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 311.986
c starts	: 325
c conflicts	: 0
c decisions	: 4814550
c propagations	: 5024180
c inspects	: 474847
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 325
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 312.888
c starts	: 326
c conflicts	: 0
c decisions	: 4829364
c propagations	: 5039639
c inspects	: 476238
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 326
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 313.786
c starts	: 327
c conflicts	: 0
c decisions	: 4844178
c propagations	: 5055098
c inspects	: 477629
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 327
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 314.682
c starts	: 328
c conflicts	: 0
c decisions	: 4858992
c propagations	: 5070557
c inspects	: 479020
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 328
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 315.935
c starts	: 329
c conflicts	: 0
c decisions	: 4873806
c propagations	: 5086016
c inspects	: 480411
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 329
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 316.815
c starts	: 330
c conflicts	: 0
c decisions	: 4888620
c propagations	: 5101475
c inspects	: 481749
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 330
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 317.736
c starts	: 331
c conflicts	: 0
c decisions	: 4903434
c propagations	: 5116934
c inspects	: 483140
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 331
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 318.653
c starts	: 332
c conflicts	: 0
c decisions	: 4918248
c propagations	: 5132393
c inspects	: 484531
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 332
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 319.573
c starts	: 333
c conflicts	: 0
c decisions	: 4933062
c propagations	: 5147852
c inspects	: 485922
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 333
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 320.804
c starts	: 334
c conflicts	: 0
c decisions	: 4947876
c propagations	: 5163311
c inspects	: 487313
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 334
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 321.722
c starts	: 335
c conflicts	: 0
c decisions	: 4962690
c propagations	: 5178770
c inspects	: 488704
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 335
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 322.647
c starts	: 336
c conflicts	: 0
c decisions	: 4977504
c propagations	: 5194229
c inspects	: 490095
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 336
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 323.572
c starts	: 337
c conflicts	: 0
c decisions	: 4992318
c propagations	: 5209688
c inspects	: 491486
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 337
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 324.49
c starts	: 338
c conflicts	: 0
c decisions	: 5007132
c propagations	: 5225147
c inspects	: 492877
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 338
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 325.743
c starts	: 339
c conflicts	: 0
c decisions	: 5021946
c propagations	: 5240606
c inspects	: 494268
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 339
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 326.666
c starts	: 340
c conflicts	: 0
c decisions	: 5036760
c propagations	: 5256065
c inspects	: 495659
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 340
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 327.594
c starts	: 341
c conflicts	: 0
c decisions	: 5051574
c propagations	: 5271524
c inspects	: 497050
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 341
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 328.526
c starts	: 342
c conflicts	: 0
c decisions	: 5066388
c propagations	: 5286983
c inspects	: 498441
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 342
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 329.777
c starts	: 343
c conflicts	: 0
c decisions	: 5081202
c propagations	: 5302442
c inspects	: 499832
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 343
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 330.708
c starts	: 344
c conflicts	: 0
c decisions	: 5096016
c propagations	: 5317901
c inspects	: 501223
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 344
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 331.639
c starts	: 345
c conflicts	: 0
c decisions	: 5110830
c propagations	: 5333360
c inspects	: 502614
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 345
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 332.573
c starts	: 346
c conflicts	: 0
c decisions	: 5125644
c propagations	: 5348819
c inspects	: 504005
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 346
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 333.509
c starts	: 347
c conflicts	: 0
c decisions	: 5140458
c propagations	: 5364278
c inspects	: 505396
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 347
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 334.773
c starts	: 348
c conflicts	: 0
c decisions	: 5155272
c propagations	: 5379737
c inspects	: 506787
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 348
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 335.673
c starts	: 349
c conflicts	: 0
c decisions	: 5170086
c propagations	: 5395196
c inspects	: 508125
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 349
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 336.613
c starts	: 350
c conflicts	: 0
c decisions	: 5184900
c propagations	: 5410655
c inspects	: 509516
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 350
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 337.553
c starts	: 351
c conflicts	: 0
c decisions	: 5199714
c propagations	: 5426114
c inspects	: 510907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 351
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 338.834
c starts	: 352
c conflicts	: 0
c decisions	: 5214528
c propagations	: 5441573
c inspects	: 512298
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 352
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 339.779
c starts	: 353
c conflicts	: 0
c decisions	: 5229342
c propagations	: 5457032
c inspects	: 513689
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 353
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 340.728
c starts	: 354
c conflicts	: 0
c decisions	: 5244156
c propagations	: 5472491
c inspects	: 515080
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 354
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 341.674
c starts	: 355
c conflicts	: 0
c decisions	: 5258970
c propagations	: 5487950
c inspects	: 516471
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 355
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 342.625
c starts	: 356
c conflicts	: 0
c decisions	: 5273784
c propagations	: 5503409
c inspects	: 517862
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 356
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 343.89
c starts	: 357
c conflicts	: 0
c decisions	: 5288598
c propagations	: 5518868
c inspects	: 519253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 357
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 344.808
c starts	: 358
c conflicts	: 0
c decisions	: 5303412
c propagations	: 5534327
c inspects	: 520594
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 358
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 345.76
c starts	: 359
c conflicts	: 0
c decisions	: 5318226
c propagations	: 5549786
c inspects	: 521985
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 359
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 346.717
c starts	: 360
c conflicts	: 0
c decisions	: 5333040
c propagations	: 5565245
c inspects	: 523376
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 360
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 347.673
c starts	: 361
c conflicts	: 0
c decisions	: 5347854
c propagations	: 5580704
c inspects	: 524767
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 361
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 348.976
c starts	: 362
c conflicts	: 0
c decisions	: 5362668
c propagations	: 5596163
c inspects	: 526158
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 362
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 349.942
c starts	: 363
c conflicts	: 0
c decisions	: 5377482
c propagations	: 5611622
c inspects	: 527549
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 363
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 350.91
c starts	: 364
c conflicts	: 0
c decisions	: 5392296
c propagations	: 5627081
c inspects	: 528940
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 364
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 351.874
c starts	: 365
c conflicts	: 0
c decisions	: 5407110
c propagations	: 5642540
c inspects	: 530331
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 365
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 353.192
c starts	: 366
c conflicts	: 0
c decisions	: 5421924
c propagations	: 5657999
c inspects	: 531722
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 366
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 354.172
c starts	: 367
c conflicts	: 0
c decisions	: 5436738
c propagations	: 5673458
c inspects	: 533113
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 367
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 355.143
c starts	: 368
c conflicts	: 0
c decisions	: 5451552
c propagations	: 5688917
c inspects	: 534504
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 368
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 356.116
c starts	: 369
c conflicts	: 0
c decisions	: 5466366
c propagations	: 5704376
c inspects	: 535895
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 369
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 357.094
c starts	: 370
c conflicts	: 0
c decisions	: 5481180
c propagations	: 5719835
c inspects	: 537286
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 370
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 358.392
c starts	: 371
c conflicts	: 0
c decisions	: 5495994
c propagations	: 5735294
c inspects	: 538677
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 371
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 359.338
c starts	: 372
c conflicts	: 0
c decisions	: 5510808
c propagations	: 5750753
c inspects	: 540016
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 372
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 360.321
c starts	: 373
c conflicts	: 0
c decisions	: 5525622
c propagations	: 5766212
c inspects	: 541407
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 373
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 361.302
c starts	: 374
c conflicts	: 0
c decisions	: 5540436
c propagations	: 5781671
c inspects	: 542798
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 374
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 362.292
c starts	: 375
c conflicts	: 0
c decisions	: 5555250
c propagations	: 5797130
c inspects	: 544189
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 375
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 363.625
c starts	: 376
c conflicts	: 0
c decisions	: 5570064
c propagations	: 5812589
c inspects	: 545580
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 376
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 364.58
c starts	: 377
c conflicts	: 0
c decisions	: 5584878
c propagations	: 5828048
c inspects	: 546918
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 377
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 365.572
c starts	: 378
c conflicts	: 0
c decisions	: 5599692
c propagations	: 5843507
c inspects	: 548309
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 378
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 366.566
c starts	: 379
c conflicts	: 0
c decisions	: 5614506
c propagations	: 5858966
c inspects	: 549700
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 379
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 367.907
c starts	: 380
c conflicts	: 0
c decisions	: 5629320
c propagations	: 5874425
c inspects	: 551091
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 380
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 368.909
c starts	: 381
c conflicts	: 0
c decisions	: 5644134
c propagations	: 5889884
c inspects	: 552482
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 381
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 369.872
c starts	: 382
c conflicts	: 0
c decisions	: 5658948
c propagations	: 5905343
c inspects	: 553820
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 382
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 370.876
c starts	: 383
c conflicts	: 0
c decisions	: 5673762
c propagations	: 5920802
c inspects	: 555211
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 383
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 371.839
c starts	: 384
c conflicts	: 0
c decisions	: 5688576
c propagations	: 5936261
c inspects	: 556552
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 384
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 373.174
c starts	: 385
c conflicts	: 0
c decisions	: 5703390
c propagations	: 5951720
c inspects	: 557943
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 385
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 374.206
c starts	: 386
c conflicts	: 0
c decisions	: 5718204
c propagations	: 5967179
c inspects	: 559334
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 386
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 375.209
c starts	: 387
c conflicts	: 0
c decisions	: 5733018
c propagations	: 5982638
c inspects	: 560725
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 387
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 376.223
c starts	: 388
c conflicts	: 0
c decisions	: 5747832
c propagations	: 5998097
c inspects	: 562116
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 388
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 377.204
c starts	: 389
c conflicts	: 0
c decisions	: 5762646
c propagations	: 6013556
c inspects	: 563454
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 389
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 378.614
c starts	: 390
c conflicts	: 0
c decisions	: 5777460
c propagations	: 6029015
c inspects	: 564845
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 390
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 379.629
c starts	: 391
c conflicts	: 0
c decisions	: 5792274
c propagations	: 6044474
c inspects	: 566236
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 391
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 380.64
c starts	: 392
c conflicts	: 0
c decisions	: 5807088
c propagations	: 6059933
c inspects	: 567627
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 392
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 381.655
c starts	: 393
c conflicts	: 0
c decisions	: 5821902
c propagations	: 6075392
c inspects	: 569018
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 393
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 382.973
c starts	: 394
c conflicts	: 0
c decisions	: 5836716
c propagations	: 6090851
c inspects	: 570409
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 394
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 383.992
c starts	: 395
c conflicts	: 0
c decisions	: 5851530
c propagations	: 6106310
c inspects	: 571800
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 395
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 385.011
c starts	: 396
c conflicts	: 0
c decisions	: 5866344
c propagations	: 6121769
c inspects	: 573191
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 396
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 386.032
c starts	: 397
c conflicts	: 0
c decisions	: 5881158
c propagations	: 6137228
c inspects	: 574582
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 397
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 387.055
c starts	: 398
c conflicts	: 0
c decisions	: 5895972
c propagations	: 6152687
c inspects	: 575973
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 398
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 388.393
c starts	: 399
c conflicts	: 0
c decisions	: 5910786
c propagations	: 6168146
c inspects	: 577364
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 399
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 389.422
c starts	: 400
c conflicts	: 0
c decisions	: 5925600
c propagations	: 6183605
c inspects	: 578755
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 400
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 390.45
c starts	: 401
c conflicts	: 0
c decisions	: 5940414
c propagations	: 6199064
c inspects	: 580146
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 401
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 391.479
c starts	: 402
c conflicts	: 0
c decisions	: 5955228
c propagations	: 6214523
c inspects	: 581537
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 402
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 392.855
c starts	: 403
c conflicts	: 0
c decisions	: 5970042
c propagations	: 6229982
c inspects	: 582928
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 403
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 393.888
c starts	: 404
c conflicts	: 0
c decisions	: 5984856
c propagations	: 6245441
c inspects	: 584319
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 404
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 394.94
c starts	: 405
c conflicts	: 0
c decisions	: 5999670
c propagations	: 6260900
c inspects	: 585710
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 405
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 395.987
c starts	: 406
c conflicts	: 0
c decisions	: 6014484
c propagations	: 6276359
c inspects	: 587101
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 406
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 397.038
c starts	: 407
c conflicts	: 0
c decisions	: 6029298
c propagations	: 6291818
c inspects	: 588492
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 407
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 398.402
c starts	: 408
c conflicts	: 0
c decisions	: 6044112
c propagations	: 6307277
c inspects	: 589883
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 408
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 399.452
c starts	: 409
c conflicts	: 0
c decisions	: 6058926
c propagations	: 6322736
c inspects	: 591274
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 409
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 400.472
c starts	: 410
c conflicts	: 0
c decisions	: 6073740
c propagations	: 6338195
c inspects	: 592614
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 410
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 401.489
c starts	: 411
c conflicts	: 0
c decisions	: 6088554
c propagations	: 6353654
c inspects	: 593952
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 411
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 402.548
c starts	: 412
c conflicts	: 0
c decisions	: 6103368
c propagations	: 6369113
c inspects	: 595343
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 412
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 403.941
c starts	: 413
c conflicts	: 0
c decisions	: 6118182
c propagations	: 6384572
c inspects	: 596734
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 413
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 405.003
c starts	: 414
c conflicts	: 0
c decisions	: 6132996
c propagations	: 6400031
c inspects	: 598125
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 414
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 406.069
c starts	: 415
c conflicts	: 0
c decisions	: 6147810
c propagations	: 6415490
c inspects	: 599516
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 415
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 407.131
c starts	: 416
c conflicts	: 0
c decisions	: 6162624
c propagations	: 6430949
c inspects	: 600907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 416
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 408.529
c starts	: 417
c conflicts	: 0
c decisions	: 6177438
c propagations	: 6446408
c inspects	: 602298
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 417
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 409.601
c starts	: 418
c conflicts	: 0
c decisions	: 6192252
c propagations	: 6461867
c inspects	: 603689
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 418
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 410.668
c starts	: 419
c conflicts	: 0
c decisions	: 6207066
c propagations	: 6477326
c inspects	: 605080
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 419
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 411.742
c starts	: 420
c conflicts	: 0
c decisions	: 6221880
c propagations	: 6492785
c inspects	: 606471
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 420
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 412.817
c starts	: 421
c conflicts	: 0
c decisions	: 6236694
c propagations	: 6508244
c inspects	: 607862
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 421
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 414.207
c starts	: 422
c conflicts	: 0
c decisions	: 6251508
c propagations	: 6523703
c inspects	: 609253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 422
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 415.288
c starts	: 423
c conflicts	: 0
c decisions	: 6266322
c propagations	: 6539162
c inspects	: 610644
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 423
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 416.368
c starts	: 424
c conflicts	: 0
c decisions	: 6281136
c propagations	: 6554621
c inspects	: 612035
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 424
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 417.452
c starts	: 425
c conflicts	: 0
c decisions	: 6295950
c propagations	: 6570080
c inspects	: 613426
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 425
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 418.864
c starts	: 426
c conflicts	: 0
c decisions	: 6310764
c propagations	: 6585539
c inspects	: 614817
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 426
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 419.956
c starts	: 427
c conflicts	: 0
c decisions	: 6325578
c propagations	: 6600998
c inspects	: 616208
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 427
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 421.044
c starts	: 428
c conflicts	: 0
c decisions	: 6340392
c propagations	: 6616457
c inspects	: 617599
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 428
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 422.136
c starts	: 429
c conflicts	: 0
c decisions	: 6355206
c propagations	: 6631916
c inspects	: 618990
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 429
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 423.22
c starts	: 430
c conflicts	: 0
c decisions	: 6370020
c propagations	: 6647375
c inspects	: 620381
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 430
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 424.585
c starts	: 431
c conflicts	: 0
c decisions	: 6384834
c propagations	: 6662834
c inspects	: 621721
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 431
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 425.642
c starts	: 432
c conflicts	: 0
c decisions	: 6399648
c propagations	: 6678293
c inspects	: 623059
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 432
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 426.739
c starts	: 433
c conflicts	: 0
c decisions	: 6414462
c propagations	: 6693752
c inspects	: 624450
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 433
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 427.835
c starts	: 434
c conflicts	: 0
c decisions	: 6429276
c propagations	: 6709211
c inspects	: 625841
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 434
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 428.938
c starts	: 435
c conflicts	: 0
c decisions	: 6444090
c propagations	: 6724670
c inspects	: 627232
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 435
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 430.376
c starts	: 436
c conflicts	: 0
c decisions	: 6458904
c propagations	: 6740129
c inspects	: 628623
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 436
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 431.483
c starts	: 437
c conflicts	: 0
c decisions	: 6473718
c propagations	: 6755588
c inspects	: 630014
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 437
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 432.581
c starts	: 438
c conflicts	: 0
c decisions	: 6488532
c propagations	: 6771047
c inspects	: 631405
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 438
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 433.674
c starts	: 439
c conflicts	: 0
c decisions	: 6503346
c propagations	: 6786506
c inspects	: 632796
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 439
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 451.551
c starts	: 440
c conflicts	: 0
c decisions	: 6518160
c propagations	: 6801965
c inspects	: 634187
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 440
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 452.666
c starts	: 441
c conflicts	: 0
c decisions	: 6532974
c propagations	: 6817424
c inspects	: 635578
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 441
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 453.776
c starts	: 442
c conflicts	: 0
c decisions	: 6547788
c propagations	: 6832883
c inspects	: 636969
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 442
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 454.889
c starts	: 443
c conflicts	: 0
c decisions	: 6562602
c propagations	: 6848342
c inspects	: 638360
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 443
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 456.003
c starts	: 444
c conflicts	: 0
c decisions	: 6577416
c propagations	: 6863801
c inspects	: 639751
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 444
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 457.299
c starts	: 445
c conflicts	: 0
c decisions	: 6592230
c propagations	: 6879260
c inspects	: 641142
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 445
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 458.421
c starts	: 446
c conflicts	: 0
c decisions	: 6607044
c propagations	: 6894719
c inspects	: 642533
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 446
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 459.54
c starts	: 447
c conflicts	: 0
c decisions	: 6621858
c propagations	: 6910178
c inspects	: 643924
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 447
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 460.658
c starts	: 448
c conflicts	: 0
c decisions	: 6636672
c propagations	: 6925637
c inspects	: 645315
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 448
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 462.087
c starts	: 449
c conflicts	: 0
c decisions	: 6651486
c propagations	: 6941096
c inspects	: 646706
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 449
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 463.201
c starts	: 450
c conflicts	: 0
c decisions	: 6666300
c propagations	: 6956555
c inspects	: 648097
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 450
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 464.319
c starts	: 451
c conflicts	: 0
c decisions	: 6681114
c propagations	: 6972014
c inspects	: 649488
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 451
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 465.438
c starts	: 452
c conflicts	: 0
c decisions	: 6695928
c propagations	: 6987473
c inspects	: 650879
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 452
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 466.53
c starts	: 453
c conflicts	: 0
c decisions	: 6710742
c propagations	: 7002932
c inspects	: 652217
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 453
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 467.988
c starts	: 454
c conflicts	: 0
c decisions	: 6725556
c propagations	: 7018391
c inspects	: 653608
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 454
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 469.086
c starts	: 455
c conflicts	: 0
c decisions	: 6740370
c propagations	: 7033850
c inspects	: 654945
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 455
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 470.223
c starts	: 456
c conflicts	: 0
c decisions	: 6755184
c propagations	: 7049309
c inspects	: 656336
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 456
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 471.361
c starts	: 457
c conflicts	: 0
c decisions	: 6769998
c propagations	: 7064768
c inspects	: 657727
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 457
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 472.5
c starts	: 458
c conflicts	: 0
c decisions	: 6784812
c propagations	: 7080227
c inspects	: 659118
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 458
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 487.007
c starts	: 459
c conflicts	: 0
c decisions	: 6799626
c propagations	: 7095686
c inspects	: 660509
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 459
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 488.154
c starts	: 460
c conflicts	: 0
c decisions	: 6814440
c propagations	: 7111145
c inspects	: 661900
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 460
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 489.298
c starts	: 461
c conflicts	: 0
c decisions	: 6829254
c propagations	: 7126604
c inspects	: 663291
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 461
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 490.446
c starts	: 462
c conflicts	: 0
c decisions	: 6844068
c propagations	: 7142063
c inspects	: 664682
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 462
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 505.071
c starts	: 463
c conflicts	: 0
c decisions	: 6858882
c propagations	: 7157522
c inspects	: 666073
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 463
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 506.22
c starts	: 464
c conflicts	: 0
c decisions	: 6873696
c propagations	: 7172981
c inspects	: 667464
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 464
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 507.373
c starts	: 465
c conflicts	: 0
c decisions	: 6888510
c propagations	: 7188440
c inspects	: 668855
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 465
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 508.528
c starts	: 466
c conflicts	: 0
c decisions	: 6903324
c propagations	: 7203899
c inspects	: 670246
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 466
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 509.68
c starts	: 467
c conflicts	: 0
c decisions	: 6918138
c propagations	: 7219358
c inspects	: 671637
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 467
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 530.512
c starts	: 468
c conflicts	: 0
c decisions	: 6932952
c propagations	: 7234817
c inspects	: 673028
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 468
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 531.673
c starts	: 469
c conflicts	: 0
c decisions	: 6947766
c propagations	: 7250276
c inspects	: 674419
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 469
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 532.835
c starts	: 470
c conflicts	: 0
c decisions	: 6962580
c propagations	: 7265735
c inspects	: 675810
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 470
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 534.0
c starts	: 471
c conflicts	: 0
c decisions	: 6977394
c propagations	: 7281194
c inspects	: 677201
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 471
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 548.763
c starts	: 472
c conflicts	: 0
c decisions	: 6992208
c propagations	: 7296653
c inspects	: 678592
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 472
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 549.936
c starts	: 473
c conflicts	: 0
c decisions	: 7007022
c propagations	: 7312112
c inspects	: 679983
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 473
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 551.107
c starts	: 474
c conflicts	: 0
c decisions	: 7021836
c propagations	: 7327571
c inspects	: 681374
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 474
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 552.278
c starts	: 475
c conflicts	: 0
c decisions	: 7036650
c propagations	: 7343030
c inspects	: 682765
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 475
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 553.45
c starts	: 476
c conflicts	: 0
c decisions	: 7051464
c propagations	: 7358489
c inspects	: 684156
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 476
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 568.306
c starts	: 477
c conflicts	: 0
c decisions	: 7066278
c propagations	: 7373948
c inspects	: 685496
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 477
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 569.485
c starts	: 478
c conflicts	: 0
c decisions	: 7081092
c propagations	: 7389407
c inspects	: 686887
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 478
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 570.665
c starts	: 479
c conflicts	: 0
c decisions	: 7095906
c propagations	: 7404866
c inspects	: 688278
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 479
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 571.843
c starts	: 480
c conflicts	: 0
c decisions	: 7110720
c propagations	: 7420325
c inspects	: 689669
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 480
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 573.022
c starts	: 481
c conflicts	: 0
c decisions	: 7125534
c propagations	: 7435784
c inspects	: 691060
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 481
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 588.058
c starts	: 482
c conflicts	: 0
c decisions	: 7140348
c propagations	: 7451243
c inspects	: 692451
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 482
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 589.247
c starts	: 483
c conflicts	: 0
c decisions	: 7155162
c propagations	: 7466702
c inspects	: 693842
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 483
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 590.437
c starts	: 484
c conflicts	: 0
c decisions	: 7169976
c propagations	: 7482161
c inspects	: 695233
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 484
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 591.587
c starts	: 485
c conflicts	: 0
c decisions	: 7184790
c propagations	: 7497620
c inspects	: 696579
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 485
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 606.972
c starts	: 486
c conflicts	: 0
c decisions	: 7199604
c propagations	: 7513079
c inspects	: 697970
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 486
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 608.167
c starts	: 487
c conflicts	: 0
c decisions	: 7214418
c propagations	: 7528538
c inspects	: 699361
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 487
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 609.363
c starts	: 488
c conflicts	: 0
c decisions	: 7229232
c propagations	: 7543997
c inspects	: 700752
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 488
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 610.561
c starts	: 489
c conflicts	: 0
c decisions	: 7244046
c propagations	: 7559456
c inspects	: 702143
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 489
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 611.757
c starts	: 490
c conflicts	: 0
c decisions	: 7258860
c propagations	: 7574915
c inspects	: 703534
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 490
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 627.217
c starts	: 491
c conflicts	: 0
c decisions	: 7273674
c propagations	: 7590374
c inspects	: 704925
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 491
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 628.424
c starts	: 492
c conflicts	: 0
c decisions	: 7288488
c propagations	: 7605833
c inspects	: 706316
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 492
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 629.588
c starts	: 493
c conflicts	: 0
c decisions	: 7303302
c propagations	: 7621292
c inspects	: 707654
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 493
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 630.79
c starts	: 494
c conflicts	: 0
c decisions	: 7318116
c propagations	: 7636751
c inspects	: 709045
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 494
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 631.993
c starts	: 495
c conflicts	: 0
c decisions	: 7332930
c propagations	: 7652210
c inspects	: 710436
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 495
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 647.583
c starts	: 496
c conflicts	: 0
c decisions	: 7347744
c propagations	: 7667669
c inspects	: 711827
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 496
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 648.795
c starts	: 497
c conflicts	: 0
c decisions	: 7362558
c propagations	: 7683128
c inspects	: 713218
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 497
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 650.005
c starts	: 498
c conflicts	: 0
c decisions	: 7377372
c propagations	: 7698587
c inspects	: 714609
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 498
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 651.223
c starts	: 499
c conflicts	: 0
c decisions	: 7392186
c propagations	: 7714046
c inspects	: 716000
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 499
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 666.923
c starts	: 500
c conflicts	: 0
c decisions	: 7407000
c propagations	: 7729505
c inspects	: 717338
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 500
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 668.139
c starts	: 501
c conflicts	: 0
c decisions	: 7421814
c propagations	: 7744964
c inspects	: 718729
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 501
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 669.356
c starts	: 502
c conflicts	: 0
c decisions	: 7436628
c propagations	: 7760423
c inspects	: 720120
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 502
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 670.574
c starts	: 503
c conflicts	: 0
c decisions	: 7451442
c propagations	: 7775882
c inspects	: 721511
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 503
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 671.793
c starts	: 504
c conflicts	: 0
c decisions	: 7466256
c propagations	: 7791341
c inspects	: 722902
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 504
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 687.846
c starts	: 505
c conflicts	: 0
c decisions	: 7481070
c propagations	: 7806800
c inspects	: 724293
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 505
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 689.071
c starts	: 506
c conflicts	: 0
c decisions	: 7495884
c propagations	: 7822259
c inspects	: 725684
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 506
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 690.293
c starts	: 507
c conflicts	: 0
c decisions	: 7510698
c propagations	: 7837718
c inspects	: 727075
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 507
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 691.519
c starts	: 508
c conflicts	: 0
c decisions	: 7525512
c propagations	: 7853177
c inspects	: 728466
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 508
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 692.743
c starts	: 509
c conflicts	: 0
c decisions	: 7540326
c propagations	: 7868636
c inspects	: 729857
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 509
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 708.673
c starts	: 510
c conflicts	: 0
c decisions	: 7555140
c propagations	: 7884095
c inspects	: 731248
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 510
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 709.908
c starts	: 511
c conflicts	: 0
c decisions	: 7569954
c propagations	: 7899554
c inspects	: 732639
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 511
c 
c CURRENT OPTIMUM=1432158208
c Current CPU time (ms) : 711.145
c starts	: 512
c conflicts	: 0
c decisions	: 7584768
c propagations	: 7915013
c inspects	: 734030
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 512
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
#### 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.79 0.93 0.90 2/54 29256
Raw data (stat): 29256 (runsolver) R 29255 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481787668 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.89 0.95 0.91 2/63 29265
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 17980 0 1 0 877 41 0 0 25 0 10 0 481787668 853471232 19175 4294967295 134512640 134569956 3221224400 3221214704 1131201629 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208367 19175 13073 16 0 208351 0
vsize: 833468
[startup+20.002 s]
Raw data (loadavg): 0.91 0.95 0.91 2/63 29265
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 17980 0 1 0 1773 41 0 0 25 0 10 0 481787668 853803008 19753 4294967295 134512640 134569956 3221224400 3221214272 1077558376 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208448 19753 13073 16 0 208432 0
vsize: 833792
[startup+30.0032 s]
Raw data (loadavg): 0.92 0.95 0.91 2/63 29265
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 17980 0 1 0 2674 41 0 0 25 0 10 0 481787668 853569536 20132 4294967295 134512640 134569956 3221224400 3221214716 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208391 20132 13073 16 0 208375 0
vsize: 833564
[startup+40.003 s]
Raw data (loadavg): 0.93 0.95 0.91 2/63 29265
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 17980 0 1 0 3603 42 0 0 25 0 10 0 481787668 853569536 20371 4294967295 134512640 134569956 3221224400 3221214716 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208391 20371 13073 16 0 208375 0
vsize: 833564
[startup+50.0042 s]
Raw data (loadavg): 0.94 0.95 0.91 2/63 29265
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 17980 0 1 0 4536 42 0 0 25 0 10 0 481787668 853569536 20491 4294967295 134512640 134569956 3221224400 3221214716 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208391 20491 13073 16 0 208375 0
vsize: 833564
[startup+60.0044 s]
Raw data (loadavg): 0.95 0.95 0.91 2/63 29265
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 17980 0 1 0 5469 42 0 0 25 0 10 0 481787668 853569536 20590 4294967295 134512640 134569956 3221224400 3221214820 1080204163 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208391 20590 13073 16 0 208375 0
vsize: 833564
[startup+70.0051 s]
Raw data (loadavg): 0.96 0.96 0.91 4/63 29265
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 17984 0 1 0 6403 42 0 0 25 0 10 0 481787668 855437312 21142 4294967295 134512640 134569956 3221224400 3221214432 1130916111 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 208847 21142 13073 16 0 208831 0
vsize: 835388
[startup+80.1273 s]
Raw data (loadavg): 1.19 1.01 0.93 2/63 29265
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 17988 0 1 0 7328 42 0 0 25 0 10 0 481787668 866037760 23831 4294967295 134512640 134569956 3221224400 3221214872 1131169782 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211435 23831 13073 16 0 211419 0
vsize: 845740
[startup+90.1277 s]
Raw data (loadavg): 1.16 1.00 0.93 2/64 29270
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18018 3 1 0 8238 45 0 0 17 0 11 0 481787668 858030080 23317 4294967295 134512640 134569956 3221224400 3221214760 1131463549 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 23317 13073 16 0 209464 0
vsize: 837920
[startup+100.127 s]
Raw data (loadavg): 1.14 1.00 0.93 2/64 29293
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18018 3 1 0 9073 46 0 0 25 0 11 0 481787668 858030080 31313 4294967295 134512640 134569956 3221224400 3221214760 1131463593 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 31313 13073 16 0 209464 0
vsize: 837920
[startup+110.129 s]
Raw data (loadavg): 1.12 1.00 0.93 2/64 29314
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18018 3 1 0 9912 47 1 0 25 0 11 0 481787668 858030080 38416 4294967295 134512640 134569956 3221224400 3221214840 1131244089 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 38416 13073 16 0 209464 0
vsize: 837920
[startup+120.129 s]
Raw data (loadavg): 1.10 1.00 0.93 2/64 29334
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18018 3 1 0 10778 48 1 0 25 0 11 0 481787668 858030080 45385 4294967295 134512640 134569956 3221224400 3221214808 1131487397 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 45385 13073 16 0 209464 0
vsize: 837920
[startup+130.129 s]
Raw data (loadavg): 1.08 1.00 0.93 2/64 29353
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18018 3 1 0 11657 49 2 0 25 0 11 0 481787668 858030080 50085 4294967295 134512640 134569956 3221224400 3221214808 1131487339 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 50085 13073 16 0 209464 0
vsize: 837920
[startup+140.13 s]
Raw data (loadavg): 1.07 1.00 0.93 2/64 29370
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18018 3 1 0 12532 50 2 1 25 0 11 0 481787668 858030080 54819 4294967295 134512640 134569956 3221224400 3221214840 1131244270 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 54819 13073 16 0 209464 0
vsize: 837920
[startup+150.13 s]
Raw data (loadavg): 1.06 1.00 0.93 2/63 29386
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18019 3 1 0 13407 51 3 1 25 0 10 0 481787668 858030080 60003 4294967295 134512640 134569956 3221224400 3221214216 1131359686 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 60003 13073 16 0 209464 0
vsize: 837920
[startup+160.13 s]
Raw data (loadavg): 1.05 1.00 0.93 2/64 29402
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18019 3 1 0 14284 51 3 1 25 0 11 0 481787668 858030080 67643 4294967295 134512640 134569956 3221224400 3221214808 1131487358 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 67643 13073 16 0 209464 0
vsize: 837920
[startup+170.13 s]
Raw data (loadavg): 1.04 1.00 0.93 2/63 29417
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18019 3 1 0 15185 52 4 1 25 0 10 0 481787668 858030080 71774 4294967295 134512640 134569956 3221224400 3221214664 1131259950 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 71774 13073 16 0 209464 0
vsize: 837920
[startup+180.13 s]
Raw data (loadavg): 1.03 1.00 0.93 2/64 29432
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18019 3 1 0 16084 54 4 2 25 0 11 0 481787668 858030080 75430 4294967295 134512640 134569956 3221224400 3221214760 1131463769 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 75430 13073 16 0 209464 0
vsize: 837920
[startup+190.131 s]
Raw data (loadavg): 1.03 1.00 0.93 2/63 29446
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18019 3 1 0 16987 55 5 2 25 0 10 0 481787668 858030080 79086 4294967295 134512640 134569956 3221224400 3221215188 1130916400 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 79086 13073 16 0 209464 0
vsize: 837920
[startup+200.131 s]
Raw data (loadavg): 1.02 1.00 0.93 2/64 29460
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18019 3 1 0 17890 55 5 2 25 0 11 0 481787668 858030080 82745 4294967295 134512640 134569956 3221224400 3221214808 1131486500 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 82745 13073 16 0 209464 0
vsize: 837920
[startup+210.132 s]
Raw data (loadavg): 1.10 1.02 0.93 2/64 29473
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 18790 56 5 2 25 0 11 0 481787668 858030080 86894 4294967295 134512640 134569956 3221224400 3221214848 1131304711 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 86894 13073 16 0 209464 0
vsize: 837920
[startup+220.132 s]
Raw data (loadavg): 1.08 1.02 0.93 2/64 29486
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 19697 57 6 3 18 0 11 0 481787668 858030080 90557 4294967295 134512640 134569956 3221224400 3221214808 1131487407 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 90557 13073 16 0 209464 0
vsize: 837920
[startup+230.132 s]
Raw data (loadavg): 1.07 1.01 0.93 2/64 29499
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 20633 58 6 3 25 0 11 0 481787668 858030080 92907 4294967295 134512640 134569956 3221224400 3221214808 1131487434 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 92907 13073 16 0 209464 0
vsize: 837920
[startup+240.133 s]
Raw data (loadavg): 1.06 1.01 0.93 2/64 29511
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 21539 59 6 3 25 0 11 0 481787668 858030080 96564 4294967295 134512640 134569956 3221224400 3221214808 1131486617 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 96564 13073 16 0 209464 0
vsize: 837920
[startup+250.15 s]
Raw data (loadavg): 1.05 1.01 0.93 2/64 29522
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 22447 59 7 3 25 0 11 0 481787668 858030080 100220 4294967295 134512640 134569956 3221224400 3221214828 1080204031 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 100220 13073 16 0 209464 0
vsize: 837920
[startup+260.171 s]
Raw data (loadavg): 1.20 1.04 0.94 2/63 29533
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 23339 60 7 3 24 0 10 0 481787668 858030080 110838 4294967295 134512640 134569956 3221224400 3221214760 1131288122 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 110838 13073 16 0 209464 0
vsize: 837920
[startup+270.171 s]
Raw data (loadavg): 1.16 1.04 0.94 2/64 29545
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 24276 60 7 3 25 0 11 0 481787668 858030080 113188 4294967295 134512640 134569956 3221224400 3221214808 1131486558 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 113188 13073 16 0 209464 0
vsize: 837920
[startup+280.172 s]
Raw data (loadavg): 1.14 1.04 0.94 2/64 29556
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 25209 61 8 3 25 0 11 0 481787668 858030080 115800 4294967295 134512640 134569956 3221224400 3221214952 1131500045 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 115800 13073 16 0 209464 0
vsize: 837920
[startup+290.173 s]
Raw data (loadavg): 1.12 1.04 0.94 2/64 29567
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 26110 61 8 4 25 0 11 0 481787668 858030080 119455 4294967295 134512640 134569956 3221224400 3221214808 1131487460 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 119455 13073 16 0 209464 0
vsize: 837920
[startup+300.172 s]
Raw data (loadavg): 1.10 1.04 0.94 2/64 29578
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 27044 62 8 4 25 0 11 0 481787668 858030080 121826 4294967295 134512640 134569956 3221224400 3221214808 1131487407 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 121826 13073 16 0 209464 0
vsize: 837920
[startup+310.173 s]
Raw data (loadavg): 1.08 1.04 0.94 2/64 29588
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 27976 63 9 4 21 0 11 0 481787668 858030080 124327 4294967295 134512640 134569956 3221224400 3221214808 1131487366 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 124327 13073 16 0 209464 0
vsize: 837920
[startup+320.172 s]
Raw data (loadavg): 1.07 1.03 0.94 2/63 29598
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 28907 64 9 4 25 0 10 0 481787668 858030080 126770 4294967295 134512640 134569956 3221224400 3221214672 1131315394 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 126770 13073 16 0 209464 0
vsize: 837920
[startup+330.173 s]
Raw data (loadavg): 1.06 1.03 0.94 2/63 29608
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 29822 65 10 4 25 0 10 0 481787668 858030080 129603 4294967295 134512640 134569956 3221224400 3221213504 1073952481 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 129606 13073 16 0 209464 0
vsize: 837920
[startup+340.173 s]
Raw data (loadavg): 1.05 1.03 0.94 2/64 29618
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 30743 65 10 4 22 0 11 0 481787668 858030080 132774 4294967295 134512640 134569956 3221224400 3221214800 1131320332 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 132774 13073 16 0 209464 0
vsize: 837920
[startup+350.174 s]
Raw data (loadavg): 1.04 1.03 0.94 2/64 29628
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 31678 66 10 4 20 0 11 0 481787668 858030080 135125 4294967295 134512640 134569956 3221224400 3221214808 1131487366 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 135125 13073 16 0 209464 0
vsize: 837920
[startup+360.174 s]
Raw data (loadavg): 1.03 1.03 0.94 2/64 29638
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 32611 67 11 5 17 0 11 0 481787668 858030080 137536 4294967295 134512640 134569956 3221224400 3221214808 1131487324 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 137536 13073 16 0 209464 0
vsize: 837920
[startup+370.174 s]
Raw data (loadavg): 1.03 1.03 0.94 2/64 29647
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 33541 67 11 5 25 0 11 0 481787668 858030080 140087 4294967295 134512640 134569956 3221224400 3221214808 1131486511 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 140087 13073 16 0 209464 0
vsize: 837920
[startup+380.175 s]
Raw data (loadavg): 1.02 1.03 0.94 2/63 29656
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 34469 68 11 5 25 0 10 0 481787668 858030080 142930 4294967295 134512640 134569956 3221224400 3221214760 1131272000 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 142930 13073 16 0 209464 0
vsize: 837920
[startup+390.175 s]
Raw data (loadavg): 1.02 1.02 0.94 2/64 29666
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 35406 68 12 5 17 0 11 0 481787668 858030080 145803 4294967295 134512640 134569956 3221224400 3221214808 1131487309 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 145803 13073 16 0 209464 0
vsize: 837920
[startup+400.18 s]
Raw data (loadavg): 1.02 1.02 0.94 2/64 29675
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 36340 69 12 5 17 0 11 0 481787668 858030080 148180 4294967295 134512640 134569956 3221224400 3221214808 1131486493 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 148180 13073 16 0 209464 0
vsize: 837920
[startup+410.181 s]
Raw data (loadavg): 1.01 1.02 0.94 2/63 29683
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 37272 70 12 5 25 0 10 0 481787668 858030080 150732 4294967295 134512640 134569956 3221224400 3221214760 1131288232 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 150732 13073 16 0 209464 0
vsize: 837920
[startup+420.181 s]
Raw data (loadavg): 1.01 1.02 0.94 2/64 29692
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 38207 70 13 5 25 0 11 0 481787668 858030080 153088 4294967295 134512640 134569956 3221224400 3221214808 1131486580 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 153088 13073 16 0 209464 0
vsize: 837920
[startup+430.183 s]
Raw data (loadavg): 1.01 1.02 0.94 2/64 29701
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 39175 71 13 6 25 0 11 0 481787668 858030080 154232 4294967295 134512640 134569956 3221224400 3221214808 1131487366 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 154232 13073 16 0 209464 0
vsize: 837920
[startup+440.184 s]
Raw data (loadavg): 1.01 1.02 0.94 2/63 29705
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 39659 71 13 6 25 0 10 0 481787668 858030080 155447 4294967295 134512640 134569956 3221224400 3221213424 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 155447 13073 16 0 209464 0
vsize: 837920
[startup+450.183 s]
Raw data (loadavg): 1.01 1.02 0.94 2/63 29705
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 39659 71 13 6 25 0 10 0 481787668 858030080 155448 4294967295 134512640 134569956 3221224400 3221213424 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 155448 13073 16 0 209464 0
vsize: 837920
[startup+460.184 s]
Raw data (loadavg): 1.00 1.02 0.94 2/63 29712
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 40445 71 13 6 25 0 10 0 481787668 858030080 155450 4294967295 134512640 134569956 3221224400 3221214472 1131359804 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 155450 13073 16 0 209464 0
vsize: 837920
[startup+470.185 s]
Raw data (loadavg): 1.00 1.02 0.94 2/64 29721
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 41381 72 14 6 25 0 11 0 481787668 858030080 156133 4294967295 134512640 134569956 3221224400 3221214808 1131486504 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 156133 13073 16 0 209464 0
vsize: 837920
[startup+480.186 s]
Raw data (loadavg): 1.00 1.02 0.94 2/64 29724
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 41772 72 14 6 25 0 11 0 481787668 858030080 156133 4294967295 134512640 134569956 3221224400 3221213592 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 156133 13073 16 0 209464 0
vsize: 837920
[startup+490.186 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 29727
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 42045 72 14 6 25 0 11 0 481787668 858030080 158646 4294967295 134512640 134569956 3221224400 3221214808 1131487362 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 158646 13073 16 0 209464 0
vsize: 837920
[startup+500.186 s]
Raw data (loadavg): 1.00 1.01 0.94 2/63 29728
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 42245 72 14 6 25 0 10 0 481787668 858030080 158646 4294967295 134512640 134569956 3221224400 3221213504 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 158646 13073 16 0 209464 0
vsize: 837920
[startup+510.187 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 29732
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 42697 72 14 6 25 0 11 0 481787668 858030080 160015 4294967295 134512640 134569956 3221224400 3221214960 1131521740 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 160015 13073 16 0 209464 0
vsize: 837920
[startup+520.187 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 29733
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 42808 72 14 6 25 0 11 0 481787668 858030080 160015 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 160015 13073 16 0 209464 0
vsize: 837920
[startup+530.188 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 29733
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 42808 72 14 6 25 0 11 0 481787668 858030080 160015 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 160015 13073 16 0 209464 0
vsize: 837920
[startup+540.189 s]
Raw data (loadavg): 1.00 1.01 0.94 2/63 29737
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 43286 73 15 6 25 0 10 0 481787668 858030080 160015 4294967295 134512640 134569956 3221224400 3221213376 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 160015 13073 16 0 209464 0
vsize: 837920
[startup+550.189 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 29738
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 43368 73 15 6 24 0 11 0 481787668 858030080 160015 4294967295 134512640 134569956 3221224400 3221214808 1131486504 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 160015 13073 16 0 209464 0
vsize: 837920
[startup+560.19 s]
Raw data (loadavg): 1.00 1.01 0.94 2/63 29742
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 43862 73 15 6 25 0 10 0 481787668 858030080 160015 4294967295 134512640 134569956 3221224400 3221213504 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 160015 13073 16 0 209464 0
vsize: 837920
[startup+570.19 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 29744
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 43996 73 15 6 25 0 11 0 481787668 858030080 160015 4294967295 134512640 134569956 3221224400 3221214808 1131486511 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 160015 13073 16 0 209464 0
vsize: 837920
[startup+580.191 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 29747
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 44439 73 15 6 25 0 11 0 481787668 858030080 160015 4294967295 134512640 134569956 3221224400 3221213464 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 160015 13073 16 0 209464 0
vsize: 837920
[startup+590.192 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29749
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 44611 73 15 6 25 0 11 0 481787668 858030080 160560 4294967295 134512640 134569956 3221224400 3221214808 1131487366 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 160560 13073 16 0 209464 0
vsize: 837920
[startup+600.192 s]
Raw data (loadavg): 1.00 1.00 0.94 2/63 29751
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 44930 73 15 6 25 0 10 0 481787668 858030080 160560 4294967295 134512640 134569956 3221224400 3221213416 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 160560 13073 16 0 209464 0
vsize: 837920
[startup+610.193 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29754
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 45191 73 15 6 25 0 11 0 481787668 858030080 161492 4294967295 134512640 134569956 3221224400 3221214808 1131487407 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 161492 13073 16 0 209464 0
vsize: 837920
[startup+620.193 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29756
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 45516 73 15 6 25 0 11 0 481787668 858030080 161492 4294967295 134512640 134569956 3221224400 3221213592 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 161492 13073 16 0 209464 0
vsize: 837920
[startup+630.194 s]
Raw data (loadavg): 1.00 1.00 0.94 2/63 29758
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 45765 74 15 6 25 0 10 0 481787668 858030080 162623 4294967295 134512640 134569956 3221224400 3221214760 1131288924 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 162623 13073 16 0 209464 0
vsize: 837920
[startup+640.194 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29761
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 46107 74 15 6 25 0 11 0 481787668 858030080 162623 4294967295 134512640 134569956 3221224400 3221213592 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 162623 13073 16 0 209464 0
vsize: 837920
[startup+650.194 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29763
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 46327 74 15 6 25 0 11 0 481787668 858030080 163978 4294967295 134512640 134569956 3221224400 3221214808 1131486598 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 163978 13073 16 0 209464 0
vsize: 837920
[startup+660.197 s]
Raw data (loadavg): 1.00 1.00 0.94 2/63 29765
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 46607 74 16 6 25 0 10 0 481787668 858030080 163978 4294967295 134512640 134569956 3221224400 3221213504 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 163978 13073 16 0 209464 0
vsize: 837920
[startup+670.196 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29768
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 46874 74 16 6 25 0 11 0 481787668 858030080 165347 4294967295 134512640 134569956 3221224400 3221214808 1131486577 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 165347 13073 16 0 209464 0
vsize: 837920
[startup+680.197 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29770
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 47204 74 16 6 25 0 11 0 481787668 858030080 165347 4294967295 134512640 134569956 3221224400 3221213464 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 165347 13073 16 0 209464 0
vsize: 837920
[startup+690.197 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29772
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 47391 74 16 6 25 0 11 0 481787668 858030080 166176 4294967295 134512640 134569956 3221224400 3221214808 1131487366 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 166176 13073 16 0 209464 0
vsize: 837920
[startup+700.197 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29775
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 47804 74 16 7 25 0 11 0 481787668 858030080 166176 4294967295 134512640 134569956 3221224400 3221213488 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 166176 13073 16 0 209464 0
vsize: 837920
[startup+710.197 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29776
Raw data (stat): 29256 (java) R 29255 30854 30853 0 -1 0 18020 3 1 0 47921 75 16 7 25 0 11 0 481787668 858030080 167531 4294967295 134512640 134569956 3221224400 3221214808 1131487366 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 167531 13073 16 0 209464 0
vsize: 837920
[startup+720.198 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29778
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 48174 75 16 7 25 0 11 0 481787668 858030080 167531 4294967295 134512640 134569956 3221224400 3221213440 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 167531 13073 16 0 209464 0
vsize: 837920
[startup+730.198 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29778
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 48174 75 16 7 25 0 11 0 481787668 858030080 168362 4294967295 134512640 134569956 3221224400 3221213440 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 168362 13073 16 0 209464 0
vsize: 837920
[startup+740.199 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 29778
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 48174 75 16 7 25 0 11 0 481787668 858030080 168362 4294967295 134512640 134569956 3221224400 3221213440 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 168362 13073 16 0 209464 0
vsize: 837920
[startup+742.298 s]
Raw data (loadavg): 1.00 1.00 0.94 1/53 29778
Raw data (stat): 29256 (java) S 29255 30854 30853 0 -1 0 18020 3 1 0 48174 75 16 7 25 0 11 0 481787668 858030080 168362 4294967295 134512640 134569956 3221224400 3221213440 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209480 168362 13073 16 0 209464 0
vsize: 0

Child status: 1
Real time (s): 742.298
CPU time (s): 754.614
CPU user time (s): 750.057
CPU system time (s): 4.55731
CPU usage (%): 101.659
Max. virtual memory (Kb): 845740
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####