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.95:98.opb
MD5SUM	5f5bedf3690a537deb8cc97cc5d565ae
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	94
Optimality of the best value was proved	NO
Number of terms in the objective function	4624
Biggest coefficient in the objective function	2577
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	13335
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	2577
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	13335
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.07084
Number of variables	4624
Total number of constraints	9886
Number of constraints which are clauses	4404
Number of constraints which are cardinality constraints (but not clauses)	5482
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	22
Trace number 6474

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        820312 kB
Buffers:         35428 kB
Cached:         136252 kB
SwapCached:       3828 kB
Active:          63412 kB
Inactive:       114996 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        820032 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30380 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:31:04 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 4886 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5262 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 870]---> BDD-cost:   11
c ---[ 869]---> BDD-cost:   20
c ---[ 868]---> BDD-cost:   29
c ---[ 867]---> BDD-cost:   29
c ---[ 866]---> BDD-cost:   29
c ---[ 865]---> BDD-cost:   26
c ---[ 864]---> BDD-cost:   38
c ---[ 863]---> BDD-cost:   26
c ---[ 862]---> BDD-cost:   20
c ---[ 861]---> BDD-cost:   20
c ---[ 860]---> BDD-cost:   23
c ---[ 859]---> BDD-cost:   20
c ---[ 858]---> BDD-cost:   23
c ---[ 857]---> BDD-cost:   23
c ---[ 856]---> BDD-cost:   26
c ---[ 855]---> BDD-cost:   11
c ---[ 854]---> BDD-cost:   11
c ---[ 853]---> BDD-cost:    8
c ---[ 852]---> BDD-cost:   11
c ---[ 851]---> BDD-cost:    8
c ---[ 850]---> BDD-cost:   14
c ---[ 849]---> BDD-cost:    8
c ---[ 848]---> BDD-cost:    7
c ---[ 843]---> BDD-cost:   26
c ---[ 842]---> BDD-cost:   35
c ---[ 841]---> BDD-cost:   32
c ---[ 840]---> BDD-cost:   38
c ---[ 839]---> BDD-cost:   38
c ---[ 838]---> BDD-cost:   44
c ---[ 837]---> BDD-cost:   35
c ---[ 836]---> BDD-cost:   29
c ---[ 835]---> BDD-cost:   29
c ---[ 834]---> BDD-cost:   24
c ---[ 833]---> BDD-cost:   29
c ---[ 832]---> BDD-cost:   26
c ---[ 831]---> BDD-cost:   26
c ---[ 830]---> BDD-cost:   17
c ---[ 829]---> BDD-cost:   20
c ---[ 828]---> BDD-cost:   11
c ---[ 827]---> BDD-cost:   17
c ---[ 826]---> BDD-cost:   20
c ---[ 825]---> BDD-cost:   23
c ---[ 824]---> BDD-cost:   18
c ---[ 823]---> BDD-cost:   18
c ---[ 821]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:   35
c ---[ 816]---> BDD-cost:   25
c ---[ 815]---> BDD-cost:   45
c ---[ 814]---> BDD-cost:   39
c ---[ 813]---> BDD-cost:   44
c ---[ 812]---> BDD-cost:   41
c ---[ 811]---> BDD-cost:   50
c ---[ 810]---> BDD-cost:   44
c ---[ 809]---> BDD-cost:   38
c ---[ 808]---> BDD-cost:   35
c ---[ 807]---> BDD-cost:   35
c ---[ 806]---> BDD-cost:   32
c ---[ 805]---> BDD-cost:   38
c ---[ 804]---> BDD-cost:   26
c ---[ 803]---> BDD-cost:   26
c ---[ 802]---> BDD-cost:   20
c ---[ 801]---> BDD-cost:   23
c ---[ 800]---> BDD-cost:   17
c ---[ 799]---> BDD-cost:   20
c ---[ 798]---> BDD-cost:   21
c ---[ 797]---> BDD-cost:   26
c ---[ 796]---> BDD-cost:   23
c ---[ 795]---> BDD-cost:   26
c ---[ 794]---> BDD-cost:   13
c ---[ 793]---> BDD-cost:   20
c ---[ 792]---> BDD-cost:   11
c ---[ 789]---> BDD-cost:   20
c ---[ 788]---> BDD-cost:   29
c ---[ 787]---> BDD-cost:   41
c ---[ 786]---> BDD-cost:   44
c ---[ 785]---> BDD-cost:   56
c ---[ 784]---> BDD-cost:   53
c ---[ 783]---> BDD-cost:   53
c ---[ 782]---> BDD-cost:   47
c ---[ 781]---> BDD-cost:   47
c ---[ 780]---> BDD-cost:   44
c ---[ 779]---> BDD-cost:   47
c ---[ 778]---> BDD-cost:   41
c ---[ 777]---> BDD-cost:   38
c ---[ 776]---> BDD-cost:   35
c ---[ 775]---> BDD-cost:   38
c ---[ 774]---> BDD-cost:   35
c ---[ 773]---> BDD-cost:   29
c ---[ 772]---> BDD-cost:   20
c ---[ 771]---> BDD-cost:   20
c ---[ 770]---> BDD-cost:   17
c ---[ 769]---> BDD-cost:   20
c ---[ 768]---> BDD-cost:   29
c ---[ 767]---> BDD-cost:   32
c ---[ 766]---> BDD-cost:   26
c ---[ 765]---> BDD-cost:   32
c ---[ 764]---> BDD-cost:   19
c ---[ 763]---> BDD-cost:   26
c ---[ 762]---> BDD-cost:   17
c ---[ 761]---> BDD-cost:    7
c ---[ 760]---> BDD-cost:   17
c ---[ 759]---> BDD-cost:   26
c ---[ 758]---> BDD-cost:   32
c ---[ 757]---> BDD-cost:   44
c ---[ 756]---> BDD-cost:   47
c ---[ 755]---> BDD-cost:   53
c ---[ 754]---> BDD-cost:   53
c ---[ 753]---> BDD-cost:   47
c ---[ 752]---> BDD-cost:   47
c ---[ 751]---> BDD-cost:   50
c ---[ 750]---> BDD-cost:   47
c ---[ 749]---> BDD-cost:   45
c ---[ 748]---> BDD-cost:   44
c ---[ 747]---> BDD-cost:   41
c ---[ 746]---> BDD-cost:   38
c ---[ 745]---> BDD-cost:   35
c ---[ 744]---> BDD-cost:   29
c ---[ 743]---> BDD-cost:   20
c ---[ 742]---> BDD-cost:   23
c ---[ 741]---> BDD-cost:   23
c ---[ 740]---> BDD-cost:   20
c ---[ 739]---> BDD-cost:   23
c ---[ 738]---> BDD-cost:   26
c ---[ 737]---> BDD-cost:   30
c ---[ 736]---> BDD-cost:   35
c ---[ 735]---> BDD-cost:   35
c ---[ 734]---> BDD-cost:   29
c ---[ 733]---> BDD-cost:   23
c ---[ 732]---> BDD-cost:   20
c ---[ 731]---> BDD-cost:   17
c ---[ 730]---> BDD-cost:   17
c ---[ 729]---> BDD-cost:   27
c ---[ 728]---> BDD-cost:   35
c ---[ 727]---> BDD-cost:   47
c ---[ 726]---> BDD-cost:   50
c ---[ 725]---> BDD-cost:   47
c ---[ 724]---> BDD-cost:   44
c ---[ 723]---> BDD-cost:   47
c ---[ 722]---> BDD-cost:   50
c ---[ 721]---> BDD-cost:   44
c ---[ 720]---> BDD-cost:   41
c ---[ 719]---> BDD-cost:   44
c ---[ 718]---> BDD-cost:   47
c ---[ 717]---> BDD-cost:   38
c ---[ 716]---> BDD-cost:   35
c ---[ 715]---> BDD-cost:   35
c ---[ 714]---> BDD-cost:   29
c ---[ 713]---> BDD-cost:   20
c ---[ 712]---> BDD-cost:   20
c ---[ 711]---> BDD-cost:   20
c ---[ 710]---> BDD-cost:   23
c ---[ 709]---> BDD-cost:   17
c ---[ 708]---> BDD-cost:   26
c ---[ 707]---> BDD-cost:   32
c ---[ 706]---> BDD-cost:   29
c ---[ 705]---> BDD-cost:   29
c ---[ 704]---> BDD-cost:   32
c ---[ 703]---> BDD-cost:   24
c ---[ 702]---> BDD-cost:   17
c ---[ 701]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:   23
c ---[ 699]---> BDD-cost:   35
c ---[ 698]---> BDD-cost:   38
c ---[ 697]---> BDD-cost:   41
c ---[ 696]---> BDD-cost:   38
c ---[ 695]---> BDD-cost:   44
c ---[ 694]---> BDD-cost:   47
c ---[ 693]---> BDD-cost:   44
c ---[ 692]---> BDD-cost:   44
c ---[ 691]---> BDD-cost:   47
c ---[ 690]---> BDD-cost:   44
c ---[ 689]---> BDD-cost:   47
c ---[ 688]---> BDD-cost:   44
c ---[ 687]---> BDD-cost:   38
c ---[ 686]---> BDD-cost:   32
c ---[ 685]---> BDD-cost:   23
c ---[ 684]---> BDD-cost:   29
c ---[ 683]---> BDD-cost:   20
c ---[ 682]---> BDD-cost:   20
c ---[ 681]---> BDD-cost:   11
c ---[ 680]---> BDD-cost:   14
c ---[ 679]---> BDD-cost:   17
c ---[ 678]---> BDD-cost:   26
c ---[ 677]---> BDD-cost:   29
c ---[ 676]---> BDD-cost:   29
c ---[ 675]---> BDD-cost:   32
c ---[ 674]---> BDD-cost:   32
c ---[ 673]---> BDD-cost:   29
c ---[ 672]---> BDD-cost:   20
c ---[ 671]---> BDD-cost:   26
c ---[ 670]---> BDD-cost:   26
c ---[ 669]---> BDD-cost:   38
c ---[ 668]---> BDD-cost:   41
c ---[ 667]---> BDD-cost:   41
c ---[ 666]---> BDD-cost:   41
c ---[ 665]---> BDD-cost:   38
c ---[ 664]---> BDD-cost:   44
c ---[ 663]---> BDD-cost:   44
c ---[ 662]---> BDD-cost:   41
c ---[ 661]---> BDD-cost:   47
c ---[ 660]---> BDD-cost:   47
c ---[ 659]---> BDD-cost:   44
c ---[ 658]---> BDD-cost:   44
c ---[ 657]---> BDD-cost:   32
c ---[ 656]---> BDD-cost:   29
c ---[ 655]---> BDD-cost:   29
c ---[ 654]---> BDD-cost:   23
c ---[ 653]---> BDD-cost:   14
c ---[ 652]---> BDD-cost:   11
c ---[ 651]---> BDD-cost:    8
c ---[ 650]---> BDD-cost:   14
c ---[ 649]---> BDD-cost:   17
c ---[ 648]---> BDD-cost:   17
c ---[ 647]---> BDD-cost:   24
c ---[ 646]---> BDD-cost:   32
c ---[ 645]---> BDD-cost:   29
c ---[ 644]---> BDD-cost:   26
c ---[ 643]---> BDD-cost:   20
c ---[ 642]---> BDD-cost:   26
c ---[ 641]---> BDD-cost:   29
c ---[ 640]---> BDD-cost:   35
c ---[ 639]---> BDD-cost:   41
c ---[ 638]---> BDD-cost:   38
c ---[ 637]---> BDD-cost:   38
c ---[ 636]---> BDD-cost:   38
c ---[ 635]---> BDD-cost:   41
c ---[ 634]---> BDD-cost:   41
c ---[ 633]---> BDD-cost:   38
c ---[ 632]---> BDD-cost:   42
c ---[ 631]---> BDD-cost:   47
c ---[ 630]---> BDD-cost:   41
c ---[ 629]---> BDD-cost:   41
c ---[ 628]---> BDD-cost:   32
c ---[ 627]---> BDD-cost:   29
c ---[ 626]---> BDD-cost:   26
c ---[ 625]---> BDD-cost:   18
c ---[ 624]---> BDD-cost:   14
c ---[ 623]---> BDD-cost:   11
c ---[ 622]---> BDD-cost:    8
c ---[ 621]---> BDD-cost:   11
c ---[ 620]---> BDD-cost:   23
c ---[ 619]---> BDD-cost:   23
c ---[ 618]---> BDD-cost:   23
c ---[ 617]---> BDD-cost:   26
c ---[ 616]---> BDD-cost:   29
c ---[ 615]---> BDD-cost:   20
c ---[ 614]---> BDD-cost:   17
c ---[ 613]---> BDD-cost:   24
c ---[ 612]---> BDD-cost:   26
c ---[ 611]---> BDD-cost:   29
c ---[ 610]---> BDD-cost:   35
c ---[ 609]---> BDD-cost:   35
c ---[ 608]---> BDD-cost:   35
c ---[ 607]---> BDD-cost:   44
c ---[ 606]---> BDD-cost:   47
c ---[ 605]---> BDD-cost:   53
c ---[ 604]---> BDD-cost:   38
c ---[ 603]---> BDD-cost:   41
c ---[ 602]---> BDD-cost:   41
c ---[ 601]---> BDD-cost:   38
c ---[ 600]---> BDD-cost:   50
c ---[ 599]---> BDD-cost:   53
c ---[ 598]---> BDD-cost:   44
c ---[ 597]---> BDD-cost:   41
c ---[ 596]---> BDD-cost:   29
c ---[ 595]---> BDD-cost:   26
c ---[ 594]---> BDD-cost:   20
c ---[ 593]---> BDD-cost:   11
c ---[ 592]---> BDD-cost:    8
c ---[ 591]---> BDD-cost:    8
c ---[ 590]---> BDD-cost:   17
c ---[ 589]---> BDD-cost:   20
c ---[ 588]---> BDD-cost:   26
c ---[ 587]---> BDD-cost:   26
c ---[ 586]---> BDD-cost:   26
c ---[ 585]---> BDD-cost:   20
c ---[ 584]---> BDD-cost:   14
c ---[ 583]---> BDD-cost:   23
c ---[ 582]---> BDD-cost:   32
c ---[ 581]---> BDD-cost:   32
c ---[ 580]---> BDD-cost:   41
c ---[ 579]---> BDD-cost:   38
c ---[ 578]---> BDD-cost:   48
c ---[ 577]---> BDD-cost:   53
c ---[ 576]---> BDD-cost:   56
c ---[ 575]---> BDD-cost:   47
c ---[ 574]---> BDD-cost:   47
c ---[ 573]---> BDD-cost:   44
c ---[ 572]---> BDD-cost:   53
c ---[ 571]---> BDD-cost:   53
c ---[ 570]---> BDD-cost:   53
c ---[ 569]---> BDD-cost:   47
c ---[ 568]---> BDD-cost:   41
c ---[ 567]---> BDD-cost:   35
c ---[ 566]---> BDD-cost:   29
c ---[ 565]---> BDD-cost:   23
c ---[ 564]---> BDD-cost:   17
c ---[ 563]---> BDD-cost:   11
c ---[ 562]---> BDD-cost:    8
c ---[ 561]---> BDD-cost:   11
c ---[ 560]---> BDD-cost:   20
c ---[ 559]---> BDD-cost:   23
c ---[ 558]---> BDD-cost:   20
c ---[ 557]---> BDD-cost:   20
c ---[ 556]---> BDD-cost:   17
c ---[ 555]---> BDD-cost:   17
c ---[ 554]---> BDD-cost:   23
c ---[ 553]---> BDD-cost:   29
c ---[ 552]---> BDD-cost:   35
c ---[ 551]---> BDD-cost:   41
c ---[ 550]---> BDD-cost:   50
c ---[ 549]---> BDD-cost:   47
c ---[ 548]---> BDD-cost:   47
c ---[ 547]---> BDD-cost:   47
c ---[ 546]---> BDD-cost:   50
c ---[ 545]---> BDD-cost:   50
c ---[ 544]---> BDD-cost:   56
c ---[ 543]---> BDD-cost:   59
c ---[ 542]---> BDD-cost:   59
c ---[ 541]---> BDD-cost:   47
c ---[ 540]---> BDD-cost:   44
c ---[ 539]---> BDD-cost:   47
c ---[ 538]---> BDD-cost:   32
c ---[ 537]---> BDD-cost:   26
c ---[ 536]---> BDD-cost:   26
c ---[ 535]---> BDD-cost:   20
c ---[ 534]---> BDD-cost:   14
c ---[ 533]---> BDD-cost:   17
c ---[ 532]---> BDD-cost:   20
c ---[ 531]---> BDD-cost:   23
c ---[ 530]---> BDD-cost:   20
c ---[ 529]---> BDD-cost:   20
c ---[ 528]---> BDD-cost:   17
c ---[ 527]---> BDD-cost:   11
c ---[ 526]---> BDD-cost:   11
c ---[ 525]---> BDD-cost:   23
c ---[ 524]---> BDD-cost:   29
c ---[ 523]---> BDD-cost:   32
c ---[ 522]---> BDD-cost:   41
c ---[ 521]---> BDD-cost:   41
c ---[ 520]---> BDD-cost:   44
c ---[ 519]---> BDD-cost:   47
c ---[ 518]---> BDD-cost:   50
c ---[ 517]---> BDD-cost:   50
c ---[ 516]---> BDD-cost:   50
c ---[ 515]---> BDD-cost:   53
c ---[ 514]---> BDD-cost:   56
c ---[ 513]---> BDD-cost:   47
c ---[ 512]---> BDD-cost:   53
c ---[ 511]---> BDD-cost:   53
c ---[ 510]---> BDD-cost:   47
c ---[ 509]---> BDD-cost:   47
c ---[ 508]---> BDD-cost:   41
c ---[ 507]---> BDD-cost:   35
c ---[ 506]---> BDD-cost:   24
c ---[ 505]---> BDD-cost:   29
c ---[ 504]---> BDD-cost:   26
c ---[ 503]---> BDD-cost:   26
c ---[ 502]---> BDD-cost:   23
c ---[ 501]---> BDD-cost:   32
c ---[ 500]---> BDD-cost:   26
c ---[ 499]---> BDD-cost:   26
c ---[ 498]---> BDD-cost:   17
c ---[ 497]---> BDD-cost:   14
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:   17
c ---[ 494]---> BDD-cost:   29
c ---[ 493]---> BDD-cost:   26
c ---[ 492]---> BDD-cost:   32
c ---[ 491]---> BDD-cost:   38
c ---[ 490]---> BDD-cost:   38
c ---[ 489]---> BDD-cost:   47
c ---[ 488]---> BDD-cost:   44
c ---[ 487]---> BDD-cost:   41
c ---[ 486]---> BDD-cost:   50
c ---[ 485]---> BDD-cost:   56
c ---[ 484]---> BDD-cost:   56
c ---[ 483]---> BDD-cost:   56
c ---[ 482]---> BDD-cost:   50
c ---[ 481]---> BDD-cost:   47
c ---[ 480]---> BDD-cost:   44
c ---[ 479]---> BDD-cost:   44
c ---[ 478]---> BDD-cost:   38
c ---[ 477]---> BDD-cost:   36
c ---[ 476]---> BDD-cost:   35
c ---[ 475]---> BDD-cost:   38
c ---[ 474]---> BDD-cost:   38
c ---[ 473]---> BDD-cost:   35
c ---[ 472]---> BDD-cost:   41
c ---[ 471]---> BDD-cost:   32
c ---[ 470]---> BDD-cost:   32
c ---[ 469]---> BDD-cost:   20
c ---[ 468]---> BDD-cost:   20
c ---[ 467]---> BDD-cost:   11
c ---[ 466]---> BDD-cost:   11
c ---[ 465]---> BDD-cost:   23
c ---[ 464]---> BDD-cost:   35
c ---[ 463]---> BDD-cost:   44
c ---[ 462]---> BDD-cost:   41
c ---[ 461]---> BDD-cost:   47
c ---[ 460]---> BDD-cost:   47
c ---[ 459]---> BDD-cost:   45
c ---[ 458]---> BDD-cost:   47
c ---[ 457]---> BDD-cost:   50
c ---[ 456]---> BDD-cost:   56
c ---[ 455]---> BDD-cost:   50
c ---[ 454]---> BDD-cost:   53
c ---[ 453]---> BDD-cost:   38
c ---[ 452]---> BDD-cost:   35
c ---[ 451]---> BDD-cost:   41
c ---[ 450]---> BDD-cost:   41
c ---[ 449]---> BDD-cost:   35
c ---[ 448]---> BDD-cost:   38
c ---[ 447]---> BDD-cost:   44
c ---[ 446]---> BDD-cost:   41
c ---[ 445]---> BDD-cost:   38
c ---[ 444]---> BDD-cost:   41
c ---[ 443]---> BDD-cost:   41
c ---[ 442]---> BDD-cost:   35
c ---[ 441]---> BDD-cost:   35
c ---[ 440]---> BDD-cost:   29
c ---[ 439]---> BDD-cost:   20
c ---[ 438]---> BDD-cost:   14
c ---[ 437]---> BDD-cost:   12
c ---[ 436]---> BDD-cost:   14
c ---[ 435]---> BDD-cost:   20
c ---[ 434]---> BDD-cost:   35
c ---[ 433]---> BDD-cost:   38
c ---[ 432]---> BDD-cost:   50
c ---[ 431]---> BDD-cost:   50
c ---[ 430]---> BDD-cost:   50
c ---[ 429]---> BDD-cost:   41
c ---[ 428]---> BDD-cost:   47
c ---[ 427]---> BDD-cost:   50
c ---[ 426]---> BDD-cost:   50
c ---[ 425]---> BDD-cost:   38
c ---[ 424]---> BDD-cost:   41
c ---[ 423]---> BDD-cost:   30
c ---[ 422]---> BDD-cost:   35
c ---[ 421]---> BDD-cost:   29
c ---[ 420]---> BDD-cost:   32
c ---[ 419]---> BDD-cost:   32
c ---[ 418]---> BDD-cost:   41
c ---[ 417]---> BDD-cost:   41
c ---[ 416]---> BDD-cost:   41
c ---[ 415]---> BDD-cost:   41
c ---[ 414]---> BDD-cost:   41
c ---[ 413]---> BDD-cost:   50
c ---[ 412]---> BDD-cost:   41
c ---[ 411]---> BDD-cost:   41
c ---[ 410]---> BDD-cost:   29
c ---[ 409]---> BDD-cost:   20
c ---[ 408]---> BDD-cost:   14
c ---[ 407]---> BDD-cost:   14
c ---[ 406]---> BDD-cost:   14
c ---[ 405]---> BDD-cost:   20
c ---[ 404]---> BDD-cost:   26
c ---[ 403]---> BDD-cost:   29
c ---[ 402]---> BDD-cost:   44
c ---[ 401]---> BDD-cost:   47
c ---[ 400]---> BDD-cost:   53
c ---[ 399]---> BDD-cost:   44
c ---[ 398]---> BDD-cost:   44
c ---[ 397]---> BDD-cost:   38
c ---[ 396]---> BDD-cost:   35
c ---[ 395]---> BDD-cost:   26
c ---[ 394]---> BDD-cost:   35
c ---[ 393]---> BDD-cost:   23
c ---[ 392]---> BDD-cost:   26
c ---[ 391]---> BDD-cost:   32
c ---[ 390]---> BDD-cost:   32
c ---[ 389]---> BDD-cost:   29
c ---[ 388]---> BDD-cost:   32
c ---[ 387]---> BDD-cost:   45
c ---[ 386]---> BDD-cost:   44
c ---[ 385]---> BDD-cost:   44
c ---[ 384]---> BDD-cost:   41
c ---[ 383]---> BDD-cost:   47
c ---[ 382]---> BDD-cost:   47
c ---[ 381]---> BDD-cost:   50
c ---[ 380]---> BDD-cost:   32
c ---[ 379]---> BDD-cost:   29
c ---[ 378]---> BDD-cost:   11
c ---[ 377]---> BDD-cost:    8
c ---[ 376]---> BDD-cost:   14
c ---[ 375]---> BDD-cost:   20
c ---[ 374]---> BDD-cost:   23
c ---[ 373]---> BDD-cost:   27
c ---[ 372]---> BDD-cost:   38
c ---[ 371]---> BDD-cost:   32
c ---[ 370]---> BDD-cost:   47
c ---[ 369]---> BDD-cost:   35
c ---[ 368]---> BDD-cost:   35
c ---[ 367]---> BDD-cost:   26
c ---[ 366]---> BDD-cost:   23
c ---[ 365]---> BDD-cost:   23
c ---[ 364]---> BDD-cost:   23
c ---[ 363]---> BDD-cost:   17
c ---[ 362]---> BDD-cost:   23
c ---[ 361]---> BDD-cost:   20
c ---[ 360]---> BDD-cost:   26
c ---[ 359]---> BDD-cost:   29
c ---[ 358]---> BDD-cost:   38
c ---[ 357]---> BDD-cost:   47
c ---[ 356]---> BDD-cost:   50
c ---[ 355]---> BDD-cost:   50
c ---[ 354]---> BDD-cost:   47
c ---[ 353]---> BDD-cost:   50
c ---[ 352]---> BDD-cost:   44
c ---[ 351]---> BDD-cost:   53
c ---[ 350]---> BDD-cost:   47
c ---[ 349]---> BDD-cost:   29
c ---[ 348]---> BDD-cost:   14
c ---[ 347]---> BDD-cost:   11
c ---[ 346]---> BDD-cost:   11
c ---[ 345]---> BDD-cost:   17
c ---[ 344]---> BDD-cost:   26
c ---[ 343]---> BDD-cost:   26
c ---[ 342]---> BDD-cost:   30
c ---[ 341]---> BDD-cost:   26
c ---[ 340]---> BDD-cost:   29
c ---[ 339]---> BDD-cost:   23
c ---[ 338]---> BDD-cost:   32
c ---[ 337]---> BDD-cost:   32
c ---[ 336]---> BDD-cost:   23
c ---[ 335]---> BDD-cost:   14
c ---[ 334]---> BDD-cost:   23
c ---[ 333]---> BDD-cost:   14
c ---[ 332]---> BDD-cost:   20
c ---[ 331]---> BDD-cost:   14
c ---[ 330]---> BDD-cost:   17
c ---[ 329]---> BDD-cost:   20
c ---[ 328]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   44
c ---[ 326]---> BDD-cost:   53
c ---[ 325]---> BDD-cost:   47
c ---[ 324]---> BDD-cost:   50
c ---[ 323]---> BDD-cost:   53
c ---[ 322]---> BDD-cost:   56
c ---[ 321]---> BDD-cost:   47
c ---[ 320]---> BDD-cost:   38
c ---[ 319]---> BDD-cost:   29
c ---[ 318]---> BDD-cost:   17
c ---[ 317]---> BDD-cost:    8
c ---[ 316]---> BDD-cost:    8
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   20
c ---[ 313]---> BDD-cost:   23
c ---[ 312]---> BDD-cost:   26
c ---[ 311]---> BDD-cost:   26
c ---[ 310]---> BDD-cost:   26
c ---[ 309]---> BDD-cost:   26
c ---[ 308]---> BDD-cost:   26
c ---[ 307]---> BDD-cost:   26
c ---[ 306]---> BDD-cost:   23
c ---[ 305]---> BDD-cost:   17
c ---[ 304]---> BDD-cost:   11
c ---[ 303]---> BDD-cost:   11
c ---[ 302]---> BDD-cost:   17
c ---[ 301]---> BDD-cost:   12
c ---[ 300]---> BDD-cost:   11
c ---[ 299]---> BDD-cost:   14
c ---[ 298]---> BDD-cost:   26
c ---[ 297]---> BDD-cost:   29
c ---[ 296]---> BDD-cost:   41
c ---[ 295]---> BDD-cost:   44
c ---[ 294]---> BDD-cost:   47
c ---[ 293]---> BDD-cost:   44
c ---[ 292]---> BDD-cost:   50
c ---[ 291]---> BDD-cost:   38
c ---[ 290]---> BDD-cost:   26
c ---[ 289]---> BDD-cost:   17
c ---[ 288]---> BDD-cost:   14
c ---[ 287]---> BDD-cost:   11
c ---[ 286]---> BDD-cost:   17
c ---[ 285]---> BDD-cost:   20
c ---[ 284]---> BDD-cost:   32
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:   26
c ---[ 281]---> BDD-cost:   26
c ---[ 280]---> BDD-cost:   23
c ---[ 279]---> BDD-cost:   26
c ---[ 278]---> BDD-cost:   20
c ---[ 277]---> BDD-cost:   17
c ---[ 276]---> BDD-cost:   14
c ---[ 275]---> BDD-cost:   11
c ---[ 274]---> BDD-cost:   14
c ---[ 273]---> BDD-cost:   14
c ---[ 272]---> BDD-cost:   14
c ---[ 271]---> BDD-cost:   11
c ---[ 270]---> BDD-cost:   17
c ---[ 269]---> BDD-cost:   23
c ---[ 268]---> BDD-cost:   32
c ---[ 267]---> BDD-cost:   38
c ---[ 266]---> BDD-cost:   44
c ---[ 265]---> BDD-cost:   35
c ---[ 264]---> BDD-cost:   41
c ---[ 263]---> BDD-cost:   35
c ---[ 262]---> BDD-cost:   26
c ---[ 261]---> BDD-cost:   17
c ---[ 260]---> BDD-cost:    8
c ---[ 259]---> BDD-cost:   12
c ---[ 258]---> BDD-cost:   23
c ---[ 257]---> BDD-cost:   26
c ---[ 256]---> BDD-cost:   32
c ---[ 255]---> BDD-cost:   32
c ---[ 254]---> BDD-cost:   29
c ---[ 253]---> BDD-cost:   29
c ---[ 252]---> BDD-cost:   29
c ---[ 251]---> BDD-cost:   18
c ---[ 250]---> BDD-cost:   20
c ---[ 249]---> BDD-cost:   20
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   11
c ---[ 246]---> BDD-cost:   14
c ---[ 245]---> BDD-cost:   20
c ---[ 244]---> BDD-cost:   20
c ---[ 243]---> BDD-cost:   17
c ---[ 242]---> BDD-cost:   23
c ---[ 241]---> BDD-cost:   21
c ---[ 240]---> BDD-cost:   26
c ---[ 239]---> BDD-cost:   30
c ---[ 238]---> BDD-cost:   38
c ---[ 237]---> BDD-cost:   35
c ---[ 236]---> BDD-cost:   29
c ---[ 235]---> BDD-cost:   35
c ---[ 234]---> BDD-cost:   30
c ---[ 233]---> BDD-cost:   23
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   11
c ---[ 230]---> BDD-cost:   14
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:   32
c ---[ 227]---> BDD-cost:   35
c ---[ 226]---> BDD-cost:   29
c ---[ 225]---> BDD-cost:   29
c ---[ 224]---> BDD-cost:   35
c ---[ 223]---> BDD-cost:   35
c ---[ 222]---> BDD-cost:   29
c ---[ 221]---> BDD-cost:   29
c ---[ 220]---> BDD-cost:   17
c ---[ 219]---> BDD-cost:   17
c ---[ 218]---> BDD-cost:   17
c ---[ 217]---> BDD-cost:   26
c ---[ 216]---> BDD-cost:   26
c ---[ 215]---> BDD-cost:   23
c ---[ 214]---> BDD-cost:   29
c ---[ 213]---> BDD-cost:   26
c ---[ 212]---> BDD-cost:   26
c ---[ 211]---> BDD-cost:   29
c ---[ 210]---> BDD-cost:   32
c ---[ 209]---> BDD-cost:   32
c ---[ 208]---> BDD-cost:   35
c ---[ 207]---> BDD-cost:   35
c ---[ 206]---> BDD-cost:   29
c ---[ 205]---> BDD-cost:   23
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:   14
c ---[ 202]---> BDD-cost:   17
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:   26
c ---[ 199]---> BDD-cost:   29
c ---[ 198]---> BDD-cost:   38
c ---[ 197]---> BDD-cost:   35
c ---[ 196]---> BDD-cost:   26
c ---[ 195]---> BDD-cost:   35
c ---[ 194]---> BDD-cost:   32
c ---[ 193]---> BDD-cost:   26
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   26
c ---[ 190]---> BDD-cost:   23
c ---[ 189]---> BDD-cost:   29
c ---[ 188]---> BDD-cost:   35
c ---[ 187]---> BDD-cost:   29
c ---[ 186]---> BDD-cost:   32
c ---[ 185]---> BDD-cost:   38
c ---[ 184]---> BDD-cost:   29
c ---[ 183]---> BDD-cost:   23
c ---[ 182]---> BDD-cost:   20
c ---[ 181]---> BDD-cost:   26
c ---[ 180]---> BDD-cost:   32
c ---[ 179]---> BDD-cost:   26
c ---[ 178]---> BDD-cost:   32
c ---[ 177]---> BDD-cost:   26
c ---[ 176]---> BDD-cost:   23
c ---[ 175]---> BDD-cost:   20
c ---[ 174]---> BDD-cost:   14
c ---[ 173]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   23
c ---[ 171]---> BDD-cost:   29
c ---[ 170]---> BDD-cost:   32
c ---[ 169]---> BDD-cost:   29
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   35
c ---[ 166]---> BDD-cost:   29
c ---[ 165]---> BDD-cost:   26
c ---[ 164]---> BDD-cost:   32
c ---[ 163]---> BDD-cost:   26
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   26
c ---[ 160]---> BDD-cost:   32
c ---[ 159]---> BDD-cost:   35
c ---[ 158]---> BDD-cost:   26
c ---[ 157]---> BDD-cost:   29
c ---[ 156]---> BDD-cost:   35
c ---[ 155]---> BDD-cost:   32
c ---[ 154]---> BDD-cost:   23
c ---[ 153]---> BDD-cost:   23
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   23
c ---[ 150]---> BDD-cost:   29
c ---[ 149]---> BDD-cost:   26
c ---[ 148]---> BDD-cost:   17
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   17
c ---[ 145]---> BDD-cost:   17
c ---[ 144]---> BDD-cost:   20
c ---[ 143]---> BDD-cost:   29
c ---[ 142]---> BDD-cost:   35
c ---[ 141]---> BDD-cost:   32
c ---[ 140]---> BDD-cost:   23
c ---[ 139]---> BDD-cost:   20
c ---[ 138]---> BDD-cost:   26
c ---[ 137]---> BDD-cost:   32
c ---[ 136]---> BDD-cost:   32
c ---[ 135]---> BDD-cost:   32
c ---[ 134]---> BDD-cost:   29
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   29
c ---[ 131]---> BDD-cost:   35
c ---[ 130]---> BDD-cost:   35
c ---[ 129]---> BDD-cost:   32
c ---[ 128]---> BDD-cost:   29
c ---[ 127]---> BDD-cost:   38
c ---[ 126]---> BDD-cost:   38
c ---[ 125]---> BDD-cost:   41
c ---[ 124]---> BDD-cost:   32
c ---[ 123]---> BDD-cost:   32
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   26
c ---[ 120]---> BDD-cost:   29
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:   17
c ---[ 117]---> BDD-cost:   14
c ---[ 116]---> BDD-cost:    8
c ---[ 115]---> BDD-cost:   17
c ---[ 114]---> BDD-cost:   23
c ---[ 113]---> BDD-cost:   20
c ---[ 112]---> BDD-cost:   29
c ---[ 111]---> BDD-cost:   32
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   26
c ---[ 108]---> BDD-cost:   23
c ---[ 107]---> BDD-cost:   29
c ---[ 106]---> BDD-cost:   29
c ---[ 105]---> BDD-cost:   23
c ---[ 104]---> BDD-cost:   29
c ---[ 103]---> BDD-cost:   29
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:   38
c ---[ 100]---> BDD-cost:   38
c ---[  99]---> BDD-cost:   36
c ---[  98]---> BDD-cost:   32
c ---[  97]---> BDD-cost:   38
c ---[  96]---> BDD-cost:   44
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:   38
c ---[  93]---> BDD-cost:   38
c ---[  92]---> BDD-cost:   35
c ---[  91]---> BDD-cost:   32
c ---[  90]---> BDD-cost:   26
c ---[  89]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   20
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:    7
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:   26
c ---[  81]---> BDD-cost:   23
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   26
c ---[  78]---> BDD-cost:   27
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   20
c ---[  75]---> BDD-cost:   20
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   23
c ---[  72]---> BDD-cost:   29
c ---[  71]---> BDD-cost:   35
c ---[  70]---> BDD-cost:   38
c ---[  69]---> BDD-cost:   35
c ---[  68]---> BDD-cost:   38
c ---[  67]---> BDD-cost:   38
c ---[  66]---> BDD-cost:   35
c ---[  65]---> BDD-cost:   38
c ---[  64]---> BDD-cost:   35
c ---[  63]---> BDD-cost:   35
c ---[  62]---> BDD-cost:   32
c ---[  61]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   20
c ---[  59]---> BDD-cost:   17
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:    3
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   20
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   17
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   17
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   20
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   23
c ---[  42]---> BDD-cost:   26
c ---[  41]---> BDD-cost:   26
c ---[  40]---> BDD-cost:   26
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   29
c ---[  37]---> BDD-cost:   38
c ---[  36]---> BDD-cost:   29
c ---[  35]---> BDD-cost:   30
c ---[  34]---> BDD-cost:   29
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   24
c ---[  31]---> BDD-cost:   23
c ---[  30]---> BDD-cost:   17
c ---[  29]---> BDD-cost:   17
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    5
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:    8
c ---[  18]---> BDD-cost:    8
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:    8
c ---[  14]---> BDD-cost:   17
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   20
c ---[  11]---> BDD-cost:   23
c ---[  10]---> BDD-cost:   26
c ---[   9]---> BDD-cost:   17
c ---[   8]---> BDD-cost:   23
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   23
c ---[   5]---> BDD-cost:   21
c ---[   4]---> BDD-cost:   23
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  124692   350668 |   41564       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 4900[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11365   maxlim: 3281   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |  204189   634560 |   68063       1        3     3.0 |  0.000 % |
c |       101 |  204189   634560 |   74869     101      318     3.1 |  2.098 % |
c |       251 |  204189   634560 |   82356     251      777     3.1 |  2.098 % |
c |       476 |  204189   634560 |   90591     476     1642     3.4 |  2.098 % |
c |       813 |  204189   634560 |   99651     813     2790     3.4 |  2.098 % |
c |      1319 |  204189   634560 |  109616    1319     4957     3.8 |  2.098 % |
c |      2078 |  204189   634560 |  120577    2078     8610     4.1 |  2.098 % |
c |      3217 |  204189   634560 |  132635    3217    14277     4.4 |  2.098 % |
c |      4925 |  204189   634560 |  145899    4925    23442     4.8 |  2.098 % |
c |      7487 |  204189   634560 |  160488    7487    42537     5.7 |  2.098 % |
c |     11331 |  204180   634529 |  176537   11327    70672     6.2 |  2.100 % |
c |     17099 |  204180   634529 |  194191   17095   117040     6.8 |  2.100 % |
c |     25748 |  204180   634529 |  213610   25744   187712     7.3 |  2.100 % |
c |     38722 |  204180   634529 |  234971   38718   381878     9.9 |  2.100 % |
c ==============================================================================
c [1mFound solution: 870[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 7311   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49996 |  204197   634589 |   68065   49992   499971    10.0 |  2.100 % |
c |     50096 |  204197   634589 |   74871   50092   500730    10.0 |  2.112 % |
c |     50246 |  204197   634589 |   82358   50242   501735    10.0 |  2.112 % |
c |     50471 |  204197   634589 |   90594   50467   503251    10.0 |  2.112 % |
c |     50808 |  204197   634589 |   99653   50804   505758    10.0 |  2.112 % |
c |     51314 |  204197   634589 |  109619   51310   509355     9.9 |  2.112 % |
c |     52073 |  204197   634589 |  120581   52069   515395     9.9 |  2.112 % |
c |     53212 |  204197   634589 |  132639   53208   525741     9.9 |  2.112 % |
c |     54920 |  204197   634589 |  145903   54916   540858     9.8 |  2.112 % |
c ==============================================================================
c [1mFound solution: 822[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7359   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56836 |  204204   634610 |   68068   56832   560937     9.9 |  2.112 % |
c |     56936 |  204204   634610 |   74874   56932   562274     9.9 |  2.114 % |
c |     57086 |  204204   634610 |   82362   57082   564572     9.9 |  2.114 % |
c |     57311 |  204204   634610 |   90598   57307   567533     9.9 |  2.114 % |
c |     57648 |  204204   634610 |   99658   57644   571726     9.9 |  2.114 % |
c ==============================================================================
c [1mFound solution: 813[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7368   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57977 |  204210   634649 |   68070   57973   575010     9.9 |  2.114 % |
c |     58077 |  204210   634649 |   74877   58073   575919     9.9 |  2.119 % |
c |     58227 |  204210   634649 |   82364   58223   578748     9.9 |  2.119 % |
c |     58453 |  204210   634649 |   90601   58449   581868    10.0 |  2.119 % |
c |     58790 |  204210   634649 |   99661   58786   585028    10.0 |  2.119 % |
c |     59297 |  204210   634649 |  109627   59293   593958    10.0 |  2.119 % |
c |     60056 |  204195   634580 |  120590   60051   601241    10.0 |  2.124 % |
c |     61196 |  204195   634580 |  132649   61191   610935    10.0 |  2.124 % |
c |     62904 |  204195   634580 |  145914   62899   627815    10.0 |  2.124 % |
c |     65467 |  204195   634580 |  160505   65462   657163    10.0 |  2.124 % |
c |     69311 |  204195   634580 |  176556   69306   718761    10.4 |  2.124 % |
c |     75078 |  204195   634580 |  194211   75073   797380    10.6 |  2.124 % |
c |     83728 |  204195   634580 |  213632   83723  1469806    17.6 |  2.124 % |
c |     96702 |  204195   634580 |  234996   96697  2123566    22.0 |  2.124 % |
c ==============================================================================
c [1mFound solution: 749[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7432   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    106900 |  204207   634632 |   68069  106895  2289454    21.4 |  2.124 % |
c |    107000 |  204207   634632 |   74875   23778   351568    14.8 |  2.131 % |
c |    107150 |  204207   634632 |   82363   23928   352453    14.7 |  2.131 % |
c |    107375 |  204207   634632 |   90599   24153   354202    14.7 |  2.131 % |
c |    107712 |  204207   634632 |   99659   24490   356899    14.6 |  2.131 % |
c |    108218 |  204207   634632 |  109625   24996   361060    14.4 |  2.131 % |
c |    108978 |  204207   634632 |  120588   25756   370913    14.4 |  2.131 % |
c |    110117 |  204207   634632 |  132647   26895   380202    14.1 |  2.131 % |
c |    111825 |  204207   634632 |  145911   28603   389214    13.6 |  2.131 % |
c |    114387 |  204207   634632 |  160503   31165   405314    13.0 |  2.131 % |
c |    118231 |  204207   634632 |  176553   35009   435429    12.4 |  2.131 % |
c |    123997 |  204207   634632 |  194208   40775   517788    12.7 |  2.131 % |
c |    132648 |  204207   634632 |  213629   49426   659069    13.3 |  2.131 % |
c |    145622 |  204207   634632 |  234992   62400  1183317    19.0 |  2.131 % |
c |    165084 |  204207   634632 |  258491   81862  1573831    19.2 |  2.131 % |
c |    194276 |  204207   634632 |  284341  111054  3019924    27.2 |  2.131 % |
c ==============================================================================
c [1mFound solution: 729[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7452   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    231429 |  204214   634689 |   68071  148207  4768124    32.2 |  2.131 % |
c |    231529 |  204214   634689 |   74878   22581   524873    23.2 |  2.140 % |
c |    231679 |  204214   634689 |   82365   22731   525874    23.1 |  2.140 % |
c |    231904 |  204214   634689 |   90602   22956   527557    23.0 |  2.140 % |
c |    232242 |  204214   634689 |   99662   23294   529858    22.7 |  2.140 % |
c |    232748 |  204214   634689 |  109629   23800   533321    22.4 |  2.140 % |
c |    233507 |  204214   634689 |  120591   24559   540065    22.0 |  2.140 % |
c |    234646 |  204214   634689 |  132651   25698   547966    21.3 |  2.140 % |
c |    236355 |  204214   634689 |  145916   27407   560505    20.5 |  2.140 % |
c |    238917 |  204214   634689 |  160507   29969   589357    19.7 |  2.140 % |
c |    242761 |  204214   634689 |  176558   33813   623030    18.4 |  2.140 % |
c |    248527 |  204214   634689 |  194214   39579   692098    17.5 |  2.140 % |
c |    257176 |  204214   634689 |  213635   48228   809886    16.8 |  2.140 % |
c |    270150 |  204214   634689 |  234999   61202  1040892    17.0 |  2.140 % |
c |    289612 |  204214   634689 |  258499   80664  1444563    17.9 |  2.140 % |
c |    318804 |  204214   634689 |  284349  109856  2351547    21.4 |  2.140 % |
c |    362593 |  204214   634689 |  312784  153645  7148405    46.5 |  2.140 % |
c |    428277 |  204214   634689 |  344062  219329  8802750    40.1 |  2.140 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v4221 -v3659 -v4226 -v3780 -v3680 v3132 v2610 -v4225 -v3895 -v3779 -v3679 v2609 -v334 -v4026 v3781 v3133 v2615 v1996 -v335 -v4228 -v4025 -v3894 v3782 -v3681 -v3135 v2614 -v1405 -v1103 -v559 -v338 -v4229 v4031 -v3898 v3783 -v3683 -v3136 v2616 -v1997 -v1108 -v336 -v4232 v4030 -v3790 v2620 -v1999 -v1408 v1107 -v558 -v416 -v337 -v4230 v4032 -v3899 -v3784 -v3684 v2619 -v2000 -v1409 -v1083 -v562 v4476 -v4285 -v4231 -v4036 -v3785 -v3724 v3686 v2617 -v1359 -v1225 -v1110 -v1082 -v4035 -v3786 v3723 v3687 v2618 -v1230 -v1111 -v1088 -v563 -v4479 v4284 -v4033 v3725 v3310 -v1229 v1114 -v1087 -v4480 -v4034 v3728 -v1112 -v1089 -v654 v4290 v3727 v3309 v2165 v1232 -v1113 v1093 -v989 -v653 -v4335 v4288 v3732 v1233 -v1092 -v655 -v4334 -v3731 -v3315 v2164 v1236 -v1090 -v992 -v656 -v387 -v4289 -v3729 -v3313 v1234 -v1091 -v993 v657 -v391 -v4359 -v4336 -v4293 -v3730 v2170 -v1235 v853 v664 -v4338 -v3314 v2168 v858 v658 -v4362 -v3318 v857 v659 -v4363 -v4339 v2169 v660 -v4341 v3572 v2173 v860 -v52 -v4342 v3571 v1979 v861 -v56 -v3708 v3573 v1978 -v1336 v864 -v316 v4621 v1983 v862 -v3634 v1982 -v1335 v863 -v319 -v3638 v4622 -v320 -v3655 v3148 -v3130 -v1993 -v3658 -v1992 -v4220 -v3675 v3134 -v4222 -v3674 -v3138 -v1938 -v4227 -v3137 v2611 v1998 -v339 v4224 -v3896 v3793 v3682 v2612 v2002 -v1404 -v638 -v412 -v4233 -v4027 -v3900 v3794 v3685 v2613 -v2001 -v1102 -v4028 -v3789 v3689 -v2624 -v2451 -v1410 -v1355 v1104 v560 -v415 v4029 v3688 -v2455 v1109 v564 v4475 -v4280 v4040 v3902 -v3787 -v1358 v1106 -v3903 -v1224 v1115 -v1084 -v4481 v4286 -v3305 -v1413 -v1226 -v1085 -v833 -v566 v3726 -v1231 v1086 -v837 -v567 v4291 v3740 v3311 v2160 v1228 v1097 v988 -v4330 v3736 v1237 -v4484 v4329 v4294 v3735 v3316 v2166 -v994 -v667 v386 v4292 -v668 -v390 -v4358 -v4337 v3319 v2171 v663 -v4340 v3317 v852 v4364 -v4344 v2174 -v997 v854 -v661 -v4343 v2172 v859 -v3704 v856 -v51 v865 -v55 -v4367 v3707 v315 -v224 v3574 v1980 v228 -v3633 v3582 v1981 -v1337 -v321 -v3637 v3578 v3577 v1987 -v1459 -v3654 v3147 -v3129 v3660 -v3131 -v1934 v3890 -v1994 -v4268 v3889 -v3792 -v3142 -v1995 -v1937 v1400 -v634 -v347 -v4223 v3791 -v3676 v554 v343 v4241 -v3897 -v3677 -v3663 -v3456 v2627 -v2006 -v1406 -v637 v553 -v411 v342 v4237 -v3901 v3678 v2628 -v4471 -v4236 v4043 v3905 -v3693 -v3285 -v2623 -v2450 -v1411 v1354 v561 -v417 v4044 v3904 -v3289 -v2454 v1105 v565 v4477 v4039 -v3788 -v2621 -v1414 -v1360 -v1123 -v569 -v4279 -v1412 -v1119 -v568 -v4482 -v4281 v4037 v3737 -v1118 v1100 -v984 -v832 -v420 v4287 v3739 -v3304 -v1227 v1101 -v836 v4485 v4283 -v3306 v1363 -v1245 v1096 v990 -v666 -v512 -v4483 v4295 v3312 v2159 v1241 -v665 -v516 -v4354 v3733 v3308 v2161 v1240 v1094 -v995 -v491 v388 v4331 v3320 v2167 -v392 -v4360 v4332 v3734 v2163 -v998 v4333 v2175 -v996 v4365 v4348 -v662 v394 v855 v395 v4368 -v3703 v873 -v311 -v53 v4366 v1332 -v869 -v57 v3709 v3579 -v1719 v1331 -v868 v317 -v223 v3581 -v1723 v227 -v3635 -v1990 -v1455 -v1338 -v322 -v59 -v3639 -v1991 -v60 -v3712 -v3575 v1986 -v1458 v1339 -v541 v323 v1340 v324 -v3656 v3149 -v2279 v4269 v3661 v3145 -v1933 -v344 -v4267 v3146 -v346 v4238 -v3664 -v3452 -v3153 -v3141 -v2626 -v2194 -v2009 -v1939 -v633 -v407 v4240 v3891 -v3662 v2625 -v2010 v1399 v4042 v3892 v3696 -v3455 -v3213 -v3139 -v2005 v1401 -v1350 -v639 -v413 -v340 v4041 v3893 v3697 -v3217 -v1407 v555 -v4234 v3909 -v3692 -v3284 -v2452 -v2003 -v1942 v1403 v1356 -v1120 v556 -v418 -v341 -v4470 -v3288 v2456 -v1415 -v1122 v557 -v4472 -v4235 -v3690 -v2622 -v1361 -v1099 -v642 v573 -v421 v4478 v3738 -v1098 -v419 v4474 v4038 -v2458 v1364 -v1242 -v1116 -v834 -v462 v4486 -v4282 -v2459 v1362 -v1244 -v983 -v838 -v466 -v382 -v4303 -v1117 -v985 -v511 -v487 -v381 v4299 -v3307 v991 -v515 v4298 -v3328 v1238 -v1095 v987 -v840 -v490 v389 -v4353 -v3324 v2162 v999 -v841 -v393 v4355 -v4351 -v3323 v2183 v1239 v397 -v4361 -v4352 v2179 v396 -v47 v4357 v4347 -v3699 v2178 -v870 -v46 v4369 v872 -v4345 -v3705 -v54 -v3629 -v3580 -v310 -v58 v3710 -v3628 -v2263 -v1989 -v1718 -v866 -v312 v225 -v62 -v1988 -v1722 v1333 v318 v229 -v61 -v3801 v3713 -v3636 -v1454 v1334 -v867 -v537 v314 -v3805 -v3711 -v3640 v325 -v3641 -v3576 v1984 -v1460 v1344 -v540 -v231 -v3642 -v232 v3652 v3150 -v3144 -v2278 -v1929 v4270 v3657 -v3143 -v345 v3653 v3154 -v2190 -v2008 -v1935 -v629 v4239 -v3665 -v3152 -v2007 -v3695 -v3451 -v2193 -v2046 -v1940 -v635 -v3694 -v2446 -v406 -v3912 -v3457 -v3212 -v3140 -v2789 -v2445 -v1943 -v640 -v408 -v3913 -v3216 -v1941 v1402 -v1349 -v1121 -v414 v3908 v3286 -v2453 -v2004 -v1423 -v1351 -v643 -v576 -v410 -v3290 v2457 -v1419 v1357 -v828 -v641 v577 -v422 -v3906 -v3691 -v3460 v2461 -v1811 -v1418 v1353 -v827 v572 -v203 -v4473 -v2460 -v1815 v1365 -v1243 v4494 -v4300 v3292 -v835 v570 -v461 -v4490 -v4302 v3293 -v839 -v465 -v4489 -v3325 -v2928 -v843 -v513 -v486 -v156 -v3327 -v2932 -v986 -v842 -v517 -v383 -v4350 v4296 v2180 -v1007 -v492 v384 -v4349 v2182 -v1003 v385 v4297 -v3321 -v1002 -v519 v401 v4356 -v871 -v520 v4377 -v3322 v2176 -v495 v4373 -v3698 -v219 -v48 v4372 -v4346 v3700 -v2259 v2177 -v218 -v49 -v3706 -v50 v3702 -v2262 -v1720 -v1450 v226 -v66 v3714 -v3630 v1724 v313 v230 v4579 -v3800 -v3631 v1456 -v1347 -v536 -v333 v234 -v3804 -v3632 -v1348 v329 v233 -v3646 v1985 -v1726 -v1461 v1343 v542 -v328 -v1727 -v4278 v3151 -v2280 -v808 v294 v4274 v3651 v3155 -v1928 -v812 v4273 v3673 -v3613 -v3447 -v2189 v2042 -v1930 v3669 -v1936 -v628 -v3911 -v3668 -v3453 -v2839 v2785 -v2284 -v2195 -v2045 v1932 -v630 -v3910 -v3280 -v1944 -v636 -v3458 -v3279 v3214 -v2788 -v1420 v632 -v575 -v3218 v2447 -v1422 v644 -v574 -v409 -v3461 v3287 v2448 -v2301 v2198 -v430 -v199 -v3459 v3291 v2449 -v2305 -v1352 -v426 -v4491 -v3907 v3295 -v3220 v2465 -v1810 -v1416 v1373 -v425 -v202 v4493 -v4301 v3294 -v3221 -v1814 v1369 -v829 -v507 -v1417 -v1368 v830 -v571 -v506 -v482 -v463 -v152 -v3326 v831 v467 -v4487 -v2927 -v1836 -v1004 v847 -v514 v488 -v155 -v2931 v2181 -v1840 -v1006 -v518 -v4488 -v522 -v493 -v469 v404 -v521 -v470 v405 v4374 -v1000 -v496 v400 v4376 -v494 -v1001 v398 v1714 v4370 -v2258 v1713 -v69 v3701 -v220 -v70 v4575 v4371 v3722 v2264 -v1721 -v1346 -v532 -v330 -v221 -v65 v3718 v1725 -v1449 -v1345 -v332 v222 v4578 -v3802 -v3717 -v3649 v1729 -v1451 -v538 v238 -v63 -v3806 -v3650 v1728 v1457 -v3645 -v2267 v1453 v1341 v543 -v326 v1462 -v4277 -v3670 -v3609 v3163 -v2281 -v2185 -v807 v293 -v3672 v3159 -v811 v4271 -v3612 v3158 -v2835 v2285 v2191 v2041 -v3446 v3208 -v2283 -v1931 -v4272 -v3666 -v3448 v3207 -v2838 v2784 -v2196 v2047 -v1952 -v1573 -v3454 v1948 -v1421 -v631 -v3667 -v3450 v3215 v2790 v2199 -v1947 -v652 -v427 -v3462 -v3281 -v3219 v2197 v648 -v429 v3282 -v3223 v2468 -v2300 -v2050 -v1370 -v647 -v198 -v4492 v3283 -v3222 v2469 -v2304 v1372 -v457 v3299 -v2793 v2464 v1812 -v1619 -v456 -v423 v204 v1816 -v1623 -v4010 -v3357 -v2462 -v1366 v850 -v464 -v424 -v151 -v3361 -v1005 v851 -v508 -v481 v468 -v2929 -v1835 -v1818 -v1367 v846 v509 -v483 -v472 -v403 -v207 v157 -v2933 -v1839 -v1819 v510 v489 -v471 -v402 v844 v526 v485 v4375 -v497 v2935 -v160 v2936 v2254 v399 -v68 -v67 -v3719 -v2260 v1786 v3796 -v3721 -v1790 v1715 -v331 v4574 v3795 -v3648 v2265 v1716 v241 -v3647 v1717 -v531 v242 v4580 -v3803 -v3715 -v2268 -v1911 v1733 -v533 v237 -v64 -v3807 -v2266 -v1915 -v1452 -v539 v3808 -v3716 -v3643 -v1470 v1342 v535 -v327 v235 v3809 -v1466 -v544 -v4275 -v3671 -v3608 v3162 v2282 -v2037 -v809 v295 v2286 v2184 -v813 -v3614 v3156 -v2834 -v2780 v2186 v2043 -v1949 -v1569 v2192 -v1951 v3157 -v2840 v2786 v2188 -v2095 v2048 -v1572 -v815 -v649 -v299 -v3449 v3209 v2200 -v816 -v651 -v428 -v3617 -v3470 v3210 v2791 v2467 -v2051 -v1945 -v194 -v3466 v3211 v2466 -v2049 -v1806 -v1371 -v3465 -v3302 v3227 -v2843 -v2794 -v2302 -v1946 -v1805 -v645 -v200 v3303 -v2792 -v2306 -v4006 v3298 v1813 -v1618 -v1434 -v849 -v646 v205 -v147 -v2923 v1817 -v1622 -v848 -v458 -v4009 -v3356 v3296 -v2922 -v2463 -v2308 v1821 v459 -v208 -v153 -v3360 -v2309 -v1820 v460 -v206 -v2978 -v2930 -v1837 v529 -v476 v158 -v2982 -v2934 -v1841 v530 -v484 v2938 -v845 -v720 v525 -v505 v161 v2937 v724 v501 -v159 -v1843 -v523 v500 -v1844 -v2502 -v3720 v2253 v4570 -v2764 v2255 v1785 -v240 -v2261 -v1789 -v239 v4576 v2257 -v1736 v3797 -v2269 -v1737 v4581 v3798 -v1910 v1732 -v1467 v3799 -v1914 -v1469 -v534 v4582 -v3813 -v3644 -v3118 v1730 v552 v236 -v34 -v4583 -v3122 -v1465 v548 -v4276 -v3610 v3160 -v2830 -v2294 -v810 v740 v296 v2290 -v2036 -v1950 -v814 -v3615 -v2836 v2289 -v2091 -v2038 -v1568 -v818 -v300 -v2779 v2187 v2044 -v817 -v650 -v298 -v3618 -v3467 -v2841 -v2781 -v2326 -v2208 -v2094 v2040 v1574 -v3616 -v3469 v2787 -v2330 -v2296 v2204 -v2052 -v3301 v3230 -v2844 v2783 -v2295 v2203 -v3300 v3231 -v2842 -v2795 -v193 -v3463 -v3226 v2430 -v2303 -v1577 v1430 v195 -v2307 v1807 -v201 -v4005 -v3464 -v3224 -v2311 v1808 -v1620 -v1433 v197 -v2310 -v1831 v1809 -v1624 v209 -v146 -v4011 -v3358 -v3297 -v1959 -v1830 v1825 -v790 v528 v479 -v148 -v3362 v2924 -v1963 v527 v480 -v154 -v3751 -v2977 v2925 -v1838 -v1626 -v502 -v475 v150 -v2981 v2926 -v1842 -v1627 -v504 v162 -v4014 -v3386 v3364 v2942 -v2116 -v1846 -v719 -v473 -v3365 -v2120 -v1845 v723 -v2498 -v524 v498 v2760 -v2501 v499 -v2763 v1787 -v1735 v4569 v2256 -v1791 -v1734 v4571 v2277 v4577 v2273 -v1468 v4573 -v3816 v2272 -v1912 -v1793 v549 -v30 v4584 v3817 -v1916 -v1794 v551 -v3812 -v3117 v1731 -v33 v3121 -v1463 v547 -v3606 -v3161 -v2293 v1564 -v806 v739 v297 -v3611 -v2829 -v805 -v301 -v3607 -v2831 v2287 -v2205 -v2090 v1570 -v822 -v3619 -v3468 -v2837 -v2207 -v2039 v3229 -v2833 -v2325 -v2288 -v2096 v2060 v1575 v3228 -v2845 -v2782 -v2329 v2056 v2803 -v2426 -v2201 v2055 -v1578 -v1180 -v81 v2799 -v2297 -v1614 -v1576 -v1184 -v4001 -v3920 -v2798 v2429 -v2298 -v2202 -v2099 -v1673 -v1613 v1429 -v3924 -v3352 -v2299 v196 -v4007 -v3351 -v3225 -v2315 v1828 -v1621 -v1435 v786 -v478 -v217 v1829 -v1625 -v477 v213 -v4012 -v3747 v3359 -v1958 v1824 -v1629 -v789 v212 v3363 -v1962 -v1832 -v1628 -v503 -v149 -v4015 -v3750 -v3382 v3367 -v2979 -v2945 -v1833 v1822 -v1594 -v1438 v170 -v4013 v3366 -v2983 -v2946 -v1834 v1598 -v166 -v3385 v2941 -v2115 -v1850 -v721 -v474 -v165 -v2119 v725 -v2985 -v2939 -v2497 -v253 -v2986 -v1781 v2759 -v2503 -v1780 v727 v728 -v2765 v2274 v1788 v2276 -v1906 -v1792 -v3815 v2506 -v1905 -v1796 v4572 -v3814 -v1795 v550 -v4592 -v2768 v2270 -v1913 -v29 -v7 v4588 -v1917 -v11 v4587 -v3810 -v3119 v2271 v1918 -v35 v3123 v1919 -v1464 v545 -v2291 -v2086 -v1315 -v825 v741 v309 -v3605 -v2206 v1563 -v826 v305 -v3627 -v2590 -v2092 -v2057 v1565 -v821 v304 -v3623 -v2832 v2594 -v2059 v1571 -v3622 -v2853 -v2800 -v2327 -v2097 v2021 v1567 -v819 -v745 -v77 -v2849 v2802 -v2331 -v1579 -v4426 -v2848 -v2425 -v2100 v2053 -v1669 -v1425 -v1179 -v80 -v4430 -v2098 -v1183 -v3919 v2953 -v2796 v2431 -v2333 -v2318 v2054 v1827 -v1672 v1431 -v214 -v4000 -v3923 -v2957 -v2334 -v2319 v1826 -v1615 -v216 -v4130 -v4002 -v2797 -v2314 -v1616 -v1436 v785 -v4008 -v3353 -v2973 -v1617 -v4004 -v3746 v3354 -v2972 -v2944 -v2635 v2434 -v2312 -v1960 -v1633 -v1439 -v791 v210 -v167 -v4016 v3355 -v2943 -v2639 -v1964 -v1437 -v715 v169 -v3752 -v3381 -v3371 -v2980 -v1865 -v1853 v1823 -v1593 -v714 v211 -v2984 -v1854 v1597 -v3387 -v2988 -v2493 -v2117 -v1966 -v1849 v794 -v722 v249 -v163 -v2987 -v2121 -v1967 v726 -v3755 -v2940 v2755 v2499 -v1847 v730 -v252 -v164 v729 -v4155 -v3390 v2761 -v2504 v2123 v2275 v2124 -v1782 -v2766 v2507 -v1783 v2505 v1784 -v4589 -v4505 -v2769 v1800 -v25 -v4591 v3113 -v2767 v1907 v3112 v1908 -v31 -v6 v1909 -v10 v4585 -v3811 -v3120 -v1923 v370 -v36 v3124 -v546 -v374 -v3624 -v2292 -v1314 -v823 v742 v308 -v3626 -v2321 -v2085 -v2058 -v3019 -v2850 -v2589 -v2320 -v2087 v2017 -v746 v302 -v3023 -v2852 -v2801 v2593 -v2093 v1566 -v744 -v3620 -v2421 -v2328 -v2089 v2020 -v1587 -v820 v303 -v76 -v2332 -v2101 -v1583 -v4425 -v3621 -v2846 -v2427 -v2336 -v2317 -v1668 -v1582 -v1181 -v82 -v4429 -v2335 -v2316 -v1424 -v1185 -v215 -v4126 -v3921 v2952 -v2847 v2432 -v1674 -v1426 v781 -v3925 -v2956 -v1954 v1432 -v4129 -v3742 v2435 -v1953 -v1636 v1428 -v1187 v787 -v85 -v4003 v2433 -v1637 -v1440 -v1188 -v168 -v4024 -v3927 -v3748 -v3377 -v3374 -v2634 -v2313 -v1961 -v1861 -v1852 -v1677 -v1632 -v792 -v4020 -v3928 -v3375 -v2974 -v2638 v2111 -v1965 -v1851 -v4019 -v3753 -v3383 -v3370 -v2975 v2110 -v1969 -v1864 -v1630 -v1595 v795 -v2976 -v1968 v1599 v793 -v716 -v3756 -v3388 -v3368 -v2992 -v2118 -v717 -v613 v248 -v3754 -v2492 -v2122 v718 -v4151 -v3391 -v2494 v2126 -v1848 v1601 -v734 -v254 -v3389 v2754 v2500 v2125 v1602 -v4154 v2756 -v2664 v2496 v2762 v2508 -v4501 -v3044 v2758 -v1803 v1018 -v257 -v4590 v3048 -v2770 -v1804 -v4504 v1799 -v24 -v1926 v1797 -v26 -v8 v3114 -v1927 -v32 -v12 v4586 v3115 -v1922 v369 v28 v3116 v373 -v37 -v3625 -v1316 -v824 v743 -v306 -v2851 -v747 -v3018 v2591 v2016 -v1584 -v72 -v3022 v2595 -v2322 -v2088 -v1586 -v1175 -v2323 -v2109 v2022 -v1664 v1320 -v1174 -v78 -v3915 -v2420 v2324 -v2105 -v4427 v3981 -v3914 -v2597 -v2422 -v2340 -v2104 -v1670 -v1580 -v1182 -v83 -v4431 v3985 -v2598 -v2428 -v1186 -v4125 -v3922 v2954 v2424 -v2025 -v1675 -v1635 -v1581 -v1519 -v1190 -v86 -v3926 v2958 v2436 -v1634 -v1523 -v1427 -v1189 v780 -v84 -v4433 -v4131 -v4021 -v3930 -v3373 -v1678 -v1448 v782 -v4434 -v4023 -v3929 -v3741 -v3372 -v1955 -v1676 -v1589 -v1444 v788 -v3743 -v2960 -v2636 -v1956 -v1860 v1694 -v1588 -v1443 v784 v3749 -v3376 -v2961 -v2640 v1957 v1698 v796 -v4134 -v4017 v3745 -v3378 -v2995 v1973 -v1866 -v1631 v1596 -v609 -v244 -v3757 -v3384 -v2996 v2112 v1600 -v4248 -v4018 -v3380 -v3369 -v2991 -v2642 v2113 v1604 -v737 -v612 v250 -v4252 -v3392 -v2643 v2114 v1603 -v738 -v4150 -v2989 -v2660 v2130 -v1869 -v733 -v255 v2495 -v4156 -v2663 v2516 -v1802 -v1014 -v731 -v258 v2757 -v2512 -v1801 -v256 -v4530 -v4500 -v4451 v3043 v2778 -v2511 v1017 -v4455 v3047 -v2774 -v2 -v4506 -v4159 -v2773 -v1925 -v1380 -v934 -v1 -v1924 v1384 -v1798 -v9 -v27 -v13 -v4509 v3127 v2480 -v1920 v371 -v45 -v14 v3128 v375 v41 -v15 -v3821 v2586 v2012 v1317 v755 -v307 -v3825 -v1585 v751 -v3020 v2592 -v2106 v2018 v1321 -v750 -v4421 -v3024 v2596 -v2108 v1319 -v71 -v4420 -v2600 -v2343 v2023 -v73 -v2948 -v2599 v2344 -v1663 -v1176 -v79 -v4428 -v4121 v3980 v3556 -v3026 -v2947 -v2339 -v2102 v2026 -v1665 -v1177 -v75 -v4432 v3984 -v3916 -v3027 -v2423 v2024 -v1671 -v1178 -v87 -v4436 -v4127 -v3917 v2955 v2444 -v2337 -v2103 -v1667 -v1518 -v1445 -v1205 -v1194 -v4435 -v4022 -v3918 v2959 -v2630 v2440 -v1679 -v1522 -v1447 v1209 -v4132 -v3934 -v2963 -v2629 -v2439 -v1856 -v1063 -v2962 -v1067 v783 -v4135 -v2994 -v2637 -v1976 -v1862 v1693 -v1441 v804 -v4133 v3744 -v2993 -v2641 v1977 v1697 -v1590 v800 v3765 -v2645 v1972 -v1867 -v1591 -v1442 v799 -v736 -v608 -v3761 -v3379 -v2644 v1592 -v735 -v243 -v4247 -v4146 -v3760 -v3400 v2133 -v1970 -v1870 v1608 -v614 -v245 -v4251 -v3396 v2134 -v1868 v251 -v4152 -v3395 -v2990 -v2659 v2513 -v2129 v247 v2515 -v259 -v4526 -v4496 -v4157 v2775 -v2665 -v2127 -v1013 -v732 v617 v2777 -v4529 -v4502 -v4450 -v4160 -v3242 v3045 -v2566 -v2509 v1019 -v930 -v4454 -v4158 v3049 v2570 -v4507 v3097 -v2771 -v2668 -v2510 -v1379 -v933 v1383 -v365 -v3 -v4510 -v3126 v3051 -v2772 v2476 -v1022 -v364 -v42 -v4 -v4508 -v3125 -v3052 -v44 -v5 v2479 -v1921 v372 v181 -v19 v376 -v40 -v3820 -v3015 v1318 v754 -v3824 v2585 -v2107 v2011 v1322 -v3021 v2587 -v2342 v2013 -v761 -v748 -v3025 v2588 -v2341 v2019 -v765 v3552 -v3029 -v2604 v2015 -v749 -v4422 -v3028 v2027 -v74 -v4423 v3982 v3555 v2882 -v2441 -v1197 -v95 -v4424 -v4120 v3986 -v2949 -v2443 -v1666 -v1446 -v1198 -v91 -v4440 -v4122 -v3937 v2950 -v2338 -v1687 -v1520 -v1204 -v1193 v441 -v90 -v4128 -v3938 v2951 -v1683 -v1524 v1208 -v4124 v3988 -v3933 -v2967 -v2437 -v1975 -v1682 -v1191 -v1062 -v801 -v4136 v3989 -v2631 -v1974 -v1855 -v1066 -v803 -v3931 -v3762 -v2632 -v2438 -v1857 v1695 -v1526 v604 v3764 -v2633 -v1863 v1699 -v1527 -v3397 -v2649 v2132 -v1859 -v1611 v797 -v610 -v3399 v2131 -v1871 -v1612 -v4249 -v3758 -v2655 -v1971 v1701 -v1607 v798 -v615 -v4253 -v4145 v2514 v1702 -v246 -v4147 -v3759 -v3393 -v2661 -v1605 -v1009 v618 v267 -v4153 -v3039 -v2776 v616 -v263 -v4525 -v4255 -v4149 -v3394 v3238 -v3038 -v2666 -v2128 v1015 -v262 -v4495 -v4256 -v4161 -v4531 -v4497 -v4452 v3241 -v3093 v3046 -v2669 -v2565 v1020 -v929 -v4503 -v4456 v3050 -v2667 v2569 -v4499 v3096 v3054 -v1481 -v1381 -v1023 -v935 -v4511 v3053 v1385 -v1021 -v43 -v4534 v4458 v2475 -v177 -v22 v4459 -v366 -v23 v2481 v1387 -v938 -v367 v180 -v18 v1388 v368 -v38 -v3822 -v1330 v752 v3826 -v3014 -v1326 -v3016 -v2607 -v1325 v760 v3976 -v3017 -v2608 v2014 -v764 v3975 -v3828 v3551 -v3033 v2878 -v2603 -v2035 -v1196 -v92 -v3829 -v2442 -v2031 -v1514 -v1195 -v94 -v4443 v3983 -v3936 v3557 v2881 -v2601 -v2030 -v1684 -v1513 -v437 -v4444 v3987 -v3935 -v1686 -v4439 v3991 v2970 v1521 -v1206 v440 -v88 -v4123 v3990 v2971 -v1689 v1525 v1210 -v802 -v4437 -v4144 -v3560 -v2966 -v1688 -v1680 -v1529 -v1192 -v1064 -v89 -v4140 -v3763 -v1528 -v1068 -v4139 -v3932 -v2964 -v2652 v1696 -v1681 -v1610 v1212 v4243 -v3398 -v2653 -v1858 v1700 -v1609 -v1213 v603 v4242 -v2648 -v1879 v1704 -v1070 v605 -v1875 v1703 -v1071 -v611 -v4250 -v2646 -v1874 v607 -v264 -v4254 -v2654 v619 -v266 -v4521 v4258 -v4101 -v2656 -v1606 -v4446 v4257 -v4148 -v4105 -v2662 -v1008 v4527 -v4445 -v4169 v3237 v2658 -v1010 -v925 -v260 -v4165 -v3040 -v2670 -v1375 v1016 v4532 -v4453 -v4164 -v3407 v3243 -v3092 -v3041 -v2567 -v1477 -v1374 v1012 -v931 -v261 -v4498 -v4457 -v3411 v3042 v2571 -v1024 -v4535 -v4519 v4461 -v4310 -v3481 v3098 v3058 -v2471 -v1480 -v1382 -v936 -v21 -v4533 -v4515 v4460 -v4314 v1386 -v20 -v4514 -v3246 -v2573 v2477 v1390 v939 -v176 -v2574 v1389 -v937 -v3101 v2482 -v379 v182 -v16 -v380 -v39 -v3823 -v2606 -v1329 v753 v3827 -v2605 v3831 -v3547 -v3172 -v3036 -v2032 -v1323 v762 -v3830 -v3037 -v2034 -v766 -v93 -v4442 v3553 -v3032 v2877 -v1324 -v4441 v3977 -v1685 -v1200 v3978 v3558 -v3030 -v2969 v2883 -v2602 -v2028 -v1765 -v1544 -v1199 v768 -v436 v3979 v2968 -v1548 v1515 -v1058 v769 -v4141 v3995 -v3561 -v2029 v1516 -v1207 -v1057 v442 -v4143 -v3559 v1517 v1211 -v4438 -v2886 -v2651 v1533 v1215 -v1065 -v2650 -v1690 v1214 -v1069 -v4137 -v2965 -v1876 -v1691 -v1073 v445 -v1878 v1692 -v1072 -v4138 v1708 -v675 v4244 -v679 v606 -v265 v4245 v4051 -v2647 -v1872 v627 v4246 -v4055 v623 v4262 -v4166 -v4100 v3233 -v2215 -v1873 v622 -v4520 -v4168 -v4104 -v2657 -v2561 -v2219 v4522 v3239 v3088 v2678 -v2560 v4528 -v4447 v2674 -v1011 -v924 v4524 -v4516 -v4448 -v4162 -v3477 -v3406 v3244 -v3094 -v3061 v2673 v2568 -v1476 -v1032 -v926 -v4536 -v4518 v4449 -v3410 -v3062 v2572 -v1376 v1028 -v932 v4465 -v4309 -v4163 -v3480 -v3247 v3099 -v3057 v2576 -v1482 -v1377 v1027 v928 -v172 -v4313 -v3245 v2575 -v2470 v1378 v940 -v4512 -v3875 -v3102 -v3055 -v2472 v1394 -v378 -v178 -v3100 v2478 -v377 -v4513 -v3339 -v3003 v2474 -v1485 v183 -v17 -v3007 v2483 v3819 v3168 -v3035 -v1327 v757 v3818 -v3034 -v2033 v3835 -v3171 v2873 v763 -v3546 v767 -v3548 v2879 -v1761 v771 -v432 v3554 v770 v3998 v3550 -v3031 v2884 -v1764 -v1543 -v438 -v4142 v3999 -v3562 -v1547 -v1201 v3994 -v2887 v1536 -v1202 -v909 v443 -v2885 v1537 v1203 -v1059 v3992 v1532 v1219 -v1060 v446 -v1877 -v1061 v444 v1711 v1530 -v1077 v1712 v1707 -v674 v624 -v678 v626 v4265 v4050 v1705 v4266 -v4167 -v4054 v4261 -v4102 v2675 -v2214 v620 -v4106 v3232 v2677 -v2218 v4259 v3234 -v3060 -v1472 -v1029 v621 v4523 -v4517 v3240 v3087 -v3059 -v2562 -v1031 -v4544 v4468 -v4201 -v4108 -v3476 -v3408 v3236 v3089 v2671 -v2563 -v1478 v4540 v4469 -v4205 -v4109 -v3412 -v3248 -v3095 v2564 -v927 -v4539 v4464 v4311 -v3871 -v3482 v3091 v2672 -v2580 -v1483 v1397 v1025 v948 -v4315 -v3103 v1398 -v944 -v171 v4462 -v3874 v3414 -v3335 -v3056 -v2071 -v1486 v1393 v1026 -v943 -v173 v3415 -v2473 -v1484 -v179 v4317 -v3485 -v3338 -v3002 v2491 v1391 v175 v4318 -v3006 v2487 -v184 v3838 -v3260 v3167 -v1739 -v1328 v3839 -v3264 v756 v3834 v3173 v758 v2872 v759 v3997 v3832 v2874 -v1760 v775 v3996 -v3549 v2880 -v431 -v3570 -v3176 v2876 -v1766 -v1545 v1535 -v905 v433 -v3566 -v2888 -v1549 v1534 -v439 -v3565 -v1222 -v908 v435 -v1223 v447 v3993 -v2351 v1769 v1710 -v1551 v1218 -v1080 v2355 v1709 -v1552 -v1081 v1531 v1216 -v1076 v625 v4264 -v1074 -v676 v4263 v4096 -v680 v4095 v4052 v1706 -v4056 v2676 -v4103 -v2216 -v682 -v4107 v3402 -v2220 -v1030 -v683 -v4541 v4467 v4260 -v4111 -v4058 -v3472 v3401 -v4543 v4466 -v4305 -v4110 -v4059 v3235 -v1471 -v4304 -v4200 -v3478 -v3409 -v3256 -v2583 -v2222 -v1473 v1396 v945 -v4204 -v3413 -v3252 v3090 -v2584 -v2223 -v1479 v1395 v947 -v4537 v4312 -v3870 -v3483 v3417 -v3251 -v3111 -v2579 -v2067 -v1475 -v4316 v3416 -v3107 -v1487 -v4538 v4463 v4320 -v3876 -v3486 -v3334 -v3106 -v2577 v2488 -v2070 -v941 v4319 -v3484 v2490 -v174 -v3340 -v3004 v1392 -v942 -v192 -v3008 v2486 -v188 v3836 -v3259 v3169 -v1738 -v3263 v3174 v1756 -v778 -v1539 -v779 v3833 -v3567 -v3177 -v1762 -v1538 v774 -v3569 -v3175 v2875 -v2907 -v2896 -v1767 -v1546 -v1221 -v904 v772 v2892 -v1550 -v1220 v434 -v3563 v2891 v1770 -v1554 -v1079 -v910 -v455 v1768 -v1553 -v1078 -v451 v4384 -v3564 -v2350 -v450 v4388 v2354 -v670 v1217 -v913 -v669 -v4046 v4045 -v2380 -v1075 -v677 -v2210 -v681 v4053 v2545 -v2209 -v685 v4097 -v4057 -v684 v4098 -v4061 -v2217 -v1299 -v4542 v4099 -v4060 -v2221 -v4115 -v3253 -v2582 -v2225 -v3471 v3403 -v3255 -v2581 -v2224 v946 v4202 -v3866 -v3473 v3404 -v3108 -v131 -v4306 v4206 -v3479 v3405 -v3110 -v1474 -v4307 -v3872 v3475 -v3421 -v3330 -v3249 -v2066 -v1495 v102 v4308 -v3487 -v2998 v2489 -v1491 -v106 v4324 -v4208 -v3877 -v3336 -v3250 -v3104 -v2997 -v2578 -v2072 -v1490 -v189 -v4209 -v191 -v3878 -v3341 -v3105 -v3005 v1502 -v3879 -v3009 v2484 v1506 -v187 v4404 v3837 -v3261 v3165 -v1740 -v964 -v777 -v3265 v3170 v968 -v776 v3166 -v3568 -v3178 v1755 -v3502 -v3267 v2903 -v2893 v1757 -v1744 -v900 -v884 v3506 -v3268 -v2895 -v1763 -v1540 -v2906 v2739 v1759 -v1541 -v906 v773 -v452 v1771 -v1542 -v454 v2889 -v1558 -v911 v4383 v2890 -v2352 -v914 -v448 v4387 v2356 -v912 -v2376 -v449 -v671 v2541 -v2379 -v2358 -v672 v4047 -v2359 -v673 v4048 v2544 -v1295 -v689 v4049 -v2211 v4118 v4065 -v2212 -v1298 v4196 v4119 -v3254 -v2213 v4195 -v4114 -v2229 v127 -v3109 v4203 -v4112 -v3424 v2062 -v1492 -v130 v4207 -v3865 -v3474 -v3425 -v1494 -v4327 -v4211 -v3867 -v3495 -v3420 v2068 v101 -v4328 -v4210 -v3873 v3491 -v3329 -v190 -v105 v4323 -v3869 v3490 -v3418 -v3331 v3073 -v2073 -v1488 -v3880 -v3337 -v2999 v4321 -v3333 -v3000 -v2074 v1501 -v1489 -v3342 -v3001 v2485 -v2075 v1505 -v185 v4403 v3262 -v1741 -v963 -v3266 v3164 v967 -v3270 v3186 -v1745 v880 -v3269 -v3182 -v2894 -v1743 v3501 -v3181 v2902 -v2735 -v883 v3505 v1758 -v899 -v453 -v2908 v2738 v2401 -v1779 -v1561 -v901 -v2405 -v2346 -v1775 -v1562 -v907 v2345 -v1774 -v1557 -v903 -v588 -v915 v4385 v2911 -v2810 -v2353 -v1555 v4389 v2814 v2357 -v2375 v2361 -v1648 v2360 -v4391 v2540 v2381 -v692 -v4392 -v693 v4117 v4068 v2546 -v1294 v1270 -v688 -v278 v4116 v4069 -v1274 v4064 v2710 -v2384 -v2232 -v1300 -v686 -v2714 -v2233 v4062 -v3423 -v2549 -v2228 v1155 v126 v4197 -v3422 -v1493 -v1159 -v4326 v4198 -v4113 -v4080 -v3492 -v2226 -v1303 -v132 -v4325 v4199 -v3494 v2061 -v4215 v3069 v2063 v103 -v3868 v2069 -v107 -v3888 v3488 -v3419 v3072 v2065 -v135 -v3884 -v3332 v2076 v4322 -v3883 -v3489 -v3350 -v3012 v1503 v109 -v3346 -v3013 v1507 -v186 v110 v4405 -v3258 v3183 -v1742 -v965 v3257 v3185 -v1746 v969 -v3274 v2898 -v1038 v879 -v1042 -v4409 v3503 -v3179 v2904 -v2734 -v1776 -v1560 -v971 -v885 v3507 -v1778 -v1559 -v972 -v4176 -v3180 -v2909 v2740 v2400 -v584 v4379 -v4180 -v2404 -v902 v4378 v3509 v2912 -v1772 -v923 -v888 -v587 v3510 v2910 v2347 -v919 v4386 -v2809 -v2743 v2371 v2348 -v1773 -v1644 -v1556 -v918 v4390 v2813 v2349 -v4394 v2536 -v2377 v2365 -v1647 -v691 -v4393 -v690 -v4067 -v3846 v2542 v2382 -v1290 -v274 v4066 -v3850 v3531 v2547 -v2385 -v2231 -v1296 v1269 -v277 -v2383 -v2230 -v1273 v2709 -v2550 -v1301 -v687 v122 -v2713 -v2548 -v4076 -v4063 -v1304 v1154 v128 -v3493 -v1302 -v1158 v97 -v4218 -v4079 -v2227 -v133 v96 -v4219 -v4214 -v3885 v3068 -v1886 -v136 v104 -v3887 v2064 -v1890 -v1497 -v134 -v108 -v4212 -v3347 v3074 -v3011 v2084 -v1496 v112 -v3349 -v3010 v2080 v111 -v3881 v2079 v1504 -v3345 v1508 v4406 v3277 -v3184 -v1754 v966 -v950 v875 -v3497 v3278 -v1750 v970 -v4410 -v3946 -v3496 -v3273 -v2730 -v1749 -v1037 -v974 v881 -v4408 v2897 -v1777 -v1041 -v973 v3504 -v3271 v2899 -v2736 -v886 v3508 v2905 -v4175 v3512 v2901 v2741 v2402 -v920 -v889 -v583 -v4179 v3511 v2913 -v2406 -v922 -v887 -v2744 -v589 v4380 -v2742 v4381 -v2811 -v2408 -v2368 -v1643 -v916 v4382 v2815 -v2409 v2370 -v2369 -v4398 v2372 v2364 -v2145 -v1649 -v917 -v592 v2535 -v2378 -v3845 -v3527 v2817 v2537 v2374 v2362 -v273 v3849 -v2818 v2543 -v2386 -v1289 v3530 -v2685 v2539 -v1652 -v1291 v1271 -v279 -v2689 -v2551 -v1297 -v1275 -v4555 v2711 -v1293 v2715 -v1305 v121 -v4217 -v4075 -v1277 v1156 -v282 v123 -v4216 -v1278 v1160 v129 -v4081 -v3064 -v2717 -v1130 v125 -v3886 -v2718 -v1134 -v137 v98 v3070 -v2081 v1885 -v1162 v99 -v3348 v2083 -v1889 -v1163 v100 -v4213 -v4084 -v3589 v3075 v116 -v3593 v1498 -v3882 v3076 -v2077 v1499 -v3343 v3077 v1500 v4407 -v3942 v3275 -v1753 v962 -v949 v4411 v961 v874 -v3945 -v1747 -v1039 v978 v876 -v3498 -v2729 v2396 -v1043 v882 -v3499 -v3272 -v2731 v2395 -v1748 v878 -v579 v3500 v2900 -v2737 -v921 -v890 -v4177 v3516 v2921 v2733 v2403 -v1045 -v585 -v4181 v2917 -v2805 -v2745 -v2407 -v1046 v2916 -v2804 -v2411 -v2367 -v1639 -v590 -v2410 -v2366 -v4401 -v4183 -v2812 v2141 -v1645 v704 -v593 -v4402 -v4184 v2816 -v591 -v4397 v2820 -v2144 -v1650 -v269 v2819 v2373 v1265 -v4395 -v3847 -v3526 v2394 v2363 -v1653 v1264 -v275 v3851 v2705 v2538 v2390 -v1651 -v4551 v3532 v2704 -v2684 -v2559 v2389 v1272 -v280 -v2688 v2555 -v1292 -v1276 -v1150 -v4554 -v4071 -v3853 v3436 v2712 v2554 -v1313 -v1280 -v1149 -v283 -v3854 v2716 -v1309 -v1279 -v281 -v4077 v3535 -v3197 -v2720 -v1308 v1157 -v2719 v1161 v124 -v4082 -v1165 -v1129 v145 -v3063 -v2082 -v1164 -v1133 v141 -v4085 v3065 v1887 v140 v119 -v4083 v3071 v1891 v120 -v3588 v3067 v2244 v115 -v3592 v3078 -v2078 -v1893 v1511 v113 -v3344 -v1894 v1512 -v4419 -v3941 -v3276 -v1751 v1034 v981 -v951 -v4415 v982 -v4594 -v4414 -v3947 -v1040 v977 -v4598 -v4171 -v1044 v877 -v4170 -v3519 -v2918 v1048 -v975 v954 v898 -v3520 v2920 -v2732 v2397 v1047 -v894 -v578 -v4178 v3950 v3515 v2753 v2398 -v893 -v580 -v4182 v2749 v2399 -v586 -v4400 -v4186 -v3513 v2914 v2748 v2415 -v700 -v582 -v4399 -v4185 -v2806 -v1638 -v594 -v3963 v2915 -v2807 v2140 -v1640 v703 -v3967 -v3841 v2808 -v1646 -v3840 v3522 v2824 v2391 -v2146 -v1642 v2393 -v1654 -v268 -v4396 -v3848 -v3528 -v2556 -v357 -v270 v3852 -v2558 v1266 -v276 -v4550 -v3856 v3533 -v3432 -v2686 v2387 -v2149 -v1310 v1267 v272 -v3855 v2706 -v2690 -v1312 v1268 v284 -v4556 v3536 v3435 -v3193 v2707 v2552 -v2388 v1284 -v4070 v3534 v2708 -v1151 -v4614 -v4072 -v3196 v2724 -v2692 v2553 -v1306 -v1252 v1152 v142 -v4078 -v2693 -v1881 -v1256 v1153 v144 v4559 v4074 -v2523 -v1880 -v1307 -v1169 -v1131 v118 -v4086 -v2527 -v1135 v117 -v2860 -v2240 v1888 v138 v3066 -v2864 v1892 -v3590 -v3086 v2243 -v1896 v1510 -v1137 v139 -v3594 v3082 -v1895 v1509 -v1138 -v3775 v3081 v114 -v4418 -v3943 -v1752 v979 -v952 v1033 -v4593 -v4412 -v3948 -v3518 v1035 v955 v895 -v4597 -v3517 -v2919 v1036 v953 v897 -v4413 v3951 -v2750 v1052 -v976 -v4172 v3949 v2752 -v4173 v2418 -v891 v4174 v2419 -v581 v4190 -v3514 v2746 v2414 v2136 -v892 -v699 -v602 -v598 -v3962 -v2827 -v2747 v2412 v2142 v705 -v597 -v3966 -v2828 v2392 -v1641 -v2823 -v2147 -v1662 -v353 -v3842 v3521 -v2680 -v2557 -v1658 v4546 -v3843 v3523 -v2821 -v2679 -v2150 -v1657 v708 -v356 v3844 -v3529 -v2148 -v1311 -v271 -v4552 v3860 v3525 -v3431 -v2687 -v1287 v292 v3537 -v2691 v1288 v288 v4610 -v4557 v3437 -v3192 -v2727 -v2695 -v1283 -v287 -v2728 -v2694 -v1125 v143 -v4613 v4560 v3198 -v2723 -v1281 -v1251 -v1172 -v1124 v4558 -v4073 -v1255 -v1173 v4094 -v3440 -v2721 -v2522 -v1168 -v1132 -v4090 v3584 -v2526 -v1882 -v1136 -v4089 v3583 -v3201 -v3083 -v2859 -v2239 -v1883 -v1166 -v1140 -v3085 -v2863 v1884 -v1139 -v3771 v3591 v2245 -v1900 -v3595 -v3774 -v3596 v3079 -v3597 -v4416 v3940 -v980 -v3944 v956 v896 -v4595 v1055 -v4599 v3952 -v2751 v1056 v2417 v1051 v2416 v4601 v4193 v1049 v695 -v599 -v4602 v4194 -v601 v4189 -v2826 -v701 -v2825 v2135 v4187 -v3964 v2413 v2137 -v1659 v706 -v595 -v3968 v2143 -v1661 v2139 v709 -v596 -v352 -v2151 v707 -v3970 v3863 -v3427 -v2822 -v1655 -v1286 -v358 v289 v4545 -v3971 v3864 v3524 -v2681 -v1285 v291 v4547 -v3859 v3545 -v3433 v3188 -v2726 -v2682 -v1656 -v4553 -v3541 -v2725 v2683 v4609 v4549 -v3857 -v3540 v3438 -v3194 v2699 -v1171 -v361 -v285 v4561 -v1170 -v4615 -v4091 -v3441 v3199 -v1282 -v1253 -v286 -v4093 -v3439 -v1257 -v1126 -v3202 -v2722 -v2524 -v2235 v1127 -v3200 -v3084 -v2528 v1128 -v4618 -v4087 -v2861 v2241 v1903 v1259 -v1167 v1144 v3585 -v2865 v1904 -v1260 -v4088 v3770 v3586 -v2530 v2246 -v1899 v3587 -v2531 -v3776 v3600 -v3080 v2867 v2247 -v1897 v2868 v2248 -v4417 -v1054 v3939 v1053 v960 -v4596 v959 -v4600 -v3956 v4604 v4192 -v3955 v4603 v4191 -v600 v1050 -v3958 v694 -v3957 v696 -v1660 -v702 v4188 -v3#### 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 0.98 0.93 2/54 4539
Raw data (stat): 4539 (runsolver) R 4538 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481964360 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99976 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 11768 0 0 0 971 27 0 0 25 0 1 0 481964360 50970624 10363 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12444 10363 603 41 0 12403 0
vsize: 49776
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 11824 0 0 0 1971 27 0 0 25 0 1 0 481964360 51240960 10419 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12510 10419 603 41 0 12469 0
vsize: 50040
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 11874 0 0 0 2971 28 0 0 25 0 1 0 481964360 51376128 10469 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12543 10469 603 41 0 12502 0
vsize: 50172
[startup+40.0018 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 11926 0 0 0 3970 28 0 0 25 0 1 0 481964360 51646464 10521 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12609 10521 603 41 0 12568 0
vsize: 50436
[startup+50.003 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 11990 0 0 0 4970 29 0 0 25 0 1 0 481964360 51929088 10585 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12678 10585 603 41 0 12637 0
vsize: 50712
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 12056 0 0 0 5969 29 0 0 25 0 1 0 481964360 52199424 10651 4294967295 134512640 134672761 3221224544 3221223680 134560675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12744 10651 603 41 0 12703 0
vsize: 50976
[startup+70.0029 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 12123 0 0 0 6968 30 0 0 25 0 1 0 481964360 52469760 10718 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12810 10718 603 41 0 12769 0
vsize: 51240
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 12208 0 0 0 7968 31 0 0 25 0 1 0 481964360 52740096 10803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12876 10803 603 41 0 12835 0
vsize: 51504
[startup+90.0048 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 12449 0 0 0 8966 32 0 0 25 0 1 0 481964360 53813248 11044 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13138 11044 603 41 0 13097 0
vsize: 52552
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 12556 0 0 0 9966 33 0 0 25 0 1 0 481964360 54218752 11151 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13237 11151 603 41 0 13196 0
vsize: 52948
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 12659 0 0 0 10966 33 0 0 25 0 1 0 481964360 54620160 11254 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13335 11254 603 41 0 13294 0
vsize: 53340
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 12714 0 0 0 11965 34 0 0 25 0 1 0 481964360 54886400 11309 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13400 11309 603 41 0 13359 0
vsize: 53600
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 12964 0 0 0 12964 35 0 0 25 0 1 0 481964360 55603200 11486 4294967295 134512640 134672761 3221224544 3221223668 134566054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13575 11486 603 41 0 13534 0
vsize: 54300
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 12982 0 0 0 13964 35 0 0 25 0 1 0 481964360 55603200 11504 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13575 11504 603 41 0 13534 0
vsize: 54300
[startup+150.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 13044 0 0 0 14964 36 0 0 25 0 1 0 481964360 55738368 11566 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13608 11566 603 41 0 13567 0
vsize: 54432
[startup+160.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 13485 0 0 0 15962 38 0 0 25 0 1 0 481964360 56033280 11641 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13680 11641 603 41 0 13639 0
vsize: 54720
[startup+170.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 13533 0 0 0 16962 38 0 0 25 0 1 0 481964360 56303616 11689 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13746 11689 603 41 0 13705 0
vsize: 54984
[startup+180.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 13616 0 0 0 17961 38 0 0 25 0 1 0 481964360 56836096 11772 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13876 11772 603 41 0 13835 0
vsize: 55504
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 13760 0 0 0 18960 39 0 0 25 0 1 0 481964360 57376768 11916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14008 11916 603 41 0 13967 0
vsize: 56032
[startup+200.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 13877 0 0 0 19960 40 0 0 25 0 1 0 481964360 57917440 12033 4294967295 134512640 134672761 3221224544 3221223668 134566142 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14140 12033 603 41 0 14099 0
vsize: 56560
[startup+210.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 14401 0 0 0 20958 42 0 0 25 0 1 0 481964360 60067840 12557 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14665 12557 603 41 0 14624 0
vsize: 58660
[startup+220.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 14763 0 0 0 21956 44 0 0 25 0 1 0 481964360 61542400 12919 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15025 12919 603 41 0 14984 0
vsize: 60100
[startup+230.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15398 0 0 0 22953 47 0 0 25 0 1 0 481964360 64106496 13554 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15651 13554 603 41 0 15610 0
vsize: 62604
[startup+240.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15608 0 0 0 23953 48 0 0 25 0 1 0 481964360 64917504 13764 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15849 13764 603 41 0 15808 0
vsize: 63396
[startup+250.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15699 0 0 0 24952 48 0 0 25 0 1 0 481964360 65187840 13855 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15915 13855 603 41 0 15874 0
vsize: 63660
[startup+260.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 25951 49 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+270.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 26951 50 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+280.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 27950 51 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+290.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 28950 51 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+300.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 29949 51 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+310.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 30949 52 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+320.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 31949 52 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+330.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 32948 52 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223696 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+340.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 33948 53 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+350.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 34948 53 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+360.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 35948 53 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+370.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 36948 54 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+380.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 37947 54 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+390.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 15955 0 0 0 38947 55 0 0 25 0 1 0 481964360 65441792 13923 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15977 13923 603 41 0 15936 0
vsize: 63908
[startup+400.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 16114 0 0 0 39946 56 0 0 25 0 1 0 481964360 66113536 14082 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16141 14082 603 41 0 16100 0
vsize: 64564
[startup+410.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 16467 0 0 0 40945 57 0 0 25 0 1 0 481964360 67588096 14435 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16501 14435 603 41 0 16460 0
vsize: 66004
[startup+420.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 17041 0 0 0 41943 59 0 0 25 0 1 0 481964360 70004736 15009 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17091 15009 603 41 0 17050 0
vsize: 68364
[startup+430.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 17567 0 0 0 42941 61 0 0 25 0 1 0 481964360 72015872 15535 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17582 15535 603 41 0 17541 0
vsize: 70328
[startup+440.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 17989 0 0 0 43939 63 0 0 25 0 1 0 481964360 73756672 15957 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18007 15957 603 41 0 17966 0
vsize: 72028
[startup+450.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 18171 0 0 0 44938 64 0 0 25 0 1 0 481964360 74567680 16139 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18205 16139 603 41 0 18164 0
vsize: 72820
[startup+460.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 18330 0 0 0 45938 64 0 0 25 0 1 0 481964360 75632640 16298 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18465 16298 603 41 0 18424 0
vsize: 73860
[startup+470.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 18763 0 0 0 46937 66 0 0 25 0 1 0 481964360 77377536 16731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18891 16731 603 41 0 18850 0
vsize: 75564
[startup+480.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19303 0 0 0 47935 67 0 0 25 0 1 0 481964360 79282176 17151 4294967295 134512640 134672761 3221224544 3221222204 134544737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19356 17151 603 41 0 19315 0
vsize: 77424
[startup+490.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 48935 68 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+500.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 49935 68 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+510.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 50934 68 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+520.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 51934 69 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+530.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 52934 69 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+540.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 53933 70 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+550.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 54933 70 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+560.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 55933 70 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+570.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 56933 71 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+580.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 57932 71 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+590.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 58932 71 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+600.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 59932 71 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+610.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 60932 72 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+620.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 61932 72 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+630.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 62931 73 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+640.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 63930 73 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+650.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 64930 74 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+660.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 65930 74 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+670.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 66929 75 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+680.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 67929 75 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+690.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 68928 76 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+700.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 69928 76 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223744 134557915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+710.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19315 0 0 0 70927 77 0 0 25 0 1 0 481964360 78888960 17116 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19260 17116 603 41 0 19219 0
vsize: 77040
[startup+720.039 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 19992 0 0 0 71926 79 0 0 25 0 1 0 481964360 81707008 17793 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 17793 603 41 0 19907 0
vsize: 79792
[startup+730.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 20804 0 0 0 72924 81 0 0 25 0 1 0 481964360 85069824 18605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20769 18605 603 41 0 20728 0
vsize: 83076
[startup+740.039 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 21776 0 0 0 73921 84 0 0 25 0 1 0 481964360 88981504 19577 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21724 19577 603 41 0 21683 0
vsize: 86896
[startup+750.039 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 22205 0 0 0 74920 85 0 0 25 0 1 0 481964360 90726400 20006 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22150 20006 603 41 0 22109 0
vsize: 88600
[startup+760.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 22433 0 0 0 75919 86 0 0 25 0 1 0 481964360 91672576 20234 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22381 20234 603 41 0 22340 0
vsize: 89524
[startup+770.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 22862 0 0 0 76917 88 0 0 25 0 1 0 481964360 93290496 20663 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22776 20663 603 41 0 22735 0
vsize: 91104
[startup+780.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 23093 0 0 0 77916 89 0 0 25 0 1 0 481964360 94232576 20894 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23006 20894 603 41 0 22965 0
vsize: 92024
[startup+790.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 23209 0 0 0 78915 90 0 0 25 0 1 0 481964360 94773248 21010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23138 21010 603 41 0 23097 0
vsize: 92552
[startup+800.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 23372 0 0 0 79915 90 0 0 25 0 1 0 481964360 95313920 21173 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23270 21173 603 41 0 23229 0
vsize: 93080
[startup+810.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 23626 0 0 0 80914 92 0 0 25 0 1 0 481964360 96391168 21427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23533 21427 603 41 0 23492 0
vsize: 94132
[startup+820.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 23736 0 0 0 81913 92 0 0 25 0 1 0 481964360 96788480 21537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23630 21537 603 41 0 23589 0
vsize: 94520
[startup+830.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 23992 0 0 0 82912 93 0 0 25 0 1 0 481964360 97869824 21793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23894 21793 603 41 0 23853 0
vsize: 95576
[startup+840.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 24180 0 0 0 83911 94 0 0 25 0 1 0 481964360 98545664 21981 4294967295 134512640 134672761 3221224544 3221223744 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24059 21981 603 41 0 24018 0
vsize: 96236
[startup+850.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 24300 0 0 0 84910 96 0 0 25 0 1 0 481964360 99082240 22101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24190 22101 603 41 0 24149 0
vsize: 96760
[startup+860.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 24458 0 0 0 85909 97 0 0 25 0 1 0 481964360 99622912 22259 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24322 22259 603 41 0 24281 0
vsize: 97288
[startup+870.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 24650 0 0 0 86908 97 0 0 25 0 1 0 481964360 100425728 22451 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24518 22451 603 41 0 24477 0
vsize: 98072
[startup+880.045 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 24731 0 0 0 87907 98 0 0 25 0 1 0 481964360 100831232 22532 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24617 22532 603 41 0 24576 0
vsize: 98468
[startup+890.044 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 24803 0 0 0 88907 99 0 0 25 0 1 0 481964360 101101568 22604 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24683 22604 603 41 0 24642 0
vsize: 98732
[startup+900.045 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 25178 0 0 0 89906 100 0 0 25 0 1 0 481964360 102572032 22979 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25042 22979 603 41 0 25001 0
vsize: 100168
[startup+910.045 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 25843 0 0 0 90904 102 0 0 25 0 1 0 481964360 105254912 23644 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25697 23644 603 41 0 25656 0
vsize: 102788
[startup+920.045 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 26463 0 0 0 91902 104 0 0 25 0 1 0 481964360 107806720 24264 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26320 24264 603 41 0 26279 0
vsize: 105280
[startup+930.047 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 27020 0 0 0 92901 105 0 0 25 0 1 0 481964360 110100480 24821 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26880 24821 603 41 0 26839 0
vsize: 107520
[startup+940.046 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 27532 0 0 0 93899 107 0 0 25 0 1 0 481964360 112123904 25333 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27374 25333 603 41 0 27333 0
vsize: 109496
[startup+950.046 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 28050 0 0 0 94897 109 0 0 25 0 1 0 481964360 114286592 25851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27902 25851 603 41 0 27861 0
vsize: 111608
[startup+960.047 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 28535 0 0 0 95896 110 0 0 25 0 1 0 481964360 116310016 26336 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28396 26336 603 41 0 28355 0
vsize: 113584
[startup+970.048 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 29011 0 0 0 96895 112 0 0 25 0 1 0 481964360 119242752 26812 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29112 26812 603 41 0 29071 0
vsize: 116448
[startup+980.048 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 29445 0 0 0 97894 113 0 0 25 0 1 0 481964360 120995840 27246 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29540 27246 603 41 0 29499 0
vsize: 118160
[startup+990.048 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 29895 0 0 0 98892 115 0 0 25 0 1 0 481964360 122875904 27696 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29999 27696 603 41 0 29958 0
vsize: 119996
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 30353 0 0 0 99891 116 0 0 25 0 1 0 481964360 124760064 28154 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30459 28154 603 41 0 30418 0
vsize: 121836
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 30768 0 0 0 100889 118 0 0 25 0 1 0 481964360 126509056 28569 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30886 28569 603 41 0 30845 0
vsize: 123544
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 31165 0 0 0 101887 120 0 0 25 0 1 0 481964360 128122880 28966 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31280 28966 603 41 0 31239 0
vsize: 125120
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 31553 0 0 0 102886 121 0 0 25 0 1 0 481964360 129609728 29354 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31643 29354 603 41 0 31602 0
vsize: 126572
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 31971 0 0 0 103885 123 0 0 25 0 1 0 481964360 131366912 29772 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32072 29772 603 41 0 32031 0
vsize: 128288
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 32365 0 0 0 104883 125 0 0 25 0 1 0 481964360 132984832 30166 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32467 30166 603 41 0 32426 0
vsize: 129868
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 32743 0 0 0 105882 126 0 0 25 0 1 0 481964360 134590464 30544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32859 30544 603 41 0 32818 0
vsize: 131436
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 33163 0 0 0 106881 127 0 0 25 0 1 0 481964360 136200192 30964 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 30964 603 41 0 33211 0
vsize: 133008
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 33597 0 0 0 107880 128 0 0 25 0 1 0 481964360 137961472 31398 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33682 31398 603 41 0 33641 0
vsize: 134728
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 34005 0 0 0 108879 129 0 0 25 0 1 0 481964360 139710464 31806 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34109 31806 603 41 0 34068 0
vsize: 136436
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 34360 0 0 0 109877 131 0 0 25 0 1 0 481964360 141189120 32161 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34470 32161 603 41 0 34429 0
vsize: 137880
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 34715 0 0 0 110876 132 0 0 25 0 1 0 481964360 142548992 32516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34802 32516 603 41 0 34761 0
vsize: 139208
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 35065 0 0 0 111875 133 0 0 25 0 1 0 481964360 144052224 32866 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35169 32866 603 41 0 35128 0
vsize: 140676
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 35401 0 0 0 112874 135 0 0 25 0 1 0 481964360 145395712 33202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35497 33202 603 41 0 35456 0
vsize: 141988
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 35734 0 0 0 113873 136 0 0 25 0 1 0 481964360 146755584 33535 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35829 33535 603 41 0 35788 0
vsize: 143316
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 36074 0 0 0 114872 137 0 0 25 0 1 0 481964360 148107264 33875 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36159 33875 603 41 0 36118 0
vsize: 144636
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 36412 0 0 0 115871 138 0 0 25 0 1 0 481964360 149450752 34213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36487 34213 603 41 0 36446 0
vsize: 145948
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 36747 0 0 0 116870 139 0 0 25 0 1 0 481964360 150925312 34548 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36847 34548 603 41 0 36806 0
vsize: 147388
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 37076 0 0 0 117868 141 0 0 25 0 1 0 481964360 152260608 34877 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37173 34877 603 41 0 37132 0
vsize: 148692
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 37394 0 0 0 118867 142 0 0 25 0 1 0 481964360 153620480 35195 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37505 35195 603 41 0 37464 0
vsize: 150020
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 4539
Raw data (stat): 4539 (minisat+) R 4538 28546 28545 0 -1 0 37720 0 0 0 119865 144 0 0 25 0 1 0 481964360 154836992 35521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37802 35521 603 41 0 37761 0
vsize: 151208
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 4539
Raw data (stat): 4539 (minisat+) Z 4538 28546 28545 0 -1 12 37723 0 0 0 119866 151 0 0 25 0 1 0 481964360 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.13
CPU time (s): 1200.18
CPU user time (s): 1198.66
CPU system time (s): 1.51577
CPU usage (%): 100.004
Max. virtual memory (Kb): 151208
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####