thf(decl_true_0_0, type, (true_0_0 : $i)).
thf(decl_false_0_0, type, (false_0_0 : $i)).
thf(decl_forall_1_1, type, (forall_1_1 : (($i > $i) > $i))).
thf(decl_implies_0_2, type, (implies_0_2 : ($i > ($i > $i)))).
thf(decl_equals_0_2, type, (equals_0_2 : ($i > ($i > $i)))).
thf(decl_not_0_1, type, (not_0_1 : ($i > $i))).

thf(modusPonens, axiom, (! [A : $i, B : $i]: (((implies_0_2 @ A @ B) = true_0_0) => ((A = true_0_0) => (B = true_0_0))))).

thf(allIntro, axiom, (! [A : ($i > $i)]: ((! [X : $i]: ((A @ X) = true_0_0)) => ((forall_1_1 @ A) = true_0_0)))).

thf(axiom1, axiom, ((true_0_0) = (true_0_0))).

thf(axiom2, axiom, (! [B_0 : $i, A_0 : $i]: ((implies_0_2 @ (A_0) @ (implies_0_2 @ (B_0) @ (A_0))) = (true_0_0)))).

thf(axiom3, axiom, (! [C_0 : $i, A_0 : $i, B_0 : $i]: ((implies_0_2 @ (implies_0_2 @ (A_0) @ (implies_0_2 @ (B_0) @ (C_0))) @ (implies_0_2 @ (implies_0_2 @ (A_0) @ (B_0)) @ (implies_0_2 @ (A_0) @ (C_0)))) = (true_0_0)))).

thf(axiom4, axiom, (! [P_1 : ($i > $i), Y_0 : $i]: ((implies_0_2 @ (forall_1_1 @ (^[X_0 : $i]: (P_1 @ (X_0)))) @ (P_1 @ (Y_0))) = (true_0_0)))).

thf(axiom5, axiom, (! [A_0 : $i, P_1 : ($i > $i)]: ((implies_0_2 @ (forall_1_1 @ (^[X_0 : $i]: (implies_0_2 @ (A_0) @ (P_1 @ (X_0))))) @ (implies_0_2 @ (A_0) @ (forall_1_1 @ (^[X_0 : $i]: (P_1 @ (X_0)))))) = (true_0_0)))).

thf(axiom6, axiom, (! [X_0 : $i]: ((equals_0_2 @ (X_0) @ (X_0)) = (true_0_0)))).

thf(axiom7, axiom, (! [Y_0 : $i, P_1 : ($i > $i), X_0 : $i]: ((implies_0_2 @ (equals_0_2 @ (X_0) @ (Y_0)) @ (implies_0_2 @ (P_1 @ (X_0)) @ (P_1 @ (Y_0)))) = (true_0_0)))).

thf(axiom8, axiom, (! [A_0 : $i]: ((implies_0_2 @ (A_0) @ (equals_0_2 @ (A_0) @ (true_0_0))) = (true_0_0)))).

thf(axiom9, axiom, ((equals_0_2 @ (false_0_0) @ (forall_1_1 @ (^[X_0 : $i]: (X_0)))) = (true_0_0))).

thf(axiom10, axiom, (! [A_0 : $i]: ((equals_0_2 @ (not_0_1 @ (A_0)) @ (implies_0_2 @ (A_0) @ (false_0_0))) = (true_0_0)))).

thf(conjecture, conjecture, (! [A_0 : $i, B_0 : $i]: ((implies_0_2 @ (A_0) @ (implies_0_2 @ (not_0_1 @ (A_0)) @ (B_0))) = (true_0_0)))).