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 5697

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        834776 kB
Buffers:         35148 kB
Cached:         124352 kB
SwapCached:       2476 kB
Active:          55584 kB
Inactive:       109264 kB
HighTotal:      131008 kB
HighFree:         3528 kB
LowTotal:       903652 kB
LowFree:        831248 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29344 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:47:43 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 4134 7 1200.25 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   62745   180525 |   18823       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/28987          
c   -- var.elim.:  2000/28987          
c   -- var.elim.:  3000/28987          
c   -- var.elim.:  4000/28987          
c   -- var.elim.:  5000/28987          
c   -- var.elim.:  6000/28987          
c   -- var.elim.:  7000/28987          
c   -- var.elim.:  8000/28987          
c   -- var.elim.:  9000/28987          
c   -- var.elim.:  10000/28987          
c   -- var.elim.:  11000/28987          
c   -- var.elim.:  12000/28987          
c   -- var.elim.:  13000/28987          
c   -- var.elim.:  14000/28987          
c   -- var.elim.:  15000/28987          
c   -- var.elim.:  16000/28987          
c   -- var.elim.:  17000/28987          
c   -- var.elim.:  18000/28987          
c   -- var.elim.:  19000/28987          
c   -- var.elim.:  20000/28987          
c   -- var.elim.:  21000/28987          
c   -- var.elim.:  22000/28987          
c   -- var.elim.:  23000/28987          
c   -- var.elim.:  24000/28987          
c   -- var.elim.:  25000/28987          
c   -- var.elim.:  26000/28987          
c   -- var.elim.:  27000/28987          
c   -- var.elim.:  28000/28987          
c   -- var.elim.:  28987/28987          
c   -- var.elim.:  1000/13778          
c   -- var.elim.:  2000/13778          
c   -- var.elim.:  3000/13778          
c   -- var.elim.:  4000/13778          
c   -- var.elim.:  5000/13778          
c   -- var.elim.:  6000/13778          
c   -- var.elim.:  7000/13778          
c   -- var.elim.:  8000/13778          
c   -- var.elim.:  9000/13778          
c   -- var.elim.:  10000/13778          
c   -- var.elim.:  11000/13778          
c   -- var.elim.:  12000/13778          
c   -- var.elim.:  13000/13778          
c   -- var.elim.:  13778/13778          
c   -- subsuming                       
c   -- var.elim.:  1000/12920          
c   -- var.elim.:  2000/12920          
c   -- var.elim.:  3000/12920          
c   -- var.elim.:  4000/12920          
c   -- var.elim.:  5000/12920          
c   -- var.elim.:  6000/12920          
c   -- var.elim.:  7000/12920          
c   -- var.elim.:  8000/12920          
c   -- var.elim.:  9000/12920          
c   -- var.elim.:  10000/12920          
c   -- var.elim.:  11000/12920          
c   -- var.elim.:  12000/12920          
c   -- var.elim.:  12920/12920          
c   -- var.elim.:  1000/6261          
c   -- var.elim.:  2000/6261          
c   -- var.elim.:  3000/6261          
c   -- var.elim.:  4000/6261          
c   -- var.elim.:  5000/6261          
c   -- var.elim.:  6000/6261          
c   -- var.elim.:  6261/6261          
c   -- subsuming                       
c   -- var.elim.:  36/36          
c   -- var.elim.:  32/32          
c |         0 |   46934   180181 |      --       0       --      -- |     --   | -15811/2230
c |         0 |   46934   180181 |   18773       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 3.60145 s)
c ==============================================================================
c [1mFound solution: 5409[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11365   maxlim: 2772   bits: 13/12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  126414   464031 |   37924       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15991          
c   -- var.elim.:  2000/15991          
c   -- var.elim.:  3000/15991          
c   -- var.elim.:  4000/15991          
c   -- var.elim.:  5000/15991          
c   -- var.elim.:  6000/15991          
c   -- var.elim.:  7000/15991          
c   -- var.elim.:  8000/15991          
c   -- var.elim.:  9000/15991          
c   -- var.elim.:  10000/15991          
c   -- var.elim.:  11000/15991          
c   -- var.elim.:  12000/15991          
c   -- var.elim.:  13000/15991          
c   -- var.elim.:  14000/15991          
c   -- var.elim.:  15000/15991          
c   -- var.elim.:  15991/15991          
c   -- var.elim.:  37/37          
c |         0 |  125872   461383 |      --       0       --      -- |     --   | -542/-2641
c |         0 |  125872   461383 |   50348       0        0     nan |  0.000 % |
c |       100 |  125872   461383 |   55383     100      309     3.1 |  2.739 % |
c |       250 |  125872   461383 |   60922     250      785     3.1 |  2.739 % |
c |       475 |  125872   461383 |   67014     475     1497     3.2 |  2.739 % |
c |       812 |  125872   461383 |   73715     812     2563     3.2 |  2.739 % |
c |      1318 |  125872   461383 |   81087    1318     4595     3.5 |  2.739 % |
c |      2078 |  125872   461383 |   89195    2078     7665     3.7 |  2.739 % |
c |      3217 |  125872   461383 |   98115    3217    12915     4.0 |  2.739 % |
c |      4925 |  125872   461383 |  107927    4925    23573     4.8 |  2.739 % |
c |      7487 |  125862   461343 |  118710    7485    40715     5.4 |  2.742 % |
c |     11332 |  125862   461343 |  130581   11330    68990     6.1 |  2.742 % |
c |     17098 |  125862   461343 |  143639   17096   114602     6.7 |  2.742 % |
c ==============================================================================
c (current CPU-time: 66.2539 s)
c ==============================================================================
c [1mFound solution: 926[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 7255   bits: 14/13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24442 |  125908   461516 |   37772   24440   175986     7.2 |  2.742 % |
c   -- subsuming                       
c   -- var.elim.:  46/46          
c   -- var.elim.:  22/22          
c |     24442 |  125885   461436 |      --   24440       --      -- |     --   | -23/-74
c |     24442 |  125885   461436 |   50354   24438   175973     7.2 |  2.742 % |
c |     24542 |  125885   461436 |   55389   24538   176665     7.2 |  2.760 % |
c |     24692 |  125885   461436 |   60928   24688   177722     7.2 |  2.760 % |
c |     24917 |  125885   461436 |   67021   24913   179490     7.2 |  2.760 % |
c |     25254 |  125885   461436 |   73723   25250   184280     7.3 |  2.760 % |
c |     25760 |  125885   461436 |   81095   25756   191409     7.4 |  2.760 % |
c |     26519 |  125885   461436 |   89205   26515   195807     7.4 |  2.760 % |
c |     27658 |  125885   461436 |   98125   27654   203357     7.4 |  2.760 % |
c |     29366 |  125885   461436 |  107938   29362   216482     7.4 |  2.760 % |
c |     31929 |  125885   461436 |  118732   31925   238982     7.5 |  2.760 % |
c ==============================================================================
c (current CPU-time: 98.0841 s)
c ==============================================================================
c [1mFound solution: 866[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7315   bits: 14/13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     35481 |  125913   461550 |   37773   35477   272212     7.7 |  2.760 % |
c   -- subsuming                       
c   -- var.elim.:  30/30          
c   -- var.elim.:  17/17          
c |     35481 |  125906   461553 |      --   35477       --      -- |     --   | -7/6
c |     35481 |  125906   461553 |   50362   35477   272212     7.7 |  2.760 % |
c |     35581 |  125906   461553 |   55398   35577   273157     7.7 |  2.769 % |
c |     35731 |  125906   461553 |   60938   35727   274357     7.7 |  2.769 % |
c |     35956 |  125906   461553 |   67032   35952   276214     7.7 |  2.769 % |
c |     36293 |  125906   461553 |   73735   36289   280096     7.7 |  2.769 % |
c |     36800 |  125906   461553 |   81109   36796   284389     7.7 |  2.769 % |
c ==============================================================================
c (current CPU-time: 104.916 s)
c ==============================================================================
c [1mFound solution: 808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7373   bits: 14/13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     37412 |  125923   461647 |   37776   37408   290109     7.8 |  2.769 % |
c   -- subsuming                       
c   -- var.elim.:  24/24          
c   -- var.elim.:  15/15          
c |     37412 |  125920   461683 |      --   37408       --      -- |     --   | -3/40
c |     37412 |  125920   461683 |   50368   37408   290109     7.8 |  2.769 % |
c |     37512 |  125920   461683 |   55404   37508   290927     7.8 |  2.781 % |
c |     37663 |  125920   461683 |   60945   37659   295194     7.8 |  2.781 % |
c |     37888 |  125920   461683 |   67039   37884   296696     7.8 |  2.781 % |
c |     38225 |  125920   461683 |   73743   38221   299019     7.8 |  2.781 % |
c |     38731 |  125920   461683 |   81118   38727   302921     7.8 |  2.781 % |
c |     39491 |  125920   461683 |   89229   39487   310289     7.9 |  2.781 % |
c |     40630 |  125920   461683 |   98152   40626   321047     7.9 |  2.781 % |
c |     42339 |  125920   461683 |  107968   42335   338207     8.0 |  2.781 % |
c |     44902 |  125920   461683 |  118765   44898   639858    14.3 |  2.781 % |
c |     48746 |  125920   461683 |  130641   48742   716974    14.7 |  2.781 % |
c |     54512 |  125920   461683 |  143705   54508   815949    15.0 |  2.781 % |
c |     63161 |  125920   461683 |  158076   63157  1395363    22.1 |  2.781 % |
c |     76136 |  125920   461683 |  173883   76132  1740547    22.9 |  2.781 % |
c |     95598 |  125920   461683 |  191272   95594  3564329    37.3 |  2.781 % |
c |    124790 |  125920   461683 |  210399  124786  9508391    76.2 |  2.781 % |
c |    168579 |  125920   461683 |  231439  168575 16166770    95.9 |  2.781 % |
c ==============================================================================
c (current CPU-time: 386.123 s)
c ==============================================================================
c [1mFound solution: 734[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7447   bits: 14/13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    170943 |  125931   461735 |   37779  170939 16221504    94.9 |  2.781 % |
c   -- subsuming                       
c   -- var.elim.:  20/20          
c   -- var.elim.:  13/13          
c |    170943 |  125920   461692 |      --  170939       --      -- |     --   | -11/-40
c |    170943 |  125920   461692 |   50368  170834 16215576    94.9 |  2.781 % |
c |    171044 |  125920   461692 |   55404   18181  2008424   110.5 |  2.791 % |
c |    171194 |  125920   461692 |   60945   18331  2009305   109.6 |  2.791 % |
c |    171419 |  125920   461692 |   67039   18556  2010527   108.3 |  2.791 % |
c |    171756 |  125920   461692 |   73743   18893  2012759   106.5 |  2.791 % |
c |    172262 |  125920   461692 |   81118   19399  2016440   103.9 |  2.791 % |
c |    173021 |  125920   461692 |   89229   20158  2021467   100.3 |  2.791 % |
c |    174160 |  125920   461692 |   98152   21297  2030383    95.3 |  2.791 % |
c |    175869 |  125920   461692 |  107968   23006  2043264    88.8 |  2.791 % |
c |    178431 |  125920   461692 |  118765   25568  2328117    91.1 |  2.791 % |
c |    182275 |  125920   461692 |  130641   29412  2353801    80.0 |  2.791 % |
c |    188041 |  125920   461692 |  143705   35178  2403393    68.3 |  2.791 % |
c |    196690 |  125920   461692 |  158076   43827  2495795    56.9 |  2.791 % |
c |    209664 |  125920   461692 |  173883   56801  2653552    46.7 |  2.791 % |
c |    229125 |  125920   461692 |  191272   76262  3162737    41.5 |  2.791 % |
c |    258317 |  125920   461692 |  210399  105454  4230730    40.1 |  2.791 % |
c |    302107 |  125920   461692 |  231439  149244 10785764    72.3 |  2.791 % |
c |    367792 |  125920   461692 |  254583  214929 18983589    88.3 |  2.791 % |
c |    466320 |  125920   461692 |  280041   67088 10023578   149.4 |  2.791 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v4221 -v3659 v4226 -v3780 -v3680 -v3132 -v2610 v4225 v3895 -v3779 -v3679 -v2609 v334 -v4026 v3781 -v3133 -v2615 -v1996 -v335 v4228 -v4025 v3894 v3782 -v3681 -v3135 -v2614 -v1405 -v1103 v559 -v338 -v4229 v4031 v3898 v3783 -v3683 -v3136 -v2616 -v1997 -v1108 -v336 v4232 v4030 -v3790 -v2620 -v1999 -v1408 v1107 v558 -v416 -v337 v4230 v4032 v3899 v3784 -v3684 -v2619 -v2000 -v1409 -v1083 -v562 -v4476 v4285 -v4231 v4036 v3785 -v3724 -v3686 -v2617 -v1359 -v1225 -v1110 -v1082 v4035 v3786 -v3723 -v3687 -v2618 -v1230 -v1111 -v1088 -v563 -v4479 v4284 v4033 -v3725 -v3310 -v1229 v1114 -v1087 -v4480 -v4034 v3728 -v1112 v1089 -v654 v4290 v3727 -v3309 -v2165 v1232 -v1113 -v1093 -v989 -v653 v4335 -v4288 v3732 -v1233 -v1092 v655 v4334 v3731 v3315 -v2164 v1236 -v1090 -v992 v656 -v387 -v4289 v3729 v3313 -v1234 -v1091 -v993 v657 -v391 -v4359 v4336 -v4293 -v3730 v2170 -v1235 -v853 v664 -v4338 v3314 v2168 -v858 v658 -v4362 v3318 v857 v659 -v4363 -v4339 v2169 v660 v4341 -v3572 v2173 v860 v52 v4342 -v3571 v1979 v861 -v56 -v3708 v3573 v1978 -v1336 v864 -v316 v4621 v1983 v862 -v3634 v1982 -v1335 -v863 v319 -v3638 v4622 -v320 v3655 -v3148 -v3130 -v1993 -v3658 -v1992 -v4220 -v3675 -v3134 -v4222 -v3674 v3138 -v1938 v4227 v3137 -v2611 -v1998 -v339 v4224 v3896 v3793 -v3682 -v2612 -v2002 -v1404 -v638 -v412 v4233 -v4027 v3900 v3794 -v3685 v2613 -v2001 -v1102 v4028 -v3789 v3689 -v2624 -v2451 v1410 -v1355 -v1104 v560 -v415 v4029 v3688 -v2455 v1109 v564 -v4475 -v4280 v4040 -v3902 -v3787 -v1358 v1106 -v3903 -v1224 v1115 v1084 -v4481 v4286 -v3305 -v1413 -v1226 v1085 -v833 -v566 v3726 -v1231 v1086 -v837 -v567 v4291 v3740 -v3311 -v2160 v1228 v1097 -v988 -v4330 v3736 v1237 -v4484 -v4329 -v4294 v3735 v3316 -v2166 v994 v667 -v386 -v4292 v668 -v390 -v4358 v4337 v3319 v2171 v663 -v4340 v3317 -v852 -v4364 v4344 v2174 v997 -v854 v661 v4343 v2172 v859 -v3704 v856 v51 v865 -v55 v4367 -v3707 -v315 -v224 v3574 v1980 -v228 -v3633 v3582 v1981 -v1337 v321 -v3637 v3578 v3577 v1987 v1459 v3654 -v3147 -v3129 -v3660 v3131 -v1934 -v3890 -v1994 -v4268 -v3889 v3792 v3142 -v1995 -v1937 -v1400 -v634 v347 -v4223 v3791 -v3676 -v554 -v343 v4241 v3897 -v3677 v3663 -v3456 v2627 v2006 v1406 -v637 -v553 -v411 -v342 -v4237 v3901 v3678 v2628 -v4471 -v4236 -v4043 -v3905 v3693 -v3285 -v2623 -v2450 v1411 -v1354 v561 -v417 -v4044 -v3904 -v3289 v2454 -v1105 v565 -v4477 v4039 -v3788 -v2621 v1414 -v1360 -v1123 -v569 -v4279 -v1412 v1119 -v568 -v4482 v4281 -v4037 -v3737 v1118 v1100 -v984 -v832 -v420 v4287 v3739 -v3304 -v1227 v1101 -v836 v4485 v4283 v3306 -v1363 v1245 v1096 v990 -v666 -v512 -v4483 -v4295 -v3312 -v2159 v1241 -v665 -v516 -v4354 v3733 v3308 v2161 v1240 v1094 v995 -v491 -v388 -v4331 v3320 -v2167 -v392 -v4360 -v4332 v3734 v2163 v998 v4333 v2175 v996 -v4365 v4348 -v662 -v394 -v855 -v395 v4368 -v3703 -v873 -v311 v53 v4366 -v1332 -v869 -v57 -v3709 -v3579 v1719 -v1331 -v868 -v317 -v223 v3581 -v1723 -v227 v3635 -v1990 -v1455 -v1338 v322 -v59 -v3639 -v1991 -v60 v3712 -v3575 v1986 v1458 v1339 v541 -v323 v1340 -v324 v3656 v3149 -v2279 v4269 v3661 v3145 -v1933 -v344 v4267 v3146 v346 v4238 v3664 -v3452 -v3153 -v3141 -v2626 -v2194 -v2009 -v1939 -v633 -v407 v4240 v3891 v3662 v2625 -v2010 -v1399 -v4042 v3892 -v3696 -v3455 -v3213 -v3139 v2005 -v1401 -v1350 -v639 -v413 -v340 -v4041 v3893 -v3697 -v3217 v1407 -v555 -v4234 v3909 v3692 -v3284 -v2452 v2003 -v1942 v1403 -v1356 -v1120 v556 -v418 -v341 -v4470 -v3288 v2456 v1415 -v1122 v557 -v4472 -v4235 -v3690 -v2622 -v1361 v1099 -v642 v573 v421 -v4478 -v3738 v1098 v419 v4474 -v4038 -v2458 v1364 -v1242 -v1116 -v834 -v462 v4486 v4282 -v2459 -v1362 v1244 -v983 -v838 -v466 -v382 v4303 -v1117 -v985 -v511 -v487 -v381 -v4299 v3307 v991 -v515 -v4298 v3328 -v1238 v1095 v987 -v840 -v490 -v389 -v4353 -v3324 v2162 v999 -v841 -v393 -v4355 -v4351 -v3323 v2183 -v1239 v397 -v4361 -v4352 -v2179 -v396 v47 v4357 -v4347 -v3699 -v2178 -v870 v46 v4369 -v872 -v4345 -v3705 v54 v3629 -v3580 -v310 -v58 -v3710 v3628 -v2263 -v1989 v1718 -v866 -v312 -v225 v62 -v1988 -v1722 -v1333 -v318 v229 v61 -v3801 v3713 v3636 v1454 -v1334 -v867 -v537 v314 -v3805 v3711 -v3640 -v325 v3641 -v3576 -v1984 v1460 -v1344 v540 -v231 -v3642 -v232 -v3652 v3150 -v3144 -v2278 v1929 v4270 v3657 -v3143 -v345 v3653 -v3154 -v2190 -v2008 -v1935 v629 v4239 v3665 -v3152 -v2007 -v3695 -v3451 -v2193 -v2046 v1940 -v635 -v3694 -v2446 -v406 v3912 -v3457 -v3212 -v3140 -v2789 -v2445 -v1943 -v640 -v408 v3913 -v3216 -v1941 -v1402 -v1349 -v1121 v414 v3908 -v3286 -v2453 v2004 -v1423 -v1351 -v643 -v576 v410 v3290 v2457 -v1419 -v1357 v828 -v641 -v577 v422 v3906 -v3691 -v3460 v2461 -v1811 -v1418 v1353 v827 v572 -v203 -v4473 v2460 -v1815 v1365 -v1243 -v4494 v4300 -v3292 -v835 v570 -v461 v4490 v4302 -v3293 -v839 -v465 v4489 -v3325 -v2928 -v843 -v513 -v486 -v156 v3327 -v2932 -v986 -v842 v517 -v383 -v4350 -v4296 -v2180 v1007 -v492 v384 -v4349 v2182 v1003 v385 -v4297 -v3321 v1002 -v519 v401 v4356 -v871 -v520 v4377 -v3322 -v2176 v495 v4373 -v3698 -v219 v48 v4372 -v4346 v3700 -v2259 -v2177 -v218 v49 -v3706 v50 v3702 -v2262 v1720 -v1450 v226 v66 v3714 v3630 -v1724 -v313 v230 -v4579 -v3800 v3631 v1456 v1347 -v536 -v333 v234 -v3804 v3632 v1348 v329 v233 v3646 -v1985 v1726 v1461 -v1343 v542 v328 v1727 -v4278 v3151 v2280 -v808 -v294 v4274 v3651 -v3155 v1928 -v812 v4273 -v3673 -v3613 v3447 -v2189 -v2042 v1930 -v3669 v1936 v628 v3911 -v3668 -v3453 -v2839 -v2785 -v2284 -v2195 -v2045 v1932 v630 v3910 -v3280 -v1944 -v636 -v3458 -v3279 -v3214 -v2788 -v1420 v632 -v575 -v3218 v2447 -v1422 -v644 -v574 -v409 v3461 -v3287 v2448 -v2301 v2198 -v430 -v199 -v3459 v3291 v2449 -v2305 -v1352 -v426 -v4491 -v3907 v3295 -v3220 -v2465 -v1810 -v1416 -v1373 -v425 -v202 -v4493 v4301 -v3294 -v3221 -v1814 v1369 v829 -v507 -v1417 v1368 v830 -v571 -v506 -v482 -v463 -v152 -v3326 v831 -v467 v4487 -v2927 -v1836 v1004 v847 v514 v488 -v155 -v2931 -v2181 -v1840 v1006 v518 -v4488 v522 -v493 -v469 v404 v521 -v470 v405 v4374 v1000 v496 -v400 v4376 v494 -v1001 -v398 v1714 v4370 -v2258 v1713 v69 v3701 -v220 v70 -v4575 v4371 -v3722 -v2264 v1721 v1346 -v532 -v330 -v221 -v65 -v3718 -v1725 -v1449 v1345 -v332 v222 -v4578 -v3802 -v3717 -v3649 v1729 -v1451 -v538 v238 -v63 -v3806 v3650 v1728 v1457 v3645 -v2267 v1453 -v1341 v543 v326 v1462 -v4277 -v3670 -v3609 v3163 v2281 -v2185 -v807 -v293 -v3672 v3159 -v811 -v4271 -v3612 v3158 -v2835 -v2285 -v2191 -v2041 v3446 v3208 -v2283 v1931 -v4272 -v3666 v3448 v3207 -v2838 -v2784 -v2196 -v2047 v1952 -v1573 v3454 -v1948 -v1421 v631 -v3667 v3450 v3215 -v2790 v2199 -v1947 -v652 -v427 v3462 v3281 -v3219 v2197 -v648 -v429 v3282 -v3223 -v2468 -v2300 -v2050 -v1370 -v647 -v198 -v4492 v3283 -v3222 -v2469 -v2304 -v1372 v457 v3299 -v2793 -v2464 v1812 -v1619 v456 -v423 -v204 v1816 -v1623 -v4010 -v3357 -v2462 v1366 v850 -v464 -v424 -v151 -v3361 v1005 v851 -v508 -v481 -v468 v2929 -v1835 -v1818 -v1367 v846 -v509 v483 -v472 v403 -v207 -v157 -v2933 -v1839 -v1819 v510 v489 -v471 v402 -v844 v526 v485 v4375 v497 v2935 -v160 v2936 v2254 -v399 -v68 v67 -v3719 -v2260 v1786 -v3796 -v3721 -v1790 v1715 -v331 -v4574 -v3795 -v3648 v2265 v1716 v241 -v3647 v1717 -v531 v242 -v4580 -v3803 -v3715 -v2268 v1911 v1733 -v533 v237 -v64 -v3807 -v2266 -v1915 -v1452 -v539 v3808 -v3716 v3643 v1470 -v1342 v535 v327 -v235 v3809 v1466 -v544 -v4275 -v3671 v3608 v3162 v2282 -v2037 -v809 -v295 -v2286 -v2184 -v813 -v3614 -v3156 -v2834 -v2780 -v2186 -v2043 v1949 -v1569 -v2192 v1951 -v3157 -v2840 -v2786 v2188 -v2095 -v2048 -v1572 -v815 -v649 -v299 v3449 v3209 v2200 -v816 -v651 -v428 -v3617 v3470 v3210 -v2791 -v2467 -v2051 -v1945 -v194 -v3466 v3211 -v2466 -v2049 v1806 -v1371 -v3465 -v3302 v3227 -v2843 -v2794 -v2302 -v1946 v1805 -v645 -v200 -v3303 -v2792 -v2306 -v4006 v3298 v1813 -v1618 -v1434 v849 -v646 -v205 -v147 -v2923 v1817 -v1622 v848 v458 -v4009 -v3356 -v3296 -v2922 -v2463 -v2308 v1821 v459 -v208 -v153 v3360 -v2309 -v1820 v460 -v206 -v2978 v2930 -v1837 -v529 v476 -v158 -v2982 -v2934 -v1841 -v530 v484 v2938 -v845 -v720 v525 v505 -v161 v2937 -v724 v501 -v159 -v1843 v523 v500 -v1844 -v2502 -v3720 v2253 v4570 -v2764 v2255 v1785 -v240 -v2261 -v1789 v239 -v4576 v2257 v1736 -v3797 -v2269 v1737 -v4581 -v3798 v1910 v1732 v1467 v3799 -v1914 v1469 -v534 v4582 -v3813 -v3644 -v3118 v1730 v552 -v236 v34 v4583 -v3122 -v1465 -v548 -v4276 v3610 v3160 -v2830 v2294 -v810 -v740 -v296 v2290 -v2036 v1950 -v814 -v3615 -v2836 v2289 -v2091 -v2038 -v1568 -v818 -v300 -v2779 -v2187 -v2044 -v817 -v650 -v298 -v3618 -v3467 v2841 -v2781 -v2326 -v2208 -v2094 -v2040 v1574 -v3616 v3469 -v2787 -v2330 -v2296 v2204 -v2052 -v3301 v3230 -v2844 -v2783 -v2295 v2203 -v3300 v3231 -v2842 -v2795 -v193 -v3463 v3226 -v2430 -v2303 -v1577 -v1430 -v195 -v2307 v1807 -v201 -v4005 -v3464 v3224 -v2311 v1808 -v1620 -v1433 -v197 -v2310 -v1831 v1809 -v1624 -v209 -v146 -v4011 -v3358 -v3297 v1959 -v1830 -v1825 v790 -v528 -v479 -v148 v3362 -v2924 v1963 -v527 v480 -v154 -v3751 -v2977 -v2925 -v1838 -v1626 -v502 v475 -v150 -v2981 v2926 -v1842 -v1627 v504 -v162 -v4014 -v3386 -v3364 -v2942 -v2116 -v1846 -v719 v473 -v3365 -v2120 -v1845 -v723 -v2498 v524 v498 -v2760 v2501 v499 v2763 v1787 v1735 v4569 v2256 -v1791 v1734 v4571 -v2277 -v4577 -v2273 v1468 v4573 -v3816 -v2272 v1912 -v1793 -v549 -v30 v4584 -v3817 -v1916 -v1794 v551 -v3812 -v3117 v1731 v33 -v3121 -v1463 -v547 v3606 v3161 v2293 -v1564 -v806 -v739 v297 v3611 v2829 -v805 -v301 v3607 v2831 v2287 -v2205 -v2090 -v1570 -v822 -v3619 -v3468 -v2837 -v2207 -v2039 -v3229 v2833 -v2325 v2288 -v2096 -v2060 v1575 v3228 -v2845 -v2782 -v2329 -v2056 -v2803 -v2426 v2201 -v2055 -v1578 v1180 v81 -v2799 -v2297 -v1614 -v1576 -v1184 -v4001 -v3920 -v2798 -v2429 -v2298 v2202 -v2099 -v1673 -v1613 -v1429 -v3924 v3352 -v2299 -v196 -v4007 v3351 v3225 -v2315 -v1828 -v1621 -v1435 v786 -v478 -v217 -v1829 -v1625 -v477 -v213 -v4012 v3747 -v3359 v1958 -v1824 -v1629 v789 -v212 v3363 v1962 -v1832 -v1628 -v503 -v149 -v4015 -v3750 v3382 v3367 -v2979 -v2945 -v1833 -v1822 -v1594 -v1438 -v170 -v4013 v3366 v2983 -v2946 v1834 -v1598 -v166 -v3385 -v2941 -v2115 v1850 -v721 v474 -v165 -v2119 -v725 v2985 -v2939 -v2497 v253 v2986 v1781 -v2759 v2503 v1780 -v727 -v728 v2765 -v2274 v1788 -v2276 -v1906 -v1792 -v3815 -v2506 -v1905 -v1796 v4572 -v3814 -v1795 -v550 -v4592 -v2768 -v2270 v1913 -v29 v7 -v4588 -v1917 v11 -v4587 -v3810 -v3119 -v2271 v1918 v35 -v3123 v1919 -v1464 -v545 v2291 -v2086 -v1315 -v825 -v741 v309 v3605 -v2206 -v1563 -v826 v305 v3627 -v2590 -v2092 -v2057 -v1565 -v821 -v304 -v3623 v2832 -v2594 -v2059 v1571 -v3622 -v2853 -v2800 -v2327 -v2097 -v2021 v1567 -v819 -v745 v77 -v2849 -v2802 -v2331 -v1579 -v4426 -v2848 -v2425 -v2100 -v2053 -v1669 -v1425 v1179 v80 -v4430 -v2098 -v1183 -v3919 -v2953 -v2796 -v2431 -v2333 -v2318 -v2054 -v1827 -v1672 -v1431 -v214 -v4000 -v3923 -v2957 -v2334 -v2319 -v1826 -v1615 -v216 -v4130 -v4002 -v2797 -v2314 -v1616 -v1436 v785 -v4008 v3353 -v2973 -v1617 v4004 v3746 v3354 -v2972 -v2944 -v2635 -v2434 -v2312 v1960 -v1633 -v1439 v791 -v210 -v167 v4016 v3355 -v2943 -v2639 v1964 -v1437 v715 -v169 -v3752 v3381 -v3371 -v2980 v1865 -v1853 -v1823 -v1593 v714 -v211 v2984 -v1854 -v1597 -v3387 v2988 -v2493 -v2117 -v1966 v1849 -v794 v722 -v249 -v163 v2987 -v2121 -v1967 -v726 -v3755 -v2940 -v2755 -v2499 v1847 -v730 v252 -v164 -v729 v4155 -v3390 v2761 v2504 -v2123 -v2275 -v2124 v1782 v2766 -v2507 v1783 -v2505 v1784 -v4589 -v4505 v2769 -v1800 v25 -v4591 v3113 v2767 -v1907 v3112 -v1908 v31 v6 v1909 v10 -v4585 -v3811 -v3120 -v1923 v370 v36 -v3124 -v546 -v374 -v3624 v2292 v1314 -v823 -v742 v308 v3626 v2321 -v2085 -v2058 -v3019 -v2850 v2589 v2320 -v2087 -v2017 v746 -v302 -v3023 -v2852 -v2801 -v2593 -v2093 v1566 v744 -v3620 -v2421 -v2328 -v2089 v2020 -v1587 -v820 -v303 v76 -v2332 -v2101 -v1583 -v4425 -v3621 -v2846 v2427 -v2336 -v2317 -v1668 -v1582 v1181 v82 -v4429 -v2335 -v2316 -v1424 v1185 -v215 v4126 -v3921 -v2952 -v2847 -v2432 -v1674 -v1426 -v781 -v3925 -v2956 -v1954 -v1432 -v4129 -v3742 -v2435 -v1953 -v1636 -v1428 -v1187 v787 -v85 v4003 -v2433 -v1637 -v1440 -v1188 -v168 -v4024 v3927 v3748 -v3377 -v3374 v2634 -v2313 v1961 -v1861 -v1852 -v1677 -v1632 v792 -v4020 v3928 -v3375 -v2974 -v2638 -v2111 v1965 -v1851 -v4019 -v3753 v3383 -v3370 -v2975 -v2110 v1969 v1864 -v1630 -v1595 v795 v2976 -v1968 -v1599 v793 v716 v3756 -v3388 -v3368 -v2992 -v2118 v717 -v613 -v248 -v3754 -v2492 -v2122 v718 -v4151 v3391 v2494 -v2126 v1848 -v1601 -v734 v254 v3389 -v2754 -v2500 -v2125 -v1602 v4154 v2756 -v2664 v2496 v2762 -v2508 -v4501 -v3044 v2758 v1803 -v1018 -v257 -v4590 -v3048 v2770 v1804 -v4504 -v1799 v24 -v1926 -v1797 v26 v8 v3114 -v1927 v32 v12 -v4586 v3115 -v1922 v369 v28 v3116 -v373 v37 -v3625 v1316 -v824 v743 v306 -v2851 v747 -v3018 v2591 -v2016 -v1584 -v72 -v3022 -v2595 v2322 -v2088 -v1586 -v1175 v2323 -v2109 v2022 -v1664 -v1320 -v1174 v78 -v3915 -v2420 v2324 -v2105 -v4427 v3981 -v3914 -v2597 -v2422 v2340 -v2104 -v1670 -v1580 v1182 v83 -v4431 v3985 -v2598 v2428 v1186 v4125 -v3922 -v2954 v2424 -v2025 -v1675 -v1635 -v1581 -v1519 -v1190 v86 -v3926 -v2958 -v2436 -v1634 -v1523 -v1427 -v1189 -v780 v84 -v4433 -v4131 -v4021 v3930 -v3373 -v1678 -v1448 v782 -v4434 -v4023 v3929 -v3741 -v3372 v1955 -v1676 -v1589 -v1444 v788 -v3743 -v2960 v2636 v1956 -v1860 -v1694 -v1588 -v1443 v784 v3749 -v3376 -v2961 -v2640 v1957 -v1698 v796 -v4134 -v4017 v3745 v3378 -v2995 v1973 v1866 -v1631 -v1596 -v609 -v244 v3757 v3384 v2996 -v2112 -v1600 -v4248 -v4018 v3380 -v3369 -v2991 -v2642 -v2113 -v1604 -v737 -v612 -v250 -v4252 v3392 -v2643 v2114 -v1603 -v738 -v4150 -v2989 v2660 -v2130 v1869 -v733 v255 v2495 v4156 -v2663 v2516 -v1802 -v1014 -v731 -v258 v2757 v2512 -v1801 -v256 v4530 -v4500 v4451 -v3043 v2778 v2511 -v1017 v4455 -v3047 -v2774 -v2 -v4506 -v4159 -v2773 -v1925 v1380 v934 -v1 -v1924 -v1384 -v1798 v9 v27 v13 -v4509 v3127 -v2480 -v1920 v371 -v45 v14 v3128 -v375 v41 v15 -v3821 -v2586 -v2012 v1317 v755 v307 -v3825 -v1585 -v751 v3020 v2592 -v2106 v2018 -v1321 -v750 -v4421 -v3024 -v2596 -v2108 -v1319 -v71 -v4420 v2600 -v2343 v2023 -v73 -v2948 v2599 -v2344 -v1663 -v1176 v79 -v4428 -v4121 v3980 -v3556 -v3026 -v2947 v2339 -v2102 -v2026 v1665 v1177 v75 -v4432 v3984 -v3916 -v3027 -v2423 -v2024 -v1671 v1178 v87 -v4436 v4127 -v3917 -v2955 -v2444 -v2337 -v2103 v1667 -v1518 -v1445 -v1205 -v1194 -v4435 -v4022 v3918 -v2959 -v2630 -v2440 -v1679 -v1522 -v1447 v1209 -v4132 -v3934 -v2963 -v2629 -v2439 v1856 -v1063 -v2962 -v1067 v783 -v4135 -v2994 v2637 -v1976 v1862 -v1693 -v1441 -v804 -v4133 -v3744 -v2993 -v2641 -v1977 -v1697 -v1590 -v800 -v3765 -v2645 v1972 v1867 -v1591 -v1442 -v799 -v736 -v608 -v3761 v3379 -v2644 -v1592 -v735 -v243 -v4247 v4146 -v3760 v3400 v2133 -v1970 v1870 -v1608 -v614 -v245 -v4251 v3396 v2134 v1868 v251 -v4152 -v3395 -v2990 v2659 -v2513 -v2129 v247 v2515 -v259 -v4526 -v4496 v4157 -v2775 -v2665 -v2127 -v1013 -v732 -v617 -v2777 v4529 -v4502 v4450 -v4160 -v3242 -v3045 -v2566 v2509 -v1019 -v930 v4454 -v4158 -v3049 -v2570 -v4507 -v3097 -v2771 -v2668 -v2510 v1379 v933 -v1383 -v365 -v3 -v4510 -v3126 -v3051 -v2772 -v2476 -v1022 -v364 -v42 v4 -v4508 v3125 -v3052 -v44 v5 -v2479 -v1921 v372 -v181 v19 v376 v40 v3820 -v3015 v1318 v754 -v3824 v2585 -v2107 -v2011 -v1322 v3021 v2587 -v2342 v2013 -v761 -v748 -v3025 v2588 -v2341 v2019 -v765 -v3552 -v3029 v2604 v2015 -v749 -v4422 -v3028 -v2027 v74 -v4423 v3982 -v3555 -v2882 -v2441 v1197 -v95 v4424 -v4120 v3986 -v2949 -v2443 v1666 -v1446 v1198 -v91 v4440 -v4122 v3937 -v2950 -v2338 v1687 -v1520 -v1204 -v1193 -v441 -v90 v4128 v3938 -v2951 v1683 -v1524 v1208 v4124 -v3988 -v3933 -v2967 -v2437 -v1975 v1682 -v1191 -v1062 -v801 -v4136 -v3989 v2631 -v1974 v1855 -v1066 -v803 -v3931 -v3762 v2632 -v2438 v1857 -v1695 -v1526 v604 -v3764 v2633 v1863 v1699 -v1527 -v3397 -v2649 v2132 v1859 -v1611 -v797 -v610 v3399 v2131 v1871 -v1612 -v4249 -v3758 -v2655 -v1971 -v1701 -v1607 -v798 -v615 -v4253 v4145 -v2514 -v1702 -v246 v4147 -v3759 -v3393 v2661 -v1605 v1009 -v618 -v267 -v4153 -v3039 -v2776 -v616 v263 -v4525 -v4255 v4149 -v3394 -v3238 -v3038 -v2666 -v2128 -v1015 v262 -v4495 -v4256 -v4161 v4531 -v4497 v4452 -v3241 -v3093 -v3046 -v2669 -v2565 -v1020 -v929 -v4503 v4456 -v3050 -v2667 -v2569 -v4499 -v3096 -v3054 -v1481 v1381 v1023 v935 -v4511 -v3053 -v1385 v1021 -v43 -v4534 -v4458 v2475 v177 -v22 -v4459 -v366 -v23 -v2481 -v1387 v938 -v367 v180 v18 -v1388 v368 v38 v3822 v1330 v752 -v3826 v3014 v1326 v3016 -v2607 v1325 v760 -v3976 v3017 -v2608 v2014 v764 -v3975 -v3828 -v3551 -v3033 -v2878 v2603 v2035 -v1196 -v92 -v3829 -v2442 v2031 -v1514 -v1195 -v94 v4443 v3983 -v3936 -v3557 -v2881 -v2601 v2030 -v1684 -v1513 -v437 v4444 v3987 -v3935 v1686 v4439 v3991 -v2970 -v1521 -v1206 -v440 -v88 -v4123 -v3990 -v2971 -v1689 -v1525 v1210 -v802 -v4437 -v4144 -v3560 -v2966 -v1688 -v1680 -v1529 -v1192 v1064 -v89 -v4140 -v3763 -v1528 v1068 -v4139 -v3932 -v2964 -v2652 -v1696 -v1681 -v1610 -v1212 -v4243 -v3398 -v2653 v1858 v1700 -v1609 -v1213 v603 v4242 -v2648 v1879 v1704 v1070 v605 -v1875 v1703 v1071 -v611 -v4250 -v2646 -v1874 v607 -v264 -v4254 -v2654 -v619 -v266 -v4521 -v4258 -v4101 -v2656 -v1606 -v4446 -v4257 v4148 -v4105 v2662 v1008 -v4527 -v4445 v4169 -v3237 v2658 v1010 -v925 -v260 v4165 v3040 -v2670 -v1375 -v1016 v4532 v4453 v4164 -v3407 -v3243 -v3092 v3041 -v2567 -v1477 -v1374 v1012 -v931 -v261 -v4498 v4457 -v3411 v3042 -v2571 v1024 v4535 -v4519 -v4461 -v4310 -v3481 -v3098 v3058 -v2471 -v1480 v1382 v936 -v21 -v4533 -v4515 -v4460 -v4314 -v1386 -v20 -v4514 -v3246 -v2573 v2477 -v1390 v939 v176 -v2574 -v1389 v937 -v3101 -v2482 -v379 v182 v16 -v380 v39 v3823 -v2606 v1329 -v753 -v3827 -v2605 v3831 v3547 -v3172 -v3036 -v2032 -v1323 v762 v3830 -v3037 v2034 v766 -v93 v4442 -v3553 -v3032 -v2877 -v1324 v4441 -v3977 -v1685 -v1200 -v3978 -v3558 -v3030 -v2969 -v2883 -v2602 v2028 -v1765 v1544 -v1199 -v768 -v436 v3979 -v2968 v1548 -v1515 -v1058 -v769 -v4141 v3995 -v3561 -v2029 -v1516 v1207 -v1057 -v442 -v4143 -v3559 v1517 v1211 -v4438 -v2886 -v2651 v1533 -v1215 v1065 -v2650 v1690 -v1214 v1069 -v4137 -v2965 v1876 v1691 v1073 -v445 v1878 v1692 v1072 -v4138 v1708 v675 v4244 -v679 v606 -v265 v4245 -v4051 -v2647 -v1872 v627 v4246 -v4055 v623 -v4262 v4166 v4100 -v3233 -v2215 -v1873 v622 -v4520 v4168 v4104 -v2657 -v2561 -v2219 -v4522 -v3239 -v3088 v2678 -v2560 v4528 v4447 v2674 v1011 -v924 v4524 -v4516 v4448 v4162 -v3477 -v3406 -v3244 -v3094 -v3061 -v2673 -v2568 -v1476 -v1032 -v926 v4536 -v4518 v4449 -v3410 -v3062 -v2572 -v1376 -v1028 -v932 -v4465 -v4309 v4163 -v3480 -v3247 -v3099 v3057 -v2576 -v1482 -v1377 -v1027 v928 v172 -v4313 -v3245 -v2575 -v2470 v1378 v940 -v4512 v3875 -v3102 v3055 -v2472 -v1394 -v378 v178 -v3100 v2478 -v377 -v4513 v3339 -v3003 v2474 -v1485 v183 -v17 v3007 v2483 v3819 v3168 -v3035 v1327 -v757 v3818 -v3034 -v2033 v3835 -v3171 -v2873 v763 v3546 v767 v3548 v2879 -v1761 -v771 -v432 -v3554 -v770 -v3998 v3550 -v3031 -v2884 v1764 v1543 v438 -v4142 -v3999 -v3562 v1547 -v1201 v3994 -v2887 -v1536 v1202 -v909 -v443 -v2885 -v1537 v1203 -v1059 -v3992 v1532 -v1219 -v1060 v446 v1877 v1061 -v444 -v1711 v1530 -v1077 -v1712 v1707 v674 -v624 -v678 v626 -v4265 -v4050 v1705 -v4266 v4167 -v4054 -v4261 v4102 v2675 -v2214 -v620 v4106 -v3232 v2677 -v2218 -v4259 -v3234 -v3060 -v1472 -v1029 -v621 -v4523 -v4517 -v3240 -v3087 -v3059 -v2562 -v1031 v4544 v4468 -v4201 -v4108 -v3476 v3408 -v3236 -v3089 -v2671 -v2563 -v1478 -v4540 v4469 -v4205 -v4109 v3412 -v3248 -v3095 -v2564 -v927 -v4539 -v4464 -v4311 -v3871 -v3482 -v3091 -v2672 -v2580 -v1483 -v1397 -v1025 -v948 -v4315 -v3103 -v1398 v944 v171 -v4462 v3874 -v3414 -v3335 v3056 -v2071 -v1486 -v1393 -v1026 -v943 v173 -v3415 -v2473 -v1484 v179 -v4317 -v3485 v3338 -v3002 v2491 -v1391 v175 -v4318 v3006 -v2487 v184 v3838 v3260 v3167 -v1739 -v1328 v3839 v3264 -v756 -v3834 v3173 -v758 -v2872 v759 -v3997 -v3832 -v2874 -v1760 v775 -v3996 v3549 v2880 -v431 v3570 v3176 v2876 v1766 v1545 -v1535 -v905 v433 -v3566 -v2888 v1549 -v1534 v439 -v3565 v1222 -v908 v435 v1223 v447 -v3993 -v2351 v1769 -v1710 -v1551 -v1218 v1080 v2355 -v1709 -v1552 v1081 v1531 -v1216 -v1076 -v625 -v4264 -v1074 v676 -v4263 -v4096 v680 -v4095 v4052 v1706 v4056 -v2676 v4103 v2216 -v682 v4107 v3402 -v2220 -v1030 -v683 -v4541 v4467 -v4260 v4111 -v4058 v3472 v3401 v4543 v4466 -v4305 v4110 -v4059 -v3235 -v1471 -v4304 -v4200 -v3478 v3409 -v3256 -v2583 -v2222 -v1473 -v1396 -v945 -v4204 v3413 -v3252 -v3090 -v2584 -v2223 v1479 -v1395 -v947 -v4537 -v4312 -v3870 v3483 v3417 -v3251 -v3111 -v2579 -v2067 v1475 -v4316 v3416 -v3107 v1487 -v4538 -v4463 v4320 v3876 -v3486 -v3334 -v3106 -v2577 -v2488 -v2070 -v941 -v4319 -v3484 v2490 v174 v3340 v3004 -v1392 -v942 v192 v3008 -v2486 v188 v3836 v3259 v3169 -v1738 v3263 v3174 -v1756 -v778 -v1539 v779 -v3833 v3567 v3177 v1762 -v1538 v774 v3569 v3175 v2875 -v2907 v2896 v1767 v1546 -v1221 -v904 -v772 v2892 v1550 -v1220 v434 -v3563 v2891 v1770 v1554 v1079 v910 v455 v1768 v1553 v1078 v451 -v4384 -v3564 -v2350 v450 -v4388 v2354 v670 -v1217 v913 v669 v4046 v4045 -v2380 -v1075 v677 -v2210 v681 v4053 -v2545 v2209 v685 -v4097 v4057 v684 -v4098 v4061 v2217 v1299 -v4542 v4099 v4060 -v2221 -v4115 -v3253 -v2582 v2225 v3471 v3403 -v3255 -v2581 v2224 -v946 -v4202 -v3866 v3473 v3404 -v3108 -v131 v4306 -v4206 -v3479 v3405 -v3110 -v1474 v4307 -v3872 v3475 -v3421 -v3330 -v3249 -v2066 v1495 -v102 v4308 -v3487 -v2998 -v2489 v1491 -v106 v4324 -v4208 v3877 -v3336 -v3250 -v3104 -v2997 -v2578 -v2072 v1490 -v189 -v4209 v191 v3878 v3341 -v3105 v3005 -v1502 -v3879 v3009 -v2484 v1506 v187 -v4404 v3837 v3261 -v3165 v1740 -v964 -v777 v3265 v3170 v968 -v776 v3166 v3568 v3178 -v1755 v3502 -v3267 v2903 -v2893 -v1757 -v1744 -v900 v884 -v3506 -v3268 -v2895 v1763 -v1540 -v2906 -v2739 v1759 -v1541 -v906 -v773 -v452 v1771 v1542 -v454 -v2889 v1558 v911 -v4383 -v2890 -v2352 v914 -v448 -v4387 v2356 v912 -v2376 -v449 v671 v2541 -v2379 -v2358 v672 v4047 -v2359 v673 v4048 v2544 -v1295 v689 v4049 v2211 -v4118 v4065 v2212 v1298 v4196 -v4119 -v3254 v2213 v4195 -v4114 -v2229 -v127 -v3109 -v4203 -v4112 v3424 -v2062 v1492 -v130 -v4207 -v3865 v3474 v3425 v1494 -v4327 -v4211 v3867 v3495 -v3420 -v2068 -v101 -v4328 -v4210 v3873 v3491 -v3329 -v190 -v105 v4323 v3869 -v3490 -v3418 -v3331 -v3073 v2073 -v1488 v3880 v3337 -v2999 -v4321 v3333 v3000 -v2074 -v1501 -v1489 v3342 v3001 -v2485 -v2075 v1505 -v185 -v4403 v3262 v1741 v963 v3266 -v3164 v967 -v3270 v3186 -v1745 -v880 -v3269 v3182 -v2894 -v1743 v3501 v3181 v2902 -v2735 v883 -v3505 -v1758 -v899 -v453 -v2908 -v2738 -v2401 -v1779 v1561 v901 -v2405 -v2346 v1775 v1562 v907 -v2345 v1774 v1557 v903 -v588 v915 v4385 -v2911 -v2810 -v2353 -v1555 -v4389 -v2814 v2357 -v2375 -v2361 -v1648 -v2360 v4391 v2540 v2381 -v692 v4392 -v693 -v4117 v4068 v2546 -v1294 -v1270 v688 -v278 -v4116 v4069 -v1274 -v4064 -v2710 -v2384 v2232 v1300 -v686 -v2714 v2233 -v4062 -v3423 -v2549 -v2228 -v1155 -v126 v4197 v3422 -v1493 -v1159 -v4326 v4198 -v4113 -v4080 v3492 -v2226 -v1303 v132 -v4325 v4199 v3494 -v2061 v4215 -v3069 v2063 -v103 v3868 v2069 v107 v3888 -v3488 -v3419 -v3072 v2065 -v135 v3884 -v3332 -v2076 -v4322 v3883 -v3489 v3350 v3012 v1503 -v109 v3346 v3013 v1507 -v186 -v110 v4405 -v3258 v3183 v1742 v965 v3257 v3185 -v1746 v969 -v3274 -v2898 -v1038 -v879 -v1042 -v4409 v3503 -v3179 v2904 v2734 -v1776 -v1560 v971 v885 v3507 -v1778 -v1559 v972 -v4176 -v3180 -v2909 -v2740 -v2400 -v584 -v4379 -v4180 -v2404 v902 -v4378 -v3509 v2912 -v1772 v923 v888 -v587 -v3510 -v2910 v2347 v919 v4386 -v2809 -v2743 -v2371 v2348 -v1773 -v1644 -v1556 v918 v4390 -v2813 v2349 v4394 -v2536 -v2377 v2365 -v1647 -v691 v4393 -v690 -v4067 -v3846 v2542 v2382 -v1290 -v274 -v4066 -v3850 -v3531 v2547 v2385 -v2231 v1296 -v1269 -v277 -v2383 -v2230 -v1273 -v2709 v2550 v1301 -v687 v122 -v2713 -v2548 v4076 -v4063 -v1304 -v1154 v128 v3493 -v1302 -v1158 v97 v4218 -v4079 -v2227 v133 v96 v4219 -v4214 v3885 -v3068 v1886 -v136 v104 v3887 v2064 -v1890 -v1497 -v134 v108 -v4212 -v3347 v3074 v3011 v2084 -v1496 -v112 -v3349 v3010 -v2080 -v111 v3881 -v2079 v1504 v3345 v1508 v4406 v3277 -v3184 -v1754 v966 -v950 v875 -v3497 v3278 v1750 v970 v4410 v3946 -v3496 -v3273 -v2730 v1749 -v1037 v974 v881 -v4408 -v2897 -v1777 -v1041 v973 v3504 -v3271 v2899 v2736 v886 v3508 v2905 -v4175 v3512 v2901 -v2741 -v2402 -v920 v889 -v583 v4179 v3511 v2913 -v2406 -v922 v887 -v2744 -v589 v4380 -v2742 v4381 -v2811 v2408 v2368 -v1643 -v916 v4382 -v2815 v2409 -v2370 v2369 v4398 v2372 v2364 -v2145 -v1649 -v917 -v592 -v2535 v2378 -v3845 -v3527 -v2817 v2537 v2374 v2362 -v273 -v3849 -v2818 v2543 v2386 -v1289 -v3530 -v2685 v2539 -v1652 -v1291 -v1271 v279 v2689 v2551 v1297 v1275 -v4555 -v2711 v1293 -v2715 -v1305 v121 v4217 v4075 -v1277 -v1156 -v282 v123 v4216 -v1278 -v1160 v129 -v4081 -v3064 -v2717 -v1130 v125 v3886 -v2718 -v1134 -v137 v98 -v3070 v2081 v1885 -v1162 v99 -v3348 v2083 -v1889 -v1163 v100 -v4213 -v4084 -v3589 v3075 -v116 -v3593 v1498 v3882 v3076 -v2077 v1499 v3343 v3077 v1500 v4407 -v3942 v3275 -v1753 v962 -v949 v4411 v961 v874 v3945 v1747 -v1039 v978 v876 v3498 -v2729 -v2396 v1043 v882 v3499 -v3272 -v2731 -v2395 v1748 v878 -v579 v3500 v2900 v2737 -v921 v890 v4177 v3516 -v2921 v2733 -v2403 -v1045 -v585 v4181 -v2917 -v2805 -v2745 -v2407 -v1046 -v2916 v2804 v2411 -v2367 -v1639 -v590 v2410 -v2366 v4401 v4183 -v2812 -v2141 v1645 -v704 -v593 v4402 v4184 -v2816 -v591 v4397 -v2820 -v2144 -v1650 -v269 -v2819 v2373 -v1265 -v4395 -v3847 -v3526 v2394 v2363 v1653 v1264 -v275 -v3851 -v2705 v2538 -v2390 -v1651 -v4551 -v3532 -v2704 -v2684 v2559 -v2389 v1272 v280 v2688 -v2555 -v1292 v1276 -v1150 -v4554 v4071 -v3853 -v3436 -v2712 -v2554 -v1313 -v1280 -v1149 v283 -v3854 -v2716 v1309 -v1279 -v281 v4077 -v3535 -v3197 -v2720 v1308 -v1157 -v2719 -v1161 v124 -v4082 v1165 -v1129 -v145 -v3063 v2082 v1164 -v1133 v141 -v4085 -v3065 v1887 v140 -v119 -v4083 -v3071 -v1891 v120 -v3588 v3067 -v2244 -v115 -v3592 v3078 -v2078 v1893 v1511 -v113 v3344 v1894 v1512 v4419 -v3941 -v3276 -v1751 -v1034 v981 -v951 -v4415 v982 -v4594 -v4414 v3947 -v1040 v977 -v4598 -v4171 v1044 v877 -v4170 -v3519 -v2918 v1048 v975 -v954 -v898 -v3520 -v2920 -v2732 -v2397 -v1047 v894 -v578 v4178 -v3950 v3515 v2753 -v2398 v893 -v580 v4182 -v2749 v2399 v586 -v4400 v4186 -v3513 -v2914 -v2748 v2415 -v700 v582 -v4399 v4185 v2806 -v1638 -v594 -v3963 -v2915 v2807 -v2140 -v1640 -v703 -v3967 -v3841 v2808 v1646 -v3840 -v3522 v2824 -v2391 -v2146 v1642 v2393 v1654 -v268 -v4396 -v3848 -v3528 -v2556 -v357 -v270 v3852 -v2558 v1266 v276 -v4550 -v3856 -v3533 -v3432 -v2686 -v2387 v2149 -v1310 v1267 v272 -v3855 -v2706 v2690 -v1312 v1268 v284 -v4556 v3536 -v3435 -v3193 -v2707 -v2552 -v2388 -v1284 v4070 -v3534 v2708 v1151 -v4614 v4072 -v3196 v2724 -v2692 -v2553 -v1306 -v1252 v1152 -v142 v4078 -v2693 -v1881 -v1256 v1153 -v144 -v4559 v4074 v2523 -v1880 -v1307 -v1169 v1131 -v118 -v4086 v2527 -v1135 -v117 -v2860 -v2240 v1888 v138 -v3066 v2864 -v1892 v3590 v3086 -v2243 v1896 v1510 -v1137 v139 -v3594 v3082 v1895 v1509 -v1138 -v3775 v3081 -v114 -v4418 v3943 -v1752 v979 -v952 -v1033 -v4593 -v4412 v3948 -v3518 -v1035 v955 -v895 -v4597 -v3517 -v2919 v1036 -v953 -v897 -v4413 v3951 v2750 v1052 v976 -v4172 -v3949 v2752 v4173 -v2418 v891 v4174 v2419 -v581 v4190 -v3514 -v2746 v2414 v2136 v892 -v699 v602 v598 -v3962 -v2827 -v2747 v2412 v2142 -v705 -v597 -v3966 -v2828 -v2392 -v1641 v2823 -v2147 v1662 v353 -v3842 -v3521 v2680 -v2557 -v1658 v4546 -v3843 v3523 -v2821 v2679 v2150 -v1657 -v708 -v356 v3844 v3529 v2148 -v1311 v271 -v4552 v3860 v3525 -v3431 -v2687 v1287 v292 v3537 v2691 v1288 v288 -v4610 v4557 -v3437 -v3192 -v2727 -v2695 -v1283 v287 -v2728 -v2694 v1125 -v143 -v4613 -v4560 -v3198 -v2723 -v1281 -v1251 -v1172 v1124 -v4558 v4073 -v1255 v1173 v4094 -v3440 -v2721 v2522 -v1168 v1132 v4090 -v3584 v2526 -v1882 -v1136 v4089 -v3583 v3201 v3083 -v2859 -v2239 -v1883 -v1166 v1140 v3085 v2863 v1884 -v1139 -v3771 v3591 -v2245 -v1900 -v3595 -v3774 -v3596 v3079 -v3597 -v4416 v3940 v980 v3944 v956 -v896 -v4595 v1055 -v4599 v3952 v2751 v1056 -v2417 v1051 -v2416 v4601 v4193 v1049 -v695 v599 -v4602 v4194 v601 v4189 -v2826 -v701 -v2825 v2135 v4187 -v3964 v2413 v2137 v1659 -v706 -v595 -v3968 v2143 v1661 v2139 -v709 -v596 v352 v2151 -v707 -v3970 v3863 -v3427 -v2822 -v1655 -v1286 -v358 v289 v4545 -v3971 v3864 v3524 v2681 -v1285 v291 v4547 v3859 -v3545 -v3433 -v3188 -v2726 v2682 -v1656 -v4553 v3541 -v2725 v2683 -v4609 v4549 v3857 v3540 -v3438 -v3194 -v2699 -v1171 -v361 -v285 -v4561 -v1170 -v4615 -v4091 -v3441 v3199 -v1282 -v1253 -v286 v4093 -v3439 v1257 v1126 v3202 -v2722 v2524 -v2235 v1127 v3200 v3084 v2528 v1128 -v4618 v4087 -v2861 -v2241 -v1903 -v1259 -v1167 -v1144 -v3585 v2865 -v1904 -v1260 v4088 -v3770 -v3586 -v2530 -v2246 -v1899 v3587 -v2531 -v3776 v3600 -v3080 v2867 v2247 -v1897 v2868 v2248 -v4417 v1054 v3939 v1053 v960 v4596 v959 v4600 v3956 v4604 v4192 v3955 v4603 v4191 v600 v1050 -v3958 v694 -v39#### 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.93 0.98 0.92 2/54 28928
Raw data (stat): 28928 (runsolver) R 28927 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480632435 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 14443 0 0 0 964 34 0 0 25 0 1 0 480632435 59031552 12124 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14412 12124 603 41 0 14371 0
vsize: 57648
[startup+20.002 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 14537 0 0 0 1964 35 0 0 25 0 1 0 480632435 59437056 12218 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14511 12218 603 41 0 14470 0
vsize: 58044
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 14610 0 0 0 2963 35 0 0 25 0 1 0 480632435 59707392 12291 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14577 12291 603 41 0 14536 0
vsize: 58308
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 14701 0 0 0 3963 36 0 0 25 0 1 0 480632435 60108800 12382 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14675 12382 603 41 0 14634 0
vsize: 58700
[startup+50.0031 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 14784 0 0 0 4962 36 0 0 25 0 1 0 480632435 60518400 12465 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14775 12465 603 41 0 14734 0
vsize: 59100
[startup+60.0034 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 14859 0 0 0 5962 37 0 0 25 0 1 0 480632435 60788736 12540 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 12540 603 41 0 14800 0
vsize: 59364
[startup+70.0045 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 16737 0 0 0 6956 42 0 0 25 0 1 0 480632435 61661184 12778 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 12778 603 41 0 15013 0
vsize: 60216
[startup+80.0052 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 16749 0 0 0 7956 43 0 0 25 0 1 0 480632435 61661184 12790 4294967295 134512640 134672761 3221224544 3221223704 134614477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15054 12790 603 41 0 15013 0
vsize: 60216
[startup+90.0054 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 16842 0 0 0 8956 44 0 0 25 0 1 0 480632435 61923328 12883 4294967295 134512640 134672761 3221224544 3221223720 134615853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15118 12883 603 41 0 15077 0
vsize: 60472
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 18461 0 0 0 9950 49 0 0 25 0 1 0 480632435 62902272 13046 4294967295 134512640 134672761 3221224544 3221222108 134523229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15357 13046 603 41 0 15316 0
vsize: 61428
[startup+110.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 20556 0 0 0 10943 56 0 0 25 0 1 0 480632435 62672896 13044 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15301 13044 603 41 0 15260 0
vsize: 61204
[startup+120.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 20645 0 0 0 11942 57 0 0 25 0 1 0 480632435 63074304 13133 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15399 13133 603 41 0 15358 0
vsize: 61596
[startup+130.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 21111 0 0 0 12941 58 0 0 25 0 1 0 480632435 64925696 13599 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15851 13599 603 41 0 15810 0
vsize: 63404
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 21333 0 0 0 13940 60 0 0 25 0 1 0 480632435 65859584 13821 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16079 13821 603 41 0 16038 0
vsize: 64316
[startup+150.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 21764 0 0 0 14939 61 0 0 25 0 1 0 480632435 67588096 14252 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16501 14252 603 41 0 16460 0
vsize: 66004
[startup+160.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 22237 0 0 0 15937 63 0 0 25 0 1 0 480632435 69718016 14725 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17021 14725 603 41 0 16980 0
vsize: 68084
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 22388 0 0 0 16937 64 0 0 25 0 1 0 480632435 70393856 14876 4294967295 134512640 134672761 3221224544 3221223536 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17186 14876 603 41 0 17145 0
vsize: 68744
[startup+180.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 22672 0 0 0 17936 65 0 0 25 0 1 0 480632435 71454720 15160 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17445 15160 603 41 0 17404 0
vsize: 69780
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 23538 0 0 0 18932 68 0 0 25 0 1 0 480632435 75018240 16026 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18315 16026 603 41 0 18274 0
vsize: 73260
[startup+200.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 24350 0 0 0 19929 71 0 0 25 0 1 0 480632435 78327808 16838 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19123 16838 603 41 0 19082 0
vsize: 76492
[startup+210.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 25036 0 0 0 20927 74 0 0 25 0 1 0 480632435 81121280 17524 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19805 17524 603 41 0 19764 0
vsize: 79220
[startup+220.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 25935 0 0 0 21924 76 0 0 25 0 1 0 480632435 84824064 18423 4294967295 134512640 134672761 3221224544 3221223584 134603565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20709 18423 603 41 0 20668 0
vsize: 82836
[startup+230.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 26978 0 0 0 22920 80 0 0 25 0 1 0 480632435 89042944 19466 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21739 19466 603 41 0 21698 0
vsize: 86956
[startup+240.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 27887 0 0 0 23917 84 0 0 25 0 1 0 480632435 92733440 20375 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22640 20375 603 41 0 22599 0
vsize: 90560
[startup+250.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 28721 0 0 0 24915 86 0 0 25 0 1 0 480632435 96157696 21209 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23476 21209 603 41 0 23435 0
vsize: 93904
[startup+260.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 29447 0 0 0 25913 88 0 0 25 0 1 0 480632435 99045376 21935 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24181 21935 603 41 0 24140 0
vsize: 96724
[startup+270.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 30137 0 0 0 26911 90 0 0 25 0 1 0 480632435 101937152 22625 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24887 22625 603 41 0 24846 0
vsize: 99548
[startup+280.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 30781 0 0 0 27909 92 0 0 25 0 1 0 480632435 104591360 23269 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25535 23269 603 41 0 25494 0
vsize: 102140
[startup+290.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 31262 0 0 0 28908 93 0 0 25 0 1 0 480632435 106450944 23750 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25989 23750 603 41 0 25948 0
vsize: 103956
[startup+300.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 32254 0 0 0 29905 97 0 0 25 0 1 0 480632435 111058944 24742 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27114 24742 603 41 0 27073 0
vsize: 108456
[startup+310.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 33168 0 0 0 30903 99 0 0 25 0 1 0 480632435 114749440 25656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28015 25656 603 41 0 27974 0
vsize: 112060
[startup+320.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 34018 0 0 0 31899 103 0 0 25 0 1 0 480632435 118312960 26506 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28885 26506 603 41 0 28844 0
vsize: 115540
[startup+330.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 34783 0 0 0 32897 105 0 0 25 0 1 0 480632435 121352192 27271 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29627 27271 603 41 0 29586 0
vsize: 118508
[startup+340.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 35502 0 0 0 33895 107 0 0 25 0 1 0 480632435 124264448 27990 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30338 27990 603 41 0 30297 0
vsize: 121352
[startup+350.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 36168 0 0 0 34893 109 0 0 25 0 1 0 480632435 127029248 28656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31013 28656 603 41 0 30972 0
vsize: 124052
[startup+360.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 36815 0 0 0 35891 111 0 0 25 0 1 0 480632435 129654784 29303 4294967295 134512640 134672761 3221224544 3221223680 134614503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31654 29303 603 41 0 31613 0
vsize: 126616
[startup+370.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 37344 0 0 0 36889 114 0 0 25 0 1 0 480632435 131768320 29832 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32170 29832 603 41 0 32129 0
vsize: 128680
[startup+380.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 37873 0 0 0 37887 116 0 0 25 0 1 0 480632435 134012928 30361 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32718 30361 603 41 0 32677 0
vsize: 130872
[startup+390.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 39970 0 0 0 38880 123 0 0 25 0 1 0 480632435 135401472 30730 4294967295 134512640 134672761 3221224544 3221223800 134616233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33057 30730 603 41 0 33016 0
vsize: 132228
[startup+400.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 39879 124 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+410.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 40878 125 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+420.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 41878 125 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+430.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 42878 125 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+440.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 43878 126 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+450.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 44878 126 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+460.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 45878 126 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+470.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 46877 127 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+480.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 47877 127 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+490.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 48877 127 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+500.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 49877 127 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+510.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 50877 128 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223680 134614664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+520.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 51877 128 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+530.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 52877 128 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+540.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 53877 128 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+550.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 54876 129 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+560.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 55876 129 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+570.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 56876 129 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+580.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 57876 130 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+590.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 58875 130 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+600.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 59875 130 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+610.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 60875 131 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+620.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 61875 131 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+630.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 62875 131 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+640.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 63875 131 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+650.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 64875 131 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+660.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 65875 131 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+670.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 66875 131 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+680.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 67875 131 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+690.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 68875 132 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+700.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 69875 132 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+710.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40287 0 0 0 70874 132 0 0 25 0 1 0 480632435 136450048 30880 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30880 603 41 0 33272 0
vsize: 133252
[startup+720.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40292 0 0 0 71874 132 0 0 25 0 1 0 480632435 136450048 30885 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30885 603 41 0 33272 0
vsize: 133252
[startup+730.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40297 0 0 0 72874 133 0 0 25 0 1 0 480632435 136450048 30890 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30890 603 41 0 33272 0
vsize: 133252
[startup+740.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40302 0 0 0 73874 133 0 0 25 0 1 0 480632435 136450048 30895 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30895 603 41 0 33272 0
vsize: 133252
[startup+750.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40307 0 0 0 74874 133 0 0 25 0 1 0 480632435 136450048 30900 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30900 603 41 0 33272 0
vsize: 133252
[startup+760.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40310 0 0 0 75874 134 0 0 25 0 1 0 480632435 136450048 30903 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30903 603 41 0 33272 0
vsize: 133252
[startup+770.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40313 0 0 0 76873 134 0 0 25 0 1 0 480632435 136450048 30906 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33313 30906 603 41 0 33272 0
vsize: 133252
[startup+780.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 40576 0 0 0 77872 135 0 0 25 0 1 0 480632435 137633792 31169 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33602 31169 603 41 0 33561 0
vsize: 134408
[startup+790.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 41124 0 0 0 78871 137 0 0 25 0 1 0 480632435 139751424 31717 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34119 31717 603 41 0 34078 0
vsize: 136476
[startup+800.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 41703 0 0 0 79868 139 0 0 25 0 1 0 480632435 142127104 32296 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34699 32296 603 41 0 34658 0
vsize: 138796
[startup+810.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 42289 0 0 0 80867 141 0 0 25 0 1 0 480632435 144642048 32882 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35313 32882 603 41 0 35272 0
vsize: 141252
[startup+820.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 42843 0 0 0 81864 144 0 0 25 0 1 0 480632435 146878464 33436 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35859 33436 603 41 0 35818 0
vsize: 143436
[startup+830.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 43371 0 0 0 82862 146 0 0 25 0 1 0 480632435 148987904 33964 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36374 33964 603 41 0 36333 0
vsize: 145496
[startup+840.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 43971 0 0 0 83861 148 0 0 25 0 1 0 480632435 151474176 34564 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36981 34564 603 41 0 36940 0
vsize: 147924
[startup+850.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 44331 0 0 0 84860 149 0 0 25 0 1 0 480632435 152952832 34924 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37342 34924 603 41 0 37301 0
vsize: 149368
[startup+860.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 44696 0 0 0 85859 149 0 0 25 0 1 0 480632435 154411008 35289 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37698 35289 603 41 0 37657 0
vsize: 150792
[startup+870.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 45157 0 0 0 86858 151 0 0 25 0 1 0 480632435 156274688 35750 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38153 35750 603 41 0 38112 0
vsize: 152612
[startup+880.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 45543 0 0 0 87857 152 0 0 25 0 1 0 480632435 157855744 36136 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38539 36136 603 41 0 38498 0
vsize: 154156
[startup+890.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 45697 0 0 0 88857 153 0 0 25 0 1 0 480632435 158392320 36290 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38670 36290 603 41 0 38629 0
vsize: 154680
[startup+900.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 45797 0 0 0 89856 153 0 0 25 0 1 0 480632435 158797824 36390 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38769 36390 603 41 0 38728 0
vsize: 155076
[startup+910.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 46078 0 0 0 90856 154 0 0 25 0 1 0 480632435 160006144 36671 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39064 36671 603 41 0 39023 0
vsize: 156256
[startup+920.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 46278 0 0 0 91856 154 0 0 25 0 1 0 480632435 160804864 36871 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39259 36871 603 41 0 39218 0
vsize: 157036
[startup+930.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 46665 0 0 0 92855 155 0 0 25 0 1 0 480632435 162267136 37258 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39616 37258 603 41 0 39575 0
vsize: 158464
[startup+940.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 47295 0 0 0 93853 157 0 0 25 0 1 0 480632435 165957632 37888 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40517 37888 603 41 0 40476 0
vsize: 162068
[startup+950.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48211 0 0 0 94851 160 0 0 25 0 1 0 480632435 170438656 38772 4294967295 134512640 134672761 3221224544 3221223600 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41611 38772 603 41 0 41570 0
vsize: 166444
[startup+960.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 95851 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+970.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 96851 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+980.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 97852 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+990.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 98852 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 99852 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 100852 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 101852 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 102852 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 103853 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 104853 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 105853 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 106853 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 107854 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 108854 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 109854 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 110854 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 111854 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 112855 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 113855 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 114855 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 115855 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 116855 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223712 134564767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 117855 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 118856 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28928
Raw data (stat): 28928 (minisat+) R 28927 22612 22611 0 -1 0 48292 0 0 0 119856 160 0 0 25 0 1 0 480632435 168341504 38590 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41099 38590 603 41 0 41058 0
vsize: 164396
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.98 0.92 1/54 28928
Raw data (stat): 28928 (minisat+) Z 28927 22612 22611 0 -1 12 48293 0 0 0 119856 167 0 0 25 0 1 0 480632435 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.13
CPU time (s): 1200.25
CPU user time (s): 1198.57
CPU system time (s): 1.67974
CPU usage (%): 100.01
Max. virtual memory (Kb): 166444
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####