Commit 912aac9f authored by MARCHE Claude's avatar MARCHE Claude

Fix nightly bench

parent f0b52f95
This diff is collapsed.
......@@ -4,90 +4,91 @@
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.3.1" timelimit="10" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../coincidence_count.mlw" expanded="true">
<theory name="CoincidenceCount" sum="c8fb7856ca9e35d98067c6b03ff5c8e4" expanded="true">
<goal name="drop_left" expanded="true">
<proof prover="1"><result status="valid" time="0.80" steps="1147"/></proof>
<goal name="drop_left">
<proof prover="2"><result status="valid" time="0.15" steps="486"/></proof>
</goal>
<goal name="not_mem_inter_r" expanded="true">
<goal name="not_mem_inter_r">
<proof prover="1"><result status="valid" time="1.02" steps="585"/></proof>
</goal>
<goal name="not_mem_inter_l" expanded="true">
<goal name="not_mem_inter_l">
<proof prover="1"><result status="valid" time="1.01" steps="585"/></proof>
</goal>
<goal name="WP_parameter coincidence_count" expl="VC for coincidence_count" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter coincidence_count.1" expl="1. loop invariant init" expanded="true">
<goal name="WP_parameter coincidence_count.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.2" expl="2. loop invariant init" expanded="true">
<goal name="WP_parameter coincidence_count.2" expl="2. loop invariant init">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.3" expl="3. loop invariant init" expanded="true">
<goal name="WP_parameter coincidence_count.3" expl="3. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.4" expl="4. index in array bounds" expanded="true">
<goal name="WP_parameter coincidence_count.4" expl="4. index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.5" expl="5. index in array bounds" expanded="true">
<goal name="WP_parameter coincidence_count.5" expl="5. index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.6" expl="6. loop invariant preservation" expanded="true">
<goal name="WP_parameter coincidence_count.6" expl="6. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.7" expl="7. loop invariant preservation" expanded="true">
<goal name="WP_parameter coincidence_count.7" expl="7. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.8" expl="8. loop invariant preservation" expanded="true">
<goal name="WP_parameter coincidence_count.8" expl="8. loop invariant preservation">
<proof prover="1"><result status="valid" time="1.19" steps="375"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.9" expl="9. loop variant decrease" expanded="true">
<goal name="WP_parameter coincidence_count.9" expl="9. loop variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.10" expl="10. index in array bounds" expanded="true">
<goal name="WP_parameter coincidence_count.10" expl="10. index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.11" expl="11. index in array bounds" expanded="true">
<goal name="WP_parameter coincidence_count.11" expl="11. index in array bounds">
<proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.12" expl="12. loop invariant preservation" expanded="true">
<goal name="WP_parameter coincidence_count.12" expl="12. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.13" expl="13. loop invariant preservation" expanded="true">
<goal name="WP_parameter coincidence_count.13" expl="13. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.14" expl="14. loop invariant preservation" expanded="true">
<goal name="WP_parameter coincidence_count.14" expl="14. loop invariant preservation">
<proof prover="1"><result status="valid" time="1.29" steps="376"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.15" expl="15. loop variant decrease" expanded="true">
<goal name="WP_parameter coincidence_count.15" expl="15. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.16" expl="16. assertion" expanded="true">
<goal name="WP_parameter coincidence_count.16" expl="16. assertion">
<proof prover="0"><result status="valid" time="2.23"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.17" expl="17. assertion" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="WP_parameter coincidence_count.17.1" expl="1. assertion" expanded="true">
<goal name="WP_parameter coincidence_count.17" expl="17. assertion">
<transf name="inline_goal">
<goal name="WP_parameter coincidence_count.17.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.69" steps="302"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter coincidence_count.18" expl="18. loop invariant preservation" expanded="true">
<goal name="WP_parameter coincidence_count.18" expl="18. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.19" expl="19. loop invariant preservation" expanded="true">
<goal name="WP_parameter coincidence_count.19" expl="19. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.20" expl="20. loop invariant preservation" expanded="true">
<goal name="WP_parameter coincidence_count.20" expl="20. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.70" steps="167"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.21" expl="21. loop variant decrease" expanded="true">
<goal name="WP_parameter coincidence_count.21" expl="21. loop variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.22" expl="22. postcondition" expanded="true">
<goal name="WP_parameter coincidence_count.22" expl="22. postcondition">
<proof prover="1"><result status="valid" time="0.08" steps="109"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.23" expl="23. postcondition" expanded="true">
<goal name="WP_parameter coincidence_count.23" expl="23. postcondition">
<proof prover="1"><result status="valid" time="0.08" steps="108"/></proof>
</goal>
</transf>
......
......@@ -16,7 +16,7 @@
<file name="../mergesort_array.mlw" expanded="true">
<theory name="Elt" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Merge" sum="f74a571cba2d178cff9430cfa205e5f0">
<theory name="Merge" sum="f74a571cba2d178cff9430cfa205e5f0" expanded="true">
<goal name="WP_parameter merge" expl="VC for merge">
<transf name="split_goal_wp">
<goal name="WP_parameter merge.1" expl="1. postcondition">
......@@ -490,7 +490,7 @@
</transf>
</goal>
</theory>
<theory name="TopDownMergesort" sum="922fab320c7b139966ac3aec4ab18b47">
<theory name="TopDownMergesort" sum="922fab320c7b139966ac3aec4ab18b47" expanded="true">
<goal name="WP_parameter mergesort_rec" expl="VC for mergesort_rec">
<transf name="split_goal_wp">
<goal name="WP_parameter mergesort_rec.1" expl="1. division by zero">
......@@ -589,7 +589,7 @@
<proof prover="9"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="BottomUpMergesort" sum="118377a4f46d4dfa609fb0951e6f3d4e">
<theory name="BottomUpMergesort" sum="118377a4f46d4dfa609fb0951e6f3d4e" expanded="true">
<goal name="WP_parameter bottom_up_mergesort" expl="VC for bottom_up_mergesort">
<transf name="split_goal_wp">
<goal name="WP_parameter bottom_up_mergesort.1" expl="1. loop invariant init">
......@@ -705,10 +705,7 @@
<goal name="WP_parameter bottom_up_mergesort.20.2" expl="2. assertion">
<proof prover="2"><result status="valid" time="1.37" steps="158"/></proof>
<proof prover="4"><result status="valid" time="0.38"/></proof>
<proof prover="6"><result status="valid" time="0.06"/></proof>
<proof prover="7"><result status="valid" time="0.07"/></proof>
<proof prover="9"><result status="valid" time="0.04"/></proof>
<proof prover="10" timelimit="5"><result status="valid" time="0.56"/></proof>
</goal>
</transf>
</goal>
......@@ -851,7 +848,7 @@
</transf>
</goal>
</theory>
<theory name="NaturalMergesort" sum="6754450ec8389180aa10a1c38a5b0a9e">
<theory name="NaturalMergesort" sum="6754450ec8389180aa10a1c38a5b0a9e" expanded="true">
<goal name="WP_parameter find_run" expl="VC for find_run">
<transf name="split_goal_wp">
<goal name="WP_parameter find_run.1" expl="1. loop invariant init">
......
This diff is collapsed.
......@@ -701,14 +701,6 @@
<proof prover="4"><result status="valid" time="0.10" steps="48"/></proof>
</goal>
</theory>
<theory name="RandomSolver" sum="9972114a2bccda157e2154eda59d32bd" expanded="true">
<goal name="WP_parameter solve_aux" expl="VC for solve_aux" expanded="true">
</goal>
<goal name="WP_parameter solve" expl="VC for solve" expanded="true">
</goal>
<goal name="WP_parameter check_then_solve" expl="VC for check_then_solve" expanded="true">
</goal>
</theory>
<theory name="Test" sum="8351ae643fa75ec6f93e5f543be80ac2" expanded="true">
<goal name="WP_parameter test0" expl="VC for test0">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......@@ -719,9 +711,7 @@
</goal>
<goal name="valid_values_solvable">
<proof prover="0"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.98"/></proof>
<proof prover="7"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter test1" expl="VC for test1">
<proof prover="0"><result status="valid" time="1.12"/></proof>
......
......@@ -8,6 +8,7 @@
<prover id="3" name="Z3" version="3.2" timelimit="10" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="4000"/>
<prover id="5" name="CVC4" version="1.3" timelimit="10" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../verifythis_PrefixSumRec.mlw" expanded="true">
<theory name="PrefixSumRec" sum="6d81c9f0aa6d78cffe93173557ccd286" expanded="true">
<goal name="Div_mod_2">
......@@ -319,9 +320,8 @@
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter downsweep.11" expl="11. assertion">
<proof prover="0"><result status="valid" time="10.22"/></proof>
<proof prover="4"><result status="valid" time="0.23" steps="65"/></proof>
<proof prover="5"><result status="valid" time="0.83"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.55"/></proof>
<proof prover="6"><result status="valid" time="0.12" steps="58"/></proof>
</goal>
<goal name="WP_parameter downsweep.12" expl="12. variant decrease">
<proof prover="4"><result status="valid" time="0.02" steps="22"/></proof>
......@@ -341,10 +341,8 @@
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter downsweep.15" expl="15. precondition">
<proof prover="0"><result status="valid" time="1.15"/></proof>
<proof prover="3"><result status="valid" time="4.95"/></proof>
<proof prover="4"><result status="valid" time="0.06" steps="50"/></proof>
<proof prover="5"><result status="valid" time="0.34"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.23"/></proof>
<proof prover="6"><result status="valid" time="0.11" steps="42"/></proof>
</goal>
<goal name="WP_parameter downsweep.16" expl="16. precondition">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......
......@@ -14,6 +14,8 @@
<prover id="9" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="4000"/>
<prover id="10" name="CVC4" version="1.3" timelimit="5" memlimit="4000"/>
<prover id="11" name="Vampire" version="0.6" timelimit="5" memlimit="4000"/>
<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="13" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../verifythis_fm2012_LRS.mlw" expanded="true">
<theory name="LCP" sum="005205768844ee0b7ae11fcc8290692b" expanded="true">
<goal name="not_common_prefix_if_last_char_are_different">
......@@ -640,10 +642,8 @@
<proof prover="11"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter sort.23" expl="23. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.05"/></proof>
<proof prover="6"><result status="valid" time="0.05"/></proof>
<proof prover="9"><result status="valid" time="1.84" steps="220"/></proof>
<proof prover="12"><result status="valid" time="2.25" steps="411"/></proof>
<proof prover="13"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter sort.24" expl="24. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -660,9 +660,8 @@
<proof prover="10"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter sort.26" expl="26. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.08"/></proof>
<proof prover="6"><result status="valid" time="0.08"/></proof>
<proof prover="12"><result status="valid" time="4.62" steps="697"/></proof>
<proof prover="13"><result status="valid" time="0.76"/></proof>
</goal>
<goal name="WP_parameter sort.27" expl="27. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.08"/></proof>
......
......@@ -46,7 +46,7 @@
</transf>
</goal>
</theory>
<theory name="BFS" sum="133103db518ef60f8e79ea66ecc9e6bf" expanded="true">
<theory name="BFS" sum="5846be4f5e134b08034954a2eaf8f555" expanded="true">
<goal name="WP_parameter fill_next" expl="VC for fill_next">
<transf name="split_goal_wp">
<goal name="WP_parameter fill_next.1" expl="1. loop invariant init">
......@@ -113,8 +113,8 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter bfs" expl="VC for bfs" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter bfs" expl="VC for bfs">
<transf name="split_goal_wp">
<goal name="WP_parameter bfs.1" expl="1. loop invariant init">
<transf name="split_goal_wp">
<goal name="WP_parameter bfs.1.1" expl="1. VC for bfs">
......@@ -177,558 +177,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter bfs.5.1.1.5" expl="5. VC for bfs">
<proof prover="2" timelimit="5"><result status="timeout" time="4.99"/></proof>
<proof prover="7"><result status="timeout" time="4.96"/></proof>
<metas>
<ts_pos name="ref" arity="1" id="3533"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="ref"/>
</ts_pos>
<ts_pos name="t" arity="1" id="3682"
ip_theory="Impset">
<ip_library name="impset"/>
<ip_qualid name="t"/>
</ts_pos>
<ls_pos name="zero" id="221"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="zero"/>
</ls_pos>
<ls_pos name="one" id="222"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="one"/>
</ls_pos>
<ls_pos name="infix &lt;" id="223"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &lt;"/>
</ls_pos>
<ls_pos name="infix &gt;" id="226"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &gt;"/>
</ls_pos>
<ls_pos name="infix +" id="1392"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix +"/>
</ls_pos>
<ls_pos name="prefix -" id="1393"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="prefix -"/>
</ls_pos>
<ls_pos name="infix *" id="1394"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix *"/>
</ls_pos>
<ls_pos name="infix -" id="1442"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix -"/>
</ls_pos>
<ls_pos name="infix &gt;=" id="1462"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &gt;="/>
</ls_pos>
<ls_pos name="mem" id="2554"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="mem"/>
</ls_pos>
<ls_pos name="infix ==" id="2557"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="infix =="/>
</ls_pos>
<ls_pos name="empty" id="2596"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="empty"/>
</ls_pos>
<ls_pos name="is_empty" id="2598"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="is_empty"/>
</ls_pos>
<ls_pos name="add" id="2608"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="add"/>
</ls_pos>
<ls_pos name="singleton" id="2614"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="singleton"/>
</ls_pos>
<ls_pos name="remove" id="2619"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="remove"/>
</ls_pos>
<ls_pos name="union" id="2637"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="union"/>
</ls_pos>
<ls_pos name="inter" id="2644"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="inter"/>
</ls_pos>
<ls_pos name="diff" id="2651"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="diff"/>
</ls_pos>
<ls_pos name="choose" id="2663"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="choose"/>
</ls_pos>
<ls_pos name="cardinal" id="2667"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="cardinal"/>
</ls_pos>
<ls_pos name="succ" id="3464"
ip_theory="Graph">
<ip_qualid name="succ"/>
</ls_pos>
<ls_pos name="prefix !" id="3539"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="prefix !"/>
</ls_pos>
<ls_pos name="inv" id="3775" ip_theory="BFS">
<ip_qualid name="inv"/>
</ls_pos>
<ls_pos name="closure" id="3834"
ip_theory="BFS">
<ip_qualid name="closure"/>
</ls_pos>
<pr_pos name="Assoc" id="1395"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Unit_def_l" id="1402"
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="1405"
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="1408"
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="1411"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_r"/>
</pr_pos>
<pr_pos name="Comm" id="1414"
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="1419"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Assoc"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Mul_distr_l" id="1426"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_l"/>
</pr_pos>
<pr_pos name="Mul_distr_r" id="1433"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_r"/>
</pr_pos>
<pr_pos name="Comm" id="1451"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Unitary" id="1456"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Unitary"/>
</pr_pos>
<pr_pos name="NonTrivialRing" id="1459"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="NonTrivialRing"/>
</pr_pos>
<pr_pos name="Refl" id="1471"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Refl"/>
</pr_pos>
<pr_pos name="Trans" id="1474"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Trans"/>
</pr_pos>
<pr_pos name="Antisymm" id="1481"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Antisymm"/>
</pr_pos>
<pr_pos name="Total" id="1486"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Total"/>
</pr_pos>
<pr_pos name="ZeroLessOne" id="1491"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="ZeroLessOne"/>
</pr_pos>
<pr_pos name="CompatOrderAdd" id="1492"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderAdd"/>
</pr_pos>
<pr_pos name="CompatOrderMult" id="1499"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderMult"/>
</pr_pos>
<pr_pos name="extensionality" id="2568"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="extensionality"/>
</pr_pos>
<pr_pos name="subset_refl" id="2586"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="subset_refl"/>
</pr_pos>
<pr_pos name="subset_trans" id="2589"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="subset_trans"/>
</pr_pos>
<pr_pos name="empty_def1" id="2605"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="empty_def1"/>
</pr_pos>
<pr_pos name="mem_empty" id="2606"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="mem_empty"/>
</pr_pos>
<pr_pos name="add_def1" id="2609"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="add_def1"/>
</pr_pos>
<pr_pos name="remove_def1" id="2620"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="remove_def1"/>
</pr_pos>
<pr_pos name="subset_remove" id="2633"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="subset_remove"/>
</pr_pos>
<pr_pos name="union_def1" id="2638"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="union_def1"/>
</pr_pos>
<pr_pos name="inter_def1" id="2645"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="inter_def1"/>
</pr_pos>
<pr_pos name="diff_def1" id="2652"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="diff_def1"/>
</pr_pos>
<pr_pos name="subset_diff" id="2658"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="subset_diff"/>
</pr_pos>
<pr_pos name="choose_def" id="2664"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="choose_def"/>
</pr_pos>
<pr_pos name="cardinal_nonneg" id="2669"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="cardinal_nonneg"/>
</pr_pos>
<pr_pos name="cardinal_empty" id="2672"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="cardinal_empty"/>
</pr_pos>
<pr_pos name="cardinal_add" id="2675"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="cardinal_add"/>
</pr_pos>
<pr_pos name="cardinal_remove" id="2680"
ip_theory="Fset">
<ip_library name="set"/>
<ip_qualid name="cardinal_remove"/>