=== list-app-assoc-base.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  6 / 17  provers found a proof.
=== list-app-assoc-indinst.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Timeout
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Timeout
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  0 / 17  provers found a proof.
=== list-app-assoc-indstep1.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Timeout
[SUMMARY]  3 / 17  provers found a proof.
=== list-app-assoc-indstep2.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Timeout
[SUMMARY]  3 / 17  provers found a proof.
=== list-app-assoc-indstep3.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Theorem
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  6 / 17  provers found a proof.
=== list-app-assoc-indstep4.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Timeout
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Timeout
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  0 / 17  provers found a proof.
=== list-app-assoc-indstep5.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Timeout
[SUMMARY]  6 / 17  provers found a proof.
=== list-app-assoc-m1-step1.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  7 / 17  provers found a proof.
=== list-app-assoc-m1-step2.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Timeout
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Timeout
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  0 / 17  provers found a proof.
=== list-app-assoc-m1-step3.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  2 / 17  provers found a proof.
=== list-app-assoc-m1-step4.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Theorem
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  7 / 17  provers found a proof.
=== list-app-assoc-m1-step5.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  6 / 17  provers found a proof.
=== list-app-assoc.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  7 / 17  provers found a proof.
=== list-app-nil-base.p ===
agsyHOL---1.0 says Theorem
cocATP---0.2.0 says Theorem
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Theorem
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  10 / 17  provers found a proof.
=== list-app-nil-indinst.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Timeout
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Timeout
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  0 / 17  provers found a proof.
=== list-app-nil-indstep.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Theorem
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  7 / 17  provers found a proof.
=== list-app-nil.p ===
agsyHOL---1.0 says Theorem
cocATP---0.2.0 says Theorem
cvc5---1.0.5 says Timeout
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Timeout
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  3 / 17  provers found a proof.
=== list-rev-invol-lem-base-step1.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Theorem
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  7 / 17  provers found a proof.
=== list-rev-invol-lem-base-step2.p ===
agsyHOL---1.0 says Theorem
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Theorem
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  9 / 17  provers found a proof.
=== list-rev-invol-lem-base-step3.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  6 / 17  provers found a proof.
=== list-rev-invol-lem-indinst.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Theorem
cvc5---1.0.5 says Timeout
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Timeout
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  2 / 17  provers found a proof.
=== list-rev-invol-lem-indstep1.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Timeout
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  1 / 17  provers found a proof.
=== list-rev-invol-lem-indstep2.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  2 / 17  provers found a proof.
=== list-rev-invol-lem-indstep3.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Theorem
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  7 / 17  provers found a proof.
=== list-rev-invol-lem-indstep4.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Timeout
[SUMMARY]  4 / 17  provers found a proof.
=== list-rev-invol-lem-indstep5.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Theorem
[SUMMARY]  3 / 17  provers found a proof.
=== list-rev-invol-lem-indstep6.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  2 / 17  provers found a proof.
=== list-rev-invol-lem-indstep7.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  3 / 17  provers found a proof.
=== list-rev-invol-lem.p ===
agsyHOL---1.0 says Theorem
cocATP---0.2.0 says Theorem
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Timeout
[SUMMARY]  6 / 17  provers found a proof.
=== list-rev-invol-step1.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  6 / 17  provers found a proof.
=== list-rev-invol-step2.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Theorem
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  7 / 17  provers found a proof.
=== list-rev-invol-step3.p ===
agsyHOL---1.0 says Timeout
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Timeout
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Timeout
HOLyHammer---0.21 says Timeout
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Timeout
Leo-III---1.7.10 says Timeout
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Timeout
Zipperpin---2.1 says Timeout
[SUMMARY]  0 / 17  provers found a proof.
=== list-rev-invol-step4.p ===
agsyHOL---1.0 says Theorem
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Theorem
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Unknown
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  8 / 17  provers found a proof.
=== list-rev-invol-step5.p ===
agsyHOL---1.0 says Theorem
cocATP---0.2.0 says Timeout
cvc5---1.0.5 says Theorem
cvc5-SAT---1.0.5 says Unknown
E---3.0.03 says Theorem
HOLyHammer---0.21 says Theorem
Isabelle---2016 says Timeout
Isabelle-HOT---2016 says Timeout
Lash---1.13 says Unknown
LEO-II---1.7.0 says Theorem
Leo-III---1.7.10 says Theorem
Leo-III-SAT---1.7.10 says Timeout
Nitpick---2016 says Timeout
Satallax---3.5 says Theorem
TPS---3.120601S1b says Timeout
Vampire---4.8 says Theorem
Zipperpin---2.1 says Theorem
[SUMMARY]  9 / 17  provers found a proof.