helm/software/matita/tests/depends

   1 TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
   2 TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
   3 TPTP/Unsatisfiable/PLA011-2.ma logic/equality.ma
   4 dependent_guarded_bove_capretta.ma nat/nat.ma
   5 interactive/test5.ma
   6 TPTP/Veloci/SYN083-1.p.ma logic/equality.ma
   7 TPTP/Unsatisfiable/SWV014-1.ma logic/equality.ma
   8 TPTP/Veloci/COL008-1.p.ma logic/equality.ma
   9 TPTP/Unsatisfiable/LCL063-1.ma logic/equality.ma
  10 TPTP/Unsatisfiable/NUM017-1.ma logic/equality.ma
  11 TPTP/Veloci/GRP604-1.p.ma logic/equality.ma
  12 record.ma
  13 TPTP/Veloci/GRP516-1.p.ma logic/equality.ma
  14 TPTP/Veloci/COL060-3.p.ma logic/equality.ma
  15 TPTP/Veloci/COL016-1.p.ma logic/equality.ma
  16 TPTP/Veloci/GRP612-1.p.ma logic/equality.ma
  17 TPTP/Veloci/COL024-1.p.ma logic/equality.ma
  18 TPTP/Veloci/GRP139-1.p.ma logic/equality.ma
  19 TPTP/Unsatisfiable/LCL167-1.ma logic/equality.ma
  20 TPTP/Veloci/ROB010-1.p.ma logic/equality.ma
  21 TPTP/Veloci/BOO006-2.p.ma logic/equality.ma
  22 TPTP/Veloci/LCL157-1.p.ma logic/equality.ma
  23 TPTP/Veloci/LCL132-1.p.ma logic/equality.ma
  24 constructor.ma coq.ma
  25 TPTP/Veloci/GRP565-1.p.ma logic/equality.ma
  26 elim.ma coq.ma
  27 TPTP/Veloci/GRP155-1.p.ma logic/equality.ma
  28 TPTP/Veloci/BOO004-4.p.ma logic/equality.ma
  29 TPTP/Veloci/LCL140-1.p.ma logic/equality.ma
  30 TPTP/Veloci/GRP573-1.p.ma logic/equality.ma
  31 TPTP/Veloci/GRP598-1.p.ma logic/equality.ma
  32 TPTP/Unsatisfiable/LCL393-1.ma logic/equality.ma
  33 TPTP/Veloci/GRP460-1.p.ma logic/equality.ma
  34 TPTP/Veloci/GRP163-1.p.ma logic/equality.ma
  35 TPTP/Veloci/GRP485-1.p.ma logic/equality.ma
  36 TPTP/Veloci/GRP188-1.p.ma logic/equality.ma
  37 TPTP/Unsatisfiable/LCL253-1.ma logic/equality.ma
  38 TPTP/Veloci/BOO012-4.p.ma logic/equality.ma
  39 TPTP/Unsatisfiable/LCL375-1.ma logic/equality.ma
  40 TPTP/Veloci/GRP581-1.p.ma logic/equality.ma
  41 TPTP/Veloci/COL063-3.p.ma logic/equality.ma
  42 TPTP/Veloci/LCL112-2.p.ma logic/equality.ma
  43 TPTP/Veloci/GRP493-1.p.ma logic/equality.ma
  44 formal_topology.ma logic/connectives.ma
  45 TPTP/Veloci/RNG023-7.p.ma logic/equality.ma
  46 replace.ma coq.ma
  47 test2.ma coq.ma
  48 TPTP/Veloci/BOO009-2.p.ma logic/equality.ma
  49 TPTP/Veloci/COL064-7.p.ma logic/equality.ma
  50 TPTP/Veloci/GRP510-1.p.ma logic/equality.ma
  51 TPTP/Unsatisfiable/LCL037-1.ma logic/equality.ma
  52 TPTP/Veloci/COL010-1.p.ma logic/equality.ma
  53 TPTP/Unsatisfiable/SYN615-1.ma logic/equality.ma
  54 TPTP/Veloci/COL061-2.p.ma logic/equality.ma
  55 TPTP/Veloci/LCL135-1.p.ma logic/equality.ma
  56 TPTP/Veloci/BOO017-2.p.ma logic/equality.ma
  57 TPTP/Unsatisfiable/SYN600-1.ma logic/equality.ma
  58 TPTP/Unsatisfiable/LCL019-1.ma logic/equality.ma
  59 elim_pattern.ma nat/plus.ma
  60 assumption.ma coq.ma
  61 TPTP/Veloci/GRP551-1.p.ma logic/equality.ma
  62 interactive/grafite.ma
  63 TPTP/Veloci/GRP141-1.p.ma logic/equality.ma
  64 TPTP/Veloci/GRP463-1.p.ma logic/equality.ma
  65 TPTP/Unsatisfiable/LCL001-1.ma logic/equality.ma
  66 fix_betareduction.ma coq.ma
  67 TPTP/Unsatisfiable/SYN704-1.ma logic/equality.ma
  68 TPTP/Veloci/GRP606-1.p.ma logic/equality.ma
  69 coercions_dependent.ma decidable_kit/list_aux.ma list/list.ma nat/nat.ma
  70 TPTP/Veloci/GRP518-1.p.ma logic/equality.ma
  71 TPTP/Veloci/GRP584-1.p.ma logic/equality.ma
  72 TPTP/Unsatisfiable/PLA016-1.ma logic/equality.ma
  73 TPTP/Veloci/COL084-1.p.ma logic/equality.ma
  74 TPTP/Veloci/GRP174-1.p.ma logic/equality.ma
  75 paramodulation/boolean_algebra.ma coq.ma
  76 TPTP/Veloci/GRP496-1.p.ma logic/equality.ma
  77 TPTP/Veloci/RNG011-5.p.ma logic/equality.ma
  78 TPTP/Veloci/GRP614-1.p.ma logic/equality.ma
  79 TPTP/Unsatisfiable/PLA001-1.ma logic/equality.ma
  80 inversion.ma coq.ma
  81 TPTP/Veloci/GRP592-1.p.ma logic/equality.ma
  82 TPTP/Unsatisfiable/LCL105-1.ma logic/equality.ma
  83 bad_tests/baseuri.ma
  84 TPTP/Veloci/GRP182-1.p.ma logic/equality.ma
  85 TPTP/Veloci/GRP116-1.p.ma logic/equality.ma
  86 TPTP/Unsatisfiable/LCL230-1.ma logic/equality.ma
  87 coercions.ma nat/compare.ma nat/times.ma
  88 TPTP/Unsatisfiable/LCL227-1.ma logic/equality.ma
  89 TPTP/Veloci/GRP011-4.p.ma logic/equality.ma
  90 TPTP/Veloci/GRP149-1.p.ma logic/equality.ma
  91 TPTP/Veloci/COL013-1.p.ma logic/equality.ma
  92 TPTP/Veloci/COL064-2.p.ma logic/equality.ma
  93 TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
  94 comments.ma coq.ma
  95 TPTP/Unsatisfiable/LCL032-1.ma logic/equality.ma
  96 TPTP/Veloci/BOO006-4.p.ma logic/equality.ma
  97 TPTP/Veloci/COL021-1.p.ma logic/equality.ma
  98 TPTP/Veloci/BOO003-2.p.ma logic/equality.ma
  99 TPTP/Veloci/RNG024-6.p.ma logic/equality.ma
 100 bool.ma coq.ma
 101 ng_tactics.ma logic/connectives.ma nat/plus.ma
 102 TPTP/Veloci/BOO011-2.p.ma logic/equality.ma
 103 TPTP/Veloci/LCL154-1.p.ma logic/equality.ma
 104 TPTP/Veloci/LCL114-2.p.ma logic/equality.ma
 105 TPTP/Unsatisfiable/LCL423-1.ma logic/equality.ma
 106 letrec.ma
 107 TPTP/Unsatisfiable/LCL395-1.ma logic/equality.ma
 108 TPTP/Unsatisfiable/PLA011-1.ma logic/equality.ma
 109 TPTP/Veloci/GRP160-1.p.ma logic/equality.ma
 110 TPTP/Veloci/BOO001-1.p.ma logic/equality.ma
 111 TPTP/Unsatisfiable/PLA008-1.ma logic/equality.ma
 112 TPTP/Veloci/GRP600-1.p.ma logic/equality.ma
 113 TPTP/Unsatisfiable/LCL377-1.ma logic/equality.ma
 114 TPTP/Unsatisfiable/PLA005-2.ma logic/equality.ma
 115 TPTP/Veloci/GRP512-1.p.ma logic/equality.ma
 116 TPTP/Veloci/COL063-5.p.ma logic/equality.ma
 117 continuationals.ma coq.ma
 118 TPTP/Veloci/GRP490-1.p.ma logic/equality.ma
 119 TPTP/Unsatisfiable/SYN653-1.ma logic/equality.ma
 120 TPTP/Veloci/BOO034-1.p.ma logic/equality.ma
 121 TPTP/Unsatisfiable/ANA003-2.ma logic/equality.ma
 122 ng_pts.ma
 123 fold.ma coq.ma
 124 TPTP/Unsatisfiable/LCL084-3.ma logic/equality.ma
 125 TPTP/Veloci/GRP520-1.p.ma logic/equality.ma
 126 TPTP/Veloci/GRP545-1.p.ma logic/equality.ma
 127 a.ma nat/nat.ma
 128 TPTP/Veloci/GRP457-1.p.ma logic/equality.ma
 129 TPTP/Veloci/LAT040-1.p.ma logic/equality.ma
 130 TPTP/Veloci/COL064-9.p.ma logic/equality.ma
 131 TPTP/Veloci/BOO009-4.p.ma logic/equality.ma
 132 TPTP/Veloci/GRP578-1.p.ma logic/equality.ma
 133 change.ma coq.ma
 134 TPTP/Veloci/BOO075-1.p.ma logic/equality.ma
 135 TPTP/Veloci/GRP143-1.p.ma logic/equality.ma
 136 TPTP/Veloci/GRP168-1.p.ma logic/equality.ma
 137 TPTP/Unsatisfiable/SYN617-1.ma logic/equality.ma
 138 TPTP/Unsatisfiable/LCL024-1.ma logic/equality.ma
 139 TPTP/Veloci/GRP561-1.p.ma logic/equality.ma
 140 TPTP/Veloci/GRP586-1.p.ma logic/equality.ma
 141 TPTP/Veloci/GRP498-1.p.ma logic/equality.ma
 142 TPTP/Veloci/GRP176-1.p.ma logic/equality.ma
 143 overred.ma logic/equality.ma
 144 TPTP/Veloci/COL007-1.p.ma logic/equality.ma
 145 TPTP/Unsatisfiable/PLA021-1.ma logic/equality.ma
 146 TPTP/Unsatisfiable/SYN556-1.ma logic/equality.ma
 147 TPTP/Unsatisfiable/LCL125-1.ma logic/equality.ma
 148 TPTP/Unsatisfiable/PLA018-1.ma logic/equality.ma
 149 TPTP/Veloci/GRP603-1.p.ma logic/equality.ma
 150 TPTP/Veloci/COL058-2.p.ma logic/equality.ma
 151 TPTP/Veloci/GRP515-1.p.ma logic/equality.ma
 152 TPTP/Veloci/RNG007-4.p.ma logic/equality.ma
 153 TPTP/Veloci/COL015-1.p.ma logic/equality.ma
 154 TPTP/Unsatisfiable/LCL085-1.ma logic/equality.ma
 155 TPTP/Unsatisfiable/LCL369-1.ma logic/equality.ma
 156 TPTP/Veloci/GRP548-1.p.ma logic/equality.ma
 157 TPTP/Veloci/GRP182-3.p.ma logic/equality.ma
 158 TPTP/Veloci/COL048-1.p.ma logic/equality.ma
 159 TPTP/Veloci/GRP189-2.p.ma logic/equality.ma
 160 TPTP/Veloci/BOO005-2.p.ma logic/equality.ma
 161 TPTP/Veloci/GRP556-1.p.ma logic/equality.ma
 162 TPTP/Veloci/GRP146-1.p.ma logic/equality.ma
 163 TPTP/Veloci/LCL156-1.p.ma logic/equality.ma
 164 TPTP/Veloci/COL064-4.p.ma logic/equality.ma
 165 contradiction.ma coq.ma
 166 TPTP/Veloci/GRP564-1.p.ma logic/equality.ma
 167 inversion2.ma coq.ma
 168 TPTP/Veloci/GRP154-1.p.ma logic/equality.ma
 169 TPTP/Unsatisfiable/SYN599-1.ma logic/equality.ma
 170 TPTP/Veloci/LCL164-1.p.ma logic/equality.ma
 171 TPTP/Veloci/ROB009-1.p.ma logic/equality.ma
 172 TPTP/Veloci/BOO003-4.p.ma logic/equality.ma
 173 ng_elim.ma
 174 TPTP/Veloci/GRP597-1.p.ma logic/equality.ma
 175 TPTP/Veloci/GRP572-1.p.ma logic/equality.ma
 176 TPTP/Veloci/GRP484-1.p.ma logic/equality.ma
 177 TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
 178 fix_che_non_passa_ma_dovrebbe.ma list/list.ma nat/nat.ma
 179 TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
 180 TPTP/Unsatisfiable/LCL425-1.ma logic/equality.ma
 181 TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
 182 TPTP/Veloci/COL062-3.p.ma logic/equality.ma
 183 TPTP/Veloci/GRP492-1.p.ma logic/equality.ma
 184 cut.ma coq.ma
 185 TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
 186 TPTP/Veloci/COL018-1.p.ma logic/equality.ma
 187 TPTP/Unsatisfiable/PLA013-1.ma logic/equality.ma
 188 coercions_contravariant.ma logic/equality.ma nat/nat.ma
 189 tinycals.ma logic/connectives.ma
 190 interactive/automatic_insertion.ma
 191 clearbody.ma coq.ma
 192 TPTP/Unsatisfiable/SYN655-1.ma logic/equality.ma
 193 TPTP/Unsatisfiable/LCL062-1.ma logic/equality.ma
 194 TPTP/Veloci/BOO016-2.p.ma logic/equality.ma
 195 TPTP/Veloci/LCL134-1.p.ma logic/equality.ma
 196 TPTP/Unsatisfiable/SYN640-1.ma logic/equality.ma
 197 TPTP/Veloci/COL060-2.p.ma logic/equality.ma
 198 TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
 199 TPTP/Veloci/LAT039-2.p.ma logic/equality.ma
 200 TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
 201 TPTP/Veloci/GRP186-4.p.ma logic/equality.ma
 202 TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
 203 TPTP/Veloci/GRP550-1.p.ma logic/equality.ma
 204 TPTP/Veloci/GRP509-1.p.ma logic/equality.ma
 205 TPTP/Unsatisfiable/LCL166-1.ma logic/equality.ma
 206 ng_commands.ma ng_pts.ma
 207 TPTP/Veloci/GRP487-1.p.ma logic/equality.ma
 208 TPTP/Veloci/GRP605-1.p.ma logic/equality.ma
 209 paramodulation/BOO075-1.ma
 210 fguidi.ma logic/connectives.ma nat/nat.ma
 211 TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
 212 TPTP/Veloci/GRP517-1.p.ma logic/equality.ma
 213 TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
 214 TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
 215 TPTP/Veloci/COL083-1.p.ma logic/equality.ma
 216 TPTP/Unsatisfiable/SYN711-1.ma logic/equality.ma
 217 TPTP/Unsatisfiable/LCL005-1.ma logic/equality.ma
 218 TPTP/Unsatisfiable/SYN708-1.ma logic/equality.ma
 219 TPTP/Unsatisfiable/PLA023-1.ma logic/equality.ma
 220 coercions_propagation.ma logic/connectives.ma nat/orders.ma
 221 TPTP/Veloci/LAT045-1.p.ma logic/equality.ma
 222 TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
 223 TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
 224 TPTP/Unsatisfiable/LCL249-1.ma logic/equality.ma
 225 TPTP/Unsatisfiable/PLA005-1.ma logic/equality.ma
 226 interactive/test_instance.ma
 227 TPTP/Veloci/COL012-1.p.ma logic/equality.ma
 228 TPTP/Veloci/COL063-2.p.ma logic/equality.ma
 229 TPTP/Unsatisfiable/LCL084-2.ma logic/equality.ma
 230 first.ma
 231 TPTP/Veloci/COL045-1.p.ma logic/equality.ma
 232 TPTP/Unsatisfiable/SYN647-1.ma logic/equality.ma
 233 TPTP/Veloci/BOO005-4.p.ma logic/equality.ma
 234 interactive/test7.ma
 235 bad_induction.ma logic/equality.ma nat/nat.ma
 236 TPTP/Veloci/RNG023-6.p.ma logic/equality.ma
 237 color.ma logic/equality.ma nat/nat.ma
 238 TPTP/Veloci/COL064-6.p.ma logic/equality.ma
 239 apply2.ma nat/nat.ma
 240 metasenv_ordering.ma coq.ma
 241 TPTP/Veloci/GRP608-1.p.ma logic/equality.ma
 242 TPTP/Veloci/BOO010-2.p.ma logic/equality.ma
 243 TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
 244 TPTP/Unsatisfiable/SYN614-1.ma logic/equality.ma
 245 pullback.ma logic/equality.ma
 246 TPTP/Veloci/COL086-1.p.ma logic/equality.ma
 247 TPTP/Veloci/GRP151-1.p.ma logic/equality.ma
 248 TPTP/Unsatisfiable/LCL021-1.ma logic/equality.ma
 249 TPTP/Veloci/LCL161-1.p.ma logic/equality.ma
 250 TPTP/Veloci/GRP616-1.p.ma logic/equality.ma
 251 TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
 252 TPTP/Veloci/GRP206-1.p.ma logic/equality.ma
 253 decompose.ma logic/connectives.ma
 254 TPTP/Veloci/GRP481-1.p.ma logic/equality.ma
 255 TPTP/Veloci/GRP118-1.p.ma logic/equality.ma
 256 generalize.ma coq.ma
 257 TPTP/Veloci/GRP511-1.p.ma logic/equality.ma
 258 TPTP/Veloci/GRP192-1.p.ma logic/equality.ma
 259 TPTP/Unsatisfiable/LCL122-1.ma logic/equality.ma
 260 TPTP/Unsatisfiable/PLA015-1.ma logic/equality.ma
 261 TPTP/Veloci/GRP569-1.p.ma logic/equality.ma
 262 TPTP/Veloci/GRP544-1.p.ma logic/equality.ma
 263 TPTP/Unsatisfiable/LCL119-1.ma logic/equality.ma
 264 dependent_type_inference.ma nat/nat.ma
 265 TPTP/Veloci/GRP456-1.p.ma logic/equality.ma
 266 TPTP/Veloci/GRP159-1.p.ma logic/equality.ma
 267 TPTP/Veloci/ROB030-1.p.ma logic/equality.ma
 268 TPTP/Unsatisfiable/PLA009-2.ma logic/equality.ma
 269 TPTP/Veloci/GRP577-1.p.ma logic/equality.ma
 270 TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
 271 TPTP/Veloci/BOO013-2.p.ma logic/equality.ma
 272 TPTP/Unsatisfiable/SYN639-1.ma logic/equality.ma
 273 rewrite.ma coq.ma
 274 bad_tests/auto.ma coq.ma
 275 TPTP/Veloci/GRP497-1.p.ma logic/equality.ma
 276 diabolic_fix.ma nat/nat.ma
 277 TPTP/Veloci/GRP001-2.p.ma logic/equality.ma
 278 test4.ma coq.ma
 279 clear.ma coq.ma
 280 TPTP/Veloci/GRP602-1.p.ma logic/equality.ma
 281 TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
 282 TPTP/Veloci/LCL139-1.p.ma logic/equality.ma
 283 TPTP/Veloci/GRP547-1.p.ma logic/equality.ma
 284 TPTP/Veloci/COL004-3.p.ma logic/equality.ma
 285 TPTP/Veloci/GRP459-1.p.ma logic/equality.ma
 286 TPTP/Veloci/BOO069-1.p.ma logic/equality.ma
 287 TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
 288 TPTP/Unsatisfiable/LCL394-1.ma logic/equality.ma
 289 TPTP/Unsatisfiable/PLA010-1.ma logic/equality.ma
 290 TPTP/Veloci/GRP188-2.p.ma logic/equality.ma
 291 apply.ma coq.ma
 292 TPTP/Unsatisfiable/PLA007-1.ma logic/equality.ma
 293 TPTP/Veloci/GRP467-1.p.ma logic/equality.ma
 294 TPTP/Veloci/GRP145-1.p.ma logic/equality.ma
 295 TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
 296 TPTP/Veloci/COL063-4.p.ma logic/equality.ma
 297 TPTP/Unsatisfiable/PLA004-2.ma logic/equality.ma
 298 TPTP/Unsatisfiable/LCL074-1.ma logic/equality.ma
 299 TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
 300 TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
 301 TPTP/Unsatisfiable/SYN649-1.ma logic/equality.ma
 302 TPTP/Unsatisfiable/LCL218-1.ma logic/equality.ma
 303 paramodulation.ma coq.ma
 304 TPTP/Veloci/GRP596-1.p.ma logic/equality.ma
 305 coercions_nonuniform.ma
 306 TPTP/Veloci/GRP161-1.p.ma logic/equality.ma
 307 TPTP/Veloci/COL064-8.p.ma logic/equality.ma
 308 TPTP/Veloci/LDA001-1.p.ma logic/equality.ma
 309 TPTP/Veloci/COL050-1.p.ma logic/equality.ma
 310 TPTP/Veloci/BOO010-4.p.ma logic/equality.ma
 311 TPTP/Unsatisfiable/LCL038-1.ma logic/equality.ma
 312 TPTP/Veloci/LCL110-2.p.ma logic/equality.ma
 313 TPTP/Veloci/GRP491-1.p.ma logic/equality.ma
 314 TPTP/Veloci/COL061-3.p.ma logic/equality.ma
 315 TPTP/Veloci/COL017-1.p.ma logic/equality.ma
 316 TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
 317 compose.ma logic/equality.ma
 318 TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
 319 TPTP/Veloci/COL025-1.p.ma logic/equality.ma
 320 TPTP/Unsatisfiable/LCL002-1.ma logic/equality.ma
 321 unifhint.ma list/list.ma nat/nat.ma nat/plus.ma
 322 letrecand.ma nat/nat.ma
 323 hard_refine.ma coq.ma
 324 paramodulation/group.ma coq.ma
 325 TPTP/Unsatisfiable/LCL124-1.ma logic/equality.ma
 326 TPTP/Veloci/LCL158-1.p.ma logic/equality.ma
 327 TPTP/Veloci/LCL133-1.p.ma logic/equality.ma
 328 TPTP/Veloci/GRP541-1.p.ma logic/equality.ma
 329 TPTP/Veloci/GRP566-1.p.ma logic/equality.ma
 330 TPTP/Unsatisfiable/PLA014-2.ma logic/equality.ma
 331 decl.ma nat/orders.ma nat/times.ma
 332 TPTP/Veloci/GRP156-1.p.ma logic/equality.ma
 333 mysql_escaping.ma
 334 TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
 335 TPTP/Unsatisfiable/LCL231-1.ma logic/equality.ma
 336 TPTP/Unsatisfiable/PUZ040-1.ma logic/equality.ma
 337 TPTP/Veloci/GRP182-2.p.ma logic/equality.ma
 338 TPTP/Veloci/GRP574-1.p.ma logic/equality.ma
 339 TPTP/Veloci/GRP599-1.p.ma logic/equality.ma
 340 interactive/drop.ma
 341 interactive/test6.ma
 342 TPTP/Veloci/LDA007-3.p.ma logic/equality.ma
 343 unfold.ma coq.ma
 344 TPTP/Veloci/GRP486-1.p.ma logic/equality.ma
 345 TPTP/Veloci/GRP189-1.p.ma logic/equality.ma
 346 TPTP/Veloci/BOO071-1.p.ma logic/equality.ma
 347 TPTP/Veloci/BOO013-4.p.ma logic/equality.ma
 348 TPTP/Veloci/GRP582-1.p.ma logic/equality.ma
 349 TPTP/Veloci/COL064-3.p.ma logic/equality.ma
 350 TPTP/Veloci/LCL113-2.p.ma logic/equality.ma
 351 TPTP/Veloci/GRP494-1.p.ma logic/equality.ma
 352 TPTP/Veloci/RNG008-4.p.ma logic/equality.ma
 353 demodulation_matita.ma nat/minus.ma
 354 TPTP/Veloci/ROB002-1.p.ma logic/equality.ma
 355 tacticals.ma
 356 TPTP/Veloci/GRP590-1.p.ma logic/equality.ma
 357 TPTP/Veloci/GRP549-1.p.ma logic/equality.ma
 358 TPTP/Veloci/GRP001-4.p.ma logic/equality.ma
 359 TPTP/Unsatisfiable/SYN598-1.ma logic/equality.ma
 360 applys.ma nat/div_and_mod.ma nat/factorial.ma nat/primes.ma
 361 TPTP/Veloci/RNG024-7.p.ma logic/equality.ma
 362 TPTP/Unsatisfiable/RNG004-3.ma logic/equality.ma
 363 injection.ma coq.ma
 364 second.ma first.ma
 365 TPTP/Veloci/COL062-2.p.ma logic/equality.ma
 366 match_inference.ma
 367 TPTP/Unsatisfiable/PLA012-1.ma logic/equality.ma
 368 unifhint_simple.ma logic/equality.ma
 369 simpl.ma coq.ma
 370 TPTP/Unsatisfiable/PLA009-1.ma logic/equality.ma
 371 TPTP/Unsatisfiable/PUZ050-1.ma logic/equality.ma
 372 TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
 373 TPTP/Veloci/COL063-6.p.ma logic/equality.ma
 374 TPTP/Unsatisfiable/SYN654-1.ma logic/equality.ma
 375 third.ma first.ma second.ma
 376 TPTP/Unsatisfiable/LCL061-1.ma logic/equality.ma
 377 TPTP/Veloci/GRP560-1.p.ma logic/equality.ma
 378 TPTP/Veloci/COL085-1.p.ma logic/equality.ma
 379 TPTP/Veloci/GRP150-1.p.ma logic/equality.ma
 380 TPTP/Veloci/GRP615-1.p.ma logic/equality.ma
 381 TPTP/Veloci/LAT039-1.p.ma logic/equality.ma
 382 luo.ma Z/times.ma logic/equality.ma
 383 TPTP/Veloci/GRP022-2.p.ma logic/equality.ma
 384 TPTP/Veloci/GRP186-3.p.ma logic/equality.ma
 385 coercions_russell.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma list/sort.ma nat/compare.ma nat/orders.ma
 386 TPTP/Veloci/GRP117-1.p.ma logic/equality.ma
 387 multiple_inheritance.ma logic/equality.ma
 388 test3.ma coq.ma
 389 TPTP/Veloci/GRP168-2.p.ma logic/equality.ma
 390 TPTP/Veloci/ROB013-1.p.ma logic/equality.ma
 391 TPTP/Veloci/GRP012-4.p.ma logic/equality.ma
 392 naiveparamod.ma logic/equality.ma
 393 TPTP/Veloci/GRP176-2.p.ma logic/equality.ma
 394 TPTP/Veloci/COL014-1.p.ma logic/equality.ma
 395 TPTP/Veloci/GRP543-1.p.ma logic/equality.ma
 396 TPTP/Veloci/GRP568-1.p.ma logic/equality.ma
 397 TPTP/Veloci/GRP158-1.p.ma logic/equality.ma
 398 TPTP/Veloci/GRP455-1.p.ma logic/equality.ma
 399 TPTP/Veloci/COL022-1.p.ma logic/equality.ma
 400 TPTP/Veloci/GRP576-1.p.ma logic/equality.ma
 401 TPTP/Veloci/BOO004-2.p.ma logic/equality.ma
 402 TPTP/Unsatisfiable/SYN707-1.ma logic/equality.ma
 403 TPTP/Veloci/GRP488-1.p.ma logic/equality.ma
 404 TPTP/Veloci/COL058-3.p.ma logic/equality.ma
 405 TPTP/Unsatisfiable/PLA019-1.ma logic/equality.ma
 406 dependent_injection.ma coq.ma
 407 TPTP/Veloci/BOO012-2.p.ma logic/equality.ma
 408 TPTP/Unsatisfiable/PLA004-1.ma logic/equality.ma
 409 TPTP/Veloci/LCL115-2.p.ma logic/equality.ma
 410 absurd.ma coq.ma
 411 TPTP/Unsatisfiable/PUZ042-1.ma logic/equality.ma
 412 TPTP/Veloci/GRP182-4.p.ma logic/equality.ma
 413 TPTP/Unsatisfiable/PUZ039-1.ma logic/equality.ma
 414 TPTP/Unsatisfiable/SYN646-1.ma logic/equality.ma
 415 destruct.ma datatypes/constructors.ma logic/equality.ma nat/nat.ma
 416 TPTP/Unsatisfiable/SYN631-1.ma logic/equality.ma
 417 TPTP/Veloci/GRP513-1.p.ma logic/equality.ma
 418 TPTP/Veloci/COL064-5.p.ma logic/equality.ma
 419 TPTP/Unsatisfiable/SYN628-1.ma logic/equality.ma
 420 TPTP/Veloci/LAT033-1.p.ma logic/equality.ma
 421 TPTP/Veloci/GRP546-1.p.ma logic/equality.ma
 422 TPTP/Unsatisfiable/LCL020-1.ma logic/equality.ma
 423 TPTP/Veloci/GRP458-1.p.ma logic/equality.ma
 424 TPTP/Veloci/GRP136-1.p.ma logic/equality.ma
 425 coercions_open.ma logic/equality.ma nat/nat.ma
 426 paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma
 427 TPTP/Veloci/GRP144-1.p.ma logic/equality.ma
 428 TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
 429 TPTP/Veloci/LAT008-1.p.ma logic/equality.ma
 430 demodulation_coq.ma coq.ma
 431 TPTP/Veloci/GRP562-1.p.ma logic/equality.ma
 432 TPTP/Unsatisfiable/PLA014-1.ma logic/equality.ma
 433 TPTP/Veloci/GRP152-1.p.ma logic/equality.ma
 434 Z/times.ma
 435 coq.ma
 436 datatypes/bool.ma
 437 datatypes/constructors.ma
 438 decidable_kit/list_aux.ma
 439 list/list.ma
 440 list/sort.ma
 441 logic/connectives.ma
 442 logic/equality.ma
 443 nat/compare.ma
 444 nat/div_and_mod.ma
 445 nat/factorial.ma
 446 nat/minus.ma
 447 nat/nat.ma
 448 nat/orders.ma
 449 nat/plus.ma
 450 nat/primes.ma
 451 nat/times.ma