fof(t34_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => B = k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t33_bvfunc25,t19_bvfunc_1,t27_bvfunc_8,t19_bvfunc_1,t18_bvfunc_1]),
    [file(bvfunc25,t34_bvfunc25),interesting(1.00)]).

fof(t4_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,C) = k15_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_4,t3_bvfunc25,t3_bvfunc25,t7_bvfunc_4]),
    [file(bvfunc25,t4_bvfunc25),interesting(0.94)]).

fof(t32_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => B = k14_bvfunc_1(A,k5_valuat_1(A,B),B) ) ) ),
    inference(mizar_proof,[status(thm)],[t22_bvfunc25,t19_bvfunc_1,t12_bvfunc_5,t19_bvfunc_1,t18_bvfunc_1]),
    [file(bvfunc25,t32_bvfunc25),interesting(0.86)]).

fof(t3_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,B,C) = k14_bvfunc_1(A,k5_valuat_1(A,C),k5_valuat_1(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_bvfunc25,t19_bvfunc_1,t33_bvfunc_5,t19_bvfunc_1,t18_bvfunc_1]),
    [file(bvfunc25,t3_bvfunc25),interesting(0.83)]).

fof(t33_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,B,k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),B)) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t16_bvfunc_1,t4_bvfunc_1,t14_bvfunc_1,t10_bvfunc_1,t15_bvfunc_1,t6_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1]),
    [file(bvfunc25,t33_bvfunc25),interesting(0.75)]).

fof(t15_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,C,B)) = k14_bvfunc_1(A,C,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t16_bvfunc_1,t4_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t10_bvfunc_1,t14_bvfunc_1,t11_bvfunc_1,t10_bvfunc_1,t6_bvfunc_1,t8_bvfunc_4]),
    [file(bvfunc25,t15_bvfunc25),interesting(0.70)]).

fof(t5_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,B,C) = k14_bvfunc_1(A,B,k6_valuat_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t8_bvfunc_4]),
    [file(bvfunc25,t5_bvfunc25),interesting(0.68)]).

fof(t13_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k9_bvfunc_1(A,B,B) = k18_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t5_bvfunc_4,t5_bvfunc_4,t10_bvfunc_1]),
    [file(bvfunc25,t13_bvfunc25),interesting(0.60)]).

fof(t22_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k14_bvfunc_1(A,B,k14_bvfunc_1(A,k5_valuat_1(A,B),B)) = k19_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t4_bvfunc_1,t10_bvfunc_1,t6_bvfunc_4]),
    [file(bvfunc25,t22_bvfunc25),interesting(0.55)]).

fof(t30_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,B,C) = k15_bvfunc_1(A,B,k6_valuat_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t17_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t9_bvfunc_1,t8_bvfunc_4]),
    [file(bvfunc25,t30_bvfunc25),interesting(0.54)]).

fof(t38_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k8_bvfunc_1(A,B,C) = k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t16_bvfunc_1,t4_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1]),
    [file(bvfunc25,t38_bvfunc25),interesting(0.53)]).

fof(t2_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k14_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)),k14_bvfunc_1(A,C,B)) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t4_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t8_bvfunc_4,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1]),
    [file(bvfunc25,t2_bvfunc25),interesting(0.50)]).

fof(t11_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k6_valuat_1(A,B,k9_bvfunc_1(A,C,D)) = k9_bvfunc_1(A,k6_valuat_1(A,B,C),k6_valuat_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t15_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t9_bvfunc_4,t17_bvfunc_1,t17_bvfunc_1,t15_bvfunc_1,t15_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t5_bvfunc_4,t5_bvfunc_4,t8_bvfunc_1,t8_bvfunc_1,t10_bvfunc_1,t12_bvfunc_1]),
    [file(bvfunc25,t11_bvfunc25),interesting(0.49)]).

fof(t46_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,B,k14_bvfunc_1(A,B,C)),k14_bvfunc_1(A,C,D)),D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t10_bvfunc_7,t7_bvfunc_1,t10_bvfunc_7,t7_bvfunc_1,t17_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t19_bvfunc_1]),
    [file(bvfunc25,t46_bvfunc25),interesting(0.44)]).

fof(t39_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,B)) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_5,t16_bvfunc_7]),
    [file(bvfunc25,t39_bvfunc25),interesting(0.43)]).

fof(t14_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k9_bvfunc_1(A,B,k5_valuat_1(A,B)) = k19_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t4_bvfunc_1,t6_bvfunc_1,t6_bvfunc_1,t6_bvfunc_4]),
    [file(bvfunc25,t14_bvfunc25),interesting(0.41)]).

fof(t36_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k6_valuat_1(A,B,C) = k5_valuat_1(A,k14_bvfunc_1(A,B,k5_valuat_1(A,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_bvfunc_6,t19_bvfunc_1,t36_bvfunc_6,t19_bvfunc_1,t18_bvfunc_1]),
    [file(bvfunc25,t36_bvfunc25),interesting(0.40)]).

fof(t6_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,C) = k14_bvfunc_1(A,k8_bvfunc_1(A,B,C),k6_valuat_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_bvfunc_7,t5_bvfunc25,t5_bvfunc25,t7_bvfunc_4]),
    [file(bvfunc25,t6_bvfunc25),interesting(0.40)]).

fof(t24_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k8_bvfunc_1(A,B,k14_bvfunc_1(A,B,C)) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1]),
    [file(bvfunc25,t24_bvfunc25),interesting(0.39)]).

fof(t7_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k15_bvfunc_1(A,B,k5_valuat_1(A,B)) = k18_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t10_bvfunc_1,t4_bvfunc_1,t10_bvfunc_1,t5_bvfunc_4]),
    [file(bvfunc25,t7_bvfunc25),interesting(0.39)]).

fof(t23_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k15_bvfunc_1(A,k14_bvfunc_1(A,k5_valuat_1(A,B),B),B) = k19_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_4,t12_bvfunc_5,t9_bvfunc_1,t22_bvfunc25]),
    [file(bvfunc25,t23_bvfunc25),interesting(0.36)]).

fof(t20_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k14_bvfunc_1(A,k5_valuat_1(A,k5_valuat_1(A,B)),B) = k19_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t4_bvfunc_1,t8_bvfunc_5]),
    [file(bvfunc25,t20_bvfunc25),interesting(0.32)]).

fof(t41_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),B),D),C) = k19_bvfunc_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,t8_bvfunc_4,t17_bvfunc_1,t17_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1]),
    [file(bvfunc25,t41_bvfunc25),interesting(0.31)]).

fof(t21_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),B),C) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_bvfunc_7,t41_bvfunc_6]),
    [file(bvfunc25,t21_bvfunc25),interesting(0.30)]).

fof(t42_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k6_valuat_1(A,D,B),C)) = k19_bvfunc_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t16_bvfunc_1,t4_bvfunc_1,t17_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1]),
    [file(bvfunc25,t42_bvfunc25),interesting(0.28)]).

fof(t1_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k5_valuat_1(A,k14_bvfunc_1(A,B,C)) = k6_valuat_1(A,B,k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t16_bvfunc_1,t4_bvfunc_1]),
    [file(bvfunc25,t1_bvfunc25),interesting(0.27)]).

fof(t16_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k6_valuat_1(A,k8_bvfunc_1(A,B,C),k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C))) = k8_bvfunc_1(A,k6_valuat_1(A,k5_valuat_1(A,B),C),k6_valuat_1(A,B,k5_valuat_1(A,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t13_bvfunc_8]),
    [file(bvfunc25,t16_bvfunc25),interesting(0.26)]).

fof(t35_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => B = k6_valuat_1(A,k14_bvfunc_1(A,C,B),k14_bvfunc_1(A,k5_valuat_1(A,C),B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_8,t8_bvfunc_4,t4_bvfunc_1,t8_bvfunc_4]),
    [file(bvfunc25,t35_bvfunc25),interesting(0.26)]).

fof(t17_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k8_bvfunc_1(A,k6_valuat_1(A,B,C),k6_valuat_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C))) = k6_valuat_1(A,k8_bvfunc_1(A,k5_valuat_1(A,B),C),k8_bvfunc_1(A,B,k5_valuat_1(A,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t4_bvfunc_1,t16_bvfunc25,t4_bvfunc_1]),
    [file(bvfunc25,t17_bvfunc25),interesting(0.25)]).

fof(t37_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k8_bvfunc_1(A,B,C) = k14_bvfunc_1(A,k5_valuat_1(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t4_bvfunc_1]),
    [file(bvfunc25,t37_bvfunc25),interesting(0.24)]).

fof(t10_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,C) = k9_bvfunc_1(A,B,k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_bvfunc_8,t4_bvfunc_1,t17_bvfunc_8]),
    [file(bvfunc25,t10_bvfunc25),interesting(0.23)]).

fof(t25_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k8_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,D,B)) = k19_bvfunc_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1]),
    [file(bvfunc25,t25_bvfunc25),interesting(0.22)]).

fof(t43_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,k14_bvfunc_1(A,k6_valuat_1(A,B,C),D),k14_bvfunc_1(A,k6_valuat_1(A,B,C),k6_valuat_1(A,D,C))) = k19_bvfunc_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t16_bvfunc_1,t4_bvfunc_1,t17_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1]),
    [file(bvfunc25,t43_bvfunc25),interesting(0.21)]).

fof(t12_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,C) = k5_valuat_1(A,k9_bvfunc_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_bvfunc_8,t4_bvfunc_1]),
    [file(bvfunc25,t12_bvfunc25),interesting(0.18)]).

fof(t45_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k6_valuat_1(A,B,D)),k6_valuat_1(A,C,D)) = k19_bvfunc_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_1,t10_bvfunc_7,t7_bvfunc_1,t39_bvfunc_6]),
    [file(bvfunc25,t45_bvfunc25),interesting(0.18)]).

fof(t27_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k8_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,k5_valuat_1(A,C))) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1]),
    [file(bvfunc25,t27_bvfunc25),interesting(0.15)]).

fof(t28_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k5_valuat_1(A,B),k15_bvfunc_1(A,k5_valuat_1(A,C),k14_bvfunc_1(A,C,B))) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t7_bvfunc_4,t4_bvfunc_1,t8_bvfunc_4,t4_bvfunc_1,t8_bvfunc_4,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t9_bvfunc_1,t8_bvfunc_4,t8_bvfunc_4,t16_bvfunc_1,t4_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1]),
    [file(bvfunc25,t28_bvfunc25),interesting(0.15)]).

fof(t44_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k6_valuat_1(A,B,D),k6_valuat_1(A,C,D))) = k19_bvfunc_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_bvfunc_9,t19_bvfunc_1]),
    [file(bvfunc25,t44_bvfunc25),interesting(0.13)]).

fof(t26_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k8_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k5_valuat_1(A,B),C)) = k19_bvfunc_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t4_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1]),
    [file(bvfunc25,t26_bvfunc25),interesting(0.10)]).

fof(t12_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k9_bvfunc_1(A,B,C) = k5_valuat_1(A,k15_bvfunc_1(A,B,C)) ) ) ) ),
    file(bvfunc_8,t12_bvfunc_8),
    [interesting(0.00)]).

fof(t4_bvfunc_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_valuat_1(A) )
     => k3_valuat_1(k3_valuat_1(A)) = A ) ),
    file(bvfunc_1,t4_bvfunc_1),
    [interesting(0.00)]).

fof(t17_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k5_valuat_1(A,k9_bvfunc_1(A,B,C)) = k9_bvfunc_1(A,B,k5_valuat_1(A,C)) ) ) ) ),
    file(bvfunc_8,t17_bvfunc_8),
    [interesting(0.00)]).

fof(t9_bvfunc_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k9_bvfunc_1(A,B,C) = k8_bvfunc_1(A,k6_valuat_1(A,k5_valuat_1(A,B),C),k6_valuat_1(A,B,k5_valuat_1(A,C))) ) ) ) ),
    file(bvfunc_4,t9_bvfunc_4),
    [interesting(0.00)]).

fof(t15_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k6_valuat_1(A,k8_bvfunc_1(A,B,C),D) = k8_bvfunc_1(A,k6_valuat_1(A,B,D),k6_valuat_1(A,C,D)) ) ) ) ) ),
    file(bvfunc_1,t15_bvfunc_1),
    [interesting(0.00)]).

fof(t7_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k6_valuat_1(A,k6_valuat_1(A,B,C),D) = k6_valuat_1(A,B,k6_valuat_1(A,C,D)) ) ) ) ) ),
    file(bvfunc_1,t7_bvfunc_1),
    [interesting(0.00)]).

fof(t17_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k5_valuat_1(A,k6_valuat_1(A,B,C)) = k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)) ) ) ) ),
    file(bvfunc_1,t17_bvfunc_1),
    [interesting(0.00)]).

fof(t11_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D) = k8_bvfunc_1(A,B,k8_bvfunc_1(A,C,D)) ) ) ) ) ),
    file(bvfunc_1,t11_bvfunc_1),
    [interesting(0.00)]).

fof(t5_bvfunc_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k6_valuat_1(A,B,k5_valuat_1(A,B)) = k18_bvfunc_1(A) ) ) ),
    file(bvfunc_4,t5_bvfunc_4),
    [interesting(0.00)]).

fof(t8_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k6_valuat_1(A,B,k18_bvfunc_1(A)) = k18_bvfunc_1(A) ) ) ),
    file(bvfunc_1,t8_bvfunc_1),
    [interesting(0.00)]).

fof(t10_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k8_bvfunc_1(A,B,B) = B ) ) ),
    file(bvfunc_1,t10_bvfunc_1),
    [interesting(0.00)]).

fof(t12_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k8_bvfunc_1(A,B,k18_bvfunc_1(A)) = B ) ) ),
    file(bvfunc_1,t12_bvfunc_1),
    [interesting(0.00)]).

fof(t6_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k6_valuat_1(A,B,B) = B ) ) ) ),
    file(bvfunc_1,t6_bvfunc_1),
    [interesting(0.00)]).

fof(t6_bvfunc_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k8_bvfunc_1(A,B,k5_valuat_1(A,B)) = k19_bvfunc_1(A) ) ) ),
    file(bvfunc_4,t6_bvfunc_4),
    [interesting(0.00)]).

fof(t8_bvfunc_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,B,C) = k8_bvfunc_1(A,k5_valuat_1(A,B),C) ) ) ) ),
    file(bvfunc_4,t8_bvfunc_4),
    [interesting(0.00)]).

fof(t16_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k5_valuat_1(A,k8_bvfunc_1(A,B,C)) = k6_valuat_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)) ) ) ) ),
    file(bvfunc_1,t16_bvfunc_1),
    [interesting(0.00)]).

fof(t14_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k8_bvfunc_1(A,k6_valuat_1(A,B,C),D) = k6_valuat_1(A,k8_bvfunc_1(A,B,D),k8_bvfunc_1(A,C,D)) ) ) ) ) ),
    file(bvfunc_1,t14_bvfunc_1),
    [interesting(0.00)]).

fof(t13_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k9_bvfunc_1(A,B,C) = k6_valuat_1(A,k8_bvfunc_1(A,B,C),k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C))) ) ) ) ),
    file(bvfunc_8,t13_bvfunc_8),
    [interesting(0.00)]).

fof(t18_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k9_bvfunc_1(A,B,k9_bvfunc_1(A,C,D)) = k9_bvfunc_1(A,k9_bvfunc_1(A,B,C),D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t9_bvfunc_4,t9_bvfunc_4,t15_bvfunc_1,t16_bvfunc_1,t17_bvfunc_1,t4_bvfunc_1,t17_bvfunc_1,t4_bvfunc_1,t17_bvfunc25,t15_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t11_bvfunc_1,t9_bvfunc_4,t9_bvfunc_4,t16_bvfunc_1,t17_bvfunc_1,t4_bvfunc_1,t17_bvfunc_1,t4_bvfunc_1,t15_bvfunc_1,t17_bvfunc25,t15_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1]),
    [file(bvfunc25,t18_bvfunc25),interesting(0.00)]).

fof(t7_bvfunc_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k15_bvfunc_1(A,B,C) = k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,C,B)) ) ) ) ),
    file(bvfunc_4,t7_bvfunc_4),
    [interesting(0.00)]).

fof(t19_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k15_bvfunc_1(A,B,k15_bvfunc_1(A,C,D)) = k15_bvfunc_1(A,k15_bvfunc_1(A,B,C),D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_4,t7_bvfunc_4,t7_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t17_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t16_bvfunc25,t14_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t7_bvfunc_1,t7_bvfunc_4,t7_bvfunc_4,t7_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t17_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t16_bvfunc25,t14_bvfunc_1,t14_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1]),
    [file(bvfunc25,t19_bvfunc25),interesting(0.00)]).

fof(t8_bvfunc_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k14_bvfunc_1(A,B,B) = k19_bvfunc_1(A) ) ) ),
    file(bvfunc_5,t8_bvfunc_5),
    [interesting(0.00)]).

fof(t10_bvfunc_7,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k6_valuat_1(A,B,k14_bvfunc_1(A,B,C)) = k6_valuat_1(A,B,C) ) ) ) ),
    file(bvfunc_7,t10_bvfunc_7),
    [interesting(0.00)]).

fof(t41_bvfunc_6,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k6_valuat_1(A,B,C),C) = k19_bvfunc_1(A) ) ) ) ),
    file(bvfunc_6,t41_bvfunc_6),
    [interesting(0.00)]).

fof(t12_bvfunc_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k14_bvfunc_1(A,k14_bvfunc_1(A,k5_valuat_1(A,B),B),B) = k19_bvfunc_1(A) ) ) ),
    file(bvfunc_5,t12_bvfunc_5),
    [interesting(0.00)]).

fof(t9_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k6_valuat_1(A,B,k19_bvfunc_1(A)) = B ) ) ),
    file(bvfunc_1,t9_bvfunc_1),
    [interesting(0.00)]).

fof(t13_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k8_bvfunc_1(A,B,k19_bvfunc_1(A)) = k19_bvfunc_1(A) ) ) ),
    file(bvfunc_1,t13_bvfunc_1),
    [interesting(0.00)]).

fof(t29_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k14_bvfunc_1(A,k14_bvfunc_1(A,B,D),C),C)) = k19_bvfunc_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t16_bvfunc_1,t4_bvfunc_1,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t16_bvfunc_1,t4_bvfunc_1,t16_bvfunc_1,t17_bvfunc_1,t4_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1]),
    [file(bvfunc25,t29_bvfunc25),interesting(0.00)]).

fof(t10_bvfunc_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ( k15_bvfunc_1(A,B,C) = k19_bvfunc_1(A)
              <=> ( k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A)
                  & k14_bvfunc_1(A,C,B) = k19_bvfunc_1(A) ) ) ) ) ) ),
    file(bvfunc_4,t10_bvfunc_4),
    [interesting(0.00)]).

fof(t20_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ( k15_bvfunc_1(A,B,C) = k19_bvfunc_1(A)
              <=> B = C ) ) ) ) ),
    file(bvfunc_1,t20_bvfunc_1),
    [interesting(0.00)]).

fof(t31_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ( ( k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A)
                  & k14_bvfunc_1(A,C,B) = k19_bvfunc_1(A) )
              <=> B = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_bvfunc_4,t20_bvfunc_1]),
    [file(bvfunc25,t31_bvfunc25),interesting(0.00)]).

fof(t19_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ( k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A)
              <=> r1_bvfunc_1(A,B,C) ) ) ) ) ),
    file(bvfunc_1,t19_bvfunc_1),
    [interesting(0.00)]).

fof(t18_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => ( ( ( r1_bvfunc_1(A,B,C)
                        & r1_bvfunc_1(A,C,B) )
                     => B = C )
                    & ( ( r1_bvfunc_1(A,B,C)
                        & r1_bvfunc_1(A,C,D) )
                     => r1_bvfunc_1(A,B,D) ) ) ) ) ) ) ),
    file(bvfunc_1,t18_bvfunc_1),
    [interesting(0.00)]).

fof(t27_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),B),B) = k19_bvfunc_1(A) ) ) ) ),
    file(bvfunc_8,t27_bvfunc_8),
    [interesting(0.00)]).

fof(t7_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => B = k6_valuat_1(A,k8_bvfunc_1(A,B,C),k8_bvfunc_1(A,B,k5_valuat_1(A,C))) ) ) ) ),
    file(bvfunc_8,t7_bvfunc_8),
    [interesting(0.00)]).

fof(t35_bvfunc_6,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k6_valuat_1(A,B,C),k5_valuat_1(A,k14_bvfunc_1(A,B,k5_valuat_1(A,C)))) = k19_bvfunc_1(A) ) ) ) ),
    file(bvfunc_6,t35_bvfunc_6),
    [interesting(0.00)]).

fof(t36_bvfunc_6,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k5_valuat_1(A,k14_bvfunc_1(A,B,k5_valuat_1(A,C))),k6_valuat_1(A,B,C)) = k19_bvfunc_1(A) ) ) ) ),
    file(bvfunc_6,t36_bvfunc_6),
    [interesting(0.00)]).

fof(t16_bvfunc_7,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k14_bvfunc_1(A,B,k19_bvfunc_1(A)) = k19_bvfunc_1(A) ) ) ),
    file(bvfunc_7,t16_bvfunc_7),
    [interesting(0.00)]).

fof(t40_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => k14_bvfunc_1(A,k14_bvfunc_1(A,B,k14_bvfunc_1(A,C,D)),k14_bvfunc_1(A,k14_bvfunc_1(A,E,C),k14_bvfunc_1(A,B,k14_bvfunc_1(A,E,D)))) = k19_bvfunc_1(A) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t16_bvfunc_1,t16_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t4_bvfunc_1,t4_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1,t13_bvfunc_1]),
    [file(bvfunc25,t40_bvfunc25),interesting(0.00)]).

fof(t10_bvfunc_9,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => r1_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k6_valuat_1(A,B,D),k6_valuat_1(A,C,D))) ) ) ) ) ),
    file(bvfunc_9,t10_bvfunc_9),
    [interesting(0.00)]).

fof(t39_bvfunc_6,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k6_valuat_1(A,B,C),B) = k19_bvfunc_1(A) ) ) ) ),
    file(bvfunc_6,t39_bvfunc_6),
    [interesting(0.00)]).

fof(t47_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k8_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,D)),k14_bvfunc_1(A,C,D)),k14_bvfunc_1(A,k5_valuat_1(A,B),k8_bvfunc_1(A,C,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t17_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t17_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t14_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t15_bvfunc_1,t7_bvfunc_1,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1,t13_bvfunc_1,t13_bvfunc_1,t19_bvfunc_1]),
    [file(bvfunc25,t47_bvfunc25),interesting(0.00)]).

fof(t33_bvfunc_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k5_valuat_1(A,C),k5_valuat_1(A,B))) = k19_bvfunc_1(A) ) ) ) ),
    file(bvfunc_5,t33_bvfunc_5),
    [interesting(0.00)]).

fof(t5_bvfunc_7,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,k8_bvfunc_1(A,B,C),D) = k6_valuat_1(A,k14_bvfunc_1(A,B,D),k14_bvfunc_1(A,C,D)) ) ) ) ) ),
    file(bvfunc_7,t5_bvfunc_7),
    [interesting(0.00)]).

fof(t8_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,B,k14_bvfunc_1(A,C,D)) = k14_bvfunc_1(A,C,k14_bvfunc_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t11_bvfunc_1,t8_bvfunc_4,t8_bvfunc_4]),
    [file(bvfunc25,t8_bvfunc25),interesting(0.00)]).

fof(t9_bvfunc25,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ! [C] : 
              ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k14_bvfunc_1(A,B,k14_bvfunc_1(A,C,D)) = k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t16_bvfunc_1,t4_bvfunc_1,t11_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t8_bvfunc_4,t8_bvfunc_4]),
    [file(bvfunc25,t9_bvfunc25),interesting(0.00)]).