fof(t4_multop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ~ v1_xboole_0(D)
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,k3_zfmisc_1(A,B,C),D)
                        & m2_relset_1(E,k3_zfmisc_1(A,B,C),D) )
                     => ! [F] : 
                          ( ( v1_funct_1(F)
                            & v1_funct_2(F,k3_zfmisc_1(A,B,C),D)
                            & m2_relset_1(F,k3_zfmisc_1(A,B,C),D) )
                         => ( ! [G] : 
                                ( m1_subset_1(G,A)
                               => ! [H] : 
                                    ( m1_subset_1(H,B)
                                   => ! [I] : 
                                        ( m1_subset_1(I,C)
                                       => k2_multop_1(A,B,C,D,E,G,H,I) = k2_multop_1(A,B,C,D,F,G,H,I) ) ) )
                           => E = F ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t3_multop_1]),
    [file(multop_1,t4_multop_1),interesting(1.00)]).

fof(t8_multop_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] : 
                          ( ( v1_funct_1(F)
                            & v1_funct_2(F,k4_zfmisc_1(A,B,C,D),E)
                            & m2_relset_1(F,k4_zfmisc_1(A,B,C,D),E) )
                         => ! [G] : 
                              ( ( v1_funct_1(G)
                                & v1_funct_2(G,k4_zfmisc_1(A,B,C,D),E)
                                & m2_relset_1(G,k4_zfmisc_1(A,B,C,D),E) )
                             => ( ! [H] : 
                                    ( m1_subset_1(H,A)
                                   => ! [I] : 
                                        ( m1_subset_1(I,B)
                                       => ! [J] : 
                                            ( m1_subset_1(J,C)
                                           => ! [K] : 
                                                ( m1_subset_1(K,D)
                                               => k4_multop_1(A,B,C,D,E,F,H,I,J,K) = k4_multop_1(A,B,C,D,E,G,H,I,J,K) ) ) ) )
                               => F = G ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_multop_1]),
    [file(multop_1,t8_multop_1),interesting(0.96)]).

fof(t2_multop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B,C,D,E] : 
          ( ( v1_funct_1(E)
            & v1_funct_2(E,k3_zfmisc_1(B,C,D),A)
            & m2_relset_1(E,k3_zfmisc_1(B,C,D),A) )
         => ! [F] : 
              ( ( v1_funct_1(F)
                & v1_funct_2(F,k3_zfmisc_1(B,C,D),A)
                & m2_relset_1(F,k3_zfmisc_1(B,C,D),A) )
             => ( ! [G,H,I] : 
                    ( ( r2_hidden(G,B)
                      & r2_hidden(H,C)
                      & r2_hidden(I,D) )
                   => k1_funct_1(E,k3_mcart_1(G,H,I)) = k1_funct_1(F,k3_mcart_1(G,H,I)) )
               => E = F ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t72_mcart_1,t18_funct_2]),
    [file(multop_1,t2_multop_1),interesting(0.73)]).

fof(t3_multop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ~ v1_xboole_0(D)
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,k3_zfmisc_1(A,B,C),D)
                        & m2_relset_1(E,k3_zfmisc_1(A,B,C),D) )
                     => ! [F] : 
                          ( ( v1_funct_1(F)
                            & v1_funct_2(F,k3_zfmisc_1(A,B,C),D)
                            & m2_relset_1(F,k3_zfmisc_1(A,B,C),D) )
                         => ( ! [G] : 
                                ( m1_subset_1(G,A)
                               => ! [H] : 
                                    ( m1_subset_1(H,B)
                                   => ! [I] : 
                                        ( m1_subset_1(I,C)
                                       => k8_funct_2(k3_zfmisc_1(A,B,C),D,E,k4_domain_1(A,B,C,G,H,I)) = k8_funct_2(k3_zfmisc_1(A,B,C),D,F,k4_domain_1(A,B,C,G,H,I)) ) ) )
                           => E = F ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_multop_1]),
    [file(multop_1,t3_multop_1),interesting(0.73)]).

fof(t6_multop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B,C,D,E,F] : 
          ( ( v1_funct_1(F)
            & v1_funct_2(F,k4_zfmisc_1(B,C,D,E),A)
            & m2_relset_1(F,k4_zfmisc_1(B,C,D,E),A) )
         => ! [G] : 
              ( ( v1_funct_1(G)
                & v1_funct_2(G,k4_zfmisc_1(B,C,D,E),A)
                & m2_relset_1(G,k4_zfmisc_1(B,C,D,E),A) )
             => ( ! [H,I,J,K] : 
                    ( ( r2_hidden(H,B)
                      & r2_hidden(I,C)
                      & r2_hidden(J,D)
                      & r2_hidden(K,E) )
                   => k1_funct_1(F,k4_mcart_1(H,I,J,K)) = k1_funct_1(G,k4_mcart_1(H,I,J,K)) )
               => F = G ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t83_mcart_1,t18_funct_2]),
    [file(multop_1,t6_multop_1),interesting(0.72)]).

fof(s8_multop_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k4_zfmisc_1(f1_s8_multop_1,f1_s8_multop_1,f1_s8_multop_1,f1_s8_multop_1),f1_s8_multop_1)
      & m2_relset_1(A,k4_zfmisc_1(f1_s8_multop_1,f1_s8_multop_1,f1_s8_multop_1,f1_s8_multop_1),f1_s8_multop_1)
      & ! [B] : 
          ( m1_subset_1(B,f1_s8_multop_1)
         => ! [C] : 
              ( m1_subset_1(C,f1_s8_multop_1)
             => ! [D] : 
                  ( m1_subset_1(D,f1_s8_multop_1)
                 => ! [E] : 
                      ( m1_subset_1(E,f1_s8_multop_1)
                     => k4_multop_1(f1_s8_multop_1,f1_s8_multop_1,f1_s8_multop_1,f1_s8_multop_1,f1_s8_multop_1,A,B,C,D,E) = f2_s8_multop_1(B,C,D,E) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s7_multop_1]),
    [file(multop_1,s8_multop_1),interesting(0.71)]).

fof(t7_multop_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] : 
                          ( ( v1_funct_1(F)
                            & v1_funct_2(F,k4_zfmisc_1(A,B,C,D),E)
                            & m2_relset_1(F,k4_zfmisc_1(A,B,C,D),E) )
                         => ! [G] : 
                              ( ( v1_funct_1(G)
                                & v1_funct_2(G,k4_zfmisc_1(A,B,C,D),E)
                                & m2_relset_1(G,k4_zfmisc_1(A,B,C,D),E) )
                             => ( ! [H] : 
                                    ( m1_subset_1(H,A)
                                   => ! [I] : 
                                        ( m1_subset_1(I,B)
                                       => ! [J] : 
                                            ( m1_subset_1(J,C)
                                           => ! [K] : 
                                                ( m1_subset_1(K,D)
                                               => k8_funct_2(k4_zfmisc_1(A,B,C,D),E,F,k5_domain_1(A,B,C,D,H,I,J,K)) = k8_funct_2(k4_zfmisc_1(A,B,C,D),E,G,k5_domain_1(A,B,C,D,H,I,J,K)) ) ) ) )
                               => F = G ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t6_multop_1]),
    [file(multop_1,t7_multop_1),interesting(0.69)]).

fof(s4_multop_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k3_zfmisc_1(f1_s4_multop_1,f2_s4_multop_1,f3_s4_multop_1),f4_s4_multop_1)
      & m2_relset_1(A,k3_zfmisc_1(f1_s4_multop_1,f2_s4_multop_1,f3_s4_multop_1),f4_s4_multop_1)
      & ! [B] : 
          ( m1_subset_1(B,f1_s4_multop_1)
         => ! [C] : 
              ( m1_subset_1(C,f2_s4_multop_1)
             => ! [D] : 
                  ( m1_subset_1(D,f3_s4_multop_1)
                 => k2_multop_1(f1_s4_multop_1,f2_s4_multop_1,f3_s4_multop_1,f4_s4_multop_1,A,B,C,D) = f5_s4_multop_1(B,C,D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s3_multop_1]),
    [file(multop_1,s4_multop_1),interesting(0.60)]).

fof(s2_multop_1,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s2_multop_1)
       => ! [B] : 
            ( m1_subset_1(B,f1_s2_multop_1)
           => ! [C] : 
                ( m1_subset_1(C,f1_s2_multop_1)
               => ? [D] : 
                    ( m1_subset_1(D,f1_s2_multop_1)
                    & p1_s2_multop_1(A,B,C,D) ) ) ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & v1_funct_2(A,k3_zfmisc_1(f1_s2_multop_1,f1_s2_multop_1,f1_s2_multop_1),f1_s2_multop_1)
        & m2_relset_1(A,k3_zfmisc_1(f1_s2_multop_1,f1_s2_multop_1,f1_s2_multop_1),f1_s2_multop_1)
        & ! [B] : 
            ( m1_subset_1(B,f1_s2_multop_1)
           => ! [C] : 
                ( m1_subset_1(C,f1_s2_multop_1)
               => ! [D] : 
                    ( m1_subset_1(D,f1_s2_multop_1)
                   => p1_s2_multop_1(B,C,D,k2_multop_1(f1_s2_multop_1,f1_s2_multop_1,f1_s2_multop_1,f1_s2_multop_1,A,B,C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s1_multop_1]),
    [file(multop_1,s2_multop_1),interesting(0.53)]).

fof(s6_multop_1,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s6_multop_1)
       => ! [B] : 
            ( m1_subset_1(B,f1_s6_multop_1)
           => ! [C] : 
                ( m1_subset_1(C,f1_s6_multop_1)
               => ! [D] : 
                    ( m1_subset_1(D,f1_s6_multop_1)
                   => ? [E] : 
                        ( m1_subset_1(E,f1_s6_multop_1)
                        & p1_s6_multop_1(A,B,C,D,E) ) ) ) ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & v1_funct_2(A,k4_zfmisc_1(f1_s6_multop_1,f1_s6_multop_1,f1_s6_multop_1,f1_s6_multop_1),f1_s6_multop_1)
        & m2_relset_1(A,k4_zfmisc_1(f1_s6_multop_1,f1_s6_multop_1,f1_s6_multop_1,f1_s6_multop_1),f1_s6_multop_1)
        & ! [B] : 
            ( m1_subset_1(B,f1_s6_multop_1)
           => ! [C] : 
                ( m1_subset_1(C,f1_s6_multop_1)
               => ! [D] : 
                    ( m1_subset_1(D,f1_s6_multop_1)
                   => ! [E] : 
                        ( m1_subset_1(E,f1_s6_multop_1)
                       => p1_s6_multop_1(B,C,D,E,k4_multop_1(f1_s6_multop_1,f1_s6_multop_1,f1_s6_multop_1,f1_s6_multop_1,f1_s6_multop_1,A,B,C,D,E)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s5_multop_1]),
    [file(multop_1,s6_multop_1),interesting(0.41)]).

fof(s3_multop_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k3_zfmisc_1(f1_s3_multop_1,f2_s3_multop_1,f3_s3_multop_1),f4_s3_multop_1)
      & m2_relset_1(A,k3_zfmisc_1(f1_s3_multop_1,f2_s3_multop_1,f3_s3_multop_1),f4_s3_multop_1)
      & ! [B] : 
          ( m1_subset_1(B,f1_s3_multop_1)
         => ! [C] : 
              ( m1_subset_1(C,f2_s3_multop_1)
             => ! [D] : 
                  ( m1_subset_1(D,f3_s3_multop_1)
                 => k8_funct_2(k3_zfmisc_1(f1_s3_multop_1,f2_s3_multop_1,f3_s3_multop_1),f4_s3_multop_1,A,k4_domain_1(f1_s3_multop_1,f2_s3_multop_1,f3_s3_multop_1,B,C,D)) = f5_s3_multop_1(B,C,D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s1_multop_1]),
    [file(multop_1,s3_multop_1),interesting(0.35)]).

fof(s7_multop_1,theorem,(
    ? [A] : 
      ( v1_funct_1(A)
      & v1_funct_2(A,k4_zfmisc_1(f1_s7_multop_1,f2_s7_multop_1,f3_s7_multop_1,f4_s7_multop_1),f5_s7_multop_1)
      & m2_relset_1(A,k4_zfmisc_1(f1_s7_multop_1,f2_s7_multop_1,f3_s7_multop_1,f4_s7_multop_1),f5_s7_multop_1)
      & ! [B] : 
          ( m1_subset_1(B,f1_s7_multop_1)
         => ! [C] : 
              ( m1_subset_1(C,f2_s7_multop_1)
             => ! [D] : 
                  ( m1_subset_1(D,f3_s7_multop_1)
                 => ! [E] : 
                      ( m1_subset_1(E,f4_s7_multop_1)
                     => k8_funct_2(k4_zfmisc_1(f1_s7_multop_1,f2_s7_multop_1,f3_s7_multop_1,f4_s7_multop_1),f5_s7_multop_1,A,k5_domain_1(f1_s7_multop_1,f2_s7_multop_1,f3_s7_multop_1,f4_s7_multop_1,B,C,D,E)) = f6_s7_multop_1(B,C,D,E) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s5_multop_1]),
    [file(multop_1,s7_multop_1),interesting(0.22)]).

fof(s1_multop_1,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s1_multop_1)
       => ! [B] : 
            ( m1_subset_1(B,f2_s1_multop_1)
           => ! [C] : 
                ( m1_subset_1(C,f3_s1_multop_1)
               => ? [D] : 
                    ( m1_subset_1(D,f4_s1_multop_1)
                    & p1_s1_multop_1(A,B,C,D) ) ) ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & v1_funct_2(A,k3_zfmisc_1(f1_s1_multop_1,f2_s1_multop_1,f3_s1_multop_1),f4_s1_multop_1)
        & m2_relset_1(A,k3_zfmisc_1(f1_s1_multop_1,f2_s1_multop_1,f3_s1_multop_1),f4_s1_multop_1)
        & ! [B] : 
            ( m1_subset_1(B,f1_s1_multop_1)
           => ! [C] : 
                ( m1_subset_1(C,f2_s1_multop_1)
               => ! [D] : 
                    ( m1_subset_1(D,f3_s1_multop_1)
                   => p1_s1_multop_1(B,C,D,k8_funct_2(k3_zfmisc_1(f1_s1_multop_1,f2_s1_multop_1,f3_s1_multop_1),f4_s1_multop_1,A,k4_domain_1(f1_s1_multop_1,f2_s1_multop_1,f3_s1_multop_1,B,C,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t72_mcart_1,t28_mcart_1,s3_funct_2]),
    [file(multop_1,s1_multop_1),interesting(0.16)]).

fof(t72_mcart_1,theorem,(
    ! [A,B,C,D] : ~ ( r2_hidden(A,k3_zfmisc_1(B,C,D))
      & ! [E,F,G] : ~ ( r2_hidden(E,B)
          & r2_hidden(F,C)
          & r2_hidden(G,D)
          & A = k3_mcart_1(E,F,G) ) ) ),
    file(mcart_1,t72_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(s3_funct_2,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s3_funct_2)
       => ? [B] : 
            ( m1_subset_1(B,f2_s3_funct_2)
            & p1_s3_funct_2(A,B) ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & v1_funct_2(A,f1_s3_funct_2,f2_s3_funct_2)
        & m2_relset_1(A,f1_s3_funct_2,f2_s3_funct_2)
        & ! [B] : 
            ( m1_subset_1(B,f1_s3_funct_2)
           => p1_s3_funct_2(B,k8_funct_2(f1_s3_funct_2,f2_s3_funct_2,A,B)) ) ) ),
    file(funct_2,s3_funct_2),
    [interesting(0.00)]).

fof(t83_mcart_1,theorem,(
    ! [A,B,C,D,E] : ~ ( r2_hidden(A,k4_zfmisc_1(B,C,D,E))
      & ! [F,G,H,I] : ~ ( r2_hidden(F,B)
          & r2_hidden(G,C)
          & r2_hidden(H,D)
          & r2_hidden(I,E)
          & A = k4_mcart_1(F,G,H,I) ) ) ),
    file(mcart_1,t83_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(s5_multop_1,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s5_multop_1)
       => ! [B] : 
            ( m1_subset_1(B,f2_s5_multop_1)
           => ! [C] : 
                ( m1_subset_1(C,f3_s5_multop_1)
               => ! [D] : 
                    ( m1_subset_1(D,f4_s5_multop_1)
                   => ? [E] : 
                        ( m1_subset_1(E,f5_s5_multop_1)
                        & p1_s5_multop_1(A,B,C,D,E) ) ) ) ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & v1_funct_2(A,k4_zfmisc_1(f1_s5_multop_1,f2_s5_multop_1,f3_s5_multop_1,f4_s5_multop_1),f5_s5_multop_1)
        & m2_relset_1(A,k4_zfmisc_1(f1_s5_multop_1,f2_s5_multop_1,f3_s5_multop_1,f4_s5_multop_1),f5_s5_multop_1)
        & ! [B] : 
            ( m1_subset_1(B,f1_s5_multop_1)
           => ! [C] : 
                ( m1_subset_1(C,f2_s5_multop_1)
               => ! [D] : 
                    ( m1_subset_1(D,f3_s5_multop_1)
                   => ! [E] : 
                        ( m1_subset_1(E,f4_s5_multop_1)
                       => p1_s5_multop_1(B,C,D,E,k8_funct_2(k4_zfmisc_1(f1_s5_multop_1,f2_s5_multop_1,f3_s5_multop_1,f4_s5_multop_1),f5_s5_multop_1,A,k5_domain_1(f1_s5_multop_1,f2_s5_multop_1,f3_s5_multop_1,f4_s5_multop_1,B,C,D,E))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t83_mcart_1,t33_mcart_1,s3_funct_2]),
    [file(multop_1,s5_multop_1),interesting(0.00)]).

fof(t1_multop_1,theorem,(
    $true ),
    file(multop_1,t1_multop_1),
    [interesting(0.00)]).

fof(t18_funct_2,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,A,B)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & v1_funct_2(D,A,B)
            & m2_relset_1(D,A,B) )
         => ( ! [E] : 
                ( r2_hidden(E,A)
               => k1_funct_1(C,E) = k1_funct_1(D,E) )
           => C = D ) ) ) ),
    file(funct_2,t18_funct_2),
    [interesting(0.00)]).

fof(t5_multop_1,theorem,(
    $true ),
    file(multop_1,t5_multop_1),
    [interesting(0.00)]).