% Mizar problem: t65_rewrite1,rewrite1,2168,24 
fof(t65_rewrite1,conjecture,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v10_rewrite1(B) )
         => ( r12_rewrite1(A,B)
           => m2_rewrite1(B,A) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[cc10_rewrite1,cc11_rewrite1,cc13_rewrite1,cc14_rewrite1,cc15_rewrite1,cc2_rewrite1,cc3_rewrite1,cc5_rewrite1,cc6_rewrite1,cc7_rewrite1,cc9_rewrite1,d23_rewrite1,d26_rewrite1,d28_rewrite1,dt_m2_rewrite1,existence_m2_rewrite1,symmetry_r12_rewrite1,t38_rewrite1]),
    [file(rewrite1,t65_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(cc13_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v3_rewrite1(A)
        & v9_rewrite1(A) )
     => ( v1_relat_1(A)
        & v4_rewrite1(A)
        & v5_rewrite1(A)
        & v7_rewrite1(A)
        & v8_rewrite1(A)
        & v9_rewrite1(A) ) ) ),
    file(rewrite1,cc13_rewrite1),
    []).

fof(cc14_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v10_rewrite1(A) )
     => ( v1_relat_1(A)
        & v2_relat_2(A)
        & v1_rewrite1(A)
        & v2_rewrite1(A)
        & v3_rewrite1(A)
        & v4_rewrite1(A)
        & v5_rewrite1(A)
        & v7_rewrite1(A)
        & v8_rewrite1(A)
        & v9_rewrite1(A) ) ) ),
    file(rewrite1,cc14_rewrite1),
    []).

fof(cc15_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v3_rewrite1(A)
        & v7_rewrite1(A) )
     => ( v1_relat_1(A)
        & v10_rewrite1(A) ) ) ),
    file(rewrite1,cc15_rewrite1),
    []).

fof(cc2_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v3_rewrite1(A) )
     => ( v1_relat_1(A)
        & v2_relat_2(A)
        & v1_rewrite1(A) ) ) ),
    file(rewrite1,cc2_rewrite1),
    []).

fof(cc3_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v2_relat_2(A)
        & v1_rewrite1(A) )
     => ( v1_relat_1(A)
        & v3_rewrite1(A) ) ) ),
    file(rewrite1,cc3_rewrite1),
    []).

fof(cc5_rewrite1,axiom,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v3_rewrite1(A) )
     => ( v1_relat_1(A)
        & v2_rewrite1(A) ) ) ),
    file(rewrite1,cc5_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(d23_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v8_rewrite1(A)
      <=> ! [B,C] : 
            ( r2_rewrite1(A,B,C)
           => r5_rewrite1(A,B,C) ) ) ) ),
    file(rewrite1,d23_rewrite1),
    []).

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

fof(d28_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v10_rewrite1(B) )
         => ( m2_rewrite1(B,A)
          <=> ! [C,D] : 
                ( r2_rewrite1(A,C,D)
              <=> r5_rewrite1(B,C,D) ) ) ) ) ),
    file(rewrite1,d28_rewrite1),
    []).

fof(dt_m2_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( m2_rewrite1(B,A)
         => ( v1_relat_1(B)
            & v10_rewrite1(B) ) ) ) ),
    file(rewrite1,m2_rewrite1),
    []).

fof(existence_m2_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ? [B] : m2_rewrite1(B,A) ) ),
    file(rewrite1,m2_rewrite1),
    []).

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

fof(t38_rewrite1,axiom,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B,C] : 
          ( ( r5_rewrite1(A,B,C)
            | r6_rewrite1(A,B,C) )
         => r2_rewrite1(A,B,C) ) ) ),
    file(rewrite1,t38_rewrite1),
    []).