PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.95:98.opb
MD5SUM	5f5bedf3690a537deb8cc97cc5d565ae
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	94
Optimality of the best value was proved	NO
Number of terms in the objective function	4624
Biggest coefficient in the objective function	2577
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	13335
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	2577
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	13335
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07084
Number of variables	4624
Total number of constraints	9886
Number of constraints which are clauses	4404
Number of constraints which are cardinality constraints (but not clauses)	5482
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	22
Trace number 6079

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        878184 kB
Buffers:         36452 kB
Cached:          97788 kB
SwapCached:       2644 kB
Active:          54468 kB
Inactive:        85280 kB
HighTotal:      131008 kB
HighFree:        29344 kB
LowTotal:       903652 kB
LowFree:        848840 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11168 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:38:05 (client local time) WITH STATUS 10 IN 1200.54 SECONDS
stats: 4510 7 1200.54 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5262 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 870]---> BDD-cost:   11
c ---[ 869]---> BDD-cost:   20
c ---[ 868]---> BDD-cost:   29
c ---[ 867]---> BDD-cost:   29
c ---[ 866]---> BDD-cost:   29
c ---[ 865]---> BDD-cost:   26
c ---[ 864]---> BDD-cost:   38
c ---[ 863]---> BDD-cost:   26
c ---[ 862]---> BDD-cost:   20
c ---[ 861]---> BDD-cost:   20
c ---[ 860]---> BDD-cost:   23
c ---[ 859]---> BDD-cost:   20
c ---[ 858]---> BDD-cost:   23
c ---[ 857]---> BDD-cost:   23
c ---[ 856]---> BDD-cost:   26
c ---[ 855]---> BDD-cost:   11
c ---[ 854]---> BDD-cost:   11
c ---[ 853]---> BDD-cost:    8
c ---[ 852]---> BDD-cost:   11
c ---[ 851]---> BDD-cost:    8
c ---[ 850]---> BDD-cost:   14
c ---[ 849]---> BDD-cost:    8
c ---[ 848]---> BDD-cost:    7
c ---[ 843]---> BDD-cost:   26
c ---[ 842]---> BDD-cost:   35
c ---[ 841]---> BDD-cost:   32
c ---[ 840]---> BDD-cost:   38
c ---[ 839]---> BDD-cost:   38
c ---[ 838]---> BDD-cost:   44
c ---[ 837]---> BDD-cost:   35
c ---[ 836]---> BDD-cost:   29
c ---[ 835]---> BDD-cost:   29
c ---[ 834]---> BDD-cost:   24
c ---[ 833]---> BDD-cost:   29
c ---[ 832]---> BDD-cost:   26
c ---[ 831]---> BDD-cost:   26
c ---[ 830]---> BDD-cost:   17
c ---[ 829]---> BDD-cost:   20
c ---[ 828]---> BDD-cost:   11
c ---[ 827]---> BDD-cost:   17
c ---[ 826]---> BDD-cost:   20
c ---[ 825]---> BDD-cost:   23
c ---[ 824]---> BDD-cost:   18
c ---[ 823]---> BDD-cost:   18
c ---[ 821]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:   35
c ---[ 816]---> BDD-cost:   25
c ---[ 815]---> BDD-cost:   45
c ---[ 814]---> BDD-cost:   39
c ---[ 813]---> BDD-cost:   44
c ---[ 812]---> BDD-cost:   41
c ---[ 811]---> BDD-cost:   50
c ---[ 810]---> BDD-cost:   44
c ---[ 809]---> BDD-cost:   38
c ---[ 808]---> BDD-cost:   35
c ---[ 807]---> BDD-cost:   35
c ---[ 806]---> BDD-cost:   32
c ---[ 805]---> BDD-cost:   38
c ---[ 804]---> BDD-cost:   26
c ---[ 803]---> BDD-cost:   26
c ---[ 802]---> BDD-cost:   20
c ---[ 801]---> BDD-cost:   23
c ---[ 800]---> BDD-cost:   17
c ---[ 799]---> BDD-cost:   20
c ---[ 798]---> BDD-cost:   21
c ---[ 797]---> BDD-cost:   26
c ---[ 796]---> BDD-cost:   23
c ---[ 795]---> BDD-cost:   26
c ---[ 794]---> BDD-cost:   13
c ---[ 793]---> BDD-cost:   20
c ---[ 792]---> BDD-cost:   11
c ---[ 789]---> BDD-cost:   20
c ---[ 788]---> BDD-cost:   29
c ---[ 787]---> BDD-cost:   41
c ---[ 786]---> BDD-cost:   44
c ---[ 785]---> BDD-cost:   56
c ---[ 784]---> BDD-cost:   53
c ---[ 783]---> BDD-cost:   53
c ---[ 782]---> BDD-cost:   47
c ---[ 781]---> BDD-cost:   47
c ---[ 780]---> BDD-cost:   44
c ---[ 779]---> BDD-cost:   47
c ---[ 778]---> BDD-cost:   41
c ---[ 777]---> BDD-cost:   38
c ---[ 776]---> BDD-cost:   35
c ---[ 775]---> BDD-cost:   38
c ---[ 774]---> BDD-cost:   35
c ---[ 773]---> BDD-cost:   29
c ---[ 772]---> BDD-cost:   20
c ---[ 771]---> BDD-cost:   20
c ---[ 770]---> BDD-cost:   17
c ---[ 769]---> BDD-cost:   20
c ---[ 768]---> BDD-cost:   29
c ---[ 767]---> BDD-cost:   32
c ---[ 766]---> BDD-cost:   26
c ---[ 765]---> BDD-cost:   32
c ---[ 764]---> BDD-cost:   19
c ---[ 763]---> BDD-cost:   26
c ---[ 762]---> BDD-cost:   17
c ---[ 761]---> BDD-cost:    7
c ---[ 760]---> BDD-cost:   17
c ---[ 759]---> BDD-cost:   26
c ---[ 758]---> BDD-cost:   32
c ---[ 757]---> BDD-cost:   44
c ---[ 756]---> BDD-cost:   47
c ---[ 755]---> BDD-cost:   53
c ---[ 754]---> BDD-cost:   53
c ---[ 753]---> BDD-cost:   47
c ---[ 752]---> BDD-cost:   47
c ---[ 751]---> BDD-cost:   50
c ---[ 750]---> BDD-cost:   47
c ---[ 749]---> BDD-cost:   45
c ---[ 748]---> BDD-cost:   44
c ---[ 747]---> BDD-cost:   41
c ---[ 746]---> BDD-cost:   38
c ---[ 745]---> BDD-cost:   35
c ---[ 744]---> BDD-cost:   29
c ---[ 743]---> BDD-cost:   20
c ---[ 742]---> BDD-cost:   23
c ---[ 741]---> BDD-cost:   23
c ---[ 740]---> BDD-cost:   20
c ---[ 739]---> BDD-cost:   23
c ---[ 738]---> BDD-cost:   26
c ---[ 737]---> BDD-cost:   30
c ---[ 736]---> BDD-cost:   35
c ---[ 735]---> BDD-cost:   35
c ---[ 734]---> BDD-cost:   29
c ---[ 733]---> BDD-cost:   23
c ---[ 732]---> BDD-cost:   20
c ---[ 731]---> BDD-cost:   17
c ---[ 730]---> BDD-cost:   17
c ---[ 729]---> BDD-cost:   27
c ---[ 728]---> BDD-cost:   35
c ---[ 727]---> BDD-cost:   47
c ---[ 726]---> BDD-cost:   50
c ---[ 725]---> BDD-cost:   47
c ---[ 724]---> BDD-cost:   44
c ---[ 723]---> BDD-cost:   47
c ---[ 722]---> BDD-cost:   50
c ---[ 721]---> BDD-cost:   44
c ---[ 720]---> BDD-cost:   41
c ---[ 719]---> BDD-cost:   44
c ---[ 718]---> BDD-cost:   47
c ---[ 717]---> BDD-cost:   38
c ---[ 716]---> BDD-cost:   35
c ---[ 715]---> BDD-cost:   35
c ---[ 714]---> BDD-cost:   29
c ---[ 713]---> BDD-cost:   20
c ---[ 712]---> BDD-cost:   20
c ---[ 711]---> BDD-cost:   20
c ---[ 710]---> BDD-cost:   23
c ---[ 709]---> BDD-cost:   17
c ---[ 708]---> BDD-cost:   26
c ---[ 707]---> BDD-cost:   32
c ---[ 706]---> BDD-cost:   29
c ---[ 705]---> BDD-cost:   29
c ---[ 704]---> BDD-cost:   32
c ---[ 703]---> BDD-cost:   24
c ---[ 702]---> BDD-cost:   17
c ---[ 701]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:   23
c ---[ 699]---> BDD-cost:   35
c ---[ 698]---> BDD-cost:   38
c ---[ 697]---> BDD-cost:   41
c ---[ 696]---> BDD-cost:   38
c ---[ 695]---> BDD-cost:   44
c ---[ 694]---> BDD-cost:   47
c ---[ 693]---> BDD-cost:   44
c ---[ 692]---> BDD-cost:   44
c ---[ 691]---> BDD-cost:   47
c ---[ 690]---> BDD-cost:   44
c ---[ 689]---> BDD-cost:   47
c ---[ 688]---> BDD-cost:   44
c ---[ 687]---> BDD-cost:   38
c ---[ 686]---> BDD-cost:   32
c ---[ 685]---> BDD-cost:   23
c ---[ 684]---> BDD-cost:   29
c ---[ 683]---> BDD-cost:   20
c ---[ 682]---> BDD-cost:   20
c ---[ 681]---> BDD-cost:   11
c ---[ 680]---> BDD-cost:   14
c ---[ 679]---> BDD-cost:   17
c ---[ 678]---> BDD-cost:   26
c ---[ 677]---> BDD-cost:   29
c ---[ 676]---> BDD-cost:   29
c ---[ 675]---> BDD-cost:   32
c ---[ 674]---> BDD-cost:   32
c ---[ 673]---> BDD-cost:   29
c ---[ 672]---> BDD-cost:   20
c ---[ 671]---> BDD-cost:   26
c ---[ 670]---> BDD-cost:   26
c ---[ 669]---> BDD-cost:   38
c ---[ 668]---> BDD-cost:   41
c ---[ 667]---> BDD-cost:   41
c ---[ 666]---> BDD-cost:   41
c ---[ 665]---> BDD-cost:   38
c ---[ 664]---> BDD-cost:   44
c ---[ 663]---> BDD-cost:   44
c ---[ 662]---> BDD-cost:   41
c ---[ 661]---> BDD-cost:   47
c ---[ 660]---> BDD-cost:   47
c ---[ 659]---> BDD-cost:   44
c ---[ 658]---> BDD-cost:   44
c ---[ 657]---> BDD-cost:   32
c ---[ 656]---> BDD-cost:   29
c ---[ 655]---> BDD-cost:   29
c ---[ 654]---> BDD-cost:   23
c ---[ 653]---> BDD-cost:   14
c ---[ 652]---> BDD-cost:   11
c ---[ 651]---> BDD-cost:    8
c ---[ 650]---> BDD-cost:   14
c ---[ 649]---> BDD-cost:   17
c ---[ 648]---> BDD-cost:   17
c ---[ 647]---> BDD-cost:   24
c ---[ 646]---> BDD-cost:   32
c ---[ 645]---> BDD-cost:   29
c ---[ 644]---> BDD-cost:   26
c ---[ 643]---> BDD-cost:   20
c ---[ 642]---> BDD-cost:   26
c ---[ 641]---> BDD-cost:   29
c ---[ 640]---> BDD-cost:   35
c ---[ 639]---> BDD-cost:   41
c ---[ 638]---> BDD-cost:   38
c ---[ 637]---> BDD-cost:   38
c ---[ 636]---> BDD-cost:   38
c ---[ 635]---> BDD-cost:   41
c ---[ 634]---> BDD-cost:   41
c ---[ 633]---> BDD-cost:   38
c ---[ 632]---> BDD-cost:   42
c ---[ 631]---> BDD-cost:   47
c ---[ 630]---> BDD-cost:   41
c ---[ 629]---> BDD-cost:   41
c ---[ 628]---> BDD-cost:   32
c ---[ 627]---> BDD-cost:   29
c ---[ 626]---> BDD-cost:   26
c ---[ 625]---> BDD-cost:   18
c ---[ 624]---> BDD-cost:   14
c ---[ 623]---> BDD-cost:   11
c ---[ 622]---> BDD-cost:    8
c ---[ 621]---> BDD-cost:   11
c ---[ 620]---> BDD-cost:   23
c ---[ 619]---> BDD-cost:   23
c ---[ 618]---> BDD-cost:   23
c ---[ 617]---> BDD-cost:   26
c ---[ 616]---> BDD-cost:   29
c ---[ 615]---> BDD-cost:   20
c ---[ 614]---> BDD-cost:   17
c ---[ 613]---> BDD-cost:   24
c ---[ 612]---> BDD-cost:   26
c ---[ 611]---> BDD-cost:   29
c ---[ 610]---> BDD-cost:   35
c ---[ 609]---> BDD-cost:   35
c ---[ 608]---> BDD-cost:   35
c ---[ 607]---> BDD-cost:   44
c ---[ 606]---> BDD-cost:   47
c ---[ 605]---> BDD-cost:   53
c ---[ 604]---> BDD-cost:   38
c ---[ 603]---> BDD-cost:   41
c ---[ 602]---> BDD-cost:   41
c ---[ 601]---> BDD-cost:   38
c ---[ 600]---> BDD-cost:   50
c ---[ 599]---> BDD-cost:   53
c ---[ 598]---> BDD-cost:   44
c ---[ 597]---> BDD-cost:   41
c ---[ 596]---> BDD-cost:   29
c ---[ 595]---> BDD-cost:   26
c ---[ 594]---> BDD-cost:   20
c ---[ 593]---> BDD-cost:   11
c ---[ 592]---> BDD-cost:    8
c ---[ 591]---> BDD-cost:    8
c ---[ 590]---> BDD-cost:   17
c ---[ 589]---> BDD-cost:   20
c ---[ 588]---> BDD-cost:   26
c ---[ 587]---> BDD-cost:   26
c ---[ 586]---> BDD-cost:   26
c ---[ 585]---> BDD-cost:   20
c ---[ 584]---> BDD-cost:   14
c ---[ 583]---> BDD-cost:   23
c ---[ 582]---> BDD-cost:   32
c ---[ 581]---> BDD-cost:   32
c ---[ 580]---> BDD-cost:   41
c ---[ 579]---> BDD-cost:   38
c ---[ 578]---> BDD-cost:   48
c ---[ 577]---> BDD-cost:   53
c ---[ 576]---> BDD-cost:   56
c ---[ 575]---> BDD-cost:   47
c ---[ 574]---> BDD-cost:   47
c ---[ 573]---> BDD-cost:   44
c ---[ 572]---> BDD-cost:   53
c ---[ 571]---> BDD-cost:   53
c ---[ 570]---> BDD-cost:   53
c ---[ 569]---> BDD-cost:   47
c ---[ 568]---> BDD-cost:   41
c ---[ 567]---> BDD-cost:   35
c ---[ 566]---> BDD-cost:   29
c ---[ 565]---> BDD-cost:   23
c ---[ 564]---> BDD-cost:   17
c ---[ 563]---> BDD-cost:   11
c ---[ 562]---> BDD-cost:    8
c ---[ 561]---> BDD-cost:   11
c ---[ 560]---> BDD-cost:   20
c ---[ 559]---> BDD-cost:   23
c ---[ 558]---> BDD-cost:   20
c ---[ 557]---> BDD-cost:   20
c ---[ 556]---> BDD-cost:   17
c ---[ 555]---> BDD-cost:   17
c ---[ 554]---> BDD-cost:   23
c ---[ 553]---> BDD-cost:   29
c ---[ 552]---> BDD-cost:   35
c ---[ 551]---> BDD-cost:   41
c ---[ 550]---> BDD-cost:   50
c ---[ 549]---> BDD-cost:   47
c ---[ 548]---> BDD-cost:   47
c ---[ 547]---> BDD-cost:   47
c ---[ 546]---> BDD-cost:   50
c ---[ 545]---> BDD-cost:   50
c ---[ 544]---> BDD-cost:   56
c ---[ 543]---> BDD-cost:   59
c ---[ 542]---> BDD-cost:   59
c ---[ 541]---> BDD-cost:   47
c ---[ 540]---> BDD-cost:   44
c ---[ 539]---> BDD-cost:   47
c ---[ 538]---> BDD-cost:   32
c ---[ 537]---> BDD-cost:   26
c ---[ 536]---> BDD-cost:   26
c ---[ 535]---> BDD-cost:   20
c ---[ 534]---> BDD-cost:   14
c ---[ 533]---> BDD-cost:   17
c ---[ 532]---> BDD-cost:   20
c ---[ 531]---> BDD-cost:   23
c ---[ 530]---> BDD-cost:   20
c ---[ 529]---> BDD-cost:   20
c ---[ 528]---> BDD-cost:   17
c ---[ 527]---> BDD-cost:   11
c ---[ 526]---> BDD-cost:   11
c ---[ 525]---> BDD-cost:   23
c ---[ 524]---> BDD-cost:   29
c ---[ 523]---> BDD-cost:   32
c ---[ 522]---> BDD-cost:   41
c ---[ 521]---> BDD-cost:   41
c ---[ 520]---> BDD-cost:   44
c ---[ 519]---> BDD-cost:   47
c ---[ 518]---> BDD-cost:   50
c ---[ 517]---> BDD-cost:   50
c ---[ 516]---> BDD-cost:   50
c ---[ 515]---> BDD-cost:   53
c ---[ 514]---> BDD-cost:   56
c ---[ 513]---> BDD-cost:   47
c ---[ 512]---> BDD-cost:   53
c ---[ 511]---> BDD-cost:   53
c ---[ 510]---> BDD-cost:   47
c ---[ 509]---> BDD-cost:   47
c ---[ 508]---> BDD-cost:   41
c ---[ 507]---> BDD-cost:   35
c ---[ 506]---> BDD-cost:   24
c ---[ 505]---> BDD-cost:   29
c ---[ 504]---> BDD-cost:   26
c ---[ 503]---> BDD-cost:   26
c ---[ 502]---> BDD-cost:   23
c ---[ 501]---> BDD-cost:   32
c ---[ 500]---> BDD-cost:   26
c ---[ 499]---> BDD-cost:   26
c ---[ 498]---> BDD-cost:   17
c ---[ 497]---> BDD-cost:   14
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:   17
c ---[ 494]---> BDD-cost:   29
c ---[ 493]---> BDD-cost:   26
c ---[ 492]---> BDD-cost:   32
c ---[ 491]---> BDD-cost:   38
c ---[ 490]---> BDD-cost:   38
c ---[ 489]---> BDD-cost:   47
c ---[ 488]---> BDD-cost:   44
c ---[ 487]---> BDD-cost:   41
c ---[ 486]---> BDD-cost:   50
c ---[ 485]---> BDD-cost:   56
c ---[ 484]---> BDD-cost:   56
c ---[ 483]---> BDD-cost:   56
c ---[ 482]---> BDD-cost:   50
c ---[ 481]---> BDD-cost:   47
c ---[ 480]---> BDD-cost:   44
c ---[ 479]---> BDD-cost:   44
c ---[ 478]---> BDD-cost:   38
c ---[ 477]---> BDD-cost:   36
c ---[ 476]---> BDD-cost:   35
c ---[ 475]---> BDD-cost:   38
c ---[ 474]---> BDD-cost:   38
c ---[ 473]---> BDD-cost:   35
c ---[ 472]---> BDD-cost:   41
c ---[ 471]---> BDD-cost:   32
c ---[ 470]---> BDD-cost:   32
c ---[ 469]---> BDD-cost:   20
c ---[ 468]---> BDD-cost:   20
c ---[ 467]---> BDD-cost:   11
c ---[ 466]---> BDD-cost:   11
c ---[ 465]---> BDD-cost:   23
c ---[ 464]---> BDD-cost:   35
c ---[ 463]---> BDD-cost:   44
c ---[ 462]---> BDD-cost:   41
c ---[ 461]---> BDD-cost:   47
c ---[ 460]---> BDD-cost:   47
c ---[ 459]---> BDD-cost:   45
c ---[ 458]---> BDD-cost:   47
c ---[ 457]---> BDD-cost:   50
c ---[ 456]---> BDD-cost:   56
c ---[ 455]---> BDD-cost:   50
c ---[ 454]---> BDD-cost:   53
c ---[ 453]---> BDD-cost:   38
c ---[ 452]---> BDD-cost:   35
c ---[ 451]---> BDD-cost:   41
c ---[ 450]---> BDD-cost:   41
c ---[ 449]---> BDD-cost:   35
c ---[ 448]---> BDD-cost:   38
c ---[ 447]---> BDD-cost:   44
c ---[ 446]---> BDD-cost:   41
c ---[ 445]---> BDD-cost:   38
c ---[ 444]---> BDD-cost:   41
c ---[ 443]---> BDD-cost:   41
c ---[ 442]---> BDD-cost:   35
c ---[ 441]---> BDD-cost:   35
c ---[ 440]---> BDD-cost:   29
c ---[ 439]---> BDD-cost:   20
c ---[ 438]---> BDD-cost:   14
c ---[ 437]---> BDD-cost:   12
c ---[ 436]---> BDD-cost:   14
c ---[ 435]---> BDD-cost:   20
c ---[ 434]---> BDD-cost:   35
c ---[ 433]---> BDD-cost:   38
c ---[ 432]---> BDD-cost:   50
c ---[ 431]---> BDD-cost:   50
c ---[ 430]---> BDD-cost:   50
c ---[ 429]---> BDD-cost:   41
c ---[ 428]---> BDD-cost:   47
c ---[ 427]---> BDD-cost:   50
c ---[ 426]---> BDD-cost:   50
c ---[ 425]---> BDD-cost:   38
c ---[ 424]---> BDD-cost:   41
c ---[ 423]---> BDD-cost:   30
c ---[ 422]---> BDD-cost:   35
c ---[ 421]---> BDD-cost:   29
c ---[ 420]---> BDD-cost:   32
c ---[ 419]---> BDD-cost:   32
c ---[ 418]---> BDD-cost:   41
c ---[ 417]---> BDD-cost:   41
c ---[ 416]---> BDD-cost:   41
c ---[ 415]---> BDD-cost:   41
c ---[ 414]---> BDD-cost:   41
c ---[ 413]---> BDD-cost:   50
c ---[ 412]---> BDD-cost:   41
c ---[ 411]---> BDD-cost:   41
c ---[ 410]---> BDD-cost:   29
c ---[ 409]---> BDD-cost:   20
c ---[ 408]---> BDD-cost:   14
c ---[ 407]---> BDD-cost:   14
c ---[ 406]---> BDD-cost:   14
c ---[ 405]---> BDD-cost:   20
c ---[ 404]---> BDD-cost:   26
c ---[ 403]---> BDD-cost:   29
c ---[ 402]---> BDD-cost:   44
c ---[ 401]---> BDD-cost:   47
c ---[ 400]---> BDD-cost:   53
c ---[ 399]---> BDD-cost:   44
c ---[ 398]---> BDD-cost:   44
c ---[ 397]---> BDD-cost:   38
c ---[ 396]---> BDD-cost:   35
c ---[ 395]---> BDD-cost:   26
c ---[ 394]---> BDD-cost:   35
c ---[ 393]---> BDD-cost:   23
c ---[ 392]---> BDD-cost:   26
c ---[ 391]---> BDD-cost:   32
c ---[ 390]---> BDD-cost:   32
c ---[ 389]---> BDD-cost:   29
c ---[ 388]---> BDD-cost:   32
c ---[ 387]---> BDD-cost:   45
c ---[ 386]---> BDD-cost:   44
c ---[ 385]---> BDD-cost:   44
c ---[ 384]---> BDD-cost:   41
c ---[ 383]---> BDD-cost:   47
c ---[ 382]---> BDD-cost:   47
c ---[ 381]---> BDD-cost:   50
c ---[ 380]---> BDD-cost:   32
c ---[ 379]---> BDD-cost:   29
c ---[ 378]---> BDD-cost:   11
c ---[ 377]---> BDD-cost:    8
c ---[ 376]---> BDD-cost:   14
c ---[ 375]---> BDD-cost:   20
c ---[ 374]---> BDD-cost:   23
c ---[ 373]---> BDD-cost:   27
c ---[ 372]---> BDD-cost:   38
c ---[ 371]---> BDD-cost:   32
c ---[ 370]---> BDD-cost:   47
c ---[ 369]---> BDD-cost:   35
c ---[ 368]---> BDD-cost:   35
c ---[ 367]---> BDD-cost:   26
c ---[ 366]---> BDD-cost:   23
c ---[ 365]---> BDD-cost:   23
c ---[ 364]---> BDD-cost:   23
c ---[ 363]---> BDD-cost:   17
c ---[ 362]---> BDD-cost:   23
c ---[ 361]---> BDD-cost:   20
c ---[ 360]---> BDD-cost:   26
c ---[ 359]---> BDD-cost:   29
c ---[ 358]---> BDD-cost:   38
c ---[ 357]---> BDD-cost:   47
c ---[ 356]---> BDD-cost:   50
c ---[ 355]---> BDD-cost:   50
c ---[ 354]---> BDD-cost:   47
c ---[ 353]---> BDD-cost:   50
c ---[ 352]---> BDD-cost:   44
c ---[ 351]---> BDD-cost:   53
c ---[ 350]---> BDD-cost:   47
c ---[ 349]---> BDD-cost:   29
c ---[ 348]---> BDD-cost:   14
c ---[ 347]---> BDD-cost:   11
c ---[ 346]---> BDD-cost:   11
c ---[ 345]---> BDD-cost:   17
c ---[ 344]---> BDD-cost:   26
c ---[ 343]---> BDD-cost:   26
c ---[ 342]---> BDD-cost:   30
c ---[ 341]---> BDD-cost:   26
c ---[ 340]---> BDD-cost:   29
c ---[ 339]---> BDD-cost:   23
c ---[ 338]---> BDD-cost:   32
c ---[ 337]---> BDD-cost:   32
c ---[ 336]---> BDD-cost:   23
c ---[ 335]---> BDD-cost:   14
c ---[ 334]---> BDD-cost:   23
c ---[ 333]---> BDD-cost:   14
c ---[ 332]---> BDD-cost:   20
c ---[ 331]---> BDD-cost:   14
c ---[ 330]---> BDD-cost:   17
c ---[ 329]---> BDD-cost:   20
c ---[ 328]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   44
c ---[ 326]---> BDD-cost:   53
c ---[ 325]---> BDD-cost:   47
c ---[ 324]---> BDD-cost:   50
c ---[ 323]---> BDD-cost:   53
c ---[ 322]---> BDD-cost:   56
c ---[ 321]---> BDD-cost:   47
c ---[ 320]---> BDD-cost:   38
c ---[ 319]---> BDD-cost:   29
c ---[ 318]---> BDD-cost:   17
c ---[ 317]---> BDD-cost:    8
c ---[ 316]---> BDD-cost:    8
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   20
c ---[ 313]---> BDD-cost:   23
c ---[ 312]---> BDD-cost:   26
c ---[ 311]---> BDD-cost:   26
c ---[ 310]---> BDD-cost:   26
c ---[ 309]---> BDD-cost:   26
c ---[ 308]---> BDD-cost:   26
c ---[ 307]---> BDD-cost:   26
c ---[ 306]---> BDD-cost:   23
c ---[ 305]---> BDD-cost:   17
c ---[ 304]---> BDD-cost:   11
c ---[ 303]---> BDD-cost:   11
c ---[ 302]---> BDD-cost:   17
c ---[ 301]---> BDD-cost:   12
c ---[ 300]---> BDD-cost:   11
c ---[ 299]---> BDD-cost:   14
c ---[ 298]---> BDD-cost:   26
c ---[ 297]---> BDD-cost:   29
c ---[ 296]---> BDD-cost:   41
c ---[ 295]---> BDD-cost:   44
c ---[ 294]---> BDD-cost:   47
c ---[ 293]---> BDD-cost:   44
c ---[ 292]---> BDD-cost:   50
c ---[ 291]---> BDD-cost:   38
c ---[ 290]---> BDD-cost:   26
c ---[ 289]---> BDD-cost:   17
c ---[ 288]---> BDD-cost:   14
c ---[ 287]---> BDD-cost:   11
c ---[ 286]---> BDD-cost:   17
c ---[ 285]---> BDD-cost:   20
c ---[ 284]---> BDD-cost:   32
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:   26
c ---[ 281]---> BDD-cost:   26
c ---[ 280]---> BDD-cost:   23
c ---[ 279]---> BDD-cost:   26
c ---[ 278]---> BDD-cost:   20
c ---[ 277]---> BDD-cost:   17
c ---[ 276]---> BDD-cost:   14
c ---[ 275]---> BDD-cost:   11
c ---[ 274]---> BDD-cost:   14
c ---[ 273]---> BDD-cost:   14
c ---[ 272]---> BDD-cost:   14
c ---[ 271]---> BDD-cost:   11
c ---[ 270]---> BDD-cost:   17
c ---[ 269]---> BDD-cost:   23
c ---[ 268]---> BDD-cost:   32
c ---[ 267]---> BDD-cost:   38
c ---[ 266]---> BDD-cost:   44
c ---[ 265]---> BDD-cost:   35
c ---[ 264]---> BDD-cost:   41
c ---[ 263]---> BDD-cost:   35
c ---[ 262]---> BDD-cost:   26
c ---[ 261]---> BDD-cost:   17
c ---[ 260]---> BDD-cost:    8
c ---[ 259]---> BDD-cost:   12
c ---[ 258]---> BDD-cost:   23
c ---[ 257]---> BDD-cost:   26
c ---[ 256]---> BDD-cost:   32
c ---[ 255]---> BDD-cost:   32
c ---[ 254]---> BDD-cost:   29
c ---[ 253]---> BDD-cost:   29
c ---[ 252]---> BDD-cost:   29
c ---[ 251]---> BDD-cost:   18
c ---[ 250]---> BDD-cost:   20
c ---[ 249]---> BDD-cost:   20
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   11
c ---[ 246]---> BDD-cost:   14
c ---[ 245]---> BDD-cost:   20
c ---[ 244]---> BDD-cost:   20
c ---[ 243]---> BDD-cost:   17
c ---[ 242]---> BDD-cost:   23
c ---[ 241]---> BDD-cost:   21
c ---[ 240]---> BDD-cost:   26
c ---[ 239]---> BDD-cost:   30
c ---[ 238]---> BDD-cost:   38
c ---[ 237]---> BDD-cost:   35
c ---[ 236]---> BDD-cost:   29
c ---[ 235]---> BDD-cost:   35
c ---[ 234]---> BDD-cost:   30
c ---[ 233]---> BDD-cost:   23
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   11
c ---[ 230]---> BDD-cost:   14
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:   32
c ---[ 227]---> BDD-cost:   35
c ---[ 226]---> BDD-cost:   29
c ---[ 225]---> BDD-cost:   29
c ---[ 224]---> BDD-cost:   35
c ---[ 223]---> BDD-cost:   35
c ---[ 222]---> BDD-cost:   29
c ---[ 221]---> BDD-cost:   29
c ---[ 220]---> BDD-cost:   17
c ---[ 219]---> BDD-cost:   17
c ---[ 218]---> BDD-cost:   17
c ---[ 217]---> BDD-cost:   26
c ---[ 216]---> BDD-cost:   26
c ---[ 215]---> BDD-cost:   23
c ---[ 214]---> BDD-cost:   29
c ---[ 213]---> BDD-cost:   26
c ---[ 212]---> BDD-cost:   26
c ---[ 211]---> BDD-cost:   29
c ---[ 210]---> BDD-cost:   32
c ---[ 209]---> BDD-cost:   32
c ---[ 208]---> BDD-cost:   35
c ---[ 207]---> BDD-cost:   35
c ---[ 206]---> BDD-cost:   29
c ---[ 205]---> BDD-cost:   23
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:   14
c ---[ 202]---> BDD-cost:   17
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:   26
c ---[ 199]---> BDD-cost:   29
c ---[ 198]---> BDD-cost:   38
c ---[ 197]---> BDD-cost:   35
c ---[ 196]---> BDD-cost:   26
c ---[ 195]---> BDD-cost:   35
c ---[ 194]---> BDD-cost:   32
c ---[ 193]---> BDD-cost:   26
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   26
c ---[ 190]---> BDD-cost:   23
c ---[ 189]---> BDD-cost:   29
c ---[ 188]---> BDD-cost:   35
c ---[ 187]---> BDD-cost:   29
c ---[ 186]---> BDD-cost:   32
c ---[ 185]---> BDD-cost:   38
c ---[ 184]---> BDD-cost:   29
c ---[ 183]---> BDD-cost:   23
c ---[ 182]---> BDD-cost:   20
c ---[ 181]---> BDD-cost:   26
c ---[ 180]---> BDD-cost:   32
c ---[ 179]---> BDD-cost:   26
c ---[ 178]---> BDD-cost:   32
c ---[ 177]---> BDD-cost:   26
c ---[ 176]---> BDD-cost:   23
c ---[ 175]---> BDD-cost:   20
c ---[ 174]---> BDD-cost:   14
c ---[ 173]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   23
c ---[ 171]---> BDD-cost:   29
c ---[ 170]---> BDD-cost:   32
c ---[ 169]---> BDD-cost:   29
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   35
c ---[ 166]---> BDD-cost:   29
c ---[ 165]---> BDD-cost:   26
c ---[ 164]---> BDD-cost:   32
c ---[ 163]---> BDD-cost:   26
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   26
c ---[ 160]---> BDD-cost:   32
c ---[ 159]---> BDD-cost:   35
c ---[ 158]---> BDD-cost:   26
c ---[ 157]---> BDD-cost:   29
c ---[ 156]---> BDD-cost:   35
c ---[ 155]---> BDD-cost:   32
c ---[ 154]---> BDD-cost:   23
c ---[ 153]---> BDD-cost:   23
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   23
c ---[ 150]---> BDD-cost:   29
c ---[ 149]---> BDD-cost:   26
c ---[ 148]---> BDD-cost:   17
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   17
c ---[ 145]---> BDD-cost:   17
c ---[ 144]---> BDD-cost:   20
c ---[ 143]---> BDD-cost:   29
c ---[ 142]---> BDD-cost:   35
c ---[ 141]---> BDD-cost:   32
c ---[ 140]---> BDD-cost:   23
c ---[ 139]---> BDD-cost:   20
c ---[ 138]---> BDD-cost:   26
c ---[ 137]---> BDD-cost:   32
c ---[ 136]---> BDD-cost:   32
c ---[ 135]---> BDD-cost:   32
c ---[ 134]---> BDD-cost:   29
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   29
c ---[ 131]---> BDD-cost:   35
c ---[ 130]---> BDD-cost:   35
c ---[ 129]---> BDD-cost:   32
c ---[ 128]---> BDD-cost:   29
c ---[ 127]---> BDD-cost:   38
c ---[ 126]---> BDD-cost:   38
c ---[ 125]---> BDD-cost:   41
c ---[ 124]---> BDD-cost:   32
c ---[ 123]---> BDD-cost:   32
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   26
c ---[ 120]---> BDD-cost:   29
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:   17
c ---[ 117]---> BDD-cost:   14
c ---[ 116]---> BDD-cost:    8
c ---[ 115]---> BDD-cost:   17
c ---[ 114]---> BDD-cost:   23
c ---[ 113]---> BDD-cost:   20
c ---[ 112]---> BDD-cost:   29
c ---[ 111]---> BDD-cost:   32
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   26
c ---[ 108]---> BDD-cost:   23
c ---[ 107]---> BDD-cost:   29
c ---[ 106]---> BDD-cost:   29
c ---[ 105]---> BDD-cost:   23
c ---[ 104]---> BDD-cost:   29
c ---[ 103]---> BDD-cost:   29
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:   38
c ---[ 100]---> BDD-cost:   38
c ---[  99]---> BDD-cost:   36
c ---[  98]---> BDD-cost:   32
c ---[  97]---> BDD-cost:   38
c ---[  96]---> BDD-cost:   44
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:   38
c ---[  93]---> BDD-cost:   38
c ---[  92]---> BDD-cost:   35
c ---[  91]---> BDD-cost:   32
c ---[  90]---> BDD-cost:   26
c ---[  89]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   20
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:    7
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:   26
c ---[  81]---> BDD-cost:   23
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   26
c ---[  78]---> BDD-cost:   27
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   20
c ---[  75]---> BDD-cost:   20
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   23
c ---[  72]---> BDD-cost:   29
c ---[  71]---> BDD-cost:   35
c ---[  70]---> BDD-cost:   38
c ---[  69]---> BDD-cost:   35
c ---[  68]---> BDD-cost:   38
c ---[  67]---> BDD-cost:   38
c ---[  66]---> BDD-cost:   35
c ---[  65]---> BDD-cost:   38
c ---[  64]---> BDD-cost:   35
c ---[  63]---> BDD-cost:   35
c ---[  62]---> BDD-cost:   32
c ---[  61]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   20
c ---[  59]---> BDD-cost:   17
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:    3
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   20
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   17
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   17
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   20
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   23
c ---[  42]---> BDD-cost:   26
c ---[  41]---> BDD-cost:   26
c ---[  40]---> BDD-cost:   26
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   29
c ---[  37]---> BDD-cost:   38
c ---[  36]---> BDD-cost:   29
c ---[  35]---> BDD-cost:   30
c ---[  34]---> BDD-cost:   29
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   24
c ---[  31]---> BDD-cost:   23
c ---[  30]---> BDD-cost:   17
c ---[  29]---> BDD-cost:   17
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    5
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:    8
c ---[  18]---> BDD-cost:    8
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:    8
c ---[  14]---> BDD-cost:   17
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   20
c ---[  11]---> BDD-cost:   23
c ---[  10]---> BDD-cost:   26
c ---[   9]---> BDD-cost:   17
c ---[   8]---> BDD-cost:   23
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   23
c ---[   5]---> BDD-cost:   21
c ---[   4]---> BDD-cost:   23
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   62745   180525 |   20915       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 5404[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:591012     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  826468  1966881 |  275489       0        0     nan |  0.000 % |
c |       100 |  824543  1962781 |  303037      64     1008    15.8 |  0.374 % |
c |       250 |  824113  1961835 |  333341     194     2314    11.9 |  0.409 % |
c |       476 |  823891  1961342 |  366675     418     5485    13.1 |  0.434 % |
c |       813 |  822823  1959007 |  403343     739    10648    14.4 |  0.551 % |
c |      1323 |  822823  1959007 |  443677    1249    22567    18.1 |  0.551 % |
c |      2082 |  822823  1959007 |  488045    2008    39789    19.8 |  0.551 % |
c |      3222 |  822761  1958877 |  536850    3146    67836    21.6 |  0.558 % |
c |      4930 |  822509  1958343 |  590535    4847   115599    23.8 |  0.584 % |
c |      7492 |  822034  1957288 |  649588    7387   150309    20.3 |  0.637 % |
c |     11339 |  821644  1956412 |  714547   11227   274162    24.4 |  0.682 % |
c |     17107 |  821030  1955074 |  786002   16974   466648    27.5 |  0.750 % |
c |     25756 |  818643  1949808 |  864602   25535   725270    28.4 |  1.016 % |
c ==============================================================================
c [1mFound solution: 641[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38194 | 1093913  2592262 |  364637   37962  1093585    28.8 |  1.016 % |
c |     38294 | 1093913  2592262 |  401100   38062  1093950    28.7 |  1.016 % |
c |     38444 | 1093913  2592262 |  441210   38212  1096602    28.7 |  1.016 % |
c |     38669 | 1093913  2592262 |  485331   38437  1099341    28.6 |  1.016 % |
c |     39006 | 1093913  2592262 |  533865   38774  1102199    28.4 |  1.016 % |
c |     39512 | 1093617  2591576 |  587251   39278  1106703    28.2 |  1.039 % |
c |     40272 | 1093617  2591576 |  645976   40038  1118601    27.9 |  1.039 % |
c |     41411 | 1093617  2591576 |  710574   41177  1126424    27.4 |  1.039 % |
c |     43119 | 1093617  2591576 |  781631   42885  1142529    26.6 |  1.039 % |
c |     45681 | 1092463  2588899 |  859794   45428  1171255    25.8 |  1.129 % |
c |     49525 | 1092343  2588645 |  945774   49268  1244906    25.3 |  1.141 % |
c |     55291 | 1092156  2588215 | 1040351   55027  1329845    24.2 |  1.152 % |
c |     63940 | 1091540  2586869 | 1144387   63650  1512509    23.8 |  1.209 % |
c |     76914 | 1091142  2585964 | 1258825   76615  1662903    21.7 |  1.237 % |
c |     96376 | 1090979  2585591 | 1384708   96071  2210601    23.0 |  1.246 % |
c |    125568 | 1089321  2581865 | 1523179  125126  2740150    21.9 |  1.387 % |
c |    169359 | 1089265  2581747 | 1675497  168916  3963005    23.5 |  1.393 % |
c |    235044 | 1088031  2578952 | 1843046  234540  5926007    25.3 |  1.489 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v4221 -v3659 -v4226 v3780 -v3680 -v3132 -v2610 -v4225 -v3895 v3779 -v3679 -v2609 v334 v4026 v3781 -v3133 -v2615 -v1996 v335 -v4228 v4025 -v3894 v3782 -v3681 v3135 -v2614 v1405 -v1103 -v559 -v338 -v4229 -v4031 -v3898 v3783 -v3683 v3136 -v2616 -v1997 -v1108 -v336 -v4232 -v4030 -v3790 v2620 -v1999 v1408 -v1107 -v558 v416 -v337 -v4230 -v4032 -v3899 -v3784 -v3684 v2619 -v2000 v1409 -v1083 v562 v4476 -v4285 -v4231 v4036 -v3785 -v3724 -v3686 v2617 -v1359 -v1225 -v1110 -v1082 v4035 -v3786 -v3723 -v3687 v2618 -v1230 -v1111 -v1088 v563 -v4479 -v4284 v4033 -v3725 v3310 -v1229 -v1114 -v1087 -v4480 v4034 v3728 -v1112 -v1089 -v654 -v4290 v3727 v3309 v2165 -v1232 -v1113 -v1093 v989 -v653 -v4335 -v4288 -v3732 -v1233 -v1092 -v655 -v4334 -v3731 -v3315 v2164 -v1236 -v1090 v992 -v656 v387 -v4289 -v3729 -v3313 -v1234 -v1091 v993 -v657 v391 v4359 -v4336 -v4293 -v3730 v2170 -v1235 -v853 -v664 v4338 -v3314 v2168 -v858 -v658 v4362 v3318 -v857 -v659 v4363 v4339 v2169 -v660 v4341 v3572 v2173 -v860 v52 v4342 v3571 v1979 -v861 -v56 v3708 v3573 v1978 v1336 -v864 -v316 v4621 v1983 -v862 -v3634 v1982 v1335 -v863 -v319 v3638 -v4622 -v320 v3655 -v3148 -v3130 -v1993 v3658 -v1992 -v4220 -v3675 -v3134 -v4222 -v3674 v3138 -v1938 -v4227 v3137 -v2611 -v1998 -v339 -v4224 -v3896 -v3793 -v3682 -v2612 -v2002 v1404 -v638 -v412 -v4233 v4027 -v3900 -v3794 -v3685 v2613 -v2001 -v1102 v4028 -v3789 -v3689 -v2624 -v2451 v1410 -v1355 -v1104 -v560 v415 v4029 -v3688 -v2455 -v1109 v564 v4475 v4280 v4040 -v3902 -v3787 -v1358 -v1106 -v3903 -v1224 -v1115 -v1084 -v4481 -v4286 v3305 -v1413 -v1226 -v1085 -v833 -v566 -v3726 -v1231 -v1086 -v837 -v567 -v4291 v3740 v3311 -v2160 -v1228 -v1097 v988 -v4330 -v3736 -v1237 v4484 -v4329 -v4294 -v3735 -v3316 v2166 v994 -v667 v386 -v4292 -v668 v390 v4358 -v4337 v3319 v2171 -v663 v4340 v3317 -v852 v4364 v4344 v2174 -v997 -v854 -v661 v4343 v2172 -v859 -v3704 -v856 v51 -v865 -v55 -v4367 v3707 -v315 -v224 v3574 v1980 -v228 v3633 -v3582 v1981 v1337 -v321 v3637 -v3578 -v3577 -v1987 v1459 v3654 -v3147 -v3129 v3660 -v3131 -v1934 -v3890 -v1994 v4268 -v3889 -v3792 -v3142 -v1995 v1937 -v1400 -v634 -v347 -v4223 -v3791 -v3676 v554 -v343 -v4241 -v3897 -v3677 v3663 -v3456 v2627 -v2006 v1406 -v637 v553 -v411 -v342 -v4237 -v3901 -v3678 v2628 -v4471 -v4236 -v4043 -v3905 -v3693 -v3285 -v2623 v2450 v1411 -v1354 -v561 v417 -v4044 -v3904 -v3289 -v2454 -v1105 v565 v4477 v4039 -v3788 -v2621 v1414 -v1360 -v1123 -v569 v4279 -v1412 -v1119 -v568 -v4482 v4281 v4037 v3737 -v1118 -v1100 -v984 -v832 -v420 -v4287 v3739 v3304 -v1227 -v1101 -v836 v4485 v4283 v3306 -v1363 -v1245 -v1096 v990 -v666 -v512 v4483 -v4295 v3312 -v2159 -v1241 -v665 -v516 -v4354 -v3733 v3308 -v2161 -v1240 -v1094 v995 -v491 v388 -v4331 v3320 v2167 v392 v4360 -v4332 -v3734 v2163 -v998 v4333 v2175 -v996 v4365 v4348 -v662 -v394 -v855 -v395 -v4368 v3703 -v873 v311 v53 -v4366 -v1332 -v869 -v57 v3709 -v3579 v1719 -v1331 -v868 -v317 -v223 -v3581 -v1723 -v227 v3635 -v1990 v1455 v1338 -v322 v59 v3639 -v1991 v60 -v3712 -v3575 -v1986 v1458 -v1339 -v541 v323 -v1340 v324 v3656 -v3149 -v2279 v4269 v3661 v3145 -v1933 -v344 v4267 v3146 -v346 -v4238 v3664 -v3452 -v3153 -v3141 v2626 -v2194 -v2009 v1939 -v633 -v407 -v4240 -v3891 v3662 v2625 -v2010 -v1399 -v4042 -v3892 -v3696 -v3455 -v3213 -v3139 -v2005 -v1401 -v1350 -v639 -v413 -v340 -v4041 v3893 -v3697 -v3217 v1407 v555 -v4234 v3909 -v3692 -v3284 v2452 -v2003 -v1942 v1403 -v1356 -v1120 v556 v418 -v341 -v4470 -v3288 -v2456 v1415 -v1122 v557 -v4472 -v4235 -v3690 -v2622 -v1361 -v1099 -v642 -v573 -v421 v4478 -v3738 -v1098 -v419 v4474 v4038 v2458 -v1364 -v1242 -v1116 -v834 -v462 v4486 v4282 v2459 -v1362 -v1244 -v983 -v838 -v466 v382 -v4303 -v1117 -v985 -v511 -v487 v381 -v4299 v3307 v991 -v515 -v4298 v3328 -v1238 -v1095 v987 v840 -v490 v389 -v4353 v3324 -v2162 -v999 v841 v393 v4355 -v4351 v3323 v2183 -v1239 -v397 v4361 -v4352 -v2179 -v396 v47 v4357 v4347 -v3699 -v2178 -v870 v46 -v4369 -v872 v4345 v3705 v54 v3629 -v3580 v310 -v58 v3710 v3628 -v2263 -v1989 v1718 -v866 v312 -v225 v62 -v1988 -v1722 -v1333 -v318 -v229 v61 -v3801 v3713 v3636 v1454 -v1334 -v867 -v537 v314 -v3805 v3711 v3640 v325 v3641 -v3576 -v1984 v1460 v1344 -v540 -v231 v3642 -v232 v3652 -v3150 v3144 -v2278 v1929 v4270 v3657 v3143 -v345 v3653 -v3154 v2190 -v2008 -v1935 -v629 -v4239 v3665 -v3152 -v2007 -v3695 -v3451 -v2193 -v2046 v1940 -v635 -v3694 v2446 -v406 v3912 -v3457 -v3212 -v3140 -v2789 v2445 -v1943 -v640 -v408 v3913 -v3216 -v1941 -v1402 -v1349 -v1121 -v414 v3908 -v3286 v2453 -v2004 -v1423 -v1351 -v643 v576 v410 -v3290 -v2457 -v1419 -v1357 v828 -v641 v577 -v422 v3906 -v3691 -v3460 v2461 -v1811 -v1418 -v1353 v827 -v572 -v203 -v4473 v2460 -v1815 -v1365 -v1243 -v4494 -v4300 -v3292 -v835 -v570 v461 -v4490 -v4302 -v3293 -v839 -v465 -v4489 v3325 -v2928 v843 -v513 -v486 -v156 v3327 -v2932 -v986 v842 -v517 v383 -v4350 -v4296 v2180 -v1007 -v492 v384 -v4349 v2182 -v1003 v385 -v4297 v3321 -v1002 -v519 -v401 v4356 -v871 -v520 v4377 v3322 -v2176 v495 -v4373 -v3698 -v219 v48 -v4372 v4346 -v3700 -v2259 -v2177 -v218 v49 v3706 v50 v3702 -v2262 v1720 -v1450 -v226 -v66 v3714 v3630 -v1724 v313 -v230 -v4579 -v3800 v3631 v1456 v1347 -v536 v333 -v234 -v3804 v3632 v1348 -v329 -v233 v3646 -v1985 -v1726 v1461 v1343 -v542 -v328 -v1727 -v4278 -v3151 -v2280 -v808 -v294 v4274 v3651 -v3155 v1928 -v812 v4273 -v3673 -v3613 -v3447 v2189 -v2042 v1930 -v3669 -v1936 -v628 v3911 -v3668 -v3453 -v2839 -v2785 -v2284 -v2195 -v2045 v1932 -v630 v3910 -v3280 -v1944 -v636 -v3458 -v3279 -v3214 -v2788 -v1420 -v632 v575 -v3218 v2447 -v1422 -v644 v574 -v409 -v3461 -v3287 v2448 -v2301 -v2198 v430 -v199 -v3459 -v3291 v2449 -v2305 -v1352 v426 -v4491 v3907 -v3295 -v3220 v2465 -v1810 -v1416 -v1373 v425 -v202 -v4493 -v4301 -v3294 -v3221 -v1814 -v1369 v829 -v507 -v1417 -v1368 v830 -v571 -v506 v482 v463 -v152 v3326 v831 -v467 -v4487 -v2927 -v1836 -v1004 v847 -v514 -v488 -v155 -v2931 v2181 -v1840 -v1006 -v518 -v4488 -v522 -v493 -v469 v404 -v521 -v470 v405 v4374 -v1000 v496 -v400 v4376 v494 -v1001 -v398 v1714 -v4370 v2258 v1713 v69 -v3701 -v220 v70 -v4575 -v4371 -v3722 -v2264 v1721 -v1346 -v532 v330 -v221 -v65 v3718 -v1725 -v1449 v1345 v332 -v222 v4578 -v3802 v3717 -v3649 -v1729 -v1451 -v538 -v238 -v63 -v3806 -v3650 -v1728 v1457 v3645 -v2267 v1453 v1341 -v543 -v326 v1462 -v4277 -v3670 -v3609 -v3163 v2281 v2185 -v807 -v293 -v3672 -v3159 -v811 v4271 -v3612 -v3158 -v2835 -v2285 v2191 -v2041 -v3446 -v3208 -v2283 v1931 v4272 -v3666 -v3448 -v3207 -v2838 -v2784 v2196 -v2047 v1952 -v1573 -v3454 v1948 -v1421 -v631 -v3667 -v3450 -v3215 -v2790 -v2199 v1947 -v652 v427 -v3462 -v3281 -v3219 -v2197 -v648 v429 -v3282 -v3223 v2468 -v2300 -v2050 -v1370 -v647 -v198 -v4492 -v3283 -v3222 v2469 -v2304 -v1372 -v457 -v3299 v2793 v2464 -v1812 -v1619 v456 v423 -v204 -v1816 -v1623 -v4010 -v3357 v2462 -v1366 -v850 v464 v424 -v151 -v3361 -v1005 -v851 -v508 v481 -v468 -v2929 -v1835 -v1818 -v1367 v846 -v509 v483 -v472 v403 -v207 -v157 -v2933 -v1839 -v1819 -v510 -v489 -v471 v402 v844 -v526 v485 v4375 v497 -v2935 -v160 -v2936 -v2254 -v399 v68 v67 -v3719 v2260 v1786 -v3796 -v3721 -v1790 v1715 v331 -v4574 v3795 -v3648 -v2265 v1716 -v241 -v3647 v1717 -v531 -v242 v4580 -v3803 v3715 -v2268 -v1911 -v1733 -v533 -v237 -v64 -v3807 -v2266 v1915 -v1452 -v539 v3808 v3716 v3643 -v1470 v1342 -v535 -v327 -v235 v3809 -v1466 -v544 -v4275 -v3671 -v3608 -v3162 v2282 -v2037 -v809 -v295 -v2286 v2184 -v813 -v3614 -v3156 -v2834 -v2780 v2186 -v2043 v1949 v1569 v2192 v1951 -v3157 -v2840 -v2786 v2188 v2095 -v2048 -v1572 -v815 -v649 -v299 -v3449 -v3209 -v2200 -v816 -v651 v428 v3617 -v3470 -v3210 -v2791 v2467 -v2051 v1945 v194 -v3466 -v3211 v2466 -v2049 -v1806 -v1371 -v3465 -v3302 -v3227 -v2843 v2794 -v2302 v1946 -v1805 -v645 -v200 -v3303 v2792 -v2306 -v4006 -v3298 -v1813 -v1618 -v1434 -v849 -v646 -v205 v147 -v2923 -v1817 -v1622 -v848 v458 -v4009 -v3356 -v3296 -v2922 v2463 -v2308 -v1821 v459 -v208 -v153 -v3360 -v2309 -v1820 v460 -v206 v2978 -v2930 -v1837 -v529 -v476 -v158 -v2982 -v2934 -v1841 -v530 v484 -v2938 v845 v720 -v525 -v505 -v161 -v2937 v724 v501 -v159 v1843 -v523 v500 v1844 v2502 -v3720 -v2253 v4570 -v2764 -v2255 v1785 -v240 v2261 -v1789 -v239 -v4576 v2257 v1736 v3797 -v2269 v1737 v4581 v3798 -v1910 -v1732 -v1467 v3799 v1914 -v1469 -v534 -v4582 v3813 v3644 v3118 -v1730 -v552 -v236 v34 -v4583 -v3122 -v1465 -v548 -v4276 -v3610 -v3160 -v2830 -v2294 -v810 v740 -v296 -v2290 -v2036 -v1950 -v814 -v3615 -v2836 -v2289 v2091 -v2038 v1568 -v818 -v300 -v2779 v2187 -v2044 -v817 -v650 -v298 v3618 -v3467 -v2841 -v2781 -v2326 -v2208 v2094 -v2040 -v1574 v3616 -v3469 -v2787 -v2330 -v2296 -v2204 -v2052 -v3301 -v3230 -v2844 v2783 -v2295 -v2203 -v3300 -v3231 -v2842 v2795 v193 -v3463 -v3226 -v2430 -v2303 -v1577 -v1430 v195 -v2307 -v1807 -v201 -v4005 -v3464 -v3224 -v2311 -v1808 -v1620 -v1433 v197 -v2310 -v1831 -v1809 -v1624 -v209 v146 -v4011 -v3358 -v3297 v1959 -v1830 -v1825 -v790 -v528 -v479 v148 -v3362 -v2924 v1963 -v527 -v480 -v154 -v3751 v2977 -v2925 -v1838 -v1626 -v502 -v475 v150 v2981 -v2926 -v1842 -v1627 -v504 -v162 -v4014 -v3386 -v3364 -v2942 -v2116 v1846 v719 -v473 -v3365 -v2120 v1845 v723 -v2498 -v524 v498 -v2760 v2501 v499 -v2763 v1787 v1735 v4569 -v2256 -v1791 v1734 v4571 v2277 -v4577 -v2273 -v1468 v4573 -v3816 -v2272 -v1912 v1793 -v549 -v30 -v4584 -v3817 v1916 v1794 -v551 v3812 v3117 -v1731 v33 -v3121 -v1463 -v547 -v3606 -v3161 -v2293 v1564 -v806 v739 v297 -v3611 -v2829 -v805 -v301 v3607 -v2831 -v2287 -v2205 v2090 v1570 -v822 v3619 -v3468 -v2837 -v2207 -v2039 -v3229 -v2833 v2325 -v2288 v2096 -v2060 -v1575 -v3228 -v2845 -v2782 -v2329 -v2056 -v2803 -v2426 -v2201 -v2055 -v1578 -v1180 v81 -v2799 v2297 -v1614 -v1576 -v1184 -v4001 v3920 -v2798 -v2429 v2298 -v2202 -v2099 -v1673 -v1613 -v1429 -v3924 -v3352 v2299 v196 -v4007 -v3351 -v3225 -v2315 -v1828 -v1621 -v1435 -v786 -v478 -v217 -v1829 -v1625 -v477 -v213 -v4012 -v3747 -v3359 v1958 -v1824 -v1629 -v789 -v212 -v3363 v1962 -v1832 -v1628 -v503 v149 -v4015 -v3750 -v3382 -v3367 v2979 -v2945 -v1833 -v1822 -v1594 -v1438 -v170 -v4013 -v3366 v2983 -v2946 v1834 -v1598 -v166 -v3385 -v2941 -v2115 -v1850 v721 -v474 -v165 -v2119 v725 -v2985 -v2939 -v2497 -v253 -v2986 -v1781 -v2759 v2503 v1780 v727 v728 -v2765 v2274 v1788 v2276 -v1906 -v1792 -v3815 -v2506 -v1905 v1796 v4572 -v3814 v1795 -v550 v4592 -v2768 -v2270 -v1913 -v29 -v7 -v4588 v1917 -v11 -v4587 v3810 v3119 -v2271 v1918 v35 -v3123 v1919 -v1464 -v545 -v2291 -v2086 -v1315 -v825 v741 v309 -v3605 -v2206 v1563 -v826 v305 -v3627 -v2590 v2092 -v2057 v1565 -v821 v304 -v3623 -v2832 -v2594 -v2059 v1571 -v3622 -v2853 -v2800 v2327 v2097 v2021 v1567 -v819 -v745 v77 -v2849 -v2802 -v2331 -v1579 -v4426 -v2848 -v2425 -v2100 -v2053 -v1669 -v1425 -v1179 v80 -v4430 -v2098 -v1183 v3919 -v2953 -v2796 v2431 -v2333 v2318 -v2054 -v1827 -v1672 v1431 -v214 -v4000 -v3923 -v2957 -v2334 v2319 -v1826 -v1615 -v216 -v4130 v4002 -v2797 -v2314 -v1616 -v1436 -v785 -v4008 v3353 -v2973 -v1617 v4004 -v3746 v3354 -v2972 -v2944 v2635 -v2434 -v2312 v1960 -v1633 -v1439 -v791 -v210 -v167 -v4016 v3355 -v2943 -v2639 v1964 -v1437 -v715 -v169 -v3752 -v3381 -v3371 v2980 v1865 v1853 -v1823 -v1593 -v714 -v211 v2984 v1854 -v1597 -v3387 v2988 -v2493 v2117 -v1966 -v1849 -v794 v722 -v249 -v163 v2987 v2121 -v1967 v726 -v3755 -v2940 -v2755 v2499 -v1847 v730 -v252 -v164 v729 -v4155 -v3390 -v2761 v2504 v2123 v2275 v2124 v1782 -v2766 -v2507 v1783 -v2505 v1784 v4589 -v4505 -v2769 v1800 v25 v4591 -v3113 -v2767 -v1907 -v3112 v1908 -v31 -v6 v1909 v10 -v4585 v3811 v3120 v1923 v370 v36 -v3124 -v546 -v374 -v3624 -v2292 -v1314 -v823 v742 v308 -v3626 v2321 -v2085 -v2058 -v3019 -v2850 -v2589 v2320 -v2087 -v2017 -v746 v302 -v3023 -v2852 -v2801 -v2593 v2093 v1566 -v744 -v3620 v2421 v2328 v2089 v2020 v1587 -v820 v303 v76 -v2332 -v2101 -v1583 -v4425 -v3621 -v2846 -v2427 -v2336 v2317 -v1668 -v1582 -v1181 v82 -v4429 -v2335 v2316 -v1424 -v1185 -v215 -v4126 v3921 -v2952 -v2847 v2432 -v1674 -v1426 -v781 -v3925 -v2956 -v1954 v1432 -v4129 -v3742 -v2435 -v1953 -v1636 v1428 -v1187 -v787 v85 v4003 -v2433 -v1637 -v1440 -v1188 -v168 v4024 -v3927 -v3748 -v3377 -v3374 v2634 -v2313 v1961 v1861 v1852 -v1677 -v1632 -v792 v4020 -v3928 -v3375 -v2974 -v2638 -v2111 v1965 v1851 v4019 -v3753 -v3383 -v3370 -v2975 -v2110 -v1969 v1864 -v1630 -v1595 -v795 v2976 -v1968 -v1599 -v793 -v716 -v3756 -v3388 -v3368 v2992 v2118 -v717 -v613 -v248 -v3754 -v2492 v2122 v718 v4151 -v3391 -v2494 v2126 -v1848 -v1601 v734 -v254 -v3389 -v2754 v2500 v2125 -v1602 -v4154 -v2756 v2664 v2496 -v2762 -v2508 v4501 v3044 -v2758 -v1803 v1018 -v257 v4590 -v3048 -v2770 -v1804 -v4504 v1799 v24 -v1926 -v1797 v26 -v8 -v3114 -v1927 -v32 v12 -v4586 -v3115 v1922 v369 v28 v3116 -v373 -v37 -v3625 -v1316 -v824 v743 v306 -v2851 -v747 -v3018 -v2591 -v2016 v1584 -v72 -v3022 -v2595 v2322 -v2088 v1586 -v1175 v2323 v2109 v2022 -v1664 -v1320 -v1174 v78 -v3915 v2420 v2324 -v2105 -v4427 -v3981 v3914 -v2597 v2422 -v2340 -v2104 -v1670 -v1580 -v1182 v83 -v4431 -v3985 -v2598 -v2428 -v1186 -v4125 v3922 -v2954 v2424 -v2025 -v1675 -v1635 -v1581 -v1519 -v1190 v86 -v3926 -v2958 -v2436 -v1634 -v1523 -v1427 -v1189 -v780 v84 -v4433 -v4131 v4021 -v3930 -v3373 -v1678 -v1448 -v782 -v4434 v4023 -v3929 -v3741 -v3372 -v1955 -v1676 -v1589 -v1444 -v788 -v3743 -v2960 v2636 -v1956 v1860 -v1694 -v1588 -v1443 -v784 -v3749 -v3376 -v2961 -v2640 v1957 -v1698 -v796 -v4134 -v4017 -v3745 -v3378 v2995 -v1973 v1866 -v1631 -v1596 -v609 -v244 -v3757 -v3384 v2996 -v2112 -v1600 -v4248 -v4018 -v3380 -v3369 v2991 -v2642 -v2113 -v1604 -v737 -v612 -v250 -v4252 -v3392 -v2643 v2114 -v1603 -v738 v4150 v2989 -v2660 -v2130 -v1869 v733 -v255 -v2495 -v4156 v2663 -v2516 -v1802 -v1014 v731 -v258 -v2757 -v2512 -v1801 -v256 -v4530 v4500 -v4451 v3043 -v2778 -v2511 v1017 -v4455 v3047 -v2774 -v2 -v4506 -v4159 -v2773 -v1925 -v1380 -v934 -v1 -v1924 -v1384 -v1798 -v9 v27 v13 -v4509 -v3127 v2480 v1920 v371 -v45 v14 -v3128 -v375 v41 v15 -v3821 -v2586 v2012 -v1317 v755 v307 -v3825 -v1585 v751 -v3020 -v2592 v2106 -v2018 -v1321 v750 -v4421 -v3024 -v2596 v2108 -v1319 -v71 -v4420 -v2600 v2343 v2023 -v73 -v2948 -v2599 v2344 -v1663 v1176 v79 -v4428 -v4121 -v3980 -v3556 -v3026 -v2947 -v2339 -v2102 -v2026 -v1665 v1177 v75 -v4432 -v3984 v3916 -v3027 v2423 -v2024 -v1671 v1178 v87 -v4436 -v4127 v3917 -v2955 v2444 -v2337 -v2103 -v1667 -v1518 -v1445 -v1205 v1194 -v4435 -v4022 v3918 -v2959 -v2630 v2440 -v1679 -v1522 -v1447 -v1209 -v4132 -v3934 -v2963 v2629 v2439 -v1856 -v1063 -v2962 -v1067 -v783 v4135 -v2994 v2637 -v1976 v1862 -v1693 -v1441 -v804 v4133 -v3744 v2993 -v2641 -v1977 v1697 -v1590 -v800 -v3765 -v2645 -v1972 v1867 -v1591 -v1442 -v799 -v736 -v608 -v3761 -v3379 -v2644 -v1592 -v735 -v243 v4247 -v4146 -v3760 -v3400 -v2133 -v1970 -v1870 -v1608 v614 -v245 v4251 -v3396 -v2134 -v1868 -v251 v4152 -v3395 -v2990 -v2659 -v2513 -v2129 -v247 -v2515 -v259 -v4526 -v4496 -v4157 -v2775 v2665 -v2127 v1013 -v732 -v617 -v2777 -v4529 v4502 -v4450 -v4160 -v3242 v3045 -v2566 -v2509 v1019 -v930 -v4454 -v4158 v3049 -v2570 -v4507 -v3097 -v2771 -v2668 -v2510 -v1379 -v933 v1383 -v365 -v3 v4510 -v3126 v3051 -v2772 -v2476 -v1022 -v364 -v42 -v4 v4508 -v3125 -v3052 -v44 v5 v2479 v1921 v372 -v181 -v19 -v376 -v40 -v3820 v3015 -v1318 v754 v3824 -v2585 -v2107 v2011 -v1322 -v3021 -v2587 -v2342 v2013 -v761 v748 -v3025 -v2588 v2341 -v2019 -v765 -v3552 -v3029 -v2604 v2015 -v749 -v4422 -v3028 -v2027 -v74 -v4423 -v3982 v3555 -v2882 v2441 -v1197 -v95 -v4424 v4120 -v3986 -v2949 v2443 -v1666 -v1446 -v1198 -v91 -v4440 v4122 -v3937 -v2950 -v2338 -v1687 -v1520 -v1204 v1193 -v441 -v90 -v4128 -v3938 -v2951 -v1683 -v1524 -v1208 v4124 -v3988 -v3933 -v2967 v2437 -v1975 -v1682 -v1191 v1062 -v801 v4136 -v3989 v2631 -v1974 -v1855 v1066 -v803 -v3931 -v3762 v2632 -v2438 -v1857 -v1695 v1526 -v604 -v3764 v2633 v1863 v1699 -v1527 -v3397 v2649 -v2132 v1859 -v1611 -v797 -v610 -v3399 -v2131 -v1871 -v1612 v4249 -v3758 -v2655 -v1971 v1701 -v1607 -v798 v615 v4253 v4145 -v2514 -v1702 -v246 v4147 -v3759 -v3393 -v2661 -v1605 -v1009 v618 -v267 v4153 -v3039 -v2776 -v616 -v263 -v4525 -v4255 v4149 -v3394 -v3238 -v3038 v2666 -v2128 v1015 -v262 -v4495 -v4256 -v4161 -v4531 -v4497 -v4452 -v3241 -v3093 v3046 v2669 -v2565 v1020 -v929 v4503 -v4456 v3050 v2667 -v2569 v4499 -v3096 v3054 -v1481 -v1381 v1023 -v935 v4511 v3053 v1385 -v1021 -v43 -v4534 -v4458 -v2475 -v177 v22 -v4459 -v366 v23 v2481 v1387 -v938 v367 -v180 -v18 v1388 v368 -v38 -v3822 -v1330 v752 v3826 v3014 -v1326 v3016 -v2607 -v1325 -v760 -v3976 v3017 -v2608 v2014 -v764 -v3975 v3828 v3551 -v3033 -v2878 -v2603 v2035 -v1196 -v92 -v3829 -v2442 v2031 v1514 -v1195 -v94 -v4443 -v3983 -v3936 v3557 -v2881 -v2601 v2030 -v1684 v1513 -v437 -v4444 -v3987 -v3935 -v1686 -v4439 -v3991 -v2970 -v1521 -v1206 -v440 -v88 v4123 -v3990 -v2971 -v1689 -v1525 -v1210 -v802 -v4437 -v4144 v3560 -v2966 -v1688 -v1680 v1529 -v1192 v1064 -v89 v4140 -v3763 v1528 v1068 v4139 -v3932 -v2964 -v2652 -v1696 -v1681 -v1610 -v1212 -v4243 -v3398 -v2653 v1858 v1700 -v1609 -v1213 -v603 v4242 v2648 -v1879 v1704 -v1070 -v605 -v1875 v1703 -v1071 -v611 v4250 v2646 -v1874 v607 -v264 v4254 -v2654 v619 -v266 -v4521 v4258 -v4101 -v2656 -v1606 -v4446 v4257 v4148 -v4105 -v2662 v1008 -v4527 v4445 v4169 -v3237 v2658 v1010 -v925 -v260 -v4165 v3040 v2670 -v1375 v1016 -v4532 -v4453 -v4164 -v3407 -v3243 -v3092 v3041 -v2567 -v1477 -v1374 v1012 -v931 -v261 -v4498 -v4457 -v3411 v3042 -v2571 v1024 v4535 v4519 -v4461 -v4310 -v3481 -v3098 -v3058 -v2471 -v1480 -v1382 -v936 -v21 v4533 -v4515 -v4460 -v4314 v1386 v20 -v4514 -v3246 -v2573 -v2477 v1390 -v939 -v176 -v2574 v1389 -v937 -v3101 v2482 v379 -v182 -v16 v380 -v39 -v3823 -v2606 -v1329 v753 v3827 -v2605 v3831 v3547 -v3172 v3036 -v2032 -v1323 -v762 v3830 v3037 v2034 -v766 -v93 -v4442 v3553 -v3032 -v2877 -v1324 -v4441 -v3977 -v1685 -v1200 -v3978 v3558 -v3030 -v2969 -v2883 -v2602 v2028 -v1765 -v1544 -v1199 v768 -v436 -v3979 -v2968 -v1548 v1515 v1058 v769 -v4141 -v3995 v3561 v2029 v1516 -v1207 v1057 -v442 -v4143 v3559 v1517 -v1211 -v4438 -v2886 -v2651 v1533 -v1215 v1065 -v2650 -v1690 -v1214 v1069 v4137 -v2965 -v1876 -v1691 v1073 -v445 -v1878 v1692 v1072 v4138 v1708 v675 v4244 -v679 -v606 -v265 v4245 -v4051 -v2647 -v1872 v627 v4246 -v4055 v623 v4262 v4166 -v4100 -v3233 -v2215 -v1873 v622 -v4520 v4168 -v4104 -v2657 -v2561 -v2219 -v4522 -v3239 -v3088 -v2678 -v2560 -v4528 v4447 -v2674 v1011 -v924 v4524 v4516 v4448 -v4162 -v3477 -v3406 -v3244 -v3094 v3061 -v2673 -v2568 -v1476 v1032 -v926 v4536 v4518 v4449 -v3410 v3062 -v2572 -v1376 v1028 -v932 v4465 -v4309 -v4163 -v3480 -v3247 -v3099 -v3057 -v2576 -v1482 -v1377 v1027 -v928 -v172 -v4313 -v3245 -v2575 v2470 v1378 -v940 -v4512 -v3875 -v3102 -v3055 v2472 v1394 v378 -v178 -v3100 -v2478 v377 -v4513 v3339 -v3003 v2474 -v1485 -v183 -v17 -v3007 v2483 v3819 v3168 -v3035 -v1327 v757 v3818 v3034 -v2033 v3835 -v3171 -v2873 -v763 v3546 -v767 v3548 -v2879 -v1761 v771 -v432 v3554 v770 -v3998 v3550 -v3031 -v2884 -v1764 -v1543 -v438 -v4142 -v3999 v3562 -v1547 -v1201 -v3994 -v2887 v1536 -v1202 -v909 -v443 -v2885 v1537 -v1203 v1059 -v3992 v1532 -v1219 v1060 -v446 -v1877 v1061 -v444 v1711 -v1530 v1077 v1712 v1707 v674 v624 -v678 v626 v4265 -v4050 v1705 v4266 -v4167 v4054 v4261 -v4102 -v2675 -v2214 v620 -v4106 -v3232 -v2677 -v2218 v4259 -v3234 v3060 -v1472 v1029 -v621 -v4523 v4517 -v3240 -v3087 v3059 -v2562 v1031 -v4544 -v4468 -v4201 -v4108 -v3476 -v3408 -v3236 -v3089 -v2671 -v2563 -v1478 -v4540 -v4469 -v4205 -v4109 -v3412 -v3248 -v3095 -v2564 -v927 -v4539 v4464 -v4311 -v3871 -v3482 -v3091 -v2672 -v2580 -v1483 v1397 v1025 -v948 -v4315 -v3103 v1398 -v944 -v171 v4462 -v3874 -v3414 -v3335 -v3056 -v2071 -v1486 v1393 -v1026 -v943 -v173 -v3415 v2473 -v1484 -v179 -v4317 -v3485 v3338 v3002 -v2491 v1391 -v175 -v4318 -v3006 -v2487 -v184 v3838 -v3260 v3167 -v1739 -v1328 v3839 v3264 v756 v3834 -v3173 v758 -v2872 v759 -v3997 v3832 -v2874 -v1760 v775 -v3996 v3549 -v2880 -v431 v3570 -v3176 -v2876 -v1766 -v1545 -v1535 v905 -v433 v3566 -v2888 -v1549 -v1534 -v439 v3565 -v1222 v908 -v435 -v1223 -v447 -v3993 v2351 -v1769 v1710 -v1551 -v1218 -v1080 -v2355 v1709 -v1552 -v1081 -v1531 -v1216 v1076 -v625 v4264 v1074 v676 v4263 -v4096 -v680 -v4095 v4052 -v1706 v4056 -v2676 -v4103 -v2216 v682 -v4107 -v3402 v2220 -v1030 v683 -v4541 -v4467 v4260 -v4111 -v4058 -v3472 v3401 -v4543 -v4466 -v4305 -v4110 -v4059 -v3235 -v1471 -v4304 v4200 -v3478 -v3409 -v3256 -v2583 v2222 -v1473 -v1396 -v945 v4204 -v3413 -v3252 -v3090 -v2584 -v2223 -v1479 -v1395 -v947 -v4537 -v4312 -v3870 -v3483 -v3417 -v3251 -v3111 -v2579 -v2067 -v1475 -v4316 -v3416 -v3107 -v1487 -v4538 -v4463 -v4320 -v3876 -v3486 v3334 -v3106 -v2577 -v2488 -v2070 -v941 -v4319 -v3484 -v2490 -v174 v3340 v3004 v1392 -v942 -v192 -v3008 -v2486 -v188 v3836 -v3259 v3169 -v1738 v3263 -v3174 -v1756 -v778 -v1539 -v779 v3833 v3567 v3177 -v1762 -v1538 -v774 v3569 v3175 -v2875 v2907 -v2896 -v1767 -v1546 -v1221 v904 -v772 -v2892 -v1550 -v1220 -v434 v3563 -v2891 -v1770 -v1554 -v1079 v910 -v455 -v1768 -v1553 -v1078 -v451 -v4384 v3564 v2350 -v450 -v4388 v2354 v670 -v1217 v913 v669 v4046 v4045 v2380 v1075 v677 -v2210 -v681 v4053 -v2545 v2209 v685 -v4097 v4057 v684 -v4098 -v4061 -v2217 v1299 -v4542 -v4099 -v4060 v2221 -v4115 -v3253 -v2582 v2225 -v3471 v3403 -v3255 -v2581 v2224 -v946 v4202 -v3866 -v3473 v3404 -v3108 -v131 -v4306 v4206 -v3479 v3405 -v3110 -v1474 -v4307 v3872 -v3475 -v3421 -v3330 -v3249 -v2066 -v1495 v102 v4308 -v3487 -v2998 -v2489 -v1491 -v106 v4324 v4208 -v3877 v3336 -v3250 -v3104 -v2997 -v2578 -v2072 -v1490 -v189 -v4209 -v191 v3878 v3341 -v3105 v3005 -v1502 v3879 v3009 -v2484 -v1506 -v187 v4404 v3837 -v3261 v3165 -v1740 -v964 -v777 v3265 v3170 -v968 -v776 v3166 v3568 v3178 -v1755 v3502 -v3267 -v2903 -v2893 -v1757 -v1744 -v900 -v884 -v3506 -v3268 -v2895 -v1763 -v1540 v2906 v2739 -v1759 -v1541 v906 -v773 -v452 -v1771 -v1542 -v454 -v2889 -v1558 v911 v4383 -v2890 v2352 v914 -v448 -v4387 v2356 v912 -v2376 -v449 v671 -v2541 v2379 -v2358 v672 v4047 -v2359 v673 v4048 -v2544 -v1295 -v689 v4049 v2211 -v4118 -v4065 v2212 v1298 v4196 -v4119 -v3254 v2213 v4195 -v4114 -v2229 v127 -v3109 v4203 -v4112 v3424 -v2062 -v1492 -v130 v4207 -v3865 -v3474 v3425 -v1494 v4327 v4211 -v3867 -v3495 -v3420 -v2068 v101 v4328 v4210 v3873 -v3491 -v3329 -v190 -v105 v4323 v3869 -v3490 -v3418 -v3331 v3073 -v2073 -v1488 v3880 v3337 -v2999 v4321 v3333 -v3000 -v2074 -v1501 -v1489 v3342 v3001 -v2485 -v2075 -v1505 -v185 v4403 v3262 -v1741 -v963 v3266 v3164 -v967 -v3270 -v3186 -v1745 v880 -v3269 v3182 -v2894 -v1743 v3501 v3181 -v2902 -v2735 v883 v3505 -v1758 -v899 -v453 v2908 v2738 v2401 -v1779 -v1561 -v901 -v2405 -v2346 -v1775 -v1562 v907 -v2345 -v1774 -v1557 v903 -v588 v915 v4385 -v2911 -v2810 v2353 -v1555 -v4389 -v2814 v2357 v2375 -v2361 v1648 -v2360 -v4391 v2540 v2381 -v692 -v4392 -v693 -v4117 v4068 -v2546 -v1294 -v1270 -v688 -v278 -v4116 v4069 -v1274 -v4064 -v2710 -v2384 v2232 v1300 -v686 v2714 v2233 -v4062 -v3423 -v2549 -v2228 -v1155 v126 v4197 v3422 -v1493 -v1159 -v4326 v4198 -v4113 -v4080 -v3492 -v2226 v1303 -v132 -v4325 v4199 -v3494 -v2061 v4215 v3069 -v2063 v103 -v3868 -v2069 -v107 -v3888 -v3488 -v3419 v3072 -v2065 -v135 -v3884 -v3332 -v2076 v4322 -v3883 -v3489 v3350 -v3012 -v1503 v109 -v3346 -v3013 -v1507 -v186 v110 v4405 v3258 -v3183 -v1742 -v965 v3257 -v3185 -v1746 -v969 -v3274 -v2898 -v1038 v879 -v1042 -v4409 v3503 v3179 -v2904 -v2734 -v1776 -v1560 -v971 v885 v3507 -v1778 -v1559 -v972 -v4176 -v3180 v2909 v2740 v2400 -v584 -v4379 v4180 -v2404 -v902 -v4378 v3509 -v2912 -v1772 -v923 v888 -v587 v3510 -v2910 -v2347 -v919 v4386 -v2809 v2743 v2371 -v2348 -v1773 v1644 -v1556 -v918 -v4390 -v2813 v2349 -v4394 -v2536 v2377 -v2365 v1647 -v691 -v4393 -v690 v4067 -v3846 v2542 v2382 -v1290 v274 v4066 -v3850 -v3531 -v2547 v2385 -v2231 v1296 -v1269 -v277 v2383 -v2230 -v1273 -v2709 v2550 v1301 -v687 v122 v2713 -v2548 -v4076 -v4063 v1304 -v1154 v128 -v3493 v1302 -v1158 -v97 -v4218 -v4079 -v2227 -v133 -v96 -v4219 v4214 -v3885 v3068 -v1886 v136 v104 -v3887 -v2064 v1890 -v1497 -v134 -v108 -v4212 v3347 v3074 -v3011 -v2084 -v1496 v112 v3349 -v3010 -v2080 v111 -v3881 -v2079 -v1504 -v3345 v1508 v4406 v3277 -v3184 -v1754 -v966 v950 -v875 -v3497 v3278 -v1750 -v970 -v4410 v3946 -v3496 -v3273 v2730 -v1749 -v1037 -v974 v881 -v4408 -v2897 -v1777 -v1041 -v973 v3504 -v3271 -v2899 -v2736 v886 v3508 -v2905 -v4175 v3512 v2901 v2741 v2402 -v920 v889 -v583 v4179 v3511 -v2913 -v2406 -v922 v887 v2744 -v589 -v4380 v2742 -v4381 -v2811 -v2408 -v2368 v1643 -v916 v4382 -v2815 -v2409 v2370 -v2369 v4398 v2372 -v2364 -v2145 v1649 -v917 v592 -v2535 v2378 -v3845 -v3527 -v2817 -v2537 v2374 -v2362 v273 -v3849 -v2818 v2543 v2386 v1289 -v3530 -v2685 v2539 v1652 v1291 -v1271 -v279 -v2689 v2551 v1297 -v1275 -v4555 -v2711 v1293 v2715 v1305 v121 -v4217 -v4075 v1277 -v1156 v282 v123 -v4216 v1278 -v1160 v129 -v4081 -v3064 v2717 -v1130 v125 -v3886 v2718 -v1134 v137 -v98 v3070 -v2081 -v1885 v1162 -v99 v3348 -v2083 v1889 -v1163 v100 -v4213 -v4084 -v3589 v3075 v116 -v3593 -v1498 -v3882 v3076 -v2077 -v1499 -v3343 v3077 v1500 v4407 v3942 -v3275 -v1753 -v962 v949 -v4411 -v961 -v874 v3945 -v1747 -v1039 -v978 -v876 -v3498 v2729 -v2396 -v1043 v882 -v3499 -v3272 v2731 -v2395 -v1748 v878 -v579 v3500 -v2900 -v2737 -v921 v890 -v4177 -v3516 v2921 v2733 v2403 -v1045 -v585 v4181 -v2917 -v2805 v2745 -v2407 -v1046 -v2916 -v2804 -v2411 -v2367 -v1639 -v590 -v2410 -v2366 -v4401 v4183 -v2812 -v2141 v1645 -v704 v593 -v4402 v4184 -v2816 v591 v4397 -v2820 -v2144 v1650 -v269 -v2819 v2373 v1265 v4395 -v3847 -v3526 -v2394 -v2363 v1653 v1264 v275 -v3851 v2705 -v2538 -v2390 v1651 -v4551 -v3532 v2704 -v2684 -v2559 -v2389 -v1272 -v280 -v2688 v2555 v1292 -v1276 v1150 -v4554 -v4071 -v3853 -v3436 -v2712 v2554 v1313 v1280 v1149 v283 -v3854 v2716 -v1309 v1279 v281 -v4077 -v3535 -v3197 v2720 -v1308 -v1157 v2719 -v1161 v124 -v4082 v1165 -v1129 v145 -v3063 -v2082 v1164 -v1133 v141 -v4085 -v3065 -v1887 v140 v119 -v4083 v3071 v1891 v120 -v3588 v3067 -v2244 v115 -v3592 v3078 -v2078 v1893 v1511 -v113 -v3344 v1894 v1512 v4419 v3941 -v3276 -v1751 -v1034 -v981 v951 v4415 -v982 -v4594 v4414 v3947 -v1040 -v977 -v4598 -v4171 -v1044 -v877 -v4170 v3519 -v2918 -v1048 -v975 -v954 v898 v3520 v2920 v2732 -v2397 -v1047 v894 -v578 -v4178 v3950 -v3515 -v2753 -v2398 v893 -v580 v4182 v2749 v2399 -v586 -v4400 v4186 -v3513 -v2914 v2748 -v2415 -v700 v582 -v4399 v4185 -v2806 -v1638 v594 -v3963 -v2915 -v2807 -v2140 -v1640 -v703 -v3967 -v3841 v2808 v1646 -v3840 v3522 -v2824 -v2391 -v2146 v1642 -v2393 v1654 -v268 v4396 -v3848 -v3528 -v2556 -v357 -v270 -v3852 -v2558 v1266 v276 -v4550 -v3856 -v3533 -v3432 -v2686 -v2387 -v2149 v1310 v1267 v272 -v3855 v2706 -v2690 v1312 v1268 v284 -v4556 -v3536 -v3435 -v3193 v2707 v2552 -v2388 v1284 -v4070 -v3534 v2708 v1151 -v4614 -v4072 -v3196 -v2724 v2692 v2553 -v1306 -v1252 v1152 v142 -v4078 v2693 -v1881 v1256 v1153 v144 v4559 -v4074 -v2523 -v1880 -v1307 v1169 -v1131 v118 -v4086 -v2527 -v1135 v117 -v2860 -v2240 -v1888 v138 -v3066 -v2864 v1892 -v3590 v3086 -v2243 v1896 v1510 -v1137 v139 -v3594 v3082 v1895 v1509 -v1138 -v3775 v3081 -v114 v4418 v3943 -v1752 -v979 v952 -v1033 -v4593 v4412 v3948 -v3518 -v1035 -v955 v895 -v4597 -v3517 -v2919 v1036 -v953 v897 v4413 v3951 -v2750 v1052 -v976 -v4172 v3949 -v2752 -v4173 v2418 v891 v4174 v2419 -v581 -v4190 -v3514 v2746 -v2414 v2136 v892 -v699 -v602 v598 -v3962 v2827 v2747 -v2412 -v2142 -v705 v597 -v3966 v2828 -v2392 -v1641 -v2823 -v2147 -v1662 -v353 -v3842 v3521 -v2680 -v2557 -v1658 v4546 -v3843 v3523 -v2821 -v2679 -v2150 -v1657 -v708 -v356 -v3844 -v3529 -v2148 v1311 -v271 -v4552 -v3860 v3525 -v3431 -v2687 -v1287 v292 -v3537 -v2691 -v1288 -v288 -v4610 -v4557 -v3437 -v3192 -v2727 v2695 v1283 -v287 -v2728 v2694 -v1125 -v143 -v4613 v4560 -v3198 -v2723 v1281 -v1251 -v1172 -v1124 v4558 -v4073 v1255 -v1173 -v4094 -v3440 -v2721 -v2522 v1168 -v1132 -v4090 -v3584 -v2526 -v1882 -v1136 -v4089 -v3583 -v3201 v3083 -v2859 -v2239 -v1883 v1166 -v1140 v3085 -v2863 v1884 -v1139 -v3771 v3591 v2245 -v1900 -v3595 -v3774 -v3596 v3079 -v3597 v4416 v3940 -v980 v3944 -v956 v896 -v4595 -v1055 -v4599 v3952 -v2751 -v1056 v2417 v1051 v2416 v4601 -v4193 v1049 v695 -v599 v4602 -v4194 -v601 -v4189 v2826 -v701 v2825 v2135 -v4187 -v3964 -v2413 v2137 -v1659 -v706 v595 -v3968 -v2143 -v1661 v2139 -v709 v596 -v352 v2151 -v707 v3970 -v3863 -v3427 -v2822 -v1655 -v1286 -v358 v289 v4545 v3971 -v3864 v3524 -v2681 -v1285 v291 v4547 -v3859 -v3545 -v3433 v3188 -v2726 -v2682 -v1656 -v4553 -v3541 -v2725 v2683 -v4609 v4549 -v3857 -v3540 -v3438 -v3194 -v2699 -v1171 -v361 -v285 v4561 -v1170 -v4615 -v4091 -v3441 v3199 v1282 -v1253 -v286 -v4093 -v3439 v1257 -v1126 -v3202 -v2722 -v2524 -v2235 -v1127 -v3200 v3084 -v2528 v1128 -v4618 -v4087 -v2861 -v2241 -v1903 -v1259 v1167 v1144 -v3585 -v2865 -v1904 -v1260 -v4088 -v3770 v3586 -v2530 v2246 -v1899 v3587 -v2531 v3776 v3600 v3080 v2867 -v2247 -v1897 v2868 -v2248 -v4417 -v1054 v3939 -v1053 v960 v4596 v#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.91 2/54 2702
Raw data (stat): 2702 (runsolver) R 2701 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423068163 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 38063 0 0 0 910 88 0 0 25 0 1 0 423068163 195194880 36682 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47655 36682 603 41 0 47614 0
vsize: 190620
[startup+20.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 38579 0 0 0 1908 89 0 0 25 0 1 0 423068163 197083136 37198 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48116 37198 603 41 0 48075 0
vsize: 192464
[startup+30.0032 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 38781 0 0 0 2907 90 0 0 25 0 1 0 423068163 197890048 37400 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48313 37400 603 41 0 48272 0
vsize: 193252
[startup+40.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 39098 0 0 0 3906 91 0 0 25 0 1 0 423068163 199102464 37717 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48609 37717 603 41 0 48568 0
vsize: 194436
[startup+50.0051 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 39379 0 0 0 4905 92 0 0 25 0 1 0 423068163 200200192 37998 4294967295 134512640 134672761 3221224544 3221223696 1074743860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48877 37998 603 41 0 48836 0
vsize: 195508
[startup+60.0053 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 39901 0 0 0 5904 94 0 0 25 0 1 0 423068163 201687040 38520 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49240 38520 603 41 0 49199 0
vsize: 196960
[startup+70.0065 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 40035 0 0 0 6903 95 0 0 25 0 1 0 423068163 202215424 38654 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49369 38654 603 41 0 49328 0
vsize: 197476
[startup+80.0076 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 40173 0 0 0 7903 96 0 0 25 0 1 0 423068163 202887168 38792 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49533 38792 603 41 0 49492 0
vsize: 198132
[startup+90.0078 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 40288 0 0 0 8903 96 0 0 25 0 1 0 423068163 203386880 38907 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49655 38907 603 41 0 49614 0
vsize: 198620
[startup+100.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 40352 0 0 0 9903 96 0 0 25 0 1 0 423068163 203653120 38971 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49720 38971 603 41 0 49679 0
vsize: 198880
[startup+110.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 40502 0 0 0 10903 97 0 0 25 0 1 0 423068163 204185600 39121 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49850 39121 603 41 0 49809 0
vsize: 199400
[startup+120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 40632 0 0 0 11903 97 0 0 25 0 1 0 423068163 204722176 39251 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49981 39251 603 41 0 49940 0
vsize: 199924
[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 40849 0 0 0 12903 98 0 0 25 0 1 0 423068163 205664256 39468 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50211 39468 603 41 0 50170 0
vsize: 200844
[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 41056 0 0 0 13902 99 0 0 25 0 1 0 423068163 206602240 39675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50440 39675 603 41 0 50399 0
vsize: 201760
[startup+150.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 43357 0 0 0 14898 104 0 0 25 0 1 0 423068163 215478272 41957 4294967295 134512640 134672761 3221224544 3221206248 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52607 41957 603 41 0 52566 0
vsize: 210428
[startup+160.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 44794 0 0 0 15895 107 0 0 25 0 1 0 423068163 224698368 43394 4294967295 134512640 134672761 3221224544 3221223680 134560652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54858 43394 603 41 0 54817 0
vsize: 219432
[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 44841 0 0 0 16895 108 0 0 25 0 1 0 423068163 224968704 43441 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54924 43441 603 41 0 54883 0
vsize: 219696
[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 44947 0 0 0 17894 108 0 0 25 0 1 0 423068163 225374208 43547 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55023 43547 603 41 0 54982 0
vsize: 220092
[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45021 0 0 0 18895 109 0 0 25 0 1 0 423068163 225644544 43621 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55089 43621 603 41 0 55048 0
vsize: 220356
[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45079 0 0 0 19895 109 0 0 25 0 1 0 423068163 225914880 43679 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55155 43679 603 41 0 55114 0
vsize: 220620
[startup+210.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45178 0 0 0 20895 109 0 0 25 0 1 0 423068163 226316288 43778 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55253 43778 603 41 0 55212 0
vsize: 221012
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45225 0 0 0 21895 109 0 0 25 0 1 0 423068163 226451456 43825 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55286 43825 603 41 0 55245 0
vsize: 221144
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45251 0 0 0 22895 110 0 0 25 0 1 0 423068163 226582528 43851 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55318 43851 603 41 0 55277 0
vsize: 221272
[startup+240.015 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45310 0 0 0 23895 110 0 0 25 0 1 0 423068163 226717696 43910 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55351 43910 603 41 0 55310 0
vsize: 221404
[startup+250.016 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45351 0 0 0 24895 110 0 0 25 0 1 0 423068163 226988032 43951 4294967295 134512640 134672761 3221224544 3221223752 1075346913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55417 43951 603 41 0 55376 0
vsize: 221668
[startup+260.017 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45421 0 0 0 25895 110 0 0 25 0 1 0 423068163 227258368 44021 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55483 44021 603 41 0 55442 0
vsize: 221932
[startup+270.017 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45486 0 0 0 26895 111 0 0 25 0 1 0 423068163 227782656 44086 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55611 44086 603 41 0 55570 0
vsize: 222444
[startup+280.018 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45539 0 0 0 27895 111 0 0 25 0 1 0 423068163 227917824 44139 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55644 44139 603 41 0 55603 0
vsize: 222576
[startup+290.019 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45662 0 0 0 28895 112 0 0 25 0 1 0 423068163 228446208 44262 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55773 44262 603 41 0 55732 0
vsize: 223092
[startup+300.019 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45759 0 0 0 29895 112 0 0 25 0 1 0 423068163 228851712 44359 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55872 44359 603 41 0 55831 0
vsize: 223488
[startup+310.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45874 0 0 0 30895 113 0 0 25 0 1 0 423068163 229253120 44474 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55970 44474 603 41 0 55929 0
vsize: 223880
[startup+320.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 45986 0 0 0 31895 113 0 0 25 0 1 0 423068163 229658624 44586 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56069 44586 603 41 0 56028 0
vsize: 224276
[startup+330.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46076 0 0 0 32895 114 0 0 25 0 1 0 423068163 230064128 44676 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56168 44676 603 41 0 56127 0
vsize: 224672
[startup+340.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46194 0 0 0 33894 114 0 0 25 0 1 0 423068163 230600704 44794 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56299 44794 603 41 0 56258 0
vsize: 225196
[startup+350.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46307 0 0 0 34894 115 0 0 25 0 1 0 423068163 231006208 44907 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56398 44907 603 41 0 56357 0
vsize: 225592
[startup+360.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46394 0 0 0 35895 115 0 0 25 0 1 0 423068163 231276544 44994 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56464 44994 603 41 0 56423 0
vsize: 225856
[startup+370.024 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46481 0 0 0 36895 115 0 0 25 0 1 0 423068163 231682048 45081 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56563 45081 603 41 0 56522 0
vsize: 226252
[startup+380.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46564 0 0 0 37896 115 0 0 25 0 1 0 423068163 232083456 45164 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56661 45164 603 41 0 56620 0
vsize: 226644
[startup+390.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46650 0 0 0 38895 115 0 0 25 0 1 0 423068163 232353792 45250 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56727 45250 603 41 0 56686 0
vsize: 226908
[startup+400.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46700 0 0 0 39896 115 0 0 25 0 1 0 423068163 232488960 45300 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56760 45300 603 41 0 56719 0
vsize: 227040
[startup+410.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46774 0 0 0 40896 116 0 0 25 0 1 0 423068163 232890368 45374 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56858 45374 603 41 0 56817 0
vsize: 227432
[startup+420.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46841 0 0 0 41896 116 0 0 25 0 1 0 423068163 233156608 45441 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56923 45441 603 41 0 56882 0
vsize: 227692
[startup+430.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 46913 0 0 0 42896 116 0 0 25 0 1 0 423068163 233422848 45513 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56988 45513 603 41 0 56947 0
vsize: 227952
[startup+440.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 47004 0 0 0 43896 116 0 0 25 0 1 0 423068163 233697280 45604 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57055 45604 603 41 0 57014 0
vsize: 228220
[startup+450.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 47060 0 0 0 44896 117 0 0 25 0 1 0 423068163 233967616 45660 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57121 45660 603 41 0 57080 0
vsize: 228484
[startup+460.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 47173 0 0 0 45896 117 0 0 25 0 1 0 423068163 234369024 45773 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57219 45773 603 41 0 57178 0
vsize: 228876
[startup+470.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 47280 0 0 0 46896 117 0 0 25 0 1 0 423068163 234901504 45880 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57349 45880 603 41 0 57308 0
vsize: 229396
[startup+480.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 47408 0 0 0 47896 118 0 0 25 0 1 0 423068163 235827200 46009 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57575 46009 603 41 0 57534 0
vsize: 230300
[startup+490.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 47638 0 0 0 48896 118 0 0 25 0 1 0 423068163 236765184 46238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57804 46238 603 41 0 57763 0
vsize: 231216
[startup+500.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 47750 0 0 0 49896 119 0 0 25 0 1 0 423068163 237305856 46350 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57936 46350 603 41 0 57895 0
vsize: 231744
[startup+510.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 47868 0 0 0 50896 119 0 0 25 0 1 0 423068163 237707264 46468 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58034 46468 603 41 0 57993 0
vsize: 232136
[startup+520.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 47944 0 0 0 51896 120 0 0 25 0 1 0 423068163 237981696 46544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58101 46544 603 41 0 58060 0
vsize: 232404
[startup+530.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48025 0 0 0 52896 120 0 0 25 0 1 0 423068163 238383104 46625 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58199 46625 603 41 0 58158 0
vsize: 232796
[startup+540.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48104 0 0 0 53897 120 0 0 25 0 1 0 423068163 238645248 46704 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58263 46704 603 41 0 58222 0
vsize: 233052
[startup+550.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48180 0 0 0 54897 120 0 0 25 0 1 0 423068163 238911488 46780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58328 46780 603 41 0 58287 0
vsize: 233312
[startup+560.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48249 0 0 0 55897 120 0 0 25 0 1 0 423068163 239316992 46849 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58427 46849 603 41 0 58386 0
vsize: 233708
[startup+570.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48318 0 0 0 56897 121 0 0 25 0 1 0 423068163 239587328 46918 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58493 46918 603 41 0 58452 0
vsize: 233972
[startup+580.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48405 0 0 0 57897 121 0 0 25 0 1 0 423068163 239857664 47005 4294967295 134512640 134672761 3221224544 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58559 47005 603 41 0 58518 0
vsize: 234236
[startup+590.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48479 0 0 0 58897 121 0 0 25 0 1 0 423068163 240136192 47079 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58627 47079 603 41 0 58586 0
vsize: 234508
[startup+600.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48525 0 0 0 59897 122 0 0 25 0 1 0 423068163 240402432 47125 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58692 47125 603 41 0 58651 0
vsize: 234768
[startup+610.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48578 0 0 0 60897 122 0 0 25 0 1 0 423068163 240537600 47178 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58725 47178 603 41 0 58684 0
vsize: 234900
[startup+620.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48637 0 0 0 61897 122 0 0 25 0 1 0 423068163 240803840 47237 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58790 47237 603 41 0 58749 0
vsize: 235160
[startup+630.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48696 0 0 0 62897 122 0 0 25 0 1 0 423068163 241065984 47296 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58854 47296 603 41 0 58813 0
vsize: 235416
[startup+640.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48759 0 0 0 63898 123 0 0 25 0 1 0 423068163 241332224 47359 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58919 47359 603 41 0 58878 0
vsize: 235676
[startup+650.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48829 0 0 0 64897 123 0 0 25 0 1 0 423068163 241602560 47429 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58985 47429 603 41 0 58944 0
vsize: 235940
[startup+660.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 48916 0 0 0 65897 123 0 0 25 0 1 0 423068163 241868800 47516 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59050 47516 603 41 0 59009 0
vsize: 236200
[startup+670.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 49018 0 0 0 66897 124 0 0 25 0 1 0 423068163 242405376 47618 4294967295 134512640 134672761 3221224544 3221223744 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59181 47618 603 41 0 59140 0
vsize: 236724
[startup+680.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 49160 0 0 0 67897 125 0 0 25 0 1 0 423068163 242937856 47760 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59311 47760 603 41 0 59270 0
vsize: 237244
[startup+690.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 49287 0 0 0 68897 125 0 0 25 0 1 0 423068163 243466240 47887 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59440 47887 603 41 0 59399 0
vsize: 237760
[startup+700.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 49412 0 0 0 69897 125 0 0 25 0 1 0 423068163 243867648 48012 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59538 48012 603 41 0 59497 0
vsize: 238152
[startup+710.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 49530 0 0 0 70897 126 0 0 25 0 1 0 423068163 244400128 48130 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59668 48130 603 41 0 59627 0
vsize: 238672
[startup+720.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 49616 0 0 0 71896 126 0 0 25 0 1 0 423068163 244801536 48216 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59766 48216 603 41 0 59725 0
vsize: 239064
[startup+730.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 49796 0 0 0 72896 127 0 0 25 0 1 0 423068163 245473280 48396 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59930 48396 603 41 0 59889 0
vsize: 239720
[startup+740.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 49859 0 0 0 73896 127 0 0 25 0 1 0 423068163 245743616 48459 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59996 48459 603 41 0 59955 0
vsize: 239984
[startup+750.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 49931 0 0 0 74897 128 0 0 25 0 1 0 423068163 246013952 48531 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60062 48531 603 41 0 60021 0
vsize: 240248
[startup+760.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 49989 0 0 0 75897 128 0 0 25 0 1 0 423068163 246284288 48589 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60128 48589 603 41 0 60087 0
vsize: 240512
[startup+770.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50047 0 0 0 76897 128 0 0 25 0 1 0 423068163 246419456 48647 4294967295 134512640 134672761 3221224544 3221223712 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60161 48647 603 41 0 60120 0
vsize: 240644
[startup+780.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50172 0 0 0 77896 129 0 0 25 0 1 0 423068163 246947840 48772 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60290 48772 603 41 0 60249 0
vsize: 241160
[startup+790.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50273 0 0 0 78896 129 0 0 25 0 1 0 423068163 247353344 48873 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60389 48873 603 41 0 60348 0
vsize: 241556
[startup+800.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50438 0 0 0 79896 130 0 0 25 0 1 0 423068163 248020992 49038 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60552 49038 603 41 0 60511 0
vsize: 242208
[startup+810.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50482 0 0 0 80896 130 0 0 25 0 1 0 423068163 248287232 49082 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60617 49082 603 41 0 60576 0
vsize: 242468
[startup+820.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50573 0 0 0 81896 130 0 0 25 0 1 0 423068163 248557568 49173 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60683 49173 603 41 0 60642 0
vsize: 242732
[startup+830.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50620 0 0 0 82897 130 0 0 25 0 1 0 423068163 248819712 49220 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60747 49220 603 41 0 60706 0
vsize: 242988
[startup+840.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50661 0 0 0 83897 131 0 0 25 0 1 0 423068163 248954880 49261 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60780 49261 603 41 0 60739 0
vsize: 243120
[startup+850.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50708 0 0 0 84897 131 0 0 25 0 1 0 423068163 249090048 49308 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60813 49308 603 41 0 60772 0
vsize: 243252
[startup+860.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50767 0 0 0 85897 131 0 0 25 0 1 0 423068163 249352192 49367 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60877 49367 603 41 0 60836 0
vsize: 243508
[startup+870.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50826 0 0 0 86897 131 0 0 25 0 1 0 423068163 249618432 49426 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60942 49426 603 41 0 60901 0
vsize: 243768
[startup+880.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50890 0 0 0 87897 132 0 0 25 0 1 0 423068163 249888768 49490 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61008 49490 603 41 0 60967 0
vsize: 244032
[startup+890.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 50946 0 0 0 88897 132 0 0 25 0 1 0 423068163 250023936 49546 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61041 49546 603 41 0 61000 0
vsize: 244164
[startup+900.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51022 0 0 0 89898 132 0 0 25 0 1 0 423068163 250421248 49622 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61138 49622 603 41 0 61097 0
vsize: 244552
[startup+910.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51082 0 0 0 90898 132 0 0 25 0 1 0 423068163 250687488 49682 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61203 49682 603 41 0 61162 0
vsize: 244812
[startup+920.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51140 0 0 0 91898 133 0 0 25 0 1 0 423068163 250818560 49740 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61235 49740 603 41 0 61194 0
vsize: 244940
[startup+930.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51212 0 0 0 92898 133 0 0 25 0 1 0 423068163 251244544 49812 4294967295 134512640 134672761 3221224544 3221223712 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61339 49812 603 41 0 61298 0
vsize: 245356
[startup+940.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51270 0 0 0 93898 133 0 0 25 0 1 0 423068163 251375616 49870 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61371 49870 603 41 0 61330 0
vsize: 245484
[startup+950.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51318 0 0 0 94898 134 0 0 25 0 1 0 423068163 251641856 49918 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61436 49918 603 41 0 61395 0
vsize: 245744
[startup+960.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51367 0 0 0 95899 134 0 0 25 0 1 0 423068163 251777024 49967 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61469 49967 603 41 0 61428 0
vsize: 245876
[startup+970.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51434 0 0 0 96899 134 0 0 25 0 1 0 423068163 252039168 50034 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61533 50034 603 41 0 61492 0
vsize: 246132
[startup+980.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51507 0 0 0 97898 134 0 0 25 0 1 0 423068163 252440576 50107 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61631 50107 603 41 0 61590 0
vsize: 246524
[startup+990.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51575 0 0 0 98898 135 0 0 25 0 1 0 423068163 252710912 50175 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61697 50175 603 41 0 61656 0
vsize: 246788
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51641 0 0 0 99899 135 0 0 25 0 1 0 423068163 252846080 50241 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61730 50241 603 41 0 61689 0
vsize: 246920
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51746 0 0 0 100899 135 0 0 25 0 1 0 423068163 253382656 50346 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61861 50346 603 41 0 61820 0
vsize: 247444
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 51890 0 0 0 101899 135 0 0 25 0 1 0 423068163 253915136 50490 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61991 50490 603 41 0 61950 0
vsize: 247964
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52065 0 0 0 102899 136 0 0 25 0 1 0 423068163 254578688 50665 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62153 50665 603 41 0 62112 0
vsize: 248612
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52144 0 0 0 103899 137 0 0 25 0 1 0 423068163 254984192 50744 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62252 50744 603 41 0 62211 0
vsize: 249008
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52194 0 0 0 104899 137 0 0 25 0 1 0 423068163 255115264 50794 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62284 50794 603 41 0 62243 0
vsize: 249136
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52282 0 0 0 105899 137 0 0 25 0 1 0 423068163 255516672 50882 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62382 50882 603 41 0 62341 0
vsize: 249528
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52480 0 0 0 106899 138 0 0 25 0 1 0 423068163 256319488 51080 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62578 51080 603 41 0 62537 0
vsize: 250312
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52607 0 0 0 107899 138 0 0 25 0 1 0 423068163 256720896 51207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62676 51207 603 41 0 62635 0
vsize: 250704
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52674 0 0 0 108899 138 0 0 25 0 1 0 423068163 258035712 51274 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62997 51274 603 41 0 62956 0
vsize: 251988
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52753 0 0 0 109899 139 0 0 25 0 1 0 423068163 258441216 51353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63096 51353 603 41 0 63055 0
vsize: 252384
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52843 0 0 0 110899 139 0 0 25 0 1 0 423068163 258711552 51443 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63162 51443 603 41 0 63121 0
vsize: 252648
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52922 0 0 0 111899 139 0 0 25 0 1 0 423068163 259112960 51522 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63260 51522 603 41 0 63219 0
vsize: 253040
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 52997 0 0 0 112899 140 0 0 25 0 1 0 423068163 259383296 51597 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63326 51597 603 41 0 63285 0
vsize: 253304
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 53080 0 0 0 113899 140 0 0 25 0 1 0 423068163 259780608 51680 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63423 51680 603 41 0 63382 0
vsize: 253692
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 53161 0 0 0 114900 140 0 0 25 0 1 0 423068163 260046848 51761 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63488 51761 603 41 0 63447 0
vsize: 253952
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 53235 0 0 0 115900 141 0 0 25 0 1 0 423068163 260317184 51835 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63554 51835 603 41 0 63513 0
vsize: 254216
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 53316 0 0 0 116900 141 0 0 25 0 1 0 423068163 260714496 51916 4294967295 134512640 134672761 3221224544 3221223680 134560637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63651 51916 603 41 0 63610 0
vsize: 254604
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 53396 0 0 0 117900 141 0 0 25 0 1 0 423068163 260984832 51996 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63717 51996 603 41 0 63676 0
vsize: 254868
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 53464 0 0 0 118900 142 0 0 25 0 1 0 423068163 261255168 52064 4294967295 134512640 134672761 3221224544 3221223680 134560579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63783 52064 603 41 0 63742 0
vsize: 255132
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2702
Raw data (stat): 2702 (minisat+) R 2701 29653 29652 0 -1 0 53534 0 0 0 119900 142 0 0 25 0 1 0 423068163 261525504 52134 4294967295 134512640 134672761 3221224544 3221223744 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63849 52134 603 41 0 63808 0
vsize: 255396
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 2702
Raw data (stat): 2702 (minisat+) Z 2701 29653 29652 0 -1 12 53537 0 0 0 119900 152 0 0 25 0 1 0 423068163 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.19
CPU time (s): 1200.54
CPU user time (s): 1199.01
CPU system time (s): 1.52977
CPU usage (%): 100.029
Max. virtual memory (Kb): 255396
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####