============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13117 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:29 2006 The command was "/home/mccune/bin/prover9 -f gt.in DA.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). clauses(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 DA.in clauses(sos). (x @ y) * (z @ y) = x * z @ y. end_of_list. clauses(sos). (A @ B) @ C != D @ (F @ G) # answer(A). end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 (x * y) * z = x * y * z. [input]. 2 e * x = x. [input]. 3 x ' * x = e. [input]. 4 x @ y = x ' * y ' * x * y. [input]. 5 (x @ y) * (z @ y) = x * z @ y. [input]. 6 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). 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: clauses(usable). end_of_list. clauses(sos). 7 (x * y) * z = x * y * z. [input]. 8 e * x = x. [input]. 9 x ' * x = e. [input]. 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. 11 (x @ y) * (z @ y) = x * z @ y. [input]. 12 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. end_of_list. clauses(demodulators). 7 (x * y) * z = x * y * z. [input]. 8 e * x = x. [input]. 9 x ' * x = e. [input]. 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. 11 (x @ y) * (z @ y) = x * z @ y. [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 7 (x * y) * z = x * y * z. [input]. given #2 (I,wt=5): 8 e * x = x. [input]. given #3 (I,wt=6): 9 x ' * x = e. [input]. given #4 (I,wt=13): 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. given #5 (I,wt=13): 11 (x @ y) * (z @ y) = x * z @ y. [input]. given #6 (I,wt=11): 12 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. given #7 (F,wt=5): 16 e @ x = e. [para(8(a,1),10(a,1,2,2)),demod(9(4),9(4)),flip(a)]. given #8 (F,wt=6): 17 x ' @ x = e. [para(9(a,1),10(a,1,2,2)),demod(13(6)),flip(a)]. given #9 (T,wt=8): 13 x ' * x * y = y. [para(9(a,1),7(a,1,1)),demod(8(2)),flip(a)]. given #10 (T,wt=5): 28 x @ x = e. [para(13(a,1),10(a,1,2)),demod(9(2)),flip(a)]. given #11 (A,wt=17): 14 x ' * y ' * x * y * z = (x @ y) * z. [para(10(a,1),7(a,1,1)),demod(7(7),7(6)),flip(a)]. given #12 (F,wt=5): 34 x * e = x. [back_demod(26),demod(31(4))]. given #13 (F,wt=4): 57 e ' = e. [para(34(a,1),9(a,1))]. given #14 (T,wt=5): 58 x @ e = e. [para(34(a,1),10(a,1,2,2)),demod(57(3),8(3),9(2)),flip(a)]. given #15 (T,wt=9): 31 x ' ' * y = x * y. [para(13(a,1),13(a,1,2))]. given #16 (A,wt=19): 15 (x * y) ' * z ' * x * y * z = x * y @ z. [para(7(a,1),10(a,1,2,2))]. given #17 (F,wt=5): 67 x ' ' = x. [para(31(a,1),34(a,1)),demod(34(2)),flip(a)]. given #18 (F,wt=6): 59 x * x ' = e. [para(31(a,1),9(a,1))]. given #19 (T,wt=6): 78 x @ x ' = e. [para(67(a,1),17(a,1,1))]. given #20 (T,wt=8): 63 x * x ' * y = y. [para(31(a,1),13(a,1))]. given #21 (A,wt=17): 19 (x * y @ z) * u = (x @ z) * (y @ z) * u. [para(11(a,1),7(a,1,1))]. given #22 (F,wt=8): 77 x ' @ y = y @ x. [back_demod(69),demod(74(6))]. given #23 (F,wt=12): 103 (B ' @ A) @ C != D @ (F @ G) # answer(A). [para(77(a,2),12(a,1,1))]. given #24 (T,wt=8): 85 x @ y ' = y @ x. [para(78(a,1),11(a,1,2)),demod(34(4),83(5))]. given #25 (T,wt=9): 37 x * y @ x = y @ x. [para(28(a,1),11(a,1,1)),demod(8(3)),flip(a)]. given #26 (A,wt=23): 20 (x @ y) ' * (z @ y) ' * (x * z @ y) = (x @ y) @ (z @ y). [para(11(a,1),10(a,1,2,2))]. given #27 (F,wt=12): 104 C ' @ (A @ B) != D @ (F @ G) # answer(A). [para(77(a,2),12(a,1))]. given #28 (F,wt=12): 126 (B @ A ') @ C != D @ (F @ G) # answer(A). [para(85(a,2),12(a,1,1))]. given #29 (T,wt=9): 38 x * y @ y = x @ y. [para(28(a,1),11(a,1,2)),demod(34(3)),flip(a)]. given #30 (T,wt=9): 114 x ' @ y ' = x @ y. [para(77(a,2),77(a,1))]. given #31 (A,wt=10): 22 x ' * y @ x = y @ x. [para(17(a,1),11(a,1,1)),demod(8(3)),flip(a)]. given #32 (F,wt=12): 128 D @ (G @ F ') != (A @ B) @ C # answer(A). [para(85(a,2),12(a,2,2)),flip(a)]. given #33 (F,wt=12): 129 (F @ G) @ D ' != (A @ B) @ C # answer(A). [para(85(a,2),12(a,2)),flip(a)]. given #34 (T,wt=7): 196 (x @ y) @ x = e. [para(10(a,1),22(a,1,1)),demod(144(6),9(4),16(4))]. given #35 (T,wt=7): 211 (x @ y) @ y = e. [para(85(a,1),196(a,1,1))]. given #36 (A,wt=12): 24 (x * y) ' * x * y * z = z. [para(7(a,1),13(a,1,2))]. given #37 (F,wt=13): 137 C ' @ (B @ A ') != D @ (F @ G) # answer(A). [para(85(a,2),103(a,1)),demod(136(5),136(7,R))]. given #38 (F,wt=13): 138 D @ (G @ F ') != (B @ A ') @ C # answer(A). [para(85(a,2),103(a,2,2)),demod(136(4)),flip(a)]. given #39 (T,wt=8): 207 x ' @ (x @ y) = e. [para(196(a,1),77(a,2))]. given #40 (T,wt=7): 252 x @ (y @ x) = e. [para(77(a,1),207(a,1,2)),demod(67(2))]. given #41 (A,wt=14): 30 (x @ y) ' * (x * z @ y) = z @ y. [para(11(a,1),13(a,1,2))]. given #42 (F,wt=13): 139 (F @ G) @ D ' != (B @ A ') @ C # answer(A). [para(85(a,2),103(a,2)),demod(136(4)),flip(a)]. given #43 (F,wt=12): 310 (F @ G) @ D ' != C @ (B @ A) # answer(A). [para(85(a,2),139(a,2)),demod(272(12),114(12))]. given #44 (T,wt=7): 255 x @ (x @ y) = e. [para(114(a,1),207(a,1,2)),demod(67(2))]. given #45 (T,wt=8): 208 (x @ y) @ y ' = e. [para(77(a,1),196(a,1,1))]. given #46 (A,wt=12): 32 x ' * y * x = y * (y @ x). [back_demod(29),demod(31(4)),flip(a)]. given #47 (F,wt=11): 312 D @ (F @ G) != C @ (B @ A) # answer(A). [para(77(a,2),310(a,1)),demod(67(3))]. given #48 (F,wt=12): 351 D @ (G @ F ') != C @ (B @ A) # answer(A). [para(77(a,2),312(a,1,2)),demod(136(5))]. given #49 (T,wt=8): 210 x @ (x ' @ y) = e. [para(196(a,1),85(a,1)),flip(a)]. given #50 (T,wt=8): 212 (x @ y ') @ y = e. [para(85(a,2),196(a,1,1))]. given #51 (A,wt=10): 36 x * y ' @ y = x @ y. [back_demod(23),demod(34(5))]. given #52 (F,wt=11): 355 (G @ F) @ D != C @ (B @ A) # answer(A). [para(77(a,2),351(a,1)),demod(272(5),114(5))]. given #53 (F,wt=12): 352 (F ' @ G) @ D != C @ (B @ A) # answer(A). [para(77(a,2),312(a,1)),demod(272(4))]. given #54 (T,wt=8): 216 (x @ y) @ x ' = e. [para(114(a,1),196(a,1,1))]. given #55 (T,wt=8): 223 x ' @ (y @ x) = e. [para(211(a,1),77(a,2))]. given #56 (A,wt=21): 39 x * y ' * z ' * y * z * u = x * (y @ z) * u. [para(14(a,1),7(a,2,2)),demod(7(7))]. given #57 (F,wt=12): 353 C @ (A ' @ B) != D @ (F @ G) # answer(A). [para(77(a,2),312(a,2,2)),flip(a)]. given #58 (F,wt=12): 354 (B @ A) @ C ' != D @ (F @ G) # answer(A). [para(85(a,2),312(a,2)),flip(a)]. given #59 (T,wt=8): 224 (x ' @ y) @ x = e. [para(77(a,2),211(a,1,1))]. given #60 (T,wt=8): 225 x @ (y @ x ') = e. [para(211(a,1),85(a,1)),flip(a)]. given #61 (A,wt=23): 40 x ' * (y * z) ' * x * y * z * u = (x @ y * z) * u. [para(7(a,1),14(a,1,2,2,2))]. given #62 (F,wt=12): 377 D ' @ (G @ F) != C @ (B @ A) # answer(A). [para(77(a,2),355(a,1))]. given #63 (F,wt=12): 378 C @ (A ' @ B) != (G @ F) @ D # answer(A). [para(77(a,2),355(a,2,2)),flip(a)]. given #64 (T,wt=9): 136 x ' @ y = x @ y '. [para(85(a,1),77(a,1)),flip(a)]. given #65 (T,wt=9): 182 x @ y * x = x @ y. [para(13(a,1),38(a,1,1)),demod(151(5))]. given #66 (A,wt=25): 41 (x * y) ' * z ' * x * y * z * u = (x @ z) * (y @ z) * u. [para(7(a,1),14(a,1,2,2)),demod(19(11))]. given #67 (F,wt=11): 458 (G @ F) @ D != (A @ B) @ C # answer(A). [para(77(a,2),378(a,1)),demod(272(5),67(3)),flip(a)]. given #68 (F,wt=12): 379 (B @ A ') @ C != (G @ F) @ D # answer(A). [para(77(a,2),355(a,2)),demod(272(9),136(9)),flip(a)]. given #69 (T,wt=9): 213 (x @ y) @ y * x = e. [para(37(a,1),196(a,1,1))]. given #70 (T,wt=9): 215 (x @ y) @ x * y = e. [para(38(a,1),196(a,1,1))]. given #71 (A,wt=13): 43 x ' * y * x = (x @ y ') * y. [para(9(a,1),14(a,1,2,2,2)),demod(34(5),31(4))]. given #72 (F,wt=12): 380 (B @ A) @ C ' != (G @ F) @ D # answer(A). [para(85(a,2),355(a,2)),flip(a)]. given #73 (F,wt=12): 471 (F ' @ G) @ D != (A @ B) @ C # answer(A). [para(136(a,2),129(a,1)),demod(272(4))]. given #74 (T,wt=9): 242 (x * y) ' * x = y '. [para(59(a,1),24(a,1,2,2)),demod(34(4))]. given #75 (T,wt=9): 272 (x @ y) ' = x ' @ y. [para(59(a,1),30(a,1,2,1)),demod(16(4),34(4))]. given #76 (A,wt=12): 48 (x ' @ y) * x = x * (y @ x). [para(10(a,1),14(a,1,2)),demod(31(4)),flip(a)]. given #77 (F,wt=12): 509 D ' @ (G @ F) != (A @ B) @ C # answer(A). [para(77(a,2),458(a,1))]. given #78 (F,wt=12): 510 C ' @ (A @ B) != (G @ F) @ D # answer(A). [para(77(a,2),458(a,2)),flip(a)]. given #79 (T,wt=9): 273 (x @ y) * (y @ x) = e. [para(78(a,1),30(a,2)),demod(272(3),114(3),83(4))]. given #80 (T,wt=9): 298 (x @ y) @ (y @ x) = e. [back_demod(190),demod(272(2),272(4),102(5),9(2),16(2)),flip(a)]. given #81 (A,wt=19): 49 x ' * y ' * x * y * (z @ y) = x * z @ y. [para(14(a,2),11(a,1))]. given #82 (F,wt=13): 177 D @ (G @ F ') != C ' @ (A @ B) # answer(A). [para(77(a,2),104(a,2,2)),demod(136(11)),flip(a)]. given #83 (F,wt=13): 178 (F @ G) @ D ' != C ' @ (A @ B) # answer(A). [para(77(a,2),104(a,2)),demod(136(12)),flip(a)]. given #84 (T,wt=9): 523 x * y @ y * x = e. [para(213(a,1),37(a,2)),demod(7(3),330(3))]. given #85 (T,wt=9): 555 x @ x * y = x @ y. [back_demod(342),demod(538(4))]. given #86 (A,wt=21): 50 x ' * y ' * x * y * z @ u = (x @ y) * z @ u. [para(14(a,1),11(a,2,1)),demod(11(8))]. given #87 (F,wt=13): 204 (G @ F ') @ D ' != (A @ B) @ C # answer(A). [para(77(a,2),128(a,1)),demod(136(7))]. given #88 (F,wt=13): 311 (G @ F ') @ D ' != C @ (B @ A) # answer(A). [para(77(a,2),310(a,1,1)),demod(136(4))]. given #89 (T,wt=10): 83 x * y @ y ' = y @ x. [para(59(a,1),15(a,1,2,2,2)),demod(67(4),34(4),74(4)),flip(a)]. given #90 (T,wt=10): 151 x ' @ x * y = y @ x. [para(37(a,1),77(a,2))]. given #91 (A,wt=16): 52 x ' * y * x * z = y * (y @ x) * z. [para(14(a,1),13(a,1,2)),demod(31(5)),flip(a)]. given #92 (F,wt=13): 313 (F @ G) @ D ' != C @ (A ' @ B) # answer(A). [para(77(a,2),310(a,2,2))]. given #93 (F,wt=13): 315 (F @ G) @ D ' != (B @ A) @ C ' # answer(A). [para(85(a,2),310(a,2))]. given #94 (T,wt=10): 185 x ' @ y * x = y @ x. [para(38(a,1),77(a,2))]. given #95 (T,wt=10): 217 (x @ y) @ y ' * x = e. [para(22(a,1),196(a,1,1))]. given #96 (A,wt=17): 54 x ' * y * x * z = (x @ y ') * y * z. [para(13(a,1),14(a,1,2,2,2)),demod(31(5))]. given #97 (F,wt=13): 356 D @ (G @ F ') != C @ (A ' @ B) # answer(A). [para(77(a,2),351(a,2,2))]. given #98 (F,wt=13): 357 D @ (G @ F ') != (B @ A) @ C ' # answer(A). [para(85(a,2),351(a,2))]. given #99 (T,wt=10): 285 (x @ y) @ (x ' @ y) = e. [back_demod(158),demod(272(2),272(5),67(4),11(4),9(2),16(2)),flip(a)]. given #100 (T,wt=10): 286 (x ' @ y) @ (x @ y) = e. [back_demod(155),demod(272(3),67(2),272(3),11(4),59(2),16(2)),flip(a)]. given #101 (A,wt=16): 56 (x ' @ y) * x * z = x * (y @ x) * z. [para(14(a,1),14(a,1,2)),demod(31(5)),flip(a)]. given #102 (F,wt=13): 381 (F ' @ G) @ D != C @ (A ' @ B) # answer(A). [para(77(a,2),352(a,2,2))]. given #103 (F,wt=13): 382 (F ' @ G) @ D != (B @ A ') @ C # answer(A). [para(77(a,2),352(a,2)),demod(272(10),136(10))]. given #104 (T,wt=10): 364 (x @ y) @ (y ' @ x) = e. [para(210(a,1),37(a,2)),demod(48(3),359(5))]. given #105 (T,wt=10): 371 (x @ y) * (x @ y ') = e. [back_demod(366),demod(370(6))]. given #106 (A,wt=14): 61 x ' * y * x * y ' = x @ y '. [para(31(a,1),10(a,1,2))]. given #107 (F,wt=13): 383 (F ' @ G) @ D != (B @ A) @ C ' # answer(A). [para(85(a,2),352(a,2))]. given #108 (F,wt=13): 455 D ' @ (G @ F) != C @ (A ' @ B) # answer(A). [para(77(a,2),377(a,2,2))]. given #109 (T,wt=10): 375 (x @ y) @ x * y ' = e. [para(36(a,1),196(a,1,1))]. given #110 (T,wt=10): 388 (x ' @ y) @ y * x = e. [para(37(a,1),216(a,1,1)),demod(136(4,R),272(2))]. given #111 (A,wt=14): 62 x * y ' * x ' * y = x ' @ y. [para(31(a,1),10(a,1))]. given #112 (F,wt=13): 456 D ' @ (G @ F) != (B @ A ') @ C # answer(A). [para(77(a,2),377(a,2)),demod(272(10),136(10))]. given #113 (F,wt=13): 457 D ' @ (G @ F) != (B @ A) @ C ' # answer(A). [para(85(a,2),377(a,2))]. given #114 (T,wt=10): 389 (x ' @ y) @ x * y = e. [para(38(a,1),216(a,1,1)),demod(136(4,R),272(2))]. given #115 (T,wt=10): 427 (x @ y) @ (x @ y ') = e. [para(225(a,1),22(a,2)),demod(272(3),114(3),423(5))]. given #116 (A,wt=18): 65 x ' * y * x * y ' * z = (x @ y ') * z. [para(31(a,1),14(a,1,2))]. given #117 (F,wt=13): 511 C ' @ (B @ A ') != (G @ F) @ D # answer(A). [para(77(a,2),379(a,1))]. given #118 (F,wt=13): 593 (F ' @ G) @ D != C ' @ (A @ B) # answer(A). [para(77(a,2),471(a,2))]. given #119 (T,wt=10): 521 (x @ y) @ x ' * y = e. [para(85(a,1),213(a,1,1))]. given #120 (T,wt=10): 522 (x @ y ') @ x * y = e. [para(85(a,2),213(a,1,1))]. given #121 (A,wt=18): 66 (x ' @ y) * z = x * y ' * x ' * y * z. [para(31(a,1),14(a,1)),flip(a)]. given #122 (F,wt=13): 686 D ' @ (G @ F) != C ' @ (A @ B) # answer(A). [para(77(a,2),509(a,2))]. given #123 (F,wt=14): 246 D @ (G @ F ') != C ' @ (B @ A ') # answer(A). [para(77(a,2),137(a,2,2)),demod(136(12)),flip(a)]. given #124 (T,wt=10): 544 (x @ y) @ y * x ' = e. [para(85(a,1),215(a,1,1))]. given #125 (T,wt=10): 545 (x @ y ') @ y * x = e. [para(85(a,2),215(a,1,1))]. given #126 (A,wt=18): 72 x ' * y * z * x = y * z * (y * z @ x). [para(15(a,1),13(a,1,2)),demod(67(3),7(4)),flip(a)]. given #127 (F,wt=14): 247 (F @ G) @ D ' != C ' @ (B @ A ') # answer(A). [para(77(a,2),137(a,2)),demod(136(13)),flip(a)]. given #128 (F,wt=14): 248 (G @ F ') @ D ' != (B @ A ') @ C # answer(A). [para(77(a,2),138(a,1)),demod(136(7))]. given #129 (T,wt=10): 582 x @ y ' * x * y = e. [para(43(a,2),182(a,1,2)),demod(225(7))]. given #130 (T,wt=10): 595 (x * y) ' = y ' * x '. [para(13(a,1),242(a,1,1,1)),flip(a)]. given #131 (A,wt=14): 81 x ' * y ' * x = (x @ y) * y '. [para(59(a,1),14(a,1,2,2,2)),demod(34(4))]. given #132 (F,wt=14): 727 (G @ F ') @ D ' != C ' @ (A @ B) # answer(A). [para(85(a,2),177(a,1))]. given #133 (F,wt=14): 830 (G @ F ') @ D ' != C @ (A ' @ B) # answer(A). [para(85(a,2),204(a,2)),demod(272(12))]. given #134 (T,wt=10): 690 (x @ y ') * (x @ y) = e. [para(77(a,1),273(a,1,2))]. given #135 (T,wt=10): 695 (x ' @ y) @ (y @ x) = e. [para(298(a,1),77(a,2)),demod(272(2))]. given #136 (A,wt=11): 84 x * y @ x ' = y @ x '. [para(78(a,1),11(a,1,1)),demod(8(4)),flip(a)]. given #137 (F,wt=14): 831 (G @ F ') @ D ' != (B @ A) @ C ' # answer(A). [para(85(a,2),311(a,2))]. given #138 (F,wt=14): 1105 (F ' @ G) @ D != C ' @ (B @ A ') # answer(A). [para(77(a,2),382(a,2))]. given #139 (T,wt=10): 696 (x @ y ') @ (x @ y) = e. [para(77(a,1),298(a,1,2))]. given #140 (T,wt=10): 731 (x @ y) @ (y @ x ') = e. [para(10(a,1),523(a,1,1)),demod(7(6),7(5),61(6))]. given #141 (A,wt=18): 87 x ' * y ' * x * z = (x @ y) * y ' * z. [para(63(a,1),14(a,1,2,2,2))]. ============================== PROOF ================================= % Proof 1 at 0.20 (+ 0.00) seconds: A. % Length of proof is 63. % Level of proof is 17. % Maximum clause weight is 25. % Given clauses 141. 4 x @ y = x ' * y ' * x * y. [input]. 7 (x * y) * z = x * y * z. [input]. 8 e * x = x. [input]. 9 x ' * x = e. [input]. 10 x ' * y ' * x * y = x @ y. [copy(4),flip(a)]. 11 (x @ y) * (z @ y) = x * z @ y. [input]. 12 (A @ B) @ C != D @ (F @ G) # answer(A). [input]. 13 x ' * x * y = y. [para(9(a,1),7(a,1,1)),demod(8(2)),flip(a)]. 14 x ' * y ' * x * y * z = (x @ y) * z. [para(10(a,1),7(a,1,1)),demod(7(7),7(6)),flip(a)]. 15 (x * y) ' * z ' * x * y * z = x * y @ z. [para(7(a,1),10(a,1,2,2))]. 16 e @ x = e. [para(8(a,1),10(a,1,2,2)),demod(9(4),9(4)),flip(a)]. 17 x ' @ x = e. [para(9(a,1),10(a,1,2,2)),demod(13(6)),flip(a)]. 19 (x * y @ z) * u = (x @ z) * (y @ z) * u. [para(11(a,1),7(a,1,1))]. 21 (x @ y) * e = x * e @ y. [para(16(a,1),11(a,1,2))]. 22 x ' * y @ x = y @ x. [para(17(a,1),11(a,1,1)),demod(8(3)),flip(a)]. 23 x * y ' @ y = x * e @ y. [para(17(a,1),11(a,1,2)),demod(21(3)),flip(a)]. 24 (x * y) ' * x * y * z = z. [para(7(a,1),13(a,1,2))]. 26 x ' ' * e = x. [para(9(a,1),13(a,1,2))]. 28 x @ x = e. [para(13(a,1),10(a,1,2)),demod(9(2)),flip(a)]. 29 x ' ' * (x @ y) = y ' * x * y. [para(10(a,1),13(a,1,2))]. 30 (x @ y) ' * (x * z @ y) = z @ y. [para(11(a,1),13(a,1,2))]. 31 x ' ' * y = x * y. [para(13(a,1),13(a,1,2))]. 32 x ' * y * x = y * (y @ x). [back_demod(29),demod(31(4)),flip(a)]. 34 x * e = x. [back_demod(26),demod(31(4))]. 36 x * y ' @ y = x @ y. [back_demod(23),demod(34(5))]. 37 x * y @ x = y @ x. [para(28(a,1),11(a,1,1)),demod(8(3)),flip(a)]. 59 x * x ' = e. [para(31(a,1),9(a,1))]. 63 x * x ' * y = y. [para(31(a,1),13(a,1))]. 67 x ' ' = x. [para(31(a,1),34(a,1)),demod(34(2)),flip(a)]. 69 (x * y ') ' * y ' * x = x @ y. [para(9(a,1),15(a,1,2,2,2)),demod(34(6),36(9))]. 72 x ' * y * z * x = y * z * (y * z @ x). [para(15(a,1),13(a,1,2)),demod(67(3),7(4)),flip(a)]. 74 (x * y) ' * y * x = y @ x. [para(13(a,1),15(a,1,2)),demod(37(6))]. 77 x ' @ y = y @ x. [back_demod(69),demod(74(6))]. 78 x @ x ' = e. [para(67(a,1),17(a,1,1))]. 83 x * y @ y ' = y @ x. [para(59(a,1),15(a,1,2,2,2)),demod(67(4),34(4),74(4)),flip(a)]. 85 x @ y ' = y @ x. [para(78(a,1),11(a,1,2)),demod(34(4),83(5))]. 87 x ' * y ' * x * z = (x @ y) * y ' * z. [para(63(a,1),14(a,1,2,2,2))]. 103 (B ' @ A) @ C != D @ (F @ G) # answer(A). [para(77(a,2),12(a,1,1))]. 114 x ' @ y ' = x @ y. [para(77(a,2),77(a,1))]. 136 x ' @ y = x @ y '. [para(85(a,1),77(a,1)),flip(a)]. 139 (F @ G) @ D ' != (B @ A ') @ C # answer(A). [para(85(a,2),103(a,2)),demod(136(4)),flip(a)]. 144 x * y * z @ y = x * z @ y. [para(37(a,1),11(a,1,2)),demod(11(3)),flip(a)]. 196 (x @ y) @ x = e. [para(10(a,1),22(a,1,1)),demod(144(6),9(4),16(4))]. 207 x ' @ (x @ y) = e. [para(196(a,1),77(a,2))]. 242 (x * y) ' * x = y '. [para(59(a,1),24(a,1,2,2)),demod(34(4))]. 255 x @ (x @ y) = e. [para(114(a,1),207(a,1,2)),demod(67(2))]. 272 (x @ y) ' = x ' @ y. [para(59(a,1),30(a,1,2,1)),demod(16(4),34(4))]. 310 (F @ G) @ D ' != C @ (B @ A) # answer(A). [para(85(a,2),139(a,2)),demod(272(12),114(12))]. 312 D @ (F @ G) != C @ (B @ A) # answer(A). [para(77(a,2),310(a,1)),demod(67(3))]. 318 x * y @ (y @ z) = x @ (y @ z). [para(255(a,1),11(a,1,2)),demod(34(4)),flip(a)]. 336 (x * y) ' * (y ' @ z) * x * z ' * y * z = x @ (y @ z). [para(32(a,2),15(a,1,2,2,2)),demod(272(4),318(13))]. 351 D @ (G @ F ') != C @ (B @ A) # answer(A). [para(77(a,2),312(a,1,2)),demod(136(5))]. 355 (G @ F) @ D != C @ (B @ A) # answer(A). [para(77(a,2),351(a,1)),demod(272(5),114(5))]. 377 D ' @ (G @ F) != C @ (B @ A) # answer(A). [para(77(a,2),355(a,1))]. 456 D ' @ (G @ F) != (B @ A ') @ C # answer(A). [para(77(a,2),377(a,2)),demod(272(10),136(10))]. 595 (x * y) ' = y ' * x '. [para(13(a,1),242(a,1,1,1)),flip(a)]. 635 x ' * y ' * (x ' @ z) * y * z ' * x * z = y @ (x @ z). [back_demod(336),demod(595(2),7(11))]. 1188 D ' @ (G @ F) != C ' @ (B @ A ') # answer(A). [para(77(a,2),456(a,2))]. 1437 (x ' @ y) * (z ' @ y) * y ' * z * x * y = z * x. [para(72(a,2),72(a,1,2)),demod(272(3),595(2),19(9),255(14),34(12))]. 1581 (x ' @ y) * y ' * x * z = x * y ' * z. [para(13(a,1),87(a,1,2,2)),demod(67(2)),flip(a)]. 1641 (x ' @ y) * z * y ' * x * y = z * x. [back_demod(1437),demod(1581(9))]. 1643 x @ (y @ z) = e. [back_demod(635),demod(1641(9),13(4),9(2)),flip(a)]. 1670 $F # answer(A). [back_demod(1188),demod(1643(6),1643(8)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=141. Generated=9271. Kept=1663. proofs=1. Usable=115. Sos=991. Demods=687. Denials=0. Limbo=27, Disabled=536. Hints=0. Weight_deleted=1128. Literals_deleted=0. Forward_subsumed=6479. Back_subsumed=113. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1106 (2 lex), Back_demodulated=417. Back_unit_deleted=0. Demod_attempts=129429. Demod_rewrites=23070. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.27. User_CPU=0.20, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13117 exit (max_proofs) Mon Jun 19 16:41:29 2006