include('Axioms/SET010^0.ax').
thf(k15_complex1_type, type, k15_complex1: $i > $i).
thf(k6_numbers_type, type, k6_numbers: $i).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(k3_complex1_type, type, k3_complex1: $i > $i).
thf(k4_complex1_type, type, k4_complex1: $i > $i).
thf(v1_xcmplx_0_type, type, v1_xcmplx_0: $i > $o).
thf(k6_xcmplx_0_type, type, k6_xcmplx_0: $i > $i > $i).
thf(k3_xcmplx_0_type, type, k3_xcmplx_0: $i > $i > $i).
thf(k7_complex1_type, type, k7_complex1: $i).
thf(k1_xcmplx_0_type, type, k1_xcmplx_0: $i).
thf(k1_xboole_0_type, type, k1_xboole_0: $i).
thf(k14_complex1_type, type, k14_complex1: $i > $i).
thf(v1_xxreal_0_type, type, v1_xxreal_0: $i > $o).
thf(v1_xreal_0_type, type, v1_xreal_0: $i > $o).
thf(t8_boole, axiom,   (! [A: $i] :  (! [B: $i] :  ~ ( ( (v1_xboole_0 @ A)  &  ( ~ ( ( (= @ A)  @ B) )  &  (v1_xboole_0 @ B) ) ) ) ) ) , file(boole, t8_boole)).
thf(t4_complex1, axiom,   ( ( (= @  (k3_complex1 @ k6_numbers) )  @ k6_numbers)  &  ( (= @  (k4_complex1 @ k6_numbers) )  @ k6_numbers) ) , file(complex1, t4_complex1)).
thf(t4_arithm, axiom,   (! [A: $i] :  ( (v1_xcmplx_0 @ A)  =>  ( (= @  ( (k6_xcmplx_0 @ A)  @ k6_numbers) )  @ A) ) ) , file(arithm, t4_arithm)).
thf(t2_arithm, axiom,   (! [A: $i] :  ( (v1_xcmplx_0 @ A)  =>  ( (= @  ( (k3_xcmplx_0 @ A)  @ k6_numbers) )  @ k6_numbers) ) ) , file(arithm, t2_arithm)).
thf(redefinition_k7_complex1, axiom,   ( (= @ k7_complex1)  @ k1_xcmplx_0) , file(complex1, k7_complex1)).
thf(redefinition_k6_numbers, axiom,   ( (= @ k6_numbers)  @ k1_xboole_0) , file(numbers, k6_numbers)).
thf(redefinition_k15_complex1, axiom,   (! [A: $i] :  ( (v1_xcmplx_0 @ A)  =>  ( (= @  (k15_complex1 @ A) )  @  (k14_complex1 @ A) ) ) ) , file(complex1, k15_complex1)).
thf(rc4_xreal_0, axiom,   (? [A: $i] :  ( (v1_xboole_0 @ A)  &  ( (v1_xcmplx_0 @ A)  &  ( (v1_xxreal_0 @ A)  &  (v1_xreal_0 @ A) ) ) ) ) , file(xreal_0, rc4_xreal_0)).
thf(fc1_xcmplx_0, axiom,   (v1_xcmplx_0 @ k1_xcmplx_0) , file(xcmplx_0, fc1_xcmplx_0)).
thf(fc1_xboole_0, axiom,   (v1_xboole_0 @ k1_xboole_0) , file(xboole_0, fc1_xboole_0)).
thf(d11_complex1, axiom,   (! [A: $i] :  ( (v1_xcmplx_0 @ A)  =>  ( (= @  (k14_complex1 @ A) )  @  ( (k6_xcmplx_0 @  (k3_complex1 @ A) )  @  ( (k3_xcmplx_0 @  (k4_complex1 @ A) )  @ k7_complex1) ) ) ) ) , file(complex1, d11_complex1)).
thf(commutativity_k3_xcmplx_0, axiom,   (! [A: $i, B: $i] :  ( ( (v1_xcmplx_0 @ A)  &  (v1_xcmplx_0 @ B) )  =>  ( (= @  ( (k3_xcmplx_0 @ A)  @ B) )  @  ( (k3_xcmplx_0 @ B)  @ A) ) ) ) , file(xcmplx_0, k3_xcmplx_0)).
thf(t28_complex1, conjecture,   ( (= @  (k15_complex1 @ k6_numbers) )  @ k6_numbers) , file(complex1, t28_complex1)).