Commit 8ba9c228 authored by François Bobot's avatar François Bobot

Merge remote-tracking branch 'origin/bugfix/v1.0'

parents 78e5138a 230c01c5
:x: marks a potential source of incompatibility
Provers
* support for Alt-Ergo 2.2.0 (released Apr 26, 2018)
* support for Alt-Ergo 2.1.0 (released Mar 14, 2018)
Version 1.0.0, June 25, 2018
----------------------------
......
......@@ -12,7 +12,8 @@ prelude "(set-logic AUFBVDTNIRA)"
does not seem to include DT
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv-realization.gen"
import "discrimination.gen"
......
......@@ -7,7 +7,8 @@ prelude "(set-logic AUFNIRA)"
NIRA : NonLinear Integer Reals Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "no-bv.gen"
import "discrimination.gen"
......
......@@ -10,7 +10,8 @@ prelude "(set-logic AUFBVDTNIRA)"
NIRA : NonLinear Integer+Real Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "discrimination.gen"
......
(** Why3 driver for CVC4 >= 1.5 *)
(** Why3 driver for CVC4 1.5 *)
prelude ";; produced by cvc4_15.drv ;;"
prelude "(set-logic AUFBVDTNIRA)"
......@@ -10,10 +10,8 @@ prelude "(set-logic AUFBVDTNIRA)"
NIRA : NonLinear Integer+Real Arithmetic
*)
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "discrimination.gen"
......@@ -26,14 +24,12 @@ transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections.
Note: does nothing if meta get_counterexmp is not set *)
(* Prepare for counter-example query: get rid of some quantifiers
(makes it possible to query model values of the variables in
premises) and introduce counter-example projections. Note: does
nothing if meta get_counterexmp is not set *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
......
import "cvc4_15.drv"
(* Counterexamples: set model parser *)
model_parser "smtv2"
theory BuiltIn
meta "get_counterexmp" ""
......
(** Why3 driver for CVC4 >= 1.6 (with floating point support) *)
prelude ";; produced by cvc4_16.drv ;;"
prelude "(set-info :smt-lib-version 2.5)"
prelude "(set-info :smt-lib-version 2.6)"
prelude "(set-logic AUFBVFPDTNIRA)"
(*
A : Array
......@@ -11,11 +11,9 @@ prelude "(set-logic AUFBVFPDTNIRA)"
DT : Datatypes
NIRA : NonLinear Integer+Real Arithmetic
*)
prelude "(set-info :source |VC generated by SPARK 2014|)"
prelude "(set-info :category industrial)"
prelude "(set-info :status unknown)"
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2.6"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "smt-libv2-floats.gen"
......@@ -24,20 +22,22 @@ import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Prepare for counter-example query: get rid of some quantifiers
(makes it possible to query model values of the variables in
premises) and introduce counter-example projections. Note: does
nothing if meta get_counterexmp is not set *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
(* remove pointless quantifiers from the goal *)
transformation "introduce_premises"
(** Error messages specific to CVC4 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
......@@ -47,3 +47,27 @@ steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
(** Extra theories supported by CVC4 *)
(* CVC4 division seems to be the Euclidean one, not the Computer one *)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
(*
theory int.ComputerDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
*)
(** Why3 driver for CVC4 >= 1.5 *)
prelude ";; produced by cvc4_16_counterexample.drv ;;"
prelude "(set-info :smt-lib-version 2.5)"
prelude "(set-logic AUFBVFPDTNIRA)"
(*
A : Array
UF : Uninterpreted Function
BV : BitVectors
FP : FloatingPoint
DT : Datatypes
NIRA : NonLinear Integer+Real Arithmetic
*)
import "cvc4_16.drv"
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "smt-libv2-floats.gen"
import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections.
Note: does nothing if meta get_counterexmp is not set *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
(** Error messages specific to CVC4 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
theory BuiltIn
meta "get_counterexmp" ""
meta "meta_incremental" ""
end
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
(* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
have the same name for the function to_int *)
theory bv.BV_Gen
......
(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
(* preserve former smt-libv2 driver for backward compatibility *)
prelude ";;; generated by SMT-LIB2 driver"
(*
Note: we do not insert any command "set-logic" because its
interpretation is specific to provers
prelude "(set-logic AUFNIRA)"
A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
NIRA : NonLinear Integer Reals Arithmetic
*)
printer "smtv2"
filename "%f-%t-%g.smt2"
unknown "^\\(unknown\\|sat\\|Fail\\)$" ""
time "why3cpulimit time : %s s"
valid "^unsat$"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding:kept" type int
meta "encoding:ignore_polymorphism_ls" predicate (=)
end
theory int.Int
prelude ";;; SMT-LIB2: integer arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (-_) "(- %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
remove prop Unit_def_l
remove prop Unit_def_r
remove prop Inv_def_l
remove prop Inv_def_r
remove prop Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory real.Real
prelude ";;; SMT-LIB2: real arithmetic"
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (/) "(/ %1 %2)"
syntax function (-_) "(- %1)"
syntax function inv "(/ 1.0 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
remove prop Unit_def_l
remove prop Unit_def_r
remove prop Inv_def_l
remove prop Inv_def_r
remove prop Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding:kept" type real
end
theory Bool
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
meta "encoding:kept" type bool
end
theory bool.Bool
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function xorb "(xor %1 %2)"
syntax function notb "(not %1)"
syntax function implb "(=> %1 %2)"
end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding:lskept" function ite
meta "encoding:ignore_polymorphism_ls" function ite
end
(* not uniformly interpreted by provers
theory real.Truncate
syntax function floor "(to_int %1)"
remove prop Floor_down
remove prop Floor_monotonic
end
*)
theory HighOrd
syntax type (->) "(Array %1 %2)"
syntax function (@) "(select %1 %2)"
meta "encoding:lskept" function (@)
meta "encoding:ignore_polymorphism_ts" type (->)
meta "encoding:ignore_polymorphism_ls" function (@)
end
theory map.Map
syntax function get "(select %1 %2)"
syntax function set "(store %1 %2 %3)"
meta "encoding:lskept" function get
meta "encoding:lskept" function set
meta "encoding:ignore_polymorphism_ls" function get
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
meta "encoding:ignore_polymorphism_ls" function ([<-])
end
theory map.Const
meta "encoding:lskept" function const
(* syntax function const "(const[%t0] %1)" *)
end
import "smt-libv2.gen"
printer "smtv2"
\ No newline at end of file
(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
prelude ";;; generated by SMT-LIB2 driver"
(*
Note: we do not insert any command "set-logic" because its
interpretation is specific to provers
prelude "(set-logic AUFNIRA)"
A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
NIRA : NonLinear Integer Reals Arithmetic
*)
filename "%f-%t-%g.smt2"
unknown "^\\(unknown\\|sat\\|Fail\\)$" ""
time "why3cpulimit time : %s s"
valid "^unsat$"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding:kept" type int
meta "encoding:ignore_polymorphism_ls" predicate (=)
end
theory int.Int
prelude ";;; SMT-LIB2: integer arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (-_) "(- %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
remove prop Unit_def_l
remove prop Unit_def_r
remove prop Inv_def_l
remove prop Inv_def_r
remove prop Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory real.Real
prelude ";;; SMT-LIB2: real arithmetic"
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (/) "(/ %1 %2)"
syntax function (-_) "(- %1)"
syntax function inv "(/ 1.0 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
remove prop Unit_def_l
remove prop Unit_def_r
remove prop Inv_def_l
remove prop Inv_def_r
remove prop Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding:kept" type real
end
theory Bool
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
meta "encoding:kept" type bool
end
theory bool.Bool
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function xorb "(xor %1 %2)"
syntax function notb "(not %1)"
syntax function implb "(=> %1 %2)"
end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding:lskept" function ite
meta "encoding:ignore_polymorphism_ls" function ite
end
(* not uniformly interpreted by provers
theory real.Truncate
syntax function floor "(to_int %1)"
remove prop Floor_down
remove prop Floor_monotonic
end
*)
theory HighOrd
syntax type (->) "(Array %1 %2)"
syntax function (@) "(select %1 %2)"
meta "encoding:lskept" function (@)
meta "encoding:ignore_polymorphism_ts" type (->)
meta "encoding:ignore_polymorphism_ls" function (@)
end
theory map.Map
syntax function get "(select %1 %2)"
syntax function set "(store %1 %2 %3)"
meta "encoding:lskept" function get
meta "encoding:lskept" function set
meta "encoding:ignore_polymorphism_ls" function get
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
meta "encoding:ignore_polymorphism_ls" function ([<-])
end
theory map.Const
meta "encoding:lskept" function const
(* syntax function const "(const[%t0] %1)" *)
end
......@@ -7,7 +7,8 @@ prelude "(set-logic AUFLIRA)"
LIRA : Linear Integer Reals Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "discrimination.gen"
(* specific message from veriT 201310 *)
......
......@@ -7,7 +7,8 @@ prelude "(set-logic QF_AUFLIRA)"
LIRA : Linear Integer Reals Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "discrimination.gen"
(* specific messages from Yices-smt2 *)
......
......@@ -6,7 +6,8 @@ prelude "(set-logic AUFNIRA)"
NIRA : NonLinear Integer Reals Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "discrimination.gen"
transformation "inline_trivial"
......
......@@ -7,7 +7,8 @@
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "no-bv.gen"
import "discrimination.gen"
......@@ -79,7 +80,7 @@ end
(* REMOVED: we do not use BV theory from Z3 in 4.3.2 but starting from 4.4.0
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
(* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
......
......@@ -7,7 +7,8 @@
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv.gen"
import "z3_bv.gen"
import "smt-libv2-floats.gen"
......
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
(* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV_Gen
......
......@@ -27,17 +27,19 @@
<prover id="22" name="Vampire" version="0.6" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="23" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="24" name="veriT" version="201410" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="25" name="Alt-Ergo" version="2.1.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="27" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="28" name="Z3" version="4.4.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="29" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="30" name="Isabelle" version="2016-1" timelimit="100" steplimit="1" memlimit="1000"/>
<prover id="31" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="32" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="33" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="34" name="Coq" version="8.7.1" timelimit="5" steplimit="1" memlimit="4000"/>
<file name="../genealogy.why">
<theory name="Genealogy">
<goal name="Child_is_son_or_daughter" expl="">
<file name="../genealogy.why" proved="true">
<theory name="Genealogy" proved="true">
<goal name="Child_is_son_or_daughter" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -59,16 +61,18 @@
<proof prover="22"><result status="valid" time="0.00"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="21.67"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof>
<proof prover="34" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="Sibling_sym" expl="">
<goal name="Sibling_sym" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -91,15 +95,17 @@
<proof prover="22"><result status="valid" time="0.00"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.00"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Sibling_sym_1.xml"><result status="valid" time="21.58"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Sibling_is_brother_or_sister" expl="">
<goal name="Sibling_is_brother_or_sister" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -120,15 +126,17 @@
<proof prover="22"><result status="valid" time="0.00"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="26"><result status="valid" time="0.01"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="22.73"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Grandparent_is_grandfather_or_grandmother" expl="">
<goal name="Grandparent_is_grandfather_or_grandmother" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="28"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -150,15 +158,17 @@
<proof prover="22"><result status="valid" time="0.01"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="32"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="20"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="36"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="24.37"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="20"/></proof>
<proof prover="33"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Grandfather_male" expl="">
<goal name="Grandfather_male" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -181,14 +191,16 @@
<proof prover="22"><result status="valid" time="0.03"/></proof>
<proof prover="23"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="11"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="11"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Grandmother_female" expl="">
<goal name="Grandmother_female" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -211,14 +223,16 @@