Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
7b48b2c1
Commit
7b48b2c1
authored
Feb 01, 2016
by
MARCHE Claude
Browse files
sessions: upgrade isabelle 2014 to 2015
parent
93445554
Changes
1
Hide whitespace changes
Inline
Side-by-side
examples/logic/genealogy/why3session.xml
View file @
7b48b2c1
...
...
@@ -2,37 +2,37 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"
1
"
name=
"
CVC4
"
version=
"
1.2
"
timelimit=
"
60
"
memlimit=
"
1
000"
/>
<prover
id=
"
2
"
name=
"
Zenon
"
version=
"
0.8.0
"
timelimit=
"
5
"
memlimit=
"1000"
/>
<prover
id=
"
3
"
name=
"
CVC3
"
version=
"
2.4.1
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"
4
"
name=
"
Eprover
"
version=
"
1.6
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"
5
"
name=
"
Z3
"
version=
"
2.19
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"
6
"
name=
"
CVC4
"
version=
"
1.4
"
timelimit=
"5"
memlimit=
"
100
0"
/>
<prover
id=
"
7
"
name=
"CVC
3
"
version=
"
2.2
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"
8
"
name=
"
Eprover
"
version=
"
1.4
"
timelimit=
"
3
"
memlimit=
"
100
0"
/>
<prover
id=
"
9
"
name=
"
Spass
"
version=
"
3.7
"
timelimit=
"
5
"
memlimit=
"0"
/>
<prover
id=
"
10
"
name=
"
Z3
"
version=
"
4.
3.
1
"
timelimit=
"5"
memlimit=
"
400
0"
/>
<prover
id=
"1
1
"
name=
"
Simplify
"
version=
"
1.5.4
"
timelimit=
"
3
"
memlimit=
"
1
000"
/>
<prover
id=
"1
2
"
name=
"
Yices
"
version=
"1.
0.38
"
timelimit=
"
5
"
memlimit=
"0"
/>
<prover
id=
"1
3
"
name=
"
Zenon
"
version=
"
0.7.1
"
timelimit=
"5"
memlimit=
"
400
0"
/>
<prover
id=
"1
4
"
name=
"
Isabelle
"
version=
"
2014
"
timelimit=
"5"
memlimit=
"4000"
/>
<prover
id=
"15"
name=
"Metis"
version=
"2.3"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"16"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"17"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"60"
memlimit=
"1000"
/>
<prover
id=
"18"
name=
"PVS"
version=
"6.0"
timelimit=
"5"
memlimit=
"4000"
/>
<prover
id=
"19"
name=
"veriT"
version=
"201310"
timelimit=
"5"
memlimit=
"4000"
/>
<prover
id=
"20"
name=
"Z3"
version=
"4.3.2"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"21"
name=
"CVC4"
version=
"1.3"
timelimit=
"3"
memlimit=
"1000"
/>
<prover
id=
"22"
name=
"Vampire"
version=
"0.6"
timelimit=
"3"
memlimit=
"1000"
/>
<prover
id=
"23"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"24"
name=
"veriT"
version=
"201410"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"25"
name=
"Alt-Ergo"
version=
"1.00.prv"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"26"
name=
"Zenon Modulo"
version=
"0.4.1"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"27"
name=
"Coq"
version=
"8.4pl6"
timelimit=
"5"
memlimit=
"4000"
/>
<prover
id=
"
0
"
name=
"
Isabelle
"
version=
"
2015
"
timelimit=
"
5"
steplimit=
"1
"
memlimit=
"
4
000"
/>
<prover
id=
"
1
"
name=
"
CVC4
"
version=
"
1.2
"
timelimit=
"
60"
steplimit=
"1
"
memlimit=
"1000"
/>
<prover
id=
"
2
"
name=
"
Zenon
"
version=
"
0.8.0
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"
100
0"
/>
<prover
id=
"
3
"
name=
"
CVC3
"
version=
"
2.4.1
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"
4
"
name=
"
Eprover
"
version=
"
1.6
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"
5
"
name=
"
Z3
"
version=
"
2.19
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"
6
"
name=
"CVC
4
"
version=
"
1.4
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"
100
0"
/>
<prover
id=
"
7
"
name=
"
CVC3
"
version=
"
2.2
"
timelimit=
"
5"
steplimit=
"1
"
memlimit=
"0"
/>
<prover
id=
"
8
"
name=
"
Eprover
"
version=
"
1.4
"
timelimit=
"
3"
steplimit=
"1
"
memlimit=
"
100
0"
/>
<prover
id=
"
9
"
name=
"
Spass
"
version=
"3.
7
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"1
0
"
name=
"
Z3
"
version=
"
4.3.1
"
timelimit=
"
5"
steplimit=
"1
"
memlimit=
"
4
000"
/>
<prover
id=
"1
1
"
name=
"
Simplify
"
version=
"1.
5.4
"
timelimit=
"
3"
steplimit=
"1
"
memlimit=
"
100
0"
/>
<prover
id=
"1
2
"
name=
"
Yices
"
version=
"
1.0.38
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"1
3
"
name=
"
Zenon
"
version=
"
0.7.1
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"4000"
/>
<prover
id=
"15"
name=
"Metis"
version=
"2.3"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"16"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"17"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"60"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"18"
name=
"PVS"
version=
"6.0"
timelimit=
"5"
steplimit=
"1"
memlimit=
"4000"
/>
<prover
id=
"19"
name=
"veriT"
version=
"201310"
timelimit=
"5"
steplimit=
"1"
memlimit=
"4000"
/>
<prover
id=
"20"
name=
"Z3"
version=
"4.3.2"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"21"
name=
"CVC4"
version=
"1.3"
timelimit=
"3"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"22"
name=
"Vampire"
version=
"0.6"
timelimit=
"3"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"23"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"24"
name=
"veriT"
version=
"201410"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"25"
name=
"Alt-Ergo"
version=
"1.00.prv"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"26"
name=
"Zenon Modulo"
version=
"0.4.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"27"
name=
"Coq"
version=
"8.4pl6"
timelimit=
"5"
steplimit=
"1"
memlimit=
"4000"
/>
<file
name=
"../genealogy.why"
expanded=
"true"
>
<theory
name=
"Genealogy"
sum=
"35e1439432a79e05534b2c5cf39ad9dc"
expanded=
"true"
>
<goal
name=
"Child_is_son_or_daughter"
expanded=
"true"
>
<proof
prover=
"
1
"
><result
status=
"
unknown
"
time=
"
0.00
"
/></proof>
<goal
name=
"Child_is_son_or_daughter"
>
<proof
prover=
"
0"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.xml
"
><result
status=
"
valid
"
time=
"
6.55
"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
@@ -41,18 +41,14 @@
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"10"
memlimit=
"1000"
><result
status=
"unknown"
time=
"1.66"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"unknown"
time=
"0.01"
/></proof>
<proof
prover=
"13"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"14"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.xml"
><result
status=
"valid"
time=
"5.48"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.01"
steps=
"12"
/></proof>
<proof
prover=
"18"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.pvs"
><result
status=
"valid"
time=
"0.24"
/></proof>
<proof
prover=
"19"
timelimit=
"60"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"21"
><result
status=
"unknown"
time=
"0.00"
/></proof>
<proof
prover=
"22"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"23"
><result
status=
"valid"
time=
"0.01"
steps=
"10"
/></proof>
<proof
prover=
"24"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
@@ -60,9 +56,9 @@
<proof
prover=
"26"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"27"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.v"
><result
status=
"valid"
time=
"0.80"
/></proof>
</goal>
<goal
name=
"Sibling_sym"
expanded=
"true"
>
<goal
name=
"Sibling_sym"
>
<proof
prover=
"0"
edited=
"genealogy_Genealogy_Sibling_sym_1.xml"
><result
status=
"valid"
time=
"6.09"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"timeout"
time=
"5.41"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.01"
/></proof>
...
...
@@ -73,8 +69,6 @@
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"13"
><result
status=
"timeout"
time=
"5.23"
/></proof>
<proof
prover=
"14"
edited=
"genealogy_Genealogy_Sibling_sym_1.xml"
><result
status=
"valid"
time=
"6.09"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.12"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.02"
steps=
"5"
/></proof>
...
...
@@ -87,8 +81,8 @@
<proof
prover=
"25"
><result
status=
"valid"
time=
"0.00"
steps=
"2"
/></proof>
<proof
prover=
"26"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"Sibling_is_brother_or_sister"
expanded=
"true"
>
<proof
prover=
"
1
"
><result
status=
"
unknown
"
time=
"
0.01
"
/></proof>
<goal
name=
"Sibling_is_brother_or_sister"
>
<proof
prover=
"
0"
edited=
"genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml
"
><result
status=
"
valid
"
time=
"
6.19
"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
@@ -97,26 +91,22 @@
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"10"
><result
status=
"unknown"
time=
"1.68"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"unknown"
time=
"0.02"
/></proof>
<proof
prover=
"13"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"14"
edited=
"genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"
><result
status=
"valid"
time=
"6.19"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.02"
steps=
"9"
/></proof>
<proof
prover=
"19"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"21"
><result
status=
"unknown"
time=
"0.01"
/></proof>
<proof
prover=
"22"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"23"
><result
status=
"valid"
time=
"0.01"
steps=
"9"
/></proof>
<proof
prover=
"24"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"25"
><result
status=
"valid"
time=
"0.00"
steps=
"8"
/></proof>
<proof
prover=
"26"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"Grandparent_is_grandfather_or_grandmother"
expanded=
"true"
>
<goal
name=
"Grandparent_is_grandfather_or_grandmother"
>
<proof
prover=
"0"
edited=
"genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"
><result
status=
"valid"
time=
"6.50"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"timeout"
time=
"5.34"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
@@ -126,8 +116,6 @@
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"13"
><result
status=
"timeout"
time=
"5.26"
/></proof>
<proof
prover=
"14"
edited=
"genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"
><result
status=
"valid"
time=
"6.50"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.07"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.02"
steps=
"32"
/></proof>
...
...
@@ -140,9 +128,8 @@
<proof
prover=
"25"
><result
status=
"valid"
time=
"0.00"
steps=
"38"
/></proof>
<proof
prover=
"26"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"Grandfather_male"
expanded=
"true"
>
<goal
name=
"Grandfather_male"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"timeout"
time=
"5.19"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.01"
/></proof>
...
...
@@ -153,7 +140,6 @@
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"13"
><result
status=
"timeout"
time=
"5.77"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.01"
steps=
"6"
/></proof>
...
...
@@ -166,9 +152,8 @@
<proof
prover=
"25"
><result
status=
"valid"
time=
"0.00"
steps=
"5"
/></proof>
<proof
prover=
"26"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"Grandmother_female"
expanded=
"true"
>
<goal
name=
"Grandmother_female"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"timeout"
time=
"5.17"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
@@ -179,7 +164,6 @@
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"12"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"13"
><result
status=
"timeout"
time=
"5.27"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.01"
steps=
"5"
/></proof>
...
...
@@ -192,9 +176,8 @@
<proof
prover=
"25"
><result
status=
"valid"
time=
"0.00"
steps=
"5"
/></proof>
<proof
prover=
"26"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"Only_two_grandfathers"
expanded=
"true"
>
<goal
name=
"Only_two_grandfathers"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"timeout"
time=
"5.07"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.01"
/></proof>
...
...
@@ -205,7 +188,6 @@
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"13"
><result
status=
"timeout"
time=
"5.99"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.05"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.01"
steps=
"10"
/></proof>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment