fof(l59_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k5_xcmplx_0(k7_xcmplx_0(A,B)) = k7_xcmplx_0(B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d9_xcmplx_0,l58_xcmplx_1,t6_xcmplx_1,l29_xcmplx_1,d9_xcmplx_0,l55_xcmplx_1,t6_xcmplx_1,d7_xcmplx_0]),
    [file(xcmplx_1,l59_xcmplx_1),interesting(1.00)]).

fof(t52_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => k7_xcmplx_0(A,k7_xcmplx_0(A,B)) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l59_xcmplx_1,l60_xcmplx_1,l60_xcmplx_1,l29_xcmplx_1]),
    [file(xcmplx_1,t52_xcmplx_1),interesting(1.00)]).

fof(l233_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k5_xcmplx_0(k4_xcmplx_0(A)) = k4_xcmplx_0(k5_xcmplx_0(A)) ) ),
    inference(mizar_proof,[status(thm)],[l28_xcmplx_1,t189_xcmplx_1,l28_xcmplx_1]),
    [file(xcmplx_1,l233_xcmplx_1),interesting(0.99)]).

fof(t79_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(A,k3_xcmplx_0(B,C)) = k7_xcmplx_0(k7_xcmplx_0(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l92_xcmplx_1]),
    [file(xcmplx_1,t79_xcmplx_1),interesting(0.94)]).

fof(t215_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k5_xcmplx_0(k7_xcmplx_0(A,B)) = k7_xcmplx_0(B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[l59_xcmplx_1]),
    [file(xcmplx_1,t215_xcmplx_1),interesting(0.93)]).

fof(t224_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k5_xcmplx_0(k4_xcmplx_0(A)) = k4_xcmplx_0(k5_xcmplx_0(A)) ) ),
    inference(mizar_proof,[status(thm)],[l233_xcmplx_1]),
    [file(xcmplx_1,t224_xcmplx_1),interesting(0.91)]).

fof(t189_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(A,k4_xcmplx_0(B)) = k4_xcmplx_0(k7_xcmplx_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[l65_xcmplx_1,l138_xcmplx_1]),
    [file(xcmplx_1,t189_xcmplx_1),interesting(0.88)]).

fof(t192_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(k4_xcmplx_0(A),k4_xcmplx_0(B)) = k7_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t191_xcmplx_1,t189_xcmplx_1]),
    [file(xcmplx_1,t192_xcmplx_1),interesting(0.82)]).

fof(t58_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k7_xcmplx_0(A,B) = 1
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t49_xcmplx_1,l27_xcmplx_1]),
    [file(xcmplx_1,t58_xcmplx_1),interesting(0.82)]).

fof(t84_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k7_xcmplx_0(k3_xcmplx_0(A,B),k3_xcmplx_0(C,D)) = k7_xcmplx_0(k3_xcmplx_0(k7_xcmplx_0(A,C),B),D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l99_xcmplx_1,l60_xcmplx_1,l98_xcmplx_1]),
    [file(xcmplx_1,t84_xcmplx_1),interesting(0.82)]).

fof(t56_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(1,k7_xcmplx_0(1,A)) = A ) ),
    inference(mizar_proof,[status(thm)],[l26_xcmplx_1]),
    [file(xcmplx_1,t56_xcmplx_1),interesting(0.81)]).

fof(l60_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(A,k7_xcmplx_0(B,C)) = k7_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l58_xcmplx_1]),
    [file(xcmplx_1,l60_xcmplx_1),interesting(0.80)]).

fof(t193_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(k4_xcmplx_0(A),B) = k7_xcmplx_0(A,k4_xcmplx_0(B)) ) ) ),
    inference(mizar_proof,[status(thm)],[l138_xcmplx_1,t189_xcmplx_1]),
    [file(xcmplx_1,t193_xcmplx_1),interesting(0.80)]).

fof(t82_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(A,k7_xcmplx_0(B,C)) = k3_xcmplx_0(C,k7_xcmplx_0(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_xcmplx_1,d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t82_xcmplx_1),interesting(0.80)]).

fof(l92_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k7_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,D)) = k7_xcmplx_0(k3_xcmplx_0(A,D),k3_xcmplx_0(B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l59_xcmplx_1,l58_xcmplx_1]),
    [file(xcmplx_1,l92_xcmplx_1),interesting(0.78)]).

fof(t190_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k7_xcmplx_0(A,k4_xcmplx_0(B))) = k7_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t189_xcmplx_1]),
    [file(xcmplx_1,t190_xcmplx_1),interesting(0.78)]).

fof(l26_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(A,k7_xcmplx_0(B,C)) = k7_xcmplx_0(k3_xcmplx_0(A,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d9_xcmplx_0,l25_xcmplx_1,t4_xcmplx_1,d9_xcmplx_0]),
    [file(xcmplx_1,l26_xcmplx_1),interesting(0.78)]).

fof(l99_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(k7_xcmplx_0(1,A),k7_xcmplx_0(B,C)) = k7_xcmplx_0(B,k3_xcmplx_0(C,A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l28_xcmplx_1,t79_xcmplx_1]),
    [file(xcmplx_1,l99_xcmplx_1),interesting(0.76)]).

fof(l68_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k5_xcmplx_0(k3_xcmplx_0(A,k5_xcmplx_0(B))) = k3_xcmplx_0(k5_xcmplx_0(A),B) ) ) ),
    inference(mizar_proof,[status(thm)],[l25_xcmplx_1]),
    [file(xcmplx_1,l68_xcmplx_1),interesting(0.76)]).

fof(l25_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) = k5_xcmplx_0(k3_xcmplx_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d7_xcmplx_0,t6_xcmplx_1,d7_xcmplx_0,d7_xcmplx_0,d7_xcmplx_0]),
    [file(xcmplx_1,l25_xcmplx_1),interesting(0.75)]).

fof(t194_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k4_xcmplx_0(A) = k7_xcmplx_0(A,k4_xcmplx_0(1)) ) ),
    inference(mizar_proof,[status(thm)],[t189_xcmplx_1]),
    [file(xcmplx_1,t194_xcmplx_1),interesting(0.75)]).

fof(t195_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => A = k7_xcmplx_0(k4_xcmplx_0(A),k4_xcmplx_0(1)) ) ),
    inference(mizar_proof,[status(thm)],[t189_xcmplx_1]),
    [file(xcmplx_1,t195_xcmplx_1),interesting(0.75)]).

fof(t76_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(k7_xcmplx_0(A,B),C) = k3_xcmplx_0(k7_xcmplx_0(C,B),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l60_xcmplx_1,l60_xcmplx_1]),
    [file(xcmplx_1,t76_xcmplx_1),interesting(0.75)]).

fof(t50_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( A != 0
              & B != 0
              & k7_xcmplx_0(A,B) = 0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[l55_xcmplx_1,t6_xcmplx_1,d9_xcmplx_0]),
    [file(xcmplx_1,t50_xcmplx_1),interesting(0.74)]).

fof(t57_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(1,k7_xcmplx_0(A,B)) = k7_xcmplx_0(B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l28_xcmplx_1,l68_xcmplx_1,d9_xcmplx_0]),
    [file(xcmplx_1,t57_xcmplx_1),interesting(0.74)]).

fof(t234_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( B != 0
              & ! [C] : 
                  ( v1_xcmplx_0(C)
                 => A != k7_xcmplx_0(B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,t203_xcmplx_1,d9_xcmplx_0,t6_xcmplx_1,d7_xcmplx_0,d9_xcmplx_0,d7_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t234_xcmplx_1),interesting(0.73)]).

fof(t49_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(A,0) = 0 ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0]),
    [file(xcmplx_1,t49_xcmplx_1),interesting(0.70)]).

fof(t202_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k5_xcmplx_0(A) = k5_xcmplx_0(B)
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[l71_xcmplx_1]),
    [file(xcmplx_1,t202_xcmplx_1),interesting(0.70)]).

fof(t6_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( k3_xcmplx_0(A,B) = 0
              & A != 0
              & B != 0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[t4_xcmplx_1,d7_xcmplx_0]),
    [file(xcmplx_1,t6_xcmplx_1),interesting(0.69)]).

fof(l29_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( A != 0
       => k7_xcmplx_0(A,A) = 1 ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d7_xcmplx_0]),
    [file(xcmplx_1,l29_xcmplx_1),interesting(0.68)]).

fof(t59_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k7_xcmplx_0(1,A) = k7_xcmplx_0(1,B)
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[l28_xcmplx_1,l28_xcmplx_1,l71_xcmplx_1]),
    [file(xcmplx_1,t59_xcmplx_1),interesting(0.68)]).

fof(t75_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(A,k7_xcmplx_0(B,C)) = k7_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l60_xcmplx_1]),
    [file(xcmplx_1,t75_xcmplx_1),interesting(0.68)]).

fof(t78_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(A,k7_xcmplx_0(B,C)) = k7_xcmplx_0(k3_xcmplx_0(A,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_xcmplx_1]),
    [file(xcmplx_1,t78_xcmplx_1),interesting(0.67)]).

fof(t80_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(A,k7_xcmplx_0(B,C)) = k3_xcmplx_0(A,k7_xcmplx_0(C,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_xcmplx_1,d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t80_xcmplx_1),interesting(0.67)]).

fof(t81_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(A,k7_xcmplx_0(B,C)) = k3_xcmplx_0(k7_xcmplx_0(C,B),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_xcmplx_1,d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t81_xcmplx_1),interesting(0.67)]).

fof(t83_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(A,k7_xcmplx_0(B,C)) = k3_xcmplx_0(k7_xcmplx_0(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_xcmplx_1,d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t83_xcmplx_1),interesting(0.67)]).

fof(t85_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k7_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,D)) = k7_xcmplx_0(k3_xcmplx_0(A,D),k3_xcmplx_0(B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l92_xcmplx_1]),
    [file(xcmplx_1,t85_xcmplx_1),interesting(0.67)]).

fof(t191_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k7_xcmplx_0(k4_xcmplx_0(A),B)) = k7_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[l138_xcmplx_1]),
    [file(xcmplx_1,t191_xcmplx_1),interesting(0.65)]).

fof(l58_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,D)) = k7_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d9_xcmplx_0,l25_xcmplx_1,d9_xcmplx_0]),
    [file(xcmplx_1,l58_xcmplx_1),interesting(0.64)]).

fof(l138_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k7_xcmplx_0(A,B)) = k7_xcmplx_0(k4_xcmplx_0(A),B) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,l138_xcmplx_1),interesting(0.64)]).

fof(l63_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => B = k7_xcmplx_0(k3_xcmplx_0(B,A),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l29_xcmplx_1,d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,l63_xcmplx_1),interesting(0.64)]).

fof(t206_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k5_xcmplx_0(k3_xcmplx_0(A,k5_xcmplx_0(B))) = k3_xcmplx_0(k5_xcmplx_0(A),B) ) ) ),
    inference(mizar_proof,[status(thm)],[l68_xcmplx_1]),
    [file(xcmplx_1,t206_xcmplx_1),interesting(0.64)]).

fof(t88_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => k3_xcmplx_0(k7_xcmplx_0(B,A),A) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[l27_xcmplx_1]),
    [file(xcmplx_1,t88_xcmplx_1),interesting(0.64)]).

fof(t104_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(k7_xcmplx_0(1,A),k7_xcmplx_0(B,C)) = k7_xcmplx_0(B,k3_xcmplx_0(C,A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l99_xcmplx_1]),
    [file(xcmplx_1,t104_xcmplx_1),interesting(0.63)]).

fof(t205_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) = k5_xcmplx_0(k3_xcmplx_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[l25_xcmplx_1]),
    [file(xcmplx_1,t205_xcmplx_1),interesting(0.63)]).

fof(t207_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k5_xcmplx_0(k3_xcmplx_0(k5_xcmplx_0(A),k5_xcmplx_0(B))) = k3_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[l25_xcmplx_1]),
    [file(xcmplx_1,t207_xcmplx_1),interesting(0.63)]).

fof(l27_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => k3_xcmplx_0(k7_xcmplx_0(B,A),A) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d7_xcmplx_0]),
    [file(xcmplx_1,l27_xcmplx_1),interesting(0.62)]).

fof(t7_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k3_xcmplx_0(B,A) = A
           => ( A = 0
              | B = 1 ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0,t4_xcmplx_1]),
    [file(xcmplx_1,t7_xcmplx_1),interesting(0.62)]).

fof(t121_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,B)) = k7_xcmplx_0(k6_xcmplx_0(A,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l138_xcmplx_1,t63_xcmplx_1]),
    [file(xcmplx_1,t121_xcmplx_1),interesting(0.61)]).

fof(t51_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => B = k7_xcmplx_0(B,k7_xcmplx_0(A,A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l29_xcmplx_1]),
    [file(xcmplx_1,t51_xcmplx_1),interesting(0.61)]).

fof(t183_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ~ ( k3_xcmplx_0(A,A) = 1
          & A != 1
          & A != k4_xcmplx_0(1) ) ) ),
    inference(mizar_proof,[status(thm)],[t6_xcmplx_1]),
    [file(xcmplx_1,t183_xcmplx_1),interesting(0.60)]).

fof(t223_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(k5_xcmplx_0(A),B) = k5_xcmplx_0(k3_xcmplx_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l25_xcmplx_1]),
    [file(xcmplx_1,t223_xcmplx_1),interesting(0.60)]).

fof(t54_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k7_xcmplx_0(A,B) != 0
           => B = k7_xcmplx_0(A,k7_xcmplx_0(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t49_xcmplx_1,l27_xcmplx_1,l63_xcmplx_1]),
    [file(xcmplx_1,t54_xcmplx_1),interesting(0.60)]).

fof(l117_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(1,k5_xcmplx_0(A)) = A ) ),
    inference(mizar_proof,[status(thm)],[l28_xcmplx_1]),
    [file(xcmplx_1,l117_xcmplx_1),interesting(0.58)]).

fof(t63_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k2_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,B)) = k7_xcmplx_0(k2_xcmplx_0(A,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t63_xcmplx_1),interesting(0.58)]).

fof(l65_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k7_xcmplx_0(B,C) = k7_xcmplx_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d7_xcmplx_0,l25_xcmplx_1,d9_xcmplx_0]),
    [file(xcmplx_1,l65_xcmplx_1),interesting(0.57)]).

fof(t48_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(k7_xcmplx_0(A,B),C) = k7_xcmplx_0(k7_xcmplx_0(A,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d9_xcmplx_0,d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t48_xcmplx_1),interesting(0.57)]).

fof(t55_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k7_xcmplx_0(B,C) = k7_xcmplx_0(k7_xcmplx_0(B,A),k7_xcmplx_0(C,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l55_xcmplx_1,l65_xcmplx_1,d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t55_xcmplx_1),interesting(0.57)]).

fof(l28_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(1,A) = k5_xcmplx_0(A) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0]),
    [file(xcmplx_1,l28_xcmplx_1),interesting(0.56)]).

fof(t62_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(A,0) = 0 ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0]),
    [file(xcmplx_1,t62_xcmplx_1),interesting(0.55)]).

fof(t86_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,D)) = k3_xcmplx_0(k7_xcmplx_0(A,D),k7_xcmplx_0(C,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l58_xcmplx_1,l58_xcmplx_1]),
    [file(xcmplx_1,t86_xcmplx_1),interesting(0.55)]).

fof(t60_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( A != 0
       => k7_xcmplx_0(A,A) = 1 ) ) ),
    inference(mizar_proof,[status(thm)],[l29_xcmplx_1]),
    [file(xcmplx_1,t60_xcmplx_1),interesting(0.54)]).

fof(t5_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( k3_xcmplx_0(B,A) = k3_xcmplx_0(C,A)
               => ( A = 0
                  | B = C ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t4_xcmplx_1,d7_xcmplx_0,d7_xcmplx_0]),
    [file(xcmplx_1,t5_xcmplx_1),interesting(0.53)]).

fof(t61_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k7_xcmplx_0(A,B) = A
           => ( A = 0
              | B = 1 ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t49_xcmplx_1,l27_xcmplx_1,t7_xcmplx_1]),
    [file(xcmplx_1,t61_xcmplx_1),interesting(0.53)]).

fof(t210_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k3_xcmplx_0(A,k5_xcmplx_0(B)) = 1
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,t58_xcmplx_1]),
    [file(xcmplx_1,t210_xcmplx_1),interesting(0.51)]).

fof(t53_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( k7_xcmplx_0(B,A) = k7_xcmplx_0(C,A)
               => ( A = 0
                  | B = C ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l27_xcmplx_1,l27_xcmplx_1]),
    [file(xcmplx_1,t53_xcmplx_1),interesting(0.51)]).

fof(l98_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(A,k7_xcmplx_0(1,B)) = k7_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l28_xcmplx_1]),
    [file(xcmplx_1,l98_xcmplx_1),interesting(0.50)]).

fof(t77_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,D)) = k7_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l58_xcmplx_1]),
    [file(xcmplx_1,t77_xcmplx_1),interesting(0.50)]).

fof(t188_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k7_xcmplx_0(A,B)) = k7_xcmplx_0(k4_xcmplx_0(A),B) ) ) ),
    inference(mizar_proof,[status(thm)],[l138_xcmplx_1]),
    [file(xcmplx_1,t188_xcmplx_1),interesting(0.49)]).

fof(t90_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => B = k7_xcmplx_0(k3_xcmplx_0(B,A),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l63_xcmplx_1]),
    [file(xcmplx_1,t90_xcmplx_1),interesting(0.49)]).

fof(t89_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => B = k3_xcmplx_0(B,k7_xcmplx_0(A,A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l29_xcmplx_1]),
    [file(xcmplx_1,t89_xcmplx_1),interesting(0.47)]).

fof(t216_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) = k7_xcmplx_0(B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t216_xcmplx_1),interesting(0.46)]).

fof(t220_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k7_xcmplx_0(1,A) = k5_xcmplx_0(B)
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t59_xcmplx_1,l28_xcmplx_1]),
    [file(xcmplx_1,t220_xcmplx_1),interesting(0.46)]).

fof(t222_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(k5_xcmplx_0(A),k7_xcmplx_0(B,C)) = k7_xcmplx_0(B,k3_xcmplx_0(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l25_xcmplx_1,d9_xcmplx_0]),
    [file(xcmplx_1,t222_xcmplx_1),interesting(0.45)]).

fof(t235_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ! [E] : 
                      ( v1_xcmplx_0(E)
                     => k7_xcmplx_0(A,k3_xcmplx_0(k3_xcmplx_0(B,C),k7_xcmplx_0(D,E))) = k3_xcmplx_0(k7_xcmplx_0(E,C),k7_xcmplx_0(A,k3_xcmplx_0(B,D))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d9_xcmplx_0,t82_xcmplx_1,t82_xcmplx_1]),
    [file(xcmplx_1,t235_xcmplx_1),interesting(0.45)]).

fof(t87_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ! [E] : 
                      ( v1_xcmplx_0(E)
                     => k7_xcmplx_0(A,k3_xcmplx_0(k3_xcmplx_0(B,C),k7_xcmplx_0(D,E))) = k3_xcmplx_0(k7_xcmplx_0(E,C),k7_xcmplx_0(A,k3_xcmplx_0(B,D))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d9_xcmplx_0,t82_xcmplx_1,t82_xcmplx_1]),
    [file(xcmplx_1,t87_xcmplx_1),interesting(0.45)]).

fof(t107_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( A != 0
       => k3_xcmplx_0(A,k7_xcmplx_0(1,A)) = 1 ) ) ),
    inference(mizar_proof,[status(thm)],[l28_xcmplx_1,d7_xcmplx_0]),
    [file(xcmplx_1,t107_xcmplx_1),interesting(0.44)]).

fof(t199_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( A != 0
       => k7_xcmplx_0(A,k4_xcmplx_0(A)) = k4_xcmplx_0(1) ) ) ),
    inference(mizar_proof,[status(thm)],[t189_xcmplx_1,l29_xcmplx_1]),
    [file(xcmplx_1,t199_xcmplx_1),interesting(0.44)]).

fof(l218_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ~ ( A != 0
          & A = k5_xcmplx_0(A)
          & A != 1
          & A != k4_xcmplx_0(1) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0,t183_xcmplx_1]),
    [file(xcmplx_1,l218_xcmplx_1),interesting(0.42)]).

fof(t218_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(1,k5_xcmplx_0(A)) = A ) ),
    inference(mizar_proof,[status(thm)],[l117_xcmplx_1]),
    [file(xcmplx_1,t218_xcmplx_1),interesting(0.42)]).

fof(t93_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k7_xcmplx_0(B,C) = k3_xcmplx_0(k7_xcmplx_0(B,k3_xcmplx_0(C,A)),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l58_xcmplx_1,l27_xcmplx_1]),
    [file(xcmplx_1,t93_xcmplx_1),interesting(0.42)]).

fof(t211_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k3_xcmplx_0(A,B) = 1
           => A = k5_xcmplx_0(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0]),
    [file(xcmplx_1,t211_xcmplx_1),interesting(0.41)]).

fof(t74_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k3_xcmplx_0(A,B) = 1
           => A = k7_xcmplx_0(1,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0,l28_xcmplx_1]),
    [file(xcmplx_1,t74_xcmplx_1),interesting(0.41)]).

fof(t92_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k7_xcmplx_0(B,C) = k7_xcmplx_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l65_xcmplx_1]),
    [file(xcmplx_1,t92_xcmplx_1),interesting(0.41)]).

fof(t94_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k3_xcmplx_0(B,C) = k7_xcmplx_0(k3_xcmplx_0(B,A),k7_xcmplx_0(A,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0,l68_xcmplx_1,d9_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t94_xcmplx_1),interesting(0.41)]).

fof(t95_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ( k3_xcmplx_0(C,A) = k3_xcmplx_0(D,B)
                   => ( A = 0
                      | B = 0
                      | k7_xcmplx_0(C,B) = k7_xcmplx_0(D,A) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l63_xcmplx_1,l60_xcmplx_1,l63_xcmplx_1]),
    [file(xcmplx_1,t95_xcmplx_1),interesting(0.40)]).

fof(t182_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k3_xcmplx_0(B,A) = k4_xcmplx_0(A)
           => ( A = 0
              | B = k4_xcmplx_0(1) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t4_xcmplx_1,d7_xcmplx_0,d7_xcmplx_0]),
    [file(xcmplx_1,t182_xcmplx_1),interesting(0.40)]).

fof(t208_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( A != 0
              & B != 0
              & k3_xcmplx_0(A,k5_xcmplx_0(B)) = 0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[l55_xcmplx_1,t6_xcmplx_1]),
    [file(xcmplx_1,t208_xcmplx_1),interesting(0.40)]).

fof(t217_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(1,A) = k5_xcmplx_0(A) ) ),
    inference(mizar_proof,[status(thm)],[l28_xcmplx_1]),
    [file(xcmplx_1,t217_xcmplx_1),interesting(0.40)]).

fof(t219_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k5_xcmplx_0(k7_xcmplx_0(1,A)) = A ) ),
    inference(mizar_proof,[status(thm)],[l28_xcmplx_1]),
    [file(xcmplx_1,t219_xcmplx_1),interesting(0.40)]).

fof(t101_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(A,k7_xcmplx_0(1,B)) = k3_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[l28_xcmplx_1,l98_xcmplx_1,l117_xcmplx_1]),
    [file(xcmplx_1,t101_xcmplx_1),interesting(0.38)]).

fof(t103_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(k7_xcmplx_0(1,A),k7_xcmplx_0(1,B)) = k7_xcmplx_0(1,k3_xcmplx_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[l28_xcmplx_1,l28_xcmplx_1,l25_xcmplx_1,l28_xcmplx_1]),
    [file(xcmplx_1,t103_xcmplx_1),interesting(0.38)]).

fof(t116_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k2_xcmplx_0(B,C) = k7_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l63_xcmplx_1,l63_xcmplx_1,t63_xcmplx_1]),
    [file(xcmplx_1,t116_xcmplx_1),interesting(0.38)]).

fof(t96_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ( k7_xcmplx_0(C,B) = k7_xcmplx_0(D,A)
                   => ( A = 0
                      | B = 0
                      | k3_xcmplx_0(C,A) = k3_xcmplx_0(D,B) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l27_xcmplx_1,l60_xcmplx_1,l27_xcmplx_1]),
    [file(xcmplx_1,t96_xcmplx_1),interesting(0.37)]).

fof(t123_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k7_xcmplx_0(k6_xcmplx_0(k6_xcmplx_0(A,B),C),D) = k6_xcmplx_0(k6_xcmplx_0(k7_xcmplx_0(A,D),k7_xcmplx_0(B,D)),k7_xcmplx_0(C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t121_xcmplx_1,t121_xcmplx_1]),
    [file(xcmplx_1,t123_xcmplx_1),interesting(0.36)]).

fof(t204_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => B = k3_xcmplx_0(k3_xcmplx_0(B,A),k5_xcmplx_0(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0]),
    [file(xcmplx_1,t204_xcmplx_1),interesting(0.35)]).

fof(t115_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k2_xcmplx_0(B,C) = k3_xcmplx_0(A,k2_xcmplx_0(k7_xcmplx_0(B,A),k7_xcmplx_0(C,A))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l27_xcmplx_1,l27_xcmplx_1]),
    [file(xcmplx_1,t115_xcmplx_1),interesting(0.34)]).

fof(t209_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( A != 0
              & B != 0
              & k3_xcmplx_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) = 0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[l55_xcmplx_1,t6_xcmplx_1]),
    [file(xcmplx_1,t209_xcmplx_1),interesting(0.34)]).

fof(t214_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( A != 0
              & B != 0
              & k6_xcmplx_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) != k3_xcmplx_0(k6_xcmplx_0(B,A),k5_xcmplx_0(k3_xcmplx_0(A,B))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l233_xcmplx_1,t213_xcmplx_1,l233_xcmplx_1]),
    [file(xcmplx_1,t214_xcmplx_1),interesting(0.34)]).

fof(t221_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(A,k5_xcmplx_0(B)) = k3_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0]),
    [file(xcmplx_1,t221_xcmplx_1),interesting(0.34)]).

fof(t127_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k6_xcmplx_0(k7_xcmplx_0(B,A),C) = k7_xcmplx_0(k6_xcmplx_0(B,k3_xcmplx_0(C,A)),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t114_xcmplx_1]),
    [file(xcmplx_1,t127_xcmplx_1),interesting(0.33)]).

fof(t100_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(A,k7_xcmplx_0(1,B)) = k7_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[l98_xcmplx_1]),
    [file(xcmplx_1,t100_xcmplx_1),interesting(0.32)]).

fof(t113_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( A != 0
              & B != 0
              & k3_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(B,A)) != 1 ) ) ) ),
    inference(mizar_proof,[status(thm)],[l59_xcmplx_1,t50_xcmplx_1,d7_xcmplx_0]),
    [file(xcmplx_1,t113_xcmplx_1),interesting(0.32)]).

fof(t114_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k2_xcmplx_0(k7_xcmplx_0(B,A),C) = k7_xcmplx_0(k2_xcmplx_0(B,k3_xcmplx_0(A,C)),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d9_xcmplx_0,t63_xcmplx_1]),
    [file(xcmplx_1,t114_xcmplx_1),interesting(0.32)]).

fof(t196_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k7_xcmplx_0(A,B) = k4_xcmplx_0(1)
           => ( A = k4_xcmplx_0(B)
              & B = k4_xcmplx_0(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t49_xcmplx_1,l27_xcmplx_1]),
    [file(xcmplx_1,t196_xcmplx_1),interesting(0.32)]).

fof(t64_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k7_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(A,B),C),D) = k2_xcmplx_0(k2_xcmplx_0(k7_xcmplx_0(A,D),k7_xcmplx_0(B,D)),k7_xcmplx_0(C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t63_xcmplx_1,t63_xcmplx_1]),
    [file(xcmplx_1,t64_xcmplx_1),interesting(0.30)]).

fof(t98_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k7_xcmplx_0(B,C) = k3_xcmplx_0(A,k7_xcmplx_0(k7_xcmplx_0(B,A),C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l27_xcmplx_1,d9_xcmplx_0]),
    [file(xcmplx_1,t98_xcmplx_1),interesting(0.30)]).

fof(t99_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k7_xcmplx_0(B,C) = k3_xcmplx_0(k7_xcmplx_0(B,A),k7_xcmplx_0(A,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l27_xcmplx_1,d9_xcmplx_0]),
    [file(xcmplx_1,t99_xcmplx_1),interesting(0.30)]).

fof(t91_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k3_xcmplx_0(B,C) = k3_xcmplx_0(k3_xcmplx_0(B,A),k7_xcmplx_0(C,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0,d9_xcmplx_0]),
    [file(xcmplx_1,t91_xcmplx_1),interesting(0.28)]).

fof(t198_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( A != 0
       => k7_xcmplx_0(k4_xcmplx_0(A),A) = k4_xcmplx_0(1) ) ) ),
    inference(mizar_proof,[status(thm)],[l138_xcmplx_1,l29_xcmplx_1]),
    [file(xcmplx_1,t198_xcmplx_1),interesting(0.26)]).

fof(t213_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( A != 0
              & B != 0
              & k2_xcmplx_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) != k3_xcmplx_0(k2_xcmplx_0(A,B),k5_xcmplx_0(k3_xcmplx_0(A,B))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0,l25_xcmplx_1]),
    [file(xcmplx_1,t213_xcmplx_1),interesting(0.26)]).

fof(t197_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k7_xcmplx_0(A,B) = k4_xcmplx_0(A)
           => ( A = 0
              | B = k4_xcmplx_0(1) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t49_xcmplx_1,l27_xcmplx_1,t182_xcmplx_1]),
    [file(xcmplx_1,t197_xcmplx_1),interesting(0.25)]).

fof(t112_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( A != 0
              & B != 0
              & k7_xcmplx_0(1,k3_xcmplx_0(A,B)) = 0 ) ) ) ),
    inference(mizar_proof,[status(thm)],[l55_xcmplx_1,t6_xcmplx_1,l25_xcmplx_1,l28_xcmplx_1]),
    [file(xcmplx_1,t112_xcmplx_1),interesting(0.24)]).

fof(t119_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k2_xcmplx_0(k7_xcmplx_0(A,k3_xcmplx_0(2,B)),k7_xcmplx_0(A,k3_xcmplx_0(2,B))) = k7_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t63_xcmplx_1,l65_xcmplx_1]),
    [file(xcmplx_1,t119_xcmplx_1),interesting(0.24)]).

fof(t117_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ~ ( A != 0
                      & B != 0
                      & k2_xcmplx_0(k7_xcmplx_0(C,A),k7_xcmplx_0(D,B)) != k7_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(C,B),k3_xcmplx_0(D,A)),k3_xcmplx_0(A,B)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l65_xcmplx_1,l65_xcmplx_1,t63_xcmplx_1]),
    [file(xcmplx_1,t117_xcmplx_1),interesting(0.24)]).

fof(t118_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => k2_xcmplx_0(A,B) = k3_xcmplx_0(A,k2_xcmplx_0(1,k7_xcmplx_0(B,A))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t115_xcmplx_1,l29_xcmplx_1]),
    [file(xcmplx_1,t118_xcmplx_1),interesting(0.23)]).

fof(t225_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ~ ( A != 0
          & A = k5_xcmplx_0(A)
          & A != 1
          & A != k4_xcmplx_0(1) ) ) ),
    inference(mizar_proof,[status(thm)],[l218_xcmplx_1]),
    [file(xcmplx_1,t225_xcmplx_1),interesting(0.23)]).

fof(t200_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ~ ( A != 0
          & A = k7_xcmplx_0(1,A)
          & A != 1
          & A != k4_xcmplx_0(1) ) ) ),
    inference(mizar_proof,[status(thm)],[l218_xcmplx_1,l28_xcmplx_1]),
    [file(xcmplx_1,t200_xcmplx_1),interesting(0.21)]).

fof(t102_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(k7_xcmplx_0(A,B),C) = k3_xcmplx_0(k3_xcmplx_0(k7_xcmplx_0(1,B),C),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l98_xcmplx_1]),
    [file(xcmplx_1,t102_xcmplx_1),interesting(0.20)]).

fof(t108_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => B = k3_xcmplx_0(k3_xcmplx_0(B,A),k7_xcmplx_0(1,A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l29_xcmplx_1,d9_xcmplx_0,l28_xcmplx_1]),
    [file(xcmplx_1,t108_xcmplx_1),interesting(0.19)]).

fof(t111_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => B = k7_xcmplx_0(B,k3_xcmplx_0(A,k7_xcmplx_0(1,A))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t107_xcmplx_1]),
    [file(xcmplx_1,t111_xcmplx_1),interesting(0.19)]).

fof(t125_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k7_xcmplx_0(k6_xcmplx_0(k2_xcmplx_0(A,B),C),D) = k6_xcmplx_0(k2_xcmplx_0(k7_xcmplx_0(A,D),k7_xcmplx_0(B,D)),k7_xcmplx_0(C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t121_xcmplx_1,t63_xcmplx_1]),
    [file(xcmplx_1,t125_xcmplx_1),interesting(0.19)]).

fof(t126_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k7_xcmplx_0(k2_xcmplx_0(k6_xcmplx_0(A,B),C),D) = k2_xcmplx_0(k6_xcmplx_0(k7_xcmplx_0(A,D),k7_xcmplx_0(B,D)),k7_xcmplx_0(C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t63_xcmplx_1,t121_xcmplx_1]),
    [file(xcmplx_1,t126_xcmplx_1),interesting(0.19)]).

fof(t105_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(k7_xcmplx_0(A,B),C) = k3_xcmplx_0(k7_xcmplx_0(1,B),k7_xcmplx_0(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d9_xcmplx_0,d9_xcmplx_0,d9_xcmplx_0,d9_xcmplx_0,l28_xcmplx_1]),
    [file(xcmplx_1,t105_xcmplx_1),interesting(0.18)]).

fof(t106_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k7_xcmplx_0(k7_xcmplx_0(A,B),C) = k3_xcmplx_0(k7_xcmplx_0(1,C),k7_xcmplx_0(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,l28_xcmplx_1]),
    [file(xcmplx_1,t106_xcmplx_1),interesting(0.18)]).

fof(t130_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k6_xcmplx_0(B,C) = k7_xcmplx_0(k6_xcmplx_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t116_xcmplx_1]),
    [file(xcmplx_1,t130_xcmplx_1),interesting(0.18)]).

fof(t109_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => B = k3_xcmplx_0(B,k3_xcmplx_0(k7_xcmplx_0(1,A),A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l27_xcmplx_1]),
    [file(xcmplx_1,t109_xcmplx_1),interesting(0.17)]).

fof(t110_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => B = k3_xcmplx_0(k3_xcmplx_0(B,k7_xcmplx_0(1,A)),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l27_xcmplx_1]),
    [file(xcmplx_1,t110_xcmplx_1),interesting(0.17)]).

fof(t128_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k6_xcmplx_0(B,k7_xcmplx_0(C,A)) = k7_xcmplx_0(k6_xcmplx_0(k3_xcmplx_0(B,A),C),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t127_xcmplx_1,l138_xcmplx_1]),
    [file(xcmplx_1,t128_xcmplx_1),interesting(0.15)]).

fof(t97_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ( k3_xcmplx_0(C,A) = k7_xcmplx_0(D,B)
                   => ( A = 0
                      | B = 0
                      | k3_xcmplx_0(C,B) = k7_xcmplx_0(D,A) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l27_xcmplx_1,l63_xcmplx_1]),
    [file(xcmplx_1,t97_xcmplx_1),interesting(0.15)]).

fof(t236_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k2_xcmplx_0(k3_xcmplx_0(k7_xcmplx_0(k6_xcmplx_0(A,B),C),D),B) = k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,k7_xcmplx_0(D,C)),B),k3_xcmplx_0(k7_xcmplx_0(D,C),A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,d7_xcmplx_0,d9_xcmplx_0,d7_xcmplx_0,l29_xcmplx_1,l60_xcmplx_1,l60_xcmplx_1,t63_xcmplx_1,t63_xcmplx_1,l60_xcmplx_1,l60_xcmplx_1,t121_xcmplx_1,l29_xcmplx_1]),
    [file(xcmplx_1,t236_xcmplx_1),interesting(0.14)]).

fof(t201_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ( k7_xcmplx_0(C,A) = k7_xcmplx_0(D,B)
                   => ( A = 0
                      | B = 0
                      | A = k4_xcmplx_0(B)
                      | k7_xcmplx_0(C,A) = k7_xcmplx_0(k2_xcmplx_0(C,D),k2_xcmplx_0(A,B)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t96_xcmplx_1,t95_xcmplx_1]),
    [file(xcmplx_1,t201_xcmplx_1),interesting(0.12)]).

fof(t129_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k6_xcmplx_0(B,C) = k3_xcmplx_0(A,k6_xcmplx_0(k7_xcmplx_0(B,A),k7_xcmplx_0(C,A))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l27_xcmplx_1,l27_xcmplx_1]),
    [file(xcmplx_1,t129_xcmplx_1),interesting(0.11)]).

fof(t237_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => k2_xcmplx_0(k3_xcmplx_0(A,B),C) = k3_xcmplx_0(A,k2_xcmplx_0(B,k7_xcmplx_0(C,A))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t88_xcmplx_1]),
    [file(xcmplx_1,t237_xcmplx_1),interesting(0.11)]).

fof(t120_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k2_xcmplx_0(k2_xcmplx_0(k7_xcmplx_0(A,k3_xcmplx_0(3,B)),k7_xcmplx_0(A,k3_xcmplx_0(3,B))),k7_xcmplx_0(A,k3_xcmplx_0(3,B))) = k7_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[t63_xcmplx_1,t63_xcmplx_1,l65_xcmplx_1]),
    [file(xcmplx_1,t120_xcmplx_1),interesting(0.05)]).

fof(t131_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ~ ( A != 0
                      & B != 0
                      & k6_xcmplx_0(k7_xcmplx_0(C,A),k7_xcmplx_0(D,B)) != k7_xcmplx_0(k6_xcmplx_0(k3_xcmplx_0(C,B),k3_xcmplx_0(D,A)),k3_xcmplx_0(A,B)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l138_xcmplx_1,t117_xcmplx_1]),
    [file(xcmplx_1,t131_xcmplx_1),interesting(0.03)]).

fof(t132_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => k6_xcmplx_0(A,B) = k3_xcmplx_0(A,k6_xcmplx_0(1,k7_xcmplx_0(B,A))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t118_xcmplx_1,l138_xcmplx_1]),
    [file(xcmplx_1,t132_xcmplx_1),interesting(0.02)]).

fof(d9_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(A,B) = k3_xcmplx_0(A,k5_xcmplx_0(B)) ) ) ),
    file(xcmplx_0,d9_xcmplx_0),
    [interesting(0.00)]).

fof(d7_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( ( A != 0
             => ( B = k5_xcmplx_0(A)
              <=> k3_xcmplx_0(A,B) = 1 ) )
            & ( A = 0
             => ( B = k5_xcmplx_0(A)
              <=> B = 0 ) ) ) ) ) ),
    file(xcmplx_0,d7_xcmplx_0),
    [interesting(0.00)]).

fof(t4_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(A,k3_xcmplx_0(B,C)) = k3_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t4_xcmplx_1),
    [interesting(0.00)]).

fof(l55_xcmplx_1,theorem,(
    k5_xcmplx_0(0) = 0 ),
    file(xcmplx_1,l55_xcmplx_1),
    [interesting(0.00)]).

fof(t10_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k2_xcmplx_0(A,B),k2_xcmplx_0(C,D)) = k2_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(A,D)),k3_xcmplx_0(B,C)),k3_xcmplx_0(B,D)) ) ) ) ) ),
    file(xcmplx_1,t10_xcmplx_1),
    [interesting(0.00)]).

fof(t11_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k3_xcmplx_0(2,A) = k2_xcmplx_0(A,A) ) ),
    file(xcmplx_1,t11_xcmplx_1),
    [interesting(0.00)]).

fof(t122_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k6_xcmplx_0(A,k7_xcmplx_0(A,2)) = k7_xcmplx_0(A,2) ) ),
    file(xcmplx_1,t122_xcmplx_1),
    [interesting(0.00)]).

fof(t124_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ( k7_xcmplx_0(C,A) = k7_xcmplx_0(D,B)
                   => ( A = 0
                      | B = 0
                      | A = B
                      | k7_xcmplx_0(C,A) = k7_xcmplx_0(k6_xcmplx_0(C,D),k6_xcmplx_0(A,B)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t96_xcmplx_1,t95_xcmplx_1]),
    [file(xcmplx_1,t124_xcmplx_1),interesting(0.00)]).

fof(t12_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k3_xcmplx_0(3,A) = k2_xcmplx_0(k2_xcmplx_0(A,A),A) ) ),
    file(xcmplx_1,t12_xcmplx_1),
    [interesting(0.00)]).

fof(t133_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( A != 0
               => B = k7_xcmplx_0(k6_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(A,B),C),C),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l63_xcmplx_1]),
    [file(xcmplx_1,t133_xcmplx_1),interesting(0.00)]).

fof(t134_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k4_xcmplx_0(A) = k4_xcmplx_0(B)
           => A = B ) ) ) ),
    file(xcmplx_1,t134_xcmplx_1),
    [interesting(0.00)]).

fof(t135_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( k4_xcmplx_0(A) = 0
       => A = 0 ) ) ),
    file(xcmplx_1,t135_xcmplx_1),
    [interesting(0.00)]).

fof(t136_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k2_xcmplx_0(A,k4_xcmplx_0(B)) = 0
           => A = B ) ) ) ),
    file(xcmplx_1,t136_xcmplx_1),
    [interesting(0.00)]).

fof(t137_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => A = k2_xcmplx_0(k2_xcmplx_0(A,B),k4_xcmplx_0(B)) ) ) ),
    file(xcmplx_1,t137_xcmplx_1),
    [interesting(0.00)]).

fof(t138_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => A = k2_xcmplx_0(A,k2_xcmplx_0(B,k4_xcmplx_0(B))) ) ) ),
    file(xcmplx_1,t138_xcmplx_1),
    [interesting(0.00)]).

fof(t139_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => A = k2_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(B),A),B) ) ) ),
    file(xcmplx_1,t139_xcmplx_1),
    [interesting(0.00)]).

fof(t13_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k3_xcmplx_0(4,A) = k2_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(A,A),A),A) ) ),
    file(xcmplx_1,t13_xcmplx_1),
    [interesting(0.00)]).

fof(t140_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k2_xcmplx_0(A,B)) = k2_xcmplx_0(k4_xcmplx_0(A),k4_xcmplx_0(B)) ) ) ),
    file(xcmplx_1,t140_xcmplx_1),
    [interesting(0.00)]).

fof(t141_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(A),B)) = k2_xcmplx_0(A,k4_xcmplx_0(B)) ) ) ),
    file(xcmplx_1,t141_xcmplx_1),
    [interesting(0.00)]).

fof(t142_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k2_xcmplx_0(A,B) = k4_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(A),k4_xcmplx_0(B))) ) ) ),
    file(xcmplx_1,t142_xcmplx_1),
    [interesting(0.00)]).

fof(t143_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k6_xcmplx_0(A,B)) = k6_xcmplx_0(B,A) ) ) ),
    file(xcmplx_1,t143_xcmplx_1),
    [interesting(0.00)]).

fof(t144_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k6_xcmplx_0(k4_xcmplx_0(A),B) = k6_xcmplx_0(k4_xcmplx_0(B),A) ) ) ),
    file(xcmplx_1,t144_xcmplx_1),
    [interesting(0.00)]).

fof(t145_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => A = k6_xcmplx_0(k4_xcmplx_0(B),k6_xcmplx_0(k4_xcmplx_0(A),B)) ) ) ),
    file(xcmplx_1,t145_xcmplx_1),
    [interesting(0.00)]).

fof(t146_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(A),B),C) = k6_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(A),C),B) ) ) ) ),
    file(xcmplx_1,t146_xcmplx_1),
    [interesting(0.00)]).

fof(t147_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(A),B),C) = k6_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(B),C),A) ) ) ) ),
    file(xcmplx_1,t147_xcmplx_1),
    [interesting(0.00)]).

fof(t148_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(A),B),C) = k6_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(C),B),A) ) ) ) ),
    file(xcmplx_1,t148_xcmplx_1),
    [interesting(0.00)]).

fof(t149_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k6_xcmplx_0(A,B),k6_xcmplx_0(A,C)) = k4_xcmplx_0(k6_xcmplx_0(B,C)) ) ) ) ),
    file(xcmplx_1,t149_xcmplx_1),
    [interesting(0.00)]).

fof(t14_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k6_xcmplx_0(A,A) = 0 ) ),
    file(xcmplx_1,t14_xcmplx_1),
    [interesting(0.00)]).

fof(t150_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k6_xcmplx_0(0,A) = k4_xcmplx_0(A) ) ),
    file(xcmplx_1,t150_xcmplx_1),
    [interesting(0.00)]).

fof(t151_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k2_xcmplx_0(A,B) = k6_xcmplx_0(A,k4_xcmplx_0(B)) ) ) ),
    file(xcmplx_1,t151_xcmplx_1),
    [interesting(0.00)]).

fof(t152_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => A = k6_xcmplx_0(A,k2_xcmplx_0(B,k4_xcmplx_0(B))) ) ) ),
    file(xcmplx_1,t152_xcmplx_1),
    [interesting(0.00)]).

fof(t153_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( k6_xcmplx_0(A,B) = k2_xcmplx_0(C,k4_xcmplx_0(B))
               => A = C ) ) ) ) ),
    file(xcmplx_1,t153_xcmplx_1),
    [interesting(0.00)]).

fof(t154_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( k6_xcmplx_0(A,B) = k2_xcmplx_0(A,k4_xcmplx_0(C))
               => B = C ) ) ) ) ),
    file(xcmplx_1,t154_xcmplx_1),
    [interesting(0.00)]).

fof(t155_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k2_xcmplx_0(A,B),C) = k2_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(C),A),B) ) ) ) ),
    file(xcmplx_1,t155_xcmplx_1),
    [interesting(0.00)]).

fof(t156_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k2_xcmplx_0(k6_xcmplx_0(A,B),C) = k2_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(B),C),A) ) ) ) ),
    file(xcmplx_1,t156_xcmplx_1),
    [interesting(0.00)]).

fof(t157_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(A,k6_xcmplx_0(k4_xcmplx_0(B),C)) = k2_xcmplx_0(k2_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t157_xcmplx_1),
    [interesting(0.00)]).

fof(t158_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k6_xcmplx_0(A,B),C) = k2_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(B),C),A) ) ) ) ),
    file(xcmplx_1,t158_xcmplx_1),
    [interesting(0.00)]).

fof(t159_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k6_xcmplx_0(A,B),C) = k6_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(C),A),B) ) ) ) ),
    file(xcmplx_1,t159_xcmplx_1),
    [interesting(0.00)]).

fof(t15_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k6_xcmplx_0(A,B) = 0
           => A = B ) ) ) ),
    file(xcmplx_1,t15_xcmplx_1),
    [interesting(0.00)]).

fof(t160_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k6_xcmplx_0(A,B),C) = k2_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(C),B),A) ) ) ) ),
    file(xcmplx_1,t160_xcmplx_1),
    [interesting(0.00)]).

fof(t161_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k2_xcmplx_0(A,B)) = k6_xcmplx_0(k4_xcmplx_0(B),A) ) ) ),
    file(xcmplx_1,t161_xcmplx_1),
    [interesting(0.00)]).

fof(t162_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k6_xcmplx_0(A,B)) = k2_xcmplx_0(k4_xcmplx_0(A),B) ) ) ),
    file(xcmplx_1,t162_xcmplx_1),
    [interesting(0.00)]).

fof(t163_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(A),B)) = k6_xcmplx_0(A,B) ) ) ),
    file(xcmplx_1,t163_xcmplx_1),
    [interesting(0.00)]).

fof(t164_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k2_xcmplx_0(A,B) = k4_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(A),B)) ) ) ),
    file(xcmplx_1,t164_xcmplx_1),
    [interesting(0.00)]).

fof(t165_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(A),B),C) = k6_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(C),B),A) ) ) ) ),
    file(xcmplx_1,t165_xcmplx_1),
    [interesting(0.00)]).

fof(t166_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(A),B),C) = k2_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(C),A),B) ) ) ) ),
    file(xcmplx_1,t166_xcmplx_1),
    [interesting(0.00)]).

fof(t167_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k4_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(A,B),C)) = k6_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(A),B),C) ) ) ) ),
    file(xcmplx_1,t167_xcmplx_1),
    [interesting(0.00)]).

fof(t168_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k4_xcmplx_0(k6_xcmplx_0(k2_xcmplx_0(A,B),C)) = k2_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(A),B),C) ) ) ) ),
    file(xcmplx_1,t168_xcmplx_1),
    [interesting(0.00)]).

fof(t169_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k4_xcmplx_0(k2_xcmplx_0(k6_xcmplx_0(A,B),C)) = k6_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(A),B),C) ) ) ) ),
    file(xcmplx_1,t169_xcmplx_1),
    [interesting(0.00)]).

fof(t16_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k6_xcmplx_0(A,B) = A
           => B = 0 ) ) ) ),
    file(xcmplx_1,t16_xcmplx_1),
    [interesting(0.00)]).

fof(t170_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k4_xcmplx_0(k6_xcmplx_0(k6_xcmplx_0(A,B),C)) = k2_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(A),B),C) ) ) ) ),
    file(xcmplx_1,t170_xcmplx_1),
    [interesting(0.00)]).

fof(t171_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k4_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(A),B),C)) = k6_xcmplx_0(k6_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t171_xcmplx_1),
    [interesting(0.00)]).

fof(t172_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k4_xcmplx_0(k6_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(A),B),C)) = k2_xcmplx_0(k6_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t172_xcmplx_1),
    [interesting(0.00)]).

fof(t173_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k4_xcmplx_0(k2_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(A),B),C)) = k6_xcmplx_0(k2_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t173_xcmplx_1),
    [interesting(0.00)]).

fof(t174_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k4_xcmplx_0(k6_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(A),B),C)) = k2_xcmplx_0(k2_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t174_xcmplx_1),
    [interesting(0.00)]).

fof(t175_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(k4_xcmplx_0(A),B) = k4_xcmplx_0(k3_xcmplx_0(A,B)) ) ) ),
    file(xcmplx_1,t175_xcmplx_1),
    [interesting(0.00)]).

fof(t176_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(k4_xcmplx_0(A),B) = k3_xcmplx_0(A,k4_xcmplx_0(B)) ) ) ),
    file(xcmplx_1,t176_xcmplx_1),
    [interesting(0.00)]).

fof(t177_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(k4_xcmplx_0(A),k4_xcmplx_0(B)) = k3_xcmplx_0(A,B) ) ) ),
    file(xcmplx_1,t177_xcmplx_1),
    [interesting(0.00)]).

fof(t178_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k3_xcmplx_0(A,k4_xcmplx_0(B))) = k3_xcmplx_0(A,B) ) ) ),
    file(xcmplx_1,t178_xcmplx_1),
    [interesting(0.00)]).

fof(t179_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k4_xcmplx_0(k3_xcmplx_0(k4_xcmplx_0(A),B)) = k3_xcmplx_0(A,B) ) ) ),
    file(xcmplx_1,t179_xcmplx_1),
    [interesting(0.00)]).

fof(t17_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => A = k6_xcmplx_0(A,k6_xcmplx_0(B,B)) ) ) ),
    file(xcmplx_1,t17_xcmplx_1),
    [interesting(0.00)]).

fof(t180_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k3_xcmplx_0(k4_xcmplx_0(1),A) = k4_xcmplx_0(A) ) ),
    file(xcmplx_1,t180_xcmplx_1),
    [interesting(0.00)]).

fof(t181_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k3_xcmplx_0(k4_xcmplx_0(A),k4_xcmplx_0(1)) = A ) ),
    file(xcmplx_1,t181_xcmplx_1),
    [interesting(0.00)]).

fof(t184_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k2_xcmplx_0(k4_xcmplx_0(A),k3_xcmplx_0(2,A)) = A ) ),
    file(xcmplx_1,t184_xcmplx_1),
    [interesting(0.00)]).

fof(t185_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(k6_xcmplx_0(A,B),C) = k3_xcmplx_0(k6_xcmplx_0(B,A),k4_xcmplx_0(C)) ) ) ) ),
    file(xcmplx_1,t185_xcmplx_1),
    [interesting(0.00)]).

fof(t186_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(k6_xcmplx_0(A,B),C) = k4_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(B,A),C)) ) ) ) ),
    file(xcmplx_1,t186_xcmplx_1),
    [interesting(0.00)]).

fof(t187_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k6_xcmplx_0(A,k3_xcmplx_0(2,A)) = k4_xcmplx_0(A) ) ),
    file(xcmplx_1,t187_xcmplx_1),
    [interesting(0.00)]).

fof(t18_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k6_xcmplx_0(A,k6_xcmplx_0(A,B)) = B ) ) ),
    file(xcmplx_1,t18_xcmplx_1),
    [interesting(0.00)]).

fof(t19_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( k6_xcmplx_0(A,B) = k6_xcmplx_0(C,B)
               => A = C ) ) ) ) ),
    file(xcmplx_1,t19_xcmplx_1),
    [interesting(0.00)]).

fof(t1_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k2_xcmplx_0(A,k2_xcmplx_0(B,C)) = k2_xcmplx_0(k2_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t1_xcmplx_1),
    [interesting(0.00)]).

fof(l71_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( k5_xcmplx_0(A) = k5_xcmplx_0(B)
           => A = B ) ) ) ),
    file(xcmplx_1,l71_xcmplx_1),
    [interesting(0.00)]).

fof(t20_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( k6_xcmplx_0(A,B) = k6_xcmplx_0(A,C)
               => B = C ) ) ) ) ),
    file(xcmplx_1,t20_xcmplx_1),
    [interesting(0.00)]).

fof(t212_xcmplx_1,theorem,(
    $true ),
    file(xcmplx_1,t212_xcmplx_1),
    [interesting(0.00)]).

fof(t21_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k6_xcmplx_0(A,B),C) = k6_xcmplx_0(k6_xcmplx_0(A,C),B) ) ) ) ),
    file(xcmplx_1,t21_xcmplx_1),
    [interesting(0.00)]).

fof(t226_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(A,B),C),B) = k2_xcmplx_0(A,C) ) ) ) ),
    file(xcmplx_1,t226_xcmplx_1),
    [interesting(0.00)]).

fof(t227_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k2_xcmplx_0(k2_xcmplx_0(k6_xcmplx_0(A,B),C),B) = k2_xcmplx_0(A,C) ) ) ) ),
    file(xcmplx_1,t227_xcmplx_1),
    [interesting(0.00)]).

fof(t228_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k6_xcmplx_0(k2_xcmplx_0(A,B),C),B) = k6_xcmplx_0(A,C) ) ) ) ),
    file(xcmplx_1,t228_xcmplx_1),
    [interesting(0.00)]).

fof(t229_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k2_xcmplx_0(k6_xcmplx_0(k6_xcmplx_0(A,B),C),B) = k6_xcmplx_0(A,C) ) ) ) ),
    file(xcmplx_1,t229_xcmplx_1),
    [interesting(0.00)]).

fof(t22_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(A,B) = k6_xcmplx_0(k6_xcmplx_0(A,C),k6_xcmplx_0(B,C)) ) ) ) ),
    file(xcmplx_1,t22_xcmplx_1),
    [interesting(0.00)]).

fof(t230_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k6_xcmplx_0(k6_xcmplx_0(A,A),B) = k4_xcmplx_0(B) ) ) ),
    file(xcmplx_1,t230_xcmplx_1),
    [interesting(0.00)]).

fof(t231_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k6_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(A),A),B) = k4_xcmplx_0(B) ) ) ),
    file(xcmplx_1,t231_xcmplx_1),
    [interesting(0.00)]).

fof(t232_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k6_xcmplx_0(k6_xcmplx_0(A,B),A) = k4_xcmplx_0(B) ) ) ),
    file(xcmplx_1,t232_xcmplx_1),
    [interesting(0.00)]).

fof(t233_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k2_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(A),B),A) = k4_xcmplx_0(B) ) ) ),
    file(xcmplx_1,t233_xcmplx_1),
    [interesting(0.00)]).

fof(t203_xcmplx_1,theorem,(
    k5_xcmplx_0(0) = 0 ),
    file(xcmplx_1,t203_xcmplx_1),
    [interesting(0.00)]).

fof(t23_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k6_xcmplx_0(A,B),k6_xcmplx_0(A,C)) = k6_xcmplx_0(C,B) ) ) ) ),
    file(xcmplx_1,t23_xcmplx_1),
    [interesting(0.00)]).

fof(t24_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ( k6_xcmplx_0(A,B) = k6_xcmplx_0(C,D)
                   => k6_xcmplx_0(A,C) = k6_xcmplx_0(B,D) ) ) ) ) ) ),
    file(xcmplx_1,t24_xcmplx_1),
    [interesting(0.00)]).

fof(t25_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => A = k2_xcmplx_0(A,k6_xcmplx_0(B,B)) ) ) ),
    file(xcmplx_1,t25_xcmplx_1),
    [interesting(0.00)]).

fof(t26_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => A = k6_xcmplx_0(k2_xcmplx_0(A,B),B) ) ) ),
    file(xcmplx_1,t26_xcmplx_1),
    [interesting(0.00)]).

fof(t27_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => A = k2_xcmplx_0(k6_xcmplx_0(A,B),B) ) ) ),
    file(xcmplx_1,t27_xcmplx_1),
    [interesting(0.00)]).

fof(t28_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k2_xcmplx_0(A,B) = k2_xcmplx_0(k2_xcmplx_0(A,C),k6_xcmplx_0(B,C)) ) ) ) ),
    file(xcmplx_1,t28_xcmplx_1),
    [interesting(0.00)]).

fof(t29_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(k2_xcmplx_0(A,B),C) = k2_xcmplx_0(k6_xcmplx_0(A,C),B) ) ) ) ),
    file(xcmplx_1,t29_xcmplx_1),
    [interesting(0.00)]).

fof(t2_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( k2_xcmplx_0(A,B) = k2_xcmplx_0(C,B)
               => A = C ) ) ) ) ),
    file(xcmplx_1,t2_xcmplx_1),
    [interesting(0.00)]).

fof(t30_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k2_xcmplx_0(k6_xcmplx_0(A,B),C) = k2_xcmplx_0(k6_xcmplx_0(C,B),A) ) ) ) ),
    file(xcmplx_1,t30_xcmplx_1),
    [interesting(0.00)]).

fof(t31_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k2_xcmplx_0(A,B) = k6_xcmplx_0(k2_xcmplx_0(A,C),k6_xcmplx_0(C,B)) ) ) ) ),
    file(xcmplx_1,t31_xcmplx_1),
    [interesting(0.00)]).

fof(t32_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(A,B) = k6_xcmplx_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ),
    file(xcmplx_1,t32_xcmplx_1),
    [interesting(0.00)]).

fof(t33_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ( k2_xcmplx_0(A,B) = k2_xcmplx_0(C,D)
                   => k6_xcmplx_0(A,C) = k6_xcmplx_0(D,B) ) ) ) ) ) ),
    file(xcmplx_1,t33_xcmplx_1),
    [interesting(0.00)]).

fof(t34_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ( k6_xcmplx_0(A,B) = k6_xcmplx_0(C,D)
                   => k2_xcmplx_0(A,D) = k2_xcmplx_0(B,C) ) ) ) ) ) ),
    file(xcmplx_1,t34_xcmplx_1),
    [interesting(0.00)]).

fof(t35_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => ( k2_xcmplx_0(A,B) = k6_xcmplx_0(C,D)
                   => k2_xcmplx_0(A,D) = k6_xcmplx_0(C,B) ) ) ) ) ) ),
    file(xcmplx_1,t35_xcmplx_1),
    [interesting(0.00)]).

fof(t36_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(A,k2_xcmplx_0(B,C)) = k6_xcmplx_0(k6_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t36_xcmplx_1),
    [interesting(0.00)]).

fof(t37_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(A,k6_xcmplx_0(B,C)) = k2_xcmplx_0(k6_xcmplx_0(A,B),C) ) ) ) ),
    file(xcmplx_1,t37_xcmplx_1),
    [interesting(0.00)]).

fof(t38_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(A,k6_xcmplx_0(B,C)) = k2_xcmplx_0(A,k6_xcmplx_0(C,B)) ) ) ) ),
    file(xcmplx_1,t38_xcmplx_1),
    [interesting(0.00)]).

fof(t39_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k6_xcmplx_0(A,B) = k2_xcmplx_0(k6_xcmplx_0(A,C),k6_xcmplx_0(C,B)) ) ) ) ),
    file(xcmplx_1,t39_xcmplx_1),
    [interesting(0.00)]).

fof(t3_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A = k2_xcmplx_0(A,B)
           => B = 0 ) ) ) ),
    file(xcmplx_1,t3_xcmplx_1),
    [interesting(0.00)]).

fof(t40_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(A,k6_xcmplx_0(B,C)) = k6_xcmplx_0(k3_xcmplx_0(A,B),k3_xcmplx_0(A,C)) ) ) ) ),
    file(xcmplx_1,t40_xcmplx_1),
    [interesting(0.00)]).

fof(t41_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k6_xcmplx_0(A,B),k6_xcmplx_0(C,D)) = k3_xcmplx_0(k6_xcmplx_0(B,A),k6_xcmplx_0(D,C)) ) ) ) ) ),
    file(xcmplx_1,t41_xcmplx_1),
    [interesting(0.00)]).

fof(t42_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k6_xcmplx_0(k6_xcmplx_0(A,B),C),D) = k6_xcmplx_0(k6_xcmplx_0(k3_xcmplx_0(A,D),k3_xcmplx_0(B,D)),k3_xcmplx_0(C,D)) ) ) ) ) ),
    file(xcmplx_1,t42_xcmplx_1),
    [interesting(0.00)]).

fof(t43_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k6_xcmplx_0(k2_xcmplx_0(A,B),C),D) = k6_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(A,D),k3_xcmplx_0(B,D)),k3_xcmplx_0(C,D)) ) ) ) ) ),
    file(xcmplx_1,t43_xcmplx_1),
    [interesting(0.00)]).

fof(t44_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k2_xcmplx_0(k6_xcmplx_0(A,B),C),D) = k2_xcmplx_0(k6_xcmplx_0(k3_xcmplx_0(A,D),k3_xcmplx_0(B,D)),k3_xcmplx_0(C,D)) ) ) ) ) ),
    file(xcmplx_1,t44_xcmplx_1),
    [interesting(0.00)]).

fof(t45_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k2_xcmplx_0(A,B),k6_xcmplx_0(C,D)) = k6_xcmplx_0(k2_xcmplx_0(k6_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(A,D)),k3_xcmplx_0(B,C)),k3_xcmplx_0(B,D)) ) ) ) ) ),
    file(xcmplx_1,t45_xcmplx_1),
    [interesting(0.00)]).

fof(t46_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k6_xcmplx_0(A,B),k2_xcmplx_0(C,D)) = k6_xcmplx_0(k6_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(A,D)),k3_xcmplx_0(B,C)),k3_xcmplx_0(B,D)) ) ) ) ) ),
    file(xcmplx_1,t46_xcmplx_1),
    [interesting(0.00)]).

fof(t47_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k6_xcmplx_0(A,B),k6_xcmplx_0(C,D)) = k2_xcmplx_0(k6_xcmplx_0(k6_xcmplx_0(k3_xcmplx_0(A,C),k3_xcmplx_0(A,D)),k3_xcmplx_0(B,C)),k3_xcmplx_0(B,D)) ) ) ) ) ),
    file(xcmplx_1,t47_xcmplx_1),
    [interesting(0.00)]).

fof(t65_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(k2_xcmplx_0(A,A),2) = A ) ),
    file(xcmplx_1,t65_xcmplx_1),
    [interesting(0.00)]).

fof(t66_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k2_xcmplx_0(k7_xcmplx_0(A,2),k7_xcmplx_0(A,2)) = A ) ),
    file(xcmplx_1,t66_xcmplx_1),
    [interesting(0.00)]).

fof(t67_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A = k7_xcmplx_0(k2_xcmplx_0(A,B),2)
           => A = B ) ) ) ),
    file(xcmplx_1,t67_xcmplx_1),
    [interesting(0.00)]).

fof(t68_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(A,A),A),3) = A ) ),
    file(xcmplx_1,t68_xcmplx_1),
    [interesting(0.00)]).

fof(t69_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k2_xcmplx_0(k2_xcmplx_0(k7_xcmplx_0(A,3),k7_xcmplx_0(A,3)),k7_xcmplx_0(A,3)) = A ) ),
    file(xcmplx_1,t69_xcmplx_1),
    [interesting(0.00)]).

fof(t70_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(A,A),A),A),4) = A ) ),
    file(xcmplx_1,t70_xcmplx_1),
    [interesting(0.00)]).

fof(t71_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k2_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(k7_xcmplx_0(A,4),k7_xcmplx_0(A,4)),k7_xcmplx_0(A,4)),k7_xcmplx_0(A,4)) = A ) ),
    file(xcmplx_1,t71_xcmplx_1),
    [interesting(0.00)]).

fof(t72_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k2_xcmplx_0(k7_xcmplx_0(A,4),k7_xcmplx_0(A,4)) = k7_xcmplx_0(A,2) ) ),
    file(xcmplx_1,t72_xcmplx_1),
    [interesting(0.00)]).

fof(t73_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(k2_xcmplx_0(A,A),4) = k7_xcmplx_0(A,2) ) ),
    file(xcmplx_1,t73_xcmplx_1),
    [interesting(0.00)]).

fof(t8_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => k3_xcmplx_0(A,k2_xcmplx_0(B,C)) = k2_xcmplx_0(k3_xcmplx_0(A,B),k3_xcmplx_0(A,C)) ) ) ) ),
    file(xcmplx_1,t8_xcmplx_1),
    [interesting(0.00)]).

fof(t9_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ! [D] : 
                  ( v1_xcmplx_0(D)
                 => k3_xcmplx_0(k2_xcmplx_0(k2_xcmplx_0(A,B),C),D) = k2_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(A,D),k3_xcmplx_0(B,D)),k3_xcmplx_0(C,D)) ) ) ) ) ),
    file(xcmplx_1,t9_xcmplx_1),
    [interesting(0.00)]).