sunblaze-ucb/verina huggingface dataset:
-----Description-----
This task requires implementing the "Longest Increasing Subsequence" problem in Lean 4.
Given a list of integers, the function should compute the length of the longest strictly increasing
subsequence. A subsequence is formed by deleting zero or more elements without changing the order.
If the list is empty, the function should return 0.

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

-----Output-----
- A natural number representing the length of the longest strictly increasing subsequence.
- If there is no increasing subsequence, return 0.


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution
import Mathlib.Data.List.Basic
-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def longestIncreasingSubsequence (nums : List Int) (h_precond : longestIncreasingSubsequence_precond (nums)) : Nat :=
  -- !benchmark @start code
  let max2 (a : Nat) (b : Nat) : Nat :=
    if a > b then a else b

  let rec listLength (l : List Int) : Nat :=
    match l with
    | []      => 0
    | _ :: xs => 1 + listLength xs

  let rec helper (lst : List Int) (prev : Option Int) : Nat :=
    match lst with
    | [] => 0
    | h :: t =>
        let canTake : Bool :=
          if prev = none then true
          else if prev.get! < h then true else false
        let withTake : Nat :=
          if canTake then 1 + helper t (some h) else 0
        let withoutTake : Nat := helper t prev
        max2 withTake withoutTake

  let result := helper nums none
  result
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def longestIncreasingSubsequence_postcond (nums : List Int) (result: Nat) (h_precond : longestIncreasingSubsequence_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  let allSubseq := (nums.foldl fun acc x => acc ++ acc.map (fun sub => x :: sub)) [[]] |>.map List.reverse
  let increasingSubseqLens := allSubseq.filter (fun l => List.Pairwise (· < ·) l) |>.map (·.length)
  increasingSubseqLens.contains result ∧ increasingSubseqLens.all (· ≤ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem longestIncreasingSubsequence_spec_satisfied (nums: List Int) (h_precond : longestIncreasingSubsequence_precond (nums)) :
    longestIncreasingSubsequence_postcond (nums) (longestIncreasingSubsequence (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
-----Description-----  
Given an integer x, determine a pair (a, b) where the first element is twice the value of x and the second element is four times the value of x.

-----Input-----  
The input consists of:  
• x: An integer.

-----Output-----  
The output is a tuple (a, b) where:  
• a = 2 * x  
• b = 4 * x

-----Note-----  
There are no additional preconditions; the method is defined for all 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 DoubleQuadruple_precond (x : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def DoubleQuadruple (x : Int) (h_precond : DoubleQuadruple_precond (x)) : (Int × Int) :=
  -- !benchmark @start code
  let a := 2 * x
  let b := 2 * a
  (a, b)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def DoubleQuadruple_postcond (x : Int) (result: (Int × Int)) (h_precond : DoubleQuadruple_precond (x)) :=
  -- !benchmark @start postcond
  result.fst = 2 * x ∧ result.snd = 2 * result.fst
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem DoubleQuadruple_spec_satisfied (x: Int) (h_precond : DoubleQuadruple_precond (x)) :
    DoubleQuadruple_postcond (x) (DoubleQuadruple (x) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: x: 0
x: 1
x: -1
x: 10
x: -5
expected: (0, 0)
(2, 4)
(-2, -4)
(20, 40)
(-10, -20)
unexpected: (1, 0)
(0, 1)
(-1, 0)
(2, 2)
(1, 4)
(3, 4)
(-2, -2)
(-1, -4)
(-3, -4)
(20, 20)
(10, 40)
(20, 0)
(-10, -10)
(-5, -20)
(-15, -20)

Inputs rejected by the precondition:
-----Description-----  
This task requires writing a function that processes an array of integers and produces a new array containing only the even numbers from the input. The order of these even numbers should remain the same as in the original array, ensuring that every even number from the input appears in the output and that every element in the output is even.

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

-----Output-----  
The output is an array of integers that:  
• Contains exactly all even numbers from the input array, preserving their original order.  
• Meets the specified conditions that ensure no extraneous (odd or non-existing) elements are returned.

-----Note-----  
There are no additional preconditions. The function must adhere to the provided specification which enforces evenness and order preservation for the elements in the output array.
Difficulty: basic

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def isEven (n : Int) : Bool :=
  n % 2 = 0
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def FindEvenNumbers (arr : Array Int) (h_precond : FindEvenNumbers_precond (arr)) : Array Int :=
  -- !benchmark @start code
  let rec loop (i : Nat) (acc : Array Int) : Array Int :=
    if i < arr.size then
      if isEven (arr.getD i 0) then
        loop (i + 1) (acc.push (arr.getD i 0))
      else
        loop (i + 1) acc
    else
      acc
  loop 0 (Array.mkEmpty 0)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def FindEvenNumbers_postcond (arr : Array Int) (result: Array Int) (h_precond : FindEvenNumbers_precond (arr)) :=
  -- !benchmark @start postcond
  result.all (fun x => isEven x) ∧
  result.toList.Sublist arr.toList ∧
  result.size = arr.toList.countP isEven
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem FindEvenNumbers_spec_satisfied (arr: Array Int) (h_precond : FindEvenNumbers_precond (arr)) :
    FindEvenNumbers_postcond (arr) (FindEvenNumbers (arr) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 method that determines if a given string is a palindrome, ignoring all
non-alphanumeric characters and case differences. For example, the string "A man, a plan, a canal: Panama" should return
true.

-----Input-----
A single string:
s: The string to check for palindrome property.

-----Output-----
A boolean (Bool):
true if s is a palindrome when ignoring non-alphanumeric characters and case. false otherwise.


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 palindromeIgnoreNonAlnum_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def palindromeIgnoreNonAlnum (s : String) (h_precond : palindromeIgnoreNonAlnum_precond (s)) : Bool :=
  -- !benchmark @start code
  let cleaned : List Char :=
    s.data.filter (fun c => c.isAlpha || c.isDigit)
      |>.map Char.toLower

  let n := cleaned.length
  let startIndex := 0
  let endIndex := if n = 0 then 0 else n - 1

  let rec check (l r : Nat) : Bool :=
    if l >= r then
      true
    else if cleaned[l]? = cleaned[r]? then
      check (l + 1) (r - 1)
    else
      false

  check startIndex endIndex
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def palindromeIgnoreNonAlnum_postcond (s : String) (result: Bool) (h_precond : palindromeIgnoreNonAlnum_precond (s)) : Prop :=
  -- !benchmark @start postcond
  let cleaned := s.data.filter (fun c => c.isAlpha || c.isDigit) |>.map Char.toLower
let forward := cleaned
let backward := cleaned.reverse

if result then
  forward = backward
else
  forward ≠ backward
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem palindromeIgnoreNonAlnum_spec_satisfied (s: String) (h_precond : palindromeIgnoreNonAlnum_precond (s)) :
    palindromeIgnoreNonAlnum_postcond (s) (palindromeIgnoreNonAlnum (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: s: A man, a plan, a canal: Panama
s: race a car
s: No 'x' in Nixon
s: abc!!cba?
s: Hello, world!
expected: True
True
False
True
True
False
unexpected: False
False
True
False
False
True

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 method that determines the length of the longest strictly increasing subsequence in a given array of integers.

A subsequence is a sequence that can be derived from the array by deleting some or no elements without changing the order of the remaining elements. The subsequence must be strictly increasing, meaning each element must be greater than the one before it.

The goal is to find the length of the longest such subsequence that can be formed from the input array.

-----Input-----
The input consists of one array:

nums: An array of integers where nums[i] represents the ith element of the input sequence.

-----Output-----
The output is an integer:
Returns the length of the longest strictly increasing subsequence in the input array.


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 lengthOfLIS_precond (nums : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def lengthOfLIS (nums : List Int) (h_precond : lengthOfLIS_precond (nums)) : Int :=
  -- !benchmark @start code
  let rec lisHelper (dp : List Int) (x : Int) : List Int :=
    let rec replace (l : List Int) (acc : List Int) : List Int :=
      match l with
      | [] => (acc.reverse ++ [x])
      | y :: ys => if x ≤ y then acc.reverse ++ (x :: ys) else replace ys (y :: acc)
    replace dp []

  let finalDP := nums.foldl lisHelper []
  finalDP.length
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def lengthOfLIS_postcond (nums : List Int) (result: Int) (h_precond : lengthOfLIS_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  -- Helper function to check strictly increasing
  let rec isStrictlyIncreasing (l : List Int) : Bool :=
    match l with
    | [] | [_] => true
    | x :: y :: rest => x < y && isStrictlyIncreasing (y :: rest)

  -- Generate all subsequences
  let rec subsequences (xs : List Int) : List (List Int) :=
    match xs with
    | [] => [[]]
    | x :: xs' =>
      let rest := subsequences xs'
      rest ++ rest.map (fun r => x :: r)

  let allIncreasing := subsequences nums |>.filter (fun l => isStrictlyIncreasing l)

  allIncreasing.any (fun l => l.length = result) ∧
  allIncreasing.all (fun l => l.length ≤ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem lengthOfLIS_spec_satisfied (nums: List Int) (h_precond : lengthOfLIS_precond (nums)) :
    lengthOfLIS_postcond (nums) (lengthOfLIS (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
-----Description-----
Given a sorted list of distinct integers and a target value, return the index if the target is found. If it is not found, return the index where it would be inserted to maintain the sorted order.

This function must preserve the sorted property of the list. The list is assumed to be strictly increasing and contain no duplicates.

-----Input-----
xs : List Int — a sorted list of distinct integers in increasing order
target : Int — the integer to search for

-----Output-----
A natural number (Nat) representing the index at which the target is found, or the index at which it should be inserted to maintain sorted order.


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 searchInsert_precond (xs : List Int) (target : Int) : Prop :=
  -- !benchmark @start precond
  List.Pairwise (· < ·) xs
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def searchInsert (xs : List Int) (target : Int) (h_precond : searchInsert_precond (xs) (target)) : Nat :=
  -- !benchmark @start code
  match xs with
  | [] =>
      0
  | _ :: _ =>
      let rec helper : List Int → Nat → Nat :=
        fun ys idx =>
          match ys with
          | [] =>
              idx
          | y :: ys' =>
              let isCurrent := y
              let currentIndex := idx
              let targetValue := target
              let condition := targetValue ≤ isCurrent
              if condition then
                currentIndex
              else
                let incrementedIndex := currentIndex + 1
                let rest := ys'
                helper rest incrementedIndex
      let startingIndex := 0
      let result := helper xs startingIndex
      result
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def searchInsert_postcond (xs : List Int) (target : Int) (result: Nat) (h_precond : searchInsert_precond (xs) (target)) : Prop :=
  -- !benchmark @start postcond
  let allBeforeLess := (List.range result).all (fun i => xs[i]! < target)
  let inBounds := result ≤ xs.length
  let insertedCorrectly :=
    result < xs.length → target ≤ xs[result]!
  inBounds ∧ allBeforeLess ∧ insertedCorrectly
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem searchInsert_spec_satisfied (xs: List Int) (target: Int) (h_precond : searchInsert_precond (xs) (target)) :
    searchInsert_postcond (xs) (target) (searchInsert (xs) (target) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: xs: [1, 3, 5, 6]
target: 5
xs: [1, 3, 5, 6]
target: 2
xs: [1, 3, 5, 6]
target: 7
xs: [1, 3, 5, 6]
target: 0
target: 3
xs: [10]
target: 5
xs: [10]
target: 15
expected: 2
1
4
0
0
0
1
unexpected: 0
1
3
4
0
2
3
2
3
1
2
1
1
0

Inputs rejected by the precondition:
xs: [2, 1]
target: 5
xs: [1, 1]
target: 2
-----Description----- 
This task requires writing a Lean 4 method that finds the length of the logest common subsequence of two input arrays.

-----Input-----
The input consists of two arrays:
a: The first array.
b: The second array.


-----Output-----
The output is an integer:
Returns the length of array a and b's longest common subsequence.
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 LongestCommonSubsequence_precond (a : Array Int) (b : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def intMax (x y : Int) : Int :=
  if x < y then y else x
-- !benchmark @end code_aux


def LongestCommonSubsequence (a : Array Int) (b : Array Int) (h_precond : LongestCommonSubsequence_precond (a) (b)) : Int :=
  -- !benchmark @start code
  let m := a.size
  let n := b.size

  let dp := Id.run do
    let mut dp := Array.mkArray (m + 1) (Array.mkArray (n + 1) 0)
    for i in List.range (m + 1) do
      for j in List.range (n + 1) do
        if i = 0 ∨ j = 0 then
          ()
        else if a[i - 1]! = b[j - 1]! then
          let newVal := ((dp[i - 1]!)[j - 1]!) + 1
          dp := dp.set! i (dp[i]!.set! j newVal)
        else
          let newVal := intMax ((dp[i - 1]!)[j]!) ((dp[i]!)[j - 1]!)
          dp := dp.set! i (dp[i]!.set! j newVal)
    return dp
  (dp[m]!)[n]!
  -- !benchmark @end code


-- !benchmark @start postcond_aux
-- !benchmark @end postcond_aux


@[reducible, simp]
def LongestCommonSubsequence_postcond (a : Array Int) (b : Array Int) (result: Int) (h_precond : LongestCommonSubsequence_precond (a) (b)) : Prop :=
  -- !benchmark @start postcond
  let allSubseq (arr : Array Int) := (arr.foldl fun acc x => acc ++ acc.map (fun sub => x :: sub)) [[]] |>.map List.reverse
  let subseqA := allSubseq a
  let subseqB := allSubseq b
  let commonSubseqLens := subseqA.filter (fun l => subseqB.contains l) |>.map (·.length)
  commonSubseqLens.contains result ∧ commonSubseqLens.all (· ≤ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem LongestCommonSubsequence_spec_satisfied (a: Array Int) (b: Array Int) (h_precond : LongestCommonSubsequence_precond (a) (b)) :
    LongestCommonSubsequence_postcond (a) (b) (LongestCommonSubsequence (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
-----Description-----
Given a non-empty sequence of n integers, your task is to find the largest sum obtainable by choosing a contiguous subarray of the sequence. At least one number must be selected.

The algorithm uses dynamic programming (Kadane's Algorithm) to solve the problem:
1. Initialize the current maximum (cur) and the overall maximum (maxSoFar) with the first element.
2. For each subsequent element, update:
     cur = max(element, cur + element)
     maxSoFar = max(maxSoFar, cur)
3. Return maxSoFar as the answer.

-----Input-----
The input is provided as a list of integers:
  sequence: A non-empty list of n integers (n >= 1).

-----Output-----
The output is a single integer representing the maximum subarray sum.


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 task_code_precond (sequence : List Int) : Prop :=
  -- !benchmark @start precond
  sequence.length > 0  -- At least one element must be selected
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def task_code (sequence : List Int) (h_precond : task_code_precond (sequence)) : Int :=
  -- !benchmark @start code
  match sequence with
  | []      => 0  -- If no elements are provided (should not happen according to the problem)
  | x :: xs =>
      let (_, maxSoFar) :=
        xs.foldl (fun (acc : Int × Int) (x : Int) =>
          let (cur, maxSoFar) := acc
          let newCur := if cur + x >= x then cur + x else x
          let newMax := if maxSoFar >= newCur then maxSoFar else newCur
          (newCur, newMax)
        ) (x, x)
      maxSoFar
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def task_code_postcond (sequence : List Int) (result: Int) (h_precond : task_code_precond (sequence)) : Prop :=
  -- !benchmark @start postcond
  let subArrays :=
    List.range (sequence.length + 1) |>.flatMap (fun start =>
      List.range (sequence.length - start + 1) |>.map (fun len =>
        sequence.drop start |>.take len))
  let subArraySums := subArrays.filter (· ≠ []) |>.map (·.sum)
  subArraySums.contains result ∧ subArraySums.all (· ≤ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem task_code_spec_satisfied (sequence: List Int) (h_precond : task_code_precond (sequence)) :
    task_code_postcond (sequence) (task_code (sequence) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: sequence: [10, -4, 3, 1, 5, 6, -35, 12, 21, -1]
sequence: [2, 1, -4, 3, 4, -4, 6, 5, -5, 1]
sequence: [-1, -2, -3, -4, -5]
sequence: [7]
sequence: [1, 2, 3, 4, 5]
expected: 33
14
-1
7
15
unexpected: 32
34
0
13
15
0
-2
0
1
0
1
-7
14
16
0

Inputs rejected by the precondition:
{'sequence': []}