% Mizar problem: t44_gate_1,gate_1,564,21 
fof(t44_gate_1,conjecture,(
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1] : ~ ( ~ ( ~ v1_xboole_0(K)
          & v1_xboole_0(k7_gate_1(B,C)) )
      & ~ ( ~ v1_xboole_0(k7_gate_1(B,C))
          & v1_xboole_0(K) )
      & ~ ( ~ v1_xboole_0(L)
          & v1_xboole_0(k6_gate_1(B,C)) )
      & ~ ( ~ v1_xboole_0(k6_gate_1(B,C))
          & v1_xboole_0(L) )
      & ~ ( ~ v1_xboole_0(M)
          & v1_xboole_0(k34_gate_1(B,C)) )
      & ~ ( ~ v1_xboole_0(k34_gate_1(B,C))
          & v1_xboole_0(M) )
      & ~ ( ~ v1_xboole_0(N)
          & v1_xboole_0(k7_gate_1(D,E)) )
      & ~ ( ~ v1_xboole_0(k7_gate_1(D,E))
          & v1_xboole_0(N) )
      & ~ ( ~ v1_xboole_0(O)
          & v1_xboole_0(k6_gate_1(D,E)) )
      & ~ ( ~ v1_xboole_0(k6_gate_1(D,E))
          & v1_xboole_0(O) )
      & ~ ( ~ v1_xboole_0(P)
          & v1_xboole_0(k34_gate_1(D,E)) )
      & ~ ( ~ v1_xboole_0(k34_gate_1(D,E))
          & v1_xboole_0(P) )
      & ~ ( ~ v1_xboole_0(Q)
          & v1_xboole_0(k7_gate_1(F,G)) )
      & ~ ( ~ v1_xboole_0(k7_gate_1(F,G))
          & v1_xboole_0(Q) )
      & ~ ( ~ v1_xboole_0(R)
          & v1_xboole_0(k6_gate_1(F,G)) )
      & ~ ( ~ v1_xboole_0(k6_gate_1(F,G))
          & v1_xboole_0(R) )
      & ~ ( ~ v1_xboole_0(S)
          & v1_xboole_0(k34_gate_1(F,G)) )
      & ~ ( ~ v1_xboole_0(k34_gate_1(F,G))
          & v1_xboole_0(S) )
      & ~ ( ~ v1_xboole_0(T)
          & v1_xboole_0(k7_gate_1(H,I)) )
      & ~ ( ~ v1_xboole_0(k7_gate_1(H,I))
          & v1_xboole_0(T) )
      & ~ ( ~ v1_xboole_0(U)
          & v1_xboole_0(k6_gate_1(H,I)) )
      & ~ ( ~ v1_xboole_0(k6_gate_1(H,I))
          & v1_xboole_0(U) )
      & ~ ( ~ v1_xboole_0(V)
          & v1_xboole_0(k34_gate_1(H,I)) )
      & ~ ( ~ v1_xboole_0(k34_gate_1(H,I))
          & v1_xboole_0(V) )
      & ~ ( ~ v1_xboole_0(W)
          & v1_xboole_0(k1_gate_1(A)) )
      & ~ ( ~ v1_xboole_0(k1_gate_1(A))
          & v1_xboole_0(W) )
      & ~ ( ~ v1_xboole_0(X)
          & v1_xboole_0(k1_gate_1(W)) )
      & ~ ( ~ v1_xboole_0(k1_gate_1(W))
          & v1_xboole_0(X) )
      & ~ ( ~ v1_xboole_0(L1)
          & v1_xboole_0(k4_gate_1(X,M)) )
      & ~ ( ~ v1_xboole_0(k4_gate_1(X,M))
          & v1_xboole_0(L1) )
      & ~ ( ~ v1_xboole_0(Y)
          & v1_xboole_0(k2_gate_1(W,L)) )
      & ~ ( ~ v1_xboole_0(k2_gate_1(W,L))
          & v1_xboole_0(Y) )
      & ~ ( ~ v1_xboole_0(Z)
          & v1_xboole_0(k7_gate_1(Y,K)) )
      & ~ ( ~ v1_xboole_0(k7_gate_1(Y,K))
          & v1_xboole_0(Z) )
      & ~ ( ~ v1_xboole_0(M1)
          & v1_xboole_0(k4_gate_1(Z,P)) )
      & ~ ( ~ v1_xboole_0(k4_gate_1(Z,P))
          & v1_xboole_0(M1) )
      & ~ ( ~ v1_xboole_0(A1)
          & v1_xboole_0(k2_gate_1(K,O)) )
      & ~ ( ~ v1_xboole_0(k2_gate_1(K,O))
          & v1_xboole_0(A1) )
      & ~ ( ~ v1_xboole_0(B1)
          & v1_xboole_0(k8_gate_1(O,L,W)) )
      & ~ ( ~ v1_xboole_0(k8_gate_1(O,L,W))
          & v1_xboole_0(B1) )
      & ~ ( ~ v1_xboole_0(C1)
          & v1_xboole_0(k13_gate_1(A1,B1,N)) )
      & ~ ( ~ v1_xboole_0(k13_gate_1(A1,B1,N))
          & v1_xboole_0(C1) )
      & ~ ( ~ v1_xboole_0(N1)
          & v1_xboole_0(k4_gate_1(C1,S)) )
      & ~ ( ~ v1_xboole_0(k4_gate_1(C1,S))
          & v1_xboole_0(N1) )
      & ~ ( ~ v1_xboole_0(D1)
          & v1_xboole_0(k2_gate_1(N,R)) )
      & ~ ( ~ v1_xboole_0(k2_gate_1(N,R))
          & v1_xboole_0(D1) )
      & ~ ( ~ v1_xboole_0(E1)
          & v1_xboole_0(k8_gate_1(K,R,O)) )
      & ~ ( ~ v1_xboole_0(k8_gate_1(K,R,O))
          & v1_xboole_0(E1) )
      & ~ ( ~ v1_xboole_0(F1)
          & v1_xboole_0(k14_gate_1(R,O,L,W)) )
      & ~ ( ~ v1_xboole_0(k14_gate_1(R,O,L,W))
          & v1_xboole_0(F1) )
      & ~ ( ~ v1_xboole_0(G1)
          & v1_xboole_0(k17_gate_1(D1,E1,F1,Q)) )
      & ~ ( ~ v1_xboole_0(k17_gate_1(D1,E1,F1,Q))
          & v1_xboole_0(G1) )
      & ~ ( ~ v1_xboole_0(O1)
          & v1_xboole_0(k4_gate_1(G1,V)) )
      & ~ ( ~ v1_xboole_0(k4_gate_1(G1,V))
          & v1_xboole_0(O1) )
      & ~ ( ~ v1_xboole_0(H1)
          & v1_xboole_0(k2_gate_1(Q,U)) )
      & ~ ( ~ v1_xboole_0(k2_gate_1(Q,U))
          & v1_xboole_0(H1) )
      & ~ ( ~ v1_xboole_0(I1)
          & v1_xboole_0(k8_gate_1(N,U,R)) )
      & ~ ( ~ v1_xboole_0(k8_gate_1(N,U,R))
          & v1_xboole_0(I1) )
      & ~ ( ~ v1_xboole_0(J1)
          & v1_xboole_0(k14_gate_1(K,U,R,O)) )
      & ~ ( ~ v1_xboole_0(k14_gate_1(K,U,R,O))
          & v1_xboole_0(J1) )
      & ~ ( ~ v1_xboole_0(K1)
          & v1_xboole_0(k18_gate_1(U,R,O,L,W)) )
      & ~ ( ~ v1_xboole_0(k18_gate_1(U,R,O,L,W))
          & v1_xboole_0(K1) )
      & ~ ( ~ v1_xboole_0(J)
          & v1_xboole_0(k21_gate_1(T,H1,I1,J1,K1)) )
      & ~ ( ~ v1_xboole_0(k21_gate_1(T,H1,I1,J1,K1))
          & v1_xboole_0(J) )
      & ~ ( ~ ( ~ v1_xboole_0(L1)
              & v1_xboole_0(k10_gate_1(B,C,A)) )
          & ~ ( ~ v1_xboole_0(k10_gate_1(B,C,A))
              & v1_xboole_0(L1) )
          & ~ ( ~ v1_xboole_0(M1)
              & v1_xboole_0(k35_gate_1(B,C,D,E,A)) )
          & ~ ( ~ v1_xboole_0(k35_gate_1(B,C,D,E,A))
              & v1_xboole_0(M1) )
          & ~ ( ~ v1_xboole_0(N1)
              & v1_xboole_0(k37_gate_1(B,C,D,E,F,G,A)) )
          & ~ ( ~ v1_xboole_0(k37_gate_1(B,C,D,E,F,G,A))
              & v1_xboole_0(N1) )
          & ~ ( ~ v1_xboole_0(O1)
              & v1_xboole_0(k39_gate_1(B,C,D,E,F,G,H,I,A)) )
          & ~ ( ~ v1_xboole_0(k39_gate_1(B,C,D,E,F,G,H,I,A))
              & v1_xboole_0(O1) )
          & ~ ( ~ v1_xboole_0(J)
              & v1_xboole_0(k40_gate_1(B,C,D,E,F,G,H,I,A)) )
          & ~ ( ~ v1_xboole_0(k40_gate_1(B,C,D,E,F,G,H,I,A))
              & v1_xboole_0(J) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[antisymmetry_r2_hidden,d11_gate_1,d13_gate_1,d14_gate_1,d17_gate_1,d18_gate_1,d21_gate_1,d2_gate_1,d34_gate_1,d37_gate_1,d38_gate_1,d39_gate_1,d40_gate_1,d41_gate_1,d42_gate_1,d4_gate_1,d6_gate_1,d7_gate_1,d8_gate_1,dt_k10_gate_1,dt_k11_gate_1,dt_k13_gate_1,dt_k14_gate_1,dt_k17_gate_1,dt_k18_gate_1,dt_k1_gate_1,dt_k1_xboole_0,dt_k21_gate_1,dt_k2_gate_1,dt_k34_gate_1,dt_k35_gate_1,dt_k36_gate_1,dt_k37_gate_1,dt_k38_gate_1,dt_k39_gate_1,dt_k40_gate_1,dt_k4_gate_1,dt_k6_gate_1,dt_k7_gate_1,dt_k8_gate_1,fc1_xboole_0,rc1_xboole_0,rc2_xboole_0,t18_gate_1,t19_gate_1,t4_gate_1,t5_gate_1,t6_boole,t7_boole,t8_boole]),
    [file(gate_1,t44_gate_1)]).

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

fof(d11_gate_1,axiom,(
    ! [A,B,C] : 
      ( ( ~ ( ~ ( ~ v1_xboole_0(A)
                & ~ v1_xboole_0(B) )
            & ~ ( ~ v1_xboole_0(B)
                & ~ v1_xboole_0(C) )
            & ~ ( ~ v1_xboole_0(C)
                & ~ v1_xboole_0(A) ) )
       => k11_gate_1(A,B,C) = k1_gate_1(k1_xboole_0) )
      & ~ ( ~ ( ~ v1_xboole_0(A)
              & ~ v1_xboole_0(B) )
          & ~ ( ~ v1_xboole_0(B)
              & ~ v1_xboole_0(C) )
          & ~ ( ~ v1_xboole_0(C)
              & ~ v1_xboole_0(A) )
          & k11_gate_1(A,B,C) != k1_xboole_0 ) ) ),
    file(gate_1,d11_gate_1),
    []).

fof(d13_gate_1,axiom,(
    ! [A,B,C] : 
      ( ~ ( v1_xboole_0(A)
          & v1_xboole_0(B)
          & v1_xboole_0(C)
          & k13_gate_1(A,B,C) != k1_gate_1(k1_xboole_0) )
      & ( ~ ( v1_xboole_0(A)
            & v1_xboole_0(B)
            & v1_xboole_0(C) )
       => k13_gate_1(A,B,C) = k1_xboole_0 ) ) ),
    file(gate_1,d13_gate_1),
    []).

fof(d14_gate_1,axiom,(
    ! [A,B,C,D] : 
      ( ~ ( ~ v1_xboole_0(A)
          & ~ v1_xboole_0(B)
          & ~ v1_xboole_0(C)
          & ~ v1_xboole_0(D)
          & k14_gate_1(A,B,C,D) != k1_gate_1(k1_xboole_0) )
      & ( ~ ( ~ v1_xboole_0(A)
            & ~ v1_xboole_0(B)
            & ~ v1_xboole_0(C)
            & ~ v1_xboole_0(D) )
       => k14_gate_1(A,B,C,D) = k1_xboole_0 ) ) ),
    file(gate_1,d14_gate_1),
    []).

fof(d17_gate_1,axiom,(
    ! [A,B,C,D] : 
      ( ~ ( v1_xboole_0(A)
          & v1_xboole_0(B)
          & v1_xboole_0(C)
          & v1_xboole_0(D)
          & k17_gate_1(A,B,C,D) != k1_gate_1(k1_xboole_0) )
      & ( ~ ( v1_xboole_0(A)
            & v1_xboole_0(B)
            & v1_xboole_0(C)
            & v1_xboole_0(D) )
       => k17_gate_1(A,B,C,D) = k1_xboole_0 ) ) ),
    file(gate_1,d17_gate_1),
    []).

fof(d18_gate_1,axiom,(
    ! [A,B,C,D,E] : 
      ( ~ ( ~ v1_xboole_0(A)
          & ~ v1_xboole_0(B)
          & ~ v1_xboole_0(C)
          & ~ v1_xboole_0(D)
          & ~ v1_xboole_0(E)
          & k18_gate_1(A,B,C,D,E) != k1_gate_1(k1_xboole_0) )
      & ( ~ ( ~ v1_xboole_0(A)
            & ~ v1_xboole_0(B)
            & ~ v1_xboole_0(C)
            & ~ v1_xboole_0(D)
            & ~ v1_xboole_0(E) )
       => k18_gate_1(A,B,C,D,E) = k1_xboole_0 ) ) ),
    file(gate_1,d18_gate_1),
    []).

fof(d21_gate_1,axiom,(
    ! [A,B,C,D,E] : 
      ( ~ ( v1_xboole_0(A)
          & v1_xboole_0(B)
          & v1_xboole_0(C)
          & v1_xboole_0(D)
          & v1_xboole_0(E)
          & k21_gate_1(A,B,C,D,E) != k1_gate_1(k1_xboole_0) )
      & ( ~ ( v1_xboole_0(A)
            & v1_xboole_0(B)
            & v1_xboole_0(C)
            & v1_xboole_0(D)
            & v1_xboole_0(E) )
       => k21_gate_1(A,B,C,D,E) = k1_xboole_0 ) ) ),
    file(gate_1,d21_gate_1),
    []).

fof(d2_gate_1,axiom,(
    ! [A,B] : 
      ( ~ ( ~ v1_xboole_0(A)
          & ~ v1_xboole_0(B)
          & k2_gate_1(A,B) != k1_gate_1(k1_xboole_0) )
      & ( ~ ( ~ v1_xboole_0(A)
            & ~ v1_xboole_0(B) )
       => k2_gate_1(A,B) = k1_xboole_0 ) ) ),
    file(gate_1,d2_gate_1),
    []).

fof(d34_gate_1,axiom,(
    ! [A,B] : 
      ( ~ ( ~ ( v1_xboole_0(A)
              & v1_xboole_0(B) )
          & ~ ( ~ v1_xboole_0(A)
              & ~ v1_xboole_0(B) )
          & k34_gate_1(A,B) != k1_gate_1(k1_xboole_0) )
      & ( ~ ( ~ ( v1_xboole_0(A)
                & v1_xboole_0(B) )
            & ~ ( ~ v1_xboole_0(A)
                & ~ v1_xboole_0(B) ) )
       => k34_gate_1(A,B) = k1_xboole_0 ) ) ),
    file(gate_1,d34_gate_1),
    []).

fof(d37_gate_1,axiom,(
    ! [A,B,C,D,E] : k35_gate_1(A,B,C,D,E) = k10_gate_1(C,D,k11_gate_1(A,B,E)) ),
    file(gate_1,d37_gate_1),
    []).

fof(d38_gate_1,axiom,(
    ! [A,B,C,D,E] : k36_gate_1(A,B,C,D,E) = k11_gate_1(C,D,k11_gate_1(A,B,E)) ),
    file(gate_1,d38_gate_1),
    []).

fof(d39_gate_1,axiom,(
    ! [A,B,C,D,E,F,G] : k37_gate_1(A,B,C,D,E,F,G) = k10_gate_1(E,F,k36_gate_1(A,B,C,D,G)) ),
    file(gate_1,d39_gate_1),
    []).

fof(d40_gate_1,axiom,(
    ! [A,B,C,D,E,F,G] : k38_gate_1(A,B,C,D,E,F,G) = k11_gate_1(E,F,k36_gate_1(A,B,C,D,G)) ),
    file(gate_1,d40_gate_1),
    []).

fof(d41_gate_1,axiom,(
    ! [A,B,C,D,E,F,G,H,I] : k39_gate_1(A,B,C,D,E,F,G,H,I) = k10_gate_1(G,H,k38_gate_1(A,B,C,D,E,F,I)) ),
    file(gate_1,d41_gate_1),
    []).

fof(d42_gate_1,axiom,(
    ! [A,B,C,D,E,F,G,H,I] : k40_gate_1(A,B,C,D,E,F,G,H,I) = k11_gate_1(G,H,k38_gate_1(A,B,C,D,E,F,I)) ),
    file(gate_1,d42_gate_1),
    []).

fof(d4_gate_1,axiom,(
    ! [A,B] : 
      ( ( ( ( ~ v1_xboole_0(A)
            & v1_xboole_0(B) )
          | ( v1_xboole_0(A)
            & ~ v1_xboole_0(B) ) )
       => k4_gate_1(A,B) = k1_gate_1(k1_xboole_0) )
      & ~ ( ~ ( ~ v1_xboole_0(A)
              & v1_xboole_0(B) )
          & ~ ( v1_xboole_0(A)
              & ~ v1_xboole_0(B) )
          & k4_gate_1(A,B) != k1_xboole_0 ) ) ),
    file(gate_1,d4_gate_1),
    []).

fof(d6_gate_1,axiom,(
    ! [A,B] : 
      ( ( ~ ( ~ v1_xboole_0(A)
            & ~ v1_xboole_0(B) )
       => k6_gate_1(A,B) = k1_gate_1(k1_xboole_0) )
      & ~ ( ~ v1_xboole_0(A)
          & ~ v1_xboole_0(B)
          & k6_gate_1(A,B) != k1_xboole_0 ) ) ),
    file(gate_1,d6_gate_1),
    []).

fof(d7_gate_1,axiom,(
    ! [A,B] : 
      ( ~ ( v1_xboole_0(A)
          & v1_xboole_0(B)
          & k7_gate_1(A,B) != k1_gate_1(k1_xboole_0) )
      & ( ~ ( v1_xboole_0(A)
            & v1_xboole_0(B) )
       => k7_gate_1(A,B) = k1_xboole_0 ) ) ),
    file(gate_1,d7_gate_1),
    []).

fof(d8_gate_1,axiom,(
    ! [A,B,C] : 
      ( ~ ( ~ v1_xboole_0(A)
          & ~ v1_xboole_0(B)
          & ~ v1_xboole_0(C)
          & k8_gate_1(A,B,C) != k1_gate_1(k1_xboole_0) )
      & ( ~ ( ~ v1_xboole_0(A)
            & ~ v1_xboole_0(B)
            & ~ v1_xboole_0(C) )
       => k8_gate_1(A,B,C) = k1_xboole_0 ) ) ),
    file(gate_1,d8_gate_1),
    []).

fof(dt_k10_gate_1,axiom,(
    $true ),
    file(gate_1,k10_gate_1),
    []).

fof(dt_k11_gate_1,axiom,(
    $true ),
    file(gate_1,k11_gate_1),
    []).

fof(dt_k13_gate_1,axiom,(
    $true ),
    file(gate_1,k13_gate_1),
    []).

fof(dt_k14_gate_1,axiom,(
    $true ),
    file(gate_1,k14_gate_1),
    []).

fof(dt_k17_gate_1,axiom,(
    $true ),
    file(gate_1,k17_gate_1),
    []).

fof(dt_k18_gate_1,axiom,(
    $true ),
    file(gate_1,k18_gate_1),
    []).

fof(dt_k1_gate_1,axiom,(
    $true ),
    file(gate_1,k1_gate_1),
    []).

fof(dt_k1_xboole_0,axiom,(
    $true ),
    file(xboole_0,k1_xboole_0),
    []).

fof(dt_k21_gate_1,axiom,(
    $true ),
    file(gate_1,k21_gate_1),
    []).

fof(dt_k2_gate_1,axiom,(
    $true ),
    file(gate_1,k2_gate_1),
    []).

fof(dt_k34_gate_1,axiom,(
    $true ),
    file(gate_1,k34_gate_1),
    []).

fof(dt_k35_gate_1,axiom,(
    $true ),
    file(gate_1,k35_gate_1),
    []).

fof(dt_k36_gate_1,axiom,(
    $true ),
    file(gate_1,k36_gate_1),
    []).

fof(dt_k37_gate_1,axiom,(
    $true ),
    file(gate_1,k37_gate_1),
    []).

fof(dt_k38_gate_1,axiom,(
    $true ),
    file(gate_1,k38_gate_1),
    []).

fof(dt_k39_gate_1,axiom,(
    $true ),
    file(gate_1,k39_gate_1),
    []).

fof(dt_k40_gate_1,axiom,(
    $true ),
    file(gate_1,k40_gate_1),
    []).

fof(dt_k4_gate_1,axiom,(
    $true ),
    file(gate_1,k4_gate_1),
    []).

fof(dt_k6_gate_1,axiom,(
    $true ),
    file(gate_1,k6_gate_1),
    []).

fof(dt_k7_gate_1,axiom,(
    $true ),
    file(gate_1,k7_gate_1),
    []).

fof(dt_k8_gate_1,axiom,(
    $true ),
    file(gate_1,k8_gate_1),
    []).

fof(fc1_xboole_0,axiom,(
    v1_xboole_0(k1_xboole_0) ),
    file(xboole_0,fc1_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(t18_gate_1,axiom,(
    ! [A,B,C] : 
      ( ~ ( ~ v1_xboole_0(k10_gate_1(A,B,C))
          & ~ ( ( ( ~ v1_xboole_0(A)
                  & v1_xboole_0(B) )
                | ( v1_xboole_0(A)
                  & ~ v1_xboole_0(B) ) )
              & v1_xboole_0(C) )
          & ~ ( ~ ( ~ v1_xboole_0(A)
                  & v1_xboole_0(B) )
              & ~ ( v1_xboole_0(A)
                  & ~ v1_xboole_0(B) )
              & ~ v1_xboole_0(C) ) )
      & ~ ( ( ( ( ( ~ v1_xboole_0(A)
                  & v1_xboole_0(B) )
                | ( v1_xboole_0(A)
                  & ~ v1_xboole_0(B) ) )
              & v1_xboole_0(C) )
            | ( ~ ( ~ v1_xboole_0(A)
                  & v1_xboole_0(B) )
              & ~ ( v1_xboole_0(A)
                  & ~ v1_xboole_0(B) )
              & ~ v1_xboole_0(C) ) )
          & v1_xboole_0(k10_gate_1(A,B,C)) ) ) ),
    file(gate_1,t18_gate_1),
    []).

fof(t19_gate_1,axiom,(
    ! [A,B,C] : 
      ( ~ ( ~ v1_xboole_0(k11_gate_1(A,B,C))
          & ~ ( ~ v1_xboole_0(A)
              & ~ v1_xboole_0(B) )
          & ~ ( ~ v1_xboole_0(B)
              & ~ v1_xboole_0(C) )
          & ~ ( ~ v1_xboole_0(C)
              & ~ v1_xboole_0(A) ) )
      & ~ ( ~ ( ~ ( ~ v1_xboole_0(A)
                  & ~ v1_xboole_0(B) )
              & ~ ( ~ v1_xboole_0(B)
                  & ~ v1_xboole_0(C) )
              & ~ ( ~ v1_xboole_0(C)
                  & ~ v1_xboole_0(A) ) )
          & v1_xboole_0(k11_gate_1(A,B,C)) ) ) ),
    file(gate_1,t19_gate_1),
    []).

fof(t4_gate_1,axiom,(
    ! [A] : 
      ( ~ v1_xboole_0(k1_gate_1(A))
    <=> v1_xboole_0(A) ) ),
    file(gate_1,t4_gate_1),
    []).

fof(t5_gate_1,axiom,(
    ~ v1_xboole_0(k1_gate_1(k1_xboole_0)) ),
    file(gate_1,t5_gate_1),
    []).

fof(t6_boole,axiom,(
    ! [A] : 
      ( v1_xboole_0(A)
     => A = k1_xboole_0 ) ),
    file(boole,t6_boole),
    []).

fof(t7_boole,axiom,(
    ! [A,B] : ~ ( r2_hidden(A,B)
      & v1_xboole_0(B) ) ),
    file(boole,t7_boole),
    []).

fof(t8_boole,axiom,(
    ! [A,B] : ~ ( v1_xboole_0(A)
      & A != B
      & v1_xboole_0(B) ) ),
    file(boole,t8_boole),
    []).