============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11358 was started by mccune on cleo.thornwood, Sat Aug 12 20:59:57 2006 The command was "/home/mccune/bin/prover9 -f gt.in EA.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file gt.in op(450,infix,@). op(400,infix_right,*). assign(eq_defs,fold). assign(max_weight,25). formulas(sos). (x * y) * z = x * y * z. e * x = x. x' * x = e. x @ y = x' * y' * x * y. end_of_list. % Reading from file EA.in formulas(sos). x * y * z * y * x = y * x * z * x * y. end_of_list. formulas(sos). (A @ B) @ C != D @ (F @ G) # answer(A). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). (x * y) * z = x * y * z. [assumption]. e * x = x. [assumption]. x' * x = e. [assumption]. x @ y = x' * y' * x * y. [assumption]. x * y * z * y * x = y * x * z * x * y. [assumption]. (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ e, A, B, C, D, F, G, *, @, ' ]). After inverse_order: Function symbol precedence: lex([ e, A, B, C, D, F, G, *, ', @ ]). Folding symbols: @/2. After fold_eq: Function symbol precedence: lex([ e, A, B, C, D, F, G, @, *, ' ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 (x * y) * z = x * y * z. [assumption]. 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. 6 x * y * z * y * x = y * x * z * x * y. [assumption]. 7 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. end_of_list. formulas(demodulators). 1 (x * y) * z = x * y * z. [assumption]. 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 1 (x * y) * z = x * y * z. [assumption]. given #2 (I,wt=5): 2 e * x = x. [assumption]. given #3 (I,wt=6): 3 x' * x = e. [assumption]. given #4 (I,wt=13): 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. given #5 (I,wt=19): 6 x * y * z * y * x = y * x * z * x * y. [assumption]. given #6 (I,wt=11): 7 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. given #7 (F,wt=5): 11 e @ x = e. [para(2(a,1),5(a,1,2,2)),rewrite(3(4),3(4)),flip(a)]. given #8 (F,wt=6): 12 x' @ x = e. [para(3(a,1),5(a,1,2,2)),rewrite(8(6)),flip(a)]. given #9 (T,wt=8): 8 x' * x * y = y. [para(3(a,1),1(a,1,1)),rewrite(2(2)),flip(a)]. given #10 (T,wt=5): 26 x @ x = e. [para(8(a,1),5(a,1,2)),rewrite(3(2)),flip(a)]. given #11 (A,wt=17): 9 x' * y' * x * y * z = (x @ y) * z. [para(5(a,1),1(a,1,1)),rewrite(1(7),1(6)),flip(a)]. given #12 (F,wt=5): 35 x * e = x. [back_rewrite(24),rewrite(32(4))]. given #13 (F,wt=4): 56 e' = e. [para(35(a,1),3(a,1))]. given #14 (T,wt=5): 57 x @ e = e. [para(35(a,1),5(a,1,2,2)),rewrite(56(3),2(3),3(2)),flip(a)]. given #15 (T,wt=9): 32 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. given #16 (A,wt=19): 10 (x * y)' * z' * x * y * z = x * y @ z. [para(1(a,1),5(a,1,2,2))]. given #17 (F,wt=5): 67 x'' = x. [para(32(a,1),35(a,1)),rewrite(35(2)),flip(a)]. given #18 (F,wt=6): 58 x * x' = e. [para(32(a,1),3(a,1))]. given #19 (T,wt=6): 81 x @ x' = e. [para(67(a,1),12(a,1,1))]. given #20 (T,wt=7): 78 x * x @ x = e. [para(10(a,1),10(a,1,2)),rewrite(3(2),56(2),2(4),3(4),11(5))]. given #21 (A,wt=23): 14 x * y * z * y * x * u = y * x * z * x * y * u. [para(6(a,1),1(a,1,1)),rewrite(1(5),1(4),1(3),1(2),1(9),1(8),1(7))]. given #22 (F,wt=8): 63 x * x' * y = y. [para(32(a,1),8(a,1))]. given #23 (F,wt=10): 83 x * y * (x * y)' = e. [para(58(a,1),1(a,1)),flip(a)]. given #24 (T,wt=9): 117 x * (y * x)' = y'. [para(83(a,1),8(a,1,2)),rewrite(35(3)),flip(a)]. given #25 (T,wt=8): 131 (x @ y)' = y @ x. [para(9(a,2),117(a,1,2,1)),rewrite(130(7),130(5),130(3),130(2),1(5),67(7),1(6),1(5),67(8),1(7),1(6),1(5),5(6),63(4)),flip(a)]. given #26 (A,wt=23): 15 x * y * z * u * z * y = x * z * y * u * y * z. [para(6(a,1),1(a,2,2)),rewrite(1(5))]. given #27 (F,wt=9): 140 (x @ y) * (y @ x) = e. [back_rewrite(119),rewrite(130(8),130(6),130(4),130(3),1(6),67(8),1(7),1(6),67(9),1(8),1(7),1(6),5(7),63(5))]. given #28 (F,wt=9): 146 x * y @ x = y @ x. [back_rewrite(74),rewrite(130(2),1(5),5(5)),flip(a)]. given #29 (T,wt=9): 168 (x @ y) @ (y @ x) = e. [para(131(a,1),12(a,1,1))]. given #30 (T,wt=9): 186 x @ x * y = x @ y. [para(146(a,1),131(a,1,1)),rewrite(131(2)),flip(a)]. given #31 (A,wt=23): 16 x * y * z * u * y * x = y * x * z * u * x * y. [para(1(a,1),6(a,1,2,2)),rewrite(1(8))]. given #32 (F,wt=10): 130 (x * y)' = y' * x'. [para(117(a,1),8(a,1,2)),flip(a)]. given #33 (F,wt=10): 159 x * y @ y' = y @ x. [back_rewrite(86),rewrite(146(5))]. given #34 (T,wt=10): 185 x' * y @ x = y @ x. [para(63(a,1),146(a,1,1)),flip(a)]. given #35 (T,wt=10): 194 x @ x' * y = x @ y. [para(63(a,1),186(a,1,2)),flip(a)]. given #36 (A,wt=15): 18 x * y * y * x = y * x * x * y. [para(2(a,1),6(a,1,2,2)),rewrite(2(6))]. given #37 (F,wt=10): 219 x' @ y * x = y @ x. [para(159(a,1),131(a,1,1)),rewrite(131(2)),flip(a)]. given #38 (F,wt=11): 153 x' @ x * y = x' @ y. [back_rewrite(34),rewrite(130(2),1(4),61(5)),flip(a)]. given #39 (T,wt=11): 160 x * y * (y @ x) = y * x. [back_rewrite(80),rewrite(146(2))]. given #40 (T,wt=11): 161 x * y' @ y = y' @ x. [back_rewrite(79),rewrite(146(6))]. given #41 (A,wt=21): 28 x * y * x' * z * y = y * z * x * y * x'. [para(8(a,1),6(a,1,2,2,2)),rewrite(1(5),1(10),1(12),8(13))]. given #42 (F,wt=11): 169 (x @ y) * (y @ x) * z = z. [para(131(a,1),8(a,1,1))]. given #43 (F,wt=11): 181 x * y @ x' = y @ x'. [para(8(a,1),146(a,1,1)),flip(a)]. given #44 (T,wt=11): 214 x' * y' @ y * x = e. [para(130(a,1),12(a,1,1))]. given #45 (T,wt=11): 215 x * y @ y' * x' = e. [para(130(a,1),81(a,1,2))]. given #46 (A,wt=16): 29 x * y * x' * y * x = y * x * y. [para(8(a,1),6(a,1,2,2)),flip(a)]. given #47 (F,wt=11): 240 (x @ y) * y * x = x * y. [para(18(a,1),9(a,1,2,2)),rewrite(8(6),8(4)),flip(a)]. given #48 (F,wt=9): 357 (x @ y) @ y * x = e. [para(240(a,1),5(a,1,2,2)),rewrite(131(2),130(3),1(6),5(6),140(3)),flip(a)]. given #49 (T,wt=7): 397 (x @ y) @ x = e. [para(63(a,1),357(a,1,2)),rewrite(185(3))]. given #50 (T,wt=7): 415 x @ (x @ y) = e. [para(397(a,1),131(a,1,1)),rewrite(56(2)),flip(a)]. given #51 (A,wt=18): 30 x' * y * x * y * x' = y * x' * y. [para(8(a,1),6(a,1,2)),flip(a)]. given #52 (F,wt=8): 417 (x @ y) @ y' = e. [para(219(a,1),397(a,1,1))]. given #53 (F,wt=8): 432 (x @ y) @ x' = e. [para(415(a,1),159(a,2)),rewrite(418(2),181(4))]. given #54 (T,wt=7): 476 (x @ y) @ y = e. [para(219(a,1),432(a,1,1)),rewrite(67(3))]. given #55 (T,wt=7): 484 x @ (y @ x) = e. [para(476(a,1),131(a,1,1)),rewrite(56(2)),flip(a)]. given #56 (A,wt=20): 31 x' * y * x * z * x * y = y * z * y * x. [para(6(a,1),8(a,1,2))]. given #57 (F,wt=8): 434 x' @ (y @ x) = e. [para(219(a,1),415(a,1,2))]. given #58 (F,wt=8): 435 (x' @ y) @ x = e. [para(415(a,1),161(a,2)),rewrite(418(4),185(5))]. given #59 (T,wt=8): 464 (x @ y') @ y = e. [para(67(a,1),417(a,1,2))]. given #60 (T,wt=8): 471 x' @ (x @ y) = e. [para(432(a,1),131(a,1,1)),rewrite(56(2)),flip(a)]. given #61 (A,wt=12): 33 x' * y * x = y * (y @ x). [back_rewrite(27),rewrite(32(4)),flip(a)]. given #62 (F,wt=8): 479 x @ y' = y @ x. [back_rewrite(359),rewrite(471(3),2(4))]. given #63 (F,wt=11): 577 D @ (F @ G) != C @ (B @ A) # answer(A). [para(479(a,2),7(a,1)),rewrite(131(5)),flip(a)]. given #64 (T,wt=8): 492 x @ (x' @ y) = e. [para(161(a,1),484(a,1,2))]. given #65 (T,wt=8): 517 x @ (y @ x') = e. [para(67(a,1),434(a,1,1))]. given #66 (A,wt=21): 39 x * y' * z' * y * z * u = x * (y @ z) * u. [para(9(a,1),1(a,2,2)),rewrite(1(7))]. given #67 (F,wt=12): 601 (F @ G) @ D' != C @ (B @ A) # answer(A). [back_rewrite(579),rewrite(582(11))]. given #68 (F,wt=12): 602 D @ (G @ F') != C @ (B @ A) # answer(A). [back_rewrite(578),rewrite(582(11))]. given #69 (T,wt=8): 574 x' @ y = y @ x. [para(435(a,1),33(a,2,2)),rewrite(48(4),8(4),35(5)),flip(a)]. given #70 (T,wt=9): 369 (x @ y) @ x * y = e. [para(240(a,1),186(a,1,2)),rewrite(357(6))]. given #71 (A,wt=22): 46 x' * y * x * (y @ z) = (x @ y') * z' * y * z. [para(5(a,1),9(a,1,2,2,2)),rewrite(32(6))]. given #72 (F,wt=12): 603 C @ (A' @ B) != D @ (F @ G) # answer(A). [back_rewrite(576),rewrite(582(6))]. given #73 (F,wt=12): 614 (B @ A) @ C' != D @ (F @ G) # answer(A). [para(479(a,2),577(a,2)),flip(a)]. given #74 (T,wt=9): 400 x * y @ y * x = e. [para(357(a,1),146(a,2)),rewrite(1(3),160(3))]. given #75 (T,wt=9): 425 x @ y * x = x @ y. [back_rewrite(162),rewrite(418(3),8(4)),flip(a)]. given #76 (A,wt=12): 48 (x' @ y) * x = x * (y @ x). [para(5(a,1),9(a,1,2)),rewrite(32(4)),flip(a)]. given #77 (F,wt=13): 653 D' @ (F' @ G) != C @ (B @ A) # answer(A). [para(479(a,2),601(a,1,1)),rewrite(582(7))]. given #78 (F,wt=13): 654 (F @ G) @ D' != C @ (A' @ B) # answer(A). [para(479(a,2),601(a,2,2)),rewrite(593(11,R))]. given #79 (T,wt=9): 585 x' @ y' = x @ y. [para(479(a,2),146(a,1)),rewrite(130(2),253(4))]. given #80 (T,wt=9): 591 x * y @ y = x @ y. [para(479(a,2),219(a,1)),rewrite(67(3))]. given #81 (A,wt=15): 49 (x @ y) * z * y * x = z * x * y. [para(6(a,1),9(a,1,2,2)),rewrite(8(7),8(5)),flip(a)]. given #82 (F,wt=13): 655 (F @ G) @ D' != (B @ A) @ C' # answer(A). [para(479(a,2),601(a,2))]. given #83 (F,wt=13): 656 D @ (G @ F') != C @ (A' @ B) # answer(A). [para(479(a,2),602(a,2,2)),rewrite(593(11,R))]. given #84 (T,wt=9): 593 x' @ y = x @ y'. [para(479(a,2),161(a,1)),rewrite(130(3),67(2),186(3)),flip(a)]. given #85 (T,wt=10): 410 x' * y * x @ y = e. [back_rewrite(223),rewrite(397(6))]. given #86 (A,wt=13): 50 x' * y = (y @ x) * y * x'. [para(6(a,1),9(a,1,2)),rewrite(8(6),8(5))]. given #87 (F,wt=13): 657 D @ (G @ F') != (B @ A) @ C' # answer(A). [para(479(a,2),602(a,2))]. given #88 (F,wt=13): 723 (A' @ B) @ C' != D @ (F @ G) # answer(A). [para(479(a,2),603(a,1))]. given #89 (T,wt=10): 416 (x @ y) @ y' * x = e. [para(185(a,1),397(a,1,1))]. given #90 (T,wt=10): 419 (x @ y') @ y * x = e. [para(181(a,1),397(a,1,1))]. given #91 (A,wt=16): 51 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite(32(5)),flip(a)]. given #92 (F,wt=14): 806 D' @ (F' @ G) != C @ (A' @ B) # answer(A). [para(479(a,2),653(a,2,2)),rewrite(593(12,R))]. given #93 (F,wt=14): 807 D' @ (F' @ G) != (B @ A) @ C' # answer(A). [para(479(a,2),653(a,2))]. given #94 (T,wt=10): 420 x @ y' * x * y = e. [back_rewrite(228),rewrite(415(6))]. given #95 (T,wt=10): 436 x * y @ (y @ x') = e. [para(181(a,1),415(a,1,2))]. given #96 (A,wt=17): 53 x' * y * x * z = (x @ y') * y * z. [para(8(a,1),9(a,1,2,2,2)),rewrite(32(5))]. given #97 (F,wt=14): 808 (F @ G) @ D' != (A' @ B) @ C' # answer(A). [para(479(a,2),654(a,2))]. given #98 (F,wt=14): 921 D @ (G @ F') != (A' @ B) @ C' # answer(A). [para(479(a,2),656(a,2))]. given #99 (T,wt=10): 469 (x @ y) * (x @ y') = e. [para(432(a,1),5(a,2)),rewrite(131(2),67(3),388(5))]. given #100 (T,wt=10): 475 (x @ y) @ x' * y = e. [para(185(a,1),432(a,1,1)),rewrite(130(4),67(4))]. given #101 (A,wt=16): 55 (x' @ y) * x * z = x * (y @ x) * z. [para(9(a,1),9(a,1,2)),rewrite(32(5)),flip(a)]. given #102 (F,wt=15): 1173 D' @ (F' @ G) != (A' @ B) @ C' # answer(A). [para(479(a,2),806(a,2))]. given #103 (F,wt=10): 485 (x' @ y) @ x * y = e. [para(153(a,1),476(a,1,1))]. given #104 (T,wt=10): 491 x * y @ (x' @ y) = e. [para(153(a,1),484(a,1,2))]. given #105 (T,wt=10): 521 (x @ y') * (x @ y) = e. [para(435(a,1),5(a,2)),rewrite(131(3),48(6),8(6))]. given #106 (A,wt=14): 60 x' * y * x * y' = x @ y'. [para(32(a,1),5(a,1,2))]. given #107 (F,wt=10): 583 (x @ y) * (x' @ y) = e. [para(479(a,1),140(a,1,1))]. given #108 (F,wt=10): 584 (x' @ y) * (x @ y) = e. [para(479(a,1),140(a,1,2))]. given #109 (T,wt=10): 586 (x @ y) @ (x' @ y) = e. [para(479(a,1),168(a,1,1))]. given #110 (T,wt=10): 587 (x @ y) @ (y @ x') = e. [para(479(a,1),168(a,1,2)),rewrite(582(4))]. given #111 (A,wt=14): 61 x * y' * x' * y = x' @ y. [para(32(a,1),5(a,1))]. given #112 (F,wt=10): 588 (x @ y) @ (y' @ x) = e. [para(479(a,2),168(a,1,1)),rewrite(582(4))]. given #113 (F,wt=10): 589 (x @ y) @ (x @ y') = e. [para(479(a,2),168(a,1,2))]. given #114 (T,wt=10): 600 (x @ y') @ x * y = e. [para(479(a,2),357(a,1,1))]. given #115 (T,wt=10): 663 (x @ y) @ x * y' = e. [para(574(a,1),357(a,1,1))]. given #116 (A,wt=18): 65 x' * y * x * y' * z = (x @ y') * z. [para(32(a,1),9(a,1,2))]. given #117 (F,wt=10): 687 (x @ y) @ y * x' = e. [para(479(a,1),369(a,1,1))]. given #118 (F,wt=10): 690 (x' @ y) @ y * x = e. [para(574(a,2),369(a,1,1))]. given #119 (T,wt=10): 728 x @ y * x * y' = e. [para(8(a,1),400(a,1,1)),rewrite(1(3))]. given #120 (T,wt=10): 729 x * y * x' @ y = e. [para(8(a,1),400(a,1,2)),rewrite(1(3))]. given #121 (A,wt=18): 66 (x' @ y) * z = x * y' * x' * y * z. [para(32(a,1),9(a,1)),flip(a)]. given #122 (F,wt=10): 1202 x * y @ (x @ y') = e. [para(436(a,1),185(a,2)),rewrite(131(3),662(4))]. given #123 (F,wt=10): 1215 x * y @ (y' @ x) = e. [para(593(a,2),436(a,1,2))]. given #124 (T,wt=11): 253 x @ y * x' = y @ x'. [para(67(a,1),219(a,1,1))]. given #125 (T,wt=11): 321 x * y' @ y * x' = e. [para(67(a,1),214(a,1,1,1))]. given #126 (A,wt=18): 72 x' * y * z * x = y * z * (y * z @ x). [para(10(a,1),6(a,1,2,2)),rewrite(1(7),1(6),63(5),1(13),1(12),58(11),35(11),3(11),35(9)),flip(a)]. given #127 (F,wt=11): 322 x' * y @ y' * x = e. [para(67(a,1),214(a,1,1,2))]. given #128 (F,wt=11): 376 x' * y' @ x * y = e. [para(240(a,1),219(a,1,2)),rewrite(130(2),357(8))]. given #129 (T,wt=11): 411 x * y @ x' * y' = e. [back_rewrite(373),rewrite(398(3)),flip(a)]. given #130 (T,wt=11): 418 (x @ y) * x = x * (x @ y). [para(397(a,1),160(a,1,2,2)),rewrite(35(3)),flip(a)]. given #131 (A,wt=21): 77 x' * y' * x * y * z @ u = (x @ y) * z @ u. [para(9(a,2),10(a,2,1)),rewrite(10(9)),flip(a)]. given #132 (F,wt=9): 2104 (x @ (y @ z)) * y = y. [para(418(a,1),9(a,1,2,2,2)),rewrite(131(3),895(6),8(3)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.32 (+ 0.01) seconds: A. % Length of proof is 69. % Level of proof is 19. % Maximum clause weight is 20. % Given clauses 132. 1 (x * y) * z = x * y * z. [assumption]. 2 e * x = x. [assumption]. 3 x' * x = e. [assumption]. 4 x @ y = x' * y' * x * y. [assumption]. 5 x' * y' * x * y = x @ y. [copy(4),flip(a)]. 6 x * y * z * y * x = y * x * z * x * y. [assumption]. 7 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. 8 x' * x * y = y. [para(3(a,1),1(a,1,1)),rewrite(2(2)),flip(a)]. 9 x' * y' * x * y * z = (x @ y) * z. [para(5(a,1),1(a,1,1)),rewrite(1(7),1(6)),flip(a)]. 10 (x * y)' * z' * x * y * z = x * y @ z. [para(1(a,1),5(a,1,2,2))]. 12 x' @ x = e. [para(3(a,1),5(a,1,2,2)),rewrite(8(6)),flip(a)]. 18 x * y * y * x = y * x * x * y. [para(2(a,1),6(a,1,2,2)),rewrite(2(6))]. 20 x * y * (x * y)' * y * x = y * x * e. [para(3(a,1),6(a,1,2,2)),flip(a)]. 24 x'' * e = x. [para(3(a,1),8(a,1,2))]. 27 x'' * (x @ y) = y' * x * y. [para(5(a,1),8(a,1,2))]. 32 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. 33 x' * y * x = y * (y @ x). [back_rewrite(27),rewrite(32(4)),flip(a)]. 35 x * e = x. [back_rewrite(24),rewrite(32(4))]. 37 x * y * (x * y)' * y * x = y * x. [back_rewrite(20),rewrite(35(8))]. 49 (x @ y) * z * y * x = z * x * y. [para(6(a,1),9(a,1,2,2)),rewrite(8(7),8(5)),flip(a)]. 56 e' = e. [para(35(a,1),3(a,1))]. 57 x @ e = e. [para(35(a,1),5(a,1,2,2)),rewrite(56(3),2(3),3(2)),flip(a)]. 58 x * x' = e. [para(32(a,1),3(a,1))]. 60 x' * y * x * y' = x @ y'. [para(32(a,1),5(a,1,2))]. 63 x * x' * y = y. [para(32(a,1),8(a,1))]. 67 x'' = x. [para(32(a,1),35(a,1)),rewrite(35(2)),flip(a)]. 69 (x * y')' * y' * x = x * y' @ y. [para(3(a,1),10(a,1,2,2,2)),rewrite(35(6))]. 74 (x * y)' * y * x = x * y @ x. [para(8(a,1),10(a,1,2))]. 79 x * y' @ y = x * y' @ x. [back_rewrite(69),rewrite(74(6)),flip(a)]. 80 x * y * (x * y @ x) = y * x. [back_rewrite(37),rewrite(74(4))]. 81 x @ x' = e. [para(67(a,1),12(a,1,1))]. 83 x * y * (x * y)' = e. [para(58(a,1),1(a,1)),flip(a)]. 86 x * y @ y' = x * y @ x. [para(58(a,1),10(a,1,2,2,2)),rewrite(67(4),35(4),74(4)),flip(a)]. 117 x * (y * x)' = y'. [para(83(a,1),8(a,1,2)),rewrite(35(3)),flip(a)]. 119 (x @ y) * z * (x' * y' * x * y * z)' = e. [para(9(a,2),83(a,1,2,2,1))]. 130 (x * y)' = y' * x'. [para(117(a,1),8(a,1,2)),flip(a)]. 131 (x @ y)' = y @ x. [para(9(a,2),117(a,1,2,1)),rewrite(130(7),130(5),130(3),130(2),1(5),67(7),1(6),1(5),67(8),1(7),1(6),1(5),5(6),63(4)),flip(a)]. 140 (x @ y) * (y @ x) = e. [back_rewrite(119),rewrite(130(8),130(6),130(4),130(3),1(6),67(8),1(7),1(6),67(9),1(8),1(7),1(6),5(7),63(5))]. 146 x * y @ x = y @ x. [back_rewrite(74),rewrite(130(2),1(5),5(5)),flip(a)]. 159 x * y @ y' = y @ x. [back_rewrite(86),rewrite(146(5))]. 160 x * y * (y @ x) = y * x. [back_rewrite(80),rewrite(146(2))]. 161 x * y' @ y = y' @ x. [back_rewrite(79),rewrite(146(6))]. 181 x * y @ x' = y @ x'. [para(8(a,1),146(a,1,1)),flip(a)]. 185 x' * y @ x = y @ x. [para(63(a,1),146(a,1,1)),flip(a)]. 186 x @ x * y = x @ y. [para(146(a,1),131(a,1,1)),rewrite(131(2)),flip(a)]. 189 x' @ y' * x * y = x' @ (x @ y). [para(5(a,1),186(a,1,2)),flip(a)]. 219 x' @ y * x = y @ x. [para(159(a,1),131(a,1,1)),rewrite(131(2)),flip(a)]. 240 (x @ y) * y * x = x * y. [para(18(a,1),9(a,1,2,2)),rewrite(8(6),8(4)),flip(a)]. 357 (x @ y) @ y * x = e. [para(240(a,1),5(a,1,2,2)),rewrite(131(2),130(3),1(6),5(6),140(3)),flip(a)]. 359 (x' @ (x @ y)) * (y @ x') = x @ y. [para(5(a,1),240(a,2)),rewrite(189(5),1(8),1(7),60(8))]. 397 (x @ y) @ x = e. [para(63(a,1),357(a,1,2)),rewrite(185(3))]. 415 x @ (x @ y) = e. [para(397(a,1),131(a,1,1)),rewrite(56(2)),flip(a)]. 418 (x @ y) * x = x * (x @ y). [para(397(a,1),160(a,1,2,2)),rewrite(35(3)),flip(a)]. 432 (x @ y) @ x' = e. [para(415(a,1),159(a,2)),rewrite(418(2),181(4))]. 471 x' @ (x @ y) = e. [para(432(a,1),131(a,1,1)),rewrite(56(2)),flip(a)]. 479 x @ y' = y @ x. [back_rewrite(359),rewrite(471(3),2(4))]. 579 (F @ G) @ D' != (A @ B) @ C # answer(A). [para(479(a,2),7(a,2)),flip(a)]. 582 (x @ y) @ z = z @ (y @ x). [para(131(a,1),479(a,1,2)),flip(a)]. 593 x' @ y = x @ y'. [para(479(a,2),161(a,1)),rewrite(130(3),67(2),186(3)),flip(a)]. 601 (F @ G) @ D' != C @ (B @ A) # answer(A). [back_rewrite(579),rewrite(582(11))]. 653 D' @ (F' @ G) != C @ (B @ A) # answer(A). [para(479(a,2),601(a,1,1)),rewrite(582(7))]. 806 D' @ (F' @ G) != C @ (A' @ B) # answer(A). [para(479(a,2),653(a,2,2)),rewrite(593(12,R))]. 895 (x @ y) * z * y * (y @ x) = z * y. [para(33(a,1),49(a,1,2,2)),rewrite(159(3),1(8),58(7),35(7))]. 1173 D' @ (F' @ G) != (A' @ B) @ C' # answer(A). [para(479(a,2),806(a,2))]. 2104 (x @ (y @ z)) * y = y. [para(418(a,1),9(a,1,2,2,2)),rewrite(131(3),895(6),8(3)),flip(a)]. 2237 x @ ((x @ y) @ z) = (x @ y) @ z. [para(2104(a,1),5(a,1,2,2)),rewrite(131(3),3(4),35(4),582(5)),flip(a)]. 2247 (x @ y) @ z = e. [para(2104(a,1),219(a,1,2)),rewrite(593(2),81(2),582(4),2237(4)),flip(a)]. 2256 x @ (y @ z) = e. [para(2104(a,1),33(a,1,2)),rewrite(3(2),582(6),2247(5),57(5),35(5)),flip(a)]. 2284 $F # answer(A). [back_rewrite(1173),rewrite(2256(7),2247(8)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=132. Generated=13787. Kept=2282. proofs=1. Usable=100. Sos=1333. Demods=822. Limbo=37, Disabled=818. Hints=0. Weight_deleted=2878. Literals_deleted=0. Forward_subsumed=8626. Back_subsumed=359. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1481 (2 lex), Back_demodulated=453. Back_unit_deleted=0. Demod_attempts=217155. Demod_rewrites=40517. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.87. User_CPU=0.32, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11358 exit (max_proofs) Sat Aug 12 20:59:57 2006