sunblaze-ucb/verina huggingface dataset:
-----Description-----
Write a Lean 4 function that returns the first duplicate integer found in a list. The function should return the value of the first duplicate it encounters, scanning from left to right. If no duplicates exist, return -1.

-----Input-----
lst: A list of integers.

-----Output-----
An Option Int:
- `some x` where x is the first duplicated value encountered when scanning left to right
- `none` if no duplicates exist in the list


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def firstDuplicate_precond (lst : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def firstDuplicate (lst : List Int) (h_precond : firstDuplicate_precond (lst)) : Option Int :=
  -- !benchmark @start code
  let rec helper (seen : List Int) (rem : List Int) : Option Int :=
    match rem with
    | [] => none
    | h :: t => if seen.contains h then some h else helper (h :: seen) t
  helper [] lst
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def firstDuplicate_postcond (lst : List Int) (result: Option Int) (h_precond : firstDuplicate_precond (lst)) : Prop :=
  -- !benchmark @start postcond
  match result with
  | none => List.Nodup lst
  | some x =>
    lst.count x > 1 ∧
    (lst.filter (fun y => lst.count y > 1)).head? = some x
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem firstDuplicate_spec_satisfied (lst: List Int) (h_precond : firstDuplicate_precond (lst)) :
    firstDuplicate_postcond (lst) (firstDuplicate (lst) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: lst: [1, 2, 3, 2, 4]
lst: [5, 1, 2, 3, 4, 5]
lst: [1, 2, 3, 4, 5]
lst: [7, 7, 7, 7]
lst: [-1, 2, -1]
expected: some 2
some 5
none
some 7
none
some (-1)
unexpected: some 1
some 3
none
some 1
none
some 1
some 2
some 3
none
some 0
some 1
none
some 2

Inputs rejected by the precondition:
-----Description-----  
This task requires writing a Lean 4 method that finds the **majority element** in a list of integers. A majority element is defined as an element that appears **strictly more than half** the number of times in the list.

If such an element exists, the method should return that element. Otherwise, it should return `-1`. The implementation must ensure that the result is either the majority element (if one exists) or `-1` (when no such element appears more than ⌊n/2⌋ times).

-----Input-----  
The input consists of a list of integers:
- lst: A list of integers, which may include duplicates and negative numbers. The list may also be empty.

-----Output-----  
The output is a single integer:
- If a majority element exists in the input list, return that element.
- If no majority element exists, return `-1`.


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible, simp]
def findMajorityElement_precond (lst : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def countOccurrences (n : Int) (lst : List Int) : Nat :=
  lst.foldl (fun acc x => if x = n then acc + 1 else acc) 0
-- !benchmark @end code_aux


def findMajorityElement (lst : List Int) (h_precond : findMajorityElement_precond (lst)) : Int :=
  -- !benchmark @start code
  let n := lst.length
  let majority := lst.find? (fun x => countOccurrences x lst > n / 2)
  match majority with
  | some x => x
  | none => -1
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def findMajorityElement_postcond (lst : List Int) (result: Int) (h_precond : findMajorityElement_precond (lst)) : Prop :=
  -- !benchmark @start postcond
  let count := fun x => (lst.filter (fun y => y = x)).length
  let n := lst.length
  let majority := count result > n / 2 ∧ lst.all (fun x => count x ≤ n / 2 ∨ x = result)
  (result = -1 → lst.all (count · ≤ n / 2) ∨ majority) ∧
  (result ≠ -1 → majority)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem findMajorityElement_spec_satisfied (lst: List Int) (h_precond : findMajorityElement_precond (lst)) :
    findMajorityElement_postcond (lst) (findMajorityElement (lst) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: lst: [1, 2, 1, 1]
lst: [1, 2, 3, 4]
lst: [2, 2, 2, 2, 3, 3]
lst: [5, 5, 5, 5, 5, 5]
lst: [-1, -1, -1, 2, 2]
lst: [-3, -3, -3, -3, 1]
expected: 1
-1
2
-1
5
-1
-3
unexpected: 2
-1
1
2
3
4
3
-1
0
1
0
-1
2
1
-1

Inputs rejected by the precondition:
-----Description-----  
This task focuses on determining if a given integer is even. The problem requires checking whether the integer can be represented as twice another integer, meaning it is divisible by 2 without any remainder.

-----Input-----  
The input consists of a single integer:  
• x: An integer to be evaluated.

-----Output-----  
The output is a boolean value:  
• true if x is even (x mod 2 equals 0).  
• false if x is odd.

-----Note-----  
No additional preconditions are required. The method should work correctly for any integer value.
Difficulty: basic

Lean 4 solution:
-- !benchmark @start import type=solution
import Mathlib
-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible, simp]
def ComputeIsEven_precond (x : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def ComputeIsEven (x : Int) (h_precond : ComputeIsEven_precond (x)) : Bool :=
  -- !benchmark @start code
  if x % 2 = 0 then true else false
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def ComputeIsEven_postcond (x : Int) (result: Bool) (h_precond : ComputeIsEven_precond (x)) :=
  -- !benchmark @start postcond
  result = true ↔ ∃ k : Int, x = 2 * k
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem ComputeIsEven_spec_satisfied (x: Int) (h_precond : ComputeIsEven_precond (x)) :
    ComputeIsEven_postcond (x) (ComputeIsEven (x) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold ComputeIsEven ComputeIsEven_postcond
  simp
  rfl
  -- !benchmark @end proof


Tests:
input: x: 4
x: 7
x: 0
x: -2
x: -3
expected: True
False
True
True
False
unexpected: False
True
False
False
True

Inputs rejected by the precondition:
-----Description-----  
You are given an array of integers and a threshold value k. The problem is to create a new array where every element greater than k is replaced with -1 while every other element remains unchanged.

-----Input-----  
The input consists of:  
• arr: An array of integers.  
• k: An integer used as the threshold for replacement.

-----Output-----  
The output is an array of integers that satisfies the following conditions:  
• For every index i, if arr[i] is greater than k, then the returned array at index i is -1.  
• For every index i, if arr[i] is less than or equal to k, then the returned array at index i remains unchanged.

-----Note-----  
It is assumed that the input array may be empty or non-empty, and that k can be any integer. There are no additional preconditions.
Difficulty: basic

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible, simp]
def replace_precond (arr : Array Int) (k : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def replace_loop (oldArr : Array Int) (k : Int) : Nat → Array Int → Array Int
| i, acc =>
  if i < oldArr.size then
    if (oldArr[i]!) > k then
      replace_loop oldArr k (i+1) (acc.set! i (-1))
    else
      replace_loop oldArr k (i+1) acc
  else
    acc
-- !benchmark @end code_aux


def replace (arr : Array Int) (k : Int) (h_precond : replace_precond (arr) (k)) : Array Int :=
  -- !benchmark @start code
  replace_loop arr k 0 arr
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def replace_postcond (arr : Array Int) (k : Int) (result: Array Int) (h_precond : replace_precond (arr) (k)) :=
  -- !benchmark @start postcond
  (∀ i : Nat, i < arr.size → (arr[i]! > k → result[i]! = -1)) ∧
  (∀ i : Nat, i < arr.size → (arr[i]! ≤ k → result[i]! = arr[i]!))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem replace_spec_satisfied (arr: Array Int) (k: Int) (h_precond : replace_precond (arr) (k)) :
    replace_postcond (arr) (k) (replace (arr) (k) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: arr: #[1, 5, 3, 10]
k: 4
arr: #[-1, 0, 1, 2]
k: 2
arr: #[100, 50, 100]
k: 100
arr: #[-5, -2, 0, 3]
k: -3
arr: #[1, 2, 3]
k: 5
expected: #[1, -1, 3, -1]
#[-1, 0, 1, 2]
#[100, 50, 100]
#[-5, -1, -1, -1]
#[1, 2, 3]
unexpected: #[1, 5, 3, 10]
#[1, -1, 3, 10]
#[0, 0, 1, 2]
#[-1, 0, 1, 1]
#[100, 50, -1]
#[100, 50, 50]
#[-5, -2, -1, -1]
#[-5, -1, 0, -1]
#[1, 3, 3]
#[1, 2, -1]

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that rearranges an array of integers by moving all zero values to the end of the array. The method should ensure that the relative order of the non-zero elements remains the same, the overall size of the array is unchanged, and the number of zeroes in the array stays constant.

-----Input-----
The input consists of:
arr: An array of integers.

-----Output-----
The output is an array of integers:
Returns an array where:
- The length is the same as that of the input array.
- All zero values are positioned at the end.
- The relative order of non-zero elements is preserved.
- The count of zero values remains the same as in the input array.

-----Note-----
There are no preconditions; the method will always work for any array of integers.
Difficulty: basic

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

@[reducible, simp]
def MoveZeroesToEnd_precond (arr : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def MoveZeroesToEnd (arr : Array Int) (h_precond : MoveZeroesToEnd_precond (arr)) : Array Int :=
  -- !benchmark @start code
  let nonZeros := arr.toList.filter (· ≠ 0)
  let zeros := arr.toList.filter (· = 0)
  Array.mk (nonZeros ++ zeros)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def MoveZeroesToEnd_postcond (arr : Array Int) (result: Array Int) (h_precond : MoveZeroesToEnd_precond (arr)) :=
  -- !benchmark @start postcond
  let firstResZeroIdx := result.toList.idxOf 0
  List.isPerm result.toList arr.toList ∧
  result.toList.take firstResZeroIdx = arr.toList.filter (· ≠ 0) ∧
  result.toList.drop firstResZeroIdx = arr.toList.filter (· = 0)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem MoveZeroesToEnd_spec_satisfied (arr: Array Int) (h_precond : MoveZeroesToEnd_precond (arr)) :
    MoveZeroesToEnd_postcond (arr) (MoveZeroesToEnd (arr) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: arr: #[0, 1, 0, 3, 12]
arr: #[0, 0, 1]
arr: #[1, 2, 3]
arr: #[0, 0, 0]
arr: #[]
expected: #[1, 3, 12, 0, 0]
#[1, 0, 0]
#[1, 2, 3]
#[0, 0, 0]
#[]
unexpected: #[0, 1, 0, 3, 12]
#[1, 0, 3, 12, 0]
#[0, 0, 1]
#[0, 1, 0]
#[1, 3, 2]
#[2, 1, 3]
#[1, 0, 0]
#[0, 1, 0]
#[0]
#[1]

Inputs rejected by the precondition:
-----Description-----  
This task requires swapping two 8-bit unsigned integers. Given two unsigned integer inputs, the goal is to produce an output pair where the first element is the original second input and the second element is the original first input. The problem focuses solely on exchanging the values without specifying any particular method to achieve the swap.

-----Input-----  
The input consists of:  
• X: A UInt8 value.  
• Y: A UInt8 value.

-----Output-----  
The output is a pair of UInt8 values (newX, newY) where:  
• newX is equal to the original Y.  
• newY is equal to the original X.

-----Note-----  
There are no additional preconditions; the function is meant to work correctly for any pair of UInt8 values by leveraging bitwise xor operations.
Difficulty: basic

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible, simp]
def SwapBitvectors_precond (X : UInt8) (Y : UInt8) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def SwapBitvectors (X : UInt8) (Y : UInt8) (h_precond : SwapBitvectors_precond (X) (Y)) : UInt8 × UInt8 :=
  -- !benchmark @start code
  let temp := X.xor Y
  let newY := temp.xor Y
  let newX := temp.xor newY
  (newX, newY)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def SwapBitvectors_postcond (X : UInt8) (Y : UInt8) (result: UInt8 × UInt8) (h_precond : SwapBitvectors_precond (X) (Y)) :=
  -- !benchmark @start postcond
  result.fst = Y ∧ result.snd = X ∧
  (X ≠ Y → result.fst ≠ X ∧ result.snd ≠ Y)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem SwapBitvectors_spec_satisfied (X: UInt8) (Y: UInt8) (h_precond : SwapBitvectors_precond (X) (Y)) :
    SwapBitvectors_postcond (X) (Y) (SwapBitvectors (X) (Y) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: X: 0
Y: 0
X: 5
Y: 10
X: 255
Y: 1
X: 128
Y: 64
X: 15
Y: 15
expected: (0, 0)
(10, 5)
(1, 255)
(64, 128)
(15, 15)
unexpected: (0, 1)
(1, 0)
(5, 10)
(10, 10)
(5, 5)
(255, 1)
(1, 254)
(0, 255)
(128, 64)
(64, 64)
(0, 128)
(15, 16)
(16, 15)
(14, 15)

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 function that converts a binary number represented as a list of digits (0 or 1) into its corresponding decimal value. The list is ordered in big-endian format, meaning the most significant digit comes first.
The function should interpret the list as a binary number and return its decimal representation as a natural number.

-----Input-----
The input is a list of natural numbers:
digits: A list of digits, each of which is either 0 or 1, representing a binary number in big-endian order.

-----Output-----
The output is a natural number:
Returns the decimal value of the binary number represented by the input list.


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def binaryToDecimal_precond (digits : List Nat) : Prop :=
  -- !benchmark @start precond
  digits.all (fun d => d = 0 ∨ d = 1)
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def binaryToDecimal (digits : List Nat) (h_precond : binaryToDecimal_precond (digits)) : Nat :=
  -- !benchmark @start code
  let rec helper (digits : List Nat) : Nat :=
    match digits with
    | [] => 0
    | first :: rest => first * Nat.pow 2 rest.length + helper rest
  helper digits
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def binaryToDecimal_postcond (digits : List Nat) (result: Nat) (h_precond : binaryToDecimal_precond (digits)) : Prop :=
  -- !benchmark @start postcond
  result - List.foldl (λ acc bit => acc * 2 + bit) 0 digits = 0 ∧
  List.foldl (λ acc bit => acc * 2 + bit) 0 digits - result = 0
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem binaryToDecimal_spec_satisfied (digits: List Nat) (h_precond : binaryToDecimal_precond (digits)) :
    binaryToDecimal_postcond (digits) (binaryToDecimal (digits) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: digits: [1, 0, 1]
digits: [1, 1, 1, 1]
digits: [0, 0, 0]
digits: [1, 0, 0, 0, 0]
digits: [1]
expected: 5
15
0
16
0
1
unexpected: 3
4
6
14
16
1
2
8
0
1
0

Inputs rejected by the precondition:
digits: [2]
-----Description-----
This task requires writing a Lean 4 function that finds the one missing number in a list of distinct natural numbers from 0 to n. The list contains exactly n numbers and all numbers are in the range [0, n], but one number in that range is missing.

Your function must return the missing number. You may assume the input list contains no duplicates and only one number is missing.

-----Input-----
- nums: A list of natural numbers of length n, each in the range [0, n] with exactly one number missing.

-----Output-----
- A natural number: the missing number in the range [0, n] not present in the list.


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def missingNumber_precond (nums : List Nat) : Prop :=
  -- !benchmark @start precond
  nums.all (fun x => x ≤ nums.length) ∧ List.Nodup nums
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def missingNumber (nums : List Nat) (h_precond : missingNumber_precond (nums)) : Nat :=
  -- !benchmark @start code
  let n := nums.length
  let expectedSum := (n * (n + 1)) / 2
  let actualSum := nums.foldl (· + ·) 0
  expectedSum - actualSum
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def missingNumber_postcond (nums : List Nat) (result: Nat) (h_precond : missingNumber_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  let n := nums.length
  (result ∈ List.range (n + 1)) ∧
  ¬(result ∈ nums) ∧
  ∀ x, (x ∈ List.range (n + 1)) → x ≠ result → x ∈ nums
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem missingNumber_spec_satisfied (nums: List Nat) (h_precond : missingNumber_precond (nums)) :
    missingNumber_postcond (nums) (missingNumber (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: nums: [3, 0, 1]
nums: [0, 1]
nums: [9, 6, 4, 2, 3, 5, 7, 0, 1]
nums: [0]
nums: [1]
expected: 2
2
8
1
0
unexpected: 0
1
3
0
1
1
9
0
1

Inputs rejected by the precondition:
nums: [0, 0, 1]
-----Description----- 
This task requires writing a Lean 4 method that identifies the dissimilar elements between two arrays of integers. In other words, the method should return an array containing all elements that appear in one input array but not in the other. The output array must contain no duplicate elements and the order of elements does not matter.

-----Input-----
The input consists of:
a: An array of integers.
b: An array of integers.

-----Output-----
The output is an array of integers:
Returns an array containing all distinct elements from both input arrays that are not present in the other array and should be sorted
Difficulty: basic

Lean 4 solution:
-- !benchmark @start import type=solution
import Std.Data.HashSet
-- !benchmark @end import

-- !benchmark @start solution_aux
def inArray (a : Array Int) (x : Int) : Bool :=
  a.any (fun y => y = x)
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

@[reducible, simp]
def dissimilarElements_precond (a : Array Int) (b : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
-- !benchmark @end code_aux


def dissimilarElements (a : Array Int) (b : Array Int) (h_precond : dissimilarElements_precond (a) (b)) : Array Int :=
  -- !benchmark @start code
  let res := a.foldl (fun acc x => if !inArray b x then acc.insert x else acc) Std.HashSet.empty
  let res := b.foldl (fun acc x => if !inArray a x then acc.insert x else acc) res
  res.toArray.insertionSort
  -- !benchmark @end code

-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def dissimilarElements_postcond (a : Array Int) (b : Array Int) (result: Array Int) (h_precond : dissimilarElements_precond (a) (b)) :=
  -- !benchmark @start postcond
  result.all (fun x => inArray a x ≠ inArray b x)∧
  result.toList.Pairwise (· ≤ ·) ∧
  a.all (fun x => if x ∈ b then x ∉ result else x ∈ result) ∧
  b.all (fun x => if x ∈ a then x ∉ result else x ∈ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem dissimilarElements_spec_satisfied (a: Array Int) (b: Array Int) (h_precond : dissimilarElements_precond (a) (b)) :
    dissimilarElements_postcond (a) (b) (dissimilarElements (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[1, 2, 3, 4]
b: #[3, 4, 5, 6]
a: #[1, 1, 2]
b: #[2, 3]
a: #[]
b: #[4, 5]
a: #[7, 8]
b: #[]
a: #[1, 2, 3]
b: #[1, 2, 3]
a: #[1, 2, 3]
b: #[4, 5, 6]
a: #[-1, 0, 1]
b: #[0]
expected: #[1, 2, 5, 6]
#[1, 3]
#[4, 5]
#[7, 8]
#[]
#[1, 2, 3, 4, 5, 6]
#[-1, 1]
unexpected: #[1,2,3,4,5,6]
#[3,4]
#[1,3,5]
#[1]
#[3]
#[1,2,3]
#[4]
#[5]
#[]
#[7]
#[8]
#[7, 8, 9]
#[1]
#[1,2]
#[1,2,3]
#[1,2,3,4]
#[4,5,6]
#[1,2,3]
#[0]
#[-1,0,1]
#[-1]

Inputs rejected by the precondition: