% Mizar problem: t127_zfmisc_1,zfmisc_1,1605,65 
fof(t127_zfmisc_1,conjecture,(
    ! [A,B,C,D] : 
      ( ( r1_xboole_0(A,B)
        | r1_xboole_0(C,D) )
     => r1_xboole_0(k2_zfmisc_1(A,C),k2_zfmisc_1(B,D)) ) ),
    inference(mizar_bg_added,[status(thm)],[antisymmetry_r2_hidden,commutativity_k2_tarski,commutativity_k3_xboole_0,d5_tarski,dt_k1_tarski,dt_k2_tarski,dt_k2_zfmisc_1,dt_k3_xboole_0,dt_k4_tarski,fc1_zfmisc_1,idempotence_k3_xboole_0,rc1_xboole_0,rc2_xboole_0,symmetry_r1_xboole_0,t104_zfmisc_1,t4_xboole_0]),
    [file(zfmisc_1,t127_zfmisc_1)]).

fof(antisymmetry_r2_hidden,axiom,(
    ! [A,B] : 
      ( r2_hidden(A,B)
     => ~ r2_hidden(B,A) ) ),
    file(hidden,r2_hidden),
    []).

fof(commutativity_k2_tarski,axiom,(
    ! [A,B] : k2_tarski(A,B) = k2_tarski(B,A) ),
    file(tarski,k2_tarski),
    []).

fof(commutativity_k3_xboole_0,axiom,(
    ! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A) ),
    file(xboole_0,k3_xboole_0),
    []).

fof(d5_tarski,axiom,(
    ! [A,B] : k4_tarski(A,B) = k2_tarski(k2_tarski(A,B),k1_tarski(A)) ),
    file(tarski,d5_tarski),
    []).

fof(dt_k1_tarski,axiom,(
    $true ),
    file(tarski,k1_tarski),
    []).

fof(dt_k2_tarski,axiom,(
    $true ),
    file(tarski,k2_tarski),
    []).

fof(dt_k2_zfmisc_1,axiom,(
    $true ),
    file(zfmisc_1,k2_zfmisc_1),
    []).

fof(dt_k3_xboole_0,axiom,(
    $true ),
    file(xboole_0,k3_xboole_0),
    []).

fof(dt_k4_tarski,axiom,(
    $true ),
    file(tarski,k4_tarski),
    []).

fof(fc1_zfmisc_1,axiom,(
    ! [A,B] : ~ v1_xboole_0(k4_tarski(A,B)) ),
    file(zfmisc_1,fc1_zfmisc_1),
    []).

fof(idempotence_k3_xboole_0,axiom,(
    ! [A,B] : k3_xboole_0(A,A) = A ),
    file(xboole_0,k3_xboole_0),
    []).

fof(rc1_xboole_0,axiom,(
    ? [A] : v1_xboole_0(A) ),
    file(xboole_0,rc1_xboole_0),
    []).

fof(rc2_xboole_0,axiom,(
    ? [A] : ~ v1_xboole_0(A) ),
    file(xboole_0,rc2_xboole_0),
    []).

fof(symmetry_r1_xboole_0,axiom,(
    ! [A,B] : 
      ( r1_xboole_0(A,B)
     => r1_xboole_0(B,A) ) ),
    file(xboole_0,r1_xboole_0),
    []).

fof(t104_zfmisc_1,axiom,(
    ! [A,B,C,D,E] : ~ ( r2_hidden(A,k3_xboole_0(k2_zfmisc_1(B,C),k2_zfmisc_1(D,E)))
      & ! [F,G] : ~ ( A = k4_tarski(F,G)
          & r2_hidden(F,k3_xboole_0(B,D))
          & r2_hidden(G,k3_xboole_0(C,E)) ) ) ),
    file(zfmisc_1,t104_zfmisc_1),
    []).

fof(t4_xboole_0,axiom,(
    ! [A,B] : 
      ( ~ ( ~ r1_xboole_0(A,B)
          & ! [C] : ~ r2_hidden(C,k3_xboole_0(A,B)) )
      & ~ ( ? [C] : r2_hidden(C,k3_xboole_0(A,B))
          & r1_xboole_0(A,B) ) ) ),
    file(xboole_0,t4_xboole_0),
    []).