## The N-queens problem, using bit vectors

A smart and efficient code using bit-vector operations to compute the number of solutions of the N-queens problem. This case study is detailed in Inria research report 8821.

**Authors:** Clément Fumex / Claude Marché / Jean-Christophe Filliâtre

**Topics:** Ghost code / Bitwise operations

**Tools:** Why3

**References:** ProofInUse joint laboratory

see also the index (by topic, by tool, by reference, by year)

# N-queens problem

Verification of the following 2-lines C program solving the N-queens problem:

t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b+d)*2,( c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}

## finite sets of integers, with succ and pred operations

theory S use export set.Fsetint function succ (set int) : set int axiom succ_def: forall s: set int, i: int. mem i (succ s) <-> i >= 1 /\ mem (i-1) s function pred (set int) : set int axiom pred_def: forall s: set int, i: int. mem i (pred s) <-> i >= 0 /\ mem (i+1) s end

## Formalization of the set of solutions of the N-queens problem

theory Solution use int.Int use export map.Map constant n : int

the number of queens

type solution = map int int predicate eq_prefix (t u: map int 'a) (i: int) = forall k: int. 0 <= k < i -> t[k] = u[k]

solutions `t`

and `u`

have the same prefix `[0..i[`

predicate eq_sol (t u: solution) = eq_prefix t u n predicate partial_solution (k: int) (s: solution) = forall i: int. 0 <= i < k -> 0 <= s[i] < n /\ (forall j: int. 0 <= j < i -> s[i] <> s[j] /\ s[i]-s[j] <> i-j /\ s[i]-s[j] <> j-i)

`s`

stores a partial solution, for the rows `0..k-1`

predicate solution (s: solution) = partial_solution n s lemma partial_solution_eq_prefix: forall u t: solution, k: int. partial_solution k t -> eq_prefix t u k -> partial_solution k u predicate lt_sol (s1 s2: solution) = exists i: int. 0 <= i < n /\ eq_prefix s1 s2 i /\ s1[i] < s2[i] type solutions = map int solution predicate sorted (s: solutions) (a b: int) = forall i j: int. a <= i < j < b -> lt_sol s[i] s[j]

`s[a..b[`

is sorted for `lt_sol`

lemma no_duplicate: forall s: solutions, a b: int. sorted s a b -> forall i j: int. a <= i < j < b -> not (eq_sol s[i] s[j])

a sorted array of solutions contains no duplicate

```
end
```

## More realistic code with bitwise operations

module BitsSpec use S constant size : int = 32 type t = private { ghost mdl: set int; } invariant { forall i. mem i mdl -> 0 <= i < size } val empty () : t ensures { is_empty result.mdl } val is_empty (x:t) : bool ensures { result <-> is_empty x.mdl } val remove_singleton (a b: t) : t requires { b.mdl = singleton (min_elt b.mdl) } requires { mem (min_elt b.mdl) a.mdl } ensures { result.mdl = remove (min_elt b.mdl) a.mdl } val add_singleton (a b: t) : t requires { b.mdl = singleton (min_elt b.mdl) } (* requires { not (mem (min_elt b.mdl) a.mdl) } *) (* this is not required if the implementation uses or instead of add *) ensures { result.mdl = S.add (min_elt b.mdl) a.mdl } val mul2 (a: t) : t ensures { result.mdl = remove size (succ a.mdl) } val div2 (a: t) : t ensures { result.mdl = pred a.mdl } val diff (a b: t) : t ensures { result.mdl = diff a.mdl b.mdl } use ref.Ref val rightmost_bit_trick (a: t) (ghost min : ref int) : t requires { not (is_empty a.mdl) } writes { min } ensures { !min = min_elt a.mdl } ensures { result.mdl = singleton !min } use bv.BV32 as BV32 val below (n: BV32.t) : t requires { BV32.ule n (32:BV32.t) } ensures { result.mdl = interval 0 (BV32.t'int n) } end

## The 1-bits of an integer, as a set of integers

module Bits use S use bv.BV32 constant size : int = 32 type t = { bv : BV32.t; ghost mdl: set int; } invariant { forall i: int. (0 <= i < size /\ nth bv i) <-> mem i mdl } let empty () : t ensures { is_empty result.mdl } = { bv = zeros; mdl = empty } let is_empty (x:t) : bool ensures { result <-> is_empty x.mdl } = assert {is_empty x.mdl -> x.bv = zeros by x.bv == zeros}; BV32.eq x.bv zeros let remove_singleton (a b: t) : t requires { b.mdl = singleton (min_elt b.mdl) } requires { mem (min_elt b.mdl) a.mdl } ensures { result.mdl = remove (min_elt b.mdl) a.mdl } = { bv = bw_and a.bv (bw_not b.bv); mdl = ghost remove (min_elt b.mdl) a.mdl } (* { bv = sub a.bv b.bv; mdl = remove (min_elt b.mdl) a.mdl } *) let add_singleton (a b: t) : t requires { b.mdl = singleton (min_elt b.mdl) } (* requires { not (mem (min_elt b.mdl) a.mdl) } *) (* this is not required if the implementation uses or instead of add *) ensures { result.mdl = S.add (min_elt b.mdl) a.mdl } = { bv = bw_or a.bv b.bv; mdl = ghost S.add (min_elt b.mdl) a.mdl } (* { bv = add a.bv b.bv; mdl = add (min_elt b.mdl) a.mdl } *) let mul2 (a: t) : t ensures { result.mdl = remove size (succ a.mdl) } = { bv = lsl_bv a.bv (1:BV32.t); mdl = ghost remove size (succ a.mdl) } let div2 (a: t) : t ensures { result.mdl = pred a.mdl } = { bv = lsr_bv a.bv (1:BV32.t); mdl = ghost pred a.mdl } let diff (a b: t) : t ensures { result.mdl = diff a.mdl b.mdl } = { bv = bw_and a.bv (bw_not b.bv); mdl = ghost diff a.mdl b.mdl } predicate bits_interval_is_zeros_bv (a:BV32.t) (i:BV32.t) (n:BV32.t) = eq_sub_bv a zeros i n predicate bits_interval_is_one_bv (a:BV32.t) (i:BV32.t) (n:BV32.t) = eq_sub_bv a ones i n predicate bits_interval_is_zeros (a:BV32.t) (i : int) (n : int) = eq_sub a zeros i n predicate bits_interval_is_one (a:BV32.t) (i : int) (n : int) = eq_sub a ones i n let rightmost_bit_trick (a: t) : t requires { not (is_empty a.mdl) } ensures { result.mdl = singleton (min_elt a.mdl) } = let ghost n = min_elt a.mdl in let ghost n_bv = of_int n in assert {bits_interval_is_zeros_bv a.bv zeros n_bv}; assert {nth_bv a.bv n_bv}; assert {nth_bv (neg a.bv) n_bv}; let res = bw_and a.bv (neg a.bv) in assert {forall i. 0 <= i < n -> not (nth res i)}; assert {bits_interval_is_zeros_bv res (add n_bv (1:BV32.t)) (sub (31:BV32.t) n_bv )}; assert {bits_interval_is_zeros res (n + 1) (31 - n)}; { bv = res; mdl = singleton n } let below (n: BV32.t) : t requires { BV32.ule n (32:BV32.t) } ensures { result.mdl = interval 0 (t'int n) } = { bv = bw_not (lsl_bv ones n); mdl = ghost interval 0 (t'int n) } end module NQueensBits use BitsSpec use ref.Ref use Solution use int.Int val ghost col: ref solution (* solution under construction *) (* val ghost k : ref int (* current row in the current solution *) *) val ghost sol: ref solutions (* all solutions *) val ghost s : ref int (* next slot for a solution = number of solutions *) let rec t (a b c: BitsSpec.t) (ghost k : int) requires { n <= size } requires { 0 <= k } requires { k + S.cardinal a.mdl = n } requires { !s >= 0 } requires { forall i: int. S.mem i a.mdl <-> ( 0 <= i < n /\ forall j: int. 0 <= j < k -> !col[j] <> i) } requires { forall i: int. 0 <= i < size -> ( not (S.mem i b.mdl) <-> forall j: int. 0 <= j < k -> i - !col[j] <> k - j) } requires { forall i: int. 0 <= i < size -> ( not (S.mem i c.mdl) <-> forall j: int. 0 <= j < k -> i - !col[j] <> j - k ) } requires { partial_solution k !col } variant { S.cardinal a.mdl } ensures { result = !s - old !s >= 0 } ensures { sorted !sol (old !s) !s } ensures { forall i:int. old !s <= i < !s -> solution !sol[i] /\ eq_prefix !col !sol[i] k } ensures { forall u: solution. solution u /\ eq_prefix !col u k -> exists i: int. old !s <= i < !s /\ eq_sol u !sol[i] } (* assigns *) ensures { eq_prefix (old !col) !col k } ensures { eq_prefix (old !sol) !sol (old !s) } = if not (is_empty a) then begin let e = ref (diff (diff a b) c) in (* first, you show that if u is a solution with the same k-prefix as col, then u[k] (the position of the queen on the row k) must belong to e *) assert { forall u:solution. solution u /\ eq_prefix !col u k -> S.mem u[k] !e.mdl }; let f = ref 0 in let ghost min = ref (-1) in label L in while not (is_empty !e) do variant { S.cardinal !e.mdl } invariant { not (S.is_empty !e.mdl) -> !min < S.min_elt !e.mdl } invariant { !f = !s - (!s at L) >= 0 } invariant { S.subset !e.mdl (S.diff (S.diff a.mdl b.mdl) c.mdl) } invariant { partial_solution k !col } invariant { sorted !sol (!s at L) !s } invariant { forall i: int. S.mem i (!e.mdl at L) /\ not (S.mem i !e.mdl) -> i <= !min } invariant { forall i:int. (!s at L) <= i < !s -> solution !sol[i] /\ eq_prefix !col !sol[i] k /\ 0 <= !sol[i][k] <= !min } invariant { forall u: solution. (solution u /\ eq_prefix !col u k /\ 0 <= u[k] <= !min) -> S.mem u[k] (!e.mdl at L) && not (S.mem u[k] !e.mdl) && exists i: int. (!s at L) <= i < !s /\ eq_sol u !sol[i] } (* assigns *) invariant { eq_prefix (!col at L) !col k } invariant { eq_prefix (!sol at L) !sol (!s at L) } label N in let d = rightmost_bit_trick !e min in ghost col := !col[k <- !min]; assert { 0 <= !col[k] < size }; assert { not (S.mem !col[k] b.mdl) }; assert { not (S.mem !col[k] c.mdl) }; assert { eq_prefix (!col at L) !col k }; assert { forall i: int. S.mem i a.mdl -> (forall j: int. 0 <= j < k -> !col[j] <> i) }; assert { forall i: int. S.mem i (S.remove (S.min_elt d.mdl) a.mdl) <-> (0 <= i < n /\ (forall j: int. 0 <= j < k + 1 -> !col[j] <> i)) }; let ghost b' = mul2 (add_singleton b d) in assert { forall i: int. 0 <= i < size -> S.mem i b'.mdl -> (i = !min + 1 \/ S.mem (i - 1) b.mdl) && not (forall j:int. 0 <= j < k + 1 -> i - !col[j] <> k + 1 - j) }; let ghost c' = div2 (add_singleton c d) in assert { forall i: int. 0 <= i < size -> S.mem i c'.mdl -> (i = !min - 1 \/ (i + 1 < size /\ S.mem (i + 1) c.mdl)) && not (forall j:int. 0 <= j < k + 1 -> i - !col[j] <> j - k - 1) }; label M in f := !f + t (remove_singleton a d) (mul2 (add_singleton b d)) (div2 (add_singleton c d)) (k + 1); assert { forall i j. (!s at L) <= i < (!s at M) <= j < !s -> (eq_prefix !sol[i] !sol[j] k /\ !sol[i][k] <= (!min at N) < !min = !sol[j][k]) && lt_sol !sol[i] !sol[j]}; e := remove_singleton !e d done; assert { forall u:solution. solution u /\ eq_prefix !col u k -> S.mem u[k] (!e.mdl at L) && 0 <= u[k] <= !min }; !f end else begin ghost sol := !sol[!s <- !col]; ghost s := !s + 1; 1 end let queens (q: BV32.t) requires { BV32.t'int q = n } requires { BV32.ule q BV32.size_bv } requires { !s = 0 } ensures { result = !s } ensures { sorted !sol 0 !s } ensures { forall u: solution. solution u <-> exists i: int. 0 <= i < result /\ eq_sol u !sol[i] } = t (below q) (empty()) (empty()) 0 let test8 () requires { size = 32 } requires { n = 8 } = s := 0; queens (BV32.of_int 8) end

download ZIP archive

# Why3 Proof Results for Project "queens_bv"

## Theory "queens_bv.Solution": fully verified

Obligations | Alt-Ergo 0.99.1 | CVC3 2.4.1 | CVC4 1.4 |

partial_solution_eq_prefix | 0.03 | --- | --- |

no_duplicate | --- | 0.02 | 0.03 |

## Theory "queens_bv.BitsSpec": fully verified

Obligations | Eprover 1.8-001 |

VC t | 0.03 |

## Theory "queens_bv.Bits": fully verified

Obligations | Alt-Ergo 0.99.1 | Alt-Ergo 1.01 | Alt-Ergo 1.30 | CVC4 1.4 (noBV) | Eprover 1.8-001 | Z3 4.4.1 | Z3 4.5.0 | ||

VC t | --- | --- | --- | --- | 0.03 | --- | --- | ||

VC empty | 0.03 | --- | --- | --- | --- | --- | --- | ||

VC is_empty | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | |||||||||

VC is_empty.0 | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | |||||||||

VC is_empty.0.0 | --- | 0.10 | --- | --- | --- | --- | --- | ||

VC is_empty.0.1 | --- | 0.06 | --- | --- | --- | --- | --- | ||

VC is_empty.1 | --- | 0.05 | --- | --- | --- | --- | --- | ||

VC remove_singleton | 1.79 | --- | --- | --- | --- | --- | --- | ||

VC add_singleton | --- | --- | --- | 0.08 | --- | --- | --- | ||

VC mul2 | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | |||||||||

VC mul2.0 | --- | 0.32 | --- | --- | --- | --- | --- | ||

VC mul2.1 | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | |||||||||

VC mul2.1.0 | 0.04 | --- | --- | --- | --- | --- | --- | ||

VC div2 | 0.62 | --- | --- | --- | --- | --- | --- | ||

VC diff | 0.26 | --- | --- | --- | --- | --- | --- | ||

VC rightmost_bit_trick | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | |||||||||

VC rightmost_bit_trick.0 | --- | --- | --- | --- | --- | 0.02 | --- | ||

VC rightmost_bit_trick.1 | --- | 0.24 | --- | --- | --- | --- | --- | ||

VC rightmost_bit_trick.2 | --- | --- | --- | 0.08 | --- | --- | --- | ||

VC rightmost_bit_trick.3 | --- | --- | --- | --- | --- | 0.03 | --- | ||

VC rightmost_bit_trick.4 | --- | --- | 0.05 | --- | --- | --- | --- | ||

VC rightmost_bit_trick.5 | --- | --- | --- | --- | --- | 0.22 | --- | ||

VC rightmost_bit_trick.6 | --- | --- | --- | --- | --- | --- | 0.24 | ||

VC rightmost_bit_trick.7 | 0.56 | --- | --- | --- | --- | --- | --- | ||

VC rightmost_bit_trick.8 | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | |||||||||

VC rightmost_bit_trick.8.0 | 0.05 | --- | --- | --- | --- | --- | --- | ||

VC below | --- | --- | --- | 0.06 | --- | --- | --- |

## Theory "queens_bv.NQueensBits": fully verified

Obligations | Alt-Ergo 0.99.1 | Alt-Ergo 1.01 | Alt-Ergo 1.30 | CVC4 1.4 | CVC4 1.4 (noBV) | CVC4 1.5 | Z3 4.4.1 | Z3 4.5.0 | ||

VC t | --- | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||||

VC t.0 | --- | 0.82 | --- | --- | --- | --- | --- | --- | ||

VC t.1 | --- | --- | --- | 0.20 | --- | --- | --- | --- | ||

VC t.2 | --- | --- | --- | 0.03 | --- | --- | --- | --- | ||

VC t.3 | --- | --- | --- | 0.10 | --- | --- | --- | --- | ||

VC t.4 | --- | --- | --- | 0.04 | --- | --- | --- | --- | ||

VC t.5 | --- | 0.03 | 0.03 | --- | --- | --- | --- | --- | ||

VC t.6 | --- | --- | --- | 0.06 | --- | --- | --- | --- | ||

VC t.7 | --- | --- | --- | 0.02 | --- | --- | --- | --- | ||

VC t.8 | --- | --- | --- | 0.03 | --- | --- | --- | --- | ||

VC t.9 | --- | --- | --- | 0.03 | --- | --- | --- | --- | ||

VC t.10 | --- | --- | --- | 0.04 | --- | --- | --- | --- | ||

VC t.11 | --- | --- | --- | 0.03 | --- | --- | --- | --- | ||

VC t.12 | --- | --- | --- | 0.35 | --- | --- | --- | --- | ||

VC t.13 | --- | --- | --- | --- | --- | --- | --- | 0.04 | ||

VC t.14 | --- | --- | --- | 0.53 | --- | --- | --- | --- | ||

VC t.15 | --- | --- | --- | 0.07 | --- | --- | --- | --- | ||

VC t.16 | --- | --- | --- | 0.24 | --- | --- | --- | --- | ||

VC t.17 | --- | --- | --- | 1.00 | --- | --- | --- | --- | ||

VC t.18 | --- | --- | --- | 0.13 | --- | --- | --- | --- | ||

VC t.19 | --- | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||||

VC t.19.0 | --- | --- | --- | --- | --- | --- | 0.31 | --- | ||

VC t.19.1 | --- | 4.10 | --- | --- | --- | --- | --- | --- | ||

VC t.20 | --- | --- | --- | --- | --- | 0.40 | --- | --- | ||

VC t.21 | --- | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||||

VC t.21.0 | --- | 0.52 | --- | --- | --- | --- | --- | --- | ||

VC t.21.1 | --- | 1.94 | --- | --- | --- | --- | --- | --- | ||

VC t.22 | --- | --- | --- | 0.19 | --- | --- | --- | --- | ||

VC t.23 | --- | --- | --- | 0.20 | --- | --- | --- | --- | ||

VC t.24 | --- | --- | --- | 0.20 | --- | --- | --- | --- | ||

VC t.25 | --- | --- | --- | 0.23 | --- | --- | --- | --- | ||

VC t.26 | --- | --- | --- | 0.22 | --- | --- | --- | --- | ||

VC t.27 | --- | --- | --- | 0.14 | --- | --- | --- | --- | ||

VC t.28 | --- | --- | --- | 0.11 | --- | --- | --- | --- | ||

VC t.29 | --- | --- | --- | 0.70 | --- | --- | --- | --- | ||

VC t.30 | --- | --- | --- | 0.06 | --- | --- | --- | --- | ||

VC t.31 | --- | --- | --- | 0.51 | --- | --- | --- | --- | ||

VC t.32 | --- | --- | --- | 1.93 | --- | --- | --- | --- | ||

VC t.33 | --- | --- | --- | 2.15 | --- | --- | --- | --- | ||

VC t.34 | --- | --- | --- | 3.02 | --- | --- | --- | --- | ||

VC t.35 | --- | --- | --- | 2.42 | --- | --- | --- | --- | ||

VC t.36 | --- | --- | --- | 0.23 | --- | --- | --- | --- | ||

VC t.37 | --- | --- | --- | --- | --- | 0.19 | --- | --- | ||

VC t.38 | --- | --- | --- | 0.24 | --- | --- | --- | --- | ||

VC t.39 | --- | --- | --- | 0.64 | --- | --- | --- | --- | ||

VC t.40 | --- | --- | --- | 0.12 | --- | --- | --- | --- | ||

VC t.41 | --- | --- | --- | 0.15 | --- | --- | --- | --- | ||

VC t.42 | --- | --- | --- | 0.37 | --- | --- | --- | --- | ||

VC t.43 | --- | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||||

VC t.43.0 | --- | --- | --- | 0.23 | 0.25 | --- | --- | --- | ||

VC t.44 | --- | --- | --- | 0.29 | --- | --- | --- | --- | ||

VC t.45 | --- | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||||

VC t.45.0 | --- | 0.24 | --- | --- | --- | --- | --- | --- | ||

VC t.45.1 | --- | --- | --- | 9.85 | --- | --- | --- | --- | ||

VC t.45.2 | --- | --- | --- | 0.62 | --- | --- | --- | --- | ||

VC t.45.3 | --- | --- | --- | 2.30 | --- | --- | --- | --- | ||

VC t.46 | --- | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||||

VC t.46.0 | --- | --- | --- | 0.80 | --- | --- | --- | --- | ||

VC t.46.1 | --- | --- | --- | 0.12 | --- | --- | --- | --- | ||

VC t.46.2 | --- | --- | --- | 19.94 | 15.12 | --- | --- | --- | ||

VC t.47 | --- | --- | --- | 0.08 | --- | --- | --- | --- | ||

VC t.48 | --- | --- | --- | 0.19 | --- | --- | --- | --- | ||

VC t.49 | --- | --- | --- | 0.17 | --- | --- | --- | --- | ||

VC t.50 | --- | --- | --- | 0.07 | --- | --- | --- | --- | ||

VC t.51 | --- | --- | --- | 0.07 | --- | --- | --- | --- | ||

VC t.52 | --- | --- | --- | 0.04 | --- | --- | --- | --- | ||

VC t.53 | --- | --- | --- | 0.07 | --- | --- | --- | --- | ||

VC t.54 | 0.04 | --- | --- | --- | --- | --- | --- | --- | ||

VC t.55 | 0.04 | --- | --- | --- | --- | --- | --- | --- | ||

VC t.56 | --- | --- | --- | 0.07 | --- | --- | --- | --- | ||

VC t.57 | --- | --- | --- | 0.08 | --- | --- | --- | --- | ||

VC t.58 | --- | --- | --- | --- | --- | --- | --- | 0.02 | ||

VC t.59 | --- | --- | --- | --- | --- | --- | 0.04 | --- | ||

VC t.60 | --- | --- | --- | 0.06 | --- | --- | --- | --- | ||

VC t.61 | --- | --- | --- | 0.07 | --- | --- | --- | --- | ||

VC queens | --- | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||||

VC queens.0 | --- | --- | --- | 0.04 | --- | --- | --- | --- | ||

VC queens.1 | --- | --- | --- | 0.10 | --- | --- | --- | --- | ||

VC queens.2 | --- | --- | --- | 0.10 | --- | --- | --- | --- | ||

VC queens.3 | --- | --- | --- | 0.10 | --- | --- | --- | --- | ||

VC queens.4 | --- | --- | --- | 0.09 | --- | --- | --- | --- | ||

VC queens.5 | --- | --- | --- | 0.08 | --- | --- | --- | --- | ||

VC queens.6 | --- | --- | --- | 0.08 | --- | --- | --- | --- | ||

VC queens.7 | --- | --- | --- | 0.10 | --- | --- | --- | --- | ||

VC queens.8 | --- | --- | --- | 0.12 | --- | --- | --- | --- | ||

VC queens.9 | --- | --- | --- | 0.04 | --- | --- | --- | --- | ||

VC queens.10 | --- | --- | --- | 0.08 | --- | --- | --- | --- | ||

VC queens.11 | --- | --- | --- | 0.78 | --- | --- | --- | --- | ||

VC test8 | --- | --- | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||||

VC test8.0 | --- | --- | --- | 0.04 | --- | --- | --- | --- | ||

VC test8.1 | --- | --- | --- | 0.05 | --- | --- | --- | --- | ||

VC test8.2 | --- | --- | --- | 0.04 | --- | --- | --- | --- |