% Mizar problem: t19_yellow18,yellow18,2225,55 
fof(t19_yellow18,conjecture,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_altcat_1(A)
        & v11_altcat_1(A)
        & v12_altcat_1(A)
        & l2_altcat_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_altcat_1(B)
            & v11_altcat_1(B)
            & v12_altcat_1(B)
            & l2_altcat_1(B) )
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v2_altcat_1(C)
                & v11_altcat_1(C)
                & v12_altcat_1(C)
                & l2_altcat_1(C) )
             => ! [D] : 
                  ( ( ~ v3_struct_0(D)
                    & v2_altcat_1(D)
                    & v11_altcat_1(D)
                    & v12_altcat_1(D)
                    & l2_altcat_1(D) )
                 => ( ( r2_yellow18(A,B)
                      & r2_yellow18(C,D)
                      & r1_functor0(A,C) )
                   => r1_functor0(B,D) ) ) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[cc1_altcat_2,cc2_functor0,dt_l1_altcat_1,dt_l1_struct_0,dt_l2_altcat_1,existence_l1_altcat_1,existence_l1_struct_0,existence_l2_altcat_1,rc2_altcat_2,rc3_altcat_2,rc3_struct_0,rc7_functor0,reflexivity_r1_functor0,symmetry_r1_functor0,symmetry_r2_functor0,symmetry_r2_yellow18,t18_yellow18]),
    [file(yellow18,t19_yellow18)]).

fof(cc1_altcat_2,axiom,(
    ! [A] : 
      ( l2_altcat_1(A)
     => ( ( ~ v3_struct_0(A)
          & v12_altcat_1(A) )
       => ( ~ v3_struct_0(A)
          & v1_altcat_2(A) ) ) ) ),
    file(altcat_2,cc1_altcat_2),
    []).

fof(cc2_functor0,axiom,(
    ! [A] : 
      ( l2_altcat_1(A)
     => ( ( ~ v3_struct_0(A)
          & v12_altcat_1(A) )
       => ( ~ v3_struct_0(A)
          & v1_altcat_2(A) ) ) ) ),
    file(functor0,cc2_functor0),
    []).

fof(dt_l1_altcat_1,axiom,(
    ! [A] : 
      ( l1_altcat_1(A)
     => l1_struct_0(A) ) ),
    file(altcat_1,l1_altcat_1),
    []).

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

fof(dt_l2_altcat_1,axiom,(
    ! [A] : 
      ( l2_altcat_1(A)
     => l1_altcat_1(A) ) ),
    file(altcat_1,l2_altcat_1),
    []).

fof(existence_l1_altcat_1,axiom,(
    ? [A] : l1_altcat_1(A) ),
    file(altcat_1,l1_altcat_1),
    []).

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

fof(existence_l2_altcat_1,axiom,(
    ? [A] : l2_altcat_1(A) ),
    file(altcat_1,l2_altcat_1),
    []).

fof(rc2_altcat_2,axiom,(
    ? [A] : 
      ( l1_altcat_1(A)
      & ~ v3_struct_0(A)
      & v1_altcat_2(A) ) ),
    file(altcat_2,rc2_altcat_2),
    []).

fof(rc3_altcat_2,axiom,(
    ? [A] : 
      ( l2_altcat_1(A)
      & ~ v3_struct_0(A)
      & v1_altcat_2(A) ) ),
    file(altcat_2,rc3_altcat_2),
    []).

fof(rc3_struct_0,axiom,(
    ? [A] : 
      ( l1_struct_0(A)
      & ~ v3_struct_0(A) ) ),
    file(struct_0,rc3_struct_0),
    []).

fof(rc7_functor0,axiom,(
    ? [A] : 
      ( l2_altcat_1(A)
      & ~ v3_struct_0(A)
      & v1_altcat_2(A) ) ),
    file(functor0,rc7_functor0),
    []).

fof(reflexivity_r1_functor0,axiom,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(A)
        & v2_altcat_1(A)
        & v12_altcat_1(A)
        & l2_altcat_1(A)
        & ~ v3_struct_0(B)
        & v2_altcat_1(B)
        & v12_altcat_1(B)
        & l2_altcat_1(B) )
     => r1_functor0(A,A) ) ),
    file(functor0,r1_functor0),
    []).

fof(symmetry_r1_functor0,axiom,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(A)
        & v2_altcat_1(A)
        & v12_altcat_1(A)
        & l2_altcat_1(A)
        & ~ v3_struct_0(B)
        & v2_altcat_1(B)
        & v12_altcat_1(B)
        & l2_altcat_1(B) )
     => ( r1_functor0(A,B)
       => r1_functor0(B,A) ) ) ),
    file(functor0,r1_functor0),
    []).

fof(symmetry_r2_functor0,axiom,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(A)
        & v2_altcat_1(A)
        & v12_altcat_1(A)
        & l2_altcat_1(A)
        & ~ v3_struct_0(B)
        & v2_altcat_1(B)
        & v12_altcat_1(B)
        & l2_altcat_1(B) )
     => ( r2_functor0(A,B)
       => r2_functor0(B,A) ) ) ),
    file(functor0,r2_functor0),
    []).

fof(symmetry_r2_yellow18,axiom,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(A)
        & l2_altcat_1(A)
        & ~ v3_struct_0(B)
        & l2_altcat_1(B) )
     => ( r2_yellow18(A,B)
       => r2_yellow18(B,A) ) ) ),
    file(yellow18,r2_yellow18),
    []).

fof(t18_yellow18,axiom,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_altcat_1(A)
        & v11_altcat_1(A)
        & v12_altcat_1(A)
        & l2_altcat_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_altcat_1(B)
            & v11_altcat_1(B)
            & v12_altcat_1(B)
            & l2_altcat_1(B) )
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v2_altcat_1(C)
                & v11_altcat_1(C)
                & v12_altcat_1(C)
                & l2_altcat_1(C) )
             => ( r2_yellow18(A,B)
               => ( r1_functor0(A,C)
                <=> r2_functor0(B,C) ) ) ) ) ) ),
    file(yellow18,t18_yellow18),
    []).