fof(t1_extens_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( r1_tarski(B,C)
         => k9_relat_1(k7_relat_1(A,C),B) = k9_relat_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t161_relat_1,d10_xboole_0,d3_tarski,d13_relat_1,d11_relat_1,d13_relat_1]),
    [file(extens_1,t1_extens_1),interesting(1.00)]).

fof(t13_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m3_pboole(D,A,B,C)
             => ( v2_msualg_3(D,A,B,C)
              <=> r6_pboole(A,k2_extens_1(A,D),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_pboole,d18_pboole,d3_msualg_3,t31_funct_6,t3_pboole,d3_msualg_3,t31_funct_6]),
    [file(extens_1,t13_extens_1),interesting(0.94)]).

fof(t16_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( ( v2_relat_1(C)
            & m1_pboole(C,A) )
         => ! [D] : 
              ( m3_pboole(D,A,B,C)
             => ( v2_msualg_3(D,A,B,C)
              <=> ! [E] : 
                    ( ( v2_relat_1(E)
                      & m1_pboole(E,A) )
                   => ! [F] : 
                        ( m3_pboole(F,A,C,E)
                       => ! [G] : 
                            ( m3_pboole(G,A,C,E)
                           => ( r6_pboole(A,k3_msualg_3(A,B,C,E,D,F),k3_msualg_3(A,B,C,E,D,G))
                             => r6_pboole(A,F,G) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_pboole,d18_pboole,d18_pboole,d18_pboole,d3_msualg_3,t2_msualg_3,t2_msualg_3,t22_funct_2,t3_pboole,d3_msualg_3,d16_pboole,t22_funct_2,s4_pboole,s4_pboole,s4_pboole,d16_pboole,d1_cqc_lang,d1_cqc_lang,d16_pboole,d6_funcop_1,d3_pboole,d1_cqc_lang,d1_cqc_lang,d18_pboole,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,d18_pboole,l1_extens_1,d1_cqc_lang,d1_cqc_lang,t2_msualg_3,t2_msualg_3,d1_cqc_lang,d1_cqc_lang,d18_pboole,d18_pboole,d18_pboole,t2_msualg_3,t2_msualg_3,t3_pboole,d1_cqc_lang,d1_cqc_lang]),
    [file(extens_1,t16_extens_1),interesting(0.87)]).

fof(l1_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m1_pboole(D,A)
             => ! [E] : 
                  ( m3_pboole(E,A,B,C)
                 => ! [F] : 
                      ( m3_pboole(F,A,C,D)
                     => m1_pboole(k13_pboole(E,F),A) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d24_pboole,d3_pboole,d3_pboole,d3_pboole]),
    [file(extens_1,l1_extens_1),interesting(0.84)]).

fof(t17_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( ( v2_relat_1(C)
            & m1_pboole(C,A) )
         => ! [D] : 
              ( m3_pboole(D,A,B,C)
             => ( ( v2_relat_1(B)
                  & v2_relat_1(C) )
               => ( v1_msualg_3(D)
                <=> ! [E] : 
                      ( m1_pboole(E,A)
                     => ! [F] : 
                          ( m3_pboole(F,A,E,B)
                         => ! [G] : 
                              ( m3_pboole(G,A,E,B)
                             => ( k13_pboole(F,D) = k13_pboole(G,D)
                               => r6_pboole(A,F,G) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_pboole,d18_pboole,d18_pboole,d18_pboole,t1_msualg_3,t2_msualg_3,t2_msualg_3,t27_funct_2,t3_pboole,t1_msualg_3,d16_pboole,d18_pboole,t27_funct_2,s4_pboole,s4_pboole,s4_pboole,d6_funcop_1,d3_pboole,d1_cqc_lang,d1_cqc_lang,d18_pboole,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,d18_pboole,l1_extens_1,d1_cqc_lang,d1_cqc_lang,t2_msualg_3,t2_msualg_3,d1_cqc_lang,d1_cqc_lang,d18_pboole,d18_pboole,d18_pboole,t2_msualg_3,t2_msualg_3,t3_pboole,d1_cqc_lang,d1_cqc_lang]),
    [file(extens_1,t17_extens_1),interesting(0.83)]).

fof(t5_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( ( v2_relat_1(C)
            & m1_pboole(C,A) )
         => ! [D] : 
              ( m3_pboole(D,A,B,C)
             => ! [E] : 
                  ( m4_pboole(E,A,B)
                 => ( r2_pboole(A,B,E)
                   => r6_pboole(A,k1_msafree(A,B,C,E,D),D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_pboole,d5_pboole,d1_msafree,t40_funct_2,t3_pboole]),
    [file(extens_1,t5_extens_1),interesting(0.83)]).

fof(t9_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ( r1_pzfmisc1(A,B,C)
           => ! [D] : 
                ( m3_pboole(D,A,B,C)
               => ! [E] : 
                    ( m1_pboole(E,A)
                   => ( m4_pboole(C,A,E)
                     => m3_pboole(D,A,B,E) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_pboole,d23_pboole,d5_pboole,d3_pzfmisc1,d18_pboole,t9_funct_2]),
    [file(extens_1,t9_extens_1),interesting(0.80)]).

fof(t11_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( ( v2_relat_1(C)
            & m1_pboole(C,A) )
         => ! [D] : 
              ( m3_pboole(D,A,B,C)
             => ! [E] : 
                  ( m4_pboole(E,A,B)
                 => r2_pboole(A,k1_extens_1(A,k1_msafree(A,B,C,E,D)),k1_extens_1(A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_pboole,d18_pboole,d3_pboole,t31_funct_6,d1_msafree,d3_pboole,t31_funct_6,t76_funct_1]),
    [file(extens_1,t11_extens_1),interesting(0.79)]).

fof(t12_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( ( v2_relat_1(C)
            & m1_pboole(C,A) )
         => ! [D] : 
              ( m3_pboole(D,A,B,C)
             => ! [E] : 
                  ( m4_pboole(E,A,B)
                 => r2_pboole(A,k2_extens_1(A,k1_msafree(A,B,C,E,D)),k2_extens_1(A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_pboole,d18_pboole,d3_pboole,t31_funct_6,d1_msafree,d3_pboole,t31_funct_6,t76_funct_1]),
    [file(extens_1,t12_extens_1),interesting(0.79)]).

fof(t7_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( ( v2_relat_1(C)
            & m1_pboole(C,A) )
         => ! [D] : 
              ( m3_pboole(D,A,B,C)
             => ! [E] : 
                  ( m4_pboole(E,A,B)
                 => ! [F] : 
                      ( m4_pboole(F,A,B)
                     => ( r2_pboole(A,E,F)
                       => r6_pboole(A,k14_pboole(A,E,k1_msafree(A,B,C,F,D)),k14_pboole(A,E,D)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_pboole,d18_pboole,d5_pboole,d1_msafree,d25_pboole,t1_extens_1,d25_pboole,t3_pboole]),
    [file(extens_1,t7_extens_1),interesting(0.79)]).

fof(t6_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m4_pboole(D,A,B)
             => ! [E] : 
                  ( m3_pboole(E,A,B,C)
                 => r2_pboole(A,k14_pboole(A,D,E),k14_pboole(A,B,E)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_pboole,d3_tarski,d18_pboole,d25_pboole,d23_pboole,d5_pboole,t156_relat_1,d25_pboole]),
    [file(extens_1,t6_extens_1),interesting(0.77)]).

fof(t14_extens_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v2_relat_1(B)
            & m1_pboole(B,u1_struct_0(A)) )
         => r6_pboole(u1_struct_0(A),k2_extens_1(u1_struct_0(A),k15_msafree(A,B)),B) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_pboole,d18_pboole,d3_tarski,t31_funct_6,t12_relset_1,d10_xboole_0,d3_tarski,t7_msafree,d20_msafree,d1_funct_2,t7_mcart_1,t14_msafree,d5_funct_1,d19_msafree,t7_mcart_1,t31_funct_6,t3_pboole]),
    [file(extens_1,t14_extens_1),interesting(0.75)]).

fof(t8_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( ( v2_relat_1(C)
            & m1_pboole(C,A) )
         => ! [D] : 
              ( ( v2_relat_1(D)
                & m1_pboole(D,A) )
             => ! [E] : 
                  ( m3_pboole(E,A,B,C)
                 => ! [F] : 
                      ( m3_pboole(F,A,C,D)
                     => ! [G] : 
                          ( m4_pboole(G,A,B)
                         => r6_pboole(A,k1_msafree(A,B,D,G,k3_msualg_3(A,B,C,D,E,F)),k3_msualg_3(A,G,C,D,k1_msafree(A,B,C,G,E),F)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_pboole,d18_pboole,d18_pboole,d18_pboole,d1_msafree,t2_msualg_3,t112_relat_1,d1_msafree,t2_msualg_3,t3_pboole]),
    [file(extens_1,t8_extens_1),interesting(0.75)]).

fof(t10_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( ( v2_relat_1(C)
            & m1_pboole(C,A) )
         => ! [D] : 
              ( m3_pboole(D,A,B,C)
             => ! [E] : 
                  ( m4_pboole(E,A,B)
                 => ( v1_msualg_3(D)
                   => v1_msualg_3(k1_msafree(A,B,C,E,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_pboole,t1_msualg_3,t84_funct_1,d1_msafree,t1_msualg_3]),
    [file(extens_1,t10_extens_1),interesting(0.72)]).

fof(t15_extens_1,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( ( v2_relat_1(C)
            & m1_pboole(C,A) )
         => ! [D] : 
              ( ( v2_relat_1(D)
                & m1_pboole(D,A) )
             => ! [E] : 
                  ( m3_pboole(E,A,B,C)
                 => ! [F] : 
                      ( m3_pboole(F,A,C,D)
                     => ! [G] : 
                          ( ( v2_relat_1(G)
                            & m4_pboole(G,A,C) )
                         => ( r2_pboole(A,k2_extens_1(A,E),G)
                           => k13_pboole(E,k1_msafree(A,C,D,G,F)) = k3_msualg_3(A,B,C,D,E,F) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_pboole,d18_pboole,d18_pboole,d16_pboole,d16_pboole,d1_funct_2,t31_funct_6,d5_pboole,d1_funct_2,t11_relset_1,l1_extens_1,d16_pboole,d18_pboole,t31_funct_6,d5_pboole,d16_pboole,d1_funct_2,d1_funct_2,t11_relset_1,d18_pboole,d18_pboole,t12_relset_1,t2_msualg_3,d1_msafree,t1_msuhom_1,t2_msualg_3,t3_pboole]),
    [file(extens_1,t15_extens_1),interesting(0.67)]).

fof(t20_extens_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v5_msualg_1(B,A)
            & l3_msualg_1(B,A) )
         => ! [C] : 
              ( ( v5_msualg_1(C,A)
                & l3_msualg_1(C,A) )
             => ! [D] : 
                  ( m3_pboole(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                 => ( r1_msualg_3(A,B,C,D)
                   => ( r3_msualg_3(A,B,C,D)
                    <=> ! [E] : 
                          ( ( v5_msualg_1(E,A)
                            & l3_msualg_1(E,A) )
                         => ! [F] : 
                              ( m3_pboole(F,u1_struct_0(A),u4_msualg_1(A,E),u4_msualg_1(A,B))
                             => ! [G] : 
                                  ( m3_pboole(G,u1_struct_0(A),u4_msualg_1(A,E),u4_msualg_1(A,B))
                                 => ( ( r1_msualg_3(A,E,B,F)
                                      & r1_msualg_3(A,E,B,G)
                                      & r6_pboole(u1_struct_0(A),k3_msualg_3(u1_struct_0(A),u4_msualg_1(A,E),u4_msualg_1(A,B),u4_msualg_1(A,C),F,D),k3_msualg_3(u1_struct_0(A),u4_msualg_1(A,E),u4_msualg_1(A,B),u4_msualg_1(A,C),G,D)) )
                                   => r6_pboole(u1_struct_0(A),F,G) ) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_msualg_3,t17_extens_1,d11_msualg_3,t1_msualg_3,d18_pboole,d16_pboole,t25_funct_2,t17_msafree,t15_msafree,d16_pboole,t57_funcop_1,t13_funcop_1,t57_funcop_1,t13_funcop_1,s4_pboole,s4_pboole,d6_funcop_1,d3_pboole,d1_cqc_lang,d1_cqc_lang,d18_pboole,d1_cqc_lang,d1_cqc_lang,d18_pboole,d5_msafree,d5_msafree,d1_cqc_lang,d1_cqc_lang,d18_pboole,t19_funct_2,t19_funct_2,t21_funct_2,t21_funct_2,t18_funct_2,t2_msualg_3,t2_msualg_3,d1_cqc_lang,d1_cqc_lang,d18_pboole,d18_pboole,t2_msualg_3,t2_msualg_3,t3_pboole,t8_extens_1,t8_extens_1,t10_msualg_3,t18_extens_1,d1_cqc_lang,d1_cqc_lang]),
    [file(extens_1,t20_extens_1),interesting(0.41)]).

fof(t21_extens_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( m4_pboole(C,u1_struct_0(A),u4_msualg_1(A,B))
             => ! [D] : 
                  ( m4_pboole(D,u1_struct_0(A),u4_msualg_1(A,B))
                 => ( m4_pboole(C,u1_struct_0(A),D)
                   => m1_msualg_2(k12_msualg_2(A,B,C),A,k12_msualg_2(A,B,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d23_pboole,d18_msualg_2,d23_pboole,t15_pboole,d23_pboole,d18_msualg_2]),
    [file(extens_1,t21_extens_1),interesting(0.41)]).

fof(t22_extens_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( m1_msualg_2(C,A,B)
             => ! [D] : 
                  ( m4_pboole(D,u1_struct_0(A),u4_msualg_1(A,B))
                 => ! [E] : 
                      ( m4_pboole(E,u1_struct_0(A),u4_msualg_1(A,C))
                     => ( r6_pboole(u1_struct_0(A),D,E)
                       => k12_msualg_2(A,B,D) = k12_msualg_2(A,C,E) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_msualg_2,d18_msualg_2,d18_msualg_2,d18_msualg_2,d18_msualg_2,d18_msualg_2,t8_msualg_2]),
    [file(extens_1,t22_extens_1),interesting(0.40)]).

fof(t23_extens_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v4_msualg_1(B,A)
            & v5_msualg_1(B,A)
            & l3_msualg_1(B,A) )
         => ! [C] : 
              ( ( v5_msualg_1(C,A)
                & l3_msualg_1(C,A) )
             => ! [D] : 
                  ( m1_msafree(D,A,B)
                 => ! [E] : 
                      ( m3_pboole(E,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                     => ! [F] : 
                          ( m3_pboole(F,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                         => ( ( r1_msualg_3(A,B,C,E)
                              & r1_msualg_3(A,B,C,F)
                              & r6_pboole(u1_struct_0(A),k1_msafree(u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C),D,E),k1_msafree(u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C),D,F)) )
                           => r6_pboole(u1_struct_0(A),E,F) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s2_pboole,d5_pboole,d23_pboole,d3_tarski,d7_msualg_2,d6_msualg_2,d3_tarski,d5_funct_1,t86_relat_1,t21_funct_2,d6_msualg_1,d19_pboole,t72_funct_1,d10_msualg_1,t21_funct_2,d7_msualg_1,t6_msualg_3,t6_msualg_3,t6_msualg_3,t18_card_3,t18_card_3,t23_funct_1,d4_finseq_4,d8_msualg_3,d8_msualg_3,t72_funct_1,d9_msualg_3,t9_funct_1,d9_msualg_3,t72_funct_1,d7_msualg_1,t21_funct_2,d16_msualg_2,d5_pboole,d23_pboole,d3_tarski,d23_pboole,d5_pboole,t72_funct_1,d1_msafree,d1_msafree,t72_funct_1,d18_msualg_2,d4_msafree,d10_msualg_2,d23_pboole,d1_funct_2,d1_funct_2,d5_pboole,t9_funct_1,t3_pboole]),
    [file(extens_1,t23_extens_1),interesting(0.11)]).

fof(t19_extens_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v5_msualg_1(B,A)
            & l3_msualg_1(B,A) )
         => ! [C] : 
              ( ( v5_msualg_1(C,A)
                & l3_msualg_1(C,A) )
             => ! [D] : 
                  ( m3_pboole(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                 => ( ( r1_msualg_3(A,B,C,D)
                      & r2_msualg_3(A,B,C,D) )
                   => ! [E] : 
                        ( ( v5_msualg_1(E,A)
                          & l3_msualg_1(E,A) )
                       => ! [F] : 
                            ( m3_pboole(F,u1_struct_0(A),u4_msualg_1(A,C),u4_msualg_1(A,E))
                           => ! [G] : 
                                ( m3_pboole(G,u1_struct_0(A),u4_msualg_1(A,C),u4_msualg_1(A,E))
                               => ( ( r1_msualg_3(A,C,E,F)
                                    & r1_msualg_3(A,C,E,G)
                                    & r6_pboole(u1_struct_0(A),k3_msualg_3(u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C),u4_msualg_1(A,E),D,F),k3_msualg_3(u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C),u4_msualg_1(A,E),D,G)) )
                                 => r6_pboole(u1_struct_0(A),F,G) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_msualg_3,t16_extens_1]),
    [file(extens_1,t19_extens_1),interesting(0.09)]).

fof(d18_pboole,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m1_pboole(D,A)
             => ( m3_pboole(D,A,B,C)
              <=> ! [E] : 
                    ( r2_hidden(E,A)
                   => ( v1_funct_1(k1_funct_1(D,E))
                      & v1_funct_2(k1_funct_1(D,E),k1_funct_1(B,E),k1_funct_1(C,E))
                      & m2_relset_1(k1_funct_1(D,E),k1_funct_1(B,E),k1_funct_1(C,E)) ) ) ) ) ) ) ),
    file(pboole,d18_pboole),
    [interesting(0.00)]).

fof(t1_msualg_3,theorem,(
    ! [A,B] : 
      ( ( v1_funcop_1(B)
        & m1_pboole(B,A) )
     => ( v1_msualg_3(B)
      <=> ! [C] : 
            ( r2_hidden(C,A)
           => v2_funct_1(k1_funct_1(B,C)) ) ) ) ),
    file(msualg_3,t1_msualg_3),
    [interesting(0.00)]).

fof(t84_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( v2_funct_1(B)
       => v2_funct_1(k7_relat_1(B,A)) ) ) ),
    file(funct_1,t84_funct_1),
    [interesting(0.00)]).

fof(d1_msafree,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m4_pboole(D,A,B)
             => ! [E] : 
                  ( m3_pboole(E,A,B,C)
                 => ! [F] : 
                      ( m3_pboole(F,A,D,C)
                     => ( F = k1_msafree(A,B,C,D,E)
                      <=> ! [G] : 
                            ( r2_hidden(G,A)
                           => ! [H] : 
                                ( ( v1_funct_1(H)
                                  & v1_funct_2(H,k1_funct_1(B,G),k1_funct_1(C,G))
                                  & m2_relset_1(H,k1_funct_1(B,G),k1_funct_1(C,G)) )
                               => ( H = k1_funct_1(E,G)
                                 => k1_funct_1(F,G) = k8_relset_1(k1_funct_1(B,G),k1_funct_1(C,G),H,k1_funct_1(D,G)) ) ) ) ) ) ) ) ) ) ),
    file(msafree,d1_msafree),
    [interesting(0.00)]).

fof(d5_pboole,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ( r2_pboole(A,B,C)
          <=> ! [D] : 
                ( r2_hidden(D,A)
               => r1_tarski(k1_funct_1(B,D),k1_funct_1(C,D)) ) ) ) ) ),
    file(pboole,d5_pboole),
    [interesting(0.00)]).

fof(d3_pboole,definition,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( m1_pboole(B,A)
      <=> k1_relat_1(B) = A ) ) ),
    file(pboole,d3_pboole),
    [interesting(0.00)]).

fof(t31_funct_6,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( ( r2_hidden(A,k1_relat_1(B))
              & C = k1_funct_1(B,A) )
           => ( r2_hidden(A,k1_relat_1(k2_funct_6(B)))
              & k1_funct_1(k2_funct_6(B),A) = k1_relat_1(C)
              & r2_hidden(A,k1_relat_1(k3_funct_6(B)))
              & k1_funct_1(k3_funct_6(B),A) = k2_relat_1(C) ) ) ) ) ),
    file(funct_6,t31_funct_6),
    [interesting(0.00)]).

fof(t76_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( r1_tarski(k1_relat_1(k7_relat_1(B,A)),k1_relat_1(B))
        & r1_tarski(k2_relat_1(k7_relat_1(B,A)),k2_relat_1(B)) ) ) ),
    file(funct_1,t76_funct_1),
    [interesting(0.00)]).

fof(d3_msualg_3,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m3_pboole(D,A,B,C)
             => ( v2_msualg_3(D,A,B,C)
              <=> ! [E] : 
                    ( r2_hidden(E,A)
                   => k2_relat_1(k1_funct_1(D,E)) = k1_funct_1(C,E) ) ) ) ) ) ),
    file(msualg_3,d3_msualg_3),
    [interesting(0.00)]).

fof(t3_pboole,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ( ! [D] : 
                ( r2_hidden(D,A)
               => k1_funct_1(B,D) = k1_funct_1(C,D) )
           => B = C ) ) ) ),
    file(pboole,t3_pboole),
    [interesting(0.00)]).

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(t12_relset_1,theorem,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => ( r1_tarski(k1_relat_1(C),A)
        & r1_tarski(k2_relat_1(C),B) ) ) ),
    file(relset_1,t12_relset_1),
    [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(t7_msafree,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v2_relat_1(B)
            & m1_pboole(B,u1_struct_0(A)) )
         => ! [C] : 
              ( r2_hidden(C,k6_dtconstr(k5_msafree(A,B)))
            <=> ? [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                  & ? [E] : 
                      ( r2_hidden(E,k1_funct_1(B,D))
                      & C = k4_tarski(E,D) ) ) ) ) ) ),
    file(msafree,t7_msafree),
    [interesting(0.00)]).

fof(d20_msafree,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v2_relat_1(B)
            & m1_pboole(B,u1_struct_0(A)) )
         => ! [C] : 
              ( m3_pboole(C,u1_struct_0(A),k13_msafree(A,B),B)
             => ( C = k15_msafree(A,B)
              <=> ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k1_msualg_3(u1_struct_0(A),k13_msafree(A,B),B,C,D) = k14_msafree(A,B,D) ) ) ) ) ) ),
    file(msafree,d20_msafree),
    [interesting(0.00)]).

fof(d1_funct_2,definition,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => ( ( ( B = k1_xboole_0
           => A = k1_xboole_0 )
         => ( v1_funct_2(C,A,B)
          <=> A = k4_relset_1(A,B,C) ) )
        & ( B = k1_xboole_0
         => ( A = k1_xboole_0
            | ( v1_funct_2(C,A,B)
            <=> C = k1_xboole_0 ) ) ) ) ) ),
    file(funct_2,d1_funct_2),
    [interesting(0.00)]).

fof(t7_mcart_1,theorem,(
    ! [A,B] : 
      ( k1_mcart_1(k4_tarski(A,B)) = A
      & k2_mcart_1(k4_tarski(A,B)) = B ) ),
    file(mcart_1,t7_mcart_1),
    [interesting(0.00)]).

fof(t14_msafree,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v2_relat_1(B)
            & m1_pboole(B,u1_struct_0(A)) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k12_msafree(A,B,C) = a_3_1_msafree(A,B,C) ) ) ) ),
    file(msafree,t14_msafree),
    [interesting(0.00)]).

fof(d5_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( B = k2_relat_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : 
                  ( r2_hidden(D,k1_relat_1(A))
                  & C = k1_funct_1(A,D) ) ) ) ) ),
    file(funct_1,d5_funct_1),
    [interesting(0.00)]).

fof(d19_msafree,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v2_relat_1(B)
            & m1_pboole(B,u1_struct_0(A)) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k12_msafree(A,B,C),k1_funct_1(B,C))
                    & m2_relset_1(D,k12_msafree(A,B,C),k1_funct_1(B,C)) )
                 => ( D = k14_msafree(A,B,C)
                  <=> ! [E] : 
                        ( m1_subset_1(E,u1_struct_0(k5_msafree(A,B)))
                       => ( r2_hidden(k2_trees_4(u1_struct_0(k5_msafree(A,B)),E),k12_msafree(A,B,C))
                         => k1_funct_1(D,k2_trees_4(u1_struct_0(k5_msafree(A,B)),E)) = k1_mcart_1(E) ) ) ) ) ) ) ) ),
    file(msafree,d19_msafree),
    [interesting(0.00)]).

fof(d16_pboole,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ( v2_relat_1(B)
      <=> ! [C] : ~ ( r2_hidden(C,A)
            & v1_xboole_0(k1_funct_1(B,C)) ) ) ) ),
    file(pboole,d16_pboole),
    [interesting(0.00)]).

fof(t11_relset_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( ( r1_tarski(k1_relat_1(C),A)
          & r1_tarski(k2_relat_1(C),B) )
       => m2_relset_1(C,A,B) ) ) ),
    file(relset_1,t11_relset_1),
    [interesting(0.00)]).

fof(d24_pboole,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_funcop_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_funcop_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_funcop_1(C) )
             => ( C = k13_pboole(A,B)
              <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B))
                  & ! [D] : 
                      ( r2_hidden(D,k1_relat_1(C))
                     => k1_funct_1(C,D) = k5_relat_1(k1_funct_1(A,D),k1_funct_1(B,D)) ) ) ) ) ) ) ),
    file(pboole,d24_pboole),
    [interesting(0.00)]).

fof(t2_msualg_3,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m1_pboole(D,A)
             => ! [E] : 
                  ( m3_pboole(E,A,B,C)
                 => ! [F] : 
                      ( m3_pboole(F,A,C,D)
                     => ( k1_relat_1(k13_pboole(E,F)) = A
                        & ! [G] : 
                            ( r2_hidden(G,A)
                           => k1_funct_1(k13_pboole(E,F),G) = k5_relat_1(k1_funct_1(E,G),k1_funct_1(F,G)) ) ) ) ) ) ) ) ),
    file(msualg_3,t2_msualg_3),
    [interesting(0.00)]).

fof(t1_msuhom_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ! [C] : 
              ( r1_tarski(k2_relat_1(A),C)
             => k5_relat_1(A,k7_relat_1(B,C)) = k5_relat_1(A,B) ) ) ) ),
    file(msuhom_1,t1_msuhom_1),
    [interesting(0.00)]).

fof(d10_msualg_3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ! [D] : 
                  ( m3_pboole(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                 => ( r2_msualg_3(A,B,C,D)
                  <=> ( r1_msualg_3(A,B,C,D)
                      & v2_msualg_3(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C)) ) ) ) ) ) ) ),
    file(msualg_3,d10_msualg_3),
    [interesting(0.00)]).

fof(t22_funct_2,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,A,B)
        & m2_relset_1(C,A,B) )
     => ( B != k1_xboole_0
       => ( k2_relat_1(C) = B
        <=> ! [D] : 
              ( D != k1_xboole_0
             => ! [E] : 
                  ( ( v1_funct_1(E)
                    & v1_funct_2(E,B,D)
                    & m2_relset_1(E,B,D) )
                 => ! [F] : 
                      ( ( v1_funct_1(F)
                        & v1_funct_2(F,B,D)
                        & m2_relset_1(F,B,D) )
                     => ( k1_partfun1(A,B,B,D,C,E) = k1_partfun1(A,B,B,D,C,F)
                       => E = F ) ) ) ) ) ) ) ),
    file(funct_2,t22_funct_2),
    [interesting(0.00)]).

fof(s4_pboole,theorem,(
    ? [A] : 
      ( m1_pboole(A,f1_s4_pboole)
      & ! [B] : 
          ( r2_hidden(B,f1_s4_pboole)
         => k1_funct_1(A,B) = f2_s4_pboole(B) ) ) ),
    file(pboole,s4_pboole),
    [interesting(0.00)]).

fof(d1_cqc_lang,definition,(
    ! [A,B,C,D] : 
      ( ( A = B
       => k1_cqc_lang(A,B,C,D) = C )
      & ( A != B
       => k1_cqc_lang(A,B,C,D) = D ) ) ),
    file(cqc_lang,d1_cqc_lang),
    [interesting(0.00)]).

fof(d6_funcop_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v1_funcop_1(A)
      <=> ! [B] : 
            ( r2_hidden(B,k1_relat_1(A))
           => ( v1_relat_1(k1_funct_1(A,B))
              & v1_funct_1(k1_funct_1(A,B)) ) ) ) ) ),
    file(funcop_1,d6_funcop_1),
    [interesting(0.00)]).

fof(d11_msualg_3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ! [D] : 
                  ( m3_pboole(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                 => ( r3_msualg_3(A,B,C,D)
                  <=> ( r1_msualg_3(A,B,C,D)
                      & v1_msualg_3(D) ) ) ) ) ) ) ),
    file(msualg_3,d11_msualg_3),
    [interesting(0.00)]).

fof(t27_funct_2,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,A,B)
        & m2_relset_1(C,A,B) )
     => ~ ( A != k1_xboole_0
          & B != k1_xboole_0
          & ~ ( v2_funct_1(C)
            <=> ! [D,E] : 
                  ( ( v1_funct_1(E)
                    & v1_funct_2(E,D,A)
                    & m2_relset_1(E,D,A) )
                 => ! [F] : 
                      ( ( v1_funct_1(F)
                        & v1_funct_2(F,D,A)
                        & m2_relset_1(F,D,A) )
                     => ( k1_partfun1(D,A,A,B,E,C) = k1_partfun1(D,A,A,B,F,C)
                       => E = F ) ) ) ) ) ) ),
    file(funct_2,t27_funct_2),
    [interesting(0.00)]).

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

fof(t17_msafree,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v2_relat_1(B)
            & m1_pboole(B,u1_struct_0(A)) )
         => v1_msafree(k13_msafree(A,B),A,k11_msafree(A,B)) ) ) ),
    file(msafree,t17_msafree),
    [interesting(0.00)]).

fof(t15_msafree,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v2_relat_1(B)
            & m1_pboole(B,u1_struct_0(A)) )
         => v2_relat_1(k13_msafree(A,B)) ) ) ),
    file(msafree,t15_msafree),
    [interesting(0.00)]).

fof(t57_funcop_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(C,B)
     => ( v1_funct_1(k2_funcop_1(A,C))
        & v1_funct_2(k2_funcop_1(A,C),A,B)
        & m2_relset_1(k2_funcop_1(A,C),A,B) ) ) ),
    file(funcop_1,t57_funcop_1),
    [interesting(0.00)]).

fof(t13_funcop_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(B,A)
     => k1_funct_1(k2_funcop_1(A,C),B) = C ) ),
    file(funcop_1,t13_funcop_1),
    [interesting(0.00)]).

fof(d5_msafree,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( m1_msafree(C,A,B)
             => ( v1_msafree(C,A,B)
              <=> ! [D] : 
                    ( ( v5_msualg_1(D,A)
                      & l3_msualg_1(D,A) )
                   => ! [E] : 
                        ( m3_pboole(E,u1_struct_0(A),C,u4_msualg_1(A,D))
                       => ? [F] : 
                            ( m3_pboole(F,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,D))
                            & r1_msualg_3(A,B,D,F)
                            & r6_pboole(u1_struct_0(A),k1_msafree(u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,D),C,F),E) ) ) ) ) ) ) ) ),
    file(msafree,d5_msafree),
    [interesting(0.00)]).

fof(t19_funct_2,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & v1_funct_2(D,A,B)
        & m2_relset_1(D,A,B) )
     => ! [E] : 
          ( ( v1_funct_1(E)
            & v1_funct_2(E,B,C)
            & m2_relset_1(E,B,C) )
         => ( ~ ( B = k1_xboole_0
                & C != k1_xboole_0
                & A != k1_xboole_0 )
           => ( v1_funct_1(k1_partfun1(A,B,B,C,D,E))
              & v1_funct_2(k1_partfun1(A,B,B,C,D,E),A,C)
              & m2_relset_1(k1_partfun1(A,B,B,C,D,E),A,C) ) ) ) ) ),
    file(funct_2,t19_funct_2),
    [interesting(0.00)]).

fof(t21_funct_2,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & v1_funct_2(D,A,B)
        & m2_relset_1(D,A,B) )
     => ! [E] : 
          ( ( v1_relat_1(E)
            & v1_funct_1(E) )
         => ( r2_hidden(C,A)
           => ( B = k1_xboole_0
              | k1_funct_1(k5_relat_1(D,E),C) = k1_funct_1(E,k1_funct_1(D,C)) ) ) ) ) ),
    file(funct_2,t21_funct_2),
    [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(t112_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ! [C] : 
          ( v1_relat_1(C)
         => k7_relat_1(k5_relat_1(B,C),A) = k5_relat_1(k7_relat_1(B,A),C) ) ) ),
    file(relat_1,t112_relat_1),
    [interesting(0.00)]).

fof(t10_msualg_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v5_msualg_1(B,A)
            & l3_msualg_1(B,A) )
         => ! [C] : 
              ( ( v5_msualg_1(C,A)
                & l3_msualg_1(C,A) )
             => ! [D] : 
                  ( ( v5_msualg_1(D,A)
                    & l3_msualg_1(D,A) )
                 => ! [E] : 
                      ( m3_pboole(E,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                     => ! [F] : 
                          ( m3_pboole(F,u1_struct_0(A),u4_msualg_1(A,C),u4_msualg_1(A,D))
                         => ( ( r1_msualg_3(A,B,C,E)
                              & r1_msualg_3(A,C,D,F) )
                           => r1_msualg_3(A,B,D,k3_msualg_3(u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C),u4_msualg_1(A,D),E,F)) ) ) ) ) ) ) ) ),
    file(msualg_3,t10_msualg_3),
    [interesting(0.00)]).

fof(d18_msafree,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v2_relat_1(B)
            & m1_pboole(B,u1_struct_0(A)) )
         => ! [C] : 
              ( m1_msafree(C,A,k11_msafree(A,B))
             => ( C = k13_msafree(A,B)
              <=> ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k1_funct_1(C,D) = k12_msafree(A,B,D) ) ) ) ) ) ),
    file(msafree,d18_msafree),
    [interesting(0.00)]).

fof(t72_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(B,A)
       => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ),
    file(funct_1,t72_funct_1),
    [interesting(0.00)]).

fof(s3_msafree1,theorem,
    ( ( r1_msualg_3(f1_s3_msafree1,k11_msafree(f1_s3_msafree1,f2_s3_msafree1),f3_s3_msafree1,f4_s3_msafree1)
      & ! [A] : 
          ( m1_subset_1(A,u1_struct_0(f1_s3_msafree1))
         => ! [B,C] : 
              ( r2_hidden(C,k12_msafree(f1_s3_msafree1,f2_s3_msafree1,A))
             => ( k1_funct_1(k1_msualg_3(u1_struct_0(f1_s3_msafree1),u4_msualg_1(f1_s3_msafree1,k11_msafree(f1_s3_msafree1,f2_s3_msafree1)),u4_msualg_1(f1_s3_msafree1,f3_s3_msafree1),f4_s3_msafree1,A),C) = B
              <=> p1_s3_msafree1(A,B,C) ) ) )
      & r1_msualg_3(f1_s3_msafree1,k11_msafree(f1_s3_msafree1,f2_s3_msafree1),f3_s3_msafree1,f5_s3_msafree1)
      & ! [A] : 
          ( m1_subset_1(A,u1_struct_0(f1_s3_msafree1))
         => ! [B,C] : 
              ( r2_hidden(C,k12_msafree(f1_s3_msafree1,f2_s3_msafree1,A))
             => ( k1_funct_1(k1_msualg_3(u1_struct_0(f1_s3_msafree1),u4_msualg_1(f1_s3_msafree1,k11_msafree(f1_s3_msafree1,f2_s3_msafree1)),u4_msualg_1(f1_s3_msafree1,f3_s3_msafree1),f5_s3_msafree1,A),C) = B
              <=> p1_s3_msafree1(A,B,C) ) ) ) )
   => r6_pboole(u1_struct_0(f1_s3_msafree1),f4_s3_msafree1,f5_s3_msafree1) ),
    file(msafree1,s3_msafree1),
    [interesting(0.00)]).

fof(t18_extens_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v5_msualg_1(B,A)
            & l3_msualg_1(B,A) )
         => ! [C] : 
              ( ( v2_relat_1(C)
                & m1_pboole(C,u1_struct_0(A)) )
             => ! [D] : 
                  ( m3_pboole(D,u1_struct_0(A),u4_msualg_1(A,k11_msafree(A,C)),u4_msualg_1(A,B))
                 => ! [E] : 
                      ( m3_pboole(E,u1_struct_0(A),u4_msualg_1(A,k11_msafree(A,C)),u4_msualg_1(A,B))
                     => ( ( r1_msualg_3(A,k11_msafree(A,C),B,D)
                          & r1_msualg_3(A,k11_msafree(A,C),B,E)
                          & r6_pboole(u1_struct_0(A),k1_msafree(u1_struct_0(A),u4_msualg_1(A,k11_msafree(A,C)),u4_msualg_1(A,B),k13_msafree(A,C),D),k1_msafree(u1_struct_0(A),u4_msualg_1(A,k11_msafree(A,C)),u4_msualg_1(A,B),k13_msafree(A,C),E)) )
                       => r6_pboole(u1_struct_0(A),D,E) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_msafree,d18_msafree,t72_funct_1,s3_msafree1]),
    [file(extens_1,t18_extens_1),interesting(0.00)]).

fof(d23_pboole,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ( m4_pboole(C,A,B)
          <=> r2_pboole(A,C,B) ) ) ) ),
    file(pboole,d23_pboole),
    [interesting(0.00)]).

fof(d18_msualg_2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( m4_pboole(C,u1_struct_0(A),u4_msualg_1(A,B))
             => ! [D] : 
                  ( ( v4_msualg_1(D,A)
                    & m1_msualg_2(D,A,B) )
                 => ( D = k12_msualg_2(A,B,C)
                  <=> ( m4_pboole(C,u1_struct_0(A),u4_msualg_1(A,D))
                      & ! [E] : 
                          ( m1_msualg_2(E,A,B)
                         => ( m4_pboole(C,u1_struct_0(A),u4_msualg_1(A,E))
                           => m1_msualg_2(D,A,E) ) ) ) ) ) ) ) ) ),
    file(msualg_2,d18_msualg_2),
    [interesting(0.00)]).

fof(t15_pboole,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m1_pboole(D,A)
             => ( ( r2_pboole(A,B,C)
                  & r2_pboole(A,C,D) )
               => r2_pboole(A,B,D) ) ) ) ) ),
    file(pboole,t15_pboole),
    [interesting(0.00)]).

fof(t7_msualg_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ! [D] : 
                  ( l3_msualg_1(D,A)
                 => ( ( m1_msualg_2(B,A,C)
                      & m1_msualg_2(C,A,D) )
                   => m1_msualg_2(B,A,D) ) ) ) ) ) ),
    file(msualg_2,t7_msualg_2),
    [interesting(0.00)]).

fof(t8_msualg_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ( ( v4_msualg_1(B,A)
                  & m1_msualg_2(B,A,C)
                  & v4_msualg_1(C,A)
                  & m1_msualg_2(C,A,B) )
               => B = C ) ) ) ) ),
    file(msualg_2,t8_msualg_2),
    [interesting(0.00)]).

fof(s2_pboole,theorem,(
    ? [A] : 
      ( m1_pboole(A,f1_s2_pboole)
      & ! [B] : 
          ( r2_hidden(B,f1_s2_pboole)
         => ! [C] : 
              ( r2_hidden(C,k1_funct_1(A,B))
            <=> ( r2_hidden(C,k1_funct_1(f2_s2_pboole,B))
                & p1_s2_pboole(B,C) ) ) ) ) ),
    file(pboole,s2_pboole),
    [interesting(0.00)]).

fof(d7_msualg_2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( m4_pboole(C,u1_struct_0(A),u4_msualg_1(A,B))
             => ( v3_msualg_2(C,A,B)
              <=> ! [D] : 
                    ( m1_subset_1(D,u1_msualg_1(A))
                   => r1_msualg_2(A,B,D,C) ) ) ) ) ) ),
    file(msualg_2,d7_msualg_2),
    [interesting(0.00)]).

fof(d6_msualg_2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( m1_subset_1(C,u1_msualg_1(A))
             => ! [D] : 
                  ( m4_pboole(D,u1_struct_0(A),u4_msualg_1(A,B))
                 => ( r1_msualg_2(A,B,C,D)
                  <=> r1_tarski(k2_relat_1(k7_relat_1(k5_msualg_1(A,C,B),k1_funct_1(k7_pboole(u1_msualg_1(A),k3_finseq_2(u1_struct_0(A)),u2_msualg_1(A),k6_pboole(u1_struct_0(A),D)),C))),k1_funct_1(k7_pboole(u1_msualg_1(A),u1_struct_0(A),u3_msualg_1(A),D),C)) ) ) ) ) ) ),
    file(msualg_2,d6_msualg_2),
    [interesting(0.00)]).

fof(t86_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( r2_hidden(A,k1_relat_1(k7_relat_1(C,B)))
      <=> ( r2_hidden(A,B)
          & r2_hidden(A,k1_relat_1(C)) ) ) ) ),
    file(relat_1,t86_relat_1),
    [interesting(0.00)]).

fof(d6_msualg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(A))
         => k1_msualg_1(A,B) = k1_funct_1(u2_msualg_1(A),B) ) ) ),
    file(msualg_1,d6_msualg_1),
    [interesting(0.00)]).

fof(d19_pboole,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,k3_finseq_2(A))
         => ( C = k6_pboole(A,B)
          <=> ! [D] : 
                ( m2_finseq_2(D,A,k3_finseq_2(A))
               => k1_funct_1(C,D) = k4_card_3(k5_relat_1(D,B)) ) ) ) ) ),
    file(pboole,d19_pboole),
    [interesting(0.00)]).

fof(d10_msualg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(A))
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => k4_msualg_1(A,B,C) = k1_funct_1(k7_pboole(u1_msualg_1(A),u1_struct_0(A),u3_msualg_1(A),u4_msualg_1(A,C)),B) ) ) ) ),
    file(msualg_1,d10_msualg_1),
    [interesting(0.00)]).

fof(d7_msualg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(A))
         => k2_msualg_1(A,B) = k1_funct_1(u3_msualg_1(A),B) ) ) ),
    file(msualg_1,d7_msualg_1),
    [interesting(0.00)]).

fof(t6_msualg_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(A))
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ! [D] : 
                  ( ( v1_relat_1(D)
                    & v1_funct_1(D) )
                 => ( r2_hidden(D,k3_msualg_1(A,B,C))
                   => ( k1_relat_1(D) = k4_finseq_1(k1_msualg_1(A,B))
                      & ! [E] : 
                          ( r2_hidden(E,k1_relat_1(k5_relat_1(k1_msualg_1(A,B),u4_msualg_1(A,C))))
                         => r2_hidden(k1_funct_1(D,E),k1_funct_1(k5_relat_1(k1_msualg_1(A,B),u4_msualg_1(A,C)),E)) ) ) ) ) ) ) ) ),
    file(msualg_3,t6_msualg_3),
    [interesting(0.00)]).

fof(t18_card_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r2_hidden(A,k4_card_3(B))
          <=> ( k1_relat_1(A) = k1_relat_1(B)
              & ! [C] : 
                  ( r2_hidden(C,k1_relat_1(B))
                 => r2_hidden(k1_funct_1(A,C),k1_funct_1(B,C)) ) ) ) ) ) ),
    file(card_3,t18_card_3),
    [interesting(0.00)]).

fof(t23_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( r2_hidden(A,k1_relat_1(B))
           => k1_funct_1(k5_relat_1(B,C),A) = k1_funct_1(C,k1_funct_1(B,A)) ) ) ) ),
    file(funct_1,t23_funct_1),
    [interesting(0.00)]).

fof(d4_finseq_4,definition,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( r2_hidden(D,k1_relat_1(C))
         => k4_finseq_4(A,B,C,D) = k1_funct_1(C,D) ) ) ),
    file(finseq_4,d4_finseq_4),
    [interesting(0.00)]).

fof(d8_msualg_3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v5_msualg_1(B,A)
            & l3_msualg_1(B,A) )
         => ! [C] : 
              ( ( v5_msualg_1(C,A)
                & l3_msualg_1(C,A) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_msualg_1(A))
                 => ! [E] : 
                      ( m3_pboole(E,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                     => ! [F] : 
                          ( m1_subset_1(F,k3_msualg_1(A,D,B))
                         => ! [G] : 
                              ( m1_subset_1(G,k3_msualg_1(A,D,C))
                             => ( G = k6_msualg_3(A,B,C,D,E,F)
                              <=> ! [H] : 
                                    ( m2_subset_1(H,k1_numbers,k5_numbers)
                                   => ( r2_hidden(H,k1_relat_1(F))
                                     => k1_funct_1(G,H) = k1_funct_1(k1_msualg_3(u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C),E,k4_finseq_4(k5_numbers,u1_struct_0(A),k1_msualg_1(A,D),H)),k1_funct_1(F,H)) ) ) ) ) ) ) ) ) ) ) ),
    file(msualg_3,d8_msualg_3),
    [interesting(0.00)]).

fof(d9_msualg_3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ! [D] : 
                  ( m3_pboole(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                 => ( r1_msualg_3(A,B,C,D)
                  <=> ! [E] : 
                        ( m1_subset_1(E,u1_msualg_1(A))
                       => ( k3_msualg_1(A,E,B) != k1_xboole_0
                         => ! [F] : 
                              ( m1_subset_1(F,k3_msualg_1(A,E,B))
                             => k1_funct_1(k1_msualg_3(u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C),D,k2_msualg_1(A,E)),k1_funct_1(k5_msualg_1(A,E,B),F)) = k1_funct_1(k5_msualg_1(A,E,C),k5_msualg_3(A,B,C,E,D,F)) ) ) ) ) ) ) ) ) ),
    file(msualg_3,d9_msualg_3),
    [interesting(0.00)]).

fof(t9_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( ( k1_relat_1(A) = k1_relat_1(B)
              & ! [C] : 
                  ( r2_hidden(C,k1_relat_1(A))
                 => k1_funct_1(A,C) = k1_funct_1(B,C) ) )
           => A = B ) ) ) ),
    file(funct_1,t9_funct_1),
    [interesting(0.00)]).

fof(d16_msualg_2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( m4_pboole(C,u1_struct_0(A),u4_msualg_1(A,B))
             => ( v3_msualg_2(C,A,B)
               => k10_msualg_2(A,B,C) = g3_msualg_1(A,C,k4_msualg_2(A,B,C)) ) ) ) ) ),
    file(msualg_2,d16_msualg_2),
    [interesting(0.00)]).

fof(d4_msafree,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( m4_pboole(C,u1_struct_0(A),u4_msualg_1(A,B))
             => ( m1_msafree(C,A,B)
              <=> r6_pboole(u1_struct_0(A),u4_msualg_1(A,k12_msualg_2(A,B,C)),u4_msualg_1(A,B)) ) ) ) ) ),
    file(msafree,d4_msafree),
    [interesting(0.00)]).

fof(d10_msualg_2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ( m1_msualg_2(C,A,B)
              <=> ( m4_pboole(u4_msualg_1(A,C),u1_struct_0(A),u4_msualg_1(A,B))
                  & ! [D] : 
                      ( m4_pboole(D,u1_struct_0(A),u4_msualg_1(A,B))
                     => ( r6_pboole(u1_struct_0(A),D,u4_msualg_1(A,C))
                       => ( v3_msualg_2(D,A,B)
                          & r6_pboole(u1_msualg_1(A),u5_msualg_1(A,C),k4_msualg_2(A,B,D)) ) ) ) ) ) ) ) ) ),
    file(msualg_2,d10_msualg_2),
    [interesting(0.00)]).

fof(t2_extens_1,theorem,(
    $true ),
    file(extens_1,t2_extens_1),
    [interesting(0.00)]).

fof(t3_extens_1,theorem,(
    $true ),
    file(extens_1,t3_extens_1),
    [interesting(0.00)]).

fof(t4_extens_1,theorem,(
    $true ),
    file(extens_1,t4_extens_1),
    [interesting(0.00)]).

fof(t40_funct_2,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & v1_funct_2(D,A,B)
        & m2_relset_1(D,A,B) )
     => ( r1_tarski(A,C)
       => k2_partfun1(A,B,D,C) = D ) ) ),
    file(funct_2,t40_funct_2),
    [interesting(0.00)]).

fof(d25_pboole,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( ( v1_funcop_1(C)
            & m1_pboole(C,A) )
         => ! [D] : 
              ( m1_pboole(D,A)
             => ( D = k14_pboole(A,B,C)
              <=> ! [E] : 
                    ( r2_hidden(E,A)
                   => k1_funct_1(D,E) = k9_relat_1(k1_funct_1(C,E),k1_funct_1(B,E)) ) ) ) ) ) ),
    file(pboole,d25_pboole),
    [interesting(0.00)]).

fof(t156_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( r1_tarski(A,B)
       => r1_tarski(k9_relat_1(C,A),k9_relat_1(C,B)) ) ) ),
    file(relat_1,t156_relat_1),
    [interesting(0.00)]).

fof(t161_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => r1_tarski(k9_relat_1(k7_relat_1(C,A),B),k9_relat_1(C,B)) ) ),
    file(relat_1,t161_relat_1),
    [interesting(0.00)]).

fof(d13_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( C = k9_relat_1(A,B)
        <=> ! [D] : 
              ( r2_hidden(D,C)
            <=> ? [E] : 
                  ( r2_hidden(k4_tarski(E,D),A)
                  & r2_hidden(E,B) ) ) ) ) ),
    file(relat_1,d13_relat_1),
    [interesting(0.00)]).

fof(d11_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( v1_relat_1(C)
         => ( C = k7_relat_1(A,B)
          <=> ! [D,E] : 
                ( r2_hidden(k4_tarski(D,E),C)
              <=> ( r2_hidden(D,B)
                  & r2_hidden(k4_tarski(D,E),A) ) ) ) ) ) ),
    file(relat_1,d11_relat_1),
    [interesting(0.00)]).

fof(d3_pzfmisc1,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ( r1_pzfmisc1(A,B,C)
          <=> ! [D] : 
                ( ( r2_hidden(D,A)
                  & k1_funct_1(C,D) = k1_xboole_0 )
               => k1_funct_1(B,D) = k1_xboole_0 ) ) ) ) ),
    file(pzfmisc1,d3_pzfmisc1),
    [interesting(0.00)]).

fof(t9_funct_2,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & v1_funct_2(D,A,B)
        & m2_relset_1(D,A,B) )
     => ( r1_tarski(B,C)
       => ( ( B = k1_xboole_0
            & A != k1_xboole_0 )
          | ( v1_funct_1(D)
            & v1_funct_2(D,A,C)
            & m2_relset_1(D,A,C) ) ) ) ) ),
    file(funct_2,t9_funct_2),
    [interesting(0.00)]).