============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11623 was started by mccune on cleo.thornwood, Sat Aug 12 21:15:02 2006 The command was "/home/mccune/bin/prover9 -f pair-def.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file pair-def.in 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. f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer"). x' = f(x,x). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(x,y) = f(y,x). [assumption]. f(f(x,y),f(x,f(y,z))) = x. [assumption]. f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer"). [assumption]. x' = f(x,x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ a, b, c, f, ' ]). After inverse_order: (no changes). Folding symbols: '/1. After fold_eq: Function symbol precedence: lex([ a, b, c, ', f ]). 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. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 f(x,y) = f(y,x). [assumption]. 2 f(f(x,y),f(x,f(y,z))) = x. [assumption]. 6 f(x,x) = x'. [copy(5),flip(a)]. 7 a'' != a | f(a,f(b,b')) != a' | f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(4),rewrite(6(3),6(5),6(5),6(10),6(14),6(25),6(24),6(28)),flip(c)]. end_of_list. formulas(demodulators). 1 f(x,y) = f(y,x). [assumption]. % (lex-dep) 2 f(f(x,y),f(x,f(y,z))) = x. [assumption]. 6 f(x,x) = x'. [copy(5),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 1 f(x,y) = f(y,x). [assumption]. given #2 (I,wt=11): 2 f(f(x,y),f(x,f(y,z))) = x. [assumption]. given #3 (I,wt=6): 6 f(x,x) = x'. [copy(5),flip(a)]. given #4 (I,wt=30): 7 a'' != a | f(a,f(b,b')) != a' | f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(4),rewrite(6(3),6(5),6(5),6(10),6(14),6(25),6(24),6(28)),flip(c)]. given #5 (T,wt=10): 13 f(x',f(x,f(x,y))) = x. [para(6(a,1),2(a,1,1))]. given #6 (A,wt=11): 8 f(f(x,y),f(y,f(x,z))) = y. [para(1(a,1),2(a,1,1))]. given #7 (F,wt=9): 18 f(x,f(x,x')) = x'. [para(13(a,1),2(a,1,2)),rewrite(1(2),1(3))]. given #8 (F,wt=25): 37 f(a,f(b,b')) != a' | f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(7),rewrite(35(3)),xx(a)]. given #9 (T,wt=5): 35 x'' = x. [para(18(a,1),2(a,1,2)),rewrite(6(1),6(3))]. given #10 (T,wt=9): 19 f(x',f(x,x')) = x. [para(6(a,1),13(a,1,2,2))]. given #11 (A,wt=11): 9 f(f(x,y),f(x,f(z,y))) = x. [para(1(a,1),2(a,1,2,2))]. given #12 (F,wt=10): 14 f(f(x,y),f(x,y')) = x. [para(6(a,1),2(a,1,2,2))]. given #13 (F,wt=10): 16 f(x',f(x,f(y,x))) = x. [para(1(a,1),13(a,1,2,2))]. given #14 (T,wt=10): 28 f(f(x,y),f(y,x')) = y. [para(6(a,1),8(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(1(a,1),2(a,1,2))]. given #17 (F,wt=10): 54 f(f(x,y),f(y',x)) = x. [para(1(a,1),14(a,1,2))]. given #18 (F,wt=10): 69 f(x,f(y,x)') = f(y,x). [para(8(a,1),16(a,1,2)),rewrite(1(3))]. given #19 (T,wt=8): 117 f(x',f(x,y)) = x. [para(31(a,1),69(a,1,2,1)),rewrite(1(3),31(7))]. given #20 (T,wt=8): 121 f(x',f(y,x)) = x. [para(1(a,1),117(a,1,2))]. given #21 (A,wt=17): 11 f(x,f(f(x,y),f(f(x,f(y,z)),u))) = f(x,y). [para(2(a,1),2(a,1,1))]. given #22 (F,wt=9): 124 f(x,f(x',y)) = x'. [para(35(a,1),117(a,1,1))]. given #23 (F,wt=9): 126 f(x,f(y,x')) = x'. [para(121(a,1),8(a,1,2)),rewrite(1(3))]. given #24 (T,wt=10): 74 f(x,f(x,y)') = f(x,y). [para(9(a,1),16(a,1,2)),rewrite(1(3))]. given #25 (T,wt=10): 76 f(f(x,y'),f(y,x)) = x. [para(28(a,1),1(a,1)),flip(a)]. given #26 (A,wt=11): 12 f(x,f(x,f(x,y))) = f(x,y). [para(2(a,1),2(a,1,2)),rewrite(1(2),1(3))]. given #27 (F,wt=10): 77 f(f(x,y),f(x',y)) = y. [para(1(a,1),28(a,1,2))]. given #28 (F,wt=11): 21 f(f(x,f(y,z)),f(y,x)) = x. [para(8(a,1),1(a,1)),flip(a)]. given #29 (T,wt=11): 22 f(f(x,y),f(y,f(z,x))) = y. [para(1(a,1),8(a,1,2,2))]. given #30 (T,wt=11): 23 f(f(x,y),f(f(x,z),y)) = y. [para(1(a,1),8(a,1,2))]. given #31 (A,wt=17): 24 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x). [para(8(a,1),2(a,1,1))]. given #32 (F,wt=11): 25 f(x,f(x,f(y,x))) = f(y,x). [para(8(a,1),2(a,1,2)),rewrite(1(2),1(3))]. given #33 (F,wt=11): 27 f(f(f(x,y),z),f(z,x)) = z. [para(2(a,1),8(a,1,2,2))]. given #34 (T,wt=11): 33 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(1(a,1),9(a,1,2))]. given #36 (A,wt=19): 26 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [para(2(a,1),8(a,1,1))]. given #37 (F,wt=11): 100 f(f(x,f(y,z)),f(z,x)) = x. [para(8(a,1),10(a,1,2,1))]. given #38 (F,wt=10): 314 f(x,f(y,f(x,y))) = x'. [para(100(a,1),26(a,1,2)),rewrite(6(1)),flip(a)]. given #39 (T,wt=10): 316 f(x,f(y,f(y,x))) = x'. [para(1(a,1),314(a,1,2,2))]. given #40 (T,wt=11): 171 f(f(x,y),f(f(z,x),y)) = y. [para(1(a,1),22(a,1,2))]. given #41 (A,wt=19): 32 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 (F,wt=13): 44 f(x,f(f(x,y),f(y,z))) = f(x,y). [para(2(a,1),9(a,1,2)),rewrite(1(4))]. given #43 (F,wt=13): 49 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(8(a,1),9(a,1,2)),rewrite(1(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(1(4))]. given #45 (T,wt=13): 99 f(x,f(f(y,z),f(x,y))) = f(x,y). [para(10(a,1),8(a,1,2)),rewrite(1(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),2(a,1,1))]. given #47 (F,wt=12): 593 f(x,f(x',y)') = f(x,x'). [para(126(a,1),42(a,1,2,2,1)),rewrite(366(5))]. given #48 (F,wt=12): 635 f(x,f(y,x')') = f(x,x'). [para(1(a,1),593(a,1,2,1))]. given #49 (T,wt=12): 638 f(x',f(x,y)') = f(x,x'). [para(35(a,1),593(a,1,2,1,1)),rewrite(35(7),1(6))]. NOTE: New constant: f(x,x') = c_0. [new_symbol(704)]. NOTE: New Function symbol precedence: lex([ a, b, c, c_0, ', f ]). given #50 (T,wt=6): 737 f(x,x') = c_0. [new_symbol(704)]. given #51 (A,wt=17): 43 f(x,f(f(x,y),f(z,f(x,f(y,u))))) = f(x,y). [para(2(a,1),9(a,1,1))]. given #52 (F,wt=16): 799 f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(747),rewrite(748(3)),xx(a)]. given #53 (F,wt=6): 748 f(x,c_0) = x'. [back_rewrite(736),rewrite(737(2))]. given #54 (T,wt=6): 820 f(c_0,x) = x'. [para(737(a,1),8(a,1,1)),rewrite(117(4))]. given #55 (T,wt=6): 822 f(x,c_0') = c_0. [para(737(a,1),74(a,1,2,1)),rewrite(737(5))]. given #56 (A,wt=19): 47 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 #57 (F,wt=6): 884 f(c_0',x) = c_0. [para(822(a,1),1(a,1)),flip(a)]. given #58 (F,wt=9): 781 f(x',f(y,x)') = c_0. [back_rewrite(669),rewrite(737(6))]. given #59 (T,wt=9): 795 f(x',f(x,y)') = c_0. [back_rewrite(638),rewrite(737(6))]. given #60 (T,wt=9): 797 f(x,f(y,x')') = c_0. [back_rewrite(635),rewrite(737(6))]. given #61 (A,wt=17): 48 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 #62 (F,wt=9): 798 f(x,f(x',y)') = c_0. [back_rewrite(593),rewrite(737(6))]. given #63 (F,wt=10): 957 f(x,f(y,f(x,y))') = c_0. [para(314(a,1),781(a,1,2,1)),rewrite(35(5),1(4))]. given #64 (T,wt=10): 958 f(x,f(y,f(y,x))') = c_0. [para(316(a,1),781(a,1,2,1)),rewrite(35(5),1(4))]. given #65 (T,wt=12): 642 f(x,f(f(x',y)',z))' = x. [para(593(a,1),10(a,1,1)),rewrite(1(7),641(8))]. given #66 (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 #67 (F,wt=12): 653 f(x,f(y,f(x',z)'))' = x. [para(593(a,1),33(a,1,2)),rewrite(1(5),1(8),641(8))]. given #68 (F,wt=12): 667 f(x,f(f(y,x')',z))' = x. [para(635(a,1),2(a,1,1)),rewrite(641(8))]. given #69 (T,wt=12): 670 f(x,f(y,f(z,x')'))' = x. [para(635(a,1),9(a,1,1)),rewrite(641(8))]. given #70 (T,wt=12): 755 f(f(x,y)',f(x',z)') = c_0. [back_rewrite(723),rewrite(737(8))]. given #71 (A,wt=16): 55 f(x,f(f(x,y),f(f(x,y'),z))) = f(x,y). [para(14(a,1),2(a,1,1))]. given #72 (F,wt=10): 1218 f(x',y) = f(y,f(x,y)). [back_rewrite(164),rewrite(1206(5)),flip(a)]. given #73 (F,wt=10): 1278 f(x,f(y,x)) = f(x,y'). [para(1218(a,1),1(a,1))]. given #74 (T,wt=10): 1299 f(x,f(x,y)) = f(x,y'). [para(1218(a,2),12(a,1,2,2)),rewrite(1278(3),35(2),1278(4))]. given #75 (T,wt=12): 771 f(f(x,y')',f(y,z)') = c_0. [back_rewrite(694),rewrite(737(8))]. given #76 (A,wt=17): 58 f(x,f(f(x,y'),f(f(x,y),z))) = f(x,y'). [para(14(a,1),8(a,1,1))]. given #77 (F,wt=12): 784 f(x,f(y,f(x',z)')') = c_0. [back_rewrite(663),rewrite(737(2),780(6),737(8))]. given #78 (F,wt=12): 785 f(f(x',y)',f(x,z)') = c_0. [back_rewrite(662),rewrite(737(8))]. given #79 (T,wt=12): 786 f(x,f(f(x',y)',z)') = c_0. [back_rewrite(661),rewrite(737(2),780(6),737(8))]. given #80 (T,wt=12): 805 f(x,f(f(y,x')',z)') = c_0. [back_rewrite(772),rewrite(780(6))]. given #81 (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 #82 (F,wt=12): 806 f(x,f(y,f(z,x')')') = c_0. [back_rewrite(770),rewrite(780(6))]. given #83 (F,wt=12): 814 f(x',f(f(x,y)',z)') = c_0. [back_rewrite(756),rewrite(780(6))]. given #84 (T,wt=11): 1662 f(x',f(f(x,y)',z)) = x. [para(814(a,1),1299(a,1,2)),rewrite(1(3),820(3),35(2),35(6)),flip(a)]. given #85 (T,wt=11): 1663 f(x',f(f(y,x)',z)) = x. [para(1(a,1),1662(a,1,2,1,1))]. given #86 (A,wt=16): 78 f(x,f(f(y,x),f(f(x,y'),z))) = f(y,x). [para(28(a,1),2(a,1,1))]. given #87 (F,wt=11): 1664 f(x',f(y,f(x,z)')) = x. [para(1(a,1),1662(a,1,2))]. given #88 (F,wt=11): 1683 f(x',f(y,f(z,x)')) = x. [para(1(a,1),1663(a,1,2))]. given #89 (T,wt=12): 815 f(x',f(y,f(x,z)')') = c_0. [back_rewrite(754),rewrite(780(6))]. given #90 (T,wt=12): 961 f(x',f(f(y,x)',z)') = c_0. [para(781(a,1),44(a,1,2,1)),rewrite(820(6),781(10))]. given #91 (A,wt=17): 80 f(x,f(f(x,y'),f(f(y,x),z))) = f(x,y'). [para(28(a,1),8(a,1,1))]. given #92 (F,wt=12): 962 f(f(x,y)',f(y',z)') = c_0. [para(781(a,1),49(a,1,2,1)),rewrite(820(6),781(10))]. given #93 (F,wt=12): 963 f(x',f(y,f(z,x)')') = c_0. [para(781(a,1),53(a,1,2,1)),rewrite(820(6),781(10))]. given #94 (T,wt=12): 1114 f(x,f(f(x',y)',z)) = x'. [para(642(a,1),35(a,1,1)),flip(a)]. given #95 (T,wt=12): 1192 f(x,f(y,f(x',z)')) = x'. [para(653(a,1),35(a,1,1)),flip(a)]. given #96 (A,wt=16): 82 f(x,f(f(y,x),f(z,f(x,y')))) = f(y,x). [para(28(a,1),9(a,1,1))]. given #97 (F,wt=12): 1193 f(x,f(f(y,x')',z)) = x'. [para(667(a,1),35(a,1,1)),flip(a)]. given #98 (F,wt=12): 1194 f(x,f(y,f(z,x')')) = x'. [para(670(a,1),35(a,1,1)),flip(a)]. given #99 (T,wt=12): 1195 f(f(x,y)',f(z,x')') = c_0. [para(1(a,1),755(a,1,2,1))]. given #100 (T,wt=12): 1322 f(f(x,y),f(y,x)) = f(x,y)'. [para(1218(a,2),316(a,1,2,2)),rewrite(1278(4),35(3))]. given #101 (A,wt=17): 88 f(x,f(f(y',x),f(f(x,y),z))) = f(y',x). [para(31(a,1),2(a,1,1))]. given #102 (F,wt=10): 2043 f(f(x,y)',f(y,x)) = c_0. [para(1322(a,1),781(a,1,2,1)),rewrite(35(5))]. given #103 (F,wt=12): 1480 f(f(x,y')',f(z,y)') = c_0. [para(1(a,1),771(a,1,2,1))]. given #104 (T,wt=12): 1549 f(f(x',y)',f(z,x)') = c_0. [para(1(a,1),785(a,1,2,1))]. given #105 (T,wt=12): 1803 f(f(x,y)',f(z,y')') = c_0. [para(8(a,1),815(a,1,2,1,2,1))]. given #106 (A,wt=16): 89 f(x,f(f(x,y),f(f(y',x),z))) = f(x,y). [para(31(a,1),8(a,1,1))]. given #107 (F,wt=13): 175 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(8(a,1),22(a,1,2)),rewrite(1(4))]. given #108 (F,wt=13): 177 f(x,f(f(y,x),f(z,y))) = f(y,x). [para(22(a,1),9(a,1,2)),rewrite(1(4))]. given #109 (T,wt=13): 179 f(x,f(f(y,z),f(x,z))) = f(x,z). [para(9(a,1),22(a,1,2)),rewrite(1(4))]. given #110 (T,wt=13): 195 f(x,f(f(y,z),f(z,x))) = f(z,x). [para(22(a,1),22(a,1,2)),rewrite(1(4))]. given #111 (A,wt=17): 91 f(x,f(f(y',x),f(z,f(x,y)))) = f(y',x). [para(31(a,1),9(a,1,1))]. given #112 (F,wt=13): 1206 f(f(x,y)',f(x',z)) = f(x,y). [para(755(a,1),314(a,1,2,2)),rewrite(1(7),820(7),35(6),35(8))]. given #113 (F,wt=13): 1362 f(f(x,y')',f(x,f(z,y))) = c_0. [back_rewrite(1056),rewrite(1278(4),1(6))]. given #114 (T,wt=13): 1365 f(f(x,y')',f(x,f(y,z))) = c_0. [back_rewrite(1043),rewrite(1278(4),1(6))]. given #115 (T,wt=13): 1501 f(f(x,y)',f(z,x')) = f(x,y). [para(771(a,1),1278(a,1,2)),rewrite(1(4),820(4),35(3),35(7)),flip(a)]. given #116 (A,wt=17): 97 f(x,f(f(x,y),f(f(f(y,z),x),u))) = f(x,y). [para(10(a,1),2(a,1,1))]. given #117 (F,wt=13): 1666 f(f(x,y)',f(y',z)) = f(x,y). [para(8(a,1),1662(a,1,2,1,1))]. given #118 (F,wt=13): 1754 f(f(x,y)',f(z,y')) = f(x,y). [para(8(a,1),1664(a,1,2,2,1))]. given #119 (T,wt=13): 2027 f(f(x,y)',f(y,x)') = f(x,y). [para(1322(a,1),121(a,1,2))]. given #120 (T,wt=13): 2050 f(f(x,y)',f(f(y,x),z)') = c_0. [para(1322(a,1),961(a,1,2,1,1,1)),rewrite(35(5))]. given #121 (A,wt=19): 98 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 #122 (F,wt=13): 2051 f(f(x,y),f(f(y,x)',z)') = c_0. [para(1322(a,1),80(a,1,2,2,1)),rewrite(1329(5),1322(5),795(5),820(6),1329(10),1322(10),795(10))]. given #123 (F,wt=13): 2052 f(f(x,y)',f(z,f(y,x))') = c_0. [para(1322(a,1),963(a,1,2,1,2,1)),rewrite(35(5))]. given #124 (T,wt=13): 2132 f(f(x,f(y,z)')',f(z,y)) = c_0. [para(1322(a,1),1480(a,1,2,1)),rewrite(35(7))]. given #125 (T,wt=13): 2145 f(f(x,y),f(z,f(y,x)')') = c_0. [para(1322(a,1),1803(a,1,1,1)),rewrite(35(3))]. given #126 (A,wt=15): 101 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(8(a,1),10(a,1,2)),rewrite(1(3),1(4))]. given #127 (F,wt=13): 2473 f(f(x',y),f(x,z)') = f(x,z). [para(1206(a,1),1(a,1)),flip(a)]. given #128 (F,wt=13): 2498 f(f(x',y)',f(y,f(z,x))) = c_0. [para(1(a,1),1362(a,1,1,1))]. given #129 (T,wt=12): 3043 f(x',f(f(x,y),f(z,x))) = c_0. [para(117(a,1),2498(a,1,1,1))]. given #130 (T,wt=12): 3044 f(x',f(f(y,x),f(z,x))) = c_0. [para(121(a,1),2498(a,1,1,1))]. given #131 (A,wt=17): 103 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 #132 (F,wt=12): 3122 f(x',f(f(x,y),f(x,z))) = c_0. [para(1(a,1),3043(a,1,2,2))]. given #133 (F,wt=12): 3123 f(x',f(f(y,x),f(x,z))) = c_0. [para(1(a,1),3043(a,1,2))]. given #134 (T,wt=13): 2499 f(f(x,y')',f(f(z,y),x)) = c_0. [para(1(a,1),1362(a,1,2))]. given #135 (T,wt=13): 2502 f(f(x,y)',f(x,f(z,y'))) = c_0. [para(35(a,1),1362(a,1,1,1,2))]. given #136 (A,wt=16): 108 f(x,f(f(x,y),f(z,f(y',x)))) = f(x,y). [para(54(a,1),9(a,1,1))]. given #137 (F,wt=13): 2513 f(x,f(y',f(f(y,z),x))') = c_0. [para(27(a,1),1362(a,1,2)),rewrite(1(4),1(6))]. given #138 (F,wt=13): 2514 f(x,f(y',f(f(z,y),x))') = c_0. [para(33(a,1),1362(a,1,2)),rewrite(1(4),1(6))]. given #139 (T,wt=13): 2522 f(f(x,f(y,z)')',f(y,x)) = c_0. [para(49(a,1),1362(a,1,2))]. given #140 (T,wt=13): 2556 f(f(x,f(y,z)')',f(z,x)) = c_0. [para(177(a,1),1362(a,1,2))]. given #141 (A,wt=14): 123 f(x,f(f(x,y),f(x',z))) = f(x,y). [para(117(a,1),8(a,1,1))]. given #142 (F,wt=13): 2559 f(f(x',y)',f(y,f(x,z))) = c_0. [para(1(a,1),1365(a,1,1,1))]. given #143 (F,wt=13): 2560 f(f(x,y')',f(f(y,z),x)) = c_0. [para(1(a,1),1365(a,1,2))]. given #144 (T,wt=13): 2563 f(f(x,y)',f(x,f(y',z))) = c_0. [para(35(a,1),1365(a,1,1,1,2))]. given #145 (T,wt=13): 2569 f(x,f(y',f(x,f(y,z)))') = c_0. [para(21(a,1),1365(a,1,2)),rewrite(1(4),1(6))]. given #146 (A,wt=14): 125 f(x,f(f(y,x),f(x',z))) = f(y,x). [para(121(a,1),8(a,1,1))]. given #147 (F,wt=13): 2574 f(x,f(y',f(x,f(z,y)))') = c_0. [para(100(a,1),1365(a,1,2)),rewrite(1(4),1(6))]. given #148 (F,wt=13): 2588 f(f(x,y'),f(y,z)') = f(y,z). [para(1501(a,1),1(a,1)),flip(a)]. given #149 (T,wt=13): 2702 f(f(x',y),f(z,x)') = f(z,x). [para(1666(a,1),1(a,1)),flip(a)]. given #150 (T,wt=13): 2741 f(f(x,y'),f(z,y)') = f(z,y). [para(1754(a,1),1(a,1)),flip(a)]. given #151 (A,wt=21): 127 f(f(x,y),f(x,f(f(f(x,y),f(f(x,f(y,z)),u)),v))) = x. [para(11(a,1),2(a,1,1))]. given #152 (F,wt=13): 2786 f(f(x,f(y,z))',f(z,y)') = c_0. [para(2027(a,1),1480(a,1,2,1)),rewrite(35(3))]. given #153 (F,wt=13): 3027 f(f(x',y)',f(f(z,x),y)) = c_0. [para(1(a,1),2498(a,1,2))]. given #154 (T,wt=13): 3030 f(x,f(f(y,z)',f(x,y))') = c_0. [para(2(a,1),2498(a,1,2)),rewrite(1(6))]. given #155 (T,wt=13): 3032 f(x,f(f(y,z)',f(y,x))') = c_0. [para(8(a,1),2498(a,1,2)),rewrite(1(6))]. given #156 (A,wt=31): 128 f(f(x,y),f(f(f(x,y),f(f(x,f(y,z)),u)),f(x,v))) = f(f(x,y),f(f(x,f(y,z)),u)). [para(11(a,1),8(a,1,1))]. given #157 (F,wt=13): 3033 f(f(x,y)',f(y,f(z,x'))) = c_0. [para(35(a,1),2498(a,1,1,1,1))]. given #158 (F,wt=13): 3035 f(x,f(f(y,z)',f(x,z))') = c_0. [para(9(a,1),2498(a,1,2)),rewrite(1(6))]. given #159 (T,wt=13): 3040 f(f(f(x,y)',z)',f(z,x)) = c_0. [para(31(a,1),2498(a,1,2,2))]. given #160 (T,wt=13): 3045 f(f(f(x,y)',z)',f(z,y)) = c_0. [para(121(a,1),2498(a,1,2,2))]. given #161 (A,wt=21): 129 f(f(x,y),f(y,f(f(f(x,y),f(f(y,f(x,z)),u)),v))) = y. [para(8(a,1),11(a,1,2,1)),rewrite(8(13))]. given #162 (F,wt=13): 3050 f(x,f(f(y,z)',f(z,x))') = c_0. [para(22(a,1),2498(a,1,2)),rewrite(1(6))]. given #163 (F,wt=13): 3126 f(x,f(f(x',y),f(z,x'))) = c_0. [para(35(a,1),3043(a,1,1))]. given #164 (T,wt=13): 3148 f(x',f(f(x,y),f(z,x))') = x. [para(3043(a,1),1299(a,1,2)),rewrite(1(3),820(3),35(2)),flip(a)]. given #165 (T,wt=13): 3162 f(x,f(f(y,x'),f(z,x'))) = c_0. [para(35(a,1),3044(a,1,1))]. given #166 (A,wt=21): 130 f(f(x,y),f(x,f(z,f(f(x,y),f(f(x,f(y,u)),v))))) = x. [para(11(a,1),9(a,1,1))]. given #167 (F,wt=13): 3184 f(x',f(f(y,x),f(z,x))') = x. [para(3044(a,1),1299(a,1,2)),rewrite(1(3),820(3),35(2)),flip(a)]. given #168 (F,wt=13): 3294 f(x,f(f(x',y),f(x',z))) = c_0. [para(35(a,1),3122(a,1,1))]. given #169 (T,wt=13): 3313 f(x',f(f(x,y),f(x,z))') = x. [para(3122(a,1),1299(a,1,2)),rewrite(1(3),820(3),35(2)),flip(a)]. given #170 (T,wt=13): 3318 f(x,f(f(y,x'),f(x',z))) = c_0. [para(35(a,1),3123(a,1,1))]. given #171 (A,wt=15): 131 f(f(x,y),f(x,f(f(x,f(y,z)),u))) = x. [para(11(a,1),9(a,1,2)),rewrite(1(6))]. given #172 (F,wt=13): 3337 f(x',f(f(y,x),f(x,z))') = x. [para(3123(a,1),1299(a,1,2)),rewrite(1(3),820(3),35(2)),flip(a)]. given #173 (F,wt=13): 3344 f(f(x,y)',f(f(z,y'),x)) = c_0. [para(35(a,1),2499(a,1,1,1,2))]. given #174 (T,wt=13): 3440 f(x,f(y,f(f(y',z),x))') = c_0. [para(27(a,1),2502(a,1,2)),rewrite(1(4),1(6))]. given #175 (T,wt=13): 3442 f(x,f(y,f(f(z,y'),x))') = c_0. [para(33(a,1),2502(a,1,2)),rewrite(1(4),1(6))]. given #176 (A,wt=21): 132 f(f(x,y),f(x,f(f(f(x,y),f(f(x,f(z,y)),u)),v))) = x. [para(9(a,1),11(a,1,2,1)),rewrite(9(13))]. given #177 (F,wt=13): 3581 f(f(x',y)',f(f(x,z),y)) = c_0. [para(23(a,1),2513(a,1,2,1,2)),rewrite(1(6))]. given #178 (F,wt=13): 3613 f(x,f(y',f(f(y,z),x))) = x'. [para(2513(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #179 (T,wt=13): 3683 f(x,f(y',f(f(z,y),x))) = x'. [para(2514(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #180 (T,wt=13): 3806 f(f(x,y)',f(f(y',z),x)) = c_0. [para(124(a,1),2556(a,1,1,1,2,1)),rewrite(35(2))]. given #181 (A,wt=20): 134 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 #182 (F,wt=13): 3877 f(f(x,y)',f(y,f(x',z))) = c_0. [para(2473(a,1),2556(a,1,1,1))]. given #183 (F,wt=13): 4026 f(x,f(y,f(x,f(y',z)))') = c_0. [para(21(a,1),2563(a,1,2)),rewrite(1(4),1(6))]. given #184 (T,wt=13): 4039 f(x,f(y,f(x,f(z,y')))') = c_0. [para(100(a,1),2563(a,1,2)),rewrite(1(4),1(6))]. given #185 (T,wt=13): 4112 f(x,f(y',f(x,f(y,z)))) = x'. [para(2569(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #186 (A,wt=30): 135 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),28(a,1,1)),rewrite(1(8))]. given #187 (F,wt=13): 4185 f(x,f(y',f(x,f(z,y)))) = x'. [para(2574(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #188 (F,wt=13): 4387 f(f(x,y)',f(f(z,x'),y)) = c_0. [para(35(a,1),3027(a,1,1,1,1))]. given #189 (T,wt=13): 4483 f(x,f(f(y,z)',f(x,y))) = x'. [para(3030(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #190 (T,wt=13): 4562 f(x,f(f(y,z)',f(y,x))) = x'. [para(3032(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #191 (A,wt=20): 136 f(f(x,y),f(y,f(f(f(x,y),f(f(y,x'),z)),u))) = y. [para(28(a,1),11(a,1,2,1)),rewrite(28(13))]. given #192 (F,wt=13): 4837 f(x,f(f(y,z)',f(x,z))) = x'. [para(3035(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #193 (F,wt=13): 5234 f(x,f(f(y,z)',f(z,x))) = x'. [para(3050(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #194 (T,wt=13): 6010 f(x,f(y,f(f(y',z),x))) = x'. [para(3440(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #195 (T,wt=13): 6096 f(x,f(y,f(f(z,y'),x))) = x'. [para(3442(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #196 (A,wt=34): 137 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),31(a,1,1)),rewrite(1(10))]. given #197 (F,wt=13): 6776 f(x,f(y,f(x,f(y',z)))) = x'. [para(4026(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #198 (F,wt=13): 6821 f(x,f(y,f(x,f(z,y')))) = x'. [para(4039(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. given #199 (T,wt=13): 7149 f(x',y) = f(y,f(f(z,y'),x)). [back_rewrite(6095),rewrite(7125(7))]. given #200 (T,wt=13): 7150 f(x',y) = f(y,f(f(y',z),x)). [back_rewrite(6009),rewrite(7125(7))]. given #201 (A,wt=39): 139 f(f(f(x,y),z),f(x,f(f(f(x,y),z),f(f(f(x,y),f(z,u)),v)))) = f(f(f(x,y),z),f(f(f(x,y),f(z,u)),v)). [para(11(a,1),10(a,1,2)),rewrite(1(8),1(11))]. given #202 (F,wt=13): 7369 f(x,f(y,f(z,f(y,x))')') = c_0. [back_rewrite(2557),rewrite(7307(8),35(7),1(6))]. given #203 (F,wt=13): 7374 f(x,f(f(y,x'),z)') = f(x,z). [back_rewrite(7209),rewrite(7372(7))]. given #204 (T,wt=13): 7375 f(x,f(y,f(x',z))') = f(x,y). [back_rewrite(6731),rewrite(7373(7))]. given #205 (T,wt=13): 7376 f(f(x,y)',z) = f(x,f(z,y)'). [back_rewrite(5014),rewrite(7373(7),7372(5)),flip(a)]. given #206 (A,wt=23): 141 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 #207 (F,wt=13): 7378 f(x,f(y,f(z,x'))') = f(x,y). [back_rewrite(4770),rewrite(7373(7))]. given #208 (F,wt=13): 7927 f(x,f(f(x',y),z)') = f(x,z). [para(6010(a,1),91(a,1,2,2)),rewrite(1(5),1(7),1683(7),1(6)),flip(a)]. given #209 (T,wt=13): 8163 f(x,f(y,f(x',z))) = f(x,y'). [para(6776(a,1),101(a,1,2)),flip(a)]. given #210 (T,wt=13): 8236 f(x,f(y,f(z,x'))) = f(x,y'). [para(6821(a,1),101(a,1,2)),flip(a)]. given #211 (A,wt=17): 152 f(x,f(f(x,y'),f(z,f(y,x)))) = f(x,y'). [para(76(a,1),9(a,1,1))]. given #212 (F,wt=13): 8275 f(x,f(f(y,x'),z)) = f(x,z'). [para(7149(a,1),1(a,1))]. given #213 (F,wt=13): 8577 f(x,f(f(x',y),z)) = f(x,z'). [para(7150(a,1),1(a,1))]. given #214 (T,wt=13): 8969 f(x,f(y,f(f(y,x),z)')') = c_0. [para(1(a,1),7369(a,1,2,1,2,1))]. given #215 (T,wt=13): 9253 f(x,f(y,z)') = f(y,f(x,z)'). [para(7376(a,1),1(a,1))]. given #216 (A,wt=16): 159 f(x,f(f(y,x),f(f(y',x),z))) = f(y,x). [para(77(a,1),2(a,1,1))]. given #217 (F,wt=13): 9255 f(f(x,y)',z) = f(x,f(y,z)'). [para(1(a,1),7376(a,2,2,1))]. given #218 (F,wt=13): 9256 f(x,f(y,z)') = f(z,f(y,x)'). [para(1(a,1),7376(a,2)),rewrite(9255(3),9255(6))]. given #219 (T,wt=13): 9289 f(x,f(y,z)') = f(z,f(x,y)'). [para(69(a,1),7376(a,1,1,1)),rewrite(9255(3),1776(8))]. given #220 (T,wt=14): 453 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 (A,wt=17): 160 f(x,f(f(y',x),f(f(y,x),z))) = f(y',x). [para(77(a,1),8(a,1,1))]. given #222 (F,wt=14): 460 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 #223 (F,wt=14): 463 f(f(x,y'),f(x,f(f(y,x),z))) = x. [para(76(a,1),44(a,1,2,1)),rewrite(76(10))]. given #224 (T,wt=14): 488 f(f(x,y'),f(x,f(f(x,y),z))) = x. [para(14(a,1),49(a,1,2,1)),rewrite(14(10))]. given #225 (T,wt=14): 517 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 (A,wt=19): 168 f(x,f(f(f(y,x),z),f(x,f(y,u)))) = f(x,f(y,u)). [para(21(a,1),10(a,1,1))]. given #227 (F,wt=14): 524 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 #228 (F,wt=14): 527 f(f(x,y'),f(x,f(z,f(y,x)))) = x. [para(76(a,1),53(a,1,2,1)),rewrite(76(10))]. given #229 (T,wt=14): 1353 f(f(x,y),f(x',z)') = f(x',z). [para(755(a,1),1218(a,2,2)),rewrite(35(3),1(10),820(10),35(9))]. given #230 (T,wt=14): 1755 f(f(x,y),f(x,f(z,f(y,u)'))) = x. [para(1664(a,1),9(a,1,2,2)),rewrite(1(6))]. given #231 (A,wt=21): 232 f(f(x',y),f(x',f(f(f(x',y),f(x,z)),u))) = x'. [para(124(a,1),24(a,1,2,1)),rewrite(124(13))]. given #232 (F,wt=14): 1762 f(f(x,f(y,f(z,u)')),f(z,x)) = x. [para(1664(a,1),41(a,1,2,1))]. given #233 (F,wt=14): 1763 f(f(x,y),f(f(z,f(y,u)'),x)) = x. [para(1664(a,1),100(a,1,1,2))]. given #234 (T,wt=14): 1775 f(f(x,y),f(x,f(z,f(u,y)'))) = x. [para(1683(a,1),9(a,1,2,2)),rewrite(1(6))]. given #235 (T,wt=14): 1784 f(f(x,f(y,f(z,u)')),f(u,x)) = x. [para(1683(a,1),41(a,1,2,1))]. given #236 (A,wt=21): 266 f(f(x,y),f(x,f(f(f(x,y),f(f(f(z,y),x),u)),v))) = x. [para(33(a,1),24(a,1,2,1)),rewrite(33(13))]. given #237 (F,wt=14): 1785 f(f(x,y),f(f(z,f(u,y)'),x)) = x. [para(1683(a,1),100(a,1,1,2))]. given #238 (F,wt=14): 2026 f(f(x,f(y,z)),f(x,f(z,y)')) = x. [para(1322(a,1),9(a,1,2,2))]. given #239 (T,wt=14): 2034 f(f(x,f(y,z)'),f(f(z,y),x)) = x. [para(1322(a,1),100(a,1,1,2))]. given #240 (T,wt=14): 2475 f(f(x,f(y',z)),f(x,f(y,u))) = x. [para(1206(a,1),9(a,1,2,2))]. given #241 (A,wt=17): 423 f(f(x,y),f(x,f(f(f(y,z),f(x,y)),u))) = x. [para(10(a,1),32(a,1,2,1)),rewrite(10(11))]. given #242 (F,wt=14): 2481 f(f(x,f(y',z)),f(f(y,u),x)) = x. [para(1206(a,1),41(a,1,2,1))]. given #243 (F,wt=14): 2482 f(f(x,f(y,z)),f(f(y',u),x)) = x. [para(1206(a,1),100(a,1,1,2))]. given #244 (T,wt=14): 2590 f(f(x,f(y,z')),f(x,f(z,u))) = x. [para(1501(a,1),9(a,1,2,2))]. given #245 (T,wt=14): 2591 f(f(x,y),f(z,x')') = f(z,x'). [para(1501(a,1),28(a,1,1)),rewrite(35(6),1278(6))]. given #246 (A,wt=29): 498 f(f(f(x,y),f(x,z)),f(f(x,y),f(f(f(f(x,y),f(x,z)),f(y,u)),v))) = f(x,y). [para(49(a,1),24(a,1,2,1)),rewrite(49(16))]. ============================== PROOF ================================= % Proof 1 at 6.00 (+ 0.04) seconds: "Sheffer". % Length of proof is 96. % Level of proof is 30. % Maximum clause weight is 43. % Given clauses 246. 1 f(x,y) = f(y,x). [assumption]. 2 f(f(x,y),f(x,f(y,z))) = x. [assumption]. 3 f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))) # answer("Sheffer"). [assumption]. 4 f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) | f(f(a,f(b,c)),f(a,f(b,c))) != f(f(a,f(b,b)),f(a,f(c,c))) # answer("Sheffer"). [copy(3),rewrite(1(25),1(30)),flip(c)]. 5 x' = f(x,x). [assumption]. 6 f(x,x) = x'. [copy(5),flip(a)]. 7 a'' != a | f(a,f(b,b')) != a' | f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(4),rewrite(6(3),6(5),6(5),6(10),6(14),6(25),6(24),6(28)),flip(c)]. 8 f(f(x,y),f(y,f(x,z))) = y. [para(1(a,1),2(a,1,1))]. 9 f(f(x,y),f(x,f(z,y))) = x. [para(1(a,1),2(a,1,2,2))]. 10 f(f(x,y),f(f(y,z),x)) = x. [para(1(a,1),2(a,1,2))]. 12 f(x,f(x,f(x,y))) = f(x,y). [para(2(a,1),2(a,1,2)),rewrite(1(2),1(3))]. 13 f(x',f(x,f(x,y))) = x. [para(6(a,1),2(a,1,1))]. 14 f(f(x,y),f(x,y')) = x. [para(6(a,1),2(a,1,2,2))]. 16 f(x',f(x,f(y,x))) = x. [para(1(a,1),13(a,1,2,2))]. 18 f(x,f(x,x')) = x'. [para(13(a,1),2(a,1,2)),rewrite(1(2),1(3))]. 21 f(f(x,f(y,z)),f(y,x)) = x. [para(8(a,1),1(a,1)),flip(a)]. 22 f(f(x,y),f(y,f(z,x))) = y. [para(1(a,1),8(a,1,2,2))]. 24 f(x,f(f(y,x),f(f(x,f(y,z)),u))) = f(y,x). [para(8(a,1),2(a,1,1))]. 26 f(x,f(f(x,f(y,z)),f(f(x,y),u))) = f(x,f(y,z)). [para(2(a,1),8(a,1,1))]. 28 f(f(x,y),f(y,x')) = y. [para(6(a,1),8(a,1,2,2))]. 31 f(f(x',y),f(y,x)) = y. [para(13(a,1),8(a,1,2,2))]. 35 x'' = x. [para(18(a,1),2(a,1,2)),rewrite(6(1),6(3))]. 37 f(a,f(b,b')) != a' | f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(7),rewrite(35(3)),xx(a)]. 41 f(f(x,y),f(f(z,y),x)) = x. [para(1(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),2(a,1,1))]. 49 f(x,f(f(y,x),f(y,z))) = f(y,x). [para(8(a,1),9(a,1,2)),rewrite(1(4))]. 53 f(x,f(f(x,y),f(z,y))) = f(x,y). [para(9(a,1),9(a,1,2)),rewrite(1(4))]. 69 f(x,f(y,x)') = f(y,x). [para(8(a,1),16(a,1,2)),rewrite(1(3))]. 76 f(f(x,y'),f(y,x)) = x. [para(28(a,1),1(a,1)),flip(a)]. 77 f(f(x,y),f(x',y)) = y. [para(1(a,1),28(a,1,2))]. 99 f(x,f(f(y,z),f(x,y))) = f(x,y). [para(10(a,1),8(a,1,2)),rewrite(1(4))]. 100 f(f(x,f(y,z)),f(z,x)) = x. [para(8(a,1),10(a,1,2,1))]. 101 f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)). [para(8(a,1),10(a,1,2)),rewrite(1(3),1(4))]. 117 f(x',f(x,y)) = x. [para(31(a,1),69(a,1,2,1)),rewrite(1(3),31(7))]. 121 f(x',f(y,x)) = x. [para(1(a,1),117(a,1,2))]. 124 f(x,f(x',y)) = x'. [para(35(a,1),117(a,1,1))]. 126 f(x,f(y,x')) = x'. [para(121(a,1),8(a,1,2)),rewrite(1(3))]. 164 f(x,f(f(y,x)',f(y',x))) = f(y',x). [para(77(a,1),28(a,1,1)),rewrite(1(5))]. 175 f(x,f(f(y,z),f(y,x))) = f(y,x). [para(8(a,1),22(a,1,2)),rewrite(1(4))]. 314 f(x,f(y,f(x,y))) = x'. [para(100(a,1),26(a,1,2)),rewrite(6(1)),flip(a)]. 316 f(x,f(y,f(y,x))) = x'. [para(1(a,1),314(a,1,2,2))]. 330 f(x,f(f(y,x),f(y,x)')) = x'. [para(69(a,1),314(a,1,2,2)),rewrite(1(4))]. 366 f(f(x,x'),f(x',y)) = f(x',y)'. [para(124(a,1),316(a,1,2,2)),rewrite(1(5))]. 488 f(f(x,y'),f(x,f(f(x,y),z))) = x. [para(14(a,1),49(a,1,2,1)),rewrite(14(10))]. 498 f(f(f(x,y),f(x,z)),f(f(x,y),f(f(f(f(x,y),f(x,z)),f(y,u)),v))) = f(x,y). [para(49(a,1),24(a,1,2,1)),rewrite(49(16))]. 517 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(76(a,1),53(a,1,2,1)),rewrite(76(10))]. 593 f(x,f(x',y)') = f(x,x'). [para(126(a,1),42(a,1,2,2,1)),rewrite(366(5))]. 635 f(x,f(y,x')') = f(x,x'). [para(1(a,1),593(a,1,2,1))]. 638 f(x',f(x,y)') = f(x,x'). [para(35(a,1),593(a,1,2,1,1)),rewrite(35(7),1(6))]. 669 f(x',f(y,x)') = f(x,x'). [para(35(a,1),635(a,1,2,1,2)),rewrite(35(7),1(6))]. 702 f(f(x,y),f(x,y)') = f(x,x'). [para(2(a,1),638(a,1,2,1)),rewrite(1(4),638(4)),flip(a)]. 704 f(x,x') = f(y,y'). [para(8(a,1),638(a,1,2,1)),rewrite(1(4),669(4),702(6))]. 723 f(f(x,y)',f(x',z)') = f(x,x'). [para(638(a,1),49(a,1,2,1)),rewrite(366(7),638(10))]. 736 f(x,f(y,y')) = x'. [back_rewrite(330),rewrite(702(4))]. 737 f(x,x') = c_0. [new_symbol(704)]. 747 f(a,c_0) != a' | f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(37),rewrite(737(5))]. 748 f(x,c_0) = x'. [back_rewrite(736),rewrite(737(2))]. 755 f(f(x,y)',f(x',z)') = c_0. [back_rewrite(723),rewrite(737(8))]. 781 f(x',f(y,x)') = c_0. [back_rewrite(669),rewrite(737(6))]. 799 f(f(a,b'),f(a,c')) != f(a,f(b,c))' # answer("Sheffer"). [back_rewrite(747),rewrite(748(3)),xx(a)]. 820 f(c_0,x) = x'. [para(737(a,1),8(a,1,1)),rewrite(117(4))]. 957 f(x,f(y,f(x,y))') = c_0. [para(314(a,1),781(a,1,2,1)),rewrite(35(5),1(4))]. 1043 f(f(x,f(y,z)),f(x,f(y,x))') = c_0. [para(21(a,1),957(a,1,2,1,2)),rewrite(1(4))]. 1056 f(f(x,f(y,z)),f(x,f(z,x))') = c_0. [para(100(a,1),957(a,1,2,1,2)),rewrite(1(4))]. 1206 f(f(x,y)',f(x',z)) = f(x,y). [para(755(a,1),314(a,1,2,2)),rewrite(1(7),820(7),35(6),35(8))]. 1218 f(x',y) = f(y,f(x,y)). [back_rewrite(164),rewrite(1206(5)),flip(a)]. 1278 f(x,f(y,x)) = f(x,y'). [para(1218(a,1),1(a,1))]. 1290 f(f(x,y)',f(f(y,z),x)) = f(x,f(y,z)'). [para(10(a,1),1218(a,2,2)),rewrite(1(8),1278(8))]. 1299 f(x,f(x,y)) = f(x,y'). [para(1218(a,2),12(a,1,2,2)),rewrite(1278(3),35(2),1278(4))]. 1317 f(f(x,y)',f(f(z,y),x)) = f(x,f(z,y)'). [para(41(a,1),1218(a,2,2)),rewrite(1(8),1278(8))]. 1362 f(f(x,y')',f(x,f(z,y))) = c_0. [back_rewrite(1056),rewrite(1278(4),1(6))]. 1365 f(f(x,y')',f(x,f(y,z))) = c_0. [back_rewrite(1043),rewrite(1278(4),1(6))]. 2498 f(f(x',y)',f(y,f(z,x))) = c_0. [para(1(a,1),1362(a,1,1,1))]. 2563 f(f(x,y)',f(x,f(y',z))) = c_0. [para(35(a,1),1365(a,1,1,1,2))]. 3006 f(x,f(f(x,y),f(x,z))) = f(f(x,y),f(x,z))'. [para(101(a,1),175(a,1,2)),rewrite(6(7)),flip(a)]. 3030 f(x,f(f(y,z)',f(x,y))') = c_0. [para(2(a,1),2498(a,1,2)),rewrite(1(6))]. 3045 f(f(f(x,y)',z)',f(z,y)) = c_0. [para(121(a,1),2498(a,1,2,2))]. 4063 f(f(x,y),f(x,f(y',z))) = f(x,f(y',z))'. [para(2563(a,1),1278(a,1,2)),rewrite(1(5),820(5),35(10),1(9)),flip(a)]. 4483 f(x,f(f(y,z)',f(x,y))) = x'. [para(3030(a,1),1299(a,1,2)),rewrite(748(2),35(7)),flip(a)]. 5014 f(f(f(x,y)',z)',f(z,y)') = f(f(x,y)',z). [para(3045(a,1),1299(a,1,2)),rewrite(1(6),820(6),35(5)),flip(a)]. 7307 f(f(x,y)',f(z,x)) = f(f(x,y)',z'). [para(4483(a,1),101(a,1,2)),flip(a)]. 7372 f(f(x,y)',f(z,y)') = f(x,f(z,y)'). [back_rewrite(1317),rewrite(7307(5))]. 7373 f(f(x,y)',f(y,z)') = f(x,f(y,z)'). [back_rewrite(1290),rewrite(7307(5))]. 7376 f(f(x,y)',z) = f(x,f(z,y)'). [back_rewrite(5014),rewrite(7373(7),7372(5)),flip(a)]. 9255 f(f(x,y)',z) = f(x,f(y,z)'). [para(1(a,1),7376(a,2,2,1))]. 9439 f(x,f(y,f(x,z)')) = f(x,f(y,z)). [para(7376(a,1),1278(a,1,2)),rewrite(35(7))]. 9443 f(x,f(y,f(x,z))') = f(x,f(y,z')'). [para(7376(a,1),1299(a,1)),rewrite(9255(3),1(4),9439(4),9255(8))]. 11722 f(x,f(f(x,y),z)') = f(x,f(y',z)'). [para(1299(a,1),9255(a,1,1,1)),rewrite(9255(4)),flip(a)]. 12506 f(x,f(f(x,y),z)) = f(x,f(y',z)). [para(488(a,1),10(a,1,2)),rewrite(1(4),1299(4),11722(4),1(5),1299(5),35(4)),flip(a)]. 12742 f(f(x,y),f(x,z))' = f(x,f(y',f(x,z))). [back_rewrite(3006),rewrite(12506(4)),flip(a)]. 12941 f(x,f(y,f(x,z'))) = f(x,f(y,z)). [para(517(a,1),10(a,1,2)),rewrite(1(5),1299(5),9443(5),35(2),1(4),1299(4),35(3)),flip(a)]. 13081 f(x,f(y,f(x,z))) = f(x,f(y,z')). [para(527(a,1),99(a,1,2,1)),rewrite(12941(4))]. 13217 f(f(x,y),f(x,z))' = f(x,f(y',z')). [back_rewrite(12742),rewrite(13081(8))]. 14026 f(f(x,y),f(x,z)) = f(x,f(y',z'))'. [para(498(a,1),117(a,1,2)),rewrite(13217(4),1(6),4063(6)),flip(a)]. 14432 $F # answer("Sheffer"). [back_rewrite(799),rewrite(14026(9),35(4),35(5)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=246. Generated=109219. Kept=14429. proofs=1. Usable=64. Sos=2475. Demods=2789. Limbo=406, Disabled=11488. Hints=0. Weight_deleted=12. Literals_deleted=0. Forward_subsumed=94714. Back_subsumed=455. Sos_limit_deleted=63. Sos_displaced=0. Sos_removed=0. New_demodulators=14041 (1 lex), Back_demodulated=11029. Back_unit_deleted=0. Demod_attempts=1814605. Demod_rewrites=301118. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=14. Nonunit_bsub_feature_tests=4. Megabytes=8.51. User_CPU=6.00, System_CPU=0.04, Wall_clock=6. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11623 exit (max_proofs) Sat Aug 12 21:15:08 2006