============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5419 was started by mccune on cleo, Tue Nov 3 09:57:56 2009 The command was "/home/mccune/LADR/bin/prover9 -f pair-def.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file pair-def.in assign(max_seconds,30). assign(new_constants,1). assign(eq_defs,fold). formulas(sos). f(x,y) = f(y,x). f(f(x,y),f(x,f(y,z))) = x. x' = f(x,x). 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. ============================== 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(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(x,y) = f(y,x). [assumption]. f(f(x,y),f(x,f(y,z))) = x. [assumption]. x' = f(x,x). [assumption]. f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(f(c2,c2),c1),f(f(c3,c3),c1)) != f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) # 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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, f, ' ]). After inverse_order: (no changes). Folding symbols: '/1. After fold_eq: Function symbol precedence: function_order([ c1, c2, c3, ', f ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) % Operation f is commutative; C redundancy checks enabled. kept: 2 f(x,y) = f(y,x). [assumption]. kept: 3 f(f(x,y),f(x,f(y,z))) = x. [assumption]. 4 x' = f(x,x). [assumption]. kept: 5 f(x,x) = x'. [copy(4),flip(a)]. 6 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(f(c2,c2),c1),f(f(c3,c3),c1)) != f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) # answer("Sheffer"). [deny(1)]. kept: 7 c1'' != c1 | f(c1,f(c2,c2')) != c1' | f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [copy(6),rewrite([5(3),5(5),5(5),5(10),5(14),5(17),2(18),5(21),2(22),5(34)])]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 f(x,y) = f(y,x). [assumption]. 3 f(f(x,y),f(x,f(y,z))) = x. [assumption]. 5 f(x,x) = x'. [copy(4),flip(a)]. 7 c1'' != c1 | f(c1,f(c2,c2')) != c1' | f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [copy(6),rewrite([5(3),5(5),5(5),5(10),5(14),5(17),2(18),5(21),2(22),5(34)])]. end_of_list. formulas(demodulators). 2 f(x,y) = f(y,x). [assumption]. % (lex-dep) 3 f(f(x,y),f(x,f(y,z))) = x. [assumption]. 5 f(x,x) = x'. [copy(4),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=7): 2 f(x,y) = f(y,x). [assumption]. given #2 (I,wt=11): 3 f(f(x,y),f(x,f(y,z))) = x. [assumption]. given #3 (I,wt=6): 5 f(x,x) = x'. [copy(4),flip(a)]. given #4 (I,wt=30): 7 c1'' != c1 | f(c1,f(c2,c2')) != c1' | f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [copy(6),rewrite([5(3),5(5),5(5),5(10),5(14),5(17),2(18),5(21),2(22),5(34)])]. given #5 (A,wt=11): 8 f(f(x,y),f(y,f(x,z))) = y. [para(2(a,1),3(a,1,1))]. given #6 (T,wt=10): 13 f(x',f(x,f(x,y))) = x. [para(5(a,1),3(a,1,1))]. given #7 (T,wt=9): 28 f(x,f(x,x')) = x'. [para(13(a,1),3(a,1,2)),rewrite([2(2),2(3)])]. given #8 (T,wt=5): 35 x'' = x. [para(28(a,1),3(a,1,2)),rewrite([5(1),5(3)])]. given #9 (T,wt=9): 29 f(x',f(x,x')) = x. [para(5(a,1),13(a,1,2,2))]. given #10 (A,wt=11): 9 f(f(x,y),f(x,f(z,y))) = x. [para(2(a,1),3(a,1,2,2))]. given #11 (F,wt=25): 37 f(c1,f(c2,c2')) != c1' | f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(7),rewrite([35(3)]),xx(a)]. given #12 (T,wt=10): 14 f(f(x,y),f(x,y')) = x. [para(5(a,1),3(a,1,2,2))]. given #13 (T,wt=10): 23 f(f(x,y),f(y,x')) = y. [para(5(a,1),8(a,1,2,2))]. given #14 (T,wt=10): 26 f(x',f(x,f(y,x))) = x. [para(2(a,1),13(a,1,2,2))]. given #15 (T,wt=10): 31 f(f(x',y),f(y,x)) = y. [para(13(a,1),8(a,1,2,2))]. given #16 (A,wt=11): 10 f(f(x,y),f(f(y,z),x)) = x. [para(2(a,1),3(a,1,2))]. given #17 (T,wt=10): 54 f(f(x,y),f(y',x)) = x. [para(2(a,1),14(a,1,2))]. given #18 (T,wt=10): 66 f(f(x,y'),f(y,x)) = x. [para(23(a,1),2(a,1)),flip(a)]. given #19 (T,wt=10): 67 f(f(x,y),f(x',y)) = y. [para(2(a,1),23(a,1,2))]. given #20 (T,wt=10): 80 f(x,f(y,x)') = f(y,x). [para(8(a,1),26(a,1,2)),rewrite([2(3)])]. given #21 (A,wt=17): 11 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y). [para(3(a,1),3(a,1,1))]. given #22 (T,wt=8): 125 f(x',f(x,y)) = x. [para(31(a,1),80(a,1,2,1)),rewrite([2(3),31(7)])]. given #23 (T,wt=8): 129 f(x',f(y,x)) = x. [para(66(a,1),80(a,1,2,1)),rewrite([2(3),66(7)])]. given #24 (T,wt=9): 155 f(x,f(x',y)) = x'. [para(35(a,1),125(a,1,1))]. given #25 (T,wt=9): 157 f(x,f(y,x')) = x'. [para(129(a,1),8(a,1,2)),rewrite([2(3)])]. given #26 (A,wt=11): 12 f(x,f(x,f(x,y))) = f(x,y). [para(3(a,1),3(a,1,2)),rewrite([2(2),2(3)])]. given #27 (T,wt=10): 85 f(x,f(x,y)') = f(x,y). [para(9(a,1),26(a,1,2)),rewrite([2(3)])]. given #28 (T,wt=11): 16 f(f(x,f(y,z)),f(y,x)) = x. [para(8(a,1),2(a,1)),flip(a)]. given #29 (T,wt=11): 17 f(f(x,y),f(y,f(z,x))) = y. [para(2(a,1),8(a,1,2,2))]. given #30 (T,wt=11): 18 f(f(x,y),f(f(x,z),y)) = y. [para(2(a,1),8(a,1,2))]. given #31 (A,wt=17): 19 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x). [para(8(a,1),3(a,1,1))]. given #32 (T,wt=11): 20 f(x,f(x,f(y,x))) = f(y,x). [para(8(a,1),3(a,1,2)),rewrite([2(2),2(3)])]. given #33 (T,wt=11): 22 f(f(f(x,y),z),f(z,x)) = z. [para(3(a,1),8(a,1,2,2))]. given #34 (T,wt=11): 25 f(f(f(x,y),z),f(z,y)) = z. [para(8(a,1),8(a,1,2,2))]. given #35 (T,wt=11): 41 f(f(x,y),f(f(z,y),x)) = x. [para(2(a,1),9(a,1,2))]. given #36 (A,wt=19): 21 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [para(3(a,1),8(a,1,1))]. given #37 (T,wt=11): 99 f(f(x,f(y,z)),f(z,x)) = x. [para(8(a,1),10(a,1,2,1))]. given #38 (T,wt=10): 316 f(x,f(y,f(x,y))) = x'. [para(99(a,1),21(a,1,2)),rewrite([5(1)]),flip(a)]. given #39 (T,wt=10): 318 f(x,f(y,f(y,x))) = x'. [para(2(a,1),316(a,1,2,2))]. given #40 (T,wt=11): 173 f(f(x,y),f(f(z,x),y)) = y. [para(2(a,1),17(a,1,2))]. given #41 (A,wt=19): 24 f(x,f(f(x,f(y,z)),f(f(y,x),u))) = f(x,f(y,z)). [para(8(a,1),8(a,1,1))]. given #42 (T,wt=13): 44 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(3(a,1),9(a,1,2)),rewrite([2(4)])]. given #43 (T,wt=13): 47 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(8(a,1),9(a,1,2)),rewrite([2(4)])]. given #44 (T,wt=13): 53 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(9(a,1),9(a,1,2)),rewrite([2(4)])]. given #45 (T,wt=13): 98 f(x,f(f(y,z),f(x,y))) = f(x,y). [para(10(a,1),8(a,1,2)),rewrite([2(4)])]. given #46 (A,wt=17): 42 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y). [para(9(a,1),3(a,1,1))]. given #47 (T,wt=12): 597 f(x,f(x',y)') = f(x,x'). [para(157(a,1),42(a,1,2,2,1)),rewrite([369(5)])]. given #48 (T,wt=12): 637 f(x,f(y,x')') = f(x,x'). [para(2(a,1),597(a,1,2,1))]. given #49 (T,wt=12): 640 f(x',f(x,y)') = f(x,x'). [para(35(a,1),597(a,1,2,1,1)),rewrite([35(7),2(6)])]. NOTE: New constant: f(x,x') = c_0. [new_symbol(706)]. NOTE: New Function symbol precedence: function_order([ c1, c2, c3, c_0, ', f ]). given #50 (T,wt=6): 739 f(x,x') = c_0. [new_symbol(706)]. given #51 (A,wt=17): 43 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [para(3(a,1),9(a,1,1))]. given #52 (F,wt=16): 801 f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(749),rewrite([750(3)]),xx(a)]. given #53 (T,wt=6): 750 f(x,c_0) = x'. [back_rewrite(738),rewrite([739(2)])]. given #54 (T,wt=6): 822 f(c_0,x) = x'. [para(739(a,1),8(a,1,1)),rewrite([125(4)])]. given #55 (T,wt=6): 824 f(x,c_0') = c_0. [para(739(a,1),85(a,1,2,1)),rewrite([739(5)])]. given #56 (T,wt=6): 886 f(c_0',x) = c_0. [para(824(a,1),2(a,1)),flip(a)]. given #57 (A,wt=19): 45 f(x,f(f(x,f(y,z)),f(f(x,z),u))) = f(x,f(y,z)). [para(9(a,1),8(a,1,1))]. given #58 (T,wt=9): 783 f(x',f(y,x)') = c_0. [back_rewrite(671),rewrite([739(6)])]. given #59 (T,wt=9): 797 f(x',f(x,y)') = c_0. [back_rewrite(640),rewrite([739(6)])]. given #60 (T,wt=9): 799 f(x,f(y,x')') = c_0. [back_rewrite(637),rewrite([739(6)])]. given #61 (T,wt=9): 800 f(x,f(x',y)') = c_0. [back_rewrite(597),rewrite([739(6)])]. given #62 (A,wt=17): 46 f(x,f(f(y,x),f(z,f(x,f(y,u))))) = f(y,x). [para(8(a,1),9(a,1,1))]. given #63 (T,wt=10): 959 f(x,f(y,f(x,y))') = c_0. [para(316(a,1),783(a,1,2,1)),rewrite([35(5),2(4)])]. given #64 (T,wt=10): 960 f(x,f(y,f(y,x))') = c_0. [para(318(a,1),783(a,1,2,1)),rewrite([35(5),2(4)])]. given #65 (T,wt=12): 644 f(x,f(f(x',y)',z))' = x. [para(597(a,1),10(a,1,1)),rewrite([2(7),643(8)])]. given #66 (T,wt=12): 655 f(x,f(y,f(x',z)'))' = x. [para(597(a,1),25(a,1,2)),rewrite([2(5),2(8),643(8)])]. given #67 (A,wt=17): 52 f(x,f(f(x,y),f(z,f(x,f(u,y))))) = f(x,y). [para(9(a,1),9(a,1,1))]. given #68 (T,wt=12): 669 f(x,f(f(y,x')',z))' = x. [para(637(a,1),3(a,1,1)),rewrite([643(8)])]. given #69 (T,wt=12): 672 f(x,f(y,f(z,x')'))' = x. [para(637(a,1),9(a,1,1)),rewrite([643(8)])]. given #70 (T,wt=12): 757 f(f(x,y)',f(x',z)') = c_0. [back_rewrite(725),rewrite([739(8)])]. given #71 (T,wt=10): 1219 f(x',y) = f(y,f(x,y)). [back_rewrite(116),rewrite([1207(5)]),flip(a)]. given #72 (A,wt=16): 55 f(x,f(f(x,y),f(f(x,y'),z))) = f(x,y). [para(14(a,1),3(a,1,1))]. given #73 (T,wt=10): 1220 f(x,f(y,x)) = f(x,y'). [para(1219(a,1),2(a,1))]. given #74 (T,wt=10): 1241 f(x,f(x,y)) = f(x,y'). [para(1219(a,2),12(a,1,2,2)),rewrite([1220(3),35(2),1220(4)])]. given #75 (T,wt=12): 773 f(f(x,y')',f(y,z)') = c_0. [back_rewrite(696),rewrite([739(8)])]. given #76 (T,wt=12): 786 f(x,f(y,f(x',z)')') = c_0. [back_rewrite(665),rewrite([739(2),782(6),739(8)])]. given #77 (A,wt=17): 57 f(x,f(f(x,y'),f(f(x,y),z))) = f(x,y'). [para(14(a,1),8(a,1,1))]. given #78 (T,wt=12): 787 f(f(x',y)',f(x,z)') = c_0. [back_rewrite(664),rewrite([739(8)])]. given #79 (T,wt=12): 788 f(x,f(f(x',y)',z)') = c_0. [back_rewrite(663),rewrite([739(2),782(6),739(8)])]. given #80 (T,wt=12): 807 f(x,f(f(y,x')',z)') = c_0. [back_rewrite(774),rewrite([782(6)])]. given #81 (T,wt=12): 808 f(x,f(y,f(z,x')')') = c_0. [back_rewrite(772),rewrite([782(6)])]. given #82 (A,wt=16): 62 f(x,f(f(x,y),f(z,f(x,y')))) = f(x,y). [para(14(a,1),9(a,1,1))]. given #83 (T,wt=12): 816 f(x',f(f(x,y)',z)') = c_0. [back_rewrite(758),rewrite([782(6)])]. given #84 (T,wt=11): 1645 f(x',f(f(x,y)',z)) = x. [para(816(a,1),1241(a,1,2)),rewrite([2(3),822(3),35(2),35(6)]),flip(a)]. given #85 (T,wt=11): 1646 f(x',f(f(y,x)',z)) = x. [para(2(a,1),1645(a,1,2,1,1))]. given #86 (T,wt=11): 1647 f(x',f(y,f(x,z)')) = x. [para(2(a,1),1645(a,1,2))]. given #87 (A,wt=16): 68 f(x,f(f(y,x),f(f(x,y'),z))) = f(y,x). [para(23(a,1),3(a,1,1))]. given #88 (T,wt=11): 1666 f(x',f(y,f(z,x)')) = x. [para(2(a,1),1646(a,1,2))]. given #89 (T,wt=12): 817 f(x',f(y,f(x,z)')') = c_0. [back_rewrite(756),rewrite([782(6)])]. given #90 (T,wt=12): 963 f(x',f(f(y,x)',z)') = c_0. [para(783(a,1),44(a,1,2,1)),rewrite([822(6),783(10)])]. given #91 (T,wt=12): 964 f(f(x,y)',f(y',z)') = c_0. [para(783(a,1),47(a,1,2,1)),rewrite([822(6),783(10)])]. given #92 (A,wt=17): 70 f(x,f(f(x,y'),f(f(y,x),z))) = f(x,y'). [para(23(a,1),8(a,1,1))]. given #93 (T,wt=12): 965 f(x',f(y,f(z,x)')') = c_0. [para(783(a,1),53(a,1,2,1)),rewrite([822(6),783(10)])]. given #94 (T,wt=12): 1116 f(x,f(f(x',y)',z)) = x'. [para(644(a,1),35(a,1,1)),flip(a)]. given #95 (T,wt=12): 1117 f(x,f(y,f(x',z)')) = x'. [para(655(a,1),35(a,1,1)),flip(a)]. given #96 (T,wt=12): 1194 f(x,f(f(y,x')',z)) = x'. [para(669(a,1),35(a,1,1)),flip(a)]. given #97 (A,wt=16): 72 f(x,f(f(y,x),f(z,f(x,y')))) = f(y,x). [para(23(a,1),9(a,1,1))]. given #98 (T,wt=12): 1195 f(x,f(y,f(z,x')')) = x'. [para(672(a,1),35(a,1,1)),flip(a)]. given #99 (T,wt=12): 1196 f(f(x,y)',f(z,x')') = c_0. [para(2(a,1),757(a,1,2,1))]. given #100 (T,wt=12): 1264 f(f(x,y),f(y,x)) = f(x,y)'. [para(1219(a,2),318(a,1,2,2)),rewrite([1220(4),35(3)])]. given #101 (T,wt=10): 2026 f(f(x,y)',f(y,x)) = c_0. [para(1264(a,1),783(a,1,2,1)),rewrite([35(5)])]. given #102 (A,wt=17): 87 f(x,f(f(y',x),f(f(x,y),z))) = f(y',x). [para(31(a,1),3(a,1,1))]. given #103 (T,wt=12): 1463 f(f(x,y')',f(z,y)') = c_0. [para(2(a,1),773(a,1,2,1))]. given #104 (T,wt=12): 1532 f(f(x',y)',f(z,x)') = c_0. [para(2(a,1),787(a,1,2,1))]. given #105 (T,wt=12): 1786 f(f(x,y)',f(z,y')') = c_0. [para(8(a,1),817(a,1,2,1,2,1))]. given #106 (T,wt=13): 177 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(8(a,1),17(a,1,2)),rewrite([2(4)])]. given #107 (A,wt=16): 88 f(x,f(f(x,y),f(f(y',x),z))) = f(x,y). [para(31(a,1),8(a,1,1))]. given #108 (T,wt=13): 179 f(x,f(f(y,x),f(z,y))) = f(y,x). [para(17(a,1),9(a,1,2)),rewrite([2(4)])]. given #109 (T,wt=13): 181 f(x,f(f(y,z),f(x,z))) = f(x,z). [para(9(a,1),17(a,1,2)),rewrite([2(4)])]. given #110 (T,wt=13): 197 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(17(a,1),17(a,1,2)),rewrite([2(4)])]. given #111 (T,wt=13): 1207 f(f(x,y)',f(x',z)) = f(x,y). [para(757(a,1),316(a,1,2,2)),rewrite([2(7),822(7),35(6),35(8)])]. given #112 (A,wt=17): 90 f(x,f(f(y',x),f(z,f(x,y)))) = f(y',x). [para(31(a,1),9(a,1,1))]. given #113 (T,wt=13): 1303 f(f(x,y')',f(x,f(z,y))) = c_0. [back_rewrite(1058),rewrite([1220(4),2(6)])]. given #114 (T,wt=13): 1306 f(f(x,y')',f(x,f(y,z))) = c_0. [back_rewrite(1045),rewrite([1220(4),2(6)])]. given #115 (T,wt=13): 1484 f(f(x,y)',f(z,x')) = f(x,y). [para(773(a,1),1220(a,1,2)),rewrite([2(4),822(4),35(3),35(7)]),flip(a)]. given #116 (T,wt=13): 1649 f(f(x,y)',f(y',z)) = f(x,y). [para(8(a,1),1645(a,1,2,1,1))]. given #117 (A,wt=17): 96 f(x,f(f(x,y),f(f(f(y,z),x),u))) = f(x,y). [para(10(a,1),3(a,1,1))]. given #118 (T,wt=13): 1690 f(f(x,y)',f(z,y')) = f(x,y). [para(8(a,1),1647(a,1,2,2,1))]. given #119 (T,wt=13): 2010 f(f(x,y)',f(y,x)') = f(y,x). [para(1264(a,1),67(a,1,1)),rewrite([1241(7)])]. given #120 (T,wt=13): 2033 f(f(x,y)',f(f(y,x),z)') = c_0. [para(1264(a,1),963(a,1,2,1,1,1)),rewrite([35(5)])]. given #121 (T,wt=13): 2034 f(f(x,y),f(f(y,x)',z)') = c_0. [para(1264(a,1),964(a,1,1,1)),rewrite([35(3)])]. given #122 (A,wt=19): 97 f(x,f(f(f(y,z),x),f(f(x,y),u))) = f(f(y,z),x). [para(10(a,1),8(a,1,1))]. given #123 (T,wt=13): 2035 f(f(x,y)',f(z,f(y,x))') = c_0. [para(1264(a,1),965(a,1,2,1,2,1)),rewrite([35(5)])]. given #124 (T,wt=13): 2115 f(f(x,f(y,z)')',f(z,y)) = c_0. [para(1264(a,1),1463(a,1,2,1)),rewrite([35(7)])]. given #125 (T,wt=13): 2128 f(f(x,y),f(z,f(y,x)')') = c_0. [para(1264(a,1),1786(a,1,1,1)),rewrite([35(3)])]. given #126 (T,wt=13): 2382 f(f(x',y),f(x,z)') = f(x,z). [para(1207(a,1),2(a,1)),flip(a)]. given #127 (A,wt=15): 100 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(8(a,1),10(a,1,2)),rewrite([2(3),2(4)])]. given #128 (T,wt=13): 2481 f(f(x',y)',f(y,f(z,x))) = c_0. [para(2(a,1),1303(a,1,1,1))]. given #129 (T,wt=12): 3035 f(x',f(f(x,y),f(z,x))) = c_0. [para(125(a,1),2481(a,1,1,1))]. given #130 (T,wt=12): 3036 f(x',f(f(y,x),f(z,x))) = c_0. [para(129(a,1),2481(a,1,1,1))]. given #131 (T,wt=12): 3109 f(x',f(f(x,y),f(x,z))) = c_0. [para(2(a,1),3035(a,1,2,2))]. given #132 (A,wt=17): 102 f(x,f(f(x,y),f(z,f(f(y,u),x)))) = f(x,y). [para(10(a,1),9(a,1,1))]. given #133 (T,wt=12): 3110 f(x',f(f(y,x),f(x,z))) = c_0. [para(2(a,1),3035(a,1,2))]. given #134 (T,wt=13): 2482 f(f(x,y')',f(f(z,y),x)) = c_0. [para(2(a,1),1303(a,1,2))]. given #135 (T,wt=13): 2485 f(f(x,y)',f(x,f(z,y'))) = c_0. [para(35(a,1),1303(a,1,1,1,2))]. given #136 (T,wt=13): 2496 f(x,f(y',f(f(y,z),x))') = c_0. [para(22(a,1),1303(a,1,2)),rewrite([2(4),2(6)])]. given #137 (A,wt=16): 107 f(x,f(f(x,y),f(z,f(y',x)))) = f(x,y). [para(54(a,1),9(a,1,1))]. given #138 (T,wt=13): 2497 f(x,f(y',f(f(z,y),x))') = c_0. [para(25(a,1),1303(a,1,2)),rewrite([2(4),2(6)])]. given #139 (T,wt=13): 2505 f(f(x,f(y,z)')',f(y,x)) = c_0. [para(47(a,1),1303(a,1,2))]. given #140 (T,wt=13): 2539 f(f(x,f(y,z)')',f(z,x)) = c_0. [para(179(a,1),1303(a,1,2))]. given #141 (T,wt=13): 2542 f(f(x',y)',f(y,f(x,z))) = c_0. [para(2(a,1),1306(a,1,1,1))]. given #142 (A,wt=17): 109 f(x,f(f(x,y'),f(z,f(y,x)))) = f(x,y'). [para(66(a,1),9(a,1,1))]. given #143 (T,wt=13): 2543 f(f(x,y')',f(f(y,z),x)) = c_0. [para(2(a,1),1306(a,1,2))]. given #144 (T,wt=13): 2546 f(f(x,y)',f(x,f(y',z))) = c_0. [para(35(a,1),1306(a,1,1,1,2))]. given #145 (T,wt=13): 2552 f(x,f(y',f(x,f(y,z)))') = c_0. [para(16(a,1),1306(a,1,2)),rewrite([2(4),2(6)])]. given #146 (T,wt=13): 2557 f(x,f(y',f(x,f(z,y)))') = c_0. [para(99(a,1),1306(a,1,2)),rewrite([2(4),2(6)])]. given #147 (A,wt=16): 111 f(x,f(f(y,x),f(f(y',x),z))) = f(y,x). [para(67(a,1),3(a,1,1))]. given #148 (T,wt=13): 2571 f(f(x,y'),f(y,z)') = f(y,z). [para(1484(a,1),2(a,1)),flip(a)]. given #149 (T,wt=13): 2597 f(f(x',y),f(z,x)') = f(z,x). [para(1649(a,1),2(a,1)),flip(a)]. given #150 (T,wt=13): 2724 f(f(x,y'),f(z,y)') = f(z,y). [para(1690(a,1),2(a,1)),flip(a)]. given #151 (T,wt=13): 2772 f(f(x,f(y,z))',f(z,y)') = c_0. [para(2010(a,1),773(a,1,2,1)),rewrite([35(3)])]. given #152 (A,wt=17): 112 f(x,f(f(y',x),f(f(y,x),z))) = f(y',x). [para(67(a,1),8(a,1,1))]. given #153 (T,wt=13): 3015 f(f(x',y)',f(f(z,x),y)) = c_0. [para(2(a,1),2481(a,1,2))]. given #154 (T,wt=13): 3018 f(x,f(f(y,z)',f(x,y))') = c_0. [para(3(a,1),2481(a,1,2)),rewrite([2(6)])]. given #155 (T,wt=13): 3020 f(x,f(f(y,z)',f(y,x))') = c_0. [para(8(a,1),2481(a,1,2)),rewrite([2(6)])]. given #156 (T,wt=13): 3021 f(f(x,y)',f(y,f(z,x'))) = c_0. [para(35(a,1),2481(a,1,1,1,1))]. given #157 (A,wt=16): 114 f(x,f(f(y,x),f(z,f(y',x)))) = f(y,x). [para(67(a,1),9(a,1,1))]. given #158 (T,wt=13): 3023 f(x,f(f(y,z)',f(x,z))') = c_0. [para(9(a,1),2481(a,1,2)),rewrite([2(6)])]. given #159 (T,wt=13): 3028 f(f(f(x,y)',z)',f(z,x)) = c_0. [para(31(a,1),2481(a,1,2,2))]. given #160 (T,wt=13): 3031 f(f(f(x,y)',z)',f(z,y)) = c_0. [para(66(a,1),2481(a,1,2,2))]. given #161 (T,wt=13): 3038 f(x,f(f(y,z)',f(z,x))') = c_0. [para(17(a,1),2481(a,1,2)),rewrite([2(6)])]. given #162 (A,wt=21): 130 f(f(x,y),f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),w))) = x. [para(11(a,1),3(a,1,1))]. given #163 (T,wt=13): 3113 f(x,f(f(x',y),f(z,x'))) = c_0. [para(35(a,1),3035(a,1,1))]. given #164 (T,wt=13): 3135 f(x',f(f(x,y),f(z,x))') = x. [para(3035(a,1),1241(a,1,2)),rewrite([2(3),822(3),35(2)]),flip(a)]. given #165 (T,wt=13): 3149 f(x,f(f(y,x'),f(z,x'))) = c_0. [para(35(a,1),3036(a,1,1))]. given #166 (T,wt=13): 3171 f(x',f(f(y,x),f(z,x))') = x. [para(3036(a,1),1241(a,1,2)),rewrite([2(3),822(3),35(2)]),flip(a)]. given #167 (A,wt=31): 132 f(f(x,y),f(f(f(x,y),f(f(x,f(y,z)),u)),f(x,w))) = f(f(x,y),f(f(x,f(y,z)),u)). [para(11(a,1),8(a,1,1))]. given #168 (T,wt=13): 3188 f(x,f(f(x',y),f(x',z))) = c_0. [para(35(a,1),3109(a,1,1))]. given #169 (T,wt=13): 3207 f(x',f(f(x,y),f(x,z))') = x. [para(3109(a,1),1241(a,1,2)),rewrite([2(3),822(3),35(2)]),flip(a)]. given #170 (T,wt=13): 3305 f(x,f(f(y,x'),f(x',z))) = c_0. [para(35(a,1),3110(a,1,1))]. given #171 (T,wt=13): 3324 f(x',f(f(y,x),f(x,z))') = x. [para(3110(a,1),1241(a,1,2)),rewrite([2(3),822(3),35(2)]),flip(a)]. given #172 (A,wt=21): 133 f(f(x,y),f(y,f(f(f(x,y),f(f(y,f(x,z)),u)),w))) = y. [para(8(a,1),11(a,1,2,1)),rewrite([8(13)])]. given #173 (T,wt=13): 3332 f(f(x,y)',f(f(z,y'),x)) = c_0. [para(35(a,1),2482(a,1,1,1,2))]. given #174 (T,wt=13): 3427 f(x,f(y,f(f(y',z),x))') = c_0. [para(22(a,1),2485(a,1,2)),rewrite([2(4),2(6)])]. given #175 (T,wt=13): 3429 f(x,f(y,f(f(z,y'),x))') = c_0. [para(25(a,1),2485(a,1,2)),rewrite([2(4),2(6)])]. given #176 (T,wt=13): 3489 f(f(x',y)',f(f(x,z),y)) = c_0. [para(18(a,1),2496(a,1,2,1,2)),rewrite([2(6)])]. given #177 (A,wt=21): 135 f(f(x,y),f(x,f(z,f(f(x,y),f(f(x,f(y,u)),w))))) = x. [para(11(a,1),9(a,1,1))]. given #178 (T,wt=13): 3521 f(x,f(y',f(f(y,z),x))) = x'. [para(2496(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #179 (T,wt=13): 3671 f(x,f(y',f(f(z,y),x))) = x'. [para(2497(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #180 (T,wt=13): 3795 f(f(x,y)',f(f(y',z),x)) = c_0. [para(155(a,1),2539(a,1,1,1,2,1)),rewrite([35(2)])]. given #181 (T,wt=13): 3864 f(f(x,y)',f(y,f(x',z))) = c_0. [para(2382(a,1),2539(a,1,1,1))]. given #182 (A,wt=15): 136 f(f(x,y),f(x,f(f(x,f(y,z)),u))) = x. [para(11(a,1),9(a,1,2)),rewrite([2(6)])]. given #183 (T,wt=13): 4068 f(x,f(y,f(x,f(y',z)))') = c_0. [para(16(a,1),2546(a,1,2)),rewrite([2(4),2(6)])]. given #184 (T,wt=13): 4081 f(x,f(y,f(x,f(z,y')))') = c_0. [para(99(a,1),2546(a,1,2)),rewrite([2(4),2(6)])]. given #185 (T,wt=13): 4154 f(x,f(y',f(x,f(y,z)))) = x'. [para(2552(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #186 (T,wt=13): 4196 f(x,f(y',f(x,f(z,y)))) = x'. [para(2557(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #187 (A,wt=21): 137 f(f(x,y),f(x,f(f(f(x,y),f(f(x,f(z,y)),u)),w))) = x. [para(9(a,1),11(a,1,2,1)),rewrite([9(13)])]. given #188 (T,wt=13): 4395 f(f(x,y)',f(f(z,x'),y)) = c_0. [para(35(a,1),3015(a,1,1,1,1))]. given #189 (T,wt=13): 4489 f(x,f(f(y,z)',f(x,y))) = x'. [para(3018(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #190 (T,wt=13): 4566 f(x,f(f(y,z)',f(y,x))) = x'. [para(3020(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #191 (T,wt=13): 4750 f(x,f(f(y,z)',f(x,z))) = x'. [para(3023(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #192 (A,wt=20): 139 f(f(x,y),f(x,f(f(f(x,y),f(f(x,y'),z)),u))) = x. [para(14(a,1),11(a,1,2,1)),rewrite([14(13)])]. given #193 (T,wt=13): 5029 f(x,f(f(y,z)',f(z,x))) = x'. [para(3038(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #194 (T,wt=13): 5940 f(x,f(y,f(f(y',z),x))) = x'. [para(3427(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #195 (T,wt=13): 6028 f(x,f(y,f(f(z,y'),x))) = x'. [para(3429(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #196 (T,wt=13): 6764 f(x,f(y,f(x,f(y',z)))) = x'. [para(4068(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #197 (A,wt=30): 140 f(f(x,y),f(x',f(f(x,y),f(f(x,f(y,z)),u)))) = f(f(x,y),f(f(x,f(y,z)),u)). [para(11(a,1),23(a,1,1)),rewrite([2(8)])]. given #198 (T,wt=13): 6808 f(x,f(y,f(x,f(z,y')))) = x'. [para(4081(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. given #199 (T,wt=13): 6970 f(x',y) = f(y,f(f(z,y'),x)). [back_rewrite(6027),rewrite([6948(7)])]. given #200 (T,wt=13): 6971 f(x',y) = f(y,f(f(y',z),x)). [back_rewrite(5939),rewrite([6948(7)])]. given #201 (T,wt=13): 7371 f(x,f(y,f(z,f(y,x))')') = c_0. [back_rewrite(2541),rewrite([7308(8),35(7),2(6)])]. given #202 (A,wt=20): 141 f(f(x,y),f(y,f(f(f(x,y),f(f(y,x'),z)),u))) = y. [para(23(a,1),11(a,1,2,1)),rewrite([23(13)])]. given #203 (T,wt=13): 7376 f(x,f(f(y,x'),z)') = f(x,z). [back_rewrite(7208),rewrite([7374(7)])]. given #204 (T,wt=13): 7377 f(x,f(y,f(x',z))') = f(x,y). [back_rewrite(6587),rewrite([7375(7)])]. given #205 (T,wt=13): 7378 f(f(x,y)',z) = f(x,f(z,y)'). [back_rewrite(4925),rewrite([7375(7),7374(5)]),flip(a)]. given #206 (T,wt=13): 7380 f(x,f(y,f(z,x'))') = f(x,y). [back_rewrite(4629),rewrite([7375(7)])]. given #207 (A,wt=23): 146 f(f(x,y),f(f(f(x,y),f(y,z)),f(x,u))) = f(f(x,y),f(y,z)). [para(10(a,1),11(a,1,2,2,1))]. given #208 (T,wt=13): 7895 f(x,f(f(x',y),z)') = f(x,z). [para(5940(a,1),90(a,1,2,2)),rewrite([2(5),2(7),1666(7),2(6)]),flip(a)]. given #209 (T,wt=13): 8038 f(x,f(y,f(x',z))) = f(x,y'). [para(6764(a,1),100(a,1,2)),flip(a)]. given #210 (T,wt=13): 8328 f(x,f(y,f(z,x'))) = f(x,y'). [para(6808(a,1),100(a,1,2)),flip(a)]. given #211 (T,wt=13): 8372 f(x,f(f(y,x'),z)) = f(x,z'). [para(6970(a,1),2(a,1))]. given #212 (A,wt=19): 169 f(x,f(f(x,f(y,z)),f(u,f(y,x)))) = f(x,f(y,z)). [para(16(a,1),9(a,1,1))]. given #213 (T,wt=13): 8711 f(x,f(f(x',y),z)) = f(x,z'). [para(6971(a,1),2(a,1))]. given #214 (T,wt=13): 8971 f(x,f(y,f(f(y,x),z)')') = c_0. [para(2(a,1),7371(a,1,2,1,2,1))]. given #215 (T,wt=13): 9340 f(x,f(y,z)') = f(y,f(x,z)'). [para(7378(a,1),2(a,1))]. given #216 (T,wt=13): 9342 f(f(x,y)',z) = f(x,f(y,z)'). [para(2(a,1),7378(a,2,2,1))]. given #217 (A,wt=19): 170 f(x,f(f(f(y,x),z),f(x,f(y,u)))) = f(x,f(y,u)). [para(16(a,1),10(a,1,1))]. given #218 (T,wt=13): 9381 f(x,f(y,z)') = f(z,f(x,y)'). [para(80(a,1),7378(a,1,1,1)),rewrite([9342(3),1759(8)])]. given #219 (T,wt=13): 9826 f(x,f(y,z)') = f(z,f(y,x)'). [back_rewrite(9341),rewrite([9342(3),9342(6)])]. given #220 (T,wt=14): 455 f(f(x,y),f(x,f(f(x,y'),z))) = x. [para(14(a,1),44(a,1,2,1)),rewrite([14(10)])]. given #221 (T,wt=14): 462 f(f(x,y),f(x,f(f(y',x),z))) = x. [para(54(a,1),44(a,1,2,1)),rewrite([54(10)])]. given #222 (A,wt=25): 172 f(f(x,f(y,z)),f(f(y,f(x,f(y,z))),f(x,u))) = f(y,f(x,f(y,z))). [para(16(a,1),11(a,1,2,2,1)),rewrite([2(5),2(11)])]. given #223 (T,wt=14): 463 f(f(x,y'),f(x,f(f(y,x),z))) = x. [para(66(a,1),44(a,1,2,1)),rewrite([66(10)])]. given #224 (T,wt=14): 490 f(f(x,y'),f(x,f(f(x,y),z))) = x. [para(14(a,1),47(a,1,2,1)),rewrite([14(10)])]. given #225 (T,wt=14): 519 f(f(x,y),f(x,f(z,f(x,y')))) = x. [para(14(a,1),53(a,1,2,1)),rewrite([14(10)])]. given #226 (T,wt=14): 526 f(f(x,y),f(x,f(z,f(y',x)))) = x. [para(54(a,1),53(a,1,2,1)),rewrite([54(10)])]. given #227 (A,wt=15): 186 f(x,f(y,f(x,f(z,y)))) = f(x,f(z,y)). [para(17(a,1),10(a,1,2)),rewrite([2(3),2(4)])]. given #228 (T,wt=14): 527 f(f(x,y'),f(x,f(z,f(y,x)))) = x. [para(66(a,1),53(a,1,2,1)),rewrite([66(10)])]. given #229 (T,wt=14): 1295 f(f(x,y),f(x',z)') = f(x',z). [para(757(a,1),1219(a,2,2)),rewrite([35(3),2(10),822(10),35(9)])]. given #230 (T,wt=14): 1691 f(f(x,y),f(x,f(z,f(y,u)'))) = x. [para(1647(a,1),9(a,1,2,2)),rewrite([2(6)])]. given #231 (T,wt=14): 1698 f(f(x,f(y,f(z,u)')),f(z,x)) = x. [para(1647(a,1),41(a,1,2,1))]. given #232 (A,wt=21): 235 f(f(x',y),f(x',f(f(f(x',y),f(x,z)),u))) = x'. [para(155(a,1),19(a,1,2,1)),rewrite([155(13)])]. given #233 (T,wt=14): 1699 f(f(x,y),f(f(z,f(y,u)'),x)) = x. [para(1647(a,1),99(a,1,1,2))]. given #234 (T,wt=14): 1758 f(f(x,y),f(x,f(z,f(u,y)'))) = x. [para(1666(a,1),9(a,1,2,2)),rewrite([2(6)])]. given #235 (T,wt=14): 1767 f(f(x,f(y,f(z,u)')),f(u,x)) = x. [para(1666(a,1),41(a,1,2,1))]. given #236 (T,wt=14): 1768 f(f(x,y),f(f(z,f(u,y)'),x)) = x. [para(1666(a,1),99(a,1,1,2))]. given #237 (A,wt=21): 268 f(f(x,y),f(x,f(f(f(x,y),f(f(f(z,y),x),u)),w))) = x. [para(25(a,1),19(a,1,2,1)),rewrite([25(13)])]. given #238 (T,wt=14): 2009 f(f(x,f(y,z)),f(x,f(z,y)')) = x. [para(1264(a,1),9(a,1,2,2))]. given #239 (T,wt=14): 2384 f(f(x,f(y',z)),f(x,f(y,u))) = x. [para(1207(a,1),9(a,1,2,2))]. given #240 (T,wt=14): 2390 f(f(x,f(y',z)),f(f(y,u),x)) = x. [para(1207(a,1),41(a,1,2,1))]. given #241 (T,wt=14): 2391 f(f(x,f(y,z)),f(f(y',u),x)) = x. [para(1207(a,1),99(a,1,1,2))]. given #242 (A,wt=17): 425 f(f(x,y),f(x,f(f(f(y,z),f(x,y)),u))) = x. [para(10(a,1),24(a,1,2,1)),rewrite([10(11)])]. given #243 (T,wt=14): 2573 f(f(x,f(y,z')),f(x,f(z,u))) = x. [para(1484(a,1),9(a,1,2,2))]. given #244 (T,wt=14): 2574 f(f(x,y),f(z,x')') = f(z,x'). [para(1484(a,1),23(a,1,1)),rewrite([35(6),1220(6)])]. given #245 (T,wt=14): 2580 f(f(x,f(y,z')),f(f(z,u),x)) = x. [para(1484(a,1),41(a,1,2,1))]. given #246 (T,wt=14): 2581 f(f(x,f(y,z)),f(f(u,y'),x)) = x. [para(1484(a,1),99(a,1,1,2))]. given #247 (A,wt=29): 500 f(f(f(x,y),f(x,z)),f(f(x,y),f(f(f(f(x,y),f(x,z)),f(y,u)),w))) = f(x,y). [para(47(a,1),19(a,1,2,1)),rewrite([47(16)])]. ============================== PROOF ================================= % Proof 1 at 6.40 (+ 0.06) seconds: "Sheffer". % Length of proof is 119. % Level of proof is 30. % Maximum clause weight is 30.000. % Given clauses 247. 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(non_clause) # label(goal). [goal]. 2 f(x,y) = f(y,x). [assumption]. 3 f(f(x,y),f(x,f(y,z))) = x. [assumption]. 4 x' = f(x,x). [assumption]. 5 f(x,x) = x'. [copy(4),flip(a)]. 6 f(f(c1,c1),f(c1,c1)) != c1 | f(c1,f(c2,f(c2,c2))) != f(c1,c1) | f(f(f(c2,c2),c1),f(f(c3,c3),c1)) != f(f(c1,f(c2,c3)),f(c1,f(c2,c3))) # answer("Sheffer"). [deny(1)]. 7 c1'' != c1 | f(c1,f(c2,c2')) != c1' | f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [copy(6),rewrite([5(3),5(5),5(5),5(10),5(14),5(17),2(18),5(21),2(22),5(34)])]. 8 f(f(x,y),f(y,f(x,z))) = y. [para(2(a,1),3(a,1,1))]. 9 f(f(x,y),f(x,f(z,y))) = x. [para(2(a,1),3(a,1,2,2))]. 10 f(f(x,y),f(f(y,z),x)) = x. [para(2(a,1),3(a,1,2))]. 11 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y). [para(3(a,1),3(a,1,1))]. 12 f(x,f(x,f(x,y))) = f(x,y). [para(3(a,1),3(a,1,2)),rewrite([2(2),2(3)])]. 13 f(x',f(x,f(x,y))) = x. [para(5(a,1),3(a,1,1))]. 14 f(f(x,y),f(x,y')) = x. [para(5(a,1),3(a,1,2,2))]. 16 f(f(x,f(y,z)),f(y,x)) = x. [para(8(a,1),2(a,1)),flip(a)]. 19 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x). [para(8(a,1),3(a,1,1))]. 21 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [para(3(a,1),8(a,1,1))]. 22 f(f(f(x,y),z),f(z,x)) = z. [para(3(a,1),8(a,1,2,2))]. 23 f(f(x,y),f(y,x')) = y. [para(5(a,1),8(a,1,2,2))]. 25 f(f(f(x,y),z),f(z,y)) = z. [para(8(a,1),8(a,1,2,2))]. 26 f(x',f(x,f(y,x))) = x. [para(2(a,1),13(a,1,2,2))]. 28 f(x,f(x,x')) = x'. [para(13(a,1),3(a,1,2)),rewrite([2(2),2(3)])]. 31 f(f(x',y),f(y,x)) = y. [para(13(a,1),8(a,1,2,2))]. 35 x'' = x. [para(28(a,1),3(a,1,2)),rewrite([5(1),5(3)])]. 37 f(c1,f(c2,c2')) != c1' | f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(7),rewrite([35(3)]),xx(a)]. 41 f(f(x,y),f(f(z,y),x)) = x. [para(2(a,1),9(a,1,2))]. 42 f(x,f(f(x,y),f(f(x,f(z,y)),u))) = f(x,y). [para(9(a,1),3(a,1,1))]. 44 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(3(a,1),9(a,1,2)),rewrite([2(4)])]. 47 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(8(a,1),9(a,1,2)),rewrite([2(4)])]. 53 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(9(a,1),9(a,1,2)),rewrite([2(4)])]. 66 f(f(x,y'),f(y,x)) = x. [para(23(a,1),2(a,1)),flip(a)]. 67 f(f(x,y),f(x',y)) = y. [para(2(a,1),23(a,1,2))]. 80 f(x,f(y,x)') = f(y,x). [para(8(a,1),26(a,1,2)),rewrite([2(3)])]. 90 f(x,f(f(y',x),f(z,f(x,y)))) = f(y',x). [para(31(a,1),9(a,1,1))]. 98 f(x,f(f(y,z),f(x,y))) = f(x,y). [para(10(a,1),8(a,1,2)),rewrite([2(4)])]. 99 f(f(x,f(y,z)),f(z,x)) = x. [para(8(a,1),10(a,1,2,1))]. 100 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(8(a,1),10(a,1,2)),rewrite([2(3),2(4)])]. 116 f(x,f(f(y,x)',f(y',x))) = f(y',x). [para(67(a,1),23(a,1,1)),rewrite([2(5)])]. 125 f(x',f(x,y)) = x. [para(31(a,1),80(a,1,2,1)),rewrite([2(3),31(7)])]. 129 f(x',f(y,x)) = x. [para(66(a,1),80(a,1,2,1)),rewrite([2(3),66(7)])]. 140 f(f(x,y),f(x',f(f(x,y),f(f(x,f(y,z)),u)))) = f(f(x,y),f(f(x,f(y,z)),u)). [para(11(a,1),23(a,1,1)),rewrite([2(8)])]. 155 f(x,f(x',y)) = x'. [para(35(a,1),125(a,1,1))]. 157 f(x,f(y,x')) = x'. [para(129(a,1),8(a,1,2)),rewrite([2(3)])]. 316 f(x,f(y,f(x,y))) = x'. [para(99(a,1),21(a,1,2)),rewrite([5(1)]),flip(a)]. 318 f(x,f(y,f(y,x))) = x'. [para(2(a,1),316(a,1,2,2))]. 334 f(x,f(f(y,x),f(y,x)')) = x'. [para(80(a,1),316(a,1,2,2)),rewrite([2(4)])]. 369 f(f(x,x'),f(x',y)) = f(x',y)'. [para(155(a,1),318(a,1,2,2)),rewrite([2(5)])]. 500 f(f(f(x,y),f(x,z)),f(f(x,y),f(f(f(f(x,y),f(x,z)),f(y,u)),w))) = f(x,y). [para(47(a,1),19(a,1,2,1)),rewrite([47(16)])]. 506 f(f(x,f(y,x)),f(f(y,x),f(y,z))) = f(f(y,x),f(y,z))'. [para(47(a,1),318(a,1,2,2)),rewrite([2(6)])]. 519 f(f(x,y),f(x,f(z,f(x,y')))) = x. [para(14(a,1),53(a,1,2,1)),rewrite([14(10)])]. 527 f(f(x,y'),f(x,f(z,f(y,x)))) = x. [para(66(a,1),53(a,1,2,1)),rewrite([66(10)])]. 597 f(x,f(x',y)') = f(x,x'). [para(157(a,1),42(a,1,2,2,1)),rewrite([369(5)])]. 637 f(x,f(y,x')') = f(x,x'). [para(2(a,1),597(a,1,2,1))]. 640 f(x',f(x,y)') = f(x,x'). [para(35(a,1),597(a,1,2,1,1)),rewrite([35(7),2(6)])]. 671 f(x',f(y,x)') = f(x,x'). [para(35(a,1),637(a,1,2,1,2)),rewrite([35(7),2(6)])]. 675 f(f(x,x'),f(y,x)) = f(y,x)'. [para(637(a,1),31(a,1,1)),rewrite([35(3),2(2),35(4),2(5),80(5),35(6)])]. 704 f(f(x,y),f(x,y)') = f(x,x'). [para(3(a,1),640(a,1,2,1)),rewrite([2(4),640(4)]),flip(a)]. 706 f(x,x') = f(y,y'). [para(8(a,1),640(a,1,2,1)),rewrite([2(4),671(4),704(6)])]. 724 f(x',f(f(x,x'),f(f(x,y)',z))) = f(x,x'). [para(640(a,1),44(a,1,2,1)),rewrite([640(12)])]. 725 f(f(x,y)',f(x',z)') = f(x,x'). [para(640(a,1),47(a,1,2,1)),rewrite([369(7),640(10)])]. 738 f(x,f(y,y')) = x'. [back_rewrite(334),rewrite([704(4)])]. 739 f(x,x') = c_0. [new_symbol(706)]. 749 f(c1,c_0) != c1' | f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(37),rewrite([739(5)])]. 750 f(x,c_0) = x'. [back_rewrite(738),rewrite([739(2)])]. 757 f(f(x,y)',f(x',z)') = c_0. [back_rewrite(725),rewrite([739(8)])]. 758 f(x',f(c_0,f(f(x,y)',z))) = c_0. [back_rewrite(724),rewrite([739(3),739(9)])]. 782 f(c_0,f(x,y)) = f(x,y)'. [back_rewrite(675),rewrite([739(2)])]. 783 f(x',f(y,x)') = c_0. [back_rewrite(671),rewrite([739(6)])]. 801 f(f(c1,c2'),f(c1,c3')) != f(c1,f(c2,c3))' # answer("Sheffer"). [back_rewrite(749),rewrite([750(3)]),xx(a)]. 816 f(x',f(f(x,y)',z)') = c_0. [back_rewrite(758),rewrite([782(6)])]. 822 f(c_0,x) = x'. [para(739(a,1),8(a,1,1)),rewrite([125(4)])]. 959 f(x,f(y,f(x,y))') = c_0. [para(316(a,1),783(a,1,2,1)),rewrite([35(5),2(4)])]. 1045 f(f(x,f(y,z)),f(x,f(y,x))') = c_0. [para(16(a,1),959(a,1,2,1,2)),rewrite([2(4)])]. 1058 f(f(x,f(y,z)),f(x,f(z,x))') = c_0. [para(99(a,1),959(a,1,2,1,2)),rewrite([2(4)])]. 1207 f(f(x,y)',f(x',z)) = f(x,y). [para(757(a,1),316(a,1,2,2)),rewrite([2(7),822(7),35(6),35(8)])]. 1219 f(x',y) = f(y,f(x,y)). [back_rewrite(116),rewrite([1207(5)]),flip(a)]. 1220 f(x,f(y,x)) = f(x,y'). [para(1219(a,1),2(a,1))]. 1232 f(f(x,y)',f(f(y,z),x)) = f(x,f(y,z)'). [para(10(a,1),1219(a,2,2)),rewrite([2(8),1220(8)])]. 1241 f(x,f(x,y)) = f(x,y'). [para(1219(a,2),12(a,1,2,2)),rewrite([1220(3),35(2),1220(4)])]. 1259 f(f(x,y)',f(f(z,y),x)) = f(x,f(z,y)'). [para(41(a,1),1219(a,2,2)),rewrite([2(8),1220(8)])]. 1303 f(f(x,y')',f(x,f(z,y))) = c_0. [back_rewrite(1058),rewrite([1220(4),2(6)])]. 1306 f(f(x,y')',f(x,f(y,z))) = c_0. [back_rewrite(1045),rewrite([1220(4),2(6)])]. 1310 f(f(x,y'),f(f(y,x),f(y,z))) = f(f(y,x),f(y,z))'. [back_rewrite(506),rewrite([1220(2)])]. 1645 f(x',f(f(x,y)',z)) = x. [para(816(a,1),1241(a,1,2)),rewrite([2(3),822(3),35(2),35(6)]),flip(a)]. 1646 f(x',f(f(y,x)',z)) = x. [para(2(a,1),1645(a,1,2,1,1))]. 1666 f(x',f(y,f(z,x)')) = x. [para(2(a,1),1646(a,1,2))]. 2481 f(f(x',y)',f(y,f(z,x))) = c_0. [para(2(a,1),1303(a,1,1,1))]. 2496 f(x,f(y',f(f(y,z),x))') = c_0. [para(22(a,1),1303(a,1,2)),rewrite([2(4),2(6)])]. 2497 f(x,f(y',f(f(z,y),x))') = c_0. [para(25(a,1),1303(a,1,2)),rewrite([2(4),2(6)])]. 2546 f(f(x,y)',f(x,f(y',z))) = c_0. [para(35(a,1),1306(a,1,1,1,2))]. 2980 f(f(x',f(y,z)),f(x,f(y,f(x',f(y,z))))) = f(y,f(x',f(y,z))). [para(100(a,1),31(a,1,1)),rewrite([2(8)])]. 3018 f(x,f(f(y,z)',f(x,y))') = c_0. [para(3(a,1),2481(a,1,2)),rewrite([2(6)])]. 3031 f(f(f(x,y)',z)',f(z,y)) = c_0. [para(66(a,1),2481(a,1,2,2))]. 3521 f(x,f(y',f(f(y,z),x))) = x'. [para(2496(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. 3671 f(x,f(y',f(f(z,y),x))) = x'. [para(2497(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. 4068 f(x,f(y,f(x,f(y',z)))') = c_0. [para(16(a,1),2546(a,1,2)),rewrite([2(4),2(6)])]. 4105 f(f(x,y),f(x,f(y',z))) = f(x,f(y',z))'. [para(2546(a,1),1220(a,1,2)),rewrite([2(5),822(5),35(10),2(9)]),flip(a)]. 4489 f(x,f(f(y,z)',f(x,y))) = x'. [para(3018(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. 4925 f(f(f(x,y)',z)',f(z,y)') = f(f(x,y)',z). [para(3031(a,1),1241(a,1,2)),rewrite([2(6),822(6),35(5)]),flip(a)]. 6298 f(x',f(f(x,y),z)') = f(x',z). [para(3521(a,1),90(a,1,2,2)),rewrite([2(6),2(8),1666(8),2(7)]),flip(a)]. 6425 f(x',f(f(y,x),z)') = f(x',z). [para(3671(a,1),90(a,1,2,2)),rewrite([2(6),2(8),1666(8),2(7)]),flip(a)]. 6764 f(x,f(y,f(x,f(y',z)))) = x'. [para(4068(a,1),1241(a,1,2)),rewrite([750(2),35(7)]),flip(a)]. 7308 f(f(x,y)',f(z,x)) = f(f(x,y)',z'). [para(4489(a,1),100(a,1,2)),flip(a)]. 7374 f(f(x,y)',f(z,y)') = f(x,f(z,y)'). [back_rewrite(1259),rewrite([7308(5)])]. 7375 f(f(x,y)',f(y,z)') = f(x,f(y,z)'). [back_rewrite(1232),rewrite([7308(5)])]. 7378 f(f(x,y)',z) = f(x,f(z,y)'). [back_rewrite(4925),rewrite([7375(7),7374(5)]),flip(a)]. 8038 f(x,f(y,f(x',z))) = f(x,y'). [para(6764(a,1),100(a,1,2)),flip(a)]. 8066 f(f(x,y'),f(x',f(y,z))) = f(y,f(x',f(y,z))). [back_rewrite(2980),rewrite([8038(8),2(6)])]. 8078 f(x',f(f(x,y'),z)) = f(x',z'). [para(5(a,1),140(a,1,1)),rewrite([5(3),1241(5),1241(8),6298(7),1241(4),5(4),1241(6)]),flip(a)]. 8105 f(f(x,y'),f(f(y,x),z)) = f(f(x,y'),f(x',z)). [para(19(a,1),140(a,1,2,2,2,1)),rewrite([1220(2),1220(5),8078(9),6425(7),1220(7),19(13)]),flip(a)]. 8270 f(f(x,y),f(x,z))' = f(x,f(y',f(x,z))). [back_rewrite(1310),rewrite([8105(6),8066(6)]),flip(a)]. 9342 f(f(x,y)',z) = f(x,f(y,z)'). [para(2(a,1),7378(a,2,2,1))]. 9525 f(x,f(y,f(x,z)')) = f(x,f(y,z)). [para(7378(a,1),1220(a,1,2)),rewrite([35(7)])]. 9529 f(x,f(y,f(x,z))') = f(x,f(y,z')'). [para(7378(a,1),1241(a,1)),rewrite([9342(3),2(4),9525(4),9342(8)])]. 13280 f(x,f(y,f(x,z'))) = f(x,f(y,z)). [para(519(a,1),10(a,1,2)),rewrite([2(5),1241(5),9529(5),35(2),2(4),1241(4),35(3)]),flip(a)]. 13434 f(x,f(y,f(x,z))) = f(x,f(y,z')). [para(527(a,1),98(a,1,2,1)),rewrite([13280(4)])]. 13765 f(f(x,y),f(x,z))' = f(x,f(y',z')). [back_rewrite(8270),rewrite([13434(8)])]. 14481 f(f(x,y),f(x,z)) = f(x,f(y',z'))'. [para(500(a,1),125(a,1,2)),rewrite([13765(4),2(6),4105(6)]),flip(a)]. 14901 $F # answer("Sheffer"). [back_rewrite(801),rewrite([14481(9),35(4),35(5)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=247. Generated=108218. Kept=14897. proofs=1. Usable=66. Sos=2611. Demods=2933. Limbo=420, Disabled=11804. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=93320. Back_subsumed=482. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=14473 (1 lex), Back_demodulated=11318. Back_unit_deleted=0. Demod_attempts=1738246. Demod_rewrites=288997. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=10. Nonunit_bsub_feature_tests=3. Megabytes=12.45. User_CPU=6.40, System_CPU=0.06, Wall_clock=6. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5419 exit (max_proofs) Tue Nov 3 09:58:02 2009