use(hash).


% th1: 
% elem(X), set(S),in(X,S) -> trans_adds(S,X) = S.	



% th2 elem(X),set(S) -> trans_subs(S,X) = S, in(X,S).
goal set(s).
goal elem('$min').
goal in('$min',s) -> [].
goal trans_subs(s,'$min') = s -> [].

/*

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]
   8 : in(B,trans_subs(C,D)) -> in(B,C)                                 [axiom]
   9 : in(B,C) -> in(B,trans_subs(C,D)),B=D                             [axiom]
  12 + in(min,s) ->                                                     [axiom]
  13 + trans_subs(s,min)=s ->                                           [axiom]
  18 : true -> in(f(trans_subs(B,C),D),D),trans_subs(B,C)=D,in(f(trans_subs(B,C),D),B) [negative chaining of 1 from 8]
  57 : in(f(trans_subs(B,C),B),B),trans_subs(B,C)=B           [factoring on 18]
  65 : true,in(f(trans_subs(B,C),B),trans_subs(B,C)) -> trans_subs(B,C)=B,trans_subs(B,C)=B [negative chaining of 57 from 2]
  68 : in(f(trans_subs(B,C),B),trans_subs(B,C)) -> trans_subs(B,C)=B [condensement of 65]
  71 : true,in(f(trans_subs(B,C),B),B) -> f(trans_subs(B,C),B)=C,trans_subs(B,C)=B [negative chaining of 9 from 68]
  74 : trans_subs(B,C)=B,f(trans_subs(B,C),B)=C       [reduction of 71 by [57]]
  75 : trans_subs(B,C)=B,in(C,B)                      [reduction of 57 by [74]]
  78 + s=s -> in(min,s)                       [negative chaining of 75 from 13]
  80 + false                                          [reduction of 78 by [12]]


Length = 15, Depth = 10



Total time: 3120 milliseconds

Number of search inferences: 55
Number of kept clauses: 47

*/