PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        628856 kB
Buffers:         33096 kB
Cached:         344308 kB
SwapCached:        540 kB
Active:         126008 kB
Inactive:       253360 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        628604 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              44 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20592 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 10:41:49 (client local time) WITH STATUS 0 IN 1200.6 SECONDS
stats: 10788 7 1200.6 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1051 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): (none)
c ---[1050]---> BDD-cost:   10
c ---[1049]---> BDD-cost:   10
c ---[1048]---> BDD-cost:   10
c ---[1047]---> BDD-cost:   10
c ---[1046]---> BDD-cost:   10
c ---[1045]---> BDD-cost:   10
c ---[1044]---> BDD-cost:   10
c ---[1043]---> BDD-cost:   10
c ---[1042]---> BDD-cost:   10
c ---[1041]---> BDD-cost:   10
c ---[1040]---> BDD-cost:   10
c ---[1039]---> BDD-cost:   10
c ---[1038]---> BDD-cost:   10
c ---[1037]---> BDD-cost:   10
c ---[1036]---> BDD-cost:   10
c ---[1035]---> BDD-cost:   10
c ---[1034]---> BDD-cost:   10
c ---[1033]---> BDD-cost:   10
c ---[1032]---> BDD-cost:   10
c ---[1031]---> BDD-cost:   10
c ---[1030]---> BDD-cost:   10
c ---[1029]---> BDD-cost:   10
c ---[1028]---> BDD-cost:   10
c ---[1027]---> BDD-cost:   10
c ---[1026]---> BDD-cost:   10
c ---[1025]---> BDD-cost:   10
c ---[1024]---> BDD-cost:   10
c ---[1023]---> BDD-cost:   10
c ---[1022]---> BDD-cost:   10
c ---[1021]---> BDD-cost:   10
c ---[1020]---> BDD-cost:   10
c ---[1019]---> BDD-cost:   10
c ---[1018]---> BDD-cost:   10
c ---[1017]---> BDD-cost:   10
c ---[1016]---> BDD-cost:   10
c ---[1015]---> BDD-cost:   10
c ---[1014]---> BDD-cost:   10
c ---[1013]---> BDD-cost:   10
c ---[1012]---> BDD-cost:   10
c ---[1011]---> BDD-cost:   10
c ---[1010]---> BDD-cost:   10
c ---[1009]---> BDD-cost:   10
c ---[1008]---> BDD-cost:   10
c ---[1007]---> BDD-cost:   10
c ---[1006]---> BDD-cost:   10
c ---[1005]---> BDD-cost:   10
c ---[1004]---> BDD-cost:   10
c ---[1003]---> BDD-cost:   10
c ---[1002]---> BDD-cost:   10
c ---[1001]---> BDD-cost:   10
c ---[1000]---> BDD-cost:   10
c ---[ 999]---> BDD-cost:   10
c ---[ 998]---> BDD-cost:   10
c ---[ 997]---> BDD-cost:   10
c ---[ 996]---> BDD-cost:   10
c ---[ 995]---> BDD-cost:   10
c ---[ 994]---> BDD-cost:   10
c ---[ 993]---> BDD-cost:   10
c ---[ 992]---> BDD-cost:   10
c ---[ 991]---> BDD-cost:   10
c ---[ 990]---> BDD-cost:   10
c ---[ 989]---> BDD-cost:   10
c ---[ 988]---> BDD-cost:   10
c ---[ 987]---> BDD-cost:   10
c ---[ 986]---> BDD-cost:   10
c ---[ 985]---> BDD-cost:   10
c ---[ 984]---> BDD-cost:   10
c ---[ 983]---> BDD-cost:   10
c ---[ 982]---> BDD-cost:   10
c ---[ 981]---> BDD-cost:   10
c ---[ 980]---> BDD-cost:   10
c ---[ 979]---> BDD-cost:   10
c ---[ 978]---> BDD-cost:   10
c ---[ 977]---> BDD-cost:   10
c ---[ 976]---> BDD-cost:   10
c ---[ 975]---> BDD-cost:   10
c ---[ 974]---> BDD-cost:   10
c ---[ 973]---> BDD-cost:   10
c ---[ 972]---> BDD-cost:   10
c ---[ 971]---> BDD-cost:   10
c ---[ 970]---> BDD-cost:   10
c ---[ 969]---> BDD-cost:   10
c ---[ 968]---> BDD-cost:   10
c ---[ 967]---> BDD-cost:   10
c ---[ 966]---> BDD-cost:   10
c ---[ 965]---> BDD-cost:   10
c ---[ 964]---> BDD-cost:   10
c ---[ 963]---> BDD-cost:   10
c ---[ 962]---> BDD-cost:   10
c ---[ 961]---> BDD-cost:   10
c ---[ 960]---> BDD-cost:   10
c ---[ 959]---> BDD-cost:   10
c ---[ 958]---> BDD-cost:   10
c ---[ 957]---> BDD-cost:   10
c ---[ 956]---> BDD-cost:   10
c ---[ 955]---> BDD-cost:   10
c ---[ 954]---> BDD-cost:   10
c ---[ 953]---> BDD-cost:   10
c ---[ 952]---> BDD-cost:   10
c ---[ 951]---> BDD-cost:   10
c ---[ 950]---> BDD-cost:   10
c ---[ 949]---> BDD-cost:   10
c ---[ 948]---> BDD-cost:   10
c ---[ 947]---> BDD-cost:   10
c ---[ 946]---> BDD-cost:   10
c ---[ 945]---> BDD-cost:   10
c ---[ 944]---> BDD-cost:   10
c ---[ 943]---> BDD-cost:   10
c ---[ 942]---> BDD-cost:   10
c ---[ 941]---> BDD-cost:   10
c ---[ 940]---> BDD-cost:   10
c ---[ 939]---> BDD-cost:   10
c ---[ 938]---> BDD-cost:   10
c ---[ 937]---> BDD-cost:   10
c ---[ 936]---> BDD-cost:   10
c ---[ 935]---> BDD-cost:   10
c ---[ 934]---> BDD-cost:   10
c ---[ 933]---> BDD-cost:   10
c ---[ 932]---> BDD-cost:   10
c ---[ 931]---> BDD-cost:   10
c ---[ 930]---> BDD-cost:   10
c ---[ 929]---> BDD-cost:   10
c ---[ 928]---> BDD-cost:   10
c ---[ 927]---> BDD-cost:   10
c ---[ 926]---> BDD-cost:   10
c ---[ 925]---> BDD-cost:   10
c ---[ 924]---> BDD-cost:   10
c ---[ 923]---> BDD-cost:   10
c ---[ 922]---> BDD-cost:   10
c ---[ 921]---> BDD-cost:   10
c ---[ 920]---> BDD-cost:   10
c ---[ 919]---> BDD-cost:   10
c ---[ 918]---> BDD-cost:   10
c ---[ 917]---> BDD-cost:   10
c ---[ 916]---> BDD-cost:   10
c ---[ 915]---> BDD-cost:   10
c ---[ 914]---> BDD-cost:   10
c ---[ 913]---> BDD-cost:   10
c ---[ 912]---> BDD-cost:   10
c ---[ 911]---> BDD-cost:   10
c ---[ 910]---> BDD-cost:   10
c ---[ 909]---> BDD-cost:   10
c ---[ 908]---> BDD-cost:   10
c ---[ 907]---> BDD-cost:   10
c ---[ 906]---> BDD-cost:   10
c ---[ 905]---> BDD-cost:   10
c ---[ 904]---> BDD-cost:   10
c ---[ 903]---> BDD-cost:   10
c ---[ 902]---> BDD-cost:   10
c ---[ 901]---> BDD-cost:   10
c ---[ 900]---> BDD-cost:   10
c ---[ 899]---> BDD-cost:   10
c ---[ 898]---> BDD-cost:   10
c ---[ 897]---> BDD-cost:   10
c ---[ 896]---> BDD-cost:   10
c ---[ 895]---> BDD-cost:   10
c ---[ 894]---> BDD-cost:   10
c ---[ 893]---> BDD-cost:   10
c ---[ 892]---> BDD-cost:   10
c ---[ 891]---> BDD-cost:   10
c ---[ 890]---> BDD-cost:   10
c ---[ 889]---> BDD-cost:   10
c ---[ 888]---> BDD-cost:   10
c ---[ 887]---> BDD-cost:   10
c ---[ 886]---> BDD-cost:   10
c ---[ 885]---> BDD-cost:   10
c ---[ 884]---> BDD-cost:   10
c ---[ 883]---> BDD-cost:   10
c ---[ 882]---> BDD-cost:   10
c ---[ 881]---> BDD-cost:   10
c ---[ 880]---> BDD-cost:   10
c ---[ 879]---> BDD-cost:   10
c ---[ 878]---> BDD-cost:   10
c ---[ 877]---> BDD-cost:   10
c ---[ 876]---> BDD-cost:   10
c ---[ 875]---> BDD-cost:   10
c ---[ 874]---> BDD-cost:   10
c ---[ 873]---> BDD-cost:   10
c ---[ 872]---> BDD-cost:   10
c ---[ 871]---> BDD-cost:   10
c ---[ 870]---> BDD-cost:   10
c ---[ 869]---> BDD-cost:   10
c ---[ 868]---> BDD-cost:   10
c ---[ 867]---> BDD-cost:   10
c ---[ 866]---> BDD-cost:   10
c ---[ 865]---> BDD-cost:   10
c ---[ 864]---> BDD-cost:   10
c ---[ 863]---> BDD-cost:   10
c ---[ 862]---> BDD-cost:   10
c ---[ 861]---> BDD-cost:   10
c ---[ 860]---> BDD-cost:   10
c ---[ 859]---> BDD-cost:   10
c ---[ 858]---> BDD-cost:   10
c ---[ 857]---> BDD-cost:   10
c ---[ 856]---> BDD-cost:   10
c ---[ 855]---> BDD-cost:   10
c ---[ 854]---> BDD-cost:   10
c ---[ 853]---> BDD-cost:   10
c ---[ 852]---> BDD-cost:   10
c ---[ 851]---> BDD-cost:   10
c ---[ 850]---> BDD-cost:   10
c ---[ 849]---> BDD-cost:   10
c ---[ 848]---> BDD-cost:   10
c ---[ 847]---> BDD-cost:   10
c ---[ 846]---> BDD-cost:   10
c ---[ 845]---> BDD-cost:   10
c ---[ 844]---> BDD-cost:   10
c ---[ 843]---> BDD-cost:   10
c ---[ 842]---> BDD-cost:   10
c ---[ 841]---> BDD-cost:   10
c ---[ 840]---> BDD-cost:   10
c ---[ 839]---> BDD-cost:   10
c ---[ 838]---> BDD-cost:   10
c ---[ 837]---> BDD-cost:   10
c ---[ 836]---> BDD-cost:   10
c ---[ 835]---> BDD-cost:   10
c ---[ 834]---> BDD-cost:   10
c ---[ 833]---> BDD-cost:   10
c ---[ 832]---> BDD-cost:   10
c ---[ 831]---> BDD-cost:   10
c ---[ 830]---> BDD-cost:   10
c ---[ 829]---> BDD-cost:   10
c ---[ 828]---> BDD-cost:   10
c ---[ 827]---> BDD-cost:   10
c ---[ 826]---> BDD-cost:   10
c ---[ 825]---> BDD-cost:   10
c ---[ 824]---> BDD-cost:   10
c ---[ 823]---> BDD-cost:   10
c ---[ 822]---> BDD-cost:   10
c ---[ 821]---> BDD-cost:   10
c ---[ 820]---> BDD-cost:   10
c ---[ 819]---> BDD-cost:   10
c ---[ 818]---> BDD-cost:   10
c ---[ 817]---> BDD-cost:   10
c ---[ 816]---> BDD-cost:   10
c ---[ 815]---> BDD-cost:   10
c ---[ 814]---> BDD-cost:   10
c ---[ 813]---> BDD-cost:   10
c ---[ 812]---> BDD-cost:   10
c ---[ 811]---> BDD-cost:   10
c ---[ 810]---> BDD-cost:   10
c ---[ 809]---> BDD-cost:   10
c ---[ 808]---> BDD-cost:   10
c ---[ 807]---> BDD-cost:   10
c ---[ 806]---> BDD-cost:   10
c ---[ 805]---> BDD-cost:   10
c ---[ 804]---> BDD-cost:   10
c ---[ 803]---> BDD-cost:   10
c ---[ 802]---> BDD-cost:   10
c ---[ 801]---> BDD-cost:   10
c ---[ 800]---> BDD-cost:   10
c ---[ 799]---> BDD-cost:   10
c ---[ 798]---> BDD-cost:   10
c ---[ 797]---> BDD-cost:   10
c ---[ 796]---> BDD-cost:   10
c ---[ 795]---> BDD-cost:   10
c ---[ 794]---> BDD-cost:   10
c ---[ 793]---> BDD-cost:   10
c ---[ 792]---> BDD-cost:   10
c ---[ 791]---> BDD-cost:   10
c ---[ 790]---> BDD-cost:   10
c ---[ 789]---> BDD-cost:   10
c ---[ 788]---> BDD-cost:   10
c ---[ 787]---> BDD-cost:   10
c ---[ 786]---> BDD-cost:   10
c ---[ 785]---> BDD-cost:   10
c ---[ 784]---> BDD-cost:   10
c ---[ 783]---> BDD-cost:   10
c ---[ 782]---> BDD-cost:   10
c ---[ 781]---> BDD-cost:   10
c ---[ 780]---> BDD-cost:   10
c ---[ 779]---> BDD-cost:   10
c ---[ 778]---> BDD-cost:   10
c ---[ 777]---> BDD-cost:   10
c ---[ 776]---> BDD-cost:   10
c ---[ 775]---> BDD-cost:   10
c ---[ 774]---> BDD-cost:   10
c ---[ 773]---> BDD-cost:   10
c ---[ 772]---> BDD-cost:   10
c ---[ 771]---> BDD-cost:   10
c ---[ 770]---> BDD-cost:   10
c ---[ 769]---> BDD-cost:   10
c ---[ 768]---> BDD-cost:   10
c ---[ 767]---> BDD-cost:   10
c ---[ 766]---> BDD-cost:   10
c ---[ 765]---> BDD-cost:   10
c ---[ 764]---> BDD-cost:   10
c ---[ 763]---> BDD-cost:   10
c ---[ 762]---> BDD-cost:   10
c ---[ 761]---> BDD-cost:   10
c ---[ 760]---> BDD-cost:   10
c ---[ 759]---> BDD-cost:   10
c ---[ 758]---> BDD-cost:   10
c ---[ 757]---> BDD-cost:   10
c ---[ 756]---> BDD-cost:   10
c ---[ 755]---> BDD-cost:   10
c ---[ 754]---> BDD-cost:   10
c ---[ 753]---> BDD-cost:   10
c ---[ 752]---> BDD-cost:   10
c ---[ 751]---> BDD-cost:   10
c ---[ 750]---> BDD-cost:   10
c ---[ 749]---> BDD-cost:   10
c ---[ 748]---> BDD-cost:   10
c ---[ 747]---> BDD-cost:   10
c ---[ 746]---> BDD-cost:   10
c ---[ 745]---> BDD-cost:   10
c ---[ 744]---> BDD-cost:   10
c ---[ 743]---> BDD-cost:   10
c ---[ 742]---> BDD-cost:   10
c ---[ 741]---> BDD-cost:   10
c ---[ 740]---> BDD-cost:   10
c ---[ 739]---> BDD-cost:   10
c ---[ 738]---> BDD-cost:   10
c ---[ 737]---> BDD-cost:   10
c ---[ 736]---> BDD-cost:   10
c ---[ 735]---> BDD-cost:   10
c ---[ 734]---> BDD-cost:   10
c ---[ 733]---> BDD-cost:   10
c ---[ 732]---> BDD-cost:   10
c ---[ 731]---> BDD-cost:   10
c ---[ 730]---> BDD-cost:   10
c ---[ 729]---> BDD-cost:   10
c ---[ 728]---> BDD-cost:   10
c ---[ 727]---> BDD-cost:   10
c ---[ 726]---> BDD-cost:   10
c ---[ 725]---> BDD-cost:   10
c ---[ 724]---> BDD-cost:   10
c ---[ 723]---> BDD-cost:   10
c ---[ 722]---> BDD-cost:   10
c ---[ 721]---> BDD-cost:   10
c ---[ 720]---> BDD-cost:   10
c ---[ 719]---> BDD-cost:   10
c ---[ 718]---> BDD-cost:   10
c ---[ 717]---> BDD-cost:   10
c ---[ 716]---> BDD-cost:   10
c ---[ 715]---> BDD-cost:   10
c ---[ 714]---> BDD-cost:   10
c ---[ 713]---> BDD-cost:   10
c ---[ 712]---> BDD-cost:   10
c ---[ 711]---> BDD-cost:   10
c ---[ 710]---> BDD-cost:   10
c ---[ 709]---> BDD-cost:   10
c ---[ 708]---> BDD-cost:   10
c ---[ 707]---> BDD-cost:   10
c ---[ 706]---> BDD-cost:   10
c ---[ 705]---> BDD-cost:   10
c ---[ 704]---> BDD-cost:   10
c ---[ 703]---> BDD-cost:   10
c ---[ 702]---> BDD-cost:   10
c ---[ 701]---> BDD-cost:   10
c ---[ 700]---> BDD-cost:   10
c ---[ 699]---> BDD-cost:   10
c ---[ 698]---> BDD-cost:   10
c ---[ 697]---> BDD-cost:   10
c ---[ 696]---> BDD-cost:   10
c ---[ 695]---> BDD-cost:   10
c ---[ 694]---> BDD-cost:   10
c ---[ 693]---> BDD-cost:   10
c ---[ 692]---> BDD-cost:   10
c ---[ 691]---> BDD-cost:   10
c ---[ 690]---> BDD-cost:   10
c ---[ 689]---> BDD-cost:   10
c ---[ 688]---> BDD-cost:   10
c ---[ 687]---> BDD-cost:   10
c ---[ 686]---> BDD-cost:   10
c ---[ 685]---> BDD-cost:   10
c ---[ 684]---> BDD-cost:   10
c ---[ 683]---> BDD-cost:   10
c ---[ 682]---> BDD-cost:   10
c ---[ 681]---> BDD-cost:   10
c ---[ 680]---> BDD-cost:   10
c ---[ 679]---> BDD-cost:   10
c ---[ 678]---> BDD-cost:   10
c ---[ 677]---> BDD-cost:   10
c ---[ 676]---> BDD-cost:   10
c ---[ 675]---> BDD-cost:   10
c ---[ 674]---> BDD-cost:   10
c ---[ 673]---> BDD-cost:   10
c ---[ 672]---> BDD-cost:   10
c ---[ 671]---> BDD-cost:   10
c ---[ 670]---> BDD-cost:   10
c ---[ 669]---> BDD-cost:   10
c ---[ 668]---> BDD-cost:   10
c ---[ 667]---> BDD-cost:   10
c ---[ 666]---> BDD-cost:   10
c ---[ 665]---> BDD-cost:   10
c ---[ 664]---> BDD-cost:   10
c ---[ 663]---> BDD-cost:   10
c ---[ 662]---> BDD-cost:   10
c ---[ 661]---> BDD-cost:   10
c ---[ 660]---> BDD-cost:   10
c ---[ 659]---> BDD-cost:   10
c ---[ 658]---> BDD-cost:   10
c ---[ 657]---> BDD-cost:   10
c ---[ 656]---> BDD-cost:   10
c ---[ 655]---> BDD-cost:   10
c ---[ 654]---> BDD-cost:   10
c ---[ 653]---> BDD-cost:   10
c ---[ 652]---> BDD-cost:   10
c ---[ 651]---> BDD-cost:   10
c ---[ 650]---> BDD-cost:   10
c ---[ 649]---> BDD-cost:   10
c ---[ 648]---> BDD-cost:   10
c ---[ 647]---> BDD-cost:   10
c ---[ 646]---> BDD-cost:   10
c ---[ 645]---> BDD-cost:   10
c ---[ 644]---> BDD-cost:   10
c ---[ 643]---> BDD-cost:   10
c ---[ 642]---> BDD-cost:   10
c ---[ 641]---> BDD-cost:   10
c ---[ 640]---> BDD-cost:   10
c ---[ 639]---> BDD-cost:   10
c ---[ 638]---> BDD-cost:   10
c ---[ 637]---> BDD-cost:   10
c ---[ 636]---> BDD-cost:   10
c ---[ 635]---> BDD-cost:   10
c ---[ 634]---> BDD-cost:   10
c ---[ 633]---> BDD-cost:   10
c ---[ 632]---> BDD-cost:   10
c ---[ 631]---> BDD-cost:   10
c ---[ 630]---> BDD-cost:   10
c ---[ 629]---> BDD-cost:   10
c ---[ 628]---> BDD-cost:   10
c ---[ 627]---> BDD-cost:   10
c ---[ 626]---> BDD-cost:   10
c ---[ 625]---> BDD-cost:   10
c ---[ 624]---> BDD-cost:   10
c ---[ 623]---> BDD-cost:   10
c ---[ 622]---> BDD-cost:   10
c ---[ 621]---> BDD-cost:   10
c ---[ 620]---> BDD-cost:   10
c ---[ 619]---> BDD-cost:   10
c ---[ 618]---> BDD-cost:   10
c ---[ 617]---> BDD-cost:   10
c ---[ 616]---> BDD-cost:   10
c ---[ 615]---> BDD-cost:   10
c ---[ 614]---> BDD-cost:   10
c ---[ 613]---> BDD-cost:   10
c ---[ 612]---> BDD-cost:   10
c ---[ 611]---> BDD-cost:   10
c ---[ 610]---> BDD-cost:   10
c ---[ 609]---> BDD-cost:   10
c ---[ 608]---> BDD-cost:   10
c ---[ 607]---> BDD-cost:   10
c ---[ 606]---> BDD-cost:   10
c ---[ 605]---> BDD-cost:   10
c ---[ 604]---> BDD-cost:   10
c ---[ 603]---> BDD-cost:   10
c ---[ 602]---> BDD-cost:   10
c ---[ 601]---> BDD-cost:   10
c ---[ 600]---> BDD-cost:   10
c ---[ 599]---> BDD-cost:   10
c ---[ 598]---> BDD-cost:   10
c ---[ 597]---> BDD-cost:   10
c ---[ 596]---> BDD-cost:   10
c ---[ 595]---> BDD-cost:   10
c ---[ 594]---> BDD-cost:   10
c ---[ 593]---> BDD-cost:   10
c ---[ 592]---> BDD-cost:   10
c ---[ 591]---> BDD-cost:   10
c ---[ 590]---> BDD-cost:   10
c ---[ 589]---> BDD-cost:   10
c ---[ 588]---> BDD-cost:   10
c ---[ 587]---> BDD-cost:   10
c ---[ 586]---> BDD-cost:   10
c ---[ 585]---> BDD-cost:   10
c ---[ 584]---> BDD-cost:   10
c ---[ 583]---> BDD-cost:   10
c ---[ 582]---> BDD-cost:   10
c ---[ 581]---> BDD-cost:   10
c ---[ 580]---> BDD-cost:   10
c ---[ 579]---> BDD-cost:   10
c ---[ 578]---> BDD-cost:   10
c ---[ 577]---> BDD-cost:   10
c ---[ 576]---> BDD-cost:   10
c ---[ 575]---> BDD-cost:   10
c ---[ 574]---> BDD-cost:   10
c ---[ 573]---> BDD-cost:   10
c ---[ 572]---> BDD-cost:   10
c ---[ 571]---> BDD-cost:   10
c ---[ 570]---> BDD-cost:   10
c ---[ 569]---> BDD-cost:   10
c ---[ 568]---> BDD-cost:   10
c ---[ 567]---> BDD-cost:   10
c ---[ 566]---> BDD-cost:   10
c ---[ 565]---> BDD-cost:   10
c ---[ 564]---> BDD-cost:   10
c ---[ 563]---> BDD-cost:   10
c ---[ 562]---> BDD-cost:   10
c ---[ 561]---> BDD-cost:   10
c ---[ 560]---> BDD-cost:   10
c ---[ 559]---> BDD-cost:   10
c ---[ 558]---> BDD-cost:   10
c ---[ 557]---> BDD-cost:   10
c ---[ 556]---> BDD-cost:   10
c ---[ 555]---> BDD-cost:   10
c ---[ 554]---> BDD-cost:   10
c ---[ 553]---> BDD-cost:   10
c ---[ 552]---> BDD-cost:   10
c ---[ 551]---> BDD-cost:   10
c ---[ 550]---> BDD-cost:   10
c ---[ 549]---> BDD-cost:   10
c ---[ 548]---> BDD-cost:   10
c ---[ 547]---> BDD-cost:   10
c ---[ 546]---> BDD-cost:   10
c ---[ 545]---> BDD-cost:   10
c ---[ 544]---> BDD-cost:   10
c ---[ 543]---> BDD-cost:   10
c ---[ 542]---> BDD-cost:   10
c ---[ 541]---> BDD-cost:   10
c ---[ 540]---> BDD-cost:   10
c ---[ 539]---> BDD-cost:   10
c ---[ 538]---> BDD-cost:   10
c ---[ 537]---> BDD-cost:   10
c ---[ 536]---> BDD-cost:   10
c ---[ 535]---> BDD-cost:   10
c ---[ 534]---> BDD-cost:   10
c ---[ 533]---> BDD-cost:   10
c ---[ 532]---> BDD-cost:   10
c ---[ 531]---> BDD-cost:   10
c ---[ 530]---> BDD-cost:   10
c ---[ 529]---> BDD-cost:   10
c ---[ 528]---> BDD-cost:   10
c ---[ 527]---> BDD-cost:   10
c ---[ 526]---> BDD-cost:   10
c ---[ 525]---> BDD-cost:   10
c ---[ 524]---> BDD-cost:   10
c ---[ 523]---> BDD-cost:   10
c ---[ 522]---> BDD-cost:   10
c ---[ 521]---> BDD-cost:   10
c ---[ 520]---> BDD-cost:   10
c ---[ 519]---> BDD-cost:   10
c ---[ 518]---> BDD-cost:   10
c ---[ 517]---> BDD-cost:   10
c ---[ 516]---> BDD-cost:   10
c ---[ 515]---> BDD-cost:   10
c ---[ 514]---> BDD-cost:   10
c ---[ 513]---> BDD-cost:   10
c ---[ 512]---> BDD-cost:   10
c ---[ 511]---> BDD-cost:   10
c ---[ 510]---> BDD-cost:   10
c ---[ 509]---> BDD-cost:   10
c ---[ 508]---> BDD-cost:   10
c ---[ 507]---> BDD-cost:   10
c ---[ 506]---> BDD-cost:   10
c ---[ 505]---> BDD-cost:   10
c ---[ 504]---> BDD-cost:   10
c ---[ 503]---> BDD-cost:   10
c ---[ 502]---> BDD-cost:   10
c ---[ 501]---> BDD-cost:   10
c ---[ 500]---> BDD-cost:   10
c ---[ 499]---> BDD-cost:   10
c ---[ 498]---> BDD-cost:   10
c ---[ 497]---> BDD-cost:   10
c ---[ 496]---> BDD-cost:   10
c ---[ 495]---> BDD-cost:   10
c ---[ 494]---> BDD-cost:   10
c ---[ 493]---> BDD-cost:   10
c ---[ 492]---> BDD-cost:   10
c ---[ 491]---> BDD-cost:   10
c ---[ 490]---> BDD-cost:   10
c ---[ 489]---> BDD-cost:   10
c ---[ 488]---> BDD-cost:   10
c ---[ 487]---> BDD-cost:   10
c ---[ 486]---> BDD-cost:   10
c ---[ 485]---> BDD-cost:   10
c ---[ 484]---> BDD-cost:   10
c ---[ 483]---> BDD-cost:   10
c ---[ 482]---> BDD-cost:   10
c ---[ 481]---> BDD-cost:   10
c ---[ 480]---> BDD-cost:   10
c ---[ 479]---> BDD-cost:   10
c ---[ 478]---> BDD-cost:   10
c ---[ 477]---> BDD-cost:   10
c ---[ 476]---> BDD-cost:   10
c ---[ 475]---> BDD-cost:   10
c ---[ 474]---> BDD-cost:   10
c ---[ 473]---> BDD-cost:   10
c ---[ 472]---> BDD-cost:   10
c ---[ 471]---> BDD-cost:   10
c ---[ 470]---> BDD-cost:   10
c ---[ 469]---> BDD-cost:   10
c ---[ 468]---> BDD-cost:   10
c ---[ 467]---> BDD-cost:   10
c ---[ 466]---> BDD-cost:   10
c ---[ 465]---> BDD-cost:   10
c ---[ 464]---> BDD-cost:   10
c ---[ 463]---> BDD-cost:   10
c ---[ 462]---> BDD-cost:   10
c ---[ 461]---> BDD-cost:   10
c ---[ 460]---> BDD-cost:   10
c ---[ 459]---> BDD-cost:   10
c ---[ 458]---> BDD-cost:   10
c ---[ 457]---> BDD-cost:   10
c ---[ 456]---> BDD-cost:   10
c ---[ 455]---> BDD-cost:   10
c ---[ 454]---> BDD-cost:   10
c ---[ 453]---> BDD-cost:   10
c ---[ 452]---> BDD-cost:   10
c ---[ 451]---> BDD-cost:   10
c ---[ 450]---> BDD-cost:   10
c ---[ 449]---> BDD-cost:   10
c ---[ 448]---> BDD-cost:   10
c ---[ 447]---> BDD-cost:   10
c ---[ 446]---> BDD-cost:   10
c ---[ 445]---> BDD-cost:   10
c ---[ 444]---> BDD-cost:   10
c ---[ 443]---> BDD-cost:   10
c ---[ 442]---> BDD-cost:   10
c ---[ 441]---> BDD-cost:   10
c ---[ 440]---> BDD-cost:   10
c ---[ 439]---> BDD-cost:   10
c ---[ 438]---> BDD-cost:   10
c ---[ 437]---> BDD-cost:   10
c ---[ 436]---> BDD-cost:   10
c ---[ 435]---> BDD-cost:   10
c ---[ 434]---> BDD-cost:   10
c ---[ 433]---> BDD-cost:   10
c ---[ 432]---> BDD-cost:   10
c ---[ 431]---> BDD-cost:   10
c ---[ 430]---> BDD-cost:   10
c ---[ 429]---> BDD-cost:   10
c ---[ 428]---> BDD-cost:   10
c ---[ 427]---> BDD-cost:   10
c ---[ 426]---> BDD-cost:   10
c ---[ 425]---> BDD-cost:   10
c ---[ 424]---> BDD-cost:   10
c ---[ 423]---> BDD-cost:   10
c ---[ 422]---> BDD-cost:   10
c ---[ 421]---> BDD-cost:   10
c ---[ 420]---> BDD-cost:   10
c ---[ 419]---> BDD-cost:   10
c ---[ 418]---> BDD-cost:   10
c ---[ 417]---> BDD-cost:   10
c ---[ 416]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   10
c ---[ 414]---> BDD-cost:   10
c ---[ 413]---> BDD-cost:   10
c ---[ 412]---> BDD-cost:   10
c ---[ 411]---> BDD-cost:   10
c ---[ 410]---> BDD-cost:   10
c ---[ 409]---> BDD-cost:   10
c ---[ 408]---> BDD-cost:   10
c ---[ 407]---> BDD-cost:   10
c ---[ 406]---> BDD-cost:   10
c ---[ 405]---> BDD-cost:   10
c ---[ 404]---> BDD-cost:   10
c ---[ 403]---> BDD-cost:   10
c ---[ 402]---> BDD-cost:   10
c ---[ 401]---> BDD-cost:   10
c ---[ 400]---> BDD-cost:   10
c ---[ 399]---> BDD-cost:   10
c ---[ 398]---> BDD-cost:   10
c ---[ 397]---> BDD-cost:   10
c ---[ 396]---> BDD-cost:   10
c ---[ 395]---> BDD-cost:   10
c ---[ 394]---> BDD-cost:   10
c ---[ 393]---> BDD-cost:   10
c ---[ 392]---> BDD-cost:   10
c ---[ 391]---> BDD-cost:   10
c ---[ 390]---> BDD-cost:   10
c ---[ 389]---> BDD-cost:   10
c ---[ 388]---> BDD-cost:   10
c ---[ 387]---> BDD-cost:   10
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   10
c ---[ 384]---> BDD-cost:   10
c ---[ 383]---> BDD-cost:   10
c ---[ 382]---> BDD-cost:   10
c ---[ 381]---> BDD-cost:   10
c ---[ 380]---> BDD-cost:   10
c ---[ 379]---> BDD-cost:   10
c ---[ 378]---> BDD-cost:   10
c ---[ 377]---> BDD-cost:   10
c ---[ 376]---> BDD-cost:   10
c ---[ 375]---> BDD-cost:   10
c ---[ 374]---> BDD-cost:   10
c ---[ 373]---> BDD-cost:   10
c ---[ 372]---> BDD-cost:   10
c ---[ 371]---> BDD-cost:   10
c ---[ 370]---> BDD-cost:   10
c ---[ 369]---> BDD-cost:   10
c ---[ 368]---> BDD-cost:   10
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 364]---> BDD-cost:   10
c ---[ 363]---> BDD-cost:   10
c ---[ 362]---> BDD-cost:   10
c ---[ 361]---> BDD-cost:   10
c ---[ 360]---> BDD-cost:   10
c ---[ 359]---> BDD-cost:   10
c ---[ 358]---> BDD-cost:   10
c ---[ 357]---> BDD-cost:   10
c ---[ 356]---> BDD-cost:   10
c ---[ 355]---> BDD-cost:   10
c ---[ 354]---> BDD-cost:   10
c ---[ 353]---> BDD-cost:   10
c ---[ 352]---> BDD-cost:   10
c ---[ 351]---> BDD-cost:   10
c ---[ 350]---> BDD-cost:   10
c ---[ 349]---> BDD-cost:   10
c ---[ 348]---> BDD-cost:   10
c ---[ 347]---> BDD-cost:   10
c ---[ 346]---> BDD-cost:   10
c ---[ 345]---> BDD-cost:   10
c ---[ 344]---> BDD-cost:   10
c ---[ 343]---> BDD-cost:   10
c ---[ 342]---> BDD-cost:   10
c ---[ 341]---> BDD-cost:   10
c ---[ 340]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   10
c ---[ 338]---> BDD-cost:   10
c ---[ 337]---> BDD-cost:   10
c ---[ 336]---> BDD-cost:   10
c ---[ 335]---> BDD-cost:   10
c ---[ 334]---> BDD-cost:   10
c ---[ 333]---> BDD-cost:   10
c ---[ 332]---> BDD-cost:   10
c ---[ 331]---> BDD-cost:   10
c ---[ 330]---> BDD-cost:   10
c ---[ 329]---> BDD-cost:   10
c ---[ 328]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:   10
c ---[ 326]---> BDD-cost:   10
c ---[ 325]---> BDD-cost:   10
c ---[ 324]---> BDD-cost:   10
c ---[ 323]---> BDD-cost:   10
c ---[ 322]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   10
c ---[ 320]---> BDD-cost:   10
c ---[ 319]---> BDD-cost:   10
c ---[ 318]---> BDD-cost:   10
c ---[ 317]---> BDD-cost:   10
c ---[ 316]---> BDD-cost:   10
c ---[ 315]---> BDD-cost:   10
c ---[ 314]---> BDD-cost:   10
c ---[ 313]---> BDD-cost:   10
c ---[ 312]---> BDD-cost:   10
c ---[ 311]---> BDD-cost:   10
c ---[ 310]---> BDD-cost:   10
c ---[ 309]---> BDD-cost:   10
c ---[ 308]---> BDD-cost:   10
c ---[ 307]---> BDD-cost:   10
c ---[ 306]---> BDD-cost:   10
c ---[ 305]---> BDD-cost:   10
c ---[ 304]---> BDD-cost:   10
c ---[ 303]---> BDD-cost:   10
c ---[ 302]---> BDD-cost:   10
c ---[ 301]---> BDD-cost:   10
c ---[ 300]---> BDD-cost:   10
c ---[ 299]---> BDD-cost:   10
c ---[ 298]---> BDD-cost:   10
c ---[ 297]---> BDD-cost:   10
c ---[ 296]---> BDD-cost:   10
c ---[ 295]---> BDD-cost:   10
c ---[ 294]---> BDD-cost:   10
c ---[ 293]---> BDD-cost:   10
c ---[ 292]---> BDD-cost:   10
c ---[ 291]---> BDD-cost:   10
c ---[ 290]---> BDD-cost:   10
c ---[ 289]---> BDD-cost:   10
c ---[ 288]---> BDD-cost:   10
c ---[ 287]---> BDD-cost:   10
c ---[ 286]---> BDD-cost:   10
c ---[ 285]---> BDD-cost:   10
c ---[ 284]---> BDD-cost:   10
c ---[ 283]---> BDD-cost:   10
c ---[ 282]---> BDD-cost:   10
c ---[ 281]---> BDD-cost:   10
c ---[ 280]---> BDD-cost:   10
c ---[ 279]---> BDD-cost:   10
c ---[ 278]---> BDD-cost:   10
c ---[ 277]---> BDD-cost:   10
c ---[ 276]---> BDD-cost:   10
c ---[ 275]---> BDD-cost:   10
c ---[ 274]---> BDD-cost:   10
c ---[ 273]---> BDD-cost:   10
c ---[ 272]---> BDD-cost:   10
c ---[ 271]---> BDD-cost:   10
c ---[ 270]---> BDD-cost:   10
c ---[ 269]---> BDD-cost:   10
c ---[ 268]---> BDD-cost:   10
c ---[ 267]---> BDD-cost:   10
c ---[ 266]---> BDD-cost:   10
c ---[ 265]---> BDD-cost:   10
c ---[ 264]---> BDD-cost:   10
c ---[ 263]---> BDD-cost:   10
c ---[ 262]---> BDD-cost:   10
c ---[ 261]---> BDD-cost:   10
c ---[ 260]---> BDD-cost:   10
c ---[ 259]---> BDD-cost:   10
c ---[ 258]---> BDD-cost:   10
c ---[ 257]---> BDD-cost:   10
c ---[ 256]---> BDD-cost:   10
c ---[ 255]---> BDD-cost:   10
c ---[ 254]---> BDD-cost:   10
c ---[ 253]---> BDD-cost:   10
c ---[ 252]---> BDD-cost:   11
c ---[ 251]---> BDD-cost:   11
c ---[ 250]---> BDD-cost:   11
c ---[ 249]---> BDD-cost:   11
c ---[ 248]---> BDD-cost:   11
c ---[ 247]---> BDD-cost:   11
c ---[ 246]---> BDD-cost:   11
c ---[ 245]---> BDD-cost:   11
c ---[ 244]---> BDD-cost:   11
c ---[ 243]---> BDD-cost:   11
c ---[ 242]---> BDD-cost:   11
c ---[ 241]---> BDD-cost:   11
c ---[ 240]---> BDD-cost:   11
c ---[ 239]---> BDD-cost:   11
c ---[ 238]---> BDD-cost:   11
c ---[ 237]---> BDD-cost:   11
c ---[ 236]---> BDD-cost:   11
c ---[ 235]---> BDD-cost:   11
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   11
c ---[ 232]---> BDD-cost:   11
c ---[ 231]---> BDD-cost:   11
c ---[ 230]---> BDD-cost:   11
c ---[ 229]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   11
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   11
c ---[ 225]---> BDD-cost:   11
c ---[ 224]---> BDD-cost:   11
c ---[ 223]---> BDD-cost:   11
c ---[ 222]---> BDD-cost:   11
c ---[ 221]---> BDD-cost:   11
c ---[ 220]---> BDD-cost:   11
c ---[ 219]---> BDD-cost:   11
c ---[ 218]---> BDD-cost:   11
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   11
c ---[ 215]---> BDD-cost:   11
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   11
c ---[ 212]---> BDD-cost:   11
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   11
c ---[ 209]---> BDD-cost:   11
c ---[ 208]---> BDD-cost:   11
c ---[ 207]---> BDD-cost:   11
c ---[ 206]---> BDD-cost:   11
c ---[ 205]---> BDD-cost:   11
c ---[ 204]---> BDD-cost:   11
c ---[ 203]---> BDD-cost:   11
c ---[ 202]---> BDD-cost:   11
c ---[ 201]---> BDD-cost:   11
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:   11
c ---[ 198]---> BDD-cost:   11
c ---[ 197]---> BDD-cost:   11
c ---[ 196]---> BDD-cost:   11
c ---[ 195]---> BDD-cost:   11
c ---[ 194]---> BDD-cost:   11
c ---[ 193]---> BDD-cost:   11
c ---[ 192]---> BDD-cost:   11
c ---[ 191]---> BDD-cost:   11
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:   11
c ---[ 187]---> BDD-cost:   11
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   11
c ---[ 184]---> BDD-cost:   11
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:   11
c ---[ 181]---> BDD-cost:   11
c ---[ 180]---> BDD-cost:   11
c ---[ 179]---> BDD-cost:   11
c ---[ 178]---> BDD-cost:   11
c ---[ 177]---> BDD-cost:   11
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:   11
c ---[ 173]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   11
c ---[ 171]---> BDD-cost:   11
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   11
c ---[ 168]---> BDD-cost:   11
c ---[ 167]---> BDD-cost:   11
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   11
c ---[ 164]---> BDD-cost:   11
c ---[ 163]---> BDD-cost:   11
c ---[ 162]---> BDD-cost:   11
c ---[ 161]---> BDD-cost:   11
c ---[ 160]---> BDD-cost:   11
c ---[ 159]---> BDD-cost:   11
c ---[ 158]---> BDD-cost:   11
c ---[ 157]---> BDD-cost:   11
c ---[ 156]---> BDD-cost:   11
c ---[ 155]---> BDD-cost:   11
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:   11
c ---[ 151]---> BDD-cost:   11
c ---[ 150]---> BDD-cost:   11
c ---[ 149]---> BDD-cost:   11
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:   11
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:   11
c ---[ 143]---> BDD-cost:   11
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   11
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   11
c ---[ 138]---> BDD-cost:   11
c ---[ 137]---> BDD-cost:   11
c ---[ 136]---> BDD-cost:   11
c ---[ 135]---> BDD-cost:   11
c ---[ 134]---> BDD-cost:   11
c ---[ 133]---> BDD-cost:   11
c ---[ 132]---> BDD-cost:   11
c ---[ 131]---> BDD-cost:   11
c ---[ 130]---> BDD-cost:   11
c ---[ 129]---> BDD-cost:   11
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   11
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   11
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   11
c ---[ 121]---> BDD-cost:   11
c ---[ 120]---> BDD-cost:   11
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:   11
c ---[ 117]---> BDD-cost:   11
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:   11
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   11
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   11
c ---[ 109]---> BDD-cost:   11
c ---[ 108]---> BDD-cost:   11
c ---[ 107]---> BDD-cost:   11
c ---[ 106]---> BDD-cost:   11
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   11
c ---[ 103]---> BDD-cost:   11
c ---[ 102]---> BDD-cost:   11
c ---[ 101]---> BDD-cost:   11
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   11
c ---[  73]---> BDD-cost:   11
c ---[  72]---> BDD-cost:   11
c ---[  71]---> BDD-cost:   11
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   11
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   11
c ---[  62]---> BDD-cost:   11
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:   11
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   11
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:   11
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   11
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   11
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   11
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   11
c ---[  23]---> Adder-cost: 22993   maxlim: 816753   bits: 21/20
c ---[  22]---> Adder-cost: 48143   maxlim: 53250657   bits: 27/26
c ---[  21]---> Adder-cost: 24490   maxlim: 37410971   bits: 27/26
c ---[  20]---> Adder-cost: 18532   maxlim: 62407570   bits: 27/26
c ---[  19]---> Adder-cost: 64462   maxlim: 396293572   bits: 30/29
c ---[  18]---> Adder-cost: 9918   maxlim: 1625605   bits: 21/21
c ---[  17]---> Adder-cost: 39824   maxlim: 26785026   bits: 26/25
c ---[  16]---> Adder-cost: 60627   maxlim: 27028587   bits: 26/25
c ---[  15]---> Adder-cost: 50627   maxlim: 58642455   bits: 27/26
c ---[  14]---> Adder-cost: 19026   maxlim: 1373536   bits: 22/21
c ---[  13]---> Adder-cost: 25006   maxlim: 4696498   bits: 23/23
c ---[  12]---> Adder-cost: 69126   maxlim: 389685799   bits: 30/29
c ---[  11]---> Adder-cost: 2804   maxlim: 712518   bits: 20/20
c ---[  10]---> Adder-cost: 11416   maxlim: 36659016   bits: 26/26
c ---[   9]---> Adder-cost: 39511   maxlim: 31990515   bits: 26/25
c ---[   8]---> Adder-cost: 5682   maxlim: 513869   bits: 20/19
c ---[   7]---> Adder-cost: 5867   maxlim: 245639   bits: 19/18
c ---[   6]---> Adder-cost: 6404   maxlim: 282485   bits: 20/19
c ---[   5]---> Adder-cost: 11426   maxlim: 540407   bits: 21/20
c ---[   4]---> Adder-cost: 5814   maxlim: 585536   bits: 20/20
c ---[   3]---> Adder-cost: 4529   maxlim: 200605   bits: 19/18
c ---[   2]---> Adder-cost: 2945   maxlim: 126913   bits: 18/17
c ---[   1]---> Adder-cost: 7696   maxlim: 753405   bits: 21/20
c ---[   0]---> Adder-cost: 5242   maxlim: 276344   bits: 20/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 | 3943555 14068840 | 1183066       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/574577          
c   -- var.elim.:  2000/574577          
c   -- var.elim.:  3000/574577          
c   -- var.elim.:  4000/574577          
c   -- var.elim.:  5000/574577          
c   -- var.elim.:  6000/574577          
c   -- var.elim.:  7000/574577          
c   -- var.elim.:  8000/574577          
c   -- var.elim.:  9000/574577          
c   -- var.elim.:  10000/574577          
c   -- var.elim.:  11000/574577          
c   -- var.elim.:  12000/574577          
c   -- var.elim.:  13000/574577          
c   -- var.elim.:  14000/574577          
c   -- var.elim.:  15000/574577          
c   -- var.elim.:  16000/574577          
c   -- var.elim.:  17000/574577          
c   -- var.elim.:  18000/574577          
c   -- var.elim.:  19000/574577          
c   -- var.elim.:  20000/574577          
c   -- var.elim.:  21000/574577          
c   -- var.elim.:  22000/574577          
c   -- var.elim.:  23000/574577          
c   -- var.elim.:  24000/574577          
c   -- var.elim.:  25000/574577          
c   -- var.elim.:  26000/574577          
c   -- var.elim.:  27000/574577          
c   -- var.elim.:  28000/574577          
c   -- var.elim.:  29000/574577          
c   -- var.elim.:  30000/574577          
c   -- var.elim.:  31000/574577          
c   -- var.elim.:  32000/574577          
c   -- var.elim.:  33000/574577          
c   -- var.elim.:  34000/574577          
c   -- var.elim.:  35000/574577          
c   -- var.elim.:  36000/574577          
c   -- var.elim.:  37000/574577          
c   -- var.elim.:  38000/574577          
c   -- var.elim.:  39000/574577          
c   -- var.elim.:  40000/574577          
c   -- var.elim.:  41000/574577          
c   -- var.elim.:  42000/574577          
c   -- var.elim.:  43000/574577          
c   -- var.elim.:  44000/574577          
c   -- var.elim.:  45000/574577          
c   -- var.elim.:  46000/574577          
c   -- var.elim.:  47000/574577          
c   -- var.elim.:  48000/574577          
c   -- var.elim.:  49000/574577          
c   -- var.elim.:  50000/574577          
c   -- var.elim.:  51000/574577          
c   -- var.elim.:  52000/574577          
c   -- var.elim.:  53000/574577          
c   -- var.elim.:  54000/574577          
c   -- var.elim.:  55000/574577          
c   -- var.elim.:  56000/574577          
c   -- var.elim.:  57000/574577          
c   -- var.elim.:  58000/574577          
c   -- var.elim.:  59000/574577          
c   -- var.elim.:  60000/574577          
c   -- var.elim.:  61000/574577          
c   -- var.elim.:  62000/574577          
c   -- var.elim.:  63000/574577          
c   -- var.elim.:  64000/574577          
c   -- var.elim.:  65000/574577          
c   -- var.elim.:  66000/574577          
c   -- var.elim.:  67000/574577          
c   -- var.elim.:  68000/574577          
c   -- var.elim.:  69000/574577          
c   -- var.elim.:  70000/574577          
c   -- var.elim.:  71000/574577          
c   -- var.elim.:  72000/574577          
c   -- var.elim.:  73000/574577          
c   -- var.elim.:  74000/574577          
c   -- var.elim.:  75000/574577          
c   -- var.elim.:  76000/574577          
c   -- var.elim.:  77000/574577          
c   -- var.elim.:  78000/574577          
c   -- var.elim.:  79000/574577          
c   -- var.elim.:  80000/574577          
c   -- var.elim.:  81000/574577          
c   -- var.elim.:  82000/574577          
c   -- var.elim.:  83000/574577          
c   -- var.elim.:  84000/574577          
c   -- var.elim.:  85000/574577          
c   -- var.elim.:  86000/574577          
c   -- var.elim.:  87000/574577          
c   -- var.elim.:  88000/574577          
c   -- var.elim.:  89000/574577          
c   -- var.elim.:  90000/574577          
c   -- var.elim.:  91000/574577          
c   -- var.elim.:  92000/574577          
c   -- var.elim.:  93000/574577          
c   -- var.elim.:  94000/574577          
c   -- var.elim.:  95000/574577          
c   -- var.elim.:  96000/574577          
c   -- var.elim.:  97000/574577          
c   -- var.elim.:  98000/574577          
c   -- var.elim.:  99000/574577          
c   -- var.elim.:  100000/574577          
c   -- var.elim.:  101000/574577          
c   -- var.elim.:  102000/574577          
c   -- var.elim.:  103000/574577          
c   -- var.elim.:  104000/574577          
c   -- var.elim.:  105000/574577          
c   -- var.elim.:  106000/574577          
c   -- var.elim.:  107000/574577          
c   -- var.elim.:  108000/574577          
c   -- var.elim.:  109000/574577          
c   -- var.elim.:  110000/574577          
c   -- var.elim.:  111000/574577          
c   -- var.elim.:  112000/574577          
c   -- var.elim.:  113000/574577          
c   -- var.elim.:  114000/574577          
c   -- var.elim.:  115000/574577          
c   -- var.elim.:  116000/574577          
c   -- var.elim.:  117000/574577          
c   -- var.elim.:  118000/574577          
c   -- var.elim.:  119000/574577          
c   -- var.elim.:  120000/574577          
c   -- var.elim.:  121000/574577          
c   -- var.elim.:  122000/574577          
c   -- var.elim.:  123000/574577          
c   -- var.elim.:  124000/574577          
c   -- var.elim.:  125000/574577          
c   -- var.elim.:  126000/574577          
c   -- var.elim.:  127000/574577          
c   -- var.elim.:  128000/574577          
c   -- var.elim.:  129000/574577          
c   -- var.elim.:  130000/574577          
c   -- var.elim.:  131000/574577          
c   -- var.elim.:  132000/574577          
c   -- var.elim.:  133000/574577          
c   -- var.elim.:  134000/574577          
c   -- var.elim.:  135000/574577          
c   -- var.elim.:  136000/574577          
c   -- var.elim.:  137000/574577          
c   -- var.elim.:  138000/574577          
c   -- var.elim.:  139000/574577          
c   -- var.elim.:  140000/574577          
c   -- var.elim.:  141000/574577          
c   -- var.elim.:  142000/574577          
c   -- var.elim.:  143000/574577          
c   -- var.elim.:  144000/574577          
c   -- var.elim.:  145000/574577          
c   -- var.elim.:  146000/574577          
c   -- var.elim.:  147000/574577          
c   -- var.elim.:  148000/574577          
c   -- var.elim.:  149000/574577          
c   -- var.elim.:  150000/574577          
c   -- var.elim.:  151000/574577          
c   -- var.elim.:  152000/574577          
c   -- var.elim.:  153000/574577          
c   -- var.elim.:  154000/574577          
c   -- var.elim.:  155000/574577          
c   -- var.elim.:  156000/574577          
c   -- var.elim.:  157000/574577          
c   -- var.elim.:  158000/574577          
c   -- var.elim.:  159000/574577          
c   -- var.elim.:  160000/574577          
c   -- var.elim.:  161000/574577          
c   -- var.elim.:  162000/574577          
c   -- var.elim.:  163000/574577          
c   -- var.elim.:  164000/574577          
c   -- var.elim.:  165000/574577          
c   -- var.elim.:  166000/574577          
c   -- var.elim.:  167000/574577          
c   -- var.elim.:  168000/574577          
c   -- var.elim.:  169000/574577          
c   -- var.elim.:  170000/574577          
c   -- var.elim.:  171000/574577          
c   -- var.elim.:  172000/574577          
c   -- var.elim.:  173000/574577          
c   -- var.elim.:  174000/574577          
c   -- var.elim.:  175000/574577          
c   -- var.elim.:  176000/574577          
c   -- var.elim.:  177000/574577          
c   -- var.elim.:  178000/574577          
c   -- var.elim.:  179000/574577          
c   -- var.elim.:  180000/574577          
c   -- var.elim.:  181000/574577          
c   -- var.elim.:  182000/574577          
c   -- var.elim.:  183000/574577          
c   -- var.elim.:  184000/574577          
c   -- var.elim.:  185000/574577          
c   -- var.elim.:  186000/574577          
c   -- var.elim.:  187000/574577          
c   -- var.elim.:  188000/574577          
c   -- var.elim.:  189000/574577          
c   -- var.elim.:  190000/574577          
c   -- var.elim.:  191000/574577          
c   -- var.elim.:  192000/574577          
c   -- var.elim.:  193000/574577          
c   -- var.elim.:  194000/574577          
c   -- var.elim.:  195000/574577          
c   -- var.elim.:  196000/574577          
c   -- var.elim.:  197000/574577          
c   -- var.elim.:  198000/574577          
c   -- var.elim.:  199000/574577          
c   -- var.elim.:  200000/574577          
c   -- var.elim.:  201000/574577          
c   -- var.elim.:  202000/574577          
c   -- var.elim.:  203000/574577          
c   -- var.elim.:  204000/574577          
c   -- var.elim.:  205000/574577          
c   -- var.elim.:  206000/574577          
c   -- var.elim.:  207000/574577          
c   -- var.elim.:  208000/574577          
c   -- var.elim.:  209000/574577          
c   -- var.elim.:  210000/574577          
c   -- var.elim.:  211000/574577          
c   -- var.elim.:  212000/574577          
c   -- var.elim.:  213000/574577          
c   -- var.elim.:  214000/574577          
c   -- var.elim.:  215000/574577          
c   -- var.elim.:  216000/574577          
c   -- var.elim.:  217000/574577          
c   -- var.elim.:  218000/574577          
c   -- var.elim.:  219000/574577          
c   -- var.elim.:  220000/574577          
c   -- var.elim.:  221000/574577          
c   -- var.elim.:  222000/574577          
c   -- var.elim.:  223000/574577          
c   -- var.elim.:  224000/574577          
c   -- var.elim.:  225000/574577          
c   -- var.elim.:  226000/574577          
c   -- var.elim.:  227000/574577          
c   -- var.elim.:  228000/574577          
c   -- var.elim.:  229000/574577          
c   -- var.elim.:  230000/574577          
c   -- var.elim.:  231000/574577          
c   -- var.elim.:  232000/574577          
c   -- var.elim.:  233000/574577          
c   -- var.elim.:  234000/574577          
c   -- var.elim.:  235000/574577          
c   -- var.elim.:  236000/574577          
c   -- var.elim.:  237000/574577          
c   -- var.elim.:  238000/574577          
c   -- var.elim.:  239000/574577          
c   -- var.elim.:  240000/574577          
c   -- var.elim.:  241000/574577          
c   -- var.elim.:  242000/574577          
c   -- var.elim.:  243000/574577          
c   -- var.elim.:  244000/574577          
c   -- var.elim.:  245000/574577          
c   -- var.elim.:  246000/574577          
c   -- var.elim.:  247000/574577          
c   -- var.elim.:  248000/574577          
c   -- var.elim.:  249000/574577          
c   -- var.elim.:  250000/574577          
c   -- var.elim.:  251000/574577          
c   -- var.elim.:  252000/574577          
c   -- var.elim.:  253000/574577          
c   -- var.elim.:  254000/574577          
c   -- var.elim.:  255000/574577          
c   -- var.elim.:  256000/574577          
c   -- var.elim.:  257000/574577          
c   -- var.elim.:  258000/574577          
c   -- var.elim.:  259000/574577          
c   -- var.elim.:  260000/574577          
c   -- var.elim.:  261000/574577          
c   -- var.elim.:  262000/574577          
c   -- var.elim.:  263000/574577          
c   -- var.elim.:  264000/574577          
c   -- var.elim.:  265000/574577          
c   -- var.elim.:  266000/574577          
c   -- var.elim.:  267000/574577          
c   -- var.elim.:  268000/574577          
c   -- var.elim.:  269000/574577          
c   -- var.elim.:  270000/574577          
c   -- var.elim.:  271000/574577          
c   -- var.elim.:  272000/574577          
c   -- var.elim.:  273000/574577          
c   -- var.elim.:  274000/574577          
c   -- var.elim.:  275000/574577          
c   -- var.elim.:  276000/574577          
c   -- var.elim.:  277000/574577          
c   -- var.elim.:  278000/574577          
c   -- var.elim.:  279000/574577          
c   -- var.elim.:  280000/574577          
c   -- var.elim.:  281000/574577          
c   -- var.elim.:  282000/574577          
c   -- var.elim.:  283000/574577          
c   -- var.elim.:  284000/574577          
c   -- var.elim.:  285000/574577          
c   -- var.elim.:  286000/574577          
c   -- var.elim.:  287000/574577          
c   -- var.elim.:  288000/574577          
c   -- var.elim.:  289000/574577          
c   -- var.elim.:  290000/574577          
c   -- var.elim.:  291000/574577          
c   -- var.elim.:  292000/574577          
c   -- var.elim.:  293000/574577          
c   -- var.elim.:  294000/574577          
c   -- var.elim.:  295000/574577          
c   -- var.elim.:  296000/574577          
c   -- var.elim.:  297000/574577          
c   -- var.elim.:  298000/574577          
c   -- var.elim.:  299000/574577          
c   -- var.elim.:  300000/574577          
c   -- var.elim.:  301000/574577          
c   -- var.elim.:  302000/574577          
c   -- var.elim.:  303000/574577          
c   -- var.elim.:  304000/574577          
c   -- var.elim.:  305000/574577          
c   -- var.elim.:  306000/574577          
c   -- var.elim.:  307000/574577          
c   -- var.elim.:  308000/574577          
c   -- var.elim.:  309000/574577          
c   -- var.elim.:  310000/574577          
c   -- var.elim.:  311000/574577          
c   -- var.elim.:  312000/574577          
c   -- var.elim.:  313000/574577          
c   -- var.elim.:  314000/574577          
c   -- var.elim.:  315000/574577          
c   -- var.elim.:  316000/574577          
c   -- var.elim.:  317000/574577          
c   -- var.elim.:  318000/574577          
c   -- var.elim.:  319000/574577          
c   -- var.elim.:  320000/574577          
c   -- var.elim.:  321000/574577          
c   -- var.elim.:  322000/574577          
c   -- var.elim.:  323000/574577          
c   -- var.elim.:  324000/574577          
c   -- var.elim.:  325000/574577          
c   -- var.elim.:  326000/574577          
c   -- var.elim.:  327000/574577          
c   -- var.elim.:  328000/574577          
c   -- var.elim.:  329000/574577          
c   -- var.elim.:  330000/574577          
c   -- var.elim.:  331000/574577          
c   -- var.elim.:  332000/574577          
c   -- var.elim.:  333000/574577          
c   -- var.elim.:  334000/574577          
c   -- var.elim.:  335000/574577          
c   -- var.elim.:  336000/574577          
c   -- var.elim.:  337000/574577          
c   -- var.elim.:  338000/574577          
c   -- var.elim.:  339000/574577          
c   -- var.elim.:  340000/574577          
c   -- var.elim.:  341000/574577          
c   -- var.elim.:  342000/574577          
c   -- var.elim.:  343000/574577          
c   -- var.elim.:  344000/574577          
c   -- var.elim.:  345000/574577          
c   -- var.elim.:  346000/574577          
c   -- var.elim.:  347000/574577          
c   -- var.elim.:  348000/574577          
c   -- var.elim.:  349000/574577          
c   -- var.elim.:  350000/574577          
c   -- var.elim.:  351000/574577          
c   -- var.elim.:  352000/574577          
c   -- var.elim.:  353000/574577          
c   -- var.elim.:  354000/574577          
c   -- var.elim.:  355000/574577          
c   -- var.elim.:  356000/574577          
c   -- var.elim.:  357000/574577          
c   -- var.elim.:  358000/574577          
c   -- var.elim.:  359000/574577          
c   -- var.elim.:  360000/574577          
c   -- var.elim.:  361000/574577          
c   -- var.elim.:  362000/574577          
c   -- var.elim.:  363000/574577          
c   -- var.elim.:  364000/574577          
c   -- var.elim.:  365000/574577          
c   -- var.elim.:  366000/574577          
c   -- var.elim.:  367000/574577          
c   -- var.elim.:  368000/574577          
c   -- var.elim.:  369000/574577          
c   -- var.elim.:  370000/574577          
c   -- var.elim.:  371000/574577          
c   -- var.elim.:  372000/574577          
c   -- var.elim.:  373000/574577          
c   -- var.elim.:  374000/574577          
c   -- var.elim.:  375000/574577          
c   -- var.elim.:  376000/574577          
c   -- var.elim.:  377000/574577          
c   -- var.elim.:  378000/574577          
c   -- var.elim.:  379000/574577          
c   -- var.elim.:  380000/574577          
c   -- var.elim.:  381000/574577          
c   -- var.elim.:  382000/574577          
c   -- var.elim.:  383000/574577          
c   -- var.elim.:  384000/574577          
c   -- var.elim.:  385000/574577          
c   -- var.elim.:  386000/574577          
c   -- var.elim.:  387000/574577          
c   -- var.elim.:  388000/574577          
c   -- var.elim.:  389000/574577          
c   -- var.elim.:  390000/574577          
c   -- var.elim.:  391000/574577          
c   -- var.elim.:  392000/574577          
c   -- var.elim.:  393000/574577          
c   -- var.elim.:  394000/574577          
c   -- var.elim.:  395000/574577          
c   -- var.elim.:  396000/574577          
c   -- var.elim.:  397000/574577          
c   -- var.elim.:  398000/574577          
c   -- var.elim.:  399000/574577          
c   -- var.elim.:  400000/574577          
c   -- var.elim.:  401000/574577          
c   -- var.elim.:  402000/574577          
c   -- var.elim.:  403000/574577          
c   -- var.elim.:  404000/574577          
c   -- var.elim.:  405000/574577          
c   -- var.elim.:  406000/574577          
c   -- var.elim.:  407000/574577          
c   -- var.elim.:  408000/574577          
c   -- var.elim.:  409000/574577          
c   -- var.elim.:  410000/574577          
c   -- var.elim.:  411000/574577          
c   -- var.elim.:  412000/574577          
c   -- var.elim.:  413000/574577          
c   -- var.elim.:  414000/574577          
c   -- var.elim.:  415000/574577          
c   -- var.elim.:  416000/574577          
c   -- var.elim.:  417000/574577          
c   -- var.elim.:  418000/574577          
c   -- var.elim.:  419000/574577          
c   -- var.elim.:  420000/574577          
c   -- var.elim.:  421000/574577          
c   -- var.elim.:  422000/574577          
c   -- var.elim.:  423000/574577          
c   -- var.elim.:  424000/574577          
c   -- var.elim.:  425000/574577          
c   -- var.elim.:  426000/574577          
c   -- var.elim.:  427000/574577          
c   -- var.elim.:  428000/574577          
c   -- var.elim.:  429000/574577          
c   -- var.elim.:  430000/574577          
c   -- var.elim.:  431000/574577          
c   -- var.elim.:  432000/574577          
c   -- var.elim.:  433000/574577          
c   -- var.elim.:  434000/574577          
c   -- var.elim.:  435000/574577          
c   -- var.elim.:  436000/574577          
c   -- var.elim.:  437000/574577          
c   -- var.elim.:  438000/574577          
c   -- var.elim.:  439000/574577          
c   -- var.elim.:  440000/574577          
c   -- var.elim.:  441000/574577          
c   -- var.elim.:  442000/574577          
c   -- var.elim.:  443000/574577          
c   -- var.elim.:  444000/574577          
c   -- var.elim.:  445000/574577          
c   -- var.elim.:  446000/574577          
c   -- var.elim.:  447000/574577          
c   -- var.elim.:  448000/574577          
c   -- var.elim.:  449000/574577          
c   -- var.elim.:  450000/574577          
c   -- var.elim.:  451000/574577          
c   -- var.elim.:  452000/574577          
c   -- var.elim.:  453000/574577          
c   -- var.elim.:  454000/574577          
c   -- var.elim.:  455000/574577          
c   -- var.elim.:  456000/574577          
c   -- var.elim.:  457000/574577          
c   -- var.elim.:  458000/574577          
c   -- var.elim.:  459000/574577          
c   -- var.elim.:  460000/574577          
c   -- var.elim.:  461000/574577          
c   -- var.elim.:  462000/574577          
c   -- var.elim.:  463000/574577          
c   -- var.elim.:  464000/574577          
c   -- var.elim.:  465000/574577          
c   -- var.elim.:  466000/574577          
c   -- var.elim.:  467000/574577          
c   -- var.elim.:  468000/574577          
c   -- var.elim.:  469000/574577          
c   -- var.elim.:  470000/574577          
c   -- var.elim.:  471000/574577          
c   -- var.elim.:  472000/574577          
c   -- var.elim.:  473000/574577          
c   -- var.elim.:  474000/574577          
c   -- var.elim.:  475000/574577          
c   -- var.elim.:  476000/574577          
c   -- var.elim.:  477000/574577          
c   -- var.elim.:  478000/574577          
c   -- var.elim.:  479000/574577          
c   -- var.elim.:  480000/574577          
c   -- var.elim.:  481000/574577          
c   -- var.elim.:  482000/574577          
c   -- var.elim.:  483000/574577          
c   -- var.elim.:  484000/574577          
c   -- var.elim.:  485000/574577          
c   -- var.elim.:  486000/574577          
c   -- var.elim.:  487000/574577          
c   -- var.elim.:  488000/574577          
c   -- var.elim.:  489000/574577          
c   -- var.elim.:  490000/574577          
c   -- var.elim.:  491000/574577          
c   -- var.elim.:  492000/574577          
c   -- var.elim.:  493000/574577          
c   -- var.elim.:  494000/574577          
c   -- var.elim.:  495000/574577          
c   -- var.elim.:  496000/574577          
c   -- var.elim.:  497000/574577          
c   -- var.elim.:  498000/574577          
c   -- var.elim.:  499000/574577          
c   -- var.elim.:  500000/574577          
c   -- var.elim.:  501000/574577          
c   -- var.elim.:  502000/574577          
c   -- var.elim.:  503000/574577          
c   -- var.elim.:  504000/574577          
c   -- var.elim.:  505000/574577          
c   -- var.elim.:  506000/574577          
c   -- var.elim.:  507000/574577          
c   -- var.elim.:  508000/574577          
c   -- var.elim.:  509000/574577          
c   -- var.elim.:  510000/574577          
c   -- var.elim.:  511000/574577          
c   -- var.elim.:  512000/574577          
c   -- var.elim.:  513000/574577          
c   -- var.elim.:  514000/574577          
c   -- var.elim.:  515000/574577          
c   -- var.elim.:  516000/574577          
c   -- var.elim.:  517000/574577          
c   -- var.elim.:  518000/574577          
c   -- var.elim.:  519000/574577          
c   -- var.elim.:  520000/574577          
c   -- var.elim.:  521000/574577          
c   -- var.elim.:  522000/574577          
c   -- var.elim.:  523000/574577          
c   -- var.elim.:  524000/574577          
c   -- var.elim.:  525000/574577          
c   -- var.elim.:  526000/574577          
c   -- var.elim.:  527000/574577          
c   -- var.elim.:  528000/574577          
c   -- var.elim.:  529000/574577          
c   -- var.elim.:  530000/574577          
c   -- var.elim.:  531000/574577          
c   -- var.elim.:  532000/574577          
c   -- var.elim.:  533000/574577          
c   -- var.elim.:  534000/574577          
c   -- var.elim.:  535000/574577          
c   -- var.elim.:  536000/574577          
c   -- var.elim.:  537000/574577          
c   -- var.elim.:  538000/574577          
c   -- var.elim.:  539000/574577          
c   -- var.elim.:  540000/574577          
c   -- var.elim.:  541000/574577          
c   -- var.elim.:  542000/574577          
c   -- var.elim.:  543000/574577          
c   -- var.elim.:  544000/574577          
c   -- var.elim.:  545000/574577          
c   -- var.elim.:  546000/574577          
c   -- var.elim.:#### 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.92 0.97 0.99 2/54 25310
Raw data (stat): 25310 (runsolver) R 25309 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544306884 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+10.0005 s]
Raw data (loadavg): 0.93 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 11962 0 0 0 967 31 0 0 25 0 1 0 544306884 44503040 8348 4294967295 134512640 134672761 3221224544 3221221852 1075346629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10865 8348 603 41 0 10824 0
vsize: 43460
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 13593 0 0 0 1963 35 0 0 25 0 1 0 544306884 44515328 8400 4294967295 134512640 134672761 3221224544 3221222496 134522368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 8400 603 41 0 10827 0
vsize: 43472
[startup+30.001 s]
Raw data (loadavg): 0.95 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 13593 0 0 0 2963 35 0 0 25 0 1 0 544306884 44515328 8400 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 8400 603 41 0 10827 0
vsize: 43472
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 13593 0 0 0 3963 35 0 0 25 0 1 0 544306884 44515328 8400 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 8400 603 41 0 10827 0
vsize: 43472
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 21279 0 0 0 4947 52 0 0 25 0 1 0 544306884 73351168 13889 4294967295 134512640 134672761 3221224544 3221222960 134597008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17908 13889 603 41 0 17867 0
vsize: 71632
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 22106 0 0 0 5945 54 0 0 25 0 1 0 544306884 73691136 13972 4294967295 134512640 134672761 3221224544 3220302832 134522987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17991 13972 603 41 0 17950 0
vsize: 71964
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 22618 0 0 0 6944 55 0 0 25 0 1 0 544306884 73351168 13889 4294967295 134512640 134672761 3221224544 3221222960 134597218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17908 13889 603 41 0 17867 0
vsize: 71632
[startup+80.004 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 24518 0 0 0 7940 59 0 0 25 0 1 0 544306884 76304384 15044 4294967295 134512640 134672761 3221224544 3221221984 134522981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18629 15044 603 41 0 18588 0
vsize: 74516
[startup+90.0047 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 57880 0 0 0 8864 135 0 0 25 0 1 0 544306884 226594816 47888 4294967295 134512640 134672761 3221224544 3221219496 134543045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55321 47889 603 41 0 55280 0
vsize: 221284
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 101655 0 0 0 9755 243 0 0 25 0 1 0 544306884 413556736 91663 4294967295 134512640 134672761 3221224544 3221214968 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100966 91663 603 41 0 100925 0
vsize: 403864
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 133205 0 0 0 10678 321 0 0 25 0 1 0 544306884 570925056 123209 4294967295 134512640 134672761 3221224544 3221223088 134621051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139386 123209 603 41 0 139345 0
vsize: 557544
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 133205 0 0 0 11678 321 0 0 25 0 1 0 544306884 570925056 123209 4294967295 134512640 134672761 3221224544 3221223088 134621328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139386 123209 603 41 0 139345 0
vsize: 557544
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 133205 0 0 0 12678 321 0 0 25 0 1 0 544306884 570925056 123209 4294967295 134512640 134672761 3221224544 3221223096 1075347118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139386 123209 603 41 0 139345 0
vsize: 557544
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 137057 0 0 0 13669 331 0 0 25 0 1 0 544306884 592908288 127061 4294967295 134512640 134672761 3221224544 3221223136 134621199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144753 127061 603 41 0 144712 0
vsize: 579012
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 147629 0 0 0 14640 360 0 0 25 0 1 0 544306884 572211200 123541 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139700 123541 603 41 0 139659 0
vsize: 558800
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 148067 0 0 0 15640 360 0 0 25 0 1 0 544306884 574128128 123979 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140168 123979 603 41 0 140127 0
vsize: 560672
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 148459 0 0 0 16638 362 0 0 25 0 1 0 544306884 575614976 124371 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140531 124371 603 41 0 140490 0
vsize: 562124
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 148859 0 0 0 17638 363 0 0 25 0 1 0 544306884 577396736 124771 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140966 124771 603 41 0 140925 0
vsize: 563864
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 149205 0 0 0 18637 364 0 0 25 0 1 0 544306884 578768896 125117 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141301 125117 603 41 0 141260 0
vsize: 565204
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 149518 0 0 0 19637 364 0 0 25 0 1 0 544306884 580120576 125430 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141631 125430 603 41 0 141590 0
vsize: 566524
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 149769 0 0 0 20636 365 0 0 25 0 1 0 544306884 581066752 125681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141862 125681 603 41 0 141821 0
vsize: 567448
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 149963 0 0 0 21635 366 0 0 25 0 1 0 544306884 581877760 125875 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142060 125875 603 41 0 142019 0
vsize: 568240
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 150168 0 0 0 22635 367 0 0 25 0 1 0 544306884 582688768 126080 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142258 126080 603 41 0 142217 0
vsize: 569032
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 150325 0 0 0 23634 367 0 0 25 0 1 0 544306884 583364608 126237 4294967295 134512640 134672761 3221224544 3221223680 134614800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142423 126237 603 41 0 142382 0
vsize: 569692
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 150461 0 0 0 24634 367 0 0 25 0 1 0 544306884 583905280 126373 4294967295 134512640 134672761 3221224544 3221223680 134614677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142555 126373 603 41 0 142514 0
vsize: 570220
[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 150743 0 0 0 25634 369 0 0 25 0 1 0 544306884 584966144 126655 4294967295 134512640 134672761 3221224544 3221223584 134612739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142814 126655 603 41 0 142773 0
vsize: 571256
[startup+270.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 151121 0 0 0 26633 370 0 0 25 0 1 0 544306884 586698752 127033 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143237 127033 603 41 0 143196 0
vsize: 572948
[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 151265 0 0 0 27633 370 0 0 25 0 1 0 544306884 587366400 127177 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143400 127177 603 41 0 143359 0
vsize: 573600
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 151381 0 0 0 28633 370 0 0 25 0 1 0 544306884 587911168 127293 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143533 127293 603 41 0 143492 0
vsize: 574132
[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 151466 0 0 0 29633 371 0 0 25 0 1 0 544306884 588181504 127378 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143599 127378 603 41 0 143558 0
vsize: 574396
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 151556 0 0 0 30633 371 0 0 25 0 1 0 544306884 588587008 127468 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143698 127468 603 41 0 143657 0
vsize: 574792
[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 151658 0 0 0 31633 371 0 0 25 0 1 0 544306884 588992512 127570 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143797 127570 603 41 0 143756 0
vsize: 575188
[startup+330.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 151772 0 0 0 32634 372 0 0 25 0 1 0 544306884 589398016 127684 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143896 127684 603 41 0 143855 0
vsize: 575584
[startup+340.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 151848 0 0 0 33634 372 0 0 25 0 1 0 544306884 589668352 127760 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143962 127760 603 41 0 143921 0
vsize: 575848
[startup+350.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 152228 0 0 0 34634 373 0 0 25 0 1 0 544306884 591269888 128140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144353 128140 603 41 0 144312 0
vsize: 577412
[startup+360.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 152376 0 0 0 35634 374 0 0 25 0 1 0 544306884 591806464 128288 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144484 128288 603 41 0 144443 0
vsize: 577936
[startup+370.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 152483 0 0 0 36634 374 0 0 25 0 1 0 544306884 592207872 128395 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144582 128395 603 41 0 144541 0
vsize: 578328
[startup+380.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 152651 0 0 0 37633 374 0 0 25 0 1 0 544306884 592875520 128563 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144745 128563 603 41 0 144704 0
vsize: 578980
[startup+390.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 152709 0 0 0 38634 374 0 0 25 0 1 0 544306884 593145856 128621 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144811 128621 603 41 0 144770 0
vsize: 579244
[startup+400.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 152772 0 0 0 39634 375 0 0 25 0 1 0 544306884 593416192 128684 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144877 128684 603 41 0 144836 0
vsize: 579508
[startup+410.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 152833 0 0 0 40635 375 0 0 25 0 1 0 544306884 593551360 128745 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144910 128745 603 41 0 144869 0
vsize: 579640
[startup+420.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 152893 0 0 0 41635 375 0 0 25 0 1 0 544306884 593821696 128805 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144976 128805 603 41 0 144935 0
vsize: 579904
[startup+430.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 152939 0 0 0 42635 375 0 0 25 0 1 0 544306884 593956864 128851 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145009 128851 603 41 0 144968 0
vsize: 580036
[startup+440.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 152988 0 0 0 43635 376 0 0 25 0 1 0 544306884 594227200 128900 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145075 128900 603 41 0 145034 0
vsize: 580300
[startup+450.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153038 0 0 0 44635 376 0 0 25 0 1 0 544306884 594362368 128950 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145108 128950 603 41 0 145067 0
vsize: 580432
[startup+460.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153087 0 0 0 45635 376 0 0 25 0 1 0 544306884 594632704 128999 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145174 128999 603 41 0 145133 0
vsize: 580696
[startup+470.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153127 0 0 0 46635 376 0 0 25 0 1 0 544306884 595292160 129039 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145335 129039 603 41 0 145294 0
vsize: 581340
[startup+480.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153161 0 0 0 47635 376 0 0 25 0 1 0 544306884 595427328 129073 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145368 129073 603 41 0 145327 0
vsize: 581472
[startup+490.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153202 0 0 0 48635 376 0 0 25 0 1 0 544306884 595689472 129114 4294967295 134512640 134672761 3221224544 3221223668 134566142 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145432 129114 603 41 0 145391 0
vsize: 581728
[startup+500.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153233 0 0 0 49635 376 0 0 25 0 1 0 544306884 595824640 129145 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145465 129145 603 41 0 145424 0
vsize: 581860
[startup+510.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153267 0 0 0 50635 376 0 0 25 0 1 0 544306884 595955712 129179 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145497 129179 603 41 0 145456 0
vsize: 581988
[startup+520.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153297 0 0 0 51636 376 0 0 25 0 1 0 544306884 595955712 129209 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145497 129209 603 41 0 145456 0
vsize: 581988
[startup+530.073 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153326 0 0 0 52636 377 0 0 25 0 1 0 544306884 596090880 129238 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145530 129238 603 41 0 145489 0
vsize: 582120
[startup+540.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153354 0 0 0 53636 377 0 0 25 0 1 0 544306884 596226048 129266 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145563 129266 603 41 0 145522 0
vsize: 582252
[startup+550.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153385 0 0 0 54636 377 0 0 25 0 1 0 544306884 596361216 129297 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145596 129297 603 41 0 145555 0
vsize: 582384
[startup+560.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153414 0 0 0 55636 377 0 0 25 0 1 0 544306884 596496384 129326 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145629 129326 603 41 0 145588 0
vsize: 582516
[startup+570.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153446 0 0 0 56636 377 0 0 25 0 1 0 544306884 596631552 129358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145662 129358 603 41 0 145621 0
vsize: 582648
[startup+580.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153479 0 0 0 57636 377 0 0 25 0 1 0 544306884 596766720 129391 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145695 129391 603 41 0 145654 0
vsize: 582780
[startup+590.076 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153510 0 0 0 58636 377 0 0 25 0 1 0 544306884 596901888 129422 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145728 129422 603 41 0 145687 0
vsize: 582912
[startup+600.076 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153540 0 0 0 59636 378 0 0 25 0 1 0 544306884 596901888 129452 4294967295 134512640 134672761 3221224544 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145728 129452 603 41 0 145687 0
vsize: 582912
[startup+610.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153568 0 0 0 60636 378 0 0 25 0 1 0 544306884 597037056 129480 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145761 129480 603 41 0 145720 0
vsize: 583044
[startup+620.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153593 0 0 0 61636 378 0 0 25 0 1 0 544306884 597172224 129505 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145794 129505 603 41 0 145753 0
vsize: 583176
[startup+630.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153618 0 0 0 62636 378 0 0 25 0 1 0 544306884 597307392 129530 4294967295 134512640 134672761 3221224544 3221223712 134564636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145827 129530 603 41 0 145786 0
vsize: 583308
[startup+640.078 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153650 0 0 0 63637 378 0 0 25 0 1 0 544306884 597442560 129562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145860 129562 603 41 0 145819 0
vsize: 583440
[startup+650.079 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153684 0 0 0 64637 378 0 0 25 0 1 0 544306884 597577728 129596 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145893 129596 603 41 0 145852 0
vsize: 583572
[startup+660.079 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153717 0 0 0 65637 378 0 0 25 0 1 0 544306884 597712896 129629 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145926 129629 603 41 0 145885 0
vsize: 583704
[startup+670.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153757 0 0 0 66637 378 0 0 25 0 1 0 544306884 597848064 129669 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145959 129669 603 41 0 145918 0
vsize: 583836
[startup+680.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153796 0 0 0 67637 378 0 0 25 0 1 0 544306884 597983232 129708 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145992 129708 603 41 0 145951 0
vsize: 583968
[startup+690.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153833 0 0 0 68637 379 0 0 25 0 1 0 544306884 598118400 129745 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146025 129745 603 41 0 145984 0
vsize: 584100
[startup+700.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153881 0 0 0 69637 379 0 0 25 0 1 0 544306884 598253568 129793 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146058 129793 603 41 0 146017 0
vsize: 584232
[startup+710.082 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153919 0 0 0 70637 379 0 0 25 0 1 0 544306884 598388736 129831 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146091 129831 603 41 0 146050 0
vsize: 584364
[startup+720.083 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153955 0 0 0 71637 379 0 0 25 0 1 0 544306884 598659072 129867 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146157 129867 603 41 0 146116 0
vsize: 584628
[startup+730.083 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 153983 0 0 0 72637 379 0 0 25 0 1 0 544306884 598659072 129895 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146157 129895 603 41 0 146116 0
vsize: 584628
[startup+740.084 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154013 0 0 0 73638 379 0 0 25 0 1 0 544306884 598794240 129925 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146190 129925 603 41 0 146149 0
vsize: 584760
[startup+750.083 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154044 0 0 0 74637 379 0 0 25 0 1 0 544306884 598929408 129956 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146223 129956 603 41 0 146182 0
vsize: 584892
[startup+760.084 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154082 0 0 0 75637 380 0 0 25 0 1 0 544306884 599064576 129994 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146256 129994 603 41 0 146215 0
vsize: 585024
[startup+770.087 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154110 0 0 0 76638 380 0 0 25 0 1 0 544306884 599199744 130022 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146289 130022 603 41 0 146248 0
vsize: 585156
[startup+780.089 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154137 0 0 0 77638 380 0 0 25 0 1 0 544306884 599334912 130049 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146322 130049 603 41 0 146281 0
vsize: 585288
[startup+790.091 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154172 0 0 0 78638 380 0 0 25 0 1 0 544306884 599470080 130084 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146355 130084 603 41 0 146314 0
vsize: 585420
[startup+800.091 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154202 0 0 0 79638 380 0 0 25 0 1 0 544306884 599605248 130114 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146388 130114 603 41 0 146347 0
vsize: 585552
[startup+810.091 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154230 0 0 0 80638 381 0 0 25 0 1 0 544306884 599740416 130142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146421 130142 603 41 0 146380 0
vsize: 585684
[startup+820.092 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154255 0 0 0 81638 381 0 0 25 0 1 0 544306884 599740416 130167 4294967295 134512640 134672761 3221224544 3221223712 134564725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146421 130167 603 41 0 146380 0
vsize: 585684
[startup+830.093 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154284 0 0 0 82638 381 0 0 25 0 1 0 544306884 599875584 130196 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146454 130196 603 41 0 146413 0
vsize: 585816
[startup+840.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154319 0 0 0 83640 381 0 0 25 0 1 0 544306884 600010752 130231 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146487 130231 603 41 0 146446 0
vsize: 585948
[startup+850.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154341 0 0 0 84640 381 0 0 25 0 1 0 544306884 600145920 130253 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146520 130253 603 41 0 146479 0
vsize: 586080
[startup+860.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154366 0 0 0 85640 382 0 0 25 0 1 0 544306884 600145920 130278 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146520 130278 603 41 0 146479 0
vsize: 586080
[startup+870.111 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154393 0 0 0 86640 382 0 0 25 0 1 0 544306884 600281088 130305 4294967295 134512640 134672761 3221224544 3221223728 134615554 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146553 130305 603 41 0 146512 0
vsize: 586212
[startup+880.112 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154418 0 0 0 87640 382 0 0 25 0 1 0 544306884 600416256 130330 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146586 130330 603 41 0 146545 0
vsize: 586344
[startup+890.113 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154453 0 0 0 88640 382 0 0 25 0 1 0 544306884 600416256 130365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146586 130365 603 41 0 146545 0
vsize: 586344
[startup+900.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154478 0 0 0 89640 382 0 0 25 0 1 0 544306884 600551424 130390 4294967295 134512640 134672761 3221224544 3221223728 134615845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146619 130390 603 41 0 146578 0
vsize: 586476
[startup+910.114 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154499 0 0 0 90641 382 0 0 25 0 1 0 544306884 600686592 130411 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146652 130411 603 41 0 146611 0
vsize: 586608
[startup+920.115 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154533 0 0 0 91640 382 0 0 25 0 1 0 544306884 600821760 130445 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146685 130445 603 41 0 146644 0
vsize: 586740
[startup+930.115 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154561 0 0 0 92641 382 0 0 25 0 1 0 544306884 600821760 130473 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146685 130473 603 41 0 146644 0
vsize: 586740
[startup+940.115 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154587 0 0 0 93641 382 0 0 25 0 1 0 544306884 600956928 130499 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146718 130499 603 41 0 146677 0
vsize: 586872
[startup+950.117 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154612 0 0 0 94641 382 0 0 25 0 1 0 544306884 601092096 130524 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146751 130524 603 41 0 146710 0
vsize: 587004
[startup+960.116 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 154635 0 0 0 95641 383 0 0 25 0 1 0 544306884 601092096 130547 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146751 130547 603 41 0 146710 0
vsize: 587004
[startup+970.117 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 155200 0 0 0 96639 384 0 0 25 0 1 0 544306884 603475968 131112 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147333 131112 603 41 0 147292 0
vsize: 589332
[startup+980.117 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 155713 0 0 0 97638 386 0 0 25 0 1 0 544306884 605466624 131625 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147819 131625 603 41 0 147778 0
vsize: 591276
[startup+990.118 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 155765 0 0 0 98638 386 0 0 25 0 1 0 544306884 605736960 131677 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147885 131677 603 41 0 147844 0
vsize: 591540
[startup+1000.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 156137 0 0 0 99637 387 0 0 25 0 1 0 544306884 607195136 132049 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148241 132049 603 41 0 148200 0
vsize: 592964
[startup+1010.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 156553 0 0 0 100636 388 0 0 25 0 1 0 544306884 609452032 132465 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148792 132465 603 41 0 148751 0
vsize: 595168
[startup+1020.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 157202 0 0 0 101635 390 0 0 25 0 1 0 544306884 612093952 133114 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 149437 133114 603 41 0 149396 0
vsize: 597748
[startup+1030.12 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 157926 0 0 0 102633 392 0 0 25 0 1 0 544306884 614998016 133838 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150146 133838 603 41 0 150105 0
vsize: 600584
[startup+1040.13 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 158576 0 0 0 103632 394 0 0 25 0 1 0 544306884 617648128 134488 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150793 134488 603 41 0 150752 0
vsize: 603172
[startup+1050.13 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 159251 0 0 0 104631 396 0 0 25 0 1 0 544306884 620429312 135163 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151472 135163 603 41 0 151431 0
vsize: 605888
[startup+1060.13 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 159763 0 0 0 105630 397 0 0 25 0 1 0 544306884 622551040 135675 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151990 135675 603 41 0 151949 0
vsize: 607960
[startup+1070.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 160234 0 0 0 106630 398 0 0 25 0 1 0 544306884 624402432 136146 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152442 136146 603 41 0 152401 0
vsize: 609768
[startup+1080.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 160742 0 0 0 107629 399 0 0 25 0 1 0 544306884 626528256 136654 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152961 136654 603 41 0 152920 0
vsize: 611844
[startup+1090.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 161167 0 0 0 108628 400 0 0 25 0 1 0 544306884 628248576 137079 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153381 137079 603 41 0 153340 0
vsize: 613524
[startup+1100.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 161536 0 0 0 109628 401 0 0 25 0 1 0 544306884 629841920 137448 4294967295 134512640 134672761 3221224544 3221223588 1075755419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153770 137448 603 41 0 153729 0
vsize: 615080
[startup+1110.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 161951 0 0 0 110626 402 0 0 25 0 1 0 544306884 631435264 137863 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154159 137863 603 41 0 154118 0
vsize: 616636
[startup+1120.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 162383 0 0 0 111625 404 0 0 25 0 1 0 544306884 633298944 138295 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154614 138295 603 41 0 154573 0
vsize: 618456
[startup+1130.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 162774 0 0 0 112624 406 0 0 25 0 1 0 544306884 634765312 138686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154972 138686 603 41 0 154931 0
vsize: 619888
[startup+1140.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 163152 0 0 0 113623 407 0 0 25 0 1 0 544306884 636354560 139064 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155360 139065 603 41 0 155319 0
vsize: 621440
[startup+1150.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 163428 0 0 0 114622 408 0 0 25 0 1 0 544306884 637476864 139340 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155634 139340 603 41 0 155593 0
vsize: 622536
[startup+1160.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 163744 0 0 0 115621 409 0 0 25 0 1 0 544306884 638803968 139656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155958 139656 603 41 0 155917 0
vsize: 623832
[startup+1170.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 164064 0 0 0 116620 410 0 0 25 0 1 0 544306884 640122880 139976 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156280 139976 603 41 0 156239 0
vsize: 625120
[startup+1180.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 164388 0 0 0 117619 411 0 0 25 0 1 0 544306884 641441792 140300 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156602 140300 603 41 0 156561 0
vsize: 626408
[startup+1190.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 164691 0 0 0 118618 413 0 0 25 0 1 0 544306884 642646016 140603 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156896 140603 603 41 0 156855 0
vsize: 627584
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 25310
Raw data (stat): 25310 (minisat+) R 25309 23176 23175 0 -1 0 164959 0 0 0 119618 413 0 0 25 0 1 0 544306884 643854336 140871 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 157191 140871 603 41 0 157150 0
vsize: 628764
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.44 s]
Raw data (loadavg): 0.99 0.97 0.99 1/54 25310
Raw data (stat): 25310 (minisat+) Z 25309 23176 23175 0 -1 12 164959 0 0 0 119618 441 0 0 25 0 1 0 544306884 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.44
CPU time (s): 1200.6
CPU user time (s): 1196.18
CPU system time (s): 4.41933
CPU usage (%): 100.014
Max. virtual memory (Kb): 628764
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####