diff --git a/colibrics.opam b/colibrics.opam
index 5803f891cc47ae7e9fb9e984baa8ef9f9abac7bb..7cf296b7123591029635b74e5a939b8e707f1d01 100644
--- a/colibrics.opam
+++ b/colibrics.opam
@@ -28,3 +28,8 @@ build: [
]
]
dev-repo: "git+https://git.frama-c.com/bobot/colibrics.git"
+pin-depends: [
+ [ "dolmen.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+ [ "dolmen_type.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+ [ "dolmen_loop.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+]
diff --git a/colibrics.opam.template b/colibrics.opam.template
new file mode 100644
index 0000000000000000000000000000000000000000..d285ebc0aad6689347f1cc363403ff767741fcfc
--- /dev/null
+++ b/colibrics.opam.template
@@ -0,0 +1,5 @@
+pin-depends: [
+ [ "dolmen.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+ [ "dolmen_type.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+ [ "dolmen_loop.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+]
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index b4148be35d19a02c0dcb28b4272f4517e2859cb6..74aced0be13fce86277ca86449180c8bcecbb9ba 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -144,7 +144,7 @@ let rec convert ?(subst=Subst.empty) (t : Expr.Term.t) =
match t.descr with
| Var v ->
begin match Expr.Term.Var.M.find v subst.term with
- | exception Not_found -> invalid_arg "Not_ground"
+ | exception Not_found -> invalid_arg (Fmt.str "Not_ground: %a" Expr.Term.Var.pp v)
| n -> n
end
| App (f, tyargs, args) ->
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
index d6926117f061da24e89259bcff4b220e5b1e94f6..70a69ffb9e2010fc86716c69b4c89bfc1cd34594 100644
--- a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
@@ -1,6 +1,8 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exists.smt2}))))
(rule (alias runtest) (action (diff oracle exists.smt2.res)))
+(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exists2.smt2}))))
+(rule (alias runtest) (action (diff oracle exists2.smt2.res)))
(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall0.smt2}))))
(rule (alias runtest) (action (diff oracle forall0.smt2.res)))
(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall1.smt2}))))
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/exists2.smt2 b/src_colibri2/tests/solve/smt_quant/unsat/exists2.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..1bf74867074197e46aa2b2de96e559459840b1cf
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_quant/unsat/exists2.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+
+(assert (not
+ (forall ((x Real))
+ (=> (= x 1.0) (forall ((y Real)) (= y (* y x)))))))
+
+(check-sat)
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index e9dc22b96e6a035a6539b66b8aefd597f7519888..3616679c3294ddee6ecf29da379823016dc16af6 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -159,20 +159,16 @@ let skolemize d (e : Ground.ClosedQuantifier.t) =
if not (Base.List.is_empty e.ty_vars) then
invalid_arg "False type quantification";
let subst_term =
- List.map
- (fun v ->
+ List.fold_left
+ (fun acc v ->
let id = Expr.Term.Const.mk v.Expr.name [] [] v.ty in
let t = Expr.Term.apply id [] [] in
- (v, Ground.convert t))
- e.term_vars
+ Expr.Term.Var.M.add v (Ground.convert t) acc)
+ e.subst.term e.term_vars
in
let n =
Ground.convert
- ~subst:
- {
- Ground.Subst.ty = Expr.Ty.Var.M.empty;
- term = Expr.Term.Var.M.of_list subst_term;
- }
+ ~subst:{ Ground.Subst.ty = e.subst.ty; term = subst_term }
e.body
in
Egraph.register d n;
diff --git a/src_common/modulo.mlw b/src_common/modulo.mlw
index fde133d4d0483bba0b8a1c5761cb163ad771827c..9c31322821f2fbae1883a70d5b106d141fe42ed1 100644
--- a/src_common/modulo.mlw
+++ b/src_common/modulo.mlw
@@ -19,14 +19,7 @@ module Divisible
let d = a /. m in
let t = floor d in
let f = from_int t in
- assert { f <=. d <. from_int (t + 1) };
- assert { f <=. d <. f +. 1. };
- assert { (a /. m) -. 1. <. f <=. a /. m };
- assert { ((a /. m) -. 1.) *. m <. f *. m <=. (a /. m) *. m };
- assert { ((a /. m) *. m) -. m <. f *. m };
- assert { a -. m <. f *. m <=. a };
- assert { -. a <=. -. f *. m <. -. a +. m };
- assert { 0. <=. a -. f *. m <. m }
+ assert { f <=. d <. from_int (t + 1) }
predicate ddivisible_using (a b:real) (d:int) =
a = (from_int d) *. b
diff --git a/src_common/modulo/why3session.xml b/src_common/modulo/why3session.xml
index 7fb72ce5f8e891c640c403c63aa3721d11f2aad1..ae607018125e6bc8f2cc2b66a8fd9f10805be017 100644
--- a/src_common/modulo/why3session.xml
+++ b/src_common/modulo/why3session.xml
@@ -6,82 +6,101 @@
<prover id="1" name="Alt-Ergo" version="2.3.3" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="1000"/>
-<file format="whyml" proved="true">
+<prover id="4" name="Colibri2" version="0.0.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
+<file format="whyml">
<path name=".."/><path name="modulo.mlw"/>
-<theory name="Divisible" proved="true">
+<theory name="Divisible">
<goal name="round_modulo'vc" expl="VC for round_modulo" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_modulo'vc.0" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04" steps="2577"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="2577"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="round_modulo'vc.1" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.04" steps="3138"/></proof>
- </goal>
- <goal name="round_modulo'vc.2" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="2659"/></proof>
- </goal>
- <goal name="round_modulo'vc.3" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="2690"/></proof>
- </goal>
- <goal name="round_modulo'vc.4" expl="assertion" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="round_modulo'vc.4.0" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.68" steps="2340433"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="3138"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="round_modulo'vc.2" expl="postcondition" proved="true">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="2891"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="round_modulo'vc.3" expl="postcondition" proved="true">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="30206"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="round_modulo'vc.3" expl="assertion">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="2690"/></proof>
+ <proof prover="4"><undone/></proof>
+ </goal>
+ <goal name="round_modulo'vc.4" expl="assertion">
+ <transf name="split_vc" >
+ <goal name="round_modulo'vc.4.0" expl="assertion">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="8681"/></proof>
+ <proof prover="4"><undone/></proof>
</goal>
- <goal name="round_modulo'vc.4.1" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.00" steps="8464"/></proof>
+ <goal name="round_modulo'vc.4.1" expl="assertion">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="8660"/></proof>
+ <proof prover="4"><undone/></proof>
</goal>
</transf>
</goal>
- <goal name="round_modulo'vc.5" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="2785"/></proof>
- </goal>
- <goal name="round_modulo'vc.6" expl="assertion" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="round_modulo'vc.6.0" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="8681"/></proof>
+ <goal name="round_modulo'vc.4" expl="assertion">
+ <transf name="split_vc" >
+ <goal name="round_modulo'vc.4.0" expl="assertion">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.68" steps="2340433"/></proof>
+ <proof prover="4"><undone/></proof>
</goal>
- <goal name="round_modulo'vc.6.1" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="8660"/></proof>
+ <goal name="round_modulo'vc.4.1" expl="assertion">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.00" steps="8464"/></proof>
+ <proof prover="4"><undone/></proof>
</goal>
</transf>
</goal>
- <goal name="round_modulo'vc.7" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="2849"/></proof>
+ <goal name="round_modulo'vc.2" expl="assertion">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="2659"/></proof>
+ <proof prover="4"><undone/></proof>
</goal>
- <goal name="round_modulo'vc.8" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="2887"/></proof>
+ <goal name="round_modulo'vc.3" expl="assertion">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="2887"/></proof>
+ <proof prover="4"><undone/></proof>
</goal>
- <goal name="round_modulo'vc.9" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="2891"/></proof>
+ <goal name="round_modulo'vc.5" expl="assertion">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="2785"/></proof>
+ <proof prover="4"><undone/></proof>
</goal>
- <goal name="round_modulo'vc.10" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="30206"/></proof>
+ <goal name="round_modulo'vc.5" expl="assertion">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="2849"/></proof>
+ <proof prover="4"><undone/></proof>
</goal>
</transf>
</goal>
<goal name="round_down_to'vc" expl="VC for round_down_to" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="round_down_to'vc.0" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="7283"/></proof>
+ <goal name="round_down_to'vc.0" expl="precondition" proved="true">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="10725"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="round_down_to'vc.1" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="10725"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="3558"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="round_down_to'vc.2" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="3558"/></proof>
+ <goal name="round_down_to'vc.2" expl="postcondition" proved="true">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="7283"/></proof>
+ <proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="round_down_to'vc.3" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.3.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.3.0.0" expl="postcondition" proved="true">
- <proof prover="0" timelimit="5"><result status="valid" time="0.02" steps="5029"/></proof>
+ <proof prover="0" timelimit="5" obsolete="true"><result status="valid" time="0.02" steps="5029"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
<goal name="round_down_to'vc.3.1" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="80935"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="80935"/></proof>
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
@@ -90,22 +109,26 @@
<goal name="round_down_to'vc.4.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.4.0.0" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="2957"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="2957"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="round_down_to'vc.4.0.1" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="15052"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="15052"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="round_down_to'vc.4.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.4.1.0" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.05" steps="12398"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.05" steps="12398"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="round_down_to'vc.4.1.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.4.1.1.0" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="81315"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="81315"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
@@ -116,12 +139,14 @@
<goal name="round_down_to'vc.5" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.5.0" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="3067"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="3067"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="round_down_to'vc.5.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.5.1.0" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="52"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="52"/></proof>
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
@@ -129,342 +154,438 @@
</goal>
</transf>
</goal>
- <goal name="round_up_to'vc" expl="VC for round_up_to" proved="true">
- <proof prover="2"><result status="valid" time="0.06" steps="7767"/></proof>
+ <goal name="round_up_to'vc" expl="VC for round_up_to">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.06" steps="7767"/></proof>
+ <proof prover="4" obsolete="true"><path name="modulo-Divisible-round_up_toqtvc_1.psmt2"/><result status="highfailure" time="0.00"/></proof>
</goal>
- <goal name="simple_mul_div'vc" expl="VC for simple_mul_div" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="3339"/></proof>
+ <goal name="simple_mul_div'vc" expl="VC for simple_mul_div">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="3339"/></proof>
+ <proof prover="4"><result status="unknown" time="0.02"/></proof>
</goal>
- <goal name="remove_product_right'vc" expl="VC for remove_product_right" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25451"/></proof>
+ <goal name="remove_product_right'vc" expl="VC for remove_product_right">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="25451"/></proof>
+ <proof prover="4"><result status="unknown" time="0.03"/></proof>
</goal>
- <goal name="divisible_to_z'vc" expl="VC for divisible_to_z" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="divisible_to_z'vc.0" expl="assertion" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="divisible_to_z'vc" expl="VC for divisible_to_z">
+ <transf name="split_vc" >
+ <goal name="divisible_to_z'vc.0" expl="assertion">
+ <transf name="split_vc" >
<goal name="divisible_to_z'vc.0.0" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="10"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible_to_z'vc.0.1" expl="VC for divisible_to_z" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="10"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="divisible_to_z'vc.0.2" expl="VC for divisible_to_z" proved="true">
- <proof prover="1"><result status="valid" time="0.05" steps="115"/></proof>
+ <goal name="divisible_to_z'vc.0.2" expl="VC for divisible_to_z">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.05" steps="115"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="divisible_to_z'vc.0.3" expl="VC for divisible_to_z" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="3290"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="3290"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="divisible_to_z'vc.1" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.04" steps="11392"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.04" steps="11392"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="divisible_to_z'vc.2" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="3276"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="3276"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible_to_z'vc.3" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="14"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible_to_z'vc.4" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="divisible_to_z'vc.5" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="16"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible_to_z'vc.6" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="18"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible_to_z'vc.7" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="divisible_to_z'vc.7.0" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="20"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
- <goal name="divisible_to_z'vc.8" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
+ <goal name="divisible_to_z'vc.8" expl="precondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="22"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="divisible_to_z'vc.9" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="22"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="divisible_to_z'vc.10" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.05" steps="86"/></proof>
+ <goal name="divisible_to_z'vc.10" expl="precondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.05" steps="86"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="divisible_to_z'vc.11" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible_to_z'vc.12" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
- <proof prover="2"><result status="valid" time="0.03" steps="3369"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="3369"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible_to_z'vc.13" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
- <proof prover="2"><result status="valid" time="0.03" steps="3372"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="3372"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="divisible_to_z'vc.14" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
- <goal name="divisible_from_z'vc" expl="VC for divisible_from_z" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="divisible_from_z'vc.0" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04" steps="12764"/></proof>
- </goal>
- <goal name="divisible_from_z'vc.1" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="17379"/></proof>
- </goal>
- <goal name="divisible_from_z'vc.2" expl="assertion" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="divisible_from_z'vc" expl="VC for divisible_from_z">
+ <transf name="split_vc" >
+ <goal name="divisible_from_z'vc.0" expl="precondition">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="12764"/></proof>
+ <proof prover="4"><result status="unknown" time="0.05"/></proof>
+ </goal>
+ <goal name="divisible_from_z'vc.1" expl="precondition">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="17379"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
+ </goal>
+ <goal name="divisible_from_z'vc.2" expl="assertion">
+ <transf name="split_vc" >
<goal name="divisible_from_z'vc.2.0" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="14"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="divisible_from_z'vc.2.1" expl="VC for divisible_from_z" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="16"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="16"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible_from_z'vc.2.2" expl="VC for divisible_from_z" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="16"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="16"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible_from_z'vc.2.3" expl="VC for divisible_from_z" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="14"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="divisible_from_z'vc.2.4" expl="VC for divisible_from_z" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="divisible_from_z'vc.2.4" expl="VC for divisible_from_z">
+ <proof prover="3" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="divisible_from_z'vc.2.5" expl="VC for divisible_from_z" proved="true">
- <proof prover="1"><result status="valid" time="1.32" steps="182"/></proof>
+ <goal name="divisible_from_z'vc.2.5" expl="VC for divisible_from_z">
+ <proof prover="1" obsolete="true"><result status="valid" time="1.32" steps="182"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="divisible_from_z'vc.2.6" expl="VC for divisible_from_z" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="divisible_from_z'vc.3" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="17166"/></proof>
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="17166"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
- <goal name="divisible'vc" expl="VC for divisible" proved="true">
- <transf name="split_vc" proved="true" >
+ <goal name="divisible'vc" expl="VC for divisible">
+ <transf name="split_vc" >
<goal name="divisible'vc.0" expl="witness existence" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="16"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="divisible'vc.1" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="4518"/></proof>
+ <goal name="divisible'vc.1" expl="precondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="14"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="divisible'vc.2" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4523"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="14"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible'vc.3" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="26"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible'vc.4" expl="unreachable point" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="5230"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="20"/></proof>
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="divisible'vc.5" expl="witness existence" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5079"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="5079"/></proof>
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="divisible'vc.6" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+ <goal name="divisible'vc.6" expl="precondition">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="4518"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="divisible'vc.7" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="4523"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="divisible'vc.8" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4498"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="4498"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="divisible'vc.9" expl="unreachable point" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+ <goal name="divisible'vc.9" expl="unreachable point">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="5230"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.25"/></proof>
</goal>
<goal name="divisible'vc.10" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="divisible'vc.10.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="divisible'vc.10.0.0" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="5216"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="divisible'vc.10.0.1" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5216"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="18"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="divisible'vc.10.1" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="5131"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="5131"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="divisible'vc.11" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="20"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.00" steps="20"/></proof>
+ <proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
- <goal name="mult_cst_divisible'vc" expl="VC for mult_cst_divisible" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="mult_cst_divisible'vc.0" expl="witness existence" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="39"/></proof>
+ <goal name="mult_cst_divisible'vc" expl="VC for mult_cst_divisible">
+ <transf name="split_vc" >
+ <goal name="mult_cst_divisible'vc.0" expl="witness existence">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="39"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.01"/></proof>
</goal>
<goal name="mult_cst_divisible'vc.1" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="12"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="mult_cst_divisible'vc.2" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="53"/></proof>
+ <goal name="mult_cst_divisible'vc.2" expl="postcondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="53"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.01"/></proof>
</goal>
- <goal name="mult_cst_divisible'vc.3" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
+ <goal name="mult_cst_divisible'vc.3" expl="postcondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="10"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.01"/></proof>
</goal>
</transf>
</goal>
- <goal name="union_divisible'vc" expl="VC for union_divisible" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="union_divisible'vc.0" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="13363"/></proof>
+ <goal name="union_divisible'vc" expl="VC for union_divisible">
+ <transf name="split_vc" >
+ <goal name="union_divisible'vc.0" expl="precondition">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="13363"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="union_divisible'vc.1" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04" steps="21085"/></proof>
+ <goal name="union_divisible'vc.1" expl="precondition">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.04" steps="21085"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="union_divisible'vc.2" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="union_divisible'vc.3" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="26"/></proof>
+ <proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="union_divisible'vc.4" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="union_divisible'vc.5" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="67"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="67"/></proof>
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="union_divisible'vc.6" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="32"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="32"/></proof>
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="union_divisible'vc.7" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5193"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="5193"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="union_divisible'vc.8" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="32"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="32"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="union_divisible'vc.9" expl="witness existence" proved="true">
- <proof prover="1"><result status="valid" time="0.08" steps="85"/></proof>
+ <goal name="union_divisible'vc.9" expl="witness existence">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.08" steps="85"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.02"/></proof>
</goal>
<goal name="union_divisible'vc.10" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5255"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="5255"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_divisible'vc.11" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5260"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="5260"/></proof>
+ <proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="union_divisible'vc.12" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="5313"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="5313"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="union_divisible'vc.13" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="48"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="48"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="union_divisible'vc.14" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="48"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_divisible'vc.15" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="50"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="50"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_divisible'vc.16" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="50"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="50"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_divisible'vc.17" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="51"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="51"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="union_divisible'vc.18" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="52"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="52"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="union_divisible'vc.19" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.75" steps="144"/></proof>
+ <goal name="union_divisible'vc.19" expl="postcondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.75" steps="144"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.01"/></proof>
</goal>
- <goal name="union_divisible'vc.20" expl="witness existence" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="85"/></proof>
+ <goal name="union_divisible'vc.20" expl="witness existence">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="85"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.01"/></proof>
</goal>
<goal name="union_divisible'vc.21" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="40"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="40"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_divisible'vc.22" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="40"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="40"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="union_divisible'vc.23" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="46"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="46"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_divisible'vc.24" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="48"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="48"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="union_divisible'vc.25" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="48"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="union_divisible'vc.26" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="50"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="50"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_divisible'vc.27" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="50"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="50"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_divisible'vc.28" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="51"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="51"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_divisible'vc.29" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="52"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="52"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="union_divisible'vc.30" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="6733"/></proof>
+ <goal name="union_divisible'vc.30" expl="postcondition">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="6733"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.01"/></proof>
</goal>
- <goal name="union_divisible'vc.31" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="42"/></proof>
+ <goal name="union_divisible'vc.31" expl="postcondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="42"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.02"/></proof>
</goal>
- <goal name="union_divisible'vc.32" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="6351"/></proof>
+ <goal name="union_divisible'vc.32" expl="postcondition">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="6351"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.02"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter_divisible'vc" expl="VC for inter_divisible" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter_divisible'vc.0" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="52"/></proof>
+ <goal name="inter_divisible'vc" expl="VC for inter_divisible">
+ <transf name="split_vc" >
+ <goal name="inter_divisible'vc.0" expl="precondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="52"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter_divisible'vc.1" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="54"/></proof>
+ <goal name="inter_divisible'vc.1" expl="precondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="54"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter_divisible'vc.2" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
+ <goal name="inter_divisible'vc.2" expl="precondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter_divisible'vc.3" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="28139"/></proof>
+ <goal name="inter_divisible'vc.3" expl="precondition">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="28139"/></proof>
+ <proof prover="4"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="inter_divisible'vc.4" expl="witness existence" proved="true">
- <proof prover="1"><result status="valid" time="0.04" steps="82"/></proof>
+ <goal name="inter_divisible'vc.4" expl="witness existence">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.04" steps="82"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.01"/></proof>
</goal>
- <goal name="inter_divisible'vc.5" expl="witness existence" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="94"/></proof>
+ <goal name="inter_divisible'vc.5" expl="witness existence">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="94"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.01"/></proof>
</goal>
<goal name="inter_divisible'vc.6" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="34"/></proof>
- <proof prover="2"><result status="valid" time="0.03" steps="5235"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="34"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="5235"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="inter_divisible'vc.7" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="34"/></proof>
- <proof prover="2"><result status="valid" time="0.02" steps="5243"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="34"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="5243"/></proof>
+ <proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="inter_divisible'vc.8" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="40"/></proof>
- <proof prover="2"><result status="valid" time="0.02" steps="5291"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="40"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.02" steps="5291"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter_divisible'vc.9" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="40"/></proof>
- <proof prover="2"><result status="valid" time="0.03" steps="5299"/></proof>
- </goal>
- <goal name="inter_divisible'vc.10" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
- </goal>
- <goal name="inter_divisible'vc.11" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="50"/></proof>
- </goal>
- <goal name="inter_divisible'vc.12" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="6481"/></proof>
- </goal>
- <goal name="inter_divisible'vc.13" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="34"/></proof>
- <proof prover="2"><result status="valid" time="0.03" steps="6188"/></proof>
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="40"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="5299"/></proof>
+ <proof prover="4"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.10" expl="precondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.01" steps="48"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.02"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.11" expl="precondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="50"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.02"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.12" expl="postcondition">
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="6481"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.01"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.13" expl="postcondition">
+ <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="34"/></proof>
+ <proof prover="2" obsolete="true"><result status="valid" time="0.03" steps="6188"/></proof>
+ <proof prover="4"><result status="highfailure" time="0.00"/></proof>
</goal>
</transf>
</goal>