============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 4412 was started by mccune on cleo.thornwood, Wed Nov 22 12:04:01 2006 The command was "/home/mccune/bin/prover9 -f BA2.in BA2-interp.outx". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file BA2.in set(lex_order_vars). set(restrict_denials). assign(new_constants,1). assign(age_part,1). assign(false_part,4). assign(true_part,1). assign(max_minutes,5). % assign(max_minutes, 5) -> assign(max_seconds, 300). formulas(sos). f(x,y) = f(y,x) # label(commutativity). f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). end_of_list. formulas(goals). f(f(x,x),f(x,x)) = x & f(x,f(y,f(y,y))) = f(x,x) & f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # answer("Sheffer"). end_of_list. % Reading from file BA2-interp.outx list(interpretations). interpretation(6,[number = 1,seconds = 0],[function(c1,[0]),function(c2,[2]),function(c3,[1]),function(f(_,_),[3,3,1,1,1,1,3,4,5,0,1,2,1,5,5,1,1,1,1,0,1,0,1,1,1,1,1,1,1,1,1,2,1,1,1,2])]). 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 & f(x,f(y,f(y,y))) = f(x,x) & f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # answer("Sheffer") # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(x,y) = f(y,x) # label(commutativity). [assumption]. f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2). [assumption]. f(f(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(f(c5,c5),c4),f(f(c6,c6),c4)) != f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) # answer("Sheffer"). [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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c4, c5, c6, f ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: % set(back_unit_deletion). % (Horn set with negative nonunits) % set(back_unit_deletion) -> set(unit_deletion). % Operation f is commutative; C redundancy checks enabled. restricted denial: (wt=43): 5 f(f(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # answer("Sheffer"). [copy(4),rewrite(2(25),2(30)),flip(c)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 5 f(f(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # answer("Sheffer"). [copy(4),rewrite(2(25),2(30)),flip(c)]. end_of_list. formulas(sos). 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [assumption]. end_of_list. formulas(demodulators). 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. % (lex-dep) 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. given #2 (I,wt=11): 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [assumption]. given #3 (F,wt=11): 6 f(f(x,y),f(y,f(x,z))) = y # label(false). [para(2(a,1),3(a,1,1))]. given #4 (F,wt=11): 9 f(f(x,y),f(x,f(z,y))) = x # label(false). [para(6(a,1),3(a,1,2,2)),rewrite(2(4))]. given #5 (F,wt=11): 12 f(f(x,y),f(y,f(z,x))) = y # label(false). [para(6(a,1),6(a,1,2,2)),rewrite(2(2),2(3),2(4))]. given #6 (T,wt=11): 8 f(x,f(x,f(x,y))) = f(x,y). [para(3(a,1),3(a,1,2)),rewrite(2(2),2(3))]. restricted denial: (wt=34): 20 f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # answer("Sheffer"). [back_rewrite(5),rewrite(19(7)),xx(a)]. given #7 (A,wt=17): 7 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [para(3(a,1),3(a,1,1)),rewrite(2(4))]. given #8 (F,wt=9): 19 f(f(x,x),f(x,y)) = x. [para(8(a,1),3(a,1,2))]. given #9 (F,wt=11): 10 f(x,f(x,f(y,x))) = f(y,x). [para(6(a,1),3(a,1,2)),rewrite(2(2),2(3))]. given #10 (F,wt=11): 30 f(x,f(y,f(x,x))) = f(x,x). [para(19(a,1),9(a,1,2)),rewrite(2(2),2(3))]. given #11 (F,wt=9): 33 f(f(x,y),f(y,y)) = y. [para(30(a,1),6(a,1,2))]. given #12 (T,wt=13): 13 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(3(a,1),9(a,1,2)),rewrite(2(4))]. given #13 (A,wt=19): 11 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)). [para(3(a,1),6(a,1,1)),rewrite(2(4))]. given #14 (F,wt=13): 15 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(6(a,1),9(a,1,2)),rewrite(2(4))]. given #15 (F,wt=13): 16 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(3(a,1),12(a,1,2)),rewrite(2(2),2(4),2(5))]. given #16 (F,wt=13): 17 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(9(a,1),12(a,1,2)),rewrite(2(2),2(4),2(5))]. given #17 (F,wt=13): 66 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(2(a,1),16(a,1,2,1)),rewrite(2(2),2(3),2(5))]. given #18 (T,wt=15): 18 f(f(x,y),f(x,f(z,f(x,f(x,y))))) = x. [para(8(a,1),3(a,1,1)),rewrite(2(4))]. given #19 (A,wt=19): 14 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)). [para(9(a,1),6(a,1,1)),rewrite(2(4))]. given #20 (F,wt=15): 24 f(f(x,y),f(x,f(z,f(x,f(y,u))))) = x. [para(7(a,1),9(a,1,2)),rewrite(2(6))]. given #21 (F,wt=15): 26 f(x,f(f(x,x),f(y,f(x,z)))) = f(x,x). [para(8(a,1),7(a,1,2,2,2))]. given #22 (F,wt=13): 105 f(x,f(f(x,x),f(y,z))) = f(x,x). [para(11(a,1),26(a,1,2))]. given #23 (F,wt=15): 29 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y). [para(19(a,1),6(a,1,1)),rewrite(2(3))]. given #24 (T,wt=15): 36 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(3(a,1),13(a,1,2,2)),rewrite(2(3))]. given #25 (A,wt=21): 21 f(f(x,y),f(x,f(z,f(f(x,y),f(u,f(x,f(y,v))))))) = x. [para(7(a,1),3(a,1,1)),rewrite(2(7))]. given #26 (F,wt=11): 117 f(x,f(y,f(x,y))) = f(x,x) # label(false). [para(9(a,1),36(a,1,2)),rewrite(2(3)),flip(a)]. restricted denial: (wt=34): 175 f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) # answer("Sheffer"). [back_rewrite(20),rewrite(169(27),169(32))]. given #27 (F,wt=11): 169 f(x,f(y,y)) = f(x,f(x,y)) # label(false). [para(117(a,1),36(a,1,2)),rewrite(2(3))]. given #28 (F,wt=11): 176 f(x,f(y,y)) = f(x,f(y,x)) # label(false). [para(169(a,1),2(a,2)),rewrite(2(2),2(3))]. given #29 (F,wt=11): 179 f(x,f(x,f(y,y))) = f(y,x) # label(false). [para(169(a,1),9(a,1)),rewrite(2(2),176(2,R),2(4),176(4,R),2(6),6(6),2(3))]. given #30 (T,wt=15): 38 f(f(x,y),f(y,f(z,f(y,f(x,u))))) = y. [para(6(a,1),13(a,1,2,1)),rewrite(2(4),6(10))]. given #31 (A,wt=31): 22 f(f(x,y),f(f(x,z),f(f(x,y),f(u,f(x,f(y,v)))))) = f(f(x,y),f(u,f(x,f(y,v)))). [para(7(a,1),6(a,1,1)),rewrite(2(8))]. given #32 (F,wt=11): 182 f(x,f(y,f(y,x))) = f(x,x) # label(false). [para(169(a,1),33(a,1,1)),rewrite(19(5),2(3))]. given #33 (F,wt=15): 173 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x # label(false). [back_rewrite(153),rewrite(169(5),2(6))]. given #34 (F,wt=15): 197 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x) # label(false). [back_rewrite(170),rewrite(176(6,R),2(4))]. given #35 (F,wt=15): 201 f(f(x,f(y,z)),f(x,f(z,f(y,y)))) = x # label(false). [para(176(a,2),9(a,1,2,2))]. restricted denial: (wt=23): 453 f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) # answer("Sheffer"). [back_unit_del(175),unit_del(a,452)]. given #36 (T,wt=11): 452 f(x,f(y,f(y,y))) = f(x,x). [para(201(a,1),201(a,1,2)),rewrite(2(5),176(5),2(4),2(6),177(6)),flip(a)]. NOTE: New constant: f(x,f(x,x)) = c_0. [new_symbol(466)]. NOTE: New Function symbol precedence: lex([ c4, c5, c6, c_0, f ]). NOTE: sn=94, num_tables=182 NOTE: updating interpretation 1: c_0=1. restricted denial: (wt=19): 551 f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) != f(c_0,f(c4,f(c5,c6))) # answer("Sheffer"). [back_rewrite(453),rewrite(541(11,R),2(7)),flip(a)]. given #37 (A,wt=21): 23 f(f(x,y),f(y,f(z,f(f(x,y),f(u,f(y,f(x,v))))))) = y. [para(6(a,1),7(a,1,2,1)),rewrite(2(5),6(13))]. given #38 (F,wt=11): 606 f(x,f(y,f(y,x))) = f(x,x) # label(false). [para(19(a,1),23(a,1,2)),rewrite(176(2),2(1),2(3))]. given #39 (F,wt=15): 220 f(f(x,y),f(x,f(z,f(z,f(y,y))))) = x # label(false). [para(179(a,2),3(a,1,2,2))]. given #40 (F,wt=15): 221 f(f(x,y),f(y,f(z,f(z,f(x,x))))) = y # label(false). [para(179(a,2),6(a,1,2,2))]. given #41 (F,wt=15): 223 f(x,f(x,f(y,f(y,f(x,x))))) = f(x,y) # label(false). [para(179(a,2),8(a,1,2,2))]. given #42 (T,wt=7): 504 f(x,f(x,x)) = c_0. [new_symbol(466)]. given #43 (A,wt=21): 25 f(x,f(f(x,y),f(z,f(x,f(u,f(x,f(x,y))))))) = f(x,y). [para(8(a,1),7(a,1,2,1)),rewrite(2(4),8(11))]. given #44 (F,wt=15): 231 f(x,f(y,f(y,f(z,z)))) = f(x,f(z,y)) # label(false). [para(179(a,1),11(a,1,2,1,2)),rewrite(14(6)),flip(a)]. given #45 (F,wt=15): 335 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x # label(false). [para(182(a,1),12(a,1,2,2)),rewrite(2(3))]. given #46 (F,wt=15): 403 f(x,f(y,f(x,f(z,f(y,y))))) = f(x,x) # label(false). [para(19(a,1),197(a,1,2,1)),rewrite(2(2))]. given #47 (F,wt=15): 546 f(c_0,f(x,f(y,f(y,f(z,f(x,x)))))) = x # label(false). [back_rewrite(359),rewrite(504(2))]. given #48 (T,wt=7): 535 f(c_0,f(x,x)) = x. [back_rewrite(463),rewrite(504(3),2(3))]. given #49 (A,wt=27): 27 f(x,f(f(x,y),f(z,f(x,f(u,f(f(x,y),f(v,f(x,f(y,w))))))))) = f(x,y). [para(7(a,1),7(a,1,2,1)),rewrite(2(7),7(17))]. given #50 (F,wt=15): 572 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z) # label(false). [back_rewrite(247),rewrite(176(2),2(1),541(5,R),2(5))]. given #51 (F,wt=13): 897 f(f(x,x),f(y,f(y,f(x,z)))) = x # label(false). [para(3(a,1),572(a,1,2,2)),rewrite(2(5),541(5),2(5),3(9))]. given #52 (F,wt=13): 899 f(f(x,f(x,f(y,z))),f(z,z)) = z # label(false). [para(6(a,1),572(a,1,2,2)),rewrite(2(5),541(5),6(9))]. given #53 (F,wt=15): 636 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x) # label(false). [para(23(a,1),197(a,1,2,2,2)),rewrite(541(3,R),2(3),2(5))]. given #54 (T,wt=7): 541 f(x,c_0) = f(x,x). [back_rewrite(452),rewrite(504(2))]. given #55 (A,wt=19): 32 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)). [para(30(a,1),6(a,1,1)),rewrite(2(5))]. given #56 (F,wt=15): 639 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x # label(false). [para(606(a,1),9(a,1,2,2)),rewrite(176(5),2(4),2(6))]. given #57 (F,wt=15): 662 f(x,f(f(x,y),f(c_0,f(y,z)))) = f(x,x) # label(false). [para(220(a,1),197(a,1,2,2,2)),rewrite(541(3,R),2(3),2(5))]. given #58 (F,wt=15): 758 f(x,f(c_0,f(y,z))) = f(x,f(x,f(y,z))) # label(false). [para(231(a,1),176(a,1,2)),rewrite(176(2),2(1),8(3),2(2),541(3,R),2(3),176(6),2(5),8(7),2(6))]. given #59 (F,wt=15): 760 f(x,f(x,f(c_0,f(y,z)))) = f(x,f(y,z)) # label(false). [para(231(a,1),179(a,1,2,2)),rewrite(176(2),2(1),8(3),2(2),541(3,R),2(3),176(7),2(6),8(8),2(7))]. given #60 (T,wt=9): 775 f(f(x,y),f(c_0,c_0)) = c_0. [para(231(a,1),504(a,1,2)),rewrite(176(2),2(1),8(3),176(3),2(2),8(4),2(3),541(4,R),2(4),176(5,R))]. given #61 (A,wt=19): 34 f(f(x,y),f(y,f(z,f(f(x,y),f(u,f(y,y)))))) = y. [para(33(a,1),7(a,1,2,1)),rewrite(2(4),33(11))]. given #62 (F,wt=15): 811 f(x,f(y,f(x,f(z,f(z,y))))) = f(x,x) # label(false). [para(2(a,1),403(a,1,2)),rewrite(176(2),2(1),2(4))]. given #63 (F,wt=15): 821 f(x,f(y,f(z,f(x,x)))) = f(x,f(x,y)) # label(false). [para(403(a,1),36(a,1,2)),rewrite(176(2),2(1)),flip(a)]. given #64 (F,wt=15): 832 f(x,f(c_0,f(y,f(y,f(z,f(z,x)))))) = c_0 # label(false). [para(546(a,1),9(a,1,2)),rewrite(176(3),2(2),2(7))]. given #65 (F,wt=15): 834 f(x,f(y,f(y,f(z,f(x,x))))) = f(x,x) # label(false). [para(546(a,1),33(a,1,1)),rewrite(541(11,R),2(7),546(7)),flip(a)]. given #66 (T,wt=11): 530 f(x,f(c_0,f(x,y))) = f(x,y). [back_rewrite(472),rewrite(504(3),2(3))]. given #67 (A,wt=17): 35 f(f(x,y),f(x,f(z,f(f(x,y),f(y,u))))) = x. [para(13(a,1),3(a,1,1)),rewrite(2(5))]. given #68 (F,wt=15): 992 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x) # label(false). [para(19(a,1),899(a,1,2)),rewrite(176(2),2(1),2(5))]. given #69 (F,wt=15): 1054 f(x,f(f(x,f(y,z)),f(z,z))) = f(x,x) # label(false). [para(66(a,1),636(a,1,2,2)),rewrite(2(4),541(4))]. given #70 (F,wt=15): 1317 f(x,f(y,f(z,f(z,x)))) = f(x,f(y,y)) # label(false). [para(821(a,1),2(a,2)),rewrite(176(2),2(1),2(4),2(5),176(6,R))]. given #71 (F,wt=15): 1324 f(x,f(x,f(y,f(z,f(x,x))))) = f(x,y) # label(false). [para(821(a,2),8(a,1,2))]. given #72 (T,wt=11): 540 f(f(x,x),f(c_0,f(x,y))) = c_0. [back_rewrite(456),rewrite(504(4),2(4),504(7))]. given #73 (A,wt=23): 37 f(f(x,y),f(f(x,z),f(f(x,y),f(y,u)))) = f(f(x,y),f(y,u)). [para(13(a,1),6(a,1,1)),rewrite(2(6))]. given #74 (F,wt=15): 1443 f(f(x,f(y,z)),f(c_0,f(x,f(x,y)))) = c_0 # label(false). [para(7(a,1),832(a,1,2,2,2))]. given #75 (F,wt=15): 1448 f(f(x,y),f(c_0,f(x,f(x,f(y,z))))) = c_0 # label(false). [para(11(a,1),832(a,1,2,2,2))]. given #76 (F,wt=15): 1641 f(x,f(y,f(z,f(x,x)))) = f(x,f(y,y)) # label(false). [para(1317(a,2),2(a,2)),rewrite(2(2),2(3),176(4,R)),flip(a)]. given #77 (F,wt=15): 1838 f(f(x,f(y,z)),f(c_0,f(x,f(x,z)))) = c_0 # label(false). [para(2(a,1),1443(a,1,1,2))]. given #78 (T,wt=11): 604 f(x,f(c_0,f(y,x))) = f(y,x). [para(23(a,1),19(a,1,2)),rewrite(541(3,R),2(3),2(4))]. given #79 (A,wt=15): 39 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [para(6(a,1),13(a,1,2,2)),rewrite(2(3))]. given #80 (F,wt=15): 1849 f(f(x,y),f(c_0,f(y,f(y,f(x,z))))) = c_0 # label(false). [para(16(a,1),1443(a,1,1))]. given #81 (F,wt=15): 1885 f(f(x,f(y,f(y,z))),f(c_0,f(x,z))) = c_0 # label(false). [para(32(a,1),1443(a,1,1,2)),rewrite(176(2),2(1),176(6),2(5),8(7))]. given #82 (F,wt=15): 2103 f(f(x,f(y,f(y,z))),f(c_0,f(z,x))) = c_0 # label(false). [para(2(a,1),1885(a,1,1)),rewrite(2(3),2(5))]. given #83 (F,wt=17): 157 f(x,f(f(x,y),f(f(x,y),f(y,z)))) = f(x,x) # label(false). [para(13(a,1),117(a,1,2,2)),rewrite(2(5))]. given #84 (T,wt=11): 710 f(x,f(c_0,f(y,f(x,x)))) = c_0. [para(504(a,1),7(a,1,2,1)),rewrite(2(3),30(4),504(7))]. given #85 (A,wt=23): 41 f(x,f(f(x,y),f(z,f(x,f(u,f(f(x,y),f(y,v))))))) = f(x,y). [para(13(a,1),7(a,1,2,1)),rewrite(2(5),13(13))]. given #86 (F,wt=17): 161 f(x,f(f(x,y),f(f(x,y),f(z,y)))) = f(x,x) # label(false). [para(17(a,1),117(a,1,2,2)),rewrite(2(2),2(3),2(4),2(5))]. given #87 (F,wt=17): 178 f(f(x,f(x,y)),f(f(x,z),f(y,y))) = f(y,y) # label(false). [para(169(a,1),6(a,1,1)),rewrite(2(5))]. given #88 (F,wt=17): 184 f(x,f(y,f(f(x,y),f(y,z)))) = f(x,f(x,y)) # label(false). [para(13(a,1),169(a,2,2)),rewrite(125(7))]. given #89 (F,wt=15): 2507 f(x,f(y,f(z,f(x,y)))) = f(x,f(x,y)) # label(false). [para(36(a,1),184(a,1,2)),rewrite(2(2))]. given #90 (T,wt=11): 830 f(c_0,f(c_0,f(x,y))) = f(x,y). [para(3(a,1),546(a,1,2,2,2,2)),rewrite(606(6),541(4,R),2(4))]. given #91 (A,wt=23): 42 f(x,f(f(x,y),f(z,f(f(x,y),f(u,f(x,f(y,v))))))) = f(x,y). [para(7(a,1),13(a,1,2,1)),rewrite(2(7),7(15))]. given #92 (F,wt=15): 2572 f(x,f(y,f(z,f(y,x)))) = f(x,f(y,y)) # label(false). [para(2507(a,1),2(a,2)),rewrite(2(1),2(4),2(5),176(6,R))]. given #93 (F,wt=17): 222 f(f(x,y),f(f(x,z),f(f(x,z),f(y,y)))) = y # label(false). [para(179(a,2),6(a,1,2))]. given #94 (F,wt=17): 269 f(f(x,f(y,y)),f(f(y,x),f(x,z))) = f(y,x) # label(false). [para(38(a,1),24(a,1,2,2,2)),rewrite(2(2),176(2,R),2(4))]. given #95 (F,wt=17): 410 f(f(x,x),f(y,f(x,z))) = f(f(x,x),f(y,y)) # label(false). [para(197(a,1),36(a,1,2)),flip(a)]. given #96 (T,wt=11): 835 f(x,f(c_0,f(y,f(y,x)))) = c_0. [para(546(a,1),18(a,1,2)),rewrite(176(3),2(2),2(5))]. given #97 (A,wt=19): 44 f(x,f(f(x,y),f(z,f(f(x,y),f(y,u))))) = f(x,y). [para(13(a,1),13(a,1,2,1)),rewrite(2(5),13(11))]. given #98 (F,wt=17): 506 f(f(x,y),f(c_0,f(x,f(y,z)))) = f(x,f(x,y)) # label(false). [back_rewrite(493),rewrite(504(7),2(7),22(10))]. given #99 (F,wt=17): 586 f(f(x,y),f(y,f(y,f(x,z)))) = f(c_0,f(x,y)) # label(false). [back_rewrite(152),rewrite(541(8,R),2(8))]. given #100 (F,wt=17): 591 f(f(x,y),f(x,f(x,f(y,z)))) = f(c_0,f(x,y)) # label(false). [back_rewrite(119),rewrite(541(8,R),2(8))]. given #101 (F,wt=17): 666 f(x,f(f(y,x),f(z,f(z,f(y,y))))) = f(y,x) # label(false). [para(221(a,1),9(a,1,2)),rewrite(2(6))]. given #102 (T,wt=11): 1624 f(f(x,x),f(c_0,f(y,x))) = c_0. [para(1054(a,1),572(a,1,2)),rewrite(760(5),775(6),2(6)),flip(a)]. given #103 (A,wt=19): 45 f(x,f(f(y,f(x,z)),f(x,f(z,u)))) = f(x,f(z,u)). [para(2(a,1),11(a,1,2))]. given #104 (F,wt=15): 3586 f(x,f(y,f(c_0,f(z,f(x,y))))) = f(x,x) # label(false). [para(45(a,1),403(a,1)),rewrite(541(5,R),2(4))]. given #105 (F,wt=15): 3596 f(x,f(y,f(y,f(z,f(x,y))))) = f(x,x) # label(false). [para(45(a,1),811(a,1))]. given #106 (F,wt=15): 3636 f(x,f(y,f(c_0,f(z,f(y,x))))) = f(x,x) # label(false). [para(3586(a,1),2(a,2)),rewrite(2(2),2(6))]. given #107 (F,wt=15): 3717 f(x,f(y,f(y,f(z,f(y,x))))) = f(x,x) # label(false). [para(3596(a,1),2(a,2)),rewrite(2(1),2(5))]. given #108 (T,wt=13): 904 f(f(x,x),f(y,f(c_0,f(x,z)))) = x. [para(7(a,1),572(a,1,2)),rewrite(2(2),541(2),176(2),2(1),8(3),2(3),541(3),33(3),2(2),541(2)),flip(a)]. given #109 (A,wt=23): 46 f(f(x,f(y,z)),f(x,f(u,f(f(x,f(y,z)),f(v,f(x,y)))))) = x. [para(11(a,1),3(a,1,1)),rewrite(2(8))]. given #110 (F,wt=17): 895 f(f(x,y),f(c_0,f(z,f(z,x)))) = f(z,f(z,x)) # label(false). [para(572(a,1),3(a,1,2)),rewrite(2(4),2(6))]. given #111 (F,wt=15): 4063 f(x,f(x,f(y,f(z,f(z,x))))) = f(y,x) # label(false). [para(1324(a,1),895(a,1,2,2)),rewrite(176(2),2(1),2(4),2(6),4049(8),176(3),2(2)),flip(a)]. given #112 (F,wt=15): 4074 f(x,f(y,f(c_0,f(z,f(z,x))))) = f(x,x) # label(false). [para(710(a,1),895(a,1,2,2,2)),rewrite(176(3),2(2),2(5),541(8),535(8),2(6),176(9),2(8),835(11),541(8))]. given #113 (F,wt=17): 1144 f(f(x,y),f(c_0,f(y,f(x,z)))) = f(y,f(x,x)) # label(false). [para(6(a,1),758(a,2,2)),rewrite(2(8),176(8,R))]. given #114 (T,wt=13): 1173 f(x,f(c_0,f(f(x,x),f(y,z)))) = c_0. [para(105(a,1),758(a,2,2)),rewrite(504(8))]. given #115 (A,wt=33): 47 f(f(x,f(y,z)),f(f(x,u),f(f(x,f(y,z)),f(v,f(x,y))))) = f(f(x,f(y,z)),f(v,f(x,y))). [para(11(a,1),6(a,1,1)),rewrite(2(9))]. given #116 (F,wt=17): 1153 f(x,f(c_0,f(f(x,y),f(y,z)))) = f(x,f(x,y)) # label(false). [para(13(a,1),758(a,2,2))]. given #117 (F,wt=17): 1165 f(x,f(c_0,f(f(x,y),f(z,y)))) = f(x,f(x,y)) # label(false). [para(17(a,1),758(a,2,2)),rewrite(2(3),2(4),2(7))]. given #118 (F,wt=17): 2115 f(f(x,x),f(f(y,x),f(z,f(z,f(x,x))))) = c_0 # label(false). [para(33(a,1),1885(a,1,2,2)),rewrite(2(7),541(7),2(7))]. given #119 (F,wt=17): 2402 f(f(x,f(x,y)),f(f(z,x),f(y,y))) = f(y,y) # label(false). [para(6(a,1),178(a,1,2,1)),rewrite(2(3),176(4,R),176(5),2(4),2(6))]. given #120 (T,wt=13): 1223 f(f(x,x),f(y,f(c_0,f(z,x)))) = x. [para(758(a,2),899(a,1,1)),rewrite(2(6))]. given #121 (A,wt=31): 48 f(f(x,y),f(f(y,z),f(f(x,y),f(u,f(y,f(x,v)))))) = f(f(x,y),f(u,f(y,f(x,v)))). [para(6(a,1),11(a,1,2,2,2)),rewrite(2(5),2(7),2(8),2(13))]. given #122 (F,wt=17): 2486 f(x,f(y,f(f(y,x),f(y,z)))) = f(x,f(y,y)) # label(false). [para(184(a,1),2(a,2)),rewrite(2(1),2(5),2(6),176(7,R))]. given #123 (F,wt=17): 2596 f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,y) # label(false). [para(176(a,1),2507(a,1,2,2,2)),rewrite(2(2),176(8),2(7),8(9))]. given #124 (F,wt=17): 2918 f(f(x,x),f(y,f(x,z))) = f(f(y,y),f(x,x)) # label(false). [para(410(a,1),2(a,2)),rewrite(2(4),2(7))]. given #125 (F,wt=17): 3000 f(x,f(y,f(y,f(f(x,x),f(z,z))))) = f(x,x) # label(false). [para(410(a,1),897(a,1,2,2,2)),rewrite(541(3,R),2(3),535(3))]. given #126 (T,wt=13): 1253 f(f(c_0,c_0),f(x,f(c_0,f(y,z)))) = c_0. [para(758(a,2),775(a,1,1)),rewrite(2(8))]. given #127 (A,wt=17): 49 f(x,f(f(x,y),f(z,f(x,f(u,y))))) = f(x,y). [para(6(a,1),11(a,2,2)),rewrite(6(4))]. given #128 (F,wt=17): 3019 f(x,f(f(y,y),f(f(x,x),f(y,z)))) = f(x,y) # label(false). [para(410(a,2),821(a,1,2)),rewrite(176(8),2(7),8(9))]. given #129 (F,wt=17): 3106 f(x,f(y,f(f(x,x),f(z,z)))) = f(x,f(x,y)) # label(false). [para(410(a,1),410(a,1,2,2)),rewrite(541(3,R),2(3),535(3),541(8,R),2(8),535(8),176(7),2(6))]. given #130 (F,wt=17): 3132 f(f(x,f(y,z)),f(z,z)) = f(f(x,x),f(z,z)) # label(false). [back_rewrite(1593),rewrite(2991(8),3110(8)),flip(a)]. given #131 (F,wt=17): 3331 f(f(x,f(y,y)),f(c_0,f(f(y,x),f(x,z)))) = x # label(false). [para(222(a,1),506(a,2)),rewrite(33(4),2(2),176(2,R),33(7))]. given #132 (T,wt=13): 1457 f(f(c_0,c_0),f(f(x,x),f(y,z))) = c_0. [para(105(a,1),832(a,1,2,2,2,2,2)),rewrite(504(6),541(6),504(6),2(7))]. given #133 (A,wt=15): 50 f(f(x,f(y,f(x,z))),f(x,f(z,u))) = x. [para(11(a,1),9(a,1,2))]. given #134 (F,wt=17): 4091 f(f(x,x),f(c_0,f(y,f(x,z)))) = f(y,f(y,x)) # label(false). [para(410(a,1),895(a,1,2,2,2)),rewrite(2(3),2(8),176(9,R),541(8,R),2(8),535(8),2(6),176(6),2(5),1900(8),2991(8)),flip(a)]. given #135 (F,wt=15): 6340 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [para(6(a,1),4091(a,1,2,2,2)),rewrite(541(3,R),2(3),2(5),5826(7))]. given #136 (F,wt=15): 6698 f(x,f(c_0,f(y,z))) = f(y,f(y,f(x,z))) # label(false). [para(6340(a,1),2(a,1)),rewrite(2(5),2(7)),flip(a)]. given #137 (F,wt=15): 6699 f(x,f(c_0,f(y,z))) = f(z,f(z,f(y,x))) # label(false). [para(6340(a,1),2(a,2)),rewrite(2(4),2(5))]. given #138 (T,wt=13): 2839 f(f(x,x),f(f(y,x),f(x,z))) = c_0. [para(222(a,1),1443(a,1,2,2)),rewrite(33(4),2(5),541(5),2(5))]. given #139 (A,wt=31): 52 f(x,f(f(x,f(y,z)),f(u,f(x,f(v,f(f(x,f(y,z)),f(w,f(x,y)))))))) = f(x,f(y,z)). [para(11(a,1),7(a,1,2,1)),rewrite(2(8),11(18))]. given #140 (F,wt=15): 6708 f(f(x,f(y,z)),f(z,f(z,f(x,y)))) = x # label(false). [para(6340(a,1),9(a,1,2))]. given #141 (F,wt=15): 6710 f(f(x,f(y,z)),f(y,f(c_0,f(x,z)))) = x # label(false). [para(6340(a,2),9(a,1,2)),rewrite(2(4))]. given #142 (F,wt=15): 6712 f(f(x,f(x,f(y,z))),f(z,f(y,x))) = z # label(false). [para(6340(a,1),12(a,1,2)),rewrite(2(2),2(3),2(6))]. given #143 (F,wt=15): 6713 f(f(x,f(y,z)),f(y,f(c_0,f(z,x)))) = x # label(false). [para(6340(a,2),12(a,1,2)),rewrite(2(2))]. given #144 (T,wt=13): 6208 f(f(c_0,c_0),f(f(x,y),f(z,u))) = c_0. [para(758(a,1),1457(a,1,2,1)),rewrite(2(11),176(11,R),775(11),2(8),830(8))]. given #145 (A,wt=39): 53 f(x,f(f(y,f(x,z)),f(x,f(u,f(f(x,z),f(v,f(x,f(z,w)))))))) = f(x,f(u,f(f(x,z),f(v,f(x,f(z,w)))))). [para(7(a,1),11(a,1,2,2,2)),rewrite(2(6),2(10),2(17))]. given #146 (F,wt=15): 6714 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)) # label(false). [para(6340(a,2),8(a,1,2)),rewrite(2(2))]. given #147 (F,wt=15): 6715 f(x,f(x,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [para(6340(a,1),8(a,2)),rewrite(760(5))]. given #148 (F,wt=15): 6850 f(x,f(x,f(y,z))) = f(y,f(y,f(x,z))) # label(false). [para(6340(a,1),758(a,1)),rewrite(2(4))]. given #149 (F,wt=15): 6858 f(x,f(y,f(y,f(x,z)))) = f(x,f(y,z)) # label(false). [para(6340(a,1),760(a,1,2)),rewrite(2(5))]. given #150 (T,wt=15): 60 f(f(x,f(y,z)),f(x,f(u,f(x,y)))) = x. [para(3(a,1),15(a,1,2,1)),rewrite(2(4),3(10))]. given #151 (A,wt=27): 56 f(x,f(f(x,f(y,z)),f(u,f(f(x,f(y,z)),f(v,f(x,y)))))) = f(x,f(y,z)). [para(11(a,1),13(a,1,2,1)),rewrite(2(8),11(16))]. given #152 (F,wt=15): 6880 f(x,f(c_0,f(y,f(x,f(z,f(z,y)))))) = c_0 # label(false). [para(834(a,1),6340(a,2,2)),rewrite(176(3),2(2),2(5),504(9))]. given #153 (F,wt=15): 6985 f(x,f(x,f(y,z))) = f(z,f(z,f(y,x))) # label(false). [para(6340(a,1),269(a,2)),rewrite(2(5),2(13),2888(15),2(4))]. given #154 (F,wt=15): 7184 f(x,f(c_0,f(y,z))) = f(y,f(y,f(z,x))) # label(false). [back_rewrite(1092),rewrite(6714(8),2(4),2(6),582(6)),flip(a)]. given #155 (F,wt=15): 7271 f(f(x,f(y,z)),f(y,f(y,f(x,z)))) = x # label(false). [para(6698(a,1),9(a,1,2))]. given #156 (T,wt=15): 62 f(f(x,f(y,z)),f(x,f(u,f(x,z)))) = x. [para(9(a,1),15(a,1,2,1)),rewrite(2(4),9(10))]. given #157 (A,wt=17): 59 f(f(x,y),f(y,f(z,f(f(x,y),f(x,u))))) = y. [para(15(a,1),3(a,1,1)),rewrite(2(5))]. given #158 (F,wt=15): 7272 f(f(x,f(x,f(y,z))),f(z,f(x,y))) = z # label(false). [para(6698(a,1),12(a,1,2)),rewrite(2(2),2(3),2(6))]. given #159 (F,wt=15): 7388 f(x,f(y,f(y,f(z,x)))) = f(x,f(y,z)) # label(false). [para(6698(a,1),895(a,2,2)),rewrite(2(4),760(10),1220(9),2(3)),flip(a)]. given #160 (F,wt=15): 7452 f(f(x,f(y,z)),f(z,f(c_0,f(x,y)))) = x # label(false). [para(6699(a,2),9(a,1,2)),rewrite(2(4))]. given #161 (F,wt=15): 7454 f(f(x,f(y,z)),f(z,f(c_0,f(y,x)))) = x # label(false). [para(6699(a,2),12(a,1,2)),rewrite(2(2))]. given #162 (T,wt=15): 254 f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x. [para(3(a,1),38(a,1,2,2,2,2)),rewrite(2(2),2(3))]. given #163 (A,wt=23): 61 f(f(x,y),f(f(y,z),f(f(x,y),f(x,u)))) = f(f(x,y),f(x,u)). [para(15(a,1),6(a,1,1)),rewrite(2(6))]. given #164 (F,wt=15): 7604 f(x,f(y,f(c_0,f(z,x)))) = f(x,f(y,z)) # label(false). [para(6340(a,2),6699(a,2,2)),rewrite(535(4),2(2)),flip(a)]. given #165 (F,wt=15): 7869 f(f(x,f(x,f(y,z))),f(y,f(x,z))) = y # label(false). [para(6708(a,1),2(a,2)),rewrite(2(4))]. given #166 (F,wt=15): 8820 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)) # label(false). [para(8(a,1),6714(a,1,2,2,2)),rewrite(6714(5)),flip(a)]. given #167 (F,wt=15): 8827 f(x,f(y,f(y,z))) = f(x,f(y,f(x,z))) # label(false). [para(176(a,1),6714(a,1,2,2,2)),rewrite(2(2),6714(6),176(5),2(4)),flip(a)]. given #168 (T,wt=15): 255 f(f(x,f(y,z)),f(x,f(u,f(z,x)))) = x. [para(6(a,1),38(a,1,2,2,2,2)),rewrite(2(2),2(3))]. given #169 (A,wt=23): 63 f(f(f(x,y),f(x,z)),f(f(x,y),f(u,f(x,f(y,v))))) = f(x,y). [para(7(a,1),15(a,1,2,1)),rewrite(2(9),7(15))]. given #170 (F,wt=15): 9443 f(f(x,f(y,z)),f(y,f(y,f(x,x)))) = x # label(false). [para(6340(a,1),60(a,1,2))]. given #171 (F,wt=15): 9820 f(f(x,f(y,z)),f(z,f(z,f(x,x)))) = x # label(false). [para(6340(a,1),62(a,1,2))]. given #172 (F,wt=15): 9979 f(x,f(c_0,f(y,f(z,f(z,x))))) = f(x,y) # label(false). [back_rewrite(954),rewrite(9967(14),2(4))]. given #173 (F,wt=13): 11350 f(f(x,x),f(y,f(y,f(z,x)))) = x # label(false). [para(23(a,1),9979(a,2)),rewrite(2(13),6801(15),2(5))]. given #174 (T,wt=15): 437 f(f(x,f(y,z)),f(x,f(u,f(y,y)))) = x. [para(29(a,1),201(a,1,1,2)),rewrite(2(8),32(8))]. given #175 (A,wt=19): 64 f(f(f(x,y),f(x,z)),f(f(x,y),f(y,u))) = f(x,y). [para(13(a,1),15(a,1,2,1)),rewrite(2(7),13(11))]. given #176 (F,wt=15): 10686 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))) # label(false). [para(8827(a,1),2(a,2)),rewrite(2(3),2(4)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 18.35 (+ 0.04) seconds: "Sheffer". % Length of proof is 75. % Level of proof is 24. % Maximum clause weight is 43. % Given clauses 176. 1 f(f(x,x),f(x,x)) = x & f(x,f(y,f(y,y))) = f(x,x) & f(f(f(y,y),x),f(f(z,z),x)) = f(f(x,f(y,z)),f(x,f(y,z))) # answer("Sheffer") # label(goal). [goal]. 2 f(x,y) = f(y,x) # label(commutativity). [assumption]. 3 f(f(x,y),f(x,f(y,z))) = x # label(Veroff_2) # label(false). [assumption]. 4 f(f(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(f(c5,c5),c4),f(f(c6,c6),c4)) != f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) # answer("Sheffer"). [deny(1)]. 5 f(f(c4,c4),f(c4,c4)) != c4 | f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # answer("Sheffer"). [copy(4),rewrite(2(25),2(30)),flip(c)]. 6 f(f(x,y),f(y,f(x,z))) = y # label(false). [para(2(a,1),3(a,1,1))]. 7 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [para(3(a,1),3(a,1,1)),rewrite(2(4))]. 8 f(x,f(x,f(x,y))) = f(x,y). [para(3(a,1),3(a,1,2)),rewrite(2(2),2(3))]. 9 f(f(x,y),f(x,f(z,y))) = x # label(false). [para(6(a,1),3(a,1,2,2)),rewrite(2(4))]. 11 f(x,f(f(x,f(y,z)),f(u,f(x,y)))) = f(x,f(y,z)). [para(3(a,1),6(a,1,1)),rewrite(2(4))]. 12 f(f(x,y),f(y,f(z,x))) = y # label(false). [para(6(a,1),6(a,1,2,2)),rewrite(2(2),2(3),2(4))]. 13 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(3(a,1),9(a,1,2)),rewrite(2(4))]. 14 f(x,f(f(x,f(y,z)),f(u,f(x,z)))) = f(x,f(y,z)). [para(9(a,1),6(a,1,1)),rewrite(2(4))]. 16 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(3(a,1),12(a,1,2)),rewrite(2(2),2(4),2(5))]. 19 f(f(x,x),f(x,y)) = x. [para(8(a,1),3(a,1,2))]. 20 f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c5,c5)),f(c4,f(c6,c6))) # answer("Sheffer"). [back_rewrite(5),rewrite(19(7)),xx(a)]. 23 f(f(x,y),f(y,f(z,f(f(x,y),f(u,f(y,f(x,v))))))) = y. [para(6(a,1),7(a,1,2,1)),rewrite(2(5),6(13))]. 29 f(x,f(f(x,y),f(z,f(x,x)))) = f(x,y). [para(19(a,1),6(a,1,1)),rewrite(2(3))]. 30 f(x,f(y,f(x,x))) = f(x,x). [para(19(a,1),9(a,1,2)),rewrite(2(2),2(3))]. 32 f(f(x,x),f(f(x,y),f(z,f(x,x)))) = f(z,f(x,x)). [para(30(a,1),6(a,1,1)),rewrite(2(5))]. 33 f(f(x,y),f(y,y)) = y. [para(30(a,1),6(a,1,2))]. 36 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(3(a,1),13(a,1,2,2)),rewrite(2(3))]. 66 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(2(a,1),16(a,1,2,1)),rewrite(2(2),2(3),2(5))]. 117 f(x,f(y,f(x,y))) = f(x,x) # label(false). [para(9(a,1),36(a,1,2)),rewrite(2(3)),flip(a)]. 122 f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(x,y)),f(x,f(y,z))) # label(false). [para(11(a,1),36(a,1,2)),rewrite(2(10))]. 153 f(f(x,f(y,f(y,z))),f(x,f(z,z))) = x # label(false). [para(117(a,1),9(a,1,2,2)),rewrite(2(1))]. 169 f(x,f(y,y)) = f(x,f(x,y)) # label(false). [para(117(a,1),36(a,1,2)),rewrite(2(3))]. 170 f(x,f(f(x,f(y,z)),f(y,f(x,f(y,z))))) = f(x,x) # label(false). [para(36(a,1),117(a,1,2,2)),rewrite(2(6))]. 173 f(f(x,f(x,y)),f(x,f(z,f(z,y)))) = x # label(false). [back_rewrite(153),rewrite(169(5),2(6))]. 175 f(c4,f(c5,f(c5,c5))) != f(c4,c4) | f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) # answer("Sheffer"). [back_rewrite(20),rewrite(169(27),169(32))]. 176 f(x,f(y,y)) = f(x,f(y,x)) # label(false). [para(169(a,1),2(a,2)),rewrite(2(2),2(3))]. 177 f(f(x,f(x,y)),f(x,f(z,f(y,y)))) = x. [para(169(a,1),3(a,1,1)),rewrite(2(4))]. 179 f(x,f(x,f(y,y))) = f(y,x) # label(false). [para(169(a,1),9(a,1)),rewrite(2(2),176(2,R),2(4),176(4,R),2(6),6(6),2(3))]. 197 f(x,f(f(y,y),f(x,f(y,z)))) = f(x,x) # label(false). [back_rewrite(170),rewrite(176(6,R),2(4))]. 201 f(f(x,f(y,z)),f(x,f(z,f(y,y)))) = x # label(false). [para(176(a,2),9(a,1,2,2))]. 231 f(x,f(y,f(y,f(z,z)))) = f(x,f(z,y)) # label(false). [para(179(a,1),11(a,1,2,1,2)),rewrite(14(6)),flip(a)]. 247 f(f(x,f(y,y)),f(f(y,z),f(y,z))) = f(y,z). [para(179(a,2),29(a,1)),rewrite(2(10),32(10),2(7),176(7,R))]. 359 f(f(x,f(x,x)),f(x,f(y,f(y,f(z,f(x,x)))))) = x # label(false). [para(30(a,1),173(a,1,1,2))]. 410 f(f(x,x),f(y,f(x,z))) = f(f(x,x),f(y,y)) # label(false). [para(197(a,1),36(a,1,2)),flip(a)]. 452 f(x,f(y,f(y,y))) = f(x,x). [para(201(a,1),201(a,1,2)),rewrite(2(5),176(5),2(4),2(6),177(6)),flip(a)]. 453 f(f(c4,f(c5,c6)),f(c4,f(c5,c6))) != f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) # answer("Sheffer"). [back_unit_del(175),unit_del(a,452)]. 463 f(f(x,x),f(y,f(y,y))) = x. [para(452(a,2),19(a,1))]. 466 f(x,f(x,x)) = f(y,f(y,y)). [para(452(a,1),33(a,1,1)),rewrite(176(7),2(5),463(5),2(2))]. 504 f(x,f(x,x)) = c_0. [new_symbol(466)]. 535 f(c_0,f(x,x)) = x. [back_rewrite(463),rewrite(504(3),2(3))]. 541 f(x,c_0) = f(x,x). [back_rewrite(452),rewrite(504(2))]. 546 f(c_0,f(x,f(y,f(y,f(z,f(x,x)))))) = x # label(false). [back_rewrite(359),rewrite(504(2))]. 551 f(f(c4,f(c4,c5)),f(c4,f(c4,c6))) != f(c_0,f(c4,f(c5,c6))) # answer("Sheffer"). [back_rewrite(453),rewrite(541(11,R),2(7)),flip(a)]. 572 f(f(x,f(x,y)),f(c_0,f(y,z))) = f(y,z) # label(false). [back_rewrite(247),rewrite(176(2),2(1),541(5,R),2(5))]. 590 f(f(x,f(x,y)),f(x,f(y,z))) = f(c_0,f(x,f(y,z))) # label(false). [back_rewrite(122),rewrite(541(5,R),2(4)),flip(a)]. 606 f(x,f(y,f(y,x))) = f(x,x) # label(false). [para(19(a,1),23(a,1,2)),rewrite(176(2),2(1),2(3))]. 636 f(x,f(f(x,y),f(c_0,f(z,y)))) = f(x,x) # label(false). [para(23(a,1),197(a,1,2,2,2)),rewrite(541(3,R),2(3),2(5))]. 760 f(x,f(x,f(c_0,f(y,z)))) = f(x,f(y,z)) # label(false). [para(231(a,1),179(a,1,2,2)),rewrite(176(2),2(1),8(3),2(2),541(3,R),2(3),176(7),2(6),8(8),2(7))]. 830 f(c_0,f(c_0,f(x,y))) = f(x,y). [para(3(a,1),546(a,1,2,2,2,2)),rewrite(606(6),541(4,R),2(4))]. 832 f(x,f(c_0,f(y,f(y,f(z,f(z,x)))))) = c_0 # label(false). [para(546(a,1),9(a,1,2)),rewrite(176(3),2(2),2(7))]. 895 f(f(x,y),f(c_0,f(z,f(z,x)))) = f(z,f(z,x)) # label(false). [para(572(a,1),3(a,1,2)),rewrite(2(4),2(6))]. 899 f(f(x,f(x,f(y,z))),f(z,z)) = z # label(false). [para(6(a,1),572(a,1,2,2)),rewrite(2(5),541(5),6(9))]. 992 f(x,f(y,f(y,f(z,f(z,x))))) = f(x,x) # label(false). [para(19(a,1),899(a,1,2)),rewrite(176(2),2(1),2(5))]. 1054 f(x,f(f(x,f(y,z)),f(z,z))) = f(x,x) # label(false). [para(66(a,1),636(a,1,2,2)),rewrite(2(4),541(4))]. 1443 f(f(x,f(y,z)),f(c_0,f(x,f(x,y)))) = c_0 # label(false). [para(7(a,1),832(a,1,2,2,2))]. 1593 f(f(x,x),f(f(x,y),f(f(x,f(z,u)),f(u,u)))) = f(f(x,f(z,u)),f(u,u)). [para(1054(a,1),6(a,1,1)),rewrite(2(7))]. 1900 f(f(x,f(y,f(z,u))),f(c_0,f(y,f(y,z)))) = f(y,f(y,z)). [para(1443(a,1),992(a,1,2,2,2,2)),rewrite(2(8),760(10),2(8),541(17,R),2(14),830(14))]. 2962 f(f(x,x),f(f(x,y),f(f(x,y),f(z,z)))) = f(f(x,x),f(z,z)). [para(179(a,2),410(a,1,2))]. 2991 f(f(x,x),f(f(x,y),f(z,u))) = f(f(x,x),f(c_0,f(z,u))). [para(231(a,1),410(a,2,2)),rewrite(176(3),2(2),8(4),2(4),176(8),2(7),8(9),2(8),541(9,R),2(9))]. 3110 f(f(x,x),f(c_0,f(f(x,y),f(z,z)))) = f(f(x,x),f(z,z)). [back_rewrite(2962),rewrite(2991(7))]. 3132 f(f(x,f(y,z)),f(z,z)) = f(f(x,x),f(z,z)) # label(false). [back_rewrite(1593),rewrite(2991(8),3110(8)),flip(a)]. 4091 f(f(x,x),f(c_0,f(y,f(x,z)))) = f(y,f(y,x)) # label(false). [para(410(a,1),895(a,1,2,2,2)),rewrite(2(3),2(8),176(9,R),541(8,R),2(8),535(8),2(6),176(6),2(5),1900(8),2991(8)),flip(a)]. 5826 f(f(c_0,f(x,y)),f(c_0,f(y,z))) = f(x,f(c_0,f(y,z))). [para(3(a,1),3132(a,1,1)),rewrite(541(3,R),2(3),541(7,R),2(7),541(10,R),2(10)),flip(a)]. 6340 f(x,f(c_0,f(y,z))) = f(z,f(z,f(x,y))) # label(false). [para(6(a,1),4091(a,1,2,2,2)),rewrite(541(3,R),2(3),2(5),5826(7))]. 6714 f(x,f(y,f(c_0,f(x,z)))) = f(x,f(y,z)) # label(false). [para(6340(a,2),8(a,1,2)),rewrite(2(2))]. 8820 f(x,f(y,f(x,f(x,z)))) = f(x,f(y,z)) # label(false). [para(8(a,1),6714(a,1,2,2,2)),rewrite(6714(5)),flip(a)]. 8827 f(x,f(y,f(y,z))) = f(x,f(y,f(x,z))) # label(false). [para(176(a,1),6714(a,1,2,2,2)),rewrite(2(2),6714(6),176(5),2(4)),flip(a)]. 10686 f(x,f(y,f(z,x))) = f(x,f(y,f(y,z))) # label(false). [para(8827(a,1),2(a,2)),rewrite(2(3),2(4)),flip(a)]. 11795 f(f(x,f(x,y)),f(x,f(x,z))) = f(c_0,f(x,f(y,z))) # label(false). [para(8820(a,1),10686(a,1,2)),rewrite(2(3),590(5)),flip(a)]. 11796 $F # answer("Sheffer"). [resolve(11795,a,551,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=176. Generated=125850. Kept=11793. proofs=1. Usable=142. Sos=7428. Demods=6495. Limbo=104, Disabled=4121. Hints=0. Weight_deleted=31. Literals_deleted=0. Forward_subsumed=114026. Back_subsumed=650. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=10263 (5 lex), Back_demodulated=3467. Back_unit_deleted=1. Demod_attempts=2519013. Demod_rewrites=597567. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=3. Megabytes=13.52. User_CPU=18.35, System_CPU=0.04, Wall_clock=18. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4412 exit (max_proofs) Wed Nov 22 12:04:19 2006