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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.5:100.opb
MD5SUM	bc393d4b1cc38ed414c3e21eb8bc6b60
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	56
Optimality of the best value was proved	NO
Number of terms in the objective function	4447
Biggest coefficient in the objective function	2128
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	12580
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	2128
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	12580
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06284
Number of variables	4447
Total number of constraints	9372
Number of constraints which are clauses	4205
Number of constraints which are cardinality constraints (but not clauses)	5167
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	27
Trace number 6469

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-14 05:10:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4884 boxname=wulflinc20 idbench=372 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bc393d4b1cc38ed414c3e21eb8bc6b60  /oldhome/oroussel/tmp/wulflinc20/normalized-30:30:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc20/normalized-30:30:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc20/normalized-30:30:4.5:0.5:100.opb
IDLAUNCH: 4884
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        851056 kB
Buffers:         35696 kB
Cached:         112160 kB
SwapCached:       2628 kB
Active:          51384 kB
Inactive:       101996 kB
HighTotal:      131008 kB
HighFree:        15596 kB
LowTotal:       903652 kB
LowFree:        835460 kB
SwapTotal:     2097892 kB
SwapFree:      2095264 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24596 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:30:32 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 4884 7 1200.29 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4925 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 740]---> BDD-cost:   17
c ---[ 739]---> BDD-cost:   20
c ---[ 738]---> BDD-cost:   20
c ---[ 737]---> BDD-cost:   23
c ---[ 736]---> BDD-cost:   35
c ---[ 735]---> BDD-cost:   35
c ---[ 734]---> BDD-cost:   35
c ---[ 733]---> BDD-cost:   23
c ---[ 732]---> BDD-cost:   26
c ---[ 731]---> BDD-cost:   23
c ---[ 730]---> BDD-cost:   23
c ---[ 729]---> BDD-cost:   29
c ---[ 728]---> BDD-cost:   29
c ---[ 727]---> BDD-cost:   20
c ---[ 726]---> BDD-cost:   26
c ---[ 725]---> BDD-cost:   26
c ---[ 724]---> BDD-cost:   29
c ---[ 723]---> BDD-cost:   17
c ---[ 722]---> BDD-cost:   17
c ---[ 721]---> BDD-cost:   17
c ---[ 720]---> BDD-cost:    7
c ---[ 719]---> BDD-cost:    3
c ---[ 718]---> BDD-cost:    5
c ---[ 717]---> BDD-cost:    5
c ---[ 716]---> BDD-cost:    8
c ---[ 715]---> BDD-cost:    3
c ---[ 714]---> BDD-cost:   20
c ---[ 713]---> BDD-cost:   23
c ---[ 712]---> BDD-cost:   26
c ---[ 711]---> BDD-cost:   32
c ---[ 710]---> BDD-cost:   41
c ---[ 709]---> BDD-cost:   38
c ---[ 708]---> BDD-cost:   44
c ---[ 707]---> BDD-cost:   38
c ---[ 706]---> BDD-cost:   33
c ---[ 705]---> BDD-cost:   29
c ---[ 704]---> BDD-cost:   29
c ---[ 703]---> BDD-cost:   35
c ---[ 702]---> BDD-cost:   38
c ---[ 701]---> BDD-cost:   33
c ---[ 700]---> BDD-cost:   44
c ---[ 699]---> BDD-cost:   32
c ---[ 698]---> BDD-cost:   38
c ---[ 697]---> BDD-cost:   29
c ---[ 696]---> BDD-cost:   29
c ---[ 695]---> BDD-cost:   23
c ---[ 694]---> BDD-cost:   17
c ---[ 693]---> BDD-cost:   14
c ---[ 692]---> BDD-cost:    7
c ---[ 691]---> BDD-cost:   11
c ---[ 690]---> BDD-cost:   11
c ---[ 689]---> BDD-cost:   11
c ---[ 688]---> BDD-cost:    5
c ---[ 686]---> BDD-cost:   20
c ---[ 685]---> BDD-cost:   26
c ---[ 684]---> BDD-cost:   35
c ---[ 683]---> BDD-cost:   41
c ---[ 682]---> BDD-cost:   56
c ---[ 681]---> BDD-cost:   44
c ---[ 680]---> BDD-cost:   44
c ---[ 679]---> BDD-cost:   44
c ---[ 678]---> BDD-cost:   44
c ---[ 677]---> BDD-cost:   38
c ---[ 676]---> BDD-cost:   47
c ---[ 675]---> BDD-cost:   50
c ---[ 674]---> BDD-cost:   53
c ---[ 673]---> BDD-cost:   47
c ---[ 672]---> BDD-cost:   56
c ---[ 671]---> BDD-cost:   47
c ---[ 670]---> BDD-cost:   47
c ---[ 669]---> BDD-cost:   38
c ---[ 668]---> BDD-cost:   41
c ---[ 667]---> BDD-cost:   35
c ---[ 666]---> BDD-cost:   23
c ---[ 665]---> BDD-cost:   20
c ---[ 664]---> BDD-cost:   17
c ---[ 663]---> BDD-cost:   14
c ---[ 662]---> BDD-cost:   20
c ---[ 661]---> BDD-cost:   11
c ---[ 660]---> BDD-cost:   14
c ---[ 659]---> BDD-cost:   14
c ---[ 658]---> BDD-cost:    9
c ---[ 657]---> BDD-cost:    7
c ---[ 656]---> BDD-cost:   29
c ---[ 655]---> BDD-cost:   32
c ---[ 654]---> BDD-cost:   41
c ---[ 653]---> BDD-cost:   47
c ---[ 652]---> BDD-cost:   56
c ---[ 651]---> BDD-cost:   56
c ---[ 650]---> BDD-cost:   59
c ---[ 649]---> BDD-cost:   50
c ---[ 648]---> BDD-cost:   53
c ---[ 647]---> BDD-cost:   53
c ---[ 646]---> BDD-cost:   53
c ---[ 645]---> BDD-cost:   56
c ---[ 644]---> BDD-cost:   56
c ---[ 643]---> BDD-cost:   56
c ---[ 642]---> BDD-cost:   59
c ---[ 641]---> BDD-cost:   53
c ---[ 640]---> BDD-cost:   47
c ---[ 639]---> BDD-cost:   47
c ---[ 638]---> BDD-cost:   44
c ---[ 637]---> BDD-cost:   38
c ---[ 636]---> BDD-cost:   26
c ---[ 635]---> BDD-cost:   26
c ---[ 634]---> BDD-cost:   26
c ---[ 633]---> BDD-cost:   20
c ---[ 632]---> BDD-cost:   23
c ---[ 631]---> BDD-cost:   23
c ---[ 630]---> BDD-cost:   23
c ---[ 629]---> BDD-cost:   17
c ---[ 628]---> BDD-cost:   11
c ---[ 627]---> BDD-cost:   11
c ---[ 626]---> BDD-cost:   29
c ---[ 625]---> BDD-cost:   35
c ---[ 624]---> BDD-cost:   44
c ---[ 623]---> BDD-cost:   47
c ---[ 622]---> BDD-cost:   54
c ---[ 621]---> BDD-cost:   59
c ---[ 620]---> BDD-cost:   65
c ---[ 619]---> BDD-cost:   65
c ---[ 618]---> BDD-cost:   56
c ---[ 617]---> BDD-cost:   50
c ---[ 616]---> BDD-cost:   50
c ---[ 615]---> BDD-cost:   53
c ---[ 614]---> BDD-cost:   62
c ---[ 613]---> BDD-cost:   59
c ---[ 612]---> BDD-cost:   50
c ---[ 611]---> BDD-cost:   50
c ---[ 610]---> BDD-cost:   50
c ---[ 609]---> BDD-cost:   50
c ---[ 608]---> BDD-cost:   47
c ---[ 607]---> BDD-cost:   38
c ---[ 606]---> BDD-cost:   35
c ---[ 605]---> BDD-cost:   32
c ---[ 604]---> BDD-cost:   26
c ---[ 603]---> BDD-cost:   23
c ---[ 602]---> BDD-cost:   26
c ---[ 601]---> BDD-cost:   32
c ---[ 600]---> BDD-cost:   26
c ---[ 599]---> BDD-cost:   20
c ---[ 598]---> BDD-cost:   20
c ---[ 597]---> BDD-cost:   11
c ---[ 596]---> BDD-cost:   20
c ---[ 595]---> BDD-cost:   35
c ---[ 594]---> BDD-cost:   47
c ---[ 593]---> BDD-cost:   50
c ---[ 592]---> BDD-cost:   62
c ---[ 591]---> BDD-cost:   62
c ---[ 590]---> BDD-cost:   59
c ---[ 589]---> BDD-cost:   65
c ---[ 588]---> BDD-cost:   56
c ---[ 587]---> BDD-cost:   47
c ---[ 586]---> BDD-cost:   57
c ---[ 585]---> BDD-cost:   59
c ---[ 584]---> BDD-cost:   59
c ---[ 583]---> BDD-cost:   53
c ---[ 582]---> BDD-cost:   59
c ---[ 581]---> BDD-cost:   56
c ---[ 580]---> BDD-cost:   53
c ---[ 579]---> BDD-cost:   50
c ---[ 578]---> BDD-cost:   44
c ---[ 577]---> BDD-cost:   38
c ---[ 576]---> BDD-cost:   32
c ---[ 575]---> BDD-cost:   32
c ---[ 574]---> BDD-cost:   32
c ---[ 573]---> BDD-cost:   26
c ---[ 572]---> BDD-cost:   26
c ---[ 571]---> BDD-cost:   29
c ---[ 570]---> BDD-cost:   23
c ---[ 569]---> BDD-cost:   26
c ---[ 568]---> BDD-cost:   26
c ---[ 567]---> BDD-cost:   17
c ---[ 566]---> BDD-cost:   23
c ---[ 565]---> BDD-cost:   35
c ---[ 564]---> BDD-cost:   47
c ---[ 563]---> BDD-cost:   53
c ---[ 562]---> BDD-cost:   59
c ---[ 561]---> BDD-cost:   62
c ---[ 560]---> BDD-cost:   56
c ---[ 559]---> BDD-cost:   59
c ---[ 558]---> BDD-cost:   68
c ---[ 557]---> BDD-cost:   65
c ---[ 556]---> BDD-cost:   59
c ---[ 555]---> BDD-cost:   56
c ---[ 554]---> BDD-cost:   62
c ---[ 553]---> BDD-cost:   56
c ---[ 552]---> BDD-cost:   53
c ---[ 551]---> BDD-cost:   59
c ---[ 550]---> BDD-cost:   53
c ---[ 549]---> BDD-cost:   53
c ---[ 548]---> BDD-cost:   44
c ---[ 547]---> BDD-cost:   38
c ---[ 546]---> BDD-cost:   35
c ---[ 545]---> BDD-cost:   35
c ---[ 544]---> BDD-cost:   35
c ---[ 543]---> BDD-cost:   32
c ---[ 542]---> BDD-cost:   29
c ---[ 541]---> BDD-cost:   32
c ---[ 540]---> BDD-cost:   32
c ---[ 539]---> BDD-cost:   26
c ---[ 538]---> BDD-cost:   26
c ---[ 537]---> BDD-cost:   23
c ---[ 536]---> BDD-cost:   30
c ---[ 535]---> BDD-cost:   35
c ---[ 534]---> BDD-cost:   41
c ---[ 533]---> BDD-cost:   50
c ---[ 532]---> BDD-cost:   56
c ---[ 531]---> BDD-cost:   62
c ---[ 530]---> BDD-cost:   62
c ---[ 529]---> BDD-cost:   62
c ---[ 528]---> BDD-cost:   54
c ---[ 527]---> BDD-cost:   65
c ---[ 526]---> BDD-cost:   62
c ---[ 525]---> BDD-cost:   56
c ---[ 524]---> BDD-cost:   47
c ---[ 523]---> BDD-cost:   53
c ---[ 522]---> BDD-cost:   50
c ---[ 521]---> BDD-cost:   53
c ---[ 520]---> BDD-cost:   53
c ---[ 519]---> BDD-cost:   56
c ---[ 518]---> BDD-cost:   47
c ---[ 517]---> BDD-cost:   41
c ---[ 516]---> BDD-cost:   38
c ---[ 515]---> BDD-cost:   41
c ---[ 514]---> BDD-cost:   38
c ---[ 513]---> BDD-cost:   35
c ---[ 512]---> BDD-cost:   32
c ---[ 511]---> BDD-cost:   38
c ---[ 510]---> BDD-cost:   38
c ---[ 509]---> BDD-cost:   35
c ---[ 508]---> BDD-cost:   29
c ---[ 507]---> BDD-cost:   17
c ---[ 506]---> BDD-cost:   35
c ---[ 505]---> BDD-cost:   41
c ---[ 504]---> BDD-cost:   50
c ---[ 503]---> BDD-cost:   53
c ---[ 502]---> BDD-cost:   59
c ---[ 501]---> BDD-cost:   59
c ---[ 500]---> BDD-cost:   62
c ---[ 499]---> BDD-cost:   62
c ---[ 498]---> BDD-cost:   59
c ---[ 497]---> BDD-cost:   56
c ---[ 496]---> BDD-cost:   47
c ---[ 495]---> BDD-cost:   53
c ---[ 494]---> BDD-cost:   47
c ---[ 493]---> BDD-cost:   44
c ---[ 492]---> BDD-cost:   50
c ---[ 491]---> BDD-cost:   59
c ---[ 490]---> BDD-cost:   50
c ---[ 489]---> BDD-cost:   50
c ---[ 488]---> BDD-cost:   35
c ---[ 487]---> BDD-cost:   38
c ---[ 486]---> BDD-cost:   35
c ---[ 485]---> BDD-cost:   41
c ---[ 484]---> BDD-cost:   41
c ---[ 483]---> BDD-cost:   41
c ---[ 482]---> BDD-cost:   38
c ---[ 481]---> BDD-cost:   38
c ---[ 480]---> BDD-cost:   35
c ---[ 479]---> BDD-cost:   35
c ---[ 478]---> BDD-cost:   29
c ---[ 477]---> BDD-cost:   20
c ---[ 476]---> BDD-cost:   32
c ---[ 475]---> BDD-cost:   47
c ---[ 474]---> BDD-cost:   53
c ---[ 473]---> BDD-cost:   59
c ---[ 472]---> BDD-cost:   71
c ---[ 471]---> BDD-cost:   62
c ---[ 470]---> BDD-cost:   59
c ---[ 469]---> BDD-cost:   59
c ---[ 468]---> BDD-cost:   53
c ---[ 467]---> BDD-cost:   50
c ---[ 466]---> BDD-cost:   53
c ---[ 465]---> BDD-cost:   56
c ---[ 464]---> BDD-cost:   53
c ---[ 463]---> BDD-cost:   50
c ---[ 462]---> BDD-cost:   38
c ---[ 461]---> BDD-cost:   47
c ---[ 460]---> BDD-cost:   44
c ---[ 459]---> BDD-cost:   39
c ---[ 458]---> BDD-cost:   32
c ---[ 457]---> BDD-cost:   32
c ---[ 456]---> BDD-cost:   35
c ---[ 455]---> BDD-cost:   44
c ---[ 454]---> BDD-cost:   38
c ---[ 453]---> BDD-cost:   38
c ---[ 452]---> BDD-cost:   41
c ---[ 451]---> BDD-cost:   38
c ---[ 450]---> BDD-cost:   35
c ---[ 449]---> BDD-cost:   35
c ---[ 448]---> BDD-cost:   29
c ---[ 447]---> BDD-cost:   23
c ---[ 446]---> BDD-cost:   33
c ---[ 445]---> BDD-cost:   41
c ---[ 444]---> BDD-cost:   50
c ---[ 443]---> BDD-cost:   68
c ---[ 442]---> BDD-cost:   68
c ---[ 441]---> BDD-cost:   62
c ---[ 440]---> BDD-cost:   53
c ---[ 439]---> BDD-cost:   53
c ---[ 438]---> BDD-cost:   51
c ---[ 437]---> BDD-cost:   56
c ---[ 436]---> BDD-cost:   59
c ---[ 435]---> BDD-cost:   56
c ---[ 434]---> BDD-cost:   38
c ---[ 433]---> BDD-cost:   41
c ---[ 432]---> BDD-cost:   44
c ---[ 431]---> BDD-cost:   50
c ---[ 430]---> BDD-cost:   56
c ---[ 429]---> BDD-cost:   41
c ---[ 428]---> BDD-cost:   35
c ---[ 427]---> BDD-cost:   32
c ---[ 426]---> BDD-cost:   32
c ---[ 425]---> BDD-cost:   38
c ---[ 424]---> BDD-cost:   44
c ---[ 423]---> BDD-cost:   44
c ---[ 422]---> BDD-cost:   44
c ---[ 421]---> BDD-cost:   41
c ---[ 420]---> BDD-cost:   41
c ---[ 419]---> BDD-cost:   32
c ---[ 418]---> BDD-cost:   26
c ---[ 417]---> BDD-cost:   23
c ---[ 416]---> BDD-cost:   35
c ---[ 415]---> BDD-cost:   38
c ---[ 414]---> BDD-cost:   44
c ---[ 413]---> BDD-cost:   59
c ---[ 412]---> BDD-cost:   65
c ---[ 411]---> BDD-cost:   59
c ---[ 410]---> BDD-cost:   50
c ---[ 409]---> BDD-cost:   50
c ---[ 408]---> BDD-cost:   50
c ---[ 407]---> BDD-cost:   53
c ---[ 406]---> BDD-cost:   50
c ---[ 405]---> BDD-cost:   47
c ---[ 404]---> BDD-cost:   44
c ---[ 403]---> BDD-cost:   44
c ---[ 402]---> BDD-cost:   50
c ---[ 401]---> BDD-cost:   59
c ---[ 400]---> BDD-cost:   53
c ---[ 399]---> BDD-cost:   47
c ---[ 398]---> BDD-cost:   44
c ---[ 397]---> BDD-cost:   35
c ---[ 396]---> BDD-cost:   38
c ---[ 395]---> BDD-cost:   32
c ---[ 394]---> BDD-cost:   38
c ---[ 393]---> BDD-cost:   44
c ---[ 392]---> BDD-cost:   45
c ---[ 391]---> BDD-cost:   44
c ---[ 390]---> BDD-cost:   41
c ---[ 389]---> BDD-cost:   38
c ---[ 388]---> BDD-cost:   35
c ---[ 387]---> BDD-cost:   23
c ---[ 386]---> BDD-cost:   35
c ---[ 385]---> BDD-cost:   38
c ---[ 384]---> BDD-cost:   47
c ---[ 383]---> BDD-cost:   56
c ---[ 382]---> BDD-cost:   59
c ---[ 381]---> BDD-cost:   59
c ---[ 380]---> BDD-cost:   50
c ---[ 379]---> BDD-cost:   44
c ---[ 378]---> BDD-cost:   41
c ---[ 377]---> BDD-cost:   44
c ---[ 376]---> BDD-cost:   45
c ---[ 375]---> BDD-cost:   44
c ---[ 374]---> BDD-cost:   53
c ---[ 373]---> BDD-cost:   56
c ---[ 372]---> BDD-cost:   47
c ---[ 371]---> BDD-cost:   53
c ---[ 370]---> BDD-cost:   50
c ---[ 369]---> BDD-cost:   47
c ---[ 368]---> BDD-cost:   44
c ---[ 367]---> BDD-cost:   38
c ---[ 366]---> BDD-cost:   44
c ---[ 365]---> BDD-cost:   41
c ---[ 364]---> BDD-cost:   50
c ---[ 363]---> BDD-cost:   50
c ---[ 362]---> BDD-cost:   47
c ---[ 361]---> BDD-cost:   44
c ---[ 360]---> BDD-cost:   41
c ---[ 359]---> BDD-cost:   41
c ---[ 358]---> BDD-cost:   35
c ---[ 357]---> BDD-cost:   26
c ---[ 356]---> BDD-cost:   35
c ---[ 355]---> BDD-cost:   38
c ---[ 354]---> BDD-cost:   44
c ---[ 353]---> BDD-cost:   53
c ---[ 352]---> BDD-cost:   50
c ---[ 351]---> BDD-cost:   56
c ---[ 350]---> BDD-cost:   53
c ---[ 349]---> BDD-cost:   44
c ---[ 348]---> BDD-cost:   47
c ---[ 347]---> BDD-cost:   44
c ---[ 346]---> BDD-cost:   56
c ---[ 345]---> BDD-cost:   53
c ---[ 344]---> BDD-cost:   56
c ---[ 343]---> BDD-cost:   56
c ---[ 342]---> BDD-cost:   53
c ---[ 341]---> BDD-cost:   53
c ---[ 340]---> BDD-cost:   53
c ---[ 339]---> BDD-cost:   44
c ---[ 338]---> BDD-cost:   56
c ---[ 337]---> BDD-cost:   50
c ---[ 336]---> BDD-cost:   47
c ---[ 335]---> BDD-cost:   41
c ---[ 334]---> BDD-cost:   47
c ---[ 333]---> BDD-cost:   59
c ---[ 332]---> BDD-cost:   50
c ---[ 331]---> BDD-cost:   47
c ---[ 330]---> BDD-cost:   44
c ---[ 329]---> BDD-cost:   38
c ---[ 328]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   29
c ---[ 326]---> BDD-cost:   35
c ---[ 325]---> BDD-cost:   35
c ---[ 324]---> BDD-cost:   44
c ---[ 323]---> BDD-cost:   50
c ---[ 322]---> BDD-cost:   50
c ---[ 321]---> BDD-cost:   53
c ---[ 320]---> BDD-cost:   53
c ---[ 319]---> BDD-cost:   47
c ---[ 318]---> BDD-cost:   56
c ---[ 317]---> BDD-cost:   56
c ---[ 316]---> BDD-cost:   59
c ---[ 315]---> BDD-cost:   56
c ---[ 314]---> BDD-cost:   68
c ---[ 313]---> BDD-cost:   62
c ---[ 312]---> BDD-cost:   56
c ---[ 311]---> BDD-cost:   59
c ---[ 310]---> BDD-cost:   65
c ---[ 309]---> BDD-cost:   56
c ---[ 308]---> BDD-cost:   56
c ---[ 307]---> BDD-cost:   56
c ---[ 306]---> BDD-cost:   53
c ---[ 305]---> BDD-cost:   41
c ---[ 304]---> BDD-cost:   41
c ---[ 303]---> BDD-cost:   47
c ---[ 302]---> BDD-cost:   47
c ---[ 301]---> BDD-cost:   50
c ---[ 300]---> BDD-cost:   44
c ---[ 299]---> BDD-cost:   38
c ---[ 298]---> BDD-cost:   38
c ---[ 297]---> BDD-cost:   29
c ---[ 296]---> BDD-cost:   32
c ---[ 295]---> BDD-cost:   38
c ---[ 294]---> BDD-cost:   35
c ---[ 293]---> BDD-cost:   44
c ---[ 292]---> BDD-cost:   47
c ---[ 291]---> BDD-cost:   53
c ---[ 290]---> BDD-cost:   56
c ---[ 289]---> BDD-cost:   47
c ---[ 288]---> BDD-cost:   56
c ---[ 287]---> BDD-cost:   56
c ---[ 286]---> BDD-cost:   59
c ---[ 285]---> BDD-cost:   68
c ---[ 284]---> BDD-cost:   74
c ---[ 283]---> BDD-cost:   71
c ---[ 282]---> BDD-cost:   65
c ---[ 281]---> BDD-cost:   59
c ---[ 280]---> BDD-cost:   59
c ---[ 279]---> BDD-cost:   59
c ---[ 278]---> BDD-cost:   50
c ---[ 277]---> BDD-cost:   53
c ---[ 276]---> BDD-cost:   53
c ---[ 275]---> BDD-cost:   50
c ---[ 274]---> BDD-cost:   50
c ---[ 273]---> BDD-cost:   47
c ---[ 272]---> BDD-cost:   50
c ---[ 271]---> BDD-cost:   47
c ---[ 270]---> BDD-cost:   44
c ---[ 269]---> BDD-cost:   38
c ---[ 268]---> BDD-cost:   32
c ---[ 267]---> BDD-cost:   26
c ---[ 266]---> BDD-cost:   20
c ---[ 265]---> BDD-cost:   29
c ---[ 264]---> BDD-cost:   29
c ---[ 263]---> BDD-cost:   38
c ---[ 262]---> BDD-cost:   38
c ---[ 261]---> BDD-cost:   47
c ---[ 260]---> BDD-cost:   50
c ---[ 259]---> BDD-cost:   47
c ---[ 258]---> BDD-cost:   53
c ---[ 257]---> BDD-cost:   53
c ---[ 256]---> BDD-cost:   50
c ---[ 255]---> BDD-cost:   62
c ---[ 254]---> BDD-cost:   68
c ---[ 253]---> BDD-cost:   74
c ---[ 252]---> BDD-cost:   59
c ---[ 251]---> BDD-cost:   53
c ---[ 250]---> BDD-cost:   53
c ---[ 249]---> BDD-cost:   50
c ---[ 248]---> BDD-cost:   56
c ---[ 247]---> BDD-cost:   56
c ---[ 246]---> BDD-cost:   50
c ---[ 245]---> BDD-cost:   47
c ---[ 244]---> BDD-cost:   44
c ---[ 243]---> BDD-cost:   47
c ---[ 242]---> BDD-cost:   50
c ---[ 241]---> BDD-cost:   50
c ---[ 240]---> BDD-cost:   44
c ---[ 239]---> BDD-cost:   35
c ---[ 238]---> BDD-cost:   26
c ---[ 237]---> BDD-cost:   23
c ---[ 236]---> BDD-cost:   20
c ---[ 235]---> BDD-cost:   26
c ---[ 234]---> BDD-cost:   29
c ---[ 233]---> BDD-cost:   32
c ---[ 232]---> BDD-cost:   27
c ---[ 231]---> BDD-cost:   41
c ---[ 230]---> BDD-cost:   47
c ---[ 229]---> BDD-cost:   47
c ---[ 228]---> BDD-cost:   44
c ---[ 227]---> BDD-cost:   47
c ---[ 226]---> BDD-cost:   47
c ---[ 225]---> BDD-cost:   56
c ---[ 224]---> BDD-cost:   59
c ---[ 223]---> BDD-cost:   59
c ---[ 222]---> BDD-cost:   44
c ---[ 221]---> BDD-cost:   47
c ---[ 220]---> BDD-cost:   50
c ---[ 219]---> BDD-cost:   50
c ---[ 218]---> BDD-cost:   44
c ---[ 217]---> BDD-cost:   53
c ---[ 216]---> BDD-cost:   41
c ---[ 215]---> BDD-cost:   38
c ---[ 214]---> BDD-cost:   38
c ---[ 213]---> BDD-cost:   41
c ---[ 212]---> BDD-cost:   44
c ---[ 211]---> BDD-cost:   44
c ---[ 210]---> BDD-cost:   35
c ---[ 209]---> BDD-cost:   32
c ---[ 208]---> BDD-cost:   23
c ---[ 207]---> BDD-cost:   17
c ---[ 206]---> BDD-cost:   17
c ---[ 205]---> BDD-cost:   26
c ---[ 204]---> BDD-cost:   26
c ---[ 203]---> BDD-cost:   29
c ---[ 202]---> BDD-cost:   32
c ---[ 201]---> BDD-cost:   35
c ---[ 200]---> BDD-cost:   38
c ---[ 199]---> BDD-cost:   44
c ---[ 198]---> BDD-cost:   44
c ---[ 197]---> BDD-cost:   44
c ---[ 196]---> BDD-cost:   47
c ---[ 195]---> BDD-cost:   53
c ---[ 194]---> BDD-cost:   50
c ---[ 193]---> BDD-cost:   47
c ---[ 192]---> BDD-cost:   38
c ---[ 191]---> BDD-cost:   38
c ---[ 190]---> BDD-cost:   41
c ---[ 189]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:   35
c ---[ 187]---> BDD-cost:   35
c ---[ 186]---> BDD-cost:   30
c ---[ 185]---> BDD-cost:   35
c ---[ 184]---> BDD-cost:   32
c ---[ 183]---> BDD-cost:   32
c ---[ 182]---> BDD-cost:   35
c ---[ 181]---> BDD-cost:   35
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   26
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   14
c ---[ 176]---> BDD-cost:    7
c ---[ 175]---> BDD-cost:   20
c ---[ 174]---> BDD-cost:   20
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   26
c ---[ 171]---> BDD-cost:   29
c ---[ 170]---> BDD-cost:   26
c ---[ 169]---> BDD-cost:   38
c ---[ 168]---> BDD-cost:   38
c ---[ 167]---> BDD-cost:   44
c ---[ 166]---> BDD-cost:   41
c ---[ 165]---> BDD-cost:   47
c ---[ 164]---> BDD-cost:   44
c ---[ 163]---> BDD-cost:   38
c ---[ 162]---> BDD-cost:   32
c ---[ 161]---> BDD-cost:   35
c ---[ 160]---> BDD-cost:   32
c ---[ 159]---> BDD-cost:   32
c ---[ 158]---> BDD-cost:   26
c ---[ 157]---> BDD-cost:   32
c ---[ 156]---> BDD-cost:   29
c ---[ 155]---> BDD-cost:   29
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   26
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   23
c ---[ 150]---> BDD-cost:   20
c ---[ 149]---> BDD-cost:   17
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   12
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:    9
c ---[ 143]---> BDD-cost:   14
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   23
c ---[ 140]---> BDD-cost:   17
c ---[ 139]---> BDD-cost:   26
c ---[ 138]---> BDD-cost:   21
c ---[ 137]---> BDD-cost:   35
c ---[ 136]---> BDD-cost:   26
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   29
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   23
c ---[ 131]---> BDD-cost:   29
c ---[ 130]---> BDD-cost:   29
c ---[ 129]---> BDD-cost:   15
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:   20
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   23
c ---[ 124]---> BDD-cost:   20
c ---[ 123]---> BDD-cost:   20
c ---[ 122]---> BDD-cost:   20
c ---[ 121]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   11
c ---[ 116]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:    7
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:    5
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   29
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   20
c ---[ 104]---> BDD-cost:   17
c ---[ 103]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:   17
c ---[ 101]---> BDD-cost:   20
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:    5
c ---[  89]---> BDD-cost:    7
c ---[  87]---> BDD-cost:    8
c ---[  81]---> BDD-cost:   14
c ---[  80]---> BDD-cost:   14
c ---[  79]---> BDD-cost:   20
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:    8
c ---[  75]---> BDD-cost:    8
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:   11
c ---[  71]---> BDD-cost:   11
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   11
c ---[  67]---> BDD-cost:    5
c ---[  66]---> BDD-cost:    5
c ---[  64]---> BDD-cost:    5
c ---[  63]---> BDD-cost:   11
c ---[  62]---> BDD-cost:    8
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:    5
c ---[  59]---> BDD-cost:    3
c ---[  58]---> BDD-cost:    5
c ---[  57]---> BDD-cost:    8
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:    8
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:    5
c ---[  52]---> BDD-cost:    6
c ---[  51]---> BDD-cost:    8
c ---[  50]---> BDD-cost:    8
c ---[  49]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    5
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    5
c ---[  44]---> BDD-cost:    8
c ---[  43]---> BDD-cost:    3
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:    7
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    8
c ---[  38]---> BDD-cost:    8
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    5
c ---[  19]---> BDD-cost:    5
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    8
c ---[  16]---> BDD-cost:    5
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:    8
c ---[  13]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    5
c ---[   8]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:    5
c ---[   4]---> BDD-cost:    3
c ---[   1]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  129089   363866 |   43029       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 4694[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10943   maxlim: 3630   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |  205645   637277 |   68548       2        6     3.0 |  0.000 % |
c |       102 |  205645   637277 |   75402     102      310     3.0 |  1.762 % |
c |       252 |  205645   637277 |   82943     252      779     3.1 |  1.762 % |
c |       477 |  205645   637277 |   91237     477     1465     3.1 |  1.762 % |
c |       814 |  205645   637277 |  100361     814     2547     3.1 |  1.762 % |
c |      1320 |  205645   637277 |  110397    1320     6505     4.9 |  1.762 % |
c |      2079 |  205645   637277 |  121436    2079     9751     4.7 |  1.762 % |
c |      3218 |  205645   637277 |  133580    3218    14912     4.6 |  1.762 % |
c |      4926 |  205636   637246 |  146938    4923    23938     4.9 |  1.764 % |
c |      7488 |  205612   637164 |  161632    7479    39275     5.3 |  1.772 % |
c |     11332 |  205612   637164 |  177795   11323    65797     5.8 |  1.772 % |
c |     17098 |  205612   637164 |  195575   17089   131210     7.7 |  1.772 % |
c |     25747 |  205612   637164 |  215132   25738   219749     8.5 |  1.772 % |
c ==============================================================================
c [1mFound solution: 800[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 7524   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26290 |  205627   637249 |   68542   26281   224347     8.5 |  1.772 % |
c |     26391 |  205627   637249 |   75396   26382   225174     8.5 |  1.791 % |
c |     26541 |  205627   637249 |   82935   26532   226532     8.5 |  1.791 % |
c |     26768 |  205627   637249 |   91229   26759   237116     8.9 |  1.791 % |
c |     27105 |  205627   637249 |  100352   27096   239199     8.8 |  1.791 % |
c |     27611 |  205627   637249 |  110387   27602   242125     8.8 |  1.791 % |
c |     28370 |  205627   637249 |  121426   28361   246826     8.7 |  1.791 % |
c |     29509 |  205627   637249 |  133568   29500   254964     8.6 |  1.791 % |
c |     31217 |  205627   637249 |  146925   31208   269202     8.6 |  1.791 % |
c ==============================================================================
c [1mFound solution: 731[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7593   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33057 |  205635   637301 |   68545   33048   287612     8.7 |  1.791 % |
c |     33157 |  205635   637301 |   75399   33148   288438     8.7 |  1.800 % |
c |     33307 |  205635   637301 |   82939   33298   289622     8.7 |  1.800 % |
c |     33532 |  205635   637301 |   91233   33523   292346     8.7 |  1.800 % |
c |     33870 |  205635   637301 |  100356   33861   295801     8.7 |  1.800 % |
c |     34376 |  205635   637301 |  110392   34367   311812     9.1 |  1.800 % |
c |     35137 |  205635   637301 |  121431   35128   318485     9.1 |  1.800 % |
c |     36277 |  205635   637301 |  133574   36268   330378     9.1 |  1.800 % |
c |     37985 |  205635   637301 |  146932   37976   352233     9.3 |  1.800 % |
c |     40547 |  205635   637301 |  161625   40538   404525    10.0 |  1.800 % |
c |     44391 |  205635   637301 |  177788   44382   447880    10.1 |  1.800 % |
c |     50157 |  205618   637206 |  195566   50144   580537    11.6 |  1.805 % |
c |     58810 |  205618   637206 |  215123   58797  1394107    23.7 |  1.805 % |
c |     71784 |  205618   637206 |  236635   71771  2084068    29.0 |  1.805 % |
c |     91245 |  205618   637206 |  260299   91232  3737706    41.0 |  1.805 % |
c |    120438 |  205618   637206 |  286329  120425  8192856    68.0 |  1.805 % |
c |    164232 |  205614   637196 |  314962  164218 12673499    77.2 |  1.807 % |
c |    229916 |  205610   637186 |  346458  229901 17869073    77.7 |  1.810 % |
c ==============================================================================
c [1mFound solution: 710[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7614   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    239698 |  205622   637265 |   68540  239683 18322828    76.4 |  1.810 % |
c |    239798 |  205622   637265 |   75394   23009   718657    31.2 |  1.821 % |
c |    239948 |  205622   637265 |   82933   23159   719298    31.1 |  1.821 % |
c |    240174 |  205622   637265 |   91226   23385   720817    30.8 |  1.821 % |
c |    240511 |  205622   637265 |  100349   23722   723701    30.5 |  1.821 % |
c |    241017 |  205618   637255 |  110384   24227   726839    30.0 |  1.824 % |
c |    241777 |  205618   637255 |  121422   24987   732199    29.3 |  1.824 % |
c |    242916 |  205618   637255 |  133565   26126   742162    28.4 |  1.824 % |
c |    244624 |  205618   637255 |  146921   27834   777113    27.9 |  1.824 % |
c |    247186 |  205618   637255 |  161613   30396   814205    26.8 |  1.824 % |
c |    251030 |  205618   637255 |  177775   34240   856570    25.0 |  1.824 % |
c |    256797 |  205618   637255 |  195552   40007   924610    23.1 |  1.824 % |
c |    265446 |  205618   637255 |  215107   48656  1016704    20.9 |  1.824 % |
c |    278420 |  205618   637255 |  236618   61630  2153878    34.9 |  1.824 % |
c |    297881 |  205618   637255 |  260280   81091  3820298    47.1 |  1.824 % |
c |    327074 |  205618   637255 |  286308  110284  6870612    62.3 |  1.824 % |
c |    370865 |  205609   637232 |  314939  154074 10363242    67.3 |  1.829 % |
c |    436549 |  205609   637232 |  346433  219758 17950329    81.7 |  1.829 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v3896 v3446 -v3326 v3226 -v3142 v1870 -v192 -v170 v3447 -v3330 -v1960 v1871 -v3895 v3451 v3329 v3227 -v3146 -v1959 -v191 -v169 -v3450 v3331 v3228 -v3144 -v1961 -v1477 -v1436 v195 -v172 -v3901 -v3448 v3335 -v3231 -v2283 v1962 -v1851 -v1690 -v1476 -v1435 -v217 -v3899 -v3449 v3334 -v3229 -v3145 -v2287 v1963 -v1689 -v1482 -v1437 v196 -v173 -v3332 -v3230 -v3149 -v2082 v1970 -v1850 v1691 -v1481 -v1438 -v216 -v175 -v3900 -v3333 -v2440 v1964 v1694 -v1483 v1439 -v220 -v176 -v4136 -v3904 -v3755 -v2439 v1965 -v1856 v1693 -v1487 v1446 -v1403 -v4135 v2445 -v1966 -v1854 v1830 v1698 -v1486 -v1440 -v221 -v4137 v3758 -v3556 v2444 v1829 -v1697 -v1484 -v1441 -v4333 -v4140 v3759 v3560 -v2576 v2446 -v1855 v1831 -v1695 -v1485 -v1442 -v577 -v4332 v4139 -v3730 -v3484 -v2575 -v2450 -v1859 v1832 -v1696 v576 v4338 v4144 v3483 -v2449 v1833 v578 -v242 v4337 v4143 -v3733 v3485 -v2577 -v2447 -v2395 v1840 -v1570 v579 -v241 -v4339 v4141 -v3734 v3488 -v2579 -v2448 v1834 -v1574 v580 v4343 v4142 v3487 -v2394 -v2378 v1835 -v973 v587 -v243 v4342 v3492 -v2580 v2398 -v2377 v1836 -v581 -v245 v4340 -v3999 v3491 v2582 -v2379 -v582 v4341 -v3775 v3489 v2583 v2399 v4438 -v583 -v246 -v3774 v3490 -v1199 -v248 v4439 v4440 -v249 v3781 v4441 -v2358 -v2202 v3780 v2942 -v2362 v3778 v2941 -v2201 v1089 v3779 -v3891 -v3445 v3223 -v3141 -v2722 v1872 v166 v3444 v3325 v3225 -v2726 -v3897 -v3455 v3327 v3224 -v3147 -v193 v171 v3328 -v3232 v197 -v174 -v3902 v3339 -v3150 -v2282 -v2078 -v1973 -v1876 -v1846 v178 -v3148 -v2286 v1974 -v1478 v177 -v3905 -v2081 v1969 -v1897 -v1852 -v1479 v1449 v1399 -v218 -v199 -v3903 v1692 -v1480 v1450 -v222 -v200 -v3754 -v1967 v1857 v1706 -v1491 v1445 -v1402 -v2441 v1702 v3760 v3555 -v2442 -v1860 v1701 v1443 -v224 -v4138 v3559 -v2571 v2443 -v1858 -v225 v4152 -v3729 -v3375 -v2570 v2454 -v2182 -v1843 -v4334 -v4148 -v3379 -v1844 -v237 -v4335 -v4147 -v3800 -v3763 -v3735 -v2578 v1839 -v1569 -v1042 -v969 -v590 -v236 v4336 v3486 -v2581 v1573 -v1046 -v591 v4347 -v3995 -v3500 v2585 -v2396 -v1837 -v1378 -v972 -v586 -v244 -v3496 v2584 v2400 -v247 -v3998 -v3738 -v3495 -v1195 -v584 -v251 -v2380 -v250 -v4020 v2402 v2388 -v1198 v4024 -v3776 v2403 v2384 v3777 -v2383 v3785 v2465 -v2357 -v2198 -v1092 v2938 -v2469 -v2361 v1093 v2937 -v2203 v1088 v3289 -v1086 v3293 -v3458 -v3139 -v2721 v1873 -v188 -v3890 v3459 v3222 -v3143 -v2725 v165 -v4092 -v4047 -v3892 -v3454 -v3342 v3240 -v3140 -v1972 -v1877 v194 v167 -v4096 v3898 -v3343 v3236 -v3151 -v1971 -v1875 -v212 v198 v168 v3894 -v3452 -v3354 v3338 -v3235 -v2284 -v2077 -v1893 -v1448 -v211 -v202 v182 -v3906 -v2288 -v1845 -v1447 -v201 -v3750 -v3336 -v2083 v1896 -v1847 -v1703 -v1494 v1398 v219 v1853 -v1705 -v1495 -v223 -v3756 -v2290 -v2010 -v1968 v1849 -v1490 -v1404 -v1170 -v227 -v2291 -v1861 -v1174 -v226 v4149 v3761 -v3725 v3684 v3557 -v2457 -v2178 v2086 -v1842 v1699 -v1488 v1444 -v49 v4151 v3561 -v2458 -v1841 -v53 -v3796 v3764 -v3731 -v3374 v2453 v2181 v1700 -v1407 -v589 v3762 -v3378 -v2572 -v2390 -v588 v4350 -v4145 -v3799 v3736 -v3563 -v3497 v2573 -v2451 -v2389 -v1571 -v1374 -v1124 -v1041 -v968 v4351 -v3564 -v3499 v2574 v1575 -v1045 -v238 v4346 -v4146 -v3994 v3739 -v2589 -v2397 -v1838 -v1377 -v974 -v239 -v3737 v2401 v240 -v4344 -v4000 -v3493 -v3425 v2405 -v2385 v1577 -v1194 -v585 v255 -v3429 v2404 v2387 v1578 -v4019 -v3494 -v1200 v977 v4023 -v4003 v3788 -v2381 -v1091 v3789 -v1090 v3784 v2464 -v2382 -v2359 v1203 -v873 v2468 -v2363 -v2197 -v3782 -v2199 v2939 v2204 v3288 v2940 v2795 v2365 -v1087 v3292 -v2799 v2366 -v4442 -v4043 -v3456 -v3341 -v3237 -v2723 v1874 v71 -v3340 -v3239 -v3138 -v2727 -v2278 -v1878 v187 v75 -v4091 -v4046 -v3350 -v3159 -v2277 -v2073 v189 v185 -v4095 v3893 -v3155 v190 v186 v3914 -v3453 -v3353 -v3233 -v3154 -v2729 -v2490 -v2285 -v2079 -v1892 -v1493 -v1394 v206 v181 -v3910 -v2730 v2494 -v2289 -v1704 -v1492 -v213 -v3909 -v3337 -v3234 -v2293 v2084 -v2006 v1898 v1400 v214 -v179 -v3749 -v3551 -v2292 v1848 v215 -v3751 -v3680 -v3550 -v2456 -v2308 v2087 -v2009 v1869 -v1405 -v1169 -v511 v231 v4150 v3757 -v2455 -v2312 v2085 v1865 -v1173 v3753 v3683 v3558 -v2177 -v1901 v1864 -v1489 -v1408 -v48 v3765 -v3724 v3562 -v1565 -v1406 -v52 -v4349 -v3795 -v3726 -v3566 v3376 v2183 -v1564 -v1120 -v964 -v4348 v3732 -v3565 -v3498 -v3380 -v3990 -v3801 v3728 v2592 -v2452 -v1572 -v1373 -v1123 -v1043 -v970 v3740 v2593 -v2391 v1576 -v1047 v3996 -v3382 -v2588 -v2392 -v2186 v1580 -v1379 -v1190 -v975 -v258 -v3383 v2393 -v2386 v1579 -v259 -v4345 -v4001 -v3804 -v3424 -v2586 -v2409 -v1674 -v1196 -v1049 v978 v254 -v3428 -v1050 v976 -v4021 -v4004 -v3787 -v2539 -v1382 -v1201 v252 v4025 -v4002 -v3786 -v2543 -v2353 -v2352 v1204 v994 -v869 v1202 -v998 v4027 v2466 -v2360 -v872 -v333 -v4028 v2470 -v2364 -v337 -v3783 v2368 v2367 -v2200 v3290 -v2945 v2794 v2472 -v2212 v3294 -v2946 -v2798 v2473 -v2208 v4042 -v3457 -v3238 -v3156 -v2724 v1886 -v184 v70 -v3158 -v2728 -v1882 v183 v74 -v4093 -v4048 -v3911 -v3349 -v2732 v1888 -v1881 -v209 -v4097 v3913 -v2731 -v2279 -v2072 -v210 -v3355 -v3152 v2489 -v2280 -v2074 -v1894 -v673 v205 v2493 -v2281 v2080 -v1393 -v677 -v4099 -v4051 -v3907 -v3153 -v2297 v2076 -v2005 v1899 -v1866 v1461 -v1395 -v507 -v234 -v203 -v180 -v146 -v4100 v2088 -v1868 v1401 -v235 -v150 -v3908 -v3679 -v3358 -v2307 -v2173 -v2011 -v1902 v1397 -v1171 -v510 -v230 -v3752 -v3552 -v3370 -v2311 -v1900 -v1409 -v1175 -v3791 -v3773 v3685 -v3553 -v3369 -v2179 -v1862 -v228 v50 -v3769 v3554 -v1037 -v54 -v4307 -v3797 -v3768 -v3705 v3570 v3377 -v2591 v2184 -v2014 -v1863 -v1369 -v1177 -v1119 -v1036 -v3727 v3709 -v3381 -v2590 -v1566 -v1178 -v963 -v3802 -v3748 v3688 -v3385 -v2187 v1567 -v1375 -v1125 -v1044 -v965 -v257 -v56 -v3989 v3744 -v3384 -v2185 v1568 -v1048 -v971 -v256 -v57 -v3991 -v3805 -v3743 -v2412 v1670 v1645 -v1584 -v1380 -v1052 v967 v4015 v3997 -v3803 -v2413 -v1649 -v1189 -v1051 v979 v4014 v3993 -v3426 -v2587 -v2408 -v1673 -v1383 v1270 -v1191 -v1128 -v4005 -v3430 -v1381 -v1274 -v1197 -v4022 v2538 -v2406 v1193 v253 v4026 -v2542 -v2460 v1205 v4030 -v3432 -v2459 v993 -v868 v4029 -v3433 -v2354 -v997 v2467 -v2355 -v874 v408 -v332 -v3284 v2471 v2356 -v412 v336 -v3283 -v2944 v2475 -v2372 -v2209 -v1019 -v2943 v2474 -v2211 -v1023 v3291 v2796 -v877 v3295 -v2800 -v2207 -v4088 v4044 -v3345 -v3157 -v2720 -v1885 v286 -v208 v72 -v3912 v2719 -v207 v76 -v4094 -v4049 -v3351 -v2736 -v1879 v725 -v457 -v4098 v1887 -v461 -v4102 v4052 -v3356 v2491 -v2300 -v2001 v1889 -v1880 v1457 -v825 v672 -v233 v78 -v4101 -v4050 v2495 -v2301 -v2075 -v1895 -v1867 -v1165 -v676 -v232 v79 -v4068 -v3675 -v3359 -v2296 -v2096 -v2007 v1891 v1460 -v1164 -v506 -v204 -v145 -v4072 -v3357 v2092 -v1903 -v1396 -v149 -v44 -v3770 -v3681 v2497 -v2309 -v2294 v2091 -v2012 -v1417 -v1172 -v512 -v43 -v3772 v2498 -v2313 -v2172 -v1413 -v1176 -v4303 v3686 v3573 -v2174 -v2031 -v2015 -v1412 -v1180 -v1115 -v229 v51 v3790 v3574 -v3371 -v2180 -v2035 -v2013 -v1179 -v55 -v4306 v3792 -v3766 -v3745 v3704 v3689 v3569 -v3372 -v2315 v2176 v1121 -v1067 -v515 -v59 -v3798 -v3747 v3708 v3687 v3373 -v2316 -v2188 -v1368 -v1071 -v1038 -v58 v3794 -v3767 -v3567 -v3389 -v2411 -v1587 -v1370 -v1126 -v1039 -v121 -v3806 -v3420 -v2410 -v1588 -v1376 -v1040 -v966 -v125 -v3741 -v3419 v1669 v1644 -v1583 -v1372 v1129 -v1056 -v987 -v3992 -v1648 -v1384 v1127 -v983 -v4013 -v3742 -v3427 -v1675 -v1581 v1269 -v982 v4016 -v4009 -v3431 v1273 -v1192 v4017 -v4008 v3435 v2540 -v2407 -v1213 -v864 v4018 v3434 -v2544 v1209 v4034 -v1678 -v1208 v995 -v870 -v2461 -v999 -v3964 -v2546 -v2462 -v2375 -v875 v407 -v334 v2790 -v2547 v2463 -v2376 -v2210 -v411 v338 v2789 -v2479 -v2371 -v1018 v1001 -v878 -v3285 -v1022 v1002 -v876 -v3286 v2797 -v2369 -v1311 v340 v3287 -v2801 -v2205 -v341 -v4040 -v3242 v2739 -v1883 -v721 v285 v73 -v4087 v4045 -v3344 v2740 -v2485 v77 -v4089 v4041 -v3346 -v2735 -v2484 -v2299 -v821 v724 -v456 v81 -v4090 v4053 -v3352 -v2298 -v460 v80 -v4106 -v3825 -v3348 -v2733 v2492 -v2093 v1456 -v824 v674 -v502 -v3360 v2496 -v2303 -v2095 -v2000 v1890 -v678 -v4067 -v3074 v2500 v2302 -v2002 v1911 v1462 -v1414 -v508 -v147 -v4071 -v3771 -v3674 -v3078 v2499 -v2008 -v1907 -v1416 -v1166 -v151 -v3676 -v3572 -v3123 -v2310 -v2295 v2089 v2004 -v1906 -v1167 v680 -v513 -v3682 -v3571 -v2314 -v2016 -v1168 v681 -v45 -v4302 v3678 -v2318 v2090 -v2030 -v1465 -v1410 -v1184 -v516 -v153 -v46 -v3746 v3690 -v2317 -v2175 -v2034 -v1114 -v514 -v154 v47 v4308 v3706 -v3392 -v2196 -v1586 -v1411 -v1116 -v1066 -v63 v3793 v3710 -v3393 v2192 -v1585 v1122 -v1070 -v3814 -v3568 -v3388 v2191 v1665 v1118 -v1059 -v984 -v120 -v3810 -v1371 v1130 -v1060 -v986 -v124 v4311 -v4010 -v3809 v3712 -v3386 v1671 v1646 -v1392 -v1055 -v4012 -v3713 v3421 -v2534 -v1650 -v1388 v3422 v2533 -v1676 -v1582 -v1387 v1271 -v1210 -v1053 -v980 -v698 v3423 v1275 -v1212 -v989 -v702 -v4037 -v4006 v3439 v2541 v1679 -v1652 v988 -v981 -v387 -v4038 -v2545 v1677 -v1653 -v863 -v328 v4033 -v4007 -v3960 -v2549 -v2374 v1277 -v1206 v996 -v865 v327 -v2548 -v2373 v1278 -v1000 -v871 v4031 -v3963 -v2812 v2482 -v1207 v1004 -v867 v409 -v335 -v2816 v2483 v1003 -v879 -v413 v339 -v3660 -v2478 -v1307 -v1020 v343 v2791 -v1024 v342 v3298 v2792 -v2476 -v2370 -v1333 -v1310 v415 v3299 v2793 -v2206 v416 -v3241 v2737 -v1884 -v1541 -v1419 -v720 v287 v69 v4039 -v1545 v668 v68 -v4109 v4061 -v3821 -v1452 -v820 v726 v667 -v458 v85 -v4110 v4057 -v3347 v2486 -v2094 -v462 -v141 -v4105 v4056 -v3824 -v3368 -v2734 v2487 v1908 v1458 -v826 v675 -v291 -v140 -v3364 v2488 v1910 -v1415 -v679 -v501 -v4103 -v4069 -v3363 -v3119 -v3073 v2504 v1463 -v729 v683 -v503 -v464 -v148 -v4073 -v3077 v2304 -v2003 v682 -v509 -v465 -v152 -v4298 -v3122 v2305 -v2024 -v1904 -v1466 -v1187 -v829 v505 -v156 -v3700 v3677 v2306 v2020 -v1464 -v1188 v517 -v155 -v4304 -v4075 -v3699 v3698 -v3391 -v2322 -v2193 v2032 v2019 -v1905 -v1183 v66 -v4076 -v3694 -v3390 -v2195 v2036 v67 v4309 -v3811 v3707 -v3693 -v1181 -v1068 -v1058 -v62 -v3813 v3711 -v1640 -v1117 -v1072 -v1057 -v985 v4312 v3715 v2189 v2038 -v1742 -v1639 -v1389 v1138 -v122 -v60 v4310 -v4011 v3714 -v2039 v1664 -v1391 -v1265 -v1134 -v126 -v3807 -v3387 v2190 v1666 v1647 v1599 -v1264 -v1133 -v1074 -v746 v1672 -v1651 -v1211 -v1075 -v750 -v4036 -v3808 -v3442 v1668 -v1655 -v1385 v1272 -v1145 -v1054 -v697 -v383 -v128 -v4035 -v3443 v2535 v1680 -v1654 v1276 -v1149 -v701 -v129 v3438 v2536 -v1386 v1280 -v386 v2537 v1279 v990 v403 -v3959 v3436 v2553 v2481 v991 v402 v2480 -v1014 v992 -v866 v329 -v4032 -v3965 -v3656 -v2811 -v1013 v1008 -v887 v410 v330 -v2815 -v883 -v414 v331 v3659 -v3297 -v3029 -v1329 -v1306 -v1021 -v882 v418 -v347 v3296 -v1025 v417 -v3968 v2804 -v2477 -v1332 -v1312 -v1026 v2805 -v1027 -v4108 -v4058 -v3243 v2738 v1915 -v1540 -v1418 -v816 -v722 -v453 v288 v88 -v4107 -v4060 -v1919 -v1544 v89 -v4116 -v3820 -v3365 -v1790 -v822 v727 -v459 -v292 v84 -v4120 -v4063 -v3367 -v1909 -v1451 v669 -v463 -v290 -v4062 v4054 -v3826 -v3247 v2507 -v1453 -v827 -v730 v670 -v467 v82 v2508 v1459 -v728 v671 -v466 -v142 -v4104 -v4070 v4055 -v3361 -v3118 -v3075 -v2976 v2503 -v2021 v1455 -v1186 -v830 -v800 v687 -v143 -v4074 -v3079 -v2980 -v2026 -v2023 -v1467 -v1185 -v828 -v504 -v144 -v4078 -v3829 v3695 -v3362 -v3124 v2501 v2325 -v2025 v648 -v525 -v160 v65 -v4297 -v4077 v3697 v2326 -v2194 -v1062 -v652 v521 v64 -v4299 -v3081 -v2321 v2033 v2017 -v1061 v520 v4305 -v3812 v3701 -v3082 v2037 -v116 v4301 -v3875 v3702 -v3691 -v3127 -v2319 v2041 -v2018 -v1738 -v1182 v1135 -v1069 -v115 v4313 v3703 v2040 -v1390 v1137 -v1073 -v3719 -v3692 -v2337 -v1741 -v1595 -v1077 -v123 -v61 -v1641 -v1076 -v127 -v3441 -v1642 v1598 -v1131 -v745 -v131 -v3440 v1667 v1643 -v1266 -v749 -v130 v1688 v1659 -v1267 -v1144 -v1132 -v699 -v382 -v1684 v1268 v1148 -v703 -v3955 -v2556 -v1683 v1284 -v388 -v2557 -v3961 -v3437 v2552 -v1011 -v884 -v705 -v532 -v1012 -v886 -v706 -v536 v404 -v3966 -v3655 -v3025 -v2813 -v2550 -v1302 v1007 v405 -v391 v350 -v2817 -v1015 v406 v351 -v3969 v3661 -v3028 v2803 -v1815 -v1328 -v1308 -v1016 v1005 -v880 v422 -v346 -v3967 v2802 -v1017 v2819 -v1334 -v1313 -v1031 -v881 -v344 v2820 -v4059 -v3816 -v3244 v1914 -v1786 -v1542 -v1420 v718 v289 -v86 -v3366 -v1918 -v1546 -v815 -v723 -v452 -v293 -v4115 -v3822 -v3248 -v2514 v2506 -v1789 -v1353 -v817 v719 -v454 -v4119 -v3246 -v3069 -v2518 v2505 -v823 -v731 -v455 -v3827 -v3114 -v3068 -v1548 -v1424 -v819 -v796 -v690 -v471 v83 -v4064 -v2022 -v1549 -v1454 -v831 -v691 -v4065 v3830 v3170 -v3120 -v3076 -v2975 v2324 -v1475 -v799 v686 -v522 -v433 -v163 -v4066 -v3828 v3696 -v3080 -v2979 v2323 -v1471 -v524 -v437 -v164 -v4082 -v3125 -v3084 v2502 -v1470 -v684 v647 -v159 -v3083 -v2027 -v651 -v3871 -v3128 -v2918 -v2028 v518 -v157 -v4300 -v3126 -v2922 v2029 v1136 -v1063 v4362 -v4321 -v3874 -v3722 -v2333 -v2320 -v2045 -v1737 -v1064 v519 -v482 -v4317 -v3723 -v1065 -v486 -v117 -v4316 -v3718 -v2336 -v1743 -v1594 -v1081 -v118 v693 -v119 -v3716 -v2751 v1685 v1662 v1600 -v747 v692 -v378 -v135 v1687 v1663 -v751 -v3507 -v2555 -v1746 v1658 -v1287 -v1146 -v700 -v384 -v3511 -v2554 -v1288 v1150 -v704 -v1681 -v1656 -v1603 v1283 -v1010 v753 -v708 -v389 -v3954 v2807 -v1009 -v885 v754 -v707 -v3956 -v3651 v2806 -v1682 v1281 v1152 -v531 -v392 v349 -v3962 v1153 -v535 -v390 v348 -v3958 -v3657 -v3024 -v2814 -v2551 -v1811 -v1324 v1249 -v425 -v3970 -v2818 -v1301 -v426 v3662 -v3030 -v2953 v2822 -v1814 v1330 -v1303 -v1034 -v1006 v421 -v2957 v2821 -v1309 -v1035 v3663 -v1335 -v1305 -v1030 v419 -v345 v3664 -v1314 -v3245 v1916 -v1785 -v1543 -v1421 -v1349 v301 -v87 v3815 -v3249 -v1920 -v1547 v717 -v297 -v4268 -v4117 v3817 -v2513 -v1791 -v1551 v1425 -v1352 -v739 -v689 -v474 -v296 -v4121 -v3823 -v2517 -v1550 -v1423 -v818 -v735 -v688 -v475 v3819 v3166 -v1922 -v1472 -v839 -v795 -v734 -v470 -v162 v3831 -v3113 -v3070 -v1923 -v1474 -v835 -v523 -v161 -v4123 -v4085 v3169 -v3115 -v3071 -v2977 -v1794 -v834 -v801 -v468 -v432 -v4124 -v4086 -v3121 v3072 v2981 -v436 -v4081 -v3117 -v3088 -v1468 -v685 v649 -v3129 v653 -v4358 -v4318 -v4079 -v3870 -v3721 v2983 -v2917 v2048 -v1733 -v1469 -v804 -v158 -v4320 -v3720 v2984 v2921 v2049 v4361 -v3876 -v2874 -v2332 -v2044 -v1739 -v1590 -v1084 v655 -v481 -v1085 v741 v656 -v485 -v4314 -v2747 -v2338 -v2042 -v1744 -v1661 -v1596 -v1080 -v771 v740 -v138 v1686 v1660 -v1140 -v775 -v139 -v4419 -v4315 -v3879 -v3717 -v2750 -v1747 v1601 -v1286 -v1139 -v1078 v748 -v270 -v134 -v4423 -v1745 -v1285 -v752 v694 -v377 -v3506 -v2341 v1604 -v1147 v756 v695 -v379 -v132 -v3510 v1602 v1151 v755 v696 -v385 -v1657 v1155 -v919 v712 -v381 v1154 -v923 -v393 -v3404 -v3020 v1282 -v1245 -v533 -v424 -v3957 -v3650 v2808 -v537 -v423 -v3978 -v3652 -v3026 v2809 v2675 -v1810 v1248 -v1033 -v3974 v3658 v2810 -v2679 -v1323 -v1032 -v3973 v3654 v3536 -v3031 v2952 v2826 -v1816 -v1325 -v846 -v539 v3665 -v2956 v1331 -v1304 v850 -v540 -v3032 v1327 -v1322 -v1028 -v420 -v3033 v1336 -v1318 v4264 -v4112 -v3257 v1917 -v1787 -v1539 v1422 -v1348 -v736 -v473 v300 -v3253 -v1921 -v1538 v1426 -v738 -v472 -v4267 -v4118 -v3252 -v2897 v2515 -v1925 -v1792 -v1555 -v1354 -v836 v791 -v294 -v4122 v3818 v2971 v2519 -v1924 -v1473 -v838 -v4126 -v4084 -v3839 v3165 v2970 -v1795 -v898 -v797 -v732 -v295 -v4125 -v4083 v3835 -v1793 v643 v3834 v3171 -v3091 -v2978 -v2521 v1357 -v832 -v802 -v733 v642 -v469 -v434 -v3116 -v3092 v2982 -v2522 -v438 -v3866 -v3137 -v3087 v2986 v2107 v2047 -v833 v805 v650 -v24 -v4319 -v3133 v2985 v2046 v803 v654 -v28 -v4357 -v4080 -v3872 -v3174 -v3132 -v3085 -v2919 -v2870 -v2328 -v1083 v658 -v440 v2923 -v1732 -v1082 v657 -v441 v4363 -v3877 -v2873 -v2334 -v1734 -v483 -v137 -v1740 -v1589 -v487 -v136 v3880 -v3846 -v2925 -v2746 -v2339 -v2043 -v1736 v1591 -v770 -v266 -v3878 v3850 -v2926 -v1748 v1597 -v774 v742 -v4418 -v4366 -v2752 -v2604 -v2342 v1593 -v1079 v743 -v489 -v269 -v4422 -v2340 v1605 -v1141 v744 -v490 v3508 -v1142 -v760 -v715 -v133 -v3512 v1143 -v716 -v527 -v380 v3400 -v2755 -v1159 -v918 -v711 -v602 -v526 -v401 -v922 -v397 -v3975 -v3514 -v3403 -v2629 -v1806 -v1244 -v709 -v534 -v396 -v3977 -v3515 -v3019 -v538 -v3631 -v3532 -v3021 -v2829 v2674 -v1812 v1250 -v542 -v3653 -v3635 -v3027 -v2830 -v2678 -v541 -v3971 -v3673 v3535 -v3023 v2954 -v2825 -v1817 -v1319 -v845 -v3669 -v3034 -v2958 -v1326 -v1321 v849 -v3972 -v3668 -v2823 v2244 -v1818 -v1344 -v1253 -v1029 -v2248 -v1819 v1340 -v1317 v4263 -v3256 -v2893 v2510 -v1913 -v1783 -v1558 -v1497 v1434 -v1350 -v737 v298 v4111 v1912 -v1788 -v1559 v1430 -v837 -v4269 v4113 -v3836 -v3250 -v3161 -v2896 v2516 -v1929 -v1784 -v1554 v1429 v1355 -v894 v4114 -v3838 v2520 -v1796 v790 -v428 -v4130 -v3251 v3167 -v3090 v2524 -v1944 -v1552 v1358 -v897 v792 -v427 -v3089 v2972 -v2523 v1356 -v798 -v4272 v3832 v3172 -v3134 v2973 -v2103 v794 v435 -v3136 v2974 -v2913 v806 v644 -v439 v4353 -v3833 -v3175 -v2990 -v2912 v2106 -v1620 v645 v443 v23 -v3865 -v3173 -v1624 v646 -v477 v442 -v27 -v4359 -v4213 -v3867 -v3130 -v3086 -v2920 -v2869 -v662 -v476 -v3873 v2924 -v2327 v4364 v3869 -v3207 -v3131 v2928 -v2875 -v2742 -v2329 -v1713 v484 v3881 -v2927 -v2335 -v1735 -v1717 -v488 -v4367 -v3845 -v2748 -v2600 v2331 -v1756 -v772 -v492 -v265 -v4365 v3849 -v3502 -v2343 -v1752 v1592 -v776 -v491 -v4420 -v3501 v2878 v2753 -v2603 -v1751 -v1613 -v763 -v714 -v271 -v4424 -v1609 v764 -v713 v3509 -v2756 -v1608 -v1162 -v778 -v759 -v598 -v398 -v3513 -v2754 v1163 -v779 -v400 v4426 v4163 -v3606 v3517 v3399 -v2625 -v1240 -v1158 -v920 -v757 -v601 -v274 v4427 -v3976 -v3610 v3516 v924 -v528 v3405 -v2828 -v2628 -v1246 -v1156 -v710 -v529 -v394 v2948 -v2827 -v1805 -v530 -v3670 -v3630 -v3531 -v3310 v2947 v2676 -v1807 v1251 -v926 -v546 -v395 -v3672 v3634 -v3022 -v2680 -v1813 -v1320 -v927 v3537 -v3408 -v3042 v2955 -v1809 -v1341 -v1254 -v847 -v3038 -v2959 -v1820 -v1343 -v1252 v851 -v3666 -v3037 -v2960 -v2824 v2682 v2243 -v2060 -v2961 v2683 -v2247 -v1339 -v1315 v4265 v3916 -v3254 -v2892 -v1932 -v1556 -v1496 v1433 -v1346 -v299 -v3837 v2509 -v1933 -v1782 -v1351 v4270 -v4133 -v2898 v2511 -v1940 -v1928 -v1804 v1427 v1347 -v893 -v4134 -v3160 v2512 -v1800 v1359 -v4273 -v4129 -v3162 -v2528 -v2424 -v1943 -v1926 -v1799 -v1553 v1428 -v899 -v4271 v3168 -v3135 v793 -v429 -v4127 v3164 v2993 -v2901 -v2700 -v2102 v814 v430 -v3176 v2994 -v2704 -v810 v431 -v4209 -v2989 -v2865 v2108 -v1619 -v902 -v809 v665 v447 -v308 v25 v4352 -v2914 v1623 v666 -v312 v29 v4354 -v4212 -v3203 -v2987 -v2915 -v2871 -v948 -v661 -v4360 -v3868 v2916 -v766 -v478 v4356 v3889 -v3206 -v2932 -v2876 -v2111 -v1981 -v1753 -v1712 -v765 -v659 -v479 v261 -v31 -v4414 -v4368 v3885 -v2741 -v2330 -v1985 -v1755 -v1716 v480 -v32 -v4413 v3884 -v3847 v2879 -v2743 -v2654 -v2599 v2351 -v2153 -v1610 -v773 -v762 -v496 -v267 v3851 v2877 -v2749 v2347 -v2157 -v1612 -v777 -v761 -v4421 v2745 v2605 v2346 -v1749 -v1161 -v781 -v272 -v100 -v4425 v3503 -v2757 -v1160 v914 -v780 -v399 v4429 -v4159 -v3853 v3504 -v3395 -v1750 -v1606 v913 -v597 v362 -v275 v4428 -v3854 v3505 -v273 v4162 -v3605 -v3521 v3401 -v2624 v2608 -v1607 -v921 -v758 -v603 -v3609 -v2670 -v1239 v925 -v3527 v3406 -v3306 -v3049 -v2669 -v2630 -v1241 -v1157 v929 -v549 -v3671 -v3053 -v1247 -v928 -v841 -v550 -v3632 -v3533 -v3409 -v3309 -v3039 v2677 v1243 v840 -v606 -v545 v3636 -v3407 -v3041 v2949 -v2681 -v1808 -v1342 -v1255 v3538 v2950 v2685 -v2633 -v2056 -v1828 v848 -v543 v2951 v2684 -v1824 v852 -v3942 -v3667 v3638 -v3539 -v3035 -v2965 v2245 v2059 -v1823 v853 v3639 -v3540 v2249 -v1337 -v1316 -v854 -v4261 -v4132 v3915 -v3255 -v2894 -v1930 -v1801 -v1557 -v1498 v1431 -v889 v4266 -v4131 -v1803 -v1345 v4262 -v3000 -v2899 -v2531 -v2420 -v1939 -v1367 -v895 -v4274 -v3004 -v2532 -v1363 v2992 -v2902 -v2527 -v2423 v2098 -v1945 -v1927 -v1797 -v1502 -v1362 v900 -v811 -v3163 v2991 -v2900 -v813 -v19 -v4128 -v3184 -v2699 -v2525 -v2104 -v1798 -v903 v664 -v450 -v18 -v3180 -v2703 -v901 v663 v451 -v4208 -v3179 v2109 -v1948 -v1621 -v1519 -v944 -v807 -v446 -v307 v26 -v2864 v1625 -v1523 -v311 v30 -v4214 v3886 -v3202 -v2988 v2935 -v2866 -v2112 -v947 -v808 -v444 -v34 v4355 v3888 -v3841 v2936 -v2872 -v2110 -v1754 -v33 -v4376 -v3840 -v3208 -v2931 v2868 -v2650 -v2595 v2348 v1980 -v1714 -v1627 -v1224 -v660 -v499 -v4372 v2880 v2350 -v1984 -v1718 -v1628 -v1611 -v767 -v500 v260 -v4371 -v4217 v3882 -v3848 -v2929 -v2653 -v2601 -v2152 -v768 -v495 v262 -v96 -v4415 v3852 v2744 -v2156 -v769 -v268 -v4416 v3883 -v3856 -v3211 v2765 v2606 v2344 -v1720 -v785 v593 -v493 -v358 v264 -v99 v4417 -v3855 -v2761 -v1721 -v276 -v4433 -v4158 -v3524 -v3264 -v2760 -v2620 v2609 v2345 v599 v361 -v3525 -v3394 -v3268 v2607 v915 v4164 v3607 -v3520 -v3396 -v2626 v916 -v627 -v604 -v548 -v3626 -v3611 v3402 v917 -v547 -v3625 -v3518 v3398 -v3305 -v3048 -v2631 -v933 -v607 v561 -v3526 v3410 -v3052 -v3040 -v2671 -v1242 -v605 -v4167 -v3633 -v3613 -v3528 -v3311 -v2672 v2634 -v1825 -v1263 v3637 -v3614 -v3534 v2673 -v2632 -v2239 -v1827 v1259 v842 -v3938 v3641 v3530 -v2968 v2689 -v2238 -v2055 v1258 v843 -v544 v3640 -v3541 v2969 v844 -v3941 -v3314 -v3036 -v2964 v2265 v2246 v2061 -v1821 v858 -v7 v2250 -v1338 -v11 v3917 v2890 -v2530 -v1935 -v1931 -v1802 v1499 v1432 -v1364 v4260 -v2895 -v2529 -v1366 -v888 -v4282 -v2999 v2891 -v2419 v1941 v1503 -v890 v4278 -v3003 v2903 -v1501 -v896 -v812 -v4277 -v3921 -v3181 -v2425 -v2128 v1946 -v1360 v892 -v449 -v3183 v2132 v2097 v1615 -v904 -v448 -v4204 -v2701 -v2526 v2099 v1949 v1614 -v1361 -v2705 v2105 -v1947 -v20 -v4210 -v4188 -v3198 -v3177 v2934 -v2428 v2101 v1622 -v1518 v943 -v309 v21 v3887 v2933 -v2113 -v1708 v1626 -v1522 -v313 v22 -v4373 -v4215 -v3204 -v3178 -v2707 -v1763 -v1707 -v1630 -v1220 -v949 -v498 -v445 -v38 -v4375 -v2867 -v2708 v2349 -v1767 -v1629 -v497 -v4218 -v3209 -v2888 -v2649 -v2219 v1982 -v1715 -v1223 -v315 -v4216 -v3842 -v2884 -v2594 -v2223 -v1986 -v1719 -v316 -v4369 -v3843 -v3212 -v2930 -v2883 -v2762 -v2655 -v2596 -v2154 -v1723 -v952 -v788 -v95 v3844 -v3210 v2764 -v2602 v2158 -v1722 -v789 v263 -v4436 -v4370 -v4154 v3860 -v3523 v2598 v1988 -v784 -v494 -v357 -v284 -v101 -v4437 -v3601 -v3522 v2610 v1989 v592 -v280 -v4432 -v4160 -v3600 -v3263 -v2758 -v2658 -v2160 -v782 v623 v594 v363 -v279 -v3267 -v2619 -v2161 v600 -v4430 v4165 v3608 -v3301 -v2837 -v2759 -v2621 -v936 -v626 v596 -v557 -v104 -v3612 -v3397 -v2841 -v2627 -v937 v608 -v4168 v3616 -v3519 -v3418 -v3307 -v3050 v2623 -v1260 -v932 v560 -v366 -v4166 -v3627 v3615 v3414 v3054 v2635 -v1826 -v1262 -v3628 v3413 -v3312 -v2967 v2692 -v2051 -v930 v3629 -v3529 -v2966 v2693 -v3937 v3645 -v3549 v3315 -v3056 v2688 -v2261 -v2057 v1256 -v861 v3545 v3313 -v3057 -v2240 -v862 -v3943 v3544 -v2962 -v2686 v2264 -v2241 v2062 -v1822 v1257 v857 -v6 v2242 -v10 -v4279 v3918 -v2415 v1500 -v1365 -v4281 v2889 -v1934 v1504 v3922 -v3001 v2911 -v2421 -v1936 -v3920 -v3182 v3005 v2907 -v2695 v1942 -v891 -v4275 -v3465 v2906 -v2694 -v2426 -v2127 v1938 -v912 v2131 v1950 v908 -v303 -v4276 v4184 v3007 -v2702 -v2429 -v939 v907 -v302 -v4203 v3008 -v2706 -v2427 v2100 v1616 -v4386 -v4205 -v4187 -v2710 v2121 v1617 -v1520 v945 -v310 -v41 -v4374 -v4211 -v3197 -v2709 v2117 -v1976 v1618 -v1524 -v314 -v42 v4207 -v3199 -v2885 -v2645 v2116 -v1975 -v1762 -v1634 -v1219 -v950 -v318 -v37 -v4219 -v3205 -v2887 -v2148 -v1766 -v1709 -v317 -v3201 -v2651 -v2218 -v2147 v1983 -v1710 -v1526 -v1225 -v953 -v787 -v91 -v35 -v3213 -v2763 -v2222 -v1987 v1711 -v1527 -v951 -v786 -v4435 -v3863 -v2881 v2656 -v2155 v1991 v1727 -v353 -v281 -v97 -v4434 -v3864 -v2597 v2159 v1990 -v283 v3859 -v2882 -v2659 -v2618 -v2163 -v1228 -v359 -v102 -v4153 -v2657 -v2614 -v2162 v4155 v3857 -v3265 -v2613 -v935 -v783 v622 v364 -v277 -v105 -v4161 -v3602 -v3269 -v3044 -v934 v595 -v103 -v4431 v4157 -v3603 -v3415 -v3043 -v2836 -v1099 -v628 v616 -v556 v367 -v278 -v4169 v3604 -v3417 -v3300 -v2840 v2622 -v1261 v612 -v365 v3620 v3302 -v3271 v3051 -v2691 v2643 v611 v562 -v3308 -v3272 v3055 -v2690 -v2639 v3933 v3648 -v3546 -v3411 v3304 -v3059 -v2638 -v931 -v860 -v631 v3649 -v3548 v3316 -v3058 -v2050 -v859 -v3939 -v3644 -v3412 -v2260 -v2052 v565 -v2058 -v3944 -v3642 -v3542 -v2963 -v2687 v2266 v2253 v2054 v855 v8 v2254 -v2063 -v12 -v4280 v3919 v2996 v2908 v1512 -v1290 v3923 v2910 -v2414 v1508 -v1294 -v3461 v3002 -v2416 -v1507 -v909 v3006 -v2422 v1937 -v911 -v3464 v3010 v2904 -v2418 -v2129 v1958 v3009 -v2696 -v2430 v2133 v1954 -v1514 -v4382 v4183 v2905 v2697 v2118 -v1953 -v1513 v905 -v40 v2698 v2120 -v938 -v304 -v39 -v4385 -v4189 v2714 -v2135 -v1637 -v1521 -v1215 v940 v906 v305 -v4206 -v2886 -v2136 -v1638 -v1525 v946 v306 v4227 -v2114 -v1764 -v1633 -v1529 -v1221 v942 v322 v4223 -v3200 -v2644 v1977 -v1768 -v1528 -v954 v4222 -v4192 -v3862 -v3585 -v3221 -v2646 -v2220 -v2115 v1978 v1730 -v1631 -v1226 -v36 -v3861 -v3217 v2652 -v2224 v2149 v1979 v1731 -v282 -v90 -v3216 v2648 -v2615 v2150 v1995 -v1770 v1726 -v1229 -v92 -v3259 -v2660 -v2617 v2151 -v1771 -v1227 -v352 -v98 -v3258 -v2226 v2167 -v1724 -v618 -v354 -v94 -v2227 -v360 -v106 v3858 -v3266 -v2611 -v1095 v624 -v613 -v552 v356 v4156 -v3416 -v3270 v615 v368 v4177 -v3623 -v3274 -v2838 -v2640 -v2612 -v1098 -v629 -v558 v4173 -v362#### 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.92 1.00 0.95 2/54 4230
Raw data (stat): 4230 (runsolver) R 4229 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481964034 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0003 s]
Raw data (loadavg): 0.93 1.00 0.95 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 11651 0 0 0 971 27 0 0 25 0 1 0 481964034 50638848 10248 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12363 10248 603 41 0 12322 0
vsize: 49452
[startup+20.0015 s]
Raw data (loadavg): 0.94 1.00 0.95 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 11699 0 0 0 1971 28 0 0 25 0 1 0 481964034 50774016 10296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12396 10296 603 41 0 12355 0
vsize: 49584
[startup+30.0018 s]
Raw data (loadavg): 0.95 1.00 0.95 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 11743 0 0 0 2971 28 0 0 25 0 1 0 481964034 51044352 10340 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12462 10340 603 41 0 12421 0
vsize: 49848
[startup+40.0043 s]
Raw data (loadavg): 1.03 1.02 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 11827 0 0 0 3970 29 0 0 25 0 1 0 481964034 51314688 10424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12528 10424 603 41 0 12487 0
vsize: 50112
[startup+50.0053 s]
Raw data (loadavg): 1.03 1.02 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 11896 0 0 0 4970 29 0 0 25 0 1 0 481964034 51630080 10493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12605 10493 603 41 0 12564 0
vsize: 50420
[startup+60.0048 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 11965 0 0 0 5970 29 0 0 25 0 1 0 481964034 51900416 10562 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12671 10562 603 41 0 12630 0
vsize: 50684
[startup+70.0055 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 12008 0 0 0 6970 30 0 0 25 0 1 0 481964034 52035584 10605 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12704 10605 603 41 0 12663 0
vsize: 50816
[startup+80.0055 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 12284 0 0 0 7969 30 0 0 25 0 1 0 481964034 52973568 10813 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12933 10813 603 41 0 12892 0
vsize: 51732
[startup+90.005 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 12295 0 0 0 8970 30 0 0 25 0 1 0 481964034 52973568 10824 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12933 10824 603 41 0 12892 0
vsize: 51732
[startup+100.005 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 12487 0 0 0 9969 31 0 0 25 0 1 0 481964034 53690368 10953 4294967295 134512640 134672761 3221224544 3221222416 1075350051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13108 10953 603 41 0 13067 0
vsize: 52432
[startup+110.005 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 12509 0 0 0 10969 31 0 0 25 0 1 0 481964034 53571584 10945 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13079 10945 603 41 0 13038 0
vsize: 52316
[startup+120.005 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 12647 0 0 0 11968 32 0 0 25 0 1 0 481964034 54108160 11083 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13210 11083 603 41 0 13169 0
vsize: 52840
[startup+130.005 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 12836 0 0 0 12968 32 0 0 25 0 1 0 481964034 54784000 11272 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13375 11272 603 41 0 13334 0
vsize: 53500
[startup+140.005 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 13433 0 0 0 13966 34 0 0 25 0 1 0 481964034 57208832 11869 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13967 11869 603 41 0 13926 0
vsize: 55868
[startup+150.005 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 14009 0 0 0 14964 36 0 0 25 0 1 0 481964034 59498496 12445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14526 12445 603 41 0 14485 0
vsize: 58104
[startup+160.005 s]
Raw data (loadavg): 1.00 1.00 0.96 3/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 14451 0 0 0 15962 39 0 0 25 0 1 0 481964034 61640704 12887 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15049 12887 603 41 0 15008 0
vsize: 60196
[startup+170.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 14731 0 0 0 16961 40 0 0 25 0 1 0 481964034 62722048 13167 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15313 13167 603 41 0 15272 0
vsize: 61252
[startup+180.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 15533 0 0 0 17959 42 0 0 25 0 1 0 481964034 65961984 13969 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16104 13969 603 41 0 16063 0
vsize: 64416
[startup+190.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 16207 0 0 0 18957 44 0 0 25 0 1 0 481964034 68800512 14643 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16797 14643 603 41 0 16756 0
vsize: 67188
[startup+200.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 16450 0 0 0 19957 45 0 0 25 0 1 0 481964034 69742592 14886 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17027 14886 603 41 0 16986 0
vsize: 68108
[startup+210.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 16972 0 0 0 20955 47 0 0 25 0 1 0 481964034 71766016 15408 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17521 15408 603 41 0 17480 0
vsize: 70084
[startup+220.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 17943 0 0 0 21952 49 0 0 25 0 1 0 481964034 75792384 16379 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18504 16379 603 41 0 18463 0
vsize: 74016
[startup+230.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 18889 0 0 0 22950 52 0 0 25 0 1 0 481964034 79568896 17325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19426 17325 603 41 0 19385 0
vsize: 77704
[startup+240.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 19764 0 0 0 23947 55 0 0 25 0 1 0 481964034 83197952 18200 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20312 18200 603 41 0 20271 0
vsize: 81248
[startup+250.004 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 20561 0 0 0 24945 57 0 0 25 0 1 0 481964034 86441984 18997 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21104 18997 603 41 0 21063 0
vsize: 84416
[startup+260.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 21262 0 0 0 25943 59 0 0 25 0 1 0 481964034 89268224 19698 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21794 19698 603 41 0 21753 0
vsize: 87176
[startup+270.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 21739 0 0 0 26942 61 0 0 25 0 1 0 481964034 91680768 20175 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22383 20175 603 41 0 22342 0
vsize: 89532
[startup+280.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 22217 0 0 0 27941 62 0 0 25 0 1 0 481964034 93708288 20653 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22878 20653 603 41 0 22837 0
vsize: 91512
[startup+290.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 22814 0 0 0 28939 64 0 0 25 0 1 0 481964034 96137216 21250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23471 21250 603 41 0 23430 0
vsize: 93884
[startup+300.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 23544 0 0 0 29938 65 0 0 25 0 1 0 481964034 99094528 21980 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24193 21980 603 41 0 24152 0
vsize: 96772
[startup+310.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 24235 0 0 0 30935 69 0 0 25 0 1 0 481964034 101924864 22671 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24884 22671 603 41 0 24843 0
vsize: 99536
[startup+320.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 24937 0 0 0 31933 71 0 0 25 0 1 0 481964034 104755200 23373 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25575 23373 603 41 0 25534 0
vsize: 102300
[startup+330.007 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 25545 0 0 0 32931 72 0 0 25 0 1 0 481964034 107175936 23981 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26166 23981 603 41 0 26125 0
vsize: 104664
[startup+340.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 26149 0 0 0 33930 74 0 0 25 0 1 0 481964034 109731840 24585 4294967295 134512640 134672761 3221224544 3221223648 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26790 24585 603 41 0 26749 0
vsize: 107160
[startup+350.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 26649 0 0 0 34928 76 0 0 25 0 1 0 481964034 111747072 25085 4294967295 134512640 134672761 3221224544 3221223696 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27282 25085 603 41 0 27241 0
vsize: 109128
[startup+360.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 27192 0 0 0 35927 77 0 0 25 0 1 0 481964034 113893376 25628 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27806 25628 603 41 0 27765 0
vsize: 111224
[startup+370.007 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 27632 0 0 0 36926 79 0 0 25 0 1 0 481964034 115634176 26068 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28231 26068 603 41 0 28190 0
vsize: 112924
[startup+380.007 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 28056 0 0 0 37924 80 0 0 25 0 1 0 481964034 117387264 26492 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28659 26492 603 41 0 28618 0
vsize: 114636
[startup+390.007 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 28474 0 0 0 38923 82 0 0 25 0 1 0 481964034 119140352 26910 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29087 26910 603 41 0 29046 0
vsize: 116348
[startup+400.007 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 28836 0 0 0 39922 83 0 0 25 0 1 0 481964034 120610816 27272 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29446 27272 603 41 0 29405 0
vsize: 117784
[startup+410.007 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 29188 0 0 0 40921 84 0 0 25 0 1 0 481964034 122089472 27624 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29807 27624 603 41 0 29766 0
vsize: 119228
[startup+420.008 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 29545 0 0 0 41921 85 0 0 25 0 1 0 481964034 123441152 27981 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30137 27981 603 41 0 30096 0
vsize: 120548
[startup+430.008 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 29903 0 0 0 42919 87 0 0 25 0 1 0 481964034 124968960 28339 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30510 28339 603 41 0 30469 0
vsize: 122040
[startup+440.008 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 30255 0 0 0 43918 88 0 0 25 0 1 0 481964034 126468096 28691 4294967295 134512640 134672761 3221224544 3221223560 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30876 28692 603 41 0 30835 0
vsize: 123504
[startup+450.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 30570 0 0 0 44918 89 0 0 25 0 1 0 481964034 127684608 29006 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31173 29006 603 41 0 31132 0
vsize: 124692
[startup+460.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 30933 0 0 0 45916 91 0 0 25 0 1 0 481964034 129155072 29369 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31532 29369 603 41 0 31491 0
vsize: 126128
[startup+470.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 31356 0 0 0 46915 92 0 0 25 0 1 0 481964034 130899968 29792 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31958 29792 603 41 0 31917 0
vsize: 127832
[startup+480.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 31738 0 0 0 47914 93 0 0 25 0 1 0 481964034 132382720 30174 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32320 30174 603 41 0 32279 0
vsize: 129280
[startup+490.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32365 0 0 0 48911 96 0 0 25 0 1 0 481964034 134942720 30801 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32945 30801 603 41 0 32904 0
vsize: 131780
[startup+500.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32727 0 0 0 49910 97 0 0 25 0 1 0 481964034 136404992 31163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33302 31163 603 41 0 33261 0
vsize: 133208
[startup+510.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 50909 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+520.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 51909 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+530.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 52909 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+540.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 53910 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+550.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 54910 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+560.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 55910 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+570.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 56910 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+580.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 57910 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+590.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 58910 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+600.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 59910 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+610.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 60910 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+620.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 61911 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+630.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 62911 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+640.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 63911 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+650.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 64911 98 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+660.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 65911 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+670.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 66911 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+680.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 67911 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+690.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 68911 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+700.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 69911 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+710.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 70912 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+720.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 71912 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+730.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 72912 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+740.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 73912 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+750.013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 74912 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+760.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 75912 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+770.013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 76913 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+780.013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 77913 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+790.013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 78913 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+800.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 79913 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+810.013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 80913 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+820.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 81913 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+830.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 82913 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+840.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 83914 99 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+850.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 84913 100 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223728 134559583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+860.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 85914 100 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+870.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 86914 100 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+880.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 87914 100 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+890.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 88914 100 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+900.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 89914 100 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+910.014 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 90914 100 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+920.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 91915 100 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+930.016 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 32979 0 0 0 92915 100 0 0 25 0 1 0 481964034 136622080 31233 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33355 31233 603 41 0 33314 0
vsize: 133420
[startup+940.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 33403 0 0 0 93914 101 0 0 25 0 1 0 481964034 138375168 31657 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33783 31657 603 41 0 33742 0
vsize: 135132
[startup+950.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 33727 0 0 0 94913 102 0 0 25 0 1 0 481964034 139718656 31981 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34111 31981 603 41 0 34070 0
vsize: 136444
[startup+960.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 33876 0 0 0 95912 102 0 0 25 0 1 0 481964034 140390400 32130 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34275 32130 603 41 0 34234 0
vsize: 137100
[startup+970.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 33984 0 0 0 96912 103 0 0 25 0 1 0 481964034 140795904 32238 4294967295 134512640 134672761 3221224544 3221223636 1075346528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34374 32238 603 41 0 34333 0
vsize: 137496
[startup+980.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 34525 0 0 0 97911 104 0 0 25 0 1 0 481964034 143089664 32779 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34934 32779 603 41 0 34893 0
vsize: 139736
[startup+990.015 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 34760 0 0 0 98910 105 0 0 25 0 1 0 481964034 144035840 33014 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35165 33014 603 41 0 35124 0
vsize: 140660
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 35241 0 0 0 99909 106 0 0 25 0 1 0 481964034 145920000 33495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35625 33495 603 41 0 35584 0
vsize: 142500
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 35822 0 0 0 100908 108 0 0 25 0 1 0 481964034 148336640 34076 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36215 34076 603 41 0 36174 0
vsize: 144860
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 35945 0 0 0 101908 108 0 0 25 0 1 0 481964034 148742144 34199 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36314 34199 603 41 0 36273 0
vsize: 145256
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 36427 0 0 0 102907 109 0 0 25 0 1 0 481964034 150761472 34681 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36807 34681 603 41 0 36766 0
vsize: 147228
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 37083 0 0 0 103906 111 0 0 25 0 1 0 481964034 153456640 35337 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37465 35337 603 41 0 37424 0
vsize: 149860
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 37953 0 0 0 104904 113 0 0 25 0 1 0 481964034 157052928 36207 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38343 36207 603 41 0 38302 0
vsize: 153372
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 38820 0 0 0 105902 115 0 0 25 0 1 0 481964034 161558528 37074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39443 37074 603 41 0 39402 0
vsize: 157772
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 39554 0 0 0 106901 116 0 0 25 0 1 0 481964034 164634624 37808 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40194 37808 603 41 0 40153 0
vsize: 160776
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 39770 0 0 0 107901 117 0 0 25 0 1 0 481964034 165441536 38024 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40391 38024 603 41 0 40350 0
vsize: 161564
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 40043 0 0 0 108900 118 0 0 25 0 1 0 481964034 166518784 38297 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40654 38297 603 41 0 40613 0
vsize: 162616
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 40341 0 0 0 109898 119 0 0 25 0 1 0 481964034 167731200 38595 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40950 38595 603 41 0 40909 0
vsize: 163800
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 40713 0 0 0 110898 120 0 0 25 0 1 0 481964034 169213952 38967 4294967295 134512640 134672761 3221224544 3221223728 134558671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41312 38967 603 41 0 41271 0
vsize: 165248
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 41118 0 0 0 111896 122 0 0 25 0 1 0 481964034 170971136 39372 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41741 39372 603 41 0 41700 0
vsize: 166964
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 41502 0 0 0 112896 123 0 0 25 0 1 0 481964034 172449792 39756 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42102 39756 603 41 0 42061 0
vsize: 168408
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 41891 0 0 0 113895 124 0 0 25 0 1 0 481964034 174067712 40145 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42497 40145 603 41 0 42456 0
vsize: 169988
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 42285 0 0 0 114893 125 0 0 25 0 1 0 481964034 175681536 40539 4294967295 134512640 134672761 3221224544 3221223728 134559293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42891 40539 603 41 0 42850 0
vsize: 171564
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 42663 0 0 0 115892 126 0 0 25 0 1 0 481964034 177156096 40917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43251 40917 603 41 0 43210 0
vsize: 173004
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 43027 0 0 0 116891 127 0 0 25 0 1 0 481964034 178765824 41281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43644 41281 603 41 0 43603 0
vsize: 174576
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 43243 0 0 0 117891 128 0 0 25 0 1 0 481964034 179576832 41497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43842 41497 603 41 0 43801 0
vsize: 175368
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 43578 0 0 0 118890 130 0 0 25 0 1 0 481964034 180924416 41832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44171 41832 603 41 0 44130 0
vsize: 176684
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4230
Raw data (stat): 4230 (minisat+) R 4229 27565 27564 0 -1 0 44122 0 0 0 119888 131 0 0 25 0 1 0 481964034 183205888 42376 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44728 42376 603 41 0 44687 0
vsize: 178912
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 4230
Raw data (stat): 4230 (minisat+) Z 4229 27565 27564 0 -1 12 44125 0 0 0 119889 139 0 0 25 0 1 0 481964034 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 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: 10
Real time (s): 1200.11
CPU time (s): 1200.29
CPU user time (s): 1198.9
CPU system time (s): 1.39679
CPU usage (%): 100.015
Max. virtual memory (Kb): 178912
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####