fof(t142_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => r1_partfun1(k3_partfun1(k1_xboole_0,A,B),C) ) ),
    inference(mizar_proof,[status(thm)],[t91_partfun1,t141_partfun1]),
    [file(partfun1,t142_partfun1),interesting(1.00)]).

fof(t91_partfun1,theorem,(
    ! [A,B] : k3_partfun1(k1_xboole_0,A,B) = k1_xboole_0 ),
    inference(mizar_proof,[status(thm)],[t2_xboole_1,t85_partfun1]),
    [file(partfun1,t91_partfun1),interesting(0.93)]).

fof(t87_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => k3_partfun1(C,A,B) = C ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,t85_partfun1]),
    [file(partfun1,t87_partfun1),interesting(0.91)]).

fof(t95_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( v2_funct_1(C)
       => k2_funct_1(k3_partfun1(C,A,B)) = k3_partfun1(k2_funct_1(C),B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[t94_partfun1,t55_funct_1,d5_funct_1,t77_partfun1,t80_partfun1,t78_partfun1,t54_funct_1,t78_partfun1,t77_partfun1,t55_funct_1,d5_funct_1,t56_funct_1,t78_partfun1,t78_partfun1,t80_partfun1,d5_funct_1,t55_funct_1,t2_tarski,t77_partfun1,t55_funct_1,d5_funct_1,t56_funct_1,t78_partfun1,t78_partfun1,t80_partfun1,t56_funct_1,t80_partfun1,t9_funct_1]),
    [file(partfun1,t95_partfun1),interesting(0.91)]).

fof(t141_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => r1_partfun1(k1_xboole_0,A) ) ),
    inference(mizar_proof,[status(thm)],[t130_partfun1]),
    [file(partfun1,t141_partfun1),interesting(0.89)]).

fof(t92_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_relat_1(D)
        & v1_funct_1(D) )
     => ! [E] : 
          ( ( v1_relat_1(E)
            & v1_funct_1(E) )
         => r1_tarski(k1_partfun1(C,A,A,B,k3_partfun1(D,C,A),k3_partfun1(E,A,B)),k3_partfun1(k5_relat_1(D,E),C,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t21_funct_1,t78_partfun1,t80_partfun1,t78_partfun1,t21_funct_1,t23_funct_1,t78_partfun1,t21_funct_1,t78_partfun1,t80_partfun1,t78_partfun1,t21_funct_1,t23_funct_1,t78_partfun1,t22_funct_1,t80_partfun1,t80_partfun1,t23_funct_1,t80_partfun1,t8_grfunc_1]),
    [file(partfun1,t92_partfun1),interesting(0.87)]).

fof(t125_partfun1,theorem,(
    ! [A,B,C] : 
      ( r1_tarski(A,B)
     => r1_tarski(k4_partfun1(A,C),k4_partfun1(B,C)) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t120_partfun1,t30_partfun1,t119_partfun1]),
    [file(partfun1,t125_partfun1),interesting(0.86)]).

fof(t146_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => r1_partfun1(k7_relat_1(k8_relat_1(A,C),B),C) ) ),
    inference(mizar_proof,[status(thm)],[t88_relat_1,t117_relat_1,t1_xboole_1,t131_partfun1]),
    [file(partfun1,t146_partfun1),interesting(0.86)]).

fof(t83_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_relat_1(D)
        & v1_funct_1(D) )
     => ( r1_tarski(A,B)
       => r1_tarski(k3_partfun1(D,C,A),k3_partfun1(D,C,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t78_partfun1,t78_partfun1,t78_partfun1,t80_partfun1,t80_partfun1,t8_grfunc_1]),
    [file(partfun1,t83_partfun1),interesting(0.85)]).

fof(t144_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => r1_partfun1(k7_relat_1(B,A),B) ) ),
    inference(mizar_proof,[status(thm)],[t88_relat_1,t131_partfun1]),
    [file(partfun1,t144_partfun1),interesting(0.84)]).

fof(t145_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => r1_partfun1(k8_relat_1(A,B),B) ) ),
    inference(mizar_proof,[status(thm)],[t117_relat_1,t131_partfun1]),
    [file(partfun1,t145_partfun1),interesting(0.84)]).

fof(t147_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => r1_partfun1(k3_partfun1(C,A,B),C) ) ),
    inference(mizar_proof,[status(thm)],[t146_partfun1]),
    [file(partfun1,t147_partfun1),interesting(0.84)]).

fof(t82_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_relat_1(D)
        & v1_funct_1(D) )
     => ( r1_tarski(A,B)
       => r1_tarski(k3_partfun1(D,A,C),k3_partfun1(D,B,C)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t78_partfun1,t78_partfun1,t80_partfun1,t80_partfun1,t8_grfunc_1]),
    [file(partfun1,t82_partfun1),interesting(0.84)]).

fof(t162_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,B) )
         => ~ ( ( B = k1_xboole_0
               => A = k1_xboole_0 )
              & r1_partfun1(C,D)
              & ! [E] : 
                  ( ( v1_funct_1(E)
                    & m2_relset_1(E,A,B) )
                 => ~ ( v1_partfun1(E,A,B)
                      & r1_partfun1(C,E)
                      & r1_partfun1(D,E) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t112_partfun1,t142_partfun1,d3_xboole_0,d6_partfun1,s2_funct_1,d6_partfun1,d3_xboole_0,d6_partfun1,d3_xboole_0,d3_tarski,d5_funct_1,t27_partfun1,t27_partfun1,t27_partfun1,l13_partfun1,d4_partfun1]),
    [file(partfun1,t162_partfun1),interesting(0.82)]).

fof(t84_partfun1,theorem,(
    ! [A,B,C,D,E] : 
      ( ( v1_relat_1(E)
        & v1_funct_1(E) )
     => ( ( r1_tarski(A,B)
          & r1_tarski(C,D) )
       => r1_tarski(k3_partfun1(E,A,C),k3_partfun1(E,B,D)) ) ) ),
    inference(mizar_proof,[status(thm)],[t82_partfun1,t83_partfun1,t1_xboole_1]),
    [file(partfun1,t84_partfun1),interesting(0.82)]).

fof(t64_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,A,k1_xboole_0) )
     => B = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[t62_partfun1,l4_partfun1,t9_funct_1]),
    [file(partfun1,t64_partfun1),interesting(0.80)]).

fof(t30_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ( r1_tarski(A,C)
       => ( v1_funct_1(D)
          & m2_relset_1(D,C,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,t1_xboole_1,l13_partfun1]),
    [file(partfun1,t30_partfun1),interesting(0.79)]).

fof(t31_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ( r1_tarski(B,C)
       => ( v1_funct_1(D)
          & m2_relset_1(D,A,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,t1_xboole_1,l13_partfun1]),
    [file(partfun1,t31_partfun1),interesting(0.79)]).

fof(t86_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => A = k3_partfun1(A,k1_relat_1(A),k2_relat_1(A)) ) ),
    inference(mizar_proof,[status(thm)],[t85_partfun1]),
    [file(partfun1,t86_partfun1),interesting(0.79)]).

fof(t32_partfun1,theorem,(
    ! [A,B,C,D,E] : 
      ( ( v1_funct_1(E)
        & m2_relset_1(E,A,B) )
     => ( ( r1_tarski(A,C)
          & r1_tarski(B,D) )
       => ( v1_funct_1(E)
          & m2_relset_1(E,C,D) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,t1_xboole_1,l13_partfun1]),
    [file(partfun1,t32_partfun1),interesting(0.78)]).

fof(t131_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_partfun1(A,B)
          <=> ? [C] : 
                ( v1_relat_1(C)
                & v1_funct_1(C)
                & r1_tarski(A,C)
                & r1_tarski(B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_xboole_1,t6_grfunc_1,t7_xboole_1,t130_partfun1]),
    [file(partfun1,t131_partfun1),interesting(0.78)]).

fof(t85_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( ( r1_tarski(k1_relat_1(C),A)
          & r1_tarski(k2_relat_1(C),B) )
       => C = k3_partfun1(C,A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d5_funct_1,t78_partfun1,t77_partfun1,d10_xboole_0,t80_partfun1,t9_funct_1]),
    [file(partfun1,t85_partfun1),interesting(0.78)]).

fof(t120_partfun1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(C,k4_partfun1(A,B))
     => ( v1_funct_1(C)
        & m2_relset_1(C,A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_partfun1,l13_partfun1]),
    [file(partfun1,t120_partfun1),interesting(0.77)]).

fof(t57_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k1_xboole_0,A) )
     => B = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[t54_partfun1,l4_partfun1,t9_funct_1]),
    [file(partfun1,t57_partfun1),interesting(0.77)]).

fof(t119_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => r2_hidden(C,k4_partfun1(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,d5_partfun1]),
    [file(partfun1,t119_partfun1),interesting(0.77)]).

fof(t123_partfun1,theorem,(
    ! [A] : k4_partfun1(A,k1_xboole_0) = k1_tarski(k1_xboole_0) ),
    inference(mizar_proof,[status(thm)],[t120_partfun1,t64_partfun1,l4_partfun1,t55_partfun1,t119_partfun1,d1_tarski]),
    [file(partfun1,t123_partfun1),interesting(0.77)]).

fof(t127_partfun1,theorem,(
    ! [A,B,C] : 
      ( r1_tarski(A,B)
     => r1_tarski(k4_partfun1(C,A),k4_partfun1(C,B)) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t120_partfun1,t31_partfun1,t119_partfun1]),
    [file(partfun1,t127_partfun1),interesting(0.77)]).

fof(l12_partfun1,theorem,(
    ! [A,B] : 
    ? [C] : 
      ( r1_tarski(k1_relat_1(C),A)
      & r1_tarski(k2_relat_1(C),B) ) ),
    inference(mizar_proof,[status(thm)],[t2_xboole_1]),
    [file(partfun1,l12_partfun1),interesting(0.76)]).

fof(t76_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => r1_tarski(k3_partfun1(C,A,B),C) ) ),
    inference(mizar_proof,[status(thm)],[t88_relat_1,t117_relat_1,t1_xboole_1]),
    [file(partfun1,t76_partfun1),interesting(0.76)]).

fof(t122_partfun1,theorem,(
    ! [A] : k4_partfun1(k1_xboole_0,A) = k1_tarski(k1_xboole_0) ),
    inference(mizar_proof,[status(thm)],[t120_partfun1,t57_partfun1,l4_partfun1,t55_partfun1,t119_partfun1,d1_tarski]),
    [file(partfun1,t122_partfun1),interesting(0.76)]).

fof(t126_partfun1,theorem,(
    ! [A,B] : r1_tarski(k4_partfun1(k1_xboole_0,A),k4_partfun1(B,A)) ),
    inference(mizar_proof,[status(thm)],[t2_xboole_1,t125_partfun1]),
    [file(partfun1,t126_partfun1),interesting(0.76)]).

fof(t135_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_tarski(A,B)
           => r1_partfun1(A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t131_partfun1]),
    [file(partfun1,t135_partfun1),interesting(0.76)]).

fof(t128_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(C,D) )
     => r1_tarski(k4_partfun1(A,C),k4_partfun1(B,D)) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t120_partfun1,t32_partfun1,t119_partfun1]),
    [file(partfun1,t128_partfun1),interesting(0.75)]).

fof(t1_partfun1,theorem,(
    ! [A,B,C,D,E,F] : 
      ( ( r1_tarski(A,k2_zfmisc_1(B,C))
        & r1_tarski(D,k2_zfmisc_1(E,F)) )
     => r1_tarski(k2_xboole_0(A,D),k2_zfmisc_1(k2_xboole_0(B,E),k2_xboole_0(C,F))) ) ),
    inference(mizar_proof,[status(thm)],[t7_xboole_1,t119_zfmisc_1,t13_xboole_1,t13_xboole_1,t1_xboole_1]),
    [file(partfun1,t1_partfun1),interesting(0.75)]).

fof(l199_partfun1,theorem,(
    ! [A] : m2_relset_1(k6_relat_1(A),A,A) ),
    inference(mizar_proof,[status(thm)],[t71_relat_1,t11_relset_1]),
    [file(partfun1,l199_partfun1),interesting(0.74)]).

fof(t130_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_partfun1(A,B)
          <=> ? [C] : 
                ( v1_relat_1(C)
                & v1_funct_1(C)
                & k2_xboole_0(A,B) = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_partfun1,t3_partfun1,d6_partfun1]),
    [file(partfun1,t130_partfun1),interesting(0.74)]).

fof(t112_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k1_xboole_0,A) )
     => v1_partfun1(B,k1_xboole_0,A) ) ),
    inference(mizar_proof,[status(thm)],[t54_partfun1,d4_partfun1]),
    [file(partfun1,t112_partfun1),interesting(0.74)]).

fof(t66_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,A,k1_xboole_0) )
     => v2_funct_1(B) ) ),
    inference(mizar_proof,[status(thm)],[t64_partfun1]),
    [file(partfun1,t66_partfun1),interesting(0.74)]).

fof(t94_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( v2_funct_1(C)
       => v2_funct_1(k3_partfun1(C,A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t99_funct_1,t84_funct_1]),
    [file(partfun1,t94_partfun1),interesting(0.74)]).

fof(t175_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k1_xboole_0,A) )
     => k5_partfun1(k1_xboole_0,A,B) = k1_tarski(B) ) ),
    inference(mizar_proof,[status(thm)],[t112_partfun1,t174_partfun1]),
    [file(partfun1,t175_partfun1),interesting(0.73)]).

fof(t186_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,B) )
         => ~ ( ( B = k1_xboole_0
               => A = k1_xboole_0 )
              & r1_partfun1(C,D)
              & r1_xboole_0(k5_partfun1(A,B,C),k5_partfun1(A,B,D)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t162_partfun1,d7_partfun1,d3_xboole_0,d7_xboole_0]),
    [file(partfun1,t186_partfun1),interesting(0.73)]).

fof(t56_partfun1,theorem,(
    ! [A,B] : 
      ( v1_funct_1(k1_xboole_0)
      & m2_relset_1(k1_xboole_0,A,B) ) ),
    inference(mizar_proof,[status(thm)],[l4_partfun1,t55_partfun1]),
    [file(partfun1,t56_partfun1),interesting(0.73)]).

fof(t174_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ( v1_partfun1(C,A,B)
      <=> k5_partfun1(A,B,C) = k1_tarski(C) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_partfun1,t148_partfun1,d7_partfun1,d1_tarski,d1_tarski,t169_partfun1]),
    [file(partfun1,t174_partfun1),interesting(0.72)]).

fof(t81_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ! [D] : 
          ( ( v1_relat_1(D)
            & v1_funct_1(D) )
         => ( r1_tarski(C,D)
           => r1_tarski(k3_partfun1(C,A,B),k3_partfun1(D,A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t77_partfun1,d3_tarski,t25_relat_1,t78_partfun1,t8_grfunc_1,t78_partfun1,t80_partfun1,t8_grfunc_1,t8_grfunc_1]),
    [file(partfun1,t81_partfun1),interesting(0.72)]).

fof(t27_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ( r2_hidden(C,k4_relset_1(A,B,D))
       => r2_hidden(k1_funct_1(D,C),B) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,d5_funct_1]),
    [file(partfun1,t27_partfun1),interesting(0.71)]).

fof(t168_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( r2_hidden(D,k5_partfun1(A,B,C))
         => ( v1_funct_1(D)
            & m2_relset_1(D,A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_partfun1]),
    [file(partfun1,t168_partfun1),interesting(0.71)]).

fof(l13_partfun1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( m2_relset_1(C,A,B)
      <=> ( r1_tarski(k1_relat_1(C),A)
          & r1_tarski(k2_relat_1(C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_relset_1,t12_relset_1]),
    [file(partfun1,l13_partfun1),interesting(0.70)]).

fof(t148_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,B) )
         => ( ( v1_partfun1(C,A,B)
              & v1_partfun1(D,A,B)
              & r1_partfun1(C,D) )
           => C = D ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_partfun1,t136_partfun1]),
    [file(partfun1,t148_partfun1),interesting(0.70)]).

fof(t59_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k1_xboole_0,A) )
     => v2_funct_1(B) ) ),
    inference(mizar_proof,[status(thm)],[t57_partfun1]),
    [file(partfun1,t59_partfun1),interesting(0.70)]).

fof(t121_partfun1,theorem,(
    ! [A,B,C] : 
      ( m1_subset_1(C,k4_partfun1(A,B))
     => ( v1_funct_1(C)
        & m2_relset_1(C,A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t120_partfun1]),
    [file(partfun1,t121_partfun1),interesting(0.69)]).

fof(t139_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C) )
             => ( ( r1_tarski(A,C)
                  & r1_tarski(B,C) )
               => r1_partfun1(A,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t131_partfun1]),
    [file(partfun1,t139_partfun1),interesting(0.69)]).

fof(t136_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( ( k1_relat_1(A) = k1_relat_1(B)
              & r1_partfun1(A,B) )
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t132_partfun1,t9_funct_1]),
    [file(partfun1,t136_partfun1),interesting(0.69)]).

fof(t158_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,B) )
         => ! [E] : 
              ( ( v1_funct_1(E)
                & m2_relset_1(E,A,B) )
             => ( ( r1_partfun1(C,E)
                  & r1_partfun1(D,E)
                  & v1_partfun1(E,A,B) )
               => r1_partfun1(C,D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_partfun1,d6_partfun1,d3_xboole_0,d3_xboole_0,d6_partfun1]),
    [file(partfun1,t158_partfun1),interesting(0.69)]).

fof(t113_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( v1_partfun1(k3_partfun1(C,A,B),A,B)
       => r1_tarski(A,k1_relat_1(C)) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_partfun1,d3_tarski,t77_partfun1]),
    [file(partfun1,t113_partfun1),interesting(0.68)]).

fof(t55_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( k1_relat_1(C) = k1_xboole_0
       => ( v1_funct_1(C)
          & m2_relset_1(C,A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t65_relat_1,t2_xboole_1,l13_partfun1]),
    [file(partfun1,t55_partfun1),interesting(0.68)]).

fof(t114_partfun1,theorem,(
    ! [A,B] : 
      ( v1_partfun1(k3_partfun1(k1_xboole_0,A,B),A,B)
     => A = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[l4_partfun1,t113_partfun1,t3_xboole_1]),
    [file(partfun1,t114_partfun1),interesting(0.67)]).

fof(t116_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( v1_partfun1(k3_partfun1(C,A,B),A,B)
       => r1_tarski(k9_relat_1(C,A),B) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_partfun1,d3_tarski,d12_funct_1,l13_partfun1,t80_partfun1,d5_funct_1]),
    [file(partfun1,t116_partfun1),interesting(0.67)]).

fof(t138_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_xboole_0(k1_relat_1(A),k1_relat_1(B))
           => r1_partfun1(A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t31_grfunc_1,t130_partfun1]),
    [file(partfun1,t138_partfun1),interesting(0.67)]).

fof(t169_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,B) )
         => ( r2_hidden(D,k5_partfun1(A,B,C))
           => v1_partfun1(D,A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_partfun1]),
    [file(partfun1,t169_partfun1),interesting(0.67)]).

fof(t33_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,B) )
         => ( r1_tarski(C,D)
           => ( v1_funct_1(C)
              & m2_relset_1(C,A,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,t25_relat_1,t1_xboole_1,l13_partfun1]),
    [file(partfun1,t33_partfun1),interesting(0.67)]).

fof(t43_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ( v1_funct_1(k8_relset_1(A,B,D,C))
        & m2_relset_1(k8_relset_1(A,B,D,C),C,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t87_relat_1,l13_partfun1,l13_partfun1]),
    [file(partfun1,t43_partfun1),interesting(0.67)]).

fof(t53_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => k10_relat_1(C,B) = k4_relset_1(A,B,C) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,t178_relat_1,t167_relat_1,t169_relat_1,d10_xboole_0]),
    [file(partfun1,t53_partfun1),interesting(0.67)]).

fof(t45_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ( v1_funct_1(k9_relset_1(A,B,C,D))
        & m2_relset_1(k9_relset_1(A,B,C,D),A,C) ) ) ),
    inference(mizar_proof,[status(thm)],[t116_relat_1,l13_partfun1]),
    [file(partfun1,t45_partfun1),interesting(0.66)]).

fof(t65_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,k1_xboole_0) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,B,k1_xboole_0) )
         => C = D ) ) ),
    inference(mizar_proof,[status(thm)],[t64_partfun1]),
    [file(partfun1,t65_partfun1),interesting(0.66)]).

fof(t93_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_relat_1(D)
        & v1_funct_1(D) )
     => ! [E] : 
          ( ( v1_relat_1(E)
            & v1_funct_1(E) )
         => ( r1_tarski(k3_xboole_0(k2_relat_1(D),k1_relat_1(E)),A)
           => k1_partfun1(C,A,A,B,k3_partfun1(D,C,A),k3_partfun1(E,A,B)) = k3_partfun1(k5_relat_1(D,E),C,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t92_partfun1,d3_tarski,t78_partfun1,t21_funct_1,t22_funct_1,d5_funct_1,d3_xboole_0,t78_partfun1,t79_partfun1,t21_funct_1,t78_partfun1,t21_funct_1,t22_funct_1,d5_funct_1,d3_xboole_0,t78_partfun1,t80_partfun1,t22_funct_1,t80_partfun1,t80_partfun1,t22_funct_1,t8_grfunc_1,d10_xboole_0]),
    [file(partfun1,t93_partfun1),interesting(0.66)]).

fof(t143_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,k1_tarski(B)) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,k1_tarski(B)) )
         => r1_partfun1(C,D) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_partfun1,d3_xboole_0,t73_partfun1]),
    [file(partfun1,t143_partfun1),interesting(0.65)]).

fof(t67_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,k1_xboole_0) )
     => k9_relat_1(C,B) = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[t64_partfun1,t150_relat_1]),
    [file(partfun1,t67_partfun1),interesting(0.65)]).

fof(t68_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,k1_xboole_0) )
     => k10_relat_1(C,B) = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[t64_partfun1,t172_relat_1]),
    [file(partfun1,t68_partfun1),interesting(0.65)]).

fof(t69_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,k1_tarski(A),B) )
     => r1_tarski(k2_relat_1(C),k1_tarski(k1_funct_1(C,A))) ) ),
    inference(mizar_proof,[status(thm)],[t39_zfmisc_1,t14_funct_1,t65_relat_1,t39_zfmisc_1]),
    [file(partfun1,t69_partfun1),interesting(0.65)]).

fof(t80_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_relat_1(D)
        & v1_funct_1(D) )
     => ( r2_hidden(A,k4_relset_1(B,C,k3_partfun1(D,B,C)))
       => k1_funct_1(k3_partfun1(D,B,C),A) = k1_funct_1(D,A) ) ) ),
    inference(mizar_proof,[status(thm)],[t78_partfun1,t79_partfun1]),
    [file(partfun1,t80_partfun1),interesting(0.64)]).

fof(t58_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,k1_xboole_0,A) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,k1_xboole_0,B) )
         => C = D ) ) ),
    inference(mizar_proof,[status(thm)],[t57_partfun1]),
    [file(partfun1,t58_partfun1),interesting(0.64)]).

fof(t70_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,k1_tarski(A),B) )
     => v2_funct_1(C) ) ),
    inference(mizar_proof,[status(thm)],[d8_funct_1,d1_tarski]),
    [file(partfun1,t70_partfun1),interesting(0.64)]).

fof(l197_partfun1,theorem,(
    ! [A,B] : 
      ( m2_relset_1(B,A,A)
     => ( B = k6_relat_1(A)
       => v1_partfun1(B,A,A) ) ) ),
    inference(mizar_proof,[status(thm)],[t71_relat_1,d4_partfun1]),
    [file(partfun1,l197_partfun1),interesting(0.63)]).

fof(t62_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,A,k1_xboole_0) )
     => ( k4_relset_1(A,k1_xboole_0,B) = k1_xboole_0
        & k2_relat_1(B) = k1_xboole_0 ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,t3_xboole_1,t65_relat_1]),
    [file(partfun1,t62_partfun1),interesting(0.63)]).

fof(t171_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( ( v1_relat_1(D)
            & v1_funct_1(D) )
         => ( r2_hidden(D,k5_partfun1(A,B,C))
           => r1_partfun1(C,D) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_partfun1]),
    [file(partfun1,t171_partfun1),interesting(0.63)]).

fof(t28_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ( r1_tarski(k4_relset_1(A,B,D),C)
       => ( v1_funct_1(D)
          & m2_relset_1(D,C,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,l13_partfun1]),
    [file(partfun1,t28_partfun1),interesting(0.63)]).

fof(t29_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ( r1_tarski(k2_relat_1(D),C)
       => ( v1_funct_1(D)
          & m2_relset_1(D,A,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1]),
    [file(partfun1,t29_partfun1),interesting(0.63)]).

fof(t39_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ( v2_funct_1(C)
       => ( v1_funct_1(k2_funct_1(C))
          & m2_relset_1(k2_funct_1(C),B,A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1,t55_funct_1,l13_partfun1]),
    [file(partfun1,t39_partfun1),interesting(0.63)]).

fof(t73_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,k1_tarski(B)) )
     => ( r2_hidden(C,k4_relset_1(A,k1_tarski(B),D))
       => k1_funct_1(D,C) = B ) ) ),
    inference(mizar_proof,[status(thm)],[t27_partfun1,d1_tarski]),
    [file(partfun1,t73_partfun1),interesting(0.62)]).

fof(t176_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k1_xboole_0,A) )
     => k5_partfun1(k1_xboole_0,A,B) = k1_tarski(k1_xboole_0) ) ),
    inference(mizar_proof,[status(thm)],[t57_partfun1,t175_partfun1]),
    [file(partfun1,t176_partfun1),interesting(0.62)]).

fof(t51_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => k9_relat_1(C,A) = k2_relat_1(C) ) ),
    inference(mizar_proof,[status(thm)],[t156_relat_1,t144_relat_1,t146_relat_1,d10_xboole_0]),
    [file(partfun1,t51_partfun1),interesting(0.62)]).

fof(t60_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,k1_xboole_0,A) )
     => k9_relat_1(C,B) = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[t57_partfun1,t150_relat_1]),
    [file(partfun1,t60_partfun1),interesting(0.62)]).

fof(t61_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,k1_xboole_0,A) )
     => k10_relat_1(C,B) = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[t57_partfun1,t172_relat_1]),
    [file(partfun1,t61_partfun1),interesting(0.62)]).

fof(t99_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ( ( v1_partfun1(C,A,B)
          & B = k1_xboole_0 )
       => A = k1_xboole_0 ) ) ),
    inference(mizar_proof,[status(thm)],[d4_partfun1,t64_partfun1,l4_partfun1]),
    [file(partfun1,t99_partfun1),interesting(0.62)]).

fof(t54_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k1_xboole_0,A) )
     => ( k4_relset_1(k1_xboole_0,A,B) = k1_xboole_0
        & k2_relat_1(B) = k1_xboole_0 ) ) ),
    inference(mizar_proof,[status(thm)],[t3_xboole_1,t65_relat_1]),
    [file(partfun1,t54_partfun1),interesting(0.61)]).

fof(t36_partfun1,theorem,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => k5_relat_1(k6_relat_1(A),C) = C ) ),
    inference(mizar_proof,[status(thm)],[t77_relat_1]),
    [file(partfun1,t36_partfun1),interesting(0.61)]).

fof(t37_partfun1,theorem,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => k5_relat_1(C,k6_relat_1(B)) = C ) ),
    inference(mizar_proof,[status(thm)],[t79_relat_1]),
    [file(partfun1,t37_partfun1),interesting(0.61)]).

fof(t77_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r1_tarski(k4_relset_1(A,B,k3_partfun1(C,A,B)),k1_relat_1(C))
        & r1_tarski(k2_relat_1(k3_partfun1(C,A,B)),k2_relat_1(C)) ) ) ),
    inference(mizar_proof,[status(thm)],[t76_partfun1,t25_relat_1]),
    [file(partfun1,t77_partfun1),interesting(0.60)]).

fof(t79_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_relat_1(D)
        & v1_funct_1(D) )
     => ( ( r2_hidden(A,k1_relat_1(D))
          & r2_hidden(A,B)
          & r2_hidden(k1_funct_1(D,A),C) )
       => k1_funct_1(k3_partfun1(D,B,C),A) = k1_funct_1(D,A) ) ) ),
    inference(mizar_proof,[status(thm)],[t86_funct_1,t87_funct_1,t72_funct_1]),
    [file(partfun1,t79_partfun1),interesting(0.60)]).

fof(t24_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v1_funct_1(A)
        & m2_relset_1(A,k1_relat_1(A),k2_relat_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1]),
    [file(partfun1,t24_partfun1),interesting(0.60)]).

fof(t185_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,B) )
         => ( ~ r1_xboole_0(k5_partfun1(A,B,C),k5_partfun1(A,B,D))
           => r1_partfun1(C,D) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xboole_0,d3_xboole_0,t168_partfun1,t169_partfun1,t171_partfun1,t158_partfun1]),
    [file(partfun1,t185_partfun1),interesting(0.59)]).

fof(t78_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_relat_1(D)
        & v1_funct_1(D) )
     => ( r2_hidden(A,k4_relset_1(B,C,k3_partfun1(D,B,C)))
      <=> ( r2_hidden(A,k1_relat_1(D))
          & r2_hidden(A,B)
          & r2_hidden(k1_funct_1(D,A),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t90_relat_1,d3_xboole_0,t86_funct_1,t86_funct_1,d3_xboole_0,t90_relat_1]),
    [file(partfun1,t78_partfun1),interesting(0.58)]).

fof(t47_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( v1_funct_1(k7_relat_1(k8_relat_1(A,C),B))
        & m2_relset_1(k7_relat_1(k8_relat_1(A,C),B),B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[t140_relat_1,t87_relat_1,t116_relat_1,l13_partfun1]),
    [file(partfun1,t47_partfun1),interesting(0.58)]).

fof(t140_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,B) )
         => ! [E] : 
              ( ( v1_relat_1(E)
                & v1_funct_1(E) )
             => ( ( r1_partfun1(C,E)
                  & r1_tarski(D,C) )
               => r1_partfun1(D,E) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_partfun1,t25_relat_1,d3_xboole_0,t8_grfunc_1,d3_xboole_0,d6_partfun1]),
    [file(partfun1,t140_partfun1),interesting(0.57)]).

fof(t172_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,A,k1_xboole_0) )
     => ( A != k1_xboole_0
       => k5_partfun1(A,k1_xboole_0,B) = k1_xboole_0 ) ) ),
    inference(mizar_proof,[status(thm)],[d7_partfun1,t62_partfun1,d4_partfun1]),
    [file(partfun1,t172_partfun1),interesting(0.56)]).

fof(t63_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( k2_relat_1(C) = k1_xboole_0
       => ( v1_funct_1(C)
          & m2_relset_1(C,A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t65_relat_1,t2_xboole_1,l13_partfun1]),
    [file(partfun1,t63_partfun1),interesting(0.55)]).

fof(t71_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,k1_tarski(A),B) )
     => r1_tarski(k9_relat_1(D,C),k1_tarski(k1_funct_1(D,A))) ) ),
    inference(mizar_proof,[status(thm)],[t69_partfun1,t144_relat_1,t1_xboole_1]),
    [file(partfun1,t71_partfun1),interesting(0.55)]).

fof(t74_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,k1_tarski(B)) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,k1_tarski(B)) )
         => ( k4_relset_1(A,k1_tarski(B),C) = k4_relset_1(A,k1_tarski(B),D)
           => C = D ) ) ) ),
    inference(mizar_proof,[status(thm)],[t73_partfun1,t9_funct_1]),
    [file(partfun1,t74_partfun1),interesting(0.55)]).

fof(t2_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ~ ( ! [C] : 
                  ( r2_hidden(C,k3_xboole_0(k1_relat_1(A),k1_relat_1(B)))
                 => k1_funct_1(A,C) = k1_funct_1(B,C) )
              & ! [C] : 
                  ( ( v1_relat_1(C)
                    & v1_funct_1(C) )
                 => k2_xboole_0(A,B) != C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xboole_0,d2_xboole_0,t8_funct_1,d3_xboole_0,d4_relat_1,s1_funct_1,t21_relat_1,t1_partfun1,t21_relat_1,d2_xboole_0,d4_relat_1,d2_xboole_0,t110_zfmisc_1]),
    [file(partfun1,t2_partfun1),interesting(0.54)]).

fof(t25_partfun1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( r1_tarski(k2_relat_1(B),A)
       => ( v1_funct_1(B)
          & m2_relset_1(B,k1_relat_1(B),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_partfun1]),
    [file(partfun1,t25_partfun1),interesting(0.54)]).

fof(t97_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_relat_1(D)
        & v1_funct_1(D) )
     => k9_relset_1(B,C,A,k3_partfun1(D,B,C)) = k3_partfun1(D,B,k3_xboole_0(A,C)) ) ),
    inference(mizar_proof,[status(thm)],[t140_relat_1,t127_relat_1,t140_relat_1]),
    [file(partfun1,t97_partfun1),interesting(0.54)]).

fof(l198_partfun1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( B = k6_relat_1(A)
       => ( v1_relat_2(B)
          & v3_relat_2(B)
          & v4_relat_2(B)
          & v8_relat_2(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t71_relat_1,t71_relat_1,d6_relat_1,d1_relat_2,d10_relat_1,d9_relat_2,d3_relat_2,d10_relat_1,d10_relat_1,d11_relat_2,d4_relat_2,d10_relat_1,d12_relat_2,d8_relat_2,d10_relat_1,d16_relat_2]),
    [file(partfun1,l198_partfun1),interesting(0.52)]).

fof(t96_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_relat_1(D)
        & v1_funct_1(D) )
     => k2_partfun1(A,B,k3_partfun1(D,A,B),C) = k3_partfun1(D,k3_xboole_0(A,C),B) ) ),
    inference(mizar_proof,[status(thm)],[t100_relat_1]),
    [file(partfun1,t96_partfun1),interesting(0.52)]).

fof(t3_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C) )
             => ( k2_xboole_0(A,B) = C
               => ! [D] : 
                    ( r2_hidden(D,k3_xboole_0(k1_relat_1(A),k1_relat_1(B)))
                   => k1_funct_1(A,D) = k1_funct_1(B,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_xboole_0,t34_grfunc_1]),
    [file(partfun1,t3_partfun1),interesting(0.50)]).

fof(t132_partfun1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_tarski(k1_relat_1(A),k1_relat_1(B))
           => ( r1_partfun1(A,B)
            <=> ! [C] : 
                  ( r2_hidden(C,k1_relat_1(A))
                 => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t28_xboole_1,d6_partfun1]),
    [file(partfun1,t132_partfun1),interesting(0.50)]).

fof(t117_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( ( r1_tarski(A,k1_relat_1(C))
          & r1_tarski(k9_relat_1(C,A),B) )
       => v1_partfun1(k3_partfun1(C,A,B),A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d12_funct_1,t78_partfun1,d10_xboole_0,d4_partfun1]),
    [file(partfun1,t117_partfun1),interesting(0.49)]).

fof(t115_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( ( r1_tarski(A,k1_relat_1(C))
          & r1_tarski(k2_relat_1(C),B) )
       => v1_partfun1(k3_partfun1(C,A,B),A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d5_funct_1,t78_partfun1,d10_xboole_0,d4_partfun1]),
    [file(partfun1,t115_partfun1),interesting(0.48)]).

fof(s2_partfun1,theorem,
    ( ( ! [A,B] : 
          ( ( r2_hidden(A,f1_s2_partfun1)
            & p1_s2_partfun1(A,B) )
         => r2_hidden(B,f2_s2_partfun1) )
      & ! [A,B,C] : 
          ( ( r2_hidden(A,f1_s2_partfun1)
            & p1_s2_partfun1(A,B)
            & p1_s2_partfun1(A,C) )
         => B = C ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & m2_relset_1(A,f1_s2_partfun1,f2_s2_partfun1)
        & ! [B] : 
            ( r2_hidden(B,k4_relset_1(f1_s2_partfun1,f2_s2_partfun1,A))
          <=> ( r2_hidden(B,f1_s2_partfun1)
              & ? [C] : p1_s2_partfun1(B,C) ) )
        & ! [B] : 
            ( r2_hidden(B,k4_relset_1(f1_s2_partfun1,f2_s2_partfun1,A))
           => p1_s2_partfun1(B,k1_funct_1(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[l12_partfun1,l13_partfun1,l13_partfun1,t3_xboole_1,t65_relat_1,t65_relat_1,s2_funct_1,s1_xboole_0,t76_funct_1,d3_tarski,d5_funct_1,t87_relat_1,t70_funct_1,l13_partfun1,t87_relat_1,d3_xboole_0,t90_relat_1,t87_relat_1,t70_funct_1]),
    [file(partfun1,s2_partfun1),interesting(0.43)]).

fof(t34_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( ( v1_funct_1(D)
            & m2_relset_1(D,A,B) )
         => ( ( k4_relset_1(A,B,C) = k4_relset_1(A,B,D)
              & ! [E] : 
                  ( m1_subset_1(E,A)
                 => ( r2_hidden(E,k4_relset_1(A,B,C))
                   => k1_funct_1(C,E) = k1_funct_1(D,E) ) ) )
           => C = D ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_funct_1]),
    [file(partfun1,t34_partfun1),interesting(0.41)]).

fof(t72_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_relat_1(D)
        & v1_funct_1(D) )
     => ( ( k1_relat_1(D) = k1_tarski(A)
          & r2_hidden(A,B)
          & r2_hidden(k1_funct_1(D,A),C) )
       => ( v1_funct_1(D)
          & m2_relset_1(D,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t14_funct_1,t37_zfmisc_1,l13_partfun1]),
    [file(partfun1,t72_partfun1),interesting(0.40)]).

fof(t26_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ~ ( r2_hidden(C,k2_relat_1(D))
          & ! [E] : 
              ( m1_subset_1(E,A)
             => ~ ( r2_hidden(E,k4_relset_1(A,B,D))
                  & C = k1_funct_1(D,E) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_funct_1]),
    [file(partfun1,t26_partfun1),interesting(0.39)]).

fof(t49_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ~ ( r2_hidden(C,k9_relat_1(D,A))
          & ! [E] : 
              ( m1_subset_1(E,A)
             => ~ ( r2_hidden(E,k4_relset_1(A,B,D))
                  & C = k1_funct_1(D,E) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_funct_1]),
    [file(partfun1,t49_partfun1),interesting(0.39)]).

fof(t38_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ( ! [D] : 
            ( m1_subset_1(D,A)
           => ! [E] : 
                ( m1_subset_1(E,A)
               => ( ( r2_hidden(D,k4_relset_1(A,B,C))
                    & r2_hidden(E,k4_relset_1(A,B,C))
                    & k1_funct_1(C,D) = k1_funct_1(C,E) )
                 => D = E ) ) )
       => v2_funct_1(C) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_funct_1]),
    [file(partfun1,t38_partfun1),interesting(0.35)]).

fof(s3_partfun1,theorem,
    ( ! [A] : 
        ( p1_s3_partfun1(A)
       => r2_hidden(f3_s3_partfun1(A),f2_s3_partfun1) )
   => ? [A] : 
        ( v1_funct_1(A)
        & m2_relset_1(A,f1_s3_partfun1,f2_s3_partfun1)
        & ! [B] : 
            ( r2_hidden(B,k4_relset_1(f1_s3_partfun1,f2_s3_partfun1,A))
          <=> ( r2_hidden(B,f1_s3_partfun1)
              & p1_s3_partfun1(B) ) )
        & ! [B] : 
            ( r2_hidden(B,k4_relset_1(f1_s3_partfun1,f2_s3_partfun1,A))
           => k1_funct_1(A,B) = f3_s3_partfun1(B) ) ) ),
    inference(mizar_proof,[status(thm)],[s2_partfun1]),
    [file(partfun1,s3_partfun1),interesting(0.27)]).

fof(s1_partfun1,theorem,(
    ? [A] : 
      ( v1_relat_1(A)
      & v1_funct_1(A)
      & k1_relat_1(A) = f1_s1_partfun1
      & ! [B] : 
          ( r2_hidden(B,f1_s1_partfun1)
         => ( ( p1_s1_partfun1(B)
             => k1_funct_1(A,B) = f2_s1_partfun1(B) )
            & ( ~ p1_s1_partfun1(B)
             => k1_funct_1(A,B) = f3_s1_partfun1(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s2_funct_1]),
    [file(partfun1,s1_partfun1),interesting(0.26)]).

fof(t35_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,k2_zfmisc_1(A,B),C) )
     => ! [E] : 
          ( ( v1_funct_1(E)
            & m2_relset_1(E,k2_zfmisc_1(A,B),C) )
         => ( ( k4_relset_1(k2_zfmisc_1(A,B),C,D) = k4_relset_1(k2_zfmisc_1(A,B),C,E)
              & ! [F,G] : 
                  ( r2_hidden(k4_tarski(F,G),k4_relset_1(k2_zfmisc_1(A,B),C,D))
                 => k1_funct_1(D,k4_tarski(F,G)) = k1_funct_1(E,k4_tarski(F,G)) ) )
           => D = E ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_zfmisc_1,t9_funct_1]),
    [file(partfun1,t35_partfun1),interesting(0.26)]).

fof(s4_partfun1,theorem,
    ( ( ! [A,B,C] : 
          ( ( r2_hidden(A,f1_s4_partfun1)
            & r2_hidden(B,f2_s4_partfun1)
            & p1_s4_partfun1(A,B,C) )
         => r2_hidden(C,f3_s4_partfun1) )
      & ! [A,B,C,D] : 
          ( ( r2_hidden(A,f1_s4_partfun1)
            & r2_hidden(B,f2_s4_partfun1)
            & p1_s4_partfun1(A,B,C)
            & p1_s4_partfun1(A,B,D) )
         => C = D ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & m2_relset_1(A,k2_zfmisc_1(f1_s4_partfun1,f2_s4_partfun1),f3_s4_partfun1)
        & ! [B,C] : 
            ( r2_hidden(k4_tarski(B,C),k4_relset_1(k2_zfmisc_1(f1_s4_partfun1,f2_s4_partfun1),f3_s4_partfun1,A))
          <=> ( r2_hidden(B,f1_s4_partfun1)
              & r2_hidden(C,f2_s4_partfun1)
              & ? [D] : p1_s4_partfun1(B,C,D) ) )
        & ! [B,C] : 
            ( r2_hidden(k4_tarski(B,C),k4_relset_1(k2_zfmisc_1(f1_s4_partfun1,f2_s4_partfun1),f3_s4_partfun1,A))
           => p1_s4_partfun1(B,C,k1_funct_1(A,k4_tarski(B,C))) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_zfmisc_1,d2_zfmisc_1,s2_partfun1,t106_zfmisc_1,d2_zfmisc_1,t33_zfmisc_1]),
    [file(partfun1,s4_partfun1),interesting(0.18)]).

fof(t71_relat_1,theorem,(
    ! [A] : 
      ( k1_relat_1(k6_relat_1(A)) = A
      & k2_relat_1(k6_relat_1(A)) = A ) ),
    file(relat_1,t71_relat_1),
    [interesting(0.00)]).

fof(d4_partfun1,definition,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => ( v1_partfun1(C,A,B)
      <=> k4_relset_1(A,B,C) = A ) ) ),
    file(partfun1,d4_partfun1),
    [interesting(0.00)]).

fof(d6_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => k3_relat_1(A) = k2_xboole_0(k1_relat_1(A),k2_relat_1(A)) ) ),
    file(relat_1,d6_relat_1),
    [interesting(0.00)]).

fof(d1_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r1_relat_2(A,B)
        <=> ! [C] : 
              ( r2_hidden(C,B)
             => r2_hidden(k4_tarski(C,C),A) ) ) ) ),
    file(relat_2,d1_relat_2),
    [interesting(0.00)]).

fof(d10_relat_1,definition,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( B = k6_relat_1(A)
      <=> ! [C,D] : 
            ( r2_hidden(k4_tarski(C,D),B)
          <=> ( r2_hidden(C,A)
              & C = D ) ) ) ) ),
    file(relat_1,d10_relat_1),
    [interesting(0.00)]).

fof(d9_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v1_relat_2(A)
      <=> r1_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d9_relat_2),
    [interesting(0.00)]).

fof(d3_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r3_relat_2(A,B)
        <=> ! [C,D] : 
              ( ( r2_hidden(C,B)
                & r2_hidden(D,B)
                & r2_hidden(k4_tarski(C,D),A) )
             => r2_hidden(k4_tarski(D,C),A) ) ) ) ),
    file(relat_2,d3_relat_2),
    [interesting(0.00)]).

fof(d11_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v3_relat_2(A)
      <=> r3_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d11_relat_2),
    [interesting(0.00)]).

fof(d4_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r4_relat_2(A,B)
        <=> ! [C,D] : 
              ( ( r2_hidden(C,B)
                & r2_hidden(D,B)
                & r2_hidden(k4_tarski(C,D),A)
                & r2_hidden(k4_tarski(D,C),A) )
             => C = D ) ) ) ),
    file(relat_2,d4_relat_2),
    [interesting(0.00)]).

fof(d12_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v4_relat_2(A)
      <=> r4_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d12_relat_2),
    [interesting(0.00)]).

fof(d8_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r8_relat_2(A,B)
        <=> ! [C,D,E] : 
              ( ( r2_hidden(C,B)
                & r2_hidden(D,B)
                & r2_hidden(E,B)
                & r2_hidden(k4_tarski(C,D),A)
                & r2_hidden(k4_tarski(D,E),A) )
             => r2_hidden(k4_tarski(C,E),A) ) ) ) ),
    file(relat_2,d8_relat_2),
    [interesting(0.00)]).

fof(d16_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v8_relat_2(A)
      <=> r8_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d16_relat_2),
    [interesting(0.00)]).

fof(t11_relset_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( ( r1_tarski(k1_relat_1(C),A)
          & r1_tarski(k2_relat_1(C),B) )
       => m2_relset_1(C,A,B) ) ) ),
    file(relset_1,t11_relset_1),
    [interesting(0.00)]).

fof(s2_funct_1,theorem,
    ( ( ! [A,B,C] : 
          ( ( r2_hidden(A,f1_s2_funct_1)
            & p1_s2_funct_1(A,B)
            & p1_s2_funct_1(A,C) )
         => B = C )
      & ! [A] : ~ ( r2_hidden(A,f1_s2_funct_1)
          & ! [B] : ~ p1_s2_funct_1(A,B) ) )
   => ? [A] : 
        ( v1_relat_1(A)
        & v1_funct_1(A)
        & k1_relat_1(A) = f1_s2_funct_1
        & ! [B] : 
            ( r2_hidden(B,f1_s2_funct_1)
           => p1_s2_funct_1(B,k1_funct_1(A,B)) ) ) ),
    file(funct_1,s2_funct_1),
    [interesting(0.00)]).

fof(t2_xboole_1,theorem,(
    ! [A] : r1_tarski(k1_xboole_0,A) ),
    file(xboole_1,t2_xboole_1),
    [interesting(0.00)]).

fof(t12_relset_1,theorem,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => ( r1_tarski(k1_relat_1(C),A)
        & r1_tarski(k2_relat_1(C),B) ) ) ),
    file(relset_1,t12_relset_1),
    [interesting(0.00)]).

fof(t3_xboole_1,theorem,(
    ! [A] : 
      ( r1_tarski(A,k1_xboole_0)
     => A = k1_xboole_0 ) ),
    file(xboole_1,t3_xboole_1),
    [interesting(0.00)]).

fof(t65_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( k1_relat_1(A) = k1_xboole_0
      <=> k2_relat_1(A) = k1_xboole_0 ) ) ),
    file(relat_1,t65_relat_1),
    [interesting(0.00)]).

fof(s1_xboole_0,theorem,(
    ? [A] : 
    ! [B] : 
      ( r2_hidden(B,A)
    <=> ( r2_hidden(B,f1_s1_xboole_0)
        & p1_s1_xboole_0(B) ) ) ),
    file(xboole_0,s1_xboole_0),
    [interesting(0.00)]).

fof(t76_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( r1_tarski(k1_relat_1(k7_relat_1(B,A)),k1_relat_1(B))
        & r1_tarski(k2_relat_1(k7_relat_1(B,A)),k2_relat_1(B)) ) ) ),
    file(funct_1,t76_funct_1),
    [interesting(0.00)]).

fof(d3_tarski,definition,(
    ! [A,B] : 
      ( r1_tarski(A,B)
    <=> ! [C] : 
          ( r2_hidden(C,A)
         => r2_hidden(C,B) ) ) ),
    file(tarski,d3_tarski),
    [interesting(0.00)]).

fof(d5_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( B = k2_relat_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : 
                  ( r2_hidden(D,k1_relat_1(A))
                  & C = k1_funct_1(A,D) ) ) ) ) ),
    file(funct_1,d5_funct_1),
    [interesting(0.00)]).

fof(t87_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => r1_tarski(k1_relat_1(k7_relat_1(B,A)),A) ) ),
    file(relat_1,t87_relat_1),
    [interesting(0.00)]).

fof(t70_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(B,k1_relat_1(k7_relat_1(C,A)))
       => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ),
    file(funct_1,t70_funct_1),
    [interesting(0.00)]).

fof(d3_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k3_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            & r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d3_xboole_0),
    [interesting(0.00)]).

fof(t90_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => k1_relat_1(k7_relat_1(B,A)) = k3_xboole_0(k1_relat_1(B),A) ) ),
    file(relat_1,t90_relat_1),
    [interesting(0.00)]).

fof(d2_zfmisc_1,definition,(
    ! [A,B,C] : 
      ( C = k2_zfmisc_1(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ? [E,F] : 
              ( r2_hidden(E,A)
              & r2_hidden(F,B)
              & D = k4_tarski(E,F) ) ) ) ),
    file(zfmisc_1,d2_zfmisc_1),
    [interesting(0.00)]).

fof(t106_zfmisc_1,theorem,(
    ! [A,B,C,D] : 
      ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))
    <=> ( r2_hidden(A,C)
        & r2_hidden(B,D) ) ) ),
    file(zfmisc_1,t106_zfmisc_1),
    [interesting(0.00)]).

fof(t33_zfmisc_1,theorem,(
    ! [A,B,C,D] : 
      ( k4_tarski(A,B) = k4_tarski(C,D)
     => ( A = C
        & B = D ) ) ),
    file(zfmisc_1,t33_zfmisc_1),
    [interesting(0.00)]).

fof(s5_partfun1,theorem,
    ( ! [A,B] : 
        ( p1_s5_partfun1(A,B)
       => r2_hidden(f4_s5_partfun1(A,B),f3_s5_partfun1) )
   => ? [A] : 
        ( v1_funct_1(A)
        & m2_relset_1(A,k2_zfmisc_1(f1_s5_partfun1,f2_s5_partfun1),f3_s5_partfun1)
        & ! [B,C] : 
            ( r2_hidden(k4_tarski(B,C),k4_relset_1(k2_zfmisc_1(f1_s5_partfun1,f2_s5_partfun1),f3_s5_partfun1,A))
          <=> ( r2_hidden(B,f1_s5_partfun1)
              & r2_hidden(C,f2_s5_partfun1)
              & p1_s5_partfun1(B,C) ) )
        & ! [B,C] : 
            ( r2_hidden(k4_tarski(B,C),k4_relset_1(k2_zfmisc_1(f1_s5_partfun1,f2_s5_partfun1),f3_s5_partfun1,A))
           => k1_funct_1(A,k4_tarski(B,C)) = f4_s5_partfun1(B,C) ) ) ),
    inference(mizar_proof,[status(thm)],[s4_partfun1]),
    [file(partfun1,s5_partfun1),interesting(0.00)]).

fof(t100_partfun1,theorem,(
    $true ),
    file(partfun1,t100_partfun1),
    [interesting(0.00)]).

fof(t101_partfun1,theorem,(
    $true ),
    file(partfun1,t101_partfun1),
    [interesting(0.00)]).

fof(t102_partfun1,theorem,(
    $true ),
    file(partfun1,t102_partfun1),
    [interesting(0.00)]).

fof(t103_partfun1,theorem,(
    $true ),
    file(partfun1,t103_partfun1),
    [interesting(0.00)]).

fof(t104_partfun1,theorem,(
    $true ),
    file(partfun1,t104_partfun1),
    [interesting(0.00)]).

fof(t105_partfun1,theorem,(
    $true ),
    file(partfun1,t105_partfun1),
    [interesting(0.00)]).

fof(t106_partfun1,theorem,(
    $true ),
    file(partfun1,t106_partfun1),
    [interesting(0.00)]).

fof(t107_partfun1,theorem,(
    $true ),
    file(partfun1,t107_partfun1),
    [interesting(0.00)]).

fof(t108_partfun1,theorem,(
    $true ),
    file(partfun1,t108_partfun1),
    [interesting(0.00)]).

fof(t109_partfun1,theorem,(
    $true ),
    file(partfun1,t109_partfun1),
    [interesting(0.00)]).

fof(t10_partfun1,theorem,(
    k2_relat_1(k1_xboole_0) = k1_xboole_0 ),
    file(partfun1,t10_partfun1),
    [interesting(0.00)]).

fof(t110_partfun1,theorem,(
    $true ),
    file(partfun1,t110_partfun1),
    [interesting(0.00)]).

fof(t111_partfun1,theorem,(
    $true ),
    file(partfun1,t111_partfun1),
    [interesting(0.00)]).

fof(l4_partfun1,theorem,(
    k1_relat_1(k1_xboole_0) = k1_xboole_0 ),
    file(partfun1,l4_partfun1),
    [interesting(0.00)]).

fof(t88_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => r1_tarski(k7_relat_1(B,A),B) ) ),
    file(relat_1,t88_relat_1),
    [interesting(0.00)]).

fof(t117_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => r1_tarski(k8_relat_1(A,B),B) ) ),
    file(relat_1,t117_relat_1),
    [interesting(0.00)]).

fof(t1_xboole_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(B,C) )
     => r1_tarski(A,C) ) ),
    file(xboole_1,t1_xboole_1),
    [interesting(0.00)]).

fof(t25_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( r1_tarski(A,B)
           => ( r1_tarski(k1_relat_1(A),k1_relat_1(B))
              & r1_tarski(k2_relat_1(A),k2_relat_1(B)) ) ) ) ) ),
    file(relat_1,t25_relat_1),
    [interesting(0.00)]).

fof(t86_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(B,k1_relat_1(k8_relat_1(A,C)))
      <=> ( r2_hidden(B,k1_relat_1(C))
          & r2_hidden(k1_funct_1(C,B),A) ) ) ) ),
    file(funct_1,t86_funct_1),
    [interesting(0.00)]).

fof(d10_xboole_0,definition,(
    ! [A,B] : 
      ( A = B
    <=> ( r1_tarski(A,B)
        & r1_tarski(B,A) ) ) ),
    file(xboole_0,d10_xboole_0),
    [interesting(0.00)]).

fof(d12_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B,C] : 
          ( C = k9_relat_1(A,B)
        <=> ! [D] : 
              ( r2_hidden(D,C)
            <=> ? [E] : 
                  ( r2_hidden(E,k1_relat_1(A))
                  & r2_hidden(E,B)
                  & D = k1_funct_1(A,E) ) ) ) ) ),
    file(funct_1,d12_funct_1),
    [interesting(0.00)]).

fof(t87_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(B,k1_relat_1(k8_relat_1(A,C)))
       => k1_funct_1(k8_relat_1(A,C),B) = k1_funct_1(C,B) ) ) ),
    file(funct_1,t87_funct_1),
    [interesting(0.00)]).

fof(t72_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(B,A)
       => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ),
    file(funct_1,t72_funct_1),
    [interesting(0.00)]).

fof(t118_partfun1,theorem,(
    $true ),
    file(partfun1,t118_partfun1),
    [interesting(0.00)]).

fof(t11_partfun1,theorem,(
    $true ),
    file(partfun1,t11_partfun1),
    [interesting(0.00)]).

fof(d5_partfun1,definition,(
    ! [A,B,C] : 
      ( C = k4_partfun1(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ? [E] : 
              ( v1_relat_1(E)
              & v1_funct_1(E)
              & D = E
              & r1_tarski(k1_relat_1(E),A)
              & r1_tarski(k2_relat_1(E),B) ) ) ) ),
    file(partfun1,d5_partfun1),
    [interesting(0.00)]).

fof(t9_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( ( k1_relat_1(A) = k1_relat_1(B)
              & ! [C] : 
                  ( r2_hidden(C,k1_relat_1(A))
                 => k1_funct_1(A,C) = k1_funct_1(B,C) ) )
           => A = B ) ) ) ),
    file(funct_1,t9_funct_1),
    [interesting(0.00)]).

fof(d1_tarski,definition,(
    ! [A,B] : 
      ( B = k1_tarski(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> C = A ) ) ),
    file(tarski,d1_tarski),
    [interesting(0.00)]).

fof(t124_partfun1,theorem,(
    $true ),
    file(partfun1,t124_partfun1),
    [interesting(0.00)]).

fof(t129_partfun1,theorem,(
    $true ),
    file(partfun1,t129_partfun1),
    [interesting(0.00)]).

fof(t12_partfun1,theorem,(
    $true ),
    file(partfun1,t12_partfun1),
    [interesting(0.00)]).

fof(t133_partfun1,theorem,(
    $true ),
    file(partfun1,t133_partfun1),
    [interesting(0.00)]).

fof(t134_partfun1,theorem,(
    $true ),
    file(partfun1,t134_partfun1),
    [interesting(0.00)]).

fof(t8_xboole_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(C,B) )
     => r1_tarski(k2_xboole_0(A,C),B) ) ),
    file(xboole_1,t8_xboole_1),
    [interesting(0.00)]).

fof(t6_grfunc_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( r1_tarski(B,A)
         => ( v1_relat_1(B)
            & v1_funct_1(B) ) ) ) ),
    file(grfunc_1,t6_grfunc_1),
    [interesting(0.00)]).

fof(t7_xboole_1,theorem,(
    ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ),
    file(xboole_1,t7_xboole_1),
    [interesting(0.00)]).

fof(d2_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k2_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            | r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d2_xboole_0),
    [interesting(0.00)]).

fof(t8_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(k4_tarski(A,B),C)
      <=> ( r2_hidden(A,k1_relat_1(C))
          & B = k1_funct_1(C,A) ) ) ) ),
    file(funct_1,t8_funct_1),
    [interesting(0.00)]).

fof(d4_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( B = k1_relat_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : r2_hidden(k4_tarski(C,D),A) ) ) ) ),
    file(relat_1,d4_relat_1),
    [interesting(0.00)]).

fof(s1_funct_1,theorem,
    ( ! [A,B,C] : 
        ( ( p1_s1_funct_1(A,B)
          & p1_s1_funct_1(A,C) )
       => B = C )
   => ? [A] : 
        ( v1_relat_1(A)
        & v1_funct_1(A)
        & ! [B,C] : 
            ( r2_hidden(k4_tarski(B,C),A)
          <=> ( r2_hidden(B,f1_s1_funct_1)
              & p1_s1_funct_1(B,C) ) ) ) ),
    file(funct_1,s1_funct_1),
    [interesting(0.00)]).

fof(t21_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => r1_tarski(A,k2_zfmisc_1(k1_relat_1(A),k2_relat_1(A))) ) ),
    file(relat_1,t21_relat_1),
    [interesting(0.00)]).

fof(t119_zfmisc_1,theorem,(
    ! [A,B,C,D] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(C,D) )
     => r1_tarski(k2_zfmisc_1(A,C),k2_zfmisc_1(B,D)) ) ),
    file(zfmisc_1,t119_zfmisc_1),
    [interesting(0.00)]).

fof(t13_xboole_1,theorem,(
    ! [A,B,C,D] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(C,D) )
     => r1_tarski(k2_xboole_0(A,C),k2_xboole_0(B,D)) ) ),
    file(xboole_1,t13_xboole_1),
    [interesting(0.00)]).

fof(t110_zfmisc_1,theorem,(
    ! [A,B,C,D,E,F] : 
      ( ( r1_tarski(A,k2_zfmisc_1(B,C))
        & r1_tarski(D,k2_zfmisc_1(E,F))
        & ! [G,H] : 
            ( r2_hidden(k4_tarski(G,H),A)
          <=> r2_hidden(k4_tarski(G,H),D) ) )
     => A = D ) ),
    file(zfmisc_1,t110_zfmisc_1),
    [interesting(0.00)]).

fof(t34_grfunc_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ! [D] : 
              ( ( v1_relat_1(D)
                & v1_funct_1(D) )
             => ( ( r2_hidden(A,k1_relat_1(B))
                  & C = k2_xboole_0(B,D) )
               => k1_funct_1(C,A) = k1_funct_1(B,A) ) ) ) ) ),
    file(grfunc_1,t34_grfunc_1),
    [interesting(0.00)]).

fof(d6_partfun1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_partfun1(A,B)
          <=> ! [C] : 
                ( r2_hidden(C,k3_xboole_0(k1_relat_1(A),k1_relat_1(B)))
               => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) ) ),
    file(partfun1,d6_partfun1),
    [interesting(0.00)]).

fof(t137_partfun1,theorem,(
    $true ),
    file(partfun1,t137_partfun1),
    [interesting(0.00)]).

fof(t31_grfunc_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_xboole_0(k1_relat_1(A),k1_relat_1(B))
           => ( v1_relat_1(k2_xboole_0(A,B))
              & v1_funct_1(k2_xboole_0(A,B)) ) ) ) ) ),
    file(grfunc_1,t31_grfunc_1),
    [interesting(0.00)]).

fof(t13_partfun1,theorem,(
    $true ),
    file(partfun1,t13_partfun1),
    [interesting(0.00)]).

fof(t8_grfunc_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( r1_tarski(A,B)
          <=> ( r1_tarski(k1_relat_1(A),k1_relat_1(B))
              & ! [C] : 
                  ( r2_hidden(C,k1_relat_1(A))
                 => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) ) ) ),
    file(grfunc_1,t8_grfunc_1),
    [interesting(0.00)]).

fof(t149_partfun1,theorem,(
    $true ),
    file(partfun1,t149_partfun1),
    [interesting(0.00)]).

fof(t14_partfun1,theorem,(
    $true ),
    file(partfun1,t14_partfun1),
    [interesting(0.00)]).

fof(t150_partfun1,theorem,(
    $true ),
    file(partfun1,t150_partfun1),
    [interesting(0.00)]).

fof(t151_partfun1,theorem,(
    $true ),
    file(partfun1,t151_partfun1),
    [interesting(0.00)]).

fof(t152_partfun1,theorem,(
    $true ),
    file(partfun1,t152_partfun1),
    [interesting(0.00)]).

fof(t153_partfun1,theorem,(
    $true ),
    file(partfun1,t153_partfun1),
    [interesting(0.00)]).

fof(t154_partfun1,theorem,(
    $true ),
    file(partfun1,t154_partfun1),
    [interesting(0.00)]).

fof(t155_partfun1,theorem,(
    $true ),
    file(partfun1,t155_partfun1),
    [interesting(0.00)]).

fof(t156_partfun1,theorem,(
    $true ),
    file(partfun1,t156_partfun1),
    [interesting(0.00)]).

fof(t157_partfun1,theorem,(
    $true ),
    file(partfun1,t157_partfun1),
    [interesting(0.00)]).

fof(t159_partfun1,theorem,(
    $true ),
    file(partfun1,t159_partfun1),
    [interesting(0.00)]).

fof(t15_partfun1,theorem,(
    $true ),
    file(partfun1,t15_partfun1),
    [interesting(0.00)]).

fof(t160_partfun1,theorem,(
    $true ),
    file(partfun1,t160_partfun1),
    [interesting(0.00)]).

fof(t161_partfun1,theorem,(
    $true ),
    file(partfun1,t161_partfun1),
    [interesting(0.00)]).

fof(t163_partfun1,theorem,(
    $true ),
    file(partfun1,t163_partfun1),
    [interesting(0.00)]).

fof(t164_partfun1,theorem,(
    $true ),
    file(partfun1,t164_partfun1),
    [interesting(0.00)]).

fof(t165_partfun1,theorem,(
    $true ),
    file(partfun1,t165_partfun1),
    [interesting(0.00)]).

fof(t166_partfun1,theorem,(
    $true ),
    file(partfun1,t166_partfun1),
    [interesting(0.00)]).

fof(t167_partfun1,theorem,(
    $true ),
    file(partfun1,t167_partfun1),
    [interesting(0.00)]).

fof(t16_partfun1,theorem,(
    $true ),
    file(partfun1,t16_partfun1),
    [interesting(0.00)]).

fof(t170_partfun1,theorem,(
    $true ),
    file(partfun1,t170_partfun1),
    [interesting(0.00)]).

fof(d7_partfun1,definition,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( D = k5_partfun1(A,B,C)
        <=> ! [E] : 
              ( r2_hidden(E,D)
            <=> ? [F] : 
                  ( v1_funct_1(F)
                  & m2_relset_1(F,A,B)
                  & F = E
                  & v1_partfun1(F,A,B)
                  & r1_partfun1(C,F) ) ) ) ) ),
    file(partfun1,d7_partfun1),
    [interesting(0.00)]).

fof(t173_partfun1,theorem,(
    $true ),
    file(partfun1,t173_partfun1),
    [interesting(0.00)]).

fof(t28_xboole_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => k3_xboole_0(A,B) = A ) ),
    file(xboole_1,t28_xboole_1),
    [interesting(0.00)]).

fof(t177_partfun1,theorem,(
    $true ),
    file(partfun1,t177_partfun1),
    [interesting(0.00)]).

fof(t178_partfun1,theorem,(
    $true ),
    file(partfun1,t178_partfun1),
    [interesting(0.00)]).

fof(t179_partfun1,theorem,(
    $true ),
    file(partfun1,t179_partfun1),
    [interesting(0.00)]).

fof(t17_partfun1,theorem,(
    $true ),
    file(partfun1,t17_partfun1),
    [interesting(0.00)]).

fof(t180_partfun1,theorem,(
    $true ),
    file(partfun1,t180_partfun1),
    [interesting(0.00)]).

fof(t181_partfun1,theorem,(
    $true ),
    file(partfun1,t181_partfun1),
    [interesting(0.00)]).

fof(t182_partfun1,theorem,(
    $true ),
    file(partfun1,t182_partfun1),
    [interesting(0.00)]).

fof(t183_partfun1,theorem,(
    $true ),
    file(partfun1,t183_partfun1),
    [interesting(0.00)]).

fof(t184_partfun1,theorem,(
    $true ),
    file(partfun1,t184_partfun1),
    [interesting(0.00)]).

fof(d7_xboole_0,definition,(
    ! [A,B] : 
      ( r1_xboole_0(A,B)
    <=> k3_xboole_0(A,B) = k1_xboole_0 ) ),
    file(xboole_0,d7_xboole_0),
    [interesting(0.00)]).

fof(t18_partfun1,theorem,(
    $true ),
    file(partfun1,t18_partfun1),
    [interesting(0.00)]).

fof(t19_partfun1,theorem,(
    $true ),
    file(partfun1,t19_partfun1),
    [interesting(0.00)]).

fof(t20_partfun1,theorem,(
    $true ),
    file(partfun1,t20_partfun1),
    [interesting(0.00)]).

fof(t21_partfun1,theorem,(
    $true ),
    file(partfun1,t21_partfun1),
    [interesting(0.00)]).

fof(t22_partfun1,theorem,(
    $true ),
    file(partfun1,t22_partfun1),
    [interesting(0.00)]).

fof(t23_partfun1,theorem,(
    $true ),
    file(partfun1,t23_partfun1),
    [interesting(0.00)]).

fof(t77_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( r1_tarski(k1_relat_1(B),A)
       => k5_relat_1(k6_relat_1(A),B) = B ) ) ),
    file(relat_1,t77_relat_1),
    [interesting(0.00)]).

fof(t79_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( r1_tarski(k2_relat_1(B),A)
       => k5_relat_1(B,k6_relat_1(A)) = B ) ) ),
    file(relat_1,t79_relat_1),
    [interesting(0.00)]).

fof(d8_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
      <=> ! [B,C] : 
            ( ( r2_hidden(B,k1_relat_1(A))
              & r2_hidden(C,k1_relat_1(A))
              & k1_funct_1(A,B) = k1_funct_1(A,C) )
           => B = C ) ) ) ),
    file(funct_1,d8_funct_1),
    [interesting(0.00)]).

fof(t55_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
       => ( k2_relat_1(A) = k1_relat_1(k2_funct_1(A))
          & k1_relat_1(A) = k2_relat_1(k2_funct_1(A)) ) ) ) ),
    file(funct_1,t55_funct_1),
    [interesting(0.00)]).

fof(t40_partfun1,theorem,(
    $true ),
    file(partfun1,t40_partfun1),
    [interesting(0.00)]).

fof(t41_partfun1,theorem,(
    $true ),
    file(partfun1,t41_partfun1),
    [interesting(0.00)]).

fof(t42_partfun1,theorem,(
    $true ),
    file(partfun1,t42_partfun1),
    [interesting(0.00)]).

fof(t44_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ( v1_funct_1(k8_relset_1(A,B,D,C))
        & m2_relset_1(k8_relset_1(A,B,D,C),A,B) ) ) ),
    file(partfun1,t44_partfun1),
    [interesting(0.00)]).

fof(t116_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => r1_tarski(k2_relat_1(k8_relat_1(A,B)),A) ) ),
    file(relat_1,t116_relat_1),
    [interesting(0.00)]).

fof(t46_partfun1,theorem,(
    ! [A,B,C,D] : 
      ( ( v1_funct_1(D)
        & m2_relset_1(D,A,B) )
     => ( v1_funct_1(k9_relset_1(A,B,C,D))
        & m2_relset_1(k9_relset_1(A,B,C,D),A,B) ) ) ),
    file(partfun1,t46_partfun1),
    [interesting(0.00)]).

fof(t140_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => k7_relat_1(k8_relat_1(A,C),B) = k8_relat_1(A,k7_relat_1(C,B)) ) ),
    file(relat_1,t140_relat_1),
    [interesting(0.00)]).

fof(t48_partfun1,theorem,(
    $true ),
    file(partfun1,t48_partfun1),
    [interesting(0.00)]).

fof(t4_partfun1,theorem,(
    $true ),
    file(partfun1,t4_partfun1),
    [interesting(0.00)]).

fof(t50_partfun1,theorem,(
    $true ),
    file(partfun1,t50_partfun1),
    [interesting(0.00)]).

fof(t156_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( r1_tarski(A,B)
       => r1_tarski(k9_relat_1(C,A),k9_relat_1(C,B)) ) ) ),
    file(relat_1,t156_relat_1),
    [interesting(0.00)]).

fof(t144_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => r1_tarski(k9_relat_1(B,A),k2_relat_1(B)) ) ),
    file(relat_1,t144_relat_1),
    [interesting(0.00)]).

fof(t146_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => k9_relat_1(A,k1_relat_1(A)) = k2_relat_1(A) ) ),
    file(relat_1,t146_relat_1),
    [interesting(0.00)]).

fof(t52_partfun1,theorem,(
    $true ),
    file(partfun1,t52_partfun1),
    [interesting(0.00)]).

fof(t178_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( r1_tarski(A,B)
       => r1_tarski(k10_relat_1(C,A),k10_relat_1(C,B)) ) ) ),
    file(relat_1,t178_relat_1),
    [interesting(0.00)]).

fof(t167_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => r1_tarski(k10_relat_1(B,A),k1_relat_1(B)) ) ),
    file(relat_1,t167_relat_1),
    [interesting(0.00)]).

fof(t169_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => k10_relat_1(A,k2_relat_1(A)) = k1_relat_1(A) ) ),
    file(relat_1,t169_relat_1),
    [interesting(0.00)]).

fof(t5_partfun1,theorem,(
    $true ),
    file(partfun1,t5_partfun1),
    [interesting(0.00)]).

fof(t150_relat_1,theorem,(
    ! [A] : k9_relat_1(k1_xboole_0,A) = k1_xboole_0 ),
    file(relat_1,t150_relat_1),
    [interesting(0.00)]).

fof(t172_relat_1,theorem,(
    ! [A] : k10_relat_1(k1_xboole_0,A) = k1_xboole_0 ),
    file(relat_1,t172_relat_1),
    [interesting(0.00)]).

fof(t6_partfun1,theorem,(
    $true ),
    file(partfun1,t6_partfun1),
    [interesting(0.00)]).

fof(t39_zfmisc_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,k1_tarski(B))
    <=> ( A = k1_xboole_0
        | A = k1_tarski(B) ) ) ),
    file(zfmisc_1,t39_zfmisc_1),
    [interesting(0.00)]).

fof(t14_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( k1_relat_1(B) = k1_tarski(A)
       => k2_relat_1(B) = k1_tarski(k1_funct_1(B,A)) ) ) ),
    file(funct_1,t14_funct_1),
    [interesting(0.00)]).

fof(t37_zfmisc_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(k1_tarski(A),B)
    <=> r2_hidden(A,B) ) ),
    file(zfmisc_1,t37_zfmisc_1),
    [interesting(0.00)]).

fof(t75_partfun1,theorem,(
    $true ),
    file(partfun1,t75_partfun1),
    [interesting(0.00)]).

fof(t7_partfun1,theorem,(
    $true ),
    file(partfun1,t7_partfun1),
    [interesting(0.00)]).

fof(t88_partfun1,theorem,(
    $true ),
    file(partfun1,t88_partfun1),
    [interesting(0.00)]).

fof(t89_partfun1,theorem,(
    $true ),
    file(partfun1,t89_partfun1),
    [interesting(0.00)]).

fof(t8_partfun1,theorem,(
    $true ),
    file(partfun1,t8_partfun1),
    [interesting(0.00)]).

fof(t90_partfun1,theorem,(
    $true ),
    file(partfun1,t90_partfun1),
    [interesting(0.00)]).

fof(t21_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( r2_hidden(A,k1_relat_1(k5_relat_1(C,B)))
          <=> ( r2_hidden(A,k1_relat_1(C))
              & r2_hidden(k1_funct_1(C,A),k1_relat_1(B)) ) ) ) ) ),
    file(funct_1,t21_funct_1),
    [interesting(0.00)]).

fof(t23_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( r2_hidden(A,k1_relat_1(B))
           => k1_funct_1(k5_relat_1(B,C),A) = k1_funct_1(C,k1_funct_1(B,A)) ) ) ) ),
    file(funct_1,t23_funct_1),
    [interesting(0.00)]).

fof(t22_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( r2_hidden(A,k1_relat_1(k5_relat_1(C,B)))
           => k1_funct_1(k5_relat_1(C,B),A) = k1_funct_1(B,k1_funct_1(C,A)) ) ) ) ),
    file(funct_1,t22_funct_1),
    [interesting(0.00)]).

fof(t99_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( v2_funct_1(B)
       => v2_funct_1(k8_relat_1(A,B)) ) ) ),
    file(funct_1,t99_funct_1),
    [interesting(0.00)]).

fof(t84_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( v2_funct_1(B)
       => v2_funct_1(k7_relat_1(B,A)) ) ) ),
    file(funct_1,t84_funct_1),
    [interesting(0.00)]).

fof(t54_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
       => ! [B] : 
            ( ( v1_relat_1(B)
              & v1_funct_1(B) )
           => ( B = k2_funct_1(A)
            <=> ( k1_relat_1(B) = k2_relat_1(A)
                & ! [C,D] : 
                    ( ( ( r2_hidden(C,k2_relat_1(A))
                        & D = k1_funct_1(B,C) )
                     => ( r2_hidden(D,k1_relat_1(A))
                        & C = k1_funct_1(A,D) ) )
                    & ( ( r2_hidden(D,k1_relat_1(A))
                        & C = k1_funct_1(A,D) )
                     => ( r2_hidden(C,k2_relat_1(A))
                        & D = k1_funct_1(B,C) ) ) ) ) ) ) ) ) ),
    file(funct_1,t54_funct_1),
    [interesting(0.00)]).

fof(t56_funct_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( ( v2_funct_1(B)
          & r2_hidden(A,k1_relat_1(B)) )
       => ( A = k1_funct_1(k2_funct_1(B),k1_funct_1(B,A))
          & A = k1_funct_1(k5_relat_1(B,k2_funct_1(B)),A) ) ) ) ),
    file(funct_1,t56_funct_1),
    [interesting(0.00)]).

fof(t2_tarski,theorem,(
    ! [A,B] : 
      ( ! [C] : 
          ( r2_hidden(C,A)
        <=> r2_hidden(C,B) )
     => A = B ) ),
    file(tarski,t2_tarski),
    [interesting(0.00)]).

fof(t100_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => k7_relat_1(k7_relat_1(C,A),B) = k7_relat_1(C,k3_xboole_0(A,B)) ) ),
    file(relat_1,t100_relat_1),
    [interesting(0.00)]).

fof(t127_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => k8_relat_1(A,k8_relat_1(B,C)) = k8_relat_1(k3_xboole_0(A,B),C) ) ),
    file(relat_1,t127_relat_1),
    [interesting(0.00)]).

fof(t98_partfun1,theorem,(
    $true ),
    file(partfun1,t98_partfun1),
    [interesting(0.00)]).

fof(t9_partfun1,theorem,(
    $true ),
    file(partfun1,t9_partfun1),
    [interesting(0.00)]).