fof(t48_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => A = a_1_0_domain_1(A) ) ),
    inference(mizar_proof,[status(thm)],[s7_domain_1,t49_subset_1]),
    [file(domain_1,t48_domain_1),interesting(1.00)]).

fof(s7_domain_1,theorem,(
    m1_subset_1(a_0_0_domain_1,k1_zfmisc_1(f1_s7_domain_1)) ),
    inference(mizar_proof,[status(thm)],[s1_domain_1]),
    [file(domain_1,s7_domain_1),interesting(0.95)]).

fof(s1_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => m1_subset_1(a_1_2_domain_1(A),k1_zfmisc_1(A)) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski]),
    [file(domain_1,s1_domain_1),interesting(0.92)]).

fof(t56_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => k1_subset_1(A) = a_1_1_domain_1(A) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d10_xboole_0,d3_tarski]),
    [file(domain_1,t56_domain_1),interesting(0.89)]).

fof(t63_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => k7_subset_1(A,B,C) = a_3_6_domain_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s6_domain_1,t62_domain_1]),
    [file(domain_1,t63_domain_1),interesting(0.89)]).

fof(t64_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => k7_subset_1(A,B,C) = a_3_7_domain_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s6_domain_1,t62_domain_1]),
    [file(domain_1,t64_domain_1),interesting(0.89)]).

fof(s10_domain_1,theorem,(
    a_0_3_domain_1 = k3_xboole_0(a_0_4_domain_1,a_0_5_domain_1) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0]),
    [file(domain_1,s10_domain_1),interesting(0.85)]).

fof(t62_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => k7_subset_1(A,B,C) = a_3_5_domain_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s6_domain_1,t61_domain_1]),
    [file(domain_1,t62_domain_1),interesting(0.85)]).

fof(s8_domain_1,theorem,(
    m1_subset_1(a_0_1_domain_1,k1_zfmisc_1(f2_s8_domain_1)) ),
    inference(mizar_proof,[status(thm)],[d3_tarski]),
    [file(domain_1,s8_domain_1),interesting(0.83)]).

fof(s9_domain_1,theorem,(
    m1_subset_1(a_0_2_domain_1,k1_zfmisc_1(f3_s9_domain_1)) ),
    inference(mizar_proof,[status(thm)],[d3_tarski]),
    [file(domain_1,s9_domain_1),interesting(0.81)]).

fof(t49_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => k2_zfmisc_1(A,B) = a_2_0_domain_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t23_mcart_1,s2_domain_1,t49_subset_1]),
    [file(domain_1,t49_domain_1),interesting(0.81)]).

fof(t50_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => k3_zfmisc_1(A,B,C) = a_3_0_domain_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t48_mcart_1,s3_domain_1,t49_subset_1]),
    [file(domain_1,t50_domain_1),interesting(0.80)]).

fof(s2_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => m1_subset_1(a_2_3_domain_1(A,B),k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski]),
    [file(domain_1,s2_domain_1),interesting(0.79)]).

fof(t51_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ~ v1_xboole_0(D)
                 => k4_zfmisc_1(A,B,C,D) = a_4_0_domain_1(A,B,C,D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_mcart_1,s4_domain_1,t49_subset_1]),
    [file(domain_1,t51_domain_1),interesting(0.77)]).

fof(s3_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => m1_subset_1(a_3_8_domain_1(A,B,C),k1_zfmisc_1(k3_zfmisc_1(A,B,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski]),
    [file(domain_1,s3_domain_1),interesting(0.76)]).

fof(t52_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => B = a_2_1_domain_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d10_xboole_0,d3_tarski]),
    [file(domain_1,t52_domain_1),interesting(0.76)]).

fof(s4_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ~ v1_xboole_0(D)
                 => m1_subset_1(a_4_2_domain_1(A,B,C,D),k1_zfmisc_1(k4_zfmisc_1(A,B,C,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski]),
    [file(domain_1,s4_domain_1),interesting(0.74)]).

fof(t57_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => k3_subset_1(A,B) = a_2_2_domain_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t54_subset_1,d10_xboole_0,d3_tarski,t50_subset_1]),
    [file(domain_1,t57_domain_1),interesting(0.74)]).

fof(s6_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( ! [B] : 
            ( m1_subset_1(B,A)
           => ( p1_s6_domain_1(B)
            <=> p2_s6_domain_1(B) ) )
       => a_1_5_domain_1(A) = a_1_6_domain_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[s5_domain_1,s5_domain_1,d10_xboole_0]),
    [file(domain_1,s6_domain_1),interesting(0.74)]).

fof(t61_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => k7_subset_1(A,B,C) = a_3_4_domain_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t1_xboole_0,d10_xboole_0,d3_tarski,t1_xboole_0]),
    [file(domain_1,t61_domain_1),interesting(0.72)]).

fof(t15_domain_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ~ v1_xboole_0(D)
             => ( r2_hidden(A,k3_zfmisc_1(B,C,D))
              <=> ? [E] : 
                    ( m1_subset_1(E,B)
                    & ? [F] : 
                        ( m1_subset_1(F,C)
                        & ? [G] : 
                            ( m1_subset_1(G,D)
                            & A = k3_mcart_1(E,F,G) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_zfmisc_1,d2_zfmisc_1,d2_zfmisc_1,d3_mcart_1,d3_mcart_1,d3_zfmisc_1]),
    [file(domain_1,t15_domain_1),interesting(0.64)]).

fof(t31_domain_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ~ v1_xboole_0(D)
             => ! [E] : 
                  ( ~ v1_xboole_0(E)
                 => ( r2_hidden(A,k4_zfmisc_1(B,C,D,E))
                  <=> ? [F] : 
                        ( m1_subset_1(F,B)
                        & ? [G] : 
                            ( m1_subset_1(G,C)
                            & ? [H] : 
                                ( m1_subset_1(H,D)
                                & ? [I] : 
                                    ( m1_subset_1(I,E)
                                    & A = k4_mcart_1(F,G,H,I) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_zfmisc_1,d2_zfmisc_1,t15_domain_1,d4_mcart_1,d4_mcart_1,d4_zfmisc_1]),
    [file(domain_1,t31_domain_1),interesting(0.64)]).

fof(t53_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => ! [D] : 
                  ( m1_subset_1(D,k1_zfmisc_1(B))
                 => k12_mcart_1(A,B,C,D) = a_4_1_domain_1(A,B,C,D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t10_mcart_1,t23_mcart_1,d10_xboole_0,d3_tarski,t106_zfmisc_1]),
    [file(domain_1,t53_domain_1),interesting(0.62)]).

fof(t58_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => k5_subset_1(A,B,C) = a_3_1_domain_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0]),
    [file(domain_1,t58_domain_1),interesting(0.62)]).

fof(t59_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => k4_subset_1(A,B,C) = a_3_2_domain_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d2_xboole_0,d10_xboole_0,d3_tarski,d2_xboole_0]),
    [file(domain_1,t59_domain_1),interesting(0.62)]).

fof(t60_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => k6_subset_1(A,B,C) = a_3_3_domain_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d4_xboole_0,d10_xboole_0,d3_tarski,d4_xboole_0]),
    [file(domain_1,t60_domain_1),interesting(0.62)]).

fof(t16_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ~ v1_xboole_0(D)
                 => ( ! [E] : 
                        ( r2_hidden(E,A)
                      <=> ? [F] : 
                            ( m1_subset_1(F,B)
                            & ? [G] : 
                                ( m1_subset_1(G,C)
                                & ? [H] : 
                                    ( m1_subset_1(H,D)
                                    & E = k3_mcart_1(F,G,H) ) ) ) )
                   => A = k3_zfmisc_1(B,C,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_mcart_1,d2_zfmisc_1,d2_zfmisc_1,d3_mcart_1,t2_tarski,d3_zfmisc_1]),
    [file(domain_1,t16_domain_1),interesting(0.61)]).

fof(t32_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ~ v1_xboole_0(D)
                 => ! [E] : 
                      ( ~ v1_xboole_0(E)
                     => ( ! [F] : 
                            ( r2_hidden(F,A)
                          <=> ? [G] : 
                                ( m1_subset_1(G,B)
                                & ? [H] : 
                                    ( m1_subset_1(H,C)
                                    & ? [I] : 
                                        ( m1_subset_1(I,D)
                                        & ? [J] : 
                                            ( m1_subset_1(J,E)
                                            & F = k4_mcart_1(G,H,I,J) ) ) ) ) )
                       => A = k4_zfmisc_1(B,C,D,E) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_mcart_1,d2_zfmisc_1,t15_domain_1,d4_mcart_1,t2_tarski,d4_zfmisc_1]),
    [file(domain_1,t32_domain_1),interesting(0.61)]).

fof(t33_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ~ v1_xboole_0(D)
                 => ! [E] : 
                      ( ~ v1_xboole_0(E)
                     => ( A = k4_zfmisc_1(B,C,D,E)
                      <=> ! [F] : 
                            ( r2_hidden(F,A)
                          <=> ? [G] : 
                                ( m1_subset_1(G,B)
                                & ? [H] : 
                                    ( m1_subset_1(H,C)
                                    & ? [I] : 
                                        ( m1_subset_1(I,D)
                                        & ? [J] : 
                                            ( m1_subset_1(J,E)
                                            & F = k4_mcart_1(G,H,I,J) ) ) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t31_domain_1,t32_domain_1]),
    [file(domain_1,t33_domain_1),interesting(0.56)]).

fof(t17_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ~ v1_xboole_0(D)
                 => ( A = k3_zfmisc_1(B,C,D)
                  <=> ! [E] : 
                        ( r2_hidden(E,A)
                      <=> ? [F] : 
                            ( m1_subset_1(F,B)
                            & ? [G] : 
                                ( m1_subset_1(G,C)
                                & ? [H] : 
                                    ( m1_subset_1(H,D)
                                    & E = k3_mcart_1(F,G,H) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_domain_1,t16_domain_1]),
    [file(domain_1,t17_domain_1),interesting(0.53)]).

fof(t24_domain_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ~ v1_xboole_0(D)
             => ! [E] : 
                  ( m1_subset_1(E,k3_zfmisc_1(B,C,D))
                 => ( A = k5_mcart_1(B,C,D,E)
                  <=> ! [F] : 
                        ( m1_subset_1(F,B)
                       => ! [G] : 
                            ( m1_subset_1(G,C)
                           => ! [H] : 
                                ( m1_subset_1(H,D)
                               => ( E = k4_domain_1(B,C,D,F,G,H)
                                 => A = F ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t48_mcart_1,t28_mcart_1,t69_mcart_1]),
    [file(domain_1,t24_domain_1),interesting(0.53)]).

fof(t25_domain_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ~ v1_xboole_0(D)
             => ! [E] : 
                  ( m1_subset_1(E,k3_zfmisc_1(B,C,D))
                 => ( A = k6_mcart_1(B,C,D,E)
                  <=> ! [F] : 
                        ( m1_subset_1(F,B)
                       => ! [G] : 
                            ( m1_subset_1(G,C)
                           => ! [H] : 
                                ( m1_subset_1(H,D)
                               => ( E = k4_domain_1(B,C,D,F,G,H)
                                 => A = G ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t48_mcart_1,t28_mcart_1,t70_mcart_1]),
    [file(domain_1,t25_domain_1),interesting(0.53)]).

fof(t26_domain_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ~ v1_xboole_0(D)
             => ! [E] : 
                  ( m1_subset_1(E,k3_zfmisc_1(B,C,D))
                 => ( A = k7_mcart_1(B,C,D,E)
                  <=> ! [F] : 
                        ( m1_subset_1(F,B)
                       => ! [G] : 
                            ( m1_subset_1(G,C)
                           => ! [H] : 
                                ( m1_subset_1(H,D)
                               => ( E = k4_domain_1(B,C,D,F,G,H)
                                 => A = H ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t48_mcart_1,t28_mcart_1,t71_mcart_1]),
    [file(domain_1,t26_domain_1),interesting(0.53)]).

fof(t54_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( m1_subset_1(D,k1_zfmisc_1(A))
                 => ! [E] : 
                      ( m1_subset_1(E,k1_zfmisc_1(B))
                     => ! [F] : 
                          ( m1_subset_1(F,k1_zfmisc_1(C))
                         => k13_mcart_1(A,B,C,D,E,F) = a_6_0_domain_1(A,B,C,D,E,F) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t48_mcart_1,t76_mcart_1,d10_xboole_0,d3_tarski,t73_mcart_1]),
    [file(domain_1,t54_domain_1),interesting(0.53)]).

fof(s5_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( ! [B] : 
            ( m1_subset_1(B,A)
           => ( p1_s5_domain_1(B)
             => p2_s5_domain_1(B) ) )
       => r1_tarski(a_1_3_domain_1(A),a_1_4_domain_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski]),
    [file(domain_1,s5_domain_1),interesting(0.49)]).

fof(t9_domain_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ~ ( r2_hidden(A,k2_zfmisc_1(B,C))
              & ! [D] : 
                  ( m1_subset_1(D,B)
                 => ! [E] : 
                      ( m1_subset_1(E,C)
                     => A != k4_tarski(D,E) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_zfmisc_1]),
    [file(domain_1,t9_domain_1),interesting(0.49)]).

fof(t40_domain_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ~ v1_xboole_0(D)
             => ! [E] : 
                  ( ~ v1_xboole_0(E)
                 => ! [F] : 
                      ( m1_subset_1(F,k4_zfmisc_1(B,C,D,E))
                     => ( A = k8_mcart_1(B,C,D,E,F)
                      <=> ! [G] : 
                            ( m1_subset_1(G,B)
                           => ! [H] : 
                                ( m1_subset_1(H,C)
                               => ! [I] : 
                                    ( m1_subset_1(I,D)
                                   => ! [J] : 
                                        ( m1_subset_1(J,E)
                                       => ( F = k5_domain_1(B,C,D,E,G,H,I,J)
                                         => A = G ) ) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_mcart_1,t33_mcart_1,t79_mcart_1]),
    [file(domain_1,t40_domain_1),interesting(0.48)]).

fof(t41_domain_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ~ v1_xboole_0(D)
             => ! [E] : 
                  ( ~ v1_xboole_0(E)
                 => ! [F] : 
                      ( m1_subset_1(F,k4_zfmisc_1(B,C,D,E))
                     => ( A = k9_mcart_1(B,C,D,E,F)
                      <=> ! [G] : 
                            ( m1_subset_1(G,B)
                           => ! [H] : 
                                ( m1_subset_1(H,C)
                               => ! [I] : 
                                    ( m1_subset_1(I,D)
                                   => ! [J] : 
                                        ( m1_subset_1(J,E)
                                       => ( F = k5_domain_1(B,C,D,E,G,H,I,J)
                                         => A = H ) ) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_mcart_1,t33_mcart_1,t80_mcart_1]),
    [file(domain_1,t41_domain_1),interesting(0.48)]).

fof(t42_domain_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ~ v1_xboole_0(D)
             => ! [E] : 
                  ( ~ v1_xboole_0(E)
                 => ! [F] : 
                      ( m1_subset_1(F,k4_zfmisc_1(B,C,D,E))
                     => ( A = k10_mcart_1(B,C,D,E,F)
                      <=> ! [G] : 
                            ( m1_subset_1(G,B)
                           => ! [H] : 
                                ( m1_subset_1(H,C)
                               => ! [I] : 
                                    ( m1_subset_1(I,D)
                                   => ! [J] : 
                                        ( m1_subset_1(J,E)
                                       => ( F = k5_domain_1(B,C,D,E,G,H,I,J)
                                         => A = I ) ) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_mcart_1,t33_mcart_1,t81_mcart_1]),
    [file(domain_1,t42_domain_1),interesting(0.48)]).

fof(t43_domain_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ~ v1_xboole_0(D)
             => ! [E] : 
                  ( ~ v1_xboole_0(E)
                 => ! [F] : 
                      ( m1_subset_1(F,k4_zfmisc_1(B,C,D,E))
                     => ( A = k11_mcart_1(B,C,D,E,F)
                      <=> ! [G] : 
                            ( m1_subset_1(G,B)
                           => ! [H] : 
                                ( m1_subset_1(H,C)
                               => ! [I] : 
                                    ( m1_subset_1(I,D)
                                   => ! [J] : 
                                        ( m1_subset_1(J,E)
                                       => ( F = k5_domain_1(B,C,D,E,G,H,I,J)
                                         => A = J ) ) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_mcart_1,t33_mcart_1,t82_mcart_1]),
    [file(domain_1,t43_domain_1),interesting(0.46)]).

fof(t55_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ~ v1_xboole_0(D)
                 => ! [E] : 
                      ( m1_subset_1(E,k1_zfmisc_1(A))
                     => ! [F] : 
                          ( m1_subset_1(F,k1_zfmisc_1(B))
                         => ! [G] : 
                              ( m1_subset_1(G,k1_zfmisc_1(C))
                             => ! [H] : 
                                  ( m1_subset_1(H,k1_zfmisc_1(D))
                                 => k14_mcart_1(A,B,C,D,E,F,G,H) = a_8_0_domain_1(A,B,C,D,E,F,G,H) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t60_mcart_1,t87_mcart_1,d10_xboole_0,d3_tarski,t84_mcart_1]),
    [file(domain_1,t55_domain_1),interesting(0.45)]).

fof(t12_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,k2_zfmisc_1(A,B))
             => ! [D] : 
                  ( m1_subset_1(D,k2_zfmisc_1(A,B))
                 => ( ( k1_mcart_1(C) = k1_mcart_1(D)
                      & k2_mcart_1(C) = k2_mcart_1(D) )
                   => C = D ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t23_mcart_1]),
    [file(domain_1,t12_domain_1),interesting(0.32)]).

fof(t28_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( m1_subset_1(D,k3_zfmisc_1(A,B,C))
                 => ! [E] : 
                      ( m1_subset_1(E,k3_zfmisc_1(A,B,C))
                     => ( ( k5_mcart_1(A,B,C,D) = k5_mcart_1(A,B,C,E)
                          & k6_mcart_1(A,B,C,D) = k6_mcart_1(A,B,C,E)
                          & k7_mcart_1(A,B,C,D) = k7_mcart_1(A,B,C,E) )
                       => D = E ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t48_mcart_1]),
    [file(domain_1,t28_domain_1),interesting(0.18)]).

fof(d3_tarski,definition,(
    ! [A,B] : 
      ( r1_tarski(A,B)
    <=> ! [C] : 
          ( r2_hidden(C,A)
         => r2_hidden(C,B) ) ) ),
    file(tarski,d3_tarski),
    [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)]).

fof(d10_xboole_0,definition,(
    ! [A,B] : 
      ( A = B
    <=> ( r1_tarski(A,B)
        & r1_tarski(B,A) ) ) ),
    file(xboole_0,d10_xboole_0),
    [interesting(0.00)]).

fof(t10_domain_1,theorem,(
    $true ),
    file(domain_1,t10_domain_1),
    [interesting(0.00)]).

fof(t11_domain_1,theorem,(
    $true ),
    file(domain_1,t11_domain_1),
    [interesting(0.00)]).

fof(t23_mcart_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(A,k2_zfmisc_1(B,C))
     => A = k4_tarski(k1_mcart_1(A),k2_mcart_1(A)) ) ),
    file(mcart_1,t23_mcart_1),
    [interesting(0.00)]).

fof(t13_domain_1,theorem,(
    $true ),
    file(domain_1,t13_domain_1),
    [interesting(0.00)]).

fof(t14_domain_1,theorem,(
    $true ),
    file(domain_1,t14_domain_1),
    [interesting(0.00)]).

fof(d3_zfmisc_1,definition,(
    ! [A,B,C] : k3_zfmisc_1(A,B,C) = k2_zfmisc_1(k2_zfmisc_1(A,B),C) ),
    file(zfmisc_1,d3_zfmisc_1),
    [interesting(0.00)]).

fof(d2_zfmisc_1,definition,(
    ! [A,B,C] : 
      ( C = k2_zfmisc_1(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ? [E,F] : 
              ( r2_hidden(E,A)
              & r2_hidden(F,B)
              & D = k4_tarski(E,F) ) ) ) ),
    file(zfmisc_1,d2_zfmisc_1),
    [interesting(0.00)]).

fof(d3_mcart_1,definition,(
    ! [A,B,C] : k3_mcart_1(A,B,C) = k4_tarski(k4_tarski(A,B),C) ),
    file(mcart_1,d3_mcart_1),
    [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(t18_domain_1,theorem,(
    $true ),
    file(domain_1,t18_domain_1),
    [interesting(0.00)]).

fof(t19_domain_1,theorem,(
    $true ),
    file(domain_1,t19_domain_1),
    [interesting(0.00)]).

fof(t1_domain_1,theorem,(
    $true ),
    file(domain_1,t1_domain_1),
    [interesting(0.00)]).

fof(t20_domain_1,theorem,(
    $true ),
    file(domain_1,t20_domain_1),
    [interesting(0.00)]).

fof(t21_domain_1,theorem,(
    $true ),
    file(domain_1,t21_domain_1),
    [interesting(0.00)]).

fof(t22_domain_1,theorem,(
    $true ),
    file(domain_1,t22_domain_1),
    [interesting(0.00)]).

fof(t23_domain_1,theorem,(
    $true ),
    file(domain_1,t23_domain_1),
    [interesting(0.00)]).

fof(t48_mcart_1,theorem,(
    ! [A,B,C] : ~ ( A != k1_xboole_0
      & B != k1_xboole_0
      & C != k1_xboole_0
      & ~ ! [D] : 
            ( m1_subset_1(D,k3_zfmisc_1(A,B,C))
           => D = k3_mcart_1(k5_mcart_1(A,B,C,D),k6_mcart_1(A,B,C,D),k7_mcart_1(A,B,C,D)) ) ) ),
    file(mcart_1,t48_mcart_1),
    [interesting(0.00)]).

fof(t28_mcart_1,theorem,(
    ! [A,B,C,D,E,F] : 
      ( k3_mcart_1(A,B,C) = k3_mcart_1(D,E,F)
     => ( A = D
        & B = E
        & C = F ) ) ),
    file(mcart_1,t28_mcart_1),
    [interesting(0.00)]).

fof(t69_mcart_1,theorem,(
    ! [A,B,C,D,E] : 
      ( m1_subset_1(E,k3_zfmisc_1(A,B,C))
     => ( ! [F] : 
            ( m1_subset_1(F,A)
           => ! [G] : 
                ( m1_subset_1(G,B)
               => ! [H] : 
                    ( m1_subset_1(H,C)
                   => ( E = k3_mcart_1(F,G,H)
                     => D = F ) ) ) )
       => ( A = k1_xboole_0
          | B = k1_xboole_0
          | C = k1_xboole_0
          | D = k5_mcart_1(A,B,C,E) ) ) ) ),
    file(mcart_1,t69_mcart_1),
    [interesting(0.00)]).

fof(t70_mcart_1,theorem,(
    ! [A,B,C,D,E] : 
      ( m1_subset_1(E,k3_zfmisc_1(A,B,C))
     => ( ! [F] : 
            ( m1_subset_1(F,A)
           => ! [G] : 
                ( m1_subset_1(G,B)
               => ! [H] : 
                    ( m1_subset_1(H,C)
                   => ( E = k3_mcart_1(F,G,H)
                     => D = G ) ) ) )
       => ( A = k1_xboole_0
          | B = k1_xboole_0
          | C = k1_xboole_0
          | D = k6_mcart_1(A,B,C,E) ) ) ) ),
    file(mcart_1,t70_mcart_1),
    [interesting(0.00)]).

fof(t71_mcart_1,theorem,(
    ! [A,B,C,D,E] : 
      ( m1_subset_1(E,k3_zfmisc_1(A,B,C))
     => ( ! [F] : 
            ( m1_subset_1(F,A)
           => ! [G] : 
                ( m1_subset_1(G,B)
               => ! [H] : 
                    ( m1_subset_1(H,C)
                   => ( E = k3_mcart_1(F,G,H)
                     => D = H ) ) ) )
       => ( A = k1_xboole_0
          | B = k1_xboole_0
          | C = k1_xboole_0
          | D = k7_mcart_1(A,B,C,E) ) ) ) ),
    file(mcart_1,t71_mcart_1),
    [interesting(0.00)]).

fof(t27_domain_1,theorem,(
    $true ),
    file(domain_1,t27_domain_1),
    [interesting(0.00)]).

fof(t29_domain_1,theorem,(
    $true ),
    file(domain_1,t29_domain_1),
    [interesting(0.00)]).

fof(t2_domain_1,theorem,(
    $true ),
    file(domain_1,t2_domain_1),
    [interesting(0.00)]).

fof(t30_domain_1,theorem,(
    $true ),
    file(domain_1,t30_domain_1),
    [interesting(0.00)]).

fof(d4_zfmisc_1,definition,(
    ! [A,B,C,D] : k4_zfmisc_1(A,B,C,D) = k2_zfmisc_1(k3_zfmisc_1(A,B,C),D) ),
    file(zfmisc_1,d4_zfmisc_1),
    [interesting(0.00)]).

fof(d4_mcart_1,definition,(
    ! [A,B,C,D] : k4_mcart_1(A,B,C,D) = k4_tarski(k3_mcart_1(A,B,C),D) ),
    file(mcart_1,d4_mcart_1),
    [interesting(0.00)]).

fof(t34_domain_1,theorem,(
    $true ),
    file(domain_1,t34_domain_1),
    [interesting(0.00)]).

fof(t35_domain_1,theorem,(
    $true ),
    file(domain_1,t35_domain_1),
    [interesting(0.00)]).

fof(t36_domain_1,theorem,(
    $true ),
    file(domain_1,t36_domain_1),
    [interesting(0.00)]).

fof(t37_domain_1,theorem,(
    $true ),
    file(domain_1,t37_domain_1),
    [interesting(0.00)]).

fof(t38_domain_1,theorem,(
    $true ),
    file(domain_1,t38_domain_1),
    [interesting(0.00)]).

fof(t39_domain_1,theorem,(
    $true ),
    file(domain_1,t39_domain_1),
    [interesting(0.00)]).

fof(t3_domain_1,theorem,(
    $true ),
    file(domain_1,t3_domain_1),
    [interesting(0.00)]).

fof(t60_mcart_1,theorem,(
    ! [A,B,C,D] : ~ ( A != k1_xboole_0
      & B != k1_xboole_0
      & C != k1_xboole_0
      & D != k1_xboole_0
      & ~ ! [E] : 
            ( m1_subset_1(E,k4_zfmisc_1(A,B,C,D))
           => E = k4_mcart_1(k8_mcart_1(A,B,C,D,E),k9_mcart_1(A,B,C,D,E),k10_mcart_1(A,B,C,D,E),k11_mcart_1(A,B,C,D,E)) ) ) ),
    file(mcart_1,t60_mcart_1),
    [interesting(0.00)]).

fof(t33_mcart_1,theorem,(
    ! [A,B,C,D,E,F,G,H] : 
      ( k4_mcart_1(A,B,C,D) = k4_mcart_1(E,F,G,H)
     => ( A = E
        & B = F
        & C = G
        & D = H ) ) ),
    file(mcart_1,t33_mcart_1),
    [interesting(0.00)]).

fof(t79_mcart_1,theorem,(
    ! [A,B,C,D,E,F] : 
      ( m1_subset_1(F,k4_zfmisc_1(A,B,C,D))
     => ( ! [G] : 
            ( m1_subset_1(G,A)
           => ! [H] : 
                ( m1_subset_1(H,B)
               => ! [I] : 
                    ( m1_subset_1(I,C)
                   => ! [J] : 
                        ( m1_subset_1(J,D)
                       => ( F = k4_mcart_1(G,H,I,J)
                         => E = G ) ) ) ) )
       => ( A = k1_xboole_0
          | B = k1_xboole_0
          | C = k1_xboole_0
          | D = k1_xboole_0
          | E = k8_mcart_1(A,B,C,D,F) ) ) ) ),
    file(mcart_1,t79_mcart_1),
    [interesting(0.00)]).

fof(t80_mcart_1,theorem,(
    ! [A,B,C,D,E,F] : 
      ( m1_subset_1(F,k4_zfmisc_1(A,B,C,D))
     => ( ! [G] : 
            ( m1_subset_1(G,A)
           => ! [H] : 
                ( m1_subset_1(H,B)
               => ! [I] : 
                    ( m1_subset_1(I,C)
                   => ! [J] : 
                        ( m1_subset_1(J,D)
                       => ( F = k4_mcart_1(G,H,I,J)
                         => E = H ) ) ) ) )
       => ( A = k1_xboole_0
          | B = k1_xboole_0
          | C = k1_xboole_0
          | D = k1_xboole_0
          | E = k9_mcart_1(A,B,C,D,F) ) ) ) ),
    file(mcart_1,t80_mcart_1),
    [interesting(0.00)]).

fof(t81_mcart_1,theorem,(
    ! [A,B,C,D,E,F] : 
      ( m1_subset_1(F,k4_zfmisc_1(A,B,C,D))
     => ( ! [G] : 
            ( m1_subset_1(G,A)
           => ! [H] : 
                ( m1_subset_1(H,B)
               => ! [I] : 
                    ( m1_subset_1(I,C)
                   => ! [J] : 
                        ( m1_subset_1(J,D)
                       => ( F = k4_mcart_1(G,H,I,J)
                         => E = I ) ) ) ) )
       => ( A = k1_xboole_0
          | B = k1_xboole_0
          | C = k1_xboole_0
          | D = k1_xboole_0
          | E = k10_mcart_1(A,B,C,D,F) ) ) ) ),
    file(mcart_1,t81_mcart_1),
    [interesting(0.00)]).

fof(t82_mcart_1,theorem,(
    ! [A,B,C,D,E,F] : 
      ( m1_subset_1(F,k4_zfmisc_1(A,B,C,D))
     => ( ! [G] : 
            ( m1_subset_1(G,A)
           => ! [H] : 
                ( m1_subset_1(H,B)
               => ! [I] : 
                    ( m1_subset_1(I,C)
                   => ! [J] : 
                        ( m1_subset_1(J,D)
                       => ( F = k4_mcart_1(G,H,I,J)
                         => E = J ) ) ) ) )
       => ( A = k1_xboole_0
          | B = k1_xboole_0
          | C = k1_xboole_0
          | D = k1_xboole_0
          | E = k11_mcart_1(A,B,C,D,F) ) ) ) ),
    file(mcart_1,t82_mcart_1),
    [interesting(0.00)]).

fof(t44_domain_1,theorem,(
    $true ),
    file(domain_1,t44_domain_1),
    [interesting(0.00)]).

fof(t45_domain_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ~ v1_xboole_0(D)
                 => ! [E] : 
                      ( m1_subset_1(E,k4_zfmisc_1(A,B,C,D))
                     => ! [F] : 
                          ( m1_subset_1(F,k4_zfmisc_1(A,B,C,D))
                         => ( ( k8_mcart_1(A,B,C,D,E) = k8_mcart_1(A,B,C,D,F)
                              & k9_mcart_1(A,B,C,D,E) = k9_mcart_1(A,B,C,D,F)
                              & k10_mcart_1(A,B,C,D,E) = k10_mcart_1(A,B,C,D,F)
                              & k11_mcart_1(A,B,C,D,E) = k11_mcart_1(A,B,C,D,F) )
                           => E = F ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_mcart_1]),
    [file(domain_1,t45_domain_1),interesting(0.00)]).

fof(t46_domain_1,theorem,(
    $true ),
    file(domain_1,t46_domain_1),
    [interesting(0.00)]).

fof(t47_domain_1,theorem,(
    $true ),
    file(domain_1,t47_domain_1),
    [interesting(0.00)]).

fof(t49_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ( ! [C] : 
            ( m1_subset_1(C,A)
           => r2_hidden(C,B) )
       => A = B ) ) ),
    file(subset_1,t49_subset_1),
    [interesting(0.00)]).

fof(t4_domain_1,theorem,(
    $true ),
    file(domain_1,t4_domain_1),
    [interesting(0.00)]).

fof(t10_mcart_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(A,k2_zfmisc_1(B,C))
     => ( r2_hidden(k1_mcart_1(A),B)
        & r2_hidden(k2_mcart_1(A),C) ) ) ),
    file(mcart_1,t10_mcart_1),
    [interesting(0.00)]).

fof(t106_zfmisc_1,theorem,(
    ! [A,B,C,D] : 
      ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))
    <=> ( r2_hidden(A,C)
        & r2_hidden(B,D) ) ) ),
    file(zfmisc_1,t106_zfmisc_1),
    [interesting(0.00)]).

fof(t76_mcart_1,theorem,(
    ! [A,B,C,D] : 
      ( m1_subset_1(D,k1_zfmisc_1(A))
     => ! [E] : 
          ( m1_subset_1(E,k1_zfmisc_1(B))
         => ! [F] : 
              ( m1_subset_1(F,k1_zfmisc_1(C))
             => ! [G] : 
                  ( m1_subset_1(G,k3_zfmisc_1(A,B,C))
                 => ( r2_hidden(G,k3_zfmisc_1(D,E,F))
                   => ( r2_hidden(k5_mcart_1(A,B,C,G),D)
                      & r2_hidden(k6_mcart_1(A,B,C,G),E)
                      & r2_hidden(k7_mcart_1(A,B,C,G),F) ) ) ) ) ) ) ),
    file(mcart_1,t76_mcart_1),
    [interesting(0.00)]).

fof(t73_mcart_1,theorem,(
    ! [A,B,C,D,E,F] : 
      ( r2_hidden(k3_mcart_1(A,B,C),k3_zfmisc_1(D,E,F))
    <=> ( r2_hidden(A,D)
        & r2_hidden(B,E)
        & r2_hidden(C,F) ) ) ),
    file(mcart_1,t73_mcart_1),
    [interesting(0.00)]).

fof(t87_mcart_1,theorem,(
    ! [A,B,C,D,E] : 
      ( m1_subset_1(E,k1_zfmisc_1(A))
     => ! [F] : 
          ( m1_subset_1(F,k1_zfmisc_1(B))
         => ! [G] : 
              ( m1_subset_1(G,k1_zfmisc_1(C))
             => ! [H] : 
                  ( m1_subset_1(H,k1_zfmisc_1(D))
                 => ! [I] : 
                      ( m1_subset_1(I,k4_zfmisc_1(A,B,C,D))
                     => ( r2_hidden(I,k4_zfmisc_1(E,F,G,H))
                       => ( r2_hidden(k8_mcart_1(A,B,C,D,I),E)
                          & r2_hidden(k9_mcart_1(A,B,C,D,I),F)
                          & r2_hidden(k10_mcart_1(A,B,C,D,I),G)
                          & r2_hidden(k11_mcart_1(A,B,C,D,I),H) ) ) ) ) ) ) ) ),
    file(mcart_1,t87_mcart_1),
    [interesting(0.00)]).

fof(t84_mcart_1,theorem,(
    ! [A,B,C,D,E,F,G,H] : 
      ( r2_hidden(k4_mcart_1(A,B,C,D),k4_zfmisc_1(E,F,G,H))
    <=> ( r2_hidden(A,E)
        & r2_hidden(B,F)
        & r2_hidden(C,G)
        & r2_hidden(D,H) ) ) ),
    file(mcart_1,t84_mcart_1),
    [interesting(0.00)]).

fof(t54_subset_1,theorem,(
    ! [A,B,C] : 
      ( m1_subset_1(C,k1_zfmisc_1(A))
     => ~ ( r2_hidden(B,k3_subset_1(A,C))
          & r2_hidden(B,C) ) ) ),
    file(subset_1,t54_subset_1),
    [interesting(0.00)]).

fof(t50_subset_1,theorem,(
    ! [A] : 
      ( A != k1_xboole_0
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(A))
         => ! [C] : 
              ( m1_subset_1(C,A)
             => ( ~ r2_hidden(C,B)
               => r2_hidden(C,k3_subset_1(A,B)) ) ) ) ) ),
    file(subset_1,t50_subset_1),
    [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(t5_domain_1,theorem,(
    $true ),
    file(domain_1,t5_domain_1),
    [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(t1_xboole_0,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(A,k5_xboole_0(B,C))
    <=> ~ ( r2_hidden(A,B)
        <=> r2_hidden(A,C) ) ) ),
    file(xboole_0,t1_xboole_0),
    [interesting(0.00)]).

fof(t6_domain_1,theorem,(
    $true ),
    file(domain_1,t6_domain_1),
    [interesting(0.00)]).

fof(t7_domain_1,theorem,(
    $true ),
    file(domain_1,t7_domain_1),
    [interesting(0.00)]).

fof(t8_domain_1,theorem,(
    $true ),
    file(domain_1,t8_domain_1),
    [interesting(0.00)]).