Commit fd3cdc28 authored by Clément Fumex's avatar Clément Fumex
Browse files

recover lost proof in queens_bv

parent f0547868
......@@ -4,8 +4,10 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.10.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../queens_bv.mlw" expanded="true">
<theory name="S" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
......@@ -106,1987 +108,12 @@
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
</theory>
<theory name="NQueensBits" sum="e6ce77a09d0119aa54c11e903423f97b" expanded="true">
<goal name="WP_parameter t" expl="VC for t">
<transf name="split_goal_wp">
<theory name="NQueensBits" sum="8df1b20921ea50654fbd4ae90d0ca7cb" expanded="true">
<goal name="WP_parameter t" expl="VC for t" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter t.1" expl="1. assertion">
<metas>
<ts_pos name="real" arity="0" id="2"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_library name="BuiltIn"/>
<ip_qualid name="real"/>
</ts_pos>
<ts_pos name="tuple0" arity="0" id="20"
ip_theory="Tuple0">
<ip_library name="why3"/>
<ip_library name="Tuple0"/>
<ip_qualid name="tuple0"/>
</ts_pos>
<ts_pos name="unit" arity="0" id="21"
ip_theory="Unit">
<ip_library name="why3"/>
<ip_library name="Unit"/>
<ip_qualid name="unit"/>
</ts_pos>
<ts_pos name="solution" arity="0" id="3736"
ip_theory="Solution">
<ip_qualid name="solution"/>
</ts_pos>
<ts_pos name="solutions" arity="0" id="3801"
ip_theory="Solution">
<ip_qualid name="solutions"/>
</ts_pos>
<ts_pos name="t" arity="0" id="3834"
ip_theory="BitsSpec">
<ip_qualid name="t"/>
</ts_pos>
<ts_pos name="ref" arity="1" id="3890"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="ref"/>
</ts_pos>
<ls_pos name="infix =" id="10"
ip_theory="BuiltIn">
<ip_library name="why3"/>
<ip_library name="BuiltIn"/>
<ip_qualid name="infix ="/>
</ls_pos>
<ls_pos name="zero" id="777"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="one" id="778"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="one"/>
</ls_pos>
<ls_pos name="infix &lt;" id="779"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &lt;"/>
</ls_pos>
<ls_pos name="infix +" id="1948"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix +"/>
</ls_pos>
<ls_pos name="prefix -" id="1949"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="prefix -"/>
</ls_pos>
<ls_pos name="infix *" id="1950"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix *"/>
</ls_pos>
<ls_pos name="abs" id="2063"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="abs"/>
</ls_pos>
<ls_pos name="div" id="2188"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="div"/>
</ls_pos>
<ls_pos name="mod" id="2191"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="mod"/>
</ls_pos>
<ls_pos name="mem" id="2812"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="mem"/>
</ls_pos>
<ls_pos name="infix ==" id="2815"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="infix =="/>
</ls_pos>
<ls_pos name="subset" id="2833"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="subset"/>
</ls_pos>
<ls_pos name="empty" id="2854"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="empty"/>
</ls_pos>
<ls_pos name="add" id="2866"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="add"/>
</ls_pos>
<ls_pos name="singleton" id="2872"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="singleton"/>
</ls_pos>
<ls_pos name="remove" id="2877"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="remove"/>
</ls_pos>
<ls_pos name="union" id="2895"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="union"/>
</ls_pos>
<ls_pos name="inter" id="2902"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="inter"/>
</ls_pos>
<ls_pos name="diff" id="2909"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="diff"/>
</ls_pos>
<ls_pos name="choose" id="2921"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="choose"/>
</ls_pos>
<ls_pos name="cardinal" id="2925"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="cardinal"/>
</ls_pos>
<ls_pos name="min_elt" id="3030"
ip_theory="Fsetint">
<ip_library name="set"/>
<ip_qualid name="min_elt"/>
</ls_pos>
<ls_pos name="max_elt" id="3040"
ip_theory="Fsetint">
<ip_library name="set"/>
<ip_qualid name="max_elt"/>
</ls_pos>
<ls_pos name="interval" id="3050"
ip_theory="Fsetint">
<ip_library name="set"/>
<ip_qualid name="interval"/>
</ls_pos>
<ls_pos name="get" id="3135"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="3138"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="3158"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="andb" id="3562"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="andb"/>
</ls_pos>
<ls_pos name="orb" id="3571"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="orb"/>
</ls_pos>
<ls_pos name="notb" id="3580"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="notb"/>
</ls_pos>
<ls_pos name="xorb" id="3585"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="xorb"/>
</ls_pos>
<ls_pos name="implb" id="3594"
ip_theory="Bool">
<ip_library name="bool"/>
<ip_qualid name="implb"/>
</ls_pos>
<ls_pos name="succ" id="3720" ip_theory="S">
<ip_qualid name="succ"/>
</ls_pos>
<ls_pos name="pred" id="3727" ip_theory="S">
<ip_qualid name="pred"/>
</ls_pos>
<ls_pos name="n" id="3735" ip_theory="Solution">
<ip_qualid name="n"/>
</ls_pos>
<ls_pos name="eq_sol" id="3753"
ip_theory="Solution">
<ip_qualid name="eq_sol"/>
</ls_pos>
<ls_pos name="lt_sol" id="3789"
ip_theory="Solution">
<ip_qualid name="lt_sol"/>
</ls_pos>
<ls_pos name="sorted" id="3802"
ip_theory="Solution">
<ip_qualid name="sorted"/>
</ls_pos>
<ls_pos name="prefix !" id="3896"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="prefix !"/>
</ls_pos>
<ls_pos name="pow2" id="4050"
ip_theory="Pow2int">
<ip_library name="bv"/>
<ip_qualid name="pow2"/>
</ls_pos>
<ls_pos name="size" id="4942"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="size"/>
</ls_pos>
<ls_pos name="nth" id="4948"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="nth"/>
</ls_pos>
<ls_pos name="ones" id="4957"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="ones"/>
</ls_pos>
<ls_pos name="bw_and" id="4960"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_and"/>
</ls_pos>
<ls_pos name="bw_or" id="4967"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_or"/>
</ls_pos>
<ls_pos name="bw_xor" id="4974"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_xor"/>
</ls_pos>
<ls_pos name="bw_not" id="4981"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="bw_not"/>
</ls_pos>
<ls_pos name="lsr" id="4986"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsr"/>
</ls_pos>
<ls_pos name="asr" id="5000"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="asr"/>
</ls_pos>
<ls_pos name="lsl" id="5014"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsl"/>
</ls_pos>
<ls_pos name="rotate_right" id="5028"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="rotate_right"/>
</ls_pos>
<ls_pos name="rotate_left" id="5034"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="rotate_left"/>
</ls_pos>
<ls_pos name="to_int" id="5042"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="to_int"/>
</ls_pos>
<ls_pos name="of_int" id="5043"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="of_int"/>
</ls_pos>
<ls_pos name="size_bv" id="5064"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="size_bv"/>
</ls_pos>
<ls_pos name="ugt" id="5093"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="ugt"/>
</ls_pos>
<ls_pos name="uge" id="5104"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="uge"/>
</ls_pos>
<ls_pos name="sge" id="5148"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="sge"/>
</ls_pos>
<ls_pos name="add" id="5157"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="add"/>
</ls_pos>
<ls_pos name="sub" id="5168"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="sub"/>
</ls_pos>
<ls_pos name="neg" id="5179"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="neg"/>
</ls_pos>
<ls_pos name="mul" id="5183"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="mul"/>
</ls_pos>
<ls_pos name="udiv" id="5194"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="udiv"/>
</ls_pos>
<ls_pos name="urem" id="5200"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="urem"/>
</ls_pos>
<ls_pos name="lsr_bv" id="5206"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsr_bv"/>
</ls_pos>
<ls_pos name="asr_bv" id="5217"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="asr_bv"/>
</ls_pos>
<ls_pos name="lsl_bv" id="5223"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="lsl_bv"/>
</ls_pos>
<ls_pos name="nth_bv" id="5246"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="nth_bv"/>
</ls_pos>
<ls_pos name="eq_sub_bv" id="5261"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="eq_sub_bv"/>
</ls_pos>
<ls_pos name="eq_sub" id="5275"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="eq_sub"/>
</ls_pos>
<ls_pos name="eq" id="5305"
ip_theory="BV32">
<ip_library name="bv"/>
<ip_qualid name="eq"/>
</ls_pos>
<pr_pos name="Assoc" id="1951"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Unit_def_l" id="1958"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Unit_def_l"/>
</pr_pos>
<pr_pos name="Unit_def_r" id="1961"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Unit_def_r"/>
</pr_pos>
<pr_pos name="Inv_def_l" id="1964"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_l"/>
</pr_pos>
<pr_pos name="Inv_def_r" id="1967"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_r"/>
</pr_pos>
<pr_pos name="Comm" id="1970"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Assoc" id="1975"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Assoc"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Mul_distr_l" id="1982"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_l"/>
</pr_pos>
<pr_pos name="Mul_distr_r" id="1989"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_r"/>
</pr_pos>
<pr_pos name="Comm" id="2007"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Unitary" id="2012"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Unitary"/>
</pr_pos>
<pr_pos name="NonTrivialRing" id="2015"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="NonTrivialRing"/>
</pr_pos>
<pr_pos name="Refl" id="2027"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Refl"/>
</pr_pos>
<pr_pos name="Trans" id="2030"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Trans"/>
</pr_pos>
<pr_pos name="Antisymm" id="2037"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Antisymm"/>
</pr_pos>
<pr_pos name="Total" id="2042"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Total"/>
</pr_pos>
<pr_pos name="ZeroLessOne" id="2047"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="ZeroLessOne"/>
</pr_pos>
<pr_pos name="CompatOrderAdd" id="2048"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderAdd"/>
</pr_pos>
<pr_pos name="CompatOrderMult" id="2055"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderMult"/>
</pr_pos>
<pr_pos name="Abs_le" id="2068"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="Abs_le"/>
</pr_pos>
<pr_pos name="Abs_pos" id="2073"
ip_theory="Abs">
<ip_library name="int"/>
<ip_qualid name="Abs_pos"/>
</pr_pos>
<pr_pos name="Div_mod" id="2194"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_mod"/>
</pr_pos>
<pr_pos name="Mod_bound" id="2199"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_bound"/>
</pr_pos>
<pr_pos name="Div_unique" id="2204"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_unique"/>
</pr_pos>
<pr_pos name="Div_bound" id="2211"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_bound"/>
</pr_pos>
<pr_pos name="Mod_1" id="2216"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_1"/>
</pr_pos>
<pr_pos name="Div_1" id="2219"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_1"/>
</pr_pos>
<pr_pos name="Div_inf" id="2222"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_inf"/>
</pr_pos>
<pr_pos name="Div_inf_neg" id="2227"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_inf_neg"/>
</pr_pos>
<pr_pos name="Mod_0" id="2232"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_0"/>
</pr_pos>
<pr_pos name="Div_1_left" id="2235"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_1_left"/>
</pr_pos>
<pr_pos name="Div_minus1_left" id="2238"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_minus1_left"/>
</pr_pos>
<pr_pos name="Mod_1_left" id="2241"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_1_left"/>
</pr_pos>
<pr_pos name="Mod_minus1_left" id="2244"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_minus1_left"/>
</pr_pos>
<pr_pos name="Div_mult" id="2247"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Div_mult"/>
</pr_pos>
<pr_pos name="Mod_mult" id="2254"
ip_theory="EuclideanDivision">
<ip_library name="int"/>
<ip_qualid name="Mod_mult"/>
</pr_pos>
<pr_pos name="extensionality" id="2826"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="extensionality"/>
</pr_pos>
<pr_pos name="subset_refl" id="2844"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="subset_refl"/>
</pr_pos>
<pr_pos name="subset_trans" id="2847"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="subset_trans"/>
</pr_pos>