PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-set1ch.opb
MD5SUM	68664c9c03d64725e7986525f71ad273
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	1233.02
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 21992

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        409072 kB
Buffers:         32680 kB
Cached:         571396 kB
SwapCached:        444 kB
Active:         107780 kB
Inactive:       498408 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        408820 kB
SwapTotal:     2097136 kB
SwapFree:      2095948 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            13724 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:03:23 (client local time) WITH STATUS 143 IN 1312.96 SECONDS
stats: 12294 7 1312.96 143
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-set1ch.opb
c reading problem 
c [nbvar=14400]
c [nbconstr=732]
c time 61.604
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) : 71.739
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) : 320.273
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) : 330.478
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) : 336.746
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) : 342.915
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) : 347.574
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) : 352.124
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) : 356.808
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) : 361.504
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) : 366.21
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) : 370.933
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) : 375.491
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) : 380.141
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) : 384.821
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) : 389.501
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) : 394.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) : 398.849
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) : 403.497
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) : 408.158
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) : 412.75
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) : 417.386
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) : 422.0
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) : 426.687
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) : 431.407
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) : 436.151
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) : 440.889
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) : 445.654
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) : 450.337
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) : 455.133
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) : 459.815
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) : 464.45
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) : 469.071
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) : 473.69
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) : 478.344
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) : 482.972
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) : 487.696
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) : 492.423
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) : 497.159
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) : 501.853
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) : 506.542
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) : 511.247
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) : 515.865
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) : 520.568
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) : 525.288
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) : 530.021
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) : 534.814
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) : 539.595
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) : 544.405
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) : 549.212
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) : 553.935
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) : 558.726
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) : 563.522
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) : 568.355
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) : 573.275
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) : 577.822
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) : 582.384
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) : 587.013
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) : 591.706
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) : 596.476
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) : 601.204
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) : 606.052
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) : 610.898
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) : 615.743
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) : 620.595
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) : 625.465
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) : 630.323
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) : 635.19
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) : 640.079
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) : 644.966
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) : 649.813
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) : 654.703
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) : 659.429
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) : 664.267
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) : 669.22
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) : 674.066
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) : 678.913
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) : 683.757
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) : 688.597
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) : 693.429
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) : 698.285
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) : 703.144
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) : 707.99
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) : 712.838
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) : 717.688
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) : 722.57
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) : 727.454
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) : 732.383
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) : 737.276
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) : 742.189
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) : 747.103
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) : 752.027
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) : 756.964
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) : 761.909
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) : 766.906
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) : 771.875
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) : 776.716
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) : 781.676
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) : 786.596
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) : 791.518
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) : 796.485
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) : 801.482
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) : 806.506
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) : 811.735
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) : 816.739
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) : 821.747
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) : 826.762
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) : 831.772
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) : 836.764
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) : 841.759
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) : 846.782
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) : 851.816
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) : 856.852
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) : 861.887
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) : 866.931
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) : 871.974
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) : 877.024
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) : 882.067
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) : 887.125
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) : 892.19
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) : 897.242
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) : 902.305
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) : 907.369
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) : 912.431
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) : 917.503
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) : 922.572
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) : 927.653
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) : 932.741
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) : 937.836
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) : 942.934
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) : 948.033
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) : 953.138
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) : 958.237
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) : 963.358
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) : 968.47
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) : 973.692
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) : 978.778
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) : 983.893
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) : 989.023
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) : 994.149
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) : 999.261
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) : 1004.364
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) : 1009.475
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) : 1014.561
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) : 1019.67
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) : 1024.788
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) : 1029.924
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) : 1035.162
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) : 1040.229
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) : 1045.328
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) : 1050.424
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) : 1055.509
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) : 1060.625
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) : 1065.769
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) : 1070.873
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) : 1075.961
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) : 1081.099
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) : 1086.308
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) : 1091.429
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) : 1096.549
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) : 1101.681
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) : 1106.909
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) : 1112.045
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) : 1117.165
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) : 1122.306
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) : 1127.573
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) : 1132.769
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) : 1137.992
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) : 1143.224
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) : 1148.484
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) : 1153.746
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) : 1158.988
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) : 1164.282
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) : 1169.496
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) : 1174.747
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) : 1180.033
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) : 1185.318
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) : 1190.596
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) : 1195.979
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) : 1201.248
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) : 1206.551
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) : 1211.848
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) : 1217.134
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) : 1222.431
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) : 1227.818
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) : 1233.122
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) : 1238.461
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) : 1243.813
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) : 1249.179
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) : 1254.533
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) : 1260.076
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) : 1265.505
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) : 1270.872
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) : 1276.156
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) : 1281.419
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) : 1286.846
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) : 1292.209
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) : 1297.608
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.84 0.94 0.90 2/54 7175
Raw data (stat): 7175 (runsolver) R 7174 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491620006 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.0001 s]
Raw data (loadavg): 0.87 0.94 0.90 2/63 7184
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 17979 0 1 0 882 36 0 0 25 0 10 0 491620006 853393408 19272 4294967295 134512640 134569956 3221224400 3221214520 1080019600 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 208348 19272 13073 16 0 208332 0
vsize: 833392
[startup+20.0013 s]
Raw data (loadavg): 1.05 0.97 0.91 2/63 7184
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18002 0 1 0 1746 37 0 0 25 0 10 0 491620006 859590656 21483 4294967295 134512640 134569956 3221224400 3221214808 1131208460 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209861 21483 13073 16 0 209845 0
vsize: 839444
[startup+30.002 s]
Raw data (loadavg): 1.04 0.97 0.91 2/63 7184
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18004 0 1 0 2614 37 0 0 25 0 10 0 491620006 857309184 21481 4294967295 134512640 134569956 3221224400 3221214756 1130896152 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209304 21481 13073 16 0 209288 0
vsize: 837216
[startup+40.0014 s]
Raw data (loadavg): 1.11 0.99 0.92 2/63 7184
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18004 0 1 0 3499 37 0 0 25 0 10 0 491620006 857309184 21863 4294967295 134512640 134569956 3221224400 3221214708 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209304 21863 13073 16 0 209288 0
vsize: 837216
[startup+50.0021 s]
Raw data (loadavg): 1.09 0.99 0.92 2/63 7184
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18004 0 1 0 4419 38 0 0 25 0 10 0 491620006 857309184 22030 4294967295 134512640 134569956 3221224400 3221214708 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209304 22030 13073 16 0 209288 0
vsize: 837216
[startup+60.0023 s]
Raw data (loadavg): 1.08 0.99 0.92 3/63 7184
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18004 0 1 0 5332 38 0 0 25 0 10 0 491620006 858501120 22375 4294967295 134512640 134569956 3221224400 3221214708 1079677981 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209595 22375 13073 16 0 209579 0
vsize: 838380
[startup+70.0035 s]
Raw data (loadavg): 1.14 1.01 0.92 2/64 7185
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18033 0 1 0 6273 39 0 0 25 0 11 0 491620006 857837568 24078 4294967295 134512640 134569956 3221224400 3221214680 1131314689 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209433 24078 13073 16 0 209417 0
vsize: 837732
[startup+80.0048 s]
Raw data (loadavg): 1.19 1.02 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18034 4 1 0 7233 39 0 0 25 0 11 0 491620006 857837568 24094 4294967295 134512640 134569956 3221224400 3221214672 1131314220 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209433 24094 13073 16 0 209417 0
vsize: 837732
[startup+90.0045 s]
Raw data (loadavg): 1.16 1.02 0.93 3/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18076 4 1 0 8168 40 0 0 25 0 11 0 491620006 860102656 24543 4294967295 134512640 134569956 3221224400 3221214664 1131525956 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209986 24543 13073 16 0 209970 0
vsize: 839944
[startup+100.005 s]
Raw data (loadavg): 1.13 1.02 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18077 4 1 0 9113 41 0 0 25 0 11 0 491620006 859480064 24434 4294967295 134512640 134569956 3221224400 3221214520 1131562240 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 24434 13073 16 0 209818 0
vsize: 839336
[startup+110.006 s]
Raw data (loadavg): 1.11 1.02 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 10065 41 0 0 21 0 11 0 491620006 859480064 24438 4294967295 134512640 134569956 3221224400 3221214336 1131282146 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 24438 13073 16 0 209818 0
vsize: 839336
[startup+120.007 s]
Raw data (loadavg): 1.10 1.02 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 11027 41 0 0 25 0 11 0 491620006 859480064 24674 4294967295 134512640 134569956 3221224400 3221214440 1131346124 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 24674 13073 16 0 209818 0
vsize: 839336
[startup+130.007 s]
Raw data (loadavg): 1.08 1.02 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 11996 42 0 0 25 0 11 0 491620006 859480064 24691 4294967295 134512640 134569956 3221224400 3221214336 1131280257 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 24691 13073 16 0 209818 0
vsize: 839336
[startup+140.007 s]
Raw data (loadavg): 1.07 1.02 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 12971 42 0 0 25 0 11 0 491620006 859480064 24898 4294967295 134512640 134569956 3221224400 3221214536 1131559640 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 24898 13073 16 0 209818 0
vsize: 839336
[startup+150.008 s]
Raw data (loadavg): 1.06 1.02 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 13967 42 0 0 25 0 11 0 491620006 859480064 25019 4294967295 134512640 134569956 3221224400 3221214520 1131561515 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25019 13073 16 0 209818 0
vsize: 839336
[startup+160.008 s]
Raw data (loadavg): 1.05 1.02 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 14965 42 0 0 25 0 11 0 491620006 859480064 25020 4294967295 134512640 134569956 3221224400 3221214336 1131280253 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25020 13073 16 0 209818 0
vsize: 839336
[startup+170.009 s]
Raw data (loadavg): 1.04 1.01 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 15963 42 0 0 25 0 11 0 491620006 859480064 25021 4294967295 134512640 134569956 3221224400 3221214336 1131281995 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25021 13073 16 0 209818 0
vsize: 839336
[startup+180.009 s]
Raw data (loadavg): 1.03 1.01 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 16961 42 0 0 25 0 11 0 491620006 859480064 25021 4294967295 134512640 134569956 3221224400 3221214440 1131345889 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 25021 13073 16 0 209818 0
vsize: 839336
[startup+190.009 s]
Raw data (loadavg): 1.03 1.01 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 17960 42 0 0 25 0 11 0 491620006 859480064 25023 4294967295 134512640 134569956 3221224400 3221214440 1131347541 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25023 13073 16 0 209818 0
vsize: 839336
[startup+200.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 18955 43 0 0 25 0 11 0 491620006 859480064 25025 4294967295 134512640 134569956 3221224400 3221214520 1131562236 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 25025 13073 16 0 209818 0
vsize: 839336
[startup+210.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 19948 43 0 0 25 0 11 0 491620006 859480064 25025 4294967295 134512640 134569956 3221224400 3221214520 1131562146 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25025 13073 16 0 209818 0
vsize: 839336
[startup+220.011 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 20941 43 0 0 25 0 11 0 491620006 859480064 25025 4294967295 134512640 134569956 3221224400 3221214520 1131563906 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25025 13073 16 0 209818 0
vsize: 839336
[startup+230.01 s]
Raw data (loadavg): 1.01 1.01 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 21935 43 0 0 25 0 11 0 491620006 859480064 25025 4294967295 134512640 134569956 3221224400 3221214536 1131526076 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25025 13073 16 0 209818 0
vsize: 839336
[startup+240.011 s]
Raw data (loadavg): 1.01 1.01 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 22923 43 0 0 25 0 11 0 491620006 859480064 25027 4294967295 134512640 134569956 3221224400 3221214632 1131638791 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25027 13073 16 0 209818 0
vsize: 839336
[startup+250.011 s]
Raw data (loadavg): 1.01 1.01 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 23915 44 0 0 25 0 11 0 491620006 859480064 25058 4294967295 134512640 134569956 3221224400 3221214520 1131562146 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25058 13073 16 0 209818 0
vsize: 839336
[startup+260.012 s]
Raw data (loadavg): 1.01 1.01 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 24910 44 0 0 25 0 11 0 491620006 859480064 25058 4294967295 134512640 134569956 3221224400 3221214632 1131632848 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25058 13073 16 0 209818 0
vsize: 839336
[startup+270.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 25906 44 0 0 25 0 11 0 491620006 859480064 25058 4294967295 134512640 134569956 3221224400 3221214432 1131281959 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25058 13073 16 0 209818 0
vsize: 839336
[startup+280.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 26902 44 0 0 25 0 11 0 491620006 859480064 25058 4294967295 134512640 134569956 3221224400 3221214432 1131280524 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25058 13073 16 0 209818 0
vsize: 839336
[startup+290.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 27897 45 0 0 25 0 11 0 491620006 859480064 25103 4294967295 134512640 134569956 3221224400 3221214520 1131561857 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25103 13073 16 0 209818 0
vsize: 839336
[startup+300.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 28896 45 0 0 25 0 11 0 491620006 859480064 25103 4294967295 134512640 134569956 3221224400 3221214432 1131280259 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 25103 13073 16 0 209818 0
vsize: 839336
[startup+310.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 29886 45 0 0 25 0 11 0 491620006 859480064 25105 4294967295 134512640 134569956 3221224400 3221214672 1131314431 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25105 13073 16 0 209818 0
vsize: 839336
[startup+320.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7186
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 30882 45 0 0 25 0 11 0 491620006 859480064 25105 4294967295 134512640 134569956 3221224400 3221214768 1131362849 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 25105 13073 16 0 209818 0
vsize: 839336
[startup+330.116 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7187
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18078 4 1 0 31859 45 0 0 25 0 11 0 491620006 859480064 25112 4294967295 134512640 134569956 3221224400 3221214712 1131314893 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25112 13073 16 0 209818 0
vsize: 839336
[startup+340.116 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7189
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 32815 46 0 0 25 0 11 0 491620006 859480064 25114 4294967295 134512640 134569956 3221224400 3221214808 1131362849 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25114 13073 16 0 209818 0
vsize: 839336
[startup+350.117 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7191
Raw data (stat): 7175 (java) S 7174 24215 24214 0 -1 0 18079 4 1 0 33735 46 0 0 25 0 11 0 491620006 859480064 25136 4294967295 134512640 134569956 3221224400 3221213456 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 25136 13073 16 0 209818 0
vsize: 839336
[startup+360.118 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7193
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 34638 46 0 0 25 0 11 0 491620006 859480064 25527 4294967295 134512640 134569956 3221224400 3221214804 1131314188 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 25527 13073 16 0 209818 0
vsize: 839336
[startup+370.118 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7195
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 35551 46 0 0 25 0 11 0 491620006 859480064 25833 4294967295 134512640 134569956 3221224400 3221214712 1131314213 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 25833 13073 16 0 209818 0
vsize: 839336
[startup+380.118 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7197
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 36470 46 0 0 25 0 11 0 491620006 859480064 26269 4294967295 134512640 134569956 3221224400 3221214712 1131314464 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 26269 13073 16 0 209818 0
vsize: 839336
[startup+390.118 s]
Raw data (loadavg): 1.00 1.00 0.93 2/63 7199
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 37380 46 0 0 25 0 10 0 491620006 859480064 26481 4294967295 134512640 134569956 3221224400 3221214512 1131227013 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 26481 13073 16 0 209818 0
vsize: 839336
[startup+400.118 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7202
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 38291 47 0 0 25 0 11 0 491620006 859480064 27060 4294967295 134512640 134569956 3221224400 3221214712 1131314785 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 27060 13073 16 0 209818 0
vsize: 839336
[startup+410.118 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7204
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 39217 47 0 0 25 0 11 0 491620006 859480064 27491 4294967295 134512640 134569956 3221224400 3221214712 1131315159 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 27491 13073 16 0 209818 0
vsize: 839336
[startup+420.119 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7206
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 40140 47 0 0 25 0 11 0 491620006 859480064 28054 4294967295 134512640 134569956 3221224400 3221214808 1131362966 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 28054 13073 16 0 209818 0
vsize: 839336
[startup+430.119 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7208
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 41059 47 0 0 25 0 11 0 491620006 859480064 28278 4294967295 134512640 134569956 3221224400 3221214712 1131315004 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 28278 13073 16 0 209818 0
vsize: 839336
[startup+440.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7210
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 41970 47 0 0 25 0 11 0 491620006 859480064 28653 4294967295 134512640 134569956 3221224400 3221214712 1131314702 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 28653 13073 16 0 209818 0
vsize: 839336
[startup+450.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7212
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 42870 48 0 0 24 0 11 0 491620006 859480064 28869 4294967295 134512640 134569956 3221224400 3221214712 1131315626 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 28869 13073 16 0 209818 0
vsize: 839336
[startup+460.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7214
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 43786 48 1 0 25 0 11 0 491620006 859480064 29796 4294967295 134512640 134569956 3221224400 3221214712 1131314785 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 29796 13073 16 0 209818 0
vsize: 839336
[startup+470.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7217
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 44718 49 1 0 25 0 11 0 491620006 859480064 30063 4294967295 134512640 134569956 3221224400 3221214808 1131364845 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 30063 13073 16 0 209818 0
vsize: 839336
[startup+480.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7219
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 45639 49 1 0 24 0 11 0 491620006 859480064 30524 4294967295 134512640 134569956 3221224400 3221214808 1131366678 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 30524 13073 16 0 209818 0
vsize: 839336
[startup+490.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7221
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 46553 49 1 0 25 0 11 0 491620006 859480064 30916 4294967295 134512640 134569956 3221224400 3221214712 1131314770 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 30916 13073 16 0 209818 0
vsize: 839336
[startup+500.123 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7223
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 47468 50 1 0 25 0 11 0 491620006 859480064 31291 4294967295 134512640 134569956 3221224400 3221214712 1131314962 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 31291 13073 16 0 209818 0
vsize: 839336
[startup+510.124 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7225
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 48384 50 1 0 25 0 11 0 491620006 859480064 31773 4294967295 134512640 134569956 3221224400 3221214712 1131315002 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 31773 13073 16 0 209818 0
vsize: 839336
[startup+520.124 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7227
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 49308 51 1 0 25 0 11 0 491620006 859480064 32169 4294967295 134512640 134569956 3221224400 3221214808 1131363856 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 32169 13073 16 0 209818 0
vsize: 839336
[startup+530.124 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7229
Raw data (stat): 7175 (java) S 7174 24215 24214 0 -1 0 18079 4 1 0 50225 51 2 0 25 0 11 0 491620006 859480064 32451 4294967295 134512640 134569956 3221224400 3221213456 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 32451 13073 16 0 209818 0
vsize: 839336
[startup+540.125 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7231
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 51131 51 2 0 25 0 11 0 491620006 859480064 32817 4294967295 134512640 134569956 3221224400 3221214808 1131363850 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 32817 13073 16 0 209818 0
vsize: 839336
[startup+550.125 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7234
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 52036 52 2 0 25 0 11 0 491620006 859480064 33131 4294967295 134512640 134569956 3221224400 3221214712 1131315284 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 33131 13073 16 0 209818 0
vsize: 839336
[startup+560.126 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7236
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 52943 52 2 0 25 0 11 0 491620006 859480064 33523 4294967295 134512640 134569956 3221224400 3221214712 1131314887 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 33523 13073 16 0 209818 0
vsize: 839336
[startup+570.127 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7238
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 53850 52 2 0 25 0 11 0 491620006 859480064 33700 4294967295 134512640 134569956 3221224400 3221214808 1131364032 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 33700 13073 16 0 209818 0
vsize: 839336
[startup+580.127 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7240
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 54781 53 2 0 24 0 11 0 491620006 859480064 35974 4294967295 134512640 134569956 3221224400 3221214712 1131314691 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 35974 13073 16 0 209818 0
vsize: 839336
[startup+590.127 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7242
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 55731 54 2 0 25 0 11 0 491620006 859480064 35974 4294967295 134512640 134569956 3221224400 3221214992 1131350918 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 35974 13073 16 0 209818 0
vsize: 839336
[startup+600.127 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7244
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 56648 54 2 0 24 0 11 0 491620006 859480064 35974 4294967295 134512640 134569956 3221224400 3221214712 1131314946 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 35974 13073 16 0 209818 0
vsize: 839336
[startup+610.128 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7246
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 57556 55 2 0 25 0 11 0 491620006 859480064 36220 4294967295 134512640 134569956 3221224400 3221214712 1131315014 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 36220 13073 16 0 209818 0
vsize: 839336
[startup+620.129 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7248
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 58464 55 2 0 25 0 11 0 491620006 859480064 36465 4294967295 134512640 134569956 3221224400 3221214808 1131363894 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 36465 13073 16 0 209818 0
vsize: 839336
[startup+630.129 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7250
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 59370 55 3 0 25 0 11 0 491620006 859480064 36740 4294967295 134512640 134569956 3221224400 3221214712 1131314220 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 36740 13073 16 0 209818 0
vsize: 839336
[startup+640.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7252
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 60278 56 3 0 25 0 11 0 491620006 859480064 37001 4294967295 134512640 134569956 3221224400 3221214808 1131363812 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 37001 13073 16 0 209818 0
vsize: 839336
[startup+650.131 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7254
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 61187 56 3 0 25 0 11 0 491620006 859480064 37398 4294967295 134512640 134569956 3221224400 3221214808 1131362922 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 37398 13073 16 0 209818 0
vsize: 839336
[startup+660.131 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7257
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 62102 56 3 0 25 0 11 0 491620006 859480064 37840 4294967295 134512640 134569956 3221224400 3221214752 1131281899 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 37840 13073 16 0 209818 0
vsize: 839336
[startup+670.132 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7259
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 63009 57 3 0 25 0 11 0 491620006 859480064 38221 4294967295 134512640 134569956 3221224400 3221214904 1131227121 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 38221 13073 16 0 209818 0
vsize: 839336
[startup+680.134 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7261
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 63916 57 3 0 25 0 11 0 491620006 859480064 38534 4294967295 134512640 134569956 3221224400 3221214712 1131315215 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 38534 13073 16 0 209818 0
vsize: 839336
[startup+690.134 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7263
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 64838 58 3 1 25 0 11 0 491620006 859480064 38921 4294967295 134512640 134569956 3221224400 3221214712 1131315030 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 38921 13073 16 0 209818 0
vsize: 839336
[startup+700.135 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7265
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 65758 58 3 1 25 0 11 0 491620006 859480064 39396 4294967295 134512640 134569956 3221224400 3221214712 1131314785 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 39396 13073 16 0 209818 0
vsize: 839336
[startup+710.136 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7267
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 66679 59 3 1 25 0 11 0 491620006 859480064 39758 4294967295 134512640 134569956 3221224400 3221214712 1131314220 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 39758 13073 16 0 209818 0
vsize: 839336
[startup+720.136 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7269
Raw data (stat): 7175 (java) S 7174 24215 24214 0 -1 0 18079 4 1 0 67597 59 3 1 25 0 11 0 491620006 859480064 40268 4294967295 134512640 134569956 3221224400 3221213456 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 40268 13073 16 0 209818 0
vsize: 839336
[startup+730.137 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7271
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 68507 59 3 1 24 0 11 0 491620006 859480064 40604 4294967295 134512640 134569956 3221224400 3221214712 1131314488 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 40604 13073 16 0 209818 0
vsize: 839336
[startup+740.137 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7273
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 69421 60 3 1 25 0 11 0 491620006 859480064 40944 4294967295 134512640 134569956 3221224400 3221214744 1131381090 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 40944 13073 16 0 209818 0
vsize: 839336
[startup+750.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7275
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 70333 60 4 1 25 0 11 0 491620006 859480064 41348 4294967295 134512640 134569956 3221224400 3221214808 1131366581 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 41348 13073 16 0 209818 0
vsize: 839336
[startup+760.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7277
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 71245 60 4 1 25 0 11 0 491620006 859480064 41683 4294967295 134512640 134569956 3221224400 3221214712 1131314659 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 41683 13073 16 0 209818 0
vsize: 839336
[startup+770.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7279
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 72154 61 4 1 25 0 11 0 491620006 859480064 42184 4294967295 134512640 134569956 3221224400 3221214712 1131314575 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 42184 13073 16 0 209818 0
vsize: 839336
[startup+780.14 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7281
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 73063 61 4 1 25 0 11 0 491620006 859480064 42489 4294967295 134512640 134569956 3221224400 3221214808 1131364727 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 42489 13073 16 0 209818 0
vsize: 839336
[startup+790.139 s]
Raw data (loadavg): 1.08 1.02 0.93 2/64 7283
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 73981 62 4 1 25 0 11 0 491620006 859480064 42780 4294967295 134512640 134569956 3221224400 3221214752 1131217516 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 42780 13073 16 0 209818 0
vsize: 839336
[startup+800.141 s]
Raw data (loadavg): 1.07 1.02 0.93 2/64 7285
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 74889 62 4 1 25 0 11 0 491620006 859480064 42906 4294967295 134512640 134569956 3221224400 3221214712 1131314457 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 42906 13073 16 0 209818 0
vsize: 839336
[startup+810.141 s]
Raw data (loadavg): 1.06 1.01 0.93 2/64 7287
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 75793 62 4 1 25 0 11 0 491620006 859480064 43250 4294967295 134512640 134569956 3221224400 3221214808 1131362784 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 43250 13073 16 0 209818 0
vsize: 839336
[startup+820.141 s]
Raw data (loadavg): 1.05 1.01 0.93 2/64 7289
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 76693 63 4 1 25 0 11 0 491620006 859480064 45341 4294967295 134512640 134569956 3221224400 3221214712 1131315665 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 45341 13073 16 0 209818 0
vsize: 839336
[startup+830.142 s]
Raw data (loadavg): 1.04 1.01 0.93 2/64 7291
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 77599 63 4 1 25 0 11 0 491620006 859480064 45596 4294967295 134512640 134569956 3221224400 3221214808 1131363850 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 45596 13073 16 0 209818 0
vsize: 839336
[startup+840.142 s]
Raw data (loadavg): 1.03 1.01 0.93 2/64 7293
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 78507 64 4 1 25 0 11 0 491620006 859480064 45899 4294967295 134512640 134569956 3221224400 3221214712 1131314245 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 45899 13073 16 0 209818 0
vsize: 839336
[startup+850.143 s]
Raw data (loadavg): 1.03 1.01 0.93 2/64 7295
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 79413 64 4 1 25 0 11 0 491620006 859480064 46144 4294967295 134512640 134569956 3221224400 3221214712 1131314785 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 46144 13073 16 0 209818 0
vsize: 839336
[startup+860.143 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 7297
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 80318 65 4 1 25 0 11 0 491620006 859480064 46393 4294967295 134512640 134569956 3221224400 3221214808 1131362903 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 46393 13073 16 0 209818 0
vsize: 839336
[startup+870.144 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 7299
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 81224 65 5 1 25 0 11 0 491620006 859480064 46644 4294967295 134512640 134569956 3221224400 3221214808 1131366678 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 46644 13073 16 0 209818 0
vsize: 839336
[startup+880.144 s]
Raw data (loadavg): 1.02 1.01 0.93 2/64 7301
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 82130 66 5 1 25 0 11 0 491620006 859480064 46917 4294967295 134512640 134569956 3221224400 3221214808 1131364877 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 46917 13073 16 0 209818 0
vsize: 839336
[startup+890.145 s]
Raw data (loadavg): 1.01 1.01 0.93 2/64 7303
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 83036 67 5 1 25 0 11 0 491620006 859480064 47165 4294967295 134512640 134569956 3221224400 3221214712 1131314523 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 47165 13073 16 0 209818 0
vsize: 839336
[startup+900.145 s]
Raw data (loadavg): 1.01 1.01 0.93 2/64 7305
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 83941 67 5 1 25 0 11 0 491620006 859480064 47405 4294967295 134512640 134569956 3221224400 3221214712 1131314523 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 47405 13073 16 0 209818 0
vsize: 839336
[startup+910.145 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 7307
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 84847 67 5 1 25 0 11 0 491620006 859480064 47649 4294967295 134512640 134569956 3221224400 3221214808 1131363894 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 47649 13073 16 0 209818 0
vsize: 839336
[startup+920.147 s]
Raw data (loadavg): 1.01 1.00 0.93 2/64 7309
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 85752 67 5 1 25 0 11 0 491620006 859480064 47943 4294967295 134512640 134569956 3221224400 3221214712 1131314938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 47943 13073 16 0 209818 0
vsize: 839336
[startup+930.147 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7311
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 86656 68 5 1 24 0 11 0 491620006 859480064 48188 4294967295 134512640 134569956 3221224400 3221214712 1131314793 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 48188 13073 16 0 209818 0
vsize: 839336
[startup+940.147 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7313
Raw data (stat): 7175 (java) S 7174 24215 24214 0 -1 0 18079 4 1 0 87561 68 5 1 25 0 11 0 491620006 859480064 48417 4294967295 134512640 134569956 3221224400 3221213456 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 48418 13073 16 0 209818 0
vsize: 839336
[startup+950.148 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7315
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 88475 68 5 1 25 0 11 0 491620006 859480064 48584 4294967295 134512640 134569956 3221224400 3221214712 1131314842 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 48584 13073 16 0 209818 0
vsize: 839336
[startup+960.148 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7317
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 89379 68 5 1 25 0 11 0 491620006 859480064 48843 4294967295 134512640 134569956 3221224400 3221214808 1131362882 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 48843 13073 16 0 209818 0
vsize: 839336
[startup+970.149 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7319
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 90283 69 5 2 25 0 11 0 491620006 859480064 49132 4294967295 134512640 134569956 3221224400 3221214712 1131314862 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 49132 13073 16 0 209818 0
vsize: 839336
[startup+980.149 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7321
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 91191 69 5 2 25 0 11 0 491620006 859480064 49511 4294967295 134512640 134569956 3221224400 3221214808 1131362777 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 49511 13073 16 0 209818 0
vsize: 839336
[startup+990.149 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7323
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 92096 70 5 2 25 0 11 0 491620006 859480064 49776 4294967295 134512640 134569956 3221224400 3221214752 1131280427 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 49776 13073 16 0 209818 0
vsize: 839336
[startup+1000.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7325
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 93004 71 5 2 25 0 11 0 491620006 859480064 50118 4294967295 134512640 134569956 3221224400 3221214928 1131344275 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 50118 13073 16 0 209818 0
vsize: 839336
[startup+1010.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7327
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 93914 71 5 2 25 0 11 0 491620006 859480064 50532 4294967295 134512640 134569956 3221224400 3221214952 1131357137 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 50532 13073 16 0 209818 0
vsize: 839336
[startup+1020.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7328
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 94827 72 5 2 25 0 11 0 491620006 859480064 50754 4294967295 134512640 134569956 3221224400 3221214712 1131314785 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 50754 13073 16 0 209818 0
vsize: 839336
[startup+1030.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7330
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 95738 72 5 2 25 0 11 0 491620006 859480064 51117 4294967295 134512640 134569956 3221224400 3221214712 1131314785 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 51117 13073 16 0 209818 0
vsize: 839336
[startup+1040.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7332
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 96653 73 5 2 25 0 11 0 491620006 859480064 51601 4294967295 134512640 134569956 3221224400 3221214712 1131315018 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 51601 13073 16 0 209818 0
vsize: 839336
[startup+1050.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7334
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 97573 73 5 2 25 0 11 0 491620006 859480064 51948 4294967295 134512640 134569956 3221224400 3221214712 1131315651 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 51948 13073 16 0 209818 0
vsize: 839336
[startup+1060.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7336
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 98492 73 6 2 25 0 11 0 491620006 859480064 52256 4294967295 134512640 134569956 3221224400 3221214712 1131314785 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 52256 13073 16 0 209818 0
vsize: 839336
[startup+1070.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7338
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 99407 74 6 2 25 0 11 0 491620006 859480064 52940 4294967295 134512640 134569956 3221224400 3221214804 1131226995 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 52940 13073 16 0 209818 0
vsize: 839336
[startup+1080.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7340
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 100329 74 6 2 25 0 11 0 491620006 859480064 53105 4294967295 134512640 134569956 3221224400 3221214752 1131312436 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 53105 13073 16 0 209818 0
vsize: 839336
[startup+1090.15 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7342
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 101247 75 6 2 25 0 11 0 491620006 859480064 53701 4294967295 134512640 134569956 3221224400 3221214808 1131366678 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 53701 13073 16 0 209818 0
vsize: 839336
[startup+1100.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/64 7344
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 102167 75 6 2 25 0 11 0 491620006 859480064 53976 4294967295 134512640 134569956 3221224400 3221214712 1131315030 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 53976 13073 16 0 209818 0
vsize: 839336
[startup+1110.16 s]
Raw data (loadavg): 1.08 1.02 0.94 2/64 7399
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 103086 78 6 2 25 0 11 0 491620006 859480064 54655 4294967295 134512640 134569956 3221224400 3221213616 1079926801 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209834 54655 13073 16 0 209818 0
vsize: 839336
[startup+1120.16 s]
Raw data (loadavg): 1.07 1.02 0.94 2/64 7401
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 104014 78 7 2 25 0 11 0 491620006 859480064 54997 4294967295 134512640 134569956 3221224400 3221214804 1131314188 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 54997 13073 16 0 209818 0
vsize: 839336
[startup+1130.16 s]
Raw data (loadavg): 1.06 1.01 0.94 2/64 7403
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 104940 78 7 2 25 0 11 0 491620006 859480064 55202 4294967295 134512640 134569956 3221224400 3221214808 1131366648 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 55202 13073 16 0 209818 0
vsize: 839336
[startup+1140.16 s]
Raw data (loadavg): 1.05 1.01 0.94 2/64 7405
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 105859 78 7 2 25 0 11 0 491620006 859480064 55495 4294967295 134512640 134569956 3221224400 3221214712 1131314785 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 55495 13073 16 0 209818 0
vsize: 839336
[startup+1150.16 s]
Raw data (loadavg): 1.04 1.01 0.94 2/64 7407
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 106771 78 7 2 25 0 11 0 491620006 859480064 55783 4294967295 134512640 134569956 3221224400 3221214712 1131314472 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 55783 13073 16 0 209818 0
vsize: 839336
[startup+1160.16 s]
Raw data (loadavg): 1.03 1.01 0.94 2/64 7409
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 107685 79 7 2 25 0 11 0 491620006 859480064 56353 4294967295 134512640 134569956 3221224400 3221214752 1131280310 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 56353 13073 16 0 209818 0
vsize: 839336
[startup+1170.16 s]
Raw data (loadavg): 1.03 1.01 0.94 2/64 7411
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 108610 79 7 2 25 0 11 0 491620006 859480064 56604 4294967295 134512640 134569956 3221224400 3221214752 1131280259 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 56604 13073 16 0 209818 0
vsize: 839336
[startup+1180.16 s]
Raw data (loadavg): 1.02 1.01 0.94 2/64 7412
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 109521 79 7 2 24 0 11 0 491620006 859480064 56935 4294967295 134512640 134569956 3221224400 3221214712 1131314511 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 56935 13073 16 0 209818 0
vsize: 839336
[startup+1190.16 s]
Raw data (loadavg): 1.02 1.01 0.94 2/64 7416
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 110441 80 7 2 25 0 11 0 491620006 859480064 57259 4294967295 134512640 134569956 3221224400 3221214808 1131366724 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 57259 13073 16 0 209818 0
vsize: 839336
[startup+1200.16 s]
Raw data (loadavg): 1.02 1.01 0.94 2/64 7418
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 111351 80 7 2 25 0 11 0 491620006 859480064 57498 4294967295 134512640 134569956 3221224400 3221214712 1131314785 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 57498 13073 16 0 209818 0
vsize: 839336
[startup+1210.16 s]
Raw data (loadavg): 1.01 1.01 0.94 2/64 7420
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 112263 80 7 2 24 0 11 0 491620006 859480064 57931 4294967295 134512640 134569956 3221224400 3221214808 1131363917 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 57931 13073 16 0 209818 0
vsize: 839336
[startup+1220.16 s]
Raw data (loadavg): 1.01 1.01 0.94 2/64 7422
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 113183 80 7 2 25 0 11 0 491620006 859480064 58201 4294967295 134512640 134569956 3221224400 3221214808 1131363993 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 58201 13073 16 0 209818 0
vsize: 839336
[startup+1230.16 s]
Raw data (loadavg): 1.01 1.00 0.94 2/64 7424
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 114098 81 7 3 25 0 11 0 491620006 859480064 58357 4294967295 134512640 134569956 3221224400 3221214712 1131314857 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 58357 13073 16 0 209818 0
vsize: 839336
[startup+1240.16 s]
Raw data (loadavg): 1.01 1.00 0.94 2/64 7426
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 115006 81 7 3 24 0 11 0 491620006 859480064 58766 4294967295 134512640 134569956 3221224400 3221214712 1131314838 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 58766 13073 16 0 209818 0
vsize: 839336
[startup+1250.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 7428
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 115922 81 7 3 25 0 11 0 491620006 859480064 58920 4294967295 134512640 134569956 3221224400 3221214856 1131345896 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 58920 13073 16 0 209818 0
vsize: 839336
[startup+1260.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 7429
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 116820 81 7 3 25 0 11 0 491620006 859480064 59524 4294967295 134512640 134569956 3221224400 3221214808 1131363894 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 59524 13073 16 0 209818 0
vsize: 839336
[startup+1270.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 7431
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 117719 81 7 3 24 0 11 0 491620006 859480064 59940 4294967295 134512640 134569956 3221224400 3221214712 1131314575 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 59940 13073 16 0 209818 0
vsize: 839336
[startup+1280.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 7433
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 118649 81 8 3 25 0 11 0 491620006 859480064 60400 4294967295 134512640 134569956 3221224400 3221214808 1131362784 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 60400 13073 16 0 209818 0
vsize: 839336
[startup+1290.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 7435
Raw data (stat): 7175 (java) R 7174 24215 24214 0 -1 0 18079 4 1 0 119563 81 8 3 25 0 11 0 491620006 859480064 60529 4294967295 134512640 134569956 3221224400 3221214712 1131315604 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 60529 13073 16 0 209818 0
vsize: 839336
[startup+1300.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/64 7437
Raw data (stat): 7175 (java) S 7174 24215 24214 0 -1 0 18079 4 1 0 120468 81 8 3 25 0 11 0 491620006 859480064 60801 4294967295 134512640 134569956 3221224400 3221213416 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209834 60801 13073 16 0 209818 0
vsize: 839336
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1300.34 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 7439
Raw data (stat): 7175 (java) Z 7174 24215 24214 0 -1 1036 18079 47716 1 0 120473 93 10612 116 25 0 1 0 491620006 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.34
CPU time (s): 1312.96
CPU user time (s): 1310.86
CPU system time (s): 2.10068
CPU usage (%): 100.97
Max. virtual memory (Kb): 839944
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####