% Mizar ND problem: t3_boolealg,boolealg,60,40 
fof(dh_c1_7__boolealg,definition,
    ( ( ( ~ v3_struct_0(c1_7__boolealg)
        & v10_lattices(c1_7__boolealg)
        & l3_lattices(c1_7__boolealg) )
     => ! [A] : 
          ( m1_subset_1(A,u1_struct_0(c1_7__boolealg))
         => ! [B] : 
              ( m1_subset_1(B,u1_struct_0(c1_7__boolealg))
             => ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(c1_7__boolealg))
                 => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,A,B),C)
                   => ( r3_lattices(c1_7__boolealg,A,C)
                      & r3_lattices(c1_7__boolealg,B,C) ) ) ) ) ) )
   => ! [D] : 
        ( ( ~ v3_struct_0(D)
          & v10_lattices(D)
          & l3_lattices(D) )
       => ! [E] : 
            ( m1_subset_1(E,u1_struct_0(D))
           => ! [F] : 
                ( m1_subset_1(F,u1_struct_0(D))
               => ! [G] : 
                    ( m1_subset_1(G,u1_struct_0(D))
                   => ( r3_lattices(D,k3_lattices(D,E,F),G)
                     => ( r3_lattices(D,E,G)
                        & r3_lattices(D,F,G) ) ) ) ) ) ) ),
    introduced(definition,[new_symbol(c1_7__boolealg),file(boolealg,c1_7__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c1_7__boolealg)]).

fof(dh_c2_7__boolealg,definition,
    ( ( m1_subset_1(c2_7__boolealg,u1_struct_0(c1_7__boolealg))
     => ! [A] : 
          ( m1_subset_1(A,u1_struct_0(c1_7__boolealg))
         => ! [B] : 
              ( m1_subset_1(B,u1_struct_0(c1_7__boolealg))
             => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,A),B)
               => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,B)
                  & r3_lattices(c1_7__boolealg,A,B) ) ) ) ) )
   => ! [C] : 
        ( m1_subset_1(C,u1_struct_0(c1_7__boolealg))
       => ! [D] : 
            ( m1_subset_1(D,u1_struct_0(c1_7__boolealg))
           => ! [E] : 
                ( m1_subset_1(E,u1_struct_0(c1_7__boolealg))
               => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,C,D),E)
                 => ( r3_lattices(c1_7__boolealg,C,E)
                    & r3_lattices(c1_7__boolealg,D,E) ) ) ) ) ) ),
    introduced(definition,[new_symbol(c2_7__boolealg),file(boolealg,c2_7__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c2_7__boolealg)]).

fof(dh_c3_7__boolealg,definition,
    ( ( m1_subset_1(c3_7__boolealg,u1_struct_0(c1_7__boolealg))
     => ! [A] : 
          ( m1_subset_1(A,u1_struct_0(c1_7__boolealg))
         => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,c3_7__boolealg),A)
           => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,A)
              & r3_lattices(c1_7__boolealg,c3_7__boolealg,A) ) ) ) )
   => ! [B] : 
        ( m1_subset_1(B,u1_struct_0(c1_7__boolealg))
       => ! [C] : 
            ( m1_subset_1(C,u1_struct_0(c1_7__boolealg))
           => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,B),C)
             => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,C)
                & r3_lattices(c1_7__boolealg,B,C) ) ) ) ) ),
    introduced(definition,[new_symbol(c3_7__boolealg),file(boolealg,c3_7__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c3_7__boolealg)]).

fof(dh_c4_7__boolealg,definition,
    ( ( m1_subset_1(c4_7__boolealg,u1_struct_0(c1_7__boolealg))
     => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,c3_7__boolealg),c4_7__boolealg)
       => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,c4_7__boolealg)
          & r3_lattices(c1_7__boolealg,c3_7__boolealg,c4_7__boolealg) ) ) )
   => ! [A] : 
        ( m1_subset_1(A,u1_struct_0(c1_7__boolealg))
       => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,c3_7__boolealg),A)
         => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,A)
            & r3_lattices(c1_7__boolealg,c3_7__boolealg,A) ) ) ) ),
    introduced(definition,[new_symbol(c4_7__boolealg),file(boolealg,c4_7__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c4_7__boolealg)]).

fof(e1_7__boolealg,assumption,(
    r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,c3_7__boolealg),c4_7__boolealg) ),
    introduced(assumption,[file(boolealg,e1_7__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,e1_7__boolealg)]).

fof(cc2_lattices,theorem,(
    ! [A] : 
      ( l3_lattices(A)
     => ( ( ~ v3_struct_0(A)
          & v4_lattices(A)
          & v5_lattices(A)
          & v6_lattices(A)
          & v7_lattices(A)
          & v8_lattices(A)
          & v9_lattices(A) )
       => ( ~ v3_struct_0(A)
          & v10_lattices(A) ) ) ) ),
    file(lattices,cc2_lattices),
    [interesting(0.9),axiom,file(lattices,cc2_lattices)]).

fof(existence_l1_lattices,axiom,(
    ? [A] : l1_lattices(A) ),
    file(lattices,l1_lattices),
    [interesting(0.9),axiom,file(lattices,l1_lattices)]).

fof(existence_l1_struct_0,axiom,(
    ? [A] : l1_struct_0(A) ),
    file(struct_0,l1_struct_0),
    [interesting(0.9),axiom,file(struct_0,l1_struct_0)]).

fof(existence_l3_lattices,axiom,(
    ? [A] : l3_lattices(A) ),
    file(lattices,l3_lattices),
    [interesting(0.9),axiom,file(lattices,l3_lattices)]).

fof(dt_k2_lattices,axiom,(
    ! [A,B,C] : 
      ( ( ~ v3_struct_0(A)
        & l1_lattices(A)
        & m1_subset_1(B,u1_struct_0(A))
        & m1_subset_1(C,u1_struct_0(A)) )
     => m1_subset_1(k2_lattices(A,B,C),u1_struct_0(A)) ) ),
    file(lattices,k2_lattices),
    [interesting(0.9),axiom,file(lattices,k2_lattices)]).

fof(dt_l1_lattices,axiom,(
    ! [A] : 
      ( l1_lattices(A)
     => l1_struct_0(A) ) ),
    file(lattices,l1_lattices),
    [interesting(0.9),axiom,file(lattices,l1_lattices)]).

fof(dt_l1_struct_0,axiom,(
    $true ),
    file(struct_0,l1_struct_0),
    [interesting(0.9),axiom,file(struct_0,l1_struct_0)]).

fof(dt_l3_lattices,axiom,(
    ! [A] : 
      ( l3_lattices(A)
     => ( l1_lattices(A)
        & l2_lattices(A) ) ) ),
    file(lattices,l3_lattices),
    [interesting(0.9),axiom,file(lattices,l3_lattices)]).

fof(cc1_lattices,theorem,(
    ! [A] : 
      ( l3_lattices(A)
     => ( ( ~ v3_struct_0(A)
          & v10_lattices(A) )
       => ( ~ v3_struct_0(A)
          & v4_lattices(A)
          & v5_lattices(A)
          & v6_lattices(A)
          & v7_lattices(A)
          & v8_lattices(A)
          & v9_lattices(A) ) ) ) ),
    file(lattices,cc1_lattices),
    [interesting(0.9),axiom,file(lattices,cc1_lattices)]).

fof(commutativity_k4_lattices,theorem,(
    ! [A,B,C] : 
      ( ( ~ v3_struct_0(A)
        & v6_lattices(A)
        & l1_lattices(A)
        & m1_subset_1(B,u1_struct_0(A))
        & m1_subset_1(C,u1_struct_0(A)) )
     => k4_lattices(A,B,C) = k4_lattices(A,C,B) ) ),
    file(lattices,k4_lattices),
    [interesting(0.9),axiom,file(lattices,k4_lattices)]).

fof(reflexivity_r3_lattices,theorem,(
    ! [A,B,C] : 
      ( ( ~ v3_struct_0(A)
        & v6_lattices(A)
        & v8_lattices(A)
        & v9_lattices(A)
        & l3_lattices(A)
        & m1_subset_1(B,u1_struct_0(A))
        & m1_subset_1(C,u1_struct_0(A)) )
     => r3_lattices(A,B,B) ) ),
    file(lattices,r3_lattices),
    [interesting(0.9),axiom,file(lattices,r3_lattices)]).

fof(existence_l2_lattices,axiom,(
    ? [A] : l2_lattices(A) ),
    file(lattices,l2_lattices),
    [interesting(0.9),axiom,file(lattices,l2_lattices)]).

fof(existence_m1_subset_1,axiom,(
    ! [A] : 
    ? [B] : m1_subset_1(B,A) ),
    file(subset_1,m1_subset_1),
    [interesting(0.9),axiom,file(subset_1,m1_subset_1)]).

fof(redefinition_k4_lattices,definition,(
    ! [A,B,C] : 
      ( ( ~ v3_struct_0(A)
        & v6_lattices(A)
        & l1_lattices(A)
        & m1_subset_1(B,u1_struct_0(A))
        & m1_subset_1(C,u1_struct_0(A)) )
     => k4_lattices(A,B,C) = k2_lattices(A,B,C) ) ),
    file(lattices,k4_lattices),
    [interesting(0.9),axiom,file(lattices,k4_lattices)]).

fof(redefinition_r3_lattices,definition,(
    ! [A,B,C] : 
      ( ( ~ v3_struct_0(A)
        & v6_lattices(A)
        & v8_lattices(A)
        & v9_lattices(A)
        & l3_lattices(A)
        & m1_subset_1(B,u1_struct_0(A))
        & m1_subset_1(C,u1_struct_0(A)) )
     => ( r3_lattices(A,B,C)
      <=> r1_lattices(A,B,C) ) ) ),
    file(lattices,r3_lattices),
    [interesting(0.9),axiom,file(lattices,r3_lattices)]).

fof(dt_k4_lattices,axiom,(
    ! [A,B,C] : 
      ( ( ~ v3_struct_0(A)
        & v6_lattices(A)
        & l1_lattices(A)
        & m1_subset_1(B,u1_struct_0(A))
        & m1_subset_1(C,u1_struct_0(A)) )
     => m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A)) ) ),
    file(lattices,k4_lattices),
    [interesting(0.9),axiom,file(lattices,k4_lattices)]).

fof(dt_l2_lattices,axiom,(
    ! [A] : 
      ( l2_lattices(A)
     => l1_struct_0(A) ) ),
    file(lattices,l2_lattices),
    [interesting(0.9),axiom,file(lattices,l2_lattices)]).

fof(dt_m1_subset_1,axiom,(
    $true ),
    file(subset_1,m1_subset_1),
    [interesting(0.9),axiom,file(subset_1,m1_subset_1)]).

fof(dt_u1_struct_0,axiom,(
    $true ),
    file(struct_0,u1_struct_0),
    [interesting(0.9),axiom,file(struct_0,u1_struct_0)]).

fof(dt_c1_7__boolealg,assumption,
    ( ~ v3_struct_0(c1_7__boolealg)
    & v10_lattices(c1_7__boolealg)
    & l3_lattices(c1_7__boolealg) ),
    introduced(assumption,[file(boolealg,c1_7__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c1_7__boolealg)]).

fof(dt_c2_7__boolealg,assumption,(
    m1_subset_1(c2_7__boolealg,u1_struct_0(c1_7__boolealg)) ),
    introduced(assumption,[file(boolealg,c2_7__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c2_7__boolealg)]).

fof(dt_c3_7__boolealg,assumption,(
    m1_subset_1(c3_7__boolealg,u1_struct_0(c1_7__boolealg)) ),
    introduced(assumption,[file(boolealg,c3_7__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c3_7__boolealg)]).

fof(dt_c4_7__boolealg,assumption,(
    m1_subset_1(c4_7__boolealg,u1_struct_0(c1_7__boolealg)) ),
    introduced(assumption,[file(boolealg,c4_7__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c4_7__boolealg)]).

fof(t23_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_lattices(A)
        & v8_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => r1_lattices(A,k4_lattices(A,B,C),B) ) ) ) ),
    file(lattices,t23_lattices),
    [interesting(0.9),axiom,file(lattices,t23_lattices)]).

fof(e7_7__boolealg,plain,(
    r3_lattices(c1_7__boolealg,k4_lattices(c1_7__boolealg,c3_7__boolealg,c4_7__boolealg),c4_7__boolealg) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg])],[cc2_lattices,existence_l1_lattices,existence_l1_struct_0,existence_l2_lattices,dt_k2_lattices,dt_l1_lattices,dt_l1_struct_0,dt_l2_lattices,cc1_lattices,commutativity_k4_lattices,reflexivity_r3_lattices,existence_l3_lattices,existence_m1_subset_1,redefinition_k4_lattices,redefinition_r3_lattices,dt_k4_lattices,dt_l3_lattices,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,t23_lattices]),
    [interesting(0.8),file(boolealg,e7_7__boolealg),[file(boolealg,e7_7__boolealg)]]).

fof(commutativity_k3_lattices,theorem,(
    ! [A,B,C] : 
      ( ( ~ v3_struct_0(A)
        & v4_lattices(A)
        & l2_lattices(A)
        & m1_subset_1(B,u1_struct_0(A))
        & m1_subset_1(C,u1_struct_0(A)) )
     => k3_lattices(A,B,C) = k3_lattices(A,C,B) ) ),
    file(lattices,k3_lattices),
    [interesting(0.9),axiom,file(lattices,k3_lattices)]).

fof(redefinition_k3_lattices,definition,(
    ! [A,B,C] : 
      ( ( ~ v3_struct_0(A)
        & v4_lattices(A)
        & l2_lattices(A)
        & m1_subset_1(B,u1_struct_0(A))
        & m1_subset_1(C,u1_struct_0(A)) )
     => k3_lattices(A,B,C) = k1_lattices(A,B,C) ) ),
    file(lattices,k3_lattices),
    [interesting(0.9),axiom,file(lattices,k3_lattices)]).

fof(dt_k1_lattices,axiom,(
    ! [A,B,C] : 
      ( ( ~ v3_struct_0(A)
        & l2_lattices(A)
        & m1_subset_1(B,u1_struct_0(A))
        & m1_subset_1(C,u1_struct_0(A)) )
     => m1_subset_1(k1_lattices(A,B,C),u1_struct_0(A)) ) ),
    file(lattices,k1_lattices),
    [interesting(0.9),axiom,file(lattices,k1_lattices)]).

fof(dt_k3_lattices,axiom,(
    ! [A,B,C] : 
      ( ( ~ v3_struct_0(A)
        & v4_lattices(A)
        & l2_lattices(A)
        & m1_subset_1(B,u1_struct_0(A))
        & m1_subset_1(C,u1_struct_0(A)) )
     => m1_subset_1(k3_lattices(A,B,C),u1_struct_0(A)) ) ),
    file(lattices,k3_lattices),
    [interesting(0.9),axiom,file(lattices,k3_lattices)]).

fof(t27_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v7_lattices(A)
        & v8_lattices(A)
        & v9_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( r1_lattices(A,B,C)
                   => r1_lattices(A,k2_lattices(A,B,D),k2_lattices(A,C,D)) ) ) ) ) ) ),
    file(lattices,t27_lattices),
    [interesting(0.9),axiom,file(lattices,t27_lattices)]).

fof(e2_7__boolealg,plain,(
    r3_lattices(c1_7__boolealg,k4_lattices(c1_7__boolealg,c2_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,c3_7__boolealg)),k4_lattices(c1_7__boolealg,c2_7__boolealg,c4_7__boolealg)) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e1_7__boolealg])],[cc2_lattices,existence_l1_lattices,existence_l1_struct_0,existence_l2_lattices,dt_k1_lattices,dt_l1_lattices,dt_l1_struct_0,dt_l2_lattices,cc1_lattices,commutativity_k3_lattices,commutativity_k4_lattices,reflexivity_r3_lattices,existence_l3_lattices,existence_m1_subset_1,redefinition_k3_lattices,redefinition_k4_lattices,redefinition_r3_lattices,dt_k2_lattices,dt_k3_lattices,dt_k4_lattices,dt_l3_lattices,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e1_7__boolealg,t27_lattices]),
    [interesting(0.8),file(boolealg,e2_7__boolealg),[file(boolealg,e2_7__boolealg)]]).

fof(d9_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ( v9_lattices(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => k2_lattices(A,B,k1_lattices(A,B,C)) = B ) ) ) ) ),
    file(lattices,d9_lattices),
    [interesting(0.9),axiom,file(lattices,d9_lattices)]).

fof(e3_7__boolealg,plain,(
    r3_lattices(c1_7__boolealg,c2_7__boolealg,k4_lattices(c1_7__boolealg,c2_7__boolealg,c4_7__boolealg)) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e1_7__boolealg])],[cc2_lattices,existence_l1_lattices,existence_l1_struct_0,existence_l2_lattices,dt_l1_lattices,dt_l1_struct_0,dt_l2_lattices,cc1_lattices,commutativity_k3_lattices,commutativity_k4_lattices,reflexivity_r3_lattices,existence_l3_lattices,existence_m1_subset_1,redefinition_k3_lattices,redefinition_k4_lattices,redefinition_r3_lattices,dt_k1_lattices,dt_k2_lattices,dt_k3_lattices,dt_k4_lattices,dt_l3_lattices,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e2_7__boolealg,d9_lattices]),
    [interesting(0.8),file(boolealg,e3_7__boolealg),[file(boolealg,e3_7__boolealg)]]).

fof(e4_7__boolealg,plain,(
    r3_lattices(c1_7__boolealg,k4_lattices(c1_7__boolealg,c2_7__boolealg,c4_7__boolealg),c4_7__boolealg) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c4_7__boolealg])],[cc2_lattices,existence_l1_lattices,existence_l1_struct_0,existence_l2_lattices,dt_k2_lattices,dt_l1_lattices,dt_l1_struct_0,dt_l2_lattices,cc1_lattices,commutativity_k4_lattices,reflexivity_r3_lattices,existence_l3_lattices,existence_m1_subset_1,redefinition_k4_lattices,redefinition_r3_lattices,dt_k4_lattices,dt_l3_lattices,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c4_7__boolealg,t23_lattices]),
    [interesting(0.8),file(boolealg,e4_7__boolealg),[file(boolealg,e4_7__boolealg)]]).

fof(e5_7__boolealg,plain,(
    r3_lattices(c1_7__boolealg,k4_lattices(c1_7__boolealg,c3_7__boolealg,k3_lattices(c1_7__boolealg,c3_7__boolealg,c2_7__boolealg)),k4_lattices(c1_7__boolealg,c3_7__boolealg,c4_7__boolealg)) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e1_7__boolealg])],[cc2_lattices,existence_l1_lattices,existence_l1_struct_0,existence_l2_lattices,dt_k1_lattices,dt_l1_lattices,dt_l1_struct_0,dt_l2_lattices,cc1_lattices,commutativity_k3_lattices,commutativity_k4_lattices,reflexivity_r3_lattices,existence_l3_lattices,existence_m1_subset_1,redefinition_k3_lattices,redefinition_k4_lattices,redefinition_r3_lattices,dt_k2_lattices,dt_k3_lattices,dt_k4_lattices,dt_l3_lattices,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e1_7__boolealg,t27_lattices]),
    [interesting(0.8),file(boolealg,e5_7__boolealg),[file(boolealg,e5_7__boolealg)]]).

fof(e6_7__boolealg,plain,(
    r3_lattices(c1_7__boolealg,c3_7__boolealg,k4_lattices(c1_7__boolealg,c3_7__boolealg,c4_7__boolealg)) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e1_7__boolealg])],[cc2_lattices,existence_l1_lattices,existence_l1_struct_0,existence_l2_lattices,dt_l1_lattices,dt_l1_struct_0,dt_l2_lattices,cc1_lattices,commutativity_k3_lattices,commutativity_k4_lattices,reflexivity_r3_lattices,existence_l3_lattices,existence_m1_subset_1,redefinition_k3_lattices,redefinition_k4_lattices,redefinition_r3_lattices,dt_k1_lattices,dt_k2_lattices,dt_k3_lattices,dt_k4_lattices,dt_l3_lattices,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e5_7__boolealg,d9_lattices]),
    [interesting(0.8),file(boolealg,e6_7__boolealg),[file(boolealg,e6_7__boolealg)]]).

fof(t25_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v5_lattices(A)
        & l2_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( ( r1_lattices(A,B,C)
                      & r1_lattices(A,C,D) )
                   => r1_lattices(A,B,D) ) ) ) ) ) ),
    file(lattices,t25_lattices),
    [interesting(0.9),axiom,file(lattices,t25_lattices)]).

fof(e8_7__boolealg,plain,
    ( r3_lattices(c1_7__boolealg,c2_7__boolealg,c4_7__boolealg)
    & r3_lattices(c1_7__boolealg,c3_7__boolealg,c4_7__boolealg) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e1_7__boolealg])],[cc2_lattices,existence_l1_lattices,existence_l1_struct_0,existence_l3_lattices,dt_k2_lattices,dt_l1_lattices,dt_l1_struct_0,dt_l3_lattices,cc1_lattices,commutativity_k4_lattices,reflexivity_r3_lattices,existence_l2_lattices,existence_m1_subset_1,redefinition_k4_lattices,redefinition_r3_lattices,dt_k4_lattices,dt_l2_lattices,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e7_7__boolealg,e3_7__boolealg,e4_7__boolealg,e6_7__boolealg,t25_lattices]),
    [interesting(0.8),file(boolealg,e8_7__boolealg),[file(boolealg,e8_7__boolealg)]]).

fof(i6_7__boolealg,theorem,(
    $true ),
    introduced(tautology,[file(boolealg,i6_7__boolealg)]),
    [interesting(0.8),trivial,file(boolealg,i6_7__boolealg)]).

fof(i5_7__boolealg,plain,
    ( r3_lattices(c1_7__boolealg,c2_7__boolealg,c4_7__boolealg)
    & r3_lattices(c1_7__boolealg,c3_7__boolealg,c4_7__boolealg) ),
    inference(conclusion,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg,e1_7__boolealg])],[e8_7__boolealg,i6_7__boolealg]),
    [interesting(0.8),file(boolealg,i5_7__boolealg),[file(boolealg,i5_7__boolealg)]]).

fof(i4_7__boolealg,plain,
    ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,c3_7__boolealg),c4_7__boolealg)
   => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,c4_7__boolealg)
      & r3_lattices(c1_7__boolealg,c3_7__boolealg,c4_7__boolealg) ) ),
    inference(discharge_asm,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg,dt_c4_7__boolealg]),discharge_asm(discharge,[e1_7__boolealg])],[e1_7__boolealg,i5_7__boolealg]),
    [interesting(0.8),file(boolealg,i4_7__boolealg),[file(boolealg,i4_7__boolealg)]]).

fof(i4_7_tmp__boolealg,plain,
    ( m1_subset_1(c4_7__boolealg,u1_struct_0(c1_7__boolealg))
   => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,c3_7__boolealg),c4_7__boolealg)
     => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,c4_7__boolealg)
        & r3_lattices(c1_7__boolealg,c3_7__boolealg,c4_7__boolealg) ) ) ),
    inference(discharge_asm,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg]),discharge_asm(discharge,[dt_c4_7__boolealg])],[dt_c4_7__boolealg,i4_7__boolealg]),
    [interesting(0.8),i3_7__boolealg]).

fof(i3_7__boolealg,plain,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(c1_7__boolealg))
     => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,c3_7__boolealg),A)
       => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,A)
          & r3_lattices(c1_7__boolealg,c3_7__boolealg,A) ) ) ) ),
    inference(let,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg,dt_c3_7__boolealg])],[i4_7_tmp__boolealg,dh_c4_7__boolealg]),
    [interesting(0.8),file(boolealg,i3_7__boolealg),[file(boolealg,i3_7__boolealg)]]).

fof(i3_7_tmp__boolealg,plain,
    ( m1_subset_1(c3_7__boolealg,u1_struct_0(c1_7__boolealg))
   => ! [A] : 
        ( m1_subset_1(A,u1_struct_0(c1_7__boolealg))
       => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,c3_7__boolealg),A)
         => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,A)
            & r3_lattices(c1_7__boolealg,c3_7__boolealg,A) ) ) ) ),
    inference(discharge_asm,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg]),discharge_asm(discharge,[dt_c3_7__boolealg])],[dt_c3_7__boolealg,i3_7__boolealg]),
    [interesting(0.8),i2_7__boolealg]).

fof(i2_7__boolealg,plain,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(c1_7__boolealg))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(c1_7__boolealg))
         => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,A),B)
           => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,B)
              & r3_lattices(c1_7__boolealg,A,B) ) ) ) ) ),
    inference(let,[status(thm),assumptions([dt_c1_7__boolealg,dt_c2_7__boolealg])],[i3_7_tmp__boolealg,dh_c3_7__boolealg]),
    [interesting(0.8),file(boolealg,i2_7__boolealg),[file(boolealg,i2_7__boolealg)]]).

fof(i2_7_tmp__boolealg,plain,
    ( m1_subset_1(c2_7__boolealg,u1_struct_0(c1_7__boolealg))
   => ! [A] : 
        ( m1_subset_1(A,u1_struct_0(c1_7__boolealg))
       => ! [B] : 
            ( m1_subset_1(B,u1_struct_0(c1_7__boolealg))
           => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,c2_7__boolealg,A),B)
             => ( r3_lattices(c1_7__boolealg,c2_7__boolealg,B)
                & r3_lattices(c1_7__boolealg,A,B) ) ) ) ) ),
    inference(discharge_asm,[status(thm),assumptions([dt_c1_7__boolealg]),discharge_asm(discharge,[dt_c2_7__boolealg])],[dt_c2_7__boolealg,i2_7__boolealg]),
    [interesting(0.8),i1_7__boolealg]).

fof(i1_7__boolealg,plain,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(c1_7__boolealg))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(c1_7__boolealg))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(c1_7__boolealg))
             => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,A,B),C)
               => ( r3_lattices(c1_7__boolealg,A,C)
                  & r3_lattices(c1_7__boolealg,B,C) ) ) ) ) ) ),
    inference(let,[status(thm),assumptions([dt_c1_7__boolealg])],[i2_7_tmp__boolealg,dh_c2_7__boolealg]),
    [interesting(0.8),file(boolealg,i1_7__boolealg),[file(boolealg,i1_7__boolealg)]]).

fof(i1_7_tmp__boolealg,plain,
    ( ( ~ v3_struct_0(c1_7__boolealg)
      & v10_lattices(c1_7__boolealg)
      & l3_lattices(c1_7__boolealg) )
   => ! [A] : 
        ( m1_subset_1(A,u1_struct_0(c1_7__boolealg))
       => ! [B] : 
            ( m1_subset_1(B,u1_struct_0(c1_7__boolealg))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(c1_7__boolealg))
               => ( r3_lattices(c1_7__boolealg,k3_lattices(c1_7__boolealg,A,B),C)
                 => ( r3_lattices(c1_7__boolealg,A,C)
                    & r3_lattices(c1_7__boolealg,B,C) ) ) ) ) ) ),
    inference(discharge_asm,[status(thm),assumptions([]),discharge_asm(discharge,[dt_c1_7__boolealg])],[dt_c1_7__boolealg,i1_7__boolealg]),
    [interesting(1),t3_boolealg]).

fof(t3_boolealg,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( r3_lattices(A,k3_lattices(A,B,C),D)
                   => ( r3_lattices(A,B,D)
                      & r3_lattices(A,C,D) ) ) ) ) ) ) ),
    inference(let,[status(thm),assumptions([])],[i1_7_tmp__boolealg,dh_c1_7__boolealg]),
    [interesting(1),file(boolealg,t3_boolealg),[file(boolealg,t3_boolealg)]]).