============================== Prover9 =============================== Prover9 (32) version March-2007, March 2007. Process 21142 was started by mccune on cleo, Mon Mar 19 17:05:50 2007 The command was "/home/mccune/bin/prover9 -f wang-eq.in wang1-eq.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file wang-eq.in formulas(sos). y = m | p(y,m) | v1 = m | v1 = y | -p(y,v1) | -p(v1,y). y = b | -p(y,b) | v = b | v = y | -p(y,v) | -p(v,y). y = k | y = m | y = b | -p(y,k). y = m | -p(y,m) | f(y) != m. y = m | -p(y,m) | f(y) != y. y = m | -p(y,m) | p(y,f(y)). y = m | -p(y,m) | p(f(y),y). y = b | p(y,b) | g(y) != b. y = b | p(y,b) | g(y) != y. y = b | p(y,b) | p(y,g(y)). y = b | p(y,b) | p(g(y),y). y = k | y != m | p(y,k). y = k | y != b | p(y,k). end_of_list. % Reading from file wang1-eq.in formulas(sos). m != b. b != k. k != m. 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 = m | p(x,m) | y = m | y = x | -p(x,y) | -p(y,x). [assumption]. x = b | -p(x,b) | y = b | y = x | -p(x,y) | -p(y,x). [assumption]. x = k | x = m | x = b | -p(x,k). [assumption]. x = m | -p(x,m) | f(x) != m. [assumption]. x = m | -p(x,m) | f(x) != x. [assumption]. x = m | -p(x,m) | p(x,f(x)). [assumption]. x = m | -p(x,m) | p(f(x),x). [assumption]. x = b | p(x,b) | g(x) != b. [assumption]. x = b | p(x,b) | g(x) != x. [assumption]. x = b | p(x,b) | p(x,g(x)). [assumption]. x = b | p(x,b) | p(g(x),x). [assumption]. x = k | x != m | p(x,k). [assumption]. x = k | x != b | p(x,k). [assumption]. m != b. [assumption]. b != k. [assumption]. k != m. [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([ p, = ]). Function symbol precedence: lex([ b, m, k, f, g ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 m = x | p(x,m) | m = y | y = x | -p(x,y) | -p(y,x). [copy(1),flip(a),flip(c)]. 4 b = x | -p(x,b) | b = y | y = x | -p(x,y) | -p(y,x). [copy(3),flip(a),flip(c)]. 6 k = x | m = x | b = x | -p(x,k). [copy(5),flip(a),flip(b),flip(c)]. 8 m = x | -p(x,m) | f(x) != m. [copy(7),flip(a)]. 10 m = x | -p(x,m) | f(x) != x. [copy(9),flip(a)]. 12 m = x | -p(x,m) | p(x,f(x)). [copy(11),flip(a)]. 14 m = x | -p(x,m) | p(f(x),x). [copy(13),flip(a)]. 16 b = x | p(x,b) | g(x) != b. [copy(15),flip(a)]. 18 b = x | p(x,b) | g(x) != x. [copy(17),flip(a)]. 20 b = x | p(x,b) | p(x,g(x)). [copy(19),flip(a)]. 22 b = x | p(x,b) | p(g(x),x). [copy(21),flip(a)]. 24 k = x | m != x | p(x,k). [copy(23),flip(a),flip(b)]. 26 k = x | b != x | p(x,k). [copy(25),flip(a),flip(b)]. 27 m != b. [assumption]. 29 k != b. [copy(28),flip(a)]. 30 k != m. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=18): 2 m = x | p(x,m) | m = y | y = x | -p(x,y) | -p(y,x). [copy(1),flip(a),flip(c)]. given #2 (I,wt=18): 4 b = x | -p(x,b) | b = y | y = x | -p(x,y) | -p(y,x). [copy(3),flip(a),flip(c)]. given #3 (I,wt=12): 6 k = x | m = x | b = x | -p(x,k). [copy(5),flip(a),flip(b),flip(c)]. given #4 (I,wt=10): 8 m = x | -p(x,m) | f(x) != m. [copy(7),flip(a)]. given #5 (I,wt=10): 10 m = x | -p(x,m) | f(x) != x. [copy(9),flip(a)]. given #6 (I,wt=10): 12 m = x | -p(x,m) | p(x,f(x)). [copy(11),flip(a)]. given #7 (I,wt=10): 14 m = x | -p(x,m) | p(f(x),x). [copy(13),flip(a)]. given #8 (I,wt=10): 16 b = x | p(x,b) | g(x) != b. [copy(15),flip(a)]. given #9 (I,wt=10): 18 b = x | p(x,b) | g(x) != x. [copy(17),flip(a)]. given #10 (I,wt=10): 20 b = x | p(x,b) | p(x,g(x)). [copy(19),flip(a)]. given #11 (I,wt=10): 22 b = x | p(x,b) | p(g(x),x). [copy(21),flip(a)]. given #12 (I,wt=9): 24 k = x | m != x | p(x,k). [copy(23),flip(a),flip(b)]. given #13 (I,wt=9): 26 k = x | b != x | p(x,k). [copy(25),flip(a),flip(b)]. given #14 (I,wt=3): 27 m != b. [assumption]. given #15 (I,wt=3): 29 k != b. [copy(28),flip(a)]. given #16 (I,wt=3): 30 k != m. [assumption]. given #17 (A,wt=16): 31 p(g(x),b) | p(g(x),g(g(x))) | b = x | p(x,b). [resolve(20,a,16,c(flip))]. given #18 (T,wt=3): 48 p(m,k). [xx_res(24,b),unit_del(a,30)]. given #19 (T,wt=3): 53 p(b,k). [xx_res(26,b),unit_del(a,29)]. given #20 (T,wt=6): 84 p(k,m) | -p(k,b). [resolve(53,a,2,f),flip(a),flip(d),unit_del(a,30),unit_del(c,27),unit_del(d,29)]. given #21 (T,wt=6): 85 p(b,m) | -p(k,b). [resolve(53,a,2,e),flip(c),unit_del(a,27),unit_del(c,30),unit_del(d,29)]. given #22 (A,wt=13): 32 p(f(b),b) | p(f(b),g(f(b))) | -p(b,m). [resolve(20,a,10,c(flip)),unit_del(c,27)]. given #23 (F,wt=6): 82 -p(k,b) | -p(k,m). [resolve(48,a,4,f),flip(a),flip(c),flip(d),unit_del(a,29),unit_del(c,27),unit_del(d,30)]. given #24 (F,wt=6): 83 -p(m,b) | -p(k,m). [resolve(48,a,4,e),flip(a),flip(c),unit_del(a,27),unit_del(c,29),unit_del(d,30)]. given #25 (T,wt=7): 56 p(m,b) | p(g(m),m). [resolve(27,a,22,a(flip))]. given #26 (T,wt=7): 57 p(m,b) | p(m,g(m)). [resolve(27,a,20,a(flip))]. given #27 (T,wt=7): 60 p(k,b) | p(g(k),k). [resolve(29,a,22,a(flip))]. given #28 (T,wt=7): 61 p(k,b) | p(k,g(k)). [resolve(29,a,20,a(flip))]. given #29 (A,wt=25): 33 p(x,b) | p(x,g(x)) | b = y | -p(y,x) | b = z | z = y | -p(y,z) | -p(z,y). [para(20(a,1),4(b,2))]. given #30 (T,wt=10): 58 p(x,b) | p(x,g(x)) | m != x. [para(20(a,1),27(a,2))]. given #31 (T,wt=10): 59 p(x,b) | p(g(x),x) | m != x. [para(22(a,1),27(a,2))]. given #32 (T,wt=10): 62 p(x,b) | p(x,g(x)) | k != x. [para(20(a,1),29(a,2))]. given #33 (T,wt=10): 63 p(x,b) | p(g(x),x) | k != x. [para(22(a,1),29(a,2))]. given #34 (A,wt=17): 34 p(x,b) | p(x,g(x)) | b = y | p(y,b) | g(y) != x. [para(20(a,1),16(c,2))]. given #35 (T,wt=10): 86 p(x,b) | p(x,g(x)) | p(x,k). [para(20(a,1),53(a,1))]. given #36 (T,wt=10): 87 p(x,b) | p(g(x),x) | p(x,k). [para(22(a,1),53(a,1))]. given #37 (T,wt=13): 37 p(f(b),b) | p(g(f(b)),f(b)) | -p(b,m). [resolve(22,a,10,c(flip)),unit_del(c,27)]. given #38 (T,wt=13): 65 p(g(k),b) | p(g(k),g(g(k))) | p(k,b). [resolve(31,c,29,a(flip))]. given #39 (A,wt=17): 35 p(x,b) | p(x,g(x)) | x = y | p(y,b) | p(y,g(y)). [para(20(a,1),20(a,1))]. given #40 (T,wt=13): 66 p(g(m),b) | p(g(m),g(g(m))) | p(m,b). [resolve(31,c,27,a(flip))]. given #41 (T,wt=13): 89 p(x,b) | p(x,g(x)) | p(k,m) | -p(k,x). [para(20(a,1),84(b,2))]. given #42 (T,wt=13): 90 p(x,b) | p(g(x),x) | p(k,m) | -p(k,x). [para(22(a,1),84(b,2))]. given #43 (T,wt=13): 92 p(x,b) | p(x,g(x)) | p(b,m) | -p(k,x). [para(20(a,1),85(b,2))]. given #44 (A,wt=16): 36 p(g(x),b) | p(g(g(x)),g(x)) | b = x | p(x,b). [resolve(22,a,16,c(flip))]. given #45 (T,wt=13): 93 p(x,b) | p(g(x),x) | p(b,m) | -p(k,x). [para(22(a,1),85(b,2))]. given #46 (T,wt=13): 99 p(x,b) | p(x,g(x)) | -p(k,x) | -p(k,m). [para(20(a,1),82(a,2))]. given #47 (T,wt=13): 100 p(x,b) | p(g(x),x) | -p(k,x) | -p(k,m). [para(22(a,1),82(a,2))]. given #48 (T,wt=13): 102 p(x,b) | p(x,g(x)) | -p(m,x) | -p(k,m). [para(20(a,1),83(a,2))]. given #49 (A,wt=25): 38 p(x,b) | p(g(x),x) | b = y | -p(y,x) | b = z | z = y | -p(y,z) | -p(z,y). [para(22(a,1),4(b,2))]. given #50 (T,wt=13): 103 p(x,b) | p(g(x),x) | -p(m,x) | -p(k,m). [para(22(a,1),83(a,2))]. given #51 (T,wt=13): 105 p(m,b) | g(m) = m | p(f(g(m)),g(m)). [resolve(56,b,14,b),flip(b)]. given #52 (T,wt=9): 204 p(m,b) | p(f(g(m)),g(m)). [resolve(105,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #53 (T,wt=13): 106 p(m,b) | g(m) = m | p(g(m),f(g(m))). [resolve(56,b,12,b),flip(b)]. given #54 (A,wt=17): 39 p(x,b) | p(g(x),x) | b = y | p(y,b) | g(y) != x. [para(22(a,1),16(c,2))]. given #55 (T,wt=9): 214 p(m,b) | p(g(m),f(g(m))). [resolve(106,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #56 (T,wt=13): 158 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b). [resolve(36,c,29,a(flip))]. given #57 (T,wt=13): 159 p(g(m),b) | p(g(g(m)),g(m)) | p(m,b). [resolve(36,c,27,a(flip))]. given #58 (T,wt=14): 98 p(f(b),b) | p(f(b),g(f(b))) | -p(f(b),m). [factor(95,a,c),merge(c)]. given #59 (A,wt=17): 40 p(x,b) | p(g(x),x) | x = y | p(y,b) | p(y,g(y)). [para(22(a,1),20(a,1))]. given #60 (T,wt=14): 137 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(b),m). [factor(135,a,c),merge(c)]. given #61 (T,wt=15): 109 p(k,b) | g(k) = k | g(k) = m | g(k) = b. [resolve(60,b,6,d),flip(b),flip(c),flip(d)]. given #62 (T,wt=11): 249 p(k,b) | g(k) = m | g(k) = b. [resolve(109,b,18,c),flip(d),merge(e),unit_del(d,29)]. given #63 (T,wt=10): 250 p(k,b) | g(k) = b | p(k,m). [para(249(b,1),61(b,2)),merge(c)]. given #64 (A,wt=17): 41 p(x,b) | p(x,g(x)) | x = y | p(y,b) | p(g(y),y). [para(20(a,1),22(a,1))]. given #65 (T,wt=6): 257 p(k,b) | p(k,m). [resolve(250,b,16,c),flip(c),merge(d),unit_del(c,29)]. given #66 (T,wt=6): 262 p(k,b) | -p(m,b). [resolve(257,b,83,b)]. given #67 (T,wt=7): 263 p(k,b) | p(f(k),k). [resolve(257,b,14,b),flip(b),unit_del(b,30)]. given #68 (T,wt=7): 264 p(k,b) | p(k,f(k)). [resolve(257,b,12,b),flip(b),unit_del(b,30)]. given #69 (A,wt=17): 42 p(x,b) | p(g(x),x) | x = y | p(y,b) | p(g(y),y). [para(22(a,1),22(a,1))]. given #70 (T,wt=13): 258 p(k,b) | p(x,b) | p(g(x),x) | -p(m,x). [resolve(257,b,103,d)]. given #71 (T,wt=13): 259 p(k,b) | p(x,b) | p(x,g(x)) | -p(m,x). [resolve(257,b,102,d)]. given #72 (T,wt=13): 260 p(k,b) | p(x,b) | p(g(x),x) | -p(k,x). [resolve(257,b,100,d)]. given #73 (T,wt=13): 261 p(k,b) | p(x,b) | p(x,g(x)) | -p(k,x). [resolve(257,b,99,d)]. given #74 (A,wt=16): 43 p(b,b) | p(g(b),b) | g(b) = b | g(g(b)) != b. [factor(39,b,d),flip(c)]. given #75 (T,wt=13): 283 p(k,b) | p(f(k),b) | p(g(f(k)),f(k)). [resolve(260,d,264,b),merge(d)]. given #76 (T,wt=13): 284 p(k,b) | p(f(k),b) | p(f(k),g(f(k))). [resolve(261,d,264,b),merge(d)]. given #77 (T,wt=15): 241 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(b)),m). [factor(237,a,c),merge(c)]. given #78 (T,wt=15): 248 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(b)),m). [factor(245,a,c),merge(c)]. given #79 (A,wt=16): 54 p(x,b) | p(x,g(x)) | k = y | x != y | p(y,k). [para(20(a,1),26(b,1))]. given #80 (T,wt=15): 269 p(k,b) | f(k) = k | f(k) = m | f(k) = b. [resolve(263,b,6,d),flip(b),flip(c),flip(d)]. given #81 (T,wt=14): 321 p(k,b) | f(k) = m | f(k) = b | -p(k,m). [resolve(269,b,10,c),flip(d),unit_del(d,30)]. given #82 (T,wt=11): 327 p(k,b) | f(k) = m | f(k) = b. [resolve(321,d,257,b),merge(d)]. given #83 (T,wt=10): 328 p(k,b) | f(k) = b | -p(k,m). [resolve(327,b,8,c),flip(c),unit_del(c,30)]. given #84 (A,wt=16): 55 p(x,b) | p(g(x),x) | k = y | x != y | p(y,k). [para(22(a,1),26(b,1))]. given #85 (T,wt=7): 333 p(k,b) | f(k) = b. [resolve(328,c,257,b),merge(c)]. ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.00) seconds. % Length of proof is 50. % Level of proof is 15. % Maximum clause weight is 18. % Given clauses 85. 1 x = m | p(x,m) | y = m | y = x | -p(x,y) | -p(y,x). [assumption]. 2 m = x | p(x,m) | m = y | y = x | -p(x,y) | -p(y,x). [copy(1),flip(a),flip(c)]. 3 x = b | -p(x,b) | y = b | y = x | -p(x,y) | -p(y,x). [assumption]. 4 b = x | -p(x,b) | b = y | y = x | -p(x,y) | -p(y,x). [copy(3),flip(a),flip(c)]. 5 x = k | x = m | x = b | -p(x,k). [assumption]. 6 k = x | m = x | b = x | -p(x,k). [copy(5),flip(a),flip(b),flip(c)]. 7 x = m | -p(x,m) | f(x) != m. [assumption]. 8 m = x | -p(x,m) | f(x) != m. [copy(7),flip(a)]. 9 x = m | -p(x,m) | f(x) != x. [assumption]. 10 m = x | -p(x,m) | f(x) != x. [copy(9),flip(a)]. 11 x = m | -p(x,m) | p(x,f(x)). [assumption]. 12 m = x | -p(x,m) | p(x,f(x)). [copy(11),flip(a)]. 13 x = m | -p(x,m) | p(f(x),x). [assumption]. 14 m = x | -p(x,m) | p(f(x),x). [copy(13),flip(a)]. 15 x = b | p(x,b) | g(x) != b. [assumption]. 16 b = x | p(x,b) | g(x) != b. [copy(15),flip(a)]. 17 x = b | p(x,b) | g(x) != x. [assumption]. 18 b = x | p(x,b) | g(x) != x. [copy(17),flip(a)]. 19 x = b | p(x,b) | p(x,g(x)). [assumption]. 20 b = x | p(x,b) | p(x,g(x)). [copy(19),flip(a)]. 21 x = b | p(x,b) | p(g(x),x). [assumption]. 22 b = x | p(x,b) | p(g(x),x). [copy(21),flip(a)]. 23 x = k | x != m | p(x,k). [assumption]. 24 k = x | m != x | p(x,k). [copy(23),flip(a),flip(b)]. 25 x = k | x != b | p(x,k). [assumption]. 26 k = x | b != x | p(x,k). [copy(25),flip(a),flip(b)]. 27 m != b. [assumption]. 28 b != k. [assumption]. 29 k != b. [copy(28),flip(a)]. 30 k != m. [assumption]. 48 p(m,k). [xx_res(24,b),unit_del(a,30)]. 53 p(b,k). [xx_res(26,b),unit_del(a,29)]. 60 p(k,b) | p(g(k),k). [resolve(29,a,22,a(flip))]. 61 p(k,b) | p(k,g(k)). [resolve(29,a,20,a(flip))]. 82 -p(k,b) | -p(k,m). [resolve(48,a,4,f),flip(a),flip(c),flip(d),unit_del(a,29),unit_del(c,27),unit_del(d,30)]. 84 p(k,m) | -p(k,b). [resolve(53,a,2,f),flip(a),flip(d),unit_del(a,30),unit_del(c,27),unit_del(d,29)]. 109 p(k,b) | g(k) = k | g(k) = m | g(k) = b. [resolve(60,b,6,d),flip(b),flip(c),flip(d)]. 249 p(k,b) | g(k) = m | g(k) = b. [resolve(109,b,18,c),flip(d),merge(e),unit_del(d,29)]. 250 p(k,b) | g(k) = b | p(k,m). [para(249(b,1),61(b,2)),merge(c)]. 257 p(k,b) | p(k,m). [resolve(250,b,16,c),flip(c),merge(d),unit_del(c,29)]. 263 p(k,b) | p(f(k),k). [resolve(257,b,14,b),flip(b),unit_del(b,30)]. 264 p(k,b) | p(k,f(k)). [resolve(257,b,12,b),flip(b),unit_del(b,30)]. 269 p(k,b) | f(k) = k | f(k) = m | f(k) = b. [resolve(263,b,6,d),flip(b),flip(c),flip(d)]. 321 p(k,b) | f(k) = m | f(k) = b | -p(k,m). [resolve(269,b,10,c),flip(d),unit_del(d,30)]. 327 p(k,b) | f(k) = m | f(k) = b. [resolve(321,d,257,b),merge(d)]. 328 p(k,b) | f(k) = b | -p(k,m). [resolve(327,b,8,c),flip(c),unit_del(c,30)]. 333 p(k,b) | f(k) = b. [resolve(328,c,257,b),merge(c)]. 338 p(k,b). [para(333(b,1),264(b,2)),merge(b),merge(c)]. 340 p(k,m). [back_unit_del(84),unit_del(b,338)]. 341 $F. [back_unit_del(82),unit_del(a,338),unit_del(b,340)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=85. Generated=1060. Kept=326. proofs=1. Usable=58. Sos=140. Demods=0. Limbo=3, Disabled=141. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=733. Back_subsumed=122. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=3. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=4819. Nonunit_bsub_feature_tests=1256. Megabytes=0.32. User_CPU=0.03, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 21142 exit (max_proofs) Mon Mar 19 17:05:50 2007