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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-fit1d.opb
MD5SUM	6bb160e5eb0ef9c02ca7232f62836f2b
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	8436
Biggest coefficient in the objective function	368640
Number of bits for the biggest coefficient in the objective function	19
Sum of the numbers in the objective function	57614442
Number of bits of the sum of numbers in the objective function	26
Biggest number in a constraint	483840
Number of bits of the biggest number in a constraint	19
Biggest sum of numbers in a constraint	72412534
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1195.48
Number of variables	8436
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	8
Maximum length of a constraint	8436
Trace number 16214

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        896872 kB
Buffers:         12892 kB
Cached:         102164 kB
SwapCached:          0 kB
Active:          15684 kB
Inactive:       102260 kB
HighTotal:      131008 kB
HighFree:        73668 kB
LowTotal:       903652 kB
LowFree:        823204 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14036 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 06:47:13 (client local time) WITH STATUS 0 IN 1200.38 SECONDS
stats: 15780 7 1200.38 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:    7
c ---[1049]---> BDD-cost:    7
c ---[1048]---> BDD-cost:    7
c ---[1047]---> BDD-cost:    7
c ---[1046]---> BDD-cost:    7
c ---[1045]---> BDD-cost:    7
c ---[1044]---> BDD-cost:    7
c ---[1043]---> BDD-cost:    7
c ---[1042]---> BDD-cost:    7
c ---[1041]---> BDD-cost:    7
c ---[1040]---> BDD-cost:    7
c ---[1039]---> BDD-cost:    7
c ---[1038]---> BDD-cost:    7
c ---[1037]---> BDD-cost:    7
c ---[1036]---> BDD-cost:    7
c ---[1035]---> BDD-cost:    7
c ---[1034]---> BDD-cost:    7
c ---[1033]---> BDD-cost:    7
c ---[1032]---> BDD-cost:    7
c ---[1031]---> BDD-cost:    7
c ---[1030]---> BDD-cost:    7
c ---[1029]---> BDD-cost:    7
c ---[1028]---> BDD-cost:    7
c ---[1027]---> BDD-cost:    7
c ---[1026]---> BDD-cost:    7
c ---[1025]---> BDD-cost:    7
c ---[1024]---> BDD-cost:    7
c ---[1023]---> BDD-cost:    7
c ---[1022]---> BDD-cost:    7
c ---[1021]---> BDD-cost:    7
c ---[1020]---> BDD-cost:    7
c ---[1019]---> BDD-cost:    7
c ---[1018]---> BDD-cost:    7
c ---[1017]---> BDD-cost:    7
c ---[1016]---> BDD-cost:    7
c ---[1015]---> BDD-cost:    7
c ---[1014]---> BDD-cost:    7
c ---[1013]---> BDD-cost:    7
c ---[1012]---> BDD-cost:    7
c ---[1011]---> BDD-cost:    7
c ---[1010]---> BDD-cost:    7
c ---[1009]---> BDD-cost:    7
c ---[1008]---> BDD-cost:    7
c ---[1007]---> BDD-cost:    7
c ---[1006]---> BDD-cost:    7
c ---[1005]---> BDD-cost:    7
c ---[1004]---> BDD-cost:    7
c ---[1003]---> BDD-cost:    7
c ---[1002]---> BDD-cost:    7
c ---[1001]---> BDD-cost:    7
c ---[1000]---> BDD-cost:    7
c ---[ 999]---> BDD-cost:    7
c ---[ 998]---> BDD-cost:    7
c ---[ 997]---> BDD-cost:    7
c ---[ 996]---> BDD-cost:    7
c ---[ 995]---> BDD-cost:    7
c ---[ 994]---> BDD-cost:    7
c ---[ 993]---> BDD-cost:    7
c ---[ 992]---> BDD-cost:    7
c ---[ 991]---> BDD-cost:    7
c ---[ 990]---> BDD-cost:    7
c ---[ 989]---> BDD-cost:    7
c ---[ 988]---> BDD-cost:    7
c ---[ 987]---> BDD-cost:    7
c ---[ 986]---> BDD-cost:    7
c ---[ 985]---> BDD-cost:    7
c ---[ 984]---> BDD-cost:    7
c ---[ 983]---> BDD-cost:    7
c ---[ 982]---> BDD-cost:    7
c ---[ 981]---> BDD-cost:    7
c ---[ 980]---> BDD-cost:    7
c ---[ 979]---> BDD-cost:    7
c ---[ 978]---> BDD-cost:    7
c ---[ 977]---> BDD-cost:    7
c ---[ 976]---> BDD-cost:    7
c ---[ 975]---> BDD-cost:    7
c ---[ 974]---> BDD-cost:    7
c ---[ 973]---> BDD-cost:    7
c ---[ 972]---> BDD-cost:    7
c ---[ 971]---> BDD-cost:    7
c ---[ 970]---> BDD-cost:    7
c ---[ 969]---> BDD-cost:    7
c ---[ 968]---> BDD-cost:    7
c ---[ 967]---> BDD-cost:    7
c ---[ 966]---> BDD-cost:    7
c ---[ 965]---> BDD-cost:    7
c ---[ 964]---> BDD-cost:    7
c ---[ 963]---> BDD-cost:    7
c ---[ 962]---> BDD-cost:    7
c ---[ 961]---> BDD-cost:    7
c ---[ 960]---> BDD-cost:    7
c ---[ 959]---> BDD-cost:    7
c ---[ 958]---> BDD-cost:    7
c ---[ 957]---> BDD-cost:    7
c ---[ 956]---> BDD-cost:    7
c ---[ 955]---> BDD-cost:    7
c ---[ 954]---> BDD-cost:    7
c ---[ 953]---> BDD-cost:    7
c ---[ 952]---> BDD-cost:    7
c ---[ 951]---> BDD-cost:    7
c ---[ 950]---> BDD-cost:    7
c ---[ 949]---> BDD-cost:    7
c ---[ 948]---> BDD-cost:    7
c ---[ 947]---> BDD-cost:    7
c ---[ 946]---> BDD-cost:    7
c ---[ 945]---> BDD-cost:    7
c ---[ 944]---> BDD-cost:    7
c ---[ 943]---> BDD-cost:    7
c ---[ 942]---> BDD-cost:    7
c ---[ 941]---> BDD-cost:    7
c ---[ 940]---> BDD-cost:    7
c ---[ 939]---> BDD-cost:    7
c ---[ 938]---> BDD-cost:    7
c ---[ 937]---> BDD-cost:    7
c ---[ 936]---> BDD-cost:    7
c ---[ 935]---> BDD-cost:    7
c ---[ 934]---> BDD-cost:    7
c ---[ 933]---> BDD-cost:    7
c ---[ 932]---> BDD-cost:    7
c ---[ 931]---> BDD-cost:    7
c ---[ 930]---> BDD-cost:    7
c ---[ 929]---> BDD-cost:    7
c ---[ 928]---> BDD-cost:    7
c ---[ 927]---> BDD-cost:    7
c ---[ 926]---> BDD-cost:    7
c ---[ 925]---> BDD-cost:    7
c ---[ 924]---> BDD-cost:    7
c ---[ 923]---> BDD-cost:    7
c ---[ 922]---> BDD-cost:    7
c ---[ 921]---> BDD-cost:    7
c ---[ 920]---> BDD-cost:    7
c ---[ 919]---> BDD-cost:    7
c ---[ 918]---> BDD-cost:    7
c ---[ 917]---> BDD-cost:    7
c ---[ 916]---> BDD-cost:    7
c ---[ 915]---> BDD-cost:    7
c ---[ 914]---> BDD-cost:    7
c ---[ 913]---> BDD-cost:    7
c ---[ 912]---> BDD-cost:    7
c ---[ 911]---> BDD-cost:    7
c ---[ 910]---> BDD-cost:    7
c ---[ 909]---> BDD-cost:    7
c ---[ 908]---> BDD-cost:    7
c ---[ 907]---> BDD-cost:    7
c ---[ 906]---> BDD-cost:    7
c ---[ 905]---> BDD-cost:    7
c ---[ 904]---> BDD-cost:    7
c ---[ 903]---> BDD-cost:    7
c ---[ 902]---> BDD-cost:    7
c ---[ 901]---> BDD-cost:    7
c ---[ 900]---> BDD-cost:    7
c ---[ 899]---> BDD-cost:    7
c ---[ 898]---> BDD-cost:    7
c ---[ 897]---> BDD-cost:    7
c ---[ 896]---> BDD-cost:    7
c ---[ 895]---> BDD-cost:    7
c ---[ 894]---> BDD-cost:    7
c ---[ 893]---> BDD-cost:    7
c ---[ 892]---> BDD-cost:    7
c ---[ 891]---> BDD-cost:    7
c ---[ 890]---> BDD-cost:    7
c ---[ 889]---> BDD-cost:    7
c ---[ 888]---> BDD-cost:    7
c ---[ 887]---> BDD-cost:    7
c ---[ 886]---> BDD-cost:    7
c ---[ 885]---> BDD-cost:    7
c ---[ 884]---> BDD-cost:    7
c ---[ 883]---> BDD-cost:    7
c ---[ 882]---> BDD-cost:    7
c ---[ 881]---> BDD-cost:    7
c ---[ 880]---> BDD-cost:    7
c ---[ 879]---> BDD-cost:    7
c ---[ 878]---> BDD-cost:    7
c ---[ 877]---> BDD-cost:    7
c ---[ 876]---> BDD-cost:    7
c ---[ 875]---> BDD-cost:    7
c ---[ 874]---> BDD-cost:    7
c ---[ 873]---> BDD-cost:    7
c ---[ 872]---> BDD-cost:    7
c ---[ 871]---> BDD-cost:    7
c ---[ 870]---> BDD-cost:    7
c ---[ 869]---> BDD-cost:    7
c ---[ 868]---> BDD-cost:    7
c ---[ 867]---> BDD-cost:    7
c ---[ 866]---> BDD-cost:    7
c ---[ 865]---> BDD-cost:    7
c ---[ 864]---> BDD-cost:    7
c ---[ 863]---> BDD-cost:    7
c ---[ 862]---> BDD-cost:    7
c ---[ 861]---> BDD-cost:    7
c ---[ 860]---> BDD-cost:    7
c ---[ 859]---> BDD-cost:    7
c ---[ 858]---> BDD-cost:    7
c ---[ 857]---> BDD-cost:    7
c ---[ 856]---> BDD-cost:    7
c ---[ 855]---> BDD-cost:    7
c ---[ 854]---> BDD-cost:    7
c ---[ 853]---> BDD-cost:    7
c ---[ 852]---> BDD-cost:    7
c ---[ 851]---> BDD-cost:    7
c ---[ 850]---> BDD-cost:    7
c ---[ 849]---> BDD-cost:    7
c ---[ 848]---> BDD-cost:    7
c ---[ 847]---> BDD-cost:    7
c ---[ 846]---> BDD-cost:    7
c ---[ 845]---> BDD-cost:    7
c ---[ 844]---> BDD-cost:    7
c ---[ 843]---> BDD-cost:    7
c ---[ 842]---> BDD-cost:    7
c ---[ 841]---> BDD-cost:    7
c ---[ 840]---> BDD-cost:    7
c ---[ 839]---> BDD-cost:    7
c ---[ 838]---> BDD-cost:    7
c ---[ 837]---> BDD-cost:    7
c ---[ 836]---> BDD-cost:    7
c ---[ 835]---> BDD-cost:    7
c ---[ 834]---> BDD-cost:    7
c ---[ 833]---> BDD-cost:    7
c ---[ 832]---> BDD-cost:    7
c ---[ 831]---> BDD-cost:    7
c ---[ 830]---> BDD-cost:    7
c ---[ 829]---> BDD-cost:    7
c ---[ 828]---> BDD-cost:    7
c ---[ 827]---> BDD-cost:    7
c ---[ 826]---> BDD-cost:    7
c ---[ 825]---> BDD-cost:    7
c ---[ 824]---> BDD-cost:    7
c ---[ 823]---> BDD-cost:    7
c ---[ 822]---> BDD-cost:    7
c ---[ 821]---> BDD-cost:    7
c ---[ 820]---> BDD-cost:    7
c ---[ 819]---> BDD-cost:    7
c ---[ 818]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:    7
c ---[ 816]---> BDD-cost:    7
c ---[ 815]---> BDD-cost:    7
c ---[ 814]---> BDD-cost:    7
c ---[ 813]---> BDD-cost:    7
c ---[ 812]---> BDD-cost:    7
c ---[ 811]---> BDD-cost:    7
c ---[ 810]---> BDD-cost:    7
c ---[ 809]---> BDD-cost:    7
c ---[ 808]---> BDD-cost:    7
c ---[ 807]---> BDD-cost:    7
c ---[ 806]---> BDD-cost:    7
c ---[ 805]---> BDD-cost:    7
c ---[ 804]---> BDD-cost:    7
c ---[ 803]---> BDD-cost:    7
c ---[ 802]---> BDD-cost:    7
c ---[ 801]---> BDD-cost:    7
c ---[ 800]---> BDD-cost:    7
c ---[ 799]---> BDD-cost:    7
c ---[ 798]---> BDD-cost:    7
c ---[ 797]---> BDD-cost:    7
c ---[ 796]---> BDD-cost:    7
c ---[ 795]---> BDD-cost:    7
c ---[ 794]---> BDD-cost:    7
c ---[ 793]---> BDD-cost:    7
c ---[ 792]---> BDD-cost:    7
c ---[ 791]---> BDD-cost:    7
c ---[ 790]---> BDD-cost:    7
c ---[ 789]---> BDD-cost:    7
c ---[ 788]---> BDD-cost:    7
c ---[ 787]---> BDD-cost:    7
c ---[ 786]---> BDD-cost:    7
c ---[ 785]---> BDD-cost:    7
c ---[ 784]---> BDD-cost:    7
c ---[ 783]---> BDD-cost:    7
c ---[ 782]---> BDD-cost:    7
c ---[ 781]---> BDD-cost:    7
c ---[ 780]---> BDD-cost:    7
c ---[ 779]---> BDD-cost:    7
c ---[ 778]---> BDD-cost:    7
c ---[ 777]---> BDD-cost:    7
c ---[ 776]---> BDD-cost:    7
c ---[ 775]---> BDD-cost:    7
c ---[ 774]---> BDD-cost:    7
c ---[ 773]---> BDD-cost:    7
c ---[ 772]---> BDD-cost:    7
c ---[ 771]---> BDD-cost:    7
c ---[ 770]---> BDD-cost:    7
c ---[ 769]---> BDD-cost:    7
c ---[ 768]---> BDD-cost:    7
c ---[ 767]---> BDD-cost:    7
c ---[ 766]---> BDD-cost:    7
c ---[ 765]---> BDD-cost:    7
c ---[ 764]---> BDD-cost:    7
c ---[ 763]---> BDD-cost:    7
c ---[ 762]---> BDD-cost:    7
c ---[ 761]---> BDD-cost:    7
c ---[ 760]---> BDD-cost:    7
c ---[ 759]---> BDD-cost:    7
c ---[ 758]---> BDD-cost:    7
c ---[ 757]---> BDD-cost:    7
c ---[ 756]---> BDD-cost:    7
c ---[ 755]---> BDD-cost:    7
c ---[ 754]---> BDD-cost:    7
c ---[ 753]---> BDD-cost:    7
c ---[ 752]---> BDD-cost:    7
c ---[ 751]---> BDD-cost:    7
c ---[ 750]---> BDD-cost:    7
c ---[ 749]---> BDD-cost:    7
c ---[ 748]---> BDD-cost:    7
c ---[ 747]---> BDD-cost:    7
c ---[ 746]---> BDD-cost:    7
c ---[ 745]---> BDD-cost:    7
c ---[ 744]---> BDD-cost:    7
c ---[ 743]---> BDD-cost:    7
c ---[ 742]---> BDD-cost:    7
c ---[ 741]---> BDD-cost:    7
c ---[ 740]---> BDD-cost:    7
c ---[ 739]---> BDD-cost:    7
c ---[ 738]---> BDD-cost:    7
c ---[ 737]---> BDD-cost:    7
c ---[ 736]---> BDD-cost:    7
c ---[ 735]---> BDD-cost:    7
c ---[ 734]---> BDD-cost:    7
c ---[ 733]---> BDD-cost:    7
c ---[ 732]---> BDD-cost:    7
c ---[ 731]---> BDD-cost:    7
c ---[ 730]---> BDD-cost:    7
c ---[ 729]---> BDD-cost:    7
c ---[ 728]---> BDD-cost:    7
c ---[ 727]---> BDD-cost:    7
c ---[ 726]---> BDD-cost:    7
c ---[ 725]---> BDD-cost:    7
c ---[ 724]---> BDD-cost:    7
c ---[ 723]---> BDD-cost:    7
c ---[ 722]---> BDD-cost:    7
c ---[ 721]---> BDD-cost:    7
c ---[ 720]---> BDD-cost:    7
c ---[ 719]---> BDD-cost:    7
c ---[ 718]---> BDD-cost:    7
c ---[ 717]---> BDD-cost:    7
c ---[ 716]---> BDD-cost:    7
c ---[ 715]---> BDD-cost:    7
c ---[ 714]---> BDD-cost:    7
c ---[ 713]---> BDD-cost:    7
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    7
c ---[ 710]---> BDD-cost:    7
c ---[ 709]---> BDD-cost:    7
c ---[ 708]---> BDD-cost:    7
c ---[ 707]---> BDD-cost:    7
c ---[ 706]---> BDD-cost:    7
c ---[ 705]---> BDD-cost:    7
c ---[ 704]---> BDD-cost:    7
c ---[ 703]---> BDD-cost:    7
c ---[ 702]---> BDD-cost:    7
c ---[ 701]---> BDD-cost:    7
c ---[ 700]---> BDD-cost:    7
c ---[ 699]---> BDD-cost:    7
c ---[ 698]---> BDD-cost:    7
c ---[ 697]---> BDD-cost:    7
c ---[ 696]---> BDD-cost:    7
c ---[ 695]---> BDD-cost:    7
c ---[ 694]---> BDD-cost:    7
c ---[ 693]---> BDD-cost:    7
c ---[ 692]---> BDD-cost:    7
c ---[ 691]---> BDD-cost:    7
c ---[ 690]---> BDD-cost:    7
c ---[ 689]---> BDD-cost:    7
c ---[ 688]---> BDD-cost:    7
c ---[ 687]---> BDD-cost:    7
c ---[ 686]---> BDD-cost:    7
c ---[ 685]---> BDD-cost:    7
c ---[ 684]---> BDD-cost:    7
c ---[ 683]---> BDD-cost:    7
c ---[ 682]---> BDD-cost:    7
c ---[ 681]---> BDD-cost:    7
c ---[ 680]---> BDD-cost:    7
c ---[ 679]---> BDD-cost:    7
c ---[ 678]---> BDD-cost:    7
c ---[ 677]---> BDD-cost:    7
c ---[ 676]---> BDD-cost:    7
c ---[ 675]---> BDD-cost:    7
c ---[ 674]---> BDD-cost:    7
c ---[ 673]---> BDD-cost:    7
c ---[ 672]---> BDD-cost:    7
c ---[ 671]---> BDD-cost:    7
c ---[ 670]---> BDD-cost:    7
c ---[ 669]---> BDD-cost:    7
c ---[ 668]---> BDD-cost:    7
c ---[ 667]---> BDD-cost:    7
c ---[ 666]---> BDD-cost:    7
c ---[ 665]---> BDD-cost:    7
c ---[ 664]---> BDD-cost:    7
c ---[ 663]---> BDD-cost:    7
c ---[ 662]---> BDD-cost:    7
c ---[ 661]---> BDD-cost:    7
c ---[ 660]---> BDD-cost:    7
c ---[ 659]---> BDD-cost:    7
c ---[ 658]---> BDD-cost:    7
c ---[ 657]---> BDD-cost:    7
c ---[ 656]---> BDD-cost:    7
c ---[ 655]---> BDD-cost:    7
c ---[ 654]---> BDD-cost:    7
c ---[ 653]---> BDD-cost:    7
c ---[ 652]---> BDD-cost:    7
c ---[ 651]---> BDD-cost:    7
c ---[ 650]---> BDD-cost:    7
c ---[ 649]---> BDD-cost:    7
c ---[ 648]---> BDD-cost:    7
c ---[ 647]---> BDD-cost:    7
c ---[ 646]---> BDD-cost:    7
c ---[ 645]---> BDD-cost:    7
c ---[ 644]---> BDD-cost:    7
c ---[ 643]---> BDD-cost:    7
c ---[ 642]---> BDD-cost:    7
c ---[ 641]---> BDD-cost:    7
c ---[ 640]---> BDD-cost:    7
c ---[ 639]---> BDD-cost:    7
c ---[ 638]---> BDD-cost:    7
c ---[ 637]---> BDD-cost:    7
c ---[ 636]---> BDD-cost:    7
c ---[ 635]---> BDD-cost:    7
c ---[ 634]---> BDD-cost:    7
c ---[ 633]---> BDD-cost:    7
c ---[ 632]---> BDD-cost:    7
c ---[ 631]---> BDD-cost:    7
c ---[ 630]---> BDD-cost:    7
c ---[ 629]---> BDD-cost:    7
c ---[ 628]---> BDD-cost:    7
c ---[ 627]---> BDD-cost:    7
c ---[ 626]---> BDD-cost:    7
c ---[ 625]---> BDD-cost:    7
c ---[ 624]---> BDD-cost:    7
c ---[ 623]---> BDD-cost:    7
c ---[ 622]---> BDD-cost:    7
c ---[ 621]---> BDD-cost:    7
c ---[ 620]---> BDD-cost:    7
c ---[ 619]---> BDD-cost:    7
c ---[ 618]---> BDD-cost:    7
c ---[ 617]---> BDD-cost:    7
c ---[ 616]---> BDD-cost:    7
c ---[ 615]---> BDD-cost:    7
c ---[ 614]---> BDD-cost:    7
c ---[ 613]---> BDD-cost:    7
c ---[ 612]---> BDD-cost:    7
c ---[ 611]---> BDD-cost:    7
c ---[ 610]---> BDD-cost:    7
c ---[ 609]---> BDD-cost:    7
c ---[ 608]---> BDD-cost:    7
c ---[ 607]---> BDD-cost:    7
c ---[ 606]---> BDD-cost:    7
c ---[ 605]---> BDD-cost:    7
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:    7
c ---[ 602]---> BDD-cost:    7
c ---[ 601]---> BDD-cost:    7
c ---[ 600]---> BDD-cost:    7
c ---[ 599]---> BDD-cost:    7
c ---[ 598]---> BDD-cost:    7
c ---[ 597]---> BDD-cost:    7
c ---[ 596]---> BDD-cost:    7
c ---[ 595]---> BDD-cost:    7
c ---[ 594]---> BDD-cost:    7
c ---[ 593]---> BDD-cost:    7
c ---[ 592]---> BDD-cost:    7
c ---[ 591]---> BDD-cost:    7
c ---[ 590]---> BDD-cost:    7
c ---[ 589]---> BDD-cost:    7
c ---[ 588]---> BDD-cost:    7
c ---[ 587]---> BDD-cost:    7
c ---[ 586]---> BDD-cost:    7
c ---[ 585]---> BDD-cost:    7
c ---[ 584]---> BDD-cost:    7
c ---[ 583]---> BDD-cost:    7
c ---[ 582]---> BDD-cost:    7
c ---[ 581]---> BDD-cost:    7
c ---[ 580]---> BDD-cost:    7
c ---[ 579]---> BDD-cost:    7
c ---[ 578]---> BDD-cost:    7
c ---[ 577]---> BDD-cost:    7
c ---[ 576]---> BDD-cost:    7
c ---[ 575]---> BDD-cost:    7
c ---[ 574]---> BDD-cost:    7
c ---[ 573]---> BDD-cost:    7
c ---[ 572]---> BDD-cost:    7
c ---[ 571]---> BDD-cost:    7
c ---[ 570]---> BDD-cost:    7
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:    7
c ---[ 567]---> BDD-cost:    7
c ---[ 566]---> BDD-cost:    7
c ---[ 565]---> BDD-cost:    7
c ---[ 564]---> BDD-cost:    7
c ---[ 563]---> BDD-cost:    7
c ---[ 562]---> BDD-cost:    7
c ---[ 561]---> BDD-cost:    7
c ---[ 560]---> BDD-cost:    7
c ---[ 559]---> BDD-cost:    7
c ---[ 558]---> BDD-cost:    7
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    7
c ---[ 554]---> BDD-cost:    7
c ---[ 553]---> BDD-cost:    7
c ---[ 552]---> BDD-cost:    7
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    7
c ---[ 549]---> BDD-cost:    7
c ---[ 548]---> BDD-cost:    7
c ---[ 547]---> BDD-cost:    7
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    7
c ---[ 544]---> BDD-cost:    7
c ---[ 543]---> BDD-cost:    7
c ---[ 542]---> BDD-cost:    7
c ---[ 541]---> BDD-cost:    7
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    7
c ---[ 538]---> BDD-cost:    7
c ---[ 537]---> BDD-cost:    7
c ---[ 536]---> BDD-cost:    7
c ---[ 535]---> BDD-cost:    7
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:    7
c ---[ 532]---> BDD-cost:    7
c ---[ 531]---> BDD-cost:    7
c ---[ 530]---> BDD-cost:    7
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:    7
c ---[ 525]---> BDD-cost:    7
c ---[ 524]---> BDD-cost:    7
c ---[ 523]---> BDD-cost:    7
c ---[ 522]---> BDD-cost:    7
c ---[ 521]---> BDD-cost:    7
c ---[ 520]---> BDD-cost:    7
c ---[ 519]---> BDD-cost:    7
c ---[ 518]---> BDD-cost:    7
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    7
c ---[ 515]---> BDD-cost:    7
c ---[ 514]---> BDD-cost:    7
c ---[ 513]---> BDD-cost:    7
c ---[ 512]---> BDD-cost:    7
c ---[ 511]---> BDD-cost:    7
c ---[ 510]---> BDD-cost:    7
c ---[ 509]---> BDD-cost:    7
c ---[ 508]---> BDD-cost:    7
c ---[ 507]---> BDD-cost:    7
c ---[ 506]---> BDD-cost:    7
c ---[ 505]---> BDD-cost:    7
c ---[ 504]---> BDD-cost:    7
c ---[ 503]---> BDD-cost:    7
c ---[ 502]---> BDD-cost:    7
c ---[ 501]---> BDD-cost:    7
c ---[ 500]---> BDD-cost:    7
c ---[ 499]---> BDD-cost:    7
c ---[ 498]---> BDD-cost:    7
c ---[ 497]---> BDD-cost:    7
c ---[ 496]---> BDD-cost:    7
c ---[ 495]---> BDD-cost:    7
c ---[ 494]---> BDD-cost:    7
c ---[ 493]---> BDD-cost:    7
c ---[ 492]---> BDD-cost:    7
c ---[ 491]---> BDD-cost:    7
c ---[ 490]---> BDD-cost:    7
c ---[ 489]---> BDD-cost:    7
c ---[ 488]---> BDD-cost:    7
c ---[ 487]---> BDD-cost:    7
c ---[ 486]---> BDD-cost:    7
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:    7
c ---[ 475]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 470]---> BDD-cost:    7
c ---[ 469]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 464]---> BDD-cost:    7
c ---[ 463]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 456]---> BDD-cost:    7
c ---[ 455]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 449]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 443]---> BDD-cost:    7
c ---[ 442]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 438]---> BDD-cost:    7
c ---[ 437]---> BDD-cost:    7
c ---[ 436]---> BDD-cost:    7
c ---[ 435]---> BDD-cost:    7
c ---[ 434]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 432]---> BDD-cost:    7
c ---[ 431]---> BDD-cost:    7
c ---[ 430]---> BDD-cost:    7
c ---[ 429]---> BDD-cost:    7
c ---[ 428]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 426]---> BDD-cost:    7
c ---[ 425]---> BDD-cost:    7
c ---[ 424]---> BDD-cost:    7
c ---[ 423]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 420]---> BDD-cost:    7
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    7
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 414]---> BDD-cost:    7
c ---[ 413]---> BDD-cost:    7
c ---[ 412]---> BDD-cost:    7
c ---[ 411]---> BDD-cost:    7
c ---[ 410]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 407]---> BDD-cost:    7
c ---[ 406]---> BDD-cost:    7
c ---[ 405]---> BDD-cost:    7
c ---[ 404]---> BDD-cost:    7
c ---[ 403]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 401]---> BDD-cost:    7
c ---[ 400]---> BDD-cost:    7
c ---[ 399]---> BDD-cost:    7
c ---[ 398]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 395]---> BDD-cost:    7
c ---[ 394]---> BDD-cost:    7
c ---[ 393]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 389]---> BDD-cost:    7
c ---[ 388]---> BDD-cost:    7
c ---[ 387]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 383]---> BDD-cost:    7
c ---[ 382]---> BDD-cost:    7
c ---[ 381]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 377]---> BDD-cost:    7
c ---[ 376]---> BDD-cost:    7
c ---[ 375]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 371]---> BDD-cost:    7
c ---[ 370]---> BDD-cost:    7
c ---[ 369]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 363]---> BDD-cost:    7
c ---[ 362]---> BDD-cost:    7
c ---[ 361]---> BDD-cost:    7
c ---[ 360]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    7
c ---[ 357]---> BDD-cost:    7
c ---[ 356]---> BDD-cost:    7
c ---[ 355]---> BDD-cost:    7
c ---[ 354]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 352]---> BDD-cost:    7
c ---[ 351]---> BDD-cost:    7
c ---[ 350]---> BDD-cost:    7
c ---[ 349]---> BDD-cost:    7
c ---[ 348]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 346]---> BDD-cost:    7
c ---[ 345]---> BDD-cost:    7
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:    7
c ---[ 342]---> BDD-cost:    7
c ---[ 341]---> BDD-cost:    7
c ---[ 340]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    7
c ---[ 336]---> BDD-cost:    7
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 332]---> BDD-cost:    7
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:    7
c ---[ 329]---> BDD-cost:    7
c ---[ 328]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 326]---> BDD-cost:    7
c ---[ 325]---> BDD-cost:    7
c ---[ 324]---> BDD-cost:    7
c ---[ 323]---> BDD-cost:    7
c ---[ 322]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 320]---> BDD-cost:    7
c ---[ 319]---> BDD-cost:    7
c ---[ 318]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:    7
c ---[ 316]---> BDD-cost:    7
c ---[ 315]---> BDD-cost:    7
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:    7
c ---[ 312]---> BDD-cost:    7
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    7
c ---[ 309]---> BDD-cost:    7
c ---[ 308]---> BDD-cost:    7
c ---[ 307]---> BDD-cost:    7
c ---[ 306]---> BDD-cost:    7
c ---[ 305]---> BDD-cost:    7
c ---[ 304]---> BDD-cost:    7
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:    7
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    7
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:    7
c ---[ 297]---> BDD-cost:    7
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    7
c ---[ 294]---> BDD-cost:    7
c ---[ 293]---> BDD-cost:    7
c ---[ 292]---> BDD-cost:    7
c ---[ 291]---> BDD-cost:    7
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    7
c ---[ 288]---> BDD-cost:    7
c ---[ 287]---> BDD-cost:    7
c ---[ 286]---> BDD-cost:    7
c ---[ 285]---> BDD-cost:    7
c ---[ 284]---> BDD-cost:    7
c ---[ 283]---> BDD-cost:    7
c ---[ 282]---> BDD-cost:    7
c ---[ 281]---> BDD-cost:    7
c ---[ 280]---> BDD-cost:    7
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    7
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    7
c ---[ 275]---> BDD-cost:    7
c ---[ 274]---> BDD-cost:    7
c ---[ 273]---> BDD-cost:    7
c ---[ 272]---> BDD-cost:    7
c ---[ 271]---> BDD-cost:    7
c ---[ 270]---> BDD-cost:    7
c ---[ 269]---> BDD-cost:    7
c ---[ 268]---> BDD-cost:    7
c ---[ 267]---> BDD-cost:    7
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    7
c ---[ 264]---> BDD-cost:    7
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    7
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:    7
c ---[ 259]---> BDD-cost:    7
c ---[ 258]---> BDD-cost:    7
c ---[ 257]---> BDD-cost:    7
c ---[ 256]---> BDD-cost:    7
c ---[ 255]---> BDD-cost:    7
c ---[ 254]---> BDD-cost:    7
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:    8
c ---[ 251]---> BDD-cost:    8
c ---[ 250]---> BDD-cost:    8
c ---[ 249]---> BDD-cost:    8
c ---[ 248]---> BDD-cost:    8
c ---[ 247]---> BDD-cost:    8
c ---[ 246]---> BDD-cost:    8
c ---[ 245]---> BDD-cost:    8
c ---[ 244]---> BDD-cost:    8
c ---[ 243]---> BDD-cost:    8
c ---[ 242]---> BDD-cost:    8
c ---[ 241]---> BDD-cost:    8
c ---[ 240]---> BDD-cost:    8
c ---[ 239]---> BDD-cost:    8
c ---[ 238]---> BDD-cost:    8
c ---[ 237]---> BDD-cost:    8
c ---[ 236]---> BDD-cost:    8
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:    8
c ---[ 233]---> BDD-cost:    8
c ---[ 232]---> BDD-cost:    8
c ---[ 231]---> BDD-cost:    8
c ---[ 230]---> BDD-cost:    8
c ---[ 229]---> BDD-cost:    8
c ---[ 228]---> BDD-cost:    8
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    8
c ---[ 225]---> BDD-cost:    8
c ---[ 224]---> BDD-cost:    8
c ---[ 223]---> BDD-cost:    8
c ---[ 222]---> BDD-cost:    8
c ---[ 221]---> BDD-cost:    8
c ---[ 220]---> BDD-cost:    8
c ---[ 219]---> BDD-cost:    8
c ---[ 218]---> BDD-cost:    8
c ---[ 217]---> BDD-cost:    8
c ---[ 216]---> BDD-cost:    8
c ---[ 215]---> BDD-cost:    8
c ---[ 214]---> BDD-cost:    8
c ---[ 213]---> BDD-cost:    8
c ---[ 212]---> BDD-cost:    8
c ---[ 211]---> BDD-cost:    8
c ---[ 210]---> BDD-cost:    8
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    8
c ---[ 207]---> BDD-cost:    8
c ---[ 206]---> BDD-cost:    8
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    8
c ---[ 203]---> BDD-cost:    8
c ---[ 202]---> BDD-cost:    8
c ---[ 201]---> BDD-cost:    8
c ---[ 200]---> BDD-cost:    8
c ---[ 199]---> BDD-cost:    8
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:    8
c ---[ 196]---> BDD-cost:    8
c ---[ 195]---> BDD-cost:    8
c ---[ 194]---> BDD-cost:    8
c ---[ 193]---> BDD-cost:    8
c ---[ 192]---> BDD-cost:    8
c ---[ 191]---> BDD-cost:    8
c ---[ 190]---> BDD-cost:    8
c ---[ 189]---> BDD-cost:    8
c ---[ 188]---> BDD-cost:    8
c ---[ 187]---> BDD-cost:    8
c ---[ 186]---> BDD-cost:    8
c ---[ 185]---> BDD-cost:    8
c ---[ 184]---> BDD-cost:    8
c ---[ 183]---> BDD-cost:    8
c ---[ 182]---> BDD-cost:    8
c ---[ 181]---> BDD-cost:    8
c ---[ 180]---> BDD-cost:    8
c ---[ 179]---> BDD-cost:    8
c ---[ 178]---> BDD-cost:    8
c ---[ 177]---> BDD-cost:    8
c ---[ 176]---> BDD-cost:    8
c ---[ 175]---> BDD-cost:    8
c ---[ 174]---> BDD-cost:    8
c ---[ 173]---> BDD-cost:    8
c ---[ 172]---> BDD-cost:    8
c ---[ 171]---> BDD-cost:    8
c ---[ 170]---> BDD-cost:    8
c ---[ 169]---> BDD-cost:    8
c ---[ 168]---> BDD-cost:    8
c ---[ 167]---> BDD-cost:    8
c ---[ 166]---> BDD-cost:    8
c ---[ 165]---> BDD-cost:    8
c ---[ 164]---> BDD-cost:    8
c ---[ 163]---> BDD-cost:    8
c ---[ 162]---> BDD-cost:    8
c ---[ 161]---> BDD-cost:    8
c ---[ 160]---> BDD-cost:    8
c ---[ 159]---> BDD-cost:    8
c ---[ 158]---> BDD-cost:    8
c ---[ 157]---> BDD-cost:    8
c ---[ 156]---> BDD-cost:    8
c ---[ 155]---> BDD-cost:    8
c ---[ 154]---> BDD-cost:    8
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:    8
c ---[ 151]---> BDD-cost:    8
c ---[ 150]---> BDD-cost:    8
c ---[ 149]---> BDD-cost:    8
c ---[ 148]---> BDD-cost:    8
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:    8
c ---[ 145]---> BDD-cost:    8
c ---[ 144]---> BDD-cost:    8
c ---[ 143]---> BDD-cost:    8
c ---[ 142]---> BDD-cost:    8
c ---[ 141]---> BDD-cost:    8
c ---[ 140]---> BDD-cost:    8
c ---[ 139]---> BDD-cost:    8
c ---[ 138]---> BDD-cost:    8
c ---[ 137]---> BDD-cost:    8
c ---[ 136]---> BDD-cost:    8
c ---[ 135]---> BDD-cost:    8
c ---[ 134]---> BDD-cost:    8
c ---[ 133]---> BDD-cost:    8
c ---[ 132]---> BDD-cost:    8
c ---[ 131]---> BDD-cost:    8
c ---[ 130]---> BDD-cost:    8
c ---[ 129]---> BDD-cost:    8
c ---[ 128]---> BDD-cost:    8
c ---[ 127]---> BDD-cost:    8
c ---[ 126]---> BDD-cost:    8
c ---[ 125]---> BDD-cost:    8
c ---[ 124]---> BDD-cost:    8
c ---[ 123]---> BDD-cost:    8
c ---[ 122]---> BDD-cost:    8
c ---[ 121]---> BDD-cost:    8
c ---[ 120]---> BDD-cost:    8
c ---[ 119]---> BDD-cost:    8
c ---[ 118]---> BDD-cost:    8
c ---[ 117]---> BDD-cost:    8
c ---[ 116]---> BDD-cost:    8
c ---[ 115]---> BDD-cost:    8
c ---[ 114]---> BDD-cost:    8
c ---[ 113]---> BDD-cost:    8
c ---[ 112]---> BDD-cost:    8
c ---[ 111]---> BDD-cost:    8
c ---[ 110]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:    8
c ---[ 108]---> BDD-cost:    8
c ---[ 107]---> BDD-cost:    8
c ---[ 106]---> BDD-cost:    8
c ---[ 105]---> BDD-cost:    8
c ---[ 104]---> BDD-cost:    8
c ---[ 103]---> BDD-cost:    8
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    8
c ---[ 100]---> BDD-cost:    8
c ---[  99]---> BDD-cost:    8
c ---[  98]---> BDD-cost:    8
c ---[  97]---> BDD-cost:    8
c ---[  96]---> BDD-cost:    8
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    8
c ---[  90]---> BDD-cost:    8
c ---[  89]---> BDD-cost:    8
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:    8
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:    8
c ---[  84]---> BDD-cost:    8
c ---[  83]---> BDD-cost:    8
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    8
c ---[  80]---> BDD-cost:    8
c ---[  79]---> BDD-cost:    8
c ---[  78]---> BDD-cost:    8
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:    8
c ---[  75]---> BDD-cost:    8
c ---[  74]---> BDD-cost:    8
c ---[  73]---> BDD-cost:    8
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:    8
c ---[  70]---> BDD-cost:    8
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:    8
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    8
c ---[  65]---> BDD-cost:    8
c ---[  64]---> BDD-cost:    8
c ---[  63]---> BDD-cost:    8
c ---[  62]---> BDD-cost:    8
c ---[  61]---> BDD-cost:    8
c ---[  60]---> BDD-cost:    8
c ---[  59]---> BDD-cost:    8
c ---[  58]---> BDD-cost:    8
c ---[  57]---> BDD-cost:    8
c ---[  56]---> BDD-cost:    8
c ---[  55]---> BDD-cost:    8
c ---[  54]---> BDD-cost:    8
c ---[  53]---> BDD-cost:    8
c ---[  52]---> BDD-cost:    8
c ---[  51]---> BDD-cost:    8
c ---[  50]---> BDD-cost:    8
c ---[  49]---> BDD-cost:    8
c ---[  48]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    8
c ---[  46]---> BDD-cost:    8
c ---[  45]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    8
c ---[  43]---> BDD-cost:    8
c ---[  42]---> BDD-cost:    8
c ---[  41]---> BDD-cost:    8
c ---[  40]---> BDD-cost:    8
c ---[  39]---> BDD-cost:    8
c ---[  38]---> BDD-cost:    8
c ---[  37]---> BDD-cost:    8
c ---[  36]---> BDD-cost:    8
c ---[  35]---> BDD-cost:    8
c ---[  34]---> BDD-cost:    8
c ---[  33]---> BDD-cost:    8
c ---[  32]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    8
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:    8
c ---[  23]---> Adder-cost: 16837   maxlim: 101745   bits: 18/17
c ---[  22]---> Adder-cost: 35787   maxlim: 6633569   bits: 24/23
c ---[  21]---> Adder-cost: 18126   maxlim: 4660379   bits: 24/23
c ---[  20]---> Adder-cost: 13526   maxlim: 7782034   bits: 24/23
c ---[  19]---> Adder-cost: 46920   maxlim: 49412548   bits: 27/26
c ---[  18]---> Adder-cost: 7270   maxlim: 202757   bits: 18/18
c ---[  17]---> Adder-cost: 28854   maxlim: 3340290   bits: 23/22
c ---[  16]---> Adder-cost: 44525   maxlim: 3367019   bits: 23/22
c ---[  15]---> Adder-cost: 37629   maxlim: 7305239   bits: 24/23
c ---[  14]---> Adder-cost: 14038   maxlim: 171104   bits: 19/18
c ---[  13]---> Adder-cost: 18310   maxlim: 585650   bits: 20/20
c ---[  12]---> Adder-cost: 51276   maxlim: 48594727   bits: 27/26
c ---[  11]---> Adder-cost: 2096   maxlim: 88902   bits: 17/17
c ---[  10]---> Adder-cost: 8416   maxlim: 4571464   bits: 23/23
c ---[   9]---> Adder-cost: 28701   maxlim: 3985139   bits: 23/22
c ---[   8]---> Adder-cost: 4168   maxlim: 64077   bits: 17/16
c ---[   7]---> Adder-cost: 4299   maxlim: 30599   bits: 16/15
c ---[   6]---> Adder-cost: 4676   maxlim: 35189   bits: 17/16
c ---[   5]---> Adder-cost: 8358   maxlim: 67319   bits: 18/17
c ---[   4]---> Adder-cost: 4270   maxlim: 73024   bits: 17/17
c ---[   3]---> Adder-cost: 3309   maxlim: 24989   bits: 16/15
c ---[   2]---> Adder-cost: 2149   maxlim: 15809   bits: 15/14
c ---[   1]---> Adder-cost: 5642   maxlim: 93949   bits: 18/17
c ---[   0]---> Adder-cost: 3842   maxlim: 34424   bits: 17/16
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 | 2897142 10335934 |  869142       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/422416          
c   -- var.elim.:  2000/422416          
c   -- var.elim.:  3000/422416          
c   -- var.elim.:  4000/422416          
c   -- var.elim.:  5000/422416          
c   -- var.elim.:  6000/422416          
c   -- var.elim.:  7000/422416          
c   -- var.elim.:  8000/422416          
c   -- var.elim.:  9000/422416          
c   -- var.elim.:  10000/422416          
c   -- var.elim.:  11000/422416          
c   -- var.elim.:  12000/422416          
c   -- var.elim.:  13000/422416          
c   -- var.elim.:  14000/422416          
c   -- var.elim.:  15000/422416          
c   -- var.elim.:  16000/422416          
c   -- var.elim.:  17000/422416          
c   -- var.elim.:  18000/422416          
c   -- var.elim.:  19000/422416          
c   -- var.elim.:  20000/422416          
c   -- var.elim.:  21000/422416          
c   -- var.elim.:  22000/422416          
c   -- var.elim.:  23000/422416          
c   -- var.elim.:  24000/422416          
c   -- var.elim.:  25000/422416          
c   -- var.elim.:  26000/422416          
c   -- var.elim.:  27000/422416          
c   -- var.elim.:  28000/422416          
c   -- var.elim.:  29000/422416          
c   -- var.elim.:  30000/422416          
c   -- var.elim.:  31000/422416          
c   -- var.elim.:  32000/422416          
c   -- var.elim.:  33000/422416          
c   -- var.elim.:  34000/422416          
c   -- var.elim.:  35000/422416          
c   -- var.elim.:  36000/422416          
c   -- var.elim.:  37000/422416          
c   -- var.elim.:  38000/422416          
c   -- var.elim.:  39000/422416          
c   -- var.elim.:  40000/422416          
c   -- var.elim.:  41000/422416          
c   -- var.elim.:  42000/422416          
c   -- var.elim.:  43000/422416          
c   -- var.elim.:  44000/422416          
c   -- var.elim.:  45000/422416          
c   -- var.elim.:  46000/422416          
c   -- var.elim.:  47000/422416          
c   -- var.elim.:  48000/422416          
c   -- var.elim.:  49000/422416          
c   -- var.elim.:  50000/422416          
c   -- var.elim.:  51000/422416          
c   -- var.elim.:  52000/422416          
c   -- var.elim.:  53000/422416          
c   -- var.elim.:  54000/422416          
c   -- var.elim.:  55000/422416          
c   -- var.elim.:  56000/422416          
c   -- var.elim.:  57000/422416          
c   -- var.elim.:  58000/422416          
c   -- var.elim.:  59000/422416          
c   -- var.elim.:  60000/422416          
c   -- var.elim.:  61000/422416          
c   -- var.elim.:  62000/422416          
c   -- var.elim.:  63000/422416          
c   -- var.elim.:  64000/422416          
c   -- var.elim.:  65000/422416          
c   -- var.elim.:  66000/422416          
c   -- var.elim.:  67000/422416          
c   -- var.elim.:  68000/422416          
c   -- var.elim.:  69000/422416          
c   -- var.elim.:  70000/422416          
c   -- var.elim.:  71000/422416          
c   -- var.elim.:  72000/422416          
c   -- var.elim.:  73000/422416          
c   -- var.elim.:  74000/422416          
c   -- var.elim.:  75000/422416          
c   -- var.elim.:  76000/422416          
c   -- var.elim.:  77000/422416          
c   -- var.elim.:  78000/422416          
c   -- var.elim.:  79000/422416          
c   -- var.elim.:  80000/422416          
c   -- var.elim.:  81000/422416          
c   -- var.elim.:  82000/422416          
c   -- var.elim.:  83000/422416          
c   -- var.elim.:  84000/422416          
c   -- var.elim.:  85000/422416          
c   -- var.elim.:  86000/422416          
c   -- var.elim.:  87000/422416          
c   -- var.elim.:  88000/422416          
c   -- var.elim.:  89000/422416          
c   -- var.elim.:  90000/422416          
c   -- var.elim.:  91000/422416          
c   -- var.elim.:  92000/422416          
c   -- var.elim.:  93000/422416          
c   -- var.elim.:  94000/422416          
c   -- var.elim.:  95000/422416          
c   -- var.elim.:  96000/422416          
c   -- var.elim.:  97000/422416          
c   -- var.elim.:  98000/422416          
c   -- var.elim.:  99000/422416          
c   -- var.elim.:  100000/422416          
c   -- var.elim.:  101000/422416          
c   -- var.elim.:  102000/422416          
c   -- var.elim.:  103000/422416          
c   -- var.elim.:  104000/422416          
c   -- var.elim.:  105000/422416          
c   -- var.elim.:  106000/422416          
c   -- var.elim.:  107000/422416          
c   -- var.elim.:  108000/422416          
c   -- var.elim.:  109000/422416          
c   -- var.elim.:  110000/422416          
c   -- var.elim.:  111000/422416          
c   -- var.elim.:  112000/422416          
c   -- var.elim.:  113000/422416          
c   -- var.elim.:  114000/422416          
c   -- var.elim.:  115000/422416          
c   -- var.elim.:  116000/422416          
c   -- var.elim.:  117000/422416          
c   -- var.elim.:  118000/422416          
c   -- var.elim.:  119000/422416          
c   -- var.elim.:  120000/422416          
c   -- var.elim.:  121000/422416          
c   -- var.elim.:  122000/422416          
c   -- var.elim.:  123000/422416          
c   -- var.elim.:  124000/422416          
c   -- var.elim.:  125000/422416          
c   -- var.elim.:  126000/422416          
c   -- var.elim.:  127000/422416          
c   -- var.elim.:  128000/422416          
c   -- var.elim.:  129000/422416          
c   -- var.elim.:  130000/422416          
c   -- var.elim.:  131000/422416          
c   -- var.elim.:  132000/422416          
c   -- var.elim.:  133000/422416          
c   -- var.elim.:  134000/422416          
c   -- var.elim.:  135000/422416          
c   -- var.elim.:  136000/422416          
c   -- var.elim.:  137000/422416          
c   -- var.elim.:  138000/422416          
c   -- var.elim.:  139000/422416          
c   -- var.elim.:  140000/422416          
c   -- var.elim.:  141000/422416          
c   -- var.elim.:  142000/422416          
c   -- var.elim.:  143000/422416          
c   -- var.elim.:  144000/422416          
c   -- var.elim.:  145000/422416          
c   -- var.elim.:  146000/422416          
c   -- var.elim.:  147000/422416          
c   -- var.elim.:  148000/422416          
c   -- var.elim.:  149000/422416          
c   -- var.elim.:  150000/422416          
c   -- var.elim.:  151000/422416          
c   -- var.elim.:  152000/422416          
c   -- var.elim.:  153000/422416          
c   -- var.elim.:  154000/422416          
c   -- var.elim.:  155000/422416          
c   -- var.elim.:  156000/422416          
c   -- var.elim.:  157000/422416          
c   -- var.elim.:  158000/422416          
c   -- var.elim.:  159000/422416          
c   -- var.elim.:  160000/422416          
c   -- var.elim.:  161000/422416          
c   -- var.elim.:  162000/422416          
c   -- var.elim.:  163000/422416          
c   -- var.elim.:  164000/422416          
c   -- var.elim.:  165000/422416          
c   -- var.elim.:  166000/422416          
c   -- var.elim.:  167000/422416          
c   -- var.elim.:  168000/422416          
c   -- var.elim.:  169000/422416          
c   -- var.elim.:  170000/422416          
c   -- var.elim.:  171000/422416          
c   -- var.elim.:  172000/422416          
c   -- var.elim.:  173000/422416          
c   -- var.elim.:  174000/422416          
c   -- var.elim.:  175000/422416          
c   -- var.elim.:  176000/422416          
c   -- var.elim.:  177000/422416          
c   -- var.elim.:  178000/422416          
c   -- var.elim.:  179000/422416          
c   -- var.elim.:  180000/422416          
c   -- var.elim.:  181000/422416          
c   -- var.elim.:  182000/422416          
c   -- var.elim.:  183000/422416          
c   -- var.elim.:  184000/422416          
c   -- var.elim.:  185000/422416          
c   -- var.elim.:  186000/422416          
c   -- var.elim.:  187000/422416          
c   -- var.elim.:  188000/422416          
c   -- var.elim.:  189000/422416          
c   -- var.elim.:  190000/422416          
c   -- var.elim.:  191000/422416          
c   -- var.elim.:  192000/422416          
c   -- var.elim.:  193000/422416          
c   -- var.elim.:  194000/422416          
c   -- var.elim.:  195000/422416          
c   -- var.elim.:  196000/422416          
c   -- var.elim.:  197000/422416          
c   -- var.elim.:  198000/422416          
c   -- var.elim.:  199000/422416          
c   -- var.elim.:  200000/422416          
c   -- var.elim.:  201000/422416          
c   -- var.elim.:  202000/422416          
c   -- var.elim.:  203000/422416          
c   -- var.elim.:  204000/422416          
c   -- var.elim.:  205000/422416          
c   -- var.elim.:  206000/422416          
c   -- var.elim.:  207000/422416          
c   -- var.elim.:  208000/422416          
c   -- var.elim.:  209000/422416          
c   -- var.elim.:  210000/422416          
c   -- var.elim.:  211000/422416          
c   -- var.elim.:  212000/422416          
c   -- var.elim.:  213000/422416          
c   -- var.elim.:  214000/422416          
c   -- var.elim.:  215000/422416          
c   -- var.elim.:  216000/422416          
c   -- var.elim.:  217000/422416          
c   -- var.elim.:  218000/422416          
c   -- var.elim.:  219000/422416          
c   -- var.elim.:  220000/422416          
c   -- var.elim.:  221000/422416          
c   -- var.elim.:  222000/422416          
c   -- var.elim.:  223000/422416          
c   -- var.elim.:  224000/422416          
c   -- var.elim.:  225000/422416          
c   -- var.elim.:  226000/422416          
c   -- var.elim.:  227000/422416          
c   -- var.elim.:  228000/422416          
c   -- var.elim.:  229000/422416          
c   -- var.elim.:  230000/422416          
c   -- var.elim.:  231000/422416          
c   -- var.elim.:  232000/422416          
c   -- var.elim.:  233000/422416          
c   -- var.elim.:  234000/422416          
c   -- var.elim.:  235000/422416          
c   -- var.elim.:  236000/422416          
c   -- var.elim.:  237000/422416          
c   -- var.elim.:  238000/422416          
c   -- var.elim.:  239000/422416          
c   -- var.elim.:  240000/422416          
c   -- var.elim.:  241000/422416          
c   -- var.elim.:  242000/422416          
c   -- var.elim.:  243000/422416          
c   -- var.elim.:  244000/422416          
c   -- var.elim.:  245000/422416          
c   -- var.elim.:  246000/422416          
c   -- var.elim.:  247000/422416          
c   -- var.elim.:  248000/422416          
c   -- var.elim.:  249000/422416          
c   -- var.elim.:  250000/422416          
c   -- var.elim.:  251000/422416          
c   -- var.elim.:  252000/422416          
c   -- var.elim.:  253000/422416          
c   -- var.elim.:  254000/422416          
c   -- var.elim.:  255000/422416          
c   -- var.elim.:  256000/422416          
c   -- var.elim.:  257000/422416          
c   -- var.elim.:  258000/422416          
c   -- var.elim.:  259000/422416          
c   -- var.elim.:  260000/422416          
c   -- var.elim.:  261000/422416          
c   -- var.elim.:  262000/422416          
c   -- var.elim.:  263000/422416          
c   -- var.elim.:  264000/422416          
c   -- var.elim.:  265000/422416          
c   -- var.elim.:  266000/422416          
c   -- var.elim.:  267000/422416          
c   -- var.elim.:  268000/422416          
c   -- var.elim.:  269000/422416          
c   -- var.elim.:  270000/422416          
c   -- var.elim.:  271000/422416          
c   -- var.elim.:  272000/422416          
c   -- var.elim.:  273000/422416          
c   -- var.elim.:  274000/422416          
c   -- var.elim.:  275000/422416          
c   -- var.elim.:  276000/422416          
c   -- var.elim.:  277000/422416          
c   -- var.elim.:  278000/422416          
c   -- var.elim.:  279000/422416          
c   -- var.elim.:  280000/422416          
c   -- var.elim.:  281000/422416          
c   -- var.elim.:  282000/422416          
c   -- var.elim.:  283000/422416          
c   -- var.elim.:  284000/422416          
c   -- var.elim.:  285000/422416          
c   -- var.elim.:  286000/422416          
c   -- var.elim.:  287000/422416          
c   -- var.elim.:  288000/422416          
c   -- var.elim.:  289000/422416          
c   -- var.elim.:  290000/422416          
c   -- var.elim.:  291000/422416          
c   -- var.elim.:  292000/422416          
c   -- var.elim.:  293000/422416          
c   -- var.elim.:  294000/422416          
c   -- var.elim.:  295000/422416          
c   -- var.elim.:  296000/422416          
c   -- var.elim.:  297000/422416          
c   -- var.elim.:  298000/422416          
c   -- var.elim.:  299000/422416          
c   -- var.elim.:  300000/422416          
c   -- var.elim.:  301000/422416          
c   -- var.elim.:  302000/422416          
c   -- var.elim.:  303000/422416          
c   -- var.elim.:  304000/422416          
c   -- var.elim.:  305000/422416          
c   -- var.elim.:  306000/422416          
c   -- var.elim.:  307000/422416          
c   -- var.elim.:  308000/422416          
c   -- var.elim.:  309000/422416          
c   -- var.elim.:  310000/422416          
c   -- var.elim.:  311000/422416          
c   -- var.elim.:  312000/422416          
c   -- var.elim.:  313000/422416          
c   -- var.elim.:  314000/422416          
c   -- var.elim.:  315000/422416          
c   -- var.elim.:  316000/422416          
c   -- var.elim.:  317000/422416          
c   -- var.elim.:  318000/422416          
c   -- var.elim.:  319000/422416          
c   -- var.elim.:  320000/422416          
c   -- var.elim.:  321000/422416          
c   -- var.elim.:  322000/422416          
c   -- var.elim.:  323000/422416          
c   -- var.elim.:  324000/422416          
c   -- var.elim.:  325000/422416          
c   -- var.elim.:  326000/422416          
c   -- var.elim.:  327000/422416          
c   -- var.elim.:  328000/422416          
c   -- var.elim.:  329000/422416          
c   -- var.elim.:  330000/422416          
c   -- var.elim.:  331000/422416          
c   -- var.elim.:  332000/422416          
c   -- var.elim.:  333000/422416          
c   -- var.elim.:  334000/422416          
c   -- var.elim.:  335000/422416          
c   -- var.elim.:  336000/422416          
c   -- var.elim.:  337000/422416          
c   -- var.elim.:  338000/422416          
c   -- var.elim.:  339000/422416          
c   -- var.elim.:  340000/422416          
c   -- var.elim.:  341000/422416          
c   -- var.elim.:  342000/422416          
c   -- var.elim.:  343000/422416          
c   -- var.elim.:  344000/422416          
c   -- var.elim.:  345000/422416          
c   -- var.elim.:  346000/422416          
c   -- var.elim.:  347000/422416          
c   -- var.elim.:  348000/422416          
c   -- var.elim.:  349000/422416          
c   -- var.elim.:  350000/422416          
c   -- var.elim.:  351000/422416          
c   -- var.elim.:  352000/422416          
c   -- var.elim.:  353000/422416          
c   -- var.elim.:  354000/422416          
c   -- var.elim.:  355000/422416          
c   -- var.elim.:  356000/422416          
c   -- var.elim.:  357000/422416          
c   -- var.elim.:  358000/422416          
c   -- var.elim.:  359000/422416          
c   -- var.elim.:  360000/422416          
c   -- var.elim.:  361000/422416          
c   -- var.elim.:  362000/422416          
c   -- var.elim.:  363000/422416          
c   -- var.elim.:  364000/422416          
c   -- var.elim.:  365000/422416          
c   -- var.elim.:  366000/422416          
c   -- var.elim.:  367000/422416          
c   -- var.elim.:  368000/422416          
c   -- var.elim.:  369000/422416          
c   -- var.elim.:  370000/422416          
c   -- var.elim.:  371000/422416          
c   -- var.elim.:  372000/422416          
c   -- var.elim.:  373000/422416          
c   -- var.elim.:  374000/422416          
c   -- var.elim.:  375000/422416          
c   -- var.elim.:  376000/422416          
c   -- var.elim.:  377000/422416          
c   -- var.elim.:  378000/422416          
c   -- var.elim.:  379000/422416          
c   -- var.elim.:  380000/422416          
c   -- var.elim.:  381000/422416          
c   -- var.elim.:  382000/422416          
c   -- var.elim.:  383000/422416          
c   -- var.elim.:  384000/422416          
c   -- var.elim.:  385000/422416          
c   -- var.elim.:  386000/422416          
c   -- var.elim.:  387000/422416          
c   -- var.elim.:  388000/422416          
c   -- var.elim.:  389000/422416          
c   -- var.elim.:  390000/422416          
c   -- var.elim.:  391000/422416          
c   -- var.elim.:  392000/422416          
c   -- var.elim.:  393000/422416          
c   -- var.elim.:  394000/422416          
c   -- var.elim.:  395000/422416          
c   -- var.elim.:  396000/422416          
c   -- var.elim.:  397000/422416          
c   -- var.elim.:  398000/422416          
c   -- var.elim.:  399000/422416          
c   -- var.elim.:  400000/422416          
c   -- var.elim.:  401000/422416          
c   -- var.elim.:  402000/422416          
c   -- var.elim.:  403000/422416          
c   -- var.elim.:  404000/422416          
c   -- var.elim.:  405000/422416          
c   -- var.elim.:  406000/422416          
c   -- var.elim.:  407000/422416          
c   -- var.elim.:  408000/422416          
c   -- var.elim.:  409000/422416          
c   -- var.elim.:  410000/422416          
c   -- var.elim.:  411000/422416          
c   -- var.elim.:  412000/422416          
c   -- var.elim.:  413000/422416          
c   -- var.elim.:  414000/422416          
c   -- var.elim.:  415000/422416          
c   -- var.elim.:  416000/422416          
c   -- var.elim.:  417000/422416          
c   -- var.elim.:  418000/422416          
c   -- var.elim.:  419000/422416          
c   -- var.elim.:  420000/422416          
c   -- var.elim.:  421000/422416          
c   -- var.elim.:  422000/422416          
c   -- var.elim.:  422416/422416          
c   -- var.elim.:  1000/9309          
c   -- var.elim.:  2000/9309          
c   -- var.elim.:  3000/9309          
c   -- var.elim.:  4000/9309          
c   -- var.elim.:  5000/9309          
c   -- var.elim.:  6000/9309          
c   -- var.elim.:  7000/9309          
c   -- var.elim.:  8000/9309          
c   -- var.elim.:  9000/9309          
c   -- var.elim.:  9309/9309          
c   -- subsuming                       
c   -- var.elim.:  57/57          
c   -- var.elim.:  8/8          
c |         0 | 2894997 10330709 |      --       0       --      -- |     --   | -2000/-3170
c |         0 | 2894997 10330709 | 1157998       0        0     nan |  0.000 % |
c |       100 | 2894997 10330709 | 1273798     100      320     3.2 |  0.312 % |
c |       250 | 2894997 10330709 | 1401178     250      818     3.3 |  0.312 % |
c |       475 | 2894997 10330709 | 1541296     475     1578     3.3 |  0.312 % |
c |       812 | 2894997 10330709 | 1695426     812     2817     3.5 |  0.312 % |
c |      1318 | 2894997 10330709 | 1864968    1318     4528     3.4 |  0.312 % |
c |      2077 | 2894997 10330709 | 2051465    2077     7444     3.6 |  0.312 % |
c |      3216 | 2894986 10330672 | 2256603    3215    11768     3.7 |  0.312 #### 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.87 0.91 0.90 2/54 24667
Raw data (stat): 24667 (runsolver) R 24666 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 471126879 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99981 s]
Raw data (loadavg): 0.89 0.91 0.90 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 10599 0 0 0 970 28 0 0 25 0 1 0 471126879 40132608 7244 4294967295 134512640 134672761 3221224544 3221222384 134597224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9798 7244 603 41 0 9757 0
vsize: 39192
[startup+20.0009 s]
Raw data (loadavg): 0.91 0.91 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 10599 0 0 0 1970 28 0 0 25 0 1 0 471126879 40132608 7244 4294967295 134512640 134672761 3221224544 3221222960 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9798 7244 603 41 0 9757 0
vsize: 39192
[startup+30.0014 s]
Raw data (loadavg): 0.92 0.91 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 19595 0 0 0 2948 51 0 0 25 0 1 0 471126879 70737920 13473 4294967295 134512640 134672761 3221224544 3221222528 134597008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17270 13473 603 41 0 17229 0
vsize: 69080
[startup+40.0022 s]
Raw data (loadavg): 0.93 0.92 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 20551 0 0 0 3945 54 0 0 25 0 1 0 471126879 70737920 13473 4294967295 134512640 134672761 3221224544 3221222720 134544713 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17270 13473 603 41 0 17229 0
vsize: 69080
[startup+50.0037 s]
Raw data (loadavg): 0.94 0.92 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 34410 0 0 0 4912 87 0 0 25 0 1 0 471126879 127295488 26545 4294967295 134512640 134672761 3221224544 3221218728 134526585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31078 26545 603 41 0 31037 0
vsize: 124312
[startup+60.0037 s]
Raw data (loadavg): 0.95 0.92 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 77753 0 0 0 5805 194 0 0 25 0 1 0 471126879 345346048 69888 4294967295 134512640 134672761 3221224544 3221214960 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84313 69888 603 41 0 84272 0
vsize: 337252
[startup+70.0044 s]
Raw data (loadavg): 0.96 0.92 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 101146 0 0 0 6749 249 0 0 25 0 1 0 471126879 425926656 93274 4294967295 134512640 134672761 3221224544 3221223088 134621359 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 103986 93274 603 41 0 103945 0
vsize: 415944
[startup+80.0056 s]
Raw data (loadavg): 0.96 0.92 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 101146 0 0 0 7750 250 0 0 25 0 1 0 471126879 425926656 93274 4294967295 134512640 134672761 3221224544 3221223088 134621336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 103986 93274 603 41 0 103945 0
vsize: 415944
[startup+90.0059 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 103976 0 0 0 8742 257 0 0 25 0 1 0 471126879 442032128 96104 4294967295 134512640 134672761 3221224544 3221223280 134522369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107918 96104 603 41 0 107877 0
vsize: 431672
[startup+100.006 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 112019 0 0 0 9721 278 0 0 25 0 1 0 471126879 428023808 93764 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 104498 93764 603 41 0 104457 0
vsize: 417992
[startup+110.006 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 112430 0 0 0 10720 280 0 0 25 0 1 0 471126879 429645824 94175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 104894 94175 603 41 0 104853 0
vsize: 419576
[startup+120.007 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 112812 0 0 0 11719 281 0 0 25 0 1 0 471126879 431181824 94557 4294967295 134512640 134672761 3221224544 3221223808 134618040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 105269 94557 603 41 0 105228 0
vsize: 421076
[startup+130.007 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 113194 0 0 0 12716 283 0 0 25 0 1 0 471126879 432873472 94939 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 105682 94939 603 41 0 105641 0
vsize: 422728
[startup+140.007 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 113471 0 0 0 13715 284 0 0 25 0 1 0 471126879 433942528 95216 4294967295 134512640 134672761 3221224544 3221223680 134614825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 105943 95216 603 41 0 105902 0
vsize: 423772
[startup+150.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 113735 0 0 0 14715 285 0 0 25 0 1 0 471126879 435019776 95480 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 106206 95480 603 41 0 106165 0
vsize: 424824
[startup+160.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 114095 0 0 0 15713 287 0 0 25 0 1 0 471126879 436494336 95840 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 106566 95840 603 41 0 106525 0
vsize: 426264
[startup+170.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 114257 0 0 0 16712 288 0 0 25 0 1 0 471126879 437170176 96002 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 106731 96002 603 41 0 106690 0
vsize: 426924
[startup+180.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 114383 0 0 0 17712 289 0 0 25 0 1 0 471126879 437702656 96128 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 106861 96128 603 41 0 106820 0
vsize: 427444
[startup+190.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 114485 0 0 0 18711 290 0 0 25 0 1 0 471126879 438108160 96230 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 106960 96230 603 41 0 106919 0
vsize: 427840
[startup+200.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 114613 0 0 0 19710 290 0 0 25 0 1 0 471126879 438775808 96358 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107123 96358 603 41 0 107082 0
vsize: 428492
[startup+210.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 114738 0 0 0 20710 291 0 0 25 0 1 0 471126879 439312384 96483 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107254 96483 603 41 0 107213 0
vsize: 429016
[startup+220.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 114829 0 0 0 21709 291 0 0 25 0 1 0 471126879 439623680 96574 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107330 96574 603 41 0 107289 0
vsize: 429320
[startup+230.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 114926 0 0 0 22709 292 0 0 25 0 1 0 471126879 440029184 96671 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107429 96671 603 41 0 107388 0
vsize: 429716
[startup+240.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 115002 0 0 0 23710 292 0 0 25 0 1 0 471126879 440299520 96747 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107495 96747 603 41 0 107454 0
vsize: 429980
[startup+250.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 115365 0 0 0 24708 294 0 0 25 0 1 0 471126879 441765888 97110 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107853 97110 603 41 0 107812 0
vsize: 431412
[startup+260.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116045 0 0 0 25707 296 0 0 25 0 1 0 471126879 444563456 97790 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 108536 97790 603 41 0 108495 0
vsize: 434144
[startup+270.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116234 0 0 0 26706 297 0 0 25 0 1 0 471126879 445366272 97979 4294967295 134512640 134672761 3221224544 3221223744 134610511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 108732 97979 603 41 0 108691 0
vsize: 434928
[startup+280.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116313 0 0 0 27706 297 0 0 25 0 1 0 471126879 445636608 98058 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 108798 98058 603 41 0 108757 0
vsize: 435192
[startup+290.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116380 0 0 0 28706 298 0 0 25 0 1 0 471126879 445906944 98125 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 108864 98125 603 41 0 108823 0
vsize: 435456
[startup+300.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116431 0 0 0 29705 298 0 0 25 0 1 0 471126879 446042112 98176 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 108897 98176 603 41 0 108856 0
vsize: 435588
[startup+310.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116497 0 0 0 30705 299 0 0 25 0 1 0 471126879 446312448 98242 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 108963 98242 603 41 0 108922 0
vsize: 435852
[startup+320.036 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116545 0 0 0 31705 299 0 0 25 0 1 0 471126879 446582784 98290 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109029 98290 603 41 0 108988 0
vsize: 436116
[startup+330.04 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116594 0 0 0 32705 300 0 0 25 0 1 0 471126879 446980096 98339 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109126 98339 603 41 0 109085 0
vsize: 436504
[startup+340.04 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116645 0 0 0 33704 300 0 0 25 0 1 0 471126879 447246336 98390 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109191 98390 603 41 0 109150 0
vsize: 436764
[startup+350.041 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116729 0 0 0 34704 301 0 0 25 0 1 0 471126879 447643648 98474 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109288 98474 603 41 0 109247 0
vsize: 437152
[startup+360.041 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116756 0 0 0 35703 302 0 0 25 0 1 0 471126879 447778816 98501 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109321 98501 603 41 0 109280 0
vsize: 437284
[startup+370.042 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116801 0 0 0 36703 302 0 0 25 0 1 0 471126879 447913984 98546 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109354 98546 603 41 0 109313 0
vsize: 437416
[startup+380.042 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116864 0 0 0 37703 302 0 0 25 0 1 0 471126879 448184320 98609 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109420 98609 603 41 0 109379 0
vsize: 437680
[startup+390.042 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116916 0 0 0 38702 303 0 0 25 0 1 0 471126879 448319488 98661 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109453 98661 603 41 0 109412 0
vsize: 437812
[startup+400.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 116966 0 0 0 39702 303 0 0 25 0 1 0 471126879 448589824 98711 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109519 98711 603 41 0 109478 0
vsize: 438076
[startup+410.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117014 0 0 0 40702 304 0 0 25 0 1 0 471126879 448724992 98759 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109552 98759 603 41 0 109511 0
vsize: 438208
[startup+420.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117068 0 0 0 41701 304 0 0 25 0 1 0 471126879 449257472 98813 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109682 98813 603 41 0 109641 0
vsize: 438728
[startup+430.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117210 0 0 0 42701 305 0 0 25 0 1 0 471126879 449789952 98955 4294967295 134512640 134672761 3221224544 3221223668 134566082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109812 98955 603 41 0 109771 0
vsize: 439248
[startup+440.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117263 0 0 0 43700 306 0 0 25 0 1 0 471126879 449925120 99008 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109845 99008 603 41 0 109804 0
vsize: 439380
[startup+450.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117312 0 0 0 44699 306 0 0 25 0 1 0 471126879 450195456 99057 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109911 99057 603 41 0 109870 0
vsize: 439644
[startup+460.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117349 0 0 0 45699 307 0 0 25 0 1 0 471126879 450330624 99094 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109944 99094 603 41 0 109903 0
vsize: 439776
[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117382 0 0 0 46699 307 0 0 25 0 1 0 471126879 450465792 99127 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109977 99127 603 41 0 109936 0
vsize: 439908
[startup+480.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117443 0 0 0 47698 308 0 0 25 0 1 0 471126879 450736128 99188 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110043 99188 603 41 0 110002 0
vsize: 440172
[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117475 0 0 0 48698 308 0 0 25 0 1 0 471126879 450871296 99220 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110076 99220 603 41 0 110035 0
vsize: 440304
[startup+500.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117506 0 0 0 49698 308 0 0 25 0 1 0 471126879 451006464 99251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110109 99251 603 41 0 110068 0
vsize: 440436
[startup+510.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117532 0 0 0 50698 309 0 0 25 0 1 0 471126879 451006464 99277 4294967295 134512640 134672761 3221224544 3221223548 134619829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110109 99277 603 41 0 110068 0
vsize: 440436
[startup+520.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117609 0 0 0 51698 309 0 0 25 0 1 0 471126879 451276800 99354 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110175 99354 603 41 0 110134 0
vsize: 440700
[startup+530.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117635 0 0 0 52697 310 0 0 25 0 1 0 471126879 451411968 99380 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110208 99380 603 41 0 110167 0
vsize: 440832
[startup+540.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117661 0 0 0 53697 310 0 0 25 0 1 0 471126879 451547136 99406 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110241 99406 603 41 0 110200 0
vsize: 440964
[startup+550.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117698 0 0 0 54696 311 0 0 25 0 1 0 471126879 451682304 99443 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110274 99443 603 41 0 110233 0
vsize: 441096
[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117720 0 0 0 55696 311 0 0 25 0 1 0 471126879 451817472 99465 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110307 99465 603 41 0 110266 0
vsize: 441228
[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117747 0 0 0 56696 312 0 0 25 0 1 0 471126879 451817472 99492 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110307 99492 603 41 0 110266 0
vsize: 441228
[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117772 0 0 0 57696 312 0 0 25 0 1 0 471126879 451952640 99517 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110340 99517 603 41 0 110299 0
vsize: 441360
[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 117797 0 0 0 58695 313 0 0 25 0 1 0 471126879 451952640 99542 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110340 99542 603 41 0 110299 0
vsize: 441360
[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 118370 0 0 0 59693 314 0 0 25 0 1 0 471126879 454348800 100115 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110925 100115 603 41 0 110884 0
vsize: 443700
[startup+610.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 118534 0 0 0 60693 315 0 0 25 0 1 0 471126879 455016448 100279 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111088 100279 603 41 0 111047 0
vsize: 444352
[startup+620.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 119184 0 0 0 61691 317 0 0 25 0 1 0 471126879 457564160 100929 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111710 100929 603 41 0 111669 0
vsize: 446840
[startup+630.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 119681 0 0 0 62690 318 0 0 25 0 1 0 471126879 459714560 101426 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112235 101426 603 41 0 112194 0
vsize: 448940
[startup+640.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 119811 0 0 0 63689 319 0 0 25 0 1 0 471126879 460775424 101556 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112494 101556 603 41 0 112453 0
vsize: 449976
[startup+650.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 119845 0 0 0 64689 319 0 0 25 0 1 0 471126879 460910592 101590 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112527 101590 603 41 0 112486 0
vsize: 450108
[startup+660.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 119886 0 0 0 65689 320 0 0 25 0 1 0 471126879 461045760 101631 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112560 101631 603 41 0 112519 0
vsize: 450240
[startup+670.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 120360 0 0 0 66687 321 0 0 25 0 1 0 471126879 462893056 102105 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113011 102105 603 41 0 112970 0
vsize: 452044
[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 120543 0 0 0 67687 322 0 0 25 0 1 0 471126879 463695872 102288 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113207 102288 603 41 0 113166 0
vsize: 452828
[startup+690.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 120980 0 0 0 68685 324 0 0 25 0 1 0 471126879 465440768 102725 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113633 102725 603 41 0 113592 0
vsize: 454532
[startup+700.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 121424 0 0 0 69683 326 0 0 25 0 1 0 471126879 467288064 103169 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114084 103169 603 41 0 114043 0
vsize: 456336
[startup+710.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 121857 0 0 0 70681 328 0 0 25 0 1 0 471126879 469028864 103602 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114509 103602 603 41 0 114468 0
vsize: 458036
[startup+720.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 122316 0 0 0 71679 330 0 0 25 0 1 0 471126879 470884352 104061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114962 104061 603 41 0 114921 0
vsize: 459848
[startup+730.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 122763 0 0 0 72677 332 0 0 25 0 1 0 471126879 472764416 104508 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115421 104508 603 41 0 115380 0
vsize: 461684
[startup+740.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 123032 0 0 0 73676 333 0 0 25 0 1 0 471126879 473825280 104777 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115680 104777 603 41 0 115639 0
vsize: 462720
[startup+750.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 123065 0 0 0 74676 334 0 0 25 0 1 0 471126879 473960448 104810 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115713 104810 603 41 0 115672 0
vsize: 462852
[startup+760.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 123111 0 0 0 75675 334 0 0 25 0 1 0 471126879 474095616 104856 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115746 104856 603 41 0 115705 0
vsize: 462984
[startup+770.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 123163 0 0 0 76674 335 0 0 25 0 1 0 471126879 474361856 104908 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115811 104908 603 41 0 115770 0
vsize: 463244
[startup+780.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 123231 0 0 0 77674 335 0 0 25 0 1 0 471126879 474632192 104976 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115877 104976 603 41 0 115836 0
vsize: 463508
[startup+790.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 123263 0 0 0 78674 336 0 0 25 0 1 0 471126879 474779648 105008 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115913 105008 603 41 0 115872 0
vsize: 463652
[startup+800.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 123454 0 0 0 79673 337 0 0 25 0 1 0 471126879 475451392 105199 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116077 105199 603 41 0 116036 0
vsize: 464308
[startup+810.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 123669 0 0 0 80671 338 0 0 25 0 1 0 471126879 476389376 105414 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116306 105414 603 41 0 116265 0
vsize: 465224
[startup+820.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 123895 0 0 0 81671 339 0 0 25 0 1 0 471126879 477319168 105640 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116533 105640 603 41 0 116492 0
vsize: 466132
[startup+830.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 124080 0 0 0 82670 340 0 0 25 0 1 0 471126879 477978624 105825 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116694 105825 603 41 0 116653 0
vsize: 466776
[startup+840.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 124139 0 0 0 83669 341 0 0 25 0 1 0 471126879 478253056 105884 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116761 105884 603 41 0 116720 0
vsize: 467044
[startup+850.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 124216 0 0 0 84669 341 0 0 25 0 1 0 471126879 478527488 105961 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116828 105961 603 41 0 116787 0
vsize: 467312
[startup+860.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 124251 0 0 0 85669 342 0 0 25 0 1 0 471126879 478662656 105996 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116861 105996 603 41 0 116820 0
vsize: 467444
[startup+870.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 124335 0 0 0 86668 342 0 0 25 0 1 0 471126879 479064064 106080 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116959 106080 603 41 0 116918 0
vsize: 467836
[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 124522 0 0 0 87667 343 0 0 25 0 1 0 471126879 479854592 106267 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117152 106267 603 41 0 117111 0
vsize: 468608
[startup+890.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 125246 0 0 0 88665 346 0 0 25 0 1 0 471126879 482779136 106991 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117866 106991 603 41 0 117825 0
vsize: 471464
[startup+900.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 125817 0 0 0 89664 347 0 0 25 0 1 0 471126879 485023744 107562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118414 107562 603 41 0 118373 0
vsize: 473656
[startup+910.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 126305 0 0 0 90662 349 0 0 25 0 1 0 471126879 487137280 108050 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118930 108050 603 41 0 118889 0
vsize: 475720
[startup+920.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 126707 0 0 0 91661 350 0 0 25 0 1 0 471126879 488722432 108452 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119317 108452 603 41 0 119276 0
vsize: 477268
[startup+930.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 127139 0 0 0 92659 353 0 0 25 0 1 0 471126879 490586112 108884 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119772 108884 603 41 0 119731 0
vsize: 479088
[startup+940.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 127552 0 0 0 93657 355 0 0 25 0 1 0 471126879 492183552 109297 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120162 109297 603 41 0 120121 0
vsize: 480648
[startup+950.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 127932 0 0 0 94656 356 0 0 25 0 1 0 471126879 493772800 109677 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120550 109677 603 41 0 120509 0
vsize: 482200
[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 128282 0 0 0 95654 358 0 0 25 0 1 0 471126879 495226880 110027 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120905 110027 603 41 0 120864 0
vsize: 483620
[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 128584 0 0 0 96653 359 0 0 25 0 1 0 471126879 496541696 110329 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121226 110329 603 41 0 121185 0
vsize: 484904
[startup+980.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 128839 0 0 0 97652 360 0 0 25 0 1 0 471126879 497545216 110584 4294967295 134512640 134672761 3221224544 3221223728 134615964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121471 110584 603 41 0 121430 0
vsize: 485884
[startup+990.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 129091 0 0 0 98651 361 0 0 25 0 1 0 471126879 498597888 110836 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121728 110836 603 41 0 121687 0
vsize: 486912
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 129316 0 0 0 99651 362 0 0 25 0 1 0 471126879 499523584 111061 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121954 111061 603 41 0 121913 0
vsize: 487816
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 129535 0 0 0 100650 362 0 0 25 0 1 0 471126879 500494336 111280 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122191 111280 603 41 0 122150 0
vsize: 488764
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 129735 0 0 0 101649 363 0 0 25 0 1 0 471126879 502272000 111480 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122625 111480 603 41 0 122584 0
vsize: 490500
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 129923 0 0 0 102649 364 0 0 25 0 1 0 471126879 503062528 111668 4294967295 134512640 134672761 3221224544 3221223584 134612819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122818 111668 603 41 0 122777 0
vsize: 491272
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 130102 0 0 0 103648 365 0 0 25 0 1 0 471126879 503857152 111847 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123012 111847 603 41 0 122971 0
vsize: 492048
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 130308 0 0 0 104646 366 0 0 25 0 1 0 471126879 504754176 112053 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123231 112053 603 41 0 123190 0
vsize: 492924
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 130525 0 0 0 105646 367 0 0 25 0 1 0 471126879 505655296 112270 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123451 112270 603 41 0 123410 0
vsize: 493804
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 130756 0 0 0 106645 368 0 0 25 0 1 0 471126879 506568704 112501 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123674 112501 603 41 0 123633 0
vsize: 494696
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 131051 0 0 0 107644 369 0 0 25 0 1 0 471126879 507772928 112796 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123968 112796 603 41 0 123927 0
vsize: 495872
[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 131399 0 0 0 108642 371 0 0 25 0 1 0 471126879 509243392 113144 4294967295 134512640 134672761 3221224544 3221223536 134603141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124327 113144 603 41 0 124286 0
vsize: 497308
[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 131739 0 0 0 109641 372 0 0 25 0 1 0 471126879 510574592 113484 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124652 113484 603 41 0 124611 0
vsize: 498608
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 131939 0 0 0 110640 373 0 0 25 0 1 0 471126879 511393792 113684 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124852 113684 603 41 0 124811 0
vsize: 499408
[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 131963 0 0 0 111640 373 0 0 25 0 1 0 471126879 511528960 113708 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124885 113708 603 41 0 124844 0
vsize: 499540
[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 132034 0 0 0 112640 374 0 0 25 0 1 0 471126879 511799296 113779 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124951 113779 603 41 0 124910 0
vsize: 499804
[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 132219 0 0 0 113639 375 0 0 25 0 1 0 471126879 512602112 113964 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125147 113964 603 41 0 125106 0
vsize: 500588
[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 132245 0 0 0 114639 375 0 0 25 0 1 0 471126879 512737280 113990 4294967295 134512640 134672761 3221224544 3221223680 134614656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125180 113990 603 41 0 125139 0
vsize: 500720
[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 132395 0 0 0 115639 376 0 0 25 0 1 0 471126879 513265664 114140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125309 114140 603 41 0 125268 0
vsize: 501236
[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 132476 0 0 0 116638 376 0 0 25 0 1 0 471126879 513531904 114221 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125374 114221 603 41 0 125333 0
vsize: 501496
[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 132496 0 0 0 117638 376 0 0 25 0 1 0 471126879 513667072 114241 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125407 114241 603 41 0 125366 0
vsize: 501628
[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 132669 0 0 0 118638 377 0 0 25 0 1 0 471126879 514342912 114414 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125572 114414 603 41 0 125531 0
vsize: 502288
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24667
Raw data (stat): 24667 (minisat+) R 24666 26667 26666 0 -1 0 132896 0 0 0 119637 378 0 0 25 0 1 0 471126879 515272704 114641 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125799 114641 603 41 0 125758 0
vsize: 503196
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.31 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 24667
Raw data (stat): 24667 (minisat+) Z 24666 26667 26666 0 -1 12 132896 0 0 0 119637 401 0 0 25 0 1 0 471126879 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.31
CPU time (s): 1200.38
CPU user time (s): 1196.37
CPU system time (s): 4.01039
CPU usage (%): 100.006
Max. virtual memory (Kb): 503196
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####