============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11747 was started by mccune on cleo.thornwood, Sat Aug 12 21:31:39 2006 The command was "/home/mccune/bin/prover9 -f dist-short-long.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file dist-short-long.in assign(order,kbo). set(lex_order_vars). formulas(sos). f(x,x,y) = x # label(majority). f(x,y,z) = f(z,x,y) # label(2a). f(x,y,z) = f(x,z,y) # label(2b). f(f(x,w,y),w,z) = f(x,w,f(y,w,z)) # label(associativity). f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # label(dist_short). end_of_list. formulas(goals). f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) # answer(dist_long). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) # answer(dist_long). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(x,x,y) = x # label(majority). [assumption]. f(x,y,z) = f(z,x,y) # label(2a). [assumption]. f(x,y,z) = f(x,z,y) # label(2b). [assumption]. f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [assumption]. f(f(x,y,z),u,v) = f(x,f(y,u,v),f(z,u,v)) # label(dist_short). [assumption]. f(f(c1,c4,c5),f(c2,c4,c5),f(c3,c4,c5)) != f(f(c1,c2,c3),c4,c5) # answer(dist_long). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Function symbol KB weights: c1=1. c2=1. c3=1. c4=1. c5=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, f ]). Skipping inverse_order, because term ordering is KBO. 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: formulas(usable). end_of_list. formulas(sos). 2 f(x,x,y) = x # label(majority). [assumption]. 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. 4 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. 6 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(5),rewrite(3(2),3(2),3(3,R),4(3)),rewrite(3(1,R),4(1),4(3),3(4,R),4(4))]. 8 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [copy(7),rewrite(3(2),3(2)),flip(a),rewrite(3(2),3(2))]. 10 f(f(c1,c4,c5),f(c2,c4,c5),f(c3,c4,c5)) != f(c4,c5,f(c1,c2,c3)) # answer(dist_long). [copy(9),rewrite(3(20),3(20))]. end_of_list. formulas(demodulators). 2 f(x,x,y) = x # label(majority). [assumption]. 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. % (lex-dep) 4 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. % (lex-dep) 8 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [copy(7),rewrite(3(2),3(2)),flip(a),rewrite(3(2),3(2))]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 2 f(x,x,y) = x # label(majority). [assumption]. given #2 (I,wt=9): 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. given #3 (I,wt=9): 4 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. given #4 (I,wt=15): 6 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(5),rewrite(3(2),3(2),3(3,R),4(3)),rewrite(3(1,R),4(1),4(3),3(4,R),4(4))]. given #5 (I,wt=18): 8 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [copy(7),rewrite(3(2),3(2)),flip(a),rewrite(3(2),3(2))]. given #6 (I,wt=21): 10 f(f(c1,c4,c5),f(c2,c4,c5),f(c3,c4,c5)) != f(c4,c5,f(c1,c2,c3)) # answer(dist_long). [copy(9),rewrite(3(20),3(20))]. given #7 (F,wt=6): 11 f(x,y,y) = y. [para(3(a,1),2(a,1))]. given #8 (F,wt=12): 27 f(x,y,f(x,z,y)) = f(x,z,y). [para(11(a,1),6(a,1,3)),flip(a)]. given #9 (T,wt=12): 28 f(x,y,f(x,y,z)) = f(x,y,z). [para(11(a,1),6(a,1)),rewrite(4(3),27(3)),flip(a)]. given #10 (T,wt=15): 12 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(6(a,1),3(a,2)),rewrite(4(2),3(3,R),4(3)),flip(a)]. given #11 (A,wt=15): 13 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)). [para(3(a,1),6(a,1,3)),rewrite(3(1,R),4(1))]. given #12 (F,wt=15): 29 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(11(a,1),8(a,1,3)),rewrite(4(2))]. given #13 (F,wt=12): 53 f(x,y,f(z,x,y)) = f(z,x,y). [para(2(a,1),29(a,1,3)),rewrite(4(2),3(3,R),4(3)),flip(a)]. given #14 (T,wt=15): 34 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(12(a,1),3(a,2)),rewrite(4(2),3(3,R),4(3))]. given #15 (T,wt=15): 35 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)). [para(3(a,1),12(a,1)),rewrite(3(2),3(2),4(3))]. given #16 (A,wt=21): 14 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))). [para(6(a,1),6(a,1,3))]. given #17 (F,wt=15): 43 f(x,y,f(x,z,u)) = f(x,u,f(x,z,y)). [para(3(a,1),13(a,1)),rewrite(3(2),3(2),4(3))]. given #18 (F,wt=15): 54 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(3(a,1),29(a,1)),rewrite(3(2),4(2),3(3),3(3))]. given #19 (T,wt=15): 55 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(29(a,2),4(a,2)),rewrite(4(2),3(3,R),4(3))]. given #20 (T,wt=15): 60 f(x,y,f(z,u,f(x,z,y))) = f(x,z,y). [para(29(a,1),8(a,1)),rewrite(3(1),3(2),3(3,R),4(3),58(4),11(1),3(1),2(1),3(2),3(3,R),4(3),3(4,R),4(4)),flip(a)]. given #21 (A,wt=18): 16 f(x,f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [para(8(a,1),3(a,1)),rewrite(3(4),3(4),3(5,R)),flip(a)]. given #22 (F,wt=15): 143 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(54(a,2),4(a,2)),rewrite(4(2),3(3,R),4(3)),flip(a)]. given #23 (F,wt=15): 144 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [para(54(a,1),8(a,1)),rewrite(3(1),4(1),3(2,R),4(2),3(4),2(4),3(4),3(4))]. given #24 (T,wt=15): 146 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [para(8(a,1),54(a,1)),rewrite(3(1),2(1),3(2),3(2)),flip(a)]. given #25 (T,wt=15): 148 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [para(28(a,1),54(a,1,3)),rewrite(3(3,R),11(3),4(4),84(5)),flip(a)]. given #26 (A,wt=18): 17 f(x,f(y,z,u),f(y,u,v)) = f(y,u,f(x,z,v)). [para(3(a,1),8(a,1,2)),rewrite(3(2,R),4(2),3(5,R),4(5))]. given #27 (F,wt=15): 155 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [para(53(a,1),54(a,1,3)),rewrite(3(3,R),11(3),4(4),71(5),3(3,R),4(3)),flip(a)]. given #28 (F,wt=15): 164 f(x,y,f(y,z,f(u,x,z))) = f(x,y,z). [para(28(a,1),55(a,1,3)),rewrite(11(3),58(5),3(2),3(3,R),4(3)),flip(a)]. given #29 (T,wt=15): 173 f(x,f(y,z,u),f(x,z,u)) = f(x,z,u). [para(60(a,1),8(a,2)),rewrite(3(2,R),4(2),53(3),3(4,R),4(4))]. given #30 (T,wt=15): 200 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para(16(a,1),29(a,1)),rewrite(32(3),11(1),3(4,R),4(4),84(5),4(2)),flip(a)]. given #31 (A,wt=24): 18 f(x,f(y,z,u),f(x,v,f(y,z,w))) = f(x,v,f(y,z,f(x,u,w))). [para(8(a,1),6(a,1,3)),rewrite(3(4),3(4)),flip(a)]. given #32 (F,wt=15): 220 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [para(8(a,1),143(a,1)),rewrite(3(1),2(1),3(2),3(2)),flip(a)]. given #33 (F,wt=15): 226 f(x,y,f(x,z,f(z,y,u))) = f(x,z,y). [para(144(a,1),3(a,2)),rewrite(3(1,R),4(1),4(3),3(4),3(4))]. given #34 (T,wt=15): 237 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para(29(a,1),144(a,2)),rewrite(3(1),3(2),4(3),211(4),196(3),233(4),4(3),3(4,R),4(4))]. given #35 (T,wt=15): 302 f(x,y,f(z,u,y)) = f(u,y,f(z,x,y)). [para(143(a,1),155(a,2)),rewrite(4(3),3(4,R),4(4),301(5),3(3))]. given #36 (A,wt=24): 20 f(x,f(y,z,u),f(x,v,f(z,u,w))) = f(x,v,f(z,u,f(x,y,w))). [para(8(a,1),6(a,2,3))]. given #37 (F,wt=15): 304 f(x,y,f(x,z,f(z,u,y))) = f(x,z,y). [para(164(a,1),3(a,2)),rewrite(3(1),4(3),3(4),3(4))]. given #38 (F,wt=15): 305 f(x,y,f(y,z,f(x,u,z))) = f(x,y,z). [para(3(a,1),164(a,1,3)),rewrite(3(1,R),4(1),3(2),3(2))]. given #39 (T,wt=15): 318 f(x,f(y,z,u),f(x,y,u)) = f(x,y,u). [para(3(a,1),173(a,1,2)),rewrite(4(2),4(4))]. given #40 (T,wt=15): 344 f(x,y,f(x,z,f(u,y,z))) = f(x,y,z). [para(173(a,1),16(a,2)),rewrite(4(2),4(4),211(5),27(4))]. given #41 (A,wt=27): 21 f(x,f(y,z,f(y,u,v)),f(u,w,f(y,z,v))) = f(u,f(y,z,v),f(x,y,w)). [para(6(a,1),8(a,1,2)),rewrite(4(4))]. given #42 (F,wt=15): 434 f(x,y,f(z,x,f(u,z,y))) = f(z,x,y). [para(28(a,1),302(a,1,3)),rewrite(11(3),3(4,R),4(4),153(5),211(4),202(4),3(2,R),4(2)),flip(a)]. given #43 (F,wt=15): 556 f(x,y,f(z,y,f(u,z,x))) = f(z,x,y). [para(53(a,1),21(a,1,3)),rewrite(28(2),11(3),153(4)),flip(a)]. given #44 (T,wt=15): 624 f(x,y,f(z,x,f(z,u,y))) = f(z,x,y). [para(3(a,1),434(a,1)),rewrite(3(1,R),4(1),3(3),3(3))]. given #45 (T,wt=18): 32 f(x,y,f(z,u,f(x,y,v))) = f(x,y,f(z,u,v)). [para(27(a,1),8(a,1,3)),rewrite(4(2),8(3),4(3)),flip(a)]. given #46 (A,wt=24): 22 f(x,f(y,z,u),f(z,v,f(z,u,w))) = f(z,u,f(x,y,f(z,v,w))). [para(6(a,1),8(a,1,3))]. given #47 (F,wt=18): 196 f(x,y,f(z,u,f(x,v,y))) = f(x,y,f(z,v,u)). [para(27(a,1),16(a,1,2)),rewrite(17(3),4(4)),flip(a)]. given #48 (F,wt=18): 202 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(z,v,u)). [para(53(a,1),16(a,1,2)),rewrite(8(3),4(4)),flip(a)]. given #49 (T,wt=18): 228 f(x,y,f(y,z,f(x,u,f(x,z,v)))) = f(x,y,z). [para(6(a,1),144(a,1,3,3))]. given #50 (T,wt=18): 232 f(x,y,f(y,z,f(z,u,f(x,z,v)))) = f(x,y,z). [para(12(a,2),144(a,1,3,3))]. given #51 (A,wt=21): 23 f(x,y,f(z,u,f(z,v,w))) = f(x,y,f(z,v,f(z,u,w))). [para(6(a,1),8(a,2,3)),rewrite(8(4))]. given #52 (F,wt=18): 307 f(x,f(y,z,u),f(v,y,z)) = f(y,z,f(v,x,u)). [para(8(a,1),164(a,1,3,3)),rewrite(3(3),3(3),16(5),3(5,R),4(5),8(5),148(3),3(1,R),4(1),3(5,R)),flip(a)]. given #53 (F,wt=18): 316 f(x,f(y,z,u),f(y,v,z)) = f(y,z,f(v,x,u)). [para(17(a,1),164(a,1,3,3)),rewrite(3(3),3(3),16(5),3(5,R),4(5),17(5),148(3),3(1,R),4(1),3(5,R)),flip(a)]. given #54 (T,wt=18): 341 f(x,y,f(z,f(x,z,u),f(y,z,v))) = f(x,y,z). [para(173(a,1),54(a,1,3)),rewrite(3(3,R),11(3),3(2),3(2),4(5),190(6),4(3),3(4,R)),flip(a)]. given #55 (T,wt=18): 351 f(x,f(y,z,f(u,y,v)),f(x,y,v)) = f(x,y,v). [para(173(a,1),148(a,2)),rewrite(3(5),211(6),196(5),3(3,R),4(3),335(6))]. given #56 (A,wt=24): 24 f(f(x,y,z),f(x,y,u),f(v,w,v6)) = f(x,y,f(z,u,f(v,w,v6))). [para(8(a,1),8(a,1,2)),rewrite(3(3),3(3),3(5),16(5),3(3),3(3),16(5),8(3),3(4),3(4)),flip(a)]. given #57 (F,wt=18): 354 f(x,f(y,z,x),f(y,u,f(v,y,z))) = f(y,z,x). [para(173(a,1),155(a,2)),rewrite(3(2),3(2),3(4),3(4),4(5),20(6),3(3,R),11(3),31(5),3(3),3(3),3(5),3(5))]. given #58 (F,wt=18): 355 f(x,y,f(x,z,f(u,y,f(v,y,z)))) = f(x,y,z). [para(173(a,1),173(a,1,3)),rewrite(4(5),211(5),196(4),173(7))]. given #59 (T,wt=18): 407 f(x,y,f(z,y,f(x,u,f(x,z,v)))) = f(x,z,y). [para(146(a,1),18(a,1,3)),rewrite(3(2,R),4(2),307(3),2(1),3(1),3(2,R),4(2)),flip(a)]. given #60 (T,wt=18): 505 f(x,y,f(z,f(y,u,z),f(x,z,v))) = f(x,y,z). [para(318(a,1),144(a,2)),rewrite(4(5),190(6),4(3),3(4,R),444(6),32(5))]. given #61 (A,wt=30): 25 f(x,f(y,z,f(u,v,w)),f(v,w,f(z,u,v6))) = f(z,f(u,v,w),f(x,y,f(v,w,v6))). [para(8(a,1),8(a,1,3))]. ============================== PROOF ================================= % Proof 1 at 1.47 (+ 0.00) seconds: dist_long. % Length of proof is 36. % Level of proof is 9. % Maximum clause weight is 30. % Given clauses 61. 1 f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) # answer(dist_long). [goal]. 2 f(x,x,y) = x # label(majority). [assumption]. 3 f(x,y,z) = f(z,x,y) # label(2a). [assumption]. 4 f(x,y,z) = f(x,z,y) # label(2b). [assumption]. 5 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [assumption]. 6 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [copy(5),rewrite(3(2),3(2),3(3,R),4(3)),rewrite(3(1,R),4(1),4(3),3(4,R),4(4))]. 7 f(f(x,y,z),u,v) = f(x,f(y,u,v),f(z,u,v)) # label(dist_short). [assumption]. 8 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(x,y,v)). [copy(7),rewrite(3(2),3(2)),flip(a),rewrite(3(2),3(2))]. 9 f(f(c1,c4,c5),f(c2,c4,c5),f(c3,c4,c5)) != f(f(c1,c2,c3),c4,c5) # answer(dist_long). [deny(1)]. 10 f(f(c1,c4,c5),f(c2,c4,c5),f(c3,c4,c5)) != f(c4,c5,f(c1,c2,c3)) # answer(dist_long). [copy(9),rewrite(3(20),3(20))]. 11 f(x,y,y) = y. [para(3(a,1),2(a,1))]. 12 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(6(a,1),3(a,2)),rewrite(4(2),3(3,R),4(3)),flip(a)]. 16 f(x,f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [para(8(a,1),3(a,1)),rewrite(3(4),3(4),3(5,R)),flip(a)]. 17 f(x,f(y,z,u),f(y,u,v)) = f(y,u,f(x,z,v)). [para(3(a,1),8(a,1,2)),rewrite(3(2,R),4(2),3(5,R),4(5))]. 25 f(x,f(y,z,f(u,v,w)),f(v,w,f(z,u,v6))) = f(z,f(u,v,w),f(x,y,f(v,w,v6))). [para(8(a,1),8(a,1,3))]. 27 f(x,y,f(x,z,y)) = f(x,z,y). [para(11(a,1),6(a,1,3)),flip(a)]. 28 f(x,y,f(x,y,z)) = f(x,y,z). [para(11(a,1),6(a,1)),rewrite(4(3),27(3)),flip(a)]. 29 f(x,y,f(z,u,y)) = f(u,y,f(x,z,y)). [para(11(a,1),8(a,1,3)),rewrite(4(2))]. 34 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para(12(a,1),3(a,2)),rewrite(4(2),3(3,R),4(3))]. 53 f(x,y,f(z,x,y)) = f(z,x,y). [para(2(a,1),29(a,1,3)),rewrite(4(2),3(3,R),4(3)),flip(a)]. 54 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(3(a,1),29(a,1)),rewrite(3(2),4(2),3(3),3(3))]. 55 f(x,y,f(z,u,y)) = f(z,y,f(x,u,y)). [para(29(a,2),4(a,2)),rewrite(4(2),3(3,R),4(3))]. 58 f(x,f(x,y,z),f(u,v,f(x,y,z))) = f(x,y,f(z,v,f(x,z,u))). [para(6(a,1),29(a,2,3)),rewrite(4(6),16(8),3(6,R),4(6))]. 71 f(x,f(y,z,x),f(u,v,f(y,z,x))) = f(z,x,f(u,y,f(y,x,v))). [para(29(a,1),29(a,1,3)),rewrite(3(2),3(2),8(4)),flip(a)]. 84 f(x,f(y,x,z),f(u,v,f(y,x,z))) = f(y,x,f(u,z,f(x,z,v))). [para(34(a,1),29(a,1,3)),rewrite(3(2),3(2),16(4)),flip(a)]. 143 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para(54(a,2),4(a,2)),rewrite(4(2),3(3,R),4(3)),flip(a)]. 148 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [para(28(a,1),54(a,1,3)),rewrite(3(3,R),11(3),4(4),84(5)),flip(a)]. 155 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [para(53(a,1),54(a,1,3)),rewrite(3(3,R),11(3),4(4),71(5),3(3,R),4(3)),flip(a)]. 164 f(x,y,f(y,z,f(u,x,z))) = f(x,y,z). [para(28(a,1),55(a,1,3)),rewrite(11(3),58(5),3(2),3(3,R),4(3)),flip(a)]. 201 f(x,f(y,z,f(z,u,v)),f(z,v,w)) = f(z,v,f(x,w,f(y,z,u))). [para(29(a,2),16(a,1,2)),rewrite(3(1),3(3,R),4(3),4(5),4(6),3(7,R),4(7))]. 202 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(z,v,u)). [para(53(a,1),16(a,1,2)),rewrite(8(3),4(4)),flip(a)]. 220 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [para(8(a,1),143(a,1)),rewrite(3(1),2(1),3(2),3(2)),flip(a)]. 316 f(x,f(y,z,u),f(y,v,z)) = f(y,z,f(v,x,u)). [para(17(a,1),164(a,1,3,3)),rewrite(3(3),3(3),16(5),3(5,R),4(5),17(5),148(3),3(1,R),4(1),3(5,R)),flip(a)]. 1416 f(x,f(y,z,u),f(v,z,f(z,u,w))) = f(z,u,f(y,x,f(v,z,w))). [para(12(a,1),25(a,1,2)),rewrite(3(3,R),4(3),201(5),316(3),3(1,R),4(1)),flip(a)]. 1475 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(v,x,y)). [para(25(a,1),155(a,1,3)),rewrite(3(5,R),4(5),1416(6),3(4,R),4(4),3(6,R),4(6),25(6),3(4,R),4(4),220(4),4(6),202(6),4(4))]. 1581 $F # answer(dist_long). [back_rewrite(10),rewrite(1475(13),3(9),202(10),3(6,R),4(6)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=61. Generated=16200. Kept=1576. proofs=1. Usable=55. Sos=1079. Demods=960. Limbo=106, Disabled=342. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=14623. Back_subsumed=43. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1247 (2 lex), Back_demodulated=293. Back_unit_deleted=0. Demod_attempts=243565. Demod_rewrites=92363. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.71. User_CPU=1.47, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11747 exit (max_proofs) Sat Aug 12 21:31:40 2006