% Mizar problem: t51_rewrite1,rewrite1,1314,37 
fof(t51_rewrite1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v7_rewrite1(A)
      <=> r11_rewrite1(A,A) ) ) ),
    inference(mizar_bg_added,[status(thm)],[d18_rewrite1,d22_rewrite1,d7_rewrite1,d8_rewrite1,symmetry_r11_rewrite1]),
    [file(rewrite1,t51_rewrite1)]).

fof(d18_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( r11_rewrite1(A,B)
          <=> ! [C,D,E] : ~ ( r1_rewrite1(A,C,D)
                & r1_rewrite1(B,C,E)
                & ! [F] : ~ ( r1_rewrite1(B,D,F)
                    & r1_rewrite1(A,E,F) ) ) ) ) ) ),
    file(rewrite1,d18_rewrite1),
    []).

fof(d22_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v7_rewrite1(A)
      <=> ! [B,C] : 
            ( r6_rewrite1(A,B,C)
           => r5_rewrite1(A,B,C) ) ) ) ),
    file(rewrite1,d22_rewrite1),
    []).

fof(d7_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( r5_rewrite1(A,B,C)
        <=> ? [D] : 
              ( r1_rewrite1(A,B,D)
              & r1_rewrite1(A,C,D) ) ) ) ),
    file(rewrite1,d7_rewrite1),
    []).

fof(d8_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( r6_rewrite1(A,B,C)
        <=> ? [D] : 
              ( r1_rewrite1(A,D,B)
              & r1_rewrite1(A,D,C) ) ) ) ),
    file(rewrite1,d8_rewrite1),
    []).

fof(symmetry_r11_rewrite1,axiom,(
    ! [A,B] : 
      ( ( v1_relat_1(A)
        & v1_relat_1(B) )
     => ( r11_rewrite1(A,B)
       => r11_rewrite1(B,A) ) ) ),
    file(rewrite1,r11_rewrite1),
    []).