============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11356 was started by mccune on cleo.thornwood, Sat Aug 12 20:59:56 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). 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 DN.in formulas(sos). (x @ z) * (y @ z) = x * y @ z. end_of_list. formulas(sos). (A @ B) * C != C * (A @ B) # answer(N). 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 * z @ y. [assumption]. (A @ B) * C != C * (A @ B) # answer(N). [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, *, @, ' ]). 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: 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 * z @ y. [assumption]. 7 (A @ B) * C != C * (A @ B) # answer(N). [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)]. 6 (x @ y) * (z @ y) = x * z @ y. [assumption]. 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=13): 6 (x @ y) * (z @ y) = x * z @ y. [assumption]. given #6 (I,wt=11): 7 (A @ B) * C != C * (A @ B) # answer(N). [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): 23 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=17): 47 A' * B' * A * B * C != C * (A @ B) # answer(N). [para(9(a,2),7(a,1))]. given #13 (F,wt=5): 29 x * e = x. [back_rewrite(21),rewrite(26(4))]. given #14 (T,wt=4): 53 e' = e. [para(29(a,1),3(a,1))]. given #15 (T,wt=5): 54 x @ e = e. [para(29(a,1),5(a,1,2,2)),rewrite(53(3),2(3),3(2)),flip(a)]. 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=8): 64 x' @ y = y @ x. [back_rewrite(56),rewrite(61(6))]. given #18 (F,wt=12): 69 (B' @ A) * C != C * (A @ B) # answer(N). [para(64(a,2),7(a,1,1))]. given #19 (T,wt=9): 26 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. given #20 (T,wt=5): 88 x'' = x. [para(26(a,1),29(a,1)),rewrite(29(2)),flip(a)]. given #21 (A,wt=17): 14 (x * y @ z) * u = (x @ z) * (y @ z) * u. [para(6(a,1),1(a,1,1))]. given #22 (F,wt=12): 70 C * (B' @ A) != (A @ B) * C # answer(N). [para(64(a,2),7(a,2,2)),flip(a)]. given #23 (F,wt=13): 79 (B' @ A) * C != C * (B' @ A) # answer(N). [para(64(a,2),69(a,2,2))]. given #24 (T,wt=6): 80 x * x' = e. [para(26(a,1),3(a,1))]. given #25 (T,wt=6): 90 x @ x' = e. [para(88(a,1),12(a,1,1))]. given #26 (A,wt=23): 15 (x @ y)' * (z @ y)' * (x * z @ y) = (x @ y) @ (z @ y). [para(6(a,1),5(a,1,2,2))]. given #27 (F,wt=17): 78 B * A' * B' * A * C != C * (A @ B) # answer(N). [para(9(a,2),69(a,1)),rewrite(26(13))]. given #28 (F,wt=18): 73 A' * B' * A * B * C != C * (B' @ A) # answer(N). [para(64(a,2),47(a,2,2))]. given #29 (T,wt=8): 84 x * x' * y = y. [para(26(a,1),8(a,1))]. given #30 (T,wt=8): 91 x @ y' = y @ x. [para(88(a,1),64(a,1,1)),flip(a)]. given #31 (A,wt=10): 17 x' * y @ x = y @ x. [para(12(a,1),6(a,1,1)),rewrite(2(3)),flip(a)]. given #32 (F,wt=12): 135 (B @ A') * C != C * (A @ B) # answer(N). [para(91(a,2),7(a,1,1))]. given #33 (F,wt=12): 136 C * (B @ A') != (A @ B) * C # answer(N). [para(91(a,2),7(a,2,2)),flip(a)]. given #34 (T,wt=9): 32 x * y @ x = y @ x. [para(23(a,1),6(a,1,1)),rewrite(2(3)),flip(a)]. given #35 (T,wt=7): 176 (x @ y) @ x = e. [back_rewrite(156),rewrite(166(4),3(2),11(2)),flip(a)]. given #36 (A,wt=12): 19 (x * y)' * x * y * z = z. [para(1(a,1),8(a,1,2))]. given #37 (F,wt=13): 141 (B @ A') * C != C * (B @ A') # answer(N). [para(91(a,2),69(a,2,2)),rewrite(140(4))]. given #38 (F,wt=17): 163 B' * A * B * A' * C != C * (A @ B) # answer(N). [para(9(a,2),135(a,1)),rewrite(88(5))]. given #39 (T,wt=7): 187 (x @ y) @ y = e. [para(91(a,1),176(a,1,1))]. given #40 (T,wt=7): 195 x @ x * x = e. [para(19(a,1),5(a,1,2)),rewrite(3(2)),flip(a)]. given #41 (A,wt=14): 25 (x @ y)' * (x * z @ y) = z @ y. [para(6(a,1),8(a,1,2))]. given #42 (F,wt=18): 139 A' * B' * A * B * C != C * (B @ A') # answer(N). [para(91(a,2),47(a,2,2))]. given #43 (F,wt=18): 153 B * A' * B' * A * C != C * (B @ A') # answer(N). [para(91(a,2),78(a,2,2))]. given #44 (T,wt=8): 183 x' @ (x @ y) = e. [para(176(a,1),64(a,2))]. given #45 (T,wt=7): 281 x @ (y @ x) = e. [para(64(a,1),183(a,1,2)),rewrite(88(2))]. given #46 (A,wt=12): 27 x' * y * x = y * (y @ x). [back_rewrite(24),rewrite(26(4)),flip(a)]. given #47 (F,wt=18): 212 B' * A * B * A' * C != C * (B @ A') # answer(N). [para(9(a,2),141(a,1)),rewrite(88(5))]. given #48 (F,wt=7): 290 x @ (x @ y) = e. [para(64(a,1),281(a,1,2))]. given #49 (T,wt=8): 184 (x @ y) @ y' = e. [para(64(a,1),176(a,1,1))]. given #50 (T,wt=8): 186 x @ (x' @ y) = e. [para(176(a,1),91(a,1)),flip(a)]. given #51 (A,wt=10): 31 x * y' @ y = x @ y. [back_rewrite(18),rewrite(29(5))]. given #52 (F,wt=8): 188 (x @ y') @ y = e. [para(91(a,2),176(a,1,1))]. given #53 (F,wt=8): 216 x' @ (y @ x) = e. [para(187(a,1),64(a,2))]. given #54 (T,wt=8): 217 (x' @ y) @ x = e. [para(64(a,2),187(a,1,1))]. given #55 (T,wt=8): 218 x @ (y @ x') = e. [para(187(a,1),91(a,1)),flip(a)]. given #56 (A,wt=9): 33 x * y @ y = x @ y. [para(23(a,1),6(a,1,2)),rewrite(29(3)),flip(a)]. given #57 (F,wt=8): 219 (x @ y) @ x' = e. [para(91(a,1),187(a,1,1))]. given #58 (F,wt=9): 74 x' @ y' = x @ y. [para(64(a,2),64(a,1))]. given #59 (T,wt=9): 140 x' @ y = x @ y'. [para(91(a,1),64(a,1)),flip(a)]. given #60 (T,wt=9): 190 (x @ y) @ y * x = e. [para(32(a,1),176(a,1,1))]. given #61 (A,wt=21): 34 x * y' * z' * y * z * u = x * (y @ z) * u. [para(9(a,1),1(a,2,2)),rewrite(1(7))]. given #62 (F,wt=9): 209 (x * y)' * x = y'. [para(80(a,1),19(a,1,2,2)),rewrite(29(4))]. given #63 (F,wt=9): 242 (x @ y)' = x' @ y. [para(80(a,1),25(a,1,2,1)),rewrite(11(4),29(4))]. given #64 (T,wt=9): 244 (x @ y) * (y @ x) = e. [para(90(a,1),25(a,2)),rewrite(242(3),74(3),105(4))]. given #65 (T,wt=9): 259 x @ y * x = x @ y. [back_rewrite(233),rewrite(242(3),172(3)),flip(a)]. given #66 (A,wt=13): 38 x' * y * x = (x @ y') * y. [para(3(a,1),9(a,1,2,2,2)),rewrite(29(5),26(4))]. given #67 (F,wt=9): 318 (x @ y) @ (y @ x) = e. [para(290(a,1),17(a,2)),rewrite(242(2),43(3),313(4))]. given #68 (F,wt=9): 366 (x @ y) @ x * y = e. [para(33(a,1),176(a,1,1))]. given #69 (T,wt=9): 408 x * y @ y * x = e. [para(190(a,1),32(a,2)),rewrite(1(3),296(3))]. given #70 (T,wt=9): 518 x @ x * (y @ x) = e. [para(186(a,1),259(a,2)),rewrite(43(3))]. given #71 (A,wt=22): 41 x' * y * x * (y @ z) = (x @ y') * z' * y * z. [para(5(a,1),9(a,1,2,2,2)),rewrite(26(6))]. given #72 (F,wt=9): 590 x @ x * (x @ y) = e. [para(27(a,1),408(a,1,2)),rewrite(1(3),80(2),29(2))]. given #73 (F,wt=10): 105 x * y @ y' = y @ x. [para(80(a,1),10(a,1,2,2,2)),rewrite(88(4),29(4),61(4)),flip(a)]. given #74 (T,wt=10): 162 x @ y' = y @ y * x. [para(17(a,1),91(a,1)),rewrite(88(4))]. given #75 (T,wt=9): 675 x @ x * y = x @ y. [para(162(a,1),64(a,2)),rewrite(88(2)),flip(a)]. given #76 (A,wt=12): 43 (x' @ y) * x = x * (y @ x). [para(5(a,1),9(a,1,2)),rewrite(26(4)),flip(a)]. given #77 (F,wt=10): 172 x' @ x * y = y @ x. [para(32(a,1),64(a,2))]. given #78 (F,wt=10): 189 (x @ y) @ y' * x = e. [para(17(a,1),176(a,1,1))]. given #79 (T,wt=10): 251 (x @ y) @ (x' @ y) = e. [back_rewrite(123),rewrite(242(2),242(5),88(4),6(4),3(2),11(2)),flip(a)]. given #80 (T,wt=10): 254 (x' @ y) @ (x @ y) = e. [back_rewrite(111),rewrite(242(3),88(2),242(3),6(4),80(2),11(2)),flip(a)]. given #81 (A,wt=19): 44 x' * y' * x * y * (z @ y) = x * z @ y. [para(9(a,2),6(a,1))]. given #82 (F,wt=10): 331 (x @ y) @ (y' @ x) = e. [para(186(a,1),32(a,2)),rewrite(43(3),326(5))]. given #83 (F,wt=10): 336 (x @ y) @ x * y' = e. [para(31(a,1),176(a,1,1))]. given #84 (T,wt=10): 343 (x @ y) * (x @ y') = e. [back_rewrite(338),rewrite(342(6))]. given #85 (T,wt=10): 358 (x @ y) @ (x @ y') = e. [para(218(a,1),17(a,2)),rewrite(242(3),74(3),354(5))]. given #86 (A,wt=21): 45 x' * y' * x * y * z @ u = (x @ y) * z @ u. [para(9(a,1),6(a,2,1)),rewrite(6(8))]. given #87 (F,wt=10): 374 (x' @ y) @ y * x = e. [para(32(a,1),219(a,1,1)),rewrite(140(4,R),242(2))]. given #88 (F,wt=10): 377 (x' @ y) @ x * y = e. [para(33(a,1),219(a,1,1)),rewrite(140(4,R),242(2))]. given #89 (T,wt=10): 406 (x @ y) @ x' * y = e. [para(91(a,1),190(a,1,1))]. given #90 (T,wt=10): 407 (x @ y') @ x * y = e. [para(91(a,2),190(a,1,1))]. given #91 (A,wt=16): 48 x' * y * x * z = y * (y @ x) * z. [para(9(a,1),8(a,1,2)),rewrite(26(5)),flip(a)]. given #92 (F,wt=10): 440 (x * y)' = y' * x'. [para(8(a,1),209(a,1,1,1)),flip(a)]. given #93 (F,wt=10): 497 (x @ y') * (x @ y) = e. [para(64(a,1),244(a,1,2))]. given #94 (T,wt=10): 542 x @ y' * x * y = e. [para(38(a,2),259(a,1,2)),rewrite(218(7))]. given #95 (T,wt=10): 547 (x' @ y) @ (y @ x) = e. [para(318(a,1),64(a,2)),rewrite(242(2))]. given #96 (A,wt=17): 50 x' * y * x * z = (x @ y') * y * z. [para(8(a,1),9(a,1,2,2,2)),rewrite(26(5))]. given #97 (F,wt=10): 548 (x @ y') @ (x @ y) = e. [para(64(a,1),318(a,1,2))]. given #98 (F,wt=10): 560 (x @ y) @ y * x' = e. [para(91(a,1),366(a,1,1))]. given #99 (T,wt=10): 561 (x @ y') @ y * x = e. [para(91(a,2),366(a,1,1))]. given #100 (T,wt=10): 573 (x @ y) @ (y @ x') = e. [para(5(a,1),408(a,1,1)),rewrite(1(6),1(5),82(6))]. given #101 (A,wt=16): 52 (x' @ y) * x * z = x * (y @ x) * z. [para(9(a,1),9(a,1,2)),rewrite(26(5)),flip(a)]. given #102 (F,wt=10): 574 (x @ y') @ (y @ x) = e. [para(5(a,1),408(a,1,2)),rewrite(1(5),1(4),82(5))]. given #103 (F,wt=10): 578 x @ y * x * y' = e. [para(8(a,1),408(a,1,1)),rewrite(1(3))]. given #104 (T,wt=11): 108 x * y @ x' = y @ x'. [para(90(a,1),6(a,1,1)),rewrite(2(4)),flip(a)]. given #105 (T,wt=11): 174 x @ x' * y = y @ x'. [para(32(a,1),91(a,1)),flip(a)]. given #106 (A,wt=18): 59 x' * y * z * x = y * z * (y * z @ x). [para(10(a,1),8(a,1,2)),rewrite(26(6),1(4)),flip(a)]. given #107 (F,wt=11): 175 (x @ y) * z @ x = z @ x. [back_rewrite(159),rewrite(166(5),8(3)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.16 (+ 0.00) seconds: N. % Length of proof is 59. % Level of proof is 14. % Maximum clause weight is 24. % Given clauses 107. 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 * z @ y. [assumption]. 7 (A @ B) * C != C * (A @ B) # answer(N). [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))]. 11 e @ x = e. [para(2(a,1),5(a,1,2,2)),rewrite(3(4),3(4)),flip(a)]. 12 x' @ x = e. [para(3(a,1),5(a,1,2,2)),rewrite(8(6)),flip(a)]. 15 (x @ y)' * (z @ y)' * (x * z @ y) = (x @ y) @ (z @ y). [para(6(a,1),5(a,1,2,2))]. 16 (x @ y) * e = x * e @ y. [para(11(a,1),6(a,1,2))]. 17 x' * y @ x = y @ x. [para(12(a,1),6(a,1,1)),rewrite(2(3)),flip(a)]. 18 x * y' @ y = x * e @ y. [para(12(a,1),6(a,1,2)),rewrite(16(3)),flip(a)]. 19 (x * y)' * x * y * z = z. [para(1(a,1),8(a,1,2))]. 21 x'' * e = x. [para(3(a,1),8(a,1,2))]. 23 x @ x = e. [para(8(a,1),5(a,1,2)),rewrite(3(2)),flip(a)]. 25 (x @ y)' * (x * z @ y) = z @ y. [para(6(a,1),8(a,1,2))]. 26 x'' * y = x * y. [para(8(a,1),8(a,1,2))]. 29 x * e = x. [back_rewrite(21),rewrite(26(4))]. 31 x * y' @ y = x @ y. [back_rewrite(18),rewrite(29(5))]. 32 x * y @ x = y @ x. [para(23(a,1),6(a,1,1)),rewrite(2(3)),flip(a)]. 50 x' * y * x * z = (x @ y') * y * z. [para(8(a,1),9(a,1,2,2,2)),rewrite(26(5))]. 56 (x * y')' * y' * x = x @ y. [para(3(a,1),10(a,1,2,2,2)),rewrite(29(6),31(9))]. 61 (x * y)' * y * x = y @ x. [para(8(a,1),10(a,1,2)),rewrite(32(6))]. 64 x' @ y = y @ x. [back_rewrite(56),rewrite(61(6))]. 69 (B' @ A) * C != C * (A @ B) # answer(N). [para(64(a,2),7(a,1,1))]. 74 x' @ y' = x @ y. [para(64(a,2),64(a,1))]. 80 x * x' = e. [para(26(a,1),3(a,1))]. 88 x'' = x. [para(26(a,1),29(a,1)),rewrite(29(2)),flip(a)]. 90 x @ x' = e. [para(88(a,1),12(a,1,1))]. 91 x @ y' = y @ x. [para(88(a,1),64(a,1,1)),flip(a)]. 105 x * y @ y' = y @ x. [para(80(a,1),10(a,1,2,2,2)),rewrite(88(4),29(4),61(4)),flip(a)]. 121 (x' @ y) @ (z @ x) = (y @ x) @ (z @ x). [para(64(a,2),15(a,2,1)),rewrite(15(8)),flip(a)]. 133 (x @ y) * (y @ z') = x * z @ y. [para(91(a,2),6(a,1,2))]. 140 x' @ y = x @ y'. [para(91(a,1),64(a,1)),flip(a)]. 141 (B @ A') * C != C * (B @ A') # answer(N). [para(91(a,2),69(a,2,2)),rewrite(140(4))]. 148 (x @ y)' * (z @ y)' * (y @ (x * z)') = (x @ y) @ (z @ y). [para(91(a,2),15(a,1,2,2))]. 156 x' * y * x @ y = (y @ x) @ y. [para(5(a,1),17(a,1,1)),flip(a)]. 159 x' * y * x * z @ y = (y @ x) * z @ y. [para(9(a,1),17(a,1,1)),flip(a)]. 166 x * y * z @ y = x * z @ y. [para(32(a,1),6(a,1,2)),rewrite(6(3)),flip(a)]. 175 (x @ y) * z @ x = z @ x. [back_rewrite(159),rewrite(166(5),8(3)),flip(a)]. 176 (x @ y) @ x = e. [back_rewrite(156),rewrite(166(4),3(2),11(2)),flip(a)]. 183 x' @ (x @ y) = e. [para(176(a,1),64(a,2))]. 209 (x * y)' * x = y'. [para(80(a,1),19(a,1,2,2)),rewrite(29(4))]. 242 (x @ y)' = x' @ y. [para(80(a,1),25(a,1,2,1)),rewrite(11(4),29(4))]. 244 (x @ y) * (y @ x) = e. [para(90(a,1),25(a,2)),rewrite(242(3),74(3),105(4))]. 264 (x @ y) @ (z @ y) = (x @ z) @ y. [back_rewrite(148),rewrite(242(2),242(4),133(8),6(7),5(5)),flip(a)]. 278 x' * y @ (x @ z) = y @ (x @ z). [para(183(a,1),6(a,1,1)),rewrite(2(4)),flip(a)]. 440 (x * y)' = y' * x'. [para(8(a,1),209(a,1,1,1)),flip(a)]. 497 (x @ y') * (x @ y) = e. [para(64(a,1),244(a,1,2))]. 1174 ((x @ y') @ z') * z * (x @ y) = (x @ y) * z. [para(497(a,1),50(a,1,2,2)),rewrite(242(3),74(3),29(3)),flip(a)]. 1422 (x' @ y) @ (z @ x) = e. [para(175(a,1),183(a,1,2)),rewrite(440(3),242(3),278(6))]. 1448 (x @ y) @ (z @ y) = e. [back_rewrite(121),rewrite(1422(4)),flip(a)]. 1452 (x @ y) @ z = e. [back_rewrite(264),rewrite(1448(3)),flip(a)]. 1465 (x @ y) * z = z * (x @ y). [back_rewrite(1174),rewrite(1452(4),2(4)),flip(a)]. 1466 $F # answer(N). [resolve(1465,a,141,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=107. Generated=8140. Kept=1464. proofs=1. Usable=80. Sos=895. Demods=661. 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=104653. 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.16, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11356 exit (max_proofs) Sat Aug 12 20:59:57 2006