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/miplib3/normalized-mps-v2-20-10-set1ch.opb
MD5SUM	38f0a9b4a9f08223cf001d3ae518ccdb
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	569806848
Optimality of the best value was proved	NO
Number of terms in the objective function	7200
Biggest coefficient in the objective function	10737418240
Number of bits for the biggest coefficient in the objective function	34
Sum of the numbers in the objective function	1616658659871
Number of bits of the sum of numbers in the objective function	41
Biggest number in a constraint	10737418240
Number of bits of the biggest number in a constraint	34
Biggest sum of numbers in a constraint	1616658659871
Number of bits of the biggest sum of numbers	41
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1220.3
Number of variables	14400
Total number of constraints	732
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	240
Number of constraints which are nor clauses,nor cardinality constraints	492
Minimum length of a constraint	1
Maximum length of a constraint	630
Trace number 21070

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        591764 kB
Buffers:         31240 kB
Cached:         384832 kB
SwapCached:       4304 kB
Active:          67228 kB
Inactive:       354616 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        591512 kB
SwapTotal:     2097892 kB
SwapFree:      2092680 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15392 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 22:59:53 (client local time) WITH STATUS 143 IN 1312.75 SECONDS
stats: 13880 7 1312.75 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-set1ch.opb
c reading problem 
c [nbvar=14400]
c [nbconstr=732]
c time 61.871
c #vars     14400
c #clauses  733
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=569806848
c Current CPU time (ms) : 72.031
c starts	: 1
c conflicts	: 0
c decisions	: 4439
c propagations	: 14400
c inspects	: 15945
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 1
c 
c CURRENT OPTIMUM=-1741658708
c Current CPU time (ms) : 318.704
c starts	: 2
c conflicts	: 17
c decisions	: 10515
c propagations	: 39110
c inspects	: 56641
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 17
c root simplifications	: 8
c 
c CURRENT OPTIMUM=-1732010612
c Current CPU time (ms) : 328.665
c starts	: 3
c conflicts	: 30
c decisions	: 12286
c propagations	: 52668
c inspects	: 77120
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 30
c root simplifications	: 12
c 
c CURRENT OPTIMUM=-1726164416
c Current CPU time (ms) : 334.851
c starts	: 4
c conflicts	: 34
c decisions	: 13420
c propagations	: 62120
c inspects	: 91387
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 34
c root simplifications	: 15
c 
c CURRENT OPTIMUM=-1724417576
c Current CPU time (ms) : 341.038
c starts	: 5
c conflicts	: 42
c decisions	: 14633
c propagations	: 71706
c inspects	: 105737
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 16
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 345.685
c starts	: 6
c conflicts	: 42
c decisions	: 15719
c propagations	: 81031
c inspects	: 119451
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 17
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 350.259
c starts	: 7
c conflicts	: 42
c decisions	: 16805
c propagations	: 90356
c inspects	: 132878
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 18
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 354.937
c starts	: 8
c conflicts	: 42
c decisions	: 17891
c propagations	: 99681
c inspects	: 146305
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 19
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 359.627
c starts	: 9
c conflicts	: 42
c decisions	: 18977
c propagations	: 109006
c inspects	: 159732
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 20
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 364.322
c starts	: 10
c conflicts	: 42
c decisions	: 20063
c propagations	: 118331
c inspects	: 173159
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 21
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 369.025
c starts	: 11
c conflicts	: 42
c decisions	: 21149
c propagations	: 127656
c inspects	: 186586
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 22
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 373.558
c starts	: 12
c conflicts	: 42
c decisions	: 22235
c propagations	: 136981
c inspects	: 200013
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 23
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 378.198
c starts	: 13
c conflicts	: 42
c decisions	: 23321
c propagations	: 146306
c inspects	: 213440
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 24
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 382.862
c starts	: 14
c conflicts	: 42
c decisions	: 24407
c propagations	: 155631
c inspects	: 226867
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 25
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 387.516
c starts	: 15
c conflicts	: 42
c decisions	: 25493
c propagations	: 164956
c inspects	: 240294
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 26
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 392.192
c starts	: 16
c conflicts	: 42
c decisions	: 26579
c propagations	: 174281
c inspects	: 253721
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 27
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 396.833
c starts	: 17
c conflicts	: 42
c decisions	: 27665
c propagations	: 183606
c inspects	: 267148
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 28
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 401.476
c starts	: 18
c conflicts	: 42
c decisions	: 28751
c propagations	: 192931
c inspects	: 280575
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 29
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 406.129
c starts	: 19
c conflicts	: 42
c decisions	: 29837
c propagations	: 202256
c inspects	: 294002
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 30
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 410.72
c starts	: 20
c conflicts	: 42
c decisions	: 30923
c propagations	: 211581
c inspects	: 307429
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 31
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 415.336
c starts	: 21
c conflicts	: 42
c decisions	: 32009
c propagations	: 220906
c inspects	: 320856
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 32
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 419.946
c starts	: 22
c conflicts	: 42
c decisions	: 33095
c propagations	: 230231
c inspects	: 334283
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 33
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 424.58
c starts	: 23
c conflicts	: 42
c decisions	: 34181
c propagations	: 239556
c inspects	: 347710
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 34
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 429.274
c starts	: 24
c conflicts	: 42
c decisions	: 35267
c propagations	: 248881
c inspects	: 361137
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 35
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 433.991
c starts	: 25
c conflicts	: 42
c decisions	: 36353
c propagations	: 258206
c inspects	: 374564
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 36
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 438.71
c starts	: 26
c conflicts	: 42
c decisions	: 37439
c propagations	: 267531
c inspects	: 387991
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 37
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 443.453
c starts	: 27
c conflicts	: 42
c decisions	: 38525
c propagations	: 276856
c inspects	: 401418
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 38
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 448.106
c starts	: 28
c conflicts	: 42
c decisions	: 39611
c propagations	: 286181
c inspects	: 414845
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 39
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 452.871
c starts	: 29
c conflicts	: 42
c decisions	: 40697
c propagations	: 295506
c inspects	: 428272
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 40
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 457.529
c starts	: 30
c conflicts	: 42
c decisions	: 41783
c propagations	: 304831
c inspects	: 441699
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 41
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 462.154
c starts	: 31
c conflicts	: 42
c decisions	: 42869
c propagations	: 314156
c inspects	: 455126
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 42
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 466.774
c starts	: 32
c conflicts	: 42
c decisions	: 43955
c propagations	: 323481
c inspects	: 468553
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 43
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 471.372
c starts	: 33
c conflicts	: 42
c decisions	: 45041
c propagations	: 332806
c inspects	: 481980
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 44
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 475.997
c starts	: 34
c conflicts	: 42
c decisions	: 46127
c propagations	: 342131
c inspects	: 495407
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 45
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 480.59
c starts	: 35
c conflicts	: 42
c decisions	: 47213
c propagations	: 351456
c inspects	: 508834
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 46
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 485.281
c starts	: 36
c conflicts	: 42
c decisions	: 48299
c propagations	: 360781
c inspects	: 522261
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 47
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 489.978
c starts	: 37
c conflicts	: 42
c decisions	: 49385
c propagations	: 370106
c inspects	: 535688
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 48
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 494.679
c starts	: 38
c conflicts	: 42
c decisions	: 50471
c propagations	: 379431
c inspects	: 549115
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 49
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 499.337
c starts	: 39
c conflicts	: 42
c decisions	: 51557
c propagations	: 388756
c inspects	: 562542
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 50
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 503.987
c starts	: 40
c conflicts	: 42
c decisions	: 52643
c propagations	: 398081
c inspects	: 575969
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 51
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 508.65
c starts	: 41
c conflicts	: 42
c decisions	: 53729
c propagations	: 407406
c inspects	: 589396
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 52
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 513.236
c starts	: 42
c conflicts	: 42
c decisions	: 54815
c propagations	: 416731
c inspects	: 602823
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 53
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 517.901
c starts	: 43
c conflicts	: 42
c decisions	: 55901
c propagations	: 426056
c inspects	: 616250
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 54
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 522.586
c starts	: 44
c conflicts	: 42
c decisions	: 56987
c propagations	: 435381
c inspects	: 629677
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 55
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 527.284
c starts	: 45
c conflicts	: 42
c decisions	: 58073
c propagations	: 444706
c inspects	: 643104
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 56
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 532.045
c starts	: 46
c conflicts	: 42
c decisions	: 59159
c propagations	: 454031
c inspects	: 656531
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 57
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 536.789
c starts	: 47
c conflicts	: 42
c decisions	: 60245
c propagations	: 463356
c inspects	: 669958
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 58
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 541.573
c starts	: 48
c conflicts	: 42
c decisions	: 61331
c propagations	: 472681
c inspects	: 683385
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 59
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 546.345
c starts	: 49
c conflicts	: 42
c decisions	: 62417
c propagations	: 482006
c inspects	: 696812
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 60
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 551.035
c starts	: 50
c conflicts	: 42
c decisions	: 63503
c propagations	: 491331
c inspects	: 710239
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 61
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 555.79
c starts	: 51
c conflicts	: 42
c decisions	: 64589
c propagations	: 500656
c inspects	: 723666
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 62
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 560.547
c starts	: 52
c conflicts	: 42
c decisions	: 65675
c propagations	: 509981
c inspects	: 737093
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 63
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 565.345
c starts	: 53
c conflicts	: 42
c decisions	: 66761
c propagations	: 519306
c inspects	: 750520
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 64
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 570.231
c starts	: 54
c conflicts	: 42
c decisions	: 67847
c propagations	: 528631
c inspects	: 763947
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 65
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 574.733
c starts	: 55
c conflicts	: 42
c decisions	: 68933
c propagations	: 537956
c inspects	: 777374
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 66
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 579.241
c starts	: 56
c conflicts	: 42
c decisions	: 70019
c propagations	: 547281
c inspects	: 790801
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 67
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 583.819
c starts	: 57
c conflicts	: 42
c decisions	: 71105
c propagations	: 556606
c inspects	: 804228
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 68
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 588.483
c starts	: 58
c conflicts	: 42
c decisions	: 72191
c propagations	: 565931
c inspects	: 817655
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 69
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 593.275
c starts	: 59
c conflicts	: 42
c decisions	: 73277
c propagations	: 575256
c inspects	: 831082
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 70
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 598.017
c starts	: 60
c conflicts	: 42
c decisions	: 74363
c propagations	: 584581
c inspects	: 844509
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 71
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 602.877
c starts	: 61
c conflicts	: 42
c decisions	: 75449
c propagations	: 593906
c inspects	: 857936
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 72
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 607.727
c starts	: 62
c conflicts	: 42
c decisions	: 76535
c propagations	: 603231
c inspects	: 871363
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 73
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 612.594
c starts	: 63
c conflicts	: 42
c decisions	: 77621
c propagations	: 612556
c inspects	: 884790
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 74
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 617.473
c starts	: 64
c conflicts	: 42
c decisions	: 78707
c propagations	: 621881
c inspects	: 898217
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 75
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 622.358
c starts	: 65
c conflicts	: 42
c decisions	: 79793
c propagations	: 631206
c inspects	: 911644
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 76
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 627.223
c starts	: 66
c conflicts	: 42
c decisions	: 80879
c propagations	: 640531
c inspects	: 925071
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 77
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 632.111
c starts	: 67
c conflicts	: 42
c decisions	: 81965
c propagations	: 649856
c inspects	: 938498
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 78
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 637.009
c starts	: 68
c conflicts	: 42
c decisions	: 83051
c propagations	: 659181
c inspects	: 951925
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 79
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 641.922
c starts	: 69
c conflicts	: 42
c decisions	: 84137
c propagations	: 668506
c inspects	: 965352
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 80
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 646.789
c starts	: 70
c conflicts	: 42
c decisions	: 85223
c propagations	: 677831
c inspects	: 978779
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 81
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 651.683
c starts	: 71
c conflicts	: 42
c decisions	: 86309
c propagations	: 687156
c inspects	: 992206
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 82
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 656.419
c starts	: 72
c conflicts	: 42
c decisions	: 87395
c propagations	: 696481
c inspects	: 1005633
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 83
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 661.266
c starts	: 73
c conflicts	: 42
c decisions	: 88481
c propagations	: 705806
c inspects	: 1019060
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 84
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 666.138
c starts	: 74
c conflicts	: 42
c decisions	: 89567
c propagations	: 715131
c inspects	: 1032487
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 85
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 671.003
c starts	: 75
c conflicts	: 42
c decisions	: 90653
c propagations	: 724456
c inspects	: 1045914
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 86
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 675.859
c starts	: 76
c conflicts	: 42
c decisions	: 91739
c propagations	: 733781
c inspects	: 1059341
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 87
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 680.725
c starts	: 77
c conflicts	: 42
c decisions	: 92825
c propagations	: 743106
c inspects	: 1072768
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 88
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 685.577
c starts	: 78
c conflicts	: 42
c decisions	: 93911
c propagations	: 752431
c inspects	: 1086195
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 89
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 690.425
c starts	: 79
c conflicts	: 42
c decisions	: 94997
c propagations	: 761756
c inspects	: 1099622
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 90
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 695.296
c starts	: 80
c conflicts	: 42
c decisions	: 96083
c propagations	: 771081
c inspects	: 1113049
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 91
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 700.171
c starts	: 81
c conflicts	: 42
c decisions	: 97169
c propagations	: 780406
c inspects	: 1126476
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 92
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 705.024
c starts	: 82
c conflicts	: 42
c decisions	: 98255
c propagations	: 789731
c inspects	: 1139903
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 93
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 709.889
c starts	: 83
c conflicts	: 42
c decisions	: 99341
c propagations	: 799056
c inspects	: 1153330
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 94
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 714.751
c starts	: 84
c conflicts	: 42
c decisions	: 100427
c propagations	: 808381
c inspects	: 1166757
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 95
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 719.658
c starts	: 85
c conflicts	: 42
c decisions	: 101513
c propagations	: 817706
c inspects	: 1180184
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 96
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 724.559
c starts	: 86
c conflicts	: 42
c decisions	: 102599
c propagations	: 827031
c inspects	: 1193611
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 97
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 729.49
c starts	: 87
c conflicts	: 42
c decisions	: 103685
c propagations	: 836356
c inspects	: 1207038
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 98
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 734.39
c starts	: 88
c conflicts	: 42
c decisions	: 104771
c propagations	: 845681
c inspects	: 1220465
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 99
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 739.31
c starts	: 89
c conflicts	: 42
c decisions	: 105857
c propagations	: 855006
c inspects	: 1233892
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 100
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 744.245
c starts	: 90
c conflicts	: 42
c decisions	: 106943
c propagations	: 864331
c inspects	: 1247319
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 101
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 749.187
c starts	: 91
c conflicts	: 42
c decisions	: 108029
c propagations	: 873656
c inspects	: 1260746
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 102
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 754.142
c starts	: 92
c conflicts	: 42
c decisions	: 109115
c propagations	: 882981
c inspects	: 1274173
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 103
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 759.103
c starts	: 93
c conflicts	: 42
c decisions	: 110201
c propagations	: 892306
c inspects	: 1287600
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 104
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 764.113
c starts	: 94
c conflicts	: 42
c decisions	: 111287
c propagations	: 901631
c inspects	: 1301027
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 105
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 769.102
c starts	: 95
c conflicts	: 42
c decisions	: 112373
c propagations	: 910956
c inspects	: 1314454
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 106
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 773.964
c starts	: 96
c conflicts	: 42
c decisions	: 113459
c propagations	: 920281
c inspects	: 1327881
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 107
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 778.934
c starts	: 97
c conflicts	: 42
c decisions	: 114545
c propagations	: 929606
c inspects	: 1341308
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 108
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 783.868
c starts	: 98
c conflicts	: 42
c decisions	: 115631
c propagations	: 938931
c inspects	: 1354735
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 109
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 788.805
c starts	: 99
c conflicts	: 42
c decisions	: 116717
c propagations	: 948256
c inspects	: 1368162
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 110
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 793.793
c starts	: 100
c conflicts	: 42
c decisions	: 117803
c propagations	: 957581
c inspects	: 1381589
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 111
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 798.804
c starts	: 101
c conflicts	: 42
c decisions	: 118889
c propagations	: 966906
c inspects	: 1395016
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 112
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 803.836
c starts	: 102
c conflicts	: 42
c decisions	: 119975
c propagations	: 976231
c inspects	: 1408443
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 113
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 809.079
c starts	: 103
c conflicts	: 42
c decisions	: 121061
c propagations	: 985556
c inspects	: 1421870
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 114
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 814.105
c starts	: 104
c conflicts	: 42
c decisions	: 122147
c propagations	: 994881
c inspects	: 1435297
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 115
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 819.13
c starts	: 105
c conflicts	: 42
c decisions	: 123233
c propagations	: 1004206
c inspects	: 1448724
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 116
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 824.146
c starts	: 106
c conflicts	: 42
c decisions	: 124319
c propagations	: 1013531
c inspects	: 1462151
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 117
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 829.166
c starts	: 107
c conflicts	: 42
c decisions	: 125405
c propagations	: 1022856
c inspects	: 1475578
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 118
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 834.177
c starts	: 108
c conflicts	: 42
c decisions	: 126491
c propagations	: 1032181
c inspects	: 1489005
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 119
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 839.191
c starts	: 109
c conflicts	: 42
c decisions	: 127577
c propagations	: 1041506
c inspects	: 1502432
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 120
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 844.233
c starts	: 110
c conflicts	: 42
c decisions	: 128663
c propagations	: 1050831
c inspects	: 1515859
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 121
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 849.281
c starts	: 111
c conflicts	: 42
c decisions	: 129749
c propagations	: 1060156
c inspects	: 1529286
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 122
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 854.321
c starts	: 112
c conflicts	: 42
c decisions	: 130835
c propagations	: 1069481
c inspects	: 1542713
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 123
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 859.372
c starts	: 113
c conflicts	: 42
c decisions	: 131921
c propagations	: 1078806
c inspects	: 1556140
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 124
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 864.426
c starts	: 114
c conflicts	: 42
c decisions	: 133007
c propagations	: 1088131
c inspects	: 1569567
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 125
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 869.483
c starts	: 115
c conflicts	: 42
c decisions	: 134093
c propagations	: 1097456
c inspects	: 1582994
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 126
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 874.536
c starts	: 116
c conflicts	: 42
c decisions	: 135179
c propagations	: 1106781
c inspects	: 1596421
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 127
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 879.585
c starts	: 117
c conflicts	: 42
c decisions	: 136265
c propagations	: 1116106
c inspects	: 1609848
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 128
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 884.657
c starts	: 118
c conflicts	: 42
c decisions	: 137351
c propagations	: 1125431
c inspects	: 1623275
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 129
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 889.739
c starts	: 119
c conflicts	: 42
c decisions	: 138437
c propagations	: 1134756
c inspects	: 1636702
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 130
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 894.815
c starts	: 120
c conflicts	: 42
c decisions	: 139523
c propagations	: 1144081
c inspects	: 1650129
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 131
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 899.895
c starts	: 121
c conflicts	: 42
c decisions	: 140609
c propagations	: 1153406
c inspects	: 1663556
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 132
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 904.977
c starts	: 122
c conflicts	: 42
c decisions	: 141695
c propagations	: 1162731
c inspects	: 1676983
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 133
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 910.057
c starts	: 123
c conflicts	: 42
c decisions	: 142781
c propagations	: 1172056
c inspects	: 1690410
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 134
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 915.141
c starts	: 124
c conflicts	: 42
c decisions	: 143867
c propagations	: 1181381
c inspects	: 1703837
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 135
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 920.229
c starts	: 125
c conflicts	: 42
c decisions	: 144953
c propagations	: 1190706
c inspects	: 1717264
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 136
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 925.324
c starts	: 126
c conflicts	: 42
c decisions	: 146039
c propagations	: 1200031
c inspects	: 1730691
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 137
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 930.43
c starts	: 127
c conflicts	: 42
c decisions	: 147125
c propagations	: 1209356
c inspects	: 1744118
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 138
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 935.54
c starts	: 128
c conflicts	: 42
c decisions	: 148211
c propagations	: 1218681
c inspects	: 1757545
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 139
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 940.645
c starts	: 129
c conflicts	: 42
c decisions	: 149297
c propagations	: 1228006
c inspects	: 1770972
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 140
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 945.755
c starts	: 130
c conflicts	: 42
c decisions	: 150383
c propagations	: 1237331
c inspects	: 1784399
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 141
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 950.862
c starts	: 131
c conflicts	: 42
c decisions	: 151469
c propagations	: 1246656
c inspects	: 1797826
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 142
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 955.978
c starts	: 132
c conflicts	: 42
c decisions	: 152555
c propagations	: 1255981
c inspects	: 1811253
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 143
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 961.116
c starts	: 133
c conflicts	: 42
c decisions	: 153641
c propagations	: 1265306
c inspects	: 1824680
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 144
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 966.245
c starts	: 134
c conflicts	: 42
c decisions	: 154727
c propagations	: 1274631
c inspects	: 1838107
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 145
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 971.481
c starts	: 135
c conflicts	: 42
c decisions	: 155813
c propagations	: 1283956
c inspects	: 1851534
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 146
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 976.568
c starts	: 136
c conflicts	: 42
c decisions	: 156899
c propagations	: 1293281
c inspects	: 1864961
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 147
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 981.699
c starts	: 137
c conflicts	: 42
c decisions	: 157985
c propagations	: 1302606
c inspects	: 1878388
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 148
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 986.844
c starts	: 138
c conflicts	: 42
c decisions	: 159071
c propagations	: 1311931
c inspects	: 1891815
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 149
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 991.972
c starts	: 139
c conflicts	: 42
c decisions	: 160157
c propagations	: 1321256
c inspects	: 1905242
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 150
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 997.099
c starts	: 140
c conflicts	: 42
c decisions	: 161243
c propagations	: 1330581
c inspects	: 1918669
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 151
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1002.215
c starts	: 141
c conflicts	: 42
c decisions	: 162329
c propagations	: 1339906
c inspects	: 1932096
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 152
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1007.344
c starts	: 142
c conflicts	: 42
c decisions	: 163415
c propagations	: 1349231
c inspects	: 1945523
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 153
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1012.45
c starts	: 143
c conflicts	: 42
c decisions	: 164501
c propagations	: 1358556
c inspects	: 1958950
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 154
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1017.575
c starts	: 144
c conflicts	: 42
c decisions	: 165587
c propagations	: 1367881
c inspects	: 1972377
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 155
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1022.709
c starts	: 145
c conflicts	: 42
c decisions	: 166673
c propagations	: 1377206
c inspects	: 1985804
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 156
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1027.85
c starts	: 146
c conflicts	: 42
c decisions	: 167759
c propagations	: 1386531
c inspects	: 1999231
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 157
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1033.098
c starts	: 147
c conflicts	: 42
c decisions	: 168845
c propagations	: 1395856
c inspects	: 2012658
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 158
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1038.166
c starts	: 148
c conflicts	: 42
c decisions	: 169931
c propagations	: 1405181
c inspects	: 2026085
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 159
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1043.271
c starts	: 149
c conflicts	: 42
c decisions	: 171017
c propagations	: 1414506
c inspects	: 2039512
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 160
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1048.381
c starts	: 150
c conflicts	: 42
c decisions	: 172103
c propagations	: 1423831
c inspects	: 2052939
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 161
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1053.486
c starts	: 151
c conflicts	: 42
c decisions	: 173189
c propagations	: 1433156
c inspects	: 2066366
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 162
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1058.616
c starts	: 152
c conflicts	: 42
c decisions	: 174275
c propagations	: 1442481
c inspects	: 2079793
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 163
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1063.772
c starts	: 153
c conflicts	: 42
c decisions	: 175361
c propagations	: 1451806
c inspects	: 2093220
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 164
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1068.897
c starts	: 154
c conflicts	: 42
c decisions	: 176447
c propagations	: 1461131
c inspects	: 2106647
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 165
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1073.999
c starts	: 155
c conflicts	: 42
c decisions	: 177533
c propagations	: 1470456
c inspects	: 2120074
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 166
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1079.147
c starts	: 156
c conflicts	: 42
c decisions	: 178619
c propagations	: 1479781
c inspects	: 2133501
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 167
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1084.371
c starts	: 157
c conflicts	: 42
c decisions	: 179705
c propagations	: 1489106
c inspects	: 2146928
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 168
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1089.507
c starts	: 158
c conflicts	: 42
c decisions	: 180791
c propagations	: 1498431
c inspects	: 2160355
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 169
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1094.639
c starts	: 159
c conflicts	: 42
c decisions	: 181877
c propagations	: 1507756
c inspects	: 2173782
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 170
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1099.782
c starts	: 160
c conflicts	: 42
c decisions	: 182963
c propagations	: 1517081
c inspects	: 2187209
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 171
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1104.95
c starts	: 161
c conflicts	: 42
c decisions	: 184049
c propagations	: 1526406
c inspects	: 2200636
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 172
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1110.1
c starts	: 162
c conflicts	: 42
c decisions	: 185135
c propagations	: 1535731
c inspects	: 2214063
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 173
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1115.21
c starts	: 163
c conflicts	: 42
c decisions	: 186221
c propagations	: 1545056
c inspects	: 2227490
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 174
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1120.323
c starts	: 164
c conflicts	: 42
c decisions	: 187307
c propagations	: 1554381
c inspects	: 2240917
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 175
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1125.547
c starts	: 165
c conflicts	: 42
c decisions	: 188393
c propagations	: 1563706
c inspects	: 2254344
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 176
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1130.702
c starts	: 166
c conflicts	: 42
c decisions	: 189479
c propagations	: 1573031
c inspects	: 2267771
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 177
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1135.886
c starts	: 167
c conflicts	: 42
c decisions	: 190565
c propagations	: 1582356
c inspects	: 2281198
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 178
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1141.089
c starts	: 168
c conflicts	: 42
c decisions	: 191651
c propagations	: 1591681
c inspects	: 2294625
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 179
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1146.317
c starts	: 169
c conflicts	: 42
c decisions	: 192737
c propagations	: 1601006
c inspects	: 2308052
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 180
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1151.548
c starts	: 170
c conflicts	: 42
c decisions	: 193823
c propagations	: 1610331
c inspects	: 2321479
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 181
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1156.758
c starts	: 171
c conflicts	: 42
c decisions	: 194909
c propagations	: 1619656
c inspects	: 2334906
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 182
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1162.014
c starts	: 172
c conflicts	: 42
c decisions	: 195995
c propagations	: 1628981
c inspects	: 2348333
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 183
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1167.192
c starts	: 173
c conflicts	: 42
c decisions	: 197081
c propagations	: 1638306
c inspects	: 2361760
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 184
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1172.413
c starts	: 174
c conflicts	: 42
c decisions	: 198167
c propagations	: 1647631
c inspects	: 2375187
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 185
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1177.667
c starts	: 175
c conflicts	: 42
c decisions	: 199253
c propagations	: 1656956
c inspects	: 2388614
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 186
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1182.92
c starts	: 176
c conflicts	: 42
c decisions	: 200339
c propagations	: 1666281
c inspects	: 2402041
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 187
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1188.16
c starts	: 177
c conflicts	: 42
c decisions	: 201425
c propagations	: 1675606
c inspects	: 2415468
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 188
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1193.514
c starts	: 178
c conflicts	: 42
c decisions	: 202511
c propagations	: 1684931
c inspects	: 2428895
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 189
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1198.75
c starts	: 179
c conflicts	: 42
c decisions	: 203597
c propagations	: 1694256
c inspects	: 2442322
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 190
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1204.021
c starts	: 180
c conflicts	: 42
c decisions	: 204683
c propagations	: 1703581
c inspects	: 2455749
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 191
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1209.285
c starts	: 181
c conflicts	: 42
c decisions	: 205769
c propagations	: 1712906
c inspects	: 2469176
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 192
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1214.54
c starts	: 182
c conflicts	: 42
c decisions	: 206855
c propagations	: 1722231
c inspects	: 2482603
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 193
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1219.808
c starts	: 183
c conflicts	: 42
c decisions	: 207941
c propagations	: 1731556
c inspects	: 2496030
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 194
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1225.152
c starts	: 184
c conflicts	: 42
c decisions	: 209027
c propagations	: 1740881
c inspects	: 2509457
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 195
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1230.42
c starts	: 185
c conflicts	: 42
c decisions	: 210113
c propagations	: 1750206
c inspects	: 2522884
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 196
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1235.721
c starts	: 186
c conflicts	: 42
c decisions	: 211199
c propagations	: 1759531
c inspects	: 2536311
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 197
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1241.035
c starts	: 187
c conflicts	: 42
c decisions	: 212285
c propagations	: 1768856
c inspects	: 2549738
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 198
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1246.368
c starts	: 188
c conflicts	: 42
c decisions	: 213371
c propagations	: 1778181
c inspects	: 2563165
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 199
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1251.683
c starts	: 189
c conflicts	: 42
c decisions	: 214457
c propagations	: 1787506
c inspects	: 2576592
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 200
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1257.19
c starts	: 190
c conflicts	: 42
c decisions	: 215543
c propagations	: 1796831
c inspects	: 2590019
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 201
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1262.568
c starts	: 191
c conflicts	: 42
c decisions	: 216629
c propagations	: 1806156
c inspects	: 2603446
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 202
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1267.905
c starts	: 192
c conflicts	: 42
c decisions	: 217715
c propagations	: 1815481
c inspects	: 2616873
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 203
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1273.157
c starts	: 193
c conflicts	: 42
c decisions	: 218801
c propagations	: 1824806
c inspects	: 2630300
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 204
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1278.382
c starts	: 194
c conflicts	: 42
c decisions	: 219887
c propagations	: 1834131
c inspects	: 2643727
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 205
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1283.78
c starts	: 195
c conflicts	: 42
c decisions	: 220973
c propagations	: 1843456
c inspects	: 2657154
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 206
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1289.108
c starts	: 196
c conflicts	: 42
c decisions	: 222059
c propagations	: 1852781
c inspects	: 2670581
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 207
c 
c CURRENT OPTIMUM=-1725460008
c Current CPU time (ms) : 1294.468
c starts	: 197
c conflicts	: 42
c decisions	: 223145
c propagations	: 1862106
c inspects	: 2684008
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 42
c root simplifications	: 208
#### 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.85 0.94 0.91 2/54 7640
Raw data (stat): 7640 (runsolver) R 7639 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548736980 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.0011 s]
Raw data (loadavg): 1.02 0.97 0.92 2/63 7649
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 17974 0 1 0 889 37 0 0 25 0 10 0 548736980 853704704 19244 4294967295 134512640 134569956 3221224400 3221214700 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208424 19244 13073 16 0 208408 0
vsize: 833696
[startup+20.005 s]
Raw data (loadavg): 1.01 0.97 0.92 2/63 7649
Raw data (stat): 7640 (java) S 7639 27222 27221 0 -1 0 17978 0 1 0 1714 37 0 0 25 0 10 0 548736980 858951680 21327 4294967295 134512640 134569956 3221224400 3221213408 1073952481 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209705 21327 13073 16 0 209689 0
vsize: 838820
[startup+30.006 s]
Raw data (loadavg): 1.08 0.99 0.93 2/63 7649
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 17980 0 1 0 2582 38 0 0 18 0 10 0 548736980 858918912 21823 4294967295 134512640 134569956 3221224400 3221214280 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209697 21823 13073 16 0 209681 0
vsize: 838788
[startup+40.0064 s]
Raw data (loadavg): 1.07 0.99 0.93 2/63 7649
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 17980 0 1 0 3471 38 0 0 24 0 10 0 548736980 858918912 22308 4294967295 134512640 134569956 3221224400 3221214280 1080019614 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209697 22308 13073 16 0 209681 0
vsize: 838788
[startup+50.0081 s]
Raw data (loadavg): 1.06 0.99 0.93 2/63 7649
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 17980 0 1 0 4385 38 0 0 25 0 10 0 548736980 858918912 22495 4294967295 134512640 134569956 3221224400 3221214812 1080204163 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209697 22495 13073 16 0 209681 0
vsize: 838788
[startup+60.0535 s]
Raw data (loadavg): 1.05 0.99 0.93 3/63 7649
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 17980 0 1 0 5306 38 0 0 25 0 10 0 548736980 859967488 22718 4294967295 134512640 134569956 3221224400 3221214280 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209953 22718 13073 16 0 209937 0
vsize: 839812
[startup+70.0546 s]
Raw data (loadavg): 1.04 0.99 0.93 2/64 7650
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18009 0 1 0 6243 39 0 0 25 0 11 0 548736980 861544448 24778 4294967295 134512640 134569956 3221224400 3221214768 1131367034 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 24778 13073 16 0 210322 0
vsize: 841352
[startup+80.0558 s]
Raw data (loadavg): 1.04 0.99 0.93 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18010 4 1 0 7201 40 0 0 25 0 11 0 548736980 861544448 24823 4294967295 134512640 134569956 3221224400 3221214664 1131315850 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 24823 13073 16 0 210322 0
vsize: 841352
[startup+90.0558 s]
Raw data (loadavg): 1.11 1.01 0.93 3/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18049 4 1 0 8094 40 0 0 25 0 11 0 548736980 861679616 24945 4294967295 134512640 134569956 3221224400 3221214600 1131277418 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210371 24945 13073 16 0 210355 0
vsize: 841484
[startup+100.057 s]
Raw data (loadavg): 1.17 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18050 4 1 0 9037 40 0 0 25 0 11 0 548736980 861544448 24978 4294967295 134512640 134569956 3221224400 3221214544 1131526719 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 24978 13073 16 0 210322 0
vsize: 841352
[startup+110.058 s]
Raw data (loadavg): 1.14 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 9989 40 0 0 20 0 11 0 548736980 861544448 24918 4294967295 134512640 134569956 3221224400 3221214352 1131277209 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 24918 13073 16 0 210322 0
vsize: 841352
[startup+120.058 s]
Raw data (loadavg): 1.12 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 10952 41 0 0 25 0 11 0 548736980 861544448 25153 4294967295 134512640 134569956 3221224400 3221214352 1131277209 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 25153 13073 16 0 210322 0
vsize: 841352
[startup+130.058 s]
Raw data (loadavg): 1.10 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 11922 41 0 0 25 0 11 0 548736980 861544448 25171 4294967295 134512640 134569956 3221224400 3221214352 1131277110 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 25171 13073 16 0 210322 0
vsize: 841352
[startup+140.077 s]
Raw data (loadavg): 1.08 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 12898 41 0 0 25 0 11 0 548736980 861544448 25378 4294967295 134512640 134569956 3221224400 3221214352 1131277353 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 25378 13073 16 0 210322 0
vsize: 841352
[startup+150.088 s]
Raw data (loadavg): 1.07 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 13894 41 0 0 25 0 11 0 548736980 861544448 25499 4294967295 134512640 134569956 3221224400 3221214544 1131524208 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 25499 13073 16 0 210322 0
vsize: 841352
[startup+160.088 s]
Raw data (loadavg): 1.13 1.03 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 14892 41 0 0 25 0 11 0 548736980 861544448 25500 4294967295 134512640 134569956 3221224400 3221214528 1131565735 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 25500 13073 16 0 210322 0
vsize: 841352
[startup+170.088 s]
Raw data (loadavg): 1.11 1.03 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 15890 42 0 0 25 0 11 0 548736980 861544448 25500 4294967295 134512640 134569956 3221224400 3221214544 1131524333 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 25500 13073 16 0 210322 0
vsize: 841352
[startup+180.089 s]
Raw data (loadavg): 1.09 1.03 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 16888 42 0 0 25 0 11 0 548736980 861544448 25500 4294967295 134512640 134569956 3221224400 3221214352 1131277059 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25500 13073 16 0 210322 0
vsize: 841352
[startup+190.108 s]
Raw data (loadavg): 1.08 1.03 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 17887 42 0 0 25 0 11 0 548736980 861544448 25502 4294967295 134512640 134569956 3221224400 3221214544 1131524211 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25502 13073 16 0 210322 0
vsize: 841352
[startup+200.109 s]
Raw data (loadavg): 1.07 1.03 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 18883 42 0 0 25 0 11 0 548736980 861544448 25505 4294967295 134512640 134569956 3221224400 3221214352 1131277434 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25505 13073 16 0 210322 0
vsize: 841352
[startup+210.109 s]
Raw data (loadavg): 1.06 1.03 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 19875 42 0 0 25 0 11 0 548736980 861544448 25505 4294967295 134512640 134569956 3221224400 3221214352 1131277260 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25505 13073 16 0 210322 0
vsize: 841352
[startup+220.109 s]
Raw data (loadavg): 1.05 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 20869 42 0 0 25 0 11 0 548736980 861544448 25505 4294967295 134512640 134569956 3221224400 3221214456 1131346172 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25505 13073 16 0 210322 0
vsize: 841352
[startup+230.11 s]
Raw data (loadavg): 1.04 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 21864 42 0 0 25 0 11 0 548736980 861544448 25505 4294967295 134512640 134569956 3221224400 3221214544 1131526740 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25505 13073 16 0 210322 0
vsize: 841352
[startup+240.11 s]
Raw data (loadavg): 1.03 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 22853 43 0 0 25 0 11 0 548736980 861544448 25506 4294967295 134512640 134569956 3221224400 3221214640 1131633232 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25506 13073 16 0 210322 0
vsize: 841352
[startup+250.112 s]
Raw data (loadavg): 1.03 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 23846 43 0 0 25 0 11 0 548736980 861544448 25537 4294967295 134512640 134569956 3221224400 3221214640 1131633196 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25537 13073 16 0 210322 0
vsize: 841352
[startup+260.113 s]
Raw data (loadavg): 1.02 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 24842 43 0 0 25 0 11 0 548736980 861544448 25537 4294967295 134512640 134569956 3221224400 3221214528 1131564635 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 25537 13073 16 0 210322 0
vsize: 841352
[startup+270.113 s]
Raw data (loadavg): 1.02 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 25838 43 0 0 25 0 11 0 548736980 861544448 25537 4294967295 134512640 134569956 3221224400 3221214528 1131564745 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25537 13073 16 0 210322 0
vsize: 841352
[startup+280.113 s]
Raw data (loadavg): 1.02 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 26835 43 0 0 25 0 11 0 548736980 861544448 25537 4294967295 134512640 134569956 3221224400 3221214528 1131564745 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25537 13073 16 0 210322 0
vsize: 841352
[startup+290.114 s]
Raw data (loadavg): 1.01 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 27832 43 0 0 25 0 11 0 548736980 861544448 25582 4294967295 134512640 134569956 3221224400 3221214616 1131245017 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25582 13073 16 0 210322 0
vsize: 841352
[startup+300.114 s]
Raw data (loadavg): 1.01 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 28831 43 0 0 25 0 11 0 548736980 861544448 25582 4294967295 134512640 134569956 3221224400 3221214664 1131580003 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25582 13073 16 0 210322 0
vsize: 841352
[startup+310.114 s]
Raw data (loadavg): 1.01 1.02 0.94 2/64 7651
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 29822 43 0 0 25 0 11 0 548736980 861544448 25585 4294967295 134512640 134569956 3221224400 3221214760 1131363042 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25585 13073 16 0 210322 0
vsize: 841352
[startup+320.114 s]
Raw data (loadavg): 1.01 1.01 0.94 2/64 7652
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18051 4 1 0 30809 44 0 0 25 0 11 0 548736980 861544448 25591 4294967295 134512640 134569956 3221224400 3221214800 1131364243 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25591 13073 16 0 210322 0
vsize: 841352
[startup+330.115 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 7653
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 31783 44 0 0 25 0 11 0 548736980 861544448 25592 4294967295 134512640 134569956 3221224400 3221214800 1131363042 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 25592 13073 16 0 210322 0
vsize: 841352
[startup+340.116 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 7654
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 32731 44 0 0 25 0 11 0 548736980 861544448 25593 4294967295 134512640 134569956 3221224400 3221214704 1131314969 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 25593 13073 16 0 210322 0
vsize: 841352
[startup+350.117 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 7656
Raw data (stat): 7640 (java) S 7639 27222 27221 0 -1 0 18052 4 1 0 33645 45 0 0 25 0 11 0 548736980 861544448 25619 4294967295 134512640 134569956 3221224400 3221213448 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 25619 13073 16 0 210322 0
vsize: 841352
[startup+360.117 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 7658
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 34553 45 0 0 25 0 11 0 548736980 861544448 26007 4294967295 134512640 134569956 3221224400 3221214704 1131314928 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 26007 13073 16 0 210322 0
vsize: 841352
[startup+370.117 s]
Raw data (loadavg): 1.00 1.01 0.94 2/64 7661
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 35463 45 0 0 25 0 11 0 548736980 861544448 26438 4294967295 134512640 134569956 3221224400 3221214800 1131363042 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 26438 13073 16 0 210322 0
vsize: 841352
[startup+380.118 s]
Raw data (loadavg): 1.07 1.03 0.95 2/64 7663
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 36384 46 0 0 25 0 11 0 548736980 861544448 26748 4294967295 134512640 134569956 3221224400 3221214800 1131367044 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 26748 13073 16 0 210322 0
vsize: 841352
[startup+390.118 s]
Raw data (loadavg): 1.06 1.02 0.95 2/64 7665
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 37290 46 1 0 25 0 11 0 548736980 861544448 27136 4294967295 134512640 134569956 3221224400 3221214800 1131364086 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 27136 13073 16 0 210322 0
vsize: 841352
[startup+400.12 s]
Raw data (loadavg): 1.05 1.02 0.95 2/64 7667
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 38206 47 1 0 25 0 11 0 548736980 861544448 27671 4294967295 134512640 134569956 3221224400 3221214704 1131315472 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 27671 13073 16 0 210322 0
vsize: 841352
[startup+410.12 s]
Raw data (loadavg): 1.04 1.02 0.95 2/64 7669
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 39128 47 1 0 24 0 11 0 548736980 861544448 28139 4294967295 134512640 134569956 3221224400 3221214736 1131381461 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 28139 13073 16 0 210322 0
vsize: 841352
[startup+420.12 s]
Raw data (loadavg): 1.04 1.02 0.95 2/64 7671
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 40054 47 1 0 25 0 11 0 548736980 861544448 28531 4294967295 134512640 134569956 3221224400 3221214704 1131315843 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 28531 13073 16 0 210322 0
vsize: 841352
[startup+430.121 s]
Raw data (loadavg): 1.03 1.02 0.95 2/64 7674
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 40971 47 1 0 25 0 11 0 548736980 861544448 28782 4294967295 134512640 134569956 3221224400 3221214800 1131364134 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 28782 13073 16 0 210322 0
vsize: 841352
[startup+440.122 s]
Raw data (loadavg): 1.02 1.02 0.95 2/64 7676
Raw data (stat): 7640 (java) S 7639 27222 27221 0 -1 0 18052 4 1 0 41877 48 1 0 25 0 11 0 548736980 861544448 29134 4294967295 134512640 134569956 3221224400 3221213448 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 29134 13073 16 0 210322 0
vsize: 841352
[startup+450.122 s]
Raw data (loadavg): 1.02 1.02 0.95 2/64 7678
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 42776 48 1 0 25 0 11 0 548736980 861544448 29498 4294967295 134512640 134569956 3221224400 3221214800 1131365163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 29498 13073 16 0 210322 0
vsize: 841352
[startup+460.122 s]
Raw data (loadavg): 1.02 1.02 0.95 2/64 7680
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 43698 49 1 0 25 0 11 0 548736980 861544448 30405 4294967295 134512640 134569956 3221224400 3221214704 1131314969 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 30405 13073 16 0 210322 0
vsize: 841352
[startup+470.123 s]
Raw data (loadavg): 1.01 1.02 0.95 2/64 7682
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 44625 49 1 0 25 0 11 0 548736980 861544448 31005 4294967295 134512640 134569956 3221224400 3221214704 1131314969 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 31005 13073 16 0 210322 0
vsize: 841352
[startup+480.123 s]
Raw data (loadavg): 1.01 1.02 0.95 2/64 7684
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 45549 49 1 0 25 0 11 0 548736980 861544448 31126 4294967295 134512640 134569956 3221224400 3221214704 1131314969 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 31126 13073 16 0 210322 0
vsize: 841352
[startup+490.123 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 7686
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 46458 49 1 0 25 0 11 0 548736980 861544448 31397 4294967295 134512640 134569956 3221224400 3221214800 1131363074 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 31397 13073 16 0 210322 0
vsize: 841352
[startup+500.123 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 7689
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 47376 50 2 0 25 0 11 0 548736980 861544448 31892 4294967295 134512640 134569956 3221224400 3221214864 1131346092 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 31892 13073 16 0 210322 0
vsize: 841352
[startup+510.124 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 7691
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 48301 50 2 0 25 0 11 0 548736980 861544448 32254 4294967295 134512640 134569956 3221224400 3221214800 1131364056 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 32254 13073 16 0 210322 0
vsize: 841352
[startup+520.124 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 7693
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 49215 50 2 0 25 0 11 0 548736980 861544448 32859 4294967295 134512640 134569956 3221224400 3221214800 1131367171 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 32859 13073 16 0 210322 0
vsize: 841352
[startup+530.124 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 7695
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 50133 51 2 0 25 0 11 0 548736980 861544448 33128 4294967295 134512640 134569956 3221224400 3221214800 1131367104 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 33128 13073 16 0 210322 0
vsize: 841352
[startup+540.128 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 7697
Raw data (stat): 7640 (java) S 7639 27222 27221 0 -1 0 18052 4 1 0 51039 51 2 0 25 0 11 0 548736980 861544448 33448 4294967295 134512640 134569956 3221224400 3221213448 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 33448 13073 16 0 210322 0
vsize: 841352
[startup+550.129 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 7699
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 51941 51 2 0 18 0 11 0 548736980 861544448 33785 4294967295 134512640 134569956 3221224400 3221214968 1131246041 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 33785 13073 16 0 210322 0
vsize: 841352
[startup+560.13 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 7701
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 52853 51 2 0 25 0 11 0 548736980 861544448 34005 4294967295 134512640 134569956 3221224400 3221214800 1131365148 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 34005 13073 16 0 210322 0
vsize: 841352
[startup+570.13 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 7703
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 53757 51 2 1 25 0 11 0 548736980 861544448 34738 4294967295 134512640 134569956 3221224400 3221214704 1131315809 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 34738 13073 16 0 210322 0
vsize: 841352
[startup+580.131 s]
Raw data (loadavg): 1.07 1.02 0.95 2/64 7706
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 54708 51 2 1 25 0 11 0 548736980 861544448 36455 4294967295 134512640 134569956 3221224400 3221214800 1131367147 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 36455 13073 16 0 210322 0
vsize: 841352
[startup+590.13 s]
Raw data (loadavg): 1.06 1.02 0.95 2/64 7708
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 55644 52 2 1 24 0 11 0 548736980 861544448 36455 4294967295 134512640 134569956 3221224400 3221214704 1131314401 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 36455 13073 16 0 210322 0
vsize: 841352
[startup+600.131 s]
Raw data (loadavg): 1.05 1.02 0.95 2/64 7710
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 56558 52 2 1 25 0 11 0 548736980 861544448 36458 4294967295 134512640 134569956 3221224400 3221214704 1131314907 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 36458 13073 16 0 210322 0
vsize: 841352
[startup+610.132 s]
Raw data (loadavg): 1.04 1.02 0.95 2/64 7712
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 57467 52 2 1 25 0 11 0 548736980 861544448 36822 4294967295 134512640 134569956 3221224400 3221214704 1131315880 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 36822 13073 16 0 210322 0
vsize: 841352
[startup+620.132 s]
Raw data (loadavg): 1.04 1.02 0.95 2/64 7714
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 58374 53 2 1 25 0 11 0 548736980 861544448 37081 4294967295 134512640 134569956 3221224400 3221214704 1131314855 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 37081 13073 16 0 210322 0
vsize: 841352
[startup+630.132 s]
Raw data (loadavg): 1.03 1.02 0.95 2/64 7716
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 59282 53 2 1 25 0 11 0 548736980 861544448 37343 4294967295 134512640 134569956 3221224400 3221214704 1131315041 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 37343 13073 16 0 210322 0
vsize: 841352
[startup+640.134 s]
Raw data (loadavg): 1.02 1.02 0.95 2/64 7718
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 60190 54 2 1 25 0 11 0 548736980 861544448 37611 4294967295 134512640 134569956 3221224400 3221214704 1131314405 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 37611 13073 16 0 210322 0
vsize: 841352
[startup+650.134 s]
Raw data (loadavg): 1.02 1.02 0.95 2/64 7720
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 61103 54 3 1 25 0 11 0 548736980 861544448 38009 4294967295 134512640 134569956 3221224400 3221214704 1131315016 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 38009 13073 16 0 210322 0
vsize: 841352
[startup+660.134 s]
Raw data (loadavg): 1.02 1.01 0.95 2/64 7722
Raw data (stat): 7640 (java) S 7639 27222 27221 0 -1 0 18052 4 1 0 62017 54 3 1 25 0 11 0 548736980 861544448 38342 4294967295 134512640 134569956 3221224400 3221213344 1073952481 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 38342 13073 16 0 210322 0
vsize: 841352
[startup+670.134 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 7724
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 62930 54 3 1 25 0 11 0 548736980 861544448 38732 4294967295 134512640 134569956 3221224400 3221214704 1131314969 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 38732 13073 16 0 210322 0
vsize: 841352
[startup+680.135 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 7726
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 63849 55 3 1 25 0 11 0 548736980 861544448 39213 4294967295 134512640 134569956 3221224400 3221214704 1131314412 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 39213 13073 16 0 210322 0
vsize: 841352
[startup+690.135 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 7728
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 64771 55 3 1 25 0 11 0 548736980 861544448 39603 4294967295 134512640 134569956 3221224400 3221214704 1131314397 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 39603 13073 16 0 210322 0
vsize: 841352
[startup+700.136 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 7730
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 65691 55 3 1 25 0 11 0 548736980 861544448 40069 4294967295 134512640 134569956 3221224400 3221214704 1131315258 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 40069 13073 16 0 210322 0
vsize: 841352
[startup+710.137 s]
Raw data (loadavg): 1.01 1.01 0.95 2/64 7732
Raw data (stat): 7640 (java) S 7639 27222 27221 0 -1 0 18052 4 1 0 66610 56 3 1 25 0 11 0 548736980 861544448 40446 4294967295 134512640 134569956 3221224400 3221213408 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 40446 13073 16 0 210322 0
vsize: 841352
[startup+720.136 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 7734
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 67526 56 3 1 25 0 11 0 548736980 861544448 40959 4294967295 134512640 134569956 3221224400 3221214800 1131367104 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 40959 13073 16 0 210322 0
vsize: 841352
[startup+730.137 s]
Raw data (loadavg): 1.00 1.01 0.95 2/63 7736
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 68441 56 3 1 25 0 10 0 548736980 861544448 41254 4294967295 134512640 134569956 3221224400 3221214280 1131261951 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 41254 13073 16 0 210322 0
vsize: 841352
[startup+740.137 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 7739
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 69357 57 3 1 25 0 11 0 548736980 861544448 41455 4294967295 134512640 134569956 3221224400 3221214760 1131277209 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 41455 13073 16 0 210322 0
vsize: 841352
[startup+750.138 s]
Raw data (loadavg): 1.00 1.01 0.95 2/64 7741
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 70269 57 4 1 25 0 11 0 548736980 861544448 41829 4294967295 134512640 134569956 3221224400 3221214864 1131346024 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 41829 13073 16 0 210322 0
vsize: 841352
[startup+760.138 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7743
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 71182 57 4 1 25 0 11 0 548736980 861544448 42164 4294967295 134512640 134569956 3221224400 3221214800 1131367074 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 42164 13073 16 0 210322 0
vsize: 841352
[startup+770.138 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7745
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 72087 57 4 1 25 0 11 0 548736980 861544448 42665 4294967295 134512640 134569956 3221224400 3221214704 1131314710 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 42665 13073 16 0 210322 0
vsize: 841352
[startup+780.138 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7747
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 72999 58 4 1 25 0 11 0 548736980 861544448 42970 4294967295 134512640 134569956 3221224400 3221214800 1131365013 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 42970 13073 16 0 210322 0
vsize: 841352
[startup+790.138 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7749
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 73919 58 4 1 25 0 11 0 548736980 861544448 43261 4294967295 134512640 134569956 3221224400 3221214704 1131314412 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 43261 13073 16 0 210322 0
vsize: 841352
[startup+800.139 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7751
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 74825 59 4 1 25 0 11 0 548736980 861544448 43451 4294967295 134512640 134569956 3221224400 3221214704 1131315142 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 43451 13073 16 0 210322 0
vsize: 841352
[startup+810.139 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7753
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 75725 59 4 1 25 0 11 0 548736980 861544448 45560 4294967295 134512640 134569956 3221224400 3221214704 1131314651 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 45560 13073 16 0 210322 0
vsize: 841352
[startup+820.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7755
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 76632 60 4 1 25 0 11 0 548736980 861544448 45835 4294967295 134512640 134569956 3221224400 3221214760 1131277418 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 45835 13073 16 0 210322 0
vsize: 841352
[startup+830.141 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7757
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 77541 60 4 1 25 0 11 0 548736980 861544448 46110 4294967295 134512640 134569956 3221224400 3221214760 1131277059 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 46110 13073 16 0 210322 0
vsize: 841352
[startup+840.141 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7759
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 78452 60 4 1 25 0 11 0 548736980 861544448 46380 4294967295 134512640 134569956 3221224400 3221214864 1131346017 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 46380 13073 16 0 210322 0
vsize: 841352
[startup+850.141 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7761
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 79358 61 4 2 25 0 11 0 548736980 861544448 46634 4294967295 134512640 134569956 3221224400 3221214760 1131277059 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 46634 13073 16 0 210322 0
vsize: 841352
[startup+860.142 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7763
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 80265 61 5 2 25 0 11 0 548736980 861544448 46877 4294967295 134512640 134569956 3221224400 3221214864 1131346024 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 46877 13073 16 0 210322 0
vsize: 841352
[startup+870.142 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7765
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 81173 62 5 2 25 0 11 0 548736980 861544448 47149 4294967295 134512640 134569956 3221224400 3221214760 1131277059 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 47149 13073 16 0 210322 0
vsize: 841352
[startup+880.142 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7766
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 82081 62 5 2 25 0 11 0 548736980 861544448 47398 4294967295 134512640 134569956 3221224400 3221214696 1131277236 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 47398 13073 16 0 210322 0
vsize: 841352
[startup+890.143 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7768
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 82987 63 5 2 24 0 11 0 548736980 861544448 47646 4294967295 134512640 134569956 3221224400 3221214704 1131314661 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 47646 13073 16 0 210322 0
vsize: 841352
[startup+900.144 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7770
Raw data (stat): 7640 (java) S 7639 27222 27221 0 -1 0 18052 4 1 0 83901 63 5 2 25 0 11 0 548736980 861544448 47886 4294967295 134512640 134569956 3221224400 3221213408 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 47886 13073 16 0 210322 0
vsize: 841352
[startup+910.144 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7772
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 84810 63 5 2 25 0 11 0 548736980 861544448 48139 4294967295 134512640 134569956 3221224400 3221214704 1131314969 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 48139 13073 16 0 210322 0
vsize: 841352
[startup+920.146 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7774
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 85716 64 5 2 22 0 11 0 548736980 861544448 48430 4294967295 134512640 134569956 3221224400 3221214704 1131315748 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 48430 13073 16 0 210322 0
vsize: 841352
[startup+930.146 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7776
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 86622 64 5 2 25 0 11 0 548736980 861544448 48669 4294967295 134512640 134569956 3221224400 3221214704 1131315130 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 48669 13073 16 0 210322 0
vsize: 841352
[startup+940.146 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7778
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 87528 65 5 2 25 0 11 0 548736980 861544448 48921 4294967295 134512640 134569956 3221224400 3221214704 1131315202 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 48921 13073 16 0 210322 0
vsize: 841352
[startup+950.147 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7780
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 88434 65 5 2 25 0 11 0 548736980 861544448 49193 4294967295 134512640 134569956 3221224400 3221214704 1131314969 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 49193 13073 16 0 210322 0
vsize: 841352
[startup+960.147 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7782
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 89338 66 5 2 25 0 11 0 548736980 861544448 49455 4294967295 134512640 134569956 3221224400 3221214704 1131314651 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 49455 13073 16 0 210322 0
vsize: 841352
[startup+970.147 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7784
Raw data (stat): 7640 (java) S 7639 27222 27221 0 -1 0 18052 4 1 0 90244 66 6 2 25 0 11 0 548736980 861544448 49734 4294967295 134512640 134569956 3221224400 3221213448 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 49734 13073 16 0 210322 0
vsize: 841352
[startup+980.149 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7786
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 91161 66 6 2 25 0 11 0 548736980 861544448 49992 4294967295 134512640 134569956 3221224400 3221214704 1131314401 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 49992 13073 16 0 210322 0
vsize: 841352
[startup+990.149 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7788
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 92068 67 6 2 25 0 11 0 548736980 861544448 50311 4294967295 134512640 134569956 3221224400 3221214704 1131314876 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 50311 13073 16 0 210322 0
vsize: 841352
[startup+1000.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7790
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 92976 68 6 2 25 0 11 0 548736980 861544448 50755 4294967295 134512640 134569956 3221224400 3221214704 1131315122 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210338 50755 13073 16 0 210322 0
vsize: 841352
[startup+1010.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7792
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 93889 68 6 2 25 0 11 0 548736980 861544448 51049 4294967295 134512640 134569956 3221224400 3221214704 1131314401 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 51049 13073 16 0 210322 0
vsize: 841352
[startup+1020.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7794
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 94802 68 6 2 25 0 11 0 548736980 861544448 51448 4294967295 134512640 134569956 3221224400 3221214704 1131315738 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 51448 13073 16 0 210322 0
vsize: 841352
[startup+1030.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7796
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 95714 69 6 2 25 0 11 0 548736980 861544448 51805 4294967295 134512640 134569956 3221224400 3221214704 1131315308 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 51805 13073 16 0 210322 0
vsize: 841352
[startup+1040.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7798
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 96633 69 6 2 25 0 11 0 548736980 861544448 52082 4294967295 134512640 134569956 3221224400 3221214704 1131315799 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 52082 13073 16 0 210322 0
vsize: 841352
[startup+1050.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7800
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 97553 70 6 2 25 0 11 0 548736980 861544448 52429 4294967295 134512640 134569956 3221224400 3221214800 1131367074 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 52429 13073 16 0 210322 0
vsize: 841352
[startup+1060.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7802
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 98471 71 6 2 25 0 11 0 548736980 861544448 52782 4294967295 134512640 134569956 3221224400 3221214704 1131315284 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 52782 13073 16 0 210322 0
vsize: 841352
[startup+1070.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7804
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 99390 71 6 2 24 0 11 0 548736980 861544448 53421 4294967295 134512640 134569956 3221224400 3221214760 1131277170 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 53421 13073 16 0 210322 0
vsize: 841352
[startup+1080.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7806
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 100310 72 6 2 25 0 11 0 548736980 861544448 53646 4294967295 134512640 134569956 3221224400 3221214760 1131277218 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 53646 13073 16 0 210322 0
vsize: 841352
[startup+1090.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/63 7807
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 101232 72 6 2 25 0 10 0 548736980 861544448 54182 4294967295 134512640 134569956 3221224400 3221213088 1131301543 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 54182 13073 16 0 210322 0
vsize: 841352
[startup+1100.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7809
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 102154 72 6 2 25 0 11 0 548736980 861544448 54457 4294967295 134512640 134569956 3221224400 3221214800 1131367077 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 54457 13073 16 0 210322 0
vsize: 841352
[startup+1110.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7811
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 103074 73 7 2 25 0 11 0 548736980 861544448 55136 4294967295 134512640 134569956 3221224400 3221214800 1131365048 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 55136 13073 16 0 210322 0
vsize: 841352
[startup+1120.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7813
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 104003 73 7 3 25 0 11 0 548736980 861544448 55478 4294967295 134512640 134569956 3221224400 3221214704 1131314433 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 55478 13073 16 0 210322 0
vsize: 841352
[startup+1130.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7815
Raw data (stat): 7640 (java) S 7639 27222 27221 0 -1 0 18052 4 1 0 104926 73 7 3 25 0 11 0 548736980 861544448 55976 4294967295 134512640 134569956 3221224400 3221213304 1073952481 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 55976 13073 16 0 210322 0
vsize: 841352
[startup+1140.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7817
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 105850 74 7 3 25 0 11 0 548736980 861544448 56133 4294967295 134512640 134569956 3221224400 3221214704 1131314969 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 56133 13073 16 0 210322 0
vsize: 841352
[startup+1150.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7819
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 106762 74 7 3 25 0 11 0 548736980 861544448 56396 4294967295 134512640 134569956 3221224400 3221214704 1131315162 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 56396 13073 16 0 210322 0
vsize: 841352
[startup+1160.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7821
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 107679 74 7 3 25 0 11 0 548736980 861544448 56966 4294967295 134512640 134569956 3221224400 3221214800 1131367163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 56966 13073 16 0 210322 0
vsize: 841352
[startup+1170.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7823
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 108601 75 7 3 25 0 11 0 548736980 861544448 57109 4294967295 134512640 134569956 3221224400 3221214704 1131315258 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 57109 13073 16 0 210322 0
vsize: 841352
[startup+1180.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7825
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 109510 75 7 3 24 0 11 0 548736980 861544448 57607 4294967295 134512640 134569956 3221224400 3221214704 1131314651 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 57607 13073 16 0 210322 0
vsize: 841352
[startup+1190.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7827
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 110431 75 7 3 25 0 11 0 548736980 861544448 57740 4294967295 134512640 134569956 3221224400 3221214704 1131315214 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 57740 13073 16 0 210322 0
vsize: 841352
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7829
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 111345 76 7 3 23 0 11 0 548736980 861544448 57979 4294967295 134512640 134569956 3221224400 3221214704 1131315130 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 57979 13073 16 0 210322 0
vsize: 841352
[startup+1210.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7831
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 112255 76 7 3 25 0 11 0 548736980 861544448 58412 4294967295 134512640 134569956 3221224400 3221214760 1131277209 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 58412 13073 16 0 210322 0
vsize: 841352
[startup+1220.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7832
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 113169 76 7 3 25 0 11 0 548736980 861544448 58682 4294967295 134512640 134569956 3221224400 3221214704 1131315126 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 58682 13073 16 0 210322 0
vsize: 841352
[startup+1230.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7834
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 114082 76 7 3 25 0 11 0 548736980 861544448 58982 4294967295 134512640 134569956 3221224400 3221214800 1131363183 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 58982 13073 16 0 210322 0
vsize: 841352
[startup+1240.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7836
Raw data (stat): 7640 (java) S 7639 27222 27221 0 -1 0 18052 4 1 0 114994 77 7 3 25 0 11 0 548736980 861544448 59267 4294967295 134512640 134569956 3221224400 3221213448 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 59267 13073 16 0 210322 0
vsize: 841352
[startup+1250.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7838
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 115902 77 8 3 21 0 11 0 548736980 861544448 59645 4294967295 134512640 134569956 3221224400 3221214704 1131315116 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 59645 13073 16 0 210322 0
vsize: 841352
[startup+1260.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7840
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 116797 78 8 3 25 0 11 0 548736980 861544448 60125 4294967295 134512640 134569956 3221224400 3221214704 1131314648 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 60125 13073 16 0 210322 0
vsize: 841352
[startup+1270.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7842
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 117709 78 8 3 25 0 11 0 548736980 861544448 60446 4294967295 134512640 134569956 3221224400 3221214704 1131315198 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 60446 13073 16 0 210322 0
vsize: 841352
[startup+1280.17 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7844
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 118634 79 8 3 25 0 11 0 548736980 861544448 60881 4294967295 134512640 134569956 3221224400 3221214800 1131364112 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 60881 13073 16 0 210322 0
vsize: 841352
[startup+1290.17 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7846
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 119545 79 8 4 25 0 11 0 548736980 861544448 61010 4294967295 134512640 134569956 3221224400 3221214948 1131236410 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 61010 13073 16 0 210322 0
vsize: 841352
[startup+1300.17 s]
Raw data (loadavg): 1.00 1.00 0.95 2/64 7847
Raw data (stat): 7640 (java) R 7639 27222 27221 0 -1 0 18052 4 1 0 120447 80 8 4 18 0 11 0 548736980 861544448 61328 4294967295 134512640 134569956 3221224400 3221214800 1131364134 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210338 61328 13073 16 0 210322 0
vsize: 841352
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1300.33 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 7849
Raw data (stat): 7640 (java) Z 7639 27222 27221 0 -1 1036 18052 47210 1 0 120451 91 10615 115 21 0 1 0 548736980 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): 1300.33
CPU time (s): 1312.75
CPU user time (s): 1310.68
CPU system time (s): 2.06969
CPU usage (%): 100.955
Max. virtual memory (Kb): 841484
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####