/usr/share/doc/prover9-doc/examples/hard.out is in prover9-doc 0.0.200902a-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 | ============================== Prover9 ===============================
Prover9 (32) version 2009-02A, February 2009.
Process 15842 was started by mccune on cleo,
Wed Feb 25 12:26:11 2009
The command was "/home/mccune/bin/prover9 -f hard.in".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file hard.in
assign(eq_defs,fold).
set(restrict_denials).
formulas(assumptions).
f(x,y) = f(y,x).
f(f(x,y),f(x,f(y,z))) = x.
x' = f(x,x).
end_of_list.
formulas(goals).
f(f(x,x),f(x,x)) = x # label(Sheffer_1).
f(x,f(y,f(y,y))) = f(x,x) # label(Sheffer_2).
f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # label(Sheffer_3).
end_of_list.
============================== end of input ==========================
============================== PROCESS NON-CLAUSAL FORMULAS ==========
% Formulas that are not ordinary clauses:
1 f(f(x,x),f(x,x)) = x # label(Sheffer_1) # label(non_clause) # label(goal). [goal].
2 f(x,f(y,f(y,y))) = f(x,x) # label(Sheffer_2) # label(non_clause) # label(goal). [goal].
3 f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # label(Sheffer_3) # label(non_clause) # label(goal). [goal].
============================== end of process non-clausal formulas ===
============================== PROCESS INITIAL CLAUSES ===============
% Clauses before input processing:
formulas(usable).
end_of_list.
formulas(sos).
f(x,y) = f(y,x). [assumption].
f(f(x,y),f(x,f(y,z))) = x. [assumption].
x' = f(x,x). [assumption].
f(f(c1,c1),f(c1,c1)) != c1 # label(Sheffer_1). [deny(1)].
f(c2,f(c3,f(c3,c3))) != f(c2,c2) # label(Sheffer_2). [deny(2)].
f(f(f(c4,c4),c5),f(f(c6,c6),c5)) != f(f(c5,f(c4,c6)),f(c5,f(c4,c6))) # label(Sheffer_3). [deny(3)].
end_of_list.
formulas(demodulators).
end_of_list.
============================== PREDICATE ELIMINATION =================
No predicates eliminated.
============================== end predicate elimination =============
Auto_denials:
% copying label Sheffer_1 to answer in negative clause
% copying label Sheffer_2 to answer in negative clause
% copying label Sheffer_3 to answer in negative clause
% assign(max_proofs, 3). % (Horn set with more than one neg. clause)
Term ordering decisions:
Predicate symbol precedence: predicate_order([ = ]).
Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, f, ' ]).
After inverse_order: (no changes).
Folding symbols: '/1.
After fold_eq: Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, ', f ]).
Auto_inference settings:
% set(paramodulation). % (positive equality literals)
Auto_process settings: (no changes).
% Operation f is commutative; C redundancy checks enabled.
kept: 4 f(x,y) = f(y,x). [assumption].
kept: 5 f(f(x,y),f(x,f(y,z))) = x. [assumption].
6 x' = f(x,x). [assumption].
kept: 7 f(x,x) = x'. [copy(6),flip(a)].
8 f(f(c1,c1),f(c1,c1)) != c1 # label(Sheffer_1) # answer(Sheffer_1). [deny(1)].
kept: 9 c1'' != c1 # answer(Sheffer_1). [copy(8),rewrite([7(3),7(5),7(5)])].
10 f(c2,f(c3,f(c3,c3))) != f(c2,c2) # label(Sheffer_2) # answer(Sheffer_2). [deny(2)].
kept: 11 f(c2,f(c3,c3')) != c2' # answer(Sheffer_2). [copy(10),rewrite([7(5),7(9)])].
12 f(f(f(c4,c4),c5),f(f(c6,c6),c5)) != f(f(c5,f(c4,c6)),f(c5,f(c4,c6))) # label(Sheffer_3) # answer(Sheffer_3). [deny(3)].
kept: 13 f(f(c5,c4'),f(c5,c6')) != f(c5,f(c4,c6))' # answer(Sheffer_3). [copy(12),rewrite([7(3),4(4),7(7),4(8),7(20)])].
============================== end of process initial clauses ========
============================== CLAUSES FOR SEARCH ====================
% Clauses after input processing:
formulas(usable).
9 c1'' != c1 # answer(Sheffer_1). [copy(8),rewrite([7(3),7(5),7(5)])].
11 f(c2,f(c3,c3')) != c2' # answer(Sheffer_2). [copy(10),rewrite([7(5),7(9)])].
13 f(f(c5,c4'),f(c5,c6')) != f(c5,f(c4,c6))' # answer(Sheffer_3). [copy(12),rewrite([7(3),4(4),7(7),4(8),7(20)])].
end_of_list.
formulas(sos).
4 f(x,y) = f(y,x). [assumption].
5 f(f(x,y),f(x,f(y,z))) = x. [assumption].
7 f(x,x) = x'. [copy(6),flip(a)].
end_of_list.
formulas(demodulators).
4 f(x,y) = f(y,x). [assumption].
% (lex-dep)
5 f(f(x,y),f(x,f(y,z))) = x. [assumption].
7 f(x,x) = x'. [copy(6),flip(a)].
end_of_list.
============================== end of clauses for search =============
============================== SEARCH ================================
% Starting search at 0.01 seconds.
given #1 (I,wt=7): 4 f(x,y) = f(y,x). [assumption].
given #2 (I,wt=11): 5 f(f(x,y),f(x,f(y,z))) = x. [assumption].
given #3 (I,wt=6): 7 f(x,x) = x'. [copy(6),flip(a)].
given #4 (A,wt=11): 14 f(f(x,y),f(y,f(x,z))) = y. [para(4(a,1),5(a,1,1))].
given #5 (T,wt=10): 19 f(x',f(x,f(x,y))) = x. [para(7(a,1),5(a,1,1))].
given #6 (T,wt=9): 34 f(x,f(x,x')) = x'. [para(19(a,1),5(a,1,2)),rewrite([4(2),4(3)])].
============================== PROOF =================================
% Proof 1 at 0.01 (+ 0.00) seconds: Sheffer_1.
% Length of proof is 11.
% Level of proof is 5.
% Maximum clause weight is 11.
% Given clauses 6.
1 f(f(x,x),f(x,x)) = x # label(Sheffer_1) # label(non_clause) # label(goal). [goal].
4 f(x,y) = f(y,x). [assumption].
5 f(f(x,y),f(x,f(y,z))) = x. [assumption].
6 x' = f(x,x). [assumption].
7 f(x,x) = x'. [copy(6),flip(a)].
8 f(f(c1,c1),f(c1,c1)) != c1 # label(Sheffer_1) # answer(Sheffer_1). [deny(1)].
9 c1'' != c1 # answer(Sheffer_1). [copy(8),rewrite([7(3),7(5),7(5)])].
19 f(x',f(x,f(x,y))) = x. [para(7(a,1),5(a,1,1))].
34 f(x,f(x,x')) = x'. [para(19(a,1),5(a,1,2)),rewrite([4(2),4(3)])].
41 x'' = x. [para(34(a,1),5(a,1,2)),rewrite([7(1),7(3)])].
42 $F # answer(Sheffer_1). [resolve(41,a,9,a)].
============================== end of proof ==========================
% Redundant proof: 44 $F # answer(Sheffer_1). [back_rewrite(9),rewrite([41(3)]),xx(a)].
% Disable descendants (x means already disabled):
8x 9x
given #7 (T,wt=5): 41 x'' = x. [para(34(a,1),5(a,1,2)),rewrite([7(1),7(3)])].
given #8 (T,wt=9): 35 f(x',f(x,x')) = x. [para(7(a,1),19(a,1,2,2))].
given #9 (A,wt=11): 15 f(f(x,y),f(x,f(z,y))) = x. [para(4(a,1),5(a,1,2,2))].
given #10 (T,wt=10): 20 f(f(x,y),f(x,y')) = x. [para(7(a,1),5(a,1,2,2))].
given #11 (T,wt=10): 29 f(f(x,y),f(y,x')) = y. [para(7(a,1),14(a,1,2,2))].
given #12 (T,wt=10): 32 f(x',f(x,f(y,x))) = x. [para(4(a,1),19(a,1,2,2))].
given #13 (T,wt=10): 37 f(f(x',y),f(y,x)) = y. [para(19(a,1),14(a,1,2,2))].
given #14 (A,wt=11): 16 f(f(x,y),f(f(y,z),x)) = x. [para(4(a,1),5(a,1,2))].
given #15 (T,wt=10): 61 f(f(x,y),f(y',x)) = x. [para(4(a,1),20(a,1,2))].
given #16 (T,wt=10): 73 f(f(x,y'),f(y,x)) = x. [para(29(a,1),4(a,1)),flip(a)].
given #17 (T,wt=10): 74 f(f(x,y),f(x',y)) = y. [para(4(a,1),29(a,1,2))].
given #18 (T,wt=10): 87 f(x,f(y,x)') = f(y,x). [para(14(a,1),32(a,1,2)),rewrite([4(3)])].
given #19 (A,wt=17): 17 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y). [para(5(a,1),5(a,1,1))].
given #20 (T,wt=8): 132 f(x',f(x,y)) = x. [para(37(a,1),87(a,1,2,1)),rewrite([4(3),37(7)])].
given #21 (T,wt=8): 136 f(x',f(y,x)) = x. [para(73(a,1),87(a,1,2,1)),rewrite([4(3),73(7)])].
given #22 (T,wt=9): 162 f(x,f(x',y)) = x'. [para(41(a,1),132(a,1,1))].
given #23 (T,wt=9): 164 f(x,f(y,x')) = x'. [para(136(a,1),14(a,1,2)),rewrite([4(3)])].
given #24 (A,wt=11): 18 f(x,f(x,f(x,y))) = f(x,y). [para(5(a,1),5(a,1,2)),rewrite([4(2),4(3)])].
given #25 (T,wt=10): 92 f(x,f(x,y)') = f(x,y). [para(15(a,1),32(a,1,2)),rewrite([4(3)])].
given #26 (T,wt=11): 22 f(f(x,f(y,z)),f(y,x)) = x. [para(14(a,1),4(a,1)),flip(a)].
given #27 (T,wt=11): 23 f(f(x,y),f(y,f(z,x))) = y. [para(4(a,1),14(a,1,2,2))].
given #28 (T,wt=11): 24 f(f(x,y),f(f(x,z),y)) = y. [para(4(a,1),14(a,1,2))].
given #29 (A,wt=17): 25 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x). [para(14(a,1),5(a,1,1))].
given #30 (T,wt=11): 26 f(x,f(x,f(y,x))) = f(y,x). [para(14(a,1),5(a,1,2)),rewrite([4(2),4(3)])].
given #31 (T,wt=11): 28 f(f(f(x,y),z),f(z,x)) = z. [para(5(a,1),14(a,1,2,2))].
given #32 (T,wt=11): 31 f(f(f(x,y),z),f(z,y)) = z. [para(14(a,1),14(a,1,2,2))].
given #33 (T,wt=11): 48 f(f(x,y),f(f(z,y),x)) = x. [para(4(a,1),15(a,1,2))].
given #34 (A,wt=19): 27 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [para(5(a,1),14(a,1,1))].
given #35 (T,wt=11): 106 f(f(x,f(y,z)),f(z,x)) = x. [para(14(a,1),16(a,1,2,1))].
given #36 (T,wt=10): 323 f(x,f(y,f(x,y))) = x'. [para(106(a,1),27(a,1,2)),rewrite([7(1)]),flip(a)].
given #37 (T,wt=10): 325 f(x,f(y,f(y,x))) = x'. [para(4(a,1),323(a,1,2,2))].
given #38 (T,wt=11): 180 f(f(x,y),f(f(z,x),y)) = y. [para(4(a,1),23(a,1,2))].
given #39 (A,wt=19): 30 f(x,f(f(x,f(y,z)),f(f(y,x),u))) = f(x,f(y,z)). [para(14(a,1),14(a,1,1))].
given #40 (T,wt=13): 51 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(5(a,1),15(a,1,2)),rewrite([4(4)])].
given #41 (T,wt=13): 54 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(14(a,1),15(a,1,2)),rewrite([4(4)])].
given #42 (T,wt=13): 60 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(15(a,1),15(a,1,2)),rewrite([4(4)])].
given #43 (T,wt=13): 105 f(x,f(f(y,z),f(x,y))) = f(x,y). [para(16(a,1),14(a,1,2)),rewrite([4(4)])].
given #44 (A,wt=17): 49 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y). [para(15(a,1),5(a,1,1))].
given #45 (T,wt=12): 604 f(x,f(x',y)') = f(x,x'). [para(164(a,1),49(a,1,2,2,1)),rewrite([376(5)])].
given #46 (T,wt=12): 644 f(x,f(y,x')') = f(x,x'). [para(4(a,1),604(a,1,2,1))].
given #47 (T,wt=12): 647 f(x',f(x,y)') = f(x,x'). [para(41(a,1),604(a,1,2,1,1)),rewrite([41(7),4(6)])].
============================== PROOF =================================
% Proof 2 at 0.10 (+ 0.02) seconds: Sheffer_2.
% Length of proof is 34.
% Level of proof is 12.
% Maximum clause weight is 19.
% Given clauses 47.
2 f(x,f(y,f(y,y))) = f(x,x) # label(Sheffer_2) # label(non_clause) # label(goal). [goal].
4 f(x,y) = f(y,x). [assumption].
5 f(f(x,y),f(x,f(y,z))) = x. [assumption].
6 x' = f(x,x). [assumption].
7 f(x,x) = x'. [copy(6),flip(a)].
10 f(c2,f(c3,f(c3,c3))) != f(c2,c2) # label(Sheffer_2) # answer(Sheffer_2). [deny(2)].
11 f(c2,f(c3,c3')) != c2' # answer(Sheffer_2). [copy(10),rewrite([7(5),7(9)])].
14 f(f(x,y),f(y,f(x,z))) = y. [para(4(a,1),5(a,1,1))].
15 f(f(x,y),f(x,f(z,y))) = x. [para(4(a,1),5(a,1,2,2))].
16 f(f(x,y),f(f(y,z),x)) = x. [para(4(a,1),5(a,1,2))].
19 f(x',f(x,f(x,y))) = x. [para(7(a,1),5(a,1,1))].
27 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [para(5(a,1),14(a,1,1))].
29 f(f(x,y),f(y,x')) = y. [para(7(a,1),14(a,1,2,2))].
32 f(x',f(x,f(y,x))) = x. [para(4(a,1),19(a,1,2,2))].
34 f(x,f(x,x')) = x'. [para(19(a,1),5(a,1,2)),rewrite([4(2),4(3)])].
37 f(f(x',y),f(y,x)) = y. [para(19(a,1),14(a,1,2,2))].
41 x'' = x. [para(34(a,1),5(a,1,2)),rewrite([7(1),7(3)])].
49 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y). [para(15(a,1),5(a,1,1))].
73 f(f(x,y'),f(y,x)) = x. [para(29(a,1),4(a,1)),flip(a)].
87 f(x,f(y,x)') = f(y,x). [para(14(a,1),32(a,1,2)),rewrite([4(3)])].
106 f(f(x,f(y,z)),f(z,x)) = x. [para(14(a,1),16(a,1,2,1))].
132 f(x',f(x,y)) = x. [para(37(a,1),87(a,1,2,1)),rewrite([4(3),37(7)])].
136 f(x',f(y,x)) = x. [para(73(a,1),87(a,1,2,1)),rewrite([4(3),73(7)])].
162 f(x,f(x',y)) = x'. [para(41(a,1),132(a,1,1))].
164 f(x,f(y,x')) = x'. [para(136(a,1),14(a,1,2)),rewrite([4(3)])].
323 f(x,f(y,f(x,y))) = x'. [para(106(a,1),27(a,1,2)),rewrite([7(1)]),flip(a)].
325 f(x,f(y,f(y,x))) = x'. [para(4(a,1),323(a,1,2,2))].
341 f(x,f(f(y,x),f(y,x)')) = x'. [para(87(a,1),323(a,1,2,2)),rewrite([4(4)])].
376 f(f(x,x'),f(x',y)) = f(x',y)'. [para(162(a,1),325(a,1,2,2)),rewrite([4(5)])].
604 f(x,f(x',y)') = f(x,x'). [para(164(a,1),49(a,1,2,2,1)),rewrite([376(5)])].
647 f(x',f(x,y)') = f(x,x'). [para(41(a,1),604(a,1,2,1,1)),rewrite([41(7),4(6)])].
711 f(f(x,y),f(x,y)') = f(x,x'). [para(5(a,1),647(a,1,2,1)),rewrite([4(4),647(4)]),flip(a)].
745 f(x,f(y,y')) = x'. [back_rewrite(341),rewrite([711(4)])].
746 $F # answer(Sheffer_2). [resolve(745,a,11,a)].
============================== end of proof ==========================
% Redundant proof: 748 $F # answer(Sheffer_2). [back_rewrite(11),rewrite([745(6)]),xx(a)].
% Disable descendants (x means already disabled):
10x 11x
given #48 (T,wt=9): 713 f(x,x') = f(y,y'). [para(14(a,1),647(a,1,2,1)),rewrite([4(4),678(4),711(6)])].
given #49 (A,wt=17): 50 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [para(5(a,1),15(a,1,1))].
given #50 (T,wt=9): 745 f(x,f(y,y')) = x'. [back_rewrite(341),rewrite([711(4)])].
given #51 (T,wt=9): 750 f(f(x,x'),y) = y'. [para(713(a,1),14(a,1,1)),rewrite([132(5)])].
given #52 (T,wt=11): 845 f(x,x')' = f(y,y')'. [para(750(a,1),323(a,1)),rewrite([750(3)])].
given #53 (T,wt=12): 651 f(x,f(f(x',y)',z))' = x. [para(604(a,1),16(a,1,1)),rewrite([4(7),650(8)])].
given #54 (A,wt=19): 52 f(x,f(f(x,f(y,z)),f(f(x,z),u))) = f(x,f(y,z)). [para(15(a,1),14(a,1,1))].
given #55 (T,wt=12): 662 f(x,f(y,f(x',z)'))' = x. [para(604(a,1),31(a,1,2)),rewrite([4(5),4(8),650(8)])].
given #56 (T,wt=12): 676 f(x,f(f(y,x')',z))' = x. [para(644(a,1),5(a,1,1)),rewrite([650(8)])].
given #57 (T,wt=12): 678 f(x',f(y,x)') = f(x,x'). [para(41(a,1),644(a,1,2,1,2)),rewrite([41(7),4(6)])].
given #58 (T,wt=12): 679 f(x,f(y,f(z,x')'))' = x. [para(644(a,1),15(a,1,1)),rewrite([650(8)])].
given #59 (A,wt=17): 53 f(x,f(f(y,x),f(z,f(x,f(y,u))))) = f(y,x). [para(14(a,1),15(a,1,1))].
given #60 (T,wt=12): 752 f(x,f(y,y')') = f(x,x'). [para(713(a,1),92(a,1,2,1))].
given #61 (T,wt=12): 847 f(f(x,x')',y) = f(x,x'). [para(750(a,1),647(a,1,2,1)),rewrite([41(5),737(10)])].
given #62 (T,wt=12): 848 f(x,f(f(x',y)',z)) = x'. [para(651(a,1),41(a,1,1)),flip(a)].
given #63 (T,wt=11): 995 f(x',f(f(x,y)',z)) = x. [para(41(a,1),848(a,1,2,1,1,1)),rewrite([41(7)])].
given #64 (A,wt=17): 59 f(x,f(f(x,y),f(z,f(x,f(u,y))))) = f(x,y). [para(15(a,1),15(a,1,1))].
given #65 (T,wt=10): 1039 f(x',y) = f(y,f(x,y)). [back_rewrite(123),rewrite([1020(5)]),flip(a)].
given #66 (T,wt=10): 1113 f(x,f(y,x)) = f(x,y'). [para(1039(a,1),4(a,1))].
given #67 (T,wt=10): 1132 f(x,f(x,y)) = f(x,y'). [para(1039(a,2),18(a,1,2,2)),rewrite([1113(3),41(2),1113(4)])].
given #68 (T,wt=11): 1018 f(x',f(f(y,x)',z)) = x. [para(4(a,1),995(a,1,2,1,1))].
given #69 (A,wt=16): 62 f(x,f(f(x,y),f(f(x,y'),z))) = f(x,y). [para(20(a,1),5(a,1,1))].
given #70 (T,wt=11): 1019 f(x',f(y,f(x,z)')) = x. [para(4(a,1),995(a,1,2))].
given #71 (T,wt=11): 1287 f(x',f(y,f(z,x)')) = x. [para(4(a,1),1018(a,1,2))].
given #72 (T,wt=12): 918 f(x,f(y,f(x',z)')) = x'. [para(662(a,1),41(a,1,1)),flip(a)].
given #73 (T,wt=12): 920 f(x,f(f(y,x')',z)) = x'. [para(676(a,1),41(a,1,1)),flip(a)].
given #74 (A,wt=17): 64 f(x,f(f(x,y'),f(f(x,y),z))) = f(x,y'). [para(20(a,1),14(a,1,1))].
given #75 (T,wt=12): 937 f(x,f(y,f(z,x')')) = x'. [para(679(a,1),41(a,1,1)),flip(a)].
given #76 (T,wt=12): 993 f(x,f(y,y')') = f(y,y'). [para(752(a,1),87(a,1,2,1)),rewrite([751(7),737(6)]),flip(a)].
given #77 (T,wt=12): 1155 f(f(x,y),f(y,x)) = f(x,y)'. [para(1039(a,2),325(a,1,2,2)),rewrite([1113(4),41(3)])].
given #78 (T,wt=13): 184 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(14(a,1),23(a,1,2)),rewrite([4(4)])].
given #79 (A,wt=16): 69 f(x,f(f(x,y),f(z,f(x,y')))) = f(x,y). [para(20(a,1),15(a,1,1))].
given #80 (T,wt=13): 186 f(x,f(f(y,x),f(z,y))) = f(y,x). [para(23(a,1),15(a,1,2)),rewrite([4(4)])].
given #81 (T,wt=13): 188 f(x,f(f(y,z),f(x,z))) = f(x,z). [para(15(a,1),23(a,1,2)),rewrite([4(4)])].
given #82 (T,wt=13): 204 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(23(a,1),23(a,1,2)),rewrite([4(4)])].
given #83 (T,wt=13): 1020 f(f(x,y)',f(x',z)) = f(x,y). [para(5(a,1),995(a,1,2,1,1))].
given #84 (A,wt=16): 75 f(x,f(f(y,x),f(f(x,y'),z))) = f(y,x). [para(29(a,1),5(a,1,1))].
given #85 (T,wt=13): 1022 f(f(x,y)',f(y',z)) = f(x,y). [para(14(a,1),995(a,1,2,1,1))].
given #86 (T,wt=13): 1338 f(f(x,y)',f(z,x')) = f(x,y). [para(5(a,1),1019(a,1,2,2,1))].
given #87 (T,wt=13): 1340 f(f(x,y)',f(z,y')) = f(x,y). [para(14(a,1),1019(a,1,2,2,1))].
given #88 (T,wt=13): 1446 f(f(x,y)',f(y,x)') = f(y,x). [para(1155(a,1),74(a,1,1)),rewrite([1132(7)])].
given #89 (A,wt=17): 77 f(x,f(f(x,y'),f(f(y,x),z))) = f(x,y'). [para(29(a,1),14(a,1,1))].
given #90 (T,wt=13): 1462 f(f(x,y)',f(y,x)) = f(y,y'). [para(1155(a,1),678(a,1,2,1)),rewrite([41(5),1165(8),7(8),678(8)])].
given #91 (T,wt=13): 1663 f(f(x',y),f(x,z)') = f(x,z). [para(1020(a,1),4(a,1)),flip(a)].
given #92 (T,wt=13): 1743 f(f(x',y),f(z,x)') = f(z,x). [para(1022(a,1),4(a,1)),flip(a)].
given #93 (T,wt=13): 1780 f(f(x,y'),f(y,z)') = f(y,z). [para(1338(a,1),4(a,1)),flip(a)].
given #94 (A,wt=16): 79 f(x,f(f(y,x),f(z,f(x,y')))) = f(y,x). [para(29(a,1),15(a,1,1))].
given #95 (T,wt=13): 1805 f(f(x,y'),f(z,y)') = f(z,y). [para(1340(a,1),4(a,1)),flip(a)].
given #96 (T,wt=14): 161 f(x,f(f(x,y),f(x',z))) = f(x,y). [para(132(a,1),14(a,1,1))].
given #97 (T,wt=14): 163 f(x,f(f(y,x),f(x',z))) = f(y,x). [para(136(a,1),14(a,1,1))].
given #98 (T,wt=14): 199 f(x,f(f(x,y),f(z,x'))) = f(x,y). [para(132(a,1),23(a,1,1))].
given #99 (A,wt=17): 94 f(x,f(f(y',x),f(f(x,y),z))) = f(y',x). [para(37(a,1),5(a,1,1))].
given #100 (T,wt=14): 200 f(x,f(f(y,x),f(z,x'))) = f(y,x). [para(136(a,1),23(a,1,1))].
given #101 (T,wt=14): 217 f(x,f(f(x',y),f(x,z))) = f(x,z). [para(132(a,1),24(a,1,1))].
given #102 (T,wt=14): 218 f(x,f(f(x',y),f(z,x))) = f(z,x). [para(136(a,1),24(a,1,1))].
given #103 (T,wt=14): 404 f(x,f(f(y,x'),f(x,z))) = f(x,z). [para(132(a,1),180(a,1,1))].
given #104 (A,wt=16): 95 f(x,f(f(x,y),f(f(y',x),z))) = f(x,y). [para(37(a,1),14(a,1,1))].
given #105 (T,wt=14): 405 f(x,f(f(y,x'),f(z,x))) = f(z,x). [para(136(a,1),180(a,1,1))].
given #106 (T,wt=14): 462 f(f(x,y),f(x,f(f(x,y'),z))) = x. [para(20(a,1),51(a,1,2,1)),rewrite([20(10)])].
given #107 (T,wt=14): 464 f(f(x,y),f(y,f(f(y,x'),z))) = y. [para(29(a,1),51(a,1,2,1)),rewrite([29(10)])].
given #108 (T,wt=14): 466 f(f(x',y),f(y,f(f(y,x),z))) = y. [para(37(a,1),51(a,1,2,1)),rewrite([37(10)])].
given #109 (A,wt=17): 97 f(x,f(f(y',x),f(z,f(x,y)))) = f(y',x). [para(37(a,1),15(a,1,1))].
given #110 (T,wt=14): 469 f(f(x,y),f(x,f(f(y',x),z))) = x. [para(61(a,1),51(a,1,2,1)),rewrite([61(10)])].
given #111 (T,wt=14): 470 f(f(x,y'),f(x,f(f(y,x),z))) = x. [para(73(a,1),51(a,1,2,1)),rewrite([73(10)])].
given #112 (T,wt=14): 471 f(f(x,y),f(y,f(f(x',y),z))) = y. [para(74(a,1),51(a,1,2,1)),rewrite([74(10)])].
given #113 (T,wt=14): 497 f(f(x,y'),f(x,f(f(x,y),z))) = x. [para(20(a,1),54(a,1,2,1)),rewrite([20(10)])].
given #114 (A,wt=17): 103 f(x,f(f(x,y),f(f(f(y,z),x),u))) = f(x,y). [para(16(a,1),5(a,1,1))].
given #115 (T,wt=14): 501 f(f(x',y),f(y,f(f(x,y),z))) = y. [para(74(a,1),54(a,1,2,1)),rewrite([74(10)])].
given #116 (T,wt=14): 526 f(f(x,y),f(x,f(z,f(x,y')))) = x. [para(20(a,1),60(a,1,2,1)),rewrite([20(10)])].
given #117 (T,wt=14): 528 f(f(x,y),f(y,f(z,f(y,x')))) = y. [para(29(a,1),60(a,1,2,1)),rewrite([29(10)])].
given #118 (T,wt=14): 530 f(f(x',y),f(y,f(z,f(y,x)))) = y. [para(37(a,1),60(a,1,2,1)),rewrite([37(10)])].
given #119 (A,wt=19): 104 f(x,f(f(f(y,z),x),f(f(x,y),u))) = f(f(y,z),x). [para(16(a,1),14(a,1,1))].
given #120 (T,wt=14): 533 f(f(x,y),f(x,f(z,f(y',x)))) = x. [para(61(a,1),60(a,1,2,1)),rewrite([61(10)])].
given #121 (T,wt=14): 534 f(f(x,y'),f(x,f(z,f(y,x)))) = x. [para(73(a,1),60(a,1,2,1)),rewrite([73(10)])].
given #122 (T,wt=14): 535 f(f(x,y),f(y,f(z,f(x',y)))) = y. [para(74(a,1),60(a,1,2,1)),rewrite([74(10)])].
given #123 (T,wt=14): 1023 f(f(x,y),f(x,f(f(y,z)',u))) = x. [para(995(a,1),15(a,1,2,2)),rewrite([4(6)])].
given #124 (A,wt=15): 107 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(14(a,1),16(a,1,2)),rewrite([4(3),4(4)])].
given #125 (T,wt=14): 1025 f(f(f(f(x,y)',z),u),f(u,x)) = u. [para(995(a,1),23(a,1,2,2))].
given #126 (T,wt=14): 1029 f(f(x,y),f(y,f(f(x,z)',u))) = y. [para(995(a,1),31(a,1,1,1))].
given #127 (T,wt=14): 1030 f(f(x,f(f(y,z)',u)),f(y,x)) = x. [para(995(a,1),48(a,1,2,1))].
given #128 (T,wt=13): 3457 f(x,f(y,f(f(x,y),z)')) = x'. [para(1030(a,1),52(a,1,2)),rewrite([7(1),4(5)]),flip(a)].
given #129 (A,wt=17): 109 f(x,f(f(x,y),f(z,f(f(y,u),x)))) = f(x,y). [para(16(a,1),15(a,1,1))].
given #130 (T,wt=13): 3471 f(x,f(y,f(f(y,x),z)')) = x'. [para(4(a,1),3457(a,1,2,2,1,1))].
given #131 (T,wt=13): 3472 f(x,f(y,f(z,f(x,y))')) = x'. [para(4(a,1),3457(a,1,2,2,1))].
given #132 (T,wt=13): 3548 f(x,f(y,f(x,f(y',z)))) = x'. [para(1743(a,1),3457(a,1,2)),rewrite([4(4)])].
given #133 (T,wt=13): 3551 f(x,f(y,f(x,f(z,y')))) = x'. [para(1805(a,1),3457(a,1,2)),rewrite([4(4)])].
given #134 (A,wt=16): 114 f(x,f(f(x,y),f(z,f(y',x)))) = f(x,y). [para(61(a,1),15(a,1,1))].
given #135 (T,wt=13): 3705 f(x,f(y,f(z,f(y,x))')) = x'. [para(4(a,1),3471(a,1,2,2,1))].
given #136 (T,wt=13): 3765 f(x,f(y,f(f(y',z),x))) = x'. [para(1743(a,1),3471(a,1,2)),rewrite([4(4)])].
given #137 (T,wt=13): 3768 f(x,f(y,f(f(z,y'),x))) = x'. [para(1805(a,1),3471(a,1,2)),rewrite([4(4)])].
given #138 (T,wt=13): 3936 f(x,f(y',f(x,f(y,z)))) = x'. [para(41(a,1),3548(a,1,2,2,2,1))].
given #139 (A,wt=17): 116 f(x,f(f(x,y'),f(z,f(y,x)))) = f(x,y'). [para(73(a,1),15(a,1,1))].
given #140 (T,wt=13): 3977 f(x,f(y,f(x',z))') = f(x,y). [para(3548(a,1),97(a,1,2,2)),rewrite([4(5),4(7),1019(7),4(6)]),flip(a)].
given #141 (T,wt=13): 3981 f(x,f(y,f(x',z))) = f(x,y'). [para(3548(a,1),107(a,1,2)),flip(a)].
given #142 (T,wt=13): 4009 f(x,f(y',f(x,f(z,y)))) = x'. [para(41(a,1),3551(a,1,2,2,2,2))].
given #143 (T,wt=13): 4043 f(x,f(y,f(z,x'))') = f(x,y). [para(3551(a,1),97(a,1,2,2)),rewrite([4(5),4(7),1019(7),4(6)]),flip(a)].
given #144 (A,wt=16): 118 f(x,f(f(y,x),f(f(y',x),z))) = f(y,x). [para(74(a,1),5(a,1,1))].
given #145 (T,wt=13): 4046 f(x,f(y,f(z,x'))) = f(x,y'). [para(3551(a,1),107(a,1,2)),flip(a)].
given #146 (T,wt=13): 4260 f(x,f(y',f(f(y,z),x))) = x'. [para(41(a,1),3765(a,1,2,2,1,1))].
given #147 (T,wt=13): 4326 f(x,f(f(x',y),z)') = f(x,z). [para(3765(a,1),97(a,1,2,2)),rewrite([4(5),4(7),1287(7),4(6)]),flip(a)].
given #148 (T,wt=13): 4348 f(x,f(y',f(f(z,y),x))) = x'. [para(41(a,1),3768(a,1,2,2,1,2))].
given #149 (A,wt=17): 119 f(x,f(f(y',x),f(f(y,x),z))) = f(y',x). [para(74(a,1),14(a,1,1))].
given #150 (T,wt=13): 4413 f(x,f(f(y,x'),z)') = f(x,z). [para(3768(a,1),97(a,1,2,2)),rewrite([4(5),4(7),1287(7),4(6)]),flip(a)].
given #151 (T,wt=13): 4433 f(x,f(f(y,z)',f(x,y))) = x'. [para(5(a,1),3936(a,1,2,2,2))].
given #152 (T,wt=13): 4435 f(x,f(f(y,z)',f(x,z))) = x'. [para(14(a,1),3936(a,1,2,2,2))].
given #153 (T,wt=13): 4467 f(x,f(f(y,z)',f(y,x))) = x'. [para(184(a,1),3936(a,1,2,2))].
given #154 (A,wt=16): 121 f(x,f(f(y,x),f(z,f(y',x)))) = f(y,x). [para(74(a,1),15(a,1,1))].
given #155 (T,wt=13): 4469 f(x,f(f(y,z)',f(z,x))) = x'. [para(204(a,1),3936(a,1,2,2))].
given #156 (T,wt=13): 4684 f(x,f(f(x',y),z)) = f(x,z'). [para(4(a,1),3981(a,1,2))].
given #157 (T,wt=13): 5074 f(x,f(f(y,x'),z)) = f(x,z'). [para(31(a,1),4043(a,1,2,1)),flip(a)].
given #158 (T,wt=14): 1031 f(f(x,y),f(f(f(y,z)',u),x)) = x. [para(995(a,1),106(a,1,1,2))].
given #159 (A,wt=15): 143 f(f(x,y),f(x,f(f(x,f(y,z)),u))) = x. [para(17(a,1),15(a,1,2)),rewrite([4(6)])].
given #160 (T,wt=14): 1033 f(f(x,y),f(f(f(x,z)',u),y)) = y. [para(995(a,1),180(a,1,2,1)),rewrite([4(6)])].
given #161 (T,wt=14): 1117 f(f(x',y),f(y,f(z,f(x,y)))) = y. [para(1039(a,2),15(a,1,1))].
given #162 (T,wt=14): 1146 f(f(x,f(y,f(z,x))),f(z',x)) = x. [para(1039(a,2),31(a,1,2)),rewrite([4(3)])].
given #163 (T,wt=14): 1221 f(f(x,f(y,z)),f(x,f(z,y'))) = x. [para(1113(a,1),15(a,1,2,2))].
given #164 (A,wt=23): 153 f(f(x,y),f(f(f(x,y),f(y,z)),f(x,u))) = f(f(x,y),f(y,z)). [para(16(a,1),17(a,1,2,2,1))].
given #165 (T,wt=14): 1247 f(f(x,y'),f(x,f(z,f(x,y)))) = x. [para(1132(a,1),15(a,1,1))].
given #166 (T,wt=14): 1248 f(f(x,f(y,z)),f(x,f(y,z'))) = x. [para(1132(a,1),15(a,1,2,2))].
given #167 (T,wt=14): 1289 f(f(x,y),f(x,f(f(z,y)',u))) = x. [para(1018(a,1),15(a,1,2,2)),rewrite([4(6)])].
given #168 (T,wt=14): 1291 f(f(x',y)',f(x,z)) = f(x',y). [para(162(a,1),1018(a,1,2,1,1)),rewrite([41(5)])].
given #169 (A,wt=20): 168 f(f(x,y)',f(x,f(z,f(x,y)'))) = f(z,f(x,y)'). [para(164(a,1),16(a,1,2)),rewrite([4(4),4(7)])].
given #170 (T,wt=14): 1292 f(f(x,y')',f(y,z)) = f(x,y'). [para(164(a,1),1018(a,1,2,1,1)),rewrite([41(5)])].
given #171 (T,wt=14): 1298 f(f(x,f(f(y,z)',u)),f(z,x)) = x. [para(1018(a,1),48(a,1,2,1))].
given #172 (T,wt=14): 1299 f(f(x,y),f(f(f(z,y)',u),x)) = x. [para(1018(a,1),106(a,1,1,2))].
given #173 (T,wt=14): 1341 f(f(x,y),f(x,f(z,f(y,u)'))) = x. [para(1019(a,1),15(a,1,2,2)),rewrite([4(6)])].
given #174 (A,wt=19): 176 f(x,f(f(x,f(y,z)),f(u,f(y,x)))) = f(x,f(y,z)). [para(22(a,1),15(a,1,1))].
given #175 (T,wt=14): 1348 f(f(x,f(y,f(z,u)')),f(z,x)) = x. [para(1019(a,1),48(a,1,2,1))].
given #176 (T,wt=14): 1349 f(f(x,y),f(f(z,f(y,u)'),x)) = x. [para(1019(a,1),106(a,1,1,2))].
given #177 (T,wt=14): 1360 f(f(x,y),f(x,f(z,f(u,y)'))) = x. [para(1287(a,1),15(a,1,2,2)),rewrite([4(6)])].
given #178 (T,wt=14): 1362 f(f(x',y)',f(z,x)) = f(x',y). [para(162(a,1),1287(a,1,2,2,1)),rewrite([41(5)])].
given #179 (A,wt=19): 177 f(x,f(f(f(y,x),z),f(x,f(y,u)))) = f(x,f(y,u)). [para(22(a,1),16(a,1,1))].
given #180 (T,wt=14): 1363 f(f(x,y')',f(z,y)) = f(x,y'). [para(164(a,1),1287(a,1,2,2,1)),rewrite([41(5)])].
given #181 (T,wt=14): 1369 f(f(x,f(y,f(z,u)')),f(u,x)) = x. [para(1287(a,1),48(a,1,2,1))].
given #182 (T,wt=14): 1370 f(f(x,y),f(f(z,f(u,y)'),x)) = x. [para(1287(a,1),106(a,1,1,2))].
given #183 (T,wt=14): 1445 f(f(x,f(y,z)),f(x,f(z,y)')) = x. [para(1155(a,1),15(a,1,2,2))].
given #184 (A,wt=25): 179 f(f(x,f(y,z)),f(f(y,f(x,f(y,z))),f(x,u))) = f(y,f(x,f(y,z))). [para(22(a,1),17(a,1,2,2,1)),rewrite([4(5),4(11)])].
given #185 (T,wt=14): 1452 f(f(x,f(y,z)),f(f(z,y)',x)) = x. [para(1155(a,1),48(a,1,2,1))].
given #186 (T,wt=14): 1453 f(f(x,f(y,z)'),f(f(z,y),x)) = x. [para(1155(a,1),106(a,1,1,2))].
given #187 (T,wt=13): 9682 f(x,f(y,z)') = f(z,f(x,y)'). [back_rewrite(271),rewrite([9590(6),1136(5)]),flip(a)].
given #188 (T,wt=13): 9736 f(f(x,y)',z) = f(x,f(y,z)'). [para(9682(a,2),4(a,1)),flip(a)].
given #189 (A,wt=17): 181 f(x,f(f(y,x),f(f(x,f(z,y)),u))) = f(y,x). [para(23(a,1),5(a,1,1))].
given #190 (T,wt=13): 9737 f(x,f(y,z)') = f(y,f(x,z)'). [para(4(a,1),9682(a,1,2,1))].
given #191 (T,wt=13): 9738 f(x,f(y,z)') = f(z,f(y,x)'). [para(4(a,1),9682(a,2,2,1))].
given #192 (T,wt=14): 1665 f(f(x,f(y',z)),f(x,f(y,u))) = x. [para(1020(a,1),15(a,1,2,2))].
given #193 (T,wt=14): 1666 f(f(x,y),f(x',z)') = f(x',z). [para(1020(a,1),29(a,1,1)),rewrite([41(6),1113(6)])].
given #194 (A,wt=18): 240 f(f(x,y),f(x,f(f(f(x,y),f(x',z)),u))) = x. [para(132(a,1),25(a,1,2,1)),rewrite([132(11)])].
given #195 (T,wt=14): 1672 f(f(x,f(y',z)),f(f(y,u),x)) = x. [para(1020(a,1),48(a,1,2,1))].
given #196 (T,wt=14): 1673 f(f(x,f(y,z)),f(f(y',u),x)) = x. [para(1020(a,1),106(a,1,1,2))].
given #197 (T,wt=14): 1745 f(f(x,f(y',z)),f(x,f(u,y))) = x. [para(1022(a,1),15(a,1,2,2))].
given #198 (T,wt=14): 1746 f(f(x,y),f(y',z)') = f(y',z). [para(1022(a,1),29(a,1,1)),rewrite([41(6),1113(6)])].
given #199 (A,wt=21): 242 f(f(x',y),f(x',f(f(f(x',y),f(x,z)),u))) = x'. [para(162(a,1),25(a,1,2,1)),rewrite([162(13)])].
given #200 (T,wt=14): 1752 f(f(x,f(y',z)),f(f(u,y),x)) = x. [para(1022(a,1),48(a,1,2,1))].
given #201 (T,wt=14): 1753 f(f(x,f(y,z)),f(f(z',u),x)) = x. [para(1022(a,1),106(a,1,1,2))].
given #202 (T,wt=14): 1782 f(f(x,f(y,z')),f(x,f(z,u))) = x. [para(1338(a,1),15(a,1,2,2))].
given #203 (T,wt=14): 1783 f(f(x,y),f(z,x')') = f(z,x'). [para(1338(a,1),29(a,1,1)),rewrite([41(6),1113(6)])].
given #204 (A,wt=23): 246 f(f(x,f(y,z)),f(x,f(f(f(x,f(y,z)),f(f(z,x),u)),w))) = x. [para(23(a,1),25(a,1,2,1)),rewrite([23(14)])].
given #205 (T,wt=14): 1789 f(f(x,f(y,z')),f(f(z,u),x)) = x. [para(1338(a,1),48(a,1,2,1))].
given #206 (T,wt=14): 1790 f(f(x,f(y,z)),f(f(u,y'),x)) = x. [para(1338(a,1),106(a,1,1,2))].
given #207 (T,wt=14): 1807 f(f(x,f(y,z')),f(x,f(u,z))) = x. [para(1340(a,1),15(a,1,2,2))].
given #208 (T,wt=14): 1808 f(f(x,y),f(z,y')') = f(z,y'). [para(1340(a,1),29(a,1,1)),rewrite([41(6),1113(6)])].
given #209 (A,wt=21): 275 f(f(x,y),f(x,f(f(f(x,y),f(f(f(z,y),x),u)),w))) = x. [para(31(a,1),25(a,1,2,1)),rewrite([31(13)])].
given #210 (T,wt=14): 1814 f(f(x,f(y,z')),f(f(u,z),x)) = x. [para(1340(a,1),48(a,1,2,1))].
given #211 (T,wt=14): 1815 f(f(x,f(y,z)),f(f(u,z'),x)) = x. [para(1340(a,1),106(a,1,1,2))].
given #212 (T,wt=14): 1828 f(x',f(y,f(z,f(x,u)')')) = x. [para(1019(a,1),1340(a,1,1,1)),rewrite([1019(12)])].
given #213 (T,wt=14): 1830 f(x',f(y,f(z,f(u,x)')')) = x. [para(1287(a,1),1340(a,1,1,1)),rewrite([1287(12)])].
given #214 (A,wt=17): 432 f(f(x,y),f(x,f(f(f(y,z),f(x,y)),u))) = x. [para(16(a,1),30(a,1,2,1)),rewrite([16(11)])].
given #215 (T,wt=14): 1844 f(f(x,f(y,z)'),f(x,f(z,y))) = x. [para(1446(a,1),5(a,1,2,2))].
given #216 (T,wt=14): 1933 f(f(x,f(y,z)),f(z,y)') = f(z,y). [para(1446(a,1),1780(a,1,2,1)),rewrite([41(3),1446(10)])].
given #217 (T,wt=14): 3075 f(f(x,f(y,z)),f(x,f(y',u))) = x. [para(5(a,1),1023(a,1,2,2,1,1))].
given #218 (T,wt=14): 3077 f(f(x,f(y,z)),f(x,f(z',u))) = x. [para(14(a,1),1023(a,1,2,2,1,1))].
given #219 (A,wt=29): 507 f(f(f(x,y),f(x,z)),f(f(x,y),f(f(f(f(x,y),f(x,z)),f(y,u)),w))) = f(x,y). [para(54(a,1),25(a,1,2,1)),rewrite([54(16)])].
============================== PROOF =================================
% Proof 3 at 5.54 (+ 0.04) seconds: Sheffer_3.
% Length of proof is 157.
% Level of proof is 31.
% Maximum clause weight is 35.
% Given clauses 219.
3 f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # label(Sheffer_3) # label(non_clause) # label(goal). [goal].
4 f(x,y) = f(y,x). [assumption].
5 f(f(x,y),f(x,f(y,z))) = x. [assumption].
6 x' = f(x,x). [assumption].
7 f(x,x) = x'. [copy(6),flip(a)].
12 f(f(f(c4,c4),c5),f(f(c6,c6),c5)) != f(f(c5,f(c4,c6)),f(c5,f(c4,c6))) # label(Sheffer_3) # answer(Sheffer_3). [deny(3)].
13 f(f(c5,c4'),f(c5,c6')) != f(c5,f(c4,c6))' # answer(Sheffer_3). [copy(12),rewrite([7(3),4(4),7(7),4(8),7(20)])].
14 f(f(x,y),f(y,f(x,z))) = y. [para(4(a,1),5(a,1,1))].
15 f(f(x,y),f(x,f(z,y))) = x. [para(4(a,1),5(a,1,2,2))].
16 f(f(x,y),f(f(y,z),x)) = x. [para(4(a,1),5(a,1,2))].
17 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y). [para(5(a,1),5(a,1,1))].
18 f(x,f(x,f(x,y))) = f(x,y). [para(5(a,1),5(a,1,2)),rewrite([4(2),4(3)])].
19 f(x',f(x,f(x,y))) = x. [para(7(a,1),5(a,1,1))].
20 f(f(x,y),f(x,y')) = x. [para(7(a,1),5(a,1,2,2))].
23 f(f(x,y),f(y,f(z,x))) = y. [para(4(a,1),14(a,1,2,2))].
25 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x). [para(14(a,1),5(a,1,1))].
27 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [para(5(a,1),14(a,1,1))].
29 f(f(x,y),f(y,x')) = y. [para(7(a,1),14(a,1,2,2))].
31 f(f(f(x,y),z),f(z,y)) = z. [para(14(a,1),14(a,1,2,2))].
32 f(x',f(x,f(y,x))) = x. [para(4(a,1),19(a,1,2,2))].
34 f(x,f(x,x')) = x'. [para(19(a,1),5(a,1,2)),rewrite([4(2),4(3)])].
37 f(f(x',y),f(y,x)) = y. [para(19(a,1),14(a,1,2,2))].
41 x'' = x. [para(34(a,1),5(a,1,2)),rewrite([7(1),7(3)])].
48 f(f(x,y),f(f(z,y),x)) = x. [para(4(a,1),15(a,1,2))].
49 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y). [para(15(a,1),5(a,1,1))].
51 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(5(a,1),15(a,1,2)),rewrite([4(4)])].
52 f(x,f(f(x,f(y,z)),f(f(x,z),u))) = f(x,f(y,z)). [para(15(a,1),14(a,1,1))].
54 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(14(a,1),15(a,1,2)),rewrite([4(4)])].
60 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(15(a,1),15(a,1,2)),rewrite([4(4)])].
64 f(x,f(f(x,y'),f(f(x,y),z))) = f(x,y'). [para(20(a,1),14(a,1,1))].
69 f(x,f(f(x,y),f(z,f(x,y')))) = f(x,y). [para(20(a,1),15(a,1,1))].
73 f(f(x,y'),f(y,x)) = x. [para(29(a,1),4(a,1)),flip(a)].
74 f(f(x,y),f(x',y)) = y. [para(4(a,1),29(a,1,2))].
77 f(x,f(f(x,y'),f(f(y,x),z))) = f(x,y'). [para(29(a,1),14(a,1,1))].
87 f(x,f(y,x)') = f(y,x). [para(14(a,1),32(a,1,2)),rewrite([4(3)])].
92 f(x,f(x,y)') = f(x,y). [para(15(a,1),32(a,1,2)),rewrite([4(3)])].
97 f(x,f(f(y',x),f(z,f(x,y)))) = f(y',x). [para(37(a,1),15(a,1,1))].
105 f(x,f(f(y,z),f(x,y))) = f(x,y). [para(16(a,1),14(a,1,2)),rewrite([4(4)])].
106 f(f(x,f(y,z)),f(z,x)) = x. [para(14(a,1),16(a,1,2,1))].
107 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(14(a,1),16(a,1,2)),rewrite([4(3),4(4)])].
123 f(x,f(f(y,x)',f(y',x))) = f(y',x). [para(74(a,1),29(a,1,1)),rewrite([4(5)])].
132 f(x',f(x,y)) = x. [para(37(a,1),87(a,1,2,1)),rewrite([4(3),37(7)])].
136 f(x',f(y,x)) = x. [para(73(a,1),87(a,1,2,1)),rewrite([4(3),73(7)])].
153 f(f(x,y),f(f(f(x,y),f(y,z)),f(x,u))) = f(f(x,y),f(y,z)). [para(16(a,1),17(a,1,2,2,1))].
162 f(x,f(x',y)) = x'. [para(41(a,1),132(a,1,1))].
164 f(x,f(y,x')) = x'. [para(136(a,1),14(a,1,2)),rewrite([4(3)])].
184 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(14(a,1),23(a,1,2)),rewrite([4(4)])].
186 f(x,f(f(y,x),f(z,y))) = f(y,x). [para(23(a,1),15(a,1,2)),rewrite([4(4)])].
204 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(23(a,1),23(a,1,2)),rewrite([4(4)])].
271 f(f(x,y)',f(y,f(z,f(x,y)'))) = f(z,f(x,y)'). [para(164(a,1),31(a,1,1)),rewrite([4(6)])].
323 f(x,f(y,f(x,y))) = x'. [para(106(a,1),27(a,1,2)),rewrite([7(1)]),flip(a)].
325 f(x,f(y,f(y,x))) = x'. [para(4(a,1),323(a,1,2,2))].
376 f(f(x,x'),f(x',y)) = f(x',y)'. [para(162(a,1),325(a,1,2,2)),rewrite([4(5)])].
463 f(f(x,y),f(x',f(f(x,y),f(y,z)))) = f(f(x,y),f(y,z)). [para(51(a,1),29(a,1,1)),rewrite([4(6)])].
466 f(f(x',y),f(y,f(f(y,x),z))) = y. [para(37(a,1),51(a,1,2,1)),rewrite([37(10)])].
488 f(f(x,f(x,y)),f(f(x,y),f(y,z))) = f(f(x,y),f(y,z))'. [para(51(a,1),325(a,1,2,2)),rewrite([4(6)])].
501 f(f(x',y),f(y,f(f(x,y),z))) = y. [para(74(a,1),54(a,1,2,1)),rewrite([74(10)])].
507 f(f(f(x,y),f(x,z)),f(f(x,y),f(f(f(f(x,y),f(x,z)),f(y,u)),w))) = f(x,y). [para(54(a,1),25(a,1,2,1)),rewrite([54(16)])].
513 f(f(x,f(y,x)),f(f(y,x),f(y,z))) = f(f(y,x),f(y,z))'. [para(54(a,1),325(a,1,2,2)),rewrite([4(6)])].
526 f(f(x,y),f(x,f(z,f(x,y')))) = x. [para(20(a,1),60(a,1,2,1)),rewrite([20(10)])].
530 f(f(x',y),f(y,f(z,f(y,x)))) = y. [para(37(a,1),60(a,1,2,1)),rewrite([37(10)])].
581 f(f(x,y),f(x,f(f(x,y),z))) = f(x,f(f(x,y),z))'. [para(51(a,1),105(a,1,2)),rewrite([4(3),4(6),7(7),4(7),4(9)]),flip(a)].
604 f(x,f(x',y)') = f(x,x'). [para(164(a,1),49(a,1,2,2,1)),rewrite([376(5)])].
650 f(f(x,x'),f(x,y)) = f(x,y)'. [para(604(a,1),37(a,1,1)),rewrite([41(3),4(2),41(4),4(5),92(5),41(6)])].
651 f(x,f(f(x',y)',z))' = x. [para(604(a,1),16(a,1,1)),rewrite([4(7),650(8)])].
848 f(x,f(f(x',y)',z)) = x'. [para(651(a,1),41(a,1,1)),flip(a)].
995 f(x',f(f(x,y)',z)) = x. [para(41(a,1),848(a,1,2,1,1,1)),rewrite([41(7)])].
1018 f(x',f(f(y,x)',z)) = x. [para(4(a,1),995(a,1,2,1,1))].
1019 f(x',f(y,f(x,z)')) = x. [para(4(a,1),995(a,1,2))].
1020 f(f(x,y)',f(x',z)) = f(x,y). [para(5(a,1),995(a,1,2,1,1))].
1022 f(f(x,y)',f(y',z)) = f(x,y). [para(14(a,1),995(a,1,2,1,1))].
1030 f(f(x,f(f(y,z)',u)),f(y,x)) = x. [para(995(a,1),48(a,1,2,1))].
1039 f(x',y) = f(y,f(x,y)). [back_rewrite(123),rewrite([1020(5)]),flip(a)].
1113 f(x,f(y,x)) = f(x,y'). [para(1039(a,1),4(a,1))].
1124 f(f(x,y)',f(f(y,z),x)) = f(x,f(y,z)'). [para(16(a,1),1039(a,2,2)),rewrite([4(8),1113(8)])].
1132 f(x,f(x,y)) = f(x,y'). [para(1039(a,2),18(a,1,2,2)),rewrite([1113(3),41(2),1113(4)])].
1136 f(f(x,y)',f(y,f(z,x))) = f(y,f(z,x)'). [para(23(a,1),1039(a,2,2)),rewrite([4(8),1132(8)])].
1155 f(f(x,y),f(y,x)) = f(x,y)'. [para(1039(a,2),325(a,1,2,2)),rewrite([1113(4),41(3)])].
1162 f(f(x,y),f(y,z)') = f(x',f(f(x,y),f(y,z))). [para(51(a,1),1039(a,2,2)),rewrite([4(10),1132(10)]),flip(a)].
1165 f(f(x,y),f(x,z)') = f(y',f(f(x,y),f(x,z))). [para(54(a,1),1039(a,2,2)),rewrite([4(10),1132(10)]),flip(a)].
1189 f(f(x,y'),f(f(y,x),f(y,z))) = f(f(y,x),f(y,z))'. [back_rewrite(513),rewrite([1113(2)])].
1215 f(f(x,y'),f(f(x,y),f(y,z))) = f(f(x,y),f(y,z))'. [back_rewrite(488),rewrite([1132(2)])].
1248 f(f(x,f(y,z)),f(x,f(y,z'))) = x. [para(1132(a,1),15(a,1,2,2))].
1287 f(x',f(y,f(z,x)')) = x. [para(4(a,1),1018(a,1,2))].
1340 f(f(x,y)',f(z,y')) = f(x,y). [para(14(a,1),1019(a,1,2,2,1))].
1362 f(f(x',y)',f(z,x)) = f(x',y). [para(162(a,1),1287(a,1,2,2,1)),rewrite([41(5)])].
1411 f(f(x,y'),f(x',f(f(x,y'),f(f(x,y),z)))) = f(f(x,y'),f(f(x,y),z)). [para(64(a,1),29(a,1,1)),rewrite([4(9)])].
1453 f(f(x,f(y,z)'),f(f(z,y),x)) = x. [para(1155(a,1),106(a,1,1,2))].
1576 f(f(x,y),f(z,x)') = f(y',f(f(x,y),f(z,x))). [para(186(a,1),1113(a,1,2)),rewrite([4(5),1132(5),4(9)])].
1743 f(f(x',y),f(z,x)') = f(z,x). [para(1022(a,1),4(a,1)),flip(a)].
1805 f(f(x,y'),f(z,y)') = f(z,y). [para(1340(a,1),4(a,1)),flip(a)].
1856 f(f(x,y'),f(x',f(f(x,y'),f(f(y,x),z)))) = f(f(x,y'),f(f(y,x),z)). [para(77(a,1),29(a,1,1)),rewrite([4(9)])].
2337 f(x,f(y',f(x,f(f(x,y),z)))) = f(x,f(f(x,y),z)). [para(466(a,1),16(a,1,2)),rewrite([4(5),4(6)])].
2800 f(f(x',y),f(f(f(x',y),f(y,z)),f(u,f(x,f(f(x',y),f(y,z)))))) = f(f(x',y),f(y,z)). [para(51(a,1),530(a,1,1)),rewrite([4(11)])].
2838 f(f(f(x',y)',f(y,f(z,f(y,x)))),f(f(y,f(z,f(y,x))),f(y,u))) = f(y,f(z,f(y,x))). [para(530(a,1),501(a,1,2,2,1))].
3185 f(f(x',f(y,z)),f(x,f(y,f(x',f(y,z))))) = f(y,f(x',f(y,z))). [para(107(a,1),37(a,1,1)),rewrite([4(8)])].
3457 f(x,f(y,f(f(x,y),z)')) = x'. [para(1030(a,1),52(a,1,2)),rewrite([7(1),4(5)]),flip(a)].
3471 f(x,f(y,f(f(y,x),z)')) = x'. [para(4(a,1),3457(a,1,2,2,1,1))].
3472 f(x,f(y,f(z,f(x,y))')) = x'. [para(4(a,1),3457(a,1,2,2,1))].
3548 f(x,f(y,f(x,f(y',z)))) = x'. [para(1743(a,1),3457(a,1,2)),rewrite([4(4)])].
3551 f(x,f(y,f(x,f(z,y')))) = x'. [para(1805(a,1),3457(a,1,2)),rewrite([4(4)])].
3705 f(x,f(y,f(z,f(y,x))')) = x'. [para(4(a,1),3471(a,1,2,2,1))].
3765 f(x,f(y,f(f(y',z),x))) = x'. [para(1743(a,1),3471(a,1,2)),rewrite([4(4)])].
3768 f(x,f(y,f(f(z,y'),x))) = x'. [para(1805(a,1),3471(a,1,2)),rewrite([4(4)])].
3799 f(f(x,f(y,f(x,z))),f(z,f(f(z',x),f(x,u)))) = f(x,f(y,f(x,z)))'. [para(530(a,1),3471(a,1,2,2,1,1)),rewrite([1162(8),41(5)])].
3879 f(f(x,y)',f(z,f(x,y'))') = f(x,f(z,f(x,y'))'). [para(3472(a,1),184(a,1,2)),rewrite([4(2),1132(2),4(7),4(9),1132(9)])].
3886 f(f(x,f(y,z'))',f(z,y)') = f(y,f(x,f(y,z'))'). [para(3472(a,1),204(a,1,2)),rewrite([4(2),1113(2),4(9),1113(9)])].
3936 f(x,f(y',f(x,f(y,z)))) = x'. [para(41(a,1),3548(a,1,2,2,2,1))].
3977 f(x,f(y,f(x',z))') = f(x,y). [para(3548(a,1),97(a,1,2,2)),rewrite([4(5),4(7),1019(7),4(6)]),flip(a)].
3981 f(x,f(y,f(x',z))) = f(x,y'). [para(3548(a,1),107(a,1,2)),flip(a)].
3991 f(f(x,y'),f(x',f(y,z))) = f(y,f(x',f(y,z))). [back_rewrite(3185),rewrite([3981(8),4(6)])].
4043 f(x,f(y,f(z,x'))') = f(x,y). [para(3551(a,1),97(a,1,2,2)),rewrite([4(5),4(7),1019(7),4(6)]),flip(a)].
4162 f(x',f(y,f(z,f(y,x))')') = f(y,f(z,f(y,x))'). [para(3705(a,1),29(a,1,1)),rewrite([4(7),1132(8)])].
4260 f(x,f(y',f(f(y,z),x))) = x'. [para(41(a,1),3765(a,1,2,2,1,1))].
4348 f(x,f(y',f(f(z,y),x))) = x'. [para(41(a,1),3768(a,1,2,2,1,2))].
4433 f(x,f(f(y,z)',f(x,y))) = x'. [para(5(a,1),3936(a,1,2,2,2))].
4610 f(f(x,y),f(x',f(y,f(x',z))')) = f(y,f(x',z))'. [para(3977(a,1),29(a,1,1)),rewrite([4(7)])].
4684 f(x,f(f(x',y),z)) = f(x,z'). [para(4(a,1),3981(a,1,2))].
4808 f(f(x,f(y,f(x,z))),f(z,f(x,u)')) = f(x,f(y,f(x,z)))'. [back_rewrite(3799),rewrite([4684(8)])].
4845 f(f(x',y),f(f(f(x',y),f(y,z)),f(u,f(x,f(y,z)')))) = f(f(x',y),f(y,z)). [back_rewrite(2800),rewrite([4684(11)])].
5074 f(x,f(f(y,x'),z)) = f(x,z'). [para(31(a,1),4043(a,1,2,1)),flip(a)].
5418 f(x',f(f(x,y),z)') = f(x',z). [para(4260(a,1),97(a,1,2,2)),rewrite([4(6),4(8),1287(8),4(7)]),flip(a)].
5626 f(x',f(f(y,x),z)') = f(x',z). [para(4348(a,1),97(a,1,2,2)),rewrite([4(6),4(8),1287(8),4(7)]),flip(a)].
5935 f(f(x,y)',f(z,x)) = f(f(x,y)',z'). [para(4433(a,1),107(a,1,2)),flip(a)].
5989 f(f(x,y)',f(y,z)') = f(x,f(y,z)'). [back_rewrite(1124),rewrite([5935(5)])].
6425 f(x',f(f(x,y),z)) = f(x',z'). [para(41(a,1),4684(a,1,2,1,1))].
6733 f(f(x,y'),f(f(y,x),z)) = f(f(x,y'),f(x',z)). [back_rewrite(1856),rewrite([6425(9),5626(7)]),flip(a)].
6749 f(f(x,y'),f(f(x,y),z)) = f(f(x,y'),f(x',z)). [back_rewrite(1411),rewrite([6425(9),5418(7)]),flip(a)].
6758 f(f(x,y),f(y,z)') = f(x',f(y,z)'). [back_rewrite(1162),rewrite([6425(9)])].
6766 f(f(x,y),f(x',f(y,z)')) = f(f(x,y),f(y,z)). [back_rewrite(463),rewrite([6425(6)])].
6788 f(f(x,y),f(x,z))' = f(x,f(y',f(x,z))). [back_rewrite(1189),rewrite([6733(6),3991(6)]),flip(a)].
6794 f(f(x,y),f(y,z))' = f(y,f(x',f(y,z))). [back_rewrite(1215),rewrite([6749(6),3991(6)]),flip(a)].
6808 f(f(x,y),f(y,f(x',z))) = f(y,f(x',z))'. [back_rewrite(4610),rewrite([6766(8)])].
6862 f(x',f(f(y,x),z)) = f(x',z'). [para(41(a,1),5074(a,1,2,1,2))].
7142 f(f(x,y),f(z,x)') = f(y',f(z,x)'). [back_rewrite(1576),rewrite([6862(9)])].
7145 f(f(x,y),f(x,z)') = f(y',f(x,z)'). [back_rewrite(1165),rewrite([6862(9)])].
7482 f(f(x,y),f(y,z)) = f(y,f(x',f(y,z)))'. [para(164(a,1),153(a,1,2)),rewrite([6794(5),6808(6)]),flip(a)].
7755 f(f(x',y),f(f(y,f(x,f(y,z)))',f(u,f(x,f(y,z)')))) = f(y,f(x,f(y,z)))'. [back_rewrite(4845),rewrite([7482(6),41(4),7482(16),41(14)])].
7859 f(f(x,f(y,f(x,z))),f(f(z',x),f(f(x,f(y,f(x,z))),f(x,u))))' = f(x,f(y,f(x,z))). [back_rewrite(2838),rewrite([7482(13),41(7)])].
8136 f(x,f(y,f(x,z'))') = f(y,f(x,z)'). [para(1248(a,1),1132(a,1,2)),rewrite([4(3),1132(3),7145(10),3879(10)]),flip(a)].
8152 f(f(x,f(y,z'))',f(z,y)') = f(x,f(y,z)'). [back_rewrite(3886),rewrite([8136(12)])].
9590 f(x,f(y,f(z,x)')) = f(x,f(y,z)). [para(15(a,1),1453(a,1,2)),rewrite([7142(5),5989(5),4(4)])].
9631 f(x,f(y,f(x,z'))) = f(x,f(y,f(x,z)')). [para(526(a,1),1453(a,1,2)),rewrite([7142(7),8152(7),4(4)]),flip(a)].
9682 f(x,f(y,z)') = f(z,f(x,y)'). [back_rewrite(271),rewrite([9590(6),1136(5)]),flip(a)].
9736 f(f(x,y)',z) = f(x,f(y,z)'). [para(9682(a,2),4(a,1)),flip(a)].
9737 f(x,f(y,z)') = f(y,f(x,z)'). [para(4(a,1),9682(a,1,2,1))].
10012 f(x',f(y,f(z,f(u,x))')') = f(y,f(z,x')'). [para(9682(a,2),1362(a,2)),rewrite([9736(7),9736(5)])].
10421 f(x,f(y,f(x,f(f(y,f(x,z)),f(u,f(y,f(x,z)'))))'))' = f(x,f(y,f(x,z)))'. [back_rewrite(7755),rewrite([9736(11),7482(12),41(2),9631(11)])].
10865 f(x,f(y,f(x,z))') = f(x,f(y,z')'). [back_rewrite(4162),rewrite([10012(7)]),flip(a)].
11744 f(x,f(y,f(f(x,z),f(u,f(x,z'))))') = f(y,f(x,z)'). [para(69(a,1),9737(a,1,2,1)),flip(a)].
11843 f(x,f(y,f(x,z)))' = f(x,f(y,z'))'. [back_rewrite(10421),rewrite([11744(10),10865(4),1132(5),41(4)]),flip(a)].
12042 f(x,f(y,f(x,z))) = f(x,f(y,z')). [back_rewrite(7859),rewrite([11843(13),6758(8),41(5),4808(7),11843(4),41(5)]),flip(a)].
12297 f(f(x,y),f(x,z))' = f(x,f(y',z')). [back_rewrite(6788),rewrite([12042(8)])].
12365 f(x,f(f(x,y),z)) = f(x,f(y',z)). [back_rewrite(2337),rewrite([12042(6),5626(5)]),flip(a)].
12401 f(f(x,y),f(x,f(y',z))) = f(x,f(y',z))'. [back_rewrite(581),rewrite([12365(4),12365(8)])].
13505 f(f(x,y),f(x,z)) = f(x,f(y',z'))'. [para(507(a,1),132(a,1,2)),rewrite([12297(4),4(6),12401(6)]),flip(a)].
14077 $F # answer(Sheffer_3). [back_rewrite(13),rewrite([13505(9),41(4),41(5)]),xx(a)].
============================== end of proof ==========================
============================== STATISTICS ============================
Given=219. Generated=90082. Kept=14065. proofs=3.
Usable=67. Sos=2637. Demods=3099. Limbo=572, Disabled=10795. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=76014. Back_subsumed=427.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=13597 (1 lex), Back_demodulated=10362. Back_unit_deleted=0.
Demod_attempts=1425632. Demod_rewrites=230843.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=11.74.
User_CPU=5.54, System_CPU=0.04, Wall_clock=6.
============================== end of statistics =====================
============================== end of search =========================
THEOREM PROVED
Exiting with 3 proofs.
Process 15842 exit (max_proofs) Wed Feb 25 12:26:17 2009
|