fof(t20_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k15_bvfunc_1(A,B,k19_bvfunc_1(A)) = B ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t13_bvfunc_1,t5_bvfunc_1,t12_bvfunc_1,t9_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t20_bvfunc_8),interesting(1.00)]).

fof(t15_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k9_bvfunc_1(A,B,k18_bvfunc_1(A)) = B ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t5_bvfunc_1,t9_bvfunc_1,t8_bvfunc_1,t12_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t15_bvfunc_8),interesting(0.97)]).

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) ) ) ) ),
    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,t17_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t14_bvfunc_1,t10_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,d14_bvfunc_1,d14_bvfunc_1]),
    [file(bvfunc_8,t27_bvfunc_8),interesting(0.93)]).

fof(t25_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))
             => r1_bvfunc_1(A,B,k15_bvfunc_1(A,k15_bvfunc_1(A,k8_bvfunc_1(A,B,C),k8_bvfunc_1(A,C,B)),B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,t7_bvfunc_4,d6_valuat_1,t16_binarith,t8_bvfunc_4,t6_bvfunc_4,d14_bvfunc_1,t7_bvfunc_4,d6_valuat_1,t8_bvfunc_4,t8_bvfunc_4,d7_bvfunc_1,d7_bvfunc_1,d5_valuat_1,t41_margrel1,t7_binarith,t19_binarith,t50_margrel1]),
    [file(bvfunc_8,t25_bvfunc_8),interesting(0.86)]).

fof(t22_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,k15_bvfunc_1(A,B,C)) = k15_bvfunc_1(A,B,k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t17_bvfunc_1,t16_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t4_bvfunc_1,t14_bvfunc_1,t14_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t6_bvfunc_4,t9_bvfunc_1,t9_bvfunc_1,t4_bvfunc_1,t8_bvfunc_4,t8_bvfunc_4,t7_bvfunc_4,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t22_bvfunc_8),interesting(0.83)]).

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)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t16_bvfunc_1,t17_bvfunc_1,t17_bvfunc_1,t4_bvfunc_1,t4_bvfunc_1,t15_bvfunc_1,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,t4_bvfunc_1,t9_bvfunc_4,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t17_bvfunc_8),interesting(0.82)]).

fof(t21_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k15_bvfunc_1(A,B,k18_bvfunc_1(A)) = k5_valuat_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t12_bvfunc_1,t5_bvfunc_1,t13_bvfunc_1,t9_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t21_bvfunc_8),interesting(0.80)]).

fof(t14_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k9_bvfunc_1(A,B,k19_bvfunc_1(A)) = k5_valuat_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t5_bvfunc_1,t8_bvfunc_1,t12_bvfunc_1,t9_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t14_bvfunc_8),interesting(0.78)]).

fof(t19_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))
             => k15_bvfunc_1(A,B,C) = k8_bvfunc_1(A,k6_valuat_1(A,B,C),k6_valuat_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t14_bvfunc_1,t14_bvfunc_1,t14_bvfunc_1,t6_bvfunc_4,t6_bvfunc_4,t9_bvfunc_1,t9_bvfunc_1,t18_bvfunc_8,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t19_bvfunc_8),interesting(0.70)]).

fof(t24_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))
             => r1_bvfunc_1(A,k5_valuat_1(A,B),k15_bvfunc_1(A,k14_bvfunc_1(A,C,B),k5_valuat_1(A,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d5_valuat_1,t8_bvfunc_4,t7_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,d6_valuat_1,d7_bvfunc_1,d5_valuat_1,d7_bvfunc_1,d5_valuat_1,t10_binarith,t40_margrel1,d7_bvfunc_1,d7_bvfunc_1,d5_valuat_1,t4_bvfunc_1,t41_margrel1,t50_margrel1,d5_valuat_1,t18_binarith,t50_margrel1,t20_binarith,t18_binarith,t19_binarith]),
    [file(bvfunc_8,t24_bvfunc_8),interesting(0.67)]).

fof(t29_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))
             => ! [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,B,k14_bvfunc_1(A,C,D)),k14_bvfunc_1(A,B,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,t16_bvfunc_1,t16_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t4_bvfunc_1,t4_bvfunc_1,t14_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t9_bvfunc_1,t14_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t9_bvfunc_1,t14_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1,d14_bvfunc_1,d14_bvfunc_1]),
    [file(bvfunc_8,t29_bvfunc_8),interesting(0.66)]).

fof(t10_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))
             => k6_valuat_1(A,B,C) = k6_valuat_1(A,B,k8_bvfunc_1(A,k5_valuat_1(A,B),C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_valuat_1,d7_bvfunc_1,t22_binarith,d5_valuat_1,t46_margrel1,t7_binarith,d6_valuat_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t10_bvfunc_8),interesting(0.65)]).

fof(t11_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))
             => k8_bvfunc_1(A,B,C) = k8_bvfunc_1(A,B,k6_valuat_1(A,k5_valuat_1(A,B),C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_bvfunc_1,d6_valuat_1,t23_binarith,d5_valuat_1,t18_binarith,t50_margrel1,d7_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t11_bvfunc_8),interesting(0.65)]).

fof(t16_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) = k9_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t4_bvfunc_1,t4_bvfunc_1,t9_bvfunc_4,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t16_bvfunc_8),interesting(0.65)]).

fof(t23_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))
             => r1_bvfunc_1(A,k5_valuat_1(A,B),k15_bvfunc_1(A,k14_bvfunc_1(A,B,C),k5_valuat_1(A,B))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d5_valuat_1,t41_margrel1,t8_bvfunc_4,t7_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,d6_valuat_1,d7_bvfunc_1,d5_valuat_1,d7_bvfunc_1,d5_valuat_1,t10_binarith,t40_margrel1,d7_bvfunc_1,d7_bvfunc_1,d5_valuat_1,t4_bvfunc_1,d5_valuat_1,t19_binarith,t50_margrel1,t7_binarith,t19_binarith]),
    [file(bvfunc_8,t23_bvfunc_8),interesting(0.65)]).

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)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_4,t4_bvfunc_1,t16_bvfunc_1,t17_bvfunc_1,t17_bvfunc_1,t4_bvfunc_1,t4_bvfunc_1,t8_bvfunc_4,t8_bvfunc_4,t7_bvfunc_4,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t12_bvfunc_8),interesting(0.64)]).

fof(t6_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 = k8_bvfunc_1(A,k6_valuat_1(A,B,C),k6_valuat_1(A,B,k5_valuat_1(A,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t6_bvfunc_8),interesting(0.61)]).

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))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t14_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t7_bvfunc_8),interesting(0.61)]).

fof(t26_bvfunc_8,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => k14_bvfunc_1(A,B,k15_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,B))) = k19_bvfunc_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t7_bvfunc_4,t6_bvfunc_1,t8_bvfunc_4,t6_bvfunc_4,t13_bvfunc_1,d14_bvfunc_1,d14_bvfunc_1]),
    [file(bvfunc_8,t26_bvfunc_8),interesting(0.57)]).

fof(t18_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))
             => k15_bvfunc_1(A,B,C) = k6_valuat_1(A,k8_bvfunc_1(A,B,k5_valuat_1(A,C)),k8_bvfunc_1(A,k5_valuat_1(A,B),C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t7_bvfunc_4,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t18_bvfunc_8),interesting(0.48)]).

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))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_valuat_1,d7_bvfunc_1,d7_bvfunc_1,t22_binarith,t22_binarith,t22_binarith,d5_valuat_1,d5_valuat_1,t46_margrel1,t46_margrel1,t7_binarith,t7_binarith,d6_valuat_1,d6_valuat_1,d7_bvfunc_1,t9_bvfunc_4,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t13_bvfunc_8),interesting(0.42)]).

fof(t3_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))
             => ! [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,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E) = k8_bvfunc_1(A,k8_bvfunc_1(A,k14_bvfunc_1(A,B,E),k14_bvfunc_1(A,C,E)),k14_bvfunc_1(A,D,E)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_bvfunc_1,d7_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t20_binarith,t20_binarith,t20_binarith,t21_binarith,t9_binarith,t20_binarith,t20_binarith,t20_binarith,t21_binarith,t9_binarith,d6_valuat_1,d6_valuat_1,d11_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t3_bvfunc_8),interesting(0.37)]).

fof(t4_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))
             => ! [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,k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D),E) = k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,E),k14_bvfunc_1(A,C,E)),k14_bvfunc_1(A,D,E)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_valuat_1,d6_valuat_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t23_binarith,t10_binarith,d7_bvfunc_1,t23_binarith,t10_binarith,d7_bvfunc_1,d11_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t4_bvfunc_8),interesting(0.37)]).

fof(t8_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))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => B = k8_bvfunc_1(A,k8_bvfunc_1(A,k8_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),k6_valuat_1(A,k6_valuat_1(A,B,C),k5_valuat_1(A,D))),k6_valuat_1(A,k6_valuat_1(A,B,k5_valuat_1(A,C)),D)),k6_valuat_1(A,k6_valuat_1(A,B,k5_valuat_1(A,C)),k5_valuat_1(A,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t11_bvfunc_1,t15_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,t15_bvfunc_1,t6_bvfunc_4,t9_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t8_bvfunc_8),interesting(0.34)]).

fof(t9_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))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => B = k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D),k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),k5_valuat_1(A,D))),k8_bvfunc_1(A,k8_bvfunc_1(A,B,k5_valuat_1(A,C)),D)),k8_bvfunc_1(A,k8_bvfunc_1(A,B,k5_valuat_1(A,C)),k5_valuat_1(A,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t14_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,t7_bvfunc_1,t14_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,t14_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t9_bvfunc_8),interesting(0.34)]).

fof(d6_valuat_1,definition,(
    ! [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))
                 => ( D = k6_valuat_1(A,B,C)
                  <=> ! [E] : 
                        ( m1_subset_1(E,A)
                       => k8_funct_2(A,k6_margrel1,D,E) = k12_margrel1(k8_funct_2(A,k6_margrel1,B,E),k8_funct_2(A,k6_margrel1,C,E)) ) ) ) ) ) ) ),
    file(valuat_1,d6_valuat_1),
    [interesting(0.00)]).

fof(d7_bvfunc_1,definition,(
    ! [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))
                 => ( D = k8_bvfunc_1(A,B,C)
                  <=> ! [E] : 
                        ( m1_subset_1(E,A)
                       => k8_funct_2(A,k6_margrel1,D,E) = k3_binarith(k8_funct_2(A,k6_margrel1,B,E),k8_funct_2(A,k6_margrel1,C,E)) ) ) ) ) ) ) ),
    file(bvfunc_1,d7_bvfunc_1),
    [interesting(0.00)]).

fof(t22_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ! [B] : 
          ( v2_margrel1(B)
         => ! [C] : 
              ( v2_margrel1(C)
             => k10_margrel1(A,k1_binarith(B,C)) = k1_binarith(k10_margrel1(A,B),k10_margrel1(A,C)) ) ) ) ),
    file(binarith,t22_binarith),
    [interesting(0.00)]).

fof(d5_valuat_1,definition,(
    ! [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))
             => ( C = k5_valuat_1(A,B)
              <=> ! [D] : 
                    ( m1_subset_1(D,A)
                   => k8_funct_2(A,k6_margrel1,C,D) = k11_margrel1(k8_funct_2(A,k6_margrel1,B,D)) ) ) ) ) ) ),
    file(valuat_1,d5_valuat_1),
    [interesting(0.00)]).

fof(t46_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k10_margrel1(A,k9_margrel1(A)) = k7_margrel1 ) ),
    file(margrel1,t46_margrel1),
    [interesting(0.00)]).

fof(t7_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k1_binarith(A,k7_margrel1) = A ) ),
    file(binarith,t7_binarith),
    [interesting(0.00)]).

fof(d2_funct_2,definition,(
    ! [A,B,C] : 
      ( C = k1_funct_2(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ? [E] : 
              ( v1_relat_1(E)
              & v1_funct_1(E)
              & D = E
              & k1_relat_1(E) = A
              & r1_tarski(k2_relat_1(E),B) ) ) ) ),
    file(funct_2,d2_funct_2),
    [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(t23_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ! [B] : 
          ( v2_margrel1(B)
         => ! [C] : 
              ( v2_margrel1(C)
             => k1_binarith(A,k10_margrel1(B,C)) = k10_margrel1(k1_binarith(A,B),k1_binarith(A,C)) ) ) ) ),
    file(binarith,t23_binarith),
    [interesting(0.00)]).

fof(t18_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k1_binarith(A,k9_margrel1(A)) = k8_margrel1 ) ),
    file(binarith,t18_binarith),
    [interesting(0.00)]).

fof(t50_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k10_margrel1(k8_margrel1,A) = A ) ),
    file(margrel1,t50_margrel1),
    [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(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(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(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(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(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(t5_bvfunc_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ( k5_valuat_1(A,k19_bvfunc_1(A)) = k18_bvfunc_1(A)
            & k5_valuat_1(A,k18_bvfunc_1(A)) = k19_bvfunc_1(A) ) ) ) ),
    file(bvfunc_1,t5_bvfunc_1),
    [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(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(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(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(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(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(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(d11_bvfunc_1,definition,(
    ! [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))
                 => ( D = k14_bvfunc_1(A,B,C)
                  <=> ! [E] : 
                        ( m1_subset_1(E,A)
                       => k8_funct_2(A,k6_margrel1,D,E) = k1_binarith(k9_margrel1(k1_funct_1(B,E)),k1_funct_1(C,E)) ) ) ) ) ) ) ),
    file(bvfunc_1,d11_bvfunc_1),
    [interesting(0.00)]).

fof(t1_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))
             => ! [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,B,k6_valuat_1(A,k6_valuat_1(A,C,D),E)) = k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,D)),k14_bvfunc_1(A,B,E)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_valuat_1,d6_valuat_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t23_binarith,t23_binarith,d6_valuat_1,d6_valuat_1,d11_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t1_bvfunc_8),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(d15_bvfunc_1,definition,(
    ! [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))
             => ( r1_bvfunc_1(A,B,C)
              <=> ! [D] : 
                    ( m1_subset_1(D,A)
                   => ( k1_funct_1(B,D) = k8_margrel1
                     => k1_funct_1(C,D) = k8_margrel1 ) ) ) ) ) ) ),
    file(bvfunc_1,d15_bvfunc_1),
    [interesting(0.00)]).

fof(t41_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ( ( A = k7_margrel1
         => k9_margrel1(A) = k8_margrel1 )
        & ( k9_margrel1(A) = k8_margrel1
         => A = k7_margrel1 )
        & ( A = k8_margrel1
         => k9_margrel1(A) = k7_margrel1 )
        & ( k9_margrel1(A) = k7_margrel1
         => A = k8_margrel1 ) ) ) ),
    file(margrel1,t41_margrel1),
    [interesting(0.00)]).

fof(t10_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ! [B] : 
          ( v2_margrel1(B)
         => k9_margrel1(k1_binarith(A,B)) = k10_margrel1(k9_margrel1(A),k9_margrel1(B)) ) ) ),
    file(binarith,t10_binarith),
    [interesting(0.00)]).

fof(t40_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k9_margrel1(k9_margrel1(A)) = A ) ),
    file(margrel1,t40_margrel1),
    [interesting(0.00)]).

fof(t19_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k1_binarith(A,k8_margrel1) = k8_margrel1 ) ),
    file(binarith,t19_binarith),
    [interesting(0.00)]).

fof(t20_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ! [B] : 
          ( v2_margrel1(B)
         => ! [C] : 
              ( v2_margrel1(C)
             => k1_binarith(k1_binarith(A,B),C) = k1_binarith(A,k1_binarith(B,C)) ) ) ) ),
    file(binarith,t20_binarith),
    [interesting(0.00)]).

fof(t16_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k10_margrel1(A,A) = A ) ),
    file(binarith,t16_binarith),
    [interesting(0.00)]).

fof(d14_bvfunc_1,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
         => ( B = k19_bvfunc_1(A)
          <=> ! [C] : 
                ( m1_subset_1(C,A)
               => k1_funct_1(B,C) = k8_margrel1 ) ) ) ) ),
    file(bvfunc_1,d14_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(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(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(t28_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))
             => ! [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,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,D),k14_bvfunc_1(A,C,E)),k8_bvfunc_1(A,k5_valuat_1(A,D),k5_valuat_1(A,E))),k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C))) = k19_bvfunc_1(A) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t17_bvfunc_1,t17_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t4_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,t14_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1,t9_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t13_bvfunc_1,t13_bvfunc_1,d14_bvfunc_1,d14_bvfunc_1]),
    [file(bvfunc_8,t28_bvfunc_8),interesting(0.00)]).

fof(t21_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k1_binarith(A,A) = A ) ),
    file(binarith,t21_binarith),
    [interesting(0.00)]).

fof(t2_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))
             => ! [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,B,k8_bvfunc_1(A,k8_bvfunc_1(A,C,D),E)) = k8_bvfunc_1(A,k8_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,D)),k14_bvfunc_1(A,B,E)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_bvfunc_1,d7_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t20_binarith,t20_binarith,t21_binarith,t20_binarith,d7_bvfunc_1,t20_binarith,t20_binarith,t21_binarith,t20_binarith,d7_bvfunc_1,d11_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t2_bvfunc_8),interesting(0.00)]).

fof(t9_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ! [B] : 
          ( v2_margrel1(B)
         => k9_margrel1(k10_margrel1(A,B)) = k1_binarith(k9_margrel1(A),k9_margrel1(B)) ) ) ),
    file(binarith,t9_binarith),
    [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(t5_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))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,C,D)),k14_bvfunc_1(A,D,B)) = k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,C,D)),k14_bvfunc_1(A,D,B)),k14_bvfunc_1(A,C,B)),k14_bvfunc_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t15_bvfunc_1,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,t14_bvfunc_1,t14_bvfunc_1,t14_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t9_bvfunc_1,t11_bvfunc_1,t10_bvfunc_1,t7_bvfunc_1,t15_bvfunc_1,t15_bvfunc_1,t5_bvfunc_4,t12_bvfunc_1,t14_bvfunc_1,t14_bvfunc_1,t14_bvfunc_1,t11_bvfunc_1,t6_bvfunc_4,t13_bvfunc_1,t9_bvfunc_1,t11_bvfunc_1,t10_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,t8_bvfunc_4,d2_funct_2,d2_funct_2,t9_funct_1]),
    [file(bvfunc_8,t5_bvfunc_8),interesting(0.00)]).