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:100.opb
MD5SUM	ac4ddb996334a0834a018e09e97d1ecb
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	76
Optimality of the best value was proved	NO
Number of terms in the objective function	4617
Biggest coefficient in the objective function	2642
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	13340
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	2642
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	13340
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.06984
Number of variables	4617
Total number of constraints	9896
Number of constraints which are clauses	4395
Number of constraints which are cardinality constraints (but not clauses)	5501
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	23
Trace number 6467

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        858652 kB
Buffers:         35200 kB
Cached:         106068 kB
SwapCached:         36 kB
Active:          51492 kB
Inactive:        92688 kB
HighTotal:      131008 kB
HighFree:        21224 kB
LowTotal:       903652 kB
LowFree:        837428 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26224 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:29:16 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 4882 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5279 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 890]---> BDD-cost:    5
c ---[ 889]---> BDD-cost:    5
c ---[ 888]---> BDD-cost:   14
c ---[ 887]---> BDD-cost:    8
c ---[ 886]---> BDD-cost:   11
c ---[ 885]---> BDD-cost:    8
c ---[ 884]---> BDD-cost:   14
c ---[ 883]---> BDD-cost:   14
c ---[ 882]---> BDD-cost:   17
c ---[ 881]---> BDD-cost:   11
c ---[ 880]---> BDD-cost:   17
c ---[ 879]---> BDD-cost:   11
c ---[ 878]---> BDD-cost:   14
c ---[ 877]---> BDD-cost:    8
c ---[ 874]---> BDD-cost:    5
c ---[ 873]---> BDD-cost:   14
c ---[ 872]---> BDD-cost:   17
c ---[ 871]---> BDD-cost:   20
c ---[ 870]---> BDD-cost:   20
c ---[ 869]---> BDD-cost:   17
c ---[ 868]---> BDD-cost:   17
c ---[ 867]---> BDD-cost:   17
c ---[ 866]---> BDD-cost:   11
c ---[ 865]---> BDD-cost:   11
c ---[ 864]---> BDD-cost:    5
c ---[ 862]---> BDD-cost:    9
c ---[ 861]---> BDD-cost:   20
c ---[ 860]---> BDD-cost:   18
c ---[ 859]---> BDD-cost:   26
c ---[ 858]---> BDD-cost:   15
c ---[ 857]---> BDD-cost:   23
c ---[ 856]---> BDD-cost:   17
c ---[ 855]---> BDD-cost:   23
c ---[ 854]---> BDD-cost:   20
c ---[ 853]---> BDD-cost:   26
c ---[ 852]---> BDD-cost:   15
c ---[ 851]---> BDD-cost:   17
c ---[ 850]---> BDD-cost:   14
c ---[ 849]---> BDD-cost:    5
c ---[ 847]---> BDD-cost:   11
c ---[ 846]---> BDD-cost:   20
c ---[ 845]---> BDD-cost:   17
c ---[ 844]---> BDD-cost:   20
c ---[ 843]---> BDD-cost:   23
c ---[ 842]---> BDD-cost:   20
c ---[ 841]---> BDD-cost:   17
c ---[ 840]---> BDD-cost:   20
c ---[ 839]---> BDD-cost:   14
c ---[ 838]---> BDD-cost:   11
c ---[ 837]---> BDD-cost:    8
c ---[ 836]---> BDD-cost:   21
c ---[ 835]---> BDD-cost:   17
c ---[ 834]---> BDD-cost:   32
c ---[ 833]---> BDD-cost:   26
c ---[ 832]---> BDD-cost:   29
c ---[ 831]---> BDD-cost:   32
c ---[ 830]---> BDD-cost:   32
c ---[ 829]---> BDD-cost:   23
c ---[ 828]---> BDD-cost:   29
c ---[ 827]---> BDD-cost:   23
c ---[ 826]---> BDD-cost:   29
c ---[ 825]---> BDD-cost:   23
c ---[ 824]---> BDD-cost:   26
c ---[ 823]---> BDD-cost:   20
c ---[ 822]---> BDD-cost:    7
c ---[ 821]---> BDD-cost:    9
c ---[ 820]---> BDD-cost:   17
c ---[ 819]---> BDD-cost:   15
c ---[ 818]---> BDD-cost:   20
c ---[ 817]---> BDD-cost:   20
c ---[ 816]---> BDD-cost:   29
c ---[ 815]---> BDD-cost:   26
c ---[ 814]---> BDD-cost:   26
c ---[ 813]---> BDD-cost:   23
c ---[ 812]---> BDD-cost:   23
c ---[ 811]---> BDD-cost:   17
c ---[ 810]---> BDD-cost:   17
c ---[ 809]---> BDD-cost:    8
c ---[ 806]---> BDD-cost:   27
c ---[ 805]---> BDD-cost:   38
c ---[ 804]---> BDD-cost:   44
c ---[ 803]---> BDD-cost:   35
c ---[ 802]---> BDD-cost:   41
c ---[ 801]---> BDD-cost:   38
c ---[ 800]---> BDD-cost:   41
c ---[ 799]---> BDD-cost:   35
c ---[ 798]---> BDD-cost:   38
c ---[ 797]---> BDD-cost:   29
c ---[ 796]---> BDD-cost:   35
c ---[ 795]---> BDD-cost:   29
c ---[ 794]---> BDD-cost:   26
c ---[ 793]---> BDD-cost:   20
c ---[ 792]---> BDD-cost:    9
c ---[ 791]---> BDD-cost:   14
c ---[ 790]---> BDD-cost:   17
c ---[ 789]---> BDD-cost:   14
c ---[ 788]---> BDD-cost:   20
c ---[ 787]---> BDD-cost:   23
c ---[ 786]---> BDD-cost:   21
c ---[ 785]---> BDD-cost:   23
c ---[ 784]---> BDD-cost:   29
c ---[ 783]---> BDD-cost:   29
c ---[ 782]---> BDD-cost:   29
c ---[ 781]---> BDD-cost:   20
c ---[ 780]---> BDD-cost:   14
c ---[ 779]---> BDD-cost:   11
c ---[ 778]---> BDD-cost:   21
c ---[ 777]---> BDD-cost:   38
c ---[ 776]---> BDD-cost:   44
c ---[ 775]---> BDD-cost:   44
c ---[ 774]---> BDD-cost:   50
c ---[ 773]---> BDD-cost:   50
c ---[ 772]---> BDD-cost:   50
c ---[ 771]---> BDD-cost:   44
c ---[ 770]---> BDD-cost:   53
c ---[ 769]---> BDD-cost:   44
c ---[ 768]---> BDD-cost:   44
c ---[ 767]---> BDD-cost:   41
c ---[ 766]---> BDD-cost:   38
c ---[ 765]---> BDD-cost:   29
c ---[ 764]---> BDD-cost:   23
c ---[ 763]---> BDD-cost:   23
c ---[ 762]---> BDD-cost:   20
c ---[ 761]---> BDD-cost:   17
c ---[ 760]---> BDD-cost:   20
c ---[ 759]---> BDD-cost:   20
c ---[ 758]---> BDD-cost:   23
c ---[ 757]---> BDD-cost:   20
c ---[ 756]---> BDD-cost:   20
c ---[ 755]---> BDD-cost:   26
c ---[ 754]---> BDD-cost:   35
c ---[ 753]---> BDD-cost:   32
c ---[ 752]---> BDD-cost:   20
c ---[ 751]---> BDD-cost:   20
c ---[ 750]---> BDD-cost:   11
c ---[ 749]---> BDD-cost:    3
c ---[ 748]---> BDD-cost:   32
c ---[ 747]---> BDD-cost:   44
c ---[ 746]---> BDD-cost:   47
c ---[ 745]---> BDD-cost:   47
c ---[ 744]---> BDD-cost:   56
c ---[ 743]---> BDD-cost:   53
c ---[ 742]---> BDD-cost:   59
c ---[ 741]---> BDD-cost:   56
c ---[ 740]---> BDD-cost:   59
c ---[ 739]---> BDD-cost:   53
c ---[ 738]---> BDD-cost:   41
c ---[ 737]---> BDD-cost:   38
c ---[ 736]---> BDD-cost:   32
c ---[ 735]---> BDD-cost:   29
c ---[ 734]---> BDD-cost:   32
c ---[ 733]---> BDD-cost:   23
c ---[ 732]---> BDD-cost:   20
c ---[ 731]---> BDD-cost:   20
c ---[ 730]---> BDD-cost:   29
c ---[ 729]---> BDD-cost:   26
c ---[ 728]---> BDD-cost:   26
c ---[ 727]---> BDD-cost:   20
c ---[ 726]---> BDD-cost:   29
c ---[ 725]---> BDD-cost:   26
c ---[ 724]---> BDD-cost:   32
c ---[ 723]---> BDD-cost:   32
c ---[ 722]---> BDD-cost:   32
c ---[ 721]---> BDD-cost:   17
c ---[ 720]---> BDD-cost:   14
c ---[ 719]---> BDD-cost:    9
c ---[ 718]---> BDD-cost:   35
c ---[ 717]---> BDD-cost:   50
c ---[ 716]---> BDD-cost:   56
c ---[ 715]---> BDD-cost:   56
c ---[ 714]---> BDD-cost:   62
c ---[ 713]---> BDD-cost:   59
c ---[ 712]---> BDD-cost:   56
c ---[ 711]---> BDD-cost:   53
c ---[ 710]---> BDD-cost:   47
c ---[ 709]---> BDD-cost:   50
c ---[ 708]---> BDD-cost:   38
c ---[ 707]---> BDD-cost:   35
c ---[ 706]---> BDD-cost:   32
c ---[ 705]---> BDD-cost:   29
c ---[ 704]---> BDD-cost:   32
c ---[ 703]---> BDD-cost:   26
c ---[ 702]---> BDD-cost:   23
c ---[ 701]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:   23
c ---[ 699]---> BDD-cost:   26
c ---[ 698]---> BDD-cost:   29
c ---[ 697]---> BDD-cost:   29
c ---[ 696]---> BDD-cost:   38
c ---[ 695]---> BDD-cost:   29
c ---[ 694]---> BDD-cost:   38
c ---[ 693]---> BDD-cost:   35
c ---[ 692]---> BDD-cost:   32
c ---[ 691]---> BDD-cost:   26
c ---[ 690]---> BDD-cost:   17
c ---[ 689]---> BDD-cost:   11
c ---[ 688]---> BDD-cost:   26
c ---[ 687]---> BDD-cost:   47
c ---[ 686]---> BDD-cost:   50
c ---[ 685]---> BDD-cost:   59
c ---[ 684]---> BDD-cost:   59
c ---[ 683]---> BDD-cost:   53
c ---[ 682]---> BDD-cost:   47
c ---[ 681]---> BDD-cost:   41
c ---[ 680]---> BDD-cost:   41
c ---[ 679]---> BDD-cost:   41
c ---[ 678]---> BDD-cost:   35
c ---[ 677]---> BDD-cost:   38
c ---[ 676]---> BDD-cost:   26
c ---[ 675]---> BDD-cost:   20
c ---[ 674]---> BDD-cost:   23
c ---[ 673]---> BDD-cost:   26
c ---[ 672]---> BDD-cost:   17
c ---[ 671]---> BDD-cost:   14
c ---[ 670]---> BDD-cost:   18
c ---[ 669]---> BDD-cost:   26
c ---[ 668]---> BDD-cost:   32
c ---[ 667]---> BDD-cost:   35
c ---[ 666]---> BDD-cost:   38
c ---[ 665]---> BDD-cost:   38
c ---[ 664]---> BDD-cost:   41
c ---[ 663]---> BDD-cost:   38
c ---[ 662]---> BDD-cost:   35
c ---[ 661]---> BDD-cost:   26
c ---[ 660]---> BDD-cost:   20
c ---[ 659]---> BDD-cost:   14
c ---[ 658]---> BDD-cost:   29
c ---[ 657]---> BDD-cost:   35
c ---[ 656]---> BDD-cost:   38
c ---[ 655]---> BDD-cost:   53
c ---[ 654]---> BDD-cost:   56
c ---[ 653]---> BDD-cost:   50
c ---[ 652]---> BDD-cost:   50
c ---[ 651]---> BDD-cost:   38
c ---[ 650]---> BDD-cost:   38
c ---[ 649]---> BDD-cost:   41
c ---[ 648]---> BDD-cost:   35
c ---[ 647]---> BDD-cost:   32
c ---[ 646]---> BDD-cost:   26
c ---[ 645]---> BDD-cost:   17
c ---[ 644]---> BDD-cost:   20
c ---[ 643]---> BDD-cost:   14
c ---[ 642]---> BDD-cost:    8
c ---[ 641]---> BDD-cost:   11
c ---[ 640]---> BDD-cost:   23
c ---[ 639]---> BDD-cost:   26
c ---[ 638]---> BDD-cost:   32
c ---[ 637]---> BDD-cost:   35
c ---[ 636]---> BDD-cost:   36
c ---[ 635]---> BDD-cost:   44
c ---[ 634]---> BDD-cost:   44
c ---[ 633]---> BDD-cost:   41
c ---[ 632]---> BDD-cost:   38
c ---[ 631]---> BDD-cost:   26
c ---[ 630]---> BDD-cost:   26
c ---[ 629]---> BDD-cost:   20
c ---[ 628]---> BDD-cost:   26
c ---[ 627]---> BDD-cost:   38
c ---[ 626]---> BDD-cost:   41
c ---[ 625]---> BDD-cost:   44
c ---[ 624]---> BDD-cost:   50
c ---[ 623]---> BDD-cost:   53
c ---[ 622]---> BDD-cost:   47
c ---[ 621]---> BDD-cost:   44
c ---[ 620]---> BDD-cost:   41
c ---[ 619]---> BDD-cost:   38
c ---[ 618]---> BDD-cost:   35
c ---[ 617]---> BDD-cost:   35
c ---[ 616]---> BDD-cost:   26
c ---[ 615]---> BDD-cost:   20
c ---[ 614]---> BDD-cost:   23
c ---[ 613]---> BDD-cost:   12
c ---[ 612]---> BDD-cost:    5
c ---[ 611]---> BDD-cost:    8
c ---[ 610]---> BDD-cost:   20
c ---[ 609]---> BDD-cost:   26
c ---[ 608]---> BDD-cost:   32
c ---[ 607]---> BDD-cost:   38
c ---[ 606]---> BDD-cost:   44
c ---[ 605]---> BDD-cost:   41
c ---[ 604]---> BDD-cost:   44
c ---[ 603]---> BDD-cost:   47
c ---[ 602]---> BDD-cost:   44
c ---[ 601]---> BDD-cost:   29
c ---[ 600]---> BDD-cost:   29
c ---[ 599]---> BDD-cost:   23
c ---[ 598]---> BDD-cost:   17
c ---[ 597]---> BDD-cost:   32
c ---[ 596]---> BDD-cost:   35
c ---[ 595]---> BDD-cost:   44
c ---[ 594]---> BDD-cost:   47
c ---[ 593]---> BDD-cost:   44
c ---[ 592]---> BDD-cost:   35
c ---[ 591]---> BDD-cost:   44
c ---[ 590]---> BDD-cost:   44
c ---[ 589]---> BDD-cost:   41
c ---[ 588]---> BDD-cost:   32
c ---[ 587]---> BDD-cost:   29
c ---[ 586]---> BDD-cost:   26
c ---[ 585]---> BDD-cost:   20
c ---[ 584]---> BDD-cost:   20
c ---[ 583]---> BDD-cost:   20
c ---[ 582]---> BDD-cost:   11
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:   17
c ---[ 579]---> BDD-cost:   23
c ---[ 578]---> BDD-cost:   35
c ---[ 577]---> BDD-cost:   38
c ---[ 576]---> BDD-cost:   44
c ---[ 575]---> BDD-cost:   47
c ---[ 574]---> BDD-cost:   41
c ---[ 573]---> BDD-cost:   44
c ---[ 572]---> BDD-cost:   44
c ---[ 571]---> BDD-cost:   35
c ---[ 570]---> BDD-cost:   29
c ---[ 569]---> BDD-cost:   20
c ---[ 568]---> BDD-cost:   14
c ---[ 567]---> BDD-cost:   23
c ---[ 566]---> BDD-cost:   29
c ---[ 565]---> BDD-cost:   38
c ---[ 564]---> BDD-cost:   38
c ---[ 563]---> BDD-cost:   38
c ---[ 562]---> BDD-cost:   38
c ---[ 561]---> BDD-cost:   38
c ---[ 560]---> BDD-cost:   44
c ---[ 559]---> BDD-cost:   44
c ---[ 558]---> BDD-cost:   36
c ---[ 557]---> BDD-cost:   29
c ---[ 556]---> BDD-cost:   20
c ---[ 555]---> BDD-cost:   17
c ---[ 554]---> BDD-cost:   17
c ---[ 553]---> BDD-cost:   20
c ---[ 552]---> BDD-cost:   20
c ---[ 551]---> BDD-cost:   11
c ---[ 550]---> BDD-cost:   29
c ---[ 549]---> BDD-cost:   26
c ---[ 548]---> BDD-cost:   29
c ---[ 547]---> BDD-cost:   41
c ---[ 546]---> BDD-cost:   44
c ---[ 545]---> BDD-cost:   44
c ---[ 544]---> BDD-cost:   47
c ---[ 543]---> BDD-cost:   44
c ---[ 542]---> BDD-cost:   41
c ---[ 541]---> BDD-cost:   32
c ---[ 540]---> BDD-cost:   23
c ---[ 539]---> BDD-cost:   14
c ---[ 538]---> BDD-cost:   17
c ---[ 537]---> BDD-cost:   20
c ---[ 536]---> BDD-cost:   23
c ---[ 535]---> BDD-cost:   32
c ---[ 534]---> BDD-cost:   44
c ---[ 533]---> BDD-cost:   44
c ---[ 532]---> BDD-cost:   41
c ---[ 531]---> BDD-cost:   47
c ---[ 530]---> BDD-cost:   44
c ---[ 529]---> BDD-cost:   44
c ---[ 528]---> BDD-cost:   44
c ---[ 527]---> BDD-cost:   35
c ---[ 526]---> BDD-cost:   32
c ---[ 525]---> BDD-cost:   20
c ---[ 524]---> BDD-cost:   26
c ---[ 523]---> BDD-cost:   20
c ---[ 522]---> BDD-cost:   23
c ---[ 521]---> BDD-cost:   26
c ---[ 520]---> BDD-cost:   29
c ---[ 519]---> BDD-cost:   23
c ---[ 518]---> BDD-cost:   32
c ---[ 517]---> BDD-cost:   32
c ---[ 516]---> BDD-cost:   38
c ---[ 515]---> BDD-cost:   44
c ---[ 514]---> BDD-cost:   44
c ---[ 513]---> BDD-cost:   47
c ---[ 512]---> BDD-cost:   38
c ---[ 511]---> BDD-cost:   26
c ---[ 510]---> BDD-cost:   26
c ---[ 509]---> BDD-cost:   14
c ---[ 508]---> BDD-cost:   17
c ---[ 507]---> BDD-cost:   20
c ---[ 506]---> BDD-cost:   26
c ---[ 505]---> BDD-cost:   35
c ---[ 504]---> BDD-cost:   36
c ---[ 503]---> BDD-cost:   41
c ---[ 502]---> BDD-cost:   38
c ---[ 501]---> BDD-cost:   42
c ---[ 500]---> BDD-cost:   44
c ---[ 499]---> BDD-cost:   44
c ---[ 498]---> BDD-cost:   50
c ---[ 497]---> BDD-cost:   47
c ---[ 496]---> BDD-cost:   44
c ---[ 495]---> BDD-cost:   35
c ---[ 494]---> BDD-cost:   35
c ---[ 493]---> BDD-cost:   32
c ---[ 492]---> BDD-cost:   32
c ---[ 491]---> BDD-cost:   26
c ---[ 490]---> BDD-cost:   29
c ---[ 489]---> BDD-cost:   26
c ---[ 488]---> BDD-cost:   29
c ---[ 487]---> BDD-cost:   38
c ---[ 486]---> BDD-cost:   41
c ---[ 485]---> BDD-cost:   38
c ---[ 484]---> BDD-cost:   35
c ---[ 483]---> BDD-cost:   38
c ---[ 482]---> BDD-cost:   32
c ---[ 481]---> BDD-cost:   32
c ---[ 480]---> BDD-cost:   29
c ---[ 479]---> BDD-cost:   17
c ---[ 478]---> BDD-cost:   14
c ---[ 477]---> BDD-cost:   20
c ---[ 476]---> BDD-cost:   26
c ---[ 475]---> BDD-cost:   32
c ---[ 474]---> BDD-cost:   38
c ---[ 473]---> BDD-cost:   38
c ---[ 472]---> BDD-cost:   44
c ---[ 471]---> BDD-cost:   44
c ---[ 470]---> BDD-cost:   44
c ---[ 469]---> BDD-cost:   47
c ---[ 468]---> BDD-cost:   56
c ---[ 467]---> BDD-cost:   53
c ---[ 466]---> BDD-cost:   44
c ---[ 465]---> BDD-cost:   41
c ---[ 464]---> BDD-cost:   38
c ---[ 463]---> BDD-cost:   35
c ---[ 462]---> BDD-cost:   38
c ---[ 461]---> BDD-cost:   35
c ---[ 460]---> BDD-cost:   29
c ---[ 459]---> BDD-cost:   26
c ---[ 458]---> BDD-cost:   38
c ---[ 457]---> BDD-cost:   41
c ---[ 456]---> BDD-cost:   44
c ---[ 455]---> BDD-cost:   38
c ---[ 454]---> BDD-cost:   38
c ---[ 453]---> BDD-cost:   35
c ---[ 452]---> BDD-cost:   35
c ---[ 451]---> BDD-cost:   35
c ---[ 450]---> BDD-cost:   26
c ---[ 449]---> BDD-cost:   17
c ---[ 448]---> BDD-cost:   14
c ---[ 447]---> BDD-cost:   17
c ---[ 446]---> BDD-cost:   20
c ---[ 445]---> BDD-cost:   32
c ---[ 444]---> BDD-cost:   36
c ---[ 443]---> BDD-cost:   41
c ---[ 442]---> BDD-cost:   44
c ---[ 441]---> BDD-cost:   41
c ---[ 440]---> BDD-cost:   38
c ---[ 439]---> BDD-cost:   47
c ---[ 438]---> BDD-cost:   47
c ---[ 437]---> BDD-cost:   47
c ---[ 436]---> BDD-cost:   41
c ---[ 435]---> BDD-cost:   41
c ---[ 434]---> BDD-cost:   35
c ---[ 433]---> BDD-cost:   32
c ---[ 432]---> BDD-cost:   35
c ---[ 431]---> BDD-cost:   41
c ---[ 430]---> BDD-cost:   41
c ---[ 429]---> BDD-cost:   32
c ---[ 428]---> BDD-cost:   44
c ---[ 427]---> BDD-cost:   47
c ---[ 426]---> BDD-cost:   44
c ---[ 425]---> BDD-cost:   41
c ---[ 424]---> BDD-cost:   41
c ---[ 423]---> BDD-cost:   35
c ---[ 422]---> BDD-cost:   29
c ---[ 421]---> BDD-cost:   29
c ---[ 420]---> BDD-cost:   29
c ---[ 419]---> BDD-cost:   20
c ---[ 418]---> BDD-cost:   17
c ---[ 417]---> BDD-cost:   17
c ---[ 416]---> BDD-cost:   20
c ---[ 415]---> BDD-cost:   26
c ---[ 414]---> BDD-cost:   29
c ---[ 413]---> BDD-cost:   35
c ---[ 412]---> BDD-cost:   41
c ---[ 411]---> BDD-cost:   44
c ---[ 410]---> BDD-cost:   35
c ---[ 409]---> BDD-cost:   35
c ---[ 408]---> BDD-cost:   41
c ---[ 407]---> BDD-cost:   47
c ---[ 406]---> BDD-cost:   38
c ---[ 405]---> BDD-cost:   38
c ---[ 404]---> BDD-cost:   33
c ---[ 403]---> BDD-cost:   35
c ---[ 402]---> BDD-cost:   42
c ---[ 401]---> BDD-cost:   47
c ---[ 400]---> BDD-cost:   53
c ---[ 399]---> BDD-cost:   47
c ---[ 398]---> BDD-cost:   47
c ---[ 397]---> BDD-cost:   44
c ---[ 396]---> BDD-cost:   44
c ---[ 395]---> BDD-cost:   44
c ---[ 394]---> BDD-cost:   50
c ---[ 393]---> BDD-cost:   35
c ---[ 392]---> BDD-cost:   32
c ---[ 391]---> BDD-cost:   29
c ---[ 390]---> BDD-cost:   20
c ---[ 389]---> BDD-cost:   20
c ---[ 388]---> BDD-cost:   11
c ---[ 387]---> BDD-cost:   14
c ---[ 386]---> BDD-cost:   20
c ---[ 385]---> BDD-cost:   26
c ---[ 384]---> BDD-cost:   32
c ---[ 383]---> BDD-cost:   32
c ---[ 382]---> BDD-cost:   41
c ---[ 381]---> BDD-cost:   38
c ---[ 380]---> BDD-cost:   35
c ---[ 379]---> BDD-cost:   38
c ---[ 378]---> BDD-cost:   38
c ---[ 377]---> BDD-cost:   35
c ---[ 376]---> BDD-cost:   35
c ---[ 375]---> BDD-cost:   41
c ---[ 374]---> BDD-cost:   44
c ---[ 373]---> BDD-cost:   38
c ---[ 372]---> BDD-cost:   50
c ---[ 371]---> BDD-cost:   59
c ---[ 370]---> BDD-cost:   59
c ---[ 369]---> BDD-cost:   53
c ---[ 368]---> BDD-cost:   59
c ---[ 367]---> BDD-cost:   50
c ---[ 366]---> BDD-cost:   47
c ---[ 365]---> BDD-cost:   50
c ---[ 364]---> BDD-cost:   53
c ---[ 363]---> BDD-cost:   41
c ---[ 362]---> BDD-cost:   29
c ---[ 361]---> BDD-cost:   20
c ---[ 360]---> BDD-cost:   17
c ---[ 359]---> BDD-cost:   14
c ---[ 358]---> BDD-cost:    8
c ---[ 357]---> BDD-cost:   11
c ---[ 356]---> BDD-cost:   17
c ---[ 355]---> BDD-cost:   26
c ---[ 354]---> BDD-cost:   29
c ---[ 353]---> BDD-cost:   29
c ---[ 352]---> BDD-cost:   26
c ---[ 351]---> BDD-cost:   38
c ---[ 350]---> BDD-cost:   29
c ---[ 349]---> BDD-cost:   35
c ---[ 348]---> BDD-cost:   35
c ---[ 347]---> BDD-cost:   32
c ---[ 346]---> BDD-cost:   29
c ---[ 345]---> BDD-cost:   41
c ---[ 344]---> BDD-cost:   44
c ---[ 343]---> BDD-cost:   44
c ---[ 342]---> BDD-cost:   53
c ---[ 341]---> BDD-cost:   56
c ---[ 340]---> BDD-cost:   56
c ---[ 339]---> BDD-cost:   59
c ---[ 338]---> BDD-cost:   59
c ---[ 337]---> BDD-cost:   59
c ---[ 336]---> BDD-cost:   44
c ---[ 335]---> BDD-cost:   44
c ---[ 334]---> BDD-cost:   50
c ---[ 333]---> BDD-cost:   41
c ---[ 332]---> BDD-cost:   32
c ---[ 331]---> BDD-cost:   20
c ---[ 330]---> BDD-cost:   11
c ---[ 329]---> BDD-cost:   11
c ---[ 328]---> BDD-cost:    8
c ---[ 327]---> BDD-cost:   11
c ---[ 326]---> BDD-cost:   17
c ---[ 325]---> BDD-cost:   26
c ---[ 324]---> BDD-cost:   23
c ---[ 323]---> BDD-cost:   20
c ---[ 322]---> BDD-cost:   14
c ---[ 321]---> BDD-cost:   23
c ---[ 320]---> BDD-cost:   20
c ---[ 319]---> BDD-cost:   29
c ---[ 318]---> BDD-cost:   29
c ---[ 317]---> BDD-cost:   32
c ---[ 316]---> BDD-cost:   29
c ---[ 315]---> BDD-cost:   41
c ---[ 314]---> BDD-cost:   41
c ---[ 313]---> BDD-cost:   44
c ---[ 312]---> BDD-cost:   47
c ---[ 311]---> BDD-cost:   56
c ---[ 310]---> BDD-cost:   62
c ---[ 309]---> BDD-cost:   59
c ---[ 308]---> BDD-cost:   56
c ---[ 307]---> BDD-cost:   53
c ---[ 306]---> BDD-cost:   41
c ---[ 305]---> BDD-cost:   44
c ---[ 304]---> BDD-cost:   41
c ---[ 303]---> BDD-cost:   41
c ---[ 302]---> BDD-cost:   35
c ---[ 301]---> BDD-cost:   20
c ---[ 300]---> BDD-cost:   20
c ---[ 299]---> BDD-cost:   11
c ---[ 298]---> BDD-cost:   11
c ---[ 297]---> BDD-cost:   11
c ---[ 296]---> BDD-cost:   23
c ---[ 295]---> BDD-cost:   26
c ---[ 294]---> BDD-cost:   23
c ---[ 293]---> BDD-cost:   14
c ---[ 292]---> BDD-cost:   11
c ---[ 291]---> BDD-cost:   14
c ---[ 290]---> BDD-cost:   17
c ---[ 289]---> BDD-cost:   20
c ---[ 288]---> BDD-cost:   26
c ---[ 287]---> BDD-cost:   29
c ---[ 286]---> BDD-cost:   20
c ---[ 285]---> BDD-cost:   35
c ---[ 284]---> BDD-cost:   41
c ---[ 283]---> BDD-cost:   50
c ---[ 282]---> BDD-cost:   50
c ---[ 281]---> BDD-cost:   47
c ---[ 280]---> BDD-cost:   56
c ---[ 279]---> BDD-cost:   62
c ---[ 278]---> BDD-cost:   56
c ---[ 277]---> BDD-cost:   53
c ---[ 276]---> BDD-cost:   44
c ---[ 275]---> BDD-cost:   41
c ---[ 274]---> BDD-cost:   44
c ---[ 273]---> BDD-cost:   38
c ---[ 272]---> BDD-cost:   35
c ---[ 271]---> BDD-cost:   29
c ---[ 270]---> BDD-cost:   29
c ---[ 269]---> BDD-cost:   20
c ---[ 268]---> BDD-cost:   17
c ---[ 267]---> BDD-cost:   20
c ---[ 266]---> BDD-cost:   23
c ---[ 265]---> BDD-cost:   29
c ---[ 264]---> BDD-cost:   29
c ---[ 263]---> BDD-cost:   20
c ---[ 262]---> BDD-cost:   14
c ---[ 261]---> BDD-cost:   14
c ---[ 260]---> BDD-cost:   23
c ---[ 259]---> BDD-cost:   20
c ---[ 258]---> BDD-cost:   20
c ---[ 257]---> BDD-cost:   20
c ---[ 256]---> BDD-cost:   20
c ---[ 255]---> BDD-cost:   35
c ---[ 254]---> BDD-cost:   35
c ---[ 253]---> BDD-cost:   41
c ---[ 252]---> BDD-cost:   47
c ---[ 251]---> BDD-cost:   47
c ---[ 250]---> BDD-cost:   53
c ---[ 249]---> BDD-cost:   53
c ---[ 248]---> BDD-cost:   50
c ---[ 247]---> BDD-cost:   56
c ---[ 246]---> BDD-cost:   47
c ---[ 245]---> BDD-cost:   47
c ---[ 244]---> BDD-cost:   41
c ---[ 243]---> BDD-cost:   38
c ---[ 242]---> BDD-cost:   35
c ---[ 241]---> BDD-cost:   29
c ---[ 240]---> BDD-cost:   26
c ---[ 239]---> BDD-cost:   23
c ---[ 238]---> BDD-cost:   17
c ---[ 237]---> BDD-cost:   17
c ---[ 236]---> BDD-cost:   20
c ---[ 235]---> BDD-cost:   29
c ---[ 234]---> BDD-cost:   26
c ---[ 233]---> BDD-cost:   26
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   17
c ---[ 230]---> BDD-cost:   20
c ---[ 229]---> BDD-cost:   20
c ---[ 228]---> BDD-cost:   20
c ---[ 227]---> BDD-cost:   26
c ---[ 226]---> BDD-cost:   26
c ---[ 225]---> BDD-cost:   29
c ---[ 224]---> BDD-cost:   35
c ---[ 223]---> BDD-cost:   41
c ---[ 222]---> BDD-cost:   47
c ---[ 221]---> BDD-cost:   41
c ---[ 220]---> BDD-cost:   45
c ---[ 219]---> BDD-cost:   53
c ---[ 218]---> BDD-cost:   50
c ---[ 217]---> BDD-cost:   56
c ---[ 216]---> BDD-cost:   41
c ---[ 215]---> BDD-cost:   41
c ---[ 214]---> BDD-cost:   32
c ---[ 213]---> BDD-cost:   32
c ---[ 212]---> BDD-cost:   32
c ---[ 211]---> BDD-cost:   29
c ---[ 210]---> BDD-cost:   23
c ---[ 209]---> BDD-cost:   17
c ---[ 208]---> BDD-cost:   23
c ---[ 207]---> BDD-cost:   23
c ---[ 206]---> BDD-cost:   20
c ---[ 205]---> BDD-cost:   23
c ---[ 204]---> BDD-cost:   20
c ---[ 203]---> BDD-cost:   23
c ---[ 202]---> BDD-cost:   17
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:   12
c ---[ 199]---> BDD-cost:   17
c ---[ 198]---> BDD-cost:   20
c ---[ 197]---> BDD-cost:   26
c ---[ 196]---> BDD-cost:   26
c ---[ 195]---> BDD-cost:   35
c ---[ 194]---> BDD-cost:   38
c ---[ 193]---> BDD-cost:   41
c ---[ 192]---> BDD-cost:   44
c ---[ 191]---> BDD-cost:   38
c ---[ 190]---> BDD-cost:   38
c ---[ 189]---> BDD-cost:   41
c ---[ 188]---> BDD-cost:   35
c ---[ 187]---> BDD-cost:   44
c ---[ 186]---> BDD-cost:   32
c ---[ 185]---> BDD-cost:   35
c ---[ 184]---> BDD-cost:   36
c ---[ 183]---> BDD-cost:   35
c ---[ 182]---> BDD-cost:   29
c ---[ 181]---> BDD-cost:   23
c ---[ 180]---> BDD-cost:   20
c ---[ 179]---> BDD-cost:   14
c ---[ 178]---> BDD-cost:   20
c ---[ 177]---> BDD-cost:   20
c ---[ 176]---> BDD-cost:   17
c ---[ 175]---> BDD-cost:   20
c ---[ 174]---> BDD-cost:   20
c ---[ 173]---> BDD-cost:   20
c ---[ 172]---> BDD-cost:   14
c ---[ 171]---> BDD-cost:   14
c ---[ 170]---> BDD-cost:   14
c ---[ 169]---> BDD-cost:   17
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   32
c ---[ 166]---> BDD-cost:   29
c ---[ 165]---> BDD-cost:   29
c ---[ 164]---> BDD-cost:   32
c ---[ 163]---> BDD-cost:   33
c ---[ 162]---> BDD-cost:   32
c ---[ 161]---> BDD-cost:   35
c ---[ 160]---> BDD-cost:   29
c ---[ 159]---> BDD-cost:   32
c ---[ 158]---> BDD-cost:   29
c ---[ 157]---> BDD-cost:   32
c ---[ 156]---> BDD-cost:   32
c ---[ 155]---> BDD-cost:   35
c ---[ 154]---> BDD-cost:   32
c ---[ 153]---> BDD-cost:   32
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   23
c ---[ 150]---> BDD-cost:   23
c ---[ 149]---> BDD-cost:   11
c ---[ 148]---> BDD-cost:   20
c ---[ 147]---> BDD-cost:   20
c ---[ 146]---> BDD-cost:   20
c ---[ 145]---> BDD-cost:   20
c ---[ 144]---> BDD-cost:   23
c ---[ 143]---> BDD-cost:   20
c ---[ 142]---> BDD-cost:   14
c ---[ 141]---> BDD-cost:    8
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   17
c ---[ 138]---> BDD-cost:   23
c ---[ 137]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   23
c ---[ 135]---> BDD-cost:   32
c ---[ 134]---> BDD-cost:   29
c ---[ 133]---> BDD-cost:   23
c ---[ 132]---> BDD-cost:   23
c ---[ 131]---> BDD-cost:   23
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   23
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   35
c ---[ 126]---> BDD-cost:   32
c ---[ 125]---> BDD-cost:   32
c ---[ 124]---> BDD-cost:   32
c ---[ 123]---> BDD-cost:   26
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   26
c ---[ 120]---> BDD-cost:   29
c ---[ 119]---> BDD-cost:   17
c ---[ 118]---> BDD-cost:   20
c ---[ 117]---> BDD-cost:   20
c ---[ 116]---> BDD-cost:   23
c ---[ 115]---> BDD-cost:   26
c ---[ 114]---> BDD-cost:   26
c ---[ 113]---> BDD-cost:   23
c ---[ 112]---> BDD-cost:   17
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   14
c ---[ 109]---> BDD-cost:   14
c ---[ 108]---> BDD-cost:   17
c ---[ 107]---> BDD-cost:   24
c ---[ 106]---> BDD-cost:   20
c ---[ 105]---> BDD-cost:   17
c ---[ 104]---> BDD-cost:   17
c ---[ 103]---> BDD-cost:   23
c ---[ 102]---> BDD-cost:   17
c ---[ 101]---> BDD-cost:   17
c ---[ 100]---> BDD-cost:   23
c ---[  99]---> BDD-cost:   23
c ---[  98]---> BDD-cost:   23
c ---[  97]---> BDD-cost:   26
c ---[  96]---> BDD-cost:   26
c ---[  95]---> BDD-cost:   29
c ---[  94]---> BDD-cost:   29
c ---[  93]---> BDD-cost:   35
c ---[  92]---> BDD-cost:   35
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   23
c ---[  89]---> BDD-cost:   20
c ---[  88]---> BDD-cost:   17
c ---[  87]---> BDD-cost:   23
c ---[  86]---> BDD-cost:   23
c ---[  85]---> BDD-cost:   26
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   20
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   14
c ---[  80]---> BDD-cost:   17
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   17
c ---[  76]---> BDD-cost:   12
c ---[  75]---> BDD-cost:   17
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   14
c ---[  72]---> BDD-cost:   14
c ---[  71]---> BDD-cost:   14
c ---[  70]---> BDD-cost:   12
c ---[  69]---> BDD-cost:   14
c ---[  68]---> BDD-cost:   20
c ---[  67]---> BDD-cost:   26
c ---[  66]---> BDD-cost:   23
c ---[  65]---> BDD-cost:   23
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   23
c ---[  61]---> BDD-cost:   24
c ---[  60]---> BDD-cost:   20
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:    8
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   20
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   14
c ---[  48]---> BDD-cost:   14
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:    8
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:    8
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   17
c ---[  37]---> BDD-cost:   20
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   23
c ---[  34]---> BDD-cost:   26
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   17
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:    8
c ---[  28]---> BDD-cost:    5
c ---[  27]---> BDD-cost:    6
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:    5
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    5
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:    8
c ---[  16]---> BDD-cost:    8
c ---[  15]---> BDD-cost:    8
c ---[  14]---> BDD-cost:    8
c ---[  13]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    5
c ---[  11]---> BDD-cost:    8
c ---[  10]---> BDD-cost:   11
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   17
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   20
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   11
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  126282   355112 |   42094       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 4790[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11317   maxlim: 3266   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  205461   637882 |   68487       0        0     nan |  0.000 % |
c |       100 |  205461   637882 |   75335     100      307     3.1 |  2.145 % |
c |       250 |  205461   637882 |   82869     250      883     3.5 |  2.145 % |
c |       475 |  205461   637882 |   91156     475     1764     3.7 |  2.145 % |
c |       812 |  205461   637882 |  100271     812     3094     3.8 |  2.145 % |
c |      1318 |  205461   637882 |  110298    1318     5075     3.9 |  2.145 % |
c |      2077 |  205461   637882 |  121328    2077     8684     4.2 |  2.145 % |
c |      3216 |  205461   637882 |  133461    3216    15894     4.9 |  2.145 % |
c |      4925 |  205461   637882 |  146807    4925    26586     5.4 |  2.145 % |
c |      7487 |  205452   637851 |  161488    7485    43494     5.8 |  2.147 % |
c |     11331 |  205452   637851 |  177637   11329    81987     7.2 |  2.147 % |
c |     17097 |  205443   637820 |  195401   17093   374522    21.9 |  2.150 % |
c |     25746 |  205443   637820 |  214941   25742   482673    18.8 |  2.150 % |
c ==============================================================================
c [1mFound solution: 855[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 7201   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35361 |  205450   637852 |   68483   35355   632500    17.9 |  2.150 % |
c |     35461 |  205450   637852 |   75331   35455   633210    17.9 |  2.164 % |
c |     35611 |  205450   637852 |   82864   35605   634278    17.8 |  2.164 % |
c |     35836 |  205450   637852 |   91150   35830   635785    17.7 |  2.164 % |
c |     36173 |  205450   637852 |  100265   36167   643385    17.8 |  2.164 % |
c |     36679 |  205450   637852 |  110292   36673   645764    17.6 |  2.164 % |
c |     37438 |  205450   637852 |  121321   37432   650323    17.4 |  2.164 % |
c |     38577 |  205450   637852 |  133453   38571   658088    17.1 |  2.164 % |
c |     40286 |  205450   637852 |  146799   40280   675571    16.8 |  2.164 % |
c |     42848 |  205450   637852 |  161479   42842   737717    17.2 |  2.164 % |
c |     46692 |  205450   637852 |  177627   46686   833843    17.9 |  2.164 % |
c |     52458 |  205450   637852 |  195389   52452   908273    17.3 |  2.164 % |
c |     61107 |  205450   637852 |  214928   61101   996450    16.3 |  2.164 % |
c |     74084 |  205435   637779 |  236421   74072  1941537    26.2 |  2.169 % |
c ==============================================================================
c [1mFound solution: 824[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7232   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86704 |  205437   637803 |   68479   86692  2184344    25.2 |  2.169 % |
c |     86805 |  205437   637803 |   75326   19156   277482    14.5 |  2.173 % |
c |     86955 |  205437   637803 |   82859   19306   278262    14.4 |  2.173 % |
c |     87180 |  205437   637803 |   91145   19531   279793    14.3 |  2.173 % |
c |     87517 |  205437   637803 |  100260   19868   288283    14.5 |  2.173 % |
c |     88024 |  205437   637803 |  110286   20375   296867    14.6 |  2.173 % |
c |     88783 |  205437   637803 |  121314   21134   303636    14.4 |  2.173 % |
c |     89922 |  205437   637803 |  133446   22273   316778    14.2 |  2.173 % |
c |     91630 |  205437   637803 |  146790   23981   334308    13.9 |  2.173 % |
c |     94193 |  205437   637803 |  161469   26544   355930    13.4 |  2.173 % |
c ==============================================================================
c [1mFound solution: 751[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7305   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96993 |  205445   637847 |   68481   29344   379567    12.9 |  2.173 % |
c |     97093 |  205445   637847 |   75329   29444   380266    12.9 |  2.180 % |
c |     97243 |  205445   637847 |   82862   29594   381613    12.9 |  2.180 % |
c |     97468 |  205445   637847 |   91148   29819   389853    13.1 |  2.180 % |
c |     97805 |  205445   637847 |  100263   30156   391646    13.0 |  2.180 % |
c |     98311 |  205445   637847 |  110289   30662   394167    12.9 |  2.180 % |
c |     99071 |  205445   637847 |  121318   31422   399179    12.7 |  2.180 % |
c |    100211 |  205445   637847 |  133450   32562   407577    12.5 |  2.180 % |
c |    101920 |  205445   637847 |  146795   34271   433467    12.6 |  2.180 % |
c |    104482 |  205445   637847 |  161474   36833   496862    13.5 |  2.180 % |
c |    108326 |  205445   637847 |  177622   40677   538753    13.2 |  2.180 % |
c |    114092 |  205445   637847 |  195384   46443  1038041    22.4 |  2.180 % |
c |    122742 |  205445   637847 |  214922   55093  1120509    20.3 |  2.180 % |
c |    135717 |  205445   637847 |  236414   68068  2517131    37.0 |  2.180 % |
c |    155180 |  205445   637847 |  260056   87531  3924638    44.8 |  2.180 % |
c |    184374 |  205445   637847 |  286062  116725  5810692    49.8 |  2.180 % |
c |    228164 |  205445   637847 |  314668  160515 15417055    96.0 |  2.180 % |
c |    293848 |  205445   637847 |  346135  226199 18287478    80.8 |  2.180 % |
c |    392375 |  205440   637832 |  380748  324725 30107442    92.7 |  2.183 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v4075 -v3895 v668 v176 v4076 v180 v3894 -v2907 -v1568 -v1450 v671 -v3178 v1573 -v1454 v672 v3900 -v3177 -v2876 v1572 v3898 v2881 -v1265 -v3179 v2880 v1575 -v1264 -v1034 -v78 v3899 -v3181 v1576 -v1266 -v1038 v3903 -v2883 v1579 -v1267 v1009 -v77 -v3182 -v2884 v1577 -v1268 v1013 v81 -v3920 -v3184 v2887 -v1578 -v1275 v7 -v3185 v2885 -v1269 v82 v11 -v3923 v2886 v2380 -v1270 -v196 -v3924 v3071 -v1271 v4616 v3070 -v3454 -v2333 -v1615 v199 -v3570 v2332 v1620 -v200 -v4286 -v3569 v3078 v2334 -v1637 v1619 v203 -v4290 v4117 -v3571 v3072 v2337 -v1636 v201 v4116 -v3572 -v3311 v3073 v2336 -v1638 -v1622 v202 v4118 -v3573 -v3310 v3074 -v2559 -v2341 -v1954 v1641 -v1623 v4119 -v3580 -v3312 -v2558 -v2340 v1953 v1640 v1626 v4120 -v3574 -v3315 -v2560 -v2338 -v1645 v1624 v4127 -v3575 -v3314 -v2561 -v2339 v1955 -v1644 v1625 v4121 -v3576 -v3318 v2562 v1957 -v1642 v4122 -v3316 v2567 -v1643 v625 v4123 -v3317 v2563 v1958 -v3380 v3384 -v4140 v4077 -v3890 -v2903 v667 v175 v179 v3896 -v2906 -v2670 -v1449 v673 -v236 -v3173 -v1567 -v1453 -v240 -v4080 v3901 -v3172 -v1569 -v2875 v1574 v3904 -v3180 -v2877 v1571 v1033 -v676 v3902 -v3183 v2882 v1580 -v1037 -v3187 v2879 -v1278 v1008 -v79 -v3186 v2888 -v1279 v1012 v83 -v3919 -v1274 -v760 v6 v10 -v3925 v2379 -v1272 -v85 -v195 -v86 -v3450 -v197 v3928 -v3453 v3081 v3082 -v1614 v204 -v4285 v3077 v2384 -v1616 -v4289 v2335 v1621 -v3583 -v3075 v2349 v1618 -v3584 -v2345 -v1949 -v1639 v1627 v4130 -v3579 -v2344 -v1948 v1653 v4131 -v3313 v1649 v4126 -v3577 -v3326 -v2570 v1956 v1648 -v621 -v3322 v2571 v1959 v4124 -v3321 v2566 -v1960 v624 -v1961 -v4136 -v3379 v3111 v663 v3383 -v3115 -v4139 v4078 -v2902 v2671 -v1903 v669 v177 -v3889 -v2669 v181 -v4456 -v4081 -v3891 -v2908 -v2216 -v1451 v674 -v235 -v4079 v3897 -v2220 -v1455 -v239 v3893 v677 -v183 v3905 -v3174 -v1570 v675 -v184 -v73 -v4390 -v3175 -v2911 -v1588 -v1457 -v1277 v1035 -v72 -v3176 -v2878 -v1584 -v1458 -v1276 -v1039 v3915 -v3191 -v2896 -v1980 -v1583 v1010 -v756 -v80 v2892 v1014 v84 -v3921 v3093 v2891 -v2376 -v1041 -v759 -v88 v8 -v1042 -v87 v12 -v3926 -v2772 v2381 -v1273 v1016 v1017 v3929 -v3449 v3080 v14 v3927 v3079 -v198 v15 -v3455 v2385 -v212 v2383 v208 -v4287 -v3582 v2346 v207 -v4291 -v3581 v2348 -v1617 v4129 -v3458 -v3076 v1650 v1635 -v382 -v265 v4128 v1652 v1631 -v386 v4293 -v3323 -v2569 -v2342 v1630 v4294 -v3325 -v2568 -v1950 -v3578 -v2343 -v1951 v1646 -v620 -v334 v1952 -v338 v4125 v3949 -v3319 v2564 v1965 v1647 v626 -v4135 -v4074 -v3381 v3110 -v2898 -v1899 v172 v3385 -v3114 v2672 -v1445 v662 -v4457 -v4141 -v3030 -v2904 -v1902 -v1499 -v1444 v664 v178 -v4455 -v4082 -v1503 v670 v182 v3387 -v3003 -v2909 v2215 -v1452 v666 -v237 v186 -v3892 v3388 -v3007 -v2219 -v1456 v1029 v678 -v241 -v185 -v4386 -v4144 v3913 -v2912 -v1585 -v1460 -v1059 v1028 v3909 -v2910 -v1587 -v1459 -v1063 -v1004 -v4389 -v3908 -v3194 -v2893 -v1976 v1036 v1003 v243 -v3195 -v2895 -v1040 v244 -v74 v2 -v3190 -v3089 -v1979 -v1581 -v1044 v1011 -v755 -v361 -v75 v1 v3914 -v1043 v1015 v76 v3916 -v3188 v3092 v2889 v2768 -v1582 v1019 -v761 v92 v9 -v3922 -v2375 v1018 v13 v3918 -v3445 -v2890 -v2771 -v2377 v17 v3930 v2382 v16 -v3451 v764 -v209 -v4281 v2386 -v211 -v4280 -v3456 -v1789 v2347 -v4288 -v3459 v1632 -v261 -v205 -v4292 -v3457 v1651 v1634 v4296 -v3479 -v381 -v264 -v206 v4295 -v3324 -v385 v1628 -v616 -v3945 v1968 v1629 -v1355 -v1238 -v622 -v333 v1969 -v1359 -v337 v3948 -v3320 -v2565 v1964 v627 -v4137 v3382 v3112 -v3026 -v2680 -v1932 -v1898 -v4458 -v4073 v3386 -v3116 -v2897 -v2676 -v231 v171 -v4142 v4090 v3390 -v3029 -v2899 -v2675 -v1904 -v1498 -v230 v173 v4086 v3389 -v2905 -v1502 -v1446 v665 v174 -v4145 v4085 -v3910 -v3118 -v3002 -v2901 v2217 -v1447 -v686 v238 v190 -v4143 v3912 -v3119 -v3006 -v2913 -v2221 -v1586 -v1448 -v682 -v242 -v4385 -v4012 -v3193 v1907 -v1464 -v1058 -v681 v246 -v3192 -v2894 -v1062 v1030 v245 -v4391 v4315 -v3906 -v2223 -v1975 v1031 -v751 -v357 -v2224 v1032 v1005 -v3907 -v3088 -v2096 -v1981 -v1048 v1006 v757 -v360 v95 -v2100 v1007 v96 v3 -v4394 -v3189 v3094 v2767 -v1023 -v762 v91 v4 v3917 v5 -v3938 -v2773 -v1984 v765 v89 v21 -v3934 -v3444 -v2378 v763 -v210 -v3933 -v3446 -v3097 -v2394 v1785 -v3452 -v2390 -v3448 -v3295 v2776 -v2389 v1788 v4282 -v3460 v1633 v4283 v3983 v3475 -v260 v4284 -v3987 v4300 -v3478 -v1876 -v383 v266 -v1880 -v387 -v4265 v1967 -v1234 v1966 v615 -v3944 -v1354 -v1237 v617 -v389 v335 -v269 -v1358 v623 -v390 v339 v3950 v1962 v619 v628 -v4466 -v4133 -v4087 -v3378 v3113 -v3025 -v2679 -v1931 -v1900 -v4462 -v4138 v4089 v3377 -v3117 -v2211 -v4461 v4134 v3394 -v3121 -v3031 -v2673 -v2210 -v1905 v1500 -v683 -v313 v193 -v4146 -v3911 -v3120 -v2900 -v1504 -v685 -v232 v194 v4381 v4083 -v4008 -v3004 -v2921 -v2674 -v2401 v2218 v1908 -v1467 -v233 -v189 -v3008 -v2917 -v2405 -v2222 v1906 -v1468 v234 -v4387 -v4311 v4084 -v4011 -v3034 -v2916 -v2226 -v1971 -v1760 -v1506 -v1463 -v1060 -v679 v250 -v187 -v2225 v1764 -v1507 -v1064 -v4392 v4314 -v3084 v3010 -v1977 -v1461 -v1051 -v680 -v356 v94 v3011 -v1052 -v750 v93 -v4395 -v3090 v2763 -v2095 -v1982 -v1066 -v1047 v1026 -v752 -v362 -v4393 -v2099 -v1067 v1027 v758 -v3935 v3095 v2769 -v1985 -v1045 -v1022 v754 v24 -v3937 -v1983 v766 v25 -v3098 -v2774 -v2391 -v1020 -v365 v90 v20 -v3096 -v2393 -v3931 -v3291 v2777 v1784 v18 -v3447 v2775 -v3932 -v3468 v3294 -v2387 v1790 -v571 -v256 -v3464 -v575 -v377 -v4303 v3982 v3474 -v3463 -v2388 -v376 v262 v4304 -v3986 v4299 -v4261 -v3480 -v1875 v1793 v525 -v384 v267 -v1879 v388 -v329 v4297 -v4264 -v4186 v3940 -v1233 v392 -v328 -v270 -v4190 -v391 -v268 -v3946 v3483 -v1356 -v1239 v336 -v32 -v1360 v618 v340 -v36 v3951 v1963 v636 v341 v632 v342 -v4465 -v4088 -v3397 -v3109 v3027 -v2677 -v2288 -v1933 -v1896 v1495 -v309 v192 -v4132 -v3398 v3108 -v2998 -v2292 -v1901 -v684 v191 -v4459 v4154 -v3393 v3125 -v3032 -v2997 -v2918 v1897 v1501 -v1466 -v312 v4150 -v2920 -v2212 v1909 -v1505 -v1465 v1054 -v4460 v4149 -v4007 -v3391 -v3035 -v3005 -v2400 -v2213 -v1937 -v1509 v1053 -v253 v4380 -v3033 -v3009 -v2404 v2214 -v1508 -v254 v4382 -v4310 -v4013 v3013 -v2914 -v2230 -v1759 -v1061 -v1050 -v352 v249 -v188 -v4388 v3012 -v1970 v1763 -v1065 -v1049 v4384 v4316 -v2915 -v1972 -v1462 v1069 v1025 -v358 -v247 -v4396 -v3083 -v1978 v1068 v1024 -v4016 -v3085 -v2097 -v1974 -v363 -v23 -v3936 -v3091 v2762 -v2101 -v1986 -v753 -v22 v4319 v3087 v2764 -v1046 -v774 -v366 v3099 v2770 -v2392 v770 -v364 v2766 -v2103 v1780 -v1021 v769 v2778 -v2104 -v3465 -v3290 v1786 -v19 -v3467 -v4302 -v3470 v3296 v1791 -v570 -v4301 -v574 -v255 v3984 v3476 -v3461 v1794 v521 -v257 -v3988 v1792 -v378 v263 v4260 -v3637 -v3481 -v3462 -v3299 -v1877 -v1229 v524 v379 v259 -v1881 -v1350 v380 -v271 -v4298 -v4266 -v4185 v3990 v3484 -v1349 -v1235 -v396 -v4189 v3991 v3939 v3482 -v330 v3941 -v3778 -v1883 -v1357 -v1240 v633 -v331 -v31 -v3947 -v1884 -v1361 v635 v332 -v35 -v4269 v3943 -v1362 -v1241 v346 v3952 -v1363 -v1242 v631 -v4463 v4151 -v3395 v3128 -v3023 -v2678 -v2287 -v1934 -v308 v4153 v3129 v3028 -v2919 -v2291 -v1895 v1494 -v4003 -v3124 v3024 -v1938 -v1917 v1496 -v808 -v314 -v252 -v3036 -v2999 -v1936 v1913 v1497 -v251 -v4306 v4147 -v4009 -v3392 -v3122 -v3000 -v2402 -v2233 v1912 -v1513 v3001 -v2406 -v2234 v1055 -v4312 v4148 v4014 -v3017 -v2229 -v1761 v1056 -v317 v4383 -v2091 v1765 v1057 -v351 -v4404 v4317 -v4017 -v2408 -v2227 -v2090 -v1073 -v947 -v353 -v248 -v4400 -v4015 -v2409 -v1973 -v359 -v4399 v4320 -v3658 -v2098 -v1994 -v1767 -v771 -v355 v4318 -v3662 -v3086 -v2102 -v1990 -v1768 -v773 -v367 v3107 -v2106 -v1989 v3103 v2765 -v2105 v3286 v3102 v2786 v767 -v3466 v2782 v1779 -v3292 v2781 v1781 v768 v3978 v1787 v3977 v3297 v1783 -v572 -v3469 v1871 v1795 v576 v4256 v3985 -v3633 -v3471 -v3300 v1870 v520 -v3989 v3477 -v3298 -v258 v4262 v3993 -v3802 -v3636 v3473 -v1878 -v578 v526 -v399 -v279 v3992 v3485 -v1882 -v1228 -v579 v400 -v275 -v4267 -v4187 -v3774 -v1886 -v1230 -v647 -v395 -v274 -v4191 -v1885 -v1351 -v1236 -v634 -v4270 -v3777 -v1352 -v1232 v529 -v393 -v349 -v33 -v4268 v3942 -v1353 -v1243 v350 -v37 -v4193 v3960 -v1367 v345 -v4194 v3956 v629 -v4464 -v4152 -v3396 v3126 -v2289 -v1935 -v1914 v804 -v402 -v310 -v3022 -v2396 -v2293 -v1939 -v1916 v3044 -v2395 -v2232 -v1851 v1516 -v807 -v315 -v4002 -v3040 -v2231 -v1855 -v1755 v1517 -v4361 -v4004 -v3123 -v3039 v3020 -v2403 -v2295 -v1910 -v1754 -v1512 -v318 v4365 -v4305 v4010 v3021 -v2407 -v2296 -v316 -v4401 -v4307 -v4211 v4006 -v3016 -v2654 -v2411 -v1911 v1762 -v1510 v1076 -v943 -v4403 v4313 v4215 -v4018 -v2410 v1766 v1077 v4309 -v3014 -v2228 -v1991 v1770 -v1072 -v946 v4321 v2092 -v1993 v1769 -v772 -v354 -v4397 -v3657 -v3104 v2093 -v1685 -v1070 -v375 -v3661 v3106 v2094 -v1689 -v371 -v4398 -v2783 v2110 -v1987 -v1404 -v370 v2785 v3100 -v1988 v3285 -v566 v3287 v3101 v2779 -v565 -v3293 v1782 v3289 v2780 v1803 v573 -v516 v3979 -v3301 v1799 v577 v3980 -v3798 -v3632 -v1798 -v833 v581 v522 -v398 -v276 v4255 -v4181 v3981 -v3472 v1872 v580 -v397 -v278 v4257 -v4180 v3997 -v3801 -v3638 v3493 v1873 -v643 v527 v4263 v3489 v1874 -v27 v4259 -v4188 -v3773 v3488 -v1890 -v646 v530 -v348 -v272 -v26 -v4271 -v4192 -v1231 v528 -v347 v4196 -v3957 -v3779 -v3641 -v1370 -v1251 -v394 -v273 -v34 v4195 v3959 -v1371 -v1247 v38 -v1366 -v1290 -v1246 v343 v219 v39 v3955 -v630 -v223 v40 -v3133 v3127 v3041 -v2290 -v1947 -v1915 -v1515 v803 -v401 -v306 -v3137 v3043 -v2294 -v1943 -v1514 -v311 v3019 -v2298 -v1942 -v1850 v809 -v307 v3018 -v2397 -v2297 -v1854 -v319 v4360 -v3037 -v2650 -v2398 v1075 -v4402 v4364 -v4005 -v2399 -v1756 v1074 -v4210 -v4026 -v3038 -v2653 -v2415 -v1757 -v1511 -v942 v812 -v4308 v4214 -v4022 -v1992 v1758 -v4329 -v4021 -v3015 v1774 -v948 -v372 v4325 -v3105 -v374 v4324 -v3659 v2113 -v1684 -v1400 -v1071 -v3663 -v2784 v2114 v1688 v2109 -v1403 -v951 -v368 -v3665 -v3595 v2107 -v369 -v3666 v1800 v3288 v1802 -v567 -v3628 v3309 -v829 -v568 v3305 v569 -v515 -v277 -v4000 -v3797 -v3634 -v3490 v3304 -v1796 -v832 -v585 v517 -v4001 v3492 v523 v3996 -v3803 -v3769 -v3639 -v1893 -v1797 -v642 v519 v4258 -v4182 -v1894 v531 -v4279 -v4183 v3994 -v3775 -v3642 v3486 -v2982 -v1889 v1425 -v1369 -v1248 -v648 -v4275 v4184 -v3958 -v3640 v1429 -v1368 -v1250 -v28 -v4274 -v4200 v3806 -v3780 v3487 -v1887 -v1286 -v29 v30 v3781 -v3274 -v1364 v1289 -v1244 -v651 -v344 v218 -v44 -v3953 v3782 v3278 -v222 -v3132 v3042 -v2286 -v1946 v805 v403 -v3136 -v2285 -v305 -v2302 -v1940 -v1852 v810 -v327 -v1856 -v323 v4362 -v4023 -v2649 -v2418 -v1941 -v938 v813 -v407 -v322 v4366 -v4025 -v2419 v811 -v4326 -v4212 -v2655 -v2414 -v2071 -v1858 -v1777 -v944 -v4328 v4216 -v3653 -v2075 -v1859 -v1778 -v373 -v4368 -v4019 -v3652 -v2412 -v2112 v1773 -v1138 v949 -v4369 -v2111 v4322 -v4218 -v4020 -v3660 -v3333 -v2658 v1771 -v1686 -v1399 v952 -v4219 -v3664 v3337 v1690 -v950 v4323 -v3668 -v3591 -v2001 -v1405 -v3667 -v2005 v4415 -v3594 v2108 v1692 v1801 v1693 v3306 v1408 v3308 -v3999 -v3793 -v828 v588 -v3998 -v3627 -v3491 v589 -v3845 v3799 -v3629 -v3302 -v1892 -v1664 -v834 -v638 -v584 -v3849 -v3635 -v1891 v518 -v4276 v3804 -v3631 -v3303 -v2978 -v644 -v582 v539 -v4278 -v3768 -v3643 -v1249 -v535 -v4203 v3995 v3807 -v3770 -v2981 v1424 v837 -v649 -v534 -v4204 v3805 -v3776 v1428 -v4272 -v4199 v3772 -v1888 -v1285 -v736 -v652 -v47 v3783 -v650 v48 -v4273 -v4197 -v3273 -v1365 v1291 -v1245 v220 -v43 -v3954 v3277 -v224 v3134 -v2305 -v1944 -v1847 v801 v404 -v324 -v4356 -v3138 -v2306 v806 -v326 -v4355 -v3253 -v2645 -v2417 -v2301 -v1853 v802 v408 v4206 -v4024 -v2416 -v1857 v814 v406 v4363 v4205 -v3140 -v2651 -v2299 -v2270 -v1861 -v1776 -v320 v4367 -v4327 -v3141 -v1860 -v1775 -v937 -v4371 -v4213 -v3230 -v2656 -v2070 v1134 -v939 v918 -v321 -v4370 v4217 -v2074 -v1680 -v945 -v922 -v4221 -v2659 -v2539 -v2413 -v1679 v1395 -v1137 -v1088 v941 -v4220 -v3654 -v2657 -v2543 v953 -v3655 v3332 -v1772 -v1687 -v1401 -v1334 -v3656 v3336 v1691 v4411 -v3672 -v3590 -v2000 v1695 -v1406 -v2004 v1694 v4414 -v3596 -v2928 v1409 -v3307 -v2932 v1407 -v4161 -v824 v587 -v4165 v586 -v3599 -v2313 v1660 v830 -v3792 -v2317 -v3844 v3794 -v1663 v835 v536 -v4277 -v3848 v3800 -v3630 -v637 v538 v4597 -v4202 v3796 -v3651 -v2977 v838 -v639 -v583 -v4601 -v4201 v3808 -v3647 v836 -v645 -v3646 -v2983 v1426 -v1281 -v732 -v641 -v532 -v286 -v131 -v46 -v3771 v1430 -v653 -v290 v214 -v45 -v3791 -v1287 -v735 -v533 v213 v3787 -v4198 v3786 -v3275 -v2986 v1432 v1292 v221 -v41 v3279 v1433 -v225 v3249 v3135 -v2303 -v1945 v405 -v325 -v3139 -v1846 v800 v409 v3252 -v3143 v2266 -v1848 -v822 -v4357 -v3142 -v2644 -v1849 -v818 -v4358 -v3226 -v2646 -v2300 -v2269 -v1865 -v817 v4359 v4207 -v2652 -v4375 v4208 -v3229 -v2648 v2072 v1133 -v1084 v917 v4209 -v2660 -v2076 v940 -v921 -v4225 -v2538 -v1330 -v1139 -v1087 v961 -v2542 -v1681 v1394 -v957 -v4527 -v3675 -v3586 v3334 v2078 -v1682 v1396 -v1333 -v956 -v3676 v3338 v2079 v1683 -v1402 v4410 -v3671 -v3592 -v2002 v1699 v1398 -v1142 -v984 -v2006 v1410 -v988 v4416 -v3669 -v3597 -v3504 v3340 v2927 -v3341 -v2931 -v4160 -v3600 -v2195 -v2008 -v4164 -v3598 -v2009 -v823 -v4419 v2312 v1659 -v825 -v2316 v831 -v537 -v3846 -v3648 -v2973 -v2430 -v1665 v827 -v3850 v3795 -v3650 -v1420 v839 v4596 v3816 -v2979 -v1419 -v127 -v4600 v3812 -v640 -v3852 v3811 -v3788 -v3644 -v2984 -v1668 v1427 -v731 -v661 -v285 -v130 -v3853 -v3790 -v3269 v1431 -v1280 -v657 -v289 -v3645 -v3268 -v2987 v1435 -v1282 -v737 -v656 -v2985 v1434 -v1288 v215 v3784 -v3276 -v2030 v1284 v216 -v42 v3280 -v1293 v217 v3248 -v3131 -v2304 v1805 -v819 -v417 v3130 -v821 -v413 v3254 v3147 v2265 -v1868 -v412 v2066 -v1869 v4378 -v3225 -v2271 v2065 -v1864 -v1129 -v815 v4379 -v2647 -v4374 v4228 -v3257 -v3231 -v2668 v2073 -v1862 v1135 -v1083 v958 v919 -v816 v4229 -v3328 -v2664 v2077 v960 -v923 -v4523 -v4372 -v4224 -v3674 v3327 -v2663 -v2540 -v2274 v2081 -v1329 -v1140 -v1089 -v3673 -v2544 v2080 v1996 -v4526 -v4406 -v4222 v3335 -v3234 v1995 -v1702 -v1335 -v1143 -v954 v925 -v3585 v3339 v1703 v1397 -v1141 v926 v4412 -v3587 -v3500 v3343 -v2546 -v2514 v2003 v1698 v1418 -v1092 -v983 -v955 -v3593 v3342 -v2547 -v2518 -v2007 -v1414 -v987 v4417 -v3670 -v3589 -v3503 v2929 -v2191 -v2011 v1696 -v1413 -v1338 -v3601 -v2933 -v2010 v4420 -v4162 -v2194 -v1655 v471 -v4418 -v4166 v3840 -v475 v3839 -v2935 -v2426 v2314 v1661 -v3649 -v2936 -v2318 -v826 -v4168 -v3847 v3813 -v2429 -v1666 v847 -v4169 -v3851 v3815 -v2972 v843 v4598 -v3855 -v2974 v2320 -v2170 -v1669 v842 -v727 -v658 -v126 -v4602 -v3854 -v3789 -v2980 v2321 -v1667 v1421 -v660 v3809 -v2976 v1422 -v733 -v287 -v132 -v2988 v1423 -v291 v4604 v3810 -v2026 -v1439 -v738 -v654 v4605 -v3270 -v1283 v3785 -v3271 -v2125 v2029 v1301 -v739 -v655 -v293 v228 -v135 v3272 v1297 -v740 -v294 v229 v3250 v3150 -v2261 -v1867 v1804 -v820 -v416 v3151 -v1866 v4377 v3255 -v3221 v3146 v2267 -v876 -v410 v4376 -v913 -v880 v4227 -v3258 -v3227 v3144 -v2665 -v2272 -v1079 -v912 -v411 v4226 -v3256 -v2667 -v2534 v2067 -v1128 v959 -v3232 -v2793 v2533 v2275 v2068 -v1863 -v1325 -v1130 -v1085 v920 v785 -v2797 -v2273 v2069 v1136 -v924 -v4522 -v4373 -v3235 -v2661 -v2541 v2085 -v1701 -v1331 v1132 -v1090 v928 v3329 -v3233 -v2545 -v1700 -v1144 v927 -v4528 -v4223 v3330 -v2662 -v2549 -v1415 -v1336 -v1093 -v4405 v3331 -v2923 -v2548 v1997 -v1417 -v1091 v4407 -v3499 v3347 -v2922 -v2513 v1998 -v1339 -v985 v4413 -v4156 -v3588 -v2517 v1999 -v1337 -v989 v4531 v4409 -v4155 -v3609 -v3505 v2930 -v2190 -v2015 v1697 -v1411 v4421 -v3605 -v2934 -v2308 -v4163 -v3604 -v2938 -v2307 -v2196 -v1412 v991 v470 -v4167 -v2937 -v1654 v992 -v474 -v4171 -v3508 -v2425 v2315 -v1656 v844 v4592 -v4170 v3841 v3814 -v2319 v1662 v846 v4591 v3842 -v3683 -v2431 v2323 -v2199 v2166 -v1831 v1658 -v122 v3843 -v3687 v2322 v1670 -v659 -v281 v4599 -v3859 -v3055 -v2169 -v840 -v280 -v128 -v4603 -v2975 -v726 v4607 -v2996 -v2434 v1442 -v841 v728 v288 -v133 v4606 -v2992 v1443 -v734 -v292 -v2991 -v2121 -v2025 -v1438 v1298 v730 -v296 -v227 v136 -v55 v1300 -v741 -v295 -v226 -v134 v59 v3283 -v2124 v2031 -v1436 v3284 -v1296 -v3246 v3148 v1806 v710 -v414 v3251 -v2260 v3247 -v2262 -v875 -v3259 -v3220 -v2666 v2268 -v879 -v3222 -v3145 v2264 -v1810 v781 -v3228 v2276 -v1078 -v914 -v4518 -v4058 -v3224 -v2792 -v2088 -v1080 -v915 v784 -v3236 -v2796 v2535 -v2089 -v1324 -v1131 -v1086 v916 -v4524 v2536 -v2084 -v1326 v1152 -v1082 -v932 v2537 -v1416 -v1332 -v1148 -v1094 -v979 -v4529 v3495 -v3350 -v2553 -v2082 -v1328 -v1147 v978 v3351 -v1340 v4532 -v3606 -v3501 v3346 -v2515 -v2186 -v2018 -v986 v4530 v4408 -v3608 -v2924 v2519 -v2019 -v990 -v4429 -v3506 -v3344 -v2925 -v2192 -v2014 v994 -v4425 -v4157 v2926 v993 -v4436 -v4424 -v4158 -v3602 v3509 -v2942 -v2521 -v2421 -v2197 -v2012 v472 -v4440 -v4159 v3507 -v2522 -v2309 v845 -v476 -v4175 -v3603 -v2427 -v2310 -v2200 -v1827 v2311 -v2198 -v1657 v3862 -v3682 v3051 -v2432 v2327 v2165 -v1830 -v1714 v1678 -v1209 -v478 v4593 v3863 -v3686 -v1674 -v1213 -v479 -v121 v4594 -v3858 v3054 -v2993 -v2435 -v2171 -v1673 v1441 -v123 v4595 -v2995 -v2433 v1440 -v282 -v129 -v4611 -v3856 -v2021 -v283 v125 -v1299 v729 v284 v137 -v3282 -v2989 v2174 -v2120 -v2027 v749 -v300 -v54 -v3281 v745 v58 -v2990 -v2582 -v2126 v2032 -v1437 v744 -v1294 v3149 v1807 v1305 v709 -v415 v3245 -v1309 v3267 -v1811 -v877 v3263 -v2263 -v1809 -v881 -v4054 v3262 v2284 -v2087 v780 -v3223 v2280 -v2086 v4057 v3550 -v3244 -v2794 v2279 v1149 v935 -v883 v786 -v4517 v3554 -v3240 -v2798 v1151 -v1081 v936 -v884 -v4519 -v3349 -v3239 -v2556 -v1102 -v931 -v4525 -v3348 -v2557 v2509 -v1327 -v1098 v4521 -v2800 -v2552 v2508 -v2083 -v2017 -v1348 -v1145 -v1097 -v929 v789 v4533 -v3607 v3494 -v2801 -v2016 -v1344 v980 -v4426 v3496 -v2550 v2516 -v1343 -v1146 v981 -v4428 -v3502 v2520 -v2185 v982 -v466 v3498 -v3345 v2953 v2945 -v2524 -v2187 v998 -v465 v3510 -v2957 v2946 -v2523 -v2193 -v4435 -v4422 -v4178 -v2941 -v2604 -v2451 -v2189 -v2013 v473 -v4439 -v4179 -v2455 -v2420 -v2201 -v477 -v4423 -v4236 -v4174 v3861 -v3728 -v2939 v2422 -v2330 -v2161 -v1826 -v1710 -v1675 -v481 -v4240 v3860 -v2428 -v2331 -v1677 -v480 -v4172 -v3684 v3050 v2424 v2326 v2167 -v1832 -v1713 -v1208 -v3688 -v2994 -v2436 -v1212 -v4614 -v4336 -v3529 v3056 v2324 v2172 -v1671 -v4615 -v4340 -v124 -v4610 -v3857 -v3690 v2175 -v2116 -v1835 -v1672 v746 -v596 v303 -v145 -v3691 v2173 -v2020 v748 -v600 v304 v141 -v4608 v3059 -v2578 -v2122 -v2022 -v299 -v140 -v56 -v2028 v60 v2581 -v2127 v2024 v742 -v297 v2033 -v1295 v3264 v1808 v1304 -v872 v711 v3266 -v1812 v1308 -v2281 -v878 -v776 -v2788 -v2283 -v882 -v4053 -v3260 -v3241 -v2787 v934 v886 v782 -v715 -v3243 v1150 v933 -v885 v4059 v3549 -v3261 -v2795 -v2555 v2277 -v1184 -v1099 v787 v3553 -v2799 -v2554 -v1188 -v1101 -v3237 -v2803 -v2278 -v1345 v790 -v4520 -v2802 -v1347 v788 -v4541 -v4062 -v3238 -v1095 -v930 v4537 -v4427 v2510 v4552 -v4536 v2944 -v2551 v2511 -v1341 -v1096 -v1001 v3497 v2943 v2512 v1002 -v4177 -v3518 v2952 -v2600 -v2528 -v1342 v997 -v156 -v4176 v3514 -v2956 -v2188 -v467 v4437 -v3724 v3513 -v2603 -v2450 -v2356 -v2329 -v2209 -v1822 -v995 v468 v4441 -v3678 -v2454 -v2360 -v2328 -v2205 -v1676 v469 v4235 -v3727 -v3677 -v3046 -v2940 -v2709 -v2204 -v1828 -v1709 -v485 -v4239 -v2713 v2423 -v2160 -v4613 -v4443 -v4173 -v3685 -v3525 v3052 v2444 v2162 -v1833 -v1715 -v1210 -v4612 -v4444 -v3689 -v2440 v2168 -v1214 -v4335 -v3693 -v3528 v3057 -v2439 -v2325 v2164 -v1836 v1479 v302 -v142 -v4339 -v3692 v2176 -v1834 -v747 v301 -v144 -v50 v3060 v1718 -v1216 -v595 -v550 -v49 v3058 -v2115 -v1217 -v599 -v4609 -v2577 -v2117 -v138 -v57 -v2123 v2023 v61 v2583 -v2119 v2041 v743 -v298 -v139 v62 -v2128 -v2037 v63 v3265 -v1820 v1306 v712 -v2282 -v1816 v1310 v871 -v4049 -v1815 v873 -v716 -v3242 v874 v775 -v714 -v4055 v1312 v890 v777 -v2789 v1313 -v1100 v783 v4060 v3551 -v2790 -v1183 v779 v3555 -v2791 -v1346 -v1187 v791 -v4538 v4063 -v2807 -v4540 -v4061 -v4548 v3557 v1524 -v1000 v3558 -v1528 -v999 v4551 -v4534 -v3515 -v2531 -v1599 v152 -v4431 -v3517 v2532 -v4535 -v4430 v2954 -v2625 -v2599 -v2527 -v2206 -v155 v2958 v2629 -v2208 v4438 -v3723 -v3511 -v2605 -v2525 -v2452 -v2355 -v1705 -v996 -v488 v4442 v2456 -v2359 -v1821 -v1204 -v489 -v4446 v4237 v3729 -v3512 -v2960 -v2708 -v2441 -v2202 -v1823 v1711 -v1203 -v484 -v4445 v4241 -v3679 -v3045 -v2961 -v2712 v2443 -v1829 -v3680 -v3524 v3047 -v2860 -v2608 -v2458 -v2203 -v1825 -v1716 -v1475 -v1211 -v482 -v3681 v3053 -v2459 v2163 -v1837 -v1215 -v143 -v4337 -v4243 -v3732 -v3697 -v3530 v3049 -v2437 v2184 v1719 v1478 -v1219 -v546 -v4341 -v4244 v3061 v2180 v1717 -v1218 -v2573 -v2438 v2179 -v597 -v549 -v601 -v51 -v4343 v3533 -v2579 v2038 -v52 -v4344 -v2118 v2040 v53 v2584 -v2136 v901 v603 v67 -v2132 -v2036 -v905 v604 v2731 -v1819 v1307 v713 v2735 v1311 -v717 -v1813 v1315 v893 -v4048 -v3545 v1314 v894 -v4050 -v3544 -v1814 v889 -v4056 v778 v4052 v3552 -v2810 -v1185 -v887 v799 -v4539 v4064 v3556 -v2811 -v1189 -v795 v3560 -v2806 -v794 v3559 -v4547 -v2804 -v2530 -v1595 v1523 v1191 -v3516 v2948 -v2529 -v1527 -v1192 v4553 -v4502 v2947 -v2595 -v1598 v151 v2446 -v2207 -v3719 v2955 -v2624 -v2601 v2445 -v487 -v157 -v4432 -v4231 v2959 v2628 -v486 -v4556 v4433 -v4230 -v3870 -v3725 v2963 -v2606 -v2526 -v2453 -v2357 v4434 -v3874 v2962 v2457 -v2442 v2361 -v1704 -v4450 v4238 v3730 -v3520 -v2856 -v2710 v2609 -v2461 -v1706 -v160 -v4331 v4242 -v2714 -v2607 -v2460 -v1824 v1712 -v1205 -v4330 v4246 v3733 -v3700 -v3526 -v2859 -v2363 -v2181 -v1845 v1708 -v1474 -v1206 -v1113 -v483 v4245 -v3731 -v3701 v3048 -v2364 v2183 -v1841 v1720 -v1207 -v591 -v4338 -v3696 -v3531 -v3069 -v2716 -v1840 v1480 -v1223 -v590 -v545 -v4342 -v3065 -v2717 -v4346 -v3694 v3534 -v3064 -v2177 -v1159 -v598 -v551 -v4345 v3532 -v2572 -v2039 -v1163 -v602 -v2574 -v2178 -v2143 -v2133 -v1483 v606 -v70 v2580 -v2147 -v2135 v605 -v71 v2576 v900 v697 -v554 v66 v2585 -v2131 -v2034 -v904 v2730 v2684 -v1817 -v1303 v892 -v725 v2734 v2688 v1302 v891 -v721 -v2050 -v1548 -v1319 -v720 -v1552 -v1179 -v2809 v1178 v796 -v4051 v3546 -v2808 v798 v4072 v3547 -v1186 -v888 v4068 v3548 v1190 -v4543 v4067 -v3564 v1194 -v792 v1193 -v4549 -v4498 -v2805 -v1594 v1525 -v793 -v147 -v1529 v4554 -v4501 v1600 v153 v2949 -v2594 -v2351 -v4557 -v4473 v2950 -v2626 v2596 -v2350 -v1531 -v158 -v4555 -v4477 -v3718 v2951 -v2704 v2630 v2602 v2447 -v1532 -v4453 -v3869 -v3720 -v2967 -v2703 v2598 v2448 -v2358 -v1603 -v161 -v4454 -v4232 -v3873 -v3726 v2610 v2449 v2362 -v159 -v4449 -v4233 v3722 -v3699 -v2855 -v2711 -v2632 v2465 v2366 -v1842 -v1470 -v1109 v4234 v3734 -v3698 -v3519 -v2715 -v2633 v2365 -v2182 -v1844 -v1707 -v4447 -v4250 v3521 -v3066 -v2861 -v2719 -v1728 v1476 -v1226 -v1112 -v541 -v4332 -v3527 -v3068 -v2718 v1724 -v1227 -v4333 v3523 -v1838 v1723 v1481 -v1222 -v547 v4334 v3535 -v592 -v4350 -v3695 -v3409 -v3062 v2864 -v1839 -v1484 -v1220 -v1158 -v593 -v552 -v69 -v2134 -v1482 -v1162 v594 -v68 -v3063 -v2476 -v2142 -v693 v610 v555 -v2575 -v2480 -v2146 v553 -v3616 -v2593 v902 v696 v64 -v3620 -v2589 -v2129 -v2035 -v906 -v3820 v2732 v2683 -v2046 -v1818 v1322 -v724 v3824 v2736 v2687 v1323 -v3201 -v2049 -v1547 -v1318 -v718 -v3205 -v1551 v797 -v4069 -v2738 -v1316 -v719 -v4071 -v2739 v1180 v3567 -v2241 v1181 v3568 -v2245 v1519 v1182 v4065 -v3563 v1590 v1518 v1198 -v4542 v4544 -v4497 -v4066 -v3561 v1596 v1526 -v500 -v4550 -v2620 -v1530 -v146 v4546 v4503 -v2619 v1601 v1534 -v148 -v4558 v1533 v154 -v4472 -v4452 v2970 -v2627 -v1604 v150 -v4476 -v4451 v2971 v2631 v2597 -v2352 -v1602 -v162 -v4506 -v3871 -v2966 -v2851 v2635 -v2618 v2468 v2353 v3875 -v3721 v2705 v2634 -v2614 v2469 v2354 -v1843 -v4253 v3742 -v3362 -v2964 -v2857 v2706 -v2613 -v2464 -v2370 -v1725 -v1225 -v1108 v4254 v3738 -v3067 v2707 -v1727 -v1469 -v1224 -v4448 -v4249 -v3877 -v3737 v2862 v2723 -v2462 -v1471 -v1114 -v3878 v3522 v1477 -v540 v4353 -v4247 v3543 -v3405 v2865 -v1721 v1473 -v542 v4354 -v3539 v2863 v1485 -v548 -v4349 -v3538 v3408 -v1722 -v1221 -v1160 -v1117 v613 v544 -v1164 v896 v614 v556 -v4347 -v2590 -v2475 -v2144 v895 -v692 v609 -v2592 -v2479 -v2148 -v3615 v1166 v903 v698 v607 v65 -v3619 -v2588 -v2130 v1167 v907 -v3819 v2733 v2685 -v2045 v1320 -v722 v3823 v2737 v2689 -v3200 v2741 -v2051 -v1549 -v856 -v4070 -v3204 -v2740 v1553 v3566 v2691 -v1317 v3565 -v2692 -v2240 -v2054 v1555 v1201 -v2244 v1556 v1202 -v4493 v1197 -v496 v1589 v1520 v4499 -v3562 v1591 v1521 v1195 -v499 v4545 v1597 v1522 v4566 v4504 -v3753 v2969 v1593 -v1538 v4562 -v3865 v2968 -v2621 v1605 -v149 v4561 v4507 -v4474 -v3864 -v2622 -v2615 v2467 -v450 -v170 -v4505 -v4478 v2623 -v2617 v2466 -v166 -v4252 v3872 v3739 -v3358 v2639 -v2373 v1104 -v165 -v4251 v3876 v3741 -v2850 -v2374 -v1726 -v4480 v3880 -v3361 -v2965 v2852 v2726 -v2611 -v2369 -v1110 -v4481 v3879 v2858 v2727 v4352 -v3735 -v3540 v2854 v2722 -v2612 -v2463 -v2367 -v1735 v1115 v4351 -v3542 v2866 -v1739 -v1472 -v1154 -v4248 -v3736 -v3404 v2720 v1493 -v1153 -v1118 -v612 -v2138 v1489 -v1116 -v611 -v543 -v3536 v3410 -v2822 -v2137 -v1488 -v1161 v688 -v564 -v2591 -v1165 -v560 -v4348 -v3537 -v2477 -v2145 v1169 -v694 -v559 -v2481 -v2149 v1168 v897 -v3617 v3413 -v2150 v898 v699 -v608 -v3621 -v2586 -v2151 v899 -v4030 -v3821 -v2729 v2686 -v2047 v1544 v1321 -v852 -v723 -v4034 v3825 v2728 v2690 -v3202 v2745 v2694 -v2052 -v1550 -v855 v3206 v2693 v1554 -v3827 -v2055 v1558 v1200 -v3828 -v2053 v1557 v1199 -v3208 v2242 -v3209 -v2246 -v495 -v4492 -v4563 v4494 -v3749 -v2248 v1541 -v1196 -v501 -v4565 v4500 -v4468 -v2249 v1592 v1542 -v4577 v4496 -v4467 -v3752 v1613 -v1537 v446 -v167 v4508 -v2616 -v1609 -v169 -v4559 -v4475 v2642 -v2372 -v1608 -v1535 -v504 -v449 -v4479 v3866 v3740 v2643 -v2371 -v4560 v4483 v3867 -v3357 -v2725 v2638 -v163 -v4482 v3868 -v2724 v1103 v3884 v3363 -v2636 v1105 -v164 -v3541 v2853 -v1111 -v3400 v2874 -v2368 -v1734 -v1490 v1107 -v2870 v1738 v1492 -v1119 -v3406 -v3366 -v2869 -v2818 v2721 -v561 v107 -v2471 -v1155 -v563 -v4097 v3411 -v2821 -v2470 -v1486 -v1156 -v4101 -v3611 -v2139 v1157 v687 v3610 v3414 -v2478 -v2140 -v1487 v1173 v689 -v557 v3412 -v2482 -v2141 -v695 -v3618 -v2483 -v2155 v910 v691 -v558 v3622 -v2587 -v2484 v911 -v700 -v4029 -v3822 v3197 -v2751 v2748 -v2682 -v2043 v851 -v4033 v3826 v2749 v2681 -v2048 v1543 -v3830 -v3203 v2744 -v2698 -v2044 v1545 v857 -v3829 v3207 -v2236 -v2056 v1546 v3211 -v2742 -v2235 v1562 v3210 v2243 -v860 -v491 v2247 v2251 v1540 -v497 -v4564 v2250 v1539 -v4573 -v3748 -v1610 -v1378 -v502 v4495 v1612 v1382 -v168 -v4576 v4516 v3754 -v2641 -v505 v445 v4512 v4469 -v2640 -v503 v4511 v4470 v3353 -v1606 -v1536 -v451 v4471 v4487 v3887 -v3757 -v3359 -v1607 v3888 v3883 v3364 -v2871 -v2637 v454 -v424 -v2873 -v1491 v1106 -v428 v3881 -v3434 -v3367 -v1736 v1127 -v103 v3399 -v3365 v1740 v1123 -v562 v3401 -v3162 -v2867 -v2817 v1122 v106 -v3407 -v4096 v3403 -v2868 -v2823 -v1742 -v1176 -v4100 v3415 -v2472 -v1743 -v1177 -v2473 -v2158 v1172 -v909 v3612 -v2474 -v2159 -v908 v690 v3712 v3613 -v2826 -v2488 -v2154 v1170 v708 v3614 -v704 -v4031 -v3818 -v2750 v2746 -v2701 v853 -v4035 v3817 v3196 v2702 -v2042 v3834 v3198 -v2697 -v2064 v1565 v858 v3199 -v2060 v1566 -v4037 v3215 -v2743 -v2695 -v2059 v1926 v1561 -v861 -v4038 v2237 -v859 v2501 v2238 v1559 v2239 -v490 v3744 v2255 v492 -v1611 v498 -v4572 -v4513 -v3750 -v1377 v1257 v494 -v441 -v4515 v1381 -v506 -v4578 v3755 v447 v4509 -v4490 -v3886 -v3758 -v452 v4491 -v3885 -v3756 v3352 -v4581 v4510 v4486 v3354 v455 -v3360 -v2872 -v1730 v453 v4484 -v3430 v3356 -v1729 v1124 -v423 v3368 v1126 -v427 v3882 -v3433 -v3158 v2813 v1737 -v102 v1741 -v3161 v2819 v1745 -v1175 -v1120 v108 v3402 v1744 -v1174 -v4098 -v3423 v2824 -v2157 -v1121 -v971 v4102 v3419 -v2156 -v3967 v3708 v3418 -v2827 -v2491 -v705 -v111 -v3971 -v2825 -v2492 -v707 v4104 v3711 -v3625 v2846 -v2487 -v2152 v1171 v4105 -v3626 -v703 -v4032 v3837 -v2752 -v2747 -v2699 -v2061 v1564 v849 v4036 v3838 -v2063 v1563 v854 -v4040 v3833 v3218 -v1922 v850 -v4039 v3219 v862 -v3831 v3214 -v2756 -v2696 -v2497 -v2057 v1925 -v3212 v2500 v2258 -v2058 v1560 v2259 -v4568 v2254 -v1253 -v4514 v3743 v493 -v4574 v3745 -v2252 -v1379 v1256 v514 -v3751 v1383 -v510 -v440 v4579 -v4489 v3747 -v509 -v442 -v4488 -v3759 v448 -v4582 v1385 v444 -v4580 v1386 v456 v3355 v1125 v4485 -v3429 v3376 -v425 -v98 -v3372 -v1731 -v429 -v3435 -v3371 -v3157 v1732 -v104 -v4092 v2812 v1733 -v4091 -v3420 -v3163 v2814 v1749 -v967 -v431 v109 -v3422 v2820 -v432 -v4099 v3438 v2816 -v2490 -v970 -v112 v4103 v2828 -v2489 -v706 -v110 v4107 -v3966 v3707 -v3624 v3416 -v3166 -v2842 v4106 -v3970 -v3623 v3713 v3417 v2845 -v2485 -v2153 -v701 -v4028 v3835 v3217 -v2753 -v2700 -v2062 v4027 v3216 v848 v4044 v2757 -v1921 v870 v2755 v866 -v3832 v2496 v2257 v1927 v865 v2256 -v3213 v2502 -v1373 v1930 -v1372 v1252 v511 -v4567 v513 -v4569 v2505 -v2253 -v1380 v1258 v4575 v3746 v1384 v4571 v3767 v1388 -v507 -v4583 -v3763 v1387 -v443 -v3762 v1261 -v508 -v464 v460 v419 v3425 v3373 -v459 v418 v3375 v3431 -v3153 -v426 v430 -v97 -v3436 -v3369 v3159 -v1752 -v434 -v99 -v3421 -v1753 -v433 v105 v3439 -v3370 v3164 v1748 -v966 v101 -v4093 v3437 v2815 -v113 -v4094 v3703 -v3167 v2836 -v1746 -v972 v4095 -v3165 -v2832 v4111 -v3968 v3709 -v2841 -v2831 v3972 v3714 v2847 -v2486 -v975 -v702 v4045 v3836 v2754 -v1920 v867 v4047 v2758 v869 v4043 -v2495 -v1923 v4041 v2498 v1928 -v863 v2503#### 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): 1.01 1.00 0.92 2/54 3586
Raw data (stat): 3586 (runsolver) R 3585 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481966866 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+10 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 11769 0 0 0 970 28 0 0 25 0 1 0 481966866 51011584 10366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12454 10366 603 41 0 12413 0
vsize: 49816
[startup+20.0002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 11810 0 0 0 1970 28 0 0 25 0 1 0 481966866 51146752 10407 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12487 10407 603 41 0 12446 0
vsize: 49948
[startup+30.0009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 11844 0 0 0 2970 28 0 0 25 0 1 0 481966866 51281920 10441 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12520 10441 603 41 0 12479 0
vsize: 50080
[startup+40.0007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 11943 0 0 0 3968 29 0 0 25 0 1 0 481966866 51683328 10540 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12618 10540 603 41 0 12577 0
vsize: 50472
[startup+50.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 12354 0 0 0 4968 30 0 0 25 0 1 0 481966866 53374976 10951 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13031 10951 603 41 0 12990 0
vsize: 52124
[startup+60.0006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 12425 0 0 0 5967 30 0 0 25 0 1 0 481966866 53645312 11022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13097 11022 603 41 0 13056 0
vsize: 52388
[startup+70.0006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 12681 0 0 0 6967 31 0 0 25 0 1 0 481966866 54853632 11278 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13392 11278 603 41 0 13351 0
vsize: 53568
[startup+80.0008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 12946 0 0 0 7966 32 0 0 25 0 1 0 481966866 55709696 11483 4294967295 134512640 134672761 3221224544 3221223728 134593788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13601 11483 603 41 0 13560 0
vsize: 54404
[startup+90.0004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 12949 0 0 0 8966 32 0 0 25 0 1 0 481966866 55558144 11476 4294967295 134512640 134672761 3221224544 3221223800 134562229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13564 11476 603 41 0 13523 0
vsize: 54256
[startup+100.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 13055 0 0 0 9967 32 0 0 25 0 1 0 481966866 55959552 11582 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13662 11582 603 41 0 13621 0
vsize: 54648
[startup+110.002 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 13294 0 0 0 10966 33 0 0 25 0 1 0 481966866 56905728 11821 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13893 11821 603 41 0 13852 0
vsize: 55572
[startup+120.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 13350 0 0 0 11966 33 0 0 25 0 1 0 481966866 57176064 11877 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 11877 603 41 0 13918 0
vsize: 55836
[startup+130.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 13419 0 0 0 12966 33 0 0 25 0 1 0 481966866 57311232 11946 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13992 11946 603 41 0 13951 0
vsize: 55968
[startup+140.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 13553 0 0 0 13966 34 0 0 25 0 1 0 481966866 57851904 12080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14124 12080 603 41 0 14083 0
vsize: 56496
[startup+150.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 14198 0 0 0 14963 36 0 0 25 0 1 0 481966866 60796928 12725 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14843 12725 603 41 0 14802 0
vsize: 59372
[startup+160.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 14874 0 0 0 15962 37 0 0 25 0 1 0 481966866 63492096 13401 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15501 13401 603 41 0 15460 0
vsize: 62004
[startup+170.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 14980 0 0 0 16962 37 0 0 25 0 1 0 481966866 63897600 13507 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15600 13507 603 41 0 15559 0
vsize: 62400
[startup+180.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15210 0 0 0 17962 37 0 0 25 0 1 0 481966866 64024576 13550 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15631 13550 603 41 0 15590 0
vsize: 62524
[startup+190 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15210 0 0 0 18962 37 0 0 25 0 1 0 481966866 64024576 13550 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15631 13550 603 41 0 15590 0
vsize: 62524
[startup+200.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15210 0 0 0 19962 37 0 0 25 0 1 0 481966866 64024576 13550 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15631 13550 603 41 0 15590 0
vsize: 62524
[startup+210.001 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15291 0 0 0 20962 38 0 0 25 0 1 0 481966866 64024576 13551 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15631 13551 603 41 0 15590 0
vsize: 62524
[startup+220 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15291 0 0 0 21962 38 0 0 25 0 1 0 481966866 64024576 13551 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15631 13551 603 41 0 15590 0
vsize: 62524
[startup+230 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15291 0 0 0 22962 38 0 0 25 0 1 0 481966866 64024576 13551 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15631 13551 603 41 0 15590 0
vsize: 62524
[startup+239.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15291 0 0 0 23962 38 0 0 25 0 1 0 481966866 64024576 13551 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15631 13551 603 41 0 15590 0
vsize: 62524
[startup+250 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15291 0 0 0 24963 38 0 0 25 0 1 0 481966866 64024576 13551 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15631 13551 603 41 0 15590 0
vsize: 62524
[startup+260 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15291 0 0 0 25963 38 0 0 25 0 1 0 481966866 64024576 13551 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15631 13551 603 41 0 15590 0
vsize: 62524
[startup+269.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15291 0 0 0 26963 38 0 0 25 0 1 0 481966866 64024576 13551 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15631 13551 603 41 0 15590 0
vsize: 62524
[startup+279.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15730 0 0 0 27962 39 0 0 25 0 1 0 481966866 65904640 13990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16090 13990 603 41 0 16049 0
vsize: 64360
[startup+289.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 15909 0 0 0 28961 39 0 0 25 0 1 0 481966866 66580480 14169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16255 14169 603 41 0 16214 0
vsize: 65020
[startup+299.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 16572 0 0 0 29960 41 0 0 25 0 1 0 481966866 69406720 14832 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16945 14832 603 41 0 16904 0
vsize: 67780
[startup+309.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 17368 0 0 0 30958 44 0 0 25 0 1 0 481966866 72626176 15628 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17731 15628 603 41 0 17690 0
vsize: 70924
[startup+319.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 17642 0 0 0 31957 44 0 0 25 0 1 0 481966866 73703424 15902 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17994 15902 603 41 0 17953 0
vsize: 71976
[startup+329.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 18101 0 0 0 32955 46 0 0 25 0 1 0 481966866 75587584 16361 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18454 16361 603 41 0 18413 0
vsize: 73816
[startup+339.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 18677 0 0 0 33953 49 0 0 25 0 1 0 481966866 77877248 16937 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19013 16937 603 41 0 18972 0
vsize: 76052
[startup+350 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 19472 0 0 0 34951 51 0 0 25 0 1 0 481966866 81121280 17732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19805 17732 603 41 0 19764 0
vsize: 79220
[startup+360 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 19920 0 0 0 35949 53 0 0 25 0 1 0 481966866 82878464 18180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20234 18180 603 41 0 20193 0
vsize: 80936
[startup+369.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 20669 0 0 0 36948 55 0 0 25 0 1 0 481966866 86503424 18929 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21119 18930 603 41 0 21078 0
vsize: 84476
[startup+379.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 21575 0 0 0 37946 57 0 0 25 0 1 0 481966866 90128384 19835 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22004 19835 603 41 0 21963 0
vsize: 88016
[startup+389.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 22719 0 0 0 38943 60 0 0 25 0 1 0 481966866 94769152 20979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23137 20979 603 41 0 23096 0
vsize: 92548
[startup+400 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 23769 0 0 0 39940 63 0 0 25 0 1 0 481966866 99151872 22029 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24207 22029 603 41 0 24166 0
vsize: 96828
[startup+410.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 24769 0 0 0 40940 64 0 0 25 0 1 0 481966866 103247872 23029 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25207 23029 603 41 0 25166 0
vsize: 100828
[startup+420.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 25477 0 0 0 41937 67 0 0 25 0 1 0 481966866 106065920 23737 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25895 23737 603 41 0 25854 0
vsize: 103580
[startup+430.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 26037 0 0 0 42937 68 0 0 25 0 1 0 481966866 108359680 24297 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26455 24298 603 41 0 26414 0
vsize: 105820
[startup+440.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 26993 0 0 0 43934 70 0 0 25 0 1 0 481966866 112250880 25253 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27405 25254 603 41 0 27364 0
vsize: 109620
[startup+450.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 27963 0 0 0 44932 73 0 0 25 0 1 0 481966866 116318208 26223 4294967295 134512640 134672761 3221224544 3221223728 134558771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28398 26223 603 41 0 28357 0
vsize: 113592
[startup+460.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 28759 0 0 0 45931 74 0 0 25 0 1 0 481966866 119570432 27019 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29192 27019 603 41 0 29151 0
vsize: 116768
[startup+470.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 29378 0 0 0 46930 75 0 0 25 0 1 0 481966866 122114048 27638 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29813 27638 603 41 0 29772 0
vsize: 119252
[startup+480.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 29549 0 0 0 47929 76 0 0 25 0 1 0 481966866 122785792 27809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29977 27809 603 41 0 29936 0
vsize: 119908
[startup+490.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 29719 0 0 0 48928 77 0 0 25 0 1 0 481966866 123461632 27979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30142 27979 603 41 0 30101 0
vsize: 120568
[startup+500.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 30085 0 0 0 49927 78 0 0 25 0 1 0 481966866 124944384 28345 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30504 28345 603 41 0 30463 0
vsize: 122016
[startup+510.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 30493 0 0 0 50926 80 0 0 25 0 1 0 481966866 126550016 28753 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30896 28753 603 41 0 30855 0
vsize: 123584
[startup+520.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 31105 0 0 0 51925 81 0 0 25 0 1 0 481966866 128966656 29365 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31486 29365 603 41 0 31445 0
vsize: 125944
[startup+530.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 31555 0 0 0 52924 82 0 0 25 0 1 0 481966866 130854912 29815 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31947 29815 603 41 0 31906 0
vsize: 127788
[startup+540.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 31795 0 0 0 53924 83 0 0 25 0 1 0 481966866 131796992 30055 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32177 30055 603 41 0 32136 0
vsize: 128708
[startup+550.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 32146 0 0 0 54923 84 0 0 25 0 1 0 481966866 133279744 30406 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32539 30406 603 41 0 32498 0
vsize: 130156
[startup+560.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 32267 0 0 0 55923 84 0 0 25 0 1 0 481966866 133685248 30527 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32638 30527 603 41 0 32597 0
vsize: 130552
[startup+570.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 32505 0 0 0 56922 85 0 0 25 0 1 0 481966866 134631424 30765 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32869 30765 603 41 0 32828 0
vsize: 131476
[startup+580.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 32869 0 0 0 57921 86 0 0 25 0 1 0 481966866 136114176 31129 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33231 31129 603 41 0 33190 0
vsize: 132924
[startup+590.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 33264 0 0 0 58920 88 0 0 25 0 1 0 481966866 137732096 31524 4294967295 134512640 134672761 3221224544 3221223728 134558841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33626 31524 603 41 0 33585 0
vsize: 134504
[startup+600.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 33621 0 0 0 59920 88 0 0 25 0 1 0 481966866 139079680 31881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33955 31881 603 41 0 33914 0
vsize: 135820
[startup+610.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 34188 0 0 0 60918 90 0 0 25 0 1 0 481966866 141488128 32448 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34543 32448 603 41 0 34502 0
vsize: 138172
[startup+620.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 34799 0 0 0 61917 91 0 0 25 0 1 0 481966866 143908864 33059 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35134 33059 603 41 0 35093 0
vsize: 140536
[startup+630.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 35315 0 0 0 62916 92 0 0 25 0 1 0 481966866 146051072 33575 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35657 33575 603 41 0 35616 0
vsize: 142628
[startup+640.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 35785 0 0 0 63915 93 0 0 25 0 1 0 481966866 147931136 34045 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36116 34045 603 41 0 36075 0
vsize: 144464
[startup+650.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 36270 0 0 0 64914 94 0 0 25 0 1 0 481966866 149942272 34530 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36607 34530 603 41 0 36566 0
vsize: 146428
[startup+660.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 36704 0 0 0 65914 96 0 0 25 0 1 0 481966866 151691264 34964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37034 34964 603 41 0 36993 0
vsize: 148136
[startup+670.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 37138 0 0 0 66912 97 0 0 25 0 1 0 481966866 153444352 35398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37462 35398 603 41 0 37421 0
vsize: 149848
[startup+680.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 37576 0 0 0 67911 98 0 0 25 0 1 0 481966866 156246016 35836 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38146 35836 603 41 0 38105 0
vsize: 152584
[startup+690.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 37956 0 0 0 68911 99 0 0 25 0 1 0 481966866 157855744 36216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38539 36216 603 41 0 38498 0
vsize: 154156
[startup+700.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 38318 0 0 0 69910 100 0 0 25 0 1 0 481966866 159318016 36578 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38896 36578 603 41 0 38855 0
vsize: 155584
[startup+710.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 38703 0 0 0 70909 101 0 0 25 0 1 0 481966866 160935936 36963 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39291 36963 603 41 0 39250 0
vsize: 157164
[startup+720.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 39080 0 0 0 71908 102 0 0 25 0 1 0 481966866 162439168 37340 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39658 37340 603 41 0 39617 0
vsize: 158632
[startup+730.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 39425 0 0 0 72907 104 0 0 25 0 1 0 481966866 163778560 37685 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39985 37685 603 41 0 39944 0
vsize: 159940
[startup+740.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 39769 0 0 0 73906 104 0 0 25 0 1 0 481966866 165253120 38029 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40345 38029 603 41 0 40304 0
vsize: 161380
[startup+750.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 40108 0 0 0 74906 105 0 0 25 0 1 0 481966866 166596608 38368 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40673 38368 603 41 0 40632 0
vsize: 162692
[startup+760.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 40476 0 0 0 75905 106 0 0 25 0 1 0 481966866 168062976 38736 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41031 38736 603 41 0 40990 0
vsize: 164124
[startup+770.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 40859 0 0 0 76905 106 0 0 25 0 1 0 481966866 169668608 39119 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41423 39119 603 41 0 41382 0
vsize: 165692
[startup+780.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 41239 0 0 0 77904 107 0 0 25 0 1 0 481966866 171282432 39499 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41817 39499 603 41 0 41776 0
vsize: 167268
[startup+790.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 41587 0 0 0 78903 109 0 0 25 0 1 0 481966866 172634112 39847 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42147 39847 603 41 0 42106 0
vsize: 168588
[startup+800.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 41973 0 0 0 79902 110 0 0 25 0 1 0 481966866 174247936 40233 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42541 40233 603 41 0 42500 0
vsize: 170164
[startup+810.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 42378 0 0 0 80901 111 0 0 25 0 1 0 481966866 175857664 40638 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42934 40638 603 41 0 42893 0
vsize: 171736
[startup+820.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 42748 0 0 0 81900 112 0 0 25 0 1 0 481966866 177328128 41008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43293 41008 603 41 0 43252 0
vsize: 173172
[startup+830.021 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 43156 0 0 0 82899 114 0 0 25 0 1 0 481966866 179077120 41416 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43720 41416 603 41 0 43679 0
vsize: 174880
[startup+840.02 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 43498 0 0 0 83898 115 0 0 25 0 1 0 481966866 180416512 41758 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44047 41758 603 41 0 44006 0
vsize: 176188
[startup+850.02 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 43695 0 0 0 84897 115 0 0 25 0 1 0 481966866 181223424 41955 4294967295 134512640 134672761 3221224544 3221223600 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44244 41955 603 41 0 44203 0
vsize: 176976
[startup+860.021 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 43994 0 0 0 85897 116 0 0 25 0 1 0 481966866 182431744 42254 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44539 42254 603 41 0 44498 0
vsize: 178156
[startup+870.02 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 44355 0 0 0 86896 117 0 0 25 0 1 0 481966866 183914496 42615 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44901 42615 603 41 0 44860 0
vsize: 179604
[startup+880.02 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 44606 0 0 0 87896 118 0 0 25 0 1 0 481966866 184852480 42866 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45130 42866 603 41 0 45089 0
vsize: 180520
[startup+890.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 44931 0 0 0 88895 119 0 0 25 0 1 0 481966866 186200064 43191 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45459 43191 603 41 0 45418 0
vsize: 181836
[startup+900.019 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 45135 0 0 0 89895 119 0 0 25 0 1 0 481966866 187006976 43395 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45656 43395 603 41 0 45615 0
vsize: 182624
[startup+910.019 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 45440 0 0 0 90894 120 0 0 25 0 1 0 481966866 188338176 43700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 43700 603 41 0 45940 0
vsize: 183924
[startup+920.018 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 45730 0 0 0 91892 121 0 0 25 0 1 0 481966866 189411328 43990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46243 43990 603 41 0 46202 0
vsize: 184972
[startup+930.019 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 45977 0 0 0 92891 122 0 0 25 0 1 0 481966866 190488576 44237 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46506 44237 603 41 0 46465 0
vsize: 186024
[startup+940.019 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 46474 0 0 0 93890 123 0 0 25 0 1 0 481966866 192499712 44734 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46997 44734 603 41 0 46956 0
vsize: 187988
[startup+950.018 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 46840 0 0 0 94889 124 0 0 25 0 1 0 481966866 193978368 45100 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47358 45100 603 41 0 47317 0
vsize: 189432
[startup+960.018 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 47450 0 0 0 95888 126 0 0 25 0 1 0 481966866 196407296 45710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47951 45710 603 41 0 47910 0
vsize: 191804
[startup+970.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 48062 0 0 0 96887 127 0 0 25 0 1 0 481966866 198959104 46322 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48574 46322 603 41 0 48533 0
vsize: 194296
[startup+980.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 48636 0 0 0 97885 129 0 0 25 0 1 0 481966866 201256960 46896 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49135 46896 603 41 0 49094 0
vsize: 196540
[startup+990.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 49161 0 0 0 98884 130 0 0 25 0 1 0 481966866 203436032 47421 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49667 47421 603 41 0 49626 0
vsize: 198668
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 49759 0 0 0 99882 132 0 0 25 0 1 0 481966866 205856768 48019 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50258 48019 603 41 0 50217 0
vsize: 201032
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 50296 0 0 0 100881 133 0 0 25 0 1 0 481966866 208007168 48556 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50783 48556 603 41 0 50742 0
vsize: 203132
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 50808 0 0 0 101880 135 0 0 25 0 1 0 481966866 210153472 49068 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51307 49068 603 41 0 51266 0
vsize: 205228
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 51342 0 0 0 102878 137 0 0 25 0 1 0 481966866 212312064 49602 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51834 49602 603 41 0 51793 0
vsize: 207336
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 51844 0 0 0 103877 138 0 0 25 0 1 0 481966866 214466560 50104 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52360 50104 603 41 0 52319 0
vsize: 209440
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 52321 0 0 0 104877 139 0 0 25 0 1 0 481966866 216379392 50581 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52827 50581 603 41 0 52786 0
vsize: 211308
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 52803 0 0 0 105876 140 0 0 25 0 1 0 481966866 218402816 51063 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53321 51063 603 41 0 53280 0
vsize: 213284
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 53249 0 0 0 106874 142 0 0 25 0 1 0 481966866 220160000 51509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53750 51509 603 41 0 53709 0
vsize: 215000
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 53696 0 0 0 107873 143 0 0 25 0 1 0 481966866 222044160 51956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54210 51956 603 41 0 54169 0
vsize: 216840
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 54108 0 0 0 108872 144 0 0 25 0 1 0 481966866 223637504 52368 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54599 52368 603 41 0 54558 0
vsize: 218396
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 54495 0 0 0 109871 145 0 0 25 0 1 0 481966866 225234944 52755 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54989 52755 603 41 0 54948 0
vsize: 219956
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 54885 0 0 0 110870 146 0 0 25 0 1 0 481966866 226848768 53145 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55383 53145 603 41 0 55342 0
vsize: 221532
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 55346 0 0 0 111869 147 0 0 25 0 1 0 481966866 228814848 53606 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55863 53606 603 41 0 55822 0
vsize: 223452
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 55742 0 0 0 112869 148 0 0 25 0 1 0 481966866 230436864 54002 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56259 54002 603 41 0 56218 0
vsize: 225036
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 56149 0 0 0 113867 150 0 0 25 0 1 0 481966866 232058880 54409 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56655 54409 603 41 0 56614 0
vsize: 226620
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 56539 0 0 0 114866 151 0 0 25 0 1 0 481966866 233668608 54799 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57048 54799 603 41 0 57007 0
vsize: 228192
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 56945 0 0 0 115865 152 0 0 25 0 1 0 481966866 235290624 55205 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57444 55205 603 41 0 57403 0
vsize: 229776
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 57322 0 0 0 116864 153 0 0 25 0 1 0 481966866 236769280 55582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57805 55582 603 41 0 57764 0
vsize: 231220
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 57710 0 0 0 117863 154 0 0 25 0 1 0 481966866 238419968 55970 4294967295 134512640 134672761 3221224544 3221223648 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58208 55970 603 41 0 58167 0
vsize: 232832
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 58124 0 0 0 118863 155 0 0 25 0 1 0 481966866 240041984 56384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58604 56384 603 41 0 58563 0
vsize: 234416
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3586
Raw data (stat): 3586 (minisat+) R 3585 28099 28098 0 -1 0 58538 0 0 0 119862 156 0 0 25 0 1 0 481966866 241823744 56798 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59039 56798 603 41 0 58998 0
vsize: 236156
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 3586
Raw data (stat): 3586 (minisat+) Z 3585 28099 28098 0 -1 12 58541 0 0 0 119862 167 0 0 25 0 1 0 481966866 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.14
CPU time (s): 1200.3
CPU user time (s): 1198.63
CPU system time (s): 1.67674
CPU usage (%): 100.014
Max. virtual memory (Kb): 236156
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####