fof(l13_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => k1_arytm_1(A,A) = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[d1_arytm_1,t1_arytm_1]),
    [file(arytm_1,l13_arytm_1),interesting(1.00)]).

fof(t4_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( ( r1_arytm_2(A,B)
              & r1_arytm_2(B,A) )
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_arytm_2,t10_arytm_2,t7_arytm_2,t1_arytm_1,t6_arytm_2,d8_arytm_2]),
    [file(arytm_1,t4_arytm_1),interesting(0.99)]).

fof(t18_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => k2_arytm_1(A,A) = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[d2_arytm_1,l13_arytm_1]),
    [file(arytm_1,t18_arytm_1),interesting(0.92)]).

fof(t11_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => r1_arytm_2(k1_arytm_1(A,B),A) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_arytm_1,t20_arytm_2,d1_arytm_1,t6_arytm_1]),
    [file(arytm_1,t11_arytm_1),interesting(0.92)]).

fof(l23_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => k1_arytm_1(k1_arytm_1(A,B),C) = k1_arytm_1(k1_arytm_1(A,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l22_arytm_1,l22_arytm_1]),
    [file(arytm_1,l23_arytm_1),interesting(0.92)]).

fof(t7_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
              <=> r1_arytm_2(k7_arytm_2(A,C),k7_arytm_2(B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_arytm_2,t7_arytm_2,t20_arytm_2,t10_arytm_2,t7_arytm_2,t12_arytm_2,t20_arytm_2]),
    [file(arytm_1,t7_arytm_1),interesting(0.87)]).

fof(l22_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => k1_arytm_1(k1_arytm_1(A,B),C) = k1_arytm_1(A,k7_arytm_2(C,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t20_arytm_2,t3_arytm_1,l21_arytm_1,t7_arytm_2,d1_arytm_1,d1_arytm_1,d1_arytm_1,l17_arytm_1,d8_arytm_2,d1_arytm_1,t5_arytm_1,t20_arytm_2,t3_arytm_1,d1_arytm_1,d1_arytm_1,l21_arytm_1,d1_arytm_1,d1_arytm_1]),
    [file(arytm_1,l22_arytm_1),interesting(0.86)]).

fof(t3_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( ( r1_arytm_2(A,B)
                  & r1_arytm_2(B,C) )
               => r1_arytm_2(A,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_arytm_2,t10_arytm_2,t7_arytm_2,t20_arytm_2]),
    [file(arytm_1,t3_arytm_1),interesting(0.84)]).

fof(l19_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( r1_arytm_2(A,B)
           => k1_arytm_1(B,k1_arytm_1(B,A)) = A ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_arytm_1,d1_arytm_1,d1_arytm_1,t12_arytm_2]),
    [file(arytm_1,l19_arytm_1),interesting(0.84)]).

fof(l20_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(k1_arytm_1(A,B),C)
              <=> r1_arytm_2(A,k7_arytm_2(C,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_arytm_1,t7_arytm_1,d1_arytm_1,t20_arytm_2,t3_arytm_1,t6_arytm_1]),
    [file(arytm_1,l20_arytm_1),interesting(0.83)]).

fof(t25_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( ( r1_arytm_2(A,B)
                  & r1_arytm_2(C,B) )
               => k2_arytm_1(k1_arytm_1(B,C),A) = k2_arytm_1(k1_arytm_1(B,A),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l21_arytm_1,d2_arytm_1,l23_arytm_1,l21_arytm_1,l13_arytm_1,t4_arytm_1,l19_arytm_1,l17_arytm_1,d2_arytm_1,d2_arytm_1,l21_arytm_1,l13_arytm_1,t4_arytm_1,l17_arytm_1,l19_arytm_1,d2_arytm_1,d2_arytm_1,l21_arytm_1,l28_arytm_1,d2_arytm_1,d2_arytm_1]),
    [file(arytm_1,t25_arytm_1),interesting(0.83)]).

fof(l33_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => k8_arytm_2(A,k1_arytm_1(B,C)) = k1_arytm_1(k8_arytm_2(A,B),k8_arytm_2(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_arytm_1,t14_arytm_2,d1_arytm_1,d1_arytm_1,t12_arytm_2,t4_arytm_2,t4_arytm_2,l17_arytm_1,l11_arytm_1,d1_arytm_1,t4_arytm_2,d1_arytm_1]),
    [file(arytm_1,l33_arytm_1),interesting(0.82)]).

fof(l21_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
               => ( r1_arytm_2(k7_arytm_2(C,A),B)
                <=> r1_arytm_2(C,k1_arytm_1(B,A)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_arytm_1,t7_arytm_1]),
    [file(arytm_1,l21_arytm_1),interesting(0.80)]).

fof(l18_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => k1_arytm_1(k7_arytm_2(A,B),B) = A ) ) ),
    inference(mizar_proof,[status(thm)],[t20_arytm_2,d1_arytm_1]),
    [file(arytm_1,l18_arytm_1),interesting(0.79)]).

fof(l28_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( ( r1_arytm_2(A,B)
                  & r1_arytm_2(C,B) )
               => k1_arytm_1(A,k1_arytm_1(B,C)) = k1_arytm_1(C,k1_arytm_1(B,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_arytm_1,l26_arytm_1]),
    [file(arytm_1,l28_arytm_1),interesting(0.79)]).

fof(l17_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( A = k1_xboole_0
           => k1_arytm_1(B,A) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t6_arytm_1,d8_arytm_2,d1_arytm_1]),
    [file(arytm_1,l17_arytm_1),interesting(0.78)]).

fof(l2_arytm_1,theorem,(
    m1_subset_1(k4_ordinal2,k2_arytm_2) ),
    inference(mizar_proof,[status(thm)],[t21_arytm_2]),
    [file(arytm_1,l2_arytm_1),interesting(0.77)]).

fof(t6_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( A = k1_xboole_0
           => r1_arytm_2(A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_arytm_2,t20_arytm_2]),
    [file(arytm_1,t6_arytm_1),interesting(0.77)]).

fof(t23_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ~ ( ~ r1_arytm_2(A,B)
                  & ~ r1_arytm_2(A,C)
                  & k2_arytm_1(B,k1_arytm_1(A,C)) != k2_arytm_1(C,k1_arytm_1(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l20_arytm_1,d2_arytm_1,l28_arytm_1,l20_arytm_1,l23_arytm_1,d2_arytm_1,d2_arytm_1]),
    [file(arytm_1,t23_arytm_1),interesting(0.77)]).

fof(t1_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( k7_arytm_2(A,B) = B
           => A = k1_xboole_0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[t21_arytm_2,d8_arytm_2,t12_arytm_2]),
    [file(arytm_1,t1_arytm_1),interesting(0.75)]).

fof(t13_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
               => k7_arytm_2(C,k1_arytm_1(B,A)) = k1_arytm_1(k7_arytm_2(C,B),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t20_arytm_2,t3_arytm_1,t7_arytm_2,d1_arytm_1,d1_arytm_1,t12_arytm_2]),
    [file(arytm_1,t13_arytm_1),interesting(0.74)]).

fof(l26_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
               => k1_arytm_1(C,k1_arytm_1(B,A)) = k1_arytm_1(k7_arytm_2(C,A),B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l20_arytm_1,d1_arytm_1,l18_arytm_1,d1_arytm_1,t7_arytm_2,t13_arytm_1,t12_arytm_2,l20_arytm_1,d1_arytm_1,d1_arytm_1]),
    [file(arytm_1,l26_arytm_1),interesting(0.74)]).

fof(t8_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
               => r1_arytm_2(k8_arytm_2(A,C),k8_arytm_2(B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_arytm_2,t14_arytm_2,t20_arytm_2]),
    [file(arytm_1,t8_arytm_1),interesting(0.74)]).

fof(t16_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
               => r1_arytm_2(k1_arytm_1(C,B),k1_arytm_1(C,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t3_arytm_1,t7_arytm_1,d1_arytm_1,d1_arytm_1,t7_arytm_1,d1_arytm_1,t6_arytm_1]),
    [file(arytm_1,t16_arytm_1),interesting(0.70)]).

fof(l27_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( ( r1_arytm_2(A,B)
                  & r1_arytm_2(C,A) )
               => k1_arytm_1(B,k1_arytm_1(A,C)) = k7_arytm_2(k1_arytm_1(B,A),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_arytm_1,t13_arytm_1]),
    [file(arytm_1,l27_arytm_1),interesting(0.70)]).

fof(t10_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( ( r1_arytm_2(A,B)
              & k1_arytm_1(B,A) = k1_xboole_0 )
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_arytm_1,t4_arytm_1]),
    [file(arytm_1,t10_arytm_1),interesting(0.69)]).

fof(t17_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
               => r1_arytm_2(k1_arytm_1(A,C),k1_arytm_1(B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t3_arytm_1,d1_arytm_1,t7_arytm_1,d1_arytm_1,t6_arytm_1]),
    [file(arytm_1,t17_arytm_1),interesting(0.69)]).

fof(l11_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(k8_arytm_2(A,B),k8_arytm_2(A,C))
               => ( A = k1_xboole_0
                  | r1_arytm_2(B,C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_arytm_2,t15_arytm_2,t16_arytm_2,t13_arytm_2,t14_arytm_2,l3_arytm_1,t20_arytm_2]),
    [file(arytm_1,l11_arytm_1),interesting(0.69)]).

fof(t9_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ~ ( ~ r1_arytm_2(A,B)
              & k1_arytm_1(A,B) = k1_xboole_0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_arytm_1,d8_arytm_2]),
    [file(arytm_1,t9_arytm_1),interesting(0.66)]).

fof(t5_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( ( r1_arytm_2(A,B)
              & B = k1_xboole_0 )
           => A = k1_xboole_0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_arytm_2,t6_arytm_2]),
    [file(arytm_1,t5_arytm_1),interesting(0.64)]).

fof(t21_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( ~ r1_arytm_2(A,B)
               => k2_arytm_1(C,k1_arytm_1(A,B)) = k2_arytm_1(k7_arytm_2(C,B),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l20_arytm_1,d2_arytm_1,l26_arytm_1,l20_arytm_1,l22_arytm_1,d2_arytm_1,d2_arytm_1]),
    [file(arytm_1,t21_arytm_1),interesting(0.64)]).

fof(t24_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
               => k2_arytm_1(B,k7_arytm_2(A,C)) = k2_arytm_1(k1_arytm_1(B,A),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l21_arytm_1,d2_arytm_1,l22_arytm_1,l21_arytm_1,t4_arytm_1,l13_arytm_1,l18_arytm_1,l17_arytm_1,d2_arytm_1,d2_arytm_1,l21_arytm_1,l26_arytm_1,d2_arytm_1,d2_arytm_1]),
    [file(arytm_1,t24_arytm_1),interesting(0.62)]).

fof(l3_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( k8_arytm_2(A,B) = k8_arytm_2(A,C)
               => ( A = k1_xboole_0
                  | B = C ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_arytm_2,t16_arytm_2,t13_arytm_2,t13_arytm_2,t16_arytm_2]),
    [file(arytm_1,l3_arytm_1),interesting(0.61)]).

fof(t2_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ~ ( k8_arytm_2(A,B) = k1_xboole_0
              & A != k1_xboole_0
              & B != k1_xboole_0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_arytm_2,t16_arytm_2,t13_arytm_2,t4_arytm_2]),
    [file(arytm_1,t2_arytm_1),interesting(0.55)]).

fof(t14_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( ( r1_arytm_2(A,B)
                  & r1_arytm_2(C,A) )
               => k7_arytm_2(k1_arytm_1(B,A),C) = k1_arytm_1(B,k1_arytm_1(A,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_arytm_1,t13_arytm_1]),
    [file(arytm_1,t14_arytm_1),interesting(0.52)]).

fof(t19_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( A = k1_xboole_0
           => ( B = k1_xboole_0
              | k2_arytm_1(A,B) = k4_tarski(k1_xboole_0,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t6_arytm_1,t4_arytm_1,d2_arytm_1,l17_arytm_1]),
    [file(arytm_1,t19_arytm_1),interesting(0.51)]).

fof(t20_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
               => k7_arytm_2(C,k1_arytm_1(B,A)) = k2_arytm_1(k7_arytm_2(C,B),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t20_arytm_2,t3_arytm_1,d2_arytm_1,t13_arytm_1]),
    [file(arytm_1,t20_arytm_1),interesting(0.49)]).

fof(t26_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
               => k8_arytm_2(C,k1_arytm_1(B,A)) = k2_arytm_1(k8_arytm_2(C,B),k8_arytm_2(C,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_arytm_1,d2_arytm_1,l33_arytm_1]),
    [file(arytm_1,t26_arytm_1),interesting(0.49)]).

fof(t22_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(A,B)
               => ( r1_arytm_2(A,C)
                  | k2_arytm_1(B,k1_arytm_1(A,C)) = k7_arytm_2(k1_arytm_1(B,A),C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_arytm_1,t3_arytm_1,d2_arytm_1,l27_arytm_1]),
    [file(arytm_1,t22_arytm_1),interesting(0.46)]).

fof(t12_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( ( r1_arytm_2(A,B)
                  & r1_arytm_2(A,C) )
               => k7_arytm_2(B,k1_arytm_1(C,A)) = k7_arytm_2(k1_arytm_1(B,A),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_arytm_2,d1_arytm_1,d1_arytm_1,t7_arytm_2,t12_arytm_2]),
    [file(arytm_1,t12_arytm_1),interesting(0.34)]).

fof(t15_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( ( r1_arytm_2(A,B)
                  & r1_arytm_2(A,C) )
               => k7_arytm_2(k1_arytm_1(C,A),B) = k7_arytm_2(k1_arytm_1(B,A),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_arytm_2,d1_arytm_1,d1_arytm_1,t7_arytm_2,t12_arytm_2]),
    [file(arytm_1,t15_arytm_1),interesting(0.34)]).

fof(t27_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ~ ( ~ r1_arytm_2(A,B)
                  & C != k1_xboole_0
                  & k4_tarski(k1_xboole_0,k8_arytm_2(C,k1_arytm_1(A,B))) != k2_arytm_1(k8_arytm_2(C,B),k8_arytm_2(C,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l11_arytm_1,l33_arytm_1,d2_arytm_1]),
    [file(arytm_1,t27_arytm_1),interesting(0.32)]).

fof(t21_arytm_2,theorem,
    ( r2_hidden(k12_arytm_3,k2_arytm_2)
    & r2_hidden(k13_arytm_3,k2_arytm_2) ),
    file(arytm_2,t21_arytm_2),
    [interesting(0.00)]).

fof(d1_arytm_1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( ( r1_arytm_2(B,A)
                 => ( C = k1_arytm_1(A,B)
                  <=> k7_arytm_2(C,B) = A ) )
                & ( ~ r1_arytm_2(B,A)
                 => ( C = k1_arytm_1(A,B)
                  <=> C = k1_xboole_0 ) ) ) ) ) ) ),
    file(arytm_1,d1_arytm_1),
    [interesting(0.00)]).

fof(d8_arytm_2,definition,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( ( B = k12_arytm_3
             => k7_arytm_2(A,B) = A )
            & ( A = k12_arytm_3
             => k7_arytm_2(A,B) = B )
            & ~ ( B != k12_arytm_3
                & A != k12_arytm_3
                & k7_arytm_2(A,B) != k4_arytm_2(k5_arytm_2(k3_arytm_2(A),k3_arytm_2(B))) ) ) ) ) ),
    file(arytm_2,d8_arytm_2),
    [interesting(0.00)]).

fof(t10_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ~ ( r1_arytm_2(A,B)
              & ! [C] : 
                  ( m1_subset_1(C,k2_arytm_2)
                 => k7_arytm_2(A,C) != B ) ) ) ) ),
    file(arytm_2,t10_arytm_2),
    [interesting(0.00)]).

fof(t7_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => k7_arytm_2(A,k7_arytm_2(B,C)) = k7_arytm_2(k7_arytm_2(A,B),C) ) ) ) ),
    file(arytm_2,t7_arytm_2),
    [interesting(0.00)]).

fof(t12_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( k7_arytm_2(A,B) = k7_arytm_2(A,C)
               => B = C ) ) ) ) ),
    file(arytm_2,t12_arytm_2),
    [interesting(0.00)]).

fof(t6_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( k7_arytm_2(A,B) = k12_arytm_3
           => A = k12_arytm_3 ) ) ) ),
    file(arytm_2,t6_arytm_2),
    [interesting(0.00)]).

fof(t20_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( A = k7_arytm_2(B,C)
               => r1_arytm_2(C,A) ) ) ) ) ),
    file(arytm_2,t20_arytm_2),
    [interesting(0.00)]).

fof(d2_arytm_1,definition,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( ( r1_arytm_2(B,A)
             => k2_arytm_1(A,B) = k1_arytm_1(A,B) )
            & ( ~ r1_arytm_2(B,A)
             => k2_arytm_1(A,B) = k4_tarski(k1_xboole_0,k1_arytm_1(B,A)) ) ) ) ) ),
    file(arytm_1,d2_arytm_1),
    [interesting(0.00)]).

fof(t14_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => k8_arytm_2(A,k7_arytm_2(B,C)) = k7_arytm_2(k8_arytm_2(A,B),k8_arytm_2(A,C)) ) ) ) ),
    file(arytm_2,t14_arytm_2),
    [interesting(0.00)]).

fof(t4_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( A = k12_arytm_3
           => k8_arytm_2(A,B) = k12_arytm_3 ) ) ) ),
    file(arytm_2,t4_arytm_2),
    [interesting(0.00)]).

fof(t15_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ~ ( A != k12_arytm_3
          & ! [B] : 
              ( m1_subset_1(B,k2_arytm_2)
             => k8_arytm_2(A,B) != k13_arytm_3 ) ) ) ),
    file(arytm_2,t15_arytm_2),
    [interesting(0.00)]).

fof(t16_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( A = k13_arytm_3
           => k8_arytm_2(A,B) = B ) ) ) ),
    file(arytm_2,t16_arytm_2),
    [interesting(0.00)]).

fof(t13_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => k8_arytm_2(A,k8_arytm_2(B,C)) = k8_arytm_2(k8_arytm_2(A,B),C) ) ) ) ),
    file(arytm_2,t13_arytm_2),
    [interesting(0.00)]).

fof(t28_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ! [C] : 
              ( m1_subset_1(C,k2_arytm_2)
             => ( r1_arytm_2(B,A)
               => ( k1_arytm_1(A,B) = k1_xboole_0
                  | C = k1_xboole_0
                  | k2_arytm_1(k8_arytm_2(C,B),k8_arytm_2(C,A)) = k4_tarski(k1_xboole_0,k8_arytm_2(C,k1_arytm_1(A,B))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l13_arytm_1,t4_arytm_1,t27_arytm_1]),
    [file(arytm_1,t28_arytm_1),interesting(0.00)]).