Certification of Nontermination Proofs
using Strategies and Nonlooping Derivations
 
Content
general formalization examples partial proofs TPDB

General

This site provides supporting material for the paper Certification of Nontermination Proofs using Strategies and Nonlooping Derivations by Julian Nagele, René Thiemann, and Sarah Winkler.

In the paper we present an Isabelle/HOL formalization of an extended repertoire of nontermination techniques. First, we formalized techniques for nonlooping TRSs. Second, the available strategies include (an extended version of) forbidden patterns, which does in particular cover outermost and context-sensitive rewriting. Finally, a mechanism to support partial nontermination proofs allows to further extend the applicability of the proof checker CeTA.

Formalization

All relevant theories are available within the IsaFoR directory of the sources of IsaFoR/CeTA v2.14.1. A compilation of the Isabelle sources requires Isabelle 2013-2 and the corresponding archive of formal proofs (version afp-2014-02-19 or later). There are also binaries for CeTA available.

To inspect the theories like Forbidden_Patterns.thy, one has to add the following line into ~/.isabelle/Isabelle2013-2/etc/settings: 

init_component "/the/path/to/afp-2014-02-19"
Afterwards one can navigate into the IsaFoR directory and invoke 
/the/path/to/Isabelle2013-2/bin/isabelle jedit -d . -l QTRS Forbidden_Patterns.thy
For further compilation instructions, we refer to the README-file within the IsaFoR-sources.


Experiments

Examples
Here are some examples from the paper, plus their certified nontermination proofs. All of the following proofs are provided in the certification problem format (CPF). For all examples we provide automatically generated proofs, but in cases where these proofs are overly complex we additionally provide small hand written proofs which correspond more to the proofs which are described in the paper.
TRS hand written proof automatic proof description
map – NO The TRS for map, i.e., Example 1 with the strategy as described in Example 3.
run_again1 NO NO The TRS R of Example 13, where R' contains rules for the Ackermann function.
run_again2 NO NO The TRS R of Example 13, where R' contains rules to compute square roots. Proving nontermination of R' is as hard as showing that sqrt(2) is irrational.
rewrite1 NO NO The TRS R of Example 16, with R' for Ackermann as in run_again1.
rewrite2 NO NO The TRS R of Example 16, with R' for square roots as in run_again2.
nonloop – NO The TRS R of Example 17 for innermost rewriting.

Partial Proofs
The following 12 proofs by AProVE are partially certifiable by CeTA, i.e., they use proof techniques which are not covered by CeTA (such as reasoning modulo AC), but CeTA can certify all proof steps applying supported techniques. Note that for these proofs one has to invoke CeTA with the --allow-assumptions option.
AProVE
AProVE_10-isList NO
Applicative_05-TypeEx5 NO
Mixed_AC-RENAMED-BOOL_nosorts-noand NO
Mixed_AC-RENAMED-BOOL_nosorts NO
Secret_05_TRS-ttt2 NO
Strategy_outermost_added_08-Ex6_GM04_FR NO
Strategy_outermost_added_08-Ex6_GM04_Z NO
Transformed_CSR_04-LengthOfFiniteLists_nosorts_C NO
Transformed_CSR_04-LengthOfFiniteLists_nosorts_noand_C NO
Transformed_CSR_04-OvConsOS_nosorts_C NO
Transformed_CSR_04-OvConsOS_nosorts_noand_C NO
Zantema_08-ffb_SL NO

Nonterminating TRSs in TPDB
For the following experiments we ran two configurations of AProVE as well as TTT2 on all 596 first-order TRSs in TPDB 8.0.7 where at least one of the termination tools could find a nontermination proof in the full run of termination tools in December 2013. AProVE '13 and TTT2 '13 are the versions of AProVE and TTT2 which participated in the certified category of the termination competition in 2013, AProVE '14 and TTT2 '14 are the current versions. The proofs of AProVE '13 and TTT2 '13 have been extracted from the full run, the proofs of AProVE '14 and TTT2 '14 have been generated on a standard PC with the same timeout of 60 seconds as in the full run.

AProVE '13 AProVE '14 TTT2 '13 TTT2 '14
AProVE_06-nonterm MAYBE NO NO NO
AProVE_07-thiemann28 MAYBE NO MAYBE MAYBE
AProVE_08-round_nonterm NO NO NO NO
AProVE_10-andIsNat MAYBE NO MAYBE MAYBE
AProVE_10-double MAYBE NO MAYBE MAYBE
AProVE_10-ex1 NO NO MAYBE MAYBE
AProVE_10-ex2 MAYBE NO MAYBE MAYBE
AProVE_10-ex3 MAYBE NO MAYBE MAYBE
AProVE_10-ex4 MAYBE NO MAYBE MAYBE
AProVE_10-halfdouble MAYBE NO MAYBE MAYBE
AProVE_10-isList NO NO NO NO
AProVE_10-isNat NO NO MAYBE MAYBE
AotoYamada_05-001 NO NO NO NO
AotoYamada_05-003 NO NO NO NO
Applicative_05-Ex2_8_1ConstSubstFix NO NO NO NO
Applicative_05-Hamming NO NO NO NO
Applicative_05-TypeEx3 NO NO NO NO
Applicative_05-TypeEx5 NO NO NO NO
Applicative_05-nonTermF NO NO NO NO
Applicative_05-termMonTypes NO NO NO NO
Bouchare_06-08 NO NO NO NO
Bouchare_06-09 NO NO NO NO
CiME_04-append-wrong NO NO NO NO
EEG_IJCAR_12-emmes-nonloop-ex1_1 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex1_4 NO NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex1_5 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex2_2 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex2_4 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex2_5 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex3_1 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex3_2 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex3_3 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex4_1 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex4_2 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex4_3 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex4_4 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex5_1 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex5_2 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex5_3 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex6_1 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex6_2 NO NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex7_1 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex7_2 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex7_4 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex7_7 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-emmes-nonloop-ex7_9 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-add MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-addTrue MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-isDNat MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-isList NO NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-isTrueList NO NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-swapX NO NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-swapXY NO NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-swapXY2 NO NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-swap_decr MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-toOne MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-unbounded MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-enger-nonloop-while-lt NO NO MAYBE MAYBE
EEG_IJCAR_12-rybalchenko-nonloop-popl08 MAYBE NO MAYBE MAYBE
EEG_IJCAR_12-velroyen-nonloop-ConvLower_c MAYBE NO MAYBE MAYBE
Gebhardt_06-03 MAYBE NO MAYBE MAYBE
Gebhardt_06-05 MAYBE NO MAYBE MAYBE
Gebhardt_06-08 MAYBE NO MAYBE MAYBE
Gebhardt_06-12 MAYBE NO MAYBE MAYBE
Gebhardt_06-15 MAYBE NO MAYBE MAYBE
HirokawaMiddeldorp_04-n002 NO NO NO NO
HirokawaMiddeldorp_04-n003 NO NO NO NO
HirokawaMiddeldorp_04-n004 NO NO NO NO
HirokawaMiddeldorp_04-n005 NO NO NO NO
HirokawaMiddeldorp_04-n006 NO NO NO NO
HirokawaMiddeldorp_04-n007 NO NO NO NO
HirokawaMiddeldorp_04-n008 NO NO NO NO
Maude_06-LengthOfFiniteLists_nosorts-noand MAYBE NO MAYBE NO
Maude_06-LengthOfFiniteLists_nosorts MAYBE NO MAYBE NO
Maude_06-OvConsOS_nosorts-noand MAYBE NO MAYBE NO
Maude_06-OvConsOS_nosorts MAYBE NO MAYBE NO
Mixed_AC-RENAMED-BOOL_nosorts-noand MAYBE NO MAYBE MAYBE
Mixed_AC-RENAMED-BOOL_nosorts MAYBE NO MAYBE MAYBE
Mixed_SRS-01-oppelt08 MAYBE NO MAYBE MAYBE
Mixed_SRS-02-oppelt08 MAYBE MAYBE MAYBE MAYBE
Mixed_SRS-03-oppelt08 MAYBE NO MAYBE MAYBE
Mixed_SRS-04-oppelt08 MAYBE NO MAYBE MAYBE
Mixed_SRS-05-oppelt08 MAYBE NO MAYBE MAYBE
Mixed_SRS-06-oppelt08 NO NO MAYBE MAYBE
Mixed_SRS-07-oppelt08 MAYBE NO MAYBE MAYBE
Mixed_SRS-08-oppelt08 MAYBE NO MAYBE MAYBE
Mixed_SRS-1 NO NO MAYBE MAYBE
Mixed_SRS-turing_copy NO NO NO NO
Mixed_SRS-turing_mult NO NO NO NO
Mixed_innermost-muladd NO NO MAYBE NO
Mixed_innermost-n001 NO NO MAYBE NO
Mixed_outermost-even MAYBE NO MAYBE NO
Mixed_relative_SRS-zr13 MAYBE NO NO NO
Mixed_relative_TRS-assoc NO NO MAYBE MAYBE
Mixed_relative_TRS-gcd_many NO NO NO NO
Relative_05-rt2-8 NO NO MAYBE MAYBE
Relative_05-rt3-3 NO NO MAYBE MAYBE
Relative_05-rt3-6 NO NO NO NO
Relative_05-rt3-8 NO NO NO NO
Relative_05-rtL-evnz NO NO MAYBE NO
Relative_05-rtL-evo NO NO NO NO
SK90-2.05 NO NO NO NO
SK90-4.06 NO NO NO NO
SK90-4.34 NO NO NO NO
SK90-4.40 NO NO NO NO
SK90-4.49 NO NO NO NO
SK90-4.54 NO NO NO NO
Secret_05_TRS-cime4 NO NO MAYBE NO
Secret_05_TRS-ttt1 NO NO NO NO
Secret_05_TRS-ttt2 NO NO NO NO
Secret_06_SRS-1-matchbox MAYBE MAYBE MAYBE MAYBE
Secret_07_SRS-num-514 MAYBE MAYBE MAYBE MAYBE
Secret_07_SRS-num-515 NO NO MAYBE MAYBE
Secret_07_SRS-num-519 NO NO MAYBE MAYBE
Secret_07_SRS-num-521 NO MAYBE MAYBE MAYBE
Secret_07_SRS-num-525 NO NO MAYBE MAYBE
Secret_07_SRS-num-527 NO MAYBE MAYBE MAYBE
Secret_07_SRS-num-530 NO NO MAYBE MAYBE
Secret_07_SRS-num-539 NO NO MAYBE MAYBE
Strategy_outermost_added_08-#4.12a MAYBE NO MAYBE NO
Strategy_outermost_added_08-#4.14 MAYBE NO MAYBE NO
Strategy_outermost_added_08-#4.15 MAYBE NO MAYBE NO
Strategy_outermost_added_08-#4.16 MAYBE NO MAYBE NO
Strategy_outermost_added_08-#4.17 MAYBE NO MAYBE NO
Strategy_outermost_added_08-#4.18 MAYBE NO MAYBE NO
Strategy_outermost_added_08-#4.2 MAYBE NO MAYBE NO
Strategy_outermost_added_08-#4.3 MAYBE NO MAYBE NO
Strategy_outermost_added_08-#4.4 MAYBE NO MAYBE NO
Strategy_outermost_added_08-#4.7 MAYBE NO MAYBE NO
Strategy_outermost_added_08-001 MAYBE NO MAYBE NO
Strategy_outermost_added_08-003 MAYBE NO MAYBE NO
Strategy_outermost_added_08-2.05 MAYBE NO MAYBE NO
Strategy_outermost_added_08-4.06 MAYBE NO MAYBE NO
Strategy_outermost_added_08-4.34 MAYBE NO MAYBE NO
Strategy_outermost_added_08-4.40 MAYBE MAYBE MAYBE NO
Strategy_outermost_added_08-4.49 MAYBE NO MAYBE NO
Strategy_outermost_added_08-4.54 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex14_AEGL02 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex14_AEGL02_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex14_AEGL02_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex14_Luc06_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex14_Luc06_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex14_Luc06_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex15_Luc06_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex15_Luc98 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex15_Luc98_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex16_Luc06_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_2_AEL03 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_2_AEL03_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_2_Luc02c MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_2_Luc02c_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_GL02a MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_GL02a_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_GM03 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_GM03_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_GM03_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_GM99 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_GM99_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_GM99_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_GM99_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_Luc02b MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_Luc02b_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_Luc04b_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_Luc04b_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_Zan97 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_Zan97_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_Zan97_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex1_Zan97_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex24_GM04_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex24_Luc06_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex24_Luc06_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex24_Luc06_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex26_Luc03b MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex2_8_1ConstSubstFix MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex2_Luc03b MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex3_12_Luc96a MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex3_12_Luc96a_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex3_2_Luc97 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex3_2_Luc97_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex3_3_25_Bor03 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex3_3_25_Bor03_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex49_GM04_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_4_Luc96b MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_7_15_Bor03 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_7_37_Bor03 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_7_37_Bor03_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_7_56_Bor03 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_7_56_Bor03_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_7_77_Bor03 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_7_77_Bor03_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_DLMMU04_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_DLMMU04_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_DLMMU04_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_Zan97 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex4_Zan97_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex5_7_Luc97 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex5_7_Luc97_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex5_DLMMU04_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex5_Zan97_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex6_15_AEL02 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex6_15_AEL02_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex6_15_AEL02_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex6_9_Luc02c MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex6_9_Luc02c_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex6_GM04_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex6_GM04_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex6_Luc98 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex7_BLR02 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex7_BLR02_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex8_BLR02 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex8_BLR02_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex9_BLR02 MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex9_Luc04_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex9_Luc04_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex9_Luc04_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex9_Luc06_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex9_Luc06_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-Ex9_Luc06_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExAppendixB_AEL03 MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExAppendixB_AEL03_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExConc_Zan97 MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExConc_Zan97_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExIntrod_GM01 MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExIntrod_GM01_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExIntrod_GM04 MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExIntrod_GM04_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExIntrod_GM99 MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExIntrod_GM99_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExIntrod_Zan97 MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExIntrod_Zan97_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExIntrod_Zan97_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExSec11_1_Luc02a MAYBE NO MAYBE NO
Strategy_outermost_added_08-ExSec4_2_DLMMU04_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LISTUTILITIES_complete-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LISTUTILITIES_complete_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LISTUTILITIES_nokinds-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LISTUTILITIES_nokinds_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LISTUTILITIES_nosorts-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LISTUTILITIES_nosorts_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LengthOfFiniteLists_complete-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LengthOfFiniteLists_complete_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LengthOfFiniteLists_nokinds-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LengthOfFiniteLists_nokinds_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LengthOfFiniteLists_nosorts-noand_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-LengthOfFiniteLists_nosorts-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LengthOfFiniteLists_nosorts-noand_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-LengthOfFiniteLists_nosorts_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-LengthOfFiniteLists_nosorts_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-LengthOfFiniteLists_nosorts_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-MYNAT_complete-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-MYNAT_complete_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-MYNAT_nokinds-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-MYNAT_nokinds_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-MYNAT_nosorts-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-MYNAT_nosorts_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-OvConsOS_complete-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-OvConsOS_complete_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-OvConsOS_nokinds-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-OvConsOS_nokinds_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-OvConsOS_nosorts-noand_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-OvConsOS_nosorts-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-OvConsOS_nosorts-noand_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-OvConsOS_nosorts_FR MAYBE NO MAYBE NO
Strategy_outermost_added_08-OvConsOS_nosorts_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-OvConsOS_nosorts_Z MAYBE NO MAYBE NO
Strategy_outermost_added_08-PALINDROME_complete-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-PALINDROME_complete_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-PALINDROME_nokinds-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-PALINDROME_nokinds_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-PALINDROME_nosorts_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-PEANO_complete-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-PEANO_complete_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-PEANO_nokinds-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-PEANO_nokinds_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-PEANO_nosorts-noand_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-PEANO_nosorts_L MAYBE NO MAYBE NO
Strategy_outermost_added_08-TypeEx5 MAYBE NO MAYBE NO
Strategy_outermost_added_08-cime4 MAYBE NO MAYBE NO
Strategy_outermost_added_08-gkg MAYBE NO MAYBE NO
Strategy_outermost_added_08-jwno1 MAYBE NO MAYBE NO
Strategy_outermost_added_08-jwno4 MAYBE NO MAYBE NO
Strategy_outermost_added_08-jwno6 MAYBE NO MAYBE NO
Strategy_outermost_added_08-muladd MAYBE NO MAYBE NO
Strategy_outermost_added_08-n001 MAYBE NO MAYBE NO
Strategy_outermost_added_08-n002 MAYBE NO MAYBE NO
Strategy_outermost_added_08-n003 MAYBE NO MAYBE NO
Strategy_outermost_added_08-n004 MAYBE NO MAYBE NO
Strategy_outermost_added_08-n005 MAYBE NO MAYBE NO
Strategy_outermost_added_08-n006 MAYBE NO MAYBE NO
Strategy_outermost_added_08-n007 MAYBE NO MAYBE NO
Strategy_outermost_added_08-n008 MAYBE NO MAYBE NO
Strategy_outermost_added_08-nonTermF MAYBE NO MAYBE NO
Strategy_outermost_added_08-round_nonterm MAYBE NO MAYBE NO
Strategy_outermost_added_08-termMonTypes MAYBE NO MAYBE NO
Strategy_outermost_added_08-test10 MAYBE NO MAYBE NO
Strategy_outermost_added_08-test75 MAYBE NO MAYBE NO
Strategy_outermost_added_08-test76 MAYBE NO MAYBE NO
Strategy_outermost_added_08-test9 MAYBE NO MAYBE NO
Strategy_outermost_added_08-toyama MAYBE NO MAYBE NO
Strategy_outermost_added_08-ttt1 MAYBE NO MAYBE NO
Strategy_outermost_added_08-ttt2 MAYBE NO MAYBE NO
Strategy_removed_AG01-#4.12a NO NO NO NO
Strategy_removed_AG01-#4.13 NO NO MAYBE MAYBE
Strategy_removed_AG01-#4.14 NO NO NO NO
Strategy_removed_AG01-#4.15 NO NO NO NO
Strategy_removed_AG01-#4.16 NO NO NO NO
Strategy_removed_AG01-#4.17 NO NO NO NO
Strategy_removed_AG01-#4.18 NO NO NO NO
Strategy_removed_AG01-#4.2 NO NO NO NO
Strategy_removed_AG01-#4.3 NO NO MAYBE MAYBE
Strategy_removed_AG01-#4.4 NO NO NO NO
Strategy_removed_AG01-#4.7 NO NO NO NO
Strategy_removed_CSR_05-Ex14_AEGL02 NO NO NO NO
Strategy_removed_CSR_05-Ex15_Luc98 NO NO NO NO
Strategy_removed_CSR_05-Ex1_2_AEL03 NO NO NO NO
Strategy_removed_CSR_05-Ex1_2_Luc02c NO NO NO NO
Strategy_removed_CSR_05-Ex1_GL02a NO NO NO NO
Strategy_removed_CSR_05-Ex1_GM03 NO NO NO NO
Strategy_removed_CSR_05-Ex1_GM99 NO NO NO NO
Strategy_removed_CSR_05-Ex1_Luc02b NO NO NO NO
Strategy_removed_CSR_05-Ex1_Zan97 NO NO NO NO
Strategy_removed_CSR_05-Ex24_GM04 NO NO MAYBE MAYBE
Strategy_removed_CSR_05-Ex26_Luc03b NO NO NO NO
Strategy_removed_CSR_05-Ex2_Luc03b NO NO NO NO
Strategy_removed_CSR_05-Ex3_12_Luc96a NO NO NO NO
Strategy_removed_CSR_05-Ex3_2_Luc97 NO NO NO NO
Strategy_removed_CSR_05-Ex3_3_25_Bor03 NO NO NO NO
Strategy_removed_CSR_05-Ex4_4_Luc96b NO NO NO NO
Strategy_removed_CSR_05-Ex4_7_15_Bor03 NO NO NO NO
Strategy_removed_CSR_05-Ex4_7_37_Bor03 NO NO NO NO
Strategy_removed_CSR_05-Ex4_7_56_Bor03 NO NO NO NO
Strategy_removed_CSR_05-Ex4_7_77_Bor03 NO NO NO NO
Strategy_removed_CSR_05-Ex4_Zan97 NO NO NO NO
Strategy_removed_CSR_05-Ex5_7_Luc97 NO NO NO NO
Strategy_removed_CSR_05-Ex5_Zan97 NO NO NO NO
Strategy_removed_CSR_05-Ex6_15_AEL02 NO NO NO NO
Strategy_removed_CSR_05-Ex6_9_Luc02c NO NO NO NO
Strategy_removed_CSR_05-Ex6_GM04 NO NO NO NO
Strategy_removed_CSR_05-Ex6_Luc98 NO NO NO NO
Strategy_removed_CSR_05-Ex7_BLR02 NO NO NO NO
Strategy_removed_CSR_05-Ex8_BLR02 NO NO NO NO
Strategy_removed_CSR_05-Ex9_BLR02 NO NO NO NO
Strategy_removed_CSR_05-ExAppendixB_AEL03 NO NO NO NO
Strategy_removed_CSR_05-ExConc_Zan97 NO NO NO NO
Strategy_removed_CSR_05-ExIntrod_GM01 NO NO NO NO
Strategy_removed_CSR_05-ExIntrod_GM04 NO NO NO NO
Strategy_removed_CSR_05-ExIntrod_GM99 NO NO NO NO
Strategy_removed_CSR_05-ExIntrod_Zan97 NO NO NO NO
Strategy_removed_mixed_05-ExSec11_1_Luc02a NO NO NO NO
Strategy_removed_mixed_05-ex1 NO NO NO NO
Strategy_removed_mixed_05-ex2 NO NO NO NO
Strategy_removed_mixed_05-ex3 NO NO NO NO
Strategy_removed_mixed_05-ex4 NO NO NO NO
Strategy_removed_mixed_05-ex5 NO NO NO NO
Strategy_removed_mixed_05-ex6 NO NO NO NO
Strategy_removed_mixed_05-gkg NO NO NO NO
Strategy_removed_mixed_05-muladd NO NO NO NO
Strategy_removed_mixed_05-n001 NO NO NO NO
Strategy_removed_mixed_05-test10 NO NO NO NO
Strategy_removed_mixed_05-test75 NO NO NO NO
Strategy_removed_mixed_05-test76 NO NO MAYBE MAYBE
Strategy_removed_mixed_05-test77 NO NO MAYBE MAYBE
Strategy_removed_mixed_05-test9 NO NO NO NO
Strategy_removed_mixed_05-toyama NO NO MAYBE NO
Trafo_06-un04 MAYBE NO MAYBE MAYBE
Transformed_CSR_04-Ex14_AEGL02_FR NO NO MAYBE MAYBE
Transformed_CSR_04-Ex14_AEGL02_L NO NO NO NO
Transformed_CSR_04-Ex14_AEGL02_Z NO NO NO NO
Transformed_CSR_04-Ex14_Luc06_FR NO NO NO NO
Transformed_CSR_04-Ex14_Luc06_GM NO MAYBE MAYBE MAYBE
Transformed_CSR_04-Ex14_Luc06_L NO NO NO NO
Transformed_CSR_04-Ex15_Luc06_L NO NO NO NO
Transformed_CSR_04-Ex15_Luc98_L NO NO NO NO
Transformed_CSR_04-Ex16_Luc06_L NO NO NO NO
Transformed_CSR_04-Ex1_2_AEL03_L NO NO NO NO
Transformed_CSR_04-Ex1_2_Luc02c_L NO NO NO NO
Transformed_CSR_04-Ex1_GL02a_L NO NO NO NO
Transformed_CSR_04-Ex1_GL02a_Z MAYBE NO MAYBE MAYBE
Transformed_CSR_04-Ex1_GM03_L NO NO NO NO
Transformed_CSR_04-Ex1_GM03_Z NO NO NO NO
Transformed_CSR_04-Ex1_GM99_FR NO NO NO NO
Transformed_CSR_04-Ex1_GM99_GM NO NO MAYBE MAYBE
Transformed_CSR_04-Ex1_GM99_L NO NO NO NO
Transformed_CSR_04-Ex1_GM99_iGM NO NO MAYBE MAYBE
Transformed_CSR_04-Ex1_Luc02b_L NO NO NO NO
Transformed_CSR_04-Ex1_Luc04b_FR NO NO NO NO
Transformed_CSR_04-Ex1_Luc04b_L NO NO NO NO
Transformed_CSR_04-Ex1_Luc04b_Z NO NO NO NO
Transformed_CSR_04-Ex1_Zan97_FR NO NO NO NO
Transformed_CSR_04-Ex1_Zan97_L NO NO NO NO
Transformed_CSR_04-Ex24_GM04_GM NO NO MAYBE MAYBE
Transformed_CSR_04-Ex24_GM04_L NO NO NO NO
Transformed_CSR_04-Ex24_GM04_Z NO NO NO NO
Transformed_CSR_04-Ex24_Luc06_FR NO NO NO NO
Transformed_CSR_04-Ex24_Luc06_GM NO NO NO NO
Transformed_CSR_04-Ex24_Luc06_L NO NO NO NO
Transformed_CSR_04-Ex24_Luc06_iGM NO NO MAYBE NO
Transformed_CSR_04-Ex3_12_Luc96a_L NO NO NO NO
Transformed_CSR_04-Ex3_2_Luc97_L NO NO NO NO
Transformed_CSR_04-Ex3_3_25_Bor03_FR MAYBE NO MAYBE MAYBE
Transformed_CSR_04-Ex3_3_25_Bor03_Z NO NO NO NO
Transformed_CSR_04-Ex49_GM04_L NO NO NO NO
Transformed_CSR_04-Ex4_4_Luc96b_FR NO NO NO NO
Transformed_CSR_04-Ex4_4_Luc96b_Z NO NO NO NO
Transformed_CSR_04-Ex4_7_37_Bor03_L NO NO NO NO
Transformed_CSR_04-Ex4_7_56_Bor03_L NO NO NO NO
Transformed_CSR_04-Ex4_7_77_Bor03_L NO NO NO NO
Transformed_CSR_04-Ex4_DLMMU04_FR NO NO NO NO
Transformed_CSR_04-Ex4_DLMMU04_L NO NO NO NO
Transformed_CSR_04-Ex4_DLMMU04_Z NO NO NO NO
Transformed_CSR_04-Ex4_Zan97_L NO NO NO NO
Transformed_CSR_04-Ex5_7_Luc97_L NO NO NO NO
Transformed_CSR_04-Ex5_DLMMU04_FR NO NO MAYBE NO
Transformed_CSR_04-Ex5_DLMMU04_L NO NO NO NO
Transformed_CSR_04-Ex5_DLMMU04_Z NO NO NO NO
Transformed_CSR_04-Ex5_Zan97_L NO NO NO NO
Transformed_CSR_04-Ex6_15_AEL02_FR NO MAYBE MAYBE MAYBE
Transformed_CSR_04-Ex6_15_AEL02_L NO NO NO NO
Transformed_CSR_04-Ex6_15_AEL02_Z NO NO MAYBE MAYBE
Transformed_CSR_04-Ex6_9_Luc02c_L NO NO NO NO
Transformed_CSR_04-Ex6_GM04_FR NO NO NO NO
Transformed_CSR_04-Ex7_BLR02_L NO NO NO NO
Transformed_CSR_04-Ex8_BLR02_L NO NO NO NO
Transformed_CSR_04-Ex9_Luc04_FR NO NO NO NO
Transformed_CSR_04-Ex9_Luc04_GM NO NO MAYBE MAYBE
Transformed_CSR_04-Ex9_Luc04_L NO NO NO NO
Transformed_CSR_04-Ex9_Luc06_FR NO NO NO NO
Transformed_CSR_04-ExAppendixB_AEL03_L NO NO NO NO
Transformed_CSR_04-ExConc_Zan97_Z NO NO NO NO
Transformed_CSR_04-ExIntrod_GM01_FR NO NO NO NO
Transformed_CSR_04-ExIntrod_GM01_L NO NO NO NO
Transformed_CSR_04-ExIntrod_GM01_Z NO NO NO NO
Transformed_CSR_04-ExIntrod_GM04_FR NO NO MAYBE MAYBE
Transformed_CSR_04-ExIntrod_GM04_L NO NO NO NO
Transformed_CSR_04-ExIntrod_GM04_Z NO NO NO NO
Transformed_CSR_04-ExIntrod_GM99_L NO NO NO NO
Transformed_CSR_04-ExIntrod_GM99_Z NO NO NO NO
Transformed_CSR_04-ExIntrod_Zan97_L NO NO NO NO
Transformed_CSR_04-ExIntrod_Zan97_Z NO NO NO NO
Transformed_CSR_04-ExSec4_2_DLMMU04_L NO NO NO NO
Transformed_CSR_04-LISTUTILITIES_complete-noand_L NO NO NO NO
Transformed_CSR_04-LISTUTILITIES_complete_L NO NO NO NO
Transformed_CSR_04-LISTUTILITIES_nokinds-noand_L NO NO NO NO
Transformed_CSR_04-LISTUTILITIES_nokinds_L NO NO NO NO
Transformed_CSR_04-LISTUTILITIES_nosorts-noand_L NO NO NO NO
Transformed_CSR_04-LISTUTILITIES_nosorts_L NO NO NO NO
Transformed_CSR_04-LengthOfFiniteLists_complete-noand_L NO NO NO NO
Transformed_CSR_04-LengthOfFiniteLists_complete_L NO NO NO NO
Transformed_CSR_04-LengthOfFiniteLists_nokinds-noand_FR NO NO MAYBE MAYBE
Transformed_CSR_04-LengthOfFiniteLists_nokinds-noand_L NO NO NO NO
Transformed_CSR_04-LengthOfFiniteLists_nokinds-noand_Z NO NO MAYBE MAYBE
Transformed_CSR_04-LengthOfFiniteLists_nokinds_FR MAYBE NO MAYBE MAYBE
Transformed_CSR_04-LengthOfFiniteLists_nokinds_L NO NO NO NO
Transformed_CSR_04-LengthOfFiniteLists_nokinds_Z NO NO MAYBE MAYBE
Transformed_CSR_04-LengthOfFiniteLists_nosorts-noand_FR NO NO NO NO
Transformed_CSR_04-LengthOfFiniteLists_nosorts-noand_L NO NO NO NO
Transformed_CSR_04-LengthOfFiniteLists_nosorts_C MAYBE NO MAYBE MAYBE
Transformed_CSR_04-LengthOfFiniteLists_nosorts_FR NO NO NO NO
Transformed_CSR_04-LengthOfFiniteLists_nosorts_GM NO NO NO NO
Transformed_CSR_04-LengthOfFiniteLists_nosorts_L NO NO NO NO
Transformed_CSR_04-LengthOfFiniteLists_nosorts_iGM NO NO MAYBE MAYBE
Transformed_CSR_04-LengthOfFiniteLists_nosorts_noand_C MAYBE NO MAYBE MAYBE
Transformed_CSR_04-LengthOfFiniteLists_nosorts_noand_GM NO NO NO NO
Transformed_CSR_04-MYNAT_complete-noand_L NO NO NO NO
Transformed_CSR_04-MYNAT_complete_L NO NO NO NO
Transformed_CSR_04-MYNAT_nokinds-noand_L NO NO NO NO
Transformed_CSR_04-MYNAT_nokinds_L NO NO NO NO
Transformed_CSR_04-MYNAT_nosorts-noand_L NO NO NO NO
Transformed_CSR_04-MYNAT_nosorts_L NO NO NO NO
Transformed_CSR_04-OvConsOS_complete-noand_L NO NO NO NO
Transformed_CSR_04-OvConsOS_complete-noand_Z MAYBE NO MAYBE MAYBE
Transformed_CSR_04-OvConsOS_complete_L NO NO NO NO
Transformed_CSR_04-OvConsOS_nokinds-noand_FR MAYBE NO MAYBE MAYBE
Transformed_CSR_04-OvConsOS_nokinds-noand_L NO NO NO NO
Transformed_CSR_04-OvConsOS_nokinds-noand_Z MAYBE NO MAYBE MAYBE
Transformed_CSR_04-OvConsOS_nokinds_L NO NO NO NO
Transformed_CSR_04-OvConsOS_nosorts-noand_FR NO NO MAYBE NO
Transformed_CSR_04-OvConsOS_nosorts-noand_L NO NO NO NO
Transformed_CSR_04-OvConsOS_nosorts-noand_Z NO NO MAYBE NO
Transformed_CSR_04-OvConsOS_nosorts_C MAYBE NO MAYBE MAYBE
Transformed_CSR_04-OvConsOS_nosorts_FR NO NO NO NO
Transformed_CSR_04-OvConsOS_nosorts_GM NO NO NO NO
Transformed_CSR_04-OvConsOS_nosorts_L NO NO NO NO
Transformed_CSR_04-OvConsOS_nosorts_Z NO NO NO NO
Transformed_CSR_04-OvConsOS_nosorts_iGM NO NO MAYBE MAYBE
Transformed_CSR_04-OvConsOS_nosorts_noand_C MAYBE NO MAYBE MAYBE
Transformed_CSR_04-OvConsOS_nosorts_noand_GM NO NO MAYBE NO
Transformed_CSR_04-PALINDROME_complete-noand_L NO NO NO NO
Transformed_CSR_04-PALINDROME_complete_L NO NO NO NO
Transformed_CSR_04-PALINDROME_nokinds-noand_L NO NO NO NO
Transformed_CSR_04-PALINDROME_nokinds_L NO NO NO NO
Transformed_CSR_04-PALINDROME_nosorts_L NO NO NO NO
Transformed_CSR_04-PEANO_complete-noand_L NO NO NO NO
Transformed_CSR_04-PEANO_complete_L NO NO NO NO
Transformed_CSR_04-PEANO_nokinds-noand_L NO NO NO NO
Transformed_CSR_04-PEANO_nokinds_L NO NO NO NO
Transformed_CSR_04-PEANO_nosorts-noand_L NO NO NO NO
Transformed_CSR_04-PEANO_nosorts_L NO NO NO NO
Transformed_CSR_innermost_04-LengthOfFiniteLists_nosorts_GM NO NO MAYBE NO
Transformed_CSR_innermost_04-LengthOfFiniteLists_nosorts_noand_GM NO NO MAYBE NO
Transformed_CSR_innermost_04-OvConsOS_nosorts_GM NO NO MAYBE NO
Transformed_CSR_innermost_04-OvConsOS_nosorts_noand_GM NO NO MAYBE NO
Waldmann_06_SRS-uni-2 NO NO NO NO
Waldmann_06_SRS-uni-3 MAYBE NO MAYBE MAYBE
Waldmann_06_SRS-uni-4 MAYBE NO MAYBE NO
Waldmann_06_SRS-uni-6 MAYBE NO MAYBE MAYBE
Waldmann_06-jwno1 NO NO NO NO
Waldmann_06-jwno4 NO NO NO NO
Waldmann_06-jwno6 NO NO NO NO
Waldmann_06-jwno9 NO NO NO NO
Waldmann_07_size11-size-11-alpha-3-num-1 MAYBE NO MAYBE MAYBE
Waldmann_07_size11-size-11-alpha-3-num-15 NO NO MAYBE MAYBE
Waldmann_07_size11-size-11-alpha-3-num-18 MAYBE NO MAYBE MAYBE
Waldmann_07_size11-size-11-alpha-3-num-21 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-2-num-10 NO MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-2-num-11 NO MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-2-num-20 MAYBE MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-100 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-101 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-11 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-127 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-129 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-135 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-140 NO NO NO MAYBE
Waldmann_07_size12-size-12-alpha-3-num-146 NO NO NO MAYBE
Waldmann_07_size12-size-12-alpha-3-num-158 NO NO NO MAYBE
Waldmann_07_size12-size-12-alpha-3-num-159 NO NO NO NO
Waldmann_07_size12-size-12-alpha-3-num-160 MAYBE NO NO MAYBE
Waldmann_07_size12-size-12-alpha-3-num-170 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-177 MAYBE NO NO MAYBE
Waldmann_07_size12-size-12-alpha-3-num-178 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-179 MAYBE NO NO MAYBE
Waldmann_07_size12-size-12-alpha-3-num-181 MAYBE NO NO MAYBE
Waldmann_07_size12-size-12-alpha-3-num-195 MAYBE NO NO MAYBE
Waldmann_07_size12-size-12-alpha-3-num-20 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-206 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-207 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-21 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-217 MAYBE NO NO MAYBE
Waldmann_07_size12-size-12-alpha-3-num-22 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-227 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-23 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-233 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-239 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-241 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-243 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-249 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-257 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-260 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-270 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-298 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-3 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-328 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-339 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-353 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-356 MAYBE MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-362 MAYBE MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-368 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-369 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-373 NO NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-378 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-401 MAYBE MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-402 MAYBE MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-406 NO MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-409 NO MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-450 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-47 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-474 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-475 NO MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-488 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-491 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-492 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-493 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-497 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-511 NO NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-522 NO NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-558 MAYBE MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-564 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-7 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-83 MAYBE MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-90 MAYBE NO MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-95 MAYBE MAYBE MAYBE MAYBE
Waldmann_07_size12-size-12-alpha-3-num-99 MAYBE NO NO MAYBE
Zantema_04-z042 NO NO NO NO
Zantema_04-z044 NO NO NO NO
Zantema_04-z046 NO NO NO NO
Zantema_04-z073 MAYBE NO MAYBE MAYBE
Zantema_04-z096 NO NO NO NO
Zantema_04-z127 NO NO NO NO
Zantema_04-z128 NO NO NO NO
Zantema_06-loop1 NO NO NO NO
Zantema_06-loop2 NO NO NO NO
Zantema_08-ffb_SL MAYBE NO MAYBE NO
Zantema_08-inn_out MAYBE NO MAYBE NO
Zantema_08-outermost_gr MAYBE NO MAYBE NO
Zantema_08-toyama_out MAYBE NO MAYBE NO
number of successful proofs 276 575 221 417