% Mizar problem: t56_rewrite1,rewrite1,1573,66 
fof(t56_rewrite1,conjecture,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v2_rewrite1(A)
        & v4_rewrite1(A) )
     => ! [B,C] : 
          ( r2_rewrite1(A,B,C)
         => k2_rewrite1(A,B) = k2_rewrite1(A,C) ) ) ),
    inference(mizar_bg_added,[status(thm)],[cc10_rewrite1,cc11_rewrite1,cc6_rewrite1,cc7_rewrite1,cc9_rewrite1,d19_rewrite1,d6_rewrite1,dt_k2_rewrite1,t26_rewrite1,t31_rewrite1,t55_rewrite1]),
    [file(rewrite1,t56_rewrite1)]).

fof(cc10_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v5_rewrite1(A) )
     => ( v1_relat_1(A)
        & v4_rewrite1(A) ) ) ),
    file(rewrite1,cc10_rewrite1),
    []).

fof(cc11_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v2_rewrite1(A)
        & v4_rewrite1(A) )
     => ( v1_relat_1(A)
        & v8_rewrite1(A) ) ) ),
    file(rewrite1,cc11_rewrite1),
    []).

fof(cc6_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v8_rewrite1(A) )
     => ( v1_relat_1(A)
        & v7_rewrite1(A) ) ) ),
    file(rewrite1,cc6_rewrite1),
    []).

fof(cc7_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v7_rewrite1(A) )
     => ( v1_relat_1(A)
        & v8_rewrite1(A)
        & v9_rewrite1(A) ) ) ),
    file(rewrite1,cc7_rewrite1),
    []).

fof(cc9_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v8_rewrite1(A) )
     => ( v1_relat_1(A)
        & v5_rewrite1(A) ) ) ),
    file(rewrite1,cc9_rewrite1),
    []).

fof(d19_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v4_rewrite1(A)
      <=> ! [B,C] : 
            ( ( r3_rewrite1(A,B)
              & r3_rewrite1(A,C)
              & r2_rewrite1(A,B,C) )
           => B = C ) ) ) ),
    file(rewrite1,d19_rewrite1),
    []).

fof(d6_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( r4_rewrite1(A,B,C)
        <=> ( r3_rewrite1(A,C)
            & r1_rewrite1(A,B,C) ) ) ) ),
    file(rewrite1,d6_rewrite1),
    []).

fof(dt_k2_rewrite1,axiom,(
    $true ),
    file(rewrite1,k2_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),
    []).

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

fof(t55_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v2_rewrite1(A)
        & v4_rewrite1(A) )
     => ! [B] : r4_rewrite1(A,B,k2_rewrite1(A,B)) ) ),
    file(rewrite1,t55_rewrite1),
    []).