Sudoku

In this notebook we're going to use Imandra to reason about the classic kind of puzzle that you can find everywhere.

(note: this example was adapted from code from Koen Claessen and Dan Rosén)

We're going to define what a sudoku puzzle is, and how to check if a given sudoku is a solution. From that we can get Imandra to find solutions for us, without actually writing a sudoku solver.

Helpers

We're going to define a sudoku as a 9×9 grid.

Numbers

However, for now, the bounded model checker that comes along with Imandra doesn't handle numbers. We do not need much here besides length, so a unary notation (classic Peano arithmetic) will do.

In [1]:
type nat = Z | S of nat;;

(* readability matters, so we write a pretty-printer for nats *)
let rec int_of_nat = function Z -> 0i | S n -> Caml.Int.(1i + int_of_nat n) [@@program]
let pp_nat out n = Format.fprintf out "%d" (int_of_nat n) [@@program];;
#install_printer pp_nat;;
Out[1]:
type nat = Z | S of nat
val int_of_nat : nat -> int = <fun>
val pp_nat : Format.formatter -> nat -> unit = <fun>
In [2]:
let rec length = function
  | [] -> Z
  | _ :: tl -> S (length tl)

let n3 = S (S (S Z));;
let n6 = S (S (S n3));;
let n9 = S (S (S n6));;
Out[2]:
val length : 'a list -> nat = <fun>
val n3 : nat = 3
val n6 : nat = 6
val n9 : nat = 9
termination proof

Termination proof

call `length (List.tl _x)` from `length _x`
original:length _x
sub:length (List.tl _x)
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl _x))
path:[_x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.013s
details:
Expand
smt_stats:
num checks:8
arith assert lower:5
arith tableau max rows:4
arith tableau max columns:11
arith pivots:4
rlimit count:1806
mk clause:12
datatype occurs check:12
mk bool var:52
arith assert upper:5
datatype splits:1
decisions:10
arith row summations:7
propagations:12
conflicts:7
arith fixed eqs:4
datatype accessor ax:10
arith conflicts:1
arith num rows:4
datatype constructor ax:8
num allocs:5515574
final checks:4
added eqs:37
del clause:4
arith eq adapter:5
memory:15.370000
max memory:15.370000
Expand
  • start[0.013s]
      let (_x_0 : int) = count.list (const 0) _x in
      let (_x_1 : ty_0 list) = List.tl _x in
      let (_x_2 : int) = count.list (const 0) _x_1 in
      _x <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
      ==> not (_x_1 <> [])
          || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into:
    let (_x_0 : ty_0 list) = List.tl _x in
    let (_x_1 : int) = count.list (const 0) _x_0 in
    let (_x_2 : int) = count.list (const 0) _x in
    not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
    || not (_x <> [] && (_x_2 >= 0) && (_x_1 >= 0))
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • unroll
        expr:
        (|Ordinal.<<| (|Ordinal.Int_79/boot|
                        (|count.list_394/server| (|get.::.1_377/server|…
        expansions:
        • unroll
          expr:
          (|count.list_394/server| (|get.::.1_377/server| _x_383/server))
          expansions:
          • unroll
            expr:
            (|count.list_394/server| _x_383/server)
            expansions:
            • Unsat

            Rows, columns, blocks

            Sudokus have some constraints that work on rows, and some that work on columns. Using a transpose function we can always work on rows.

            In [3]:
            (** helper for {!transpose} *)
            let rec transpose3 = function
              | [] -> []
              | [] :: tl -> transpose3 tl
              | (_::t) :: tl -> t :: transpose3 tl
            
            let rec get_heads = function
              | [] -> []
              | [] :: tl -> get_heads tl
              | (h :: _) :: tl -> h :: get_heads tl
            ;;
            
            (** We need a custom termination function here *)
            let measure_transpose = function
            | [] -> 0
            | x :: _ -> List.length x
            ;;
            
            (** Transpose rows and columns in a list of lists *)
            let rec transpose l =
              match l with
              | [] -> []
              | [] :: _ -> []
              | (x1 :: xs) :: xss ->
                (x1 :: get_heads xss) :: transpose (xs :: transpose3 xss)
            [@@measure Ordinal.of_int (measure_transpose l)]
            ;;
            
            Out[3]:
            val transpose3 : 'a list list -> 'a list list = <fun>
            val get_heads : 'a list list -> 'a list = <fun>
            val measure_transpose : 'a list list -> Z.t = <fun>
            val transpose : 'a list list -> 'a list list = <fun>
            
            termination proof

            Termination proof

            call `transpose3 (List.tl _x)` from `transpose3 _x`
            original:transpose3 _x
            sub:transpose3 (List.tl _x)
            original ordinal:Ordinal.Int (_cnt _x)
            sub ordinal:Ordinal.Int (_cnt (List.tl _x))
            path:[(List.hd _x) <> [] && _x <> []]
            proof:
            detailed proof
            ground_instances:3
            definitions:0
            inductions:0
            search_time:
            0.012s
            details:
            Expand
            smt_stats:
            num checks:8
            arith assert lower:15
            arith tableau max rows:6
            arith tableau max columns:17
            arith pivots:11
            rlimit count:6017
            mk clause:34
            datatype occurs check:27
            mk bool var:126
            arith assert upper:12
            datatype splits:8
            decisions:34
            arith row summations:17
            propagations:63
            conflicts:11
            arith fixed eqs:8
            datatype accessor ax:23
            arith conflicts:2
            arith num rows:6
            datatype constructor ax:28
            num allocs:15925054
            final checks:6
            added eqs:116
            del clause:9
            arith eq adapter:11
            memory:16.200000
            max memory:16.240000
            Expand
            • start[0.012s]
                let (_x_0 : int) = count.list (count.list (const 0)) _x in
                let (_x_1 : ty_0 list list) = List.tl _x in
                let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                let (_x_3 : bool) = (List.hd _x_1) <> [] in
                let (_x_4 : bool) = _x_1 <> [] in
                (List.hd _x) <> [] && (_x <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
                ==> (not (_x_3 && _x_4) && not (not _x_3 && _x_4))
                    || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
            • simplify
              into:
              let (_x_0 : ty_0 list list) = List.tl _x in
              let (_x_1 : bool) = (List.hd _x_0) <> [] in
              let (_x_2 : bool) = _x_0 <> [] in
              let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in
              let (_x_4 : int) = count.list (count.list (const 0)) _x in
              (not (_x_1 && _x_2) && not (not _x_1 && _x_2))
              || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4)
              || not ((List.hd _x) <> [] && _x <> [] && (_x_4 >= 0) && (_x_3 >= 0))
              expansions:
              []
              rewrite_steps:
                forward_chaining:
                • unroll
                  expr:
                  (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                  (|count.list_453/server| (|get.::.1_433/server|…
                  expansions:
                  • unroll
                    expr:
                    (|count.list_453/server| (|get.::.1_433/server| _x_440/server))
                    expansions:
                    • unroll
                      expr:
                      (|count.list_453/server| _x_440/server)
                      expansions:
                      • Unsat
                      call `transpose3 (List.tl _x)` from `transpose3 _x`
                      original:transpose3 _x
                      sub:transpose3 (List.tl _x)
                      original ordinal:Ordinal.Int (_cnt _x)
                      sub ordinal:Ordinal.Int (_cnt (List.tl _x))
                      path:[not ((List.hd _x) <> []) && _x <> []]
                      proof:
                      detailed proof
                      ground_instances:3
                      definitions:0
                      inductions:0
                      search_time:
                      0.013s
                      details:
                      Expand
                      smt_stats:
                      num checks:8
                      arith assert lower:15
                      arith tableau max rows:6
                      arith tableau max columns:17
                      arith pivots:11
                      rlimit count:2977
                      mk clause:34
                      datatype occurs check:22
                      mk bool var:112
                      arith assert upper:12
                      datatype splits:3
                      decisions:30
                      arith row summations:17
                      propagations:62
                      conflicts:11
                      arith fixed eqs:8
                      datatype accessor ax:15
                      arith conflicts:2
                      arith num rows:6
                      datatype constructor ax:23
                      num allocs:10521530
                      final checks:6
                      added eqs:102
                      del clause:9
                      arith eq adapter:11
                      memory:16.240000
                      max memory:16.240000
                      Expand
                      • start[0.013s]
                          let (_x_0 : int) = count.list (count.list (const 0)) _x in
                          let (_x_1 : ty_0 list list) = List.tl _x in
                          let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                          let (_x_3 : bool) = (List.hd _x_1) <> [] in
                          let (_x_4 : bool) = _x_1 <> [] in
                          not ((List.hd _x) <> []) && (_x <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
                          ==> (not (_x_3 && _x_4) && not (not _x_3 && _x_4))
                              || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                      • simplify
                        into:
                        let (_x_0 : ty_0 list list) = List.tl _x in
                        let (_x_1 : bool) = (List.hd _x_0) <> [] in
                        let (_x_2 : bool) = _x_0 <> [] in
                        let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in
                        let (_x_4 : int) = count.list (count.list (const 0)) _x in
                        (not (_x_1 && _x_2) && not (not _x_1 && _x_2))
                        || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4)
                        || not (not ((List.hd _x) <> []) && _x <> [] && (_x_4 >= 0) && (_x_3 >= 0))
                        expansions:
                        []
                        rewrite_steps:
                          forward_chaining:
                          • unroll
                            expr:
                            (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                            (|count.list_453/server| (|get.::.1_433/server|…
                            expansions:
                            • unroll
                              expr:
                              (|count.list_453/server| (|get.::.1_433/server| _x_440/server))
                              expansions:
                              • unroll
                                expr:
                                (|count.list_453/server| _x_440/server)
                                expansions:
                                • Unsat
                                termination proof

                                Termination proof

                                call `get_heads (List.tl _x)` from `get_heads _x`
                                original:get_heads _x
                                sub:get_heads (List.tl _x)
                                original ordinal:Ordinal.Int (_cnt _x)
                                sub ordinal:Ordinal.Int (_cnt (List.tl _x))
                                path:[(List.hd _x) <> [] && _x <> []]
                                proof:
                                detailed proof
                                ground_instances:3
                                definitions:0
                                inductions:0
                                search_time:
                                0.011s
                                details:
                                Expand
                                smt_stats:
                                num checks:8
                                arith assert lower:15
                                arith tableau max rows:6
                                arith tableau max columns:17
                                arith pivots:11
                                rlimit count:6081
                                mk clause:34
                                datatype occurs check:25
                                mk bool var:119
                                arith assert upper:12
                                datatype splits:6
                                decisions:33
                                arith row summations:23
                                propagations:62
                                conflicts:11
                                arith fixed eqs:8
                                datatype accessor ax:21
                                arith conflicts:2
                                arith num rows:6
                                datatype constructor ax:26
                                num allocs:30448801
                                final checks:6
                                added eqs:109
                                del clause:9
                                arith eq adapter:11
                                memory:16.510000
                                max memory:16.510000
                                Expand
                                • start[0.011s]
                                    let (_x_0 : int) = count.list (count.list (const 0)) _x in
                                    let (_x_1 : ty_0 list list) = List.tl _x in
                                    let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                                    let (_x_3 : bool) = (List.hd _x_1) <> [] in
                                    let (_x_4 : bool) = _x_1 <> [] in
                                    (List.hd _x) <> [] && (_x <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
                                    ==> (not (_x_3 && _x_4) && not (not _x_3 && _x_4))
                                        || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                • simplify
                                  into:
                                  let (_x_0 : ty_0 list list) = List.tl _x in
                                  let (_x_1 : bool) = (List.hd _x_0) <> [] in
                                  let (_x_2 : bool) = _x_0 <> [] in
                                  let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in
                                  let (_x_4 : int) = count.list (count.list (const 0)) _x in
                                  (not (_x_1 && _x_2) && not (not _x_1 && _x_2))
                                  || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4)
                                  || not ((List.hd _x) <> [] && _x <> [] && (_x_4 >= 0) && (_x_3 >= 0))
                                  expansions:
                                  []
                                  rewrite_steps:
                                    forward_chaining:
                                    • unroll
                                      expr:
                                      (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                      (|count.list_564/server| (|get.::.1_544/server|…
                                      expansions:
                                      • unroll
                                        expr:
                                        (|count.list_564/server| (|get.::.1_544/server| _x_551/server))
                                        expansions:
                                        • unroll
                                          expr:
                                          (|count.list_564/server| _x_551/server)
                                          expansions:
                                          • Unsat
                                          call `get_heads (List.tl _x)` from `get_heads _x`
                                          original:get_heads _x
                                          sub:get_heads (List.tl _x)
                                          original ordinal:Ordinal.Int (_cnt _x)
                                          sub ordinal:Ordinal.Int (_cnt (List.tl _x))
                                          path:[not ((List.hd _x) <> []) && _x <> []]
                                          proof:
                                          detailed proof
                                          ground_instances:3
                                          definitions:0
                                          inductions:0
                                          search_time:
                                          0.014s
                                          details:
                                          Expand
                                          smt_stats:
                                          num checks:8
                                          arith assert lower:15
                                          arith tableau max rows:6
                                          arith tableau max columns:17
                                          arith pivots:11
                                          rlimit count:2977
                                          mk clause:34
                                          datatype occurs check:22
                                          mk bool var:112
                                          arith assert upper:12
                                          datatype splits:3
                                          decisions:30
                                          arith row summations:17
                                          propagations:62
                                          conflicts:11
                                          arith fixed eqs:8
                                          datatype accessor ax:15
                                          arith conflicts:2
                                          arith num rows:6
                                          datatype constructor ax:23
                                          num allocs:22831417
                                          final checks:6
                                          added eqs:102
                                          del clause:9
                                          arith eq adapter:11
                                          memory:16.510000
                                          max memory:16.510000
                                          Expand
                                          • start[0.014s]
                                              let (_x_0 : int) = count.list (count.list (const 0)) _x in
                                              let (_x_1 : ty_0 list list) = List.tl _x in
                                              let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                                              let (_x_3 : bool) = (List.hd _x_1) <> [] in
                                              let (_x_4 : bool) = _x_1 <> [] in
                                              not ((List.hd _x) <> []) && (_x <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
                                              ==> (not (_x_3 && _x_4) && not (not _x_3 && _x_4))
                                                  || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                          • simplify
                                            into:
                                            let (_x_0 : ty_0 list list) = List.tl _x in
                                            let (_x_1 : bool) = (List.hd _x_0) <> [] in
                                            let (_x_2 : bool) = _x_0 <> [] in
                                            let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in
                                            let (_x_4 : int) = count.list (count.list (const 0)) _x in
                                            (not (_x_1 && _x_2) && not (not _x_1 && _x_2))
                                            || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4)
                                            || not (not ((List.hd _x) <> []) && _x <> [] && (_x_4 >= 0) && (_x_3 >= 0))
                                            expansions:
                                            []
                                            rewrite_steps:
                                              forward_chaining:
                                              • unroll
                                                expr:
                                                (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                (|count.list_564/server| (|get.::.1_544/server|…
                                                expansions:
                                                • unroll
                                                  expr:
                                                  (|count.list_564/server| (|get.::.1_544/server| _x_551/server))
                                                  expansions:
                                                  • unroll
                                                    expr:
                                                    (|count.list_564/server| _x_551/server)
                                                    expansions:
                                                    • Unsat
                                                    termination proof

                                                    Termination proof

                                                    call `transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))` from `transpose l`
                                                    original:transpose l
                                                    sub:transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))
                                                    original ordinal:let (_x_0 : int) = measure_transpose l in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
                                                    sub ordinal:let (_x_0 : int) = measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
                                                    path:[(List.hd l) <> [] && l <> []]
                                                    proof:
                                                    detailed proof
                                                    ground_instances:3
                                                    definitions:0
                                                    inductions:0
                                                    search_time:
                                                    0.011s
                                                    details:
                                                    Expand
                                                    smt_stats:
                                                    num checks:7
                                                    arith assert lower:5
                                                    arith tableau max rows:2
                                                    arith tableau max columns:6
                                                    arith pivots:1
                                                    rlimit count:2086
                                                    mk clause:6
                                                    datatype occurs check:13
                                                    mk bool var:37
                                                    arith assert upper:3
                                                    datatype splits:2
                                                    decisions:6
                                                    propagations:4
                                                    conflicts:4
                                                    datatype accessor ax:11
                                                    arith conflicts:1
                                                    arith num rows:2
                                                    datatype constructor ax:9
                                                    num allocs:39870096
                                                    final checks:4
                                                    added eqs:28
                                                    del clause:3
                                                    arith eq adapter:2
                                                    memory:16.910000
                                                    max memory:16.910000
                                                    Expand
                                                    • start[0.011s]
                                                        let (_x_0 : ty_0 list) = List.hd l in
                                                        let (_x_1 : bool) = l <> [] in
                                                        let (_x_2 : int) = if _x_1 then List.length _x_0 else 0 in
                                                        let (_x_3 : int) = if _x_2 >= 0 then _x_2 else 0 in
                                                        let (_x_4 : int) = List.length … in
                                                        let (_x_5 : int) = if _x_4 >= 0 then _x_4 else 0 in
                                                        _x_0 <> [] && (_x_1 && ((_x_3 >= 0) && (_x_5 >= 0)))
                                                        ==> not ((List.tl _x_0) <> [])
                                                            || Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_3)
                                                    • simplify
                                                      into:
                                                      let (_x_0 : ty_0 list) = List.hd l in
                                                      let (_x_1 : ty_0 list) = List.tl _x_0 in
                                                      let (_x_2 : int) = List.length _x_1 in
                                                      let (_x_3 : int) = List.length _x_0 in
                                                      let (_x_4 : bool) = l <> [] in
                                                      let (_x_5 : bool) = not _x_4 || (_x_3 >= 0) in
                                                      not (_x_1 <> [])
                                                      || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 0 then _x_2 else 0))
                                                         (Ordinal.Int (if _x_5 then if _x_4 then _x_3 else 0 else 0))
                                                      || not (_x_0 <> [] && _x_4 && (_x_5 || not _x_5))
                                                      expansions:
                                                      []
                                                      rewrite_steps:
                                                        forward_chaining:
                                                        • unroll
                                                          expr:
                                                          (let ((a!1 (>= (|List.length_720/server|
                                                                           (|get.::.1_690/server| (|get.::.0_692/serv…
                                                          expansions:
                                                          • unroll
                                                            expr:
                                                            (|List.length_720/server|
                                                              (|get.::.1_690/server| (|get.::.0_692/server| l_712/server)))
                                                            expansions:
                                                            • unroll
                                                              expr:
                                                              (|List.length_720/server| (|get.::.0_692/server| l_712/server))
                                                              expansions:
                                                              • Unsat

                                                              Now we also need to extract 3×3 blocks for the additional constraint that none of them contains a duplicate.

                                                              This require a few helpers on lists and options, nothing too complicated.

                                                              In [4]:
                                                              let rec take (x:nat) l : _ list =
                                                                match x with
                                                                | Z -> []
                                                                | S x' ->
                                                                  match l with
                                                                  | [] -> []
                                                                  | y :: tl -> y :: take x' tl
                                                              
                                                              let rec drop x y =
                                                                match x with
                                                                | Z -> y
                                                                | S x' ->
                                                                  match y with
                                                                  | [] -> []
                                                                  | _ :: y' -> drop x' y'
                                                              
                                                              let rec elem x y =  match y with [] -> false | z :: ys -> x=z || elem x ys ;;
                                                              
                                                              (** Is the list [l] composed of unique elements (without duplicates)? *)
                                                              let rec unique x : bool =
                                                                match x with
                                                                | [] -> true
                                                                | y :: xs -> not (elem y xs) && unique xs
                                                              ;;
                                                              
                                                              (** Keep the elements that are [Some _], drop the others *)
                                                              let rec keep_some_list l =
                                                                match l with
                                                                | [] -> []
                                                                | y :: tail ->
                                                                  let tail = keep_some_list tail in
                                                                  match y with None -> tail | Some x -> x :: tail
                                                              ;;
                                                              
                                                              (** A block is valid if it doesn't contain duplicates *)
                                                              let block_satisfies_constraints x = unique (keep_some_list x) ;;
                                                              
                                                              let rec blocks_3_34 = function
                                                                | [] -> []
                                                                | y :: z -> drop n6 y :: blocks_3_34 z
                                                              ;;
                                                              
                                                              let rec blocks_3_33 = function
                                                                | [] -> []
                                                                | y :: z -> take n3 (drop n3 y) :: blocks_3_33 z
                                                              ;;
                                                              
                                                              let rec blocks_3_32 = function
                                                                | [] -> []
                                                                | y :: z -> take n3 y :: blocks_3_32 z
                                                              ;;
                                                              
                                                              (*
                                                              
                                                              let rec group3 = function
                                                                | xs1 :: xs2 :: xs3 :: xss ->
                                                                  (xs1 @ xs2 @ xs3) :: (group3 xss)
                                                                | _ -> []
                                                                ;;
                                                              *)
                                                              
                                                              let rec group3 = function
                                                                | [] -> []
                                                                | xs1 :: y ->
                                                                  match y with
                                                                  | [] -> []
                                                                  | xs2 :: z ->
                                                                    match z with
                                                                    | [] -> []
                                                                    | xs3 :: xss -> (xs1 @ xs2 @ xs3) :: (group3 xss)
                                                              ;;
                                                              
                                                              let blocks_3_3 l =
                                                                group3 (blocks_3_32 l) @
                                                                  group3 (blocks_3_33 l) @
                                                                    group3 (blocks_3_34 l)
                                                              ;;
                                                              
                                                              Out[4]:
                                                              val take : nat -> 'a list -> 'a list = <fun>
                                                              val drop : nat -> 'a list -> 'a list = <fun>
                                                              val elem : 'a -> 'a list -> bool = <fun>
                                                              val unique : 'a list -> bool = <fun>
                                                              val keep_some_list : 'a option list -> 'a list = <fun>
                                                              val block_satisfies_constraints : 'a option list -> bool = <fun>
                                                              val blocks_3_34 : 'a list list -> 'a list list = <fun>
                                                              val blocks_3_33 : 'a list list -> 'a list list = <fun>
                                                              val blocks_3_32 : 'a list list -> 'a list list = <fun>
                                                              val group3 : 'a list list -> 'a list list = <fun>
                                                              val blocks_3_3 : 'a list list -> 'a list list = <fun>
                                                              
                                                              termination proof

                                                              Termination proof

                                                              call `take (Destruct(S, 0, x)) (List.tl l)` from `take x l`
                                                              original:take x l
                                                              sub:take (Destruct(S, 0, x)) (List.tl l)
                                                              original ordinal:Ordinal.Int (_cnt x)
                                                              sub ordinal:Ordinal.Int (_cnt (Destruct(S, 0, x)))
                                                              path:[l <> [] && Is_a(S, x)]
                                                              proof:
                                                              detailed proof
                                                              ground_instances:3
                                                              definitions:0
                                                              inductions:0
                                                              search_time:
                                                              0.012s
                                                              details:
                                                              Expand
                                                              smt_stats:
                                                              num checks:8
                                                              arith assert lower:7
                                                              arith tableau max rows:5
                                                              arith tableau max columns:12
                                                              arith pivots:6
                                                              rlimit count:1982
                                                              mk clause:13
                                                              datatype occurs check:17
                                                              mk bool var:69
                                                              arith assert upper:7
                                                              datatype splits:2
                                                              decisions:13
                                                              arith row summations:9
                                                              propagations:14
                                                              conflicts:7
                                                              arith fixed eqs:4
                                                              datatype accessor ax:14
                                                              arith conflicts:1
                                                              arith num rows:5
                                                              arith assert diseq:1
                                                              datatype constructor ax:12
                                                              num allocs:50170403
                                                              final checks:4
                                                              added eqs:55
                                                              del clause:5
                                                              arith eq adapter:8
                                                              memory:17.170000
                                                              max memory:17.170000
                                                              Expand
                                                              • start[0.012s]
                                                                  let (_x_0 : int) = count.nat x in
                                                                  let (_x_1 : nat) = Destruct(S, 0, x) in
                                                                  let (_x_2 : int) = count.nat _x_1 in
                                                                  l <> [] && (Is_a(S, x) && ((_x_0 >= 0) && (_x_2 >= 0)))
                                                                  ==> not ((List.tl l) <> [] && Is_a(S, _x_1))
                                                                      || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                              • simplify
                                                                into:
                                                                let (_x_0 : nat) = Destruct(S, 0, x) in
                                                                let (_x_1 : int) = count.nat _x_0 in
                                                                let (_x_2 : int) = count.nat x in
                                                                not ((List.tl l) <> [] && Is_a(S, _x_0))
                                                                || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                || not (l <> [] && Is_a(S, x) && (_x_2 >= 0) && (_x_1 >= 0))
                                                                expansions:
                                                                []
                                                                rewrite_steps:
                                                                  forward_chaining:
                                                                  • unroll
                                                                    expr:
                                                                    (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                    (|count.nat_1259/client| (|get.S.0_773/server| …
                                                                    expansions:
                                                                    • unroll
                                                                      expr:
                                                                      (|count.nat_1259/client| (|get.S.0_773/server| x_783/server))
                                                                      expansions:
                                                                      • unroll
                                                                        expr:
                                                                        (|count.nat_1259/client| x_783/server)
                                                                        expansions:
                                                                        • Unsat
                                                                        termination proof

                                                                        Termination proof

                                                                        call `drop (Destruct(S, 0, x)) (List.tl y)` from `drop x y`
                                                                        original:drop x y
                                                                        sub:drop (Destruct(S, 0, x)) (List.tl y)
                                                                        original ordinal:Ordinal.Int (_cnt x)
                                                                        sub ordinal:Ordinal.Int (_cnt (Destruct(S, 0, x)))
                                                                        path:[y <> [] && Is_a(S, x)]
                                                                        proof:
                                                                        detailed proof
                                                                        ground_instances:3
                                                                        definitions:0
                                                                        inductions:0
                                                                        search_time:
                                                                        0.011s
                                                                        details:
                                                                        Expand
                                                                        smt_stats:
                                                                        num checks:8
                                                                        arith assert lower:7
                                                                        arith tableau max rows:5
                                                                        arith tableau max columns:12
                                                                        arith pivots:6
                                                                        rlimit count:1982
                                                                        mk clause:13
                                                                        datatype occurs check:17
                                                                        mk bool var:69
                                                                        arith assert upper:7
                                                                        datatype splits:2
                                                                        decisions:13
                                                                        arith row summations:9
                                                                        propagations:14
                                                                        conflicts:7
                                                                        arith fixed eqs:4
                                                                        datatype accessor ax:14
                                                                        arith conflicts:1
                                                                        arith num rows:5
                                                                        arith assert diseq:1
                                                                        datatype constructor ax:12
                                                                        num allocs:61649786
                                                                        final checks:4
                                                                        added eqs:55
                                                                        del clause:5
                                                                        arith eq adapter:8
                                                                        memory:17.410000
                                                                        max memory:17.410000
                                                                        Expand
                                                                        • start[0.011s]
                                                                            let (_x_0 : int) = count.nat x in
                                                                            let (_x_1 : nat) = Destruct(S, 0, x) in
                                                                            let (_x_2 : int) = count.nat _x_1 in
                                                                            y <> [] && (Is_a(S, x) && ((_x_0 >= 0) && (_x_2 >= 0)))
                                                                            ==> not ((List.tl y) <> [] && Is_a(S, _x_1))
                                                                                || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                        • simplify
                                                                          into:
                                                                          let (_x_0 : nat) = Destruct(S, 0, x) in
                                                                          let (_x_1 : int) = count.nat _x_0 in
                                                                          let (_x_2 : int) = count.nat x in
                                                                          not ((List.tl y) <> [] && Is_a(S, _x_0))
                                                                          || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                          || not (y <> [] && Is_a(S, x) && (_x_2 >= 0) && (_x_1 >= 0))
                                                                          expansions:
                                                                          []
                                                                          rewrite_steps:
                                                                            forward_chaining:
                                                                            • unroll
                                                                              expr:
                                                                              (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                              (|count.nat_1259/client| (|get.S.0_824/server| …
                                                                              expansions:
                                                                              • unroll
                                                                                expr:
                                                                                (|count.nat_1259/client| (|get.S.0_824/server| x_834/server))
                                                                                expansions:
                                                                                • unroll
                                                                                  expr:
                                                                                  (|count.nat_1259/client| x_834/server)
                                                                                  expansions:
                                                                                  • Unsat
                                                                                  termination proof

                                                                                  Termination proof

                                                                                  call `elem x (List.tl y)` from `elem x y`
                                                                                  original:elem x y
                                                                                  sub:elem x (List.tl y)
                                                                                  original ordinal:Ordinal.Int (_cnt y)
                                                                                  sub ordinal:Ordinal.Int (_cnt (List.tl y))
                                                                                  path:[not (x = List.hd y) && y <> []]
                                                                                  proof:
                                                                                  detailed proof
                                                                                  ground_instances:3
                                                                                  definitions:0
                                                                                  inductions:0
                                                                                  search_time:
                                                                                  0.011s
                                                                                  details:
                                                                                  Expand
                                                                                  smt_stats:
                                                                                  num checks:8
                                                                                  arith assert lower:8
                                                                                  arith tableau max rows:4
                                                                                  arith tableau max columns:11
                                                                                  arith pivots:5
                                                                                  rlimit count:1996
                                                                                  mk clause:14
                                                                                  datatype occurs check:12
                                                                                  mk bool var:60
                                                                                  arith assert upper:6
                                                                                  datatype splits:1
                                                                                  decisions:11
                                                                                  arith row summations:8
                                                                                  propagations:16
                                                                                  conflicts:7
                                                                                  arith fixed eqs:5
                                                                                  datatype accessor ax:10
                                                                                  arith conflicts:1
                                                                                  arith num rows:4
                                                                                  datatype constructor ax:8
                                                                                  num allocs:74269813
                                                                                  final checks:4
                                                                                  added eqs:46
                                                                                  del clause:6
                                                                                  arith eq adapter:7
                                                                                  memory:17.650000
                                                                                  max memory:17.650000
                                                                                  Expand
                                                                                  • start[0.011s]
                                                                                      let (_x_0 : int) = count.list (const 0) y in
                                                                                      let (_x_1 : ty_0 list) = List.tl y in
                                                                                      let (_x_2 : int) = count.list (const 0) _x_1 in
                                                                                      not (x = List.hd y) && (y <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
                                                                                      ==> not (not (x = List.hd _x_1) && _x_1 <> [])
                                                                                          || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                  • simplify
                                                                                    into:
                                                                                    let (_x_0 : ty_0 list) = List.tl y in
                                                                                    let (_x_1 : int) = count.list (const 0) _x_0 in
                                                                                    let (_x_2 : int) = count.list (const 0) y in
                                                                                    not (not (x = List.hd _x_0) && _x_0 <> [])
                                                                                    || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                    || not (not (x = List.hd y) && y <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                                                                    expansions:
                                                                                    []
                                                                                    rewrite_steps:
                                                                                      forward_chaining:
                                                                                      • unroll
                                                                                        expr:
                                                                                        (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                        (|count.list_896/server| (|get.::.1_877/server|…
                                                                                        expansions:
                                                                                        • unroll
                                                                                          expr:
                                                                                          (|count.list_896/server| (|get.::.1_877/server| y_884/server))
                                                                                          expansions:
                                                                                          • unroll
                                                                                            expr:
                                                                                            (|count.list_896/server| y_884/server)
                                                                                            expansions:
                                                                                            • Unsat
                                                                                            termination proof

                                                                                            Termination proof

                                                                                            call `unique (List.tl x)` from `unique x`
                                                                                            original:unique x
                                                                                            sub:unique (List.tl x)
                                                                                            original ordinal:Ordinal.Int (_cnt x)
                                                                                            sub ordinal:Ordinal.Int (_cnt (List.tl x))
                                                                                            path:[not (elem (List.hd x) (List.tl x)) && x <> []]
                                                                                            proof:
                                                                                            detailed proof
                                                                                            ground_instances:3
                                                                                            definitions:0
                                                                                            inductions:0
                                                                                            search_time:
                                                                                            0.011s
                                                                                            details:
                                                                                            Expand
                                                                                            smt_stats:
                                                                                            num checks:8
                                                                                            arith assert lower:5
                                                                                            arith tableau max rows:4
                                                                                            arith tableau max columns:11
                                                                                            arith pivots:4
                                                                                            rlimit count:2046
                                                                                            mk clause:11
                                                                                            datatype occurs check:12
                                                                                            mk bool var:50
                                                                                            arith assert upper:5
                                                                                            datatype splits:1
                                                                                            decisions:10
                                                                                            arith row summations:7
                                                                                            propagations:10
                                                                                            conflicts:7
                                                                                            arith fixed eqs:4
                                                                                            datatype accessor ax:9
                                                                                            arith conflicts:1
                                                                                            arith num rows:4
                                                                                            datatype constructor ax:7
                                                                                            num allocs:88273765
                                                                                            final checks:4
                                                                                            added eqs:34
                                                                                            del clause:3
                                                                                            arith eq adapter:4
                                                                                            memory:17.890000
                                                                                            max memory:17.890000
                                                                                            Expand
                                                                                            • start[0.011s]
                                                                                                let (_x_0 : ty_0 list) = List.tl x in
                                                                                                let (_x_1 : int) = count.list (const 0) x in
                                                                                                let (_x_2 : int) = count.list (const 0) _x_0 in
                                                                                                not (elem (List.hd x) _x_0) && (x <> [] && ((_x_1 >= 0) && (_x_2 >= 0)))
                                                                                                ==> not (not (elem (List.hd _x_0) (List.tl _x_0)) && _x_0 <> [])
                                                                                                    || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_1)
                                                                                            • simplify
                                                                                              into:
                                                                                              let (_x_0 : ty_0 list) = List.tl x in
                                                                                              let (_x_1 : int) = count.list (const 0) _x_0 in
                                                                                              let (_x_2 : int) = count.list (const 0) x in
                                                                                              not (not (elem (List.hd _x_0) (List.tl _x_0)) && _x_0 <> [])
                                                                                              || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                              || not (not (elem (List.hd x) _x_0) && x <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                                                                              expansions:
                                                                                              []
                                                                                              rewrite_steps:
                                                                                                forward_chaining:
                                                                                                • unroll
                                                                                                  expr:
                                                                                                  (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                                  (|count.list_950/server| (|get.::.1_929/server|…
                                                                                                  expansions:
                                                                                                  • unroll
                                                                                                    expr:
                                                                                                    (|count.list_950/server| (|get.::.1_929/server| x_939/server))
                                                                                                    expansions:
                                                                                                    • unroll
                                                                                                      expr:
                                                                                                      (|count.list_950/server| x_939/server)
                                                                                                      expansions:
                                                                                                      • Unsat
                                                                                                      termination proof

                                                                                                      Termination proof

                                                                                                      call `keep_some_list (List.tl l)` from `keep_some_list l`
                                                                                                      original:keep_some_list l
                                                                                                      sub:keep_some_list (List.tl l)
                                                                                                      original ordinal:Ordinal.Int (_cnt l)
                                                                                                      sub ordinal:Ordinal.Int (_cnt (List.tl l))
                                                                                                      path:[l <> []]
                                                                                                      proof:
                                                                                                      detailed proof
                                                                                                      ground_instances:3
                                                                                                      definitions:0
                                                                                                      inductions:0
                                                                                                      search_time:
                                                                                                      0.014s
                                                                                                      details:
                                                                                                      Expand
                                                                                                      smt_stats:
                                                                                                      num checks:8
                                                                                                      arith assert lower:8
                                                                                                      arith tableau max rows:4
                                                                                                      arith tableau max columns:12
                                                                                                      arith pivots:5
                                                                                                      rlimit count:1955
                                                                                                      mk clause:14
                                                                                                      datatype occurs check:14
                                                                                                      mk bool var:66
                                                                                                      arith assert upper:6
                                                                                                      datatype splits:3
                                                                                                      decisions:18
                                                                                                      arith row summations:8
                                                                                                      propagations:15
                                                                                                      conflicts:7
                                                                                                      arith fixed eqs:5
                                                                                                      datatype accessor ax:13
                                                                                                      arith conflicts:1
                                                                                                      arith num rows:4
                                                                                                      datatype constructor ax:14
                                                                                                      num allocs:103150556
                                                                                                      final checks:4
                                                                                                      added eqs:58
                                                                                                      del clause:6
                                                                                                      arith eq adapter:7
                                                                                                      memory:18.140000
                                                                                                      max memory:18.140000
                                                                                                      Expand
                                                                                                      • start[0.014s]
                                                                                                          let (_x_0 : int) = count.list (count.option (const 0)) l in
                                                                                                          let (_x_1 : ty_0 option list) = List.tl l in
                                                                                                          let (_x_2 : int) = count.list (count.option (const 0)) _x_1 in
                                                                                                          l <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
                                                                                                          ==> not (_x_1 <> [])
                                                                                                              || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                      • simplify
                                                                                                        into:
                                                                                                        let (_x_0 : ty_0 option list) = List.tl l in
                                                                                                        let (_x_1 : int) = count.list (count.option (const 0)) _x_0 in
                                                                                                        let (_x_2 : int) = count.list (count.option (const 0)) l in
                                                                                                        not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                        || not (l <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                                                                                        expansions:
                                                                                                        []
                                                                                                        rewrite_steps:
                                                                                                          forward_chaining:
                                                                                                          • unroll
                                                                                                            expr:
                                                                                                            (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                                            (|count.list_1006/server| (|get.::.1_985/server…
                                                                                                            expansions:
                                                                                                            • unroll
                                                                                                              expr:
                                                                                                              (|count.list_1006/server| (|get.::.1_985/server| l_995/server))
                                                                                                              expansions:
                                                                                                              • unroll
                                                                                                                expr:
                                                                                                                (|count.list_1006/server| l_995/server)
                                                                                                                expansions:
                                                                                                                • Unsat
                                                                                                                termination proof

                                                                                                                Termination proof

                                                                                                                call `blocks_3_34 (List.tl _x)` from `blocks_3_34 _x`
                                                                                                                original:blocks_3_34 _x
                                                                                                                sub:blocks_3_34 (List.tl _x)
                                                                                                                original ordinal:Ordinal.Int (_cnt _x)
                                                                                                                sub ordinal:Ordinal.Int (_cnt (List.tl _x))
                                                                                                                path:[_x <> []]
                                                                                                                proof:
                                                                                                                detailed proof
                                                                                                                ground_instances:3
                                                                                                                definitions:0
                                                                                                                inductions:0
                                                                                                                search_time:
                                                                                                                0.012s
                                                                                                                details:
                                                                                                                Expand
                                                                                                                smt_stats:
                                                                                                                num checks:8
                                                                                                                arith assert lower:18
                                                                                                                arith tableau max rows:7
                                                                                                                arith tableau max columns:18
                                                                                                                arith pivots:9
                                                                                                                rlimit count:2520
                                                                                                                mk clause:27
                                                                                                                datatype occurs check:14
                                                                                                                mk bool var:87
                                                                                                                arith assert upper:16
                                                                                                                datatype splits:3
                                                                                                                decisions:23
                                                                                                                arith row summations:19
                                                                                                                propagations:26
                                                                                                                conflicts:10
                                                                                                                arith fixed eqs:8
                                                                                                                datatype accessor ax:11
                                                                                                                minimized lits:1
                                                                                                                arith conflicts:2
                                                                                                                arith num rows:7
                                                                                                                datatype constructor ax:15
                                                                                                                num allocs:120087248
                                                                                                                final checks:4
                                                                                                                added eqs:64
                                                                                                                del clause:15
                                                                                                                arith eq adapter:13
                                                                                                                memory:18.680000
                                                                                                                max memory:18.680000
                                                                                                                Expand
                                                                                                                • start[0.012s]
                                                                                                                    let (_x_0 : int) = count.list (count.list (const 0)) _x in
                                                                                                                    let (_x_1 : ty_0 list list) = List.tl _x in
                                                                                                                    let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                                                                                                                    _x <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
                                                                                                                    ==> not (_x_1 <> [])
                                                                                                                        || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                • simplify
                                                                                                                  into:
                                                                                                                  let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                  let (_x_1 : int) = count.list (count.list (const 0)) _x_0 in
                                                                                                                  let (_x_2 : int) = count.list (count.list (const 0)) _x in
                                                                                                                  not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                  || not (_x <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                                                                                                  expansions:
                                                                                                                  []
                                                                                                                  rewrite_steps:
                                                                                                                    forward_chaining:
                                                                                                                    • unroll
                                                                                                                      expr:
                                                                                                                      (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                                                      (|count.list_1096/server|
                                                                                                                                        (|g…
                                                                                                                      expansions:
                                                                                                                      • unroll
                                                                                                                        expr:
                                                                                                                        (|count.list_1096/server| (|get.::.1_1073/server| _x_1085/server))
                                                                                                                        expansions:
                                                                                                                        • unroll
                                                                                                                          expr:
                                                                                                                          (|count.list_1096/server| _x_1085/server)
                                                                                                                          expansions:
                                                                                                                          • Unsat
                                                                                                                          termination proof

                                                                                                                          Termination proof

                                                                                                                          call `blocks_3_33 (List.tl _x)` from `blocks_3_33 _x`
                                                                                                                          original:blocks_3_33 _x
                                                                                                                          sub:blocks_3_33 (List.tl _x)
                                                                                                                          original ordinal:Ordinal.Int (_cnt _x)
                                                                                                                          sub ordinal:Ordinal.Int (_cnt (List.tl _x))
                                                                                                                          path:[_x <> []]
                                                                                                                          proof:
                                                                                                                          detailed proof
                                                                                                                          ground_instances:3
                                                                                                                          definitions:0
                                                                                                                          inductions:0
                                                                                                                          search_time:
                                                                                                                          0.014s
                                                                                                                          details:
                                                                                                                          Expand
                                                                                                                          smt_stats:
                                                                                                                          num checks:8
                                                                                                                          arith assert lower:22
                                                                                                                          arith tableau max rows:7
                                                                                                                          arith tableau max columns:18
                                                                                                                          arith pivots:11
                                                                                                                          rlimit count:2643
                                                                                                                          mk clause:34
                                                                                                                          datatype occurs check:14
                                                                                                                          mk bool var:98
                                                                                                                          arith assert upper:18
                                                                                                                          datatype splits:3
                                                                                                                          decisions:22
                                                                                                                          arith row summations:20
                                                                                                                          arith bound prop:1
                                                                                                                          propagations:41
                                                                                                                          conflicts:9
                                                                                                                          arith fixed eqs:12
                                                                                                                          datatype accessor ax:13
                                                                                                                          minimized lits:1
                                                                                                                          arith conflicts:2
                                                                                                                          arith num rows:7
                                                                                                                          arith assert diseq:1
                                                                                                                          datatype constructor ax:15
                                                                                                                          num allocs:137629069
                                                                                                                          final checks:4
                                                                                                                          added eqs:84
                                                                                                                          del clause:14
                                                                                                                          arith eq adapter:17
                                                                                                                          memory:18.940000
                                                                                                                          max memory:18.940000
                                                                                                                          Expand
                                                                                                                          • start[0.014s]
                                                                                                                              let (_x_0 : int) = count.list (count.list (const 0)) _x in
                                                                                                                              let (_x_1 : ty_0 list list) = List.tl _x in
                                                                                                                              let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                                                                                                                              _x <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
                                                                                                                              ==> not (_x_1 <> [])
                                                                                                                                  || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                          • simplify
                                                                                                                            into:
                                                                                                                            let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                            let (_x_1 : int) = count.list (count.list (const 0)) _x_0 in
                                                                                                                            let (_x_2 : int) = count.list (count.list (const 0)) _x in
                                                                                                                            not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                            || not (_x <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                                                                                                            expansions:
                                                                                                                            []
                                                                                                                            rewrite_steps:
                                                                                                                              forward_chaining:
                                                                                                                              • unroll
                                                                                                                                expr:
                                                                                                                                (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                                                                (|count.list_1165/server|
                                                                                                                                                  (|g…
                                                                                                                                expansions:
                                                                                                                                • unroll
                                                                                                                                  expr:
                                                                                                                                  (|count.list_1165/server| (|get.::.1_1136/server| _x_1154/server))
                                                                                                                                  expansions:
                                                                                                                                  • unroll
                                                                                                                                    expr:
                                                                                                                                    (|count.list_1165/server| _x_1154/server)
                                                                                                                                    expansions:
                                                                                                                                    • Unsat
                                                                                                                                    termination proof

                                                                                                                                    Termination proof

                                                                                                                                    call `blocks_3_32 (List.tl _x)` from `blocks_3_32 _x`
                                                                                                                                    original:blocks_3_32 _x
                                                                                                                                    sub:blocks_3_32 (List.tl _x)
                                                                                                                                    original ordinal:Ordinal.Int (_cnt _x)
                                                                                                                                    sub ordinal:Ordinal.Int (_cnt (List.tl _x))
                                                                                                                                    path:[_x <> []]
                                                                                                                                    proof:
                                                                                                                                    detailed proof
                                                                                                                                    ground_instances:3
                                                                                                                                    definitions:0
                                                                                                                                    inductions:0
                                                                                                                                    search_time:
                                                                                                                                    0.013s
                                                                                                                                    details:
                                                                                                                                    Expand
                                                                                                                                    smt_stats:
                                                                                                                                    num checks:8
                                                                                                                                    arith assert lower:22
                                                                                                                                    arith tableau max rows:7
                                                                                                                                    arith tableau max columns:18
                                                                                                                                    arith pivots:11
                                                                                                                                    rlimit count:2643
                                                                                                                                    mk clause:34
                                                                                                                                    datatype occurs check:14
                                                                                                                                    mk bool var:98
                                                                                                                                    arith assert upper:18
                                                                                                                                    datatype splits:3
                                                                                                                                    decisions:22
                                                                                                                                    arith row summations:20
                                                                                                                                    arith bound prop:1
                                                                                                                                    propagations:41
                                                                                                                                    conflicts:9
                                                                                                                                    arith fixed eqs:12
                                                                                                                                    datatype accessor ax:13
                                                                                                                                    minimized lits:1
                                                                                                                                    arith conflicts:2
                                                                                                                                    arith num rows:7
                                                                                                                                    arith assert diseq:1
                                                                                                                                    datatype constructor ax:15
                                                                                                                                    num allocs:156369657
                                                                                                                                    final checks:4
                                                                                                                                    added eqs:84
                                                                                                                                    del clause:14
                                                                                                                                    arith eq adapter:17
                                                                                                                                    memory:19.220000
                                                                                                                                    max memory:19.220000
                                                                                                                                    Expand
                                                                                                                                    • start[0.013s]
                                                                                                                                        let (_x_0 : int) = count.list (count.list (const 0)) _x in
                                                                                                                                        let (_x_1 : ty_0 list list) = List.tl _x in
                                                                                                                                        let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
                                                                                                                                        _x <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
                                                                                                                                        ==> not (_x_1 <> [])
                                                                                                                                            || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                    • simplify
                                                                                                                                      into:
                                                                                                                                      let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                                      let (_x_1 : int) = count.list (count.list (const 0)) _x_0 in
                                                                                                                                      let (_x_2 : int) = count.list (count.list (const 0)) _x in
                                                                                                                                      not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                                      || not (_x <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                                                                                                                      expansions:
                                                                                                                                      []
                                                                                                                                      rewrite_steps:
                                                                                                                                        forward_chaining:
                                                                                                                                        • unroll
                                                                                                                                          expr:
                                                                                                                                          (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                                                                          (|count.list_1228/server|
                                                                                                                                                            (|g…
                                                                                                                                          expansions:
                                                                                                                                          • unroll
                                                                                                                                            expr:
                                                                                                                                            (|count.list_1228/server| (|get.::.1_1205/server| _x_1217/server))
                                                                                                                                            expansions:
                                                                                                                                            • unroll
                                                                                                                                              expr:
                                                                                                                                              (|count.list_1228/server| _x_1217/server)
                                                                                                                                              expansions:
                                                                                                                                              • Unsat
                                                                                                                                              termination proof

                                                                                                                                              Termination proof

                                                                                                                                              call `group3 (List.tl (List.tl (List.tl _x)))` from `group3 _x`
                                                                                                                                              original:group3 _x
                                                                                                                                              sub:group3 (List.tl (List.tl (List.tl _x)))
                                                                                                                                              original ordinal:Ordinal.Int (_cnt _x)
                                                                                                                                              sub ordinal:Ordinal.Int (_cnt (List.tl (List.tl (List.tl _x))))
                                                                                                                                              path:[(List.tl (List.tl _x)) <> [] && (List.tl _x) <> [] && _x <> []]
                                                                                                                                              proof:
                                                                                                                                              detailed proof
                                                                                                                                              ground_instances:12
                                                                                                                                              definitions:0
                                                                                                                                              inductions:0
                                                                                                                                              search_time:
                                                                                                                                              0.051s
                                                                                                                                              details:
                                                                                                                                              Expand
                                                                                                                                              smt_stats:
                                                                                                                                              arith offset eqs:47
                                                                                                                                              num checks:26
                                                                                                                                              arith assert lower:830
                                                                                                                                              arith tableau max rows:50
                                                                                                                                              arith tableau max columns:91
                                                                                                                                              arith pivots:240
                                                                                                                                              rlimit count:85404
                                                                                                                                              mk clause:754
                                                                                                                                              datatype occurs check:256
                                                                                                                                              mk bool var:1903
                                                                                                                                              arith assert upper:755
                                                                                                                                              datatype splits:80
                                                                                                                                              decisions:1871
                                                                                                                                              arith row summations:1315
                                                                                                                                              arith bound prop:71
                                                                                                                                              propagations:1924
                                                                                                                                              interface eqs:9
                                                                                                                                              conflicts:107
                                                                                                                                              arith fixed eqs:362
                                                                                                                                              arith assume eqs:9
                                                                                                                                              datatype accessor ax:204
                                                                                                                                              minimized lits:30
                                                                                                                                              arith conflicts:23
                                                                                                                                              arith num rows:50
                                                                                                                                              arith assert diseq:282
                                                                                                                                              datatype constructor ax:436
                                                                                                                                              num allocs:178715953
                                                                                                                                              final checks:39
                                                                                                                                              added eqs:2667
                                                                                                                                              del clause:487
                                                                                                                                              arith eq adapter:502
                                                                                                                                              time:0.001000
                                                                                                                                              memory:20.310000
                                                                                                                                              max memory:20.310000
                                                                                                                                              Expand
                                                                                                                                              • start[0.051s]
                                                                                                                                                  let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                                                  let (_x_1 : ty_0 list list) = List.tl _x_0 in
                                                                                                                                                  let (_x_2 : int) = count.list (count.list (const 0)) _x in
                                                                                                                                                  let (_x_3 : ty_0 list list) = List.tl _x_1 in
                                                                                                                                                  let (_x_4 : int) = count.list (count.list (const 0)) _x_3 in
                                                                                                                                                  let (_x_5 : ty_0 list list) = List.tl _x_3 in
                                                                                                                                                  _x_1 <> [] && (_x_0 <> [] && (_x <> [] && ((_x_2 >= 0) && (_x_4 >= 0))))
                                                                                                                                                  ==> not ((List.tl _x_5) <> [] && (_x_5 <> [] && _x_3 <> []))
                                                                                                                                                      || Ordinal.( << ) (Ordinal.Int _x_4) (Ordinal.Int _x_2)
                                                                                                                                              • simplify
                                                                                                                                                into:
                                                                                                                                                let (_x_0 : ty_0 list list) = List.tl _x in
                                                                                                                                                let (_x_1 : ty_0 list list) = List.tl _x_0 in
                                                                                                                                                let (_x_2 : ty_0 list list) = List.tl _x_1 in
                                                                                                                                                let (_x_3 : int) = count.list (count.list (const 0)) _x_2 in
                                                                                                                                                let (_x_4 : int) = count.list (count.list (const 0)) _x in
                                                                                                                                                let (_x_5 : ty_0 list list) = List.tl _x_2 in
                                                                                                                                                Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4)
                                                                                                                                                || not ((List.tl _x_5) <> [] && _x_5 <> [] && _x_2 <> [])
                                                                                                                                                || not (_x_1 <> [] && _x_0 <> [] && _x <> [] && (_x_4 >= 0) && (_x_3 >= 0))
                                                                                                                                                expansions:
                                                                                                                                                []
                                                                                                                                                rewrite_steps:
                                                                                                                                                  forward_chaining:
                                                                                                                                                  • unroll
                                                                                                                                                    expr:
                                                                                                                                                    (let ((a!1 (|count.list_1293/server|
                                                                                                                                                                 (|get.::.1_1268/server|
                                                                                                                                                                   (|get.::.1_…
                                                                                                                                                    expansions:
                                                                                                                                                    • unroll
                                                                                                                                                      expr:
                                                                                                                                                      (|count.list_1293/server|
                                                                                                                                                        (|get.::.1_1268/server|
                                                                                                                                                          (|get.::.1_1268/server| (|get.::.1_1268/serv…
                                                                                                                                                      expansions:
                                                                                                                                                      • unroll
                                                                                                                                                        expr:
                                                                                                                                                        (|count.list_1293/server| _x_1282/server)
                                                                                                                                                        expansions:
                                                                                                                                                        • unroll
                                                                                                                                                          expr:
                                                                                                                                                          (let ((a!1 (|get.::.1_1268/server|
                                                                                                                                                                       (|get.::.1_1268/server|
                                                                                                                                                                         (|get.::.1_12…
                                                                                                                                                          expansions:
                                                                                                                                                          • unroll
                                                                                                                                                            expr:
                                                                                                                                                            (let ((a!1 (|count.list_1293/server|
                                                                                                                                                                         (|get.::.1_1268/server|
                                                                                                                                                                           (|get.::.1_…
                                                                                                                                                            expansions:
                                                                                                                                                            • unroll
                                                                                                                                                              expr:
                                                                                                                                                              (let ((a!1 (|get.::.0_1267/server|
                                                                                                                                                                           (|get.::.1_1268/server|
                                                                                                                                                                             (|get.::.1_12…
                                                                                                                                                              expansions:
                                                                                                                                                              • unroll
                                                                                                                                                                expr:
                                                                                                                                                                (|count.list_1293/server| (|get.::.1_1268/server| _x_1282/server))
                                                                                                                                                                expansions:
                                                                                                                                                                • unroll
                                                                                                                                                                  expr:
                                                                                                                                                                  (|count.list_1297/server| (|get.::.0_1267/server| _x_1282/server))
                                                                                                                                                                  expansions:
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr:
                                                                                                                                                                    (let ((a!1 (|get.::.1_1268/server|
                                                                                                                                                                                 (|get.::.1_1268/server|
                                                                                                                                                                                   (|get.::.1_12…
                                                                                                                                                                    expansions:
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr:
                                                                                                                                                                      (let ((a!1 (|count.list_1293/server|
                                                                                                                                                                                   (|get.::.1_1268/server|
                                                                                                                                                                                     (|get.::.1_…
                                                                                                                                                                      expansions:
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr:
                                                                                                                                                                        (let ((a!1 (|get.::.1_1268/server|
                                                                                                                                                                                     (|get.::.1_1268/server|
                                                                                                                                                                                       (|get.::.1_12…
                                                                                                                                                                        expansions:
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr:
                                                                                                                                                                          (|count.list_1293/server|
                                                                                                                                                                            (|get.::.1_1268/server| (|get.::.1_1268/server| _x_1282/server)))
                                                                                                                                                                          expansions:
                                                                                                                                                                          • Unsat

                                                                                                                                                                          The Sudoku type

                                                                                                                                                                          We're ready to define the sudoku as a list of lists of (possibly empty) cells.

                                                                                                                                                                          First, cells are just an enumeration of 9 distinct cases:

                                                                                                                                                                          In [5]:
                                                                                                                                                                          type cell = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 ;;
                                                                                                                                                                          
                                                                                                                                                                          (* let us also write a nice printer for cells. We will put
                                                                                                                                                                             it to good use later. *)
                                                                                                                                                                          let doc_of_cell c =
                                                                                                                                                                            Document.s (match c with C1->"1"|C2->"2"|C3->"3"|C4->"4"|C5->"5"|C6->"6"|C7->"7"|C8->"8"|C9->"9") [@@program];;
                                                                                                                                                                          
                                                                                                                                                                          #install_doc doc_of_cell;;
                                                                                                                                                                          
                                                                                                                                                                          Out[5]:
                                                                                                                                                                          type cell = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9
                                                                                                                                                                          val doc_of_cell : cell -> Document.t = <fun>
                                                                                                                                                                          

                                                                                                                                                                          And the sudoku itself:

                                                                                                                                                                          In [6]:
                                                                                                                                                                          type sudoku = { rows: cell option list list } ;;
                                                                                                                                                                          
                                                                                                                                                                          (* now install a nice printer for sudoku grids *)
                                                                                                                                                                          let doc_of_sudoku (s:sudoku) : Document.t =
                                                                                                                                                                            let module D = Document in
                                                                                                                                                                            let d_of_c = function None -> D.s "·" | Some c -> doc_of_cell c in
                                                                                                                                                                            D.tbl_of d_of_c s.rows [@@program]
                                                                                                                                                                            ;;
                                                                                                                                                                          
                                                                                                                                                                          #install_doc doc_of_sudoku;;
                                                                                                                                                                          
                                                                                                                                                                          Out[6]:
                                                                                                                                                                          type sudoku = { rows : cell option list list; }
                                                                                                                                                                          val doc_of_sudoku : sudoku -> Document.t = <fun>
                                                                                                                                                                          

                                                                                                                                                                          We're going to solve the following instance (still from Dan Rosén and Koen Claessen's code). The custom printer we installed earlier shows the grid in a readable way.

                                                                                                                                                                          In [7]:
                                                                                                                                                                          let the_problem : sudoku =
                                                                                                                                                                            {rows=
                                                                                                                                                                              [ [ (Some C8) ; None ; None ; None ; None ; None ; None ; None ; None ];
                                                                                                                                                                              [ None ; None ; (Some C3) ; (Some C6) ; None ; None ; None ; None ; None ];
                                                                                                                                                                              [ None ; (Some C7) ; None ; None ; (Some C9) ; None ; (Some C2) ; None ; None ];
                                                                                                                                                                              [ None ; (Some C5) ; None ; None ; None ; (Some C7) ; None ; None ; None ];
                                                                                                                                                                              [ None ; None ; None ; None ; (Some C4) ; (Some C5) ; (Some C7) ; None ; None ];
                                                                                                                                                                              [ None ; None ; None ; (Some C1) ; None ; None ; None ; (Some C3) ; None ];
                                                                                                                                                                              [ None ; None ; (Some C1) ; None ; None ; None ; None ; (Some C6) ; (Some C8); ];
                                                                                                                                                                              [ None ; None ; (Some C8) ; (Some C5) ; None ; None ; None ; (Some C1) ; None ];
                                                                                                                                                                              [ None ; (Some C9) ; None ; None ; None ; None ; (Some C4) ; None ; None ];
                                                                                                                                                                            ]}
                                                                                                                                                                          ;;
                                                                                                                                                                          
                                                                                                                                                                          Out[7]:
                                                                                                                                                                          val the_problem : sudoku = <document>
                                                                                                                                                                          
                                                                                                                                                                          8········
                                                                                                                                                                          ··36·····
                                                                                                                                                                          ·7··9·2··
                                                                                                                                                                          ·5···7···
                                                                                                                                                                          ····457··
                                                                                                                                                                          ···1···3·
                                                                                                                                                                          ··1····68
                                                                                                                                                                          ··85···1·
                                                                                                                                                                          ·9····4··
                                                                                                                                                                          In [8]:
                                                                                                                                                                          (** All the relevant blocks: rows, columns, and 3×3 sub-squares *)
                                                                                                                                                                          let blocks (x:sudoku) =
                                                                                                                                                                            x.rows @ transpose x.rows @ blocks_3_3 x.rows
                                                                                                                                                                          
                                                                                                                                                                          (** Are all constraints satisfied? *)
                                                                                                                                                                          let satisfies_constraints (x:sudoku) = List.for_all block_satisfies_constraints (blocks x);;
                                                                                                                                                                          
                                                                                                                                                                          (** is a sudoku entirely defined (all cells are filled)? *)
                                                                                                                                                                          let is_solved (x:sudoku) =
                                                                                                                                                                            List.for_all (List.for_all Option.is_some) x.rows;;
                                                                                                                                                                          
                                                                                                                                                                          (** Is [x] of the correct shape, i.e. a 9×9 grid? *)
                                                                                                                                                                          let is_valid_sudoku (x:sudoku) =
                                                                                                                                                                            length x.rows = n9 &&
                                                                                                                                                                            List.for_all (fun col -> length col = n9) x.rows
                                                                                                                                                                          ;;
                                                                                                                                                                          
                                                                                                                                                                          Out[8]:
                                                                                                                                                                          val blocks : sudoku -> cell option list list = <fun>
                                                                                                                                                                          val satisfies_constraints : sudoku -> bool = <fun>
                                                                                                                                                                          val is_solved : sudoku -> bool = <fun>
                                                                                                                                                                          val is_valid_sudoku : sudoku -> bool = <fun>
                                                                                                                                                                          

                                                                                                                                                                          We have a template (the initial problem) and we want to solve it. It means the sudoku we're looking for must be:

                                                                                                                                                                          • solved (all cells are Some _ rather than None)
                                                                                                                                                                          • a solution of the template (i.e. cells defined in the template must match)
                                                                                                                                                                          In [9]:
                                                                                                                                                                          (** Combine lists together *)
                                                                                                                                                                          let rec zip l1 l2 = match l1, l2 with
                                                                                                                                                                            | [], _ | _, [] -> []
                                                                                                                                                                            | x1::tl1, x2 :: tl2 -> (x1,x2) :: zip tl1 tl2
                                                                                                                                                                          
                                                                                                                                                                          let rec match_cols y =
                                                                                                                                                                            match y with
                                                                                                                                                                            | [] -> true
                                                                                                                                                                            | z :: x2 ->
                                                                                                                                                                              match z with
                                                                                                                                                                              | None,_ | _, None -> match_cols x2
                                                                                                                                                                              | (Some n1,Some n2) -> n1=n2 && match_cols x2
                                                                                                                                                                          ;;
                                                                                                                                                                          
                                                                                                                                                                          let rec match_rows x =
                                                                                                                                                                            match x with
                                                                                                                                                                            | [] -> true
                                                                                                                                                                            | (row1,row2) :: z -> match_cols (zip row1 row2) && match_rows z
                                                                                                                                                                          ;;
                                                                                                                                                                          
                                                                                                                                                                          (** is [x] a solution of [y]? We check that each cell in each rows,
                                                                                                                                                                              if defined in [y], has the same value in [x] *)
                                                                                                                                                                          let is_solution_of (x:sudoku) (y:sudoku) : bool =
                                                                                                                                                                            is_solved x &&
                                                                                                                                                                            satisfies_constraints x &&
                                                                                                                                                                            match_rows (zip x.rows y.rows)
                                                                                                                                                                          
                                                                                                                                                                          Out[9]:
                                                                                                                                                                          val zip : 'a list -> 'b list -> ('a * 'b) list = <fun>
                                                                                                                                                                          val match_cols : ('a option * 'a option) list -> bool = <fun>
                                                                                                                                                                          val match_rows : ('a option list * 'a option list) list -> bool = <fun>
                                                                                                                                                                          val is_solution_of : sudoku -> sudoku -> bool = <fun>
                                                                                                                                                                          
                                                                                                                                                                          termination proof

                                                                                                                                                                          Termination proof

                                                                                                                                                                          call `zip (List.tl l1) (List.tl l2)` from `zip l1 l2`
                                                                                                                                                                          original:zip l1 l2
                                                                                                                                                                          sub:zip (List.tl l1) (List.tl l2)
                                                                                                                                                                          original ordinal:Ordinal.Int (_cnt l1)
                                                                                                                                                                          sub ordinal:Ordinal.Int (_cnt (List.tl l1))
                                                                                                                                                                          path:[l2 <> [] && l1 <> []]
                                                                                                                                                                          proof:
                                                                                                                                                                          detailed proof
                                                                                                                                                                          ground_instances:3
                                                                                                                                                                          definitions:0
                                                                                                                                                                          inductions:0
                                                                                                                                                                          search_time:
                                                                                                                                                                          0.013s
                                                                                                                                                                          details:
                                                                                                                                                                          Expand
                                                                                                                                                                          smt_stats:
                                                                                                                                                                          num checks:8
                                                                                                                                                                          arith assert lower:7
                                                                                                                                                                          arith tableau max rows:5
                                                                                                                                                                          arith tableau max columns:12
                                                                                                                                                                          arith pivots:6
                                                                                                                                                                          rlimit count:1992
                                                                                                                                                                          mk clause:13
                                                                                                                                                                          datatype occurs check:17
                                                                                                                                                                          mk bool var:71
                                                                                                                                                                          arith assert upper:7
                                                                                                                                                                          datatype splits:2
                                                                                                                                                                          decisions:13
                                                                                                                                                                          arith row summations:9
                                                                                                                                                                          propagations:14
                                                                                                                                                                          conflicts:7
                                                                                                                                                                          arith fixed eqs:4
                                                                                                                                                                          datatype accessor ax:14
                                                                                                                                                                          arith conflicts:1
                                                                                                                                                                          arith num rows:5
                                                                                                                                                                          arith assert diseq:1
                                                                                                                                                                          datatype constructor ax:12
                                                                                                                                                                          num allocs:209259757
                                                                                                                                                                          final checks:4
                                                                                                                                                                          added eqs:57
                                                                                                                                                                          del clause:5
                                                                                                                                                                          arith eq adapter:8
                                                                                                                                                                          memory:21.430000
                                                                                                                                                                          max memory:21.430000
                                                                                                                                                                          Expand
                                                                                                                                                                          • start[0.013s]
                                                                                                                                                                              let (_x_0 : int) = count.list (const 0) l1 in
                                                                                                                                                                              let (_x_1 : ty_0 list) = List.tl l1 in
                                                                                                                                                                              let (_x_2 : int) = count.list (const 0) _x_1 in
                                                                                                                                                                              l2 <> [] && (l1 <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
                                                                                                                                                                              ==> not ((List.tl l2) <> [] && _x_1 <> [])
                                                                                                                                                                                  || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                                                          • simplify
                                                                                                                                                                            into:
                                                                                                                                                                            let (_x_0 : ty_0 list) = List.tl l1 in
                                                                                                                                                                            let (_x_1 : int) = count.list (const 0) _x_0 in
                                                                                                                                                                            let (_x_2 : int) = count.list (const 0) l1 in
                                                                                                                                                                            not ((List.tl l2) <> [] && _x_0 <> [])
                                                                                                                                                                            || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                                                                            || not (l2 <> [] && l1 <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                                                                                                                                                            expansions:
                                                                                                                                                                            []
                                                                                                                                                                            rewrite_steps:
                                                                                                                                                                              forward_chaining:
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr:
                                                                                                                                                                                (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                                                                                                                (|count.list_1675/server|
                                                                                                                                                                                                  (|g…
                                                                                                                                                                                expansions:
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr:
                                                                                                                                                                                  (|count.list_1675/server| (|get.::.1_1638/server| l1_1662/server))
                                                                                                                                                                                  expansions:
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr:
                                                                                                                                                                                    (|count.list_1675/server| l1_1662/server)
                                                                                                                                                                                    expansions:
                                                                                                                                                                                    • Unsat
                                                                                                                                                                                    termination proof

                                                                                                                                                                                    Termination proof

                                                                                                                                                                                    call `match_cols (List.tl y)` from `match_cols y`
                                                                                                                                                                                    original:match_cols y
                                                                                                                                                                                    sub:match_cols (List.tl y)
                                                                                                                                                                                    original ordinal:Ordinal.Int (_cnt y)
                                                                                                                                                                                    sub ordinal:Ordinal.Int (_cnt (List.tl y))
                                                                                                                                                                                    path:[Is_a(None, (List.hd y).0) && y <> []]
                                                                                                                                                                                    proof:
                                                                                                                                                                                    detailed proof
                                                                                                                                                                                    ground_instances:3
                                                                                                                                                                                    definitions:0
                                                                                                                                                                                    inductions:0
                                                                                                                                                                                    search_time:
                                                                                                                                                                                    0.013s
                                                                                                                                                                                    details:
                                                                                                                                                                                    Expand
                                                                                                                                                                                    smt_stats:
                                                                                                                                                                                    num checks:8
                                                                                                                                                                                    arith assert lower:11
                                                                                                                                                                                    arith tableau max rows:6
                                                                                                                                                                                    arith tableau max columns:14
                                                                                                                                                                                    arith pivots:5
                                                                                                                                                                                    rlimit count:9007
                                                                                                                                                                                    mk clause:29
                                                                                                                                                                                    datatype occurs check:27
                                                                                                                                                                                    mk bool var:140
                                                                                                                                                                                    arith assert upper:9
                                                                                                                                                                                    datatype splits:6
                                                                                                                                                                                    decisions:36
                                                                                                                                                                                    arith row summations:15
                                                                                                                                                                                    propagations:63
                                                                                                                                                                                    conflicts:12
                                                                                                                                                                                    arith fixed eqs:5
                                                                                                                                                                                    datatype accessor ax:28
                                                                                                                                                                                    arith conflicts:1
                                                                                                                                                                                    arith num rows:6
                                                                                                                                                                                    arith assert diseq:1
                                                                                                                                                                                    datatype constructor ax:37
                                                                                                                                                                                    num allocs:283968306
                                                                                                                                                                                    final checks:6
                                                                                                                                                                                    added eqs:140
                                                                                                                                                                                    del clause:15
                                                                                                                                                                                    arith eq adapter:9
                                                                                                                                                                                    memory:21.780000
                                                                                                                                                                                    max memory:21.810000
                                                                                                                                                                                    Expand
                                                                                                                                                                                    • start[0.013s]
                                                                                                                                                                                        let (_x_0 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                        let (_x_1 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                        let (_x_2 : int) = count.list anon_fun._cnt.1 _x_1 in
                                                                                                                                                                                        let (_x_3 : (ty_0 option * ty_0 option)) = List.hd _x_1 in
                                                                                                                                                                                        let (_x_4 : ty_0 option) = _x_3.0 in
                                                                                                                                                                                        let (_x_5 : bool) = Is_a(None, _x_4) in
                                                                                                                                                                                        let (_x_6 : bool) = _x_1 <> [] in
                                                                                                                                                                                        let (_x_7 : ty_0 option) = _x_3.1 in
                                                                                                                                                                                        let (_x_8 : bool) = Is_a(None, _x_7) in
                                                                                                                                                                                        let (_x_9 : bool) = not _x_5 && _x_6 in
                                                                                                                                                                                        Is_a(None, (List.hd y).0) && (y <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
                                                                                                                                                                                        ==> (not (_x_5 && _x_6)
                                                                                                                                                                                             && (not (_x_8 && _x_9)
                                                                                                                                                                                                 && not ((Option.get _x_4 = Option.get _x_7) && (not _x_8 && _x_9))))
                                                                                                                                                                                            || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                                                                                                                                    • simplify
                                                                                                                                                                                      into:
                                                                                                                                                                                      let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                      let (_x_1 : int) = count.list anon_fun._cnt.1 _x_0 in
                                                                                                                                                                                      let (_x_2 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                      let (_x_3 : (ty_0 option * ty_0 option)) = List.hd _x_0 in
                                                                                                                                                                                      let (_x_4 : ty_0 option) = _x_3.0 in
                                                                                                                                                                                      let (_x_5 : bool) = Is_a(None, _x_4) in
                                                                                                                                                                                      let (_x_6 : bool) = _x_0 <> [] in
                                                                                                                                                                                      let (_x_7 : ty_0 option) = _x_3.1 in
                                                                                                                                                                                      let (_x_8 : bool) = Is_a(None, _x_7) in
                                                                                                                                                                                      let (_x_9 : bool) = not _x_5 in
                                                                                                                                                                                      Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                                                                                      || (not (_x_5 && _x_6) && not (_x_8 && _x_9 && _x_6)
                                                                                                                                                                                          && not ((Option.get _x_4 = Option.get _x_7) && not _x_8 && _x_9 && _x_6))
                                                                                                                                                                                      || not (Is_a(None, (List.hd y).0) && y <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                                                                                                                                                                      expansions:
                                                                                                                                                                                      []
                                                                                                                                                                                      rewrite_steps:
                                                                                                                                                                                        forward_chaining:
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr:
                                                                                                                                                                                          (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                                                                                                                          (|count.list_1742/server|
                                                                                                                                                                                                            (|g…
                                                                                                                                                                                          expansions:
                                                                                                                                                                                          • unroll
                                                                                                                                                                                            expr:
                                                                                                                                                                                            (|count.list_1742/server| (|get.::.1_1714/server| y_1723/server))
                                                                                                                                                                                            expansions:
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr:
                                                                                                                                                                                              (|count.list_1742/server| y_1723/server)
                                                                                                                                                                                              expansions:
                                                                                                                                                                                              • Unsat
                                                                                                                                                                                              call `match_cols (List.tl y)` from `match_cols y`
                                                                                                                                                                                              original:match_cols y
                                                                                                                                                                                              sub:match_cols (List.tl y)
                                                                                                                                                                                              original ordinal:Ordinal.Int (_cnt y)
                                                                                                                                                                                              sub ordinal:Ordinal.Int (_cnt (List.tl y))
                                                                                                                                                                                              path:[Is_a(None, (List.hd y).1) && not Is_a(None, (List.hd y).0) && y <> []]
                                                                                                                                                                                              proof:
                                                                                                                                                                                              detailed proof
                                                                                                                                                                                              ground_instances:3
                                                                                                                                                                                              definitions:0
                                                                                                                                                                                              inductions:0
                                                                                                                                                                                              search_time:
                                                                                                                                                                                              0.012s
                                                                                                                                                                                              details:
                                                                                                                                                                                              Expand
                                                                                                                                                                                              smt_stats:
                                                                                                                                                                                              num checks:8
                                                                                                                                                                                              arith assert lower:10
                                                                                                                                                                                              arith tableau max rows:5
                                                                                                                                                                                              arith tableau max columns:13
                                                                                                                                                                                              arith pivots:6
                                                                                                                                                                                              rlimit count:6046
                                                                                                                                                                                              mk clause:31
                                                                                                                                                                                              datatype occurs check:22
                                                                                                                                                                                              mk bool var:138
                                                                                                                                                                                              arith assert upper:9
                                                                                                                                                                                              datatype splits:3
                                                                                                                                                                                              decisions:33
                                                                                                                                                                                              arith row summations:15
                                                                                                                                                                                              propagations:77
                                                                                                                                                                                              conflicts:13
                                                                                                                                                                                              arith fixed eqs:5
                                                                                                                                                                                              datatype accessor ax:30
                                                                                                                                                                                              arith conflicts:1
                                                                                                                                                                                              arith num rows:5
                                                                                                                                                                                              arith assert diseq:1
                                                                                                                                                                                              datatype constructor ax:33
                                                                                                                                                                                              num allocs:258459363
                                                                                                                                                                                              final checks:6
                                                                                                                                                                                              added eqs:140
                                                                                                                                                                                              del clause:6
                                                                                                                                                                                              arith eq adapter:9
                                                                                                                                                                                              memory:21.770000
                                                                                                                                                                                              max memory:21.810000
                                                                                                                                                                                              Expand
                                                                                                                                                                                              • start[0.012s]
                                                                                                                                                                                                  let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                                  let (_x_1 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                                  let (_x_2 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                                  let (_x_3 : int) = count.list anon_fun._cnt.1 _x_2 in
                                                                                                                                                                                                  let (_x_4 : (ty_0 option * ty_0 option)) = List.hd _x_2 in
                                                                                                                                                                                                  let (_x_5 : ty_0 option) = _x_4.0 in
                                                                                                                                                                                                  let (_x_6 : bool) = Is_a(None, _x_5) in
                                                                                                                                                                                                  let (_x_7 : bool) = _x_2 <> [] in
                                                                                                                                                                                                  let (_x_8 : ty_0 option) = _x_4.1 in
                                                                                                                                                                                                  let (_x_9 : bool) = Is_a(None, _x_8) in
                                                                                                                                                                                                  let (_x_10 : bool) = not _x_6 && _x_7 in
                                                                                                                                                                                                  Is_a(None, _x_0.1)
                                                                                                                                                                                                  && (not Is_a(None, _x_0.0) && (y <> [] && ((_x_1 >= 0) && (_x_3 >= 0))))
                                                                                                                                                                                                  ==> (not (_x_6 && _x_7)
                                                                                                                                                                                                       && (not (_x_9 && _x_10)
                                                                                                                                                                                                           && not
                                                                                                                                                                                                              ((Option.get _x_5 = Option.get _x_8) && (not _x_9 && _x_10))))
                                                                                                                                                                                                      || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
                                                                                                                                                                                              • simplify
                                                                                                                                                                                                into:
                                                                                                                                                                                                let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                                let (_x_1 : int) = count.list anon_fun._cnt.1 _x_0 in
                                                                                                                                                                                                let (_x_2 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                                let (_x_3 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                                let (_x_4 : (ty_0 option * ty_0 option)) = List.hd _x_0 in
                                                                                                                                                                                                let (_x_5 : ty_0 option) = _x_4.0 in
                                                                                                                                                                                                let (_x_6 : bool) = Is_a(None, _x_5) in
                                                                                                                                                                                                let (_x_7 : bool) = _x_0 <> [] in
                                                                                                                                                                                                let (_x_8 : ty_0 option) = _x_4.1 in
                                                                                                                                                                                                let (_x_9 : bool) = Is_a(None, _x_8) in
                                                                                                                                                                                                let (_x_10 : bool) = not _x_6 in
                                                                                                                                                                                                Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                                                                                                || not
                                                                                                                                                                                                   (Is_a(None, _x_3.1) && not Is_a(None, _x_3.0) && y <> [] && (_x_2 >= 0)
                                                                                                                                                                                                    && (_x_1 >= 0))
                                                                                                                                                                                                || (not (_x_6 && _x_7) && not (_x_9 && _x_10 && _x_7)
                                                                                                                                                                                                    && not ((Option.get _x_5 = Option.get _x_8) && not _x_9 && _x_10 && _x_7))
                                                                                                                                                                                                expansions:
                                                                                                                                                                                                []
                                                                                                                                                                                                rewrite_steps:
                                                                                                                                                                                                  forward_chaining:
                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                    expr:
                                                                                                                                                                                                    (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                                                                                                                                    (|count.list_1742/server|
                                                                                                                                                                                                                      (|g…
                                                                                                                                                                                                    expansions:
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr:
                                                                                                                                                                                                      (|count.list_1742/server| (|get.::.1_1714/server| y_1723/server))
                                                                                                                                                                                                      expansions:
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr:
                                                                                                                                                                                                        (|count.list_1742/server| y_1723/server)
                                                                                                                                                                                                        expansions:
                                                                                                                                                                                                        • Unsat
                                                                                                                                                                                                        call `match_cols (List.tl y)` from `match_cols y`
                                                                                                                                                                                                        original:match_cols y
                                                                                                                                                                                                        sub:match_cols (List.tl y)
                                                                                                                                                                                                        original ordinal:Ordinal.Int (_cnt y)
                                                                                                                                                                                                        sub ordinal:Ordinal.Int (_cnt (List.tl y))
                                                                                                                                                                                                        path:[let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in Option.get _x_0.0 = Option.get _x_0.1 && not Is_a(None, (List.hd y).1) && not Is_a(None, (List.hd y).0) && y <> []]
                                                                                                                                                                                                        proof:
                                                                                                                                                                                                        detailed proof
                                                                                                                                                                                                        ground_instances:3
                                                                                                                                                                                                        definitions:0
                                                                                                                                                                                                        inductions:0
                                                                                                                                                                                                        search_time:
                                                                                                                                                                                                        0.016s
                                                                                                                                                                                                        details:
                                                                                                                                                                                                        Expand
                                                                                                                                                                                                        smt_stats:
                                                                                                                                                                                                        num checks:8
                                                                                                                                                                                                        arith assert lower:10
                                                                                                                                                                                                        arith tableau max rows:5
                                                                                                                                                                                                        arith tableau max columns:13
                                                                                                                                                                                                        arith pivots:6
                                                                                                                                                                                                        rlimit count:3045
                                                                                                                                                                                                        mk clause:31
                                                                                                                                                                                                        datatype occurs check:22
                                                                                                                                                                                                        mk bool var:141
                                                                                                                                                                                                        arith assert upper:9
                                                                                                                                                                                                        datatype splits:3
                                                                                                                                                                                                        decisions:33
                                                                                                                                                                                                        arith row summations:15
                                                                                                                                                                                                        propagations:77
                                                                                                                                                                                                        conflicts:13
                                                                                                                                                                                                        arith fixed eqs:5
                                                                                                                                                                                                        datatype accessor ax:33
                                                                                                                                                                                                        arith conflicts:1
                                                                                                                                                                                                        arith num rows:5
                                                                                                                                                                                                        arith assert diseq:1
                                                                                                                                                                                                        datatype constructor ax:33
                                                                                                                                                                                                        num allocs:234000381
                                                                                                                                                                                                        final checks:6
                                                                                                                                                                                                        added eqs:145
                                                                                                                                                                                                        del clause:6
                                                                                                                                                                                                        arith eq adapter:9
                                                                                                                                                                                                        memory:21.810000
                                                                                                                                                                                                        max memory:21.810000
                                                                                                                                                                                                        Expand
                                                                                                                                                                                                        • start[0.016s]
                                                                                                                                                                                                            let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                                            let (_x_1 : ty_0 option) = _x_0.0 in
                                                                                                                                                                                                            let (_x_2 : ty_0 option) = _x_0.1 in
                                                                                                                                                                                                            let (_x_3 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                                            let (_x_4 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                                            let (_x_5 : int) = count.list anon_fun._cnt.1 _x_4 in
                                                                                                                                                                                                            let (_x_6 : (ty_0 option * ty_0 option)) = List.hd _x_4 in
                                                                                                                                                                                                            let (_x_7 : ty_0 option) = _x_6.0 in
                                                                                                                                                                                                            let (_x_8 : bool) = Is_a(None, _x_7) in
                                                                                                                                                                                                            let (_x_9 : bool) = _x_4 <> [] in
                                                                                                                                                                                                            let (_x_10 : ty_0 option) = _x_6.1 in
                                                                                                                                                                                                            let (_x_11 : bool) = Is_a(None, _x_10) in
                                                                                                                                                                                                            let (_x_12 : bool) = not _x_8 && _x_9 in
                                                                                                                                                                                                            (Option.get _x_1 = Option.get _x_2)
                                                                                                                                                                                                            && (not Is_a(None, _x_2)
                                                                                                                                                                                                                && (not Is_a(None, _x_1) && (y <> [] && ((_x_3 >= 0) && (_x_5 >= 0)))))
                                                                                                                                                                                                            ==> (not (_x_8 && _x_9)
                                                                                                                                                                                                                 && (not (_x_11 && _x_12)
                                                                                                                                                                                                                     && not
                                                                                                                                                                                                                        ((Option.get _x_7 = Option.get _x_10) && (not _x_11 && _x_12))))
                                                                                                                                                                                                                || Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_3)
                                                                                                                                                                                                        • simplify
                                                                                                                                                                                                          into:
                                                                                                                                                                                                          let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in
                                                                                                                                                                                                          let (_x_1 : int) = count.list anon_fun._cnt.1 _x_0 in
                                                                                                                                                                                                          let (_x_2 : int) = count.list anon_fun._cnt.1 y in
                                                                                                                                                                                                          let (_x_3 : (ty_0 option * ty_0 option)) = List.hd _x_0 in
                                                                                                                                                                                                          let (_x_4 : ty_0 option) = _x_3.0 in
                                                                                                                                                                                                          let (_x_5 : bool) = Is_a(None, _x_4) in
                                                                                                                                                                                                          let (_x_6 : bool) = _x_0 <> [] in
                                                                                                                                                                                                          let (_x_7 : ty_0 option) = _x_3.1 in
                                                                                                                                                                                                          let (_x_8 : bool) = Is_a(None, _x_7) in
                                                                                                                                                                                                          let (_x_9 : bool) = not _x_5 in
                                                                                                                                                                                                          let (_x_10 : (ty_0 option * ty_0 option)) = List.hd y in
                                                                                                                                                                                                          let (_x_11 : ty_0 option) = _x_10.0 in
                                                                                                                                                                                                          let (_x_12 : ty_0 option) = _x_10.1 in
                                                                                                                                                                                                          Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
                                                                                                                                                                                                          || (not (_x_5 && _x_6) && not (_x_8 && _x_9 && _x_6)
                                                                                                                                                                                                              && not ((Option.get _x_4 = Option.get _x_7) && not _x_8 && _x_9 && _x_6))
                                                                                                                                                                                                          || not
                                                                                                                                                                                                             ((Option.get _x_11 = Option.get _x_12) && not Is_a(None, _x_12)
                                                                                                                                                                                                              && not Is_a(None, _x_11) && y <> [] && (_x_2 >= 0) && (_x_1 >= 0))
                                                                                                                                                                                                          expansions:
                                                                                                                                                                                                          []
                                                                                                                                                                                                          rewrite_steps:
                                                                                                                                                                                                            forward_chaining:
                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                              expr:
                                                                                                                                                                                                              (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                                                                                                                                              (|count.list_1742/server|
                                                                                                                                                                                                                                (|g…
                                                                                                                                                                                                              expansions:
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr:
                                                                                                                                                                                                                (|count.list_1742/server| (|get.::.1_1714/server| y_1723/server))
                                                                                                                                                                                                                expansions:
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr:
                                                                                                                                                                                                                  (|count.list_1742/server| y_1723/server)
                                                                                                                                                                                                                  expansions:
                                                                                                                                                                                                                  • Unsat
                                                                                                                                                                                                                  termination proof

                                                                                                                                                                                                                  Termination proof

                                                                                                                                                                                                                  call `match_rows (List.tl x)` from `match_rows x`
                                                                                                                                                                                                                  original:match_rows x
                                                                                                                                                                                                                  sub:match_rows (List.tl x)
                                                                                                                                                                                                                  original ordinal:Ordinal.Int (_cnt x)
                                                                                                                                                                                                                  sub ordinal:Ordinal.Int (_cnt (List.tl x))
                                                                                                                                                                                                                  path:[let (_x_0 : (ty_0 option list * ty_0 option list)) = List.hd x in match_cols (zip _x_0.0 _x_0.1) && x <> []]
                                                                                                                                                                                                                  proof:
                                                                                                                                                                                                                  detailed proof
                                                                                                                                                                                                                  ground_instances:3
                                                                                                                                                                                                                  definitions:0
                                                                                                                                                                                                                  inductions:0
                                                                                                                                                                                                                  search_time:
                                                                                                                                                                                                                  0.013s
                                                                                                                                                                                                                  details:
                                                                                                                                                                                                                  Expand
                                                                                                                                                                                                                  smt_stats:
                                                                                                                                                                                                                  arith offset eqs:24
                                                                                                                                                                                                                  num checks:8
                                                                                                                                                                                                                  arith assert lower:59
                                                                                                                                                                                                                  arith tableau max rows:11
                                                                                                                                                                                                                  arith tableau max columns:28
                                                                                                                                                                                                                  arith pivots:19
                                                                                                                                                                                                                  rlimit count:4831
                                                                                                                                                                                                                  mk clause:71
                                                                                                                                                                                                                  datatype occurs check:21
                                                                                                                                                                                                                  mk bool var:198
                                                                                                                                                                                                                  arith assert upper:63
                                                                                                                                                                                                                  datatype splits:7
                                                                                                                                                                                                                  decisions:93
                                                                                                                                                                                                                  arith row summations:23
                                                                                                                                                                                                                  arith bound prop:4
                                                                                                                                                                                                                  propagations:110
                                                                                                                                                                                                                  conflicts:21
                                                                                                                                                                                                                  arith fixed eqs:25
                                                                                                                                                                                                                  datatype accessor ax:18
                                                                                                                                                                                                                  minimized lits:2
                                                                                                                                                                                                                  arith conflicts:6
                                                                                                                                                                                                                  arith num rows:11
                                                                                                                                                                                                                  arith assert diseq:8
                                                                                                                                                                                                                  datatype constructor ax:39
                                                                                                                                                                                                                  num allocs:312734263
                                                                                                                                                                                                                  final checks:5
                                                                                                                                                                                                                  added eqs:205
                                                                                                                                                                                                                  del clause:39
                                                                                                                                                                                                                  arith eq adapter:49
                                                                                                                                                                                                                  memory:22.180000
                                                                                                                                                                                                                  max memory:22.180000
                                                                                                                                                                                                                  Expand
                                                                                                                                                                                                                  • start[0.013s]
                                                                                                                                                                                                                      let (_x_0 : (ty_0 option list * ty_0 option list)) = List.hd x in
                                                                                                                                                                                                                      let (_x_1 : int) = count.list anon_fun._cnt.1 x in
                                                                                                                                                                                                                      let (_x_2 : (ty_0 option list * ty_0 option list) list) = List.tl x in
                                                                                                                                                                                                                      let (_x_3 : int) = count.list anon_fun._cnt.1 _x_2 in
                                                                                                                                                                                                                      let (_x_4 : (ty_0 option list * ty_0 option list)) = List.hd _x_2 in
                                                                                                                                                                                                                      match_cols (zip _x_0.0 _x_0.1) && (x <> [] && ((_x_1 >= 0) && (_x_3 >= 0)))
                                                                                                                                                                                                                      ==> not (match_cols (zip _x_4.0 _x_4.1) && _x_2 <> [])
                                                                                                                                                                                                                          || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
                                                                                                                                                                                                                  • simplify
                                                                                                                                                                                                                    into:
                                                                                                                                                                                                                    let (_x_0 : (ty_0 option list * ty_0 option list) list) = List.tl x in
                                                                                                                                                                                                                    let (_x_1 : (ty_0 option list * ty_0 option list)) = List.hd _x_0 in
                                                                                                                                                                                                                    let (_x_2 : int) = count.list anon_fun._cnt.1 _x_0 in
                                                                                                                                                                                                                    let (_x_3 : int) = count.list anon_fun._cnt.1 x in
                                                                                                                                                                                                                    let (_x_4 : (ty_0 option list * ty_0 option list)) = List.hd x in
                                                                                                                                                                                                                    not (match_cols (zip _x_1.0 _x_1.1) && _x_0 <> [])
                                                                                                                                                                                                                    || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3)
                                                                                                                                                                                                                    || not
                                                                                                                                                                                                                       (match_cols (zip _x_4.0 _x_4.1) && x <> [] && (_x_3 >= 0) && (_x_2 >= 0))
                                                                                                                                                                                                                    expansions:
                                                                                                                                                                                                                    []
                                                                                                                                                                                                                    rewrite_steps:
                                                                                                                                                                                                                      forward_chaining:
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr:
                                                                                                                                                                                                                        (|Ordinal.<<| (|Ordinal.Int_79/boot|
                                                                                                                                                                                                                                        (|count.list_2058/server|
                                                                                                                                                                                                                                          (|g…
                                                                                                                                                                                                                        expansions:
                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                          expr:
                                                                                                                                                                                                                          (|count.list_2058/server| (|get.::.1_2012/server| x_2043/server))
                                                                                                                                                                                                                          expansions:
                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                            expr:
                                                                                                                                                                                                                            (|count.list_2058/server| x_2043/server)
                                                                                                                                                                                                                            expansions:
                                                                                                                                                                                                                            • Unsat

                                                                                                                                                                                                                            The Satisfaction of Subrepticiously Solving Sudokus using Satisfiability

                                                                                                                                                                                                                            We can now, finally, ask Imandra to find a sudoku that satisfies all the constraints defined before!

                                                                                                                                                                                                                            NOTE: we have to use [@@blast] because this problem is prone to combinatorial explosion and is too hard for Imandra's default unrolling algorithm.

                                                                                                                                                                                                                            In [10]:
                                                                                                                                                                                                                            instance (fun (s:sudoku) -> is_valid_sudoku s && is_solution_of s the_problem) [@@blast] ;;
                                                                                                                                                                                                                            
                                                                                                                                                                                                                            Out[10]:
                                                                                                                                                                                                                            - : sudoku -> bool = <fun>
                                                                                                                                                                                                                            module CX : sig val s : sudoku end
                                                                                                                                                                                                                            
                                                                                                                                                                                                                            Instance (after 283 steps, 1.511s):
                                                                                                                                                                                                                            let s : sudoku =
                                                                                                                                                                                                                              let (_x_0 : cell option) = Some C8 in
                                                                                                                                                                                                                              let (_x_1 : cell option) = Some C1 in
                                                                                                                                                                                                                              let (_x_2 : cell option) = Some C2 in
                                                                                                                                                                                                                              let (_x_3 : cell option) = Some C7 in
                                                                                                                                                                                                                              let (_x_4 : cell option) = Some C5 in
                                                                                                                                                                                                                              let (_x_5 : cell option) = Some C3 in
                                                                                                                                                                                                                              let (_x_6 : cell option) = Some C6 in
                                                                                                                                                                                                                              let (_x_7 : cell option) = Some C4 in
                                                                                                                                                                                                                              let (_x_8 : cell option) = Some C9 in
                                                                                                                                                                                                                              {rows =
                                                                                                                                                                                                                               [[_x_0; _x_1; _x_2; _x_3; _x_4; _x_5; _x_6; _x_7; _x_8];
                                                                                                                                                                                                                                [_x_8; _x_7; _x_5; _x_6; _x_0; _x_2; _x_1; _x_3; _x_4];
                                                                                                                                                                                                                                [_x_6; _x_3; _x_4; _x_7; _x_8; _x_1; _x_2; _x_0; _x_5];
                                                                                                                                                                                                                                [_x_1; _x_4; _x_7; _x_2; _x_5; _x_3; _x_0; _x_8; _x_6];
                                                                                                                                                                                                                                [_x_5; _x_6; _x_8; _x_0; _x_7; _x_4; _x_3; _x_2; _x_1];
                                                                                                                                                                                                                                [_x_2; _x_0; _x_3; _x_1; _x_6; _x_8; _x_4; _x_5; _x_7];
                                                                                                                                                                                                                                [_x_4; _x_2; _x_1; _x_8; _x_3; _x_7; _x_5; _x_6; _x_0];
                                                                                                                                                                                                                                [_x_7; _x_5; _x_0; _x_4; _x_2; _x_6; _x_8; _x_1; _x_3];
                                                                                                                                                                                                                                [_x_3; _x_8; _x_6; _x_5; _x_1; _x_0; _x_7; _x_4; _x_2]]}
                                                                                                                                                                                                                            
                                                                                                                                                                                                                            Instance

                                                                                                                                                                                                                            Let us look at the initial sudoku and its solution side to side:

                                                                                                                                                                                                                            In [11]:
                                                                                                                                                                                                                            Imandra.display (Document.tbl [[doc_of_sudoku the_problem; Document.s "-->"; doc_of_sudoku CX.s]]) ;;
                                                                                                                                                                                                                            
                                                                                                                                                                                                                            Out[11]:
                                                                                                                                                                                                                            - : unit = ()
                                                                                                                                                                                                                            
                                                                                                                                                                                                                            8········
                                                                                                                                                                                                                            ··36·····
                                                                                                                                                                                                                            ·7··9·2··
                                                                                                                                                                                                                            ·5···7···
                                                                                                                                                                                                                            ····457··
                                                                                                                                                                                                                            ···1···3·
                                                                                                                                                                                                                            ··1····68
                                                                                                                                                                                                                            ··85···1·
                                                                                                                                                                                                                            ·9····4··
                                                                                                                                                                                                                            -->
                                                                                                                                                                                                                            812753649
                                                                                                                                                                                                                            943682175
                                                                                                                                                                                                                            675491283
                                                                                                                                                                                                                            154237896
                                                                                                                                                                                                                            369845721
                                                                                                                                                                                                                            287169534
                                                                                                                                                                                                                            521974368
                                                                                                                                                                                                                            438526917
                                                                                                                                                                                                                            796318452

                                                                                                                                                                                                                            We can manipulate CX.s easily, directly in OCaml:

                                                                                                                                                                                                                            In [12]:
                                                                                                                                                                                                                            let transpose_sudoku (s:sudoku) : sudoku = {rows = transpose s.rows};;
                                                                                                                                                                                                                            
                                                                                                                                                                                                                            transpose_sudoku CX.s;;
                                                                                                                                                                                                                            
                                                                                                                                                                                                                            Out[12]:
                                                                                                                                                                                                                            val transpose_sudoku : sudoku -> sudoku = <fun>
                                                                                                                                                                                                                            - : sudoku = <document>
                                                                                                                                                                                                                            
                                                                                                                                                                                                                            896132547
                                                                                                                                                                                                                            147568239
                                                                                                                                                                                                                            235497186
                                                                                                                                                                                                                            764281953
                                                                                                                                                                                                                            589346721
                                                                                                                                                                                                                            321759468
                                                                                                                                                                                                                            612875394
                                                                                                                                                                                                                            478923615
                                                                                                                                                                                                                            953614872