fof(t1_xboole_0,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(A,k5_xboole_0(B,C))
    <=> ~ ( r2_hidden(A,B)
        <=> r2_hidden(A,C) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xboole_0,d4_xboole_0]),
    [file(xboole_0,t1_xboole_0),interesting(1.00)]).

fof(s3_xboole_0,theorem,(
    ! [A,B] : 
      ( ( ! [C] : 
            ( r2_hidden(C,A)
          <=> p1_s3_xboole_0(C) )
        & ! [C] : 
            ( r2_hidden(C,B)
          <=> p1_s3_xboole_0(C) ) )
     => A = B ) ),
    inference(mizar_proof,[status(thm)],[s2_xboole_0]),
    [file(xboole_0,s3_xboole_0),interesting(0.93)]).

fof(s1_xboole_0,theorem,(
    ? [A] : 
    ! [B] : 
      ( r2_hidden(B,A)
    <=> ( r2_hidden(B,f1_s1_xboole_0)
        & p1_s1_xboole_0(B) ) ) ),
    inference(mizar_proof,[status(thm)],[s1_tarski]),
    [file(xboole_0,s1_xboole_0),interesting(0.89)]).

fof(t2_xboole_0,theorem,(
    ! [A,B,C] : 
      ( ! [D] : 
          ( ~ r2_hidden(D,A)
        <=> ( r2_hidden(D,B)
          <=> r2_hidden(D,C) ) )
     => A = k5_xboole_0(B,C) ) ),
    inference(mizar_proof,[status(thm)],[d4_xboole_0,d2_xboole_0,t2_tarski]),
    [file(xboole_0,t2_xboole_0),interesting(0.87)]).

fof(t3_xboole_0,theorem,(
    ! [A,B] : 
      ( ~ ( ~ r1_xboole_0(A,B)
          & ! [C] : ~ ( r2_hidden(C,A)
              & r2_hidden(C,B) ) )
      & ~ ( ? [C] : 
              ( r2_hidden(C,A)
              & r2_hidden(C,B) )
          & r1_xboole_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xboole_0,d1_xboole_0,d3_xboole_0,d3_xboole_0,d1_xboole_0,d7_xboole_0]),
    [file(xboole_0,t3_xboole_0),interesting(0.75)]).

fof(t5_xboole_0,theorem,(
    ! [A,B,C] : ~ ( r1_xboole_0(A,B)
      & r2_hidden(C,k2_xboole_0(A,B))
      & ~ ( r2_hidden(C,A)
          & ~ r2_hidden(C,B) )
      & ~ ( r2_hidden(C,B)
          & ~ r2_hidden(C,A) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xboole_0,t3_xboole_0]),
    [file(xboole_0,t5_xboole_0),interesting(0.66)]).

fof(t4_xboole_0,theorem,(
    ! [A,B] : 
      ( ~ ( ~ r1_xboole_0(A,B)
          & ! [C] : ~ r2_hidden(C,k3_xboole_0(A,B)) )
      & ~ ( ? [C] : r2_hidden(C,k3_xboole_0(A,B))
          & r1_xboole_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xboole_0,d1_xboole_0,d1_xboole_0,d7_xboole_0]),
    [file(xboole_0,t4_xboole_0),interesting(0.24)]).

fof(s1_tarski,theorem,
    ( ! [A,B,C] : 
        ( ( p1_s1_tarski(A,B)
          & p1_s1_tarski(A,C) )
       => B = C )
   => ? [A] : 
      ! [B] : 
        ( r2_hidden(B,A)
      <=> ? [C] : 
            ( r2_hidden(C,f1_s1_tarski)
            & p1_s1_tarski(C,B) ) ) ),
    file(tarski,s1_tarski),
    [interesting(0.00)]).

fof(t2_tarski,theorem,(
    ! [A,B] : 
      ( ! [C] : 
          ( r2_hidden(C,A)
        <=> r2_hidden(C,B) )
     => A = B ) ),
    file(tarski,t2_tarski),
    [interesting(0.00)]).

fof(s2_xboole_0,theorem,
    ( ( ! [A] : 
          ( r2_hidden(A,f1_s2_xboole_0)
        <=> p1_s2_xboole_0(A) )
      & ! [A] : 
          ( r2_hidden(A,f2_s2_xboole_0)
        <=> p1_s2_xboole_0(A) ) )
   => f1_s2_xboole_0 = f2_s2_xboole_0 ),
    inference(mizar_proof,[status(thm)],[t2_tarski]),
    [file(xboole_0,s2_xboole_0),interesting(0.00)]).

fof(d2_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k2_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            | r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d2_xboole_0),
    [interesting(0.00)]).

fof(d4_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k4_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            & ~ r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d4_xboole_0),
    [interesting(0.00)]).

fof(d7_xboole_0,definition,(
    ! [A,B] : 
      ( r1_xboole_0(A,B)
    <=> k3_xboole_0(A,B) = k1_xboole_0 ) ),
    file(xboole_0,d7_xboole_0),
    [interesting(0.00)]).

fof(d1_xboole_0,definition,(
    ! [A] : 
      ( A = k1_xboole_0
    <=> ! [B] : ~ r2_hidden(B,A) ) ),
    file(xboole_0,d1_xboole_0),
    [interesting(0.00)]).

fof(d3_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k3_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            & r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d3_xboole_0),
    [interesting(0.00)]).