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-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-fit1d.opb
MD5SUM	de6e9dcd85d0fedc70e76c82543d6a33
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	11514
Biggest coefficient in the objective function	2949120
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	462466666
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	3870720
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	580921206
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.18
Number of variables	11514
Total number of constraints	1050
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1050
Minimum length of a constraint	11
Maximum length of a constraint	11514
Trace number 22960

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-22 04:09:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=10789 boxname=wulflinc27 idbench=830 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  de6e9dcd85d0fedc70e76c82543d6a33  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-fit1d.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-fit1d.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-fit1d.opb
IDLAUNCH: 10789
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        501344 kB
Buffers:         21968 kB
Cached:         488324 kB
SwapCached:        524 kB
Active:         146052 kB
Inactive:       366184 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        501092 kB
SwapTotal:     2097892 kB
SwapFree:      2096420 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5056 kB
Slab:            15496 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 04:22:53 (client local time) WITH STATUS 0 IN 809.975 SECONDS
stats: 10789 7 809.975 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1051 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): (none)
c ---[1050]---> BDD-cost:   10
c ---[1049]---> BDD-cost:   10
c ---[1048]---> BDD-cost:   10
c ---[1047]---> BDD-cost:   10
c ---[1046]---> BDD-cost:   10
c ---[1045]---> BDD-cost:   10
c ---[1044]---> BDD-cost:   10
c ---[1043]---> BDD-cost:   10
c ---[1042]---> BDD-cost:   10
c ---[1041]---> BDD-cost:   10
c ---[1040]---> BDD-cost:   10
c ---[1039]---> BDD-cost:   10
c ---[1038]---> BDD-cost:   10
c ---[1037]---> BDD-cost:   10
c ---[1036]---> BDD-cost:   10
c ---[1035]---> BDD-cost:   10
c ---[1034]---> BDD-cost:   10
c ---[1033]---> BDD-cost:   10
c ---[1032]---> BDD-cost:   10
c ---[1031]---> BDD-cost:   10
c ---[1030]---> BDD-cost:   10
c ---[1029]---> BDD-cost:   10
c ---[1028]---> BDD-cost:   10
c ---[1027]---> BDD-cost:   10
c ---[1026]---> BDD-cost:   10
c ---[1025]---> BDD-cost:   10
c ---[1024]---> BDD-cost:   10
c ---[1023]---> BDD-cost:   10
c ---[1022]---> BDD-cost:   10
c ---[1021]---> BDD-cost:   10
c ---[1020]---> BDD-cost:   10
c ---[1019]---> BDD-cost:   10
c ---[1018]---> BDD-cost:   10
c ---[1017]---> BDD-cost:   10
c ---[1016]---> BDD-cost:   10
c ---[1015]---> BDD-cost:   10
c ---[1014]---> BDD-cost:   10
c ---[1013]---> BDD-cost:   10
c ---[1012]---> BDD-cost:   10
c ---[1011]---> BDD-cost:   10
c ---[1010]---> BDD-cost:   10
c ---[1009]---> BDD-cost:   10
c ---[1008]---> BDD-cost:   10
c ---[1007]---> BDD-cost:   10
c ---[1006]---> BDD-cost:   10
c ---[1005]---> BDD-cost:   10
c ---[1004]---> BDD-cost:   10
c ---[1003]---> BDD-cost:   10
c ---[1002]---> BDD-cost:   10
c ---[1001]---> BDD-cost:   10
c ---[1000]---> BDD-cost:   10
c ---[ 999]---> BDD-cost:   10
c ---[ 998]---> BDD-cost:   10
c ---[ 997]---> BDD-cost:   10
c ---[ 996]---> BDD-cost:   10
c ---[ 995]---> BDD-cost:   10
c ---[ 994]---> BDD-cost:   10
c ---[ 993]---> BDD-cost:   10
c ---[ 992]---> BDD-cost:   10
c ---[ 991]---> BDD-cost:   10
c ---[ 990]---> BDD-cost:   10
c ---[ 989]---> BDD-cost:   10
c ---[ 988]---> BDD-cost:   10
c ---[ 987]---> BDD-cost:   10
c ---[ 986]---> BDD-cost:   10
c ---[ 985]---> BDD-cost:   10
c ---[ 984]---> BDD-cost:   10
c ---[ 983]---> BDD-cost:   10
c ---[ 982]---> BDD-cost:   10
c ---[ 981]---> BDD-cost:   10
c ---[ 980]---> BDD-cost:   10
c ---[ 979]---> BDD-cost:   10
c ---[ 978]---> BDD-cost:   10
c ---[ 977]---> BDD-cost:   10
c ---[ 976]---> BDD-cost:   10
c ---[ 975]---> BDD-cost:   10
c ---[ 974]---> BDD-cost:   10
c ---[ 973]---> BDD-cost:   10
c ---[ 972]---> BDD-cost:   10
c ---[ 971]---> BDD-cost:   10
c ---[ 970]---> BDD-cost:   10
c ---[ 969]---> BDD-cost:   10
c ---[ 968]---> BDD-cost:   10
c ---[ 967]---> BDD-cost:   10
c ---[ 966]---> BDD-cost:   10
c ---[ 965]---> BDD-cost:   10
c ---[ 964]---> BDD-cost:   10
c ---[ 963]---> BDD-cost:   10
c ---[ 962]---> BDD-cost:   10
c ---[ 961]---> BDD-cost:   10
c ---[ 960]---> BDD-cost:   10
c ---[ 959]---> BDD-cost:   10
c ---[ 958]---> BDD-cost:   10
c ---[ 957]---> BDD-cost:   10
c ---[ 956]---> BDD-cost:   10
c ---[ 955]---> BDD-cost:   10
c ---[ 954]---> BDD-cost:   10
c ---[ 953]---> BDD-cost:   10
c ---[ 952]---> BDD-cost:   10
c ---[ 951]---> BDD-cost:   10
c ---[ 950]---> BDD-cost:   10
c ---[ 949]---> BDD-cost:   10
c ---[ 948]---> BDD-cost:   10
c ---[ 947]---> BDD-cost:   10
c ---[ 946]---> BDD-cost:   10
c ---[ 945]---> BDD-cost:   10
c ---[ 944]---> BDD-cost:   10
c ---[ 943]---> BDD-cost:   10
c ---[ 942]---> BDD-cost:   10
c ---[ 941]---> BDD-cost:   10
c ---[ 940]---> BDD-cost:   10
c ---[ 939]---> BDD-cost:   10
c ---[ 938]---> BDD-cost:   10
c ---[ 937]---> BDD-cost:   10
c ---[ 936]---> BDD-cost:   10
c ---[ 935]---> BDD-cost:   10
c ---[ 934]---> BDD-cost:   10
c ---[ 933]---> BDD-cost:   10
c ---[ 932]---> BDD-cost:   10
c ---[ 931]---> BDD-cost:   10
c ---[ 930]---> BDD-cost:   10
c ---[ 929]---> BDD-cost:   10
c ---[ 928]---> BDD-cost:   10
c ---[ 927]---> BDD-cost:   10
c ---[ 926]---> BDD-cost:   10
c ---[ 925]---> BDD-cost:   10
c ---[ 924]---> BDD-cost:   10
c ---[ 923]---> BDD-cost:   10
c ---[ 922]---> BDD-cost:   10
c ---[ 921]---> BDD-cost:   10
c ---[ 920]---> BDD-cost:   10
c ---[ 919]---> BDD-cost:   10
c ---[ 918]---> BDD-cost:   10
c ---[ 917]---> BDD-cost:   10
c ---[ 916]---> BDD-cost:   10
c ---[ 915]---> BDD-cost:   10
c ---[ 914]---> BDD-cost:   10
c ---[ 913]---> BDD-cost:   10
c ---[ 912]---> BDD-cost:   10
c ---[ 911]---> BDD-cost:   10
c ---[ 910]---> BDD-cost:   10
c ---[ 909]---> BDD-cost:   10
c ---[ 908]---> BDD-cost:   10
c ---[ 907]---> BDD-cost:   10
c ---[ 906]---> BDD-cost:   10
c ---[ 905]---> BDD-cost:   10
c ---[ 904]---> BDD-cost:   10
c ---[ 903]---> BDD-cost:   10
c ---[ 902]---> BDD-cost:   10
c ---[ 901]---> BDD-cost:   10
c ---[ 900]---> BDD-cost:   10
c ---[ 899]---> BDD-cost:   10
c ---[ 898]---> BDD-cost:   10
c ---[ 897]---> BDD-cost:   10
c ---[ 896]---> BDD-cost:   10
c ---[ 895]---> BDD-cost:   10
c ---[ 894]---> BDD-cost:   10
c ---[ 893]---> BDD-cost:   10
c ---[ 892]---> BDD-cost:   10
c ---[ 891]---> BDD-cost:   10
c ---[ 890]---> BDD-cost:   10
c ---[ 889]---> BDD-cost:   10
c ---[ 888]---> BDD-cost:   10
c ---[ 887]---> BDD-cost:   10
c ---[ 886]---> BDD-cost:   10
c ---[ 885]---> BDD-cost:   10
c ---[ 884]---> BDD-cost:   10
c ---[ 883]---> BDD-cost:   10
c ---[ 882]---> BDD-cost:   10
c ---[ 881]---> BDD-cost:   10
c ---[ 880]---> BDD-cost:   10
c ---[ 879]---> BDD-cost:   10
c ---[ 878]---> BDD-cost:   10
c ---[ 877]---> BDD-cost:   10
c ---[ 876]---> BDD-cost:   10
c ---[ 875]---> BDD-cost:   10
c ---[ 874]---> BDD-cost:   10
c ---[ 873]---> BDD-cost:   10
c ---[ 872]---> BDD-cost:   10
c ---[ 871]---> BDD-cost:   10
c ---[ 870]---> BDD-cost:   10
c ---[ 869]---> BDD-cost:   10
c ---[ 868]---> BDD-cost:   10
c ---[ 867]---> BDD-cost:   10
c ---[ 866]---> BDD-cost:   10
c ---[ 865]---> BDD-cost:   10
c ---[ 864]---> BDD-cost:   10
c ---[ 863]---> BDD-cost:   10
c ---[ 862]---> BDD-cost:   10
c ---[ 861]---> BDD-cost:   10
c ---[ 860]---> BDD-cost:   10
c ---[ 859]---> BDD-cost:   10
c ---[ 858]---> BDD-cost:   10
c ---[ 857]---> BDD-cost:   10
c ---[ 856]---> BDD-cost:   10
c ---[ 855]---> BDD-cost:   10
c ---[ 854]---> BDD-cost:   10
c ---[ 853]---> BDD-cost:   10
c ---[ 852]---> BDD-cost:   10
c ---[ 851]---> BDD-cost:   10
c ---[ 850]---> BDD-cost:   10
c ---[ 849]---> BDD-cost:   10
c ---[ 848]---> BDD-cost:   10
c ---[ 847]---> BDD-cost:   10
c ---[ 846]---> BDD-cost:   10
c ---[ 845]---> BDD-cost:   10
c ---[ 844]---> BDD-cost:   10
c ---[ 843]---> BDD-cost:   10
c ---[ 842]---> BDD-cost:   10
c ---[ 841]---> BDD-cost:   10
c ---[ 840]---> BDD-cost:   10
c ---[ 839]---> BDD-cost:   10
c ---[ 838]---> BDD-cost:   10
c ---[ 837]---> BDD-cost:   10
c ---[ 836]---> BDD-cost:   10
c ---[ 835]---> BDD-cost:   10
c ---[ 834]---> BDD-cost:   10
c ---[ 833]---> BDD-cost:   10
c ---[ 832]---> BDD-cost:   10
c ---[ 831]---> BDD-cost:   10
c ---[ 830]---> BDD-cost:   10
c ---[ 829]---> BDD-cost:   10
c ---[ 828]---> BDD-cost:   10
c ---[ 827]---> BDD-cost:   10
c ---[ 826]---> BDD-cost:   10
c ---[ 825]---> BDD-cost:   10
c ---[ 824]---> BDD-cost:   10
c ---[ 823]---> BDD-cost:   10
c ---[ 822]---> BDD-cost:   10
c ---[ 821]---> BDD-cost:   10
c ---[ 820]---> BDD-cost:   10
c ---[ 819]---> BDD-cost:   10
c ---[ 818]---> BDD-cost:   10
c ---[ 817]---> BDD-cost:   10
c ---[ 816]---> BDD-cost:   10
c ---[ 815]---> BDD-cost:   10
c ---[ 814]---> BDD-cost:   10
c ---[ 813]---> BDD-cost:   10
c ---[ 812]---> BDD-cost:   10
c ---[ 811]---> BDD-cost:   10
c ---[ 810]---> BDD-cost:   10
c ---[ 809]---> BDD-cost:   10
c ---[ 808]---> BDD-cost:   10
c ---[ 807]---> BDD-cost:   10
c ---[ 806]---> BDD-cost:   10
c ---[ 805]---> BDD-cost:   10
c ---[ 804]---> BDD-cost:   10
c ---[ 803]---> BDD-cost:   10
c ---[ 802]---> BDD-cost:   10
c ---[ 801]---> BDD-cost:   10
c ---[ 800]---> BDD-cost:   10
c ---[ 799]---> BDD-cost:   10
c ---[ 798]---> BDD-cost:   10
c ---[ 797]---> BDD-cost:   10
c ---[ 796]---> BDD-cost:   10
c ---[ 795]---> BDD-cost:   10
c ---[ 794]---> BDD-cost:   10
c ---[ 793]---> BDD-cost:   10
c ---[ 792]---> BDD-cost:   10
c ---[ 791]---> BDD-cost:   10
c ---[ 790]---> BDD-cost:   10
c ---[ 789]---> BDD-cost:   10
c ---[ 788]---> BDD-cost:   10
c ---[ 787]---> BDD-cost:   10
c ---[ 786]---> BDD-cost:   10
c ---[ 785]---> BDD-cost:   10
c ---[ 784]---> BDD-cost:   10
c ---[ 783]---> BDD-cost:   10
c ---[ 782]---> BDD-cost:   10
c ---[ 781]---> BDD-cost:   10
c ---[ 780]---> BDD-cost:   10
c ---[ 779]---> BDD-cost:   10
c ---[ 778]---> BDD-cost:   10
c ---[ 777]---> BDD-cost:   10
c ---[ 776]---> BDD-cost:   10
c ---[ 775]---> BDD-cost:   10
c ---[ 774]---> BDD-cost:   10
c ---[ 773]---> BDD-cost:   10
c ---[ 772]---> BDD-cost:   10
c ---[ 771]---> BDD-cost:   10
c ---[ 770]---> BDD-cost:   10
c ---[ 769]---> BDD-cost:   10
c ---[ 768]---> BDD-cost:   10
c ---[ 767]---> BDD-cost:   10
c ---[ 766]---> BDD-cost:   10
c ---[ 765]---> BDD-cost:   10
c ---[ 764]---> BDD-cost:   10
c ---[ 763]---> BDD-cost:   10
c ---[ 762]---> BDD-cost:   10
c ---[ 761]---> BDD-cost:   10
c ---[ 760]---> BDD-cost:   10
c ---[ 759]---> BDD-cost:   10
c ---[ 758]---> BDD-cost:   10
c ---[ 757]---> BDD-cost:   10
c ---[ 756]---> BDD-cost:   10
c ---[ 755]---> BDD-cost:   10
c ---[ 754]---> BDD-cost:   10
c ---[ 753]---> BDD-cost:   10
c ---[ 752]---> BDD-cost:   10
c ---[ 751]---> BDD-cost:   10
c ---[ 750]---> BDD-cost:   10
c ---[ 749]---> BDD-cost:   10
c ---[ 748]---> BDD-cost:   10
c ---[ 747]---> BDD-cost:   10
c ---[ 746]---> BDD-cost:   10
c ---[ 745]---> BDD-cost:   10
c ---[ 744]---> BDD-cost:   10
c ---[ 743]---> BDD-cost:   10
c ---[ 742]---> BDD-cost:   10
c ---[ 741]---> BDD-cost:   10
c ---[ 740]---> BDD-cost:   10
c ---[ 739]---> BDD-cost:   10
c ---[ 738]---> BDD-cost:   10
c ---[ 737]---> BDD-cost:   10
c ---[ 736]---> BDD-cost:   10
c ---[ 735]---> BDD-cost:   10
c ---[ 734]---> BDD-cost:   10
c ---[ 733]---> BDD-cost:   10
c ---[ 732]---> BDD-cost:   10
c ---[ 731]---> BDD-cost:   10
c ---[ 730]---> BDD-cost:   10
c ---[ 729]---> BDD-cost:   10
c ---[ 728]---> BDD-cost:   10
c ---[ 727]---> BDD-cost:   10
c ---[ 726]---> BDD-cost:   10
c ---[ 725]---> BDD-cost:   10
c ---[ 724]---> BDD-cost:   10
c ---[ 723]---> BDD-cost:   10
c ---[ 722]---> BDD-cost:   10
c ---[ 721]---> BDD-cost:   10
c ---[ 720]---> BDD-cost:   10
c ---[ 719]---> BDD-cost:   10
c ---[ 718]---> BDD-cost:   10
c ---[ 717]---> BDD-cost:   10
c ---[ 716]---> BDD-cost:   10
c ---[ 715]---> BDD-cost:   10
c ---[ 714]---> BDD-cost:   10
c ---[ 713]---> BDD-cost:   10
c ---[ 712]---> BDD-cost:   10
c ---[ 711]---> BDD-cost:   10
c ---[ 710]---> BDD-cost:   10
c ---[ 709]---> BDD-cost:   10
c ---[ 708]---> BDD-cost:   10
c ---[ 707]---> BDD-cost:   10
c ---[ 706]---> BDD-cost:   10
c ---[ 705]---> BDD-cost:   10
c ---[ 704]---> BDD-cost:   10
c ---[ 703]---> BDD-cost:   10
c ---[ 702]---> BDD-cost:   10
c ---[ 701]---> BDD-cost:   10
c ---[ 700]---> BDD-cost:   10
c ---[ 699]---> BDD-cost:   10
c ---[ 698]---> BDD-cost:   10
c ---[ 697]---> BDD-cost:   10
c ---[ 696]---> BDD-cost:   10
c ---[ 695]---> BDD-cost:   10
c ---[ 694]---> BDD-cost:   10
c ---[ 693]---> BDD-cost:   10
c ---[ 692]---> BDD-cost:   10
c ---[ 691]---> BDD-cost:   10
c ---[ 690]---> BDD-cost:   10
c ---[ 689]---> BDD-cost:   10
c ---[ 688]---> BDD-cost:   10
c ---[ 687]---> BDD-cost:   10
c ---[ 686]---> BDD-cost:   10
c ---[ 685]---> BDD-cost:   10
c ---[ 684]---> BDD-cost:   10
c ---[ 683]---> BDD-cost:   10
c ---[ 682]---> BDD-cost:   10
c ---[ 681]---> BDD-cost:   10
c ---[ 680]---> BDD-cost:   10
c ---[ 679]---> BDD-cost:   10
c ---[ 678]---> BDD-cost:   10
c ---[ 677]---> BDD-cost:   10
c ---[ 676]---> BDD-cost:   10
c ---[ 675]---> BDD-cost:   10
c ---[ 674]---> BDD-cost:   10
c ---[ 673]---> BDD-cost:   10
c ---[ 672]---> BDD-cost:   10
c ---[ 671]---> BDD-cost:   10
c ---[ 670]---> BDD-cost:   10
c ---[ 669]---> BDD-cost:   10
c ---[ 668]---> BDD-cost:   10
c ---[ 667]---> BDD-cost:   10
c ---[ 666]---> BDD-cost:   10
c ---[ 665]---> BDD-cost:   10
c ---[ 664]---> BDD-cost:   10
c ---[ 663]---> BDD-cost:   10
c ---[ 662]---> BDD-cost:   10
c ---[ 661]---> BDD-cost:   10
c ---[ 660]---> BDD-cost:   10
c ---[ 659]---> BDD-cost:   10
c ---[ 658]---> BDD-cost:   10
c ---[ 657]---> BDD-cost:   10
c ---[ 656]---> BDD-cost:   10
c ---[ 655]---> BDD-cost:   10
c ---[ 654]---> BDD-cost:   10
c ---[ 653]---> BDD-cost:   10
c ---[ 652]---> BDD-cost:   10
c ---[ 651]---> BDD-cost:   10
c ---[ 650]---> BDD-cost:   10
c ---[ 649]---> BDD-cost:   10
c ---[ 648]---> BDD-cost:   10
c ---[ 647]---> BDD-cost:   10
c ---[ 646]---> BDD-cost:   10
c ---[ 645]---> BDD-cost:   10
c ---[ 644]---> BDD-cost:   10
c ---[ 643]---> BDD-cost:   10
c ---[ 642]---> BDD-cost:   10
c ---[ 641]---> BDD-cost:   10
c ---[ 640]---> BDD-cost:   10
c ---[ 639]---> BDD-cost:   10
c ---[ 638]---> BDD-cost:   10
c ---[ 637]---> BDD-cost:   10
c ---[ 636]---> BDD-cost:   10
c ---[ 635]---> BDD-cost:   10
c ---[ 634]---> BDD-cost:   10
c ---[ 633]---> BDD-cost:   10
c ---[ 632]---> BDD-cost:   10
c ---[ 631]---> BDD-cost:   10
c ---[ 630]---> BDD-cost:   10
c ---[ 629]---> BDD-cost:   10
c ---[ 628]---> BDD-cost:   10
c ---[ 627]---> BDD-cost:   10
c ---[ 626]---> BDD-cost:   10
c ---[ 625]---> BDD-cost:   10
c ---[ 624]---> BDD-cost:   10
c ---[ 623]---> BDD-cost:   10
c ---[ 622]---> BDD-cost:   10
c ---[ 621]---> BDD-cost:   10
c ---[ 620]---> BDD-cost:   10
c ---[ 619]---> BDD-cost:   10
c ---[ 618]---> BDD-cost:   10
c ---[ 617]---> BDD-cost:   10
c ---[ 616]---> BDD-cost:   10
c ---[ 615]---> BDD-cost:   10
c ---[ 614]---> BDD-cost:   10
c ---[ 613]---> BDD-cost:   10
c ---[ 612]---> BDD-cost:   10
c ---[ 611]---> BDD-cost:   10
c ---[ 610]---> BDD-cost:   10
c ---[ 609]---> BDD-cost:   10
c ---[ 608]---> BDD-cost:   10
c ---[ 607]---> BDD-cost:   10
c ---[ 606]---> BDD-cost:   10
c ---[ 605]---> BDD-cost:   10
c ---[ 604]---> BDD-cost:   10
c ---[ 603]---> BDD-cost:   10
c ---[ 602]---> BDD-cost:   10
c ---[ 601]---> BDD-cost:   10
c ---[ 600]---> BDD-cost:   10
c ---[ 599]---> BDD-cost:   10
c ---[ 598]---> BDD-cost:   10
c ---[ 597]---> BDD-cost:   10
c ---[ 596]---> BDD-cost:   10
c ---[ 595]---> BDD-cost:   10
c ---[ 594]---> BDD-cost:   10
c ---[ 593]---> BDD-cost:   10
c ---[ 592]---> BDD-cost:   10
c ---[ 591]---> BDD-cost:   10
c ---[ 590]---> BDD-cost:   10
c ---[ 589]---> BDD-cost:   10
c ---[ 588]---> BDD-cost:   10
c ---[ 587]---> BDD-cost:   10
c ---[ 586]---> BDD-cost:   10
c ---[ 585]---> BDD-cost:   10
c ---[ 584]---> BDD-cost:   10
c ---[ 583]---> BDD-cost:   10
c ---[ 582]---> BDD-cost:   10
c ---[ 581]---> BDD-cost:   10
c ---[ 580]---> BDD-cost:   10
c ---[ 579]---> BDD-cost:   10
c ---[ 578]---> BDD-cost:   10
c ---[ 577]---> BDD-cost:   10
c ---[ 576]---> BDD-cost:   10
c ---[ 575]---> BDD-cost:   10
c ---[ 574]---> BDD-cost:   10
c ---[ 573]---> BDD-cost:   10
c ---[ 572]---> BDD-cost:   10
c ---[ 571]---> BDD-cost:   10
c ---[ 570]---> BDD-cost:   10
c ---[ 569]---> BDD-cost:   10
c ---[ 568]---> BDD-cost:   10
c ---[ 567]---> BDD-cost:   10
c ---[ 566]---> BDD-cost:   10
c ---[ 565]---> BDD-cost:   10
c ---[ 564]---> BDD-cost:   10
c ---[ 563]---> BDD-cost:   10
c ---[ 562]---> BDD-cost:   10
c ---[ 561]---> BDD-cost:   10
c ---[ 560]---> BDD-cost:   10
c ---[ 559]---> BDD-cost:   10
c ---[ 558]---> BDD-cost:   10
c ---[ 557]---> BDD-cost:   10
c ---[ 556]---> BDD-cost:   10
c ---[ 555]---> BDD-cost:   10
c ---[ 554]---> BDD-cost:   10
c ---[ 553]---> BDD-cost:   10
c ---[ 552]---> BDD-cost:   10
c ---[ 551]---> BDD-cost:   10
c ---[ 550]---> BDD-cost:   10
c ---[ 549]---> BDD-cost:   10
c ---[ 548]---> BDD-cost:   10
c ---[ 547]---> BDD-cost:   10
c ---[ 546]---> BDD-cost:   10
c ---[ 545]---> BDD-cost:   10
c ---[ 544]---> BDD-cost:   10
c ---[ 543]---> BDD-cost:   10
c ---[ 542]---> BDD-cost:   10
c ---[ 541]---> BDD-cost:   10
c ---[ 540]---> BDD-cost:   10
c ---[ 539]---> BDD-cost:   10
c ---[ 538]---> BDD-cost:   10
c ---[ 537]---> BDD-cost:   10
c ---[ 536]---> BDD-cost:   10
c ---[ 535]---> BDD-cost:   10
c ---[ 534]---> BDD-cost:   10
c ---[ 533]---> BDD-cost:   10
c ---[ 532]---> BDD-cost:   10
c ---[ 531]---> BDD-cost:   10
c ---[ 530]---> BDD-cost:   10
c ---[ 529]---> BDD-cost:   10
c ---[ 528]---> BDD-cost:   10
c ---[ 527]---> BDD-cost:   10
c ---[ 526]---> BDD-cost:   10
c ---[ 525]---> BDD-cost:   10
c ---[ 524]---> BDD-cost:   10
c ---[ 523]---> BDD-cost:   10
c ---[ 522]---> BDD-cost:   10
c ---[ 521]---> BDD-cost:   10
c ---[ 520]---> BDD-cost:   10
c ---[ 519]---> BDD-cost:   10
c ---[ 518]---> BDD-cost:   10
c ---[ 517]---> BDD-cost:   10
c ---[ 516]---> BDD-cost:   10
c ---[ 515]---> BDD-cost:   10
c ---[ 514]---> BDD-cost:   10
c ---[ 513]---> BDD-cost:   10
c ---[ 512]---> BDD-cost:   10
c ---[ 511]---> BDD-cost:   10
c ---[ 510]---> BDD-cost:   10
c ---[ 509]---> BDD-cost:   10
c ---[ 508]---> BDD-cost:   10
c ---[ 507]---> BDD-cost:   10
c ---[ 506]---> BDD-cost:   10
c ---[ 505]---> BDD-cost:   10
c ---[ 504]---> BDD-cost:   10
c ---[ 503]---> BDD-cost:   10
c ---[ 502]---> BDD-cost:   10
c ---[ 501]---> BDD-cost:   10
c ---[ 500]---> BDD-cost:   10
c ---[ 499]---> BDD-cost:   10
c ---[ 498]---> BDD-cost:   10
c ---[ 497]---> BDD-cost:   10
c ---[ 496]---> BDD-cost:   10
c ---[ 495]---> BDD-cost:   10
c ---[ 494]---> BDD-cost:   10
c ---[ 493]---> BDD-cost:   10
c ---[ 492]---> BDD-cost:   10
c ---[ 491]---> BDD-cost:   10
c ---[ 490]---> BDD-cost:   10
c ---[ 489]---> BDD-cost:   10
c ---[ 488]---> BDD-cost:   10
c ---[ 487]---> BDD-cost:   10
c ---[ 486]---> BDD-cost:   10
c ---[ 485]---> BDD-cost:   10
c ---[ 484]---> BDD-cost:   10
c ---[ 483]---> BDD-cost:   10
c ---[ 482]---> BDD-cost:   10
c ---[ 481]---> BDD-cost:   10
c ---[ 480]---> BDD-cost:   10
c ---[ 479]---> BDD-cost:   10
c ---[ 478]---> BDD-cost:   10
c ---[ 477]---> BDD-cost:   10
c ---[ 476]---> BDD-cost:   10
c ---[ 475]---> BDD-cost:   10
c ---[ 474]---> BDD-cost:   10
c ---[ 473]---> BDD-cost:   10
c ---[ 472]---> BDD-cost:   10
c ---[ 471]---> BDD-cost:   10
c ---[ 470]---> BDD-cost:   10
c ---[ 469]---> BDD-cost:   10
c ---[ 468]---> BDD-cost:   10
c ---[ 467]---> BDD-cost:   10
c ---[ 466]---> BDD-cost:   10
c ---[ 465]---> BDD-cost:   10
c ---[ 464]---> BDD-cost:   10
c ---[ 463]---> BDD-cost:   10
c ---[ 462]---> BDD-cost:   10
c ---[ 461]---> BDD-cost:   10
c ---[ 460]---> BDD-cost:   10
c ---[ 459]---> BDD-cost:   10
c ---[ 458]---> BDD-cost:   10
c ---[ 457]---> BDD-cost:   10
c ---[ 456]---> BDD-cost:   10
c ---[ 455]---> BDD-cost:   10
c ---[ 454]---> BDD-cost:   10
c ---[ 453]---> BDD-cost:   10
c ---[ 452]---> BDD-cost:   10
c ---[ 451]---> BDD-cost:   10
c ---[ 450]---> BDD-cost:   10
c ---[ 449]---> BDD-cost:   10
c ---[ 448]---> BDD-cost:   10
c ---[ 447]---> BDD-cost:   10
c ---[ 446]---> BDD-cost:   10
c ---[ 445]---> BDD-cost:   10
c ---[ 444]---> BDD-cost:   10
c ---[ 443]---> BDD-cost:   10
c ---[ 442]---> BDD-cost:   10
c ---[ 441]---> BDD-cost:   10
c ---[ 440]---> BDD-cost:   10
c ---[ 439]---> BDD-cost:   10
c ---[ 438]---> BDD-cost:   10
c ---[ 437]---> BDD-cost:   10
c ---[ 436]---> BDD-cost:   10
c ---[ 435]---> BDD-cost:   10
c ---[ 434]---> BDD-cost:   10
c ---[ 433]---> BDD-cost:   10
c ---[ 432]---> BDD-cost:   10
c ---[ 431]---> BDD-cost:   10
c ---[ 430]---> BDD-cost:   10
c ---[ 429]---> BDD-cost:   10
c ---[ 428]---> BDD-cost:   10
c ---[ 427]---> BDD-cost:   10
c ---[ 426]---> BDD-cost:   10
c ---[ 425]---> BDD-cost:   10
c ---[ 424]---> BDD-cost:   10
c ---[ 423]---> BDD-cost:   10
c ---[ 422]---> BDD-cost:   10
c ---[ 421]---> BDD-cost:   10
c ---[ 420]---> BDD-cost:   10
c ---[ 419]---> BDD-cost:   10
c ---[ 418]---> BDD-cost:   10
c ---[ 417]---> BDD-cost:   10
c ---[ 416]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   10
c ---[ 414]---> BDD-cost:   10
c ---[ 413]---> BDD-cost:   10
c ---[ 412]---> BDD-cost:   10
c ---[ 411]---> BDD-cost:   10
c ---[ 410]---> BDD-cost:   10
c ---[ 409]---> BDD-cost:   10
c ---[ 408]---> BDD-cost:   10
c ---[ 407]---> BDD-cost:   10
c ---[ 406]---> BDD-cost:   10
c ---[ 405]---> BDD-cost:   10
c ---[ 404]---> BDD-cost:   10
c ---[ 403]---> BDD-cost:   10
c ---[ 402]---> BDD-cost:   10
c ---[ 401]---> BDD-cost:   10
c ---[ 400]---> BDD-cost:   10
c ---[ 399]---> BDD-cost:   10
c ---[ 398]---> BDD-cost:   10
c ---[ 397]---> BDD-cost:   10
c ---[ 396]---> BDD-cost:   10
c ---[ 395]---> BDD-cost:   10
c ---[ 394]---> BDD-cost:   10
c ---[ 393]---> BDD-cost:   10
c ---[ 392]---> BDD-cost:   10
c ---[ 391]---> BDD-cost:   10
c ---[ 390]---> BDD-cost:   10
c ---[ 389]---> BDD-cost:   10
c ---[ 388]---> BDD-cost:   10
c ---[ 387]---> BDD-cost:   10
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   10
c ---[ 384]---> BDD-cost:   10
c ---[ 383]---> BDD-cost:   10
c ---[ 382]---> BDD-cost:   10
c ---[ 381]---> BDD-cost:   10
c ---[ 380]---> BDD-cost:   10
c ---[ 379]---> BDD-cost:   10
c ---[ 378]---> BDD-cost:   10
c ---[ 377]---> BDD-cost:   10
c ---[ 376]---> BDD-cost:   10
c ---[ 375]---> BDD-cost:   10
c ---[ 374]---> BDD-cost:   10
c ---[ 373]---> BDD-cost:   10
c ---[ 372]---> BDD-cost:   10
c ---[ 371]---> BDD-cost:   10
c ---[ 370]---> BDD-cost:   10
c ---[ 369]---> BDD-cost:   10
c ---[ 368]---> BDD-cost:   10
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 364]---> BDD-cost:   10
c ---[ 363]---> BDD-cost:   10
c ---[ 362]---> BDD-cost:   10
c ---[ 361]---> BDD-cost:   10
c ---[ 360]---> BDD-cost:   10
c ---[ 359]---> BDD-cost:   10
c ---[ 358]---> BDD-cost:   10
c ---[ 357]---> BDD-cost:   10
c ---[ 356]---> BDD-cost:   10
c ---[ 355]---> BDD-cost:   10
c ---[ 354]---> BDD-cost:   10
c ---[ 353]---> BDD-cost:   10
c ---[ 352]---> BDD-cost:   10
c ---[ 351]---> BDD-cost:   10
c ---[ 350]---> BDD-cost:   10
c ---[ 349]---> BDD-cost:   10
c ---[ 348]---> BDD-cost:   10
c ---[ 347]---> BDD-cost:   10
c ---[ 346]---> BDD-cost:   10
c ---[ 345]---> BDD-cost:   10
c ---[ 344]---> BDD-cost:   10
c ---[ 343]---> BDD-cost:   10
c ---[ 342]---> BDD-cost:   10
c ---[ 341]---> BDD-cost:   10
c ---[ 340]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   10
c ---[ 338]---> BDD-cost:   10
c ---[ 337]---> BDD-cost:   10
c ---[ 336]---> BDD-cost:   10
c ---[ 335]---> BDD-cost:   10
c ---[ 334]---> BDD-cost:   10
c ---[ 333]---> BDD-cost:   10
c ---[ 332]---> BDD-cost:   10
c ---[ 331]---> BDD-cost:   10
c ---[ 330]---> BDD-cost:   10
c ---[ 329]---> BDD-cost:   10
c ---[ 328]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:   10
c ---[ 326]---> BDD-cost:   10
c ---[ 325]---> BDD-cost:   10
c ---[ 324]---> BDD-cost:   10
c ---[ 323]---> BDD-cost:   10
c ---[ 322]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   10
c ---[ 320]---> BDD-cost:   10
c ---[ 319]---> BDD-cost:   10
c ---[ 318]---> BDD-cost:   10
c ---[ 317]---> BDD-cost:   10
c ---[ 316]---> BDD-cost:   10
c ---[ 315]---> BDD-cost:   10
c ---[ 314]---> BDD-cost:   10
c ---[ 313]---> BDD-cost:   10
c ---[ 312]---> BDD-cost:   10
c ---[ 311]---> BDD-cost:   10
c ---[ 310]---> BDD-cost:   10
c ---[ 309]---> BDD-cost:   10
c ---[ 308]---> BDD-cost:   10
c ---[ 307]---> BDD-cost:   10
c ---[ 306]---> BDD-cost:   10
c ---[ 305]---> BDD-cost:   10
c ---[ 304]---> BDD-cost:   10
c ---[ 303]---> BDD-cost:   10
c ---[ 302]---> BDD-cost:   10
c ---[ 301]---> BDD-cost:   10
c ---[ 300]---> BDD-cost:   10
c ---[ 299]---> BDD-cost:   10
c ---[ 298]---> BDD-cost:   10
c ---[ 297]---> BDD-cost:   10
c ---[ 296]---> BDD-cost:   10
c ---[ 295]---> BDD-cost:   10
c ---[ 294]---> BDD-cost:   10
c ---[ 293]---> BDD-cost:   10
c ---[ 292]---> BDD-cost:   10
c ---[ 291]---> BDD-cost:   10
c ---[ 290]---> BDD-cost:   10
c ---[ 289]---> BDD-cost:   10
c ---[ 288]---> BDD-cost:   10
c ---[ 287]---> BDD-cost:   10
c ---[ 286]---> BDD-cost:   10
c ---[ 285]---> BDD-cost:   10
c ---[ 284]---> BDD-cost:   10
c ---[ 283]---> BDD-cost:   10
c ---[ 282]---> BDD-cost:   10
c ---[ 281]---> BDD-cost:   10
c ---[ 280]---> BDD-cost:   10
c ---[ 279]---> BDD-cost:   10
c ---[ 278]---> BDD-cost:   10
c ---[ 277]---> BDD-cost:   10
c ---[ 276]---> BDD-cost:   10
c ---[ 275]---> BDD-cost:   10
c ---[ 274]---> BDD-cost:   10
c ---[ 273]---> BDD-cost:   10
c ---[ 272]---> BDD-cost:   10
c ---[ 271]---> BDD-cost:   10
c ---[ 270]---> BDD-cost:   10
c ---[ 269]---> BDD-cost:   10
c ---[ 268]---> BDD-cost:   10
c ---[ 267]---> BDD-cost:   10
c ---[ 266]---> BDD-cost:   10
c ---[ 265]---> BDD-cost:   10
c ---[ 264]---> BDD-cost:   10
c ---[ 263]---> BDD-cost:   10
c ---[ 262]---> BDD-cost:   10
c ---[ 261]---> BDD-cost:   10
c ---[ 260]---> BDD-cost:   10
c ---[ 259]---> BDD-cost:   10
c ---[ 258]---> BDD-cost:   10
c ---[ 257]---> BDD-cost:   10
c ---[ 256]---> BDD-cost:   10
c ---[ 255]---> BDD-cost:   10
c ---[ 254]---> BDD-cost:   10
c ---[ 253]---> BDD-cost:   10
c ---[ 252]---> BDD-cost:   11
c ---[ 251]---> BDD-cost:   11
c ---[ 250]---> BDD-cost:   11
c ---[ 249]---> BDD-cost:   11
c ---[ 248]---> BDD-cost:   11
c ---[ 247]---> BDD-cost:   11
c ---[ 246]---> BDD-cost:   11
c ---[ 245]---> BDD-cost:   11
c ---[ 244]---> BDD-cost:   11
c ---[ 243]---> BDD-cost:   11
c ---[ 242]---> BDD-cost:   11
c ---[ 241]---> BDD-cost:   11
c ---[ 240]---> BDD-cost:   11
c ---[ 239]---> BDD-cost:   11
c ---[ 238]---> BDD-cost:   11
c ---[ 237]---> BDD-cost:   11
c ---[ 236]---> BDD-cost:   11
c ---[ 235]---> BDD-cost:   11
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   11
c ---[ 232]---> BDD-cost:   11
c ---[ 231]---> BDD-cost:   11
c ---[ 230]---> BDD-cost:   11
c ---[ 229]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   11
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   11
c ---[ 225]---> BDD-cost:   11
c ---[ 224]---> BDD-cost:   11
c ---[ 223]---> BDD-cost:   11
c ---[ 222]---> BDD-cost:   11
c ---[ 221]---> BDD-cost:   11
c ---[ 220]---> BDD-cost:   11
c ---[ 219]---> BDD-cost:   11
c ---[ 218]---> BDD-cost:   11
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   11
c ---[ 215]---> BDD-cost:   11
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   11
c ---[ 212]---> BDD-cost:   11
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   11
c ---[ 209]---> BDD-cost:   11
c ---[ 208]---> BDD-cost:   11
c ---[ 207]---> BDD-cost:   11
c ---[ 206]---> BDD-cost:   11
c ---[ 205]---> BDD-cost:   11
c ---[ 204]---> BDD-cost:   11
c ---[ 203]---> BDD-cost:   11
c ---[ 202]---> BDD-cost:   11
c ---[ 201]---> BDD-cost:   11
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:   11
c ---[ 198]---> BDD-cost:   11
c ---[ 197]---> BDD-cost:   11
c ---[ 196]---> BDD-cost:   11
c ---[ 195]---> BDD-cost:   11
c ---[ 194]---> BDD-cost:   11
c ---[ 193]---> BDD-cost:   11
c ---[ 192]---> BDD-cost:   11
c ---[ 191]---> BDD-cost:   11
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:   11
c ---[ 187]---> BDD-cost:   11
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   11
c ---[ 184]---> BDD-cost:   11
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:   11
c ---[ 181]---> BDD-cost:   11
c ---[ 180]---> BDD-cost:   11
c ---[ 179]---> BDD-cost:   11
c ---[ 178]---> BDD-cost:   11
c ---[ 177]---> BDD-cost:   11
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:   11
c ---[ 173]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   11
c ---[ 171]---> BDD-cost:   11
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   11
c ---[ 168]---> BDD-cost:   11
c ---[ 167]---> BDD-cost:   11
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   11
c ---[ 164]---> BDD-cost:   11
c ---[ 163]---> BDD-cost:   11
c ---[ 162]---> BDD-cost:   11
c ---[ 161]---> BDD-cost:   11
c ---[ 160]---> BDD-cost:   11
c ---[ 159]---> BDD-cost:   11
c ---[ 158]---> BDD-cost:   11
c ---[ 157]---> BDD-cost:   11
c ---[ 156]---> BDD-cost:   11
c ---[ 155]---> BDD-cost:   11
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:   11
c ---[ 151]---> BDD-cost:   11
c ---[ 150]---> BDD-cost:   11
c ---[ 149]---> BDD-cost:   11
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:   11
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:   11
c ---[ 143]---> BDD-cost:   11
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   11
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   11
c ---[ 138]---> BDD-cost:   11
c ---[ 137]---> BDD-cost:   11
c ---[ 136]---> BDD-cost:   11
c ---[ 135]---> BDD-cost:   11
c ---[ 134]---> BDD-cost:   11
c ---[ 133]---> BDD-cost:   11
c ---[ 132]---> BDD-c#### 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.65 0.87 0.89 2/54 2964
Raw data (stat): 2964 (runsolver) R 2963 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550724652 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.0002 s]
Raw data (loadavg): 0.70 0.87 0.89 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 13175 0 0 0 970 29 0 0 25 0 1 0 550724652 44257280 9327 4294967295 134512640 134672761 3221224544 3220196496 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10805 9327 603 41 0 10764 0
vsize: 43220
[startup+20.0014 s]
Raw data (loadavg): 0.75 0.87 0.89 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 15582 0 0 0 1966 33 0 0 25 0 1 0 550724652 57982976 11734 4294967295 134512640 134672761 3221224544 3220428336 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14156 11735 603 41 0 14115 0
vsize: 56624
[startup+30.0022 s]
Raw data (loadavg): 0.79 0.88 0.89 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 22439 0 0 0 2950 49 0 0 25 0 1 0 550724652 73654272 15955 4294967295 134512640 134672761 3221224544 3220301520 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17982 15955 603 41 0 17941 0
vsize: 71928
[startup+40.0016 s]
Raw data (loadavg): 0.82 0.88 0.89 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 23841 0 0 0 3949 51 0 0 25 0 1 0 550724652 77979648 17357 4294967295 134512640 134672761 3221224544 3220200256 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19038 17357 603 41 0 18997 0
vsize: 76152
[startup+50.0029 s]
Raw data (loadavg): 0.85 0.88 0.89 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 25411 0 0 0 4945 54 0 0 25 0 1 0 550724652 82845696 18927 4294967295 134512640 134672761 3221224544 3220196320 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20226 18927 603 41 0 20185 0
vsize: 80904
[startup+60.0027 s]
Raw data (loadavg): 0.87 0.89 0.89 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 26856 0 0 0 5942 57 0 0 25 0 1 0 550724652 99889152 20372 4294967295 134512640 134672761 3221224544 3220193728 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24387 20372 603 41 0 24346 0
vsize: 97548
[startup+70.0061 s]
Raw data (loadavg): 0.89 0.89 0.89 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 28084 0 0 0 6941 59 0 0 25 0 1 0 550724652 103673856 21600 4294967295 134512640 134672761 3221224544 3220204480 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25311 21600 603 41 0 25270 0
vsize: 101244
[startup+80.0093 s]
Raw data (loadavg): 0.91 0.89 0.90 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 34474 0 0 0 7929 72 0 0 25 0 1 0 550724652 128786432 27990 4294967295 134512640 134672761 3221224544 3220294912 134523714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31442 27990 603 41 0 31401 0
vsize: 125768
[startup+90.0091 s]
Raw data (loadavg): 0.92 0.90 0.90 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 40767 0 0 0 8915 86 0 0 25 0 1 0 550724652 131891200 29009 4294967295 134512640 134672761 3221224544 3220272064 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32200 29009 603 41 0 32159 0
vsize: 128800
[startup+100.01 s]
Raw data (loadavg): 0.93 0.90 0.90 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 41812 0 0 0 9914 87 0 0 25 0 1 0 550724652 135135232 30054 4294967295 134512640 134672761 3221224544 3220291840 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32992 30054 603 41 0 32951 0
vsize: 131968
[startup+110.02 s]
Raw data (loadavg): 0.94 0.90 0.90 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 42835 0 0 0 10914 88 0 0 25 0 1 0 550724652 138244096 31077 4294967295 134512640 134672761 3221224544 3220247952 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33751 31077 603 41 0 33710 0
vsize: 135004
[startup+120.021 s]
Raw data (loadavg): 0.95 0.91 0.90 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 43824 0 0 0 11913 89 0 0 25 0 1 0 550724652 141352960 32066 4294967295 134512640 134672761 3221224544 3220265344 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34510 32066 603 41 0 34469 0
vsize: 138040
[startup+130.061 s]
Raw data (loadavg): 0.96 0.91 0.90 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 44821 0 0 0 12916 91 0 0 25 0 1 0 550724652 144326656 33063 4294967295 134512640 134672761 3221224544 3220382848 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35236 33063 603 41 0 35195 0
vsize: 140944
[startup+140.073 s]
Raw data (loadavg): 0.96 0.91 0.90 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 45705 0 0 0 13915 92 0 0 25 0 1 0 550724652 147165184 33947 4294967295 134512640 134672761 3221224544 3220285504 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35929 33947 603 41 0 35888 0
vsize: 143716
[startup+150.074 s]
Raw data (loadavg): 0.97 0.91 0.90 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 46547 0 0 0 14914 93 0 0 25 0 1 0 550724652 149733376 34789 4294967295 134512640 134672761 3221224544 3220240464 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36556 34790 603 41 0 36515 0
vsize: 146224
[startup+160.074 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 47387 0 0 0 15913 95 0 0 25 0 1 0 550724652 152301568 35629 4294967295 134512640 134672761 3221224544 3220302784 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37183 35629 603 41 0 37142 0
vsize: 148732
[startup+170.074 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 48143 0 0 0 16912 96 0 0 25 0 1 0 550724652 154599424 36385 4294967295 134512640 134672761 3221224544 3220246032 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37744 36385 603 41 0 37703 0
vsize: 150976
[startup+180.074 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 48936 0 0 0 17910 98 0 0 25 0 1 0 550724652 182198272 37178 4294967295 134512640 134672761 3221224544 3220290152 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44482 37178 603 41 0 44441 0
vsize: 177928
[startup+190.09 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 49705 0 0 0 18911 99 0 0 25 0 1 0 550724652 184631296 37947 4294967295 134512640 134672761 3221224544 3220282720 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45076 37947 603 41 0 45035 0
vsize: 180304
[startup+200.099 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 50424 0 0 0 19910 101 0 0 25 0 1 0 550724652 186793984 38666 4294967295 134512640 134672761 3221224544 3220300384 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45604 38666 603 41 0 45563 0
vsize: 182416
[startup+210.099 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 51125 0 0 0 20909 102 0 0 25 0 1 0 550724652 188956672 39367 4294967295 134512640 134672761 3221224544 3220284624 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46132 39367 603 41 0 46091 0
vsize: 184528
[startup+220.1 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 51824 0 0 0 21908 103 0 0 25 0 1 0 550724652 191119360 40066 4294967295 134512640 134672761 3221224544 3220265424 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46660 40066 603 41 0 46619 0
vsize: 186640
[startup+230.1 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 52510 0 0 0 22907 104 0 0 25 0 1 0 550724652 193282048 40752 4294967295 134512640 134672761 3221224544 3220284736 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47188 40752 603 41 0 47147 0
vsize: 188752
[startup+240.1 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 53169 0 0 0 23906 106 0 0 25 0 1 0 550724652 195309568 41411 4294967295 134512640 134672761 3221224544 3220375744 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47683 41411 603 41 0 47642 0
vsize: 190732
[startup+250.1 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 53792 0 0 0 24905 107 0 0 25 0 1 0 550724652 197201920 42034 4294967295 134512640 134672761 3221224544 3220346256 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48145 42034 603 41 0 48104 0
vsize: 192580
[startup+260.101 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 54392 0 0 0 25904 108 0 0 25 0 1 0 550724652 199094272 42634 4294967295 134512640 134672761 3221224544 3220407024 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48607 42634 603 41 0 48566 0
vsize: 194428
[startup+270.102 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 55037 0 0 0 26903 110 0 0 25 0 1 0 550724652 200986624 43279 4294967295 134512640 134672761 3221224544 3220735728 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49069 43279 603 41 0 49028 0
vsize: 196276
[startup+280.103 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 55605 0 0 0 27902 111 0 0 25 0 1 0 550724652 202743808 43847 4294967295 134512640 134672761 3221224544 3220363160 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49498 43847 603 41 0 49457 0
vsize: 197992
[startup+290.102 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 77035 0 0 0 28853 160 0 0 25 0 1 0 550724652 247021568 54731 4294967295 134512640 134672761 3221224544 3220423824 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60308 54731 603 41 0 60267 0
vsize: 241232
[startup+300.103 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 77575 0 0 0 29852 161 0 0 25 0 1 0 550724652 248643584 55271 4294967295 134512640 134672761 3221224544 3220309008 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60704 55271 603 41 0 60663 0
vsize: 242816
[startup+310.103 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 78115 0 0 0 30852 161 0 0 25 0 1 0 550724652 250400768 55811 4294967295 134512640 134672761 3221224544 3220290496 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61133 55811 603 41 0 61092 0
vsize: 244532
[startup+320.104 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 78628 0 0 0 31852 162 0 0 25 0 1 0 550724652 251887616 56324 4294967295 134512640 134672761 3221224544 3220386688 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61496 56324 603 41 0 61455 0
vsize: 245984
[startup+330.105 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 79147 0 0 0 32851 162 0 0 25 0 1 0 550724652 253509632 56843 4294967295 134512640 134672761 3221224544 3220408368 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61892 56843 603 41 0 61851 0
vsize: 247568
[startup+340.105 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 79721 0 0 0 33850 164 0 0 25 0 1 0 550724652 255266816 57417 4294967295 134512640 134672761 3221224544 3220320144 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62321 57417 603 41 0 62280 0
vsize: 249284
[startup+350.105 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 80207 0 0 0 34849 165 0 0 25 0 1 0 550724652 256753664 57903 4294967295 134512640 134672761 3221224544 3220336960 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62684 57903 603 41 0 62643 0
vsize: 250736
[startup+360.105 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 80707 0 0 0 35849 166 0 0 25 0 1 0 550724652 258375680 58403 4294967295 134512640 134672761 3221224544 3220406560 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63080 58403 603 41 0 63039 0
vsize: 252320
[startup+370.106 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 81166 0 0 0 36848 167 0 0 25 0 1 0 550724652 259727360 58862 4294967295 134512640 134672761 3221224544 3220382848 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63410 58862 603 41 0 63369 0
vsize: 253640
[startup+380.107 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 81659 0 0 0 37848 167 0 0 25 0 1 0 550724652 261349376 59355 4294967295 134512640 134672761 3221224544 3220387456 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63806 59355 603 41 0 63765 0
vsize: 255224
[startup+390.107 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 82088 0 0 0 38847 168 0 0 25 0 1 0 550724652 262565888 59784 4294967295 134512640 134672761 3221224544 3220345024 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64103 59784 603 41 0 64062 0
vsize: 256412
[startup+400.107 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 82567 0 0 0 39847 169 0 0 25 0 1 0 550724652 264052736 60263 4294967295 134512640 134672761 3221224544 3220333488 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64466 60263 603 41 0 64425 0
vsize: 257864
[startup+410.107 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 83121 0 0 0 40846 169 0 0 25 0 1 0 550724652 265809920 60817 4294967295 134512640 134672761 3221224544 3220339152 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64895 60817 603 41 0 64854 0
vsize: 259580
[startup+420.108 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 83618 0 0 0 41846 170 0 0 25 0 1 0 550724652 267296768 61314 4294967295 134512640 134672761 3221224544 3220461568 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65258 61314 603 41 0 65217 0
vsize: 261032
[startup+430.109 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 84098 0 0 0 42845 171 0 0 25 0 1 0 550724652 268783616 61794 4294967295 134512640 134672761 3221224544 3220404008 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65621 61794 603 41 0 65580 0
vsize: 262484
[startup+440.108 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 84614 0 0 0 43844 172 0 0 25 0 1 0 550724652 270405632 62310 4294967295 134512640 134672761 3221224544 3220428640 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66017 62310 603 41 0 65976 0
vsize: 264068
[startup+450.109 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 85078 0 0 0 44844 172 0 0 25 0 1 0 550724652 271892480 62774 4294967295 134512640 134672761 3221224544 3220364304 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66380 62774 603 41 0 66339 0
vsize: 265520
[startup+460.109 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 85540 0 0 0 45843 173 0 0 25 0 1 0 550724652 273244160 63236 4294967295 134512640 134672761 3221224544 3220476160 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66710 63236 603 41 0 66669 0
vsize: 266840
[startup+470.11 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 86037 0 0 0 46843 174 0 0 25 0 1 0 550724652 274731008 63733 4294967295 134512640 134672761 3221224544 3220342712 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67073 63733 603 41 0 67032 0
vsize: 268292
[startup+480.112 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 86475 0 0 0 47842 175 0 0 25 0 1 0 550724652 276082688 64171 4294967295 134512640 134672761 3221224544 3220401360 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67403 64171 603 41 0 67362 0
vsize: 269612
[startup+490.113 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 86930 0 0 0 48842 176 0 0 25 0 1 0 550724652 277569536 64626 4294967295 134512640 134672761 3221224544 3220504464 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67766 64626 603 41 0 67725 0
vsize: 271064
[startup+500.116 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 87404 0 0 0 49842 176 0 0 25 0 1 0 550724652 279056384 65100 4294967295 134512640 134672761 3221224544 3220449280 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68129 65100 603 41 0 68088 0
vsize: 272516
[startup+510.116 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 87816 0 0 0 50841 177 0 0 25 0 1 0 550724652 280272896 65512 4294967295 134512640 134672761 3221224544 3220375536 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68426 65512 603 41 0 68385 0
vsize: 273704
[startup+520.116 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 88404 0 0 0 51840 178 0 0 25 0 1 0 550724652 282030080 66100 4294967295 134512640 134672761 3221224544 3220778160 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68855 66100 603 41 0 68814 0
vsize: 275420
[startup+530.117 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 89314 0 0 0 52839 180 0 0 25 0 1 0 550724652 284868608 67010 4294967295 134512640 134672761 3221224544 3220549600 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69548 67010 603 41 0 69507 0
vsize: 278192
[startup+540.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 90182 0 0 0 53838 181 0 0 25 0 1 0 550724652 287571968 67878 4294967295 134512640 134672761 3221224544 3220377264 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70208 67878 603 41 0 70167 0
vsize: 280832
[startup+550.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 90979 0 0 0 54836 183 0 0 25 0 1 0 550724652 290004992 68675 4294967295 134512640 134672761 3221224544 3220599696 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70802 68675 603 41 0 70761 0
vsize: 283208
[startup+560.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 91773 0 0 0 55835 184 0 0 25 0 1 0 550724652 292438016 69469 4294967295 134512640 134672761 3221224544 3220600080 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71396 69469 603 41 0 71355 0
vsize: 285584
[startup+570.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 92495 0 0 0 56834 185 0 0 25 0 1 0 550724652 294735872 70191 4294967295 134512640 134672761 3221224544 3220512912 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71957 70191 603 41 0 71916 0
vsize: 287828
[startup+580.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 93166 0 0 0 57833 187 0 0 25 0 1 0 550724652 296763392 70862 4294967295 134512640 134672761 3221224544 3220380256 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72452 70862 603 41 0 72411 0
vsize: 289808
[startup+590.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 93881 0 0 0 58832 188 0 0 25 0 1 0 550724652 298926080 71577 4294967295 134512640 134672761 3221224544 3220421920 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72980 71577 603 41 0 72939 0
vsize: 291920
[startup+600.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 94549 0 0 0 59830 190 0 0 25 0 1 0 550724652 351420416 72245 4294967295 134512640 134672761 3221224544 3220674496 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85796 72245 603 41 0 85755 0
vsize: 343184
[startup+610.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 95184 0 0 0 60830 191 0 0 25 0 1 0 550724652 353312768 72880 4294967295 134512640 134672761 3221224544 3220409424 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86258 72880 603 41 0 86217 0
vsize: 345032
[startup+620.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 95796 0 0 0 61829 192 0 0 25 0 1 0 550724652 355205120 73492 4294967295 134512640 134672761 3221224544 3220543840 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86720 73492 603 41 0 86679 0
vsize: 346880
[startup+630.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 96425 0 0 0 62829 193 0 0 25 0 1 0 550724652 357097472 74121 4294967295 134512640 134672761 3221224544 3220531552 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87182 74121 603 41 0 87141 0
vsize: 348728
[startup+640.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 97039 0 0 0 63829 193 0 0 25 0 1 0 550724652 358989824 74735 4294967295 134512640 134672761 3221224544 3220671504 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87644 74735 603 41 0 87603 0
vsize: 350576
[startup+650.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 97793 0 0 0 64827 195 0 0 25 0 1 0 550724652 361422848 75489 4294967295 134512640 134672761 3221224544 3220553040 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88238 75489 603 41 0 88197 0
vsize: 352952
[startup+660.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 98824 0 0 0 65826 197 0 0 25 0 1 0 550724652 364531712 76520 4294967295 134512640 134672761 3221224544 3220683232 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88997 76520 603 41 0 88956 0
vsize: 355988
[startup+670.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 99806 0 0 0 66824 199 0 0 25 0 1 0 550724652 367505408 77502 4294967295 134512640 134672761 3221224544 3220425760 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89723 77502 603 41 0 89682 0
vsize: 358892
[startup+680.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 100692 0 0 0 67822 201 0 0 25 0 1 0 550724652 370343936 78388 4294967295 134512640 134672761 3221224544 3220593744 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90416 78388 603 41 0 90375 0
vsize: 361664
[startup+690.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 101533 0 0 0 68821 202 0 0 25 0 1 0 550724652 372912128 79229 4294967295 134512640 134672761 3221224544 3220562944 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91043 79229 603 41 0 91002 0
vsize: 364172
[startup+700.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 102366 0 0 0 69820 204 0 0 25 0 1 0 550724652 375480320 80062 4294967295 134512640 134672761 3221224544 3220466368 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91670 80062 603 41 0 91629 0
vsize: 366680
[startup+710.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 103156 0 0 0 70819 205 0 0 25 0 1 0 550724652 377913344 80852 4294967295 134512640 134672761 3221224544 3220606512 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92264 80852 603 41 0 92223 0
vsize: 369056
[startup+720.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 103861 0 0 0 71818 206 0 0 25 0 1 0 550724652 380076032 81557 4294967295 134512640 134672761 3221224544 3220453872 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92792 81557 603 41 0 92751 0
vsize: 371168
[startup+730.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 108398 0 0 0 72813 213 0 0 25 0 1 0 550724652 393998336 86094 4294967295 134512640 134672761 3221224544 3221000992 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96191 86094 603 41 0 96150 0
vsize: 384764
[startup+740.157 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 152024 0 0 0 73707 319 0 0 25 0 1 0 550724652 484843520 108628 4294967295 134512640 134672761 3221224544 3220500080 134522892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118370 108628 603 41 0 118329 0
vsize: 473480
[startup+750.158 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 156732 0 0 0 74701 325 0 0 25 0 1 0 550724652 499441664 113336 4294967295 134512640 134672761 3221224544 3220594660 134593035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121934 113336 603 41 0 121893 0
vsize: 487736
[startup+760.158 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 160052 0 0 0 75695 331 0 0 25 0 1 0 550724652 509714432 116656 4294967295 134512640 134672761 3221224544 3220534252 1075358820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124442 116656 603 41 0 124401 0
vsize: 497768
[startup+770.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 162431 0 0 0 76691 336 0 0 25 0 1 0 550724652 517013504 119035 4294967295 134512640 134672761 3221224544 3220896336 134594206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 126224 119036 603 41 0 126183 0
vsize: 504896
[startup+780.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 168678 0 0 0 77681 345 0 0 25 0 1 0 550724652 536207360 125282 4294967295 134512640 134672761 3221224544 3220756328 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130910 125282 603 41 0 130869 0
vsize: 523640
[startup+790.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 179224 0 0 0 78661 361 0 0 25 0 1 0 550724652 568782848 135828 4294967295 134512640 134672761 3221224544 3220783456 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138863 135828 603 41 0 138822 0
vsize: 555452
[startup+800.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 194411 0 0 0 79627 391 0 0 25 0 1 0 550724652 716214272 151015 4294967295 134512640 134672761 3221224544 3220749456 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 174857 151015 603 41 0 174816 0
vsize: 699428
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 2964
Raw data (stat): 2964 (minisat+) R 2963 18865 18864 0 -1 0 194411 0 0 0 79627 391 0 0 25 0 1 0 550724652 716214272 151015 4294967295 134512640 134672761 3221224544 3220749456 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 174857 151015 603 41 0 174816 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 810.024
CPU time (s): 809.975
CPU user time (s): 805.321
CPU system time (s): 4.65429
CPU usage (%): 99.9939
Max. virtual memory (Kb): 699428
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####