The posted input files are now all mechanically generated from a master list of theorems.
The times shown in the following table are not the times required to find the proof, but rather
the maximum time allocated to Otter to find the proof. The time is shown only when it had to be longer than
the default, which was often 20 seconds when hints were used and 120 seconds when hints were not used.
For more information about our methodology see the top page of this project.
| Input File |
Proof |
Length |
Strategy |
Seconds |
Commentary |
| Satz5.1 | Satz5.1.prf | 127 | hints | | Connectivity of betweenness
(Gupta 1965, one of Quaife's challenge problems)
$a \neq b \land T(a,b,c) \land T(a,b,d) \rightarrow T(a,c,d) \lor T(a,d,c)$
Wos has subsequently found a 96-step proof. | | Satz5.2 | Satz5.2.prf | 3 | | | $a \neq b \land T(a,b,c) \land T(a,b,d) \rightarrow T(b,c,d) \lor T(b,d,c) $ | | Satz5.3 | Satz5.3.prf | 15 | | | $ T(a,b,d) \land T(a,c,d) \rightarrow T(a,b,c) \lor T(a,c,b) $ | | Satz5.5a | Satz5.5a.prf | 17 | | | left to right of Satz 5.5 | | Satz5.5b | Satz5.5b.prf | 8 | | | right to left of Satz 5.5 | | Satz5.6 | Satz5.6.prf | 7 | | | $\le$ respects congruence | | Satz5.7 | Satz5.7.prf | 1 | | | reflexivity of $ \le $ | | Satz5.8 | Satz5.8.prf | 8 | | | transitivity of $ \le $ | | Satz5.9 | Satz5.9.prf | 20 | diagram | | $ ab \le cd \land cd \le ef \rightarrow ab \le cd $ | | Satz5.10 | Satz5.10.prf | 5 | | | $ ab \le cd \lor cd \le ab $ | | Satz5.11 | Satz5.11.prf | 1 | | | $ aa \le cd $ | | Satz5.12a1 | Satz5.12a1.prf | 1 | | | $Col(a,b,c) \land T(a,b,c) \rightarrow ab \le ac \land bc \le ac $ | | Satz5.12a2 | Satz5.12a2.prf | 2 | | | $ Col(a,b,c) \land T(a,b,c)\rightarrow bc \le ac $ | | NarbouxLemma1 | NarbouxLemma1.prf | 4 | | | $ T(a,b,c) \land E(a,c,a,b)\rightarrow c=b $
We used this to prove 5.12b (and almost certainly nowhere else). Narboux needed this in his formalization too. | | Satz5.12b | Satz5.12b.prf | 20 | subformula | 227 | $ Col(a,b,c) \land ab \le ac \land bc \le ac \rightarrow T(a,b,c) $ |
Back to top of archive
|
