% Mizar ND problem: t4_boolealg,boolealg,73,23 
fof(dh_c1_8__boolealg,definition,
    ( ( ( ~ v3_struct_0(c1_8__boolealg)
        & v10_lattices(c1_8__boolealg)
        & l3_lattices(c1_8__boolealg) )
     => ! [A] : 
          ( m1_subset_1(A,u1_struct_0(c1_8__boolealg))
         => ! [B] : 
              ( m1_subset_1(B,u1_struct_0(c1_8__boolealg))
             => ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(c1_8__boolealg))
                 => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,A,B),k3_lattices(c1_8__boolealg,A,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,k4_lattices(D,E,F),k3_lattices(D,E,G)) ) ) ) ) ),
    introduced(definition,[new_symbol(c1_8__boolealg),file(boolealg,c1_8__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c1_8__boolealg)]).

fof(dh_c2_8__boolealg,definition,
    ( ( m1_subset_1(c2_8__boolealg,u1_struct_0(c1_8__boolealg))
     => ! [A] : 
          ( m1_subset_1(A,u1_struct_0(c1_8__boolealg))
         => ! [B] : 
              ( m1_subset_1(B,u1_struct_0(c1_8__boolealg))
             => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,A),k3_lattices(c1_8__boolealg,c2_8__boolealg,B)) ) ) )
   => ! [C] : 
        ( m1_subset_1(C,u1_struct_0(c1_8__boolealg))
       => ! [D] : 
            ( m1_subset_1(D,u1_struct_0(c1_8__boolealg))
           => ! [E] : 
                ( m1_subset_1(E,u1_struct_0(c1_8__boolealg))
               => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,C,D),k3_lattices(c1_8__boolealg,C,E)) ) ) ) ),
    introduced(definition,[new_symbol(c2_8__boolealg),file(boolealg,c2_8__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c2_8__boolealg)]).

fof(dh_c3_8__boolealg,definition,
    ( ( m1_subset_1(c3_8__boolealg,u1_struct_0(c1_8__boolealg))
     => ! [A] : 
          ( m1_subset_1(A,u1_struct_0(c1_8__boolealg))
         => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,c3_8__boolealg),k3_lattices(c1_8__boolealg,c2_8__boolealg,A)) ) )
   => ! [B] : 
        ( m1_subset_1(B,u1_struct_0(c1_8__boolealg))
       => ! [C] : 
            ( m1_subset_1(C,u1_struct_0(c1_8__boolealg))
           => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,B),k3_lattices(c1_8__boolealg,c2_8__boolealg,C)) ) ) ),
    introduced(definition,[new_symbol(c3_8__boolealg),file(boolealg,c3_8__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c3_8__boolealg)]).

fof(dh_c4_8__boolealg,definition,
    ( ( m1_subset_1(c4_8__boolealg,u1_struct_0(c1_8__boolealg))
     => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,c3_8__boolealg),k3_lattices(c1_8__boolealg,c2_8__boolealg,c4_8__boolealg)) )
   => ! [A] : 
        ( m1_subset_1(A,u1_struct_0(c1_8__boolealg))
       => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,c3_8__boolealg),k3_lattices(c1_8__boolealg,c2_8__boolealg,A)) ) ),
    introduced(definition,[new_symbol(c4_8__boolealg),file(boolealg,c4_8__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c4_8__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_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_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_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(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_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(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_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(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_8__boolealg,assumption,
    ( ~ v3_struct_0(c1_8__boolealg)
    & v10_lattices(c1_8__boolealg)
    & l3_lattices(c1_8__boolealg) ),
    introduced(assumption,[file(boolealg,c1_8__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c1_8__boolealg)]).

fof(dt_c2_8__boolealg,assumption,(
    m1_subset_1(c2_8__boolealg,u1_struct_0(c1_8__boolealg)) ),
    introduced(assumption,[file(boolealg,c2_8__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c2_8__boolealg)]).

fof(dt_c3_8__boolealg,assumption,(
    m1_subset_1(c3_8__boolealg,u1_struct_0(c1_8__boolealg)) ),
    introduced(assumption,[file(boolealg,c3_8__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c3_8__boolealg)]).

fof(dt_c4_8__boolealg,assumption,(
    m1_subset_1(c4_8__boolealg,u1_struct_0(c1_8__boolealg)) ),
    introduced(assumption,[file(boolealg,c4_8__boolealg)]),
    [interesting(0.8),axiom,file(boolealg,c4_8__boolealg)]).

fof(t22_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v5_lattices(A)
        & v6_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))
             => r1_lattices(A,B,k1_lattices(A,B,C)) ) ) ) ),
    file(lattices,t22_lattices),
    [interesting(0.9),axiom,file(lattices,t22_lattices)]).

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(e1_8__boolealg,plain,
    ( r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,c3_8__boolealg),c2_8__boolealg)
    & r3_lattices(c1_8__boolealg,c2_8__boolealg,k3_lattices(c1_8__boolealg,c2_8__boolealg,c4_8__boolealg)) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_8__boolealg,dt_c2_8__boolealg,dt_c3_8__boolealg,dt_c4_8__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_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_k3_lattices,dt_k4_lattices,dt_l3_lattices,dt_m1_subset_1,dt_u1_struct_0,dt_c1_8__boolealg,dt_c2_8__boolealg,dt_c3_8__boolealg,dt_c4_8__boolealg,t22_lattices,t23_lattices]),
    [interesting(0.8),file(boolealg,e1_8__boolealg),[file(boolealg,e1_8__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(e2_8__boolealg,plain,(
    r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,c3_8__boolealg),k3_lattices(c1_8__boolealg,c2_8__boolealg,c4_8__boolealg)) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_8__boolealg,dt_c2_8__boolealg,dt_c3_8__boolealg,dt_c4_8__boolealg])],[cc2_lattices,existence_l1_lattices,existence_l1_struct_0,existence_l3_lattices,dt_k1_lattices,dt_k2_lattices,dt_l1_lattices,dt_l1_struct_0,dt_l3_lattices,cc1_lattices,commutativity_k3_lattices,commutativity_k4_lattices,reflexivity_r3_lattices,existence_l2_lattices,existence_m1_subset_1,redefinition_k3_lattices,redefinition_k4_lattices,redefinition_r3_lattices,dt_k3_lattices,dt_k4_lattices,dt_l2_lattices,dt_m1_subset_1,dt_u1_struct_0,dt_c1_8__boolealg,dt_c2_8__boolealg,dt_c3_8__boolealg,dt_c4_8__boolealg,e1_8__boolealg,t25_lattices]),
    [interesting(0.8),file(boolealg,e2_8__boolealg),[file(boolealg,e2_8__boolealg)]]).

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

fof(i4_8__boolealg,plain,(
    r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,c3_8__boolealg),k3_lattices(c1_8__boolealg,c2_8__boolealg,c4_8__boolealg)) ),
    inference(conclusion,[status(thm),assumptions([dt_c1_8__boolealg,dt_c2_8__boolealg,dt_c3_8__boolealg,dt_c4_8__boolealg])],[e2_8__boolealg,i5_8__boolealg]),
    [interesting(0.8),file(boolealg,i4_8__boolealg),[file(boolealg,i4_8__boolealg)]]).

fof(i4_8_tmp__boolealg,plain,
    ( m1_subset_1(c4_8__boolealg,u1_struct_0(c1_8__boolealg))
   => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,c3_8__boolealg),k3_lattices(c1_8__boolealg,c2_8__boolealg,c4_8__boolealg)) ),
    inference(discharge_asm,[status(thm),assumptions([dt_c1_8__boolealg,dt_c2_8__boolealg,dt_c3_8__boolealg]),discharge_asm(discharge,[dt_c4_8__boolealg])],[dt_c4_8__boolealg,i4_8__boolealg]),
    [interesting(0.8),i3_8__boolealg]).

fof(i3_8__boolealg,plain,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(c1_8__boolealg))
     => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,c3_8__boolealg),k3_lattices(c1_8__boolealg,c2_8__boolealg,A)) ) ),
    inference(let,[status(thm),assumptions([dt_c1_8__boolealg,dt_c2_8__boolealg,dt_c3_8__boolealg])],[i4_8_tmp__boolealg,dh_c4_8__boolealg]),
    [interesting(0.8),file(boolealg,i3_8__boolealg),[file(boolealg,i3_8__boolealg)]]).

fof(i3_8_tmp__boolealg,plain,
    ( m1_subset_1(c3_8__boolealg,u1_struct_0(c1_8__boolealg))
   => ! [A] : 
        ( m1_subset_1(A,u1_struct_0(c1_8__boolealg))
       => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,c3_8__boolealg),k3_lattices(c1_8__boolealg,c2_8__boolealg,A)) ) ),
    inference(discharge_asm,[status(thm),assumptions([dt_c1_8__boolealg,dt_c2_8__boolealg]),discharge_asm(discharge,[dt_c3_8__boolealg])],[dt_c3_8__boolealg,i3_8__boolealg]),
    [interesting(0.8),i2_8__boolealg]).

fof(i2_8__boolealg,plain,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(c1_8__boolealg))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(c1_8__boolealg))
         => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,A),k3_lattices(c1_8__boolealg,c2_8__boolealg,B)) ) ) ),
    inference(let,[status(thm),assumptions([dt_c1_8__boolealg,dt_c2_8__boolealg])],[i3_8_tmp__boolealg,dh_c3_8__boolealg]),
    [interesting(0.8),file(boolealg,i2_8__boolealg),[file(boolealg,i2_8__boolealg)]]).

fof(i2_8_tmp__boolealg,plain,
    ( m1_subset_1(c2_8__boolealg,u1_struct_0(c1_8__boolealg))
   => ! [A] : 
        ( m1_subset_1(A,u1_struct_0(c1_8__boolealg))
       => ! [B] : 
            ( m1_subset_1(B,u1_struct_0(c1_8__boolealg))
           => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,c2_8__boolealg,A),k3_lattices(c1_8__boolealg,c2_8__boolealg,B)) ) ) ),
    inference(discharge_asm,[status(thm),assumptions([dt_c1_8__boolealg]),discharge_asm(discharge,[dt_c2_8__boolealg])],[dt_c2_8__boolealg,i2_8__boolealg]),
    [interesting(0.8),i1_8__boolealg]).

fof(i1_8__boolealg,plain,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(c1_8__boolealg))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(c1_8__boolealg))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(c1_8__boolealg))
             => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,A,B),k3_lattices(c1_8__boolealg,A,C)) ) ) ) ),
    inference(let,[status(thm),assumptions([dt_c1_8__boolealg])],[i2_8_tmp__boolealg,dh_c2_8__boolealg]),
    [interesting(0.8),file(boolealg,i1_8__boolealg),[file(boolealg,i1_8__boolealg)]]).

fof(i1_8_tmp__boolealg,plain,
    ( ( ~ v3_struct_0(c1_8__boolealg)
      & v10_lattices(c1_8__boolealg)
      & l3_lattices(c1_8__boolealg) )
   => ! [A] : 
        ( m1_subset_1(A,u1_struct_0(c1_8__boolealg))
       => ! [B] : 
            ( m1_subset_1(B,u1_struct_0(c1_8__boolealg))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(c1_8__boolealg))
               => r3_lattices(c1_8__boolealg,k4_lattices(c1_8__boolealg,A,B),k3_lattices(c1_8__boolealg,A,C)) ) ) ) ),
    inference(discharge_asm,[status(thm),assumptions([]),discharge_asm(discharge,[dt_c1_8__boolealg])],[dt_c1_8__boolealg,i1_8__boolealg]),
    [interesting(1),t4_boolealg]).

fof(t4_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,k4_lattices(A,B,C),k3_lattices(A,B,D)) ) ) ) ) ),
    inference(let,[status(thm),assumptions([])],[i1_8_tmp__boolealg,dh_c1_8__boolealg]),
    [interesting(1),file(boolealg,t4_boolealg),[file(boolealg,t4_boolealg)]]).