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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.95:100.opb
MD5SUMac4ddb996334a0834a018e09e97d1ecb
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers14
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.06984
Number of variables4617
Total number of constraints9896
Number of constraints which are clauses4395
Number of constraints which are cardinality constraints (but not clauses)5501
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint23

Trace number 5099

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        920676 kB
Buffers:         34224 kB
Cached:          60108 kB
SwapCached:        392 kB
Active:          52308 kB
Inactive:        45328 kB
HighTotal:      131008 kB
HighFree:        66976 kB
LowTotal:       903652 kB
LowFree:        853700 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10892 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:16:22 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3326 7 1200.21 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 |   63540   182818 |   21180       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 5397
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11317   maxlim: 2659   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  142680   465444 |   47560       0        0     nan |  0.000 % |
c |       100 |  142680   465444 |   52316     100      307     3.1 |  2.143 % |
c |       250 |  142680   465444 |   57547     250      780     3.1 |  2.143 % |
c |       475 |  142680   465444 |   63302     475     1572     3.3 |  2.143 % |
c |       812 |  142680   465444 |   69632     812     2952     3.6 |  2.143 % |
c |      1318 |  142680   465444 |   76595    1318     5235     4.0 |  2.143 % |
c |      2077 |  142680   465444 |   84255    2077     9702     4.7 |  2.143 % |
c |      3216 |  142680   465444 |   92680    3216    16502     5.1 |  2.143 % |
c |      4924 |  142671   465413 |  101949    4922    27447     5.6 |  2.145 % |
c |      7486 |  142671   465413 |  112143    7484    43366     5.8 |  2.145 % |
c |     11330 |  142671   465413 |  123358   11328    73565     6.5 |  2.145 % |
c |     17096 |  142671   465413 |  135694   17094   124776     7.3 |  2.145 % |
c ==============================================================================
c Found solution: 967
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 7089   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20219 |  142706   465566 |   47568   20217   166453     8.2 |  2.145 % |
c |     20319 |  142706   465566 |   52324   20317   167092     8.2 |  2.164 % |
c |     20469 |  142706   465566 |   57557   20467   168370     8.2 |  2.164 % |
c |     20694 |  142706   465566 |   63313   20692   169843     8.2 |  2.164 % |
c |     21031 |  142706   465566 |   69644   21029   172451     8.2 |  2.164 % |
c |     21537 |  142697   465535 |   76608   21530   176108     8.2 |  2.166 % |
c |     22296 |  142697   465535 |   84269   22289   181749     8.2 |  2.166 % |
c |     23435 |  142697   465535 |   92696   23428   192338     8.2 |  2.166 % |
c |     25143 |  142697   465535 |  101966   25136   208141     8.3 |  2.166 % |
c ==============================================================================
c Found solution: 885
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7171   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25333 |  142702   465561 |   47567   25326   209649     8.3 |  2.166 % |
c |     25433 |  142702   465561 |   52323   25426   210400     8.3 |  2.171 % |
c |     25584 |  142702   465561 |   57556   25577   211974     8.3 |  2.171 % |
c |     25809 |  142702   465561 |   63311   25802   213793     8.3 |  2.171 % |
c |     26146 |  142702   465561 |   69642   26139   216757     8.3 |  2.171 % |
c |     26652 |  142702   465561 |   76607   26645   221194     8.3 |  2.171 % |
c |     27412 |  142702   465561 |   84267   27405   227788     8.3 |  2.171 % |
c |     28551 |  142702   465561 |   92694   28544   236955     8.3 |  2.171 % |
c |     30259 |  142702   465561 |  101964   30252   286886     9.5 |  2.171 % |
c |     32821 |  142702   465561 |  112160   32814   322341     9.8 |  2.171 % |
c ==============================================================================
c Found solution: 780
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7276   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33442 |  142717   465652 |   47572   33435   328054     9.8 |  2.171 % |
c |     33542 |  142717   465652 |   52329   33535   328658     9.8 |  2.182 % |
c |     33693 |  142717   465652 |   57562   33686   330731     9.8 |  2.182 % |
c |     33919 |  142717   465652 |   63318   33912   333761     9.8 |  2.182 % |
c |     34256 |  142717   465652 |   69650   34249   337197     9.8 |  2.182 % |
c |     34763 |  142717   465652 |   76615   34756   349491    10.1 |  2.182 % |
c |     35523 |  142717   465652 |   84276   35516   358023    10.1 |  2.182 % |
c |     36662 |  142717   465652 |   92704   36655   373241    10.2 |  2.182 % |
c |     38371 |  142717   465652 |  101974   38364   392122    10.2 |  2.182 % |
c |     40933 |  142717   465652 |  112172   40926   416209    10.2 |  2.182 % |
c |     44777 |  142717   465652 |  123389   44770   454614    10.2 |  2.182 % |
c |     50545 |  142717   465652 |  135728   50538   521206    10.3 |  2.182 % |
c |     59194 |  142708   465621 |  149301   59182   662866    11.2 |  2.185 % |
c |     72168 |  142708   465621 |  164231   72156   929139    12.9 |  2.185 % |
c ==============================================================================
c Found solution: 766
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7290   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79389 |  142716   465689 |   47572   79377  1122451    14.1 |  2.185 % |
c |     79489 |  142716   465689 |   52329   19945   322886    16.2 |  2.194 % |
c |     79640 |  142716   465689 |   57562   20096   324272    16.1 |  2.194 % |
c |     79865 |  142716   465689 |   63318   20321   326164    16.1 |  2.194 % |
c |     80203 |  142716   465689 |   69650   20659   330022    16.0 |  2.194 % |
c |     80709 |  142716   465689 |   76615   21165   334612    15.8 |  2.194 % |
c |     81469 |  142716   465689 |   84276   21925   343344    15.7 |  2.194 % |
c |     82608 |  142716   465689 |   92704   23064   366917    15.9 |  2.194 % |
c |     84316 |  142709   465669 |  101974   24770   379470    15.3 |  2.197 % |
c |     86878 |  142709   465669 |  112172   27332   403192    14.8 |  2.197 % |
c |     90722 |  142709   465669 |  123389   31176   436478    14.0 |  2.197 % |
c |     96488 |  142709   465669 |  135728   36942   537058    14.5 |  2.197 % |
c |    105137 |  142709   465669 |  149301   45591   649404    14.2 |  2.197 % |
c |    118113 |  142709   465669 |  164231   58567  1326728    22.7 |  2.197 % |
c |    137575 |  142709   465669 |  180654   78029  4763199    61.0 |  2.197 % |
c |    166768 |  142709   465669 |  198720  107222  6356202    59.3 |  2.197 % |
c |    210558 |  142709   465669 |  218592  151012  9453026    62.6 |  2.197 % |
c |    276242 |  142709   465669 |  240451  216696 18571721    85.7 |  2.197 % |
c |    374768 |  142709   465669 |  264496   65647 11807005   179.9 |  2.197 % |
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 -v864 v1929 v512 v2506 -v1254 -v2504 -v1374 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 1571
Raw data (stat): 1571 (runsolver) R 1570 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421141822 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 11331 0 0 0 971 27 0 0 25 0 1 0 421141822 49586176 9928 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12106 9928 603 41 0 12065 0
vsize: 48424
[startup+20.0026 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 11386 0 0 0 1971 27 0 0 25 0 1 0 421141822 49860608 9983 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12173 9983 603 41 0 12132 0
vsize: 48692
[startup+30.0028 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 11443 0 0 0 2971 28 0 0 25 0 1 0 421141822 49995776 10040 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12206 10040 603 41 0 12165 0
vsize: 48824
[startup+40.0029 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 11491 0 0 0 3970 28 0 0 25 0 1 0 421141822 50266112 10088 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12272 10088 603 41 0 12231 0
vsize: 49088
[startup+50.0036 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 11530 0 0 0 4970 28 0 0 25 0 1 0 421141822 50397184 10127 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12304 10127 603 41 0 12263 0
vsize: 49216
[startup+60.0038 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 11879 0 0 0 5968 30 0 0 25 0 1 0 421141822 51499008 10404 4294967295 134512640 134672761 3221224624 3221223776 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12573 10404 603 41 0 12532 0
vsize: 50292
[startup+70.0052 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 11881 0 0 0 6968 30 0 0 25 0 1 0 421141822 51499008 10406 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12573 10406 603 41 0 12532 0
vsize: 50292
[startup+80.0065 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 12118 0 0 0 7966 31 0 0 25 0 1 0 421141822 51646464 10468 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12609 10468 603 41 0 12568 0
vsize: 50436
[startup+90.0058 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 12453 0 0 0 8965 32 0 0 25 0 1 0 421141822 52789248 10694 4294967295 134512640 134672761 3221224624 3221223876 134593628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12888 10694 603 41 0 12847 0
vsize: 51552
[startup+100.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 12545 0 0 0 9965 33 0 0 25 0 1 0 421141822 53010432 10770 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12942 10770 603 41 0 12901 0
vsize: 51768
[startup+110.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 12647 0 0 0 10964 34 0 0 25 0 1 0 421141822 53407744 10872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13039 10872 603 41 0 12998 0
vsize: 52156
[startup+120.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 12737 0 0 0 11963 34 0 0 25 0 1 0 421141822 53813248 10962 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13138 10962 603 41 0 13097 0
vsize: 52552
[startup+130.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 12870 0 0 0 12962 35 0 0 25 0 1 0 421141822 54353920 11095 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13270 11095 603 41 0 13229 0
vsize: 53080
[startup+140.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 13068 0 0 0 13961 36 0 0 25 0 1 0 421141822 55029760 11293 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13435 11293 603 41 0 13394 0
vsize: 53740
[startup+150.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 13321 0 0 0 14960 37 0 0 25 0 1 0 421141822 56373248 11546 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13763 11546 603 41 0 13722 0
vsize: 55052
[startup+160.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 13724 0 0 0 15959 38 0 0 25 0 1 0 421141822 57999360 11949 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14160 11949 603 41 0 14119 0
vsize: 56640
[startup+170.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 13940 0 0 0 16958 39 0 0 25 0 1 0 421141822 58052608 11988 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14173 11988 603 41 0 14132 0
vsize: 56692
[startup+180.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 13940 0 0 0 17958 40 0 0 25 0 1 0 421141822 58052608 11988 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14173 11988 603 41 0 14132 0
vsize: 56692
[startup+190.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 13940 0 0 0 18957 40 0 0 25 0 1 0 421141822 58052608 11988 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14173 11988 603 41 0 14132 0
vsize: 56692
[startup+200.012 s]
Raw data (loadavg): 1.14 0.99 0.92 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 13940 0 0 0 19957 40 0 0 25 0 1 0 421141822 58052608 11988 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14173 11988 603 41 0 14132 0
vsize: 56692
[startup+210.012 s]
Raw data (loadavg): 1.12 0.99 0.92 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 14183 0 0 0 20956 41 0 0 25 0 1 0 421141822 59129856 12231 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14436 12231 603 41 0 14395 0
vsize: 57744
[startup+220.013 s]
Raw data (loadavg): 1.10 0.99 0.92 2/54 1571
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 14918 0 0 0 21953 44 0 0 25 0 1 0 421141822 62091264 12966 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15159 12966 603 41 0 15118 0
vsize: 60636
[startup+230.013 s]
Raw data (loadavg): 1.17 1.01 0.93 2/57 1620
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 16076 0 0 0 22949 48 0 0 25 0 1 0 421141822 66928640 14124 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16340 14124 603 41 0 16299 0
vsize: 65360
[startup+240.013 s]
Raw data (loadavg): 1.14 1.01 0.93 2/54 1624
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 17058 0 0 0 23945 51 0 0 25 0 1 0 421141822 70832128 15106 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17293 15106 603 41 0 17252 0
vsize: 69172
[startup+250.013 s]
Raw data (loadavg): 1.12 1.01 0.93 2/54 1624
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 17814 0 0 0 24943 54 0 0 25 0 1 0 421141822 73924608 15862 4294967295 134512640 134672761 3221224624 3221223808 134558775 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 15862 603 41 0 18007 0
vsize: 72192
[startup+260.013 s]
Raw data (loadavg): 1.10 1.01 0.93 2/54 1624
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 18251 0 0 0 25941 55 0 0 25 0 1 0 421141822 75681792 16299 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18477 16299 603 41 0 18436 0
vsize: 73908
[startup+270.014 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 1624
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 19145 0 0 0 26939 58 0 0 25 0 1 0 421141822 79319040 17193 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19365 17193 603 41 0 19324 0
vsize: 77460
[startup+280.014 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 1624
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 19576 0 0 0 27938 59 0 0 25 0 1 0 421141822 81063936 17624 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19791 17624 603 41 0 19750 0
vsize: 79164
[startup+290.014 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 1624
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 19833 0 0 0 28937 60 0 0 25 0 1 0 421141822 82132992 17881 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20052 17881 603 41 0 20011 0
vsize: 80208
[startup+300.014 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 20595 0 0 0 29935 62 0 0 25 0 1 0 421141822 85225472 18643 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20807 18643 603 41 0 20766 0
vsize: 83228
[startup+310.013 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 21356 0 0 0 30933 64 0 0 25 0 1 0 421141822 88326144 19404 4294967295 134512640 134672761 3221224624 3221223808 134559512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21564 19404 603 41 0 21523 0
vsize: 86256
[startup+320.014 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 21756 0 0 0 31932 65 0 0 25 0 1 0 421141822 90464256 19804 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22086 19804 603 41 0 22045 0
vsize: 88344
[startup+330.014 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 22011 0 0 0 32932 66 0 0 25 0 1 0 421141822 91406336 20059 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22316 20059 603 41 0 22275 0
vsize: 89264
[startup+340.014 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 22607 0 0 0 33930 68 0 0 25 0 1 0 421141822 93835264 20655 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22909 20655 603 41 0 22868 0
vsize: 91636
[startup+350.014 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 23176 0 0 0 34929 69 0 0 25 0 1 0 421141822 96120832 21224 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23467 21224 603 41 0 23426 0
vsize: 93868
[startup+360.013 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 23617 0 0 0 35927 71 0 0 25 0 1 0 421141822 98004992 21665 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23927 21665 603 41 0 23886 0
vsize: 95708
[startup+370.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 24242 0 0 0 36926 72 0 0 25 0 1 0 421141822 100429824 22290 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24519 22290 603 41 0 24478 0
vsize: 98076
[startup+380.015 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 24792 0 0 0 37925 74 0 0 25 0 1 0 421141822 102719488 22840 4294967295 134512640 134672761 3221224624 3221223808 134559540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25078 22840 603 41 0 25037 0
vsize: 100312
[startup+390.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 25459 0 0 0 38923 76 0 0 25 0 1 0 421141822 105398272 23507 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25732 23507 603 41 0 25691 0
vsize: 102928
[startup+400.015 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 26188 0 0 0 39920 79 0 0 25 0 1 0 421141822 108363776 24236 4294967295 134512640 134672761 3221224624 3221223808 134558775 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26456 24236 603 41 0 26415 0
vsize: 105824
[startup+410.015 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 26753 0 0 0 40919 80 0 0 25 0 1 0 421141822 110657536 24801 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27016 24801 603 41 0 26975 0
vsize: 108064
[startup+420.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 27426 0 0 0 41918 82 0 0 25 0 1 0 421141822 113491968 25474 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27708 25474 603 41 0 27667 0
vsize: 110832
[startup+430.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 28107 0 0 0 42916 84 0 0 25 0 1 0 421141822 116178944 26155 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28364 26156 603 41 0 28323 0
vsize: 113456
[startup+440.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 28756 0 0 0 43914 86 0 0 25 0 1 0 421141822 118857728 26804 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29018 26804 603 41 0 28977 0
vsize: 116072
[startup+450.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 29321 0 0 0 44913 88 0 0 25 0 1 0 421141822 121139200 27369 4294967295 134512640 134672761 3221224624 3221223728 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29575 27369 603 41 0 29534 0
vsize: 118300
[startup+460.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 29826 0 0 0 45911 89 0 0 25 0 1 0 421141822 123285504 27874 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30099 27874 603 41 0 30058 0
vsize: 120396
[startup+470.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 30404 0 0 0 46910 91 0 0 25 0 1 0 421141822 125542400 28452 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30650 28452 603 41 0 30609 0
vsize: 122600
[startup+480.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 30938 0 0 0 47908 93 0 0 25 0 1 0 421141822 127696896 28986 4294967295 134512640 134672761 3221224624 3221223728 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31176 28986 603 41 0 31135 0
vsize: 124704
[startup+490.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 31486 0 0 0 48906 95 0 0 25 0 1 0 421141822 129970176 29534 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31731 29534 603 41 0 31690 0
vsize: 126924
[startup+500.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 31971 0 0 0 49905 96 0 0 25 0 1 0 421141822 131973120 30019 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32220 30019 603 41 0 32179 0
vsize: 128880
[startup+510.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 32446 0 0 0 50904 97 0 0 25 0 1 0 421141822 133853184 30494 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32679 30494 603 41 0 32638 0
vsize: 130716
[startup+520.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 32881 0 0 0 51903 98 0 0 25 0 1 0 421141822 135729152 30929 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33137 30929 603 41 0 33096 0
vsize: 132548
[startup+530.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1626
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 33309 0 0 0 52902 100 0 0 25 0 1 0 421141822 137347072 31357 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33532 31357 603 41 0 33491 0
vsize: 134128
[startup+540.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 33794 0 0 0 53900 101 0 0 25 0 1 0 421141822 139366400 31842 4294967295 134512640 134672761 3221224624 3221223792 134564496 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34025 31842 603 41 0 33984 0
vsize: 136100
[startup+550.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 34285 0 0 0 54899 102 0 0 25 0 1 0 421141822 141389824 32333 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34519 32333 603 41 0 34478 0
vsize: 138076
[startup+560.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 34782 0 0 0 55898 104 0 0 25 0 1 0 421141822 143413248 32830 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35013 32830 603 41 0 34972 0
vsize: 140052
[startup+570.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 35294 0 0 0 56897 105 0 0 25 0 1 0 421141822 145555456 33342 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35536 33342 603 41 0 35495 0
vsize: 142144
[startup+580.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 35796 0 0 0 57895 106 0 0 25 0 1 0 421141822 147558400 33844 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36025 33844 603 41 0 35984 0
vsize: 144100
[startup+590.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 36273 0 0 0 58895 107 0 0 25 0 1 0 421141822 149458944 34321 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36489 34321 603 41 0 36448 0
vsize: 145956
[startup+600.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 36712 0 0 0 59894 108 0 0 25 0 1 0 421141822 151203840 34760 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36915 34760 603 41 0 36874 0
vsize: 147660
[startup+610.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 37147 0 0 0 60893 110 0 0 25 0 1 0 421141822 153104384 35195 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37379 35195 603 41 0 37338 0
vsize: 149516
[startup+620.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 37572 0 0 0 61891 111 0 0 25 0 1 0 421141822 154845184 35620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37804 35620 603 41 0 37763 0
vsize: 151216
[startup+630.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 37999 0 0 0 62890 112 0 0 25 0 1 0 421141822 156463104 36047 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38199 36047 603 41 0 38158 0
vsize: 152796
[startup+640.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 38408 0 0 0 63889 114 0 0 25 0 1 0 421141822 158216192 36456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38627 36456 603 41 0 38586 0
vsize: 154508
[startup+650.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 38791 0 0 0 64888 115 0 0 25 0 1 0 421141822 159707136 36839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38991 36839 603 41 0 38950 0
vsize: 155964
[startup+660.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 39223 0 0 0 65887 116 0 0 25 0 1 0 421141822 161464320 37271 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39420 37271 603 41 0 39379 0
vsize: 157680
[startup+670.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 39580 0 0 0 66886 117 0 0 25 0 1 0 421141822 162930688 37628 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39778 37628 603 41 0 39737 0
vsize: 159112
[startup+680.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 39911 0 0 0 67885 118 0 0 25 0 1 0 421141822 164278272 37959 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40107 37959 603 41 0 40066 0
vsize: 160428
[startup+690.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 40283 0 0 0 68884 120 0 0 25 0 1 0 421141822 166936576 38331 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40756 38331 603 41 0 40715 0
vsize: 163024
[startup+700.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 40634 0 0 0 69883 121 0 0 25 0 1 0 421141822 168288256 38682 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41086 38682 603 41 0 41045 0
vsize: 164344
[startup+710.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 40982 0 0 0 70882 122 0 0 25 0 1 0 421141822 169750528 39030 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41443 39030 603 41 0 41402 0
vsize: 165772
[startup+720.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 41293 0 0 0 71881 123 0 0 25 0 1 0 421141822 170954752 39341 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41737 39341 603 41 0 41696 0
vsize: 166948
[startup+730.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 41606 0 0 0 72880 124 0 0 25 0 1 0 421141822 172294144 39654 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42064 39654 603 41 0 42023 0
vsize: 168256
[startup+740.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 41896 0 0 0 73879 125 0 0 25 0 1 0 421141822 173506560 39944 4294967295 134512640 134672761 3221224624 3221223808 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42360 39944 603 41 0 42319 0
vsize: 169440
[startup+750.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 74878 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223620 1075351179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+760.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 75878 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+770.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 76879 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+780.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 77879 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+790.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 78879 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223728 134560480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+800.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 79879 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223808 134559293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+810.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 80879 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+820.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 81880 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+830.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 82880 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+840.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 83880 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+850.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42161 0 0 0 84880 126 0 0 25 0 1 0 421141822 174587904 40209 4294967295 134512640 134672761 3221224624 3221223728 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40209 603 41 0 42583 0
vsize: 170496
[startup+860.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42163 0 0 0 85880 126 0 0 25 0 1 0 421141822 174587904 40211 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40211 603 41 0 42583 0
vsize: 170496
[startup+870.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 86880 126 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+880.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 87880 126 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+890.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 88881 126 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+900.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 89881 126 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+910.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 90881 126 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+920.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 91881 126 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+930.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 92881 126 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+940.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 93881 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+950.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 94880 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+960.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 95880 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+970.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 96881 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+980.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 97881 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+990.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 98881 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 99881 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223888 134562281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 100881 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 101881 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 102882 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 103882 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 104882 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 105882 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 106882 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 107882 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 108883 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 109883 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.93 3/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 110883 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 111883 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 112883 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 113884 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 114884 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 115884 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 116884 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 117884 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 118884 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1628
Raw data (stat): 1571 (minisat+) R 1570 30701 30700 0 -1 0 42164 0 0 0 119885 127 0 0 25 0 1 0 421141822 174587904 40212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42624 40212 603 41 0 42583 0
vsize: 170496
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 1628
Raw data (stat): 1571 (minisat+) Z 1570 30701 30700 0 -1 12 42167 0 0 0 119885 135 0 0 25 0 1 0 421141822 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.21
CPU user time (s): 1198.86
CPU system time (s): 1.35079
CPU usage (%): 100.009
Max. virtual memory (Kb): 170496
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####