p -> eq(A,B)==all(X,(contains(A,X)<=>contains(B,X))).
p.


goal
~ all(X,all(Y,all(Z,all(U,(eq(X,Y) and eq(Y,Z) and eq(Z,U) => eq(X,U)))))).
%~ all(X,all(Y,all(Z,(eq(X,Y) and eq(Y,Z) => eq(X,Z))))).


/*
Proof:
======

   1 : eq(A,B)==!C.(contains(A,C)<=>contains(B,C))                      [input]
   2 + !A,B,C.(eq(C,B)and eq(B,A)=>eq(C,A)) ->                          [input]
   3 + !A,B,C.(!D.(contains(C,D)<=>contains(B,D)) and!E.(contains(B,E)<=>contains(A,E))=>!F.(contains(C,F)<=>contains(A,F))) ->  [reduction of 2 by [1,1,1]]
   4 + !A,B.(!C.(contains(B,C)<=>contains(A,C)) and!D.(contains(A,D)<=>contains(s$4,D))=>!E.(contains(B,E)<=>contains(s$4,E))) ->  [expansion from 3]
   5 + !A.(!B.(contains(A,B)<=>contains(s$3,B)) and!C.(contains(s$3,C)<=>contains(s$4,C))=>!D.(contains(A,D)<=>contains(s$4,D))) ->  [expansion from 4]
   6 + !A.(contains(s$2,A)<=>contains(s$3,A)) and!B.(contains(s$3,B)<=>contains(s$4,B))=>!C.(contains(s$2,C)<=>contains(s$4,C)) ->  [expansion from 5]
   7 + !A.(contains(s$2,A)<=>contains(s$3,A)) and!B.(contains(s$3,B)<=>contains(s$4,B)) [expansion from 6]
   8 + !A.(contains(s$2,A)<=>contains(s$4,A)) ->             [expansion from 6]
   9 + contains(s$2,A)==contains(s$3,A)                      [expansion from 7]
  10 + contains(s$3,A)==contains(s$4,A)                      [expansion from 7]
  11 + contains(s$2,A)==contains(s$4,A)                [reduction of 9 by [10]]
  12 + false                                       [reduction of 8 by [11,L,L]]

Length = 12, Depth = 9, Search Depth = 0



Total time: 240 milliseconds

Number of forward inferences: 0
Number of tableau inferences: 7
Number of generated clauses: 12
Number of kept clauses: 12
yes

*/