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 17506

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        502184 kB
Buffers:          5316 kB
Cached:         503800 kB
SwapCached:          0 kB
Active:          72332 kB
Inactive:       439672 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        501932 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14832 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 10:41:06 (client local time) WITH STATUS 0 IN 1200.38 SECONDS
stats: 10790 7 1200.38 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1051 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): (none)
c ---[1050]---> BDD-cost:   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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 3945205 14082201 | 1315068       0        0     nan |  0.000 % |
c |       100 | 3945205 14082201 | 1446574     100      327     3.3 |  0.236 % |
c |       250 | 3945205 14082201 | 1591232     250      800     3.2 |  0.236 % |
c |       475 | 3945205 14082201 | 1750355     475     1534     3.2 |  0.236 % |
c |       812 | 3945205 14082201 | 1925391     812     2843     3.5 |  0.236 % |
c |      1318 | 3945205 14082201 | 2117930    1318     4503     3.4 |  0.236 % |
c |      2077 | 3945205 14082201 | 2329723    2077     7448     3.6 |  0.236 % |
c |      3216 | 3945199 14082184 | 2562695    3215    11744     3.7 |  0.236 % |
c |      4924 | 3945199 14082184 | 2818965    4923    18045     3.7 |  0.236 % |
c |      7486 | 3945199 14082184 | 3100861    7485    31399     4.2 |  0.236 % |
c |     11330 | 3945199 14082184 | 3410947   11329    57238     5.1 |  0.236 % |
c |     17096 | 3945183 14082132 | 3752042   17093    90421     5.3 |  0.237 % |
c |     25745 | 3945183 14082132 | 4127246   25742   204014     7.9 |  0.237 % |
c |     38719 | 3945183 14082132 | 4539971   38716   293444     7.6 |  0.237 % |
c |     58181 | 3945183 14082132 | 4993968   58178   759715    13.1 |  0.237 % |
c |     87373 | 3945183 14082132 | 5493365   87370  1826437    20.9 |  0.237 % |
c |    131163 | 3945183 14082132 | 6042701  131160 10181187    77.6 |  0.237 % |
c |    196847 | 3945183 14082132 | 6646972  196844 12898106    65.5 |  0.237 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/55 10039
Raw data (stat): 10039 (runsolver) R 10038 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 421580330 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.95 0.90 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 11880 0 0 0 971 27 0 0 25 0 1 0 421580330 43876352 8238 4294967295 134512640 134672761 3221224544 3221221520 134544812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10712 8238 603 41 0 10671 0
vsize: 42848
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.96 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 13513 0 0 0 1966 32 0 0 25 0 1 0 421580330 43900928 8292 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10718 8292 603 41 0 10677 0
vsize: 42872
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 13513 0 0 0 2966 32 0 0 25 0 1 0 421580330 43900928 8292 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10718 8292 603 41 0 10677 0
vsize: 42872
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 13513 0 0 0 3967 32 0 0 25 0 1 0 421580330 43900928 8292 4294967295 134512640 134672761 3221224544 3221223104 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10718 8292 603 41 0 10677 0
vsize: 42872
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 21199 0 0 0 4951 48 0 0 25 0 1 0 421580330 72740864 13782 4294967295 134512640 134672761 3221224544 3221222816 134597218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17759 13782 603 41 0 17718 0
vsize: 71036
[startup+60.0018 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 22521 0 0 0 5948 51 0 0 25 0 1 0 421580330 74092544 14112 4294967295 134512640 134672761 3221224544 3220314928 134522987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18089 14112 603 41 0 18048 0
vsize: 72356
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 22537 0 0 0 6948 52 0 0 25 0 1 0 421580330 72740864 13782 4294967295 134512640 134672761 3221224544 3221223104 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17759 13782 603 41 0 17718 0
vsize: 71036
[startup+80.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 24479 0 0 0 7943 57 0 0 25 0 1 0 421580330 75689984 14937 4294967295 134512640 134672761 3221224544 3221223872 134519316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18479 14937 603 41 0 18438 0
vsize: 73916
[startup+90.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 60677 0 0 0 8862 138 0 0 25 0 1 0 421580330 236818432 50644 4294967295 134512640 134672761 3221224544 3221217720 1075350064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57817 50644 603 41 0 57776 0
vsize: 231268
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 79101 0 0 0 9820 180 0 0 25 0 1 0 421580330 328646656 69068 4294967295 134512640 134672761 3221224544 3221223696 134565066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80236 69068 603 41 0 80195 0
vsize: 320944
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 79616 0 0 0 10818 182 0 0 25 0 1 0 421580330 330858496 69583 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80776 69583 603 41 0 80735 0
vsize: 323104
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 79996 0 0 0 11817 183 0 0 25 0 1 0 421580330 332345344 69963 4294967295 134512640 134672761 3221224544 3221223668 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81139 69963 603 41 0 81098 0
vsize: 324556
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 80394 0 0 0 12816 185 0 0 25 0 1 0 421580330 333967360 70361 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81535 70361 603 41 0 81494 0
vsize: 326140
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 80680 0 0 0 13815 186 0 0 25 0 1 0 421580330 335183872 70647 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81832 70647 603 41 0 81791 0
vsize: 327328
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 81021 0 0 0 14814 187 0 0 25 0 1 0 421580330 336588800 70988 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82175 70988 603 41 0 82134 0
vsize: 328700
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 81359 0 0 0 15812 188 0 0 25 0 1 0 421580330 337940480 71326 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82505 71326 603 41 0 82464 0
vsize: 330020
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 81601 0 0 0 16811 189 0 0 25 0 1 0 421580330 338886656 71568 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82736 71568 603 41 0 82695 0
vsize: 330944
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 81791 0 0 0 17811 190 0 0 25 0 1 0 421580330 339697664 71758 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82934 71758 603 41 0 82893 0
vsize: 331736
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 81965 0 0 0 18810 190 0 0 25 0 1 0 421580330 340373504 71932 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83099 71932 603 41 0 83058 0
vsize: 332396
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 82108 0 0 0 19810 191 0 0 25 0 1 0 421580330 341049344 72075 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83264 72075 603 41 0 83223 0
vsize: 333056
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 82219 0 0 0 20810 191 0 0 25 0 1 0 421580330 341454848 72186 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83363 72186 603 41 0 83322 0
vsize: 333452
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 82320 0 0 0 21810 192 0 0 25 0 1 0 421580330 341987328 72287 4294967295 134512640 134672761 3221224544 3221223708 134564518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83493 72287 603 41 0 83452 0
vsize: 333972
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 82445 0 0 0 22809 192 0 0 25 0 1 0 421580330 342392832 72412 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83592 72412 603 41 0 83551 0
vsize: 334368
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 82527 0 0 0 23809 192 0 0 25 0 1 0 421580330 342798336 72494 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83691 72494 603 41 0 83650 0
vsize: 334764
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 82617 0 0 0 24809 192 0 0 25 0 1 0 421580330 343068672 72584 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83757 72584 603 41 0 83716 0
vsize: 335028
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 82699 0 0 0 25809 193 0 0 25 0 1 0 421580330 343474176 72666 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83856 72666 603 41 0 83815 0
vsize: 335424
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 82871 0 0 0 26809 193 0 0 25 0 1 0 421580330 344150016 72838 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84021 72838 603 41 0 83980 0
vsize: 336084
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 83312 0 0 0 27808 194 0 0 25 0 1 0 421580330 345903104 73279 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84449 73279 603 41 0 84408 0
vsize: 337796
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 83382 0 0 0 28808 194 0 0 25 0 1 0 421580330 346173440 73349 4294967295 134512640 134672761 3221224544 3221223696 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84515 73349 603 41 0 84474 0
vsize: 338060
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 83463 0 0 0 29808 195 0 0 25 0 1 0 421580330 346578944 73430 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84614 73430 603 41 0 84573 0
vsize: 338456
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 83572 0 0 0 30808 195 0 0 25 0 1 0 421580330 346984448 73539 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84713 73539 603 41 0 84672 0
vsize: 338852
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 83658 0 0 0 31808 195 0 0 25 0 1 0 421580330 347254784 73625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84779 73625 603 41 0 84738 0
vsize: 339116
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 83762 0 0 0 32808 196 0 0 25 0 1 0 421580330 347660288 73729 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84878 73729 603 41 0 84837 0
vsize: 339512
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 84397 0 0 0 33806 198 0 0 25 0 1 0 421580330 350613504 74364 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85599 74364 603 41 0 85558 0
vsize: 342396
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 84667 0 0 0 34806 198 0 0 25 0 1 0 421580330 351694848 74634 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85863 74634 603 41 0 85822 0
vsize: 343452
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 84729 0 0 0 35805 199 0 0 25 0 1 0 421580330 351965184 74696 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85929 74696 603 41 0 85888 0
vsize: 343716
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 84799 0 0 0 36806 199 0 0 25 0 1 0 421580330 352235520 74766 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85995 74766 603 41 0 85954 0
vsize: 343980
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 84848 0 0 0 37806 199 0 0 25 0 1 0 421580330 352370688 74815 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86028 74815 603 41 0 85987 0
vsize: 344112
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 85080 0 0 0 38805 200 0 0 25 0 1 0 421580330 353312768 75047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86258 75047 603 41 0 86217 0
vsize: 345032
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 85303 0 0 0 39805 201 0 0 25 0 1 0 421580330 354250752 75270 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86487 75270 603 41 0 86446 0
vsize: 345948
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 85385 0 0 0 40805 201 0 0 25 0 1 0 421580330 354521088 75352 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86553 75352 603 41 0 86512 0
vsize: 346212
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 86414 0 0 0 41803 202 0 0 25 0 1 0 421580330 358703104 76381 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87574 76381 603 41 0 87533 0
vsize: 350296
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 87378 0 0 0 42801 205 0 0 25 0 1 0 421580330 362618880 77345 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88530 77345 603 41 0 88489 0
vsize: 354120
[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 88214 0 0 0 43799 208 0 0 25 0 1 0 421580330 366125056 78181 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 89386 78181 603 41 0 89345 0
vsize: 357544
[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 88940 0 0 0 44797 210 0 0 25 0 1 0 421580330 369090560 78907 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90110 78907 603 41 0 90069 0
vsize: 360440
[startup+460.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 89593 0 0 0 45795 212 0 0 25 0 1 0 421580330 371654656 79560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90736 79560 603 41 0 90695 0
vsize: 362944
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 90339 0 0 0 46794 213 0 0 25 0 1 0 421580330 374763520 80306 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 91495 80306 603 41 0 91454 0
vsize: 365980
[startup+480.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 91110 0 0 0 47793 215 0 0 25 0 1 0 421580330 377888768 81077 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 92258 81077 603 41 0 92217 0
vsize: 369032
[startup+490.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 91886 0 0 0 48791 217 0 0 25 0 1 0 421580330 381116416 81853 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 93046 81853 603 41 0 93005 0
vsize: 372184
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 92541 0 0 0 49790 218 0 0 25 0 1 0 421580330 383807488 82508 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 93703 82508 603 41 0 93662 0
vsize: 374812
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 93092 0 0 0 50788 220 0 0 25 0 1 0 421580330 386088960 83059 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 94260 83059 603 41 0 94219 0
vsize: 377040
[startup+520.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 93538 0 0 0 51788 222 0 0 25 0 1 0 421580330 387842048 83505 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 94688 83505 603 41 0 94647 0
vsize: 378752
[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94023 0 0 0 52787 224 0 0 25 0 1 0 421580330 389910528 83990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 95193 83990 603 41 0 95152 0
vsize: 380772
[startup+540.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94265 0 0 0 53785 225 0 0 25 0 1 0 421580330 391376896 84232 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95551 84232 603 41 0 95510 0
vsize: 382204
[startup+550.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94417 0 0 0 54784 225 0 0 25 0 1 0 421580330 392052736 84384 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95716 84384 603 41 0 95675 0
vsize: 382864
[startup+560.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94479 0 0 0 55784 226 0 0 25 0 1 0 421580330 392187904 84446 4294967295 134512640 134672761 3221224544 3221223696 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95749 84446 603 41 0 95708 0
vsize: 382996
[startup+570.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94540 0 0 0 56784 226 0 0 25 0 1 0 421580330 392458240 84507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95815 84507 603 41 0 95774 0
vsize: 383260
[startup+580.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94580 0 0 0 57784 226 0 0 25 0 1 0 421580330 392593408 84547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95848 84547 603 41 0 95807 0
vsize: 383392
[startup+590.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94628 0 0 0 58784 226 0 0 25 0 1 0 421580330 392863744 84595 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95914 84595 603 41 0 95873 0
vsize: 383656
[startup+600.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94668 0 0 0 59784 227 0 0 25 0 1 0 421580330 392998912 84635 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95947 84635 603 41 0 95906 0
vsize: 383788
[startup+610.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94709 0 0 0 60783 227 0 0 25 0 1 0 421580330 393134080 84676 4294967295 134512640 134672761 3221224544 3221223708 134564515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95980 84676 603 41 0 95939 0
vsize: 383920
[startup+620.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94750 0 0 0 61783 227 0 0 25 0 1 0 421580330 393269248 84717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96013 84717 603 41 0 95972 0
vsize: 384052
[startup+630.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 94823 0 0 0 62782 228 0 0 25 0 1 0 421580330 393539584 84790 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96079 84790 603 41 0 96038 0
vsize: 384316
[startup+640.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 95098 0 0 0 63782 229 0 0 25 0 1 0 421580330 394616832 85065 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96342 85065 603 41 0 96301 0
vsize: 385368
[startup+650.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 95363 0 0 0 64781 230 0 0 25 0 1 0 421580330 395710464 85330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96609 85330 603 41 0 96568 0
vsize: 386436
[startup+660.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 95621 0 0 0 65780 231 0 0 25 0 1 0 421580330 396783616 85588 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96871 85588 603 41 0 96830 0
vsize: 387484
[startup+670.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 95871 0 0 0 66779 232 0 0 25 0 1 0 421580330 397873152 85838 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97137 85838 603 41 0 97096 0
vsize: 388548
[startup+680.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 96099 0 0 0 67778 233 0 0 25 0 1 0 421580330 398745600 86066 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97350 86066 603 41 0 97309 0
vsize: 389400
[startup+690.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 96259 0 0 0 68778 234 0 0 25 0 1 0 421580330 399433728 86226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97518 86226 603 41 0 97477 0
vsize: 390072
[startup+700.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 96357 0 0 0 69777 234 0 0 25 0 1 0 421580330 399839232 86324 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97617 86324 603 41 0 97576 0
vsize: 390468
[startup+710.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 96565 0 0 0 70777 235 0 0 25 0 1 0 421580330 400646144 86532 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97814 86532 603 41 0 97773 0
vsize: 391256
[startup+720.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 96830 0 0 0 71776 236 0 0 25 0 1 0 421580330 401780736 86797 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 98091 86797 603 41 0 98050 0
vsize: 392364
[startup+730.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 97206 0 0 0 72775 237 0 0 25 0 1 0 421580330 403271680 87173 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 98455 87173 603 41 0 98414 0
vsize: 393820
[startup+740.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 97566 0 0 0 73774 238 0 0 25 0 1 0 421580330 404746240 87533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 98815 87533 603 41 0 98774 0
vsize: 395260
[startup+750.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 97914 0 0 0 74773 239 0 0 25 0 1 0 421580330 406106112 87881 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99147 87881 603 41 0 99106 0
vsize: 396588
[startup+760.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98061 0 0 0 75773 239 0 0 25 0 1 0 421580330 406781952 88028 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99312 88028 603 41 0 99271 0
vsize: 397248
[startup+770.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98108 0 0 0 76773 240 0 0 25 0 1 0 421580330 406917120 88075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99345 88075 603 41 0 99304 0
vsize: 397380
[startup+780.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98159 0 0 0 77772 240 0 0 25 0 1 0 421580330 407187456 88126 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99411 88126 603 41 0 99370 0
vsize: 397644
[startup+790.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98199 0 0 0 78772 240 0 0 25 0 1 0 421580330 407322624 88166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99444 88166 603 41 0 99403 0
vsize: 397776
[startup+800.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98231 0 0 0 79772 241 0 0 25 0 1 0 421580330 407457792 88198 4294967295 134512640 134672761 3221224544 3221223712 134564457 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99477 88198 603 41 0 99436 0
vsize: 397908
[startup+810.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98261 0 0 0 80772 241 0 0 25 0 1 0 421580330 407592960 88228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99510 88228 603 41 0 99469 0
vsize: 398040
[startup+820.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98292 0 0 0 81772 241 0 0 25 0 1 0 421580330 407728128 88259 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99543 88259 603 41 0 99502 0
vsize: 398172
[startup+830.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98315 0 0 0 82772 241 0 0 25 0 1 0 421580330 407863296 88282 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99576 88282 603 41 0 99535 0
vsize: 398304
[startup+840.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98338 0 0 0 83772 242 0 0 25 0 1 0 421580330 407863296 88305 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99576 88305 603 41 0 99535 0
vsize: 398304
[startup+850.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98363 0 0 0 84772 242 0 0 25 0 1 0 421580330 407998464 88330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99609 88330 603 41 0 99568 0
vsize: 398436
[startup+860.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98385 0 0 0 85772 242 0 0 25 0 1 0 421580330 408133632 88352 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99642 88352 603 41 0 99601 0
vsize: 398568
[startup+870.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98411 0 0 0 86771 242 0 0 25 0 1 0 421580330 408133632 88378 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99642 88378 603 41 0 99601 0
vsize: 398568
[startup+880.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98439 0 0 0 87771 243 0 0 25 0 1 0 421580330 408268800 88406 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99675 88406 603 41 0 99634 0
vsize: 398700
[startup+890.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98462 0 0 0 88771 243 0 0 25 0 1 0 421580330 408403968 88429 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99708 88429 603 41 0 99667 0
vsize: 398832
[startup+900.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98489 0 0 0 89771 243 0 0 25 0 1 0 421580330 408543232 88456 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99742 88456 603 41 0 99701 0
vsize: 398968
[startup+910.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98518 0 0 0 90771 243 0 0 25 0 1 0 421580330 408543232 88485 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99742 88485 603 41 0 99701 0
vsize: 398968
[startup+920.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98541 0 0 0 91771 243 0 0 25 0 1 0 421580330 408678400 88508 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99775 88508 603 41 0 99734 0
vsize: 399100
[startup+930.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98565 0 0 0 92771 243 0 0 25 0 1 0 421580330 408813568 88532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99808 88532 603 41 0 99767 0
vsize: 399232
[startup+940.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98586 0 0 0 93771 243 0 0 25 0 1 0 421580330 408813568 88553 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99808 88553 603 41 0 99767 0
vsize: 399232
[startup+950.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98611 0 0 0 94771 243 0 0 25 0 1 0 421580330 408948736 88578 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99841 88578 603 41 0 99800 0
vsize: 399364
[startup+960.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98632 0 0 0 95771 244 0 0 25 0 1 0 421580330 408948736 88599 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99841 88599 603 41 0 99800 0
vsize: 399364
[startup+970.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98664 0 0 0 96771 244 0 0 25 0 1 0 421580330 409083904 88631 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 99874 88631 603 41 0 99833 0
vsize: 399496
[startup+980.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98683 0 0 0 97771 244 0 0 25 0 1 0 421580330 409219072 88650 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 99907 88650 603 41 0 99866 0
vsize: 399628
[startup+990.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98707 0 0 0 98771 244 0 0 25 0 1 0 421580330 409354240 88674 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 99940 88674 603 41 0 99899 0
vsize: 399760
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98725 0 0 0 99771 244 0 0 25 0 1 0 421580330 409354240 88692 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 99940 88692 603 41 0 99899 0
vsize: 399760
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98744 0 0 0 100771 244 0 0 25 0 1 0 421580330 409489408 88711 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 99973 88711 603 41 0 99932 0
vsize: 399892
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98764 0 0 0 101772 244 0 0 25 0 1 0 421580330 409489408 88731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 99973 88731 603 41 0 99932 0
vsize: 399892
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98786 0 0 0 102772 244 0 0 25 0 1 0 421580330 409624576 88753 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100006 88753 603 41 0 99965 0
vsize: 400024
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98805 0 0 0 103772 244 0 0 25 0 1 0 421580330 409624576 88772 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100006 88772 603 41 0 99965 0
vsize: 400024
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98829 0 0 0 104772 244 0 0 25 0 1 0 421580330 409759744 88796 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100039 88796 603 41 0 99998 0
vsize: 400156
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98849 0 0 0 105772 244 0 0 25 0 1 0 421580330 409894912 88816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100072 88816 603 41 0 100031 0
vsize: 400288
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98868 0 0 0 106772 244 0 0 25 0 1 0 421580330 409894912 88835 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100072 88835 603 41 0 100031 0
vsize: 400288
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98885 0 0 0 107772 245 0 0 25 0 1 0 421580330 410030080 88852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100105 88852 603 41 0 100064 0
vsize: 400420
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98899 0 0 0 108772 245 0 0 25 0 1 0 421580330 410030080 88866 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100105 88866 603 41 0 100064 0
vsize: 400420
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98916 0 0 0 109773 245 0 0 25 0 1 0 421580330 410165248 88883 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100138 88883 603 41 0 100097 0
vsize: 400552
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98939 0 0 0 110773 245 0 0 25 0 1 0 421580330 410165248 88906 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100138 88906 603 41 0 100097 0
vsize: 400552
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98951 0 0 0 111773 245 0 0 25 0 1 0 421580330 410165248 88918 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100138 88918 603 41 0 100097 0
vsize: 400552
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98970 0 0 0 112774 245 0 0 25 0 1 0 421580330 410300416 88937 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100171 88937 603 41 0 100130 0
vsize: 400684
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 98986 0 0 0 113774 245 0 0 25 0 1 0 421580330 410300416 88953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100171 88953 603 41 0 100130 0
vsize: 400684
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 99010 0 0 0 114774 245 0 0 25 0 1 0 421580330 410435584 88977 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100204 88977 603 41 0 100163 0
vsize: 400816
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 99028 0 0 0 115773 245 0 0 25 0 1 0 421580330 410435584 88995 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100204 88995 603 41 0 100163 0
vsize: 400816
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 99043 0 0 0 116774 245 0 0 25 0 1 0 421580330 410570752 89010 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100237 89010 603 41 0 100196 0
vsize: 400948
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 99059 0 0 0 117774 246 0 0 25 0 1 0 421580330 410570752 89026 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100237 89026 603 41 0 100196 0
vsize: 400948
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 99077 0 0 0 118774 246 0 0 25 0 1 0 421580330 410705920 89044 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100270 89044 603 41 0 100229 0
vsize: 401080
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10039
Raw data (stat): 10039 (minisat+) R 10038 30927 30926 0 -1 0 99090 0 0 0 119774 246 0 0 25 0 1 0 421580330 410705920 89057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100270 89057 603 41 0 100229 0
vsize: 401080
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 10039
Raw data (stat): 10039 (minisat+) Z 10038 30927 30926 0 -1 12 99092 0 0 0 119774 263 0 0 25 0 1 0 421580330 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.23
CPU time (s): 1200.38
CPU user time (s): 1197.75
CPU system time (s): 2.6356
CPU usage (%): 100.012
Max. virtual memory (Kb): 401080
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####