Commit 09a173bc authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

fix session

parent f174cf1b
......@@ -9,8 +9,6 @@
<prover id="4" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Spass" version="3.7" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.7.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="9" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../div.mlw" proved="true">
<theory name="Div" proved="true">
......@@ -5964,11 +5962,6 @@
<proof prover="1" timelimit="20"><result status="valid" time="7.30"/></proof>
</goal>
<goal name="VC div_sb_qr.233" expl="assertion" proved="true">
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="timeout" time="1.00"/></proof>
<proof prover="8"><result status="timeout" time="1.00"/></proof>
<proof prover="9"><result status="timeout" time="1.00"/></proof>
<transf name="introduce_premises" proved="true" >
<goal name="VC div_sb_qr.233.0" expl="assertion" proved="true">
<transf name="use_th" proved="true" arg1="lineardecision.EqPropMP">
......@@ -5978,1751 +5971,653 @@
<proof prover="2"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1" expl="assertion" proved="true">
<transf name="rewrite" proved="true" arg1="h" arg2="in" arg3="H189">
<transf name="reflection_f" proved="true" arg1="prop_mp_decision">
<goal name="VC div_sb_qr.233.0.0.1.0" expl="assertion" proved="true">
<transf name="rewrite" proved="true" arg1="h" arg2="in" arg3="H134">
<goal name="VC div_sb_qr.233.0.0.1.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="prop_mp_decision">
<goal name="VC div_sb_qr.233.0.0.1.0.0.0" expl="assertion" proved="true">
<transf name="apply" proved="true" arg1="HR">
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.0" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.1" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.2" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.3" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.4" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.5" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.6" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.7" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.8" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.9" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.10" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.11" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.12" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.13" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.14" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.15" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.16" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.17" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.18" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.19" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.20" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.21" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.22" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.23" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.24" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.25" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.26" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.27" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.28" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.29" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.30" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.31" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.32" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.33" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.34" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.35" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.36" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.37" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.38" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.39" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.40" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.41" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.42" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.43" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.44" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.45" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.46" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.47" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.48" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.49" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.50" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.51" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.52" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.53" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.54" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.55" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.56" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.57" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.58" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.59" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.60" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.61" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.62" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.63" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.64" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.65" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.66" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.67" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.68" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.69" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.70" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.71" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.72" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.73" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.74" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.75" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.76" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.77" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.78" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.79" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.80" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.81" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.82" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.83" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.84" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.85" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.86" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.87" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.88" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.89" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.90" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.91" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.92" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.93" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.94" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.95" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.96" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.97" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.98" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.99" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.100" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.101" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.102" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.103" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.104" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.105" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.106" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.107" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.108" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.109" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.110" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.111" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.112" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.113" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.114" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.115" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.116" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.117" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.118" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.119" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.120" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.121" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.122" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.123" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.124" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.125" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.126" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.127" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.128" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.129" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.130" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.131" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.132" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.133" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.134" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.135" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.136" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.137" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.138" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.139" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.140" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.141" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.142" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.143" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.144" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.145" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.146" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.147" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.148" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.149" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.150" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.151" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.152" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.153" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.154" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.155" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.156" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.157" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.158" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.159" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.160" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.161" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.162" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.163" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.164" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.165" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.166" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.167" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.168" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.169" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.170" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.171" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.172" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.173" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.174" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.175" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.176" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.177" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC div_sb_qr.233.0.0.1.0.0.0.178" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>