============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 12993 was started by mccune on cleo.thornwood, Mon Jun 19 16:39:58 2006 The command was "/home/mccune/bin/prover9 -f gtsax.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file gtsax.in clauses(sos). x * (y * (((z * z ') * (u * y) ') * x)) ' = u. end_of_list. clauses(sos). (A * B) * C != A * (B * C) # answer(associativity). A * A ' != B * B ' # answer(inverse). A * (B * B ') != A # answer(identity). end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x * (y * (((z * z ') * (u * y) ') * x)) ' = u. [input]. 2 (A * B) * C != A * (B * C) # answer(associativity). [input]. 3 A * A ' != B * B ' # answer(inverse). [input]. 4 A * (B * B ') != A # answer(identity). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: % assign(max_proofs, 3). % (Horn set with more than one neg. clause) % assign(max_proofs, 3) -> set(restrict_denials). % Restrict denials; moving clauses to denials list: clauses(denials). 2 (A * B) * C != A * (B * C) # answer(associativity). [input]. 3 A * A ' != B * B ' # answer(inverse). [input]. 4 A * (B * B ') != A # answer(identity). [input]. end_of_list. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ A, B, C, *, ' ]). After inverse_order: Function symbol precedence: lex([ A, B, C, *, ' ]). Unfolding symbols: (none). 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). 5 x * (y * (((z * z ') * (u * y) ') * x)) ' = u. [input]. end_of_list. clauses(demodulators). 5 x * (y * (((z * z ') * (u * y) ') * x)) ' = u. [input]. end_of_list. clauses(denials). 6 (A * B) * C != A * (B * C) # answer(associativity). [input]. 7 B * B ' != A * A ' # answer(inverse). [copy(3),flip(a)]. 8 A * (B * B ') != A # answer(identity). [input]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=18): 5 x * (y * (((z * z ') * (u * y) ') * x)) ' = u. [input]. given #2 (F,wt=23): 10 x * ((((y * y ') * (z * u) ') * (v * v ')) * (z * x)) ' = u. [para(5(a,1),5(a,1,2,1,2,1))]. given #3 (F,wt=28): 13 ((x * x ') * (y * z) ') * (u * u ') = v * ((y * (w * w ')) * (z * v)) '. [para(10(a,1),5(a,1,2,1,2,1)),flip(a)]. given #4 (T,wt=22): 29 x * ((y * ((z * (u * u ')) * (v * y)) ') * (z * x)) ' = v. [para(13(a,1),10(a,1,2,1,1))]. given #5 (T,wt=23): 21 (x * x ') * (y * (z * ((u * (v * v ')) * (y * z)) ')) ' = u. [para(13(a,1),5(a,1,2,1,2))]. given #6 (A,wt=29): 9 x * ((y * (((z * z ') * (u * y) ') * v)) ' * (((w * w ') * u ') * x)) ' = v. [para(5(a,1),5(a,1,2,1,2,1,2,1))]. given #7 (F,wt=18): 117 x * (((y * y ') * ((z * z ') * x) ') * u) = u. [para(21(a,1),9(a,1,2,1,2)),demod(67(22))]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: inverse. % Length of proof is 11. % Level of proof is 7. % Maximum clause weight is 29. % Given clauses 7. 3 A * A ' != B * B ' # answer(inverse). [input]. 5 x * (y * (((z * z ') * (u * y) ') * x)) ' = u. [input]. 7 B * B ' != A * A ' # answer(inverse). [copy(3),flip(a)]. 9 x * ((y * (((z * z ') * (u * y) ') * v)) ' * (((w * w ') * u ') * x)) ' = v. [para(5(a,1),5(a,1,2,1,2,1,2,1))]. 10 x * ((((y * y ') * (z * u) ') * (v * v ')) * (z * x)) ' = u. [para(5(a,1),5(a,1,2,1,2,1))]. 13 ((x * x ') * (y * z) ') * (u * u ') = v * ((y * (w * w ')) * (z * v)) '. [para(10(a,1),5(a,1,2,1,2,1)),flip(a)]. 21 (x * x ') * (y * (z * ((u * (v * v ')) * (y * z)) ')) ' = u. [para(13(a,1),5(a,1,2,1,2))]. 67 (x * (y * ((z * (u * u ')) * (x * y)) ')) ' * (v ' * z) ' = v. [para(21(a,1),5(a,1,2,1,2))]. 117 x * (((y * y ') * ((z * z ') * x) ') * u) = u. [para(21(a,1),9(a,1,2,1,2)),demod(67(22))]. 125 x * x ' = y * y '. [para(117(a,1),5(a,1,2,1))]. 126 $F # answer(inverse). [resolve(125,a,7,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 7. given #8 (F,wt=9): 125 x * x ' = y * y '. [para(117(a,1),5(a,1,2,1))]. given #9 (T,wt=14): 164 x * (y ' * ((z * z ') * x)) ' = y. [para(125(a,1),5(a,1,2,1,2,1))]. given #10 (T,wt=14): 180 (x * x ') ' * ((y * y ') * z) = z. [para(125(a,1),117(a,1,2,1))]. given #11 (A,wt=29): 11 (x * (((y * y ') * (z * x) ') * ((u * u ') * (v * w) '))) ' * (w * z) ' = v. [para(5(a,1),5(a,1,2,1,2))]. given #12 (F,wt=16): 206 (x * x ') ' * (y ' * (z * z ')) ' = y. [para(125(a,1),164(a,1,2,1,2))]. given #13 (F,wt=16): 228 (x * x ') ' = (y * y ') ' * (z * z '). [para(125(a,1),180(a,1,2)),flip(a)]. given #14 (T,wt=11): 326 (x * x ') ' = (y * y ') '. [para(228(a,2),180(a,1))]. given #15 (T,wt=15): 356 (x * x ') * (y * y ') ' = z * z '. [para(326(a,1),125(a,1,2))]. given #16 (A,wt=34): 12 x * (((((y * y ') * (z * u) ') * (v * v ')) * (z * w)) ' * (((v6 * v6 ') * u ') * x)) ' = w. [para(10(a,1),5(a,1,2,1,2,1,2,1))]. given #17 (F,wt=15): 386 ((x * x ') ' * y) * (z ' * y) ' = z. [para(356(a,2),11(a,1,1,1,2,2,2,1)),demod(129(18))]. given #18 (F,wt=16): 479 x * ((y * y ') ' ' * (z * x)) ' = z '. [para(386(a,1),5(a,1,2,1,2,1))]. given #19 (T,wt=16): 516 x * (y ' * (x ' * (z * z ')) ') ' = y. [para(206(a,1),386(a,1,1))]. given #20 (T,wt=9): 624 x * (y * y ') ' = x. [back_demod(524),demod(603(6),582(6))]. given #21 (A,wt=34): 14 ((((x * x ') * (y * z) ') * (u * u ')) * (y * ((v * v ') * (w * v6) '))) ' * (v6 * z) ' = w. [para(10(a,1),5(a,1,2,1,2))]. given #22 (F,wt=11): 603 (x * x ') ' * y ' ' = y. [para(180(a,1),516(a,1,2,1,2,1)),demod(582(10))]. given #23 (F,wt=10): 787 x ' ' = (y * y ') * x. [back_demod(210),demod(769(17)),flip(a)]. given #24 (T,wt=11): 618 x * (y ' * x ' ') ' = y. [para(516(a,1),386(a,1,1)),demod(553(11))]. given #25 (T,wt=11): 622 ((x * x ') ' * y ') ' = y. [back_demod(532),demod(582(9))]. ============================== PROOF ================================= % Proof 2 at 0.14 (+ 0.00) seconds: identity. % Length of proof is 55. % Level of proof is 24. % Maximum clause weight is 35. % Given clauses 25. 5 x * (y * (((z * z ') * (u * y) ') * x)) ' = u. [input]. 8 A * (B * B ') != A # answer(identity). [input]. 9 x * ((y * (((z * z ') * (u * y) ') * v)) ' * (((w * w ') * u ') * x)) ' = v. [para(5(a,1),5(a,1,2,1,2,1,2,1))]. 10 x * ((((y * y ') * (z * u) ') * (v * v ')) * (z * x)) ' = u. [para(5(a,1),5(a,1,2,1,2,1))]. 11 (x * (((y * y ') * (z * x) ') * ((u * u ') * (v * w) '))) ' * (w * z) ' = v. [para(5(a,1),5(a,1,2,1,2))]. 13 ((x * x ') * (y * z) ') * (u * u ') = v * ((y * (w * w ')) * (z * v)) '. [para(10(a,1),5(a,1,2,1,2,1)),flip(a)]. 21 (x * x ') * (y * (z * ((u * (v * v ')) * (y * z)) ')) ' = u. [para(13(a,1),5(a,1,2,1,2))]. 29 x * ((y * ((z * (u * u ')) * (v * y)) ') * (z * x)) ' = v. [para(13(a,1),10(a,1,2,1,1))]. 67 (x * (y * ((z * (u * u ')) * (x * y)) ')) ' * (v ' * z) ' = v. [para(21(a,1),5(a,1,2,1,2))]. 117 x * (((y * y ') * ((z * z ') * x) ') * u) = u. [para(21(a,1),9(a,1,2,1,2)),demod(67(22))]. 125 x * x ' = y * y '. [para(117(a,1),5(a,1,2,1))]. 129 (x * (((y * y ') * (z * x) ') * ((u * u ') * ((v * v ') * w) '))) ' = w * z. [para(5(a,1),117(a,1,2)),flip(a)]. 164 x * (y ' * ((z * z ') * x)) ' = y. [para(125(a,1),5(a,1,2,1,2,1))]. 167 x * (((y * y ') * (z * z ')) * (u * x)) ' = u '. [para(125(a,1),10(a,1,2,1,1,1))]. 171 x ' * ((y * (z * z ')) * (u * u ')) ' = ((v * v ') * (y * x) ') * (w * w '). [para(125(a,1),13(a,2,2,1,2)),flip(a)]. 180 (x * x ') ' * ((y * y ') * z) = z. [para(125(a,1),117(a,1,2,1))]. 206 (x * x ') ' * (y ' * (z * z ')) ' = y. [para(125(a,1),164(a,1,2,1,2))]. 210 (x * x ') * y = z * ((((u * u ') * y ') * (v * v ')) * ((w * w ') ' * z)) '. [para(180(a,1),10(a,1,2,1,1,1,2,1)),flip(a)]. 213 ((x * x ') * y ') * (z * z ') = u * (((v * v ') ' * (w * w ')) * (((v6 * v6 ') * y) * u)) '. [para(180(a,1),13(a,1,1,2,1))]. 220 ((x * x ') * y) * ((z * (((u * u ') ' * (v * v ')) * (w * z)) ') * y) ' = w. [para(180(a,1),29(a,1,2,1,2))]. 227 (x * x ') ' * y = ((z * z ') * ((u * u ') * (v * v ')) ') * y. [para(117(a,1),180(a,1,2))]. 228 (x * x ') ' = (y * y ') ' * (z * z '). [para(125(a,1),180(a,1,2)),flip(a)]. 300 (x * x ') * ((((y * y ') * ((z * z ') ' * u) ') * (v * v ')) * (w * w ') ') ' = u. [para(228(a,2),10(a,1,2,1,2))]. 326 (x * x ') ' = (y * y ') '. [para(228(a,2),180(a,1))]. 356 (x * x ') * (y * y ') ' = z * z '. [para(326(a,1),125(a,1,2))]. 386 ((x * x ') ' * y) * (z ' * y) ' = z. [para(356(a,2),11(a,1,1,1,2,2,2,1)),demod(129(18))]. 479 x * ((y * y ') ' ' * (z * x)) ' = z '. [para(386(a,1),5(a,1,2,1,2,1))]. 516 x * (y ' * (x ' * (z * z ')) ') ' = y. [para(206(a,1),386(a,1,1))]. 524 ((x * x ') ' * y ' ') * ((z * z ') * (u * u ') ') ' = y. [para(356(a,2),386(a,1,2,1))]. 532 ((x * x ') * (y * (z * z ') ' ') ') ' = y. [para(479(a,1),5(a,1))]. 537 x ' * (y * y ') = z * (((u * u ') ' ' * (v * v ')) * ((x * (w * w ')) * z)) '. [para(479(a,1),13(a,1,1))]. 582 (x * x ') * (y * z ') ' = z * y '. [para(5(a,1),516(a,1,2,1)),flip(a)]. 603 (x * x ') ' * y ' ' = y. [para(180(a,1),516(a,1,2,1,2,1)),demod(582(10))]. 622 ((x * x ') ' * y ') ' = y. [back_demod(532),demod(582(9))]. 624 x * (y * y ') ' = x. [back_demod(524),demod(603(6),582(6))]. 633 (x * x ') * (((y * y ') * ((z * z ') ' * u) ') * (v * v ')) ' = u. [back_demod(300),demod(624(17))]. 769 x * ((((y * y ') * z ') * (u * u ')) * ((v * v ') ' * x)) ' = z ' '. [para(603(a,1),10(a,1,2,1,1,1,2,1))]. 787 x ' ' = (y * y ') * x. [back_demod(210),demod(769(17)),flip(a)]. 847 ((x * x ') * y ' ' ') * (z * z ') = y '. [para(787(a,2),13(a,1,1,2,1)),demod(167(18))]. 882 x * (((y * y ') * x) ' ' ' * z) = z. [para(787(a,2),117(a,1,2,1))]. 946 ((x * x ') * y) * (z * z ') = u * (((v * v ') ' * (w * w ')) * (y ' * u)) '. [para(622(a,1),13(a,1,1,2))]. 964 x ' * (y * y ') = x '. [para(164(a,1),622(a,1,1)),demod(624(8)),flip(a)]. 995 ((x * x ') * y) * (z * z ') = u * ((v * v ') ' * (y ' * u)) '. [back_demod(946),demod(964(12))]. 1004 (x * (y * y ')) ' = x '. [back_demod(537),demod(964(4),964(8),479(12)),flip(a)]. 1009 ((x * x ') * y) * ((z * ((u * u ') ' * (v * z)) ') * y) ' = v. [back_demod(220),demod(964(9))]. 1010 ((x * x ') * y ') * (z * z ') = u * ((v * v ') ' * (((w * w ') * y) * u)) '. [back_demod(213),demod(964(13))]. 1032 (x * x ') ' * y = y. [back_demod(633),demod(1004(14),582(12),624(8))]. 1047 (x * x ') * y = y. [back_demod(227),demod(1032(4),1004(8),624(6)),flip(a)]. 1053 (x * y) ' = y ' * x '. [back_demod(171),demod(1004(8),1004(5),1047(8),964(8)),flip(a)]. 1070 x ' ' ' = x '. [back_demod(847),demod(1047(6),964(6))]. 1106 x * (x ' * y) = y. [back_demod(882),demod(1047(3),1070(3))]. 1117 x * ((x ' * y ') * (z ' ' * z ')) = y '. [back_demod(1010),demod(1047(4),964(4),1053(4),1047(8),1053(8),1053(3),1053(9),1070(9)),flip(a)]. 1118 x ' ' = x. [back_demod(1009),demod(1047(3),1053(3),1053(7),1053(2),1053(8),1070(8),1117(9),1053(3),1106(5))]. 1119 x * (y * y ') = x. [back_demod(995),demod(1047(3),1053(6),1118(5),1047(8),1053(6),1118(6),1106(6))]. 1120 $F # answer(identity). [resolve(1119,a,8,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 8. ============================== PROOF ================================= % Proof 3 at 0.19 (+ 0.00) seconds: associativity. % Length of proof is 61. % Level of proof is 25. % Maximum clause weight is 38. % Given clauses 25. 5 x * (y * (((z * z ') * (u * y) ') * x)) ' = u. [input]. 6 (A * B) * C != A * (B * C) # answer(associativity). [input]. 9 x * ((y * (((z * z ') * (u * y) ') * v)) ' * (((w * w ') * u ') * x)) ' = v. [para(5(a,1),5(a,1,2,1,2,1,2,1))]. 10 x * ((((y * y ') * (z * u) ') * (v * v ')) * (z * x)) ' = u. [para(5(a,1),5(a,1,2,1,2,1))]. 11 (x * (((y * y ') * (z * x) ') * ((u * u ') * (v * w) '))) ' * (w * z) ' = v. [para(5(a,1),5(a,1,2,1,2))]. 13 ((x * x ') * (y * z) ') * (u * u ') = v * ((y * (w * w ')) * (z * v)) '. [para(10(a,1),5(a,1,2,1,2,1)),flip(a)]. 21 (x * x ') * (y * (z * ((u * (v * v ')) * (y * z)) ')) ' = u. [para(13(a,1),5(a,1,2,1,2))]. 29 x * ((y * ((z * (u * u ')) * (v * y)) ') * (z * x)) ' = v. [para(13(a,1),10(a,1,2,1,1))]. 67 (x * (y * ((z * (u * u ')) * (x * y)) ')) ' * (v ' * z) ' = v. [para(21(a,1),5(a,1,2,1,2))]. 117 x * (((y * y ') * ((z * z ') * x) ') * u) = u. [para(21(a,1),9(a,1,2,1,2)),demod(67(22))]. 125 x * x ' = y * y '. [para(117(a,1),5(a,1,2,1))]. 129 (x * (((y * y ') * (z * x) ') * ((u * u ') * ((v * v ') * w) '))) ' = w * z. [para(5(a,1),117(a,1,2)),flip(a)]. 164 x * (y ' * ((z * z ') * x)) ' = y. [para(125(a,1),5(a,1,2,1,2,1))]. 167 x * (((y * y ') * (z * z ')) * (u * x)) ' = u '. [para(125(a,1),10(a,1,2,1,1,1))]. 171 x ' * ((y * (z * z ')) * (u * u ')) ' = ((v * v ') * (y * x) ') * (w * w '). [para(125(a,1),13(a,2,2,1,2)),flip(a)]. 177 ((x * x ') * (y * z) ') ' = u * ((z * (v * v ')) ' * (((w * w ') * y ') * u)) '. [para(125(a,1),9(a,1,2,1,1,1,2)),flip(a)]. 180 (x * x ') ' * ((y * y ') * z) = z. [para(125(a,1),117(a,1,2,1))]. 206 (x * x ') ' * (y ' * (z * z ')) ' = y. [para(125(a,1),164(a,1,2,1,2))]. 210 (x * x ') * y = z * ((((u * u ') * y ') * (v * v ')) * ((w * w ') ' * z)) '. [para(180(a,1),10(a,1,2,1,1,1,2,1)),flip(a)]. 213 ((x * x ') * y ') * (z * z ') = u * (((v * v ') ' * (w * w ')) * (((v6 * v6 ') * y) * u)) '. [para(180(a,1),13(a,1,1,2,1))]. 220 ((x * x ') * y) * ((z * (((u * u ') ' * (v * v ')) * (w * z)) ') * y) ' = w. [para(180(a,1),29(a,1,2,1,2))]. 227 (x * x ') ' * y = ((z * z ') * ((u * u ') * (v * v ')) ') * y. [para(117(a,1),180(a,1,2))]. 228 (x * x ') ' = (y * y ') ' * (z * z '). [para(125(a,1),180(a,1,2)),flip(a)]. 279 (x ' * (y * y ')) ' = z * ((((u * u ') * x ') * (v * v ')) * ((w * w ') ' * z)) '. [para(206(a,1),10(a,1,2,1,1,1,2,1)),flip(a)]. 300 (x * x ') * ((((y * y ') * ((z * z ') ' * u) ') * (v * v ')) * (w * w ') ') ' = u. [para(228(a,2),10(a,1,2,1,2))]. 326 (x * x ') ' = (y * y ') '. [para(228(a,2),180(a,1))]. 356 (x * x ') * (y * y ') ' = z * z '. [para(326(a,1),125(a,1,2))]. 386 ((x * x ') ' * y) * (z ' * y) ' = z. [para(356(a,2),11(a,1,1,1,2,2,2,1)),demod(129(18))]. 479 x * ((y * y ') ' ' * (z * x)) ' = z '. [para(386(a,1),5(a,1,2,1,2,1))]. 516 x * (y ' * (x ' * (z * z ')) ') ' = y. [para(206(a,1),386(a,1,1))]. 524 ((x * x ') ' * y ' ') * ((z * z ') * (u * u ') ') ' = y. [para(356(a,2),386(a,1,2,1))]. 532 ((x * x ') * (y * (z * z ') ' ') ') ' = y. [para(479(a,1),5(a,1))]. 537 x ' * (y * y ') = z * (((u * u ') ' ' * (v * v ')) * ((x * (w * w ')) * z)) '. [para(479(a,1),13(a,1,1))]. 582 (x * x ') * (y * z ') ' = z * y '. [para(5(a,1),516(a,1,2,1)),flip(a)]. 594 (x ' * (((y * y ') * (z * u) ') ' * (v * v ')) ') ' = w * ((u * x) ' * (((v6 * v6 ') * z ') * w)) '. [para(516(a,1),9(a,1,2,1,1,1,2)),flip(a)]. 603 (x * x ') ' * y ' ' = y. [para(180(a,1),516(a,1,2,1,2,1)),demod(582(10))]. 622 ((x * x ') ' * y ') ' = y. [back_demod(532),demod(582(9))]. 624 x * (y * y ') ' = x. [back_demod(524),demod(603(6),582(6))]. 633 (x * x ') * (((y * y ') * ((z * z ') ' * u) ') * (v * v ')) ' = u. [back_demod(300),demod(624(17))]. 769 x * ((((y * y ') * z ') * (u * u ')) * ((v * v ') ' * x)) ' = z ' '. [para(603(a,1),10(a,1,2,1,1,1,2,1))]. 786 (x ' * (y * y ')) ' = x ' '. [back_demod(279),demod(769(19))]. 787 x ' ' = (y * y ') * x. [back_demod(210),demod(769(17)),flip(a)]. 801 (x ' * ((y * y ') * (z * u) ') ' ') ' = v * ((u * x) ' * (((w * w ') * z ') * v)) '. [back_demod(594),demod(786(11))]. 847 ((x * x ') * y ' ' ') * (z * z ') = y '. [para(787(a,2),13(a,1,1,2,1)),demod(167(18))]. 882 x * (((y * y ') * x) ' ' ' * z) = z. [para(787(a,2),117(a,1,2,1))]. 964 x ' * (y * y ') = x '. [para(164(a,1),622(a,1,1)),demod(624(8)),flip(a)]. 1004 (x * (y * y ')) ' = x '. [back_demod(537),demod(964(4),964(8),479(12)),flip(a)]. 1009 ((x * x ') * y) * ((z * ((u * u ') ' * (v * z)) ') * y) ' = v. [back_demod(220),demod(964(9))]. 1010 ((x * x ') * y ') * (z * z ') = u * ((v * v ') ' * (((w * w ') * y) * u)) '. [back_demod(213),demod(964(13))]. 1032 (x * x ') ' * y = y. [back_demod(633),demod(1004(14),582(12),624(8))]. 1047 (x * x ') * y = y. [back_demod(227),demod(1032(4),1004(8),624(6)),flip(a)]. 1049 (x * y) ' ' = z * (y ' * (x ' * z)) '. [back_demod(177),demod(1047(5),1004(7),1047(8))]. 1053 (x * y) ' = y ' * x '. [back_demod(171),demod(1004(8),1004(5),1047(8),964(8)),flip(a)]. 1070 x ' ' ' = x '. [back_demod(847),demod(1047(6),964(6))]. 1106 x * (x ' * y) = y. [back_demod(882),demod(1047(3),1070(3))]. 1109 (x ' ' * y ' ') * z ' ' = u * ((u ' * x ' ') * (y ' ' * z ' ')). [back_demod(801),demod(1053(5),1047(7),1053(5),1053(7),1070(4),1070(5),1053(6),1053(4),1053(10),1047(15),1053(15),1053(11),1053(16))]. 1117 x * ((x ' * y ') * (z ' ' * z ')) = y '. [back_demod(1010),demod(1047(4),964(4),1053(4),1047(8),1053(8),1053(3),1053(9),1070(9)),flip(a)]. 1118 x ' ' = x. [back_demod(1009),demod(1047(3),1053(3),1053(7),1053(2),1053(8),1070(8),1117(9),1053(3),1106(5))]. 1211 x * ((x ' * y) * z) = y * z. [back_demod(1049),demod(1053(2),1053(4),1118(2),1118(2),1053(6),1053(4),1118(4),1118(5)),flip(a)]. 1213 (x * y) * z = x * (y * z). [back_demod(1109),demod(1118(2),1118(2),1118(3),1118(5),1118(6),1118(6),1211(7))]. 1214 $F # answer(associativity). [resolve(1213,a,6,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=25. Generated=2646. Kept=1207. proofs=3. Usable=1. Sos=48. Demods=131. Denials=1. Limbo=101, Disabled=1059. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=1439. Back_subsumed=11. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=862 (0 lex), Back_demodulated=1042. Back_unit_deleted=0. Demod_attempts=62782. Demod_rewrites=10372. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.88. User_CPU=0.19, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 3 proofs. Process 12993 exit (max_proofs) Mon Jun 19 16:39:58 2006