============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13122 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:34 2006 The command was "/home/mccune/bin/prover9 -f gt.in DN.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 DN.in clauses(sos). (x @ y) * (z @ y) = x * z @ y. end_of_list. clauses(sos). (A @ B) * C != C * (A @ B) # answer(N). 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 != C * (A @ B) # answer(N). [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, *, @, ' ]). After inverse_order: Function symbol precedence: lex([ e, A, B, C, *, ', @ ]). Folding symbols: @/2. After fold_eq: Function symbol precedence: lex([ e, A, B, C, @, *, ' ]). 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 != C * (A @ B) # answer(N). [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 != C * (A @ B) # answer(N). [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=17): 52 A ' * B ' * A * B * C != C * (A @ B) # answer(N). [para(14(a,2),12(a,1))]. given #13 (F,wt=5): 34 x * e = x. [back_demod(26),demod(31(4))]. given #14 (T,wt=4): 58 e ' = e. [para(34(a,1),9(a,1))]. given #15 (T,wt=5): 59 x @ e = e. [para(34(a,1),10(a,1,2,2)),demod(58(3),8(3),9(2)),flip(a)]. 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=8): 69 x ' @ y = y @ x. [back_demod(61),demod(66(6))]. given #18 (F,wt=12): 74 (B ' @ A) * C != C * (A @ B) # answer(N). [para(69(a,2),12(a,1,1))]. given #19 (T,wt=9): 31 x ' ' * y = x * y. [para(13(a,1),13(a,1,2))]. given #20 (T,wt=5): 93 x ' ' = x. [para(31(a,1),34(a,1)),demod(34(2)),flip(a)]. 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=12): 75 C * (B ' @ A) != (A @ B) * C # answer(N). [para(69(a,2),12(a,2,2)),flip(a)]. given #23 (F,wt=13): 84 (B ' @ A) * C != C * (B ' @ A) # answer(N). [para(69(a,2),74(a,2,2))]. given #24 (T,wt=6): 85 x * x ' = e. [para(31(a,1),9(a,1))]. given #25 (T,wt=6): 95 x @ x ' = e. [para(93(a,1),17(a,1,1))]. 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=17): 83 B * A ' * B ' * A * C != C * (A @ B) # answer(N). [para(14(a,2),74(a,1)),demod(31(13))]. given #28 (F,wt=18): 78 A ' * B ' * A * B * C != C * (B ' @ A) # answer(N). [para(69(a,2),52(a,2,2))]. given #29 (T,wt=8): 89 x * x ' * y = y. [para(31(a,1),13(a,1))]. given #30 (T,wt=8): 96 x @ y ' = y @ x. [para(93(a,1),69(a,1,1)),flip(a)]. 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): 140 (B @ A ') * C != C * (A @ B) # answer(N). [para(96(a,2),12(a,1,1))]. given #33 (F,wt=12): 141 C * (B @ A ') != (A @ B) * C # answer(N). [para(96(a,2),12(a,2,2)),flip(a)]. given #34 (T,wt=9): 37 x * y @ x = y @ x. [para(28(a,1),11(a,1,1)),demod(8(3)),flip(a)]. given #35 (T,wt=7): 181 (x @ y) @ x = e. [back_demod(161),demod(171(4),9(2),16(2)),flip(a)]. 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): 146 (B @ A ') * C != C * (B @ A ') # answer(N). [para(96(a,2),74(a,2,2)),demod(145(4))]. given #38 (F,wt=17): 168 B ' * A * B * A ' * C != C * (A @ B) # answer(N). [para(14(a,2),140(a,1)),demod(93(5))]. given #39 (T,wt=7): 192 (x @ y) @ y = e. [para(96(a,1),181(a,1,1))]. given #40 (T,wt=7): 200 x @ x * x = e. [para(24(a,1),10(a,1,2)),demod(9(2)),flip(a)]. 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=18): 144 A ' * B ' * A * B * C != C * (B @ A ') # answer(N). [para(96(a,2),52(a,2,2))]. given #43 (F,wt=18): 158 B * A ' * B ' * A * C != C * (B @ A ') # answer(N). [para(96(a,2),83(a,2,2))]. given #44 (T,wt=8): 188 x ' @ (x @ y) = e. [para(181(a,1),69(a,2))]. given #45 (T,wt=7): 286 x @ (y @ x) = e. [para(69(a,1),188(a,1,2)),demod(93(2))]. given #46 (A,wt=12): 32 x ' * y * x = y * (y @ x). [back_demod(29),demod(31(4)),flip(a)]. given #47 (F,wt=18): 217 B ' * A * B * A ' * C != C * (B @ A ') # answer(N). [para(14(a,2),146(a,1)),demod(93(5))]. given #48 (F,wt=7): 295 x @ (x @ y) = e. [para(69(a,1),286(a,1,2))]. given #49 (T,wt=8): 189 (x @ y) @ y ' = e. [para(69(a,1),181(a,1,1))]. given #50 (T,wt=8): 191 x @ (x ' @ y) = e. [para(181(a,1),96(a,1)),flip(a)]. given #51 (A,wt=10): 36 x * y ' @ y = x @ y. [back_demod(23),demod(34(5))]. given #52 (F,wt=8): 193 (x @ y ') @ y = e. [para(96(a,2),181(a,1,1))]. given #53 (F,wt=8): 221 x ' @ (y @ x) = e. [para(192(a,1),69(a,2))]. given #54 (T,wt=8): 222 (x ' @ y) @ x = e. [para(69(a,2),192(a,1,1))]. given #55 (T,wt=8): 223 x @ (y @ x ') = e. [para(192(a,1),96(a,1)),flip(a)]. given #56 (A,wt=9): 38 x * y @ y = x @ y. [para(28(a,1),11(a,1,2)),demod(34(3)),flip(a)]. given #57 (F,wt=8): 224 (x @ y) @ x ' = e. [para(96(a,1),192(a,1,1))]. given #58 (F,wt=9): 79 x ' @ y ' = x @ y. [para(69(a,2),69(a,1))]. given #59 (T,wt=9): 145 x ' @ y = x @ y '. [para(96(a,1),69(a,1)),flip(a)]. given #60 (T,wt=9): 195 (x @ y) @ y * x = e. [para(37(a,1),181(a,1,1))]. given #61 (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 #62 (F,wt=9): 214 (x * y) ' * x = y '. [para(85(a,1),24(a,1,2,2)),demod(34(4))]. given #63 (F,wt=9): 247 (x @ y) ' = x ' @ y. [para(85(a,1),30(a,1,2,1)),demod(16(4),34(4))]. given #64 (T,wt=9): 249 (x @ y) * (y @ x) = e. [para(95(a,1),30(a,2)),demod(247(3),79(3),110(4))]. given #65 (T,wt=9): 264 x @ y * x = x @ y. [back_demod(238),demod(247(3),177(3)),flip(a)]. given #66 (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 #67 (F,wt=9): 323 (x @ y) @ (y @ x) = e. [para(295(a,1),22(a,2)),demod(247(2),48(3),318(4))]. given #68 (F,wt=9): 371 (x @ y) @ x * y = e. [para(38(a,1),181(a,1,1))]. given #69 (T,wt=9): 413 x * y @ y * x = e. [para(195(a,1),37(a,2)),demod(7(3),301(3))]. given #70 (T,wt=9): 523 x @ x * (y @ x) = e. [para(191(a,1),264(a,2)),demod(48(3))]. given #71 (A,wt=22): 46 x ' * y * x * (y @ z) = (x @ y ') * z ' * y * z. [para(10(a,1),14(a,1,2,2,2)),demod(31(6))]. given #72 (F,wt=9): 595 x @ x * (x @ y) = e. [para(32(a,1),413(a,1,2)),demod(7(3),85(2),34(2))]. given #73 (F,wt=10): 110 x * y @ y ' = y @ x. [para(85(a,1),15(a,1,2,2,2)),demod(93(4),34(4),66(4)),flip(a)]. given #74 (T,wt=10): 167 x @ y ' = y @ y * x. [para(22(a,1),96(a,1)),demod(93(4))]. given #75 (T,wt=9): 680 x @ x * y = x @ y. [para(167(a,1),69(a,2)),demod(93(2)),flip(a)]. 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=10): 177 x ' @ x * y = y @ x. [para(37(a,1),69(a,2))]. given #78 (F,wt=10): 194 (x @ y) @ y ' * x = e. [para(22(a,1),181(a,1,1))]. given #79 (T,wt=10): 256 (x @ y) @ (x ' @ y) = e. [back_demod(128),demod(247(2),247(5),93(4),11(4),9(2),16(2)),flip(a)]. given #80 (T,wt=10): 259 (x ' @ y) @ (x @ y) = e. [back_demod(116),demod(247(3),93(2),247(3),11(4),85(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=10): 336 (x @ y) @ (y ' @ x) = e. [para(191(a,1),37(a,2)),demod(48(3),331(5))]. given #83 (F,wt=10): 341 (x @ y) @ x * y ' = e. [para(36(a,1),181(a,1,1))]. given #84 (T,wt=10): 348 (x @ y) * (x @ y ') = e. [back_demod(343),demod(347(6))]. given #85 (T,wt=10): 363 (x @ y) @ (x @ y ') = e. [para(223(a,1),22(a,2)),demod(247(3),79(3),359(5))]. 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=10): 379 (x ' @ y) @ y * x = e. [para(37(a,1),224(a,1,1)),demod(145(4,R),247(2))]. given #88 (F,wt=10): 382 (x ' @ y) @ x * y = e. [para(38(a,1),224(a,1,1)),demod(145(4,R),247(2))]. given #89 (T,wt=10): 411 (x @ y) @ x ' * y = e. [para(96(a,1),195(a,1,1))]. given #90 (T,wt=10): 412 (x @ y ') @ x * y = e. [para(96(a,2),195(a,1,1))]. given #91 (A,wt=16): 53 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=10): 445 (x * y) ' = y ' * x '. [para(13(a,1),214(a,1,1,1)),flip(a)]. given #93 (F,wt=10): 502 (x @ y ') * (x @ y) = e. [para(69(a,1),249(a,1,2))]. given #94 (T,wt=10): 547 x @ y ' * x * y = e. [para(43(a,2),264(a,1,2)),demod(223(7))]. given #95 (T,wt=10): 552 (x ' @ y) @ (y @ x) = e. [para(323(a,1),69(a,2)),demod(247(2))]. given #96 (A,wt=17): 55 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=10): 553 (x @ y ') @ (x @ y) = e. [para(69(a,1),323(a,1,2))]. given #98 (F,wt=10): 565 (x @ y) @ y * x ' = e. [para(96(a,1),371(a,1,1))]. given #99 (T,wt=10): 566 (x @ y ') @ y * x = e. [para(96(a,2),371(a,1,1))]. given #100 (T,wt=10): 578 (x @ y) @ (y @ x ') = e. [para(10(a,1),413(a,1,1)),demod(7(6),7(5),87(6))]. given #101 (A,wt=16): 57 (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=10): 579 (x @ y ') @ (y @ x) = e. [para(10(a,1),413(a,1,2)),demod(7(5),7(4),87(5))]. given #103 (F,wt=10): 583 x @ y * x * y ' = e. [para(13(a,1),413(a,1,1)),demod(7(3))]. given #104 (T,wt=11): 113 x * y @ x ' = y @ x '. [para(95(a,1),11(a,1,1)),demod(8(4)),flip(a)]. given #105 (T,wt=11): 179 x @ x ' * y = y @ x '. [para(37(a,1),96(a,1)),flip(a)]. given #106 (A,wt=18): 64 x ' * y * z * x = y * z * (y * z @ x). [para(15(a,1),13(a,1,2)),demod(31(6),7(4)),flip(a)]. given #107 (F,wt=11): 180 (x @ y) * z @ x = z @ x. [back_demod(164),demod(171(5),13(3)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.14 (+ 0.02) seconds: N. % Length of proof is 59. % Level of proof is 14. % Maximum clause weight is 24. % Given clauses 107. 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 != C * (A @ B) # answer(N). [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)]. 20 (x @ y) ' * (z @ y) ' * (x * z @ y) = (x @ y) @ (z @ y). [para(11(a,1),10(a,1,2,2))]. 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)]. 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))]. 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)]. 55 x ' * y * x * z = (x @ y ') * y * z. [para(13(a,1),14(a,1,2,2,2)),demod(31(5))]. 61 (x * y ') ' * y ' * x = x @ y. [para(9(a,1),15(a,1,2,2,2)),demod(34(6),36(9))]. 66 (x * y) ' * y * x = y @ x. [para(13(a,1),15(a,1,2)),demod(37(6))]. 69 x ' @ y = y @ x. [back_demod(61),demod(66(6))]. 74 (B ' @ A) * C != C * (A @ B) # answer(N). [para(69(a,2),12(a,1,1))]. 79 x ' @ y ' = x @ y. [para(69(a,2),69(a,1))]. 85 x * x ' = e. [para(31(a,1),9(a,1))]. 93 x ' ' = x. [para(31(a,1),34(a,1)),demod(34(2)),flip(a)]. 95 x @ x ' = e. [para(93(a,1),17(a,1,1))]. 96 x @ y ' = y @ x. [para(93(a,1),69(a,1,1)),flip(a)]. 110 x * y @ y ' = y @ x. [para(85(a,1),15(a,1,2,2,2)),demod(93(4),34(4),66(4)),flip(a)]. 126 (x ' @ y) @ (z @ x) = (y @ x) @ (z @ x). [para(69(a,2),20(a,2,1)),demod(20(8)),flip(a)]. 138 (x @ y) * (y @ z ') = x * z @ y. [para(96(a,2),11(a,1,2))]. 145 x ' @ y = x @ y '. [para(96(a,1),69(a,1)),flip(a)]. 146 (B @ A ') * C != C * (B @ A ') # answer(N). [para(96(a,2),74(a,2,2)),demod(145(4))]. 153 (x @ y) ' * (z @ y) ' * (y @ (x * z) ') = (x @ y) @ (z @ y). [para(96(a,2),20(a,1,2,2))]. 161 x ' * y * x @ y = (y @ x) @ y. [para(10(a,1),22(a,1,1)),flip(a)]. 164 x ' * y * x * z @ y = (y @ x) * z @ y. [para(14(a,1),22(a,1,1)),flip(a)]. 171 x * y * z @ y = x * z @ y. [para(37(a,1),11(a,1,2)),demod(11(3)),flip(a)]. 180 (x @ y) * z @ x = z @ x. [back_demod(164),demod(171(5),13(3)),flip(a)]. 181 (x @ y) @ x = e. [back_demod(161),demod(171(4),9(2),16(2)),flip(a)]. 188 x ' @ (x @ y) = e. [para(181(a,1),69(a,2))]. 214 (x * y) ' * x = y '. [para(85(a,1),24(a,1,2,2)),demod(34(4))]. 247 (x @ y) ' = x ' @ y. [para(85(a,1),30(a,1,2,1)),demod(16(4),34(4))]. 249 (x @ y) * (y @ x) = e. [para(95(a,1),30(a,2)),demod(247(3),79(3),110(4))]. 269 (x @ y) @ (z @ y) = (x @ z) @ y. [back_demod(153),demod(247(2),247(4),138(8),11(7),10(5)),flip(a)]. 283 x ' * y @ (x @ z) = y @ (x @ z). [para(188(a,1),11(a,1,1)),demod(8(4)),flip(a)]. 445 (x * y) ' = y ' * x '. [para(13(a,1),214(a,1,1,1)),flip(a)]. 502 (x @ y ') * (x @ y) = e. [para(69(a,1),249(a,1,2))]. 1179 ((x @ y ') @ z ') * z * (x @ y) = (x @ y) * z. [para(502(a,1),55(a,1,2,2)),demod(247(3),79(3),34(3)),flip(a)]. 1427 (x ' @ y) @ (z @ x) = e. [para(180(a,1),188(a,1,2)),demod(445(3),247(3),283(6))]. 1453 (x @ y) @ (z @ y) = e. [back_demod(126),demod(1427(4)),flip(a)]. 1457 (x @ y) @ z = e. [back_demod(269),demod(1453(3)),flip(a)]. 1470 (x @ y) * z = z * (x @ y). [back_demod(1179),demod(1457(4),8(4)),flip(a)]. 1471 $F # answer(N). [resolve(1470,a,146,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=107. Generated=8140. Kept=1464. proofs=1. Usable=80. Sos=895. Demods=661. Denials=0. Limbo=14, Disabled=480. Hints=0. Weight_deleted=614. Literals_deleted=0. Forward_subsumed=6062. Back_subsumed=91. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1026 (1 lex), Back_demodulated=383. Back_unit_deleted=0. Demod_attempts=104622. Demod_rewrites=20182. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.11. User_CPU=0.14, System_CPU=0.02, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13122 exit (max_proofs) Mon Jun 19 16:41:34 2006