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 5117

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        896400 kB
Buffers:         34176 kB
Cached:          67980 kB
SwapCached:        320 kB
Active:          51012 kB
Inactive:        54372 kB
HighTotal:      131008 kB
HighFree:        58968 kB
LowTotal:       903652 kB
LowFree:        837432 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27292 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:19:59 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 3362 7 1200.28 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5262 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 870]---> BDD-cost:   11
c ---[ 869]---> BDD-cost:   20
c ---[ 868]---> BDD-cost:   29
c ---[ 867]---> BDD-cost:   29
c ---[ 866]---> BDD-cost:   29
c ---[ 865]---> BDD-cost:   26
c ---[ 864]---> BDD-cost:   38
c ---[ 863]---> BDD-cost:   26
c ---[ 862]---> BDD-cost:   20
c ---[ 861]---> BDD-cost:   20
c ---[ 860]---> BDD-cost:   23
c ---[ 859]---> BDD-cost:   20
c ---[ 858]---> BDD-cost:   23
c ---[ 857]---> BDD-cost:   23
c ---[ 856]---> BDD-cost:   26
c ---[ 855]---> BDD-cost:   11
c ---[ 854]---> BDD-cost:   11
c ---[ 853]---> BDD-cost:    8
c ---[ 852]---> BDD-cost:   11
c ---[ 851]---> BDD-cost:    8
c ---[ 850]---> BDD-cost:   14
c ---[ 849]---> BDD-cost:    8
c ---[ 848]---> BDD-cost:    7
c ---[ 843]---> BDD-cost:   26
c ---[ 842]---> BDD-cost:   35
c ---[ 841]---> BDD-cost:   32
c ---[ 840]---> BDD-cost:   38
c ---[ 839]---> BDD-cost:   38
c ---[ 838]---> BDD-cost:   44
c ---[ 837]---> BDD-cost:   35
c ---[ 836]---> BDD-cost:   29
c ---[ 835]---> BDD-cost:   29
c ---[ 834]---> BDD-cost:   24
c ---[ 833]---> BDD-cost:   29
c ---[ 832]---> BDD-cost:   26
c ---[ 831]---> BDD-cost:   26
c ---[ 830]---> BDD-cost:   17
c ---[ 829]---> BDD-cost:   20
c ---[ 828]---> BDD-cost:   11
c ---[ 827]---> BDD-cost:   17
c ---[ 826]---> BDD-cost:   20
c ---[ 825]---> BDD-cost:   23
c ---[ 824]---> BDD-cost:   18
c ---[ 823]---> BDD-cost:   18
c ---[ 821]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:   35
c ---[ 816]---> BDD-cost:   25
c ---[ 815]---> BDD-cost:   45
c ---[ 814]---> BDD-cost:   39
c ---[ 813]---> BDD-cost:   44
c ---[ 812]---> BDD-cost:   41
c ---[ 811]---> BDD-cost:   50
c ---[ 810]---> BDD-cost:   44
c ---[ 809]---> BDD-cost:   38
c ---[ 808]---> BDD-cost:   35
c ---[ 807]---> BDD-cost:   35
c ---[ 806]---> BDD-cost:   32
c ---[ 805]---> BDD-cost:   38
c ---[ 804]---> BDD-cost:   26
c ---[ 803]---> BDD-cost:   26
c ---[ 802]---> BDD-cost:   20
c ---[ 801]---> BDD-cost:   23
c ---[ 800]---> BDD-cost:   17
c ---[ 799]---> BDD-cost:   20
c ---[ 798]---> BDD-cost:   21
c ---[ 797]---> BDD-cost:   26
c ---[ 796]---> BDD-cost:   23
c ---[ 795]---> BDD-cost:   26
c ---[ 794]---> BDD-cost:   13
c ---[ 793]---> BDD-cost:   20
c ---[ 792]---> BDD-cost:   11
c ---[ 789]---> BDD-cost:   20
c ---[ 788]---> BDD-cost:   29
c ---[ 787]---> BDD-cost:   41
c ---[ 786]---> BDD-cost:   44
c ---[ 785]---> BDD-cost:   56
c ---[ 784]---> BDD-cost:   53
c ---[ 783]---> BDD-cost:   53
c ---[ 782]---> BDD-cost:   47
c ---[ 781]---> BDD-cost:   47
c ---[ 780]---> BDD-cost:   44
c ---[ 779]---> BDD-cost:   47
c ---[ 778]---> BDD-cost:   41
c ---[ 777]---> BDD-cost:   38
c ---[ 776]---> BDD-cost:   35
c ---[ 775]---> BDD-cost:   38
c ---[ 774]---> BDD-cost:   35
c ---[ 773]---> BDD-cost:   29
c ---[ 772]---> BDD-cost:   20
c ---[ 771]---> BDD-cost:   20
c ---[ 770]---> BDD-cost:   17
c ---[ 769]---> BDD-cost:   20
c ---[ 768]---> BDD-cost:   29
c ---[ 767]---> BDD-cost:   32
c ---[ 766]---> BDD-cost:   26
c ---[ 765]---> BDD-cost:   32
c ---[ 764]---> BDD-cost:   19
c ---[ 763]---> BDD-cost:   26
c ---[ 762]---> BDD-cost:   17
c ---[ 761]---> BDD-cost:    7
c ---[ 760]---> BDD-cost:   17
c ---[ 759]---> BDD-cost:   26
c ---[ 758]---> BDD-cost:   32
c ---[ 757]---> BDD-cost:   44
c ---[ 756]---> BDD-cost:   47
c ---[ 755]---> BDD-cost:   53
c ---[ 754]---> BDD-cost:   53
c ---[ 753]---> BDD-cost:   47
c ---[ 752]---> BDD-cost:   47
c ---[ 751]---> BDD-cost:   50
c ---[ 750]---> BDD-cost:   47
c ---[ 749]---> BDD-cost:   45
c ---[ 748]---> BDD-cost:   44
c ---[ 747]---> BDD-cost:   41
c ---[ 746]---> BDD-cost:   38
c ---[ 745]---> BDD-cost:   35
c ---[ 744]---> BDD-cost:   29
c ---[ 743]---> BDD-cost:   20
c ---[ 742]---> BDD-cost:   23
c ---[ 741]---> BDD-cost:   23
c ---[ 740]---> BDD-cost:   20
c ---[ 739]---> BDD-cost:   23
c ---[ 738]---> BDD-cost:   26
c ---[ 737]---> BDD-cost:   30
c ---[ 736]---> BDD-cost:   35
c ---[ 735]---> BDD-cost:   35
c ---[ 734]---> BDD-cost:   29
c ---[ 733]---> BDD-cost:   23
c ---[ 732]---> BDD-cost:   20
c ---[ 731]---> BDD-cost:   17
c ---[ 730]---> BDD-cost:   17
c ---[ 729]---> BDD-cost:   27
c ---[ 728]---> BDD-cost:   35
c ---[ 727]---> BDD-cost:   47
c ---[ 726]---> BDD-cost:   50
c ---[ 725]---> BDD-cost:   47
c ---[ 724]---> BDD-cost:   44
c ---[ 723]---> BDD-cost:   47
c ---[ 722]---> BDD-cost:   50
c ---[ 721]---> BDD-cost:   44
c ---[ 720]---> BDD-cost:   41
c ---[ 719]---> BDD-cost:   44
c ---[ 718]---> BDD-cost:   47
c ---[ 717]---> BDD-cost:   38
c ---[ 716]---> BDD-cost:   35
c ---[ 715]---> BDD-cost:   35
c ---[ 714]---> BDD-cost:   29
c ---[ 713]---> BDD-cost:   20
c ---[ 712]---> BDD-cost:   20
c ---[ 711]---> BDD-cost:   20
c ---[ 710]---> BDD-cost:   23
c ---[ 709]---> BDD-cost:   17
c ---[ 708]---> BDD-cost:   26
c ---[ 707]---> BDD-cost:   32
c ---[ 706]---> BDD-cost:   29
c ---[ 705]---> BDD-cost:   29
c ---[ 704]---> BDD-cost:   32
c ---[ 703]---> BDD-cost:   24
c ---[ 702]---> BDD-cost:   17
c ---[ 701]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:   23
c ---[ 699]---> BDD-cost:   35
c ---[ 698]---> BDD-cost:   38
c ---[ 697]---> BDD-cost:   41
c ---[ 696]---> BDD-cost:   38
c ---[ 695]---> BDD-cost:   44
c ---[ 694]---> BDD-cost:   47
c ---[ 693]---> BDD-cost:   44
c ---[ 692]---> BDD-cost:   44
c ---[ 691]---> BDD-cost:   47
c ---[ 690]---> BDD-cost:   44
c ---[ 689]---> BDD-cost:   47
c ---[ 688]---> BDD-cost:   44
c ---[ 687]---> BDD-cost:   38
c ---[ 686]---> BDD-cost:   32
c ---[ 685]---> BDD-cost:   23
c ---[ 684]---> BDD-cost:   29
c ---[ 683]---> BDD-cost:   20
c ---[ 682]---> BDD-cost:   20
c ---[ 681]---> BDD-cost:   11
c ---[ 680]---> BDD-cost:   14
c ---[ 679]---> BDD-cost:   17
c ---[ 678]---> BDD-cost:   26
c ---[ 677]---> BDD-cost:   29
c ---[ 676]---> BDD-cost:   29
c ---[ 675]---> BDD-cost:   32
c ---[ 674]---> BDD-cost:   32
c ---[ 673]---> BDD-cost:   29
c ---[ 672]---> BDD-cost:   20
c ---[ 671]---> BDD-cost:   26
c ---[ 670]---> BDD-cost:   26
c ---[ 669]---> BDD-cost:   38
c ---[ 668]---> BDD-cost:   41
c ---[ 667]---> BDD-cost:   41
c ---[ 666]---> BDD-cost:   41
c ---[ 665]---> BDD-cost:   38
c ---[ 664]---> BDD-cost:   44
c ---[ 663]---> BDD-cost:   44
c ---[ 662]---> BDD-cost:   41
c ---[ 661]---> BDD-cost:   47
c ---[ 660]---> BDD-cost:   47
c ---[ 659]---> BDD-cost:   44
c ---[ 658]---> BDD-cost:   44
c ---[ 657]---> BDD-cost:   32
c ---[ 656]---> BDD-cost:   29
c ---[ 655]---> BDD-cost:   29
c ---[ 654]---> BDD-cost:   23
c ---[ 653]---> BDD-cost:   14
c ---[ 652]---> BDD-cost:   11
c ---[ 651]---> BDD-cost:    8
c ---[ 650]---> BDD-cost:   14
c ---[ 649]---> BDD-cost:   17
c ---[ 648]---> BDD-cost:   17
c ---[ 647]---> BDD-cost:   24
c ---[ 646]---> BDD-cost:   32
c ---[ 645]---> BDD-cost:   29
c ---[ 644]---> BDD-cost:   26
c ---[ 643]---> BDD-cost:   20
c ---[ 642]---> BDD-cost:   26
c ---[ 641]---> BDD-cost:   29
c ---[ 640]---> BDD-cost:   35
c ---[ 639]---> BDD-cost:   41
c ---[ 638]---> BDD-cost:   38
c ---[ 637]---> BDD-cost:   38
c ---[ 636]---> BDD-cost:   38
c ---[ 635]---> BDD-cost:   41
c ---[ 634]---> BDD-cost:   41
c ---[ 633]---> BDD-cost:   38
c ---[ 632]---> BDD-cost:   42
c ---[ 631]---> BDD-cost:   47
c ---[ 630]---> BDD-cost:   41
c ---[ 629]---> BDD-cost:   41
c ---[ 628]---> BDD-cost:   32
c ---[ 627]---> BDD-cost:   29
c ---[ 626]---> BDD-cost:   26
c ---[ 625]---> BDD-cost:   18
c ---[ 624]---> BDD-cost:   14
c ---[ 623]---> BDD-cost:   11
c ---[ 622]---> BDD-cost:    8
c ---[ 621]---> BDD-cost:   11
c ---[ 620]---> BDD-cost:   23
c ---[ 619]---> BDD-cost:   23
c ---[ 618]---> BDD-cost:   23
c ---[ 617]---> BDD-cost:   26
c ---[ 616]---> BDD-cost:   29
c ---[ 615]---> BDD-cost:   20
c ---[ 614]---> BDD-cost:   17
c ---[ 613]---> BDD-cost:   24
c ---[ 612]---> BDD-cost:   26
c ---[ 611]---> BDD-cost:   29
c ---[ 610]---> BDD-cost:   35
c ---[ 609]---> BDD-cost:   35
c ---[ 608]---> BDD-cost:   35
c ---[ 607]---> BDD-cost:   44
c ---[ 606]---> BDD-cost:   47
c ---[ 605]---> BDD-cost:   53
c ---[ 604]---> BDD-cost:   38
c ---[ 603]---> BDD-cost:   41
c ---[ 602]---> BDD-cost:   41
c ---[ 601]---> BDD-cost:   38
c ---[ 600]---> BDD-cost:   50
c ---[ 599]---> BDD-cost:   53
c ---[ 598]---> BDD-cost:   44
c ---[ 597]---> BDD-cost:   41
c ---[ 596]---> BDD-cost:   29
c ---[ 595]---> BDD-cost:   26
c ---[ 594]---> BDD-cost:   20
c ---[ 593]---> BDD-cost:   11
c ---[ 592]---> BDD-cost:    8
c ---[ 591]---> BDD-cost:    8
c ---[ 590]---> BDD-cost:   17
c ---[ 589]---> BDD-cost:   20
c ---[ 588]---> BDD-cost:   26
c ---[ 587]---> BDD-cost:   26
c ---[ 586]---> BDD-cost:   26
c ---[ 585]---> BDD-cost:   20
c ---[ 584]---> BDD-cost:   14
c ---[ 583]---> BDD-cost:   23
c ---[ 582]---> BDD-cost:   32
c ---[ 581]---> BDD-cost:   32
c ---[ 580]---> BDD-cost:   41
c ---[ 579]---> BDD-cost:   38
c ---[ 578]---> BDD-cost:   48
c ---[ 577]---> BDD-cost:   53
c ---[ 576]---> BDD-cost:   56
c ---[ 575]---> BDD-cost:   47
c ---[ 574]---> BDD-cost:   47
c ---[ 573]---> BDD-cost:   44
c ---[ 572]---> BDD-cost:   53
c ---[ 571]---> BDD-cost:   53
c ---[ 570]---> BDD-cost:   53
c ---[ 569]---> BDD-cost:   47
c ---[ 568]---> BDD-cost:   41
c ---[ 567]---> BDD-cost:   35
c ---[ 566]---> BDD-cost:   29
c ---[ 565]---> BDD-cost:   23
c ---[ 564]---> BDD-cost:   17
c ---[ 563]---> BDD-cost:   11
c ---[ 562]---> BDD-cost:    8
c ---[ 561]---> BDD-cost:   11
c ---[ 560]---> BDD-cost:   20
c ---[ 559]---> BDD-cost:   23
c ---[ 558]---> BDD-cost:   20
c ---[ 557]---> BDD-cost:   20
c ---[ 556]---> BDD-cost:   17
c ---[ 555]---> BDD-cost:   17
c ---[ 554]---> BDD-cost:   23
c ---[ 553]---> BDD-cost:   29
c ---[ 552]---> BDD-cost:   35
c ---[ 551]---> BDD-cost:   41
c ---[ 550]---> BDD-cost:   50
c ---[ 549]---> BDD-cost:   47
c ---[ 548]---> BDD-cost:   47
c ---[ 547]---> BDD-cost:   47
c ---[ 546]---> BDD-cost:   50
c ---[ 545]---> BDD-cost:   50
c ---[ 544]---> BDD-cost:   56
c ---[ 543]---> BDD-cost:   59
c ---[ 542]---> BDD-cost:   59
c ---[ 541]---> BDD-cost:   47
c ---[ 540]---> BDD-cost:   44
c ---[ 539]---> BDD-cost:   47
c ---[ 538]---> BDD-cost:   32
c ---[ 537]---> BDD-cost:   26
c ---[ 536]---> BDD-cost:   26
c ---[ 535]---> BDD-cost:   20
c ---[ 534]---> BDD-cost:   14
c ---[ 533]---> BDD-cost:   17
c ---[ 532]---> BDD-cost:   20
c ---[ 531]---> BDD-cost:   23
c ---[ 530]---> BDD-cost:   20
c ---[ 529]---> BDD-cost:   20
c ---[ 528]---> BDD-cost:   17
c ---[ 527]---> BDD-cost:   11
c ---[ 526]---> BDD-cost:   11
c ---[ 525]---> BDD-cost:   23
c ---[ 524]---> BDD-cost:   29
c ---[ 523]---> BDD-cost:   32
c ---[ 522]---> BDD-cost:   41
c ---[ 521]---> BDD-cost:   41
c ---[ 520]---> BDD-cost:   44
c ---[ 519]---> BDD-cost:   47
c ---[ 518]---> BDD-cost:   50
c ---[ 517]---> BDD-cost:   50
c ---[ 516]---> BDD-cost:   50
c ---[ 515]---> BDD-cost:   53
c ---[ 514]---> BDD-cost:   56
c ---[ 513]---> BDD-cost:   47
c ---[ 512]---> BDD-cost:   53
c ---[ 511]---> BDD-cost:   53
c ---[ 510]---> BDD-cost:   47
c ---[ 509]---> BDD-cost:   47
c ---[ 508]---> BDD-cost:   41
c ---[ 507]---> BDD-cost:   35
c ---[ 506]---> BDD-cost:   24
c ---[ 505]---> BDD-cost:   29
c ---[ 504]---> BDD-cost:   26
c ---[ 503]---> BDD-cost:   26
c ---[ 502]---> BDD-cost:   23
c ---[ 501]---> BDD-cost:   32
c ---[ 500]---> BDD-cost:   26
c ---[ 499]---> BDD-cost:   26
c ---[ 498]---> BDD-cost:   17
c ---[ 497]---> BDD-cost:   14
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:   17
c ---[ 494]---> BDD-cost:   29
c ---[ 493]---> BDD-cost:   26
c ---[ 492]---> BDD-cost:   32
c ---[ 491]---> BDD-cost:   38
c ---[ 490]---> BDD-cost:   38
c ---[ 489]---> BDD-cost:   47
c ---[ 488]---> BDD-cost:   44
c ---[ 487]---> BDD-cost:   41
c ---[ 486]---> BDD-cost:   50
c ---[ 485]---> BDD-cost:   56
c ---[ 484]---> BDD-cost:   56
c ---[ 483]---> BDD-cost:   56
c ---[ 482]---> BDD-cost:   50
c ---[ 481]---> BDD-cost:   47
c ---[ 480]---> BDD-cost:   44
c ---[ 479]---> BDD-cost:   44
c ---[ 478]---> BDD-cost:   38
c ---[ 477]---> BDD-cost:   36
c ---[ 476]---> BDD-cost:   35
c ---[ 475]---> BDD-cost:   38
c ---[ 474]---> BDD-cost:   38
c ---[ 473]---> BDD-cost:   35
c ---[ 472]---> BDD-cost:   41
c ---[ 471]---> BDD-cost:   32
c ---[ 470]---> BDD-cost:   32
c ---[ 469]---> BDD-cost:   20
c ---[ 468]---> BDD-cost:   20
c ---[ 467]---> BDD-cost:   11
c ---[ 466]---> BDD-cost:   11
c ---[ 465]---> BDD-cost:   23
c ---[ 464]---> BDD-cost:   35
c ---[ 463]---> BDD-cost:   44
c ---[ 462]---> BDD-cost:   41
c ---[ 461]---> BDD-cost:   47
c ---[ 460]---> BDD-cost:   47
c ---[ 459]---> BDD-cost:   45
c ---[ 458]---> BDD-cost:   47
c ---[ 457]---> BDD-cost:   50
c ---[ 456]---> BDD-cost:   56
c ---[ 455]---> BDD-cost:   50
c ---[ 454]---> BDD-cost:   53
c ---[ 453]---> BDD-cost:   38
c ---[ 452]---> BDD-cost:   35
c ---[ 451]---> BDD-cost:   41
c ---[ 450]---> BDD-cost:   41
c ---[ 449]---> BDD-cost:   35
c ---[ 448]---> BDD-cost:   38
c ---[ 447]---> BDD-cost:   44
c ---[ 446]---> BDD-cost:   41
c ---[ 445]---> BDD-cost:   38
c ---[ 444]---> BDD-cost:   41
c ---[ 443]---> BDD-cost:   41
c ---[ 442]---> BDD-cost:   35
c ---[ 441]---> BDD-cost:   35
c ---[ 440]---> BDD-cost:   29
c ---[ 439]---> BDD-cost:   20
c ---[ 438]---> BDD-cost:   14
c ---[ 437]---> BDD-cost:   12
c ---[ 436]---> BDD-cost:   14
c ---[ 435]---> BDD-cost:   20
c ---[ 434]---> BDD-cost:   35
c ---[ 433]---> BDD-cost:   38
c ---[ 432]---> BDD-cost:   50
c ---[ 431]---> BDD-cost:   50
c ---[ 430]---> BDD-cost:   50
c ---[ 429]---> BDD-cost:   41
c ---[ 428]---> BDD-cost:   47
c ---[ 427]---> BDD-cost:   50
c ---[ 426]---> BDD-cost:   50
c ---[ 425]---> BDD-cost:   38
c ---[ 424]---> BDD-cost:   41
c ---[ 423]---> BDD-cost:   30
c ---[ 422]---> BDD-cost:   35
c ---[ 421]---> BDD-cost:   29
c ---[ 420]---> BDD-cost:   32
c ---[ 419]---> BDD-cost:   32
c ---[ 418]---> BDD-cost:   41
c ---[ 417]---> BDD-cost:   41
c ---[ 416]---> BDD-cost:   41
c ---[ 415]---> BDD-cost:   41
c ---[ 414]---> BDD-cost:   41
c ---[ 413]---> BDD-cost:   50
c ---[ 412]---> BDD-cost:   41
c ---[ 411]---> BDD-cost:   41
c ---[ 410]---> BDD-cost:   29
c ---[ 409]---> BDD-cost:   20
c ---[ 408]---> BDD-cost:   14
c ---[ 407]---> BDD-cost:   14
c ---[ 406]---> BDD-cost:   14
c ---[ 405]---> BDD-cost:   20
c ---[ 404]---> BDD-cost:   26
c ---[ 403]---> BDD-cost:   29
c ---[ 402]---> BDD-cost:   44
c ---[ 401]---> BDD-cost:   47
c ---[ 400]---> BDD-cost:   53
c ---[ 399]---> BDD-cost:   44
c ---[ 398]---> BDD-cost:   44
c ---[ 397]---> BDD-cost:   38
c ---[ 396]---> BDD-cost:   35
c ---[ 395]---> BDD-cost:   26
c ---[ 394]---> BDD-cost:   35
c ---[ 393]---> BDD-cost:   23
c ---[ 392]---> BDD-cost:   26
c ---[ 391]---> BDD-cost:   32
c ---[ 390]---> BDD-cost:   32
c ---[ 389]---> BDD-cost:   29
c ---[ 388]---> BDD-cost:   32
c ---[ 387]---> BDD-cost:   45
c ---[ 386]---> BDD-cost:   44
c ---[ 385]---> BDD-cost:   44
c ---[ 384]---> BDD-cost:   41
c ---[ 383]---> BDD-cost:   47
c ---[ 382]---> BDD-cost:   47
c ---[ 381]---> BDD-cost:   50
c ---[ 380]---> BDD-cost:   32
c ---[ 379]---> BDD-cost:   29
c ---[ 378]---> BDD-cost:   11
c ---[ 377]---> BDD-cost:    8
c ---[ 376]---> BDD-cost:   14
c ---[ 375]---> BDD-cost:   20
c ---[ 374]---> BDD-cost:   23
c ---[ 373]---> BDD-cost:   27
c ---[ 372]---> BDD-cost:   38
c ---[ 371]---> BDD-cost:   32
c ---[ 370]---> BDD-cost:   47
c ---[ 369]---> BDD-cost:   35
c ---[ 368]---> BDD-cost:   35
c ---[ 367]---> BDD-cost:   26
c ---[ 366]---> BDD-cost:   23
c ---[ 365]---> BDD-cost:   23
c ---[ 364]---> BDD-cost:   23
c ---[ 363]---> BDD-cost:   17
c ---[ 362]---> BDD-cost:   23
c ---[ 361]---> BDD-cost:   20
c ---[ 360]---> BDD-cost:   26
c ---[ 359]---> BDD-cost:   29
c ---[ 358]---> BDD-cost:   38
c ---[ 357]---> BDD-cost:   47
c ---[ 356]---> BDD-cost:   50
c ---[ 355]---> BDD-cost:   50
c ---[ 354]---> BDD-cost:   47
c ---[ 353]---> BDD-cost:   50
c ---[ 352]---> BDD-cost:   44
c ---[ 351]---> BDD-cost:   53
c ---[ 350]---> BDD-cost:   47
c ---[ 349]---> BDD-cost:   29
c ---[ 348]---> BDD-cost:   14
c ---[ 347]---> BDD-cost:   11
c ---[ 346]---> BDD-cost:   11
c ---[ 345]---> BDD-cost:   17
c ---[ 344]---> BDD-cost:   26
c ---[ 343]---> BDD-cost:   26
c ---[ 342]---> BDD-cost:   30
c ---[ 341]---> BDD-cost:   26
c ---[ 340]---> BDD-cost:   29
c ---[ 339]---> BDD-cost:   23
c ---[ 338]---> BDD-cost:   32
c ---[ 337]---> BDD-cost:   32
c ---[ 336]---> BDD-cost:   23
c ---[ 335]---> BDD-cost:   14
c ---[ 334]---> BDD-cost:   23
c ---[ 333]---> BDD-cost:   14
c ---[ 332]---> BDD-cost:   20
c ---[ 331]---> BDD-cost:   14
c ---[ 330]---> BDD-cost:   17
c ---[ 329]---> BDD-cost:   20
c ---[ 328]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   44
c ---[ 326]---> BDD-cost:   53
c ---[ 325]---> BDD-cost:   47
c ---[ 324]---> BDD-cost:   50
c ---[ 323]---> BDD-cost:   53
c ---[ 322]---> BDD-cost:   56
c ---[ 321]---> BDD-cost:   47
c ---[ 320]---> BDD-cost:   38
c ---[ 319]---> BDD-cost:   29
c ---[ 318]---> BDD-cost:   17
c ---[ 317]---> BDD-cost:    8
c ---[ 316]---> BDD-cost:    8
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   20
c ---[ 313]---> BDD-cost:   23
c ---[ 312]---> BDD-cost:   26
c ---[ 311]---> BDD-cost:   26
c ---[ 310]---> BDD-cost:   26
c ---[ 309]---> BDD-cost:   26
c ---[ 308]---> BDD-cost:   26
c ---[ 307]---> BDD-cost:   26
c ---[ 306]---> BDD-cost:   23
c ---[ 305]---> BDD-cost:   17
c ---[ 304]---> BDD-cost:   11
c ---[ 303]---> BDD-cost:   11
c ---[ 302]---> BDD-cost:   17
c ---[ 301]---> BDD-cost:   12
c ---[ 300]---> BDD-cost:   11
c ---[ 299]---> BDD-cost:   14
c ---[ 298]---> BDD-cost:   26
c ---[ 297]---> BDD-cost:   29
c ---[ 296]---> BDD-cost:   41
c ---[ 295]---> BDD-cost:   44
c ---[ 294]---> BDD-cost:   47
c ---[ 293]---> BDD-cost:   44
c ---[ 292]---> BDD-cost:   50
c ---[ 291]---> BDD-cost:   38
c ---[ 290]---> BDD-cost:   26
c ---[ 289]---> BDD-cost:   17
c ---[ 288]---> BDD-cost:   14
c ---[ 287]---> BDD-cost:   11
c ---[ 286]---> BDD-cost:   17
c ---[ 285]---> BDD-cost:   20
c ---[ 284]---> BDD-cost:   32
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:   26
c ---[ 281]---> BDD-cost:   26
c ---[ 280]---> BDD-cost:   23
c ---[ 279]---> BDD-cost:   26
c ---[ 278]---> BDD-cost:   20
c ---[ 277]---> BDD-cost:   17
c ---[ 276]---> BDD-cost:   14
c ---[ 275]---> BDD-cost:   11
c ---[ 274]---> BDD-cost:   14
c ---[ 273]---> BDD-cost:   14
c ---[ 272]---> BDD-cost:   14
c ---[ 271]---> BDD-cost:   11
c ---[ 270]---> BDD-cost:   17
c ---[ 269]---> BDD-cost:   23
c ---[ 268]---> BDD-cost:   32
c ---[ 267]---> BDD-cost:   38
c ---[ 266]---> BDD-cost:   44
c ---[ 265]---> BDD-cost:   35
c ---[ 264]---> BDD-cost:   41
c ---[ 263]---> BDD-cost:   35
c ---[ 262]---> BDD-cost:   26
c ---[ 261]---> BDD-cost:   17
c ---[ 260]---> BDD-cost:    8
c ---[ 259]---> BDD-cost:   12
c ---[ 258]---> BDD-cost:   23
c ---[ 257]---> BDD-cost:   26
c ---[ 256]---> BDD-cost:   32
c ---[ 255]---> BDD-cost:   32
c ---[ 254]---> BDD-cost:   29
c ---[ 253]---> BDD-cost:   29
c ---[ 252]---> BDD-cost:   29
c ---[ 251]---> BDD-cost:   18
c ---[ 250]---> BDD-cost:   20
c ---[ 249]---> BDD-cost:   20
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   11
c ---[ 246]---> BDD-cost:   14
c ---[ 245]---> BDD-cost:   20
c ---[ 244]---> BDD-cost:   20
c ---[ 243]---> BDD-cost:   17
c ---[ 242]---> BDD-cost:   23
c ---[ 241]---> BDD-cost:   21
c ---[ 240]---> BDD-cost:   26
c ---[ 239]---> BDD-cost:   30
c ---[ 238]---> BDD-cost:   38
c ---[ 237]---> BDD-cost:   35
c ---[ 236]---> BDD-cost:   29
c ---[ 235]---> BDD-cost:   35
c ---[ 234]---> BDD-cost:   30
c ---[ 233]---> BDD-cost:   23
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   11
c ---[ 230]---> BDD-cost:   14
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:   32
c ---[ 227]---> BDD-cost:   35
c ---[ 226]---> BDD-cost:   29
c ---[ 225]---> BDD-cost:   29
c ---[ 224]---> BDD-cost:   35
c ---[ 223]---> BDD-cost:   35
c ---[ 222]---> BDD-cost:   29
c ---[ 221]---> BDD-cost:   29
c ---[ 220]---> BDD-cost:   17
c ---[ 219]---> BDD-cost:   17
c ---[ 218]---> BDD-cost:   17
c ---[ 217]---> BDD-cost:   26
c ---[ 216]---> BDD-cost:   26
c ---[ 215]---> BDD-cost:   23
c ---[ 214]---> BDD-cost:   29
c ---[ 213]---> BDD-cost:   26
c ---[ 212]---> BDD-cost:   26
c ---[ 211]---> BDD-cost:   29
c ---[ 210]---> BDD-cost:   32
c ---[ 209]---> BDD-cost:   32
c ---[ 208]---> BDD-cost:   35
c ---[ 207]---> BDD-cost:   35
c ---[ 206]---> BDD-cost:   29
c ---[ 205]---> BDD-cost:   23
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:   14
c ---[ 202]---> BDD-cost:   17
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:   26
c ---[ 199]---> BDD-cost:   29
c ---[ 198]---> BDD-cost:   38
c ---[ 197]---> BDD-cost:   35
c ---[ 196]---> BDD-cost:   26
c ---[ 195]---> BDD-cost:   35
c ---[ 194]---> BDD-cost:   32
c ---[ 193]---> BDD-cost:   26
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   26
c ---[ 190]---> BDD-cost:   23
c ---[ 189]---> BDD-cost:   29
c ---[ 188]---> BDD-cost:   35
c ---[ 187]---> BDD-cost:   29
c ---[ 186]---> BDD-cost:   32
c ---[ 185]---> BDD-cost:   38
c ---[ 184]---> BDD-cost:   29
c ---[ 183]---> BDD-cost:   23
c ---[ 182]---> BDD-cost:   20
c ---[ 181]---> BDD-cost:   26
c ---[ 180]---> BDD-cost:   32
c ---[ 179]---> BDD-cost:   26
c ---[ 178]---> BDD-cost:   32
c ---[ 177]---> BDD-cost:   26
c ---[ 176]---> BDD-cost:   23
c ---[ 175]---> BDD-cost:   20
c ---[ 174]---> BDD-cost:   14
c ---[ 173]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   23
c ---[ 171]---> BDD-cost:   29
c ---[ 170]---> BDD-cost:   32
c ---[ 169]---> BDD-cost:   29
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   35
c ---[ 166]---> BDD-cost:   29
c ---[ 165]---> BDD-cost:   26
c ---[ 164]---> BDD-cost:   32
c ---[ 163]---> BDD-cost:   26
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   26
c ---[ 160]---> BDD-cost:   32
c ---[ 159]---> BDD-cost:   35
c ---[ 158]---> BDD-cost:   26
c ---[ 157]---> BDD-cost:   29
c ---[ 156]---> BDD-cost:   35
c ---[ 155]---> BDD-cost:   32
c ---[ 154]---> BDD-cost:   23
c ---[ 153]---> BDD-cost:   23
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   23
c ---[ 150]---> BDD-cost:   29
c ---[ 149]---> BDD-cost:   26
c ---[ 148]---> BDD-cost:   17
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   17
c ---[ 145]---> BDD-cost:   17
c ---[ 144]---> BDD-cost:   20
c ---[ 143]---> BDD-cost:   29
c ---[ 142]---> BDD-cost:   35
c ---[ 141]---> BDD-cost:   32
c ---[ 140]---> BDD-cost:   23
c ---[ 139]---> BDD-cost:   20
c ---[ 138]---> BDD-cost:   26
c ---[ 137]---> BDD-cost:   32
c ---[ 136]---> BDD-cost:   32
c ---[ 135]---> BDD-cost:   32
c ---[ 134]---> BDD-cost:   29
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   29
c ---[ 131]---> BDD-cost:   35
c ---[ 130]---> BDD-cost:   35
c ---[ 129]---> BDD-cost:   32
c ---[ 128]---> BDD-cost:   29
c ---[ 127]---> BDD-cost:   38
c ---[ 126]---> BDD-cost:   38
c ---[ 125]---> BDD-cost:   41
c ---[ 124]---> BDD-cost:   32
c ---[ 123]---> BDD-cost:   32
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   26
c ---[ 120]---> BDD-cost:   29
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:   17
c ---[ 117]---> BDD-cost:   14
c ---[ 116]---> BDD-cost:    8
c ---[ 115]---> BDD-cost:   17
c ---[ 114]---> BDD-cost:   23
c ---[ 113]---> BDD-cost:   20
c ---[ 112]---> BDD-cost:   29
c ---[ 111]---> BDD-cost:   32
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   26
c ---[ 108]---> BDD-cost:   23
c ---[ 107]---> BDD-cost:   29
c ---[ 106]---> BDD-cost:   29
c ---[ 105]---> BDD-cost:   23
c ---[ 104]---> BDD-cost:   29
c ---[ 103]---> BDD-cost:   29
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:   38
c ---[ 100]---> BDD-cost:   38
c ---[  99]---> BDD-cost:   36
c ---[  98]---> BDD-cost:   32
c ---[  97]---> BDD-cost:   38
c ---[  96]---> BDD-cost:   44
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:   38
c ---[  93]---> BDD-cost:   38
c ---[  92]---> BDD-cost:   35
c ---[  91]---> BDD-cost:   32
c ---[  90]---> BDD-cost:   26
c ---[  89]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   20
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:    7
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:   26
c ---[  81]---> BDD-cost:   23
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   26
c ---[  78]---> BDD-cost:   27
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   20
c ---[  75]---> BDD-cost:   20
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   23
c ---[  72]---> BDD-cost:   29
c ---[  71]---> BDD-cost:   35
c ---[  70]---> BDD-cost:   38
c ---[  69]---> BDD-cost:   35
c ---[  68]---> BDD-cost:   38
c ---[  67]---> BDD-cost:   38
c ---[  66]---> BDD-cost:   35
c ---[  65]---> BDD-cost:   38
c ---[  64]---> BDD-cost:   35
c ---[  63]---> BDD-cost:   35
c ---[  62]---> BDD-cost:   32
c ---[  61]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   20
c ---[  59]---> BDD-cost:   17
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:    3
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   20
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   17
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   17
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   20
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   23
c ---[  42]---> BDD-cost:   26
c ---[  41]---> BDD-cost:   26
c ---[  40]---> BDD-cost:   26
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   29
c ---[  37]---> BDD-cost:   38
c ---[  36]---> BDD-cost:   29
c ---[  35]---> BDD-cost:   30
c ---[  34]---> BDD-cost:   29
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   24
c ---[  31]---> BDD-cost:   23
c ---[  30]---> BDD-cost:   17
c ---[  29]---> BDD-cost:   17
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    5
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:    8
c ---[  18]---> BDD-cost:    8
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:    8
c ---[  14]---> BDD-cost:   17
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   20
c ---[  11]---> BDD-cost:   23
c ---[  10]---> BDD-cost:   26
c ---[   9]---> BDD-cost:   17
c ---[   8]---> BDD-cost:   23
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   23
c ---[   5]---> BDD-cost:   21
c ---[   4]---> BDD-cost:   23
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   62745   180525 |   20915       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 5404[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11365   maxlim: 2777   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  142221   464357 |   47407       0        0     nan |  0.000 % |
c |       100 |  142221   464357 |   52147     100      307     3.1 |  2.100 % |
c |       250 |  142221   464357 |   57362     250      780     3.1 |  2.100 % |
c |       475 |  142221   464357 |   63098     475     1460     3.1 |  2.100 % |
c |       812 |  142221   464357 |   69408     812     2566     3.2 |  2.100 % |
c |      1318 |  142221   464357 |   76349    1318     4337     3.3 |  2.100 % |
c |      2078 |  142221   464357 |   83984    2078     7446     3.6 |  2.100 % |
c |      3217 |  142221   464357 |   92382    3217    12524     3.9 |  2.100 % |
c |      4925 |  142221   464357 |  101621    4925    22669     4.6 |  2.100 % |
c |      7487 |  142221   464357 |  111783    7487    39205     5.2 |  2.100 % |
c |     11331 |  142221   464357 |  122961   11331    68550     6.0 |  2.100 % |
c |     17097 |  142212   464326 |  135257   17095   131325     7.7 |  2.103 % |
c |     25746 |  142212   464326 |  148783   25744   209659     8.1 |  2.103 % |
c |     38721 |  142212   464326 |  163661   38719   339802     8.8 |  2.103 % |
c ==============================================================================
c [1mFound solution: 784[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 7397   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50137 |  142241   464456 |   47413   50135   466389     9.3 |  2.103 % |
c |     50237 |  142241   464456 |   52154   15699   145298     9.3 |  2.122 % |
c |     50388 |  142241   464456 |   57369   15850   146463     9.2 |  2.122 % |
c |     50613 |  142241   464456 |   63106   16075   148724     9.3 |  2.122 % |
c |     50951 |  142241   464456 |   69417   16413   151032     9.2 |  2.122 % |
c |     51457 |  142241   464456 |   76359   16919   156718     9.3 |  2.122 % |
c |     52217 |  142241   464456 |   83995   17679   173239     9.8 |  2.122 % |
c |     53356 |  142241   464456 |   92394   18818   185040     9.8 |  2.122 % |
c |     55064 |  142234   464436 |  101633   20523   197448     9.6 |  2.124 % |
c |     57627 |  142234   464436 |  111797   23086   212396     9.2 |  2.124 % |
c |     61471 |  142234   464436 |  122977   26930   246288     9.1 |  2.124 % |
c |     67237 |  142234   464436 |  135274   32696   308239     9.4 |  2.124 % |
c |     75887 |  142234   464436 |  148802   41346   383600     9.3 |  2.124 % |
c |     88861 |  142234   464436 |  163682   54320   691679    12.7 |  2.124 % |
c |    108322 |  142234   464436 |  180050   73781  1073388    14.5 |  2.124 % |
c |    137515 |  142234   464436 |  198055  102974  3406989    33.1 |  2.124 % |
c |    181304 |  142234   464436 |  217861  146763  8040676    54.8 |  2.124 % |
c |    246988 |  142234   464436 |  239647  212447 15270865    71.9 |  2.124 % |
c |    345514 |  142234   464436 |  263612   61402 10429585   169.9 |  2.124 % |
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 v3957 v696 -v1660 v702 v4188 v3965 v698 v350 v3969 -v2138 v710 v3973 v3862 -v2158 v354 -v3972 v3861 -v2155 -v290 -#### 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.91 0.95 0.90 2/55 24000
Raw data (stat): 24000 (runsolver) R 23999 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479373611 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0305 s]
Raw data (loadavg): 0.93 0.95 0.90 3/58 24036
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 11292 0 3 0 970 31 0 0 25 0 1 0 479373611 49504256 9893 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12086 9893 603 41 0 12045 0
vsize: 48344
[startup+20.032 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 24053
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 11368 0 3 0 1959 41 0 0 25 0 1 0 479373611 49930240 9969 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12190 9969 603 41 0 12149 0
vsize: 48760
[startup+30.0316 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 24053
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 11425 0 3 0 2959 41 0 0 25 0 1 0 479373611 50065408 10026 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12223 10026 603 41 0 12182 0
vsize: 48892
[startup+40.0318 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 24053
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 11545 0 3 0 3958 41 0 0 25 0 1 0 479373611 50593792 10146 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12352 10146 603 41 0 12311 0
vsize: 49408
[startup+50.0327 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 24053
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 11618 0 3 0 4958 42 0 0 25 0 1 0 479373611 50864128 10219 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12418 10219 603 41 0 12377 0
vsize: 49672
[startup+60.0334 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24053
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 11700 0 3 0 5958 42 0 0 25 0 1 0 479373611 51269632 10301 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12517 10301 603 41 0 12476 0
vsize: 50068
[startup+70.0336 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24053
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 11775 0 3 0 6958 43 0 0 25 0 1 0 479373611 51539968 10376 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12583 10376 603 41 0 12542 0
vsize: 50332
[startup+80.0332 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24055
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 11859 0 3 0 7957 43 0 0 25 0 1 0 479373611 51933184 10460 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12679 10461 603 41 0 12638 0
vsize: 50716
[startup+90.0334 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24055
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 11953 0 3 0 8957 44 0 0 25 0 1 0 479373611 52338688 10554 4294967295 134512640 134672761 3221224624 3221223792 134553595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12778 10554 603 41 0 12737 0
vsize: 51112
[startup+100.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24055
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12108 0 3 0 9956 44 0 0 25 0 1 0 479373611 52879360 10709 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12910 10709 603 41 0 12869 0
vsize: 51640
[startup+110.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24055
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12465 0 3 0 10956 45 0 0 25 0 1 0 479373611 54087680 10993 4294967295 134512640 134672761 3221224624 3221223880 134562565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13205 10993 603 41 0 13164 0
vsize: 52820
[startup+120.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12465 0 3 0 11956 45 0 0 25 0 1 0 479373611 54087680 10993 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13205 10993 603 41 0 13164 0
vsize: 52820
[startup+130.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12465 0 3 0 12956 45 0 0 25 0 1 0 479373611 54087680 10993 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13205 10993 603 41 0 13164 0
vsize: 52820
[startup+140.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12465 0 3 0 13956 45 0 0 25 0 1 0 479373611 54087680 10993 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13205 10993 603 41 0 13164 0
vsize: 52820
[startup+150.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12465 0 3 0 14956 45 0 0 25 0 1 0 479373611 54087680 10993 4294967295 134512640 134672761 3221224624 3221223776 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13205 10993 603 41 0 13164 0
vsize: 52820
[startup+160.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12465 0 3 0 15956 45 0 0 25 0 1 0 479373611 54087680 10993 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13205 10993 603 41 0 13164 0
vsize: 52820
[startup+170.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12465 0 3 0 16956 45 0 0 25 0 1 0 479373611 54087680 10993 4294967295 134512640 134672761 3221224624 3221223792 134564493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13205 10993 603 41 0 13164 0
vsize: 52820
[startup+180.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12465 0 3 0 17956 45 0 0 25 0 1 0 479373611 54087680 10993 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13205 10993 603 41 0 13164 0
vsize: 52820
[startup+190.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12544 0 3 0 18956 46 0 0 25 0 1 0 479373611 54358016 11072 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13271 11072 603 41 0 13230 0
vsize: 53084
[startup+200.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 12857 0 3 0 19956 46 0 0 25 0 1 0 479373611 55574528 11385 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13568 11385 603 41 0 13527 0
vsize: 54272
[startup+210.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 13069 0 3 0 20955 47 0 0 25 0 1 0 479373611 56385536 11597 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13766 11597 603 41 0 13725 0
vsize: 55064
[startup+220.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 13432 0 3 0 21954 48 0 0 25 0 1 0 479373611 58118144 11960 4294967295 134512640 134672761 3221224624 3221223792 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14189 11960 603 41 0 14148 0
vsize: 56756
[startup+230.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 13714 0 3 0 22954 49 0 0 25 0 1 0 479373611 59187200 12242 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14450 12242 603 41 0 14409 0
vsize: 57800
[startup+240.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 14441 0 3 0 23952 50 0 0 25 0 1 0 479373611 62136320 12969 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15170 12969 603 41 0 15129 0
vsize: 60680
[startup+250.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 15134 0 3 0 24950 52 0 0 25 0 1 0 479373611 65081344 13662 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15889 13662 603 41 0 15848 0
vsize: 63556
[startup+260.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 15806 0 3 0 25949 54 0 0 25 0 1 0 479373611 67776512 14334 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16547 14334 603 41 0 16506 0
vsize: 66188
[startup+270.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 15965 0 3 0 26948 55 0 0 25 0 1 0 479373611 68448256 14493 4294967295 134512640 134672761 3221224624 3221223840 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16711 14493 603 41 0 16670 0
vsize: 66844
[startup+280.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 16142 0 3 0 27948 56 0 0 25 0 1 0 479373611 69124096 14670 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16876 14670 603 41 0 16835 0
vsize: 67504
[startup+290.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 16412 0 3 0 28947 56 0 0 25 0 1 0 479373611 70205440 14940 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17140 14940 603 41 0 17099 0
vsize: 68560
[startup+300.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 17193 0 3 0 29945 58 0 0 25 0 1 0 479373611 73302016 15721 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17896 15721 603 41 0 17855 0
vsize: 71584
[startup+310.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 17705 0 3 0 30944 60 0 0 25 0 1 0 479373611 75444224 16233 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18419 16233 603 41 0 18378 0
vsize: 73676
[startup+320.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 17862 0 3 0 31944 60 0 0 25 0 1 0 479373611 75984896 16390 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18551 16390 603 41 0 18510 0
vsize: 74204
[startup+330.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 18737 0 3 0 32942 63 0 0 25 0 1 0 479373611 80142336 17265 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19566 17265 603 41 0 19525 0
vsize: 78264
[startup+340.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 19555 0 3 0 33939 65 0 0 25 0 1 0 479373611 83501056 18083 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20386 18083 603 41 0 20345 0
vsize: 81544
[startup+350.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24057
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 20301 0 3 0 34937 68 0 0 25 0 1 0 479373611 86454272 18829 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21107 18829 603 41 0 21066 0
vsize: 84428
[startup+360.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24059
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 20939 0 3 0 35935 69 0 0 25 0 1 0 479373611 89141248 19467 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21763 19467 603 41 0 21722 0
vsize: 87052
[startup+370.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24059
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 21499 0 3 0 36934 71 0 0 25 0 1 0 479373611 91414528 20027 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22318 20027 603 41 0 22277 0
vsize: 89272
[startup+380.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24059
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 22119 0 3 0 37932 73 0 0 25 0 1 0 479373611 93843456 20647 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22911 20647 603 41 0 22870 0
vsize: 91644
[startup+390.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24059
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 22702 0 3 0 38930 75 0 0 25 0 1 0 479373611 96268288 21230 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23503 21230 603 41 0 23462 0
vsize: 94012
[startup+400.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24059
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 23313 0 3 0 39929 77 0 0 25 0 1 0 479373611 98693120 21841 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24095 21841 603 41 0 24054 0
vsize: 96380
[startup+410.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24059
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 23828 0 3 0 40927 79 0 0 25 0 1 0 479373611 100843520 22356 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24620 22356 603 41 0 24579 0
vsize: 98480
[startup+420.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 24388 0 3 0 41925 80 0 0 25 0 1 0 479373611 103120896 22916 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25176 22916 603 41 0 25135 0
vsize: 100704
[startup+430.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 24886 0 3 0 42924 82 0 0 25 0 1 0 479373611 105144320 23414 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25670 23414 603 41 0 25629 0
vsize: 102680
[startup+440.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 25340 0 3 0 43922 84 0 0 25 0 1 0 479373611 107020288 23868 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26128 23868 603 41 0 26087 0
vsize: 104512
[startup+450.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 25775 0 3 0 44921 85 0 0 25 0 1 0 479373611 108756992 24303 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26552 24303 603 41 0 26511 0
vsize: 106208
[startup+460.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 26217 0 3 0 45920 86 0 0 25 0 1 0 479373611 110522368 24745 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26983 24745 603 41 0 26942 0
vsize: 107932
[startup+470.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 26816 0 3 0 46918 88 0 0 25 0 1 0 479373611 112955392 25344 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27577 25344 603 41 0 27536 0
vsize: 110308
[startup+480.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 27408 0 3 0 47916 91 0 0 25 0 1 0 479373611 115367936 25936 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28166 25936 603 41 0 28125 0
vsize: 112664
[startup+490.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 28069 0 3 0 48914 93 0 0 25 0 1 0 479373611 118063104 26597 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28824 26597 603 41 0 28783 0
vsize: 115296
[startup+500.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 28606 0 3 0 49911 96 0 0 25 0 1 0 479373611 120217600 27134 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29350 27134 603 41 0 29309 0
vsize: 117400
[startup+510.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 29164 0 3 0 50910 97 0 0 25 0 1 0 479373611 122511360 27692 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29910 27692 603 41 0 29869 0
vsize: 119640
[startup+520.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 29901 0 3 0 51908 99 0 0 25 0 1 0 479373611 125472768 28429 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30633 28429 603 41 0 30592 0
vsize: 122532
[startup+530.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 30527 0 3 0 52906 101 0 0 25 0 1 0 479373611 128028672 29055 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31257 29055 603 41 0 31216 0
vsize: 125028
[startup+540.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 31150 0 3 0 53905 103 0 0 25 0 1 0 479373611 130592768 29678 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31883 29678 603 41 0 31842 0
vsize: 127532
[startup+550.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 31722 0 3 0 54902 105 0 0 25 0 1 0 479373611 133017600 30250 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32475 30250 603 41 0 32434 0
vsize: 129900
[startup+560.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 32229 0 3 0 55901 107 0 0 25 0 1 0 479373611 135036928 30757 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32968 30757 603 41 0 32927 0
vsize: 131872
[startup+570.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 32760 0 3 0 56899 109 0 0 25 0 1 0 479373611 137191424 31288 4294967295 134512640 134672761 3221224624 3221223728 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33494 31288 603 41 0 33453 0
vsize: 133976
[startup+580.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 33267 0 3 0 57898 110 0 0 25 0 1 0 479373611 139214848 31795 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33988 31795 603 41 0 33947 0
vsize: 135952
[startup+590.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 33717 0 3 0 58896 113 0 0 25 0 1 0 479373611 141099008 32245 4294967295 134512640 134672761 3221224624 3221223760 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34448 32245 603 41 0 34407 0
vsize: 137792
[startup+600.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 34127 0 3 0 59895 114 0 0 25 0 1 0 479373611 142721024 32655 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34844 32655 603 41 0 34803 0
vsize: 139376
[startup+610.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 34535 0 3 0 60893 116 0 0 25 0 1 0 479373611 144470016 33063 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35271 33063 603 41 0 35230 0
vsize: 141084
[startup+620.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 34951 0 3 0 61892 117 0 0 25 0 1 0 479373611 146092032 33479 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35667 33479 603 41 0 35626 0
vsize: 142668
[startup+630.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 35357 0 3 0 62891 119 0 0 25 0 1 0 479373611 147853312 33885 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36097 33885 603 41 0 36056 0
vsize: 144388
[startup+640.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 35775 0 3 0 63889 121 0 0 25 0 1 0 479373611 149606400 34303 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36525 34303 603 41 0 36484 0
vsize: 146100
[startup+650.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 36166 0 3 0 64888 122 0 0 25 0 1 0 479373611 151089152 34694 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36887 34694 603 41 0 36846 0
vsize: 147548
[startup+660.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 36523 0 3 0 65887 123 0 0 25 0 1 0 479373611 152571904 35051 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37249 35051 603 41 0 37208 0
vsize: 148996
[startup+670.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 36896 0 3 0 66886 124 0 0 25 0 1 0 479373611 154050560 35424 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37610 35424 603 41 0 37569 0
vsize: 150440
[startup+680.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 37258 0 3 0 67885 125 0 0 25 0 1 0 479373611 155537408 35786 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37973 35786 603 41 0 37932 0
vsize: 151892
[startup+690.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 37578 0 3 0 68884 126 0 0 25 0 1 0 479373611 156889088 36106 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38303 36106 603 41 0 38262 0
vsize: 153212
[startup+700.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 37920 0 3 0 69884 127 0 0 25 0 1 0 479373611 159281152 36448 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38887 36448 603 41 0 38846 0
vsize: 155548
[startup+710.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24061
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 38254 0 3 0 70883 128 0 0 25 0 1 0 479373611 160632832 36782 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39217 36782 603 41 0 39176 0
vsize: 156868
[startup+720.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 38600 0 3 0 71882 129 0 0 25 0 1 0 479373611 162119680 37128 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39580 37128 603 41 0 39539 0
vsize: 158320
[startup+730.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 38958 0 3 0 72881 130 0 0 25 0 1 0 479373611 163606528 37486 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39943 37486 603 41 0 39902 0
vsize: 159772
[startup+740.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39253 0 3 0 73880 132 0 0 25 0 1 0 479373611 164818944 37781 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40239 37781 603 41 0 40198 0
vsize: 160956
[startup+750.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39557 0 3 0 74879 133 0 0 25 0 1 0 479373611 166031360 38085 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40535 38085 603 41 0 40494 0
vsize: 162140
[startup+760.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39862 0 3 0 75878 134 0 0 25 0 1 0 479373611 167247872 38390 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40832 38390 603 41 0 40791 0
vsize: 163328
[startup+770.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39988 0 3 0 76877 135 0 0 25 0 1 0 479373611 167788544 38516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38516 603 41 0 40923 0
vsize: 163856
[startup+780.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39989 0 3 0 77877 135 0 0 25 0 1 0 479373611 167788544 38517 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38517 603 41 0 40923 0
vsize: 163856
[startup+790.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39989 0 3 0 78878 135 0 0 25 0 1 0 479373611 167788544 38517 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38517 603 41 0 40923 0
vsize: 163856
[startup+800.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39989 0 3 0 79878 135 0 0 25 0 1 0 479373611 167788544 38517 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38517 603 41 0 40923 0
vsize: 163856
[startup+810.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39989 0 3 0 80878 135 0 0 25 0 1 0 479373611 167788544 38517 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38517 603 41 0 40923 0
vsize: 163856
[startup+820.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39989 0 3 0 81878 135 0 0 25 0 1 0 479373611 167788544 38517 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38517 603 41 0 40923 0
vsize: 163856
[startup+830.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39989 0 3 0 82878 135 0 0 25 0 1 0 479373611 167788544 38517 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38517 603 41 0 40923 0
vsize: 163856
[startup+840.061 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39989 0 3 0 83878 135 0 0 25 0 1 0 479373611 167788544 38517 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38517 603 41 0 40923 0
vsize: 163856
[startup+850.061 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39989 0 3 0 84878 135 0 0 25 0 1 0 479373611 167788544 38517 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38517 603 41 0 40923 0
vsize: 163856
[startup+860.062 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39990 0 3 0 85878 136 0 0 25 0 1 0 479373611 167788544 38518 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38518 603 41 0 40923 0
vsize: 163856
[startup+870.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39990 0 3 0 86878 136 0 0 25 0 1 0 479373611 167788544 38518 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38518 603 41 0 40923 0
vsize: 163856
[startup+880.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39990 0 3 0 87879 136 0 0 25 0 1 0 479373611 167788544 38518 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38518 603 41 0 40923 0
vsize: 163856
[startup+890.064 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39990 0 3 0 88879 136 0 0 25 0 1 0 479373611 167788544 38518 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38518 603 41 0 40923 0
vsize: 163856
[startup+900.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39990 0 3 0 89879 136 0 0 25 0 1 0 479373611 167788544 38518 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38518 603 41 0 40923 0
vsize: 163856
[startup+910.065 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39990 0 3 0 90879 136 0 0 25 0 1 0 479373611 167788544 38518 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38518 603 41 0 40923 0
vsize: 163856
[startup+920.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 91879 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+930.065 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 92878 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+940.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 93878 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223748 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+950.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 94878 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+960.067 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 95878 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+970.067 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 96878 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223748 134566082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+980.068 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 97879 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+990.069 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 98879 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 99879 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24063
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 100879 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 101879 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 102879 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 103880 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 104880 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 105880 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 106880 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 107880 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 108881 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 109881 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 110881 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 111881 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 112881 136 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 113881 137 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 114881 137 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 115881 137 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 116882 137 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223544 1075351254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 117882 137 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1190.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 118882 137 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 24065
Raw data (stat): 24000 (minisat+) R 23999 20024 20023 0 -1 0 39992 0 3 0 119882 137 0 0 25 0 1 0 479373611 167788544 38520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40964 38520 603 41 0 40923 0
vsize: 163856
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.00 0.97 0.91 1/55 24065
Raw data (stat): 24000 (minisat+) Z 23999 20024 20023 0 -1 12 39995 0 3 0 119883 144 0 0 25 0 1 0 479373611 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.16
CPU time (s): 1200.28
CPU user time (s): 1198.83
CPU system time (s): 1.44578
CPU usage (%): 100.01
Max. virtual memory (Kb): 163856
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####