fof(l1_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))
             => r1_bvfunc_1(A,k6_valuat_1(A,B,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,t45_margrel1]),
    [file(bvfunc_9,l1_bvfunc_9),interesting(1.00)]).

fof(t2_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))
             => r1_bvfunc_1(A,k6_valuat_1(A,B,k14_bvfunc_1(A,B,C)),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,t8_bvfunc_4,d7_bvfunc_1,t22_binarith,d5_valuat_1,t46_margrel1,t7_binarith,t43_margrel1,t49_margrel1,t43_margrel1]),
    [file(bvfunc_9,t2_bvfunc_9),interesting(0.91)]).

fof(t28_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))
             => r1_bvfunc_1(A,k6_valuat_1(A,B,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l1_bvfunc_9]),
    [file(bvfunc_9,t28_bvfunc_9),interesting(0.90)]).

fof(t39_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))
             => r1_bvfunc_1(A,B,k8_bvfunc_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,t39_bvfunc_9),interesting(0.88)]).

fof(t40_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))
             => r1_bvfunc_1(A,k6_valuat_1(A,B,C),k8_bvfunc_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l1_bvfunc_9,t39_bvfunc_9,t18_bvfunc_1]),
    [file(bvfunc_9,t40_bvfunc_9),interesting(0.86)]).

fof(l2_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,k6_valuat_1(A,k6_valuat_1(A,B,C),D),B)
                    & r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_1,t39_bvfunc_6,t19_bvfunc_1,t7_bvfunc_1,t39_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,l2_bvfunc_9),interesting(0.84)]).

fof(t34_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ( ( r1_bvfunc_1(A,B,C)
                          & r1_bvfunc_1(A,D,E) )
                       => r1_bvfunc_1(A,k6_valuat_1(A,B,D),k6_valuat_1(A,C,E)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_bvfunc_1,t21_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,t34_bvfunc_9),interesting(0.79)]).

fof(l3_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ( r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),B)
                        & r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),C) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_1,t7_bvfunc_1,t39_bvfunc_6,t19_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t39_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,l3_bvfunc_9),interesting(0.77)]).

fof(t19_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => r1_bvfunc_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,D,E)),k14_bvfunc_1(A,k6_valuat_1(A,B,D),k6_valuat_1(A,C,E))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,t8_bvfunc_4,t8_bvfunc_4,d7_bvfunc_1,d7_bvfunc_1,t8_bvfunc_4,d7_bvfunc_1,t17_bvfunc_1,d7_bvfunc_1,d6_valuat_1,t39_margrel1,t39_margrel1,t39_margrel1,t39_margrel1,t19_binarith,t7_binarith,t49_margrel1,t43_margrel1,t7_binarith,t7_binarith,t49_margrel1,t43_margrel1,t19_binarith,t45_margrel1]),
    [file(bvfunc_9,t19_bvfunc_9),interesting(0.72)]).

fof(l4_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ( r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),B)
                            & r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),C) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t39_bvfunc_6,t19_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t39_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,l4_bvfunc_9),interesting(0.71)]).

fof(t29_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,k6_valuat_1(A,k6_valuat_1(A,B,C),D),B)
                    & r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l2_bvfunc_9]),
    [file(bvfunc_9,t29_bvfunc_9),interesting(0.71)]).

fof(t20_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,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,D)),k14_bvfunc_1(A,B,k6_valuat_1(A,C,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_bvfunc_9,t6_bvfunc_1]),
    [file(bvfunc_9,t20_bvfunc_9),interesting(0.70)]).

fof(l5_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => ( r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),B)
                                & r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),C) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t39_bvfunc_6,t19_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t39_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,l5_bvfunc_9),interesting(0.67)]).

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))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,t8_bvfunc_4,d7_bvfunc_1,t43_margrel1,t8_bvfunc_4,d7_bvfunc_1,t17_bvfunc_1,d7_bvfunc_1,t20_binarith,d6_valuat_1,t23_binarith,t50_margrel1,t20_binarith,d5_valuat_1,t18_binarith,t19_binarith,t43_margrel1]),
    [file(bvfunc_9,t10_bvfunc_9),interesting(0.66)]).

fof(t12_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,k8_bvfunc_1(A,B,D),k8_bvfunc_1(A,C,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,t8_bvfunc_4,d7_bvfunc_1,t8_bvfunc_4,d7_bvfunc_1,d7_bvfunc_1,t20_binarith,t16_bvfunc_1,d6_valuat_1,t23_binarith,t50_margrel1,t20_binarith,d5_valuat_1,t18_binarith,t19_binarith]),
    [file(bvfunc_9,t12_bvfunc_9),interesting(0.66)]).

fof(t38_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ( ( r1_bvfunc_1(A,B,C)
                          & r1_bvfunc_1(A,D,E) )
                       => r1_bvfunc_1(A,k8_bvfunc_1(A,B,D),k8_bvfunc_1(A,C,E)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_bvfunc_1,t22_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,t38_bvfunc_9),interesting(0.64)]).

fof(l6_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => ! [H] : 
                                  ( m2_fraenkel(H,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                                 => ( r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),B)
                                    & r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),C) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t39_bvfunc_6,t19_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t39_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,l6_bvfunc_9),interesting(0.63)]).

fof(t30_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ( r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),B)
                        & r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),C) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l3_bvfunc_9]),
    [file(bvfunc_9,t30_bvfunc_9),interesting(0.62)]).

fof(t8_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,k8_bvfunc_1(A,B,C),D),k14_bvfunc_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,t8_bvfunc_4,t16_bvfunc_1,d7_bvfunc_1,d6_valuat_1,t43_margrel1,t8_bvfunc_4,d7_bvfunc_1,t23_binarith,t49_margrel1,t43_margrel1]),
    [file(bvfunc_9,t8_bvfunc_9),interesting(0.62)]).

fof(t36_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,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,D,C)),k8_bvfunc_1(A,B,D)),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t21_bvfunc_9,t34_bvfunc_9,t2_bvfunc_9,t18_bvfunc_1]),
    [file(bvfunc_9,t36_bvfunc_9),interesting(0.61)]).

fof(t1_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,k6_valuat_1(A,k8_bvfunc_1(A,B,C),k14_bvfunc_1(A,C,D)),k8_bvfunc_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,t8_bvfunc_4,d7_bvfunc_1,d7_bvfunc_1,t43_margrel1,d7_bvfunc_1,t39_margrel1,t39_margrel1,t19_binarith,t7_binarith,t7_binarith,d5_valuat_1,t46_margrel1,t43_margrel1]),
    [file(bvfunc_9,t1_bvfunc_9),interesting(0.60)]).

fof(t7_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,k6_valuat_1(A,C,D)),k14_bvfunc_1(A,B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,t8_bvfunc_4,d7_bvfunc_1,d6_valuat_1,t43_margrel1,t8_bvfunc_4,d7_bvfunc_1,t23_binarith,t49_margrel1,t43_margrel1]),
    [file(bvfunc_9,t7_bvfunc_9),interesting(0.58)]).

fof(t9_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),C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,t8_bvfunc_4,d7_bvfunc_1,t43_margrel1,t8_bvfunc_4,d7_bvfunc_1,t17_bvfunc_1,d7_bvfunc_1,t20_binarith,t19_binarith,t43_margrel1]),
    [file(bvfunc_9,t9_bvfunc_9),interesting(0.58)]).

fof(t22_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => r1_bvfunc_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,D,E)),k14_bvfunc_1(A,k8_bvfunc_1(A,B,D),k8_bvfunc_1(A,C,E))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,t8_bvfunc_4,t8_bvfunc_4,d6_valuat_1,d7_bvfunc_1,d7_bvfunc_1,t8_bvfunc_4,t16_bvfunc_1,d7_bvfunc_1,d6_valuat_1,d7_bvfunc_1,t39_margrel1,t39_margrel1,t39_margrel1,t39_margrel1,t19_binarith,t7_binarith,t45_margrel1,t43_margrel1,t7_binarith,t49_margrel1,t43_margrel1,t19_binarith,t45_margrel1]),
    [file(bvfunc_9,t22_bvfunc_9),interesting(0.57)]).

fof(t13_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,k8_bvfunc_1(A,k6_valuat_1(A,B,C),D),k8_bvfunc_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d7_bvfunc_1,d6_valuat_1,t43_margrel1,d7_bvfunc_1,t23_binarith,t49_margrel1,t43_margrel1]),
    [file(bvfunc_9,t13_bvfunc_9),interesting(0.56)]).

fof(t31_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ( r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),B)
                            & r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),C) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l4_bvfunc_9]),
    [file(bvfunc_9,t31_bvfunc_9),interesting(0.56)]).

fof(t11_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,B,k8_bvfunc_1(A,C,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,t8_bvfunc_4,d7_bvfunc_1,t8_bvfunc_4,d7_bvfunc_1,d7_bvfunc_1,t20_binarith,t19_binarith]),
    [file(bvfunc_9,t11_bvfunc_9),interesting(0.54)]).

fof(t23_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,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,D)),k14_bvfunc_1(A,B,k8_bvfunc_1(A,C,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t22_bvfunc_9,t10_bvfunc_1]),
    [file(bvfunc_9,t23_bvfunc_9),interesting(0.53)]).

fof(t3_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))
             => r1_bvfunc_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k5_valuat_1(A,C)),k5_valuat_1(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,t8_bvfunc_4,d7_bvfunc_1,t22_binarith,d5_valuat_1,t46_margrel1,t7_binarith,t43_margrel1,t49_margrel1,t43_margrel1]),
    [file(bvfunc_9,t3_bvfunc_9),interesting(0.51)]).

fof(t4_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))
             => r1_bvfunc_1(A,k6_valuat_1(A,k8_bvfunc_1(A,B,C),k5_valuat_1(A,B)),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d7_bvfunc_1,t22_binarith,d5_valuat_1,t46_margrel1,t7_binarith,t43_margrel1,t49_margrel1,t43_margrel1]),
    [file(bvfunc_9,t4_bvfunc_9),interesting(0.51)]).

fof(t32_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => ( r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),B)
                                & r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),C) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l5_bvfunc_9]),
    [file(bvfunc_9,t32_bvfunc_9),interesting(0.50)]).

fof(t21_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,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,D,C)),k14_bvfunc_1(A,k8_bvfunc_1(A,B,D),C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,t21_bvfunc_9),interesting(0.48)]).

fof(t14_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => r1_bvfunc_1(A,k8_bvfunc_1(A,k6_valuat_1(A,B,C),k6_valuat_1(A,D,E)),k8_bvfunc_1(A,B,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d7_bvfunc_1,d6_valuat_1,d6_valuat_1,t43_margrel1,d7_bvfunc_1,t23_binarith,t23_binarith,t49_margrel1,t49_margrel1,t43_margrel1]),
    [file(bvfunc_9,t14_bvfunc_9),interesting(0.47)]).

fof(t35_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,k6_valuat_1(A,B,C),D)
                   => r1_bvfunc_1(A,k6_valuat_1(A,B,k5_valuat_1(A,D)),k5_valuat_1(A,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_bvfunc_1,t8_bvfunc_4,t17_bvfunc_1,t11_bvfunc_1,t4_bvfunc_1,t17_bvfunc_1,t8_bvfunc_4,t19_bvfunc_1]),
    [file(bvfunc_9,t35_bvfunc_9),interesting(0.47)]).

fof(t25_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,E),k14_bvfunc_1(A,C,F)),k14_bvfunc_1(A,D,G)),k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)),k5_valuat_1(A,k6_valuat_1(A,E,F))),k5_valuat_1(A,k6_valuat_1(A,E,G))),k5_valuat_1(A,k6_valuat_1(A,F,G))),k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,E,B),k14_bvfunc_1(A,F,C)),k14_bvfunc_1(A,G,D))) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l32_bvfunc_9,l33_bvfunc_9,l34_bvfunc_9,t18_bvfunc_6,t18_bvfunc_6,l2_bvfunc_9,t19_bvfunc_1,l2_bvfunc_9,t19_bvfunc_1,t10_bvfunc_5,t10_bvfunc_5,t24_bvfunc_9,t11_bvfunc_1,t24_bvfunc_9,t24_bvfunc_9,t19_bvfunc_1,t19_bvfunc_1,t19_bvfunc_1,t10_bvfunc_5,t10_bvfunc_5,t10_bvfunc_5,t18_bvfunc_6,t18_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,t25_bvfunc_9),interesting(0.46)]).

fof(t37_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,k6_valuat_1(A,k8_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,D,C)),k6_valuat_1(A,B,D)),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t6_bvfunc_7,t2_bvfunc_9]),
    [file(bvfunc_9,t37_bvfunc_9),interesting(0.46)]).

fof(t15_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,k6_valuat_1(A,k8_bvfunc_1(A,B,C),k14_bvfunc_1(A,C,D)),k8_bvfunc_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,t8_bvfunc_4,d6_valuat_1,d7_bvfunc_1,d7_bvfunc_1,t43_margrel1,d7_bvfunc_1,t39_margrel1,t39_margrel1,t19_binarith,t22_binarith,t22_binarith,t22_binarith,d5_valuat_1,t46_margrel1,t7_binarith,t49_margrel1,t7_binarith,t49_margrel1,t7_binarith,t49_margrel1,t43_margrel1]),
    [file(bvfunc_9,t15_bvfunc_9),interesting(0.45)]).

fof(t33_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => ! [H] : 
                                  ( m2_fraenkel(H,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                                 => ( r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),B)
                                    & r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),C) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l6_bvfunc_9]),
    [file(bvfunc_9,t33_bvfunc_9),interesting(0.45)]).

fof(t6_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))
             => r1_bvfunc_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,k5_valuat_1(A,C))),k5_valuat_1(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,t8_bvfunc_4,t8_bvfunc_4,d7_bvfunc_1,d7_bvfunc_1,t43_margrel1,t7_binarith,t7_binarith,d5_valuat_1,t46_margrel1,t43_margrel1]),
    [file(bvfunc_9,t6_bvfunc_9),interesting(0.43)]).

fof(t5_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))
             => r1_bvfunc_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k5_valuat_1(A,B),C)),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,t8_bvfunc_4,t8_bvfunc_4,t4_bvfunc_1,d7_bvfunc_1,d7_bvfunc_1,t43_margrel1,t7_binarith,t7_binarith,d5_valuat_1,t46_margrel1,t43_margrel1]),
    [file(bvfunc_9,t5_bvfunc_9),interesting(0.41)]).

fof(t24_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,C,F),k14_bvfunc_1(A,D,G)),k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)),k5_valuat_1(A,k6_valuat_1(A,E,F))),k5_valuat_1(A,k6_valuat_1(A,E,G))),k14_bvfunc_1(A,E,B)) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l4_bvfunc_9,t19_bvfunc_1,l4_bvfunc_9,t19_bvfunc_1,t18_bvfunc_6,t22_bvfunc_9,t19_bvfunc_1,t10_bvfunc_5,l2_bvfunc_9,t19_bvfunc_1,l1_bvfunc_9,t19_bvfunc_1,t18_bvfunc_6,t18_bvfunc_6,t17_bvfunc_1,t17_bvfunc_1,t8_bvfunc_4,t8_bvfunc_4,t5_bvfunc_7,t12_bvfunc_7,t39_bvfunc_6,t10_bvfunc_5,l3_bvfunc_9,t19_bvfunc_1,t18_bvfunc_6,t11_bvfunc_1,t1_bvfunc_9,t19_bvfunc_1,t10_bvfunc_5,t8_bvfunc_4,t19_bvfunc_1]),
    [file(bvfunc_9,t24_bvfunc_9),interesting(0.39)]).

fof(t26_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))
                 => ! [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)),k5_valuat_1(A,k6_valuat_1(A,D,E))),k5_valuat_1(A,k6_valuat_1(A,B,C))) = k19_bvfunc_1(A) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_valuat_1,d6_valuat_1,t8_bvfunc_4,t8_bvfunc_4,d7_bvfunc_1,d7_bvfunc_1,t17_bvfunc_1,d7_bvfunc_1,t17_bvfunc_1,d7_bvfunc_1,t39_margrel1,t39_margrel1,t7_binarith,t19_binarith,t7_binarith,t22_binarith,t52_margrel1,t52_margrel1,d5_valuat_1,d5_valuat_1,t46_margrel1,t46_margrel1,t49_margrel1,t49_margrel1,t7_binarith,t43_margrel1,d15_bvfunc_1,t19_bvfunc_1]),
    [file(bvfunc_9,t26_bvfunc_9),interesting(0.36)]).

fof(t18_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,k6_valuat_1(A,k8_bvfunc_1(A,B,C),k8_bvfunc_1(A,k5_valuat_1(A,B),D)),k8_bvfunc_1(A,C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d7_bvfunc_1,d7_bvfunc_1,t43_margrel1,d7_bvfunc_1,t39_margrel1,t39_margrel1,t19_binarith,t7_binarith,t7_binarith,d5_valuat_1,t46_margrel1,t43_margrel1]),
    [file(bvfunc_9,t18_bvfunc_9),interesting(0.32)]).

fof(t27_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,E),k14_bvfunc_1(A,C,F)),k14_bvfunc_1(A,D,G)),k5_valuat_1(A,k6_valuat_1(A,E,F))),k5_valuat_1(A,k6_valuat_1(A,E,G))),k5_valuat_1(A,k6_valuat_1(A,F,G))),k6_valuat_1(A,k6_valuat_1(A,k5_valuat_1(A,k6_valuat_1(A,B,C)),k5_valuat_1(A,k6_valuat_1(A,B,D))),k5_valuat_1(A,k6_valuat_1(A,C,D)))) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t6_bvfunc_1,t6_bvfunc_1,t6_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t7_bvfunc_1,t39_bvfunc_6,t39_bvfunc_6,t39_bvfunc_6,t10_bvfunc_5,t10_bvfunc_5,t39_bvfunc_6,t26_bvfunc_9,t26_bvfunc_9,t26_bvfunc_9,t10_bvfunc_5,t10_bvfunc_5,t10_bvfunc_5,t18_bvfunc_6,t18_bvfunc_6,t19_bvfunc_1]),
    [file(bvfunc_9,t27_bvfunc_9),interesting(0.14)]).

fof(t16_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,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k5_valuat_1(A,B),D)),k8_bvfunc_1(A,C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,t8_bvfunc_4,t8_bvfunc_4,t4_bvfunc_1,d6_valuat_1,d7_bvfunc_1,d7_bvfunc_1,t43_margrel1,d7_bvfunc_1,t39_margrel1,t39_margrel1,t19_binarith,t7_binarith,t7_binarith,d5_valuat_1,t46_margrel1,t43_margrel1]),
    [file(bvfunc_9,t16_bvfunc_9),interesting(0.11)]).

fof(l7_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => ! [H] : 
                                  ( m2_fraenkel(H,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                                 => ( k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),B) = k19_bvfunc_1(A)
                                    & k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),C) = k19_bvfunc_1(A)
                                    & k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),D) = k19_bvfunc_1(A)
                                    & k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),E) = k19_bvfunc_1(A)
                                    & k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),F) = k19_bvfunc_1(A)
                                    & k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),G) = k19_bvfunc_1(A)
                                    & k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D),E),F),G),H),H) = k19_bvfunc_1(A) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l6_bvfunc_9,l6_bvfunc_9,l5_bvfunc_9,l4_bvfunc_9,l3_bvfunc_9,l2_bvfunc_9,l1_bvfunc_9,t19_bvfunc_1]),
    [file(bvfunc_9,l7_bvfunc_9),interesting(0.11)]).

fof(t17_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,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,D,k5_valuat_1(A,C))),k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,D))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,t8_bvfunc_4,t8_bvfunc_4,d7_bvfunc_1,d7_bvfunc_1,t43_margrel1,d7_bvfunc_1,t39_margrel1,t39_margrel1,t19_binarith,t7_binarith,t7_binarith,d5_valuat_1,t46_margrel1,t43_margrel1]),
    [file(bvfunc_9,t17_bvfunc_9),interesting(0.10)]).

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(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(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(t43_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ( A != k8_margrel1
      <=> A = k7_margrel1 ) ) ),
    file(margrel1,t43_margrel1),
    [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(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(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(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(t50_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k10_margrel1(k8_margrel1,A) = A ) ),
    file(margrel1,t50_margrel1),
    [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(t18_binarith,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k1_binarith(A,k9_margrel1(A)) = k8_margrel1 ) ),
    file(binarith,t18_binarith),
    [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(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(t49_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => k10_margrel1(k7_margrel1,A) = k7_margrel1 ) ),
    file(margrel1,t49_margrel1),
    [interesting(0.00)]).

fof(t39_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ( A = k7_margrel1
        | A = k8_margrel1 ) ) ),
    file(margrel1,t39_margrel1),
    [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(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(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(t45_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ! [B] : 
          ( v2_margrel1(B)
         => ( ( k10_margrel1(A,B) = k8_margrel1
             => ( A = k8_margrel1
                & B = k8_margrel1 ) )
            & ( ( A = k8_margrel1
                & B = k8_margrel1 )
             => k10_margrel1(A,B) = k8_margrel1 )
            & ~ ( k10_margrel1(A,B) = k7_margrel1
                & A != k7_margrel1
                & B != k7_margrel1 )
            & ( ( A = k7_margrel1
                | B = k7_margrel1 )
             => k10_margrel1(A,B) = k7_margrel1 ) ) ) ) ),
    file(margrel1,t45_margrel1),
    [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(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(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(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_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))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => ( ( k14_bvfunc_1(A,D,B) = k19_bvfunc_1(A)
                      & k14_bvfunc_1(A,D,C) = k19_bvfunc_1(A) )
                   => k14_bvfunc_1(A,D,k6_valuat_1(A,B,C)) = k19_bvfunc_1(A) ) ) ) ) ) ),
    file(bvfunc_6,t18_bvfunc_6),
    [interesting(0.00)]).

fof(l32_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,E),k14_bvfunc_1(A,C,F)),k14_bvfunc_1(A,D,G)),k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)),k5_valuat_1(A,k6_valuat_1(A,E,F))),k5_valuat_1(A,k6_valuat_1(A,E,G))),k5_valuat_1(A,k6_valuat_1(A,F,G))),k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,E),k14_bvfunc_1(A,C,F)),k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)),k5_valuat_1(A,k6_valuat_1(A,G,E))),k5_valuat_1(A,k6_valuat_1(A,G,F)))) = k19_bvfunc_1(A) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l7_bvfunc_9,l7_bvfunc_9,l7_bvfunc_9,l7_bvfunc_9,l7_bvfunc_9,t18_bvfunc_6,t18_bvfunc_6,t18_bvfunc_6,t18_bvfunc_6]),
    [file(bvfunc_9,l32_bvfunc_9),interesting(0.00)]).

fof(l33_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,E),k14_bvfunc_1(A,C,F)),k14_bvfunc_1(A,D,G)),k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)),k5_valuat_1(A,k6_valuat_1(A,E,F))),k5_valuat_1(A,k6_valuat_1(A,E,G))),k5_valuat_1(A,k6_valuat_1(A,F,G))),k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,E),k14_bvfunc_1(A,D,G)),k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)),k5_valuat_1(A,k6_valuat_1(A,F,E))),k5_valuat_1(A,k6_valuat_1(A,F,G)))) = k19_bvfunc_1(A) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l7_bvfunc_9,l7_bvfunc_9,l7_bvfunc_9,l7_bvfunc_9,l7_bvfunc_9,t18_bvfunc_6,t18_bvfunc_6,t18_bvfunc_6,t18_bvfunc_6]),
    [file(bvfunc_9,l33_bvfunc_9),interesting(0.00)]).

fof(l34_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))
                 => ! [E] : 
                      ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                     => ! [F] : 
                          ( m2_fraenkel(F,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                         => ! [G] : 
                              ( m2_fraenkel(G,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                             => k14_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,E),k14_bvfunc_1(A,C,F)),k14_bvfunc_1(A,D,G)),k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)),k5_valuat_1(A,k6_valuat_1(A,E,F))),k5_valuat_1(A,k6_valuat_1(A,E,G))),k5_valuat_1(A,k6_valuat_1(A,F,G))),k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,C,F),k14_bvfunc_1(A,D,G)),k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)),k5_valuat_1(A,k6_valuat_1(A,E,F))),k5_valuat_1(A,k6_valuat_1(A,E,G)))) = k19_bvfunc_1(A) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l7_bvfunc_9,l7_bvfunc_9,l7_bvfunc_9,l7_bvfunc_9,l7_bvfunc_9,t18_bvfunc_6,t18_bvfunc_6,t18_bvfunc_6,t18_bvfunc_6]),
    [file(bvfunc_9,l34_bvfunc_9),interesting(0.00)]).

fof(t10_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))
             => ! [D] : 
                  ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1))
                 => ( ( k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A)
                      & k14_bvfunc_1(A,C,D) = k19_bvfunc_1(A) )
                   => k14_bvfunc_1(A,B,D) = k19_bvfunc_1(A) ) ) ) ) ) ),
    file(bvfunc_5,t10_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(t12_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))
                 => k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,C,D)) = k6_valuat_1(A,k6_valuat_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,C,D)),k14_bvfunc_1(A,B,D)) ) ) ) ) ),
    file(bvfunc_7,t12_bvfunc_7),
    [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(t52_margrel1,theorem,(
    ! [A] : 
      ( v2_margrel1(A)
     => ! [B] : 
          ( v2_margrel1(B)
         => ! [C] : 
              ( v2_margrel1(C)
             => k10_margrel1(A,k10_margrel1(B,C)) = k10_margrel1(k10_margrel1(A,B),C) ) ) ) ),
    file(margrel1,t52_margrel1),
    [interesting(0.00)]).

fof(t9_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))
             => ! [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,D),k14_bvfunc_1(A,C,D)),k14_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)) = k19_bvfunc_1(A) ) ) ) ) ),
    file(bvfunc_6,t9_bvfunc_6),
    [interesting(0.00)]).

fof(t21_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))
             => ! [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,C) = k19_bvfunc_1(A)
                          & k14_bvfunc_1(A,D,E) = k19_bvfunc_1(A) )
                       => k14_bvfunc_1(A,k6_valuat_1(A,B,D),k6_valuat_1(A,C,E)) = k19_bvfunc_1(A) ) ) ) ) ) ) ),
    file(bvfunc_6,t21_bvfunc_6),
    [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(t6_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,k6_valuat_1(A,B,C),D) = k8_bvfunc_1(A,k14_bvfunc_1(A,B,D),k14_bvfunc_1(A,C,D)) ) ) ) ) ),
    file(bvfunc_7,t6_bvfunc_7),
    [interesting(0.00)]).

fof(t22_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))
             => ! [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,C) = k19_bvfunc_1(A)
                          & k14_bvfunc_1(A,D,E) = k19_bvfunc_1(A) )
                       => k14_bvfunc_1(A,k8_bvfunc_1(A,B,D),k8_bvfunc_1(A,C,E)) = k19_bvfunc_1(A) ) ) ) ) ) ) ),
    file(bvfunc_6,t22_bvfunc_6),
    [interesting(0.00)]).

fof(t27_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,B,k8_bvfunc_1(A,B,C)) = k19_bvfunc_1(A) ) ) ) ),
    file(bvfunc_6,t27_bvfunc_6),
    [interesting(0.00)]).