use(hash). % th1: elem(X), set(S),in(X,S) -> trans_adds(S,X) = S. % th2 (trans_adds(trans_adds(se,ele),ele) = trans_adds(se,ele). 2 sec goal set(s). goal elem('$min'). goal trans_adds(trans_adds(s,'$min'),'$min') = trans_adds(s,'$min') -> []. /* Proof: ====== 1 : in(f(B,C),B),B=C,in(f(B,C),C) [axiom] 2 : in(f(B,C),B),in(f(B,C),C) -> B=C [axiom] 4 : in(B,trans_adds(C,D)) -> in(B,C),B=D [axiom] 5 : in(B,trans_adds(C,B)) [axiom] 6 : in(B,C) -> in(B,trans_adds(C,D)) [axiom] 13 + trans_adds(trans_adds(s,min),min)=trans_adds(s,min) -> [axiom] 29 : true -> in(f(trans_adds(B,C),D),D),trans_adds(B,C)=D,in(f(trans_adds(B,C),D),B),f(trans_adds(B,C),D)=C [negative chaining of 1 from 4] 572 : in(f(trans_adds(B,C),B),B),trans_adds(B,C)=B,f(trans_adds(B,C),B)=C [factoring on 29] 581 : true,in(f(trans_adds(B,C),B),trans_adds(B,C)) -> trans_adds(B,C)=B,f(trans_adds(B,C),B)=C,trans_adds(B,C)=B [negative chaining of 572 from 2] 584 : in(f(trans_adds(B,C),B),trans_adds(B,C)) -> f(trans_adds(B,C),B)=C,trans_adds(B,C)=B [condensement of 581] 585 : true,in(f(trans_adds(B,C),B),B) -> f(trans_adds(B,C),B)=C,trans_adds(B,C)=B [negative chaining of 6 from 584] 589 : trans_adds(B,C)=B,f(trans_adds(B,C),B)=C [reduction of 585 by [572]] 591 : in(B,C),in(f(trans_adds(C,B),C),trans_adds(C,B)) -> trans_adds(C,B)=C,trans_adds(C,B)=C [negative chaining of 589 from 2] 592 : in(B,C),in(f(trans_adds(C,B),C),trans_adds(C,B)) -> trans_adds(C,B)=C [condensement of 591] 593 : in(B,C) -> trans_adds(C,B)=C [reduction of 592 by [589,5]] 594 + trans_adds(s,min)=trans_adds(s,min),in(min,trans_adds(s,min)) -> [negative chaining of 593 from 13] 603 + false [reduction of 594 by [5]] Length = 17, Depth = 12 Total time: 33610 milliseconds Number of search inferences: 496 Number of kept clauses: 132 */