============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 11599 was started by mccune on cleo, Wed Feb 25 09:32:54 2009 The command was "/home/mccune/bin/prover9 -f cs.in DA.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file cs.in assign(max_seconds,30). op(450,infix,@). op(400,infix_right,*). assign(new_constants,1). assign(max_weight,25). formulas(sos). x * y != x * z | y = z. y * x != z * x | y = z. (x * y) * z = x * y * z. y * x * (x @ y) = x * y. end_of_list. % Reading from file DA.in formulas(sos). (x @ z) * (y @ z) = x * y @ z. 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 != x * z | y = z. [assumption]. x * y != z * y | x = z. [assumption]. (x * y) * z = x * y * z. [assumption]. x * y * (y @ x) = y * x. [assumption]. (x @ y) * (z @ y) = x * z @ 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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ A, B, C, D, F, G, *, @ ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 2). % (nonunit Horn with equality) Auto_process settings: (no changes). kept: 1 x * y != x * z | y = z. [assumption]. kept: 2 x * y != z * y | x = z. [assumption]. kept: 3 (x * y) * z = x * y * z. [assumption]. kept: 4 x * y * (y @ x) = y * x. [assumption]. 5 (x @ y) * (z @ y) = x * z @ y. [assumption]. kept: 6 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. kept: 7 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 x * y != x * z | y = z. [assumption]. 2 x * y != z * y | x = z. [assumption]. 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 6 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. 7 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. end_of_list. formulas(demodulators). 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 6 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=10): 1 x * y != x * z | y = z. [assumption]. given #2 (I,wt=10): 2 x * y != z * y | x = z. [assumption]. given #3 (I,wt=11): 3 (x * y) * z = x * y * z. [assumption]. given #4 (I,wt=11): 4 x * y * (y @ x) = y * x. [assumption]. given #5 (I,wt=13): 6 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. given #6 (I,wt=11): 7 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. given #7 (A,wt=14): 8 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite([3(4)])]. given #8 (F,wt=15): 18 ((A @ B) @ C) * x != (D @ (F @ G)) * x # answer(A). [ur(2,b,7,a)]. given #9 (F,wt=15): 19 x * ((A @ B) @ C) != x * (D @ (F @ G)) # answer(A). [ur(1,b,7,a)]. given #10 (F,wt=19): 20 x * y * ((A @ B) @ C) != x * y * (D @ (F @ G)) # answer(A). [ur(8,b,7,a)]. given #11 (F,wt=17): 29 C * (A @ B) * (D @ (F @ G)) != (A @ B) * C # answer(A). [para(4(a,1),20(a,1)),flip(a)]. given #12 (T,wt=7): 10 x * (x @ x) = x. [hyper(1,a,4,a)]. given #13 (T,wt=10): 34 x * y != x | x @ x = y. [para(10(a,1),1(a,1)),flip(a)]. given #14 (T,wt=10): 35 x * (y @ y) != y | y = x. [para(10(a,1),2(a,1)),flip(a)]. given #15 (T,wt=10): 36 x * (y @ y) != y | x = y. [para(10(a,1),2(a,2))]. given #16 (A,wt=14): 9 x * y * z != u * z | x * y = u. [para(3(a,1),2(a,1))]. given #17 (F,wt=17): 30 (F @ G) * D * ((A @ B) @ C) != D * (F @ G) # answer(A). [para(4(a,1),20(a,2))]. given #18 (F,wt=19): 25 x * ((A @ B) @ C) * y != x * (D @ (F @ G)) * y # answer(A). [ur(1,b,18,a)]. given #19 (F,wt=21): 32 C * (A @ B) * (D @ (F @ G)) * x != (A @ B) * C * x # answer(A). [ur(2,b,29,a),rewrite([3(12),3(11),3(18)])]. given #20 (F,wt=21): 33 x * C * (A @ B) * (D @ (F @ G)) != x * (A @ B) * C # answer(A). [ur(1,b,29,a)]. given #21 (T,wt=11): 37 x * (x @ x) * y = x * y. [para(10(a,1),3(a,1,1)),flip(a)]. given #22 (T,wt=7): 62 (x @ x) * y = y. [hyper(8,a,37,a)]. given #23 (T,wt=9): 69 x * ((y @ y) @ x) = x. [para(62(a,1),4(a,1,2)),rewrite([62(5)])]. given #24 (T,wt=9): 76 (x @ x) @ y = y @ y. [hyper(34,a,69,a),flip(a)]. given #25 (A,wt=14): 11 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. given #26 (F,wt=21): 53 (F @ G) * D * ((A @ B) @ C) * x != D * (F @ G) * x # answer(A). [ur(9,b,30,a),rewrite([3(11),3(18)])]. given #27 (F,wt=21): 55 x * (F @ G) * D * ((A @ B) @ C) != x * D * (F @ G) # answer(A). [ur(1,b,30,a)]. given #28 (F,wt=21): 61 C * (A @ B) * (D @ (F @ G)) * (C @ C) != (A @ B) * C # answer(A). [para(10(a,1),32(a,2,2))]. given #29 (F,wt=21): 85 (D @ (F @ G)) * ((x @ x) @ ((A @ B) @ C)) != (A @ B) @ C # answer(A). [para(69(a,1),18(a,1)),flip(a)]. given #30 (T,wt=6): 105 x != y | y = x. [para(10(a,1),11(a,2)),rewrite([62(2),70(4),10(3)])]. given #31 (T,wt=9): 96 ((x @ x) @ y) * z = z. [para(76(a,2),62(a,1,1))]. given #32 (T,wt=9): 100 x * (x @ x * x) = x. [hyper(11,a,3,a)]. given #33 (T,wt=9): 126 x @ x * x = x @ x. [hyper(34,a,100,a),flip(a)]. given #34 (A,wt=14): 12 x * y * (y @ z) != y * z | z = x. [para(4(a,1),2(a,1)),flip(a)]. given #35 (F,wt=21): 86 ((A @ B) @ C) * ((x @ x) @ (D @ (F @ G))) != D @ (F @ G) # answer(A). [para(69(a,1),18(a,2))]. given #36 (F,wt=23): 24 x * y * ((A @ B) @ C) * z != x * y * (D @ (F @ G)) * z # answer(A). [ur(8,b,18,a)]. given #37 (F,wt=23): 26 (D @ (F @ G)) * x * (x @ ((A @ B) @ C)) != x * ((A @ B) @ C) # answer(A). [para(4(a,1),18(a,1)),flip(a)]. given #38 (F,wt=23): 27 ((A @ B) @ C) * x * (x @ (D @ (F @ G))) != x * (D @ (F @ G)) # answer(A). [para(4(a,1),18(a,2))]. given #39 (T,wt=10): 68 x * y != y | z @ z = x. [para(62(a,1),2(a,1)),flip(a)]. NOTE: New constant: x @ x = c_0. [new_symbol(136)]. NOTE: New Function symbol precedence: function_order([ A, B, C, D, F, G, c_0, *, @ ]). given #40 (T,wt=5): 138 x @ x = c_0. [new_symbol(136)]. given #41 (T,wt=5): 140 c_0 @ x = c_0. [back_rewrite(135),rewrite([138(1),138(3)])]. given #42 (T,wt=5): 146 c_0 * x = x. [back_rewrite(124),rewrite([138(1),140(2),140(2)])]. given #43 (A,wt=14): 13 x * y * (y @ z) != y * z | x = z. [para(4(a,1),2(a,2))]. given #44 (F,wt=23): 28 x * y * z * ((A @ B) @ C) != x * y * z * (D @ (F @ G)) # answer(A). [ur(8,b,19,a)]. given #45 (F,wt=23): 56 x * (D @ (F @ G)) * (((A @ B) @ C) @ x) != ((A @ B) @ C) * x # answer(A). [para(4(a,1),25(a,1)),flip(a)]. given #46 (F,wt=19): 161 (D @ (F @ G)) * (((A @ B) @ C) @ c_0) != (A @ B) @ C # answer(A). [para(146(a,1),56(a,1)),rewrite([155(20)])]. given #47 (F,wt=23): 57 x * ((A @ B) @ C) * ((D @ (F @ G)) @ x) != (D @ (F @ G)) * x # answer(A). [para(4(a,1),25(a,2))]. given #48 (T,wt=5): 155 x * c_0 = x. [back_rewrite(97),rewrite([138(1),140(2),140(2)])]. given #49 (T,wt=7): 144 x @ x * x = c_0. [back_rewrite(126),rewrite([138(3)])]. given #50 (T,wt=7): 159 x * (x @ c_0) = x. [back_rewrite(150),rewrite([155(5)])]. given #51 (T,wt=8): 145 x * y != x | c_0 = y. [back_rewrite(125),rewrite([138(3),140(4),140(4)])]. given #52 (A,wt=15): 14 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite([3(2),3(5)]),flip(a)]. given #53 (F,wt=23): 60 C * (A @ B) * (D @ (F @ G)) * (C @ (A @ B)) != C * (A @ B) # answer(A). [para(4(a,1),32(a,2))]. given #54 (F,wt=23): 110 (F @ G) * D * ((A @ B) @ C) * ((F @ G) @ D) != (F @ G) * D # answer(A). [para(4(a,1),53(a,2))]. given #55 (F,wt=25): 31 x * y * C * (A @ B) * (D @ (F @ G)) != x * y * (A @ B) * C # answer(A). [ur(8,b,29,a)]. given #56 (F,wt=21): 201 B * A * C * (A @ B) * (D @ (F @ G)) != A * B * C # answer(A). [para(14(a,1),31(a,2))]. given #57 (T,wt=5): 183 x @ c_0 = c_0. [hyper(145,a,159,a),flip(a)]. given #58 (T,wt=8): 149 x * y != y | c_0 = x. [back_rewrite(117),rewrite([138(3),140(4)])]. given #59 (T,wt=10): 129 x * y != y * y | y = x. [para(10(a,1),12(a,1,2))]. given #60 (T,wt=12): 142 x * (x @ y) != x * y | c_0 = y. [back_rewrite(132),rewrite([138(5),140(6)])]. given #61 (A,wt=17): 15 x * y * z * (z @ x * y) = z * x * y. [para(4(a,1),3(a,1)),flip(a)]. given #62 (F,wt=25): 54 x * y * (F @ G) * D * ((A @ B) @ C) != x * y * D * (F @ G) # answer(A). [ur(8,b,30,a)]. given #63 (F,wt=21): 220 F * G * D * ((A @ B) @ C) != G * F * D * (F @ G) # answer(A). [para(14(a,1),54(a,1))]. given #64 (F,wt=25): 58 x * C * (A @ B) * (D @ (F @ G)) * y != x * (A @ B) * C * y # answer(A). [ur(1,b,32,a)]. given #65 (F,wt=25): 59 C * (A @ B) * (D @ (F @ G)) * x * (x @ C) != (A @ B) * x * C # answer(A). [para(4(a,1),32(a,2,2))]. given #66 (T,wt=12): 147 x * y * z != z | x * y = c_0. [back_rewrite(122),rewrite([138(4),140(5)]),flip(b)]. given #67 (T,wt=12): 154 x * y != y | x * (x @ y) = c_0. [back_rewrite(106),rewrite([138(3),140(4)]),flip(b)]. given #68 (T,wt=12): 158 x * y * z != x * y | c_0 = z. [back_rewrite(84),rewrite([138(5),140(6)])]. given #69 (T,wt=12): 225 x @ y != x * y | y * x = c_0. [para(4(a,1),147(a,1)),flip(a)]. given #70 (A,wt=19): 16 x * y * z * (y @ x) * (z @ x) = y * z * x. [para(3(a,1),4(a,1,2)),rewrite([6(2),3(8)])]. given #71 (F,wt=25): 108 x * (F @ G) * D * ((A @ B) @ C) * y != x * D * (F @ G) * y # answer(A). [ur(1,b,53,a)]. given #72 (F,wt=25): 109 D * (F @ G) * (((A @ B) @ C) @ D) != (F @ G) * ((A @ B) @ C) * D # answer(A). [para(4(a,1),53(a,1,2)),flip(a)]. given #73 (F,wt=25): 134 (F @ G) * ((A @ B) @ C) * D * (D @ (D @ (F @ G))) != D * (F @ G) # answer(A). [ur(11,b,27,a(flip))]. given #74 (F,wt=25): 202 B * A * C * (A @ B) * (D @ (F @ G)) * x != A * B * C * x # answer(A). [ur(9,b,201,a),rewrite([3(15),3(14),3(13),3(22),3(21)])]. given #75 (T,wt=12): 234 x * y != y * x | x @ y = c_0. [para(4(a,1),158(a,1)),flip(b)]. given #76 (T,wt=13): 157 (x @ x * y) * (y @ x * y) = c_0. [back_rewrite(94),rewrite([138(1),140(3)]),flip(a)]. given #77 (T,wt=13): 207 x * y * (y @ y * x) = y * x. [hyper(1,a,15,a)]. given #78 (T,wt=13): 266 x * (x @ x * y) = x * (x @ y). [hyper(11,a,207,a),flip(a)]. given #79 (A,wt=21): 17 (x @ y) * (z @ y) * ((z @ x) @ y) = (z @ y) * (x @ y). [para(4(a,1),6(a,1,1)),rewrite([6(2),6(7)]),flip(a)]. given #80 (F,wt=21): 320 (B @ C) * (A @ C) * (D @ (F @ G)) != (A @ C) * (B @ C) # answer(A). [para(17(a,1),20(a,1)),flip(a)]. given #81 (F,wt=25): 203 x * B * A * C * (A @ B) * (D @ (F @ G)) != x * A * B * C # answer(A). [ur(1,b,201,a)]. given #82 (F,wt=25): 221 F * G * D * ((A @ B) @ C) * x != G * F * D * (F @ G) * x # answer(A). [ur(9,b,220,a),rewrite([3(11),3(10),3(22),3(21),3(20)])]. given #83 (F,wt=21): 335 F * G * D * ((A @ B) @ C) * (D @ G) != F * D * G # answer(A). [para(16(a,1),221(a,2))]. given #84 (T,wt=9): 278 x @ x * y = x @ y. [hyper(1,a,266,a)]. given #85 (T,wt=11): 293 (x @ y * x) * (y @ x) = c_0. [back_rewrite(277),rewrite([278(4)])]. given #86 (T,wt=11): 307 (x @ y) * (y @ x * y) = c_0. [back_rewrite(157),rewrite([278(2)])]. given #87 (T,wt=9): 376 (x @ y) @ x * y = c_0. [para(4(a,1),307(a,1,2,2)),rewrite([339(3),6(6),278(4),351(8)])]. given #88 (A,wt=18): 21 x * y * z * u != x * y * z * w | u = w. [para(3(a,1),8(a,1,2)),rewrite([3(5)])]. given #89 (F,wt=15): 357 (C @ (A @ B) * C) * (D @ (F @ G)) != c_0 # answer(A). [para(293(a,1),19(a,1)),flip(a)]. given #90 (F,wt=15): 377 (D @ (F @ G)) * (C @ (A @ B) * C) != c_0 # answer(A). [para(307(a,1),18(a,1)),flip(a)]. given #91 (F,wt=17): 358 ((F @ G) @ D * (F @ G)) * ((A @ B) @ C) != c_0 # answer(A). [para(293(a,1),19(a,2))]. given #92 (F,wt=17): 359 x * (C @ (A @ B) * C) * (D @ (F @ G)) != x # answer(A). [para(293(a,1),20(a,1,2)),rewrite([155(2)]),flip(a)]. given #93 (T,wt=11): 372 (x @ y * x) @ (y @ x) = c_0. [para(293(a,1),234(a,1)),rewrite([307(5)]),xx(a)]. given #94 (T,wt=11): 373 (x @ y) @ (y @ x * y) = c_0. [para(293(a,1),234(a,2)),rewrite([307(4)]),xx(a)]. given #95 (T,wt=11): 397 (x @ y * x) @ y * x = c_0. [para(4(a,1),376(a,1,2)),rewrite([339(3)])]. given #96 (T,wt=11): 407 (x @ y) @ x * x * y = c_0. [para(278(a,1),376(a,1,1))]. given #97 (A,wt=18): 22 x * y * z != x * u * y | u * (u @ y) = z. [para(4(a,1),8(a,1,2)),flip(a)]. given #98 (F,wt=17): 378 ((A @ B) @ C) * ((F @ G) @ D * (F @ G)) != c_0 # answer(A). [para(307(a,1),18(a,2))]. given #99 (F,wt=17): 379 x * (D @ (F @ G)) * (C @ (A @ B) * C) != x # answer(A). [para(307(a,1),25(a,1,2)),rewrite([155(2)]),flip(a)]. given #100 (F,wt=17): 420 (C @ (A @ B) * C) * (D @ (F @ G)) * x != x # answer(A). [ur(147,b,357,a)]. given #101 (F,wt=17): 422 (D @ (F @ G)) * (C @ (A @ B) * C) * x != x # answer(A). [ur(147,b,377,a)]. given #102 (T,wt=10): 459 x * y != x * z | z = y. [para(146(a,1),22(a,1,2)),rewrite([155(3),183(5),155(5)])]. given #103 (T,wt=11): 447 (x @ y * x) @ x * y = c_0. [para(397(a,1),278(a,2)),rewrite([439(6)])]. given #104 (T,wt=12): 284 x * (x @ y) != x | x @ y = c_0. [para(266(a,1),145(a,1)),rewrite([278(6)]),flip(b)]. given #105 (T,wt=12): 297 x @ y * x != c_0 | y @ x = c_0. [back_rewrite(262),rewrite([278(6)])]. given #106 (A,wt=14): 23 x * y * z != y * x | y @ x = z. [para(4(a,1),8(a,1)),flip(a)]. given #107 (F,wt=17): 469 (F @ G) @ D * (F @ G) != C @ (A @ B) * C # answer(A). [para(307(a,1),420(a,1,2)),rewrite([155(9)]),flip(a)]. given #108 (F,wt=19): 360 x * ((F @ G) @ D * (F @ G)) * ((A @ B) @ C) != x # answer(A). [para(293(a,1),20(a,2,2)),rewrite([155(18)])]. given #109 (F,wt=19): 380 x * ((A @ B) @ C) * ((F @ G) @ D * (F @ G)) != x # answer(A). [para(307(a,1),25(a,2,2)),rewrite([155(18)])]. given #110 (F,wt=19): 382 D * (F @ G) * (C @ (A @ B) * C) != (F @ G) * D # answer(A). [para(307(a,1),53(a,1,2,2)),rewrite([155(6)]),flip(a)]. given #111 (T,wt=12): 298 x @ y != c_0 | y @ x * y = c_0. [back_rewrite(260),rewrite([278(2)])]. given #112 (T,wt=12): 495 x * y != y * x | y @ x = c_0. [para(155(a,1),23(a,1,2))]. given #113 (T,wt=13): 310 (x @ y) * (y @ x * y) * z = z. [back_rewrite(72),rewrite([278(2)])]. given #114 (T,wt=9): 536 ((x @ y) @ z) @ z = c_0. [para(310(a,1),376(a,1,2)),rewrite([534(5)])]. given #115 (A,wt=18): 47 x * y * z * u != w * u | x * y * z = w. [para(3(a,1),9(a,1,2))]. given #116 (F,wt=19): 383 (F @ G) * D * ((A @ B) @ C) * (G @ F * G) != D # answer(A). [para(307(a,1),53(a,2,2)),rewrite([155(20)])]. given #117 (F,wt=19): 424 ((F @ G) @ D * (F @ G)) * ((A @ B) @ C) * x != x # answer(A). [ur(147,b,358,a)]. given #118 (F,wt=19): 464 ((A @ B) @ C) * ((F @ G) @ D * (F @ G)) * x != x # answer(A). [ur(147,b,378,a)]. given #119 (F,wt=21): 366 x * y * (C @ (A @ B) * C) * (D @ (F @ G)) != x * y # answer(A). [para(293(a,1),28(a,1,2,2)),rewrite([155(2)]),flip(a)]. given #120 (T,wt=9): 559 x @ ((y @ z) @ x) = c_0. [para(536(a,1),293(a,1,2)),rewrite([550(3),278(4),155(5)])]. given #121 (T,wt=11): 582 (x @ y) @ ((x @ y) @ z) = c_0. [para(278(a,1),559(a,1,2)),rewrite([6(5),559(7),155(6)])]. given #122 (T,wt=13): 322 (x @ y) * ((x @ y) @ y) = x @ y. [para(138(a,1),17(a,1,1)),rewrite([146(6),138(6),155(7)])]. given #123 (T,wt=7): 589 (x @ y) @ y = c_0. [hyper(284,a,322,a)]. given #124 (A,wt=18): 48 x * y * z != u * w * z | x * y = u * w. [para(3(a,1),9(a,2))]. given #125 (F,wt=15): 578 C * ((A @ B) @ C) != (D @ (F @ G)) * C # answer(A). [para(559(a,1),26(a,1,2,2)),rewrite([155(8)]),flip(a)]. given #126 (F,wt=17): 612 (F @ G) * ((A @ B) @ C) * D != D * (F @ G) # answer(A). [back_rewrite(134),rewrite([605(16),155(11)])]. given #127 (F,wt=19): 586 (A @ B) * ((A @ B) @ C) != (D @ (F @ G)) * (A @ B) # answer(A). [para(582(a,1),26(a,1,2,2)),rewrite([155(10)]),flip(a)]. given #128 (F,wt=17): 632 C * (D @ (F @ G)) * (A @ B) != (A @ B) * C # answer(A). [ur(11,b,586,a)]. given #129 (T,wt=7): 597 x @ (y @ x) = c_0. [hyper(298,a,589,a),rewrite([590(2),278(3)])]. given #130 (T,wt=7): 605 x @ (x @ y) = c_0. [back_rewrite(409),rewrite([597(2),146(4)])]. given #131 (T,wt=9): 610 x @ (y @ x * y) = c_0. [back_rewrite(485),rewrite([605(3),146(5)])]. given #132 (T,wt=11): 590 (x @ y) * y = y * (x @ y). [para(322(a,1),4(a,1,2)),flip(a)]. given #133 (A,wt=18): 49 x * y * (y @ z) != u * y * z | u * z = x. [para(4(a,1),9(a,1,2)),flip(a)]. given #134 (F,wt=15): 647 ((A @ B) @ C) * D != D * (D @ (F @ G)) # answer(A). [para(605(a,1),27(a,1,2,2)),rewrite([155(8)])]. given #135 (F,wt=17): 696 (D @ (F @ G)) * C * (A @ B) != (A @ B) * C # answer(A). [para(590(a,1),422(a,1,2)),rewrite([3(18),386(18)])]. given #136 (F,wt=17): 701 ((A @ B) @ C) * (F @ G) * D != D * (F @ G) # answer(A). [para(590(a,1),464(a,1,2)),rewrite([3(20),386(20)])]. given #137 (F,wt=19): 623 x * C * ((A @ B) @ C) != x * (D @ (F @ G)) * C # answer(A). [ur(459,b,578,a),flip(a)]. given #138 (T,wt=10): 707 x * y != z * y | z = x. [para(155(a,1),49(a,2,2)),rewrite([183(2),155(2),155(5)])]. given #139 (T,wt=11): 604 (x @ y) @ y * (x @ y) = c_0. [para(589(a,1),278(a,2)),rewrite([590(3)])]. given #140 (T,wt=11): 636 x @ (y @ x) * (z @ x) = c_0. [para(6(a,1),597(a,1,2))]. given #141 (T,wt=11): 643 (x @ y) @ x * (x @ y) = c_0. [hyper(298,a,605,a)]. given #142 (A,wt=14): 50 x * (y @ z) != y * z | z * y = x. [para(4(a,1),9(a,1)),flip(a)]. given #143 (F,wt=19): 624 C * ((A @ B) @ C) * x != (D @ (F @ G)) * C * x # answer(A). [ur(48,b,578,a)]. given #144 (F,wt=17): 749 (D @ (F @ G)) * C * (C @ (A @ B) * C) != C # answer(A). [para(307(a,1),624(a,1,2)),rewrite([155(3)]),flip(a)]. given #145 (F,wt=19): 638 ((A @ B) @ C) * (F @ G) != (F @ G) * (D @ (F @ G)) # answer(A). [para(597(a,1),27(a,1,2,2)),rewrite([155(10)])]. given #146 (F,wt=19): 700 ((F @ G) @ D * (F @ G)) * C * ((A @ B) @ C) != C # answer(A). [para(590(a,1),424(a,1,2))]. given #147 (T,wt=11): 644 (x @ y) * x = x * (x @ y). [para(605(a,1),4(a,1,2,2)),rewrite([155(3)])]. given #148 (T,wt=7): 758 (x @ y) @ x = c_0. [hyper(234,a,644,a)]. given #149 (T,wt=11): 736 x @ (x @ y) * (x @ y) = c_0. [para(643(a,1),293(a,1,2)),rewrite([648(6),6(7),278(5),735(10),155(6),155(6)])]. given #150 (T,wt=12): 639 x * (y @ x) != x | y @ x = c_0. [para(597(a,1),142(a,1,2)),rewrite([155(2)]),flip(a),flip(b)]. given #151 (A,wt=18): 51 x * y * z * (z @ u) != z * u | x * y = u. [para(4(a,1),9(a,2))]. given #152 (F,wt=17): 782 (C @ (A @ B) * C) * D * (D @ (F @ G)) != D # answer(A). [para(644(a,1),420(a,1,2))]. given #153 (F,wt=19): 714 x * ((A @ B) @ C) * D != x * D * (D @ (F @ G)) # answer(A). [ur(459,b,647,a),flip(a)]. given #154 (F,wt=19): 716 ((A @ B) @ C) * D * x != D * (D @ (F @ G)) * x # answer(A). [ur(48,b,647,a)]. given #155 (F,wt=19): 751 C * C * ((A @ B) @ C) != (D @ (F @ G)) * C * C # answer(A). [para(590(a,1),624(a,1,2))]. given #156 (T,wt=13): 339 x @ y * (y @ x) = x @ y * x. [para(4(a,1),278(a,1,2)),flip(a)]. given #157 (T,wt=9): 816 (x @ y * x) @ y = c_0. [para(610(a,1),339(a,1,2,2)),rewrite([155(4),658(9)])]. given #158 (T,wt=13): 351 (x @ y * x) * (y @ x) * z = z. [para(293(a,1),3(a,1,1)),rewrite([146(2)]),flip(a)]. given #159 (T,wt=13): 386 x * y * (y @ x * y) = y * x. [para(307(a,1),14(a,1,2,2)),rewrite([155(2)]),flip(a)]. given #160 (A,wt=20): 101 x * y * z != u * x * y | u * (u @ x * y) = z. [para(3(a,1),11(a,1))]. given #161 (F,wt=11): 991 D @ (G @ F) != C @ (A @ B) # answer(A). [back_rewrite(469),rewrite([874(9),911(5),874(12)])]. given #162 (F,wt=11): 1119 D @ (F @ G) != C @ (B @ A) # answer(A). [back_rewrite(7),rewrite([911(5)]),flip(a)]. given #163 (F,wt=13): 1021 (C @ (B @ A)) * (D @ (G @ F)) != c_0 # answer(A). [back_rewrite(378),rewrite([911(5),874(14),911(10)])]. given #164 (F,wt=13): 1022 (D @ (F @ G)) * (C @ (A @ B)) != c_0 # answer(A). [back_rewrite(377),rewrite([874(12)])]. given #165 (T,wt=9): 874 x @ y * x = x @ y. [hyper(23,a,386,a),flip(a)]. given #166 (T,wt=9): 884 (x @ y) * (y @ x) = c_0. [para(386(a,1),293(a,1,1,2)),rewrite([874(2),6(4),278(2),376(4),155(3),874(3),339(4),874(3)])]. given #167 (T,wt=9): 886 (x @ y) @ (y @ x) = c_0. [para(386(a,1),372(a,1,1,2)),rewrite([874(2),6(4),278(2),376(4),155(3),874(3),339(4),874(3)])]. given #168 (T,wt=10): 894 x @ y != c_0 | y @ x = c_0. [para(386(a,1),297(a,1,2)),rewrite([874(2),6(4),278(2),376(4),155(3),874(5),339(6),874(5)])]. given #169 (A,wt=22): 102 x * y * z != z * u | x * y * (x @ z) * (y @ z) = u. [para(3(a,1),11(a,2)),rewrite([6(7),3(9)]),flip(a)]. given #170 (F,wt=13): 1031 (D @ (G @ F)) * (C @ (B @ A)) != c_0 # answer(A). [back_rewrite(358),rewrite([874(9),911(5),911(10)])]. given #171 (F,wt=13): 1032 (C @ (A @ B)) * (D @ (F @ G)) != c_0 # answer(A). [back_rewrite(357),rewrite([874(7)])]. given #172 (F,wt=15): 958 (C @ (B @ A)) * D * (D @ (G @ F)) != D # answer(A). [back_rewrite(807),rewrite([911(5),874(15),911(11)])]. given #173 (F,wt=15): 964 (C @ (A @ B)) * D * (D @ (F @ G)) != D # answer(A). [back_rewrite(782),rewrite([874(7)])]. given #174 (T,wt=11): 896 (x @ y) * (y @ x) * z = z. [para(386(a,1),310(a,1,2,1,2)),rewrite([874(2),339(3),874(2),874(3),6(5),278(3),376(5),155(4)])]. given #175 (T,wt=11): 911 (x @ y) @ z = z @ (y @ x). [back_rewrite(872),rewrite([874(4),874(5)])]. given #176 (T,wt=11): 916 (x @ y) @ ((y @ x) @ z) = c_0. [back_rewrite(867),rewrite([874(2)])]. given #177 (T,wt=11): 925 (x @ y) @ (z @ (y @ x)) = c_0. [back_rewrite(858),rewrite([874(5),911(7),6(7),597(4),6(6),605(4),146(7),146(6)])]. given #178 (A,wt=18): 103 x * y != z * y | z * (z @ y) = x * (x @ y). [para(4(a,1),11(a,1))]. given #179 (F,wt=15): 970 (D @ (F @ G)) * C * (C @ (A @ B)) != C # answer(A). [back_rewrite(749),rewrite([874(13)])]. given #180 (F,wt=15): 972 (D @ (G @ F)) * C * (C @ (B @ A)) != C # answer(A). [back_rewrite(700),rewrite([874(9),911(5),911(11)])]. given #181 (F,wt=15): 985 (D @ (G @ F)) * x != (C @ (A @ B)) * x # answer(A). [back_rewrite(505),rewrite([874(9),911(5),874(13)])]. given #182 (F,wt=15): 987 x * (D @ (G @ F)) != x * (C @ (A @ B)) # answer(A). [back_rewrite(503),rewrite([874(9),911(5),874(13)])]. given #183 (T,wt=11): 955 (x @ y) @ y * (y @ x) = c_0. [back_rewrite(815),rewrite([874(2)])]. given #184 (T,wt=11): 1038 x @ y * (y @ x) = x @ y. [back_rewrite(339),rewrite([874(5)])]. given #185 (T,wt=11): 1141 (x @ y) @ (x @ y * y) = c_0. [back_rewrite(1094),rewrite([1127(4)])]. given #186 (T,wt=11): 1153 (x @ y) @ (y @ x * x) = c_0. [back_rewrite(438),rewrite([1127(4)])]. given #187 (A,wt=22): 127 x * y * z * (y @ u) * (z @ u) != y * z * u | u = x. [para(3(a,1),12(a,1,2)),rewrite([6(2),3(8)])]. given #188 (F,wt=15): 995 (C @ (B @ A)) * (D @ (G @ F)) * x != x # answer(A). [back_rewrite(464),rewrite([911(5),874(14),911(10)])]. given #189 (F,wt=15): 1002 (D @ (G @ F)) * (C @ (B @ A)) * x != x # answer(A). [back_rewrite(424),rewrite([874(9),911(5),911(10)])]. given #190 (F,wt=15): 1004 (D @ (F @ G)) * (C @ (A @ B)) * x != x # answer(A). [back_rewrite(422),rewrite([874(12)])]. given #191 (F,wt=15): 1006 (C @ (A @ B)) * (D @ (F @ G)) * x != x # answer(A). [back_rewrite(420),rewrite([874(7)])]. given #192 (T,wt=12): 939 (x @ y) * z != z | y @ x = c_0. [back_rewrite(843),rewrite([874(5)])]. given #193 (T,wt=12): 942 x @ y != z | (y @ x) * z = c_0. [back_rewrite(839),rewrite([874(2)])]. given #194 (T,wt=12): 971 x * y != c_0 | y @ x = y * x. [back_rewrite(745),rewrite([874(5)])]. given #195 (T,wt=12): 1023 x * (y @ z) != x | z @ y = c_0. [back_rewrite(371),rewrite([874(2)])]. given #196 (A,wt=22): 160 x * y * z * (y @ u) * (z @ u) != y * z * u | x = u. [para(3(a,1),13(a,1,2)),rewrite([6(2),3(8)])]. given #197 (F,wt=15): 1019 x * (C @ (B @ A)) * (D @ (G @ F)) != x # answer(A). [back_rewrite(380),rewrite([911(5),874(14),911(10)])]. given #198 (F,wt=15): 1020 x * (D @ (F @ G)) * (C @ (A @ B)) != x # answer(A). [back_rewrite(379),rewrite([874(12)])]. given #199 (F,wt=15): 1029 x * (D @ (G @ F)) * (C @ (B @ A)) != x # answer(A). [back_rewrite(360),rewrite([874(9),911(5),911(10)])]. given #200 (F,wt=15): 1030 x * (C @ (A @ B)) * (D @ (F @ G)) != x # answer(A). [back_rewrite(359),rewrite([874(7)])]. given #201 (T,wt=12): 1024 x @ y != z | z * (y @ x) = c_0. [back_rewrite(369),rewrite([874(4)])]. given #202 (T,wt=12): 1035 x * (y @ z) != c_0 | z @ y = x. [back_rewrite(350),rewrite([874(6)])]. given #203 (T,wt=12): 1036 (x @ y) * z != c_0 | y @ x = z. [back_rewrite(349),rewrite([874(2)])]. given #204 (T,wt=12): 1311 (x @ y) * z != z | x @ y = c_0. [para(896(a,1),939(a,1)),flip(a)]. given #205 (A,wt=18): 184 x * y * z != y * u | x * (x @ y) * z = u. [para(14(a,1),1(a,1))]. given #206 (F,wt=15): 1049 (D @ (F @ G)) * C != C * (C @ (B @ A)) # answer(A). [back_rewrite(578),rewrite([911(6)]),flip(a)]. given #207 (F,wt=15): 1084 D * (D @ (F @ G)) != (C @ (B @ A)) * D # answer(A). [back_rewrite(647),rewrite([911(5)]),flip(a)]. given #208 (F,wt=15): 1117 x * (D @ (F @ G)) != x * (C @ (B @ A)) # answer(A). [back_rewrite(19),rewrite([911(5)]),flip(a)]. given #209 (F,wt=15): 1118 (D @ (F @ G)) * x != (C @ (B @ A)) * x # answer(A). [back_rewrite(18),rewrite([911(5)]),flip(a)]. given #210 (T,wt=12): 1345 c_0 != x | (y @ z) * x = y @ z. [para(896(a,1),1036(a,1)),flip(a),flip(b)]. given #211 (T,wt=13): 491 (x @ y) @ (z @ y) = (x @ z) @ y. [hyper(23,a,17,a)]. ============================== PROOF ================================= % Proof 1 at 0.30 (+ 0.01) seconds: A. % Length of proof is 91. % Level of proof is 26. % Maximum clause weight is 23. % Given clauses 211. 1 x * y != x * z | y = z. [assumption]. 2 x * y != z * y | x = z. [assumption]. 3 (x * y) * z = x * y * z. [assumption]. 4 x * y * (y @ x) = y * x. [assumption]. 5 (x @ y) * (z @ y) = x * z @ y. [assumption]. 6 x * y @ z = (x @ z) * (y @ z). [copy(5),flip(a)]. 7 (A @ B) @ C != D @ (F @ G) # answer(A). [assumption]. 8 x * y * z != x * y * u | z = u. [para(3(a,1),1(a,1)),rewrite([3(4)])]. 10 x * (x @ x) = x. [hyper(1,a,4,a)]. 11 x * y != z * x | z * (z @ x) = y. [para(4(a,1),1(a,1)),flip(a)]. 12 x * y * (y @ z) != y * z | z = x. [para(4(a,1),2(a,1)),flip(a)]. 14 x * y * (y @ x) * z = y * x * z. [para(4(a,1),3(a,1,1)),rewrite([3(2),3(5)]),flip(a)]. 15 x * y * z * (z @ x * y) = z * x * y. [para(4(a,1),3(a,1)),flip(a)]. 17 (x @ y) * (z @ y) * ((z @ x) @ y) = (z @ y) * (x @ y). [para(4(a,1),6(a,1,1)),rewrite([6(2),6(7)]),flip(a)]. 20 x * y * ((A @ B) @ C) != x * y * (D @ (F @ G)) # answer(A). [ur(8,b,7,a)]. 23 x * y * z != y * x | y @ x = z. [para(4(a,1),8(a,1)),flip(a)]. 30 (F @ G) * D * ((A @ B) @ C) != D * (F @ G) # answer(A). [para(4(a,1),20(a,2))]. 34 x * y != x | x @ x = y. [para(10(a,1),1(a,1)),flip(a)]. 37 x * (x @ x) * y = x * y. [para(10(a,1),3(a,1,1)),flip(a)]. 55 x * (F @ G) * D * ((A @ B) @ C) != x * D * (F @ G) # answer(A). [ur(1,b,30,a)]. 62 (x @ x) * y = y. [hyper(8,a,37,a)]. 68 x * y != y | z @ z = x. [para(62(a,1),2(a,1)),flip(a)]. 69 x * ((y @ y) @ x) = x. [para(62(a,1),4(a,1,2)),rewrite([62(5)])]. 72 (x @ x * y) * (y @ x * y) * z = z. [para(6(a,1),62(a,1,1)),rewrite([3(6)])]. 76 (x @ x) @ y = y @ y. [hyper(34,a,69,a),flip(a)]. 94 (x @ x) @ y * z = (y @ y * z) * (z @ y * z). [para(76(a,2),6(a,1))]. 96 ((x @ x) @ y) * z = z. [para(76(a,2),62(a,1,1))]. 97 x * (((y @ y) @ z) @ x) = x. [para(76(a,2),69(a,1,2,1))]. 116 x * (x @ ((y @ y) @ z)) = x * ((y @ y) @ z). [hyper(11,a,96,a)]. 124 (((x @ x) @ y) @ z) * u = u. [para(76(a,2),96(a,1,1,1))]. 125 x * y != x | ((z @ z) @ u) @ x = y. [para(96(a,1),11(a,2)),rewrite([96(8)])]. 132 x * (x @ y) != x * y | (z @ z) @ u = y. [para(96(a,1),12(a,1)),flip(b)]. 135 (x @ x) @ y = z @ z. [hyper(68,a,96,a),flip(a)]. 136 x @ x = y @ y. [hyper(68,a,62,a)]. 138 x @ x = c_0. [new_symbol(136)]. 140 c_0 @ x = c_0. [back_rewrite(135),rewrite([138(1),138(3)])]. 142 x * (x @ y) != x * y | c_0 = y. [back_rewrite(132),rewrite([138(5),140(6)])]. 145 x * y != x | c_0 = y. [back_rewrite(125),rewrite([138(3),140(4),140(4)])]. 146 c_0 * x = x. [back_rewrite(124),rewrite([138(1),140(2),140(2)])]. 150 x * (x @ c_0) = x * c_0. [back_rewrite(116),rewrite([138(1),140(2),138(4),140(5)])]. 155 x * c_0 = x. [back_rewrite(97),rewrite([138(1),140(2),140(2)])]. 157 (x @ x * y) * (y @ x * y) = c_0. [back_rewrite(94),rewrite([138(1),140(3)]),flip(a)]. 159 x * (x @ c_0) = x. [back_rewrite(150),rewrite([155(5)])]. 183 x @ c_0 = c_0. [hyper(145,a,159,a),flip(a)]. 207 x * y * (y @ y * x) = y * x. [hyper(1,a,15,a)]. 260 x @ x * y != c_0 | y @ x * y = c_0. [para(157(a,1),145(a,1)),flip(a),flip(b)]. 266 x * (x @ x * y) = x * (x @ y). [hyper(11,a,207,a),flip(a)]. 277 (x @ y * x) * (y @ y * x) = c_0. [para(157(a,1),207(a,1,2,2,2)),rewrite([183(8),155(6),157(10)])]. 278 x @ x * y = x @ y. [hyper(1,a,266,a)]. 284 x * (x @ y) != x | x @ y = c_0. [para(266(a,1),145(a,1)),rewrite([278(6)]),flip(b)]. 293 (x @ y * x) * (y @ x) = c_0. [back_rewrite(277),rewrite([278(4)])]. 298 x @ y != c_0 | y @ x * y = c_0. [back_rewrite(260),rewrite([278(2)])]. 307 (x @ y) * (y @ x * y) = c_0. [back_rewrite(157),rewrite([278(2)])]. 310 (x @ y) * (y @ x * y) * z = z. [back_rewrite(72),rewrite([278(2)])]. 322 (x @ y) * ((x @ y) @ y) = x @ y. [para(138(a,1),17(a,1,1)),rewrite([146(6),138(6),155(7)])]. 324 (x @ (y @ x)) * (y @ (y @ x)) = (y @ (y @ x)) * (x @ (y @ x)). [para(138(a,1),17(a,1,2,2)),rewrite([155(6)])]. 338 (x @ y * z) * (y @ x * y * z) = (x @ z) * (y @ z). [para(3(a,1),278(a,1,2)),rewrite([6(4),278(3),6(8)])]. 339 x @ y * (y @ x) = x @ y * x. [para(4(a,1),278(a,1,2)),flip(a)]. 351 (x @ y * x) * (y @ x) * z = z. [para(293(a,1),3(a,1,1)),rewrite([146(2)]),flip(a)]. 376 (x @ y) @ x * y = c_0. [para(4(a,1),307(a,1,2,2)),rewrite([339(3),6(6),278(4),351(8)])]. 386 x * y * (y @ x * y) = y * x. [para(307(a,1),14(a,1,2,2)),rewrite([155(2)]),flip(a)]. 396 (x @ y) * x * y = x * y * (x @ y). [para(376(a,1),4(a,1,2,2)),rewrite([155(4),3(3)]),flip(a)]. 397 (x @ y * x) @ y * x = c_0. [para(4(a,1),376(a,1,2)),rewrite([339(3)])]. 408 (x @ (x @ y)) * (y @ (x @ y)) = c_0. [para(376(a,1),293(a,1,2)),rewrite([396(4),6(5),278(4),338(8),155(7)])]. 409 (x @ (y @ x)) * (y @ (y @ x)) = c_0. [back_rewrite(324),rewrite([408(10)])]. 439 (x @ y * x) * y * x = x * y. [para(397(a,1),4(a,1,2,2)),rewrite([155(5),3(4),386(4)]),flip(a)]. 447 (x @ y * x) @ x * y = c_0. [para(397(a,1),278(a,2)),rewrite([439(6)])]. 473 (x @ y * x) * x * y = x * y * (x @ y * x). [para(447(a,1),4(a,1,2,2)),rewrite([155(5),3(4)]),flip(a)]. 485 (x @ (x @ y * x)) * (y @ (x @ y * x)) = c_0. [para(447(a,1),293(a,1,2)),rewrite([473(5),6(6),278(5),338(10),155(9)])]. 491 (x @ y) @ (z @ y) = (x @ z) @ y. [hyper(23,a,17,a)]. 534 (x @ y) @ (y @ x * y) * z = (x @ y) @ z. [para(310(a,1),278(a,1,2)),flip(a)]. 589 (x @ y) @ y = c_0. [hyper(284,a,322,a)]. 590 (x @ y) * y = y * (x @ y). [para(322(a,1),4(a,1,2)),flip(a)]. 597 x @ (y @ x) = c_0. [hyper(298,a,589,a),rewrite([590(2),278(3)])]. 605 x @ (x @ y) = c_0. [back_rewrite(409),rewrite([597(2),146(4)])]. 610 x @ (y @ x * y) = c_0. [back_rewrite(485),rewrite([605(3),146(5)])]. 639 x * (y @ x) != x | y @ x = c_0. [para(597(a,1),142(a,1,2)),rewrite([155(2)]),flip(a),flip(b)]. 669 (x @ y) @ ((y @ x * y) @ z) = c_0. [para(310(a,1),610(a,1,2,2)),rewrite([6(5),138(5),155(6)])]. 837 D * ((A @ B) @ C) != (G @ F * G) * D * (F @ G) # answer(A). [para(351(a,1),55(a,1))]. 854 (x @ y * x) @ (y @ x) * z = (x @ y * x) @ z. [para(351(a,1),278(a,1,2)),flip(a)]. 872 (x @ y) @ z = z @ (y @ x * y) * z. [para(351(a,1),339(a,2,2)),rewrite([854(9),6(9),534(8),669(5),339(8),146(6),6(7),138(7),155(8)]),flip(a)]. 874 x @ y * x = x @ y. [hyper(23,a,386,a),flip(a)]. 884 (x @ y) * (y @ x) = c_0. [para(386(a,1),293(a,1,1,2)),rewrite([874(2),6(4),278(2),376(4),155(3),874(3),339(4),874(3)])]. 911 (x @ y) @ z = z @ (y @ x). [back_rewrite(872),rewrite([874(4),874(5)])]. 944 (G @ F) * D * (F @ G) != D * (C @ (B @ A)) # answer(A). [back_rewrite(837),rewrite([911(6),874(12)]),flip(a)]. 1376 x * (y @ z) * ((y @ x) @ (z @ x)) = (y @ z) * x. [para(491(a,2),4(a,1,2,2))]. 1397 (x @ y) @ (z @ y) = c_0. [para(597(a,1),491(a,1,2)),rewrite([183(4)]),flip(a)]. 1412 (x @ y) @ z = c_0. [para(491(a,2),639(a,1,2)),rewrite([1397(3),155(2)]),xx(a)]. 1415 x @ (y @ z) = c_0. [para(491(a,2),884(a,1,1)),rewrite([1412(3),146(4)])]. 1425 (x @ y) * z = z * (x @ y). [back_rewrite(1376),rewrite([1415(4),155(3)]),flip(a)]. 1426 $F # answer(A). [back_rewrite(944),rewrite([1425(9),3(9),884(8),155(3),1415(7),155(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=211. Generated=10596. Kept=1424. proofs=1. Usable=107. Sos=611. Demods=163. Limbo=25, Disabled=687. Hints=0. Kept_by_rule=0, Deleted_by_rule=2786. Forward_subsumed=6385. Back_subsumed=67. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=421 (2 lex), Back_demodulated=614. Back_unit_deleted=0. Demod_attempts=191550. Demod_rewrites=20099. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=30969. Nonunit_bsub_feature_tests=8025. Megabytes=1.25. User_CPU=0.30, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11599 exit (max_proofs) Wed Feb 25 09:32:54 2009