% Mizar problem: t27_rewrite1,rewrite1,664,64 
fof(t27_rewrite1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : r2_rewrite1(A,B,B) ) ),
    inference(mizar_bg_added,[status(thm)],[t13_rewrite1,t26_rewrite1]),
    [file(rewrite1,t27_rewrite1)]).

fof(t13_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : r1_rewrite1(A,B,B) ) ),
    file(rewrite1,t13_rewrite1),
    []).

fof(t26_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( r1_rewrite1(A,B,C)
         => ( r2_rewrite1(A,B,C)
            & r2_rewrite1(A,C,B) ) ) ) ),
    file(rewrite1,t26_rewrite1),
    []).