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).


% th12 (trans_adds(trans_subs(se,ele),ele) = trans_adds(se,ele))).
goal elem('$min').
goal set(s).
%goal trans_adds(trans_subs(s,'$min'),'$min') = trans_adds(s,'$min') -> [].


goal S1=trans_adds(trans_subs(s,'$min'),'$min'),S2=trans_adds(s,'$min') -> in(f(S1,S2),S1),in(f(S1,S2),S2).
goal S1=trans_adds(trans_subs(s,'$min'),'$min'),S2=trans_adds(s,'$min'),in(f(S1,S2),S1),in(f(S1,S2),S2) -> [].

/*
Proof:
======

   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]
   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 + B=trans_adds(trans_subs(s,min),min),C=trans_adds(s,min) -> in(f(B,C),B),in(f(B,C),C) [axiom]
  13 + B=trans_adds(trans_subs(s,min),min),C=trans_adds(s,min),in(f(B,C),B),in(f(B,C),C) ->  [axiom]
  14 + B=trans_adds(s,min),in(f(trans_adds(trans_subs(s,min),min),B),B),in(f(trans_adds(trans_subs(s,min),min),B),trans_adds(trans_subs(s,min),min)) ->  [reflexivity resolution from 13]
  15 + B=trans_adds(s,min) -> in(f(trans_adds(trans_subs(s,min),min),B),trans_adds(trans_subs(s,min),min)),in(f(trans_adds(trans_subs(s,min),min),B),B) [reflexivity resolution from 12]
  30 + in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),trans_adds(trans_subs(s,min),min)),in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),trans_adds(s,min)) ->  [reflexivity resolution from 14]
  31 + true,in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),trans_subs(s,min)),in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),trans_adds(s,min)) ->  [negative chaining of 6 from 30]
  32 + true,in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),s),in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),trans_adds(s,min)) -> f(trans_adds(trans_subs(s,min),min),trans_adds(s,min))=min [negative chaining of 9 from 31]
  33 + in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),s) -> f(trans_adds(trans_subs(s,min),min),trans_adds(s,min))=min [reduction of 32 by [6]]
  46 + in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),trans_adds(trans_subs(s,min),min)),in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),trans_adds(s,min)) [reflexivity resolution from 15]
  48 + true -> in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),trans_adds(s,min)),in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),trans_subs(s,min)),f(trans_adds(trans_subs(s,min),min),trans_adds(s,min))=min [negative chaining of 46 from 4]
  66 + true -> f(trans_adds(trans_subs(s,min),min),trans_adds(s,min))=min,in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),trans_adds(s,min)),in(f(trans_adds(trans_subs(s,min),min),trans_adds(s,min)),s) [negative chaining of 48 from 8]
  67 + f(trans_adds(trans_subs(s,min),min),trans_adds(s,min))=min [reduction of 66 by [4,33]]
  68 + false                                   [reduction of 30 by [67,5,67,5]]


Length = 18, Depth = 8



Total time: 4010 milliseconds

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

*/