PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-bell3a.opb
MD5SUM	20897ed4b3cd94cc1a84b64d339b40e4
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	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 numbers	58
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1252.45
Number of variables	2219
Total number of constraints	194
Number of constraints which are clauses	22
Number of constraints which are cardinality constraints (but not clauses)	39
Number of constraints which are nor clauses,nor cardinality constraints	133
Minimum length of a constraint	1
Maximum length of a constraint	191
Trace number 22327

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        811396 kB
Buffers:          2164 kB
Cached:         201072 kB
SwapCached:       1444 kB
Active:          41496 kB
Inactive:       164108 kB
HighTotal:      131008 kB
HighFree:        39900 kB
LowTotal:       903652 kB
LowFree:        771496 kB
SwapTotal:     2097892 kB
SwapFree:      2095700 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4940 kB
Slab:            12004 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 03:15:24 (client local time) WITH STATUS 143 IN 1263.42 SECONDS
stats: 11696 7 1263.42 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-bell3a.opb
c reading problem 
c [nbvar=2219]
c [nbconstr=194]
c time 4.192
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.469
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) : 20.239
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.921
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) : 38.505
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) : 44.446
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) : 53.315
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) : 61.017
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) : 68.099
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) : 72.932
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) : 77.705
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) : 82.512
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) : 87.331
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) : 92.076
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) : 96.865
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) : 101.623
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) : 106.352
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) : 111.111
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) : 115.842
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) : 120.611
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) : 125.363
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) : 130.101
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) : 134.873
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) : 139.612
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) : 144.378
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) : 149.158
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) : 153.91
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) : 158.674
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) : 163.446
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) : 168.182
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) : 172.949
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) : 177.692
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) : 181.783
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) : 185.875
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) : 189.937
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) : 194.021
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) : 198.101
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) : 202.187
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) : 206.284
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) : 210.356
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) : 214.459
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) : 218.555
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) : 222.642
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) : 226.768
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.848
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.974
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) : 239.092
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) : 243.179
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) : 247.317
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) : 251.425
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) : 255.505
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) : 259.61
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.69
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.796
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.9
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.976
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) : 280.085
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) : 284.202
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) : 288.277
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) : 292.379
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) : 296.459
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.564
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.66
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.731
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.83
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.903
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) : 321.0
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) : 325.099
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) : 329.173
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) : 333.407
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) : 337.507
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) : 341.578
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) : 345.672
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) : 349.743
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) : 353.837
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.945
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) : 362.036
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) : 366.184
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) : 370.329
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) : 374.454
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) : 378.602
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) : 382.707
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) : 386.868
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) : 391.004
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) : 395.078
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) : 399.185
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) : 403.29
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) : 407.377
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) : 411.489
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) : 415.576
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) : 419.7
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) : 423.82
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) : 427.908
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) : 432.045
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) : 436.181
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) : 440.287
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) : 444.426
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) : 448.532
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) : 452.685
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) : 456.832
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) : 460.944
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) : 465.08
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) : 469.179
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) : 473.305
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) : 477.43
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) : 481.517
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) : 485.64
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) : 489.769
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) : 493.866
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) : 497.985
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) : 502.08
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) : 506.213
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) : 510.333
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) : 514.434
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) : 518.578
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) : 522.697
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) : 526.794
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) : 530.924
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) : 535.024
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) : 539.151
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) : 543.268
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) : 547.354
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) : 551.473
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) : 555.589
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) : 559.69
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.805
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.896
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) : 572.021
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) : 576.143
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) : 580.24
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) : 584.381
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) : 588.484
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) : 592.607
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) : 596.736
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) : 600.824
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) : 604.947
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) : 609.063
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) : 613.157
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) : 617.265
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) : 621.354
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) : 625.469
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) : 629.588
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) : 633.693
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) : 637.815
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) : 641.948
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) : 646.077
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) : 650.289
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) : 654.447
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) : 658.638
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) : 662.859
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) : 667.033
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) : 671.252
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) : 675.44
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) : 679.552
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) : 683.703
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) : 687.821
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) : 691.954
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) : 696.085
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) : 700.189
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) : 704.317
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) : 708.448
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) : 712.554
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) : 716.677
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) : 720.78
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) : 724.9
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) : 729.02
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) : 733.131
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) : 737.266
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) : 741.398
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) : 745.515
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) : 749.66
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) : 753.76
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) : 757.894
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) : 762.034
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) : 766.138
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) : 770.276
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) : 774.402
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) : 778.515
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) : 782.65
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) : 786.752
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) : 790.893
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) : 795.038
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) : 799.158
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) : 803.31
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) : 807.485
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) : 811.64
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) : 815.832
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) : 819.998
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) : 824.202
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) : 828.409
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) : 832.582
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) : 836.801
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) : 841.005
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) : 845.249
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) : 849.483
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) : 853.678
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) : 857.937
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) : 862.163
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) : 866.345
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) : 870.544
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) : 874.713
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) : 878.897
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) : 883.09
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) : 887.236
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) : 891.422
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) : 895.615
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) : 899.794
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) : 903.993
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) : 908.161
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) : 912.359
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) : 916.557
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) : 920.713
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) : 924.91
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) : 929.095
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) : 933.259
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) : 937.454
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) : 941.616
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) : 945.794
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) : 949.962
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) : 954.127
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) : 958.314
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) : 962.5
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) : 966.651
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) : 970.83
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) : 974.984
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) : 979.165
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) : 983.355
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) : 987.518
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) : 991.718
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) : 995.928
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) : 1000.104
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) : 1004.311
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) : 1008.478
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) : 1012.681
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) : 1016.88
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) : 1021.047
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) : 1025.236
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) : 1029.417
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) : 1033.585
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) : 1037.767
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) : 1041.925
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) : 1046.116
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) : 1050.312
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) : 1054.477
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) : 1058.673
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) : 1062.853
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) : 1067.015
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) : 1071.213
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) : 1075.365
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) : 1079.553
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) : 1083.743
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) : 1087.909
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) : 1092.109
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) : 1096.302
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) : 1100.47
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) : 1104.669
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) : 1108.83
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) : 1113.033
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) : 1117.233
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) : 1121.409
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) : 1125.618
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) : 1129.822
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) : 1133.998
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) : 1138.198
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) : 1142.377
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) : 1146.58
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) : 1150.776
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) : 1154.947
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) : 1159.132
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) : 1163.313
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) : 1167.486
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) : 1171.675
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) : 1175.844
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) : 1180.046
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) : 1184.248
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) : 1188.428
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) : 1192.632
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) : 1196.824
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) : 1200.994
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) : 1205.185
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) : 1209.352
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) : 1213.549
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) : 1217.746
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) : 1221.986
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) : 1226.167
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) : 1230.292
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) : 1234.424
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) : 1238.593
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) : 1242.779
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) : 1246.938
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
#### 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.78 0.95 0.93 2/55 28009
Raw data (stat): 28009 (runsolver) R 28008 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 427541956 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.98 0.98 0.94 3/65 28019
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18102 0 1 0 707 41 0 0 25 0 11 0 427541956 860987392 20715 4294967295 134512640 134569956 3221224400 3221214572 1130898680 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210202 20715 13073 16 0 210186 0
vsize: 840808
[startup+20.0012 s]
Raw data (loadavg): 1.13 1.02 0.95 2/65 28020
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18104 3 1 0 1617 41 0 0 25 0 11 0 427541956 861999104 21484 4294967295 134512640 134569956 3221224400 3221214776 1131293508 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210449 21484 13073 16 0 210433 0
vsize: 841796
[startup+30.0018 s]
Raw data (loadavg): 1.11 1.02 0.95 3/65 28022
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18105 3 1 0 2542 41 0 0 25 0 11 0 427541956 865144832 22357 4294967295 134512640 134569956 3221224400 3221213728 1073952732 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211217 22357 13073 16 0 211201 0
vsize: 844868
[startup+40.0019 s]
Raw data (loadavg): 1.16 1.03 0.96 2/65 28023
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 3454 42 0 0 25 0 11 0 427541956 865841152 22726 4294967295 134512640 134569956 3221224400 3221214664 1131278605 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 22726 13073 16 0 211371 0
vsize: 845548
[startup+50.0022 s]
Raw data (loadavg): 1.14 1.03 0.96 3/65 28024
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 4396 42 0 0 25 0 11 0 427541956 865841152 23208 4294967295 134512640 134569956 3221224400 3221214404 1131711488 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 23208 13073 16 0 211371 0
vsize: 845548
[startup+60.0018 s]
Raw data (loadavg): 1.12 1.03 0.96 2/65 28025
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 5364 42 0 0 25 0 11 0 427541956 865841152 23298 4294967295 134512640 134569956 3221224400 3221214664 1131278192 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 23298 13073 16 0 211371 0
vsize: 845548
[startup+70.0025 s]
Raw data (loadavg): 1.10 1.03 0.96 2/65 28027
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 6333 42 0 0 25 0 11 0 427541956 865841152 23382 4294967295 134512640 134569956 3221224400 3221214712 1131277981 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 23382 13073 16 0 211371 0
vsize: 845548
[startup+80.0033 s]
Raw data (loadavg): 1.08 1.03 0.96 2/65 28029
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 7301 42 0 0 25 0 11 0 427541956 865841152 23499 4294967295 134512640 134569956 3221224400 3221214712 1131278405 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 23499 13073 16 0 211371 0
vsize: 845548
[startup+90.003 s]
Raw data (loadavg): 1.07 1.03 0.96 2/65 28031
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 8271 43 0 0 25 0 11 0 427541956 865841152 23584 4294967295 134512640 134569956 3221224400 3221214712 1131278066 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 23584 13073 16 0 211371 0
vsize: 845548
[startup+100.004 s]
Raw data (loadavg): 1.06 1.02 0.96 2/65 28033
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 9244 43 1 0 25 0 11 0 427541956 865841152 23644 4294967295 134512640 134569956 3221224400 3221214732 1131711520 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 23644 13073 16 0 211371 0
vsize: 845548
[startup+110.004 s]
Raw data (loadavg): 1.05 1.02 0.96 2/65 28035
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 10216 43 1 0 25 0 11 0 427541956 865841152 23722 4294967295 134512640 134569956 3221224400 3221214712 1131278315 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 23722 13073 16 0 211371 0
vsize: 845548
[startup+120.005 s]
Raw data (loadavg): 1.04 1.02 0.96 2/65 28037
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 11187 43 1 0 25 0 11 0 427541956 865841152 23818 4294967295 134512640 134569956 3221224400 3221214712 1131278605 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 23818 13073 16 0 211371 0
vsize: 845548
[startup+130.005 s]
Raw data (loadavg): 1.03 1.02 0.96 2/65 28039
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 12159 44 1 0 24 0 11 0 427541956 865841152 23929 4294967295 134512640 134569956 3221224400 3221214712 1131278519 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 23929 13073 16 0 211371 0
vsize: 845548
[startup+140.004 s]
Raw data (loadavg): 1.03 1.02 0.96 2/65 28041
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 13132 44 1 0 25 0 11 0 427541956 865841152 24047 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 24047 13073 16 0 211371 0
vsize: 845548
[startup+150.005 s]
Raw data (loadavg): 1.02 1.02 0.96 2/65 28044
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 14102 44 1 0 25 0 11 0 427541956 865841152 24147 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 24147 13073 16 0 211371 0
vsize: 845548
[startup+160.005 s]
Raw data (loadavg): 1.02 1.02 0.96 2/65 28046
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 15071 44 1 0 25 0 11 0 427541956 865841152 24245 4294967295 134512640 134569956 3221224400 3221214664 1131263327 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 24245 13073 16 0 211371 0
vsize: 845548
[startup+170.005 s]
Raw data (loadavg): 1.02 1.02 0.96 2/65 28048
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 16044 44 1 0 25 0 11 0 427541956 865841152 24328 4294967295 134512640 134569956 3221224400 3221214664 1131263296 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 24328 13073 16 0 211371 0
vsize: 845548
[startup+180.005 s]
Raw data (loadavg): 1.01 1.02 0.96 2/65 28050
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 17015 44 2 0 25 0 11 0 427541956 865841152 24470 4294967295 134512640 134569956 3221224400 3221214712 1131278066 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 24470 13073 16 0 211371 0
vsize: 845548
[startup+190.005 s]
Raw data (loadavg): 1.01 1.02 0.96 2/65 28052
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 17982 44 2 0 25 0 11 0 427541956 865841152 24612 4294967295 134512640 134569956 3221224400 3221214712 1131278066 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 24612 13073 16 0 211371 0
vsize: 845548
[startup+200.005 s]
Raw data (loadavg): 1.01 1.01 0.96 2/65 28055
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 18953 44 2 0 25 0 11 0 427541956 865841152 24687 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 24687 13073 16 0 211371 0
vsize: 845548
[startup+210.005 s]
Raw data (loadavg): 1.01 1.01 0.96 2/65 28057
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 19923 45 2 0 25 0 11 0 427541956 865841152 24781 4294967295 134512640 134569956 3221224400 3221214808 1131292127 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 24781 13073 16 0 211371 0
vsize: 845548
[startup+220.008 s]
Raw data (loadavg): 1.00 1.01 0.96 2/65 28060
Raw data (stat): 28009 (java) S 28008 30927 30926 0 -1 0 18107 3 1 0 20888 45 2 0 24 0 11 0 427541956 865841152 24887 4294967295 134512640 134569956 3221224400 3221213456 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 24887 13073 16 0 211371 0
vsize: 845548
[startup+230.008 s]
Raw data (loadavg): 1.00 1.01 0.96 2/65 28062
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 21853 45 2 0 25 0 11 0 427541956 865841152 24979 4294967295 134512640 134569956 3221224400 3221214664 1131264240 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 24979 13073 16 0 211371 0
vsize: 845548
[startup+240.008 s]
Raw data (loadavg): 1.00 1.01 0.96 2/65 28065
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 22817 45 2 0 25 0 11 0 427541956 865841152 25121 4294967295 134512640 134569956 3221224400 3221214712 1131278677 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 25121 13073 16 0 211371 0
vsize: 845548
[startup+250.009 s]
Raw data (loadavg): 1.00 1.01 0.96 2/65 28067
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 23780 45 3 0 25 0 11 0 427541956 865841152 25356 4294967295 134512640 134569956 3221224400 3221214712 1131278184 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 25356 13073 16 0 211371 0
vsize: 845548
[startup+260.01 s]
Raw data (loadavg): 1.00 1.01 0.96 2/65 28069
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 24744 45 3 0 24 0 11 0 427541956 865841152 25482 4294967295 134512640 134569956 3221224400 3221214712 1131279036 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 25482 13073 16 0 211371 0
vsize: 845548
[startup+270.01 s]
Raw data (loadavg): 1.00 1.01 0.96 2/65 28072
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 25712 45 3 1 25 0 11 0 427541956 865841152 25568 4294967295 134512640 134569956 3221224400 3221214712 1131278698 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 25568 13073 16 0 211371 0
vsize: 845548
[startup+280.01 s]
Raw data (loadavg): 1.00 1.01 0.96 2/65 28074
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 26679 46 3 1 25 0 11 0 427541956 865841152 25649 4294967295 134512640 134569956 3221224400 3221214712 1131277989 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 25649 13073 16 0 211371 0
vsize: 845548
[startup+290.011 s]
Raw data (loadavg): 1.00 1.01 0.96 2/65 28077
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 27646 46 3 1 23 0 11 0 427541956 865841152 25790 4294967295 134512640 134569956 3221224400 3221214808 1131293583 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 25790 13073 16 0 211371 0
vsize: 845548
[startup+300.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28079
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 28612 46 3 1 25 0 11 0 427541956 865841152 25887 4294967295 134512640 134569956 3221224400 3221214712 1131277985 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 25887 13073 16 0 211371 0
vsize: 845548
[startup+310.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28082
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 29581 46 3 1 25 0 11 0 427541956 865841152 26039 4294967295 134512640 134569956 3221224400 3221214808 1131294367 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 26039 13073 16 0 211371 0
vsize: 845548
[startup+320.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28084
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 30551 46 4 1 25 0 11 0 427541956 865841152 26118 4294967295 134512640 134569956 3221224400 3221214808 1131293452 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 26118 13073 16 0 211371 0
vsize: 845548
[startup+330.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28087
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 31519 47 4 1 24 0 11 0 427541956 865841152 26238 4294967295 134512640 134569956 3221224400 3221214712 1131277985 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 26238 13073 16 0 211371 0
vsize: 845548
[startup+340.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28142
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 32480 56 4 1 25 0 11 0 427541956 865841152 26311 4294967295 134512640 134569956 3221224400 3221214712 1131278625 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 26311 13073 16 0 211371 0
vsize: 845548
[startup+350.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28144
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 33451 56 4 1 25 0 11 0 427541956 865841152 26405 4294967295 134512640 134569956 3221224400 3221214712 1131277989 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 26405 13073 16 0 211371 0
vsize: 845548
[startup+360.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28147
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 34421 56 4 1 25 0 11 0 427541956 865841152 26471 4294967295 134512640 134569956 3221224400 3221214712 1131278375 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 26471 13073 16 0 211371 0
vsize: 845548
[startup+370.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28149
Raw data (stat): 28009 (java) S 28008 30927 30926 0 -1 0 18107 3 1 0 35382 56 4 1 25 0 11 0 427541956 865841152 26564 4294967295 134512640 134569956 3221224400 3221213456 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 26564 13073 16 0 211371 0
vsize: 845548
[startup+380.016 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28152
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 36341 56 4 1 25 0 11 0 427541956 865841152 26666 4294967295 134512640 134569956 3221224400 3221214808 1131292143 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 26666 13073 16 0 211371 0
vsize: 845548
[startup+390.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28156
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 37300 57 4 2 25 0 11 0 427541956 865841152 26817 4294967295 134512640 134569956 3221224400 3221214712 1131278519 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 26817 13073 16 0 211371 0
vsize: 845548
[startup+400.017 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28159
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 38269 57 4 2 25 0 11 0 427541956 865841152 27189 4294967295 134512640 134569956 3221224400 3221214712 1131278609 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 27189 13073 16 0 211371 0
vsize: 845548
[startup+410.017 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28163
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 39238 57 4 2 25 0 11 0 427541956 865841152 27267 4294967295 134512640 134569956 3221224400 3221214712 1131278389 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 27267 13073 16 0 211371 0
vsize: 845548
[startup+420.018 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28165
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 40202 57 5 2 25 0 11 0 427541956 865841152 27390 4294967295 134512640 134569956 3221224400 3221214808 1131293466 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 27390 13073 16 0 211371 0
vsize: 845548
[startup+430.018 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28168
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 41168 57 5 2 25 0 11 0 427541956 865841152 27475 4294967295 134512640 134569956 3221224400 3221214712 1131278681 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 27475 13073 16 0 211371 0
vsize: 845548
[startup+440.018 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28170
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 42133 58 5 2 25 0 11 0 427541956 865841152 27568 4294967295 134512640 134569956 3221224400 3221214712 1131278597 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 27568 13073 16 0 211371 0
vsize: 845548
[startup+450.019 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28173
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 43095 58 5 2 25 0 11 0 427541956 865841152 27694 4294967295 134512640 134569956 3221224400 3221214752 1131210069 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 27694 13073 16 0 211371 0
vsize: 845548
[startup+460.019 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28175
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 44057 58 5 2 25 0 11 0 427541956 865841152 27808 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 27808 13073 16 0 211371 0
vsize: 845548
[startup+470.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28178
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 45018 59 5 2 24 0 11 0 427541956 865841152 27971 4294967295 134512640 134569956 3221224400 3221214712 1131278058 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 27971 13073 16 0 211371 0
vsize: 845548
[startup+480.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28180
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 45986 59 5 2 25 0 11 0 427541956 865841152 28071 4294967295 134512640 134569956 3221224400 3221214808 1131293466 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 28071 13073 16 0 211371 0
vsize: 845548
[startup+490.019 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28182
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 46953 59 5 2 25 0 11 0 427541956 865841152 28193 4294967295 134512640 134569956 3221224400 3221214712 1131278079 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 28193 13073 16 0 211371 0
vsize: 845548
[startup+500.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28185
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 47922 59 5 2 25 0 11 0 427541956 865841152 28285 4294967295 134512640 134569956 3221224400 3221214712 1131277996 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 28285 13073 16 0 211371 0
vsize: 845548
[startup+510.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28187
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 48888 59 5 2 25 0 11 0 427541956 865841152 28419 4294967295 134512640 134569956 3221224400 3221214712 1131278315 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 28419 13073 16 0 211371 0
vsize: 845548
[startup+520.021 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28190
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 49854 59 5 2 21 0 11 0 427541956 865841152 28520 4294967295 134512640 134569956 3221224400 3221214808 1131294351 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 28520 13073 16 0 211371 0
vsize: 845548
[startup+530.021 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28192
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 50821 59 5 2 25 0 11 0 427541956 865841152 28599 4294967295 134512640 134569956 3221224400 3221214712 1131277985 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 28599 13073 16 0 211371 0
vsize: 845548
[startup+540.022 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28195
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 51788 59 6 2 25 0 11 0 427541956 865841152 28776 4294967295 134512640 134569956 3221224400 3221214808 1131292347 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 28776 13073 16 0 211371 0
vsize: 845548
[startup+550.024 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28197
Raw data (stat): 28009 (java) S 28008 30927 30926 0 -1 0 18107 3 1 0 52756 60 6 2 25 0 11 0 427541956 865841152 28875 4294967295 134512640 134569956 3221224400 3221213456 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 28875 13073 16 0 211371 0
vsize: 845548
[startup+560.023 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28199
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 53725 60 6 2 25 0 11 0 427541956 865841152 28997 4294967295 134512640 134569956 3221224400 3221214712 1131278058 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 28997 13073 16 0 211371 0
vsize: 845548
[startup+570.024 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28202
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 54695 60 6 3 25 0 11 0 427541956 865841152 29054 4294967295 134512640 134569956 3221224400 3221214712 1131278633 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 29054 13073 16 0 211371 0
vsize: 845548
[startup+580.024 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28204
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 55663 60 6 3 25 0 11 0 427541956 865841152 29138 4294967295 134512640 134569956 3221224400 3221214808 1131293493 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 29138 13073 16 0 211371 0
vsize: 845548
[startup+590.023 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28207
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 56631 61 6 3 25 0 11 0 427541956 865841152 29244 4294967295 134512640 134569956 3221224400 3221214712 1131278673 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 29244 13073 16 0 211371 0
vsize: 845548
[startup+600.024 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28209
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 57597 61 6 3 25 0 11 0 427541956 865841152 29348 4294967295 134512640 134569956 3221224400 3221214712 1131279033 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 29348 13073 16 0 211371 0
vsize: 845548
[startup+610.024 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28212
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 58568 61 6 3 25 0 11 0 427541956 865841152 29454 4294967295 134512640 134569956 3221224400 3221214808 1131292347 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 29454 13073 16 0 211371 0
vsize: 845548
[startup+620.025 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28214
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 59539 61 6 3 25 0 11 0 427541956 865841152 29525 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 29525 13073 16 0 211371 0
vsize: 845548
[startup+630.025 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28216
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 60509 61 6 3 25 0 11 0 427541956 865841152 29610 4294967295 134512640 134569956 3221224400 3221214804 1131277964 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 29610 13073 16 0 211371 0
vsize: 845548
[startup+640.025 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28221
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 61476 62 6 3 25 0 11 0 427541956 865841152 29674 4294967295 134512640 134569956 3221224400 3221214712 1131278854 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 29674 13073 16 0 211371 0
vsize: 845548
[startup+650.025 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28223
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 62439 62 6 3 25 0 11 0 427541956 865841152 29963 4294967295 134512640 134569956 3221224400 3221214712 1131278042 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 29963 13073 16 0 211371 0
vsize: 845548
[startup+660.025 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28226
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 63391 62 6 3 25 0 11 0 427541956 865841152 30041 4294967295 134512640 134569956 3221224400 3221214712 1131278386 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 30041 13073 16 0 211371 0
vsize: 845548
[startup+670.026 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28228
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 64341 63 7 3 25 0 11 0 427541956 865841152 30310 4294967295 134512640 134569956 3221224400 3221214712 1131278698 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 30310 13073 16 0 211371 0
vsize: 845548
[startup+680.026 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28230
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 65298 63 7 3 25 0 11 0 427541956 865841152 30963 4294967295 134512640 134569956 3221224400 3221214712 1131278085 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 30963 13073 16 0 211371 0
vsize: 845548
[startup+690.026 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28233
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 66264 63 7 3 25 0 11 0 427541956 865841152 31115 4294967295 134512640 134569956 3221224400 3221214712 1131278396 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 31115 13073 16 0 211371 0
vsize: 845548
[startup+700.027 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28235
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 67233 63 7 3 25 0 11 0 427541956 865841152 31209 4294967295 134512640 134569956 3221224400 3221214712 1131277981 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 31209 13073 16 0 211371 0
vsize: 845548
[startup+710.027 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28238
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 68199 64 7 3 25 0 11 0 427541956 865841152 31336 4294967295 134512640 134569956 3221224400 3221214808 1131295016 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 31336 13073 16 0 211371 0
vsize: 845548
[startup+720.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28240
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 69168 64 7 3 25 0 11 0 427541956 865841152 31404 4294967295 134512640 134569956 3221224400 3221214808 1131292143 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 31404 13073 16 0 211371 0
vsize: 845548
[startup+730.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28243
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 70139 64 8 3 25 0 11 0 427541956 865841152 31525 4294967295 134512640 134569956 3221224400 3221214712 1131278924 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 31525 13073 16 0 211371 0
vsize: 845548
[startup+740.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28245
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 71107 64 8 3 25 0 11 0 427541956 865841152 31593 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 31593 13073 16 0 211371 0
vsize: 845548
[startup+750.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28247
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 72076 64 8 3 25 0 11 0 427541956 865841152 31678 4294967295 134512640 134569956 3221224400 3221214712 1131278128 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 31678 13073 16 0 211371 0
vsize: 845548
[startup+760.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28250
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 73042 64 8 3 25 0 11 0 427541956 865841152 31747 4294967295 134512640 134569956 3221224400 3221214808 1131293466 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 31747 13073 16 0 211371 0
vsize: 845548
[startup+770.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28252
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 74011 65 8 4 25 0 11 0 427541956 865841152 31855 4294967295 134512640 134569956 3221224400 3221214712 1131279036 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 31855 13073 16 0 211371 0
vsize: 845548
[startup+780.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28255
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 74980 65 8 4 25 0 11 0 427541956 865841152 31965 4294967295 134512640 134569956 3221224400 3221214752 1131210048 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 31965 13073 16 0 211371 0
vsize: 845548
[startup+790.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28257
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 75949 65 8 4 25 0 11 0 427541956 865841152 32049 4294967295 134512640 134569956 3221224400 3221214808 1131293466 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 32049 13073 16 0 211371 0
vsize: 845548
[startup+800.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28260
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 76915 65 8 4 25 0 11 0 427541956 865841152 32136 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 32136 13073 16 0 211371 0
vsize: 845548
[startup+810.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28262
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 77876 65 8 4 24 0 11 0 427541956 865841152 32239 4294967295 134512640 134569956 3221224400 3221214712 1131278375 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 32239 13073 16 0 211371 0
vsize: 845548
[startup+820.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28264
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 78840 65 9 4 25 0 11 0 427541956 865841152 32395 4294967295 134512640 134569956 3221224400 3221214712 1131278840 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 32395 13073 16 0 211371 0
vsize: 845548
[startup+830.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28267
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 79803 66 9 4 24 0 11 0 427541956 865841152 32467 4294967295 134512640 134569956 3221224400 3221214712 1131278014 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 32467 13073 16 0 211371 0
vsize: 845548
[startup+840.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28269
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 80762 66 9 4 24 0 11 0 427541956 865841152 32577 4294967295 134512640 134569956 3221224400 3221214712 1131278361 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 32577 13073 16 0 211371 0
vsize: 845548
[startup+850.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28271
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 81718 66 9 4 25 0 11 0 427541956 865841152 32738 4294967295 134512640 134569956 3221224400 3221214712 1131278951 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 32738 13073 16 0 211371 0
vsize: 845548
[startup+860.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28274
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 82673 66 9 4 24 0 11 0 427541956 865841152 32837 4294967295 134512640 134569956 3221224400 3221214712 1131278651 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 32837 13073 16 0 211371 0
vsize: 845548
[startup+870.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28276
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 83633 66 9 4 24 0 11 0 427541956 865841152 33027 4294967295 134512640 134569956 3221224400 3221214712 1131279036 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 33027 13073 16 0 211371 0
vsize: 845548
[startup+880.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28279
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 84597 67 9 4 24 0 11 0 427541956 865841152 33170 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 33170 13073 16 0 211371 0
vsize: 845548
[startup+890.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28281
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 85564 67 10 4 24 0 11 0 427541956 865841152 33302 4294967295 134512640 134569956 3221224400 3221214712 1131277989 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 33302 13073 16 0 211371 0
vsize: 845548
[startup+900.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28283
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 86529 67 10 4 25 0 11 0 427541956 865841152 33387 4294967295 134512640 134569956 3221224400 3221214712 1131278073 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 33387 13073 16 0 211371 0
vsize: 845548
[startup+910.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28286
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 87495 67 10 4 25 0 11 0 427541956 865841152 33523 4294967295 134512640 134569956 3221224400 3221214712 1131278386 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 33523 13073 16 0 211371 0
vsize: 845548
[startup+920.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28288
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 88460 68 10 4 25 0 11 0 427541956 865841152 33700 4294967295 134512640 134569956 3221224400 3221214712 1131278066 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 33700 13073 16 0 211371 0
vsize: 845548
[startup+930.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28291
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 89428 68 10 4 25 0 11 0 427541956 865841152 33808 4294967295 134512640 134569956 3221224400 3221214808 1131294407 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 33808 13073 16 0 211371 0
vsize: 845548
[startup+940.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28293
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 90395 68 10 4 25 0 11 0 427541956 865841152 33864 4294967295 134512640 134569956 3221224400 3221214712 1131278605 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 33864 13073 16 0 211371 0
vsize: 845548
[startup+950.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28295
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 91363 69 10 4 25 0 11 0 427541956 865841152 34033 4294967295 134512640 134569956 3221224400 3221214712 1131278544 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 34033 13073 16 0 211371 0
vsize: 845548
[startup+960.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28298
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 92331 69 10 4 25 0 11 0 427541956 865841152 34101 4294967295 134512640 134569956 3221224400 3221214712 1131278945 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 34101 13073 16 0 211371 0
vsize: 845548
[startup+970.035 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28300
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 93300 69 10 4 25 0 11 0 427541956 865841152 34169 4294967295 134512640 134569956 3221224400 3221214808 1131292416 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 34169 13073 16 0 211371 0
vsize: 845548
[startup+980.035 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28303
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 94269 70 10 4 25 0 11 0 427541956 865841152 34284 4294967295 134512640 134569956 3221224400 3221214712 1131279024 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 34284 13073 16 0 211371 0
vsize: 845548
[startup+990.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28305
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 95236 70 10 4 25 0 11 0 427541956 865841152 34361 4294967295 134512640 134569956 3221224400 3221214808 1131293526 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 34361 13073 16 0 211371 0
vsize: 845548
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28307
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 96200 71 10 4 25 0 11 0 427541956 865841152 34436 4294967295 134512640 134569956 3221224400 3221214808 1131292351 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 34436 13073 16 0 211371 0
vsize: 845548
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28310
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 97164 71 10 4 25 0 11 0 427541956 865841152 34592 4294967295 134512640 134569956 3221224400 3221214712 1131278633 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 34592 13073 16 0 211371 0
vsize: 845548
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28312
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 98128 71 10 4 25 0 11 0 427541956 865841152 34720 4294967295 134512640 134569956 3221224400 3221214808 1131293373 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 34720 13073 16 0 211371 0
vsize: 845548
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28314
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 99093 72 11 4 24 0 11 0 427541956 865841152 34901 4294967295 134512640 134569956 3221224400 3221214712 1131278014 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 34901 13073 16 0 211371 0
vsize: 845548
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28317
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 100061 72 11 5 24 0 11 0 427541956 865841152 34981 4294967295 134512640 134569956 3221224400 3221214712 1131279042 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 34981 13073 16 0 211371 0
vsize: 845548
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28319
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 101030 72 11 5 25 0 11 0 427541956 865841152 35089 4294967295 134512640 134569956 3221224400 3221214712 1131278326 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35089 13073 16 0 211371 0
vsize: 845548
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28322
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 101998 73 11 5 25 0 11 0 427541956 865841152 35169 4294967295 134512640 134569956 3221224400 3221214808 1131292416 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35169 13073 16 0 211371 0
vsize: 845548
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28324
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 102967 73 11 5 18 0 11 0 427541956 865841152 35231 4294967295 134512640 134569956 3221224400 3221214712 1131278954 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35231 13073 16 0 211371 0
vsize: 845548
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28326
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 103937 73 11 5 25 0 11 0 427541956 865841152 35354 4294967295 134512640 134569956 3221224400 3221214712 1131278073 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35354 13073 16 0 211371 0
vsize: 845548
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28329
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 104906 74 11 5 25 0 11 0 427541956 865841152 35410 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35410 13073 16 0 211371 0
vsize: 845548
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28331
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 105875 74 12 5 25 0 11 0 427541956 865841152 35469 4294967295 134512640 134569956 3221224400 3221214808 1131292347 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35469 13073 16 0 211371 0
vsize: 845548
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28334
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 106842 74 12 5 25 0 11 0 427541956 865841152 35590 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35590 13073 16 0 211371 0
vsize: 845548
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28336
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 107810 75 12 5 25 0 11 0 427541956 865841152 35660 4294967295 134512640 134569956 3221224400 3221214712 1131278326 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35660 13073 16 0 211371 0
vsize: 845548
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28338
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 108775 75 12 5 25 0 11 0 427541956 865841152 35744 4294967295 134512640 134569956 3221224400 3221214712 1131279005 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35744 13073 16 0 211371 0
vsize: 845548
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28341
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 109742 75 12 5 25 0 11 0 427541956 865841152 35855 4294967295 134512640 134569956 3221224400 3221214712 1131278453 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35855 13073 16 0 211371 0
vsize: 845548
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28343
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 110709 75 12 5 25 0 11 0 427541956 865841152 35985 4294967295 134512640 134569956 3221224400 3221214664 1131263290 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 35985 13073 16 0 211371 0
vsize: 845548
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28346
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 111679 76 12 5 18 0 11 0 427541956 865841152 36096 4294967295 134512640 134569956 3221224400 3221214664 1131263302 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211387 36096 13073 16 0 211371 0
vsize: 845548
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28348
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 112650 76 12 6 25 0 11 0 427541956 865841152 36154 4294967295 134512640 134569956 3221224400 3221214712 1131278605 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 36154 13073 16 0 211371 0
vsize: 845548
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28350
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 113620 76 12 6 25 0 11 0 427541956 865841152 36210 4294967295 134512640 134569956 3221224400 3221214712 1131278629 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 36210 13073 16 0 211371 0
vsize: 845548
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28353
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 114589 77 13 6 25 0 11 0 427541956 865841152 36294 4294967295 134512640 134569956 3221224400 3221214804 1131210028 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 36294 13073 16 0 211371 0
vsize: 845548
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28355
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 115559 77 13 6 25 0 11 0 427541956 865841152 36362 4294967295 134512640 134569956 3221224400 3221214712 1131278625 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 36362 13073 16 0 211371 0
vsize: 845548
[startup+1210.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28358
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 116529 77 13 6 25 0 11 0 427541956 865841152 36459 4294967295 134512640 134569956 3221224400 3221214808 1131477949 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 36459 13073 16 0 211371 0
vsize: 845548
[startup+1220.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28360
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 117499 78 13 6 25 0 11 0 427541956 865841152 36515 4294967295 134512640 134569956 3221224400 3221214712 1131278681 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 36515 13073 16 0 211371 0
vsize: 845548
[startup+1230.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28362
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 118470 78 13 6 24 0 11 0 427541956 865841152 38340 4294967295 134512640 134569956 3221224400 3221214808 1131292328 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 38340 13073 16 0 211371 0
vsize: 845548
[startup+1240.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28365
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 119450 78 13 6 25 0 11 0 427541956 865841152 38340 4294967295 134512640 134569956 3221224400 3221214808 1131292347 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 38340 13073 16 0 211371 0
vsize: 845548
[startup+1250.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/65 28367
Raw data (stat): 28009 (java) R 28008 30927 30926 0 -1 0 18107 3 1 0 120422 78 13 6 25 0 11 0 427541956 865841152 38340 4294967295 134512640 134569956 3221224400 3221214808 1131293466 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211387 38340 13073 16 0 211371 0
vsize: 845548
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1250.12 s]
Raw data (loadavg): 1.00 1.00 0.96 1/55 28369
Raw data (stat): 28009 (java) Z 28008 30927 30926 0 -1 1036 18107 24877 1 0 120423 85 5752 81 25 0 1 0 427541956 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.12
CPU time (s): 1263.42
CPU user time (s): 1261.75
CPU system time (s): 1.66875
CPU usage (%): 101.064
Max. virtual memory (Kb): 845548
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####