TPTP/Veloci/GRP612-1.p.ma logic/equality.ma
TPTP/Veloci/COL024-1.p.ma logic/equality.ma
TPTP/Veloci/GRP139-1.p.ma logic/equality.ma
TPTP/Veloci/GRP612-1.p.ma logic/equality.ma
TPTP/Veloci/COL024-1.p.ma logic/equality.ma
TPTP/Veloci/GRP139-1.p.ma logic/equality.ma
TPTP/Veloci/GRP155-1.p.ma logic/equality.ma
TPTP/Veloci/BOO004-4.p.ma logic/equality.ma
TPTP/Veloci/LCL140-1.p.ma logic/equality.ma
TPTP/Veloci/GRP155-1.p.ma logic/equality.ma
TPTP/Veloci/BOO004-4.p.ma logic/equality.ma
TPTP/Veloci/LCL140-1.p.ma logic/equality.ma
TPTP/Veloci/GRP606-1.p.ma logic/equality.ma
coercions_dependent.ma decidable_kit/list_aux.ma list/list.ma nat/nat.ma
TPTP/Veloci/GRP606-1.p.ma logic/equality.ma
coercions_dependent.ma decidable_kit/list_aux.ma list/list.ma nat/nat.ma
TPTP/Veloci/GRP011-4.p.ma logic/equality.ma
TPTP/Veloci/GRP149-1.p.ma logic/equality.ma
TPTP/Veloci/COL013-1.p.ma logic/equality.ma
TPTP/Veloci/COL064-2.p.ma logic/equality.ma
TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
comments.ma coq.ma
TPTP/Veloci/GRP011-4.p.ma logic/equality.ma
TPTP/Veloci/GRP149-1.p.ma logic/equality.ma
TPTP/Veloci/COL013-1.p.ma logic/equality.ma
TPTP/Veloci/COL064-2.p.ma logic/equality.ma
TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
comments.ma coq.ma
TPTP/Veloci/BOO011-2.p.ma logic/equality.ma
TPTP/Veloci/LCL154-1.p.ma logic/equality.ma
TPTP/Veloci/LCL114-2.p.ma logic/equality.ma
TPTP/Veloci/BOO011-2.p.ma logic/equality.ma
TPTP/Veloci/LCL154-1.p.ma logic/equality.ma
TPTP/Veloci/LCL114-2.p.ma logic/equality.ma
TPTP/Veloci/GRP498-1.p.ma logic/equality.ma
TPTP/Veloci/GRP176-1.p.ma logic/equality.ma
overred.ma logic/equality.ma
TPTP/Veloci/COL007-1.p.ma logic/equality.ma
TPTP/Veloci/GRP498-1.p.ma logic/equality.ma
TPTP/Veloci/GRP176-1.p.ma logic/equality.ma
overred.ma logic/equality.ma
TPTP/Veloci/COL007-1.p.ma logic/equality.ma
TPTP/Veloci/GRP603-1.p.ma logic/equality.ma
TPTP/Veloci/COL058-2.p.ma logic/equality.ma
TPTP/Veloci/GRP515-1.p.ma logic/equality.ma
TPTP/Veloci/GRP603-1.p.ma logic/equality.ma
TPTP/Veloci/COL058-2.p.ma logic/equality.ma
TPTP/Veloci/GRP515-1.p.ma logic/equality.ma
TPTP/Veloci/GRP548-1.p.ma logic/equality.ma
TPTP/Veloci/GRP182-3.p.ma logic/equality.ma
TPTP/Veloci/COL048-1.p.ma logic/equality.ma
TPTP/Veloci/GRP548-1.p.ma logic/equality.ma
TPTP/Veloci/GRP182-3.p.ma logic/equality.ma
TPTP/Veloci/COL048-1.p.ma logic/equality.ma
TPTP/Veloci/GRP597-1.p.ma logic/equality.ma
TPTP/Veloci/GRP572-1.p.ma logic/equality.ma
TPTP/Veloci/GRP484-1.p.ma logic/equality.ma
TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
fix_che_non_passa_ma_dovrebbe.ma list/list.ma nat/nat.ma
TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
TPTP/Veloci/GRP597-1.p.ma logic/equality.ma
TPTP/Veloci/GRP572-1.p.ma logic/equality.ma
TPTP/Veloci/GRP484-1.p.ma logic/equality.ma
TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
fix_che_non_passa_ma_dovrebbe.ma list/list.ma nat/nat.ma
TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
TPTP/Veloci/COL062-3.p.ma logic/equality.ma
TPTP/Veloci/GRP492-1.p.ma logic/equality.ma
cut.ma coq.ma
TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
TPTP/Veloci/COL018-1.p.ma logic/equality.ma
TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
TPTP/Veloci/COL062-3.p.ma logic/equality.ma
TPTP/Veloci/GRP492-1.p.ma logic/equality.ma
cut.ma coq.ma
TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
TPTP/Veloci/COL018-1.p.ma logic/equality.ma
fguidi.ma logic/connectives.ma nat/nat.ma
TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
TPTP/Veloci/GRP517-1.p.ma logic/equality.ma
TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
TPTP/Veloci/COL083-1.p.ma logic/equality.ma
fguidi.ma logic/connectives.ma nat/nat.ma
TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
TPTP/Veloci/GRP517-1.p.ma logic/equality.ma
TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
TPTP/Veloci/COL083-1.p.ma logic/equality.ma
coercions_propagation.ma logic/connectives.ma nat/orders.ma
TPTP/Veloci/LAT045-1.p.ma logic/equality.ma
TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
coercions_propagation.ma logic/connectives.ma nat/orders.ma
TPTP/Veloci/LAT045-1.p.ma logic/equality.ma
TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
TPTP/Veloci/BOO005-4.p.ma logic/equality.ma
interactive/test7.ma
bad_induction.ma logic/equality.ma nat/nat.ma
TPTP/Veloci/RNG023-6.p.ma logic/equality.ma
TPTP/Veloci/BOO005-4.p.ma logic/equality.ma
interactive/test7.ma
bad_induction.ma logic/equality.ma nat/nat.ma
TPTP/Veloci/RNG023-6.p.ma logic/equality.ma
TPTP/Veloci/GRP608-1.p.ma logic/equality.ma
TPTP/Veloci/BOO010-2.p.ma logic/equality.ma
TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
TPTP/Veloci/GRP608-1.p.ma logic/equality.ma
TPTP/Veloci/BOO010-2.p.ma logic/equality.ma
TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
pullback.ma logic/equality.ma
TPTP/Veloci/COL086-1.p.ma logic/equality.ma
TPTP/Veloci/GRP151-1.p.ma logic/equality.ma
pullback.ma logic/equality.ma
TPTP/Veloci/COL086-1.p.ma logic/equality.ma
TPTP/Veloci/GRP151-1.p.ma logic/equality.ma
TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
TPTP/Veloci/GRP206-1.p.ma logic/equality.ma
decompose.ma logic/connectives.ma
TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
TPTP/Veloci/GRP206-1.p.ma logic/equality.ma
decompose.ma logic/connectives.ma
dependent_type_inference.ma nat/nat.ma
TPTP/Veloci/GRP456-1.p.ma logic/equality.ma
TPTP/Veloci/GRP159-1.p.ma logic/equality.ma
TPTP/Veloci/ROB030-1.p.ma logic/equality.ma
dependent_type_inference.ma nat/nat.ma
TPTP/Veloci/GRP456-1.p.ma logic/equality.ma
TPTP/Veloci/GRP159-1.p.ma logic/equality.ma
TPTP/Veloci/ROB030-1.p.ma logic/equality.ma
TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
TPTP/Veloci/LCL139-1.p.ma logic/equality.ma
TPTP/Veloci/GRP547-1.p.ma logic/equality.ma
TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
TPTP/Veloci/LCL139-1.p.ma logic/equality.ma
TPTP/Veloci/GRP547-1.p.ma logic/equality.ma
TPTP/Veloci/GRP467-1.p.ma logic/equality.ma
TPTP/Veloci/GRP145-1.p.ma logic/equality.ma
TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
TPTP/Veloci/COL063-4.p.ma logic/equality.ma
TPTP/Veloci/GRP467-1.p.ma logic/equality.ma
TPTP/Veloci/GRP145-1.p.ma logic/equality.ma
TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
TPTP/Veloci/COL063-4.p.ma logic/equality.ma
TPTP/Veloci/LDA001-1.p.ma logic/equality.ma
TPTP/Veloci/COL050-1.p.ma logic/equality.ma
TPTP/Veloci/BOO010-4.p.ma logic/equality.ma
TPTP/Veloci/LDA001-1.p.ma logic/equality.ma
TPTP/Veloci/COL050-1.p.ma logic/equality.ma
TPTP/Veloci/BOO010-4.p.ma logic/equality.ma
TPTP/Veloci/LCL110-2.p.ma logic/equality.ma
TPTP/Veloci/GRP491-1.p.ma logic/equality.ma
TPTP/Veloci/COL061-3.p.ma logic/equality.ma
TPTP/Veloci/COL017-1.p.ma logic/equality.ma
TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
compose.ma logic/equality.ma
TPTP/Veloci/LCL110-2.p.ma logic/equality.ma
TPTP/Veloci/GRP491-1.p.ma logic/equality.ma
TPTP/Veloci/COL061-3.p.ma logic/equality.ma
TPTP/Veloci/COL017-1.p.ma logic/equality.ma
TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
compose.ma logic/equality.ma
decl.ma nat/orders.ma nat/times.ma
TPTP/Veloci/GRP156-1.p.ma logic/equality.ma
mysql_escaping.ma
TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
decl.ma nat/orders.ma nat/times.ma
TPTP/Veloci/GRP156-1.p.ma logic/equality.ma
mysql_escaping.ma
TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
TPTP/Veloci/BOO071-1.p.ma logic/equality.ma
TPTP/Veloci/BOO013-4.p.ma logic/equality.ma
TPTP/Veloci/GRP582-1.p.ma logic/equality.ma
TPTP/Veloci/BOO071-1.p.ma logic/equality.ma
TPTP/Veloci/BOO013-4.p.ma logic/equality.ma
TPTP/Veloci/GRP582-1.p.ma logic/equality.ma
TPTP/Veloci/RNG008-4.p.ma logic/equality.ma
demodulation_matita.ma nat/minus.ma
TPTP/Veloci/ROB002-1.p.ma logic/equality.ma
tacticals.ma
TPTP/Veloci/RNG008-4.p.ma logic/equality.ma
demodulation_matita.ma nat/minus.ma
TPTP/Veloci/ROB002-1.p.ma logic/equality.ma
tacticals.ma
applys.ma nat/div_and_mod.ma nat/factorial.ma nat/primes.ma
TPTP/Veloci/RNG024-7.p.ma logic/equality.ma
applys.ma nat/div_and_mod.ma nat/factorial.ma nat/primes.ma
TPTP/Veloci/RNG024-7.p.ma logic/equality.ma
TPTP/Veloci/GRP615-1.p.ma logic/equality.ma
TPTP/Veloci/LAT039-1.p.ma logic/equality.ma
luo.ma Z/times.ma logic/equality.ma
TPTP/Veloci/GRP615-1.p.ma logic/equality.ma
TPTP/Veloci/LAT039-1.p.ma logic/equality.ma
luo.ma Z/times.ma logic/equality.ma
TPTP/Veloci/GRP012-4.p.ma logic/equality.ma
naiveparamod.ma logic/equality.ma
TPTP/Veloci/GRP176-2.p.ma logic/equality.ma
TPTP/Veloci/COL014-1.p.ma logic/equality.ma
TPTP/Veloci/GRP012-4.p.ma logic/equality.ma
naiveparamod.ma logic/equality.ma
TPTP/Veloci/GRP176-2.p.ma logic/equality.ma
TPTP/Veloci/COL014-1.p.ma logic/equality.ma
TPTP/Veloci/COL022-1.p.ma logic/equality.ma
TPTP/Veloci/GRP576-1.p.ma logic/equality.ma
TPTP/Veloci/BOO004-2.p.ma logic/equality.ma
TPTP/Veloci/COL022-1.p.ma logic/equality.ma
TPTP/Veloci/GRP576-1.p.ma logic/equality.ma
TPTP/Veloci/BOO004-2.p.ma logic/equality.ma
coercions_open.ma logic/equality.ma nat/nat.ma
paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma
coercions_open.ma logic/equality.ma nat/nat.ma
paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma
TPTP/Veloci/GRP144-1.p.ma logic/equality.ma
TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
TPTP/Veloci/LAT008-1.p.ma logic/equality.ma
demodulation_coq.ma coq.ma
TPTP/Veloci/GRP562-1.p.ma logic/equality.ma
TPTP/Veloci/GRP144-1.p.ma logic/equality.ma
TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
TPTP/Veloci/LAT008-1.p.ma logic/equality.ma
demodulation_coq.ma coq.ma
TPTP/Veloci/GRP562-1.p.ma logic/equality.ma