Some explanations

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

General information on the benchmark

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-bell3a.opb
MD5SUM26dd13d463ba85c3a30386739f6ae61e
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2147483647
Optimality of the best value was proved NO
Number of terms in the objective function 1716
Biggest coefficient in the objective function 5134096531456000
Number of bits for the biggest coefficient in the objective function 53
Sum of the numbers in the objective function 216401520151185266
Number of bits of the sum of numbers in the objective function 58
Biggest number in a constraint 5134096531456000
Number of bits of the biggest number in a constraint 53
Biggest sum of numbers in a constraint 216401520151185266
Number of bits of the biggest sum of numbers58
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1243.96
Number of variables2219
Total number of constraints194
Number of constraints which are clauses22
Number of constraints which are cardinality constraints (but not clauses)39
Number of constraints which are nor clauses,nor cardinality constraints133
Minimum length of a constraint1
Maximum length of a constraint191

Trace number 16494 

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        651368 kB
Buffers:         26452 kB
Cached:         325040 kB
SwapCached:          0 kB
Active:         164100 kB
Inactive:       190172 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        651116 kB
SwapTotal:     2097892 kB
SwapFree:      2097824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            23292 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 07:51:53 (client local time) WITH STATUS 143 IN 1263.97 SECONDS
stats: 13217 7 1263.97 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-bell3a.opb
c reading problem 
c [nbvar=2219]
c [nbconstr=194]
c time 4.273
c #vars     2219
c #clauses  152
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=1373306270
c Current CPU time (ms) : 10.363
c starts	: 1
c conflicts	: 12
c decisions	: 1174
c propagations	: 2713
c inspects	: 2456
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 12
c root simplifications	: 1
c 
c CURRENT OPTIMUM=1232064248
c Current CPU time (ms) : 19.984
c starts	: 2
c conflicts	: 36
c decisions	: 5294
c propagations	: 12310
c inspects	: 17885
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 36
c root simplifications	: 6
c 
c CURRENT OPTIMUM=1113121730
c Current CPU time (ms) : 28.18
c starts	: 3
c conflicts	: 51
c decisions	: 7256
c propagations	: 17110
c inspects	: 28203
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 51
c root simplifications	: 9
c 
c CURRENT OPTIMUM=-1590168737
c Current CPU time (ms) : 37.646
c starts	: 4
c conflicts	: 63
c decisions	: 9938
c propagations	: 21232
c inspects	: 39553
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 63
c root simplifications	: 11
c 
c CURRENT OPTIMUM=111165240
c Current CPU time (ms) : 43.532
c starts	: 5
c conflicts	: 70
c decisions	: 11143
c propagations	: 23620
c inspects	: 46766
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 70
c root simplifications	: 12
c 
c CURRENT OPTIMUM=1911268886
c Current CPU time (ms) : 52.268
c starts	: 6
c conflicts	: 77
c decisions	: 13623
c propagations	: 27994
c inspects	: 60408
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 77
c root simplifications	: 14
c 
c CURRENT OPTIMUM=224479549
c Current CPU time (ms) : 59.897
c starts	: 7
c conflicts	: 82
c decisions	: 15465
c propagations	: 30873
c inspects	: 68451
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 82
c root simplifications	: 15
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 66.94
c starts	: 8
c conflicts	: 84
c decisions	: 17000
c propagations	: 33310
c inspects	: 77613
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 17
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 71.757
c starts	: 9
c conflicts	: 84
c decisions	: 18290
c propagations	: 35369
c inspects	: 82603
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 18
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 76.534
c starts	: 10
c conflicts	: 84
c decisions	: 19580
c propagations	: 37428
c inspects	: 87594
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 19
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 81.345
c starts	: 11
c conflicts	: 84
c decisions	: 20870
c propagations	: 39487
c inspects	: 92584
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 20
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 86.164
c starts	: 12
c conflicts	: 84
c decisions	: 22160
c propagations	: 41546
c inspects	: 97574
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 21
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 90.915
c starts	: 13
c conflicts	: 84
c decisions	: 23450
c propagations	: 43605
c inspects	: 102564
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 22
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 95.709
c starts	: 14
c conflicts	: 84
c decisions	: 24740
c propagations	: 45664
c inspects	: 107554
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 23
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 100.48
c starts	: 15
c conflicts	: 84
c decisions	: 26030
c propagations	: 47723
c inspects	: 112544
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 24
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 105.216
c starts	: 16
c conflicts	: 84
c decisions	: 27320
c propagations	: 49782
c inspects	: 117535
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 25
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 109.981
c starts	: 17
c conflicts	: 84
c decisions	: 28610
c propagations	: 51841
c inspects	: 122525
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 26
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 114.714
c starts	: 18
c conflicts	: 84
c decisions	: 29900
c propagations	: 53900
c inspects	: 127516
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 27
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 119.488
c starts	: 19
c conflicts	: 84
c decisions	: 31190
c propagations	: 55959
c inspects	: 132507
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 28
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 124.246
c starts	: 20
c conflicts	: 84
c decisions	: 32480
c propagations	: 58018
c inspects	: 137497
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 29
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 128.988
c starts	: 21
c conflicts	: 84
c decisions	: 33770
c propagations	: 60077
c inspects	: 142487
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 30
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 133.761
c starts	: 22
c conflicts	: 84
c decisions	: 35060
c propagations	: 62136
c inspects	: 147478
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 31
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 138.509
c starts	: 23
c conflicts	: 84
c decisions	: 36350
c propagations	: 64195
c inspects	: 152469
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 32
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 143.279
c starts	: 24
c conflicts	: 84
c decisions	: 37640
c propagations	: 66254
c inspects	: 157460
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 33
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 148.07
c starts	: 25
c conflicts	: 84
c decisions	: 38930
c propagations	: 68313
c inspects	: 162450
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 34
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 152.817
c starts	: 26
c conflicts	: 84
c decisions	: 40220
c propagations	: 70372
c inspects	: 167441
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 35
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 157.586
c starts	: 27
c conflicts	: 84
c decisions	: 41510
c propagations	: 72431
c inspects	: 172432
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 36
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 162.367
c starts	: 28
c conflicts	: 84
c decisions	: 42800
c propagations	: 74490
c inspects	: 177423
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 37
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 167.109
c starts	: 29
c conflicts	: 84
c decisions	: 44090
c propagations	: 76549
c inspects	: 182414
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 38
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 171.885
c starts	: 30
c conflicts	: 84
c decisions	: 45380
c propagations	: 78608
c inspects	: 187405
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 39
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 176.643
c starts	: 31
c conflicts	: 84
c decisions	: 46670
c propagations	: 80667
c inspects	: 192396
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 40
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 180.759
c starts	: 32
c conflicts	: 84
c decisions	: 47960
c propagations	: 82726
c inspects	: 197387
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 41
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 184.884
c starts	: 33
c conflicts	: 84
c decisions	: 49250
c propagations	: 84785
c inspects	: 202378
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 42
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 188.977
c starts	: 34
c conflicts	: 84
c decisions	: 50540
c propagations	: 86844
c inspects	: 207369
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 43
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 193.069
c starts	: 35
c conflicts	: 84
c decisions	: 51830
c propagations	: 88903
c inspects	: 212359
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 44
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 197.171
c starts	: 36
c conflicts	: 84
c decisions	: 53120
c propagations	: 90962
c inspects	: 217349
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 45
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 201.266
c starts	: 37
c conflicts	: 84
c decisions	: 54410
c propagations	: 93021
c inspects	: 222339
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 46
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 205.369
c starts	: 38
c conflicts	: 84
c decisions	: 55700
c propagations	: 95080
c inspects	: 227330
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 47
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 209.461
c starts	: 39
c conflicts	: 84
c decisions	: 56990
c propagations	: 97139
c inspects	: 232321
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 48
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 213.586
c starts	: 40
c conflicts	: 84
c decisions	: 58280
c propagations	: 99198
c inspects	: 237312
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 49
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 217.698
c starts	: 41
c conflicts	: 84
c decisions	: 59570
c propagations	: 101257
c inspects	: 242303
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 50
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 221.799
c starts	: 42
c conflicts	: 84
c decisions	: 60860
c propagations	: 103316
c inspects	: 247293
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 51
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 225.944
c starts	: 43
c conflicts	: 84
c decisions	: 62150
c propagations	: 105375
c inspects	: 252283
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 52
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 230.041
c starts	: 44
c conflicts	: 84
c decisions	: 63440
c propagations	: 107434
c inspects	: 257273
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 53
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 234.188
c starts	: 45
c conflicts	: 84
c decisions	: 64730
c propagations	: 109493
c inspects	: 262263
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 54
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 238.321
c starts	: 46
c conflicts	: 84
c decisions	: 66020
c propagations	: 111552
c inspects	: 267254
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 55
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 242.424
c starts	: 47
c conflicts	: 84
c decisions	: 67310
c propagations	: 113611
c inspects	: 272245
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 56
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 246.579
c starts	: 48
c conflicts	: 84
c decisions	: 68600
c propagations	: 115670
c inspects	: 277236
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 57
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 250.705
c starts	: 49
c conflicts	: 84
c decisions	: 69890
c propagations	: 117729
c inspects	: 282227
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 58
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 254.803
c starts	: 50
c conflicts	: 84
c decisions	: 71180
c propagations	: 119788
c inspects	: 287218
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 59
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 258.924
c starts	: 51
c conflicts	: 84
c decisions	: 72470
c propagations	: 121847
c inspects	: 292209
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 60
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 263.022
c starts	: 52
c conflicts	: 84
c decisions	: 73760
c propagations	: 123906
c inspects	: 297199
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 61
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 267.141
c starts	: 53
c conflicts	: 84
c decisions	: 75050
c propagations	: 125965
c inspects	: 302190
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 62
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 271.261
c starts	: 54
c conflicts	: 84
c decisions	: 76340
c propagations	: 128024
c inspects	: 307180
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 63
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 275.349
c starts	: 55
c conflicts	: 84
c decisions	: 77630
c propagations	: 130083
c inspects	: 312171
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 64
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 279.455
c starts	: 56
c conflicts	: 84
c decisions	: 78920
c propagations	: 132142
c inspects	: 317161
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 65
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 283.587
c starts	: 57
c conflicts	: 84
c decisions	: 80210
c propagations	: 134201
c inspects	: 322152
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 66
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 287.676
c starts	: 58
c conflicts	: 84
c decisions	: 81500
c propagations	: 136260
c inspects	: 327143
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 67
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 291.784
c starts	: 59
c conflicts	: 84
c decisions	: 82790
c propagations	: 138319
c inspects	: 332134
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 68
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 295.879
c starts	: 60
c conflicts	: 84
c decisions	: 84080
c propagations	: 140378
c inspects	: 337125
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 69
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 300.0
c starts	: 61
c conflicts	: 84
c decisions	: 85370
c propagations	: 142437
c inspects	: 342115
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 70
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 304.118
c starts	: 62
c conflicts	: 84
c decisions	: 86660
c propagations	: 144496
c inspects	: 347105
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 71
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 308.211
c starts	: 63
c conflicts	: 84
c decisions	: 87950
c propagations	: 146555
c inspects	: 352096
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 72
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 312.3
c starts	: 64
c conflicts	: 84
c decisions	: 89240
c propagations	: 148614
c inspects	: 357086
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 73
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 316.354
c starts	: 65
c conflicts	: 84
c decisions	: 90530
c propagations	: 150673
c inspects	: 362076
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 74
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 320.428
c starts	: 66
c conflicts	: 84
c decisions	: 91820
c propagations	: 152732
c inspects	: 367066
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 75
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 324.509
c starts	: 67
c conflicts	: 84
c decisions	: 93110
c propagations	: 154791
c inspects	: 372057
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 76
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 328.576
c starts	: 68
c conflicts	: 84
c decisions	: 94400
c propagations	: 156850
c inspects	: 377047
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 77
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 332.659
c starts	: 69
c conflicts	: 84
c decisions	: 95690
c propagations	: 158909
c inspects	: 382037
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 78
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 336.733
c starts	: 70
c conflicts	: 84
c decisions	: 96980
c propagations	: 160968
c inspects	: 387028
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 79
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 340.782
c starts	: 71
c conflicts	: 84
c decisions	: 98270
c propagations	: 163027
c inspects	: 392019
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 80
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 344.855
c starts	: 72
c conflicts	: 84
c decisions	: 99560
c propagations	: 165086
c inspects	: 397010
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 81
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 348.902
c starts	: 73
c conflicts	: 84
c decisions	: 100850
c propagations	: 167145
c inspects	: 402001
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 82
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 352.978
c starts	: 74
c conflicts	: 84
c decisions	: 102140
c propagations	: 169204
c inspects	: 406992
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 83
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 357.062
c starts	: 75
c conflicts	: 84
c decisions	: 103430
c propagations	: 171263
c inspects	: 411983
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 84
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 361.13
c starts	: 76
c conflicts	: 84
c decisions	: 104720
c propagations	: 173322
c inspects	: 416974
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 85
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 365.258
c starts	: 77
c conflicts	: 84
c decisions	: 106010
c propagations	: 175381
c inspects	: 421965
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 86
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 369.368
c starts	: 78
c conflicts	: 84
c decisions	: 107300
c propagations	: 177440
c inspects	: 426956
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 87
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 373.471
c starts	: 79
c conflicts	: 84
c decisions	: 108590
c propagations	: 179499
c inspects	: 431947
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 88
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 377.6
c starts	: 80
c conflicts	: 84
c decisions	: 109880
c propagations	: 181558
c inspects	: 436938
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 89
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 381.678
c starts	: 81
c conflicts	: 84
c decisions	: 111170
c propagations	: 183617
c inspects	: 441928
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 90
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 385.814
c starts	: 82
c conflicts	: 84
c decisions	: 112460
c propagations	: 185676
c inspects	: 446918
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 91
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 389.929
c starts	: 83
c conflicts	: 84
c decisions	: 113750
c propagations	: 187735
c inspects	: 451909
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 92
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 393.97
c starts	: 84
c conflicts	: 84
c decisions	: 115040
c propagations	: 189794
c inspects	: 456899
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 93
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 398.034
c starts	: 85
c conflicts	: 84
c decisions	: 116330
c propagations	: 191853
c inspects	: 461889
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 94
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 402.104
c starts	: 86
c conflicts	: 84
c decisions	: 117620
c propagations	: 193912
c inspects	: 466879
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 95
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 406.152
c starts	: 87
c conflicts	: 84
c decisions	: 118910
c propagations	: 195971
c inspects	: 471870
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 96
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 410.231
c starts	: 88
c conflicts	: 84
c decisions	: 120200
c propagations	: 198030
c inspects	: 476860
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 97
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 414.285
c starts	: 89
c conflicts	: 84
c decisions	: 121490
c propagations	: 200089
c inspects	: 481850
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 98
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 418.386
c starts	: 90
c conflicts	: 84
c decisions	: 122780
c propagations	: 202148
c inspects	: 486841
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 99
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 422.474
c starts	: 91
c conflicts	: 84
c decisions	: 124070
c propagations	: 204207
c inspects	: 491832
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 100
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 426.525
c starts	: 92
c conflicts	: 84
c decisions	: 125360
c propagations	: 206266
c inspects	: 496823
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 101
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 430.622
c starts	: 93
c conflicts	: 84
c decisions	: 126650
c propagations	: 208325
c inspects	: 501813
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 102
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 434.725
c starts	: 94
c conflicts	: 84
c decisions	: 127940
c propagations	: 210384
c inspects	: 506803
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 103
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 438.791
c starts	: 95
c conflicts	: 84
c decisions	: 129230
c propagations	: 212443
c inspects	: 511794
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 104
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 442.894
c starts	: 96
c conflicts	: 84
c decisions	: 130520
c propagations	: 214502
c inspects	: 516785
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 105
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 446.964
c starts	: 97
c conflicts	: 84
c decisions	: 131810
c propagations	: 216561
c inspects	: 521776
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 106
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 451.122
c starts	: 98
c conflicts	: 84
c decisions	: 133100
c propagations	: 218620
c inspects	: 526766
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 107
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 455.294
c starts	: 99
c conflicts	: 84
c decisions	: 134390
c propagations	: 220679
c inspects	: 531756
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 108
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 459.433
c starts	: 100
c conflicts	: 84
c decisions	: 135680
c propagations	: 222738
c inspects	: 536746
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 109
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 463.594
c starts	: 101
c conflicts	: 84
c decisions	: 136970
c propagations	: 224797
c inspects	: 541737
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 110
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 467.722
c starts	: 102
c conflicts	: 84
c decisions	: 138260
c propagations	: 226856
c inspects	: 546728
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 111
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 471.884
c starts	: 103
c conflicts	: 84
c decisions	: 139550
c propagations	: 228915
c inspects	: 551719
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 112
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 476.041
c starts	: 104
c conflicts	: 84
c decisions	: 140840
c propagations	: 230974
c inspects	: 556710
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 113
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 480.169
c starts	: 105
c conflicts	: 84
c decisions	: 142130
c propagations	: 233033
c inspects	: 561700
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 114
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 484.33
c starts	: 106
c conflicts	: 84
c decisions	: 143420
c propagations	: 235092
c inspects	: 566690
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 115
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 488.487
c starts	: 107
c conflicts	: 84
c decisions	: 144710
c propagations	: 237151
c inspects	: 571680
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 116
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 492.604
c starts	: 108
c conflicts	: 84
c decisions	: 146000
c propagations	: 239210
c inspects	: 576670
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 117
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 496.754
c starts	: 109
c conflicts	: 84
c decisions	: 147290
c propagations	: 241269
c inspects	: 581661
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 118
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 500.892
c starts	: 110
c conflicts	: 84
c decisions	: 148580
c propagations	: 243328
c inspects	: 586651
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 119
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 505.054
c starts	: 111
c conflicts	: 84
c decisions	: 149870
c propagations	: 245387
c inspects	: 591641
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 120
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 509.213
c starts	: 112
c conflicts	: 84
c decisions	: 151160
c propagations	: 247446
c inspects	: 596631
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 121
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 513.343
c starts	: 113
c conflicts	: 84
c decisions	: 152450
c propagations	: 249505
c inspects	: 601621
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 122
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 517.515
c starts	: 114
c conflicts	: 84
c decisions	: 153740
c propagations	: 251564
c inspects	: 606612
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 123
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 521.663
c starts	: 115
c conflicts	: 84
c decisions	: 155030
c propagations	: 253623
c inspects	: 611603
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 124
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 525.778
c starts	: 116
c conflicts	: 84
c decisions	: 156320
c propagations	: 255682
c inspects	: 616594
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 125
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 529.935
c starts	: 117
c conflicts	: 84
c decisions	: 157610
c propagations	: 257741
c inspects	: 621584
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 126
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 534.074
c starts	: 118
c conflicts	: 84
c decisions	: 158900
c propagations	: 259800
c inspects	: 626575
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 127
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 538.234
c starts	: 119
c conflicts	: 84
c decisions	: 160190
c propagations	: 261859
c inspects	: 631565
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 128
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 542.373
c starts	: 120
c conflicts	: 84
c decisions	: 161480
c propagations	: 263918
c inspects	: 636555
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 129
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 546.486
c starts	: 121
c conflicts	: 84
c decisions	: 162770
c propagations	: 265977
c inspects	: 641545
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 130
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 550.62
c starts	: 122
c conflicts	: 84
c decisions	: 164060
c propagations	: 268036
c inspects	: 646535
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 131
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 554.773
c starts	: 123
c conflicts	: 84
c decisions	: 165350
c propagations	: 270095
c inspects	: 651526
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 132
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 558.903
c starts	: 124
c conflicts	: 84
c decisions	: 166640
c propagations	: 272154
c inspects	: 656517
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 133
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 563.044
c starts	: 125
c conflicts	: 84
c decisions	: 167930
c propagations	: 274213
c inspects	: 661508
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 134
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 567.144
c starts	: 126
c conflicts	: 84
c decisions	: 169220
c propagations	: 276272
c inspects	: 666499
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 135
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 571.233
c starts	: 127
c conflicts	: 84
c decisions	: 170510
c propagations	: 278331
c inspects	: 671490
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 136
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 575.317
c starts	: 128
c conflicts	: 84
c decisions	: 171800
c propagations	: 280390
c inspects	: 676480
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 137
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 579.376
c starts	: 129
c conflicts	: 84
c decisions	: 173090
c propagations	: 282449
c inspects	: 681471
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 138
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 583.487
c starts	: 130
c conflicts	: 84
c decisions	: 174380
c propagations	: 284508
c inspects	: 686462
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 139
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 587.556
c starts	: 131
c conflicts	: 84
c decisions	: 175670
c propagations	: 286567
c inspects	: 691452
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 140
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 591.646
c starts	: 132
c conflicts	: 84
c decisions	: 176960
c propagations	: 288626
c inspects	: 696443
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 141
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 595.737
c starts	: 133
c conflicts	: 84
c decisions	: 178250
c propagations	: 290685
c inspects	: 701433
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 142
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 599.796
c starts	: 134
c conflicts	: 84
c decisions	: 179540
c propagations	: 292744
c inspects	: 706423
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 143
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 603.881
c starts	: 135
c conflicts	: 84
c decisions	: 180830
c propagations	: 294803
c inspects	: 711413
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 144
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 607.962
c starts	: 136
c conflicts	: 84
c decisions	: 182120
c propagations	: 296862
c inspects	: 716404
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 145
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 612.036
c starts	: 137
c conflicts	: 84
c decisions	: 183410
c propagations	: 298921
c inspects	: 721395
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 146
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 616.106
c starts	: 138
c conflicts	: 84
c decisions	: 184700
c propagations	: 300980
c inspects	: 726385
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 147
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 620.161
c starts	: 139
c conflicts	: 84
c decisions	: 185990
c propagations	: 303039
c inspects	: 731375
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 148
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 624.238
c starts	: 140
c conflicts	: 84
c decisions	: 187280
c propagations	: 305098
c inspects	: 736365
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 149
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 628.323
c starts	: 141
c conflicts	: 84
c decisions	: 188570
c propagations	: 307157
c inspects	: 741355
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 150
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 632.414
c starts	: 142
c conflicts	: 84
c decisions	: 189860
c propagations	: 309216
c inspects	: 746345
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 151
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 636.503
c starts	: 143
c conflicts	: 84
c decisions	: 191150
c propagations	: 311275
c inspects	: 751335
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 152
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 640.605
c starts	: 144
c conflicts	: 84
c decisions	: 192440
c propagations	: 313334
c inspects	: 756326
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 153
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 644.695
c starts	: 145
c conflicts	: 84
c decisions	: 193730
c propagations	: 315393
c inspects	: 761316
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 154
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 648.869
c starts	: 146
c conflicts	: 84
c decisions	: 195020
c propagations	: 317452
c inspects	: 766306
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 155
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 652.995
c starts	: 147
c conflicts	: 84
c decisions	: 196310
c propagations	: 319511
c inspects	: 771297
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 156
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 657.144
c starts	: 148
c conflicts	: 84
c decisions	: 197600
c propagations	: 321570
c inspects	: 776287
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 157
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 661.332
c starts	: 149
c conflicts	: 84
c decisions	: 198890
c propagations	: 323629
c inspects	: 781277
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 158
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 665.469
c starts	: 150
c conflicts	: 84
c decisions	: 200180
c propagations	: 325688
c inspects	: 786267
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 159
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 669.653
c starts	: 151
c conflicts	: 84
c decisions	: 201470
c propagations	: 327747
c inspects	: 791258
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 160
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 673.808
c starts	: 152
c conflicts	: 84
c decisions	: 202760
c propagations	: 329806
c inspects	: 796249
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 161
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 677.886
c starts	: 153
c conflicts	: 84
c decisions	: 204050
c propagations	: 331865
c inspects	: 801239
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 162
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 681.997
c starts	: 154
c conflicts	: 84
c decisions	: 205340
c propagations	: 333924
c inspects	: 806230
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 163
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 686.071
c starts	: 155
c conflicts	: 84
c decisions	: 206630
c propagations	: 335983
c inspects	: 811220
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 164
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 690.166
c starts	: 156
c conflicts	: 84
c decisions	: 207920
c propagations	: 338042
c inspects	: 816211
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 165
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 694.267
c starts	: 157
c conflicts	: 84
c decisions	: 209210
c propagations	: 340101
c inspects	: 821201
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 166
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 698.336
c starts	: 158
c conflicts	: 84
c decisions	: 210500
c propagations	: 342160
c inspects	: 826192
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 167
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 702.432
c starts	: 159
c conflicts	: 84
c decisions	: 211790
c propagations	: 344219
c inspects	: 831183
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 168
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 706.522
c starts	: 160
c conflicts	: 84
c decisions	: 213080
c propagations	: 346278
c inspects	: 836173
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 169
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 710.588
c starts	: 161
c conflicts	: 84
c decisions	: 214370
c propagations	: 348337
c inspects	: 841163
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 170
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 714.671
c starts	: 162
c conflicts	: 84
c decisions	: 215660
c propagations	: 350396
c inspects	: 846154
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 171
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 718.742
c starts	: 163
c conflicts	: 84
c decisions	: 216950
c propagations	: 352455
c inspects	: 851144
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 172
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 722.827
c starts	: 164
c conflicts	: 84
c decisions	: 218240
c propagations	: 354514
c inspects	: 856134
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 173
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 726.911
c starts	: 165
c conflicts	: 84
c decisions	: 219530
c propagations	: 356573
c inspects	: 861124
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 174
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 730.994
c starts	: 166
c conflicts	: 84
c decisions	: 220820
c propagations	: 358632
c inspects	: 866115
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 175
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 735.093
c starts	: 167
c conflicts	: 84
c decisions	: 222110
c propagations	: 360691
c inspects	: 871105
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 176
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 739.194
c starts	: 168
c conflicts	: 84
c decisions	: 223400
c propagations	: 362750
c inspects	: 876095
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 177
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 743.275
c starts	: 169
c conflicts	: 84
c decisions	: 224690
c propagations	: 364809
c inspects	: 881086
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 178
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 747.386
c starts	: 170
c conflicts	: 84
c decisions	: 225980
c propagations	: 366868
c inspects	: 886077
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 179
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 751.451
c starts	: 171
c conflicts	: 84
c decisions	: 227270
c propagations	: 368927
c inspects	: 891068
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 180
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 755.547
c starts	: 172
c conflicts	: 84
c decisions	: 228560
c propagations	: 370986
c inspects	: 896059
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 181
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 759.655
c starts	: 173
c conflicts	: 84
c decisions	: 229850
c propagations	: 373045
c inspects	: 901050
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 182
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 763.72
c starts	: 174
c conflicts	: 84
c decisions	: 231140
c propagations	: 375104
c inspects	: 906041
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 183
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 767.818
c starts	: 175
c conflicts	: 84
c decisions	: 232430
c propagations	: 377163
c inspects	: 911032
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 184
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 771.915
c starts	: 176
c conflicts	: 84
c decisions	: 233720
c propagations	: 379222
c inspects	: 916022
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 185
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 775.99
c starts	: 177
c conflicts	: 84
c decisions	: 235010
c propagations	: 381281
c inspects	: 921013
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 186
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 780.092
c starts	: 178
c conflicts	: 84
c decisions	: 236300
c propagations	: 383340
c inspects	: 926003
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 187
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 784.154
c starts	: 179
c conflicts	: 84
c decisions	: 237590
c propagations	: 385399
c inspects	: 930993
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 188
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 788.262
c starts	: 180
c conflicts	: 84
c decisions	: 238880
c propagations	: 387458
c inspects	: 935983
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 189
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 792.373
c starts	: 181
c conflicts	: 84
c decisions	: 240170
c propagations	: 389517
c inspects	: 940974
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 190
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 796.458
c starts	: 182
c conflicts	: 84
c decisions	: 241460
c propagations	: 391576
c inspects	: 945965
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 191
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 800.573
c starts	: 183
c conflicts	: 84
c decisions	: 242750
c propagations	: 393635
c inspects	: 950956
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 192
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 804.715
c starts	: 184
c conflicts	: 84
c decisions	: 244040
c propagations	: 395694
c inspects	: 955946
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 193
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 808.794
c starts	: 185
c conflicts	: 84
c decisions	: 245330
c propagations	: 397753
c inspects	: 960936
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 194
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 812.975
c starts	: 186
c conflicts	: 84
c decisions	: 246620
c propagations	: 399812
c inspects	: 965926
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 195
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 817.13
c starts	: 187
c conflicts	: 84
c decisions	: 247910
c propagations	: 401871
c inspects	: 970917
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 196
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 821.342
c starts	: 188
c conflicts	: 84
c decisions	: 249200
c propagations	: 403930
c inspects	: 975907
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 197
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 825.553
c starts	: 189
c conflicts	: 84
c decisions	: 250490
c propagations	: 405989
c inspects	: 980898
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 198
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 829.725
c starts	: 190
c conflicts	: 84
c decisions	: 251780
c propagations	: 408048
c inspects	: 985888
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 199
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 833.936
c starts	: 191
c conflicts	: 84
c decisions	: 253070
c propagations	: 410107
c inspects	: 990879
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 200
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 838.142
c starts	: 192
c conflicts	: 84
c decisions	: 254360
c propagations	: 412166
c inspects	: 995869
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 201
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 842.387
c starts	: 193
c conflicts	: 84
c decisions	: 255650
c propagations	: 414225
c inspects	: 1000859
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 202
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 846.619
c starts	: 194
c conflicts	: 84
c decisions	: 256940
c propagations	: 416284
c inspects	: 1005849
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 203
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 850.813
c starts	: 195
c conflicts	: 84
c decisions	: 258230
c propagations	: 418343
c inspects	: 1010839
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 204
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 855.074
c starts	: 196
c conflicts	: 84
c decisions	: 259520
c propagations	: 420402
c inspects	: 1015829
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 205
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 859.3
c starts	: 197
c conflicts	: 84
c decisions	: 260810
c propagations	: 422461
c inspects	: 1020819
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 206
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 863.482
c starts	: 198
c conflicts	: 84
c decisions	: 262100
c propagations	: 424520
c inspects	: 1025810
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 207
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 867.685
c starts	: 199
c conflicts	: 84
c decisions	: 263390
c propagations	: 426579
c inspects	: 1030801
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 208
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 871.857
c starts	: 200
c conflicts	: 84
c decisions	: 264680
c propagations	: 428638
c inspects	: 1035791
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 209
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 876.04
c starts	: 201
c conflicts	: 84
c decisions	: 265970
c propagations	: 430697
c inspects	: 1040781
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 210
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 880.22
c starts	: 202
c conflicts	: 84
c decisions	: 267260
c propagations	: 432756
c inspects	: 1045772
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 211
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 884.367
c starts	: 203
c conflicts	: 84
c decisions	: 268550
c propagations	: 434815
c inspects	: 1050763
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 212
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 888.552
c starts	: 204
c conflicts	: 84
c decisions	: 269840
c propagations	: 436874
c inspects	: 1055753
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 213
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 892.739
c starts	: 205
c conflicts	: 84
c decisions	: 271130
c propagations	: 438933
c inspects	: 1060744
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 214
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 896.92
c starts	: 206
c conflicts	: 84
c decisions	: 272420
c propagations	: 440992
c inspects	: 1065735
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 215
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 901.122
c starts	: 207
c conflicts	: 84
c decisions	: 273710
c propagations	: 443051
c inspects	: 1070725
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 216
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 905.297
c starts	: 208
c conflicts	: 84
c decisions	: 275000
c propagations	: 445110
c inspects	: 1075715
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 217
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 909.491
c starts	: 209
c conflicts	: 84
c decisions	: 276290
c propagations	: 447169
c inspects	: 1080705
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 218
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 913.694
c starts	: 210
c conflicts	: 84
c decisions	: 277580
c propagations	: 449228
c inspects	: 1085696
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 219
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 917.833
c starts	: 211
c conflicts	: 84
c decisions	: 278870
c propagations	: 451287
c inspects	: 1090687
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 220
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 922.027
c starts	: 212
c conflicts	: 84
c decisions	: 280160
c propagations	: 453346
c inspects	: 1095677
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 221
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 926.21
c starts	: 213
c conflicts	: 84
c decisions	: 281450
c propagations	: 455405
c inspects	: 1100668
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 222
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 930.374
c starts	: 214
c conflicts	: 84
c decisions	: 282740
c propagations	: 457464
c inspects	: 1105658
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 223
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 934.572
c starts	: 215
c conflicts	: 84
c decisions	: 284030
c propagations	: 459523
c inspects	: 1110649
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 224
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 938.734
c starts	: 216
c conflicts	: 84
c decisions	: 285320
c propagations	: 461582
c inspects	: 1115639
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 225
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 942.907
c starts	: 217
c conflicts	: 84
c decisions	: 286610
c propagations	: 463641
c inspects	: 1120630
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 226
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 947.081
c starts	: 218
c conflicts	: 84
c decisions	: 287900
c propagations	: 465700
c inspects	: 1125620
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 227
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 951.229
c starts	: 219
c conflicts	: 84
c decisions	: 289190
c propagations	: 467759
c inspects	: 1130610
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 228
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 955.413
c starts	: 220
c conflicts	: 84
c decisions	: 290480
c propagations	: 469818
c inspects	: 1135600
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 229
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 959.597
c starts	: 221
c conflicts	: 84
c decisions	: 291770
c propagations	: 471877
c inspects	: 1140591
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 230
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 963.745
c starts	: 222
c conflicts	: 84
c decisions	: 293060
c propagations	: 473936
c inspects	: 1145581
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 231
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 967.929
c starts	: 223
c conflicts	: 84
c decisions	: 294350
c propagations	: 475995
c inspects	: 1150571
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 232
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 972.085
c starts	: 224
c conflicts	: 84
c decisions	: 295640
c propagations	: 478054
c inspects	: 1155562
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 233
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 976.259
c starts	: 225
c conflicts	: 84
c decisions	: 296930
c propagations	: 480113
c inspects	: 1160552
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 234
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 980.438
c starts	: 226
c conflicts	: 84
c decisions	: 298220
c propagations	: 482172
c inspects	: 1165543
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 235
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 984.592
c starts	: 227
c conflicts	: 84
c decisions	: 299510
c propagations	: 484231
c inspects	: 1170533
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 236
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 988.8
c starts	: 228
c conflicts	: 84
c decisions	: 300800
c propagations	: 486290
c inspects	: 1175523
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 237
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 993.012
c starts	: 229
c conflicts	: 84
c decisions	: 302090
c propagations	: 488349
c inspects	: 1180513
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 238
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 997.195
c starts	: 230
c conflicts	: 84
c decisions	: 303380
c propagations	: 490408
c inspects	: 1185503
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 239
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1001.396
c starts	: 231
c conflicts	: 84
c decisions	: 304670
c propagations	: 492467
c inspects	: 1190493
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 240
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1005.575
c starts	: 232
c conflicts	: 84
c decisions	: 305960
c propagations	: 494526
c inspects	: 1195483
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 241
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1009.764
c starts	: 233
c conflicts	: 84
c decisions	: 307250
c propagations	: 496585
c inspects	: 1200474
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 242
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1013.96
c starts	: 234
c conflicts	: 84
c decisions	: 308540
c propagations	: 498644
c inspects	: 1205465
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 243
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1018.138
c starts	: 235
c conflicts	: 84
c decisions	: 309830
c propagations	: 500703
c inspects	: 1210456
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 244
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1022.329
c starts	: 236
c conflicts	: 84
c decisions	: 311120
c propagations	: 502762
c inspects	: 1215447
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 245
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1026.505
c starts	: 237
c conflicts	: 84
c decisions	: 312410
c propagations	: 504821
c inspects	: 1220438
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 246
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1030.676
c starts	: 238
c conflicts	: 84
c decisions	: 313700
c propagations	: 506880
c inspects	: 1225428
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 247
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1034.853
c starts	: 239
c conflicts	: 84
c decisions	: 314990
c propagations	: 508939
c inspects	: 1230418
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 248
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1039.015
c starts	: 240
c conflicts	: 84
c decisions	: 316280
c propagations	: 510998
c inspects	: 1235409
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 249
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1043.203
c starts	: 241
c conflicts	: 84
c decisions	: 317570
c propagations	: 513057
c inspects	: 1240399
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 250
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1047.397
c starts	: 242
c conflicts	: 84
c decisions	: 318860
c propagations	: 515116
c inspects	: 1245390
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 251
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1051.546
c starts	: 243
c conflicts	: 84
c decisions	: 320150
c propagations	: 517175
c inspects	: 1250381
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 252
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1055.757
c starts	: 244
c conflicts	: 84
c decisions	: 321440
c propagations	: 519234
c inspects	: 1255372
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 253
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1059.934
c starts	: 245
c conflicts	: 84
c decisions	: 322730
c propagations	: 521293
c inspects	: 1260363
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 254
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1064.095
c starts	: 246
c conflicts	: 84
c decisions	: 324020
c propagations	: 523352
c inspects	: 1265354
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 255
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1068.281
c starts	: 247
c conflicts	: 84
c decisions	: 325310
c propagations	: 525411
c inspects	: 1270344
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 256
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1072.445
c starts	: 248
c conflicts	: 84
c decisions	: 326600
c propagations	: 527470
c inspects	: 1275335
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 257
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1076.628
c starts	: 249
c conflicts	: 84
c decisions	: 327890
c propagations	: 529529
c inspects	: 1280325
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 258
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1080.813
c starts	: 250
c conflicts	: 84
c decisions	: 329180
c propagations	: 531588
c inspects	: 1285315
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 259
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1084.984
c starts	: 251
c conflicts	: 84
c decisions	: 330470
c propagations	: 533647
c inspects	: 1290306
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 260
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1089.174
c starts	: 252
c conflicts	: 84
c decisions	: 331760
c propagations	: 535706
c inspects	: 1295297
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 261
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1093.374
c starts	: 253
c conflicts	: 84
c decisions	: 333050
c propagations	: 537765
c inspects	: 1300287
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 262
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1097.546
c starts	: 254
c conflicts	: 84
c decisions	: 334340
c propagations	: 539824
c inspects	: 1305278
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 263
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1101.75
c starts	: 255
c conflicts	: 84
c decisions	: 335630
c propagations	: 541883
c inspects	: 1310269
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 264
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1105.894
c starts	: 256
c conflicts	: 84
c decisions	: 336920
c propagations	: 543942
c inspects	: 1315259
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 265
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1110.089
c starts	: 257
c conflicts	: 84
c decisions	: 338210
c propagations	: 546001
c inspects	: 1320250
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 266
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1114.293
c starts	: 258
c conflicts	: 84
c decisions	: 339500
c propagations	: 548060
c inspects	: 1325240
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 267
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1118.463
c starts	: 259
c conflicts	: 84
c decisions	: 340790
c propagations	: 550119
c inspects	: 1330231
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 268
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1122.676
c starts	: 260
c conflicts	: 84
c decisions	: 342080
c propagations	: 552178
c inspects	: 1335222
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 269
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1126.88
c starts	: 261
c conflicts	: 84
c decisions	: 343370
c propagations	: 554237
c inspects	: 1340213
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 270
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1131.057
c starts	: 262
c conflicts	: 84
c decisions	: 344660
c propagations	: 556296
c inspects	: 1345203
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 271
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1135.238
c starts	: 263
c conflicts	: 84
c decisions	: 345950
c propagations	: 558355
c inspects	: 1350193
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 272
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1139.431
c starts	: 264
c conflicts	: 84
c decisions	: 347240
c propagations	: 560414
c inspects	: 1355183
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 273
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1143.641
c starts	: 265
c conflicts	: 84
c decisions	: 348530
c propagations	: 562473
c inspects	: 1360173
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 274
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1147.832
c starts	: 266
c conflicts	: 84
c decisions	: 349820
c propagations	: 564532
c inspects	: 1365163
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 275
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1152.004
c starts	: 267
c conflicts	: 84
c decisions	: 351110
c propagations	: 566591
c inspects	: 1370153
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 276
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1156.185
c starts	: 268
c conflicts	: 84
c decisions	: 352400
c propagations	: 568650
c inspects	: 1375144
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 277
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1160.367
c starts	: 269
c conflicts	: 84
c decisions	: 353690
c propagations	: 570709
c inspects	: 1380135
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 278
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1164.542
c starts	: 270
c conflicts	: 84
c decisions	: 354980
c propagations	: 572768
c inspects	: 1385125
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 279
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1168.728
c starts	: 271
c conflicts	: 84
c decisions	: 356270
c propagations	: 574827
c inspects	: 1390116
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 280
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1172.895
c starts	: 272
c conflicts	: 84
c decisions	: 357560
c propagations	: 576886
c inspects	: 1395107
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 281
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1177.089
c starts	: 273
c conflicts	: 84
c decisions	: 358850
c propagations	: 578945
c inspects	: 1400098
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 282
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1181.298
c starts	: 274
c conflicts	: 84
c decisions	: 360140
c propagations	: 581004
c inspects	: 1405088
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 283
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1185.48
c starts	: 275
c conflicts	: 84
c decisions	: 361430
c propagations	: 583063
c inspects	: 1410078
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 284
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1189.665
c starts	: 276
c conflicts	: 84
c decisions	: 362720
c propagations	: 585122
c inspects	: 1415069
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 285
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1193.863
c starts	: 277
c conflicts	: 84
c decisions	: 364010
c propagations	: 587181
c inspects	: 1420060
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 286
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1198.035
c starts	: 278
c conflicts	: 84
c decisions	: 365300
c propagations	: 589240
c inspects	: 1425050
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 287
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1202.231
c starts	: 279
c conflicts	: 84
c decisions	: 366590
c propagations	: 591299
c inspects	: 1430041
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 288
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1206.403
c starts	: 280
c conflicts	: 84
c decisions	: 367880
c propagations	: 593358
c inspects	: 1435031
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 289
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1210.6
c starts	: 281
c conflicts	: 84
c decisions	: 369170
c propagations	: 595417
c inspects	: 1440021
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 290
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1214.803
c starts	: 282
c conflicts	: 84
c decisions	: 370460
c propagations	: 597476
c inspects	: 1445011
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 291
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1219.042
c starts	: 283
c conflicts	: 84
c decisions	: 371750
c propagations	: 599535
c inspects	: 1450001
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 292
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1223.205
c starts	: 284
c conflicts	: 84
c decisions	: 373040
c propagations	: 601594
c inspects	: 1454992
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 293
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1227.317
c starts	: 285
c conflicts	: 84
c decisions	: 374330
c propagations	: 603653
c inspects	: 1459982
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 294
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1231.433
c starts	: 286
c conflicts	: 84
c decisions	: 375620
c propagations	: 605712
c inspects	: 1464973
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 295
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1235.586
c starts	: 287
c conflicts	: 84
c decisions	: 376910
c propagations	: 607771
c inspects	: 1469963
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 296
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1239.763
c starts	: 288
c conflicts	: 84
c decisions	: 378200
c propagations	: 609830
c inspects	: 1474954
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 297
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1243.896
c starts	: 289
c conflicts	: 84
c decisions	: 379490
c propagations	: 611889
c inspects	: 1479945
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 298
c 
c CURRENT OPTIMUM=1713208429
c Current CPU time (ms) : 1248.081
c starts	: 290
c conflicts	: 84
c decisions	: 380780
c propagations	: 613948
c inspects	: 1484935
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 84
c root simplifications	: 299
#### 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.62 0.90 0.90 2/54 15071
Raw data (stat): 15071 (runsolver) R 15070 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543293310 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.83 0.94 0.91 4/64 15081
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18068 0 1 0 753 40 0 0 25 0 11 0 543293310 862662656 21063 4294967295 134512640 134569956 3221224400 3221214752 1131245957 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210611 21063 13073 16 0 210595 0
vsize: 842444
[startup+20.0009 s]
Raw data (loadavg): 0.86 0.94 0.91 3/64 15082
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18070 3 1 0 1672 40 0 0 25 0 11 0 543293310 859406336 20735 4294967295 134512640 134569956 3221224400 3221214680 1131254690 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209816 20735 13073 16 0 209800 0
vsize: 839264
[startup+30.0852 s]
Raw data (loadavg): 0.88 0.94 0.91 4/64 15084
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18071 3 1 0 2605 40 0 0 25 0 11 0 543293310 865878016 22411 4294967295 134512640 134569956 3221224400 3221214004 1073952732 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211396 22411 13073 16 0 211380 0
vsize: 845584
[startup+40.0855 s]
Raw data (loadavg): 0.90 0.94 0.91 2/64 15085
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18071 3 1 0 3519 41 0 0 24 0 11 0 543293310 862552064 21979 4294967295 134512640 134569956 3221224400 3221214664 1131254306 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 21979 13073 16 0 210568 0
vsize: 842336
[startup+50.0862 s]
Raw data (loadavg): 0.91 0.94 0.91 2/64 15086
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18071 3 1 0 4468 41 0 0 25 0 11 0 543293310 862552064 22434 4294967295 134512640 134569956 3221224400 3221214760 1131299760 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 22434 13073 16 0 210568 0
vsize: 842336
[startup+60.0865 s]
Raw data (loadavg): 0.93 0.95 0.91 2/64 15087
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18071 3 1 0 5433 41 0 0 25 0 11 0 543293310 862552064 22542 4294967295 134512640 134569956 3221224400 3221214664 1131254220 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 22542 13073 16 0 210568 0
vsize: 842336
[startup+70.0869 s]
Raw data (loadavg): 0.94 0.95 0.91 2/64 15089
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 6400 42 0 0 25 0 11 0 543293310 862552064 22649 4294967295 134512640 134569956 3221224400 3221214808 1131300777 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 22649 13073 16 0 210568 0
vsize: 842336
[startup+80.0882 s]
Raw data (loadavg): 0.95 0.95 0.91 2/64 15091
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 7372 42 0 0 25 0 11 0 543293310 862552064 22755 4294967295 134512640 134569956 3221224400 3221214808 1131300987 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 22755 13073 16 0 210568 0
vsize: 842336
[startup+90.0889 s]
Raw data (loadavg): 0.95 0.95 0.91 2/64 15093
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 8341 43 0 0 25 0 11 0 543293310 862552064 22843 4294967295 134512640 134569956 3221224400 3221214712 1131254201 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 22843 13073 16 0 210568 0
vsize: 842336
[startup+100.089 s]
Raw data (loadavg): 0.96 0.95 0.91 2/64 15095
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 9311 43 0 0 25 0 11 0 543293310 862552064 22934 4294967295 134512640 134569956 3221224400 3221214712 1131254245 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 22934 13073 16 0 210568 0
vsize: 842336
[startup+110.09 s]
Raw data (loadavg): 0.97 0.95 0.91 2/64 15097
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 10286 43 1 0 25 0 11 0 543293310 862552064 23019 4294967295 134512640 134569956 3221224400 3221214712 1131254205 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 23019 13073 16 0 210568 0
vsize: 842336
[startup+120.09 s]
Raw data (loadavg): 0.97 0.95 0.91 2/64 15099
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 11257 43 1 0 25 0 11 0 543293310 862552064 23105 4294967295 134512640 134569956 3221224400 3221214592 1131631185 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 23105 13073 16 0 210568 0
vsize: 842336
[startup+130.091 s]
Raw data (loadavg): 0.98 0.95 0.91 2/64 15102
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 12228 44 1 0 25 0 11 0 543293310 862552064 23190 4294967295 134512640 134569956 3221224400 3221214808 1131301854 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 23190 13073 16 0 210568 0
vsize: 842336
[startup+140.092 s]
Raw data (loadavg): 0.98 0.95 0.91 2/64 15104
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 13201 44 1 0 25 0 11 0 543293310 862552064 23308 4294967295 134512640 134569956 3221224400 3221214712 1131255523 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 23308 13073 16 0 210568 0
vsize: 842336
[startup+150.093 s]
Raw data (loadavg): 0.98 0.95 0.91 2/64 15106
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 14172 44 1 0 25 0 11 0 543293310 862552064 23408 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 23408 13073 16 0 210568 0
vsize: 842336
[startup+160.092 s]
Raw data (loadavg): 0.98 0.96 0.91 2/64 15108
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 15141 45 1 0 25 0 11 0 543293310 862552064 23501 4294967295 134512640 134569956 3221224400 3221214808 1131299852 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 23501 13073 16 0 210568 0
vsize: 842336
[startup+170.093 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 15110
Raw data (stat): 15071 (java) S 15070 11931 11930 0 -1 0 18072 3 1 0 16112 45 1 0 25 0 11 0 543293310 862552064 23586 4294967295 134512640 134569956 3221224400 3221213416 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 23586 13073 16 0 210568 0
vsize: 842336
[startup+180.094 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 15112
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 17083 46 1 0 24 0 11 0 543293310 862552064 23737 4294967295 134512640 134569956 3221224400 3221214712 1131254302 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 23737 13073 16 0 210568 0
vsize: 842336
[startup+190.096 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 15115
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 18052 47 1 0 25 0 11 0 543293310 862552064 23868 4294967295 134512640 134569956 3221224400 3221214808 1131301032 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 23868 13073 16 0 210568 0
vsize: 842336
[startup+200.096 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 15117
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 19023 47 1 0 25 0 11 0 543293310 862552064 23943 4294967295 134512640 134569956 3221224400 3221214808 1131302453 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 23943 13073 16 0 210568 0
vsize: 842336
[startup+210.096 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 15119
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 19992 47 1 0 25 0 11 0 543293310 862552064 24066 4294967295 134512640 134569956 3221224400 3221214784 1131245620 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 24066 13073 16 0 210568 0
vsize: 842336
[startup+220.097 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 15122
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 20958 48 1 0 24 0 11 0 543293310 862552064 24146 4294967295 134512640 134569956 3221224400 3221214808 1131302428 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 24146 13073 16 0 210568 0
vsize: 842336
[startup+230.097 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 15124
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 21921 48 2 0 25 0 11 0 543293310 862552064 24270 4294967295 134512640 134569956 3221224400 3221214712 1131255698 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 24270 13073 16 0 210568 0
vsize: 842336
[startup+240.098 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 15127
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 22885 48 2 0 25 0 11 0 543293310 862552064 24380 4294967295 134512640 134569956 3221224400 3221214712 1131254213 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 24380 13073 16 0 210568 0
vsize: 842336
[startup+250.098 s]
Raw data (loadavg): 0.99 0.96 0.91 2/64 15129
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 23848 49 2 0 25 0 11 0 543293310 862552064 24612 4294967295 134512640 134569956 3221224400 3221214808 1131301023 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 24612 13073 16 0 210568 0
vsize: 842336
[startup+260.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15132
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 24816 49 2 0 25 0 11 0 543293310 862552064 24738 4294967295 134512640 134569956 3221224400 3221214712 1131254276 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 24738 13073 16 0 210568 0
vsize: 842336
[startup+270.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15134
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 25780 50 2 1 24 0 11 0 543293310 862552064 24825 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 24825 13073 16 0 210568 0
vsize: 842336
[startup+280.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 15136
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 26748 51 2 1 25 0 10 0 543293310 862552064 24940 4294967295 134512640 134569956 3221224400 3221214704 1131221825 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 24940 13073 16 0 210568 0
vsize: 842336
[startup+290.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15139
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 27715 51 2 1 25 0 11 0 543293310 862552064 25046 4294967295 134512640 134569956 3221224400 3221214712 1131254793 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 25046 13073 16 0 210568 0
vsize: 842336
[startup+300.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15141
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 28684 52 2 1 25 0 11 0 543293310 862552064 25143 4294967295 134512640 134569956 3221224400 3221214712 1131254213 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 25143 13073 16 0 210568 0
vsize: 842336
[startup+310.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15144
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 29650 52 2 1 24 0 11 0 543293310 862552064 25295 4294967295 134512640 134569956 3221224400 3221214712 1131254490 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 25295 13073 16 0 210568 0
vsize: 842336
[startup+320.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15146
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 30620 53 2 1 25 0 11 0 543293310 862552064 25380 4294967295 134512640 134569956 3221224400 3221214752 1131253136 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 25380 13073 16 0 210568 0
vsize: 842336
[startup+330.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15149
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 31591 53 2 1 25 0 11 0 543293310 862552064 25494 4294967295 134512640 134569956 3221224400 3221214808 1131299787 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 25494 13073 16 0 210568 0
vsize: 842336
[startup+340.105 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15151
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 32559 54 2 1 25 0 11 0 543293310 862552064 25567 4294967295 134512640 134569956 3221224400 3221214712 1131254680 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 25567 13073 16 0 210568 0
vsize: 842336
[startup+350.106 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15154
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 33530 54 2 1 25 0 11 0 543293310 862552064 25661 4294967295 134512640 134569956 3221224400 3221214752 1131253142 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 25661 13073 16 0 210568 0
vsize: 842336
[startup+360.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15156
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 34499 54 2 1 25 0 11 0 543293310 862552064 25739 4294967295 134512640 134569956 3221224400 3221214752 1131253081 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 25739 13073 16 0 210568 0
vsize: 842336
[startup+370.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15159
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 35457 55 3 1 25 0 11 0 543293310 862552064 25847 4294967295 134512640 134569956 3221224400 3221214712 1131254209 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 25847 13073 16 0 210568 0
vsize: 842336
[startup+380.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15161
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 36417 55 3 1 25 0 11 0 543293310 862552064 25922 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 25922 13073 16 0 210568 0
vsize: 842336
[startup+390.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15163
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 37378 55 3 1 25 0 11 0 543293310 862552064 26380 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 26380 13073 16 0 210568 0
vsize: 842336
[startup+400.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15166
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 38344 55 3 1 24 0 11 0 543293310 862552064 26451 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 26451 13073 16 0 210568 0
vsize: 842336
[startup+410.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15168
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 39313 56 3 1 25 0 11 0 543293310 862552064 26566 4294967295 134512640 134569956 3221224400 3221214712 1131255192 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 26566 13073 16 0 210568 0
vsize: 842336
[startup+420.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15171
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 40280 56 3 1 25 0 11 0 543293310 862552064 26646 4294967295 134512640 134569956 3221224400 3221214712 1131254302 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 26646 13073 16 0 210568 0
vsize: 842336
[startup+430.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15173
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 41243 56 4 1 24 0 11 0 543293310 862552064 26733 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 26733 13073 16 0 210568 0
vsize: 842336
[startup+440.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15176
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 42206 56 4 1 25 0 11 0 543293310 862552064 26866 4294967295 134512640 134569956 3221224400 3221214808 1131301831 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 26866 13073 16 0 210568 0
vsize: 842336
[startup+450.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15178
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 43168 56 4 1 25 0 11 0 543293310 862552064 26957 4294967295 134512640 134569956 3221224400 3221214712 1131255511 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 26957 13073 16 0 210568 0
vsize: 842336
[startup+460.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15181
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 44131 57 4 1 25 0 11 0 543293310 862552064 27105 4294967295 134512640 134569956 3221224400 3221214848 1131539318 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 27105 13073 16 0 210568 0
vsize: 842336
[startup+470.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15183
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 45095 57 4 1 25 0 11 0 543293310 862552064 27231 4294967295 134512640 134569956 3221224400 3221214712 1131254276 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 27231 13073 16 0 210568 0
vsize: 842336
[startup+480.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15185
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 46059 58 4 1 24 0 11 0 543293310 862552064 27356 4294967295 134512640 134569956 3221224400 3221214712 1131254245 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 27356 13073 16 0 210568 0
vsize: 842336
[startup+490.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15188
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 47027 58 4 1 25 0 11 0 543293310 862552064 27449 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 27449 13073 16 0 210568 0
vsize: 842336
[startup+500.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15190
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 47996 58 5 1 25 0 11 0 543293310 862552064 27553 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 27553 13073 16 0 210568 0
vsize: 842336
[startup+510.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15193
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 48963 59 5 2 25 0 11 0 543293310 862552064 27675 4294967295 134512640 134569956 3221224400 3221214712 1131254662 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 27675 13073 16 0 210568 0
vsize: 842336
[startup+520.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15195
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 49929 59 5 2 25 0 11 0 543293310 862552064 27776 4294967295 134512640 134569956 3221224400 3221214712 1131254213 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 27776 13073 16 0 210568 0
vsize: 842336
[startup+530.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15197
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 50895 60 5 2 25 0 11 0 543293310 862552064 27883 4294967295 134512640 134569956 3221224400 3221214712 1131254413 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 27883 13073 16 0 210568 0
vsize: 842336
[startup+540.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15200
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 51863 60 5 2 25 0 11 0 543293310 862552064 28038 4294967295 134512640 134569956 3221224400 3221214712 1131254245 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 28038 13073 16 0 210568 0
vsize: 842336
[startup+550.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15202
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 52830 61 5 2 24 0 11 0 543293310 862552064 28131 4294967295 134512640 134569956 3221224400 3221214712 1131254245 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 28131 13073 16 0 210568 0
vsize: 842336
[startup+560.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15205
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 53799 61 5 2 25 0 11 0 543293310 862552064 28253 4294967295 134512640 134569956 3221224400 3221214712 1131254220 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 28253 13073 16 0 210568 0
vsize: 842336
[startup+570.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15207
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 54769 62 5 2 25 0 11 0 543293310 862552064 28310 4294967295 134512640 134569956 3221224400 3221214808 1131299791 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 28310 13073 16 0 210568 0
vsize: 842336
[startup+580.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15210
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 55738 62 6 2 25 0 11 0 543293310 862552064 28425 4294967295 134512640 134569956 3221224400 3221214712 1131255477 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 28425 13073 16 0 210568 0
vsize: 842336
[startup+590.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15212
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 56703 62 6 2 24 0 11 0 543293310 862552064 28500 4294967295 134512640 134569956 3221224400 3221214712 1131254295 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 28500 13073 16 0 210568 0
vsize: 842336
[startup+600.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15214
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 57672 62 6 2 25 0 11 0 543293310 862552064 28646 4294967295 134512640 134569956 3221224400 3221214712 1131255184 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 28646 13073 16 0 210568 0
vsize: 842336
[startup+610.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15217
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 58643 63 6 2 25 0 11 0 543293310 862552064 28710 4294967295 134512640 134569956 3221224400 3221214808 1131299787 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 28710 13073 16 0 210568 0
vsize: 842336
[startup+620.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15219
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 59611 63 6 2 24 0 11 0 543293310 862552064 28809 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 28809 13073 16 0 210568 0
vsize: 842336
[startup+630.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15222
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 60581 64 6 2 25 0 11 0 543293310 862552064 28866 4294967295 134512640 134569956 3221224400 3221214712 1131254209 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 28866 13073 16 0 210568 0
vsize: 842336
[startup+640.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15224
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 61550 64 6 2 25 0 11 0 543293310 862552064 28930 4294967295 134512640 134569956 3221224400 3221214712 1131254213 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 28930 13073 16 0 210568 0
vsize: 842336
[startup+650.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15227
Raw data (stat): 15071 (java) S 15070 11931 11930 0 -1 0 18072 3 1 0 62509 64 6 2 25 0 11 0 543293310 862552064 29225 4294967295 134512640 134569956 3221224400 3221213456 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 29225 13073 16 0 210568 0
vsize: 842336
[startup+660.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15229
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 63460 64 6 2 24 0 11 0 543293310 862552064 29385 4294967295 134512640 134569956 3221224400 3221214712 1131254220 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 29385 13073 16 0 210568 0
vsize: 842336
[startup+670.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15231
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 64410 64 6 2 25 0 11 0 543293310 862552064 29594 4294967295 134512640 134569956 3221224400 3221214712 1131254793 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 29594 13073 16 0 210568 0
vsize: 842336
[startup+680.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15234
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 65370 64 6 2 25 0 11 0 543293310 862552064 30219 4294967295 134512640 134569956 3221224400 3221214808 1131299787 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 30219 13073 16 0 210568 0
vsize: 842336
[startup+690.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15236
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 66336 64 6 3 25 0 11 0 543293310 862552064 30371 4294967295 134512640 134569956 3221224400 3221214712 1131254793 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 30371 13073 16 0 210568 0
vsize: 842336
[startup+700.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15239
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 67302 64 6 3 24 0 11 0 543293310 862552064 30499 4294967295 134512640 134569956 3221224400 3221214808 1131301816 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 30499 13073 16 0 210568 0
vsize: 842336
[startup+710.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15241
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 68271 65 6 3 25 0 11 0 543293310 862552064 30604 4294967295 134512640 134569956 3221224400 3221214808 1131301048 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 30604 13073 16 0 210568 0
vsize: 842336
[startup+720.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15244
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 69240 65 6 3 25 0 11 0 543293310 862552064 30712 4294967295 134512640 134569956 3221224400 3221214752 1131253212 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 30712 13073 16 0 210568 0
vsize: 842336
[startup+730.143 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15246
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 70207 65 6 3 24 0 11 0 543293310 862552064 30781 4294967295 134512640 134569956 3221224400 3221214804 1131254188 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 30781 13073 16 0 210568 0
vsize: 842336
[startup+740.143 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15249
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 71176 66 6 3 25 0 11 0 543293310 862552064 30878 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 30878 13073 16 0 210568 0
vsize: 842336
[startup+750.144 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15251
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 72145 66 6 3 25 0 11 0 543293310 862552064 30946 4294967295 134512640 134569956 3221224400 3221214712 1131255452 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 30946 13073 16 0 210568 0
vsize: 842336
[startup+760.146 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15253
Raw data (stat): 15071 (java) S 15070 11931 11930 0 -1 0 18072 3 1 0 73113 66 7 3 25 0 11 0 543293310 862552064 31070 4294967295 134512640 134569956 3221224400 3221213416 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 31070 13073 16 0 210568 0
vsize: 842336
[startup+770.147 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15256
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 74080 66 7 3 25 0 11 0 543293310 862552064 31163 4294967295 134512640 134569956 3221224400 3221214712 1131254308 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 31163 13073 16 0 210568 0
vsize: 842336
[startup+780.148 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15258
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 75049 66 7 3 25 0 11 0 543293310 862552064 31253 4294967295 134512640 134569956 3221224400 3221214808 1131301797 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 31253 13073 16 0 210568 0
vsize: 842336
[startup+790.147 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15261
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 76017 67 7 3 25 0 11 0 543293310 862552064 31333 4294967295 134512640 134569956 3221224400 3221214808 1131300908 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 31333 13073 16 0 210568 0
vsize: 842336
[startup+800.148 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15263
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 76980 67 7 3 24 0 11 0 543293310 862552064 31392 4294967295 134512640 134569956 3221224400 3221214752 1131253081 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 31392 13073 16 0 210568 0
vsize: 842336
[startup+810.148 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15266
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 77944 67 7 3 25 0 11 0 543293310 862552064 31529 4294967295 134512640 134569956 3221224400 3221214808 1131302488 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 31529 13073 16 0 210568 0
vsize: 842336
[startup+820.148 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15268
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 78906 67 7 3 25 0 11 0 543293310 862552064 31655 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 31655 13073 16 0 210568 0
vsize: 842336
[startup+830.149 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15270
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 79868 68 7 3 25 0 11 0 543293310 862552064 31782 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 31782 13073 16 0 210568 0
vsize: 842336
[startup+840.149 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15273
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 80824 68 7 4 25 0 11 0 543293310 862552064 31888 4294967295 134512640 134569956 3221224400 3221214712 1131254308 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 31888 13073 16 0 210568 0
vsize: 842336
[startup+850.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15275
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 81779 69 7 4 23 0 11 0 543293310 862552064 32010 4294967295 134512640 134569956 3221224400 3221214712 1131254276 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 32010 13073 16 0 210568 0
vsize: 842336
[startup+860.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15278
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 82734 69 7 4 20 0 11 0 543293310 862552064 32144 4294967295 134512640 134569956 3221224400 3221214712 1131254576 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 32144 13073 16 0 210568 0
vsize: 842336
[startup+870.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15280
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 83695 70 7 4 25 0 11 0 543293310 862552064 32322 4294967295 134512640 134569956 3221224400 3221214712 1131254245 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 32322 13073 16 0 210568 0
vsize: 842336
[startup+880.152 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15282
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 84659 70 7 4 25 0 11 0 543293310 862552064 32509 4294967295 134512640 134569956 3221224400 3221214712 1131254721 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 32509 13073 16 0 210568 0
vsize: 842336
[startup+890.152 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15285
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 85625 71 7 4 25 0 11 0 543293310 862552064 32586 4294967295 134512640 134569956 3221224400 3221214808 1131299780 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 32586 13073 16 0 210568 0
vsize: 842336
[startup+900.152 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15287
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 86590 71 8 4 25 0 11 0 543293310 862552064 32717 4294967295 134512640 134569956 3221224400 3221214752 1131253106 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 32717 13073 16 0 210568 0
vsize: 842336
[startup+910.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15290
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 87555 71 8 4 25 0 11 0 543293310 862552064 32819 4294967295 134512640 134569956 3221224400 3221214848 1131539205 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 32819 13073 16 0 210568 0
vsize: 842336
[startup+920.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15292
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 88520 72 8 4 25 0 11 0 543293310 862552064 32984 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 32984 13073 16 0 210568 0
vsize: 842336
[startup+930.154 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15294
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 89486 72 8 4 25 0 11 0 543293310 862552064 33064 4294967295 134512640 134569956 3221224400 3221214712 1131254655 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 33064 13073 16 0 210568 0
vsize: 842336
[startup+940.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15297
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 90452 73 8 4 25 0 11 0 543293310 862552064 33185 4294967295 134512640 134569956 3221224400 3221214712 1131255530 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 33185 13073 16 0 210568 0
vsize: 842336
[startup+950.162 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15299
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 91422 73 8 4 25 0 11 0 543293310 862552064 33289 4294967295 134512640 134569956 3221224400 3221214712 1131254793 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 33289 13073 16 0 210568 0
vsize: 842336
[startup+960.162 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15301
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 92386 74 8 4 24 0 11 0 543293310 862552064 33385 4294967295 134512640 134569956 3221224400 3221214808 1131300861 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 33385 13073 16 0 210568 0
vsize: 842336
[startup+970.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15304
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 93354 75 9 4 24 0 11 0 543293310 862552064 33472 4294967295 134512640 134569956 3221224400 3221214712 1131254205 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 33472 13073 16 0 210568 0
vsize: 842336
[startup+980.177 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15306
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 94322 75 9 4 25 0 11 0 543293310 862552064 33586 4294967295 134512640 134569956 3221224400 3221214712 1131254413 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 33586 13073 16 0 210568 0
vsize: 842336
[startup+990.177 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15309
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 95287 76 9 4 25 0 11 0 543293310 862552064 33646 4294967295 134512640 134569956 3221224400 3221214712 1131255482 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 33646 13073 16 0 210568 0
vsize: 842336
[startup+1000.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15311
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 96250 76 9 4 25 0 11 0 543293310 862552064 33720 4294967295 134512640 134569956 3221224400 3221214712 1131254793 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 33720 13073 16 0 210568 0
vsize: 842336
[startup+1010.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15313
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 97214 77 9 4 25 0 11 0 543293310 862552064 33900 4294967295 134512640 134569956 3221224400 3221214712 1131255462 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 33900 13073 16 0 210568 0
vsize: 842336
[startup+1020.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15316
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 98178 77 9 4 25 0 11 0 543293310 862552064 34076 4294967295 134512640 134569956 3221224400 3221214712 1131254628 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 34076 13073 16 0 210568 0
vsize: 842336
[startup+1030.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15318
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 99145 77 10 4 25 0 11 0 543293310 862552064 34157 4294967295 134512640 134569956 3221224400 3221214712 1131254863 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 34157 13073 16 0 210568 0
vsize: 842336
[startup+1040.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15321
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 100113 78 10 4 25 0 11 0 543293310 862552064 34289 4294967295 134512640 134569956 3221224400 3221214712 1131254902 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210584 34289 13073 16 0 210568 0
vsize: 842336
[startup+1050.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15323
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 101082 78 10 5 25 0 11 0 543293310 862552064 34345 4294967295 134512640 134569956 3221224400 3221214712 1131254740 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 34345 13073 16 0 210568 0
vsize: 842336
[startup+1060.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15325
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 102050 78 10 5 25 0 11 0 543293310 862552064 34453 4294967295 134512640 134569956 3221224400 3221214712 1131254287 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 34453 13073 16 0 210568 0
vsize: 842336
[startup+1070.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15328
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 103019 79 10 5 25 0 11 0 543293310 862552064 34551 4294967295 134512640 134569956 3221224400 3221214752 1131253081 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 34551 13073 16 0 210568 0
vsize: 842336
[startup+1080.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15330
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 103988 79 10 5 25 0 11 0 543293310 862552064 34610 4294967295 134512640 134569956 3221224400 3221214712 1131254213 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 34610 13073 16 0 210568 0
vsize: 842336
[startup+1090.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15333
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 104957 80 10 5 25 0 11 0 543293310 862552064 34695 4294967295 134512640 134569956 3221224400 3221214712 1131254401 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 34695 13073 16 0 210568 0
vsize: 842336
[startup+1100.31 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15335
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 105935 80 10 5 25 0 11 0 543293310 862552064 34753 4294967295 134512640 134569956 3221224400 3221214712 1131254801 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 34753 13073 16 0 210568 0
vsize: 842336
[startup+1110.32 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15337
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 106900 81 11 5 25 0 11 0 543293310 862552064 34881 4294967295 134512640 134569956 3221224400 3221214712 1131255407 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 34881 13073 16 0 210568 0
vsize: 842336
[startup+1120.32 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15340
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 107865 81 11 5 24 0 11 0 543293310 862552064 34944 4294967295 134512640 134569956 3221224400 3221214712 1131254302 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 34944 13073 16 0 210568 0
vsize: 842336
[startup+1130.34 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15342
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 108833 82 11 5 25 0 11 0 543293310 862552064 35049 4294967295 134512640 134569956 3221224400 3221214712 1131254793 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 35049 13073 16 0 210568 0
vsize: 842336
[startup+1140.36 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15345
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 109801 82 11 5 25 0 11 0 543293310 862552064 35163 4294967295 134512640 134569956 3221224400 3221214808 1131300908 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 35163 13073 16 0 210568 0
vsize: 842336
[startup+1150.36 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15347
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 110770 82 11 5 25 0 11 0 543293310 862552064 35272 4294967295 134512640 134569956 3221224400 3221214808 1131299787 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 35272 13073 16 0 210568 0
vsize: 842336
[startup+1160.36 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15349
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 111739 82 11 5 25 0 11 0 543293310 862552064 35382 4294967295 134512640 134569956 3221224400 3221214712 1131254884 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 35382 13073 16 0 210568 0
vsize: 842336
[startup+1170.36 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15352
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 112709 83 12 5 25 0 11 0 543293310 862552064 35438 4294967295 134512640 134569956 3221224400 3221214712 1131254595 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 35438 13073 16 0 210568 0
vsize: 842336
[startup+1180.36 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15354
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 113678 83 12 5 25 0 11 0 543293310 862552064 35494 4294967295 134512640 134569956 3221224400 3221214808 1131302468 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 35494 13073 16 0 210568 0
vsize: 842336
[startup+1190.36 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15357
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 114647 83 12 5 25 0 11 0 543293310 862552064 35590 4294967295 134512640 134569956 3221224400 3221214848 1131539357 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 35590 13073 16 0 210568 0
vsize: 842336
[startup+1200.36 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15359
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 115617 83 12 5 25 0 11 0 543293310 862552064 35646 4294967295 134512640 134569956 3221224400 3221214752 1131475245 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 35646 13073 16 0 210568 0
vsize: 842336
[startup+1210.36 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15361
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 116586 84 12 5 25 0 11 0 543293310 862552064 35715 4294967295 134512640 134569956 3221224400 3221214808 1131299567 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 35715 13073 16 0 210568 0
vsize: 842336
[startup+1220.37 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15364
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 117547 84 12 5 25 0 11 0 543293310 862552064 37596 4294967295 134512640 134569956 3221224400 3221214712 1131254692 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 37596 13073 16 0 210568 0
vsize: 842336
[startup+1230.37 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15366
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 118532 84 12 5 25 0 11 0 543293310 862552064 37596 4294967295 134512640 134569956 3221224400 3221214712 1131254220 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 37596 13073 16 0 210568 0
vsize: 842336
[startup+1240.37 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15368
Raw data (stat): 15071 (java) S 15070 11931 11930 0 -1 0 18072 3 1 0 119509 85 12 5 25 0 11 0 543293310 862552064 37596 4294967295 134512640 134569956 3221224400 3221213456 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 37596 13073 16 0 210568 0
vsize: 842336
[startup+1250.37 s]
Raw data (loadavg): 0.99 0.97 0.91 2/64 15371
Raw data (stat): 15071 (java) R 15070 11931 11930 0 -1 0 18072 3 1 0 120476 85 12 5 24 0 11 0 543293310 862552064 37624 4294967295 134512640 134569956 3221224400 3221214712 1131254641 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210584 37624 13073 16 0 210568 0
vsize: 842336
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1250.49 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 15373
Raw data (stat): 15071 (java) Z 15070 11931 11930 0 -1 1036 18072 26291 1 1 120481 92 5736 85 25 0 1 0 543293310 0 0 4294967295 0 0 0 0 0 0 4 3 23756 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 143
Real time (s): 1250.49
CPU time (s): 1263.97
CPU user time (s): 1262.19
CPU system time (s): 1.78473
CPU usage (%): 101.078
Max. virtual memory (Kb): 845584
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####