============================== Prover9 =============================== Prover9 (64) version 2017-09A, September 2017. Process 10994 was started by veroff on b146-05, Thu Aug 26 22:42:06 2021 The command was "prover9 -f Sh-1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file Sh-1.in assign(order,kbo). set(lex_order_vars). set(para_from_small). assign(max_weight,5). clear(back_demod). set(restrict_denials). clear(cac_redundancy). formulas(assumptions). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1"). end_of_list. formulas(goals). f(f(x,x),f(x,x)) = x # label("Sheffer_1"). f(x,f(y,f(y,y))) = f(x,x) # label("Sheffer_2"). f(f(x,f(y,z)),f(x,f(y,z))) = f(f(f(y,y),x),f(f(z,z),x)) # label("Sheffer_3"). end_of_list. formulas(hints). f(f(x,x),f(x,x)) = x. f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y. f(f(c1,c1),f(c1,c1)) != c1. f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z)))) = y. f(f(x,f(f(f(y,f(f(y,y),y)),x),x)),y) = f(y,f(f(y,y),y)). f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x) = f(x,f(f(x,x),x)). f(x,f(f(x,x),x)) = f(x,x). f(f(x,x),f(x,f(y,x))) = x. $F. f(x,f(y,f(y,y))) = f(x,x). f(c2,f(c3,f(c3,c3))) != f(c2,c2). f(f(x,f(f(x,x),x)),f(x,x)) = x. f(f(x,f(f(f(y,y),x),x)),y) = f(y,y). f(f(f(x,y),f(f(f(x,y),f(x,y)),f(x,y))),f(f(x,y),f(x,y))) = f(y,f(f(f(f(x,y),f(x,y)),y),y)). f(x,f(f(f(f(y,x),f(y,x)),x),x)) = f(y,x). f(f(x,x),f(y,x)) = x. f(x,f(y,f(x,x))) = f(x,x). f(f(f(x,y),f(x,y)),y) = f(x,y). f(x,f(f(y,x),x)) = f(y,x). f(f(x,y),f(x,f(z,y))) = x. f(f(x,f(y,z)),f(x,z)) = x. f(f(f(x,f(y,z)),z),x) = f(x,f(y,z)). f(x,f(f(x,y),f(z,y))) = f(x,y). f(x,f(f(y,x),x)) = f(x,y). f(f(x,y),f(y,f(z,x))) = y. f(x,y) = f(y,x). f(f(x,y),f(x,x)) = x. f(f(x,f(y,z)),f(z,x)) = x. f(f(x,y),f(y,f(x,z))) = y. f(f(x,f(y,z)),f(y,x)) = x. f(f(f(x,y),f(x,z)),z) = f(x,z). f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = f(f(x,f(y,z)),f(y,x)). f(f(x,f(y,f(x,z))),y) = f(y,f(x,z)). f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). f(f(x,f(y,f(x,z))),y) = f(y,f(z,x)). f(x,f(y,f(x,y))) = f(x,x). f(x,f(y,z)) = f(x,f(z,y)). f(f(x,f(y,x)),y) = f(y,y). f(f(x,f(y,z)),f(f(y,x),x)) = f(f(x,f(y,z)),f(x,f(y,z))). f(x,f(y,y)) = f(x,f(y,x)). f(f(x,y),z) = f(z,f(y,x)). f(f(x,y),y) = f(y,f(x,x)). f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x. f(x,f(y,f(x,f(z,f(y,x))))) = f(x,x). f(x,f(y,f(z,f(x,y)))) = f(x,f(y,y)). f(x,f(y,f(f(y,x),z))) = f(x,f(y,y)). f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(y,z)),f(x,f(y,y))). f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,y)) = f(x,f(y,y)). f(f(f(f(x,y),f(x,y)),f(f(z,f(f(x,y),z)),f(x,y))),f(x,x)) = f(f(z,f(f(x,y),z)),f(x,x)). f(f(x,f(f(y,z),x)),f(y,y)) = f(f(y,z),f(y,y)). f(f(x,f(f(y,z),x)),f(y,y)) = y. f(x,f(f(y,f(f(x,z),y)),x)) = f(y,f(f(x,z),y)). f(x,f(f(y,f(y,f(z,x))),x)) = f(y,f(f(x,f(y,f(x,z))),y)). f(x,f(f(y,f(y,f(z,x))),x)) = f(y,f(y,f(z,x))). f(x,f(y,f(z,f(z,f(u,f(y,x)))))) = f(x,f(y,y)). f(x,f(y,f(y,f(z,f(x,y))))) = f(x,f(y,f(x,x))). f(x,f(y,f(y,f(z,f(x,y))))) = f(x,x). f(f(f(x,x),y),f(f(z,z),y)) = f(f(y,f(x,z)),f(y,f(x,z))). f(f(f(c4,c4),c5),f(f(c6,c6),c5)) != f(f(c5,f(c4,c6)),f(c5,f(c4,c6))). f(f(f(x,y),y),f(y,f(z,x))) = f(f(y,f(z,x)),f(y,f(z,x))). f(x,f(y,y)) = f(x,f(x,y)). f(f(x,y),f(z,u)) = f(f(u,z),f(y,x)). f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,f(f(y,y),f(y,y))). f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,z))). f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,y). f(x,f(f(f(y,f(z,x)),f(y,f(z,x))),f(z,z))) = f(x,f(y,f(z,x))). f(x,f(y,f(z,z))) = f(x,f(y,f(z,x))). f(x,f(y,f(f(z,z),x))) = f(x,f(y,z)). f(f(f(x,x),y),f(z,u)) = f(f(u,z),f(y,f(x,f(u,z)))). f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,f(f(z,z),x)))). f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,f(x,f(z,z))))). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(f(x,x),f(x,x)) = x # label("Sheffer_1") # label(non_clause) # label(goal). [goal]. 2 f(x,f(y,f(y,y))) = f(x,x) # label("Sheffer_2") # label(non_clause) # label(goal). [goal]. 3 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(f(y,y),x),f(f(z,z),x)) # label("Sheffer_3") # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1"). [assumption]. f(f(c1,c1),f(c1,c1)) != c1 # label("Sheffer_1"). [deny(1)]. f(c2,f(c3,f(c3,c3))) != f(c2,c2) # label("Sheffer_2"). [deny(2)]. f(f(f(c5,c5),c4),f(f(c6,c6),c4)) != f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) # label("Sheffer_3"). [deny(3)]. end_of_list. formulas(demodulators). end_of_list. % 72 hints input. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label "Sheffer_1" to answer in negative clause % copying label "Sheffer_2" to answer in negative clause % copying label "Sheffer_3" to answer in negative clause % assign(max_proofs, 3). % (Horn set with more than one neg. clause) Term ordering decisions: Function symbol KB weights: c1=1. c2=1. c3=1. c4=1. c5=1. c6=1. f=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 4 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1"). [assumption]. kept: 5 f(f(c1,c1),f(c1,c1)) != c1 # label("Sheffer_1") # answer("Sheffer_1"). [deny(1)]. kept: 6 f(c2,f(c3,f(c3,c3))) != f(c2,c2) # label("Sheffer_2") # answer("Sheffer_2"). [deny(2)]. kept: 7 f(f(f(c5,c5),c4),f(f(c6,c6),c4)) != f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) # label("Sheffer_3") # answer("Sheffer_3"). [deny(3)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 5 f(f(c1,c1),f(c1,c1)) != c1 # label("Sheffer_1") # answer("Sheffer_1"). [deny(1)]. 6 f(c2,f(c3,f(c3,c3))) != f(c2,c2) # label("Sheffer_2") # answer("Sheffer_2"). [deny(2)]. 7 f(f(f(c5,c5),c4),f(f(c6,c6),c4)) != f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) # label("Sheffer_3") # answer("Sheffer_3"). [deny(3)]. end_of_list. formulas(sos). 4 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1"). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 72 hints (72 processed, 0 redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=15): 4 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1"). [assumption]. given #2 (H,wt=29): 8 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(4(a,1),4(a,1,2))]. given #3 (H,wt=19): 9 f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z)))) = y. [para(8(a,1),4(a,1,2,2))]. given #4 (H,wt=23): 10 f(f(x,f(f(f(y,f(f(y,y),y)),x),x)),y) = f(y,f(f(y,y),y)). [para(4(a,1),9(a,1,2))]. given #5 (H,wt=23): 11 f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x) = f(x,f(f(x,x),x)). [para(4(a,1),10(a,1,1,2,1))]. given #6 (H,wt=11): 12 f(x,f(f(x,x),x)) = f(x,x). [para(9(a,1),11(a,1,1)),flip(a)]. given #7 (H,wt=11): 13 f(f(x,x),f(x,f(y,x))) = x. [para(12(a,1),4(a,1,1))]. -------- Proof 1 -------- "Sheffer_1". ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds: "Sheffer_1". % Length of proof is 11. % Level of proof is 8. % Maximum clause weight is 29.000. % Given clauses 7 (0.875 givens/level). 1 f(f(x,x),f(x,x)) = x # label("Sheffer_1") # label(non_clause) # label(goal). [goal]. 4 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1"). [assumption]. 5 f(f(c1,c1),f(c1,c1)) != c1 # label("Sheffer_1") # answer("Sheffer_1"). [deny(1)]. 8 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(4(a,1),4(a,1,2))]. 9 f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z)))) = y. [para(8(a,1),4(a,1,2,2))]. 10 f(f(x,f(f(f(y,f(f(y,y),y)),x),x)),y) = f(y,f(f(y,y),y)). [para(4(a,1),9(a,1,2))]. 11 f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x) = f(x,f(f(x,x),x)). [para(4(a,1),10(a,1,1,2,1))]. 12 f(x,f(f(x,x),x)) = f(x,x). [para(9(a,1),11(a,1,1)),flip(a)]. 13 f(f(x,x),f(x,f(y,x))) = x. [para(12(a,1),4(a,1,1))]. 16 f(f(x,x),f(x,x)) = x. [para(12(a,1),13(a,1,2))]. 17 $F # answer("Sheffer_1"). [resolve(16,a,5,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 5 given #8 (H,wt=9): 16 f(f(x,x),f(x,x)) = x. [para(12(a,1),13(a,1,2))]. given #9 (H,wt=13): 14 f(f(x,f(f(x,x),x)),f(x,x)) = x. [para(12(a,1),4(a,1,2))]. given #10 (H,wt=15): 15 f(f(x,f(f(f(y,y),x),x)),y) = f(y,y). [para(13(a,1),9(a,1,2))]. given #11 (H,wt=37): 18 f(f(f(x,y),f(f(f(x,y),f(x,y)),f(x,y))),f(f(x,y),f(x,y))) = f(y,f(f(f(f(x,y),f(x,y)),y),y)). [para(15(a,1),8(a,1,1,2,1))]. given #12 (H,wt=17): 19 f(x,f(f(f(f(y,x),f(y,x)),x),x)) = f(y,x). [para(18(a,1),14(a,1))]. => 20 back subsumes hint matchers not on Sos. Reset weight to 513.000. => 21 back subsumes hint matchers not on Sos. Reset weight to 537.000. given #13 (H,wt=9): 22 f(f(x,x),f(y,x)) = x. [para(19(a,1),13(a,1,2))]. given #14 (H,wt=11): 23 f(x,f(y,f(x,x))) = f(x,x). [para(22(a,1),22(a,1,1))]. given #15 (H,wt=13): 24 f(f(f(x,y),f(x,y)),y) = f(x,y). [para(22(a,1),22(a,1,2))]. given #16 (H,wt=11): 25 f(x,f(f(y,x),x)) = f(y,x). [para(24(a,1),19(a,1,2,1))]. given #17 (H,wt=11): 26 f(f(x,y),f(x,f(z,y))) = x. [para(25(a,1),4(a,1,1))]. given #18 (H,wt=11): 27 f(f(x,f(y,z)),f(x,z)) = x. [para(22(a,1),26(a,1,2,2))]. given #19 (H,wt=13): 31 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(26(a,1),27(a,1,1))]. given #20 (H,wt=11): 32 f(x,f(f(y,x),x)) = f(x,y). [para(4(a,1),31(a,1,2)),flip(a)]. given #21 (H,wt=7): 35 f(x,y) = f(y,x). [para(32(a,1),25(a,1))]. given #22 (H,wt=9): 37 f(f(x,y),f(x,x)) = x. [para(32(a,1),27(a,1,1))]. given #23 (H,wt=11): 33 f(f(x,y),f(y,f(z,x))) = y. [para(32(a,1),4(a,1,1))]. given #24 (H,wt=11): 40 f(f(x,f(y,z)),f(z,x)) = x. [para(35(a,1),27(a,1,2))]. given #25 (H,wt=11): 44 f(f(x,y),f(y,f(x,z))) = y. [para(35(a,1),33(a,1,2,2))]. => 47 back subsumes hint matchers not on Sos. Reset weight to 513.000. given #26 (H,wt=11): 46 f(f(x,f(y,z)),f(y,x)) = x. [para(35(a,1),40(a,1,1,2))]. given #27 (H,wt=13): 48 f(f(f(x,y),f(x,z)),z) = f(x,z). [para(44(a,1),33(a,1,2))]. => 52 back subsumes hint matchers not on Sos. Reset weight to 517.000. given #28 (H,wt=15): 30 f(f(f(x,f(y,z)),z),x) = f(x,f(y,z)). [para(27(a,1),26(a,1,2))]. given #29 (H,wt=15): 50 f(f(x,f(y,f(x,z))),y) = f(y,f(x,z)). [para(46(a,1),44(a,1,2))]. given #30 (H,wt=15): 51 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(46(a,1),46(a,1,1))]. given #31 (H,wt=15): 54 f(f(x,f(y,f(x,z))),y) = f(y,f(z,x)). [para(35(a,1),50(a,2,2))]. given #32 (H,wt=11): 56 f(x,f(y,f(x,y))) = f(x,x). [para(26(a,1),54(a,1,1)),flip(a)]. given #33 (H,wt=11): 57 f(x,f(y,z)) = f(x,f(z,y)). [para(54(a,1),50(a,1))]. given #34 (H,wt=11): 58 f(f(x,f(y,x)),y) = f(y,y). [para(56(a,1),35(a,1)),flip(a)]. => 63 back subsumes hint matchers not on Sos. Reset weight to 515.000. given #35 (H,wt=11): 60 f(x,f(y,y)) = f(x,f(y,x)). [para(56(a,1),51(a,1,2))]. given #36 (H,wt=11): 61 f(f(x,y),z) = f(z,f(y,x)). [para(57(a,1),35(a,1)),flip(a)]. given #37 (H,wt=11): 66 f(f(x,y),y) = f(y,f(x,x)). [para(60(a,2),35(a,1)),flip(a)]. given #38 (H,wt=11): 67 f(x,f(y,y)) = f(x,f(x,y)). [para(35(a,1),60(a,2,2))]. given #39 (H,wt=15): 68 f(f(x,y),f(z,u)) = f(f(u,z),f(y,x)). [para(61(a,1),57(a,1))]. given #40 (H,wt=23): 49 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = f(f(x,f(y,z)),f(y,x)). [para(46(a,1),31(a,1,2,1))]. given #41 (H,wt=15): 69 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x. [para(49(a,2),46(a,1))]. given #42 (H,wt=15): 70 f(x,f(y,f(x,f(z,f(y,x))))) = f(x,x). [para(69(a,1),30(a,1,1)),flip(a)]. given #43 (H,wt=15): 71 f(x,f(y,f(z,f(x,y)))) = f(x,f(y,y)). [para(70(a,1),51(a,1,2)),flip(a)]. given #44 (H,wt=15): 72 f(x,f(y,f(f(y,x),z))) = f(x,f(y,y)). [para(61(a,2),71(a,1,2,2))]. given #45 (H,wt=23): 59 f(f(x,f(y,z)),f(f(y,x),x)) = f(f(x,f(y,z)),f(x,f(y,z))). [para(46(a,1),56(a,1,2,2))]. given #46 (H,wt=23): 64 f(f(f(x,y),y),f(y,f(z,x))) = f(f(y,f(z,x)),f(y,f(z,x))). [para(40(a,1),58(a,1,1,2))]. given #47 (H,wt=23): 73 f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,f(f(y,y),f(y,y))). [para(67(a,1),71(a,1,2,2,2))]. given #48 (H,wt=17): 76 f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,y). [para(22(a,1),73(a,2,2))]. given #49 (H,wt=23): 74 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(y,z)),f(x,f(y,y))). [para(66(a,1),59(a,1,2)),flip(a)]. given #50 (H,wt=21): 77 f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,y)) = f(x,f(y,y)). [para(74(a,2),48(a,1,1))]. given #51 (H,wt=23): 75 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,z))). [para(66(a,1),64(a,1,1)),flip(a)]. given #52 (H,wt=35): 78 f(f(f(f(x,y),f(x,y)),f(f(z,f(f(x,y),z)),f(x,y))),f(x,x)) = f(f(z,f(f(x,y),z)),f(x,x)). [para(58(a,1),77(a,1,1,1))]. given #53 (H,wt=19): 79 f(f(x,f(f(y,z),x)),f(y,y)) = f(f(y,z),f(y,y)). [para(22(a,1),78(a,1,1)),flip(a)]. => 80 back subsumes hint matchers not on Sos. Reset weight to 529.000. given #54 (H,wt=13): 81 f(f(x,f(f(y,z),x)),f(y,y)) = y. [para(79(a,2),37(a,1))]. => 82 back subsumes hint matchers not on Sos. Reset weight to 523.000. => 83 back subsumes hint matchers not on Sos. Reset weight to 515.000. given #55 (H,wt=19): 85 f(x,f(f(y,f(f(x,z),y)),x)) = f(y,f(f(x,z),y)). [para(81(a,1),27(a,1,1))]. given #56 (H,wt=23): 86 f(x,f(f(y,f(y,f(z,x))),x)) = f(y,f(f(x,f(y,f(x,z))),y)). [para(54(a,1),85(a,1,2,1,2))]. given #57 (H,wt=19): 87 f(x,f(f(y,f(y,f(z,x))),x)) = f(y,f(y,f(z,x))). [para(54(a,1),86(a,2,2))]. given #58 (H,wt=19): 88 f(x,f(y,f(z,f(z,f(u,f(y,x)))))) = f(x,f(y,y)). [para(87(a,1),72(a,1,2,2))]. given #59 (H,wt=19): 89 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,f(y,f(x,x))). [para(88(a,1),51(a,1,2)),flip(a)]. given #60 (H,wt=15): 90 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,x). [para(89(a,2),23(a,1))]. -------- Proof 2 -------- "Sheffer_2". ============================== PROOF ================================= % Proof 2 at 0.09 (+ 0.02) seconds: "Sheffer_2". % Length of proof is 57. % Level of proof is 37. % Maximum clause weight is 37.000. % Given clauses 60 (1.622 givens/level). 2 f(x,f(y,f(y,y))) = f(x,x) # label("Sheffer_2") # label(non_clause) # label(goal). [goal]. 4 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1"). [assumption]. 6 f(c2,f(c3,f(c3,c3))) != f(c2,c2) # label("Sheffer_2") # answer("Sheffer_2"). [deny(2)]. 8 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(4(a,1),4(a,1,2))]. 9 f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z)))) = y. [para(8(a,1),4(a,1,2,2))]. 10 f(f(x,f(f(f(y,f(f(y,y),y)),x),x)),y) = f(y,f(f(y,y),y)). [para(4(a,1),9(a,1,2))]. 11 f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x) = f(x,f(f(x,x),x)). [para(4(a,1),10(a,1,1,2,1))]. 12 f(x,f(f(x,x),x)) = f(x,x). [para(9(a,1),11(a,1,1)),flip(a)]. 13 f(f(x,x),f(x,f(y,x))) = x. [para(12(a,1),4(a,1,1))]. 14 f(f(x,f(f(x,x),x)),f(x,x)) = x. [para(12(a,1),4(a,1,2))]. 15 f(f(x,f(f(f(y,y),x),x)),y) = f(y,y). [para(13(a,1),9(a,1,2))]. 18 f(f(f(x,y),f(f(f(x,y),f(x,y)),f(x,y))),f(f(x,y),f(x,y))) = f(y,f(f(f(f(x,y),f(x,y)),y),y)). [para(15(a,1),8(a,1,1,2,1))]. 19 f(x,f(f(f(f(y,x),f(y,x)),x),x)) = f(y,x). [para(18(a,1),14(a,1))]. 22 f(f(x,x),f(y,x)) = x. [para(19(a,1),13(a,1,2))]. 23 f(x,f(y,f(x,x))) = f(x,x). [para(22(a,1),22(a,1,1))]. 24 f(f(f(x,y),f(x,y)),y) = f(x,y). [para(22(a,1),22(a,1,2))]. 25 f(x,f(f(y,x),x)) = f(y,x). [para(24(a,1),19(a,1,2,1))]. 26 f(f(x,y),f(x,f(z,y))) = x. [para(25(a,1),4(a,1,1))]. 27 f(f(x,f(y,z)),f(x,z)) = x. [para(22(a,1),26(a,1,2,2))]. 30 f(f(f(x,f(y,z)),z),x) = f(x,f(y,z)). [para(27(a,1),26(a,1,2))]. 31 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(26(a,1),27(a,1,1))]. 32 f(x,f(f(y,x),x)) = f(x,y). [para(4(a,1),31(a,1,2)),flip(a)]. 33 f(f(x,y),f(y,f(z,x))) = y. [para(32(a,1),4(a,1,1))]. 35 f(x,y) = f(y,x). [para(32(a,1),25(a,1))]. 37 f(f(x,y),f(x,x)) = x. [para(32(a,1),27(a,1,1))]. 40 f(f(x,f(y,z)),f(z,x)) = x. [para(35(a,1),27(a,1,2))]. 44 f(f(x,y),f(y,f(x,z))) = y. [para(35(a,1),33(a,1,2,2))]. 46 f(f(x,f(y,z)),f(y,x)) = x. [para(35(a,1),40(a,1,1,2))]. 48 f(f(f(x,y),f(x,z)),z) = f(x,z). [para(44(a,1),33(a,1,2))]. 49 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = f(f(x,f(y,z)),f(y,x)). [para(46(a,1),31(a,1,2,1))]. 50 f(f(x,f(y,f(x,z))),y) = f(y,f(x,z)). [para(46(a,1),44(a,1,2))]. 51 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(46(a,1),46(a,1,1))]. 54 f(f(x,f(y,f(x,z))),y) = f(y,f(z,x)). [para(35(a,1),50(a,2,2))]. 56 f(x,f(y,f(x,y))) = f(x,x). [para(26(a,1),54(a,1,1)),flip(a)]. 57 f(x,f(y,z)) = f(x,f(z,y)). [para(54(a,1),50(a,1))]. 58 f(f(x,f(y,x)),y) = f(y,y). [para(56(a,1),35(a,1)),flip(a)]. 59 f(f(x,f(y,z)),f(f(y,x),x)) = f(f(x,f(y,z)),f(x,f(y,z))). [para(46(a,1),56(a,1,2,2))]. 60 f(x,f(y,y)) = f(x,f(y,x)). [para(56(a,1),51(a,1,2))]. 61 f(f(x,y),z) = f(z,f(y,x)). [para(57(a,1),35(a,1)),flip(a)]. 66 f(f(x,y),y) = f(y,f(x,x)). [para(60(a,2),35(a,1)),flip(a)]. 69 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x. [para(49(a,2),46(a,1))]. 70 f(x,f(y,f(x,f(z,f(y,x))))) = f(x,x). [para(69(a,1),30(a,1,1)),flip(a)]. 71 f(x,f(y,f(z,f(x,y)))) = f(x,f(y,y)). [para(70(a,1),51(a,1,2)),flip(a)]. 72 f(x,f(y,f(f(y,x),z))) = f(x,f(y,y)). [para(61(a,2),71(a,1,2,2))]. 74 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(y,z)),f(x,f(y,y))). [para(66(a,1),59(a,1,2)),flip(a)]. 77 f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,y)) = f(x,f(y,y)). [para(74(a,2),48(a,1,1))]. 78 f(f(f(f(x,y),f(x,y)),f(f(z,f(f(x,y),z)),f(x,y))),f(x,x)) = f(f(z,f(f(x,y),z)),f(x,x)). [para(58(a,1),77(a,1,1,1))]. 79 f(f(x,f(f(y,z),x)),f(y,y)) = f(f(y,z),f(y,y)). [para(22(a,1),78(a,1,1)),flip(a)]. 81 f(f(x,f(f(y,z),x)),f(y,y)) = y. [para(79(a,2),37(a,1))]. 85 f(x,f(f(y,f(f(x,z),y)),x)) = f(y,f(f(x,z),y)). [para(81(a,1),27(a,1,1))]. 86 f(x,f(f(y,f(y,f(z,x))),x)) = f(y,f(f(x,f(y,f(x,z))),y)). [para(54(a,1),85(a,1,2,1,2))]. 87 f(x,f(f(y,f(y,f(z,x))),x)) = f(y,f(y,f(z,x))). [para(54(a,1),86(a,2,2))]. 88 f(x,f(y,f(z,f(z,f(u,f(y,x)))))) = f(x,f(y,y)). [para(87(a,1),72(a,1,2,2))]. 89 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,f(y,f(x,x))). [para(88(a,1),51(a,1,2)),flip(a)]. 90 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,x). [para(89(a,2),23(a,1))]. 91 f(x,f(y,f(y,y))) = f(x,x). [para(22(a,1),90(a,1,2,2,2))]. 92 $F # answer("Sheffer_2"). [resolve(91,a,6,a)]. ============================== end of proof ========================== => 93 back subsumes hint matchers not on Sos. Reset weight to 519.000. % Disable descendants (x means already disabled): 6 given #61 (H,wt=11): 91 f(x,f(y,f(y,y))) = f(x,x). [para(22(a,1),90(a,1,2,2,2))]. given #62 (H,wt=25): 94 f(x,f(f(f(y,f(z,x)),f(y,f(z,x))),f(z,z))) = f(x,f(y,f(z,x))). [para(90(a,1),76(a,1,2,2))]. given #63 (H,wt=15): 96 f(x,f(y,f(z,z))) = f(x,f(y,f(z,x))). [para(77(a,1),94(a,1,2))]. => 98 back subsumes hint matchers not on Sos. Reset weight to 523.000. given #64 (H,wt=15): 97 f(x,f(y,f(f(z,z),x))) = f(x,f(y,z)). [para(22(a,1),96(a,1,2,2)),flip(a)]. given #65 (H,wt=21): 99 f(f(f(x,x),y),f(z,u)) = f(f(u,z),f(y,f(x,f(u,z)))). [para(96(a,1),68(a,1)),flip(a)]. given #66 (H,wt=27): 101 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,f(f(z,z),x)))). [para(97(a,2),75(a,2,2))]. given #67 (H,wt=27): 102 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,f(x,f(z,z))))). [para(35(a,1),101(a,2,2,2,2))]. -------- Proof 3 -------- "Sheffer_3". ============================== PROOF ================================= % Proof 3 at 0.13 (+ 0.02) seconds: "Sheffer_3". % Length of proof is 69. % Level of proof is 42. % Maximum clause weight is 37.000. % Given clauses 67 (1.595 givens/level). 3 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(f(y,y),x),f(f(z,z),x)) # label("Sheffer_3") # label(non_clause) # label(goal). [goal]. 4 f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y # label("Sh1"). [assumption]. 7 f(f(f(c5,c5),c4),f(f(c6,c6),c4)) != f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) # label("Sheffer_3") # answer("Sheffer_3"). [deny(3)]. 8 f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z) = f(y,f(f(z,y),y)). [para(4(a,1),4(a,1,2))]. 9 f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z)))) = y. [para(8(a,1),4(a,1,2,2))]. 10 f(f(x,f(f(f(y,f(f(y,y),y)),x),x)),y) = f(y,f(f(y,y),y)). [para(4(a,1),9(a,1,2))]. 11 f(f(f(x,f(y,x)),f(x,f(x,f(y,x)))),x) = f(x,f(f(x,x),x)). [para(4(a,1),10(a,1,1,2,1))]. 12 f(x,f(f(x,x),x)) = f(x,x). [para(9(a,1),11(a,1,1)),flip(a)]. 13 f(f(x,x),f(x,f(y,x))) = x. [para(12(a,1),4(a,1,1))]. 14 f(f(x,f(f(x,x),x)),f(x,x)) = x. [para(12(a,1),4(a,1,2))]. 15 f(f(x,f(f(f(y,y),x),x)),y) = f(y,y). [para(13(a,1),9(a,1,2))]. 18 f(f(f(x,y),f(f(f(x,y),f(x,y)),f(x,y))),f(f(x,y),f(x,y))) = f(y,f(f(f(f(x,y),f(x,y)),y),y)). [para(15(a,1),8(a,1,1,2,1))]. 19 f(x,f(f(f(f(y,x),f(y,x)),x),x)) = f(y,x). [para(18(a,1),14(a,1))]. 22 f(f(x,x),f(y,x)) = x. [para(19(a,1),13(a,1,2))]. 23 f(x,f(y,f(x,x))) = f(x,x). [para(22(a,1),22(a,1,1))]. 24 f(f(f(x,y),f(x,y)),y) = f(x,y). [para(22(a,1),22(a,1,2))]. 25 f(x,f(f(y,x),x)) = f(y,x). [para(24(a,1),19(a,1,2,1))]. 26 f(f(x,y),f(x,f(z,y))) = x. [para(25(a,1),4(a,1,1))]. 27 f(f(x,f(y,z)),f(x,z)) = x. [para(22(a,1),26(a,1,2,2))]. 30 f(f(f(x,f(y,z)),z),x) = f(x,f(y,z)). [para(27(a,1),26(a,1,2))]. 31 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(26(a,1),27(a,1,1))]. 32 f(x,f(f(y,x),x)) = f(x,y). [para(4(a,1),31(a,1,2)),flip(a)]. 33 f(f(x,y),f(y,f(z,x))) = y. [para(32(a,1),4(a,1,1))]. 35 f(x,y) = f(y,x). [para(32(a,1),25(a,1))]. 37 f(f(x,y),f(x,x)) = x. [para(32(a,1),27(a,1,1))]. 40 f(f(x,f(y,z)),f(z,x)) = x. [para(35(a,1),27(a,1,2))]. 44 f(f(x,y),f(y,f(x,z))) = y. [para(35(a,1),33(a,1,2,2))]. 46 f(f(x,f(y,z)),f(y,x)) = x. [para(35(a,1),40(a,1,1,2))]. 48 f(f(f(x,y),f(x,z)),z) = f(x,z). [para(44(a,1),33(a,1,2))]. 49 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = f(f(x,f(y,z)),f(y,x)). [para(46(a,1),31(a,1,2,1))]. 50 f(f(x,f(y,f(x,z))),y) = f(y,f(x,z)). [para(46(a,1),44(a,1,2))]. 51 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(46(a,1),46(a,1,1))]. 54 f(f(x,f(y,f(x,z))),y) = f(y,f(z,x)). [para(35(a,1),50(a,2,2))]. 56 f(x,f(y,f(x,y))) = f(x,x). [para(26(a,1),54(a,1,1)),flip(a)]. 57 f(x,f(y,z)) = f(x,f(z,y)). [para(54(a,1),50(a,1))]. 58 f(f(x,f(y,x)),y) = f(y,y). [para(56(a,1),35(a,1)),flip(a)]. 59 f(f(x,f(y,z)),f(f(y,x),x)) = f(f(x,f(y,z)),f(x,f(y,z))). [para(46(a,1),56(a,1,2,2))]. 60 f(x,f(y,y)) = f(x,f(y,x)). [para(56(a,1),51(a,1,2))]. 61 f(f(x,y),z) = f(z,f(y,x)). [para(57(a,1),35(a,1)),flip(a)]. 64 f(f(f(x,y),y),f(y,f(z,x))) = f(f(y,f(z,x)),f(y,f(z,x))). [para(40(a,1),58(a,1,1,2))]. 66 f(f(x,y),y) = f(y,f(x,x)). [para(60(a,2),35(a,1)),flip(a)]. 67 f(x,f(y,y)) = f(x,f(x,y)). [para(35(a,1),60(a,2,2))]. 68 f(f(x,y),f(z,u)) = f(f(u,z),f(y,x)). [para(61(a,1),57(a,1))]. 69 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x. [para(49(a,2),46(a,1))]. 70 f(x,f(y,f(x,f(z,f(y,x))))) = f(x,x). [para(69(a,1),30(a,1,1)),flip(a)]. 71 f(x,f(y,f(z,f(x,y)))) = f(x,f(y,y)). [para(70(a,1),51(a,1,2)),flip(a)]. 72 f(x,f(y,f(f(y,x),z))) = f(x,f(y,y)). [para(61(a,2),71(a,1,2,2))]. 73 f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,f(f(y,y),f(y,y))). [para(67(a,1),71(a,1,2,2,2))]. 74 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(y,z)),f(x,f(y,y))). [para(66(a,1),59(a,1,2)),flip(a)]. 75 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,z))). [para(66(a,1),64(a,1,1)),flip(a)]. 76 f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,y). [para(22(a,1),73(a,2,2))]. 77 f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,y)) = f(x,f(y,y)). [para(74(a,2),48(a,1,1))]. 78 f(f(f(f(x,y),f(x,y)),f(f(z,f(f(x,y),z)),f(x,y))),f(x,x)) = f(f(z,f(f(x,y),z)),f(x,x)). [para(58(a,1),77(a,1,1,1))]. 79 f(f(x,f(f(y,z),x)),f(y,y)) = f(f(y,z),f(y,y)). [para(22(a,1),78(a,1,1)),flip(a)]. 81 f(f(x,f(f(y,z),x)),f(y,y)) = y. [para(79(a,2),37(a,1))]. 85 f(x,f(f(y,f(f(x,z),y)),x)) = f(y,f(f(x,z),y)). [para(81(a,1),27(a,1,1))]. 86 f(x,f(f(y,f(y,f(z,x))),x)) = f(y,f(f(x,f(y,f(x,z))),y)). [para(54(a,1),85(a,1,2,1,2))]. 87 f(x,f(f(y,f(y,f(z,x))),x)) = f(y,f(y,f(z,x))). [para(54(a,1),86(a,2,2))]. 88 f(x,f(y,f(z,f(z,f(u,f(y,x)))))) = f(x,f(y,y)). [para(87(a,1),72(a,1,2,2))]. 89 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,f(y,f(x,x))). [para(88(a,1),51(a,1,2)),flip(a)]. 90 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,x). [para(89(a,2),23(a,1))]. 94 f(x,f(f(f(y,f(z,x)),f(y,f(z,x))),f(z,z))) = f(x,f(y,f(z,x))). [para(90(a,1),76(a,1,2,2))]. 96 f(x,f(y,f(z,z))) = f(x,f(y,f(z,x))). [para(77(a,1),94(a,1,2))]. 97 f(x,f(y,f(f(z,z),x))) = f(x,f(y,z)). [para(22(a,1),96(a,1,2,2)),flip(a)]. 99 f(f(f(x,x),y),f(z,u)) = f(f(u,z),f(y,f(x,f(u,z)))). [para(96(a,1),68(a,1)),flip(a)]. 101 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,f(f(z,z),x)))). [para(97(a,2),75(a,2,2))]. 102 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,f(x,f(z,z))))). [para(35(a,1),101(a,2,2,2,2))]. 103 f(f(f(x,x),y),f(f(z,z),y)) = f(f(y,f(x,z)),f(y,f(x,z))). [para(102(a,2),99(a,2))]. 104 $F # answer("Sheffer_3"). [resolve(103,a,7,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=67. Generated=31563. Kept=98. proofs=3. Usable=55. Sos=25. Demods=0. Limbo=0, Disabled=21. Hints=72. Kept_by_rule=0, Deleted_by_rule=30519. Forward_subsumed=946. Back_subsumed=15. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.27. User_CPU=0.13, System_CPU=0.02, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 3 proofs. ------ process 10994 exit (max_proofs) ------  Process 10994 exit (max_proofs) Thu Aug 26 22:42:06 2021