[micromega] Simplex uses alternatively Gomory cuts and case splits

7 files changed, 577 insertions, 654 deletions

diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index dc36372d3d..f1ae07892e 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -1134,7 +1134,6 @@ let rev_concat l =
   in
   conc [] l
 
-
 let pre_process sys =
   let sys = normalise sys in
   let bnd1 = bound_monomials sys in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a8f88df079..08edd1fc5e 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -197,6 +197,7 @@ let coq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type")
 let coq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof")
 let coq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof")
 let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof")
+let coq_splitProof = lazy (constr_of_ref "micromega.ZArithProof.SplitProof")
 let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof")
 let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof")
 let coq_IsProp = lazy (constr_of_ref "micromega.kind.isProp")
@@ -1341,6 +1342,12 @@ let rec dump_proof_term = function
     EConstr.mkApp
       ( Lazy.force coq_cutProof
       , [|dump_psatz coq_Z dump_z cone; dump_proof_term prf|] )
+  | Micromega.SplitProof (p, prf1, prf2) ->
+    EConstr.mkApp
+      ( Lazy.force coq_splitProof
+      , [| dump_pol (Lazy.force coq_Z) dump_z p
+         ; dump_proof_term prf1
+         ; dump_proof_term prf2 |] )
   | Micromega.EnumProof (c1, c2, prfs) ->
     EConstr.mkApp
       ( Lazy.force coq_enumProof
@@ -1364,6 +1371,7 @@ let rec size_of_pf = function
   | Micromega.DoneProof -> 1
   | Micromega.RatProof (p, a) -> size_of_pf a + size_of_psatz p
   | Micromega.CutProof (p, a) -> size_of_pf a + size_of_psatz p
+  | Micromega.SplitProof (_, p1, p2) -> size_of_pf p1 + size_of_pf p2
   | Micromega.EnumProof (p1, p2, l) ->
     size_of_psatz p1 + size_of_psatz p2
     + List.fold_left (fun acc p -> size_of_pf p + acc) 0 l
@@ -1382,6 +1390,9 @@ let rec pp_proof_term o = function
     Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
   | Micromega.CutProof (cone, rst) ->
     Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
+  | Micromega.SplitProof (p, p1, p2) ->
+    Printf.fprintf o "S[%a,%a,%a]" (pp_pol pp_z) p pp_proof_term p1
+      pp_proof_term p2
   | Micromega.EnumProof (c1, c2, rst) ->
     Printf.fprintf o "EP[%a,%a,%a]" (pp_psatz pp_z) c1 (pp_psatz pp_z) c2
       (pp_list "[" "]" pp_proof_term)
@@ -2196,6 +2207,7 @@ let hyps_of_pt pt =
     | Mc.DoneProof -> acc
     | Mc.RatProof (c, pt) -> xhyps (base + 1) pt (xhyps_of_cone base acc c)
     | Mc.CutProof (c, pt) -> xhyps (base + 1) pt (xhyps_of_cone base acc c)
+    | Mc.SplitProof (p, p1, p2) -> xhyps (base + 1) p1 (xhyps (base + 1) p2 acc)
     | Mc.EnumProof (c1, c2, l) ->
       let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in
       List.fold_left (fun s x -> xhyps (base + 1) x s) s l
@@ -2212,6 +2224,8 @@ let compact_pt pt f =
       Mc.RatProof (compact_cone c (translate ofset), compact_pt (ofset + 1) pt)
     | Mc.CutProof (c, pt) ->
       Mc.CutProof (compact_cone c (translate ofset), compact_pt (ofset + 1) pt)
+    | Mc.SplitProof (p, p1, p2) ->
+      Mc.SplitProof (p, compact_pt (ofset + 1) p1, compact_pt (ofset + 1) p2)
     | Mc.EnumProof (c1, c2, l) ->
       Mc.EnumProof
         ( compact_cone c1 (translate ofset)
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index 1556ec31b5..57de80bd24 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -2142,6 +2142,11 @@ let zWeakChecker =
 let psub1 =
   psub0 Z0 Z.add Z.sub Z.opp zeq_bool
 
+(** val popp1 : z pol -> z pol **)
+
+let popp1 =
+  popp0 Z.opp
+
 (** val padd1 : z pol -> z pol -> z pol **)
 
 let padd1 =
@@ -2235,6 +2240,7 @@ type zArithProof =
 | DoneProof
 | RatProof of zWitness * zArithProof
 | CutProof of zWitness * zArithProof
+| SplitProof of z polC * zArithProof * zArithProof
 | EnumProof of zWitness * zWitness * zArithProof list
 | ExProof of positive * zArithProof
 
@@ -2346,6 +2352,15 @@ let rec zChecker l = function
       | Some cp -> zChecker ((nformula_of_cutting_plane cp)::l) pf0
       | None -> true)
    | None -> false)
+| SplitProof (p, pf1, pf2) ->
+  (match genCuttingPlane (p,NonStrict) with
+   | Some cp1 ->
+     (match genCuttingPlane ((popp1 p),NonStrict) with
+      | Some cp2 ->
+        (&&) (zChecker ((nformula_of_cutting_plane cp1)::l) pf1)
+          (zChecker ((nformula_of_cutting_plane cp2)::l) pf2)
+      | None -> false)
+   | None -> false)
 | EnumProof (w1, w2, pf0) ->
   (match eval_Psatz0 l w1 with
    | Some f1 ->
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 53f62e0f5b..f75d8880c6 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -1,942 +1,740 @@
+
 type __ = Obj.t
-type unit0 = Tt
+
+type unit0 =
+| Tt
 
 val negb : bool -> bool
 
-type nat = O | S of nat
-type ('a, 'b) sum = Inl of 'a | Inr of 'b
+type nat =
+| O
+| S of nat
+
+type ('a, 'b) sum =
+| Inl of 'a
+| Inr of 'b
+
+val fst : ('a1 * 'a2) -> 'a1
+
+val snd : ('a1 * 'a2) -> 'a2
 
-val fst : 'a1 * 'a2 -> 'a1
-val snd : 'a1 * 'a2 -> 'a2
 val app : 'a1 list -> 'a1 list -> 'a1 list
 
-type comparison = Eq | Lt | Gt
+type comparison =
+| Eq
+| Lt
+| Gt
 
 val compOpp : comparison -> comparison
+
 val add : nat -> nat -> nat
+
 val nth : nat -> 'a1 list -> 'a1 -> 'a1
+
 val rev_append : 'a1 list -> 'a1 list -> 'a1 list
+
 val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
-val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1
-val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
 
-type positive = XI of positive | XO of positive | XH
-type n = N0 | Npos of positive
-type z = Z0 | Zpos of positive | Zneg of positive
+val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1
 
-module Pos : sig
-  type mask = IsNul | IsPos of positive | IsNeg
-end
+val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
 
-module Coq_Pos : sig
+type positive =
+| XI of positive
+| XO of positive
+| XH
+
+type n =
+| N0
+| Npos of positive
+
+type z =
+| Z0
+| Zpos of positive
+| Zneg of positive
+
+module Pos :
+ sig
+  type mask =
+  | IsNul
+  | IsPos of positive
+  | IsNeg
+ end
+
+module Coq_Pos :
+ sig
   val succ : positive -> positive
+
   val add : positive -> positive -> positive
+
   val add_carry : positive -> positive -> positive
+
   val pred_double : positive -> positive
 
-  type mask = Pos.mask = IsNul | IsPos of positive | IsNeg
+  type mask = Pos.mask =
+  | IsNul
+  | IsPos of positive
+  | IsNeg
 
   val succ_double_mask : mask -> mask
+
   val double_mask : mask -> mask
+
   val double_pred_mask : positive -> mask
+
   val sub_mask : positive -> positive -> mask
+
   val sub_mask_carry : positive -> positive -> mask
+
   val sub : positive -> positive -> positive
+
   val mul : positive -> positive -> positive
+
   val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1
+
   val size_nat : positive -> nat
+
   val compare_cont : comparison -> positive -> positive -> comparison
+
   val compare : positive -> positive -> comparison
+
   val max : positive -> positive -> positive
+
   val leb : positive -> positive -> bool
+
   val gcdn : nat -> positive -> positive -> positive
+
   val gcd : positive -> positive -> positive
+
   val of_succ_nat : nat -> positive
-end
+ end
 
-module N : sig
+module N :
+ sig
   val of_nat : nat -> n
-end
+ end
 
 val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
 
-module Z : sig
+module Z :
+ sig
   val double : z -> z
+
   val succ_double : z -> z
+
   val pred_double : z -> z
+
   val pos_sub : positive -> positive -> z
+
   val add : z -> z -> z
+
   val opp : z -> z
+
   val sub : z -> z -> z
+
   val mul : z -> z -> z
+
   val pow_pos : z -> positive -> z
+
   val pow : z -> z -> z
+
   val compare : z -> z -> comparison
+
   val leb : z -> z -> bool
+
   val ltb : z -> z -> bool
+
   val gtb : z -> z -> bool
+
   val max : z -> z -> z
+
   val abs : z -> z
+
   val to_N : z -> n
+
   val of_nat : nat -> z
+
   val of_N : n -> z
+
   val pos_div_eucl : positive -> z -> z * z
+
   val div_eucl : z -> z -> z * z
+
   val div : z -> z -> z
+
   val gcd : z -> z -> z
-end
+ end
 
 val zeq_bool : z -> z -> bool
 
 type 'c pExpr =
-  | PEc of 'c
-  | PEX of positive
-  | PEadd of 'c pExpr * 'c pExpr
-  | PEsub of 'c pExpr * 'c pExpr
-  | PEmul of 'c pExpr * 'c pExpr
-  | PEopp of 'c pExpr
-  | PEpow of 'c pExpr * n
+| PEc of 'c
+| PEX of positive
+| PEadd of 'c pExpr * 'c pExpr
+| PEsub of 'c pExpr * 'c pExpr
+| PEmul of 'c pExpr * 'c pExpr
+| PEopp of 'c pExpr
+| PEpow of 'c pExpr * n
 
 type 'c pol =
-  | Pc of 'c
-  | Pinj of positive * 'c pol
-  | PX of 'c pol * positive * 'c pol
+| Pc of 'c
+| Pinj of positive * 'c pol
+| PX of 'c pol * positive * 'c pol
 
 val p0 : 'a1 -> 'a1 pol
+
 val p1 : 'a1 -> 'a1 pol
+
 val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool
+
 val mkPinj : positive -> 'a1 pol -> 'a1 pol
+
 val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol
 
-val mkPX :
-  'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
+val mkPX : 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
 
 val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol
+
 val mkX : 'a1 -> 'a1 -> 'a1 pol
+
 val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
+
 val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
+
 val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
 
 val paddI :
-     ('a1 -> 'a1 -> 'a1)
-  -> ('a1 pol -> 'a1 pol -> 'a1 pol)
-  -> 'a1 pol
-  -> positive
-  -> 'a1 pol
-  -> 'a1 pol
+  ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
 
 val psubI :
-     ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1)
-  -> ('a1 pol -> 'a1 pol -> 'a1 pol)
-  -> 'a1 pol
-  -> positive
-  -> 'a1 pol
-  -> 'a1 pol
+  ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive ->
+  'a1 pol -> 'a1 pol
 
 val paddX :
-     'a1
-  -> ('a1 -> 'a1 -> bool)
-  -> ('a1 pol -> 'a1 pol -> 'a1 pol)
-  -> 'a1 pol
-  -> positive
-  -> 'a1 pol
+  'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol
   -> 'a1 pol
 
 val psubX :
-     'a1
-  -> ('a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> ('a1 pol -> 'a1 pol -> 'a1 pol)
-  -> 'a1 pol
-  -> positive
-  -> 'a1 pol
-  -> 'a1 pol
+  'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol ->
+  positive -> 'a1 pol -> 'a1 pol
 
-val padd :
-     'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 pol
-  -> 'a1 pol
-  -> 'a1 pol
+val padd : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
 
 val psub :
-     'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 pol
-  -> 'a1 pol
-  -> 'a1 pol
+  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1
+  pol -> 'a1 pol -> 'a1 pol
 
-val pmulC_aux :
-     'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 pol
-  -> 'a1
-  -> 'a1 pol
+val pmulC_aux : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
 
-val pmulC :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 pol
-  -> 'a1
-  -> 'a1 pol
+val pmulC : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
 
 val pmulI :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> ('a1 pol -> 'a1 pol -> 'a1 pol)
-  -> 'a1 pol
-  -> positive
-  -> 'a1 pol
-  -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) ->
+  'a1 pol -> positive -> 'a1 pol -> 'a1 pol
 
 val pmul :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 pol
-  -> 'a1 pol
-  -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1
+  pol -> 'a1 pol
 
 val psquare :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 pol
-  -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1
+  pol
 
 val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
 
 val ppow_pos :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> ('a1 pol -> 'a1 pol)
-  -> 'a1 pol
-  -> 'a1 pol
-  -> positive
-  -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol ->
+  'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
 
 val ppow_N :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> ('a1 pol -> 'a1 pol)
-  -> 'a1 pol
-  -> n
-  -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol ->
+  'a1 pol) -> 'a1 pol -> n -> 'a1 pol
 
 val norm_aux :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 pExpr
-  -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) ->
+  ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
 
-type kind = IsProp | IsBool
+type kind =
+| IsProp
+| IsBool
 
 type ('tA, 'tX, 'aA, 'aF) gFormula =
-  | TT of kind
-  | FF of kind
-  | X of kind * 'tX
-  | A of kind * 'tA * 'aA
-  | AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-  | OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-  | NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula
-  | IMPL of
-      kind
-      * ('tA, 'tX, 'aA, 'aF) gFormula
-      * 'aF option
-      * ('tA, 'tX, 'aA, 'aF) gFormula
-  | IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-  | EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+| TT of kind
+| FF of kind
+| X of kind * 'tX
+| A of kind * 'tA * 'aA
+| AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+| OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+| NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula
+| IMPL of kind * ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula
+| IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+| EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
 
 val mapX :
-     (kind -> 'a2 -> 'a2)
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) gFormula
-  -> ('a1, 'a2, 'a3, 'a4) gFormula
+  (kind -> 'a2 -> 'a2) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula
 
-val foldA :
-  ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5
+val foldA : ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5
 
 val cons_id : 'a1 option -> 'a1 list -> 'a1 list
+
 val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list
+
 val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list
 
 type rtyp = __
+
 type eKind = __
+
 type 'a bFormula = ('a, eKind, unit0, unit0) gFormula
 
 val map_bformula :
-     kind
-  -> ('a1 -> 'a2)
-  -> ('a1, 'a3, 'a4, 'a5) gFormula
-  -> ('a2, 'a3, 'a4, 'a5) gFormula
+  kind -> ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) gFormula
 
 type ('x, 'annot) clause = ('x * 'annot) list
+
 type ('x, 'annot) cnf = ('x, 'annot) clause list
 
 val cnf_tt : ('a1, 'a2) cnf
+
 val cnf_ff : ('a1, 'a2) cnf
 
 val add_term :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> 'a1 * 'a2
-  -> ('a1, 'a2) clause
-  -> ('a1, 'a2) clause option
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> ('a1, 'a2)
+  clause option
 
 val or_clause :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> ('a1, 'a2) clause
-  -> ('a1, 'a2) clause
-  -> ('a1, 'a2) clause option
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) clause -> ('a1,
+  'a2) clause option
 
 val xor_clause_cnf :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> ('a1, 'a2) clause
-  -> ('a1, 'a2) cnf
-  -> ('a1, 'a2) cnf
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, 'a2)
+  cnf
 
 val or_clause_cnf :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> ('a1, 'a2) clause
-  -> ('a1, 'a2) cnf
-  -> ('a1, 'a2) cnf
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, 'a2)
+  cnf
 
 val or_cnf :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> ('a1, 'a2) cnf
-  -> ('a1, 'a2) cnf
-  -> ('a1, 'a2) cnf
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
 
 val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
 
 type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula
 
 val is_cnf_tt : ('a1, 'a2) cnf -> bool
+
 val is_cnf_ff : ('a1, 'a2) cnf -> bool
+
 val and_cnf_opt : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
 
 val or_cnf_opt :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> ('a1, 'a2) cnf
-  -> ('a1, 'a2) cnf
-  -> ('a1, 'a2) cnf
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
 
 val mk_and :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
-  -> kind
-  -> bool
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula ->
+  ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula
   -> ('a2, 'a3) cnf
 
 val mk_or :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
-  -> kind
-  -> bool
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula ->
+  ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula
   -> ('a2, 'a3) cnf
 
 val mk_impl :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
-  -> kind
-  -> bool
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula ->
+  ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula
   -> ('a2, 'a3) cnf
 
 val mk_iff :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
-  -> kind
-  -> bool
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula ->
+  ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula
   -> ('a2, 'a3) cnf
 
 val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option
 
 val xcnf :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
-  -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
-  -> bool
-  -> kind
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a2, 'a3) cnf
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 ->
+  ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
 
 val radd_term :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> 'a1 * 'a2
-  -> ('a1, 'a2) clause
-  -> (('a1, 'a2) clause, 'a2 list) sum
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> (('a1, 'a2)
+  clause, 'a2 list) sum
 
 val ror_clause :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> ('a1 * 'a2) list
-  -> ('a1, 'a2) clause
-  -> (('a1, 'a2) clause, 'a2 list) sum
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause -> (('a1,
+  'a2) clause, 'a2 list) sum
 
 val xror_clause_cnf :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> ('a1 * 'a2) list
-  -> ('a1, 'a2) clause list
-  -> ('a1, 'a2) clause list * 'a2 list
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1,
+  'a2) clause list * 'a2 list
 
 val ror_clause_cnf :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> ('a1 * 'a2) list
-  -> ('a1, 'a2) clause list
-  -> ('a1, 'a2) clause list * 'a2 list
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1,
+  'a2) clause list * 'a2 list
 
 val ror_cnf :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> ('a1, 'a2) clause list
-  -> ('a1, 'a2) clause list
-  -> ('a1, 'a2) cnf * 'a2 list
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list ->
+  ('a1, 'a2) cnf * 'a2 list
 
 val ror_cnf_opt :
-     ('a1 -> bool)
-  -> ('a1 -> 'a1 -> 'a1 option)
-  -> ('a1, 'a2) cnf
-  -> ('a1, 'a2) cnf
-  -> ('a1, 'a2) cnf * 'a2 list
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2)
+  cnf * 'a2 list
 
 val ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 list
 
 val rxcnf_and :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> (   bool
-      -> kind
-      -> ('a1, 'a3, 'a4, 'a5) tFormula
-      -> ('a2, 'a3) cnf * 'a3 list)
-  -> bool
-  -> kind
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a2, 'a3) cnf * 'a3 list
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula ->
+  ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4,
+  'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list
 
 val rxcnf_or :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> (   bool
-      -> kind
-      -> ('a1, 'a3, 'a4, 'a5) tFormula
-      -> ('a2, 'a3) cnf * 'a3 list)
-  -> bool
-  -> kind
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a2, 'a3) cnf * 'a3 list
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula ->
+  ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4,
+  'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list
 
 val rxcnf_impl :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> (   bool
-      -> kind
-      -> ('a1, 'a3, 'a4, 'a5) tFormula
-      -> ('a2, 'a3) cnf * 'a3 list)
-  -> bool
-  -> kind
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a2, 'a3) cnf * 'a3 list
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula ->
+  ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4,
+  'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list
 
 val rxcnf_iff :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> (   bool
-      -> kind
-      -> ('a1, 'a3, 'a4, 'a5) tFormula
-      -> ('a2, 'a3) cnf * 'a3 list)
-  -> bool
-  -> kind
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a2, 'a3) cnf * 'a3 list
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula ->
+  ('a2, 'a3) cnf * 'a3 list) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4,
+  'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list
 
 val rxcnf :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
-  -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
-  -> bool
-  -> kind
-  -> ('a1, 'a3, 'a4, 'a5) tFormula
-  -> ('a2, 'a3) cnf * 'a3 list
-
-type ('term, 'annot, 'tX) to_constrT =
-  { mkTT : kind -> 'tX
-  ; mkFF : kind -> 'tX
-  ; mkA : kind -> 'term -> 'annot -> 'tX
-  ; mkAND : kind -> 'tX -> 'tX -> 'tX
-  ; mkOR : kind -> 'tX -> 'tX -> 'tX
-  ; mkIMPL : kind -> 'tX -> 'tX -> 'tX
-  ; mkIFF : kind -> 'tX -> 'tX -> 'tX
-  ; mkNOT : kind -> 'tX -> 'tX
-  ; mkEQ : 'tX -> 'tX -> 'tX }
-
-val aformula :
-  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 ->
+  ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list
+
+type ('term, 'annot, 'tX) to_constrT = { mkTT : (kind -> 'tX); mkFF : (kind -> 'tX);
+                                         mkA : (kind -> 'term -> 'annot -> 'tX);
+                                         mkAND : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkOR : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkIMPL : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkIFF : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkNOT : (kind -> 'tX -> 'tX); mkEQ : ('tX -> 'tX -> 'tX) }
+
+val aformula : ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3
 
 val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option
 
 val abs_and :
-     ('a1, 'a2, 'a3) to_constrT
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> (   kind
-      -> ('a1, 'a2, 'a3, 'a4) tFormula
-      -> ('a1, 'a2, 'a3, 'a4) tFormula
-      -> ('a1, 'a2, 'a3, 'a4) tFormula)
-  -> ('a1, 'a3, 'a2, 'a4) gFormula
+  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4)
+  tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2,
+  'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
 
 val abs_or :
-     ('a1, 'a2, 'a3) to_constrT
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> (   kind
-      -> ('a1, 'a2, 'a3, 'a4) tFormula
-      -> ('a1, 'a2, 'a3, 'a4) tFormula
-      -> ('a1, 'a2, 'a3, 'a4) tFormula)
-  -> ('a1, 'a3, 'a2, 'a4) gFormula
+  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4)
+  tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2,
+  'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
 
 val abs_not :
-     ('a1, 'a2, 'a3) to_constrT
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula)
-  -> ('a1, 'a3, 'a2, 'a4) gFormula
+  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3,
+  'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
 
 val mk_arrow :
-     'a4 option
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  'a4 option -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2,
+  'a3, 'a4) tFormula
 
 val abst_simpl :
-     ('a1, 'a2, 'a3) to_constrT
-  -> ('a2 -> bool)
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2,
+  'a3, 'a4) tFormula
 
 val abst_and :
-     ('a1, 'a2, 'a3) to_constrT
-  -> (   bool
-      -> kind
-      -> ('a1, 'a2, 'a3, 'a4) tFormula
-      -> ('a1, 'a2, 'a3, 'a4) tFormula)
-  -> bool
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+  'a4) tFormula) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_or :
-     ('a1, 'a2, 'a3) to_constrT
-  -> (   bool
-      -> kind
-      -> ('a1, 'a2, 'a3, 'a4) tFormula
-      -> ('a1, 'a2, 'a3, 'a4) tFormula)
-  -> bool
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+  'a4) tFormula) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_impl :
-     ('a1, 'a2, 'a3) to_constrT
-  -> (   bool
-      -> kind
-      -> ('a1, 'a2, 'a3, 'a4) tFormula
-      -> ('a1, 'a2, 'a3, 'a4) tFormula)
-  -> bool
-  -> 'a4 option
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+  'a4) tFormula) -> bool -> 'a4 option -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+  'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
-val or_is_X :
-  kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool
+val or_is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool
 
 val abs_iff :
-     ('a1, 'a2, 'a3) to_constrT
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4)
+  tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> kind -> ('a1, 'a2,
+  'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_iff :
-     ('a1, 'a2, 'a3) to_constrT
-  -> ('a2 -> bool)
-  -> (   bool
-      -> kind
-      -> ('a1, 'a2, 'a3, 'a4) tFormula
-      -> ('a1, 'a2, 'a3, 'a4) tFormula)
-  -> bool
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+  ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+  'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_eq :
-     ('a1, 'a2, 'a3) to_constrT
-  -> ('a2 -> bool)
-  -> (   bool
-      -> kind
-      -> ('a1, 'a2, 'a3, 'a4) tFormula
-      -> ('a1, 'a2, 'a3, 'a4) tFormula)
-  -> bool
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+  ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4)
+  tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_form :
-     ('a1, 'a2, 'a3) to_constrT
-  -> ('a2 -> bool)
-  -> bool
-  -> kind
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+  ('a1, 'a2, 'a3, 'a4) tFormula
 
-val cnf_checker :
-  (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool
+val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool
 
 val tauto_checker :
-     ('a2 -> bool)
-  -> ('a2 -> 'a2 -> 'a2 option)
-  -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
-  -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
-  -> (('a2 * 'a3) list -> 'a4 -> bool)
-  -> ('a1, rtyp, 'a3, unit0) gFormula
-  -> 'a4 list
-  -> bool
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 ->
+  ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4
+  list -> bool
 
 val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
+
 val cltb : ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
 
 type 'c polC = 'c pol
-type op1 = Equal | NonEqual | Strict | NonStrict
+
+type op1 =
+| Equal
+| NonEqual
+| Strict
+| NonStrict
+
 type 'c nFormula = 'c polC * op1
 
 val opMult : op1 -> op1 -> op1 option
+
 val opAdd : op1 -> op1 -> op1 option
 
 type 'c psatz =
-  | PsatzIn of nat
-  | PsatzSquare of 'c polC
-  | PsatzMulC of 'c polC * 'c psatz
-  | PsatzMulE of 'c psatz * 'c psatz
-  | PsatzAdd of 'c psatz * 'c psatz
-  | PsatzC of 'c
-  | PsatzZ
+| PsatzIn of nat
+| PsatzSquare of 'c polC
+| PsatzMulC of 'c polC * 'c psatz
+| PsatzMulE of 'c psatz * 'c psatz
+| PsatzAdd of 'c psatz * 'c psatz
+| PsatzC of 'c
+| PsatzZ
 
 val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option
 
-val map_option2 :
-  ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option
+val map_option2 : ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option
 
 val pexpr_times_nformula :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 polC
-  -> 'a1 nFormula
-  -> 'a1 nFormula option
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 polC ->
+  'a1 nFormula -> 'a1 nFormula option
 
 val nformula_times_nformula :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 nFormula
-  -> 'a1 nFormula
-  -> 'a1 nFormula option
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula
+  -> 'a1 nFormula -> 'a1 nFormula option
 
 val nformula_plus_nformula :
-     'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 nFormula
-  -> 'a1 nFormula
-  -> 'a1 nFormula option
+  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula
+  option
 
 val eval_Psatz :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 nFormula list
-  -> 'a1 psatz
-  -> 'a1 nFormula option
-
-val check_inconsistent :
-  'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 ->
+  bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option
+
+val check_inconsistent : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool
 
 val check_normalised_formulas :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 nFormula list
-  -> 'a1 psatz
-  -> bool
-
-type op2 = OpEq | OpNEq | OpLe | OpGe | OpLt | OpGt
-type 't formula = {flhs : 't pExpr; fop : op2; frhs : 't pExpr}
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 ->
+  bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
+
+type op2 =
+| OpEq
+| OpNEq
+| OpLe
+| OpGe
+| OpLt
+| OpGt
+
+type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
 
 val norm :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 pExpr
-  -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) ->
+  ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
 
 val psub0 :
-     'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 pol
-  -> 'a1 pol
-  -> 'a1 pol
+  'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1
+  pol -> 'a1 pol -> 'a1 pol
 
-val padd0 :
-     'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 pol
-  -> 'a1 pol
-  -> 'a1 pol
+val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
 
 val popp0 : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
 
 val normalise :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 formula
-  -> 'a1 nFormula
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) ->
+  ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
 
 val xnormalise : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list
+
 val xnegate : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list
 
 val cnf_of_list :
-     'a1
-  -> ('a1 -> 'a1 -> bool)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 nFormula list
-  -> 'a2
-  -> ('a1 nFormula, 'a2) cnf
+  'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a2 -> ('a1 nFormula,
+  'a2) cnf
 
 val cnf_normalise :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 formula
-  -> 'a2
-  -> ('a1 nFormula, 'a2) cnf
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) ->
+  ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
 
 val cnf_negate :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 formula
-  -> 'a2
-  -> ('a1 nFormula, 'a2) cnf
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) ->
+  ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
 
 val xdenorm : positive -> 'a1 pol -> 'a1 pExpr
+
 val denorm : 'a1 pol -> 'a1 pExpr
+
 val map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr
+
 val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula
 
-val simpl_cone :
-     'a1
-  -> 'a1
-  -> ('a1 -> 'a1 -> 'a1)
-  -> ('a1 -> 'a1 -> bool)
-  -> 'a1 psatz
-  -> 'a1 psatz
+val simpl_cone : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> 'a1 psatz
 
-type q = {qnum : z; qden : positive}
+type q = { qnum : z; qden : positive }
 
 val qeq_bool : q -> q -> bool
+
 val qle_bool : q -> q -> bool
+
 val qplus : q -> q -> q
+
 val qmult : q -> q -> q
+
 val qopp : q -> q
+
 val qminus : q -> q -> q
+
 val qinv : q -> q
+
 val qpower_positive : q -> positive -> q
+
 val qpower : q -> z -> q
 
-type 'a t = Empty | Elt of 'a | Branch of 'a t * 'a * 'a t
+type 'a t =
+| Empty
+| Elt of 'a
+| Branch of 'a t * 'a * 'a t
 
 val find : 'a1 -> 'a1 t -> positive -> 'a1
+
 val singleton : 'a1 -> positive -> 'a1 -> 'a1 t
+
 val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t
+
 val zeval_const : z pExpr -> z option
 
 type zWitness = z psatz
 
 val zWeakChecker : z nFormula list -> z psatz -> bool
+
 val psub1 : z pol -> z pol -> z pol
+
+val popp1 : z pol -> z pol
+
 val padd1 : z pol -> z pol -> z pol
+
 val normZ : z pExpr -> z pol
+
 val zunsat : z nFormula -> bool
+
 val zdeduce : z nFormula -> z nFormula -> z nFormula option
+
 val xnnormalise : z formula -> z nFormula
+
 val xnormalise0 : z nFormula -> z nFormula list
+
 val cnf_of_list0 : 'a1 -> z nFormula list -> (z nFormula * 'a1) list list
+
 val normalise0 : z formula -> 'a1 -> (z nFormula, 'a1) cnf
+
 val xnegate0 : z nFormula -> z nFormula list
+
 val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf
 
-val cnfZ :
-     kind
-  -> (z formula, 'a1, 'a2, 'a3) tFormula
-  -> (z nFormula, 'a1) cnf * 'a1 list
+val cnfZ : kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list
 
 val ceiling : z -> z -> z
 
 type zArithProof =
-  | DoneProof
-  | RatProof of zWitness * zArithProof
-  | CutProof of zWitness * zArithProof
-  | EnumProof of zWitness * zWitness * zArithProof list
-  | ExProof of positive * zArithProof
+| DoneProof
+| RatProof of zWitness * zArithProof
+| CutProof of zWitness * zArithProof
+| SplitProof of z polC * zArithProof * zArithProof
+| EnumProof of zWitness * zWitness * zArithProof list
+| ExProof of positive * zArithProof
 
 val zgcdM : z -> z -> z
+
 val zgcd_pol : z polC -> z * z
+
 val zdiv_pol : z polC -> z -> z polC
+
 val makeCuttingPlane : z polC -> z polC * z
+
 val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option
-val nformula_of_cutting_plane : (z polC * z) * op1 -> z nFormula
+
+val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula
+
 val is_pol_Z0 : z polC -> bool
+
 val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option
+
 val valid_cut_sign : op1 -> bool
+
 val bound_var : positive -> z formula
+
 val mk_eq_pos : positive -> positive -> positive -> z formula
+
 val max_var : positive -> z pol -> positive
+
 val max_var_nformulae : z nFormula list -> positive
+
 val zChecker : z nFormula list -> zArithProof -> bool
+
 val zTautoChecker : z formula bFormula -> zArithProof list -> bool
 
 type qWitness = q psatz
 
 val qWeakChecker : q nFormula list -> q psatz -> bool
+
 val qnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf
+
 val qnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf
+
 val qunsat : q nFormula -> bool
+
 val qdeduce : q nFormula -> q nFormula -> q nFormula option
+
 val normQ : q pExpr -> q pol
 
-val cnfQ :
-     kind
-  -> (q formula, 'a1, 'a2, 'a3) tFormula
-  -> (q nFormula, 'a1) cnf * 'a1 list
+val cnfQ : kind -> (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list
 
 val qTautoChecker : q formula bFormula -> qWitness list -> bool
 
 type rcst =
-  | C0
-  | C1
-  | CQ of q
-  | CZ of z
-  | CPlus of rcst * rcst
-  | CMinus of rcst * rcst
-  | CMult of rcst * rcst
-  | CPow of rcst * (z, nat) sum
-  | CInv of rcst
-  | COpp of rcst
+| C0
+| C1
+| CQ of q
+| CZ of z
+| CPlus of rcst * rcst
+| CMinus of rcst * rcst
+| CMult of rcst * rcst
+| CPow of rcst * (z, nat) sum
+| CInv of rcst
+| COpp of rcst
 
 val z_of_exp : (z, nat) sum -> z
+
 val q_of_Rcst : rcst -> q
 
 type rWitness = q psatz
 
 val rWeakChecker : q nFormula list -> q psatz -> bool
+
 val rnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf
+
 val rnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf
+
 val runsat : q nFormula -> bool
+
 val rdeduce : q nFormula -> q nFormula -> q nFormula option
+
 val rTautoChecker : rcst formula bFormula -> rWitness list -> bool
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index b0317ef643..1462ade7fb 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -459,6 +459,7 @@ module ProofFormat = struct
   type proof =
     | Done
     | Step of int * prf_rule * proof
+    | Split of int * Vect.t * proof * proof
     | Enum of int * prf_rule * Vect.t * prf_rule * proof list
     | ExProof of int * int * int * var * var * var * proof
 
@@ -485,6 +486,9 @@ module ProofFormat = struct
     | Done -> Printf.fprintf o "."
     | Step (i, p, pf) ->
       Printf.fprintf o "%i:= %a ; %a" i output_prf_rule p output_proof pf
+    | Split (i, v, p1, p2) ->
+      Printf.fprintf o "%i:=%a ; { %a } { %a }" i Vect.pp v output_proof p1
+        output_proof p2
     | Enum (i, p1, v, p2, pl) ->
       Printf.fprintf o "%i{%a<=%a<=%a}%a" i output_prf_rule p1 Vect.pp v
         output_prf_rule p2 (pp_list ";" output_proof) pl
@@ -524,6 +528,7 @@ module ProofFormat = struct
   let rec proof_max_def = function
     | Done -> -1
     | Step (i, pr, prf) -> max i (max (pr_rule_max_def pr) (proof_max_def prf))
+    | Split (i, _, p1, p2) -> max i (max (proof_max_def p1) (proof_max_def p2))
     | Enum (i, p1, _, p2, l) ->
       let m = max (pr_rule_max_def p1) (pr_rule_max_def p2) in
       List.fold_left (fun i prf -> max i (proof_max_def prf)) (max i m) l
@@ -573,37 +578,40 @@ module ProofFormat = struct
       ISet.union (pr_rule_collect_defs p1) (pr_rule_collect_defs p2)
 
   (** [simplify_proof p] removes proof steps that are never re-used. *)
-  let simplify_proof p =
-    let rec simplify_proof p =
-      match p with
-      | Done -> (Done, ISet.empty)
-      | Step (i, pr, Done) -> (p, ISet.add i (pr_rule_collect_defs pr))
-      | Step (i, pr, prf) ->
-        let prf', hyps = simplify_proof prf in
-        if not (ISet.mem i hyps) then (prf', hyps)
-        else
-          ( Step (i, pr, prf')
-          , ISet.add i (ISet.union (pr_rule_collect_defs pr) hyps) )
-      | Enum (i, p1, v, p2, pl) ->
-        let pl, hl = List.split (List.map simplify_proof pl) in
-        let hyps = List.fold_left ISet.union ISet.empty hl in
-        ( Enum (i, p1, v, p2, pl)
-        , ISet.add i
-            (ISet.union
-               (ISet.union (pr_rule_collect_defs p1) (pr_rule_collect_defs p2))
-               hyps) )
-      | ExProof (i, j, k, x, z, t, prf) ->
-        let prf', hyps = simplify_proof prf in
-        if
-          (not (ISet.mem i hyps))
-          && (not (ISet.mem j hyps))
-          && not (ISet.mem k hyps)
-        then (prf', hyps)
-        else
-          ( ExProof (i, j, k, x, z, t, prf')
-          , ISet.add i (ISet.add j (ISet.add k hyps)) )
-    in
-    fst (simplify_proof p)
+  let rec simplify_proof p =
+    match p with
+    | Done -> (Done, ISet.empty)
+    | Step (i, pr, Done) -> (p, ISet.add i (pr_rule_collect_defs pr))
+    | Step (i, pr, prf) ->
+      let prf', hyps = simplify_proof prf in
+      if not (ISet.mem i hyps) then (prf', hyps)
+      else
+        ( Step (i, pr, prf')
+        , ISet.add i (ISet.union (pr_rule_collect_defs pr) hyps) )
+    | Split (i, v, p1, p2) ->
+      let p1, h1 = simplify_proof p1 in
+      let p2, h2 = simplify_proof p2 in
+      if not (ISet.mem i h1) then (p1, h1) (* Should not have computed p2 *)
+      else if not (ISet.mem i h2) then (p2, h2)
+      else (Split (i, v, p1, p2), ISet.add i (ISet.union h1 h2))
+    | Enum (i, p1, v, p2, pl) ->
+      let pl, hl = List.split (List.map simplify_proof pl) in
+      let hyps = List.fold_left ISet.union ISet.empty hl in
+      ( Enum (i, p1, v, p2, pl)
+      , ISet.add i
+          (ISet.union
+             (ISet.union (pr_rule_collect_defs p1) (pr_rule_collect_defs p2))
+             hyps) )
+    | ExProof (i, j, k, x, z, t, prf) ->
+      let prf', hyps = simplify_proof prf in
+      if
+        (not (ISet.mem i hyps))
+        && (not (ISet.mem j hyps))
+        && not (ISet.mem k hyps)
+      then (prf', hyps)
+      else
+        ( ExProof (i, j, k, x, z, t, prf')
+        , ISet.add i (ISet.add j (ISet.add k hyps)) )
 
   let rec normalise_proof id prf =
     match prf with
@@ -619,6 +627,10 @@ module ProofFormat = struct
           bds
       in
       (id, prf)
+    | Split (i, v, p1, p2) ->
+      let id, p1 = normalise_proof id p1 in
+      let id, p2 = normalise_proof id p2 in
+      (id, Split (i, v, p1, p2))
     | ExProof (i, j, k, x, z, t, prf) ->
       let id, prf = normalise_proof id prf in
       (id, ExProof (i, j, k, x, z, t, prf))
@@ -640,7 +652,7 @@ module ProofFormat = struct
           (bds2 @ bds1) )
 
   let normalise_proof id prf =
-    let prf = simplify_proof prf in
+    let prf = fst (simplify_proof prf) in
     let res = normalise_proof id prf in
     if debug then
       Printf.printf "normalise_proof %a -> %a" output_proof prf output_proof
@@ -815,6 +827,14 @@ module ProofFormat = struct
   let cmpl_prf_rule_z env r =
     cmpl_prf_rule Mc.normZ (fun x -> CamlToCoq.bigint (Q.num x)) env r
 
+  let cmpl_pol_z lp =
+    try
+      let cst x = CamlToCoq.bigint (Q.num x) in
+      Mc.normZ (LinPoly.coq_poly_of_linpol cst lp)
+    with x ->
+      Printf.printf "cmpl_pol_z %s %a\n" (Printexc.to_string x) LinPoly.pp lp;
+      raise x
+
   let rec cmpl_proof env = function
     | Done -> Mc.DoneProof
     | Step (i, p, prf) -> (
@@ -823,6 +843,11 @@ module ProofFormat = struct
         Mc.CutProof (cmpl_prf_rule_z env p', cmpl_proof (Def i :: env) prf)
       | _ -> Mc.RatProof (cmpl_prf_rule_z env p, cmpl_proof (Def i :: env) prf)
       )
+    | Split (i, v, p1, p2) ->
+      Mc.SplitProof
+        ( cmpl_pol_z v
+        , cmpl_proof (Def i :: env) p1
+        , cmpl_proof (Def i :: env) p2 )
     | Enum (i, p1, _, p2, l) ->
       Mc.EnumProof
         ( cmpl_prf_rule_z env p1
@@ -885,6 +910,7 @@ module ProofFormat = struct
         false
       end
       else eval_proof (IMap.add i (p, o) env) rst
+    | Split (i, v, p1, p2) -> failwith "Not implemented"
     | Enum (i, r1, v, r2, l) ->
       let _ = eval_prf_rule (fun i -> IMap.find i env) r1 in
       let _ = eval_prf_rule (fun i -> IMap.find i env) r2 in
diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli
index 2402a03e0d..4f59b76549 100644
--- a/plugins/micromega/polynomial.mli
+++ b/plugins/micromega/polynomial.mli
@@ -287,6 +287,7 @@ module ProofFormat : sig
   type proof =
     | Done
     | Step of int * prf_rule * proof
+    | Split of int * Vect.t * proof * proof
     | Enum of int * prf_rule * Vect.t * prf_rule * proof list
     | ExProof of int * int * int * var * var * var * proof
 
@@ -314,6 +315,7 @@ module ProofFormat : sig
   val proof_of_farkas : prf_rule IMap.t -> Vect.t -> prf_rule
   val eval_prf_rule : (int -> LinPoly.t * op) -> prf_rule -> LinPoly.t * op
   val eval_proof : (LinPoly.t * op) IMap.t -> proof -> bool
+  val simplify_proof : proof -> proof * Mutils.ISet.t
 
   module PrfRuleMap : Map.S with type key = prf_rule
 end
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index be9b990fe1..39024819be 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -725,6 +725,35 @@ let find_cut nb env u sol rst tbl =
       (fun x v acc -> merge_best lt acc (cut env u sol rst tbl (x, v)))
       tbl Forget
 
+let find_split env tbl rst =
+  let is_split x v =
+    let v, n =
+      let n, _ = Vect.decomp_cst v in
+      if Restricted.is_restricted x rst then
+        let n', v = Vect.decomp_cst (fst (fst (PrfEnv.find x env))) in
+        (v, n -/ n')
+      else (Vect.set x Q.one Vect.null, n)
+    in
+    if Restricted.is_restricted x rst then None
+    else
+      let fn = frac_num n in
+      if fn =/ Q.zero then None
+      else
+        let fn = Q.abs fn in
+        let score = Q.min fn (Q.one -/ fn) in
+        let vect = Vect.add (Vect.cst (Q.neg n)) v in
+        Some (Vect.normalise vect, score)
+  in
+  IMap.fold
+    (fun x v acc ->
+      match is_split x v with
+      | None -> acc
+      | Some (v, s) -> (
+        match acc with
+        | None -> Some (v, s)
+        | Some (v', s') -> if s' >/ s then acc else Some (v, s) ))
+    tbl None
+
 let var_of_vect v = fst (fst (Vect.decomp_fst v))
 
 let eliminate_variable (bounded, env, tbl) x =
@@ -797,40 +826,80 @@ let integer_solver lp =
         Printf.fprintf stdout "Current Tableau\n%a\n" output_tableau tbl;
         flush stdout
       end;
-      let sol = find_full_solution rst tbl in
-      match find_cut (!nb mod 2) env cr (*x*) sol rst tbl with
-      | Forget ->
-        None (* There is no hope, there should be an integer solution *)
-      | Hit (cr, ((v, op), cut)) -> (
-        let vr = LinPoly.MonT.get_fresh () in
-        if op = Eq then
-          (* This is a contradiction *)
-          Some (Step (vr, CutPrf cut, Done))
-        else
-          let res = insert_row vr v (Restricted.set_exc vr rst) tbl in
-          let prf = isolve (IMap.add vr ((v, op), Def vr) env) (Some cr) res in
+      if !nb mod 3 = 0 then
+        match find_split env tbl rst with
+        | None ->
+          None (* There is no hope, there should be an integer solution *)
+        | Some (v, s) -> (
+          let vr = LinPoly.MonT.get_fresh () in
+          let wp1 = ((v, Ge), Def vr) in
+          let wp2 = ((Vect.mul Q.minus_one v, Ge), Def vr) in
+          match (WithProof.cutting_plane wp1, WithProof.cutting_plane wp2) with
+          | None, _ | _, None ->
+            failwith "Error: splitting over an integer variable"
+          | Some wp1, Some wp2 -> (
+            if debug then
+              Printf.fprintf stdout "Splitting over (%s) %a:%a or %a \n"
+                (Q.to_string s) LinPoly.pp_var vr WithProof.output wp1
+                WithProof.output wp2;
+            let v1', v2' = (fst (fst wp1), fst (fst wp2)) in
+            if debug then
+              Printf.fprintf stdout "Solving with %a\n" LinPoly.pp v1';
+            let res1 = insert_row vr v1' (Restricted.set_exc vr rst) tbl in
+            let prf1 = isolve (IMap.add vr ((v1', Ge), Def vr) env) cr res1 in
+            match prf1 with
+            | None -> None
+            | Some prf1 ->
+              let prf', hyps = ProofFormat.simplify_proof prf1 in
+              if not (ISet.mem vr hyps) then Some prf'
+              else (
+                if debug then
+                  Printf.fprintf stdout "Solving with %a\n" Vect.pp v2';
+                let res2 = insert_row vr v2' (Restricted.set_exc vr rst) tbl in
+                let prf2 =
+                  isolve (IMap.add vr ((v2', Ge), Def vr) env) cr res2
+                in
+                match prf2 with
+                | None -> None
+                | Some prf2 -> Some (Split (vr, v, prf1, prf2)) ) ) )
+      else
+        let sol = find_full_solution rst tbl in
+        match find_cut (!nb mod 2) env cr (*x*) sol rst tbl with
+        | Forget ->
+          None (* There is no hope, there should be an integer solution *)
+        | Hit (cr, ((v, op), cut)) -> (
+          let vr = LinPoly.MonT.get_fresh () in
+          if op = Eq then
+            (* This is a contradiction *)
+            Some (Step (vr, CutPrf cut, Done))
+          else
+            let res = insert_row vr v (Restricted.set_exc vr rst) tbl in
+            let prf =
+              isolve (IMap.add vr ((v, op), Def vr) env) (Some cr) res
+            in
+            match prf with
+            | None -> None
+            | Some p -> Some (Step (vr, CutPrf cut, p)) )
+        | Keep (x, v) -> (
+          if debug then
+            Printf.fprintf stdout "Remove %a from Tableau\n" LinPoly.pp_var x;
+          let bounded, env, tbl =
+            Vect.fold
+              (fun acc x n ->
+                if x <> 0 && not (Restricted.is_restricted x rst) then
+                  eliminate_variable acc x
+                else acc)
+              (IMap.empty, env, tbl) v
+          in
+          let prf = isolve env cr (Inl (rst, tbl, None)) in
           match prf with
           | None -> None
-          | Some p -> Some (Step (vr, CutPrf cut, p)) )
-      | Keep (x, v) -> (
-        if debug then
-          Printf.fprintf stdout "Remove %a from Tableau\n" LinPoly.pp_var x;
-        let bounded, env, tbl =
-          Vect.fold
-            (fun acc x n ->
-              if x <> 0 && not (Restricted.is_restricted x rst) then
-                eliminate_variable acc x
-              else acc)
-            (IMap.empty, env, tbl) v
-        in
-        let prf = isolve env cr (Inl (rst, tbl, None)) in
-        match prf with
-        | None -> None
-        | Some pf ->
-          Some
-            (IMap.fold
-               (fun x (vr, zv, tv) acc -> ExProof (vr, zv, tv, x, zv, tv, acc))
-               bounded pf) ) )
+          | Some pf ->
+            Some
+              (IMap.fold
+                 (fun x (vr, zv, tv) acc ->
+                   ExProof (vr, zv, tv, x, zv, tv, acc))
+                 bounded pf) ) )
   in
   let res = solve true l' (Restricted.make vr0) IMap.empty in
   isolve env None res