PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.95:100.opb
MD5SUM	ac4ddb996334a0834a018e09e97d1ecb
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	76
Optimality of the best value was proved	NO
Number of terms in the objective function	4617
Biggest coefficient in the objective function	2642
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	13340
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	2642
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	13340
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06984
Number of variables	4617
Total number of constraints	9896
Number of constraints which are clauses	4395
Number of constraints which are cardinality constraints (but not clauses)	5501
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	23
Trace number 6068

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        894608 kB
Buffers:         36624 kB
Cached:          81796 kB
SwapCached:       2144 kB
Active:          64836 kB
Inactive:        58520 kB
HighTotal:      131008 kB
HighFree:        45444 kB
LowTotal:       903652 kB
LowFree:        849164 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11232 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:35:13 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 4506 7 1200.29 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 [1mFound solution: 5397[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:588218     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  822537  1958196 |  274179       0        0     nan |  0.000 % |
c |       101 |  821870  1956807 |  301596      92      860     9.3 |  0.233 % |
c |       251 |  820611  1954060 |  331756     225     1975     8.8 |  0.371 % |
c |       479 |  820245  1953270 |  364932     449     6407    14.3 |  0.411 % |
c |       816 |  819671  1952030 |  401425     780    10555    13.5 |  0.473 % |
c |      1322 |  818818  1950149 |  441568    1272    18016    14.2 |  0.568 % |
c |      2084 |  817585  1947429 |  485724    2003    31787    15.9 |  0.707 % |
c |      3224 |  817579  1947417 |  534297    3142    82303    26.2 |  0.707 % |
c |      4932 |  817427  1947070 |  587727    4846   131768    27.2 |  0.725 % |
c |      7497 |  817427  1947070 |  646499    7411   184855    24.9 |  0.725 % |
c |     11341 |  817427  1947070 |  711149   11255   292575    26.0 |  0.725 % |
c |     17108 |  817427  1947070 |  782264   17022   483487    28.4 |  0.725 % |
c |     25758 |  814990  1941720 |  860491   25583   660020    25.8 |  0.997 % |
c |     38732 |  814990  1941720 |  946540   38557  1073360    27.8 |  0.997 % |
c |     58193 |  813099  1937495 | 1041194   57798  2264480    39.2 |  1.214 % |
c |     87385 |  813099  1937495 | 1145313   86990  3084930    35.5 |  1.214 % |
c |    131174 |  813099  1937495 | 1259845  130779  4158148    31.8 |  1.214 % |
c ==============================================================================
c [1mFound solution: 539[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    160598 |  839750  2000293 |  279916  160175  4921802    30.7 |  1.214 % |
c |    160698 |  839591  1999926 |  307907  160266  4923072    30.7 |  1.271 % |
c |    160848 |  839591  1999926 |  338698  160416  4928606    30.7 |  1.271 % |
c |    161074 |  839591  1999926 |  372568  160642  4935389    30.7 |  1.271 % |
c |    161411 |  839591  1999926 |  409825  160979  4949249    30.7 |  1.271 % |
c |    161918 |  839240  1999152 |  450807  161444  4958176    30.7 |  1.310 % |
c |    162678 |  838648  1997775 |  495888  162174  4971678    30.7 |  1.380 % |
c |    163818 |  838574  1997613 |  545477  163301  5010151    30.7 |  1.388 % |
c |    165527 |  838574  1997613 |  600024  165010  5075999    30.8 |  1.388 % |
c |    168089 |  838574  1997613 |  660027  167572  5195464    31.0 |  1.388 % |
c |    171933 |  838500  1997459 |  726030  171414  5286143    30.8 |  1.396 % |
c |    177700 |  836873  1993913 |  798633  176693  5388252    30.5 |  1.569 % |
c |    186349 |  836439  1992950 |  878496  185269  5877487    31.7 |  1.617 % |
c |    199325 |  836386  1992833 |  966345  198228  6969293    35.2 |  1.623 % |
c |    218786 |  835432  1990751 | 1062980  217603  7584112    34.9 |  1.725 % |
c |    247981 |  835353  1990568 | 1169278  246789  8526206    34.5 |  1.734 % |
c |    291770 |  834693  1989104 | 1286206  290540 10315486    35.5 |  1.807 % |
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 -#### 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.89 0.94 0.90 2/54 4264
Raw data (stat): 4264 (runsolver) R 4263 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423048507 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0004 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 38062 0 0 0 912 86 0 0 25 0 1 0 423048507 195411968 36680 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47708 36680 603 41 0 47667 0
vsize: 190832
[startup+20.0013 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 38650 0 0 0 1911 88 0 0 25 0 1 0 423048507 197439488 37268 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48203 37268 603 41 0 48162 0
vsize: 192812
[startup+30.0025 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 38966 0 0 0 2909 89 0 0 25 0 1 0 423048507 198656000 37584 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48500 37584 603 41 0 48459 0
vsize: 194000
[startup+40.0028 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 39090 0 0 0 3909 90 0 0 25 0 1 0 423048507 199061504 37708 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48599 37708 603 41 0 48558 0
vsize: 194396
[startup+50.0037 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 39285 0 0 0 4908 91 0 0 25 0 1 0 423048507 199897088 37903 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48803 37903 603 41 0 48762 0
vsize: 195212
[startup+60.0034 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 39479 0 0 0 5907 91 0 0 25 0 1 0 423048507 200704000 38097 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49000 38097 603 41 0 48959 0
vsize: 196000
[startup+70.0042 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 39688 0 0 0 6907 92 0 0 25 0 1 0 423048507 201670656 38306 4294967295 134512640 134672761 3221224544 3221223680 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49236 38306 603 41 0 49195 0
vsize: 196944
[startup+80.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 39751 0 0 0 7906 92 0 0 25 0 1 0 423048507 201805824 38369 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49269 38369 603 41 0 49228 0
vsize: 197076
[startup+90.0052 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 39877 0 0 0 8906 93 0 0 25 0 1 0 423048507 202346496 38495 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49401 38495 603 41 0 49360 0
vsize: 197604
[startup+100.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 39989 0 0 0 9906 93 0 0 25 0 1 0 423048507 202883072 38607 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49532 38607 603 41 0 49491 0
vsize: 198128
[startup+110.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 40193 0 0 0 10905 94 0 0 25 0 1 0 423048507 203681792 38811 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49727 38811 603 41 0 49686 0
vsize: 198908
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 40398 0 0 0 11905 95 0 0 25 0 1 0 423048507 204607488 39016 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49953 39016 603 41 0 49912 0
vsize: 199812
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 40601 0 0 0 12904 95 0 0 25 0 1 0 423048507 205406208 39219 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50148 39219 603 41 0 50107 0
vsize: 200592
[startup+140.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 40829 0 0 0 13904 95 0 0 25 0 1 0 423048507 206217216 39447 4294967295 134512640 134672761 3221224544 3221223680 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50346 39447 603 41 0 50305 0
vsize: 201384
[startup+150.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 40880 0 0 0 14904 95 0 0 25 0 1 0 423048507 206352384 39498 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50379 39498 603 41 0 50338 0
vsize: 201516
[startup+160.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 41096 0 0 0 15904 96 0 0 25 0 1 0 423048507 207294464 39714 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50609 39714 603 41 0 50568 0
vsize: 202436
[startup+170.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 41425 0 0 0 16903 97 0 0 25 0 1 0 423048507 208625664 40043 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50934 40043 603 41 0 50893 0
vsize: 203736
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 41723 0 0 0 17902 98 0 0 25 0 1 0 423048507 209838080 40341 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51230 40341 603 41 0 51189 0
vsize: 204920
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 42049 0 0 0 18901 100 0 0 25 0 1 0 423048507 211173376 40667 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51556 40667 603 41 0 51515 0
vsize: 206224
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 42233 0 0 0 19900 100 0 0 25 0 1 0 423048507 211849216 40851 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51721 40851 603 41 0 51680 0
vsize: 206884
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 42396 0 0 0 20900 101 0 0 25 0 1 0 423048507 212516864 41014 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51884 41014 603 41 0 51843 0
vsize: 207536
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 42548 0 0 0 21900 101 0 0 25 0 1 0 423048507 213446656 41166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52111 41166 603 41 0 52070 0
vsize: 208444
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 42698 0 0 0 22900 101 0 0 25 0 1 0 423048507 213979136 41316 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52241 41316 603 41 0 52200 0
vsize: 208964
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 42837 0 0 0 23900 101 0 0 25 0 1 0 423048507 214519808 41455 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52373 41455 603 41 0 52332 0
vsize: 209492
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 42980 0 0 0 24899 102 0 0 25 0 1 0 423048507 215240704 41598 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52549 41598 603 41 0 52508 0
vsize: 210196
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 43099 0 0 0 25899 103 0 0 25 0 1 0 423048507 215638016 41717 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52646 41717 603 41 0 52605 0
vsize: 210584
[startup+270.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 43228 0 0 0 26899 103 0 0 25 0 1 0 423048507 216178688 41846 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52778 41846 603 41 0 52737 0
vsize: 211112
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 43328 0 0 0 27898 104 0 0 25 0 1 0 423048507 216633344 41946 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52889 41946 603 41 0 52848 0
vsize: 211556
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 43452 0 0 0 28898 104 0 0 25 0 1 0 423048507 217042944 42070 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52989 42070 603 41 0 52948 0
vsize: 211956
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 43551 0 0 0 29898 104 0 0 25 0 1 0 423048507 217444352 42169 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53087 42169 603 41 0 53046 0
vsize: 212348
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 43649 0 0 0 30898 105 0 0 25 0 1 0 423048507 217849856 42267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53186 42267 603 41 0 53145 0
vsize: 212744
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 43748 0 0 0 31897 105 0 0 25 0 1 0 423048507 218247168 42366 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53283 42366 603 41 0 53242 0
vsize: 213132
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 43851 0 0 0 32897 106 0 0 25 0 1 0 423048507 218644480 42469 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53380 42469 603 41 0 53339 0
vsize: 213520
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 43937 0 0 0 33896 106 0 0 25 0 1 0 423048507 219070464 42555 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53484 42555 603 41 0 53443 0
vsize: 213936
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44021 0 0 0 34896 106 0 0 25 0 1 0 423048507 219336704 42639 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53549 42639 603 41 0 53508 0
vsize: 214196
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44101 0 0 0 35895 107 0 0 25 0 1 0 423048507 219734016 42719 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53646 42719 603 41 0 53605 0
vsize: 214584
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44190 0 0 0 36895 107 0 0 25 0 1 0 423048507 220225536 42808 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53766 42808 603 41 0 53725 0
vsize: 215064
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44271 0 0 0 37895 107 0 0 25 0 1 0 423048507 220491776 42890 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53831 42890 603 41 0 53790 0
vsize: 215324
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44354 0 0 0 38895 108 0 0 25 0 1 0 423048507 220770304 42972 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53899 42972 603 41 0 53858 0
vsize: 215596
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44432 0 0 0 39895 108 0 0 25 0 1 0 423048507 221200384 43050 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54004 43050 603 41 0 53963 0
vsize: 216016
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44503 0 0 0 40895 108 0 0 25 0 1 0 423048507 221462528 43121 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54068 43121 603 41 0 54027 0
vsize: 216272
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44569 0 0 0 41896 108 0 0 25 0 1 0 423048507 221761536 43187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54141 43187 603 41 0 54100 0
vsize: 216564
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44682 0 0 0 42895 108 0 0 25 0 1 0 423048507 222232576 43300 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54256 43300 603 41 0 54215 0
vsize: 217024
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44745 0 0 0 43896 108 0 0 25 0 1 0 423048507 222363648 43363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54288 43363 603 41 0 54247 0
vsize: 217152
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44819 0 0 0 44896 109 0 0 25 0 1 0 423048507 222769152 43437 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54387 43437 603 41 0 54346 0
vsize: 217548
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 44904 0 0 0 45895 109 0 0 25 0 1 0 423048507 223580160 43522 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54585 43522 603 41 0 54544 0
vsize: 218340
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45025 0 0 0 46894 109 0 0 25 0 1 0 423048507 224178176 43643 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54731 43643 603 41 0 54690 0
vsize: 218924
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45112 0 0 0 47894 110 0 0 25 0 1 0 423048507 224571392 43730 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54827 43730 603 41 0 54786 0
vsize: 219308
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45194 0 0 0 48894 110 0 0 25 0 1 0 423048507 224833536 43812 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54891 43812 603 41 0 54850 0
vsize: 219564
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45284 0 0 0 49894 110 0 0 25 0 1 0 423048507 225230848 43902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54988 43902 603 41 0 54947 0
vsize: 219952
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45371 0 0 0 50894 111 0 0 25 0 1 0 423048507 225505280 43989 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55055 43989 603 41 0 55014 0
vsize: 220220
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45448 0 0 0 51894 111 0 0 25 0 1 0 423048507 225771520 44066 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55120 44066 603 41 0 55079 0
vsize: 220480
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45527 0 0 0 52893 112 0 0 25 0 1 0 423048507 226168832 44145 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55217 44145 603 41 0 55176 0
vsize: 220868
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45604 0 0 0 53893 112 0 0 25 0 1 0 423048507 226439168 44222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55283 44222 603 41 0 55242 0
vsize: 221132
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45679 0 0 0 54893 112 0 0 25 0 1 0 423048507 226701312 44297 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55347 44297 603 41 0 55306 0
vsize: 221388
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45834 0 0 0 55893 113 0 0 25 0 1 0 423048507 227479552 44452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55537 44452 603 41 0 55496 0
vsize: 222148
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 45947 0 0 0 56892 113 0 0 25 0 1 0 423048507 227889152 44565 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55637 44565 603 41 0 55596 0
vsize: 222548
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 46046 0 0 0 57892 114 0 0 25 0 1 0 423048507 228388864 44664 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55759 44664 603 41 0 55718 0
vsize: 223036
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 46204 0 0 0 58892 114 0 0 25 0 1 0 423048507 228929536 44822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55891 44822 603 41 0 55850 0
vsize: 223564
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 47982 0 0 0 59887 120 0 0 25 0 1 0 423048507 235794432 46589 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57567 46589 603 41 0 57526 0
vsize: 230268
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 48047 0 0 0 60886 120 0 0 25 0 1 0 423048507 236113920 46654 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57645 46654 603 41 0 57604 0
vsize: 230580
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 48199 0 0 0 61886 121 0 0 25 0 1 0 423048507 236650496 46806 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57776 46806 603 41 0 57735 0
vsize: 231104
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 48402 0 0 0 62885 121 0 0 25 0 1 0 423048507 237453312 47009 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57972 47009 603 41 0 57931 0
vsize: 231888
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 48487 0 0 0 63885 122 0 0 25 0 1 0 423048507 237854720 47094 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58070 47094 603 41 0 58029 0
vsize: 232280
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 48535 0 0 0 64885 122 0 0 25 0 1 0 423048507 237989888 47142 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58103 47142 603 41 0 58062 0
vsize: 232412
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 48562 0 0 0 65886 122 0 0 25 0 1 0 423048507 238125056 47169 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58136 47169 603 41 0 58095 0
vsize: 232544
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 48582 0 0 0 66886 122 0 0 25 0 1 0 423048507 238305280 47189 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58180 47189 603 41 0 58139 0
vsize: 232720
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 48664 0 0 0 67886 122 0 0 25 0 1 0 423048507 238575616 47271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58246 47271 603 41 0 58205 0
vsize: 232984
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 48743 0 0 0 68886 122 0 0 25 0 1 0 423048507 238845952 47350 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58312 47350 603 41 0 58271 0
vsize: 233248
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 48864 0 0 0 69885 123 0 0 25 0 1 0 423048507 239382528 47471 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58443 47471 603 41 0 58402 0
vsize: 233772
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 49171 0 0 0 70884 125 0 0 25 0 1 0 423048507 240578560 47778 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58735 47778 603 41 0 58694 0
vsize: 234940
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 49295 0 0 0 71883 125 0 0 25 0 1 0 423048507 241115136 47902 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58866 47902 603 41 0 58825 0
vsize: 235464
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 49599 0 0 0 72883 126 0 0 25 0 1 0 423048507 242315264 48206 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59159 48206 603 41 0 59118 0
vsize: 236636
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 49922 0 0 0 73882 127 0 0 25 0 1 0 423048507 243662848 48529 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59488 48529 603 41 0 59447 0
vsize: 237952
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 50295 0 0 0 74882 128 0 0 25 0 1 0 423048507 245137408 48902 4294967295 134512640 134672761 3221224544 3221223708 134564508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59848 48902 603 41 0 59807 0
vsize: 239392
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 50569 0 0 0 75881 129 0 0 25 0 1 0 423048507 246341632 49176 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60142 49176 603 41 0 60101 0
vsize: 240568
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 50650 0 0 0 76881 129 0 0 25 0 1 0 423048507 246607872 49257 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60207 49257 603 41 0 60166 0
vsize: 240828
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 50843 0 0 0 77880 130 0 0 25 0 1 0 423048507 247414784 49450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60404 49450 603 41 0 60363 0
vsize: 241616
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 50866 0 0 0 78880 130 0 0 25 0 1 0 423048507 247414784 49473 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60404 49473 603 41 0 60363 0
vsize: 241616
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 50947 0 0 0 79880 130 0 0 25 0 1 0 423048507 247820288 49554 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60503 49554 603 41 0 60462 0
vsize: 242012
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 51003 0 0 0 80880 130 0 0 25 0 1 0 423048507 247955456 49610 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60536 49610 603 41 0 60495 0
vsize: 242144
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 51103 0 0 0 81880 130 0 0 25 0 1 0 423048507 248356864 49710 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60634 49710 603 41 0 60593 0
vsize: 242536
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 51222 0 0 0 82880 131 0 0 25 0 1 0 423048507 248893440 49829 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60765 49829 603 41 0 60724 0
vsize: 243060
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 51275 0 0 0 83880 131 0 0 25 0 1 0 423048507 249028608 49882 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60798 49882 603 41 0 60757 0
vsize: 243192
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 51318 0 0 0 84880 131 0 0 25 0 1 0 423048507 249298944 49925 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60864 49925 603 41 0 60823 0
vsize: 243456
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 51379 0 0 0 85880 131 0 0 25 0 1 0 423048507 249434112 49986 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60897 49986 603 41 0 60856 0
vsize: 243588
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 51542 0 0 0 86879 132 0 0 25 0 1 0 423048507 250105856 50149 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61061 50149 603 41 0 61020 0
vsize: 244244
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 51728 0 0 0 87878 133 0 0 25 0 1 0 423048507 250900480 50335 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61255 50335 603 41 0 61214 0
vsize: 245020
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 51913 0 0 0 88878 134 0 0 25 0 1 0 423048507 251572224 50520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61419 50520 603 41 0 61378 0
vsize: 245676
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 52084 0 0 0 89877 134 0 0 25 0 1 0 423048507 252383232 50691 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61617 50691 603 41 0 61576 0
vsize: 246468
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 52247 0 0 0 90877 135 0 0 25 0 1 0 423048507 253054976 50854 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61781 50854 603 41 0 61740 0
vsize: 247124
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 52402 0 0 0 91876 136 0 0 25 0 1 0 423048507 253595648 51009 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61913 51009 603 41 0 61872 0
vsize: 247652
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 52557 0 0 0 92876 136 0 0 25 0 1 0 423048507 254271488 51164 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62078 51164 603 41 0 62037 0
vsize: 248312
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 52644 0 0 0 93876 136 0 0 25 0 1 0 423048507 254676992 51251 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62177 51251 603 41 0 62136 0
vsize: 248708
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 52696 0 0 0 94876 137 0 0 25 0 1 0 423048507 254812160 51303 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62210 51303 603 41 0 62169 0
vsize: 248840
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 52787 0 0 0 95876 137 0 0 25 0 1 0 423048507 255213568 51394 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62308 51394 603 41 0 62267 0
vsize: 249232
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 52864 0 0 0 96876 137 0 0 25 0 1 0 423048507 255619072 51471 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62407 51471 603 41 0 62366 0
vsize: 249628
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 53042 0 0 0 97875 138 0 0 25 0 1 0 423048507 256290816 51649 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62571 51649 603 41 0 62530 0
vsize: 250284
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 53300 0 0 0 98875 139 0 0 25 0 1 0 423048507 257368064 51907 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62834 51907 603 41 0 62793 0
vsize: 251336
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 53550 0 0 0 99874 140 0 0 25 0 1 0 423048507 259354624 52157 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63319 52157 603 41 0 63278 0
vsize: 253276
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 53749 0 0 0 100873 140 0 0 25 0 1 0 423048507 260157440 52356 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63515 52356 603 41 0 63474 0
vsize: 254060
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 53941 0 0 0 101873 141 0 0 25 0 1 0 423048507 260952064 52548 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63709 52548 603 41 0 63668 0
vsize: 254836
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 54118 0 0 0 102873 141 0 0 25 0 1 0 423048507 261623808 52725 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63873 52725 603 41 0 63832 0
vsize: 255492
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 54309 0 0 0 103872 142 0 0 25 0 1 0 423048507 262443008 52916 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64073 52916 603 41 0 64032 0
vsize: 256292
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 54496 0 0 0 104872 142 0 0 25 0 1 0 423048507 263249920 53103 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64270 53103 603 41 0 64229 0
vsize: 257080
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 54667 0 0 0 105872 143 0 0 25 0 1 0 423048507 263921664 53274 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64434 53274 603 41 0 64393 0
vsize: 257736
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 54822 0 0 0 106871 144 0 0 25 0 1 0 423048507 264445952 53429 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64562 53429 603 41 0 64521 0
vsize: 258248
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 55002 0 0 0 107870 144 0 0 25 0 1 0 423048507 265252864 53609 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64759 53609 603 41 0 64718 0
vsize: 259036
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 55142 0 0 0 108869 146 0 0 25 0 1 0 423048507 265785344 53749 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64889 53749 603 41 0 64848 0
vsize: 259556
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 55253 0 0 0 109868 146 0 0 25 0 1 0 423048507 266326016 53860 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65021 53860 603 41 0 64980 0
vsize: 260084
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 55327 0 0 0 110868 147 0 0 25 0 1 0 423048507 266600448 53934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65088 53934 603 41 0 65047 0
vsize: 260352
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 55473 0 0 0 111868 147 0 0 25 0 1 0 423048507 267132928 54080 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65218 54080 603 41 0 65177 0
vsize: 260872
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 55670 0 0 0 112868 148 0 0 25 0 1 0 423048507 267931648 54277 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65413 54277 603 41 0 65372 0
vsize: 261652
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 55740 0 0 0 113867 148 0 0 25 0 1 0 423048507 268234752 54347 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65487 54347 603 41 0 65446 0
vsize: 261948
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 55867 0 0 0 114867 148 0 0 25 0 1 0 423048507 268771328 54474 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65618 54475 603 41 0 65577 0
vsize: 262472
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 56012 0 0 0 115867 149 0 0 25 0 1 0 423048507 269316096 54619 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65751 54619 603 41 0 65710 0
vsize: 263004
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 56127 0 0 0 116867 149 0 0 25 0 1 0 423048507 269852672 54734 4294967295 134512640 134672761 3221224544 3221223484 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65882 54734 603 41 0 65841 0
vsize: 263528
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 56228 0 0 0 117867 150 0 0 25 0 1 0 423048507 270254080 54835 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65980 54835 603 41 0 65939 0
vsize: 263920
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 56347 0 0 0 118866 150 0 0 25 0 1 0 423048507 270655488 54954 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66078 54954 603 41 0 66037 0
vsize: 264312
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4264
Raw data (stat): 4264 (minisat+) R 4263 29151 29150 0 -1 0 56403 0 0 0 119866 150 0 0 25 0 1 0 423048507 271052800 55010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66175 55010 603 41 0 66134 0
vsize: 264700
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4264
Raw data (stat): 4264 (minisat+) Z 4263 29151 29150 0 -1 12 56406 0 0 0 119866 162 0 0 25 0 1 0 423048507 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.15
CPU time (s): 1200.29
CPU user time (s): 1198.67
CPU system time (s): 1.62075
CPU usage (%): 100.012
Max. virtual memory (Kb): 264700
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####