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/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-aflow30a.opb
MD5SUM	b74fb9cd57e8b4068255c4ac98aa23ca
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3191
Optimality of the best value was proved	NO
Number of terms in the objective function	421
Biggest coefficient in the objective function	500
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	72290
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	12800
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	416734
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.12
Number of variables	5932
Total number of constraints	1321
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	450
Number of constraints which are nor clauses,nor cardinality constraints	871
Minimum length of a constraint	1
Maximum length of a constraint	453
Trace number 18865

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 16:49:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17407 boxname=wulflinc10 idbench=1339 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b74fb9cd57e8b4068255c4ac98aa23ca  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-aflow30a.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-aflow30a.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-aflow30a.opb
IDLAUNCH: 17407
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        536796 kB
Buffers:         18256 kB
Cached:         458084 kB
SwapCached:          0 kB
Active:         270460 kB
Inactive:       208364 kB
HighTotal:      131008 kB
HighFree:        10136 kB
LowTotal:       903652 kB
LowFree:        526660 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13604 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:09:10 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 17407 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 958 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1020]---> BDD-cost:   13
c ---[1019]---> BDD-cost:   11
c ---[1018]---> BDD-cost:   11
c ---[1017]---> BDD-cost:   12
c ---[1016]---> BDD-cost:   13
c ---[1015]---> BDD-cost:   12
c ---[1014]---> BDD-cost:   13
c ---[1013]---> BDD-cost:   12
c ---[1012]---> BDD-cost:   13
c ---[1011]---> BDD-cost:   11
c ---[1010]---> BDD-cost:   13
c ---[1009]---> BDD-cost:   13
c ---[1008]---> BDD-cost:   12
c ---[1007]---> BDD-cost:   11
c ---[1006]---> BDD-cost:   12
c ---[1005]---> BDD-cost:   13
c ---[1004]---> BDD-cost:   13
c ---[1002]---> BDD-cost:   13
c ---[1001]---> BDD-cost:   13
c ---[1000]---> BDD-cost:   12
c ---[ 999]---> BDD-cost:   13
c ---[ 998]---> BDD-cost:   13
c ---[ 996]---> BDD-cost:   13
c ---[ 995]---> BDD-cost:   12
c ---[ 993]---> BDD-cost:   12
c ---[ 992]---> BDD-cost:   13
c ---[ 991]---> BDD-cost:   12
c ---[ 990]---> BDD-cost:   13
c ---[ 989]---> BDD-cost:   12
c ---[ 988]---> BDD-cost:   12
c ---[ 987]---> BDD-cost:   13
c ---[ 986]---> BDD-cost:   13
c ---[ 985]---> BDD-cost:   12
c ---[ 984]---> BDD-cost:   13
c ---[ 981]---> BDD-cost:   13
c ---[ 980]---> BDD-cost:   11
c ---[ 978]---> BDD-cost:   13
c ---[ 977]---> BDD-cost:   12
c ---[ 974]---> BDD-cost:   10
c ---[ 973]---> BDD-cost:   12
c ---[ 972]---> BDD-cost:   11
c ---[ 971]---> BDD-cost:   13
c ---[ 970]---> BDD-cost:   10
c ---[ 969]---> BDD-cost:   13
c ---[ 968]---> BDD-cost:   13
c ---[ 967]---> BDD-cost:   13
c ---[ 966]---> BDD-cost:   12
c ---[ 964]---> BDD-cost:   13
c ---[ 963]---> BDD-cost:   13
c ---[ 962]---> BDD-cost:   12
c ---[ 961]---> BDD-cost:   10
c ---[ 960]---> BDD-cost:   13
c ---[ 959]---> BDD-cost:   10
c ---[ 958]---> BDD-cost:   13
c ---[ 956]---> BDD-cost:   12
c ---[ 955]---> BDD-cost:   13
c ---[ 954]---> BDD-cost:   11
c ---[ 953]---> BDD-cost:   13
c ---[ 952]---> BDD-cost:   13
c ---[ 951]---> BDD-cost:   11
c ---[ 950]---> BDD-cost:   13
c ---[ 949]---> BDD-cost:   13
c ---[ 948]---> BDD-cost:   13
c ---[ 947]---> BDD-cost:   13
c ---[ 946]---> BDD-cost:   13
c ---[ 945]---> BDD-cost:   13
c ---[ 944]---> BDD-cost:   12
c ---[ 943]---> BDD-cost:   13
c ---[ 942]---> BDD-cost:   13
c ---[ 941]---> BDD-cost:   11
c ---[ 940]---> BDD-cost:   13
c ---[ 939]---> BDD-cost:   13
c ---[ 937]---> BDD-cost:   13
c ---[ 936]---> BDD-cost:   12
c ---[ 935]---> BDD-cost:   10
c ---[ 934]---> BDD-cost:   13
c ---[ 933]---> BDD-cost:   10
c ---[ 932]---> BDD-cost:   12
c ---[ 931]---> BDD-cost:   12
c ---[ 930]---> BDD-cost:   13
c ---[ 928]---> BDD-cost:   11
c ---[ 927]---> BDD-cost:   13
c ---[ 926]---> BDD-cost:   13
c ---[ 925]---> BDD-cost:   13
c ---[ 924]---> BDD-cost:   13
c ---[ 923]---> BDD-cost:   11
c ---[ 922]---> BDD-cost:   12
c ---[ 921]---> BDD-cost:   12
c ---[ 919]---> BDD-cost:   12
c ---[ 918]---> BDD-cost:   12
c ---[ 917]---> BDD-cost:   13
c ---[ 916]---> BDD-cost:   10
c ---[ 915]---> BDD-cost:   12
c ---[ 914]---> BDD-cost:   13
c ---[ 913]---> BDD-cost:   13
c ---[ 912]---> BDD-cost:   13
c ---[ 911]---> BDD-cost:   13
c ---[ 910]---> BDD-cost:   12
c ---[ 908]---> BDD-cost:   13
c ---[ 907]---> BDD-cost:   13
c ---[ 906]---> BDD-cost:   12
c ---[ 905]---> BDD-cost:   13
c ---[ 903]---> BDD-cost:   13
c ---[ 902]---> BDD-cost:   13
c ---[ 900]---> BDD-cost:   13
c ---[ 899]---> BDD-cost:   10
c ---[ 898]---> BDD-cost:   12
c ---[ 897]---> BDD-cost:   12
c ---[ 896]---> BDD-cost:   12
c ---[ 895]---> BDD-cost:   13
c ---[ 893]---> BDD-cost:   12
c ---[ 892]---> BDD-cost:   13
c ---[ 891]---> BDD-cost:   11
c ---[ 890]---> BDD-cost:   13
c ---[ 889]---> BDD-cost:   13
c ---[ 888]---> BDD-cost:   13
c ---[ 887]---> BDD-cost:   13
c ---[ 886]---> BDD-cost:   11
c ---[ 885]---> BDD-cost:   13
c ---[ 883]---> BDD-cost:   10
c ---[ 882]---> BDD-cost:   11
c ---[ 881]---> BDD-cost:   13
c ---[ 880]---> BDD-cost:   13
c ---[ 879]---> BDD-cost:   13
c ---[ 878]---> BDD-cost:   12
c ---[ 877]---> BDD-cost:   11
c ---[ 876]---> BDD-cost:   10
c ---[ 875]---> BDD-cost:   13
c ---[ 874]---> BDD-cost:   13
c ---[ 873]---> BDD-cost:   11
c ---[ 871]---> BDD-cost:   12
c ---[ 870]---> BDD-cost:   13
c ---[ 869]---> BDD-cost:   12
c ---[ 867]---> BDD-cost:   11
c ---[ 866]---> BDD-cost:   13
c ---[ 865]---> BDD-cost:   13
c ---[ 863]---> BDD-cost:   13
c ---[ 862]---> BDD-cost:   13
c ---[ 861]---> BDD-cost:   12
c ---[ 860]---> BDD-cost:   13
c ---[ 859]---> BDD-cost:   12
c ---[ 858]---> BDD-cost:   13
c ---[ 857]---> BDD-cost:   12
c ---[ 856]---> BDD-cost:   13
c ---[ 855]---> BDD-cost:   12
c ---[ 853]---> BDD-cost:   13
c ---[ 851]---> BDD-cost:   13
c ---[ 850]---> BDD-cost:   12
c ---[ 849]---> BDD-cost:   11
c ---[ 848]---> BDD-cost:   12
c ---[ 847]---> BDD-cost:   13
c ---[ 846]---> BDD-cost:   12
c ---[ 845]---> BDD-cost:   13
c ---[ 844]---> BDD-cost:   12
c ---[ 843]---> BDD-cost:   12
c ---[ 842]---> BDD-cost:   11
c ---[ 841]---> BDD-cost:   11
c ---[ 840]---> BDD-cost:   10
c ---[ 839]---> BDD-cost:   13
c ---[ 837]---> BDD-cost:   10
c ---[ 836]---> BDD-cost:   12
c ---[ 835]---> BDD-cost:   13
c ---[ 834]---> BDD-cost:   13
c ---[ 833]---> BDD-cost:   13
c ---[ 832]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:   13
c ---[ 829]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   12
c ---[ 825]---> BDD-cost:   11
c ---[ 824]---> BDD-cost:   13
c ---[ 823]---> BDD-cost:   13
c ---[ 822]---> BDD-cost:   12
c ---[ 821]---> BDD-cost:   13
c ---[ 820]---> BDD-cost:   13
c ---[ 819]---> BDD-cost:   13
c ---[ 818]---> BDD-cost:   13
c ---[ 817]---> BDD-cost:   13
c ---[ 816]---> BDD-cost:   13
c ---[ 815]---> BDD-cost:   13
c ---[ 814]---> BDD-cost:   10
c ---[ 812]---> BDD-cost:   13
c ---[ 811]---> BDD-cost:   11
c ---[ 809]---> BDD-cost:   12
c ---[ 808]---> BDD-cost:   12
c ---[ 807]---> BDD-cost:   13
c ---[ 806]---> BDD-cost:   13
c ---[ 805]---> BDD-cost:   12
c ---[ 804]---> BDD-cost:   12
c ---[ 803]---> BDD-cost:   13
c ---[ 801]---> BDD-cost:   13
c ---[ 800]---> BDD-cost:   13
c ---[ 799]---> BDD-cost:   11
c ---[ 798]---> BDD-cost:   12
c ---[ 797]---> BDD-cost:   13
c ---[ 796]---> BDD-cost:   11
c ---[ 795]---> BDD-cost:   13
c ---[ 793]---> BDD-cost:   12
c ---[ 791]---> BDD-cost:   13
c ---[ 790]---> BDD-cost:   12
c ---[ 789]---> BDD-cost:   11
c ---[ 788]---> BDD-cost:   13
c ---[ 787]---> BDD-cost:   13
c ---[ 786]---> BDD-cost:   13
c ---[ 785]---> BDD-cost:   13
c ---[ 784]---> BDD-cost:   11
c ---[ 782]---> BDD-cost:   10
c ---[ 781]---> BDD-cost:   13
c ---[ 780]---> BDD-cost:   11
c ---[ 779]---> BDD-cost:   13
c ---[ 778]---> BDD-cost:   13
c ---[ 777]---> BDD-cost:   11
c ---[ 776]---> BDD-cost:   11
c ---[ 774]---> BDD-cost:   13
c ---[ 772]---> BDD-cost:   12
c ---[ 771]---> BDD-cost:   13
c ---[ 770]---> BDD-cost:   13
c ---[ 769]---> BDD-cost:   13
c ---[ 768]---> BDD-cost:   13
c ---[ 767]---> BDD-cost:   11
c ---[ 766]---> BDD-cost:   13
c ---[ 764]---> BDD-cost:   13
c ---[ 763]---> BDD-cost:   10
c ---[ 762]---> BDD-cost:   13
c ---[ 761]---> BDD-cost:   13
c ---[ 760]---> BDD-cost:   13
c ---[ 759]---> BDD-cost:   12
c ---[ 758]---> BDD-cost:   12
c ---[ 757]---> BDD-cost:   11
c ---[ 756]---> BDD-cost:   12
c ---[ 754]---> BDD-cost:   10
c ---[ 753]---> BDD-cost:   13
c ---[ 752]---> BDD-cost:   13
c ---[ 751]---> BDD-cost:   10
c ---[ 750]---> BDD-cost:   12
c ---[ 749]---> BDD-cost:   13
c ---[ 747]---> BDD-cost:   12
c ---[ 746]---> BDD-cost:   12
c ---[ 745]---> BDD-cost:   12
c ---[ 744]---> BDD-cost:   11
c ---[ 743]---> BDD-cost:   12
c ---[ 742]---> BDD-cost:   13
c ---[ 741]---> BDD-cost:   11
c ---[ 740]---> BDD-cost:   12
c ---[ 738]---> BDD-cost:   12
c ---[ 737]---> BDD-cost:   12
c ---[ 736]---> BDD-cost:   12
c ---[ 734]---> BDD-cost:   11
c ---[ 733]---> BDD-cost:   12
c ---[ 732]---> BDD-cost:   11
c ---[ 730]---> BDD-cost:   12
c ---[ 729]---> BDD-cost:   10
c ---[ 728]---> BDD-cost:   12
c ---[ 727]---> BDD-cost:   12
c ---[ 726]---> BDD-cost:   12
c ---[ 725]---> BDD-cost:   11
c ---[ 723]---> BDD-cost:   13
c ---[ 722]---> BDD-cost:   12
c ---[ 721]---> BDD-cost:   13
c ---[ 720]---> BDD-cost:   13
c ---[ 719]---> BDD-cost:   10
c ---[ 718]---> BDD-cost:   13
c ---[ 717]---> BDD-cost:   12
c ---[ 716]---> BDD-cost:   11
c ---[ 713]---> BDD-cost:   12
c ---[ 712]---> BDD-cost:   11
c ---[ 711]---> BDD-cost:   12
c ---[ 710]---> BDD-cost:   12
c ---[ 708]---> BDD-cost:   13
c ---[ 706]---> BDD-cost:   13
c ---[ 705]---> BDD-cost:   13
c ---[ 704]---> BDD-cost:   10
c ---[ 703]---> BDD-cost:   13
c ---[ 702]---> BDD-cost:   13
c ---[ 701]---> BDD-cost:   13
c ---[ 700]---> BDD-cost:   13
c ---[ 699]---> BDD-cost:   12
c ---[ 698]---> BDD-cost:   13
c ---[ 695]---> BDD-cost:   11
c ---[ 694]---> BDD-cost:   12
c ---[ 693]---> BDD-cost:   13
c ---[ 692]---> BDD-cost:   13
c ---[ 691]---> BDD-cost:   13
c ---[ 690]---> BDD-cost:   12
c ---[ 688]---> BDD-cost:   12
c ---[ 687]---> BDD-cost:   11
c ---[ 686]---> BDD-cost:   13
c ---[ 684]---> BDD-cost:   13
c ---[ 683]---> BDD-cost:   11
c ---[ 682]---> BDD-cost:   11
c ---[ 681]---> BDD-cost:   13
c ---[ 680]---> BDD-cost:   13
c ---[ 679]---> BDD-cost:   12
c ---[ 678]---> BDD-cost:   12
c ---[ 677]---> BDD-cost:   12
c ---[ 676]---> BDD-cost:   13
c ---[ 675]---> BDD-cost:   12
c ---[ 673]---> BDD-cost:   11
c ---[ 672]---> BDD-cost:   13
c ---[ 671]---> BDD-cost:   13
c ---[ 670]---> BDD-cost:   13
c ---[ 668]---> BDD-cost:   13
c ---[ 667]---> BDD-cost:   13
c ---[ 666]---> BDD-cost:   11
c ---[ 665]---> BDD-cost:   12
c ---[ 664]---> BDD-cost:   12
c ---[ 663]---> BDD-cost:   13
c ---[ 662]---> BDD-cost:   13
c ---[ 661]---> BDD-cost:   12
c ---[ 660]---> BDD-cost:   11
c ---[ 659]---> BDD-cost:   13
c ---[ 658]---> BDD-cost:   13
c ---[ 657]---> BDD-cost:   12
c ---[ 656]---> BDD-cost:   13
c ---[ 655]---> BDD-cost:   12
c ---[ 654]---> BDD-cost:   10
c ---[ 653]---> BDD-cost:   10
c ---[ 651]---> BDD-cost:   12
c ---[ 649]---> BDD-cost:   12
c ---[ 648]---> BDD-cost:   12
c ---[ 647]---> BDD-cost:   13
c ---[ 645]---> BDD-cost:   13
c ---[ 644]---> BDD-cost:   10
c ---[ 643]---> BDD-cost:   13
c ---[ 642]---> BDD-cost:   13
c ---[ 640]---> BDD-cost:   12
c ---[ 638]---> BDD-cost:   13
c ---[ 637]---> BDD-cost:   12
c ---[ 636]---> BDD-cost:   13
c ---[ 635]---> BDD-cost:   12
c ---[ 634]---> BDD-cost:   11
c ---[ 633]---> BDD-cost:   12
c ---[ 632]---> BDD-cost:   13
c ---[ 631]---> BDD-cost:   12
c ---[ 630]---> BDD-cost:   13
c ---[ 628]---> BDD-cost:   12
c ---[ 627]---> BDD-cost:   13
c ---[ 625]---> BDD-cost:   13
c ---[ 624]---> BDD-cost:   13
c ---[ 623]---> BDD-cost:   12
c ---[ 622]---> BDD-cost:   12
c ---[ 621]---> BDD-cost:   10
c ---[ 620]---> BDD-cost:   12
c ---[ 619]---> BDD-cost:   13
c ---[ 618]---> BDD-cost:   11
c ---[ 617]---> BDD-cost:   11
c ---[ 616]---> BDD-cost:   13
c ---[ 615]---> BDD-cost:   13
c ---[ 614]---> BDD-cost:   10
c ---[ 613]---> BDD-cost:   12
c ---[ 608]---> BDD-cost:   12
c ---[ 607]---> BDD-cost:   13
c ---[ 606]---> BDD-cost:   11
c ---[ 605]---> BDD-cost:   13
c ---[ 604]---> BDD-cost:   11
c ---[ 603]---> BDD-cost:   13
c ---[ 602]---> BDD-cost:   13
c ---[ 601]---> BDD-cost:   13
c ---[ 600]---> BDD-cost:   10
c ---[ 598]---> BDD-cost:   17
c ---[ 596]---> BDD-cost:   25
c ---[ 595]---> BDD-cost:    8
c ---[ 594]---> BDD-cost:    4
c ---[ 593]---> BDD-cost:    8
c ---[ 592]---> BDD-cost:    8
c ---[ 591]---> BDD-cost:    6
c ---[ 590]---> BDD-cost:    8
c ---[ 589]---> BDD-cost:    8
c ---[ 588]---> BDD-cost:    8
c ---[ 587]---> BDD-cost:    5
c ---[ 586]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:   27
c ---[ 583]---> BDD-cost:    8
c ---[ 582]---> BDD-cost:    7
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:    8
c ---[ 579]---> BDD-cost:    6
c ---[ 578]---> BDD-cost:    6
c ---[ 577]---> BDD-cost:    6
c ---[ 576]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    8
c ---[ 572]---> BDD-cost:   29
c ---[ 571]---> BDD-cost:    8
c ---[ 570]---> BDD-cost:    5
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:    6
c ---[ 567]---> BDD-cost:   18
c ---[ 566]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 564]---> BDD-cost:    7
c ---[ 563]---> BDD-cost:    5
c ---[ 562]---> BDD-cost:    7
c ---[ 560]---> BDD-cost:   27
c ---[ 559]---> BDD-cost:    8
c ---[ 558]---> BDD-cost:    8
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    6
c ---[ 554]---> BDD-cost:    5
c ---[ 553]---> BDD-cost:   15
c ---[ 552]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    8
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   17
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    6
c ---[ 543]---> BDD-cost:    3
c ---[ 542]---> BDD-cost:    6
c ---[ 541]---> BDD-cost:    8
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    5
c ---[ 538]---> BDD-cost:    8
c ---[ 536]---> BDD-cost:   23
c ---[ 535]---> BDD-cost:   16
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:   15
c ---[ 532]---> BDD-cost:    8
c ---[ 531]---> BDD-cost:    6
c ---[ 530]---> BDD-cost:   15
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:   17
c ---[ 524]---> BDD-cost:   27
c ---[ 523]---> BDD-cost:    5
c ---[ 522]---> BDD-cost:    8
c ---[ 521]---> BDD-cost:    6
c ---[ 520]---> BDD-cost:    8
c ---[ 519]---> BDD-cost:    8
c ---[ 518]---> BDD-cost:    7
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    3
c ---[ 515]---> BDD-cost:    6
c ---[ 514]---> BDD-cost:    7
c ---[ 512]---> BDD-cost:   23
c ---[ 511]---> BDD-cost:    5
c ---[ 510]---> BDD-cost:    5
c ---[ 509]---> BDD-cost:    7
c ---[ 508]---> BDD-cost:    7
c ---[ 507]---> BDD-cost:    6
c ---[ 506]---> BDD-cost:    5
c ---[ 505]---> BDD-cost:    6
c ---[ 504]---> BDD-cost:    6
c ---[ 503]---> BDD-cost:    7
c ---[ 502]---> BDD-cost:    4
c ---[ 500]---> BDD-cost:   31
c ---[ 499]---> BDD-cost:    7
c ---[ 498]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:   18
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:    5
c ---[ 494]---> BDD-cost:   15
c ---[ 493]---> BDD-cost:   18
c ---[ 492]---> BDD-cost:    6
c ---[ 491]---> BDD-cost:    6
c ---[ 490]---> BDD-cost:    8
c ---[ 488]---> BDD-cost:   25
c ---[ 487]---> BDD-cost:    7
c ---[ 486]---> BDD-cost:    8
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    8
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    5
c ---[ 480]---> BDD-cost:    8
c ---[ 479]---> BDD-cost:   16
c ---[ 478]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:   23
c ---[ 474]---> BDD-cost:   33
c ---[ 473]---> BDD-cost:    3
c ---[ 472]---> BDD-cost:    4
c ---[ 471]---> BDD-cost:    6
c ---[ 470]---> BDD-cost:    6
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    6
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 464]---> BDD-cost:    8
c ---[ 462]---> BDD-cost:   19
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    8
c ---[ 458]---> BDD-cost:    3
c ---[ 457]---> BDD-cost:   18
c ---[ 456]---> BDD-cost:    4
c ---[ 455]---> BDD-cost:    4
c ---[ 454]---> BDD-cost:    6
c ---[ 453]---> BDD-cost:    4
c ---[ 452]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:   27
c ---[ 449]---> BDD-cost:    3
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    6
c ---[ 445]---> BDD-cost:   17
c ---[ 444]---> BDD-cost:    7
c ---[ 443]---> BDD-cost:    3
c ---[ 442]---> BDD-cost:    8
c ---[ 441]---> BDD-cost:    8
c ---[ 440]---> BDD-cost:    8
c ---[ 438]---> BDD-cost:   35
c ---[ 437]---> BDD-cost:   16
c ---[ 436]---> BDD-cost:    8
c ---[ 435]---> BDD-cost:    6
c ---[ 434]---> BDD-cost:    8
c ---[ 433]---> BDD-cost:    8
c ---[ 432]---> BDD-cost:    8
c ---[ 431]---> BDD-cost:    8
c ---[ 430]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    7
c ---[ 428]---> BDD-cost:    8
c ---[ 426]---> BDD-cost:   27
c ---[ 425]---> BDD-cost:   17
c ---[ 424]---> BDD-cost:    7
c ---[ 423]---> BDD-cost:    5
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 420]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    7
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:   17
c ---[ 414]---> BDD-cost:   19
c ---[ 413]---> BDD-cost:    7
c ---[ 412]---> BDD-cost:    6
c ---[ 411]---> BDD-cost:    7
c ---[ 410]---> BDD-cost:    6
c ---[ 409]---> BDD-cost:   17
c ---[ 408]---> BDD-cost:    6
c ---[ 407]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:    5
c ---[ 405]---> BDD-cost:    7
c ---[ 404]---> BDD-cost:    6
c ---[ 402]---> BDD-cost:   31
c ---[ 401]---> BDD-cost:    7
c ---[ 400]---> BDD-cost:    7
c ---[ 399]---> BDD-cost:    8
c ---[ 398]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    5
c ---[ 394]---> BDD-cost:    7
c ---[ 393]---> BDD-cost:    4
c ---[ 392]---> BDD-cost:    6
c ---[ 390]---> BDD-cost:   25
c ---[ 389]---> BDD-cost:   17
c ---[ 388]---> BDD-cost:   17
c ---[ 387]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    3
c ---[ 385]---> BDD-cost:    5
c ---[ 384]---> BDD-cost:    6
c ---[ 383]---> BDD-cost:    7
c ---[ 382]---> BDD-cost:   16
c ---[ 381]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:    6
c ---[ 376]---> BDD-cost:    6
c ---[ 375]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    8
c ---[ 373]---> BDD-cost:    6
c ---[ 372]---> BDD-cost:    5
c ---[ 371]---> BDD-cost:    5
c ---[ 370]---> BDD-cost:    8
c ---[ 369]---> BDD-cost:    8
c ---[ 368]---> BDD-cost:    5
c ---[ 366]---> BDD-cost:   33
c ---[ 365]---> BDD-cost:    3
c ---[ 364]---> BDD-cost:    6
c ---[ 363]---> BDD-cost:    5
c ---[ 362]---> BDD-cost:    6
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   16
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    8
c ---[ 356]---> BDD-cost:   14
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> Adder-cost: 693   maxlim: 102262   bits: 18/17
c ---[ 351]---> BDD-cost:    8
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    4
c ---[ 348]---> BDD-cost:   19
c ---[ 347]---> BDD-cost:   15
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:   17
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:   14
c ---[ 342]---> BDD-cost:    6
c ---[ 340]---> Adder-cost: 572   maxlim: 148723   bits: 18/18
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    8
c ---[ 336]---> BDD-cost:   17
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    8
c ---[ 333]---> BDD-cost:   19
c ---[ 332]---> BDD-cost:   16
c ---[ 331]---> BDD-cost:   19
c ---[ 330]---> BDD-cost:    3
c ---[ 328]---> Adder-cost: 880   maxlim: 181231   bits: 19/18
c ---[ 327]---> BDD-cost:    5
c ---[ 326]---> BDD-cost:    7
c ---[ 325]---> BDD-cost:    3
c ---[ 324]---> BDD-cost:    6
c ---[ 323]---> BDD-cost:    5
c ---[ 322]---> BDD-cost:    6
c ---[ 321]---> BDD-cost:    3
c ---[ 320]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    3
c ---[ 318]---> BDD-cost:    6
c ---[ 316]---> Adder-cost: 820   maxlim: 146161   bits: 19/18
c ---[ 315]---> BDD-cost:    4
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:   16
c ---[ 312]---> BDD-cost:   16
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    8
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    4
c ---[ 307]---> BDD-cost:    5
c ---[ 306]---> BDD-cost:   19
c ---[ 304]---> Adder-cost: 838   maxlim: 185456   bits: 19/18
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:   19
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 298]---> BDD-cost:   14
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    5
c ---[ 292]---> Adder-cost: 546   maxlim: 93302   bits: 18/17
c ---[ 291]---> BDD-cost:    5
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    8
c ---[ 288]---> BDD-cost:    8
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    8
c ---[ 280]---> Adder-cost: 720   maxlim: 163185   bits: 19/18
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    8
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    4
c ---[ 275]---> BDD-cost:   15
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    7
c ---[ 270]---> BDD-cost:    6
c ---[ 268]---> Adder-cost: 768   maxlim: 162802   bits: 19/18
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:   17
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    8
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:   19
c ---[ 259]---> BDD-cost:   19
c ---[ 258]---> BDD-cost:    6
c ---[ 256]---> Adder-cost: 800   maxlim: 202094   bits: 19/18
c ---[ 255]---> BDD-cost:    5
c ---[ 254]---> BDD-cost:    5
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:   14
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    5
c ---[ 249]---> BDD-cost:    7
c ---[ 248]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:    7
c ---[ 244]---> Adder-cost: 670   maxlim: 163442   bits: 19/18
c ---[ 243]---> BDD-cost:    7
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:    6
c ---[ 240]---> BDD-cost:    7
c ---[ 239]---> BDD-cost:    5
c ---[ 238]---> BDD-cost:    7
c ---[ 237]---> BDD-cost:    3
c ---[ 236]---> BDD-cost:    4
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:   19
c ---[ 232]---> BDD-cost:   27
c ---[ 230]---> Adder-cost: 706   maxlim: 157169   bits: 19/18
c ---[ 229]---> BDD-cost:    5
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    4
c ---[ 225]---> BDD-cost:    5
c ---[ 224]---> BDD-cost:   19
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:   18
c ---[ 221]---> BDD-cost:    7
c ---[ 220]---> BDD-cost:    7
c ---[ 218]---> Adder-cost: 762   maxlim: 147056   bits: 19/18
c ---[ 217]---> BDD-cost:    5
c ---[ 216]---> BDD-cost:   17
c ---[ 215]---> BDD-cost:    6
c ---[ 214]---> BDD-cost:    8
c ---[ 213]---> BDD-cost:    5
c ---[ 212]---> BDD-cost:    7
c ---[ 211]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:    8
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    3
c ---[ 206]---> Adder-cost: 759   maxlim: 130929   bits: 18/17
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    7
c ---[ 203]---> BDD-cost:   15
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    6
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:   19
c ---[ 196]---> BDD-cost:    8
c ---[ 194]---> Adder-cost: 696   maxlim: 101365   bits: 18/17
c ---[ 193]---> BDD-cost:    8
c ---[ 192]---> BDD-cost:    6
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:    5
c ---[ 189]---> BDD-cost:    8
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    8
c ---[ 186]---> BDD-cost:   18
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    3
c ---[ 182]---> Adder-cost: 614   maxlim: 144627   bits: 19/18
c ---[ 181]---> BDD-cost:    6
c ---[ 180]---> BDD-cost:    5
c ---[ 179]---> BDD-cost:    6
c ---[ 178]---> BDD-cost:    7
c ---[ 177]---> BDD-cost:    3
c ---[ 176]---> BDD-cost:    4
c ---[ 175]---> BDD-cost:    7
c ---[ 174]---> BDD-cost:    8
c ---[ 173]---> BDD-cost:    3
c ---[ 172]---> BDD-cost:    6
c ---[ 170]---> Adder-cost: 764   maxlim: 174961   bits: 19/18
c ---[ 169]---> BDD-cost:    7
c ---[ 168]---> BDD-cost:   17
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    8
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    5
c ---[ 163]---> BDD-cost:    5
c ---[ 162]---> BDD-cost:    5
c ---[ 161]---> BDD-cost:    7
c ---[ 160]---> BDD-cost:   17
c ---[ 158]---> Adder-cost: 548   maxlim: 159603   bits: 18/18
c ---[ 157]---> BDD-cost:    8
c ---[ 156]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    5
c ---[ 154]---> BDD-cost:    7
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    4
c ---[ 149]---> BDD-cost:   19
c ---[ 148]---> BDD-cost:    8
c ---[ 146]---> Adder-cost: 824   maxlim: 173423   bits: 19/18
c ---[ 145]---> BDD-cost:    6
c ---[ 144]---> BDD-cost:    8
c ---[ 143]---> BDD-cost:    4
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    7
c ---[ 140]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:   17
c ---[ 138]---> BDD-cost:    7
c ---[ 137]---> BDD-cost:    6
c ---[ 136]---> BDD-cost:    8
c ---[ 134]---> Adder-cost: 858   maxlim: 137074   bits: 19/18
c ---[ 132]---> Adder-cost: 786   maxlim: 177902   bits: 19/18
c ---[ 130]---> BDD-cost:   29
c ---[ 128]---> Adder-cost: 602   maxlim: 120053   bits: 18/17
c ---[ 126]---> Adder-cost: 646   maxlim: 154865   bits: 18/18
c ---[ 124]---> Adder-cost: 864   maxlim: 214125   bits: 19/18
c ---[ 122]---> Adder-cost: 710   maxlim: 143089   bits: 19/18
c ---[ 120]---> Adder-cost: 614   maxlim: 83701   bits: 18/17
c ---[ 118]---> Adder-cost: 706   maxlim: 144239   bits: 19/18
c ---[ 116]---> Adder-cost: 826   maxlim: 169330   bits: 19/18
c ---[ 114]---> Adder-cost: 604   maxlim: 130932   bits: 18/17
c ---[ 112]---> Adder-cost: 816   maxlim: 175726   bits: 19/18
c ---[ 111]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:    5
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:   17
c ---[ 105]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    5
c ---[ 103]---> BDD-cost:    6
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    7
c ---[  99]---> BDD-cost:    6
c ---[  97]---> BDD-cost:   27
c ---[  96]---> BDD-cost:    6
c ---[  95]---> BDD-cost:    7
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    7
c ---[  90]---> BDD-cost:    6
c ---[  89]---> BDD-cost:    3
c ---[  88]---> BDD-cost:    3
c ---[  87]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   25
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    6
c ---[  80]---> BDD-cost:    7
c ---[  79]---> BDD-cost:    7
c ---[  78]---> BDD-cost:   19
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    6
c ---[  75]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   33
c ---[  72]---> BDD-cost:    5
c ---[  71]---> BDD-cost:   16
c ---[  70]---> BDD-cost:    5
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:   16
c ---[  67]---> BDD-cost:   19
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    6
c ---[  63]---> BDD-cost:    4
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  158626   552551 |   52875       0        0     nan |  0.000 % |
c |       100 |  158608   552489 |   58162      94     1774    18.9 |  6.243 % |
c |       250 |  158591   552432 |   63978     241     2410    10.0 |  6.250 % |
c |       475 |  158574   552375 |   70376     460     3419     7.4 |  6.256 % |
c |       812 |  158539   552256 |   77414     790    37886    48.0 |  6.269 % |
c |      1319 |  158497   552116 |   85155    1290    51718    40.1 |  6.285 % |
c |      2078 |  158489   552090 |   93671    2048    88341    43.1 |  6.289 % |
c |      3217 |  158383   551728 |  103038    3159   153888    48.7 |  6.327 % |
c |      4925 |  158358   551645 |  113342    4862   309055    63.6 |  6.337 % |
c |      7490 |  158358   551645 |  124676    7427   669984    90.2 |  6.337 % |
c |     11334 |  158358   551645 |  137144   11271  1287901   114.3 |  6.337 % |
c |     17101 |  158255   551298 |  150858   17018  1972587   115.9 |  6.376 % |
c |     25750 |  158237   551236 |  165944   25662  3235698   126.1 |  6.382 % |
c |     38726 |  158228   551205 |  182538   38636  5716023   147.9 |  6.386 % |
c |     58189 |  158228   551205 |  200792   58099  9654403   166.2 |  6.386 % |
c |     87384 |  158213   551154 |  220871   87291 15372210   176.1 |  6.392 % |
c |    131173 |  158204   551123 |  242959  131078 24114781   184.0 |  6.395 % |
#### 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.85 0.97 0.93 2/54 2714
Raw data (stat): 2714 (runsolver) R 2713 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488432150 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 3743 0 0 0 988 10 0 0 25 0 1 0 488432150 17321984 3634 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4229 3634 603 41 0 4188 0
vsize: 16916
[startup+20.0001 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 3939 0 0 0 1986 11 0 0 25 0 1 0 488432150 18128896 3830 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4426 3830 603 41 0 4385 0
vsize: 17704
[startup+30 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 4340 0 0 0 2985 13 0 0 25 0 1 0 488432150 19746816 4231 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4821 4231 603 41 0 4780 0
vsize: 19284
[startup+40.0006 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 4810 0 0 0 3983 14 0 0 25 0 1 0 488432150 21622784 4701 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5279 4701 603 41 0 5238 0
vsize: 21116
[startup+50.0008 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 5172 0 0 0 4981 16 0 0 25 0 1 0 488432150 23097344 5063 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5639 5063 603 41 0 5598 0
vsize: 22556
[startup+60.0007 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 5517 0 0 0 5980 18 0 0 25 0 1 0 488432150 24559616 5408 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5996 5408 603 41 0 5955 0
vsize: 23984
[startup+70.0012 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 5999 0 0 0 6979 19 0 0 25 0 1 0 488432150 26619904 5890 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6499 5890 603 41 0 6458 0
vsize: 25996
[startup+80.0015 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 6199 0 0 0 7978 20 0 0 25 0 1 0 488432150 27422720 6090 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6695 6090 603 41 0 6654 0
vsize: 26780
[startup+90.0014 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 6375 0 0 0 8978 20 0 0 25 0 1 0 488432150 28094464 6266 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6859 6266 603 41 0 6818 0
vsize: 27436
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 6575 0 0 0 9978 20 0 0 25 0 1 0 488432150 28897280 6466 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7055 6466 603 41 0 7014 0
vsize: 28220
[startup+110 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 6796 0 0 0 10977 21 0 0 25 0 1 0 488432150 29831168 6687 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7283 6687 603 41 0 7242 0
vsize: 29132
[startup+120.001 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 7006 0 0 0 11977 22 0 0 25 0 1 0 488432150 30633984 6897 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7479 6897 603 41 0 7438 0
vsize: 29916
[startup+130.001 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 7279 0 0 0 12976 23 0 0 25 0 1 0 488432150 31838208 7170 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7773 7170 603 41 0 7732 0
vsize: 31092
[startup+140.001 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 7674 0 0 0 13975 24 0 0 25 0 1 0 488432150 33443840 7565 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8165 7565 603 41 0 8124 0
vsize: 32660
[startup+150.001 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 8216 0 0 0 14973 26 0 0 25 0 1 0 488432150 35598336 8107 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8691 8107 603 41 0 8650 0
vsize: 34764
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 8795 0 0 0 15972 28 0 0 25 0 1 0 488432150 38158336 8686 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9316 8686 603 41 0 9275 0
vsize: 37264
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 9344 0 0 0 16970 29 0 0 25 0 1 0 488432150 40300544 9235 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9839 9235 603 41 0 9798 0
vsize: 39356
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 9813 0 0 0 17969 31 0 0 25 0 1 0 488432150 42323968 9704 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10333 9704 603 41 0 10292 0
vsize: 41332
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 10200 0 0 0 18968 32 0 0 25 0 1 0 488432150 43798528 10091 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10693 10091 603 41 0 10652 0
vsize: 42772
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 10574 0 0 0 19967 33 0 0 25 0 1 0 488432150 45412352 10465 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11087 10465 603 41 0 11046 0
vsize: 44348
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 10957 0 0 0 20966 34 0 0 25 0 1 0 488432150 46886912 10848 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11447 10848 603 41 0 11406 0
vsize: 45788
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 11304 0 0 0 21966 35 0 0 25 0 1 0 488432150 48365568 11195 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11808 11195 603 41 0 11767 0
vsize: 47232
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 11657 0 0 0 22964 37 0 0 25 0 1 0 488432150 49844224 11548 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12169 11548 603 41 0 12128 0
vsize: 48676
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 12058 0 0 0 23963 38 0 0 25 0 1 0 488432150 51453952 11949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12562 11949 603 41 0 12521 0
vsize: 50248
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 12411 0 0 0 24963 38 0 0 25 0 1 0 488432150 52936704 12302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12924 12302 603 41 0 12883 0
vsize: 51696
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 12713 0 0 0 25962 39 0 0 25 0 1 0 488432150 54181888 12604 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13228 12604 603 41 0 13187 0
vsize: 52912
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 13041 0 0 0 26961 40 0 0 25 0 1 0 488432150 55525376 12932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13556 12932 603 41 0 13515 0
vsize: 54224
[startup+280 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 13379 0 0 0 27960 41 0 0 25 0 1 0 488432150 56868864 13270 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13884 13271 603 41 0 13843 0
vsize: 55536
[startup+290 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 13670 0 0 0 28959 42 0 0 25 0 1 0 488432150 58089472 13561 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14182 13561 603 41 0 14141 0
vsize: 56728
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 14003 0 0 0 29958 44 0 0 25 0 1 0 488432150 59482112 13894 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14522 13894 603 41 0 14481 0
vsize: 58088
[startup+310 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 14260 0 0 0 30957 45 0 0 25 0 1 0 488432150 60559360 14151 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14785 14151 603 41 0 14744 0
vsize: 59140
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 14559 0 0 0 31956 46 0 0 25 0 1 0 488432150 61763584 14450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15079 14450 603 41 0 15038 0
vsize: 60316
[startup+330 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 14863 0 0 0 32955 46 0 0 25 0 1 0 488432150 62984192 14754 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15377 14754 603 41 0 15336 0
vsize: 61508
[startup+340 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 15110 0 0 0 33955 47 0 0 25 0 1 0 488432150 64053248 15001 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15638 15001 603 41 0 15597 0
vsize: 62552
[startup+350 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 15348 0 0 0 34954 48 0 0 25 0 1 0 488432150 64991232 15239 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15867 15239 603 41 0 15826 0
vsize: 63468
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 15661 0 0 0 35953 49 0 0 25 0 1 0 488432150 66596864 15552 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16259 15552 603 41 0 16218 0
vsize: 65036
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 15908 0 0 0 36953 50 0 0 25 0 1 0 488432150 67592192 15799 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16502 15799 603 41 0 16461 0
vsize: 66008
[startup+380 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 16162 0 0 0 37952 50 0 0 25 0 1 0 488432150 68665344 16053 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16764 16053 603 41 0 16723 0
vsize: 67056
[startup+390 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 16415 0 0 0 38952 51 0 0 25 0 1 0 488432150 69742592 16306 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17027 16306 603 41 0 16986 0
vsize: 68108
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 16716 0 0 0 39951 52 0 0 25 0 1 0 488432150 70991872 16607 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17332 16607 603 41 0 17291 0
vsize: 69328
[startup+410 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 16965 0 0 0 40951 52 0 0 25 0 1 0 488432150 71950336 16856 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17566 16856 603 41 0 17525 0
vsize: 70264
[startup+420 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 17148 0 0 0 41951 53 0 0 25 0 1 0 488432150 72794112 17039 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17772 17039 603 41 0 17731 0
vsize: 71088
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 17286 0 0 0 42950 53 0 0 25 0 1 0 488432150 73330688 17177 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17903 17177 603 41 0 17862 0
vsize: 71612
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 17412 0 0 0 43950 53 0 0 25 0 1 0 488432150 73875456 17303 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18036 17303 603 41 0 17995 0
vsize: 72144
[startup+450.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 17565 0 0 0 44950 54 0 0 25 0 1 0 488432150 74547200 17456 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18200 17456 603 41 0 18159 0
vsize: 72800
[startup+460 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 17826 0 0 0 45949 55 0 0 25 0 1 0 488432150 75616256 17717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18461 17717 603 41 0 18420 0
vsize: 73844
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 18082 0 0 0 46949 56 0 0 25 0 1 0 488432150 76558336 17973 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18691 17973 603 41 0 18650 0
vsize: 74764
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 18258 0 0 0 47948 56 0 0 25 0 1 0 488432150 77357056 18149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18886 18149 603 41 0 18845 0
vsize: 75544
[startup+490.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 18484 0 0 0 48948 57 0 0 25 0 1 0 488432150 78303232 18375 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19117 18375 603 41 0 19076 0
vsize: 76468
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 18702 0 0 0 49948 57 0 0 25 0 1 0 488432150 79106048 18593 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19313 18593 603 41 0 19272 0
vsize: 77252
[startup+510.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 18914 0 0 0 50948 58 0 0 25 0 1 0 488432150 80039936 18805 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19541 18805 603 41 0 19500 0
vsize: 78164
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 19150 0 0 0 51947 58 0 0 25 0 1 0 488432150 80965632 19041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19767 19041 603 41 0 19726 0
vsize: 79068
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 19457 0 0 0 52946 60 0 0 25 0 1 0 488432150 82219008 19348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20073 19348 603 41 0 20032 0
vsize: 80292
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 19762 0 0 0 53946 60 0 0 25 0 1 0 488432150 83505152 19653 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20387 19653 603 41 0 20346 0
vsize: 81548
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 19945 0 0 0 54945 61 0 0 25 0 1 0 488432150 84312064 19836 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20584 19836 603 41 0 20543 0
vsize: 82336
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 20146 0 0 0 55945 61 0 0 25 0 1 0 488432150 85135360 20037 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20785 20037 603 41 0 20744 0
vsize: 83140
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 20355 0 0 0 56944 62 0 0 25 0 1 0 488432150 86102016 20246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21021 20246 603 41 0 20980 0
vsize: 84084
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 20594 0 0 0 57943 63 0 0 25 0 1 0 488432150 87097344 20485 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21264 20485 603 41 0 21223 0
vsize: 85056
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 20812 0 0 0 58942 64 0 0 25 0 1 0 488432150 88047616 20703 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21496 20703 603 41 0 21455 0
vsize: 85984
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 21116 0 0 0 59942 64 0 0 25 0 1 0 488432150 89243648 21007 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21788 21007 603 41 0 21747 0
vsize: 87152
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 21399 0 0 0 60941 65 0 0 25 0 1 0 488432150 90468352 21290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22087 21290 603 41 0 22046 0
vsize: 88348
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 21689 0 0 0 61940 66 0 0 25 0 1 0 488432150 91545600 21580 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22350 21580 603 41 0 22309 0
vsize: 89400
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 21984 0 0 0 62940 66 0 0 25 0 1 0 488432150 92753920 21875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22645 21875 603 41 0 22604 0
vsize: 90580
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 22257 0 0 0 63940 67 0 0 25 0 1 0 488432150 93962240 22148 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22940 22148 603 41 0 22899 0
vsize: 91760
[startup+650.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2714
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 22547 0 0 0 64940 67 0 0 25 0 1 0 488432150 95162368 22438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23233 22438 603 41 0 23192 0
vsize: 92932
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 2762
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 22808 0 0 0 65938 68 0 0 25 0 1 0 488432150 96235520 22699 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23495 22699 603 41 0 23454 0
vsize: 93980
[startup+670.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2767
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 23070 0 0 0 66937 69 0 0 25 0 1 0 488432150 97304576 22961 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23756 22961 603 41 0 23715 0
vsize: 95024
[startup+680.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2767
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 23321 0 0 0 67937 70 0 0 25 0 1 0 488432150 98246656 23212 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23986 23212 603 41 0 23945 0
vsize: 95944
[startup+690.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2767
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 23580 0 0 0 68936 70 0 0 25 0 1 0 488432150 99319808 23471 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24248 23472 603 41 0 24207 0
vsize: 96992
[startup+700.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2767
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 23823 0 0 0 69936 71 0 0 25 0 1 0 488432150 100413440 23714 4294967295 134512640 134672761 3221224544 3221223792 134562614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24515 23714 603 41 0 24474 0
vsize: 98060
[startup+710.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2767
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 24065 0 0 0 70935 72 0 0 25 0 1 0 488432150 101347328 23956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24743 23956 603 41 0 24702 0
vsize: 98972
[startup+720.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2767
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 24319 0 0 0 71934 73 0 0 25 0 1 0 488432150 102432768 24210 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25008 24210 603 41 0 24967 0
vsize: 100032
[startup+730.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 24541 0 0 0 72933 74 0 0 25 0 1 0 488432150 103243776 24432 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25206 24432 603 41 0 25165 0
vsize: 100824
[startup+740.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 24734 0 0 0 73933 75 0 0 25 0 1 0 488432150 104046592 24625 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25402 24625 603 41 0 25361 0
vsize: 101608
[startup+750.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 24946 0 0 0 74932 76 0 0 25 0 1 0 488432150 104988672 24837 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25632 24837 603 41 0 25591 0
vsize: 102528
[startup+760.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 25153 0 0 0 75930 77 0 0 25 0 1 0 488432150 105807872 25044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25832 25044 603 41 0 25791 0
vsize: 103328
[startup+770.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 25373 0 0 0 76929 78 0 0 25 0 1 0 488432150 106745856 25264 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26061 25264 603 41 0 26020 0
vsize: 104244
[startup+780.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 25594 0 0 0 77928 79 0 0 25 0 1 0 488432150 107573248 25485 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26263 25485 603 41 0 26222 0
vsize: 105052
[startup+790.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 25779 0 0 0 78928 80 0 0 25 0 1 0 488432150 108408832 25670 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26467 25670 603 41 0 26426 0
vsize: 105868
[startup+800.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 25948 0 0 0 79928 80 0 0 25 0 1 0 488432150 109142016 25839 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26646 25839 603 41 0 26605 0
vsize: 106584
[startup+810.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 26125 0 0 0 80927 81 0 0 25 0 1 0 488432150 109809664 26016 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26809 26016 603 41 0 26768 0
vsize: 107236
[startup+820.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 26344 0 0 0 81927 82 0 0 25 0 1 0 488432150 110743552 26235 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27037 26235 603 41 0 26996 0
vsize: 108148
[startup+830.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 26582 0 0 0 82926 82 0 0 25 0 1 0 488432150 111681536 26473 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27266 26473 603 41 0 27225 0
vsize: 109064
[startup+840 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 26791 0 0 0 83926 82 0 0 25 0 1 0 488432150 112615424 26682 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27494 26682 603 41 0 27453 0
vsize: 109976
[startup+850 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 27007 0 0 0 84925 83 0 0 25 0 1 0 488432150 113459200 26898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27700 26898 603 41 0 27659 0
vsize: 110800
[startup+860 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 27191 0 0 0 85925 84 0 0 25 0 1 0 488432150 114130944 27082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27864 27082 603 41 0 27823 0
vsize: 111456
[startup+869.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 27397 0 0 0 86924 85 0 0 25 0 1 0 488432150 115073024 27288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28094 27288 603 41 0 28053 0
vsize: 112376
[startup+879.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 27587 0 0 0 87924 85 0 0 25 0 1 0 488432150 115875840 27478 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28290 27478 603 41 0 28249 0
vsize: 113160
[startup+889.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 27755 0 0 0 88923 86 0 0 25 0 1 0 488432150 116473856 27646 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28436 27646 603 41 0 28395 0
vsize: 113744
[startup+899.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 27928 0 0 0 89923 87 0 0 25 0 1 0 488432150 117264384 27819 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28629 27819 603 41 0 28588 0
vsize: 114516
[startup+909.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 28099 0 0 0 90922 87 0 0 25 0 1 0 488432150 117936128 27990 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28793 27990 603 41 0 28752 0
vsize: 115172
[startup+919.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 28273 0 0 0 91922 88 0 0 25 0 1 0 488432150 118603776 28164 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28956 28164 603 41 0 28915 0
vsize: 115824
[startup+929.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 28465 0 0 0 92922 88 0 0 25 0 1 0 488432150 119431168 28356 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29158 28356 603 41 0 29117 0
vsize: 116632
[startup+939.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 28668 0 0 0 93921 89 0 0 25 0 1 0 488432150 120229888 28559 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29353 28559 603 41 0 29312 0
vsize: 117412
[startup+949.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 28869 0 0 0 94921 90 0 0 25 0 1 0 488432150 121126912 28760 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29572 28760 603 41 0 29531 0
vsize: 118288
[startup+959.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 29068 0 0 0 95921 90 0 0 25 0 1 0 488432150 121925632 28959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29767 28959 603 41 0 29726 0
vsize: 119068
[startup+969.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 29276 0 0 0 96920 91 0 0 25 0 1 0 488432150 122720256 29167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29961 29167 603 41 0 29920 0
vsize: 119844
[startup+979.997 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 29466 0 0 0 97920 91 0 0 25 0 1 0 488432150 123527168 29357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30158 29357 603 41 0 30117 0
vsize: 120632
[startup+989.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 29703 0 0 0 98919 92 0 0 25 0 1 0 488432150 125181952 29594 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30562 29594 603 41 0 30521 0
vsize: 122248
[startup+999.997 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2769
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 29882 0 0 0 99918 92 0 0 25 0 1 0 488432150 125902848 29773 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30738 29773 603 41 0 30697 0
vsize: 122952
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 30070 0 0 0 100918 93 0 0 25 0 1 0 488432150 126697472 29961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30932 29961 603 41 0 30891 0
vsize: 123728
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 30223 0 0 0 101917 93 0 0 25 0 1 0 488432150 127234048 30114 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31063 30114 603 41 0 31022 0
vsize: 124252
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 30381 0 0 0 102917 94 0 0 25 0 1 0 488432150 127901696 30272 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31226 30272 603 41 0 31185 0
vsize: 124904
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 30561 0 0 0 103916 95 0 0 25 0 1 0 488432150 128708608 30452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31423 30452 603 41 0 31382 0
vsize: 125692
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 30720 0 0 0 104916 95 0 0 25 0 1 0 488432150 129376256 30611 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31586 30611 603 41 0 31545 0
vsize: 126344
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 30871 0 0 0 105916 95 0 0 25 0 1 0 488432150 130076672 30762 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31757 30762 603 41 0 31716 0
vsize: 127028
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 31024 0 0 0 106916 95 0 0 25 0 1 0 488432150 130613248 30915 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31888 30915 603 41 0 31847 0
vsize: 127552
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 31211 0 0 0 107916 96 0 0 25 0 1 0 488432150 131416064 31102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32084 31102 603 41 0 32043 0
vsize: 128336
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 31387 0 0 0 108915 96 0 0 25 0 1 0 488432150 132079616 31278 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32246 31278 603 41 0 32205 0
vsize: 128984
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 31570 0 0 0 109915 97 0 0 25 0 1 0 488432150 132886528 31461 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32443 31461 603 41 0 32402 0
vsize: 129772
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 31732 0 0 0 110915 97 0 0 25 0 1 0 488432150 133570560 31623 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32610 31623 603 41 0 32569 0
vsize: 130440
[startup+1119.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 31879 0 0 0 111915 97 0 0 25 0 1 0 488432150 134103040 31770 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32740 31770 603 41 0 32699 0
vsize: 130960
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 32034 0 0 0 112915 98 0 0 25 0 1 0 488432150 134774784 31925 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32904 31925 603 41 0 32863 0
vsize: 131616
[startup+1139.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 32188 0 0 0 113915 98 0 0 25 0 1 0 488432150 135462912 32079 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33072 32079 603 41 0 33031 0
vsize: 132288
[startup+1149.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 32315 0 0 0 114915 98 0 0 25 0 1 0 488432150 135860224 32206 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33169 32206 603 41 0 33128 0
vsize: 132676
[startup+1159.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 32479 0 0 0 115914 99 0 0 25 0 1 0 488432150 136523776 32370 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33331 32370 603 41 0 33290 0
vsize: 133324
[startup+1169.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 32651 0 0 0 116914 99 0 0 25 0 1 0 488432150 137326592 32542 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33527 32542 603 41 0 33486 0
vsize: 134108
[startup+1179.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 32824 0 0 0 117914 100 0 0 25 0 1 0 488432150 137998336 32715 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33691 32715 603 41 0 33650 0
vsize: 134764
[startup+1189.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 32976 0 0 0 118913 100 0 0 25 0 1 0 488432150 138534912 32867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33822 32867 603 41 0 33781 0
vsize: 135288
[startup+1199.99 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 2771
Raw data (stat): 2714 (minisat+) R 2713 25347 25346 0 -1 0 33119 0 0 0 119913 101 0 0 25 0 1 0 488432150 139247616 33010 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33996 33010 603 41 0 33955 0
vsize: 135984
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 2771
Raw data (stat): 2714 (minisat+) Z 2713 25347 25346 0 -1 12 33121 0 0 0 119913 107 0 0 25 0 1 0 488432150 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: 0
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1199.14
CPU system time (s): 1.07184
CPU usage (%): 100.013
Max. virtual memory (Kb): 135984
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####