% Mizar problem: t31_rewrite1,rewrite1,700,32 
fof(t31_rewrite1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C,D] : 
          ( ( r2_rewrite1(A,B,C)
            & r2_rewrite1(A,C,D) )
         => r2_rewrite1(A,B,D) ) ) ),
    inference(mizar_bg_added,[status(thm)],[commutativity_k2_xboole_0,d4_rewrite1,dt_k2_xboole_0,dt_k4_relat_1,fc2_relat_1,idempotence_k2_xboole_0,involutiveness_k4_relat_1,t17_rewrite1]),
    [file(rewrite1,t31_rewrite1)]).

fof(commutativity_k2_xboole_0,axiom,(
    ! [A,B] : k2_xboole_0(A,B) = k2_xboole_0(B,A) ),
    file(xboole_0,k2_xboole_0),
    []).

fof(d4_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( r2_rewrite1(A,B,C)
        <=> r1_rewrite1(k2_xboole_0(A,k4_relat_1(A)),B,C) ) ) ),
    file(rewrite1,d4_rewrite1),
    []).

fof(dt_k2_xboole_0,axiom,(
    $true ),
    file(xboole_0,k2_xboole_0),
    []).

fof(dt_k4_relat_1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => v1_relat_1(k4_relat_1(A)) ) ),
    file(relat_1,k4_relat_1),
    []).

fof(fc2_relat_1,axiom,(
    ! [A,B] : 
      ( ( v1_relat_1(A)
        & v1_relat_1(B) )
     => v1_relat_1(k2_xboole_0(A,B)) ) ),
    file(relat_1,fc2_relat_1),
    []).

fof(idempotence_k2_xboole_0,axiom,(
    ! [A,B] : k2_xboole_0(A,A) = A ),
    file(xboole_0,k2_xboole_0),
    []).

fof(involutiveness_k4_relat_1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => k4_relat_1(k4_relat_1(A)) = A ) ),
    file(relat_1,k4_relat_1),
    []).

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