% Sheffer 1-basis: f(f(X,f(f(Y,X),X)),f(Y,f(Z,X))) = Y. % property 1 of Sheffer's 3-basis in f % ~ all(X, f(f(X,X),f(X,X)) = X). /* Proof: ====== 1 : f(f(A,f(f(B,A),A)),f(B,f(C,A)))=B [input] 2 + !A.(f(f(A,A),f(A,A))=A) -> [input] 3 + f(f(s$1,s$1),f(s$1,s$1))=s$1 -> [expansion from 2] 4 : f(f(f(A,B),f(f(f(B,f(f(C,B),B)),f(A,B)),f(A,B))),C)=f(B,f(f(C,B),B)) [chaining of 1 from 1] 8 : f(f(A,f(f(B,A),A)),f(B,f(C,f(f(A,C),C))))=B [chaining of 4 from 1] 22 : f(f(A,f(f(f(B,f(f(B,B),B)),A),A)),B)=f(B,f(f(B,B),B)) [chaining of 1 from 8] 37 : f(f(A,f(f(f(f(B,f(f(B,B),B)),f(B,f(B,f(f(B,B),B)))),A),A)),f(B,f(f(B,B),B)))=f(f(B,f(f(B,B),B)),f(f(f(B,f(f(B,B),B)),f(B,f(f(B,B),B))),f(B,f(f(B,B),B)))) [chaining of 1 from 22] 45 : f(f(A,f(f(B,A),A)),f(B,f(f(B,B),B)))=B [reduction of 37 by [8,1,8]] 60 : f(f(f(A,f(f(A,A),A)),f(A,f(A,f(f(A,A),A)))),A)=f(A,f(f(A,A),A)) [chaining of 45 from 22] 61 : f(f(A,f(f(f(f(B,f(f(B,B),B)),f(B,f(B,f(f(B,B),B)))),A),A)),f(B,f(f(B,B),B)))=f(f(B,f(f(B,B),B)),f(f(f(B,f(f(B,B),B)),f(B,f(f(B,B),B))),f(B,f(f(B,B),B)))) [chaining of 45 from 22] 70 : f(A,A)=f(A,f(f(A,A),A)) [reduction of 60 by [8]] 71 : f(f(A,f(f(f(f(B,B),f(B,f(B,B))),A),A)),f(B,B))=f(f(B,B),f(B,B)) [reduction of 61 by [70,70,70,70,70,70,70,70]] 82 : f(f(A,f(f(B,A),A)),f(B,B))=B [reduction of 45 by [70]] 91 : f(f(A,A),f(A,f(B,A)))=A [chaining of 70 from 1] 103 : A=f(f(A,A),f(A,A)) [reduction of 71 by [91,82]] 105 + false [reduction of 3 by [103,L]] Length = 16, Depth = 11 Total time: 2240 milliseconds Number of forward inferences: 64 Number of tableau inferences: 1 Number of kept clauses: 73 */ % we don't get this; AC is killing us eventually f(X,X)=g(X). f(f(g(X),X),X)=h(X). precedence([f,g,h]). % property 3 goal ~all(X,all(Y,all(Z,f(f(X,f(Y,Z)),f(X,f(Y,Z))) = f(f(f(Y,Y),X),f(f(Z,Z),X))))). :-option([term_var_weight]). % without this weight modification Saturate doesn't find the proof /* don't seem to get this one */