matita/tests/TPTP/unit_equality_problems.txt

   1 ALG005-1
   2 ALG006-1
   3 ALG007-1
   4 BOO001-1
   5 BOO002-1
   6 BOO002-2
   7 BOO003-2
   8 BOO003-4
   9 BOO004-2
  10 BOO004-4
  11 BOO005-2
  12 BOO005-4
  13 BOO006-2
  14 BOO006-4
  15 BOO007-2
  16 BOO007-4
  17 BOO008-2
  18 BOO008-4
  19 BOO009-2
  20 BOO009-4
  21 BOO010-2
  22 BOO010-4
  23 BOO011-2
  24 BOO011-4
  25 BOO012-2
  26 BOO012-4
  27 BOO013-2
  28 BOO013-4
  29 BOO014-2
  30 BOO014-4
  31 BOO015-2
  32 BOO015-4
  33 BOO016-2
  34 BOO017-2
  35 BOO018-4
  36 BOO019-1
  37 BOO021-1
  38 BOO022-1
  39 BOO023-1
  40 BOO024-1
  41 BOO025-1
  42 BOO026-1
  43 BOO027-1
  44 BOO028-1
  45 BOO029-1
  46 BOO030-1
  47 BOO031-1
  48 BOO032-1
  49 BOO033-1
  50 BOO034-1
  51 BOO036-1
  52 BOO037-2
  53 BOO037-3
  54 BOO067-1
  55 BOO068-1
  56 BOO069-1
  57 BOO070-1
  58 BOO071-1
  59 BOO072-1
  60 BOO073-1
  61 BOO074-1
  62 BOO075-1
  63 BOO076-1
  64 BOO077-1
  65 BOO078-1
  66 BOO079-1
  67 BOO080-1
  68 BOO081-1
  69 BOO082-1
  70 BOO083-1
  71 BOO084-1
  72 BOO085-1
  73 BOO086-1
  74 BOO087-1
  75 BOO088-1
  76 BOO089-1
  77 BOO090-1
  78 BOO091-1
  79 BOO092-1
  80 BOO093-1
  81 BOO094-1
  82 BOO095-1
  83 BOO096-1
  84 BOO097-1
  85 BOO098-1
  86 BOO099-1
  87 BOO100-1
  88 BOO101-1
  89 BOO102-1
  90 BOO103-1
  91 BOO104-1
  92 BOO105-1
  93 BOO106-1
  94 BOO107-1
  95 BOO108-1
  96 COL001-1
  97 COL001-2
  98 COL002-1
  99 COL002-4
 100 COL002-5
 101 COL003-1
 102 COL003-2
 103 COL004-1
 104 COL004-3
 105 COL005-1
 106 COL006-1
 107 COL006-5
 108 COL006-6
 109 COL006-7
 110 COL007-1
 111 COL008-1
 112 COL009-1
 113 COL010-1
 114 COL011-1
 115 COL012-1
 116 COL013-1
 117 COL014-1
 118 COL015-1
 119 COL016-1
 120 COL017-1
 121 COL018-1
 122 COL019-1
 123 COL020-1
 124 COL021-1
 125 COL022-1
 126 COL023-1
 127 COL024-1
 128 COL025-1
 129 COL026-1
 130 COL027-1
 131 COL029-1
 132 COL030-1
 133 COL031-1
 134 COL032-1
 135 COL033-1
 136 COL034-1
 137 COL035-1
 138 COL036-1
 139 COL037-1
 140 COL038-1
 141 COL039-1
 142 COL041-1
 143 COL042-1
 144 COL042-6
 145 COL042-7
 146 COL042-8
 147 COL042-9
 148 COL043-1
 149 COL043-3
 150 COL044-1
 151 COL044-6
 152 COL044-7
 153 COL044-8
 154 COL044-9
 155 COL045-1
 156 COL046-1
 157 COL047-1
 158 COL048-1
 159 COL049-1
 160 COL050-1
 161 COL051-1
 162 COL052-1
 163 COL053-1
 164 COL056-1
 165 COL057-1
 166 COL058-1
 167 COL058-2
 168 COL058-3
 169 COL059-1
 170 COL060-1
 171 COL060-2
 172 COL060-3
 173 COL061-1
 174 COL061-2
 175 COL061-3
 176 COL062-1
 177 COL062-2
 178 COL062-3
 179 COL063-1
 180 COL063-2
 181 COL063-3
 182 COL063-4
 183 COL063-5
 184 COL063-6
 185 COL064-1
 186 COL064-2
 187 COL064-3
 188 COL064-4
 189 COL064-5
 190 COL064-6
 191 COL064-7
 192 COL064-8
 193 COL064-9
 194 COL065-1
 195 COL066-1
 196 COL066-2
 197 COL066-3
 198 COL067-1
 199 COL068-1
 200 COL069-1
 201 COL070-1
 202 COL071-1
 203 COL073-1
 204 COL075-2
 205 COL083-1
 206 COL084-1
 207 COL085-1
 208 COL086-1
 209 COL087-1
 210 GRP001-2
 211 GRP001-4
 212 GRP002-2
 213 GRP002-3
 214 GRP002-4
 215 GRP010-4
 216 GRP011-4
 217 GRP012-4
 218 GRP014-1
 219 GRP022-2
 220 GRP023-2
 221 GRP024-5
 222 GRP114-1
 223 GRP115-1
 224 GRP116-1
 225 GRP117-1
 226 GRP118-1
 227 GRP119-1
 228 GRP120-1
 229 GRP121-1
 230 GRP122-1
 231 GRP136-1
 232 GRP137-1
 233 GRP138-1
 234 GRP139-1
 235 GRP140-1
 236 GRP141-1
 237 GRP142-1
 238 GRP143-1
 239 GRP144-1
 240 GRP145-1
 241 GRP146-1
 242 GRP147-1
 243 GRP148-1
 244 GRP149-1
 245 GRP150-1
 246 GRP151-1
 247 GRP152-1
 248 GRP153-1
 249 GRP154-1
 250 GRP155-1
 251 GRP156-1
 252 GRP157-1
 253 GRP158-1
 254 GRP159-1
 255 GRP160-1
 256 GRP161-1
 257 GRP162-1
 258 GRP163-1
 259 GRP164-1
 260 GRP164-2
 261 GRP165-1
 262 GRP165-2
 263 GRP166-1
 264 GRP166-2
 265 GRP166-3
 266 GRP166-4
 267 GRP167-1
 268 GRP167-2
 269 GRP167-3
 270 GRP167-4
 271 GRP167-5
 272 GRP168-1
 273 GRP168-2
 274 GRP169-1
 275 GRP169-2
 276 GRP170-1
 277 GRP170-2
 278 GRP170-3
 279 GRP170-4
 280 GRP171-1
 281 GRP171-2
 282 GRP172-1
 283 GRP172-2
 284 GRP173-1
 285 GRP174-1
 286 GRP175-1
 287 GRP175-2
 288 GRP175-3
 289 GRP175-4
 290 GRP176-1
 291 GRP176-2
 292 GRP177-1
 293 GRP177-2
 294 GRP178-1
 295 GRP178-2
 296 GRP179-1
 297 GRP179-2
 298 GRP179-3
 299 GRP180-1
 300 GRP180-2
 301 GRP181-1
 302 GRP181-2
 303 GRP181-3
 304 GRP181-4
 305 GRP182-1
 306 GRP182-2
 307 GRP182-3
 308 GRP182-4
 309 GRP183-1
 310 GRP183-2
 311 GRP183-3
 312 GRP183-4
 313 GRP184-1
 314 GRP184-2
 315 GRP184-3
 316 GRP184-4
 317 GRP185-1
 318 GRP185-2
 319 GRP185-3
 320 GRP185-4
 321 GRP186-1
 322 GRP186-2
 323 GRP186-3
 324 GRP186-4
 325 GRP187-1
 326 GRP188-1
 327 GRP188-2
 328 GRP189-1
 329 GRP189-2
 330 GRP190-1
 331 GRP190-2
 332 GRP191-1
 333 GRP191-2
 334 GRP192-1
 335 GRP193-1
 336 GRP193-2
 337 GRP195-1
 338 GRP196-1
 339 GRP200-1
 340 GRP201-1
 341 GRP202-1
 342 GRP203-1
 343 GRP204-1
 344 GRP205-1
 345 GRP206-1
 346 GRP207-1
 347 GRP393-2
 348 GRP394-3
 349 GRP399-1
 350 GRP403-1
 351 GRP404-1
 352 GRP405-1
 353 GRP406-1
 354 GRP407-1
 355 GRP408-1
 356 GRP409-1
 357 GRP410-1
 358 GRP411-1
 359 GRP412-1
 360 GRP413-1
 361 GRP414-1
 362 GRP415-1
 363 GRP416-1
 364 GRP417-1
 365 GRP418-1
 366 GRP419-1
 367 GRP420-1
 368 GRP421-1
 369 GRP422-1
 370 GRP423-1
 371 GRP424-1
 372 GRP425-1
 373 GRP426-1
 374 GRP427-1
 375 GRP428-1
 376 GRP429-1
 377 GRP430-1
 378 GRP431-1
 379 GRP432-1
 380 GRP433-1
 381 GRP434-1
 382 GRP435-1
 383 GRP436-1
 384 GRP437-1
 385 GRP438-1
 386 GRP439-1
 387 GRP440-1
 388 GRP441-1
 389 GRP442-1
 390 GRP443-1
 391 GRP444-1
 392 GRP445-1
 393 GRP446-1
 394 GRP447-1
 395 GRP448-1
 396 GRP449-1
 397 GRP450-1
 398 GRP451-1
 399 GRP452-1
 400 GRP453-1
 401 GRP454-1
 402 GRP455-1
 403 GRP456-1
 404 GRP457-1
 405 GRP458-1
 406 GRP459-1
 407 GRP460-1
 408 GRP461-1
 409 GRP462-1
 410 GRP463-1
 411 GRP464-1
 412 GRP465-1
 413 GRP466-1
 414 GRP467-1
 415 GRP468-1
 416 GRP469-1
 417 GRP470-1
 418 GRP471-1
 419 GRP472-1
 420 GRP473-1
 421 GRP474-1
 422 GRP475-1
 423 GRP476-1
 424 GRP477-1
 425 GRP478-1
 426 GRP479-1
 427 GRP480-1
 428 GRP481-1
 429 GRP482-1
 430 GRP483-1
 431 GRP484-1
 432 GRP485-1
 433 GRP486-1
 434 GRP487-1
 435 GRP488-1
 436 GRP489-1
 437 GRP490-1
 438 GRP491-1
 439 GRP492-1
 440 GRP493-1
 441 GRP494-1
 442 GRP495-1
 443 GRP496-1
 444 GRP497-1
 445 GRP498-1
 446 GRP499-1
 447 GRP500-1
 448 GRP501-1
 449 GRP502-1
 450 GRP503-1
 451 GRP504-1
 452 GRP505-1
 453 GRP506-1
 454 GRP507-1
 455 GRP508-1
 456 GRP509-1
 457 GRP510-1
 458 GRP511-1
 459 GRP512-1
 460 GRP513-1
 461 GRP514-1
 462 GRP515-1
 463 GRP516-1
 464 GRP517-1
 465 GRP518-1
 466 GRP519-1
 467 GRP520-1
 468 GRP521-1
 469 GRP522-1
 470 GRP523-1
 471 GRP524-1
 472 GRP525-1
 473 GRP526-1
 474 GRP527-1
 475 GRP528-1
 476 GRP529-1
 477 GRP530-1
 478 GRP531-1
 479 GRP532-1
 480 GRP533-1
 481 GRP534-1
 482 GRP535-1
 483 GRP536-1
 484 GRP537-1
 485 GRP538-1
 486 GRP539-1
 487 GRP540-1
 488 GRP541-1
 489 GRP542-1
 490 GRP543-1
 491 GRP544-1
 492 GRP545-1
 493 GRP546-1
 494 GRP547-1
 495 GRP548-1
 496 GRP549-1
 497 GRP550-1
 498 GRP551-1
 499 GRP552-1
 500 GRP553-1
 501 GRP554-1
 502 GRP555-1
 503 GRP556-1
 504 GRP557-1
 505 GRP558-1
 506 GRP559-1
 507 GRP560-1
 508 GRP561-1
 509 GRP562-1
 510 GRP563-1
 511 GRP564-1
 512 GRP565-1
 513 GRP566-1
 514 GRP567-1
 515 GRP568-1
 516 GRP569-1
 517 GRP570-1
 518 GRP571-1
 519 GRP572-1
 520 GRP573-1
 521 GRP574-1
 522 GRP575-1
 523 GRP576-1
 524 GRP577-1
 525 GRP578-1
 526 GRP579-1
 527 GRP580-1
 528 GRP581-1
 529 GRP582-1
 530 GRP583-1
 531 GRP584-1
 532 GRP585-1
 533 GRP586-1
 534 GRP587-1
 535 GRP588-1
 536 GRP589-1
 537 GRP590-1
 538 GRP591-1
 539 GRP592-1
 540 GRP593-1
 541 GRP594-1
 542 GRP595-1
 543 GRP596-1
 544 GRP597-1
 545 GRP598-1
 546 GRP599-1
 547 GRP600-1
 548 GRP601-1
 549 GRP602-1
 550 GRP603-1
 551 GRP604-1
 552 GRP605-1
 553 GRP606-1
 554 GRP607-1
 555 GRP608-1
 556 GRP609-1
 557 GRP610-1
 558 GRP611-1
 559 GRP612-1
 560 GRP613-1
 561 GRP614-1
 562 GRP615-1
 563 GRP616-1
 564 HWC004-1
 565 HWC004-2
 566 LAT006-1
 567 LAT007-1
 568 LAT008-1
 569 LAT009-1
 570 LAT010-1
 571 LAT011-1
 572 LAT012-1
 573 LAT013-1
 574 LAT014-1
 575 LAT016-1
 576 LAT017-1
 577 LAT018-1
 578 LAT019-1
 579 LAT020-1
 580 LAT021-1
 581 LAT022-1
 582 LAT023-1
 583 LAT024-1
 584 LAT025-1
 585 LAT026-1
 586 LAT027-1
 587 LAT028-1
 588 LAT031-1
 589 LAT032-1
 590 LAT033-1
 591 LAT034-1
 592 LAT038-1
 593 LAT039-1
 594 LAT039-2
 595 LAT040-1
 596 LAT042-1
 597 LAT043-1
 598 LAT044-1
 599 LAT045-1
 600 LAT046-1
 601 LAT047-1
 602 LAT048-1
 603 LAT049-1
 604 LAT050-1
 605 LAT051-1
 606 LAT052-1
 607 LAT053-1
 608 LAT054-1
 609 LAT055-2
 610 LAT059-1
 611 LAT060-1
 612 LAT061-1
 613 LAT062-1
 614 LAT063-1
 615 LAT070-1
 616 LAT071-1
 617 LAT072-1
 618 LAT073-1
 619 LAT074-1
 620 LAT075-1
 621 LAT076-1
 622 LAT077-1
 623 LAT078-1
 624 LAT079-1
 625 LAT080-1
 626 LAT081-1
 627 LAT082-1
 628 LAT083-1
 629 LAT084-1
 630 LAT085-1
 631 LAT086-1
 632 LAT087-1
 633 LAT088-1
 634 LAT089-1
 635 LAT090-1
 636 LAT091-1
 637 LAT092-1
 638 LAT093-1
 639 LAT094-1
 640 LAT095-1
 641 LAT096-1
 642 LAT097-1
 643 LAT098-1
 644 LAT099-1
 645 LAT100-1
 646 LAT101-1
 647 LAT102-1
 648 LAT103-1
 649 LAT104-1
 650 LAT105-1
 651 LAT106-1
 652 LAT107-1
 653 LAT108-1
 654 LAT109-1
 655 LAT110-1
 656 LAT111-1
 657 LAT112-1
 658 LAT113-1
 659 LAT114-1
 660 LAT115-1
 661 LAT116-1
 662 LAT117-1
 663 LAT118-1
 664 LAT119-1
 665 LAT120-1
 666 LAT121-1
 667 LAT122-1
 668 LAT123-1
 669 LAT124-1
 670 LAT125-1
 671 LAT126-1
 672 LAT127-1
 673 LAT128-1
 674 LAT129-1
 675 LAT130-1
 676 LAT131-1
 677 LAT132-1
 678 LAT133-1
 679 LAT134-1
 680 LAT135-1
 681 LAT136-1
 682 LAT137-1
 683 LAT138-1
 684 LAT139-1
 685 LAT140-1
 686 LAT141-1
 687 LAT142-1
 688 LAT143-1
 689 LAT144-1
 690 LAT145-1
 691 LAT146-1
 692 LAT147-1
 693 LAT148-1
 694 LAT149-1
 695 LAT150-1
 696 LAT151-1
 697 LAT152-1
 698 LAT153-1
 699 LAT154-1
 700 LAT155-1
 701 LAT156-1
 702 LAT157-1
 703 LAT158-1
 704 LAT159-1
 705 LAT160-1
 706 LAT161-1
 707 LAT162-1
 708 LAT163-1
 709 LAT164-1
 710 LAT165-1
 711 LAT166-1
 712 LAT167-1
 713 LAT168-1
 714 LAT169-1
 715 LAT170-1
 716 LAT171-1
 717 LAT172-1
 718 LAT173-1
 719 LAT174-1
 720 LAT175-1
 721 LAT176-1
 722 LAT177-1
 723 LCL109-2
 724 LCL109-6
 725 LCL110-2
 726 LCL111-2
 727 LCL112-2
 728 LCL113-2
 729 LCL114-2
 730 LCL115-2
 731 LCL116-2
 732 LCL132-1
 733 LCL133-1
 734 LCL134-1
 735 LCL135-1
 736 LCL136-1
 737 LCL137-1
 738 LCL138-1
 739 LCL139-1
 740 LCL140-1
 741 LCL141-1
 742 LCL153-1
 743 LCL154-1
 744 LCL155-1
 745 LCL156-1
 746 LCL157-1
 747 LCL158-1
 748 LCL159-1
 749 LCL160-1
 750 LCL161-1
 751 LCL162-1
 752 LCL163-1
 753 LCL164-1
 754 LCL165-1
 755 LCL407-1
 756 LCL407-2
 757 LCL409-1
 758 LCL410-1
 759 LDA001-1
 760 LDA002-1
 761 LDA007-3
 762 RNG007-4
 763 RNG008-3
 764 RNG008-4
 765 RNG008-7
 766 RNG009-5
 767 RNG009-7
 768 RNG010-5
 769 RNG010-6
 770 RNG010-7
 771 RNG011-5
 772 RNG012-6
 773 RNG013-6
 774 RNG014-6
 775 RNG015-6
 776 RNG016-6
 777 RNG017-6
 778 RNG018-6
 779 RNG019-6
 780 RNG019-7
 781 RNG020-6
 782 RNG020-7
 783 RNG021-6
 784 RNG021-7
 785 RNG023-6
 786 RNG023-7
 787 RNG024-6
 788 RNG024-7
 789 RNG025-4
 790 RNG025-5
 791 RNG025-6
 792 RNG025-7
 793 RNG025-8
 794 RNG025-9
 795 RNG026-6
 796 RNG026-7
 797 RNG027-5
 798 RNG027-7
 799 RNG027-8
 800 RNG027-9
 801 RNG028-5
 802 RNG028-7
 803 RNG028-8
 804 RNG028-9
 805 RNG029-5
 806 RNG029-6
 807 RNG029-7
 808 RNG030-6
 809 RNG030-7
 810 RNG031-6
 811 RNG031-7
 812 RNG032-6
 813 RNG032-7
 814 RNG033-6
 815 RNG033-7
 816 RNG033-8
 817 RNG033-9
 818 RNG035-7
 819 RNG036-7
 820 RNG042-2
 821 RNG042-3
 822 RNG043-1
 823 ROB001-1
 824 ROB002-1
 825 ROB003-1
 826 ROB004-1
 827 ROB005-1
 828 ROB006-1
 829 ROB006-2
 830 ROB007-1
 831 ROB007-2
 832 ROB008-1
 833 ROB009-1
 834 ROB010-1
 835 ROB013-1
 836 ROB020-1
 837 ROB020-2
 838 ROB022-1
 839 ROB023-1
 840 ROB024-1
 841 ROB026-1
 842 ROB027-1
 843 ROB028-1
 844 ROB030-1
 845 ROB031-1
 846 ROB032-1
 847 SYN080-1
 848 SYN083-1
 849 SYN305-1
 850 SYN552-1