==== CoFix
cic:/Lyon/COINDUCTIVES/STREAMS/Examples/mapS2.con FAIL
cic:/Marseille/CCS/Trans_Sys/refl_strong_eq.con FAIL
cic:/Marseille/CCS/Trans_Sys/sym_strong_eq.con FAIL
cic:/Marseille/CCS/Trans_Sys/trans_strong_eq.con FAIL
cic:/Marseille/CCS/Trans_Sys/refl_weak_eq.con FAIL
cic:/Marseille/CCS/Trans_Sys/strong_weak.con FAIL
cic:/Marseille/CCS/Trans_Sys/sym_weak_eq.con FAIL
cic:/Marseille/CCS/Trans_Sys/weak_eq1_weak_eq.con FAIL

==== Non positive occurrence
cic:/Suresnes/MiniC/MiniC/State/n_type.ind FAIL
cic:/Suresnes/MiniC/MiniC/CAbstractSyntax/c_type.ind FAIL
cic:/Suresnes/MiniC/MiniC/BasicTypes/c_value.ind FAIL
cic:/Lyon/FIRING-SQUAD/bib/div2.ind FAIL
cic:/Lyon/GRAPHS-BASICS/Trees/Tree.ind FAIL
cic:/Lyon/GRAPHS-BASICS/Graphs/Graph.ind FAIL
cic:/Lyon/GRAPHS-BASICS/Digraphs/Digraph.ind FAIL
cic:/Lyon/GRAPHS-BASICS/Connected/Connected.ind FAIL
cic:/Lyon/GRAPHS-BASICS/Acyclic/Acyclic.ind FAIL
cic:/Rocq/TreeAutomata/pl_path/pl_path_recon.ind FAIL
cic:/Rocq/COMPILER/Mini_ML/compilation.ind FAIL
cic:/Rocq/COMPILER/Mini_ML/compilation_id.ind FAIL
cic:/Rocq/COC/Infer/expln.ind FAIL
cic:/Rocq/COC/Machine/transition.ind FAIL


==== Convertibilita
cic:/Rocq/TreeAutomata/defs/term_list_term_ind.con FAIL
cic:/Rocq/TreeAutomata/defs/term_list_term_rec.con FAIL
cic:/Rocq/TreeAutomata/defs/term_term_list_ind.con FAIL
cic:/Rocq/TreeAutomata/defs/term_term_list_rec.con FAIL
cic:/Rocq/TreeAutomata/semantics/mlrec_ind.con FAIL
cic:/Rocq/TreeAutomata/semantics/mreconnaissance_ind.con FAIL
cic:/Rocq/TreeAutomata/semantics/mstrec_ind.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Fairness.con FAIL
cic:/Rocq/TreeAutomata/non_coacc_kill/mlrec_co_ind.con FAIL
cic:/Rocq/TreeAutomata/non_coacc_kill/mreconnaissance_co_ind.con FAIL
cic:/Rocq/TreeAutomata/non_coacc_kill/mstrec_co_ind.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Equity.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/InTrace.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state1.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state2.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state3.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state5.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state4.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique3.con FAIL
cic:/Suresnes/BDD/canonicite/Boolean_functions/Assign_k_finite.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique2.con FAIL
cic:/Suresnes/BDD/canonicite/Vars/Var_k_finite.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique1.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique45.con FAIL
cic:/Rocq/HIGMAN/Higman/higman.con FAIL


=== Unknown constant
cic:/Sophia-Antipolis/Huffman/Permutation/permutation_map_ex.con FAIL

=== Caso non implementato
cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/ACK.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/ACKING.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/OUT.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/REPEAT.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/SEND.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/SENDING.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/ACK.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/ACKING.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/OUT.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/REPEAT.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/SEND.con FAIL
cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/SENDING.con FAIL
cic:/Rocq/MUTUAL-EXCLUSION/binary/version2/Correctness/correct.con FAIL
cic:/Rocq/MUTUAL-EXCLUSION/binary/version1/Correctness/correct.con FAIL

=== Wrong branch type (Nel primo caso: esportato male (argomenti permutati
    nel tipo di Disc!)
cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/IsClear.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/OneDel.con FAIL
cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Rtalks.con FAIL

=== check_is_really_smaller su un const o mutind?
cic:/Nijmegen/QArith/positive_fraction_encoding/encoding_algorithm.con FAIL
cic:/Nijmegen/QArith/positive_fraction_encoding/encoding_algorithm_ind.con FAIL