sunblaze-ucb/verina huggingface dataset:
-----Description-----
This task requires writing a Lean 4 function that finds the length of the longest sequence of consecutive integers present in a given list. The numbers do not need to appear in order. The elements are unique.

A consecutive sequence consists of integers that can be arranged in increasing order with no gaps. Your function should find the longest such streak.

-----Input-----
- nums: A list of integers (no duplicates).

-----Output-----
- A natural number: the length of the longest consecutive sequence.


Difficulty: advanced

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

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible, simp]
def longestConsecutive_precond (nums : List Int) : Prop :=
  -- !benchmark @start precond
  List.Nodup nums
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def longestConsecutive (nums : List Int) (h_precond : longestConsecutive_precond (nums)) : Nat :=
  -- !benchmark @start code
  Id.run do
    let mut set := HashSet.empty
    for x in nums do
      set := set.insert x

    let mut maxLen := 0

    for x in nums do
      if !set.contains (x - 1) then
        let mut curr := x
        let mut length := 1
        while set.contains (curr + 1) do
          curr := curr + 1
          length := length + 1
        maxLen := Nat.max maxLen length

    return maxLen
  -- !benchmark @end code


-- !benchmark @start postcond_aux
def isConsecutive (seq : List Int) : Bool :=
  seq.length = 0 ∨ seq.zipIdx.all (fun (x, i) => x = i + seq[0]!)
-- !benchmark @end postcond_aux


@[reducible, simp]
def longestConsecutive_postcond (nums : List Int) (result: Nat) (h_precond : longestConsecutive_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  let sorted_nums := nums.mergeSort
  let consec_sublist_lens := List.range nums.length |>.flatMap (fun start =>
    List.range (nums.length - start + 1) |>.map (fun len => sorted_nums.extract start (start + len))) |>.filter isConsecutive |>.map (·.length)

  (nums = [] → result = 0) ∧
  (nums ≠ [] → consec_sublist_lens.contains result ∧ consec_sublist_lens.all (· ≤ result))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem longestConsecutive_spec_satisfied (nums: List Int) (h_precond : longestConsecutive_precond (nums)) :
    longestConsecutive_postcond (nums) (longestConsecutive (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
nums: [1, 1]
-----Description-----
This task requires creating a function that determines the correct insertion index for a given integer in a sorted array. The goal is to identify an index where every number before it is less than the specified value, and every number from that index onward is greater than or equal to the value. If the given integer is larger than all elements in the array, the function should return the array’s size.

-----Input-----
The input consists of:
• a: An array of integers that is assumed to be sorted in non-decreasing order.
• key: An integer to search for in the array.

-----Output-----
The output is a natural number (Nat) representing the index determined by the binary search. The index satisfies the following postconditions:
• It is between 0 and the size of the array.
• Every element before the returned index is less than the key.
• If the returned index equals the size of the array, then all elements are less than the key.
• Every element from the index onwards is greater than or equal to the key.

-----Note-----
It is assumed that the input array is sorted in non-decreasing order. The function returns the first index where the key could be inserted while maintaining the sorted order.
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 BinarySearch_precond (a : Array Int) (key : Int) : Prop :=
  -- !benchmark @start precond
  List.Pairwise (· ≤ ·) a.toList
  -- !benchmark @end precond


-- !benchmark @start code_aux
def binarySearchLoop (a : Array Int) (key : Int) (lo hi : Nat) : Nat :=
  if lo < hi then
    let mid := (lo + hi) / 2
    if (a[mid]! < key) then binarySearchLoop a key (mid + 1) hi
    else binarySearchLoop a key lo mid
  else
    lo
-- !benchmark @end code_aux


def BinarySearch (a : Array Int) (key : Int) (h_precond : BinarySearch_precond (a) (key)) : Nat :=
  -- !benchmark @start code
  binarySearchLoop a key 0 a.size
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def BinarySearch_postcond (a : Array Int) (key : Int) (result: Nat) (h_precond : BinarySearch_precond (a) (key)) :=
  -- !benchmark @start postcond
  result ≤ a.size ∧
  ((a.take result).all (fun x => x < key)) ∧
  ((a.drop result).all (fun x => x ≥ key))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem BinarySearch_spec_satisfied (a: Array Int) (key: Int) (h_precond : BinarySearch_precond (a) (key)) :
    BinarySearch_postcond (a) (key) (BinarySearch (a) (key) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
a: #[3, 2, 1]
key: 2
-----Description----- 
This task requires writing a Lean 4 method that transforms an array of integers by replacing every element with its cube. In other words, for each element in the input array, the output array should contain the result of multiplying that element by itself three times.

-----Input-----
The input consists of:
a: An array of integers (which may be empty or non-empty).

-----Output-----
The output is an array of integers:
Returns an array with the same length as the input, where each element is the cube of the corresponding element in the input array.

-----Note-----
There are no additional preconditions; the method should work correctly 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 cubeElements_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def cubeElements (a : Array Int) (h_precond : cubeElements_precond (a)) : Array Int :=
  -- !benchmark @start code
  a.map (fun x => x * x * x)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def cubeElements_postcond (a : Array Int) (result: Array Int) (h_precond : cubeElements_precond (a)) :=
  -- !benchmark @start postcond
  (result.size = a.size) ∧
  (∀ i, i < a.size → result[i]! = a[i]! * a[i]! * a[i]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem cubeElements_spec_satisfied (a: Array Int) (h_precond : cubeElements_precond (a)) :
    cubeElements_postcond (a) (cubeElements (a) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold cubeElements cubeElements_postcond
  simp_all
  intro i hi
  have h_maplen : (Array.map (fun x => x * x * x) a).size = a.size := by
    apply Array.size_map
  have h1 : (Array.map (fun x => x * x * x) a)[i] = (fun x => x * x * x) a[i] := by
    apply Array.getElem_map
  have h_eq : (Array.map (fun x => x * x * x) a)[i] = (Array.map (fun x => x * x * x) a)[i]! := by
    have hi' : i < (Array.map (fun x => x * x * x) a).size := by
      simp only [hi, h_maplen]
    rw [Array.getElem!_eq_getD]
    simp [hi', hi]
  rw [← h_eq]
  simp only [h1]
  have h_eq' : a[i] = a[i]! := by
    have hi_a : i < a.size := by
      simp only [hi]
    rw [Array.getElem!_eq_getD]
    simp [hi_a]
  simp only [h_eq']
  -- !benchmark @end proof


Tests:
input: a: #[1, 2, 3, 4]
a: #[0, -1, -2, 3]
a: #[]
a: #[5]
a: #[-3, -3]
expected: #[1, 8, 27, 64]
#[0, -1, -8, 27]
#[]
#[125]
#[-27, -27]
unexpected: #[1, 4, 9, 16]
#[1, 8, 27, 63]
#[0, 0, 0, 0]
#[0, 1, 8, -27]
#[0, -1, -8, 26]
#[1, -1, -8, 27]
#[1]
#[-1]
#[0]
#[5]
#[25]
#[0]
#[27, 27]
#[-9, -9]
#[-27, 27]

Inputs rejected by the precondition:
-----Description-----  
This problem requires sorting an array of integers into non-decreasing order, ensuring that the output contains exactly the same elements as the input (i.e., it is a permutation of the original array).

-----Input-----  
The input consists of:  
• a: An array of integers (Array Int).  

-----Output-----  
The output is an array of integers that is:  
• Sorted in non-decreasing order.  
• A permutation of the input, meaning it contains exactly the same elements (with the same multiplicities) as the original array.  

-----Note-----  
It is assumed that the input array is valid and that the swap operations, along with the helper functions, correctly implement the selection sort algorithm.
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 SelectionSort_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def findMinIndexInRange (arr : Array Int) (start finish : Nat) : Nat :=
  let indices := List.range (finish - start)
  indices.foldl (fun minIdx i =>
    let currIdx := start + i
    if arr[currIdx]! < arr[minIdx]! then currIdx else minIdx
  ) start

def swap (a : Array Int) (i j : Nat) : Array Int :=
  if i < a.size && j < a.size && i ≠ j then
    let temp := a[i]!
    let a' := a.set! i a[j]!
    a'.set! j temp
  else a
-- !benchmark @end code_aux


def SelectionSort (a : Array Int) (h_precond : SelectionSort_precond (a)) : Array Int :=
  -- !benchmark @start code
  let indices := List.range a.size
  indices.foldl (fun arr i =>
    let minIdx := findMinIndexInRange arr i a.size
    swap arr i minIdx
  ) a
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def SelectionSort_postcond (a : Array Int) (result: Array Int) (h_precond : SelectionSort_precond (a)) :=
  -- !benchmark @start postcond
  List.Pairwise (· ≤ ·) result.toList ∧ List.isPerm a.toList result.toList
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem SelectionSort_spec_satisfied (a: Array Int) (h_precond : SelectionSort_precond (a)) :
    SelectionSort_postcond (a) (SelectionSort (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[3, 1, 2]
a: #[0]
a: #[5, 4, 3, 2, 1]
a: #[2, 2, 1, 4]
a: #[10, -5, 0, 3]
expected: #[1, 2, 3]
#[0]
#[1, 2, 3, 4, 5]
#[1, 2, 2, 4]
#[-5, 0, 3, 10]
unexpected: #[3, 1, 2]
#[2, 3, 1]
#[0, 0]
#[1]
#[5, 4, 3, 2, 1]
#[1, 5, 4, 3, 2]
#[1, 2, 4, 3, 5]
#[2, 1, 2, 4]
#[1, 2, 4, 2]
#[10, -5, 3, 0]
#[0, -5, 3, 10]
#[3, -5, 10, 0]

Inputs rejected by the precondition:
-----Description-----  
This task involves concatenating two arrays of integers by appending the second array to the end of the first array. The goal is to produce a new array that sequentially contains all elements from the first array followed by all elements from the second array.

-----Input-----  
The input consists of two parameters:  
• a: An Array of integers representing the first part of the concatenated array.  
• b: An Array of integers representing the second part of the concatenated array.

-----Output-----  
The output is an Array of integers that satisfies the following:  
• The length of the output array is equal to the sum of the lengths of arrays a and b.  
• The first part of the output array (indices 0 to a.size - 1) is identical to array a.  
• The remaining part of the output array (indices a.size to a.size + b.size - 1) is identical to array b.

-----Note-----  
No additional preconditions are required since the function uses the sizes of the input arrays to build the resulting array.
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 concat_precond (a : Array Int) (b : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def concat (a : Array Int) (b : Array Int) (h_precond : concat_precond (a) (b)) : Array Int :=
  -- !benchmark @start code
  let n := a.size + b.size
  let rec loop (i : Nat) (c : Array Int) : Array Int :=
    if i < n then
      let value := if i < a.size then a[i]! else b[i - a.size]!
      loop (i + 1) (c.set! i value)
    else
      c
  loop 0 (Array.mkArray n 0)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def concat_postcond (a : Array Int) (b : Array Int) (result: Array Int) (h_precond : concat_precond (a) (b)) :=
  -- !benchmark @start postcond
  result.size = a.size + b.size
    ∧ (∀ k, k < a.size → result[k]! = a[k]!)
    ∧ (∀ k, k < b.size → result[k + a.size]! = b[k]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem concat_spec_satisfied (a: Array Int) (b: Array Int) (h_precond : concat_precond (a) (b)) :
    concat_postcond (a) (b) (concat (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
------Description-----
This task requires writing a Lean 4 method that given a 0-indexed integer array `nums` representing the scores of students in an exam. A teacher wants to select a non empty group of students such that the strength of group is maximized. 

The strength of a group is defined as the product of the selected student scores.

You can choose any non-empty subset of students. The goal is to compute the maximum product of any such subset. 


----Input---
nums: An non-empty list of integers.

-----Output-----

An integer representing the maximum strength.


Difficulty: advanced

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]
def maxStrength_precond (nums : List Int) : Prop :=
  -- !benchmark @start precond
  nums ≠ []
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def maxStrength (nums : List Int) (h_precond : maxStrength_precond (nums)) : Int :=
  -- !benchmark @start code
  let powerSet := fun (l : List Int) =>
    let n := l.length
    let masks := List.range (2^n)
    masks.map fun mask =>
      (List.range n).foldr (fun i acc =>
        if (mask.shiftRight i).land 1 == 1 then l[i]! :: acc else acc
      ) []

  let subsets := powerSet nums
  let nonEmpty := subsets.filter (· ≠ [])
  let products := List.map (fun subset =>
    List.foldl (fun acc x =>
      acc * x) (1 : Int) subset)
    nonEmpty
  (List.max? products).getD (-1000000)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def maxStrength_postcond (nums : List Int) (result: Int) (h_precond : maxStrength_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  let sublists := nums.sublists.filter (· ≠ [])
  let products := sublists.map (List.foldl (· * ·) 1)
  products.contains result ∧ products.all (· ≤ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem maxStrength_spec_satisfied (nums: List Int) (h_precond : maxStrength_precond (nums)) :
    maxStrength_postcond (nums) (maxStrength (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: nums: [-2]
nums: [3, -1, -5, 2, 5, -9]
nums: [-4, -5, -4]
nums: [0, -3, 4]
nums: [1, -1, -1]
expected: -2
1350
20
4
1
unexpected: 2
0
270
0
-1
80
-80
-5
0
-12
-1
-2

Inputs rejected by the precondition:
-----Description-----
This task involves computing the element-wise product of two integer arrays. For each position in the arrays, the corresponding numbers are multiplied together. If an element is missing in one of the arrays at a given index, the missing value is treated as 0. When both arrays provide values for every index, the resulting array will contain the product of the two numbers at each corresponding index.

-----Input-----
The input consists of two arrays:
• a: An array of integers.
• b: An array of integers (should be of equal length to a for the specification to hold).

-----Output-----
The output is an array of integers that:
• Has the same length as the input arrays.
• For each index i, the output array contains the product a[i] * b[i].
• In cases where one of the arrays might be shorter, missing elements default to 0 during multiplication.

-----Note-----
It is assumed that the arrays are of equal length for the theorem specification, although the implementation defaults missing indices to 0.
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 arrayProduct_precond (a : Array Int) (b : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size = b.size
  -- !benchmark @end precond


-- !benchmark @start code_aux
def loop (a b : Array Int) (len : Nat) : Nat → Array Int → Array Int
  | i, c =>
    if i < len then
      let a_val := if i < a.size then a[i]! else 0
      let b_val := if i < b.size then b[i]! else 0
      let new_c := Array.set! c i (a_val * b_val)
      loop a b len (i+1) new_c
    else c
-- !benchmark @end code_aux


def arrayProduct (a : Array Int) (b : Array Int) (h_precond : arrayProduct_precond (a) (b)) : Array Int :=
  -- !benchmark @start code
  let len := a.size
  let c := Array.mkArray len 0
  loop a b len 0 c
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def arrayProduct_postcond (a : Array Int) (b : Array Int) (result: Array Int) (h_precond : arrayProduct_precond (a) (b)) :=
  -- !benchmark @start postcond
  (result.size = a.size) ∧ (∀ i, i < a.size → a[i]! * b[i]! = result[i]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem arrayProduct_spec_satisfied (a: Array Int) (b: Array Int) (h_precond : arrayProduct_precond (a) (b)) :
    arrayProduct_postcond (a) (b) (arrayProduct (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[1, 2, 3]
b: #[4, 5, 6]
a: #[0, 0, 0]
b: #[1, 2, 3]
a: #[-1, 2, -3]
b: #[3, -4, 5]
a: #[2]
b: #[10]
a: #[1, 2, 3, 4]
b: #[2, 2, 2, 2]
expected: #[4, 10, 18]
#[0, 0, 0]
#[-3, -8, -15]
#[20]
#[2, 4, 6, 8]
unexpected: #[4, 10, 17]
#[0, 10, 18]
#[4, 10, 20]
#[1, 0, 0]
#[0, 1, 0]
#[0, 0, 1]
#[-3, -8, -14]
#[-3, -7, -15]
#[-2, -8, -15]
#[10]
#[0]
#[30]
#[2, 4, 6, 9]
#[1, 4, 6, 8]
#[2, 5, 6, 8]

Inputs rejected by the precondition:
a: #[1, 2, 3]
b: #[4, 5]
-----Description-----  
This task requires writing a Lean 4 method that counts the number of digit characters within a given string. A digit is any character between '0' and '9'. The method should determine how many such digit characters appear in the input.

-----Input-----  
The input consists of:  
s: A string.

-----Output-----  
The output is a natural number (Nat):  
Returns a non-negative count representing the number of digit characters found in the input string.

-----Note-----  
There are no additional preconditions; the method works for any provided string.
Difficulty: basic

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def isDigit (c : Char) : Bool :=
  '0' ≤ c ∧ c ≤ '9'
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

@[reducible, simp]
def countDigits_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def countDigits (s : String) (h_precond : countDigits_precond (s)) : Nat :=
  -- !benchmark @start code
  List.length (List.filter isDigit s.toList)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def countDigits_postcond (s : String) (result: Nat) (h_precond : countDigits_precond (s)) :=
  -- !benchmark @start postcond
  result - List.length (List.filter isDigit s.toList) = 0 ∧
  List.length (List.filter isDigit s.toList) - result = 0
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem countDigits_spec_satisfied (s: String) (h_precond : countDigits_precond (s)) :
    countDigits_postcond (s) (countDigits (s) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold countDigits countDigits_postcond
  simp
  -- !benchmark @end proof


Tests:
input: s: 123abc456
s: no digits here!
s: 1234567890
s: a1b2c3
s: 0
s: abc
expected: 6
0
10
0
3
1
0
unexpected: 5
7
0
1
2
3
9
11
0
1
2
10
2
4
5
0
2
10
1
8
9

Inputs rejected by the precondition: