Commit 917cd4c9 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

split_vc: perform generalize_introduced before splitting

parent adc66fc1
...@@ -10,7 +10,6 @@ ...@@ -10,7 +10,6 @@
<file name="../toom.mlw" proved="true"> <file name="../toom.mlw" proved="true">
<theory name="Toom" proved="true"> <theory name="Toom" proved="true">
<goal name="VC toom22_threshold" expl="VC for toom22_threshold" proved="true"> <goal name="VC toom22_threshold" expl="VC for toom22_threshold" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -139,12 +138,12 @@ ...@@ -139,12 +138,12 @@
</goal> </goal>
<goal name="VC toom22_mul.26" expl="precondition" proved="true"> <goal name="VC toom22_mul.26" expl="precondition" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
<goal name="VC toom22_mul.26.0" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.26.0" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC toom22_mul.26.1" expl="VC for toom22_mul" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof> <proof prover="1"><result status="valid" time="0.09"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.26.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.27" expl="precondition" proved="true"> <goal name="VC toom22_mul.27" expl="precondition" proved="true">
...@@ -174,23 +173,23 @@ ...@@ -174,23 +173,23 @@
<transf name="inline_goal" proved="true" > <transf name="inline_goal" proved="true" >
<goal name="VC toom22_mul.34.0.0" expl="precondition" proved="true"> <goal name="VC toom22_mul.34.0.0" expl="precondition" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
<goal name="VC toom22_mul.34.0.0.0" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.34.0.0.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.15"/></proof> <proof prover="3"><result status="valid" time="0.15"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.34.0.0.1" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.34.0.0.1" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.34.0.0.2" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.34.0.0.2" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.15"/></proof> <proof prover="3"><result status="valid" time="0.15"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.34.0.0.3" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.34.0.0.3" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.13"/></proof> <proof prover="3"><result status="valid" time="0.11"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.34.0.0.4" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.34.0.0.4" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.34.0.0.5" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.34.0.0.5" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.11"/></proof> <proof prover="3"><result status="valid" time="0.13"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -214,17 +213,14 @@ ...@@ -214,17 +213,14 @@
<proof prover="5"><result status="valid" time="0.63" steps="140"/></proof> <proof prover="5"><result status="valid" time="0.63" steps="140"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.40" expl="postcondition" proved="true"> <goal name="VC toom22_mul.40" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.41" expl="postcondition" proved="true"> <goal name="VC toom22_mul.41" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.42" expl="postcondition" proved="true"> <goal name="VC toom22_mul.42" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -253,17 +249,14 @@ ...@@ -253,17 +249,14 @@
<proof prover="1"><result status="valid" time="0.11"/></proof> <proof prover="1"><result status="valid" time="0.11"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.51" expl="postcondition" proved="true"> <goal name="VC toom22_mul.51" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.52" expl="postcondition" proved="true"> <goal name="VC toom22_mul.52" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.53" expl="postcondition" proved="true"> <goal name="VC toom22_mul.53" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -322,17 +315,14 @@ ...@@ -322,17 +315,14 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.93" steps="221"/></proof> <proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.93" steps="221"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.72" expl="postcondition" proved="true"> <goal name="VC toom22_mul.72" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.73" expl="postcondition" proved="true"> <goal name="VC toom22_mul.73" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.74" expl="postcondition" proved="true"> <goal name="VC toom22_mul.74" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -382,24 +372,24 @@ ...@@ -382,24 +372,24 @@
<goal name="VC toom22_mul.86.0" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.86.0" expl="VC for toom22_mul" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
<goal name="VC toom22_mul.86.0.0" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.86.0.0" expl="VC for toom22_mul" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="2.48" steps="152"/></proof> <proof prover="5" timelimit="5"><result status="valid" time="0.46" steps="154"/></proof>
</goal>
<goal name="VC toom22_mul.86.0.1" expl="VC for toom22_mul" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="1.96" steps="153"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.87" expl="postcondition" proved="true"> <goal name="VC toom22_mul.87" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.88" expl="postcondition" proved="true"> <goal name="VC toom22_mul.88" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.89" expl="postcondition" proved="true"> <goal name="VC toom22_mul.89" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -437,22 +427,18 @@ ...@@ -437,22 +427,18 @@
<proof prover="1"><result status="valid" time="0.15"/></proof> <proof prover="1"><result status="valid" time="0.15"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.101" expl="postcondition" proved="true"> <goal name="VC toom22_mul.101" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.102" expl="postcondition" proved="true"> <goal name="VC toom22_mul.102" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.103" expl="postcondition" proved="true"> <goal name="VC toom22_mul.103" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.104" expl="postcondition" proved="true"> <goal name="VC toom22_mul.104" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -481,22 +467,18 @@ ...@@ -481,22 +467,18 @@
<proof prover="5"><result status="valid" time="0.81" steps="144"/></proof> <proof prover="5"><result status="valid" time="0.81" steps="144"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.113" expl="postcondition" proved="true"> <goal name="VC toom22_mul.113" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.114" expl="postcondition" proved="true"> <goal name="VC toom22_mul.114" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.115" expl="postcondition" proved="true"> <goal name="VC toom22_mul.115" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.116" expl="postcondition" proved="true"> <goal name="VC toom22_mul.116" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -546,7 +528,6 @@ ...@@ -546,7 +528,6 @@
<proof prover="3"><result status="valid" time="0.01"/></proof> <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.132" expl="assertion" proved="true"> <goal name="VC toom22_mul.132" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -562,23 +543,23 @@ ...@@ -562,23 +543,23 @@
<transf name="inline_goal" proved="true" > <transf name="inline_goal" proved="true" >
<goal name="VC toom22_mul.135.0.0" expl="precondition" proved="true"> <goal name="VC toom22_mul.135.0.0" expl="precondition" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
<goal name="VC toom22_mul.135.0.0.0" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.135.0.0.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof> <proof prover="3"><result status="valid" time="0.07"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.135.0.0.1" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.135.0.0.1" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof> <proof prover="3"><result status="valid" time="0.05"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.135.0.0.2" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.135.0.0.2" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof> <proof prover="3"><result status="valid" time="0.06"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.135.0.0.3" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.135.0.0.3" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof> <proof prover="5"><result status="valid" time="0.69" steps="171"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.135.0.0.4" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.135.0.0.4" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof> <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.135.0.0.5" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.135.0.0.5" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="1.36" steps="234"/></proof> <proof prover="3"><result status="valid" time="0.08"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -613,22 +594,18 @@ ...@@ -613,22 +594,18 @@
<proof prover="1"><result status="valid" time="0.08"/></proof> <proof prover="1"><result status="valid" time="0.08"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.142" expl="postcondition" proved="true"> <goal name="VC toom22_mul.142" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.143" expl="postcondition" proved="true"> <goal name="VC toom22_mul.143" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.144" expl="postcondition" proved="true"> <goal name="VC toom22_mul.144" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.145" expl="postcondition" proved="true"> <goal name="VC toom22_mul.145" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -692,23 +669,23 @@ ...@@ -692,23 +669,23 @@
<transf name="inline_goal" proved="true" > <transf name="inline_goal" proved="true" >
<goal name="VC toom22_mul.152.0.0" expl="precondition" proved="true"> <goal name="VC toom22_mul.152.0.0" expl="precondition" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
<goal name="VC toom22_mul.152.0.0.0" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.152.0.0.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof> <proof prover="3"><result status="valid" time="0.06"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.152.0.0.1" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.152.0.0.1" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.152.0.0.2" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.152.0.0.2" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof> <proof prover="3"><result status="valid" time="0.05"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.152.0.0.3" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.152.0.0.3" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="5"><result status="valid" time="0.71" steps="154"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.152.0.0.4" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.152.0.0.4" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.152.0.0.5" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.152.0.0.5" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="1.08" steps="155"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -732,22 +709,18 @@ ...@@ -732,22 +709,18 @@
<proof prover="1"><result status="valid" time="0.06"/></proof> <proof prover="1"><result status="valid" time="0.06"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.158" expl="postcondition" proved="true"> <goal name="VC toom22_mul.158" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.159" expl="postcondition" proved="true"> <goal name="VC toom22_mul.159" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.160" expl="postcondition" proved="true"> <goal name="VC toom22_mul.160" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.161" expl="postcondition" proved="true"> <goal name="VC toom22_mul.161" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -779,11 +752,7 @@ ...@@ -779,11 +752,7 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="1.19" steps="287"/></proof> <proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="1.19" steps="287"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.171" expl="assertion" proved="true"> <goal name="VC toom22_mul.171" expl="assertion" proved="true">
<transf name="split_vc" proved="true" > <proof prover="5" timelimit="5"><result status="valid" time="0.45" steps="149"/></proof>
<goal name="VC toom22_mul.171.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="VC toom22_mul.172" expl="precondition" proved="true"> <goal name="VC toom22_mul.172" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
...@@ -810,19 +779,14 @@ ...@@ -810,19 +779,14 @@
<proof prover="5"><result status="valid" time="1.36" steps="224"/></proof> <proof prover="5"><result status="valid" time="1.36" steps="224"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.180" expl="assertion" proved="true"> <goal name="VC toom22_mul.180" expl="assertion" proved="true">
<transf name="split_vc" proved="true" > <proof prover="5" timelimit="5"><result status="valid" time="0.53" steps="161"/></proof>
<goal name="VC toom22_mul.180.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.12"/></proof>
<proof prover="4"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="VC toom22_mul.181" expl="assertion" proved="true"> <goal name="VC toom22_mul.181" expl="assertion" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
<goal name="VC toom22_mul.181.0" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.181.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.181.1" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.181.1" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</transf> </transf>
...@@ -894,11 +858,7 @@ ...@@ -894,11 +858,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof> <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.204" expl="precondition" proved="true"> <goal name="VC toom22_mul.204" expl="precondition" proved="true">
<transf name="split_vc" proved="true" > <proof prover="3" timelimit="5"><result status="valid" time="0.04"/></proof>
<goal name="VC toom22_mul.204.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="VC toom22_mul.205" expl="precondition" proved="true"> <goal name="VC toom22_mul.205" expl="precondition" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="1.21" steps="356"/></proof> <proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="1.21" steps="356"/></proof>
...@@ -913,17 +873,14 @@ ...@@ -913,17 +873,14 @@
<proof prover="5"><result status="valid" time="1.67" steps="185"/></proof> <proof prover="5"><result status="valid" time="1.67" steps="185"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.209" expl="postcondition" proved="true"> <goal name="VC toom22_mul.209" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.210" expl="postcondition" proved="true"> <goal name="VC toom22_mul.210" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.211" expl="postcondition" proved="true"> <goal name="VC toom22_mul.211" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -1015,17 +972,14 @@ ...@@ -1015,17 +972,14 @@
<proof prover="0"><result status="valid" time="0.10"/></proof> <proof prover="0"><result status="valid" time="0.10"/></proof>
</goal> </goal>
<goal name="VC toom22_mul.241" expl="postcondition" proved="true"> <goal name="VC toom22_mul.241" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.242" expl="postcondition" proved="true"> <goal name="VC toom22_mul.242" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
<goal name="VC toom22_mul.243" expl="postcondition" proved="true"> <goal name="VC toom22_mul.243" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
</transf> </transf>
</goal> </goal>
...@@ -1092,24 +1046,24 @@ ...@@ -1092,24 +1046,24 @@
<transf name="inline_goal" proved="true" > <transf name="inline_goal" proved="true" >
<goal name="VC toom22_mul.263.0.0" expl="precondition" proved="true"> <goal name="VC toom22_mul.263.0.0" expl="precondition" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
<goal name="VC toom22_mul.263.0.0.0" expl="VC for toom22_mul" proved="true"> <goal name="VC toom22_mul.263.0.0.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>