%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU280+1 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:27:28 AM UTC 2025
% Result : Theorem 0.21s 0.57s
% Output : Proof 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU280+1 : TPTP v9.0.0. Released v3.3.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n003.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 20 06:35:24 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.21/0.57 % SZS status Theorem
% 0.21/0.57 % SZS output start Proof
% 0.21/0.57 tff(in_type, type, (
% 0.21/0.57 in: ( $i * $i ) > $o)).
% 0.21/0.57 tff(tptp_fun_B_3_type, type, (
% 0.21/0.57 tptp_fun_B_3: $i > $i)).
% 0.21/0.57 tff(tptp_fun_A_0_type, type, (
% 0.21/0.57 tptp_fun_A_0: $i)).
% 0.21/0.57 tff(tptp_fun_C_1_type, type, (
% 0.21/0.57 tptp_fun_C_1: $i > $i)).
% 0.21/0.57 tff(ordinal_type, type, (
% 0.21/0.57 ordinal: $i > $o)).
% 0.21/0.57 tff(1,assumption,(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))), introduced(assumption)).
% 0.21/0.57 tff(2,plain,
% 0.21/0.57 (^[A: $i, C: $i] : refl((~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A)))) <=> (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A)))))),
% 0.21/0.57 inference(bind,[status(th)],[])).
% 0.21/0.57 tff(3,plain,
% 0.21/0.57 (![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A)))) <=> ![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))),
% 0.21/0.57 inference(quant_intro,[status(thm)],[2])).
% 0.21/0.57 tff(4,plain,
% 0.21/0.57 (^[A: $i, C: $i] : trans(trans(monotonicity(rewrite((ordinal(C) & in(C, A)) <=> (~((~ordinal(C)) | (~in(C, A))))), ((in(C, tptp_fun_B_3(A)) <=> (ordinal(C) & in(C, A))) <=> (in(C, tptp_fun_B_3(A)) <=> (~((~ordinal(C)) | (~in(C, A))))))), rewrite((in(C, tptp_fun_B_3(A)) <=> (~((~ordinal(C)) | (~in(C, A))))) <=> (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))), ((in(C, tptp_fun_B_3(A)) <=> (ordinal(C) & in(C, A))) <=> (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A)))))), rewrite((~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A)))) <=> (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))), ((in(C, tptp_fun_B_3(A)) <=> (ordinal(C) & in(C, A))) <=> (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))))),
% 0.21/0.57 inference(bind,[status(th)],[])).
% 0.21/0.57 tff(5,plain,
% 0.21/0.57 (![A: $i, C: $i] : (in(C, tptp_fun_B_3(A)) <=> (ordinal(C) & in(C, A))) <=> ![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))),
% 0.21/0.57 inference(quant_intro,[status(thm)],[4])).
% 0.21/0.57 tff(6,plain,
% 0.21/0.57 (![A: $i] : ![C: $i] : (in(C, tptp_fun_B_3(A)) <=> (ordinal(C) & in(C, A))) <=> ![A: $i, C: $i] : (in(C, tptp_fun_B_3(A)) <=> (ordinal(C) & in(C, A)))),
% 0.21/0.57 inference(pull_quant,[status(thm)],[])).
% 0.21/0.57 tff(7,plain,
% 0.21/0.57 (![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A))) <=> ![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A)))),
% 0.21/0.57 inference(rewrite,[status(thm)],[])).
% 0.21/0.57 tff(8,plain,
% 0.21/0.57 (^[A: $i] : trans(monotonicity(trans(quant_intro(proof_bind(^[B: $i, C: $i, D: $i] : trans(monotonicity(trans(monotonicity(rewrite((((B = C) & ordinal(C)) & (B = D)) <=> ((B = C) & ordinal(C) & (B = D))), (((((B = C) & ordinal(C)) & (B = D)) & ordinal(D)) <=> (((B = C) & ordinal(C) & (B = D)) & ordinal(D)))), rewrite((((B = C) & ordinal(C) & (B = D)) & ordinal(D)) <=> ((B = C) & ordinal(C) & (B = D) & ordinal(D))), (((((B = C) & ordinal(C)) & (B = D)) & ordinal(D)) <=> ((B = C) & ordinal(C) & (B = D) & ordinal(D)))), ((((((B = C) & ordinal(C)) & (B = D)) & ordinal(D)) => (C = D)) <=> (((B = C) & ordinal(C) & (B = D) & ordinal(D)) => (C = D)))), rewrite((((B = C) & ordinal(C) & (B = D) & ordinal(D)) => (C = D)) <=> ((~((B = C) & ordinal(C) & (B = D) & ordinal(D))) | (C = D))), ((((((B = C) & ordinal(C)) & (B = D)) & ordinal(D)) => (C = D)) <=> ((~((B = C) & ordinal(C) & (B = D) & ordinal(D))) | (C = D))))), (![B: $i, C: $i, D: $i] : (((((B = C) & ordinal(C)) & (B = D)) & ordinal(D)) => (C = D)) <=> ![B: $i, C: $i, D: $i] : ((~((B = C) & ordinal(C) & (B = D) & ordinal(D))) | (C = D)))), trans(trans(trans(der(![B: $i, C: $i, D: $i] : ((~((B = C) & ordinal(C) & (B = D) & ordinal(D))) | (C = D)) <=> ![B: $i, C: $i, D: $i] : ((C = D) | (~ordinal(D)) | (~ordinal(C)) | (~(C = D)))), der(![B: $i, C: $i, D: $i] : ((C = D) | (~ordinal(D)) | (~ordinal(C)) | (~(C = D))) <=> ![B: $i, C: $i, D: $i] : ((D = D) | (~ordinal(D)) | (~ordinal(D)))), (![B: $i, C: $i, D: $i] : ((~((B = C) & ordinal(C) & (B = D) & ordinal(D))) | (C = D)) <=> ![B: $i, C: $i, D: $i] : ((D = D) | (~ordinal(D)) | (~ordinal(D))))), elim_unused(![B: $i, C: $i, D: $i] : ((D = D) | (~ordinal(D)) | (~ordinal(D))) <=> ![D: $i] : ((D = D) | (~ordinal(D)) | (~ordinal(D)))), (![B: $i, C: $i, D: $i] : ((~((B = C) & ordinal(C) & (B = D) & ordinal(D))) | (C = D)) <=> ![D: $i] : ((D = D) | (~ordinal(D)) | (~ordinal(D))))), trans(quant_intro(proof_bind(^[D: $i] : trans(monotonicity(rewrite((D = D) <=> $true), (((D = D) | (~ordinal(D)) | (~ordinal(D))) <=> ($true | (~ordinal(D)) | (~ordinal(D))))), rewrite(($true | (~ordinal(D)) | (~ordinal(D))) <=> $true), (((D = D) | (~ordinal(D)) | (~ordinal(D))) <=> $true))), (![D: $i] : ((D = D) | (~ordinal(D)) | (~ordinal(D))) <=> ![D: $i] : $true)), elim_unused(![D: $i] : $true <=> $true), (![D: $i] : ((D = D) | (~ordinal(D)) | (~ordinal(D))) <=> $true)), (![B: $i, C: $i, D: $i] : ((~((B = C) & ordinal(C) & (B = D) & ordinal(D))) | (C = D)) <=> $true)), (![B: $i, C: $i, D: $i] : (((((B = C) & ordinal(C)) & (B = D)) & ordinal(D)) => (C = D)) <=> $true)), quant_intro(proof_bind(^[B: $i] : quant_intro(proof_bind(^[C: $i] : rewrite((in(C, B) <=> ?[D: $i] : ((in(D, A) & (D = C)) & ordinal(C))) <=> (in(C, B) <=> (ordinal(C) & in(C, A))))), (![C: $i] : (in(C, B) <=> ?[D: $i] : ((in(D, A) & (D = C)) & ordinal(C))) <=> ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A)))))), (?[B: $i] : ![C: $i] : (in(C, B) <=> ?[D: $i] : ((in(D, A) & (D = C)) & ordinal(C))) <=> ?[B: $i] : ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A))))), ((![B: $i, C: $i, D: $i] : (((((B = C) & ordinal(C)) & (B = D)) & ordinal(D)) => (C = D)) => ?[B: $i] : ![C: $i] : (in(C, B) <=> ?[D: $i] : ((in(D, A) & (D = C)) & ordinal(C)))) <=> ($true => ?[B: $i] : ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A)))))), rewrite(($true => ?[B: $i] : ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A)))) <=> ?[B: $i] : ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A)))), ((![B: $i, C: $i, D: $i] : (((((B = C) & ordinal(C)) & (B = D)) & ordinal(D)) => (C = D)) => ?[B: $i] : ![C: $i] : (in(C, B) <=> ?[D: $i] : ((in(D, A) & (D = C)) & ordinal(C)))) <=> ?[B: $i] : ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A)))))),
% 0.21/0.57 inference(bind,[status(th)],[])).
% 0.21/0.57 tff(9,plain,
% 0.21/0.57 (![A: $i] : (![B: $i, C: $i, D: $i] : (((((B = C) & ordinal(C)) & (B = D)) & ordinal(D)) => (C = D)) => ?[B: $i] : ![C: $i] : (in(C, B) <=> ?[D: $i] : ((in(D, A) & (D = C)) & ordinal(C)))) <=> ![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A)))),
% 0.21/0.57 inference(quant_intro,[status(thm)],[8])).
% 0.21/0.57 tff(10,axiom,(![A: $i] : (![B: $i, C: $i, D: $i] : (((((B = C) & ordinal(C)) & (B = D)) & ordinal(D)) => (C = D)) => ?[B: $i] : ![C: $i] : (in(C, B) <=> ?[D: $i] : ((in(D, A) & (D = C)) & ordinal(C))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','s1_tarski__e6_22__wellord2__1')).
% 0.21/0.57 tff(11,plain,
% 0.21/0.57 (![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A)))),
% 0.21/0.57 inference(modus_ponens,[status(thm)],[10, 9])).
% 0.21/0.57 tff(12,plain,
% 0.21/0.57 (![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (ordinal(C) & in(C, A)))),
% 0.21/0.57 inference(modus_ponens,[status(thm)],[11, 7])).
% 0.21/0.57 tff(13,plain,(
% 0.21/0.57 ![A: $i] : ![C: $i] : (in(C, tptp_fun_B_3(A)) <=> (ordinal(C) & in(C, A)))),
% 0.21/0.57 inference(skolemize,[status(sab)],[12])).
% 0.21/0.57 tff(14,plain,
% 0.21/0.57 (![A: $i, C: $i] : (in(C, tptp_fun_B_3(A)) <=> (ordinal(C) & in(C, A)))),
% 0.21/0.57 inference(modus_ponens,[status(thm)],[13, 6])).
% 0.21/0.57 tff(15,plain,
% 0.21/0.57 (![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))),
% 0.21/0.57 inference(modus_ponens,[status(thm)],[14, 5])).
% 0.21/0.57 tff(16,plain,
% 0.21/0.57 (![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))),
% 0.21/0.57 inference(modus_ponens,[status(thm)],[15, 3])).
% 0.21/0.57 tff(17,plain,
% 0.21/0.57 ((~![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))) | (~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.57 inference(quant_inst,[status(thm)],[])).
% 0.21/0.57 tff(18,plain,
% 0.21/0.57 ($false),
% 0.21/0.57 inference(unit_resolution,[status(thm)],[17, 16, 1])).
% 0.21/0.57 tff(19,plain,(~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.57 tff(20,assumption,(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))), introduced(assumption)).
% 0.21/0.57 tff(21,plain,
% 0.21/0.57 ((~![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))) | (~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))))),
% 0.21/0.57 inference(quant_inst,[status(thm)],[])).
% 0.21/0.57 tff(22,plain,
% 0.21/0.57 ($false),
% 0.21/0.57 inference(unit_resolution,[status(thm)],[21, 16, 20])).
% 0.21/0.57 tff(23,plain,(~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.58 tff(24,assumption,(~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))), introduced(assumption)).
% 0.21/0.58 tff(25,plain,
% 0.21/0.58 (^[B: $i] : trans(monotonicity(trans(trans(monotonicity(rewrite((in(tptp_fun_C_1(B), A!0) & ordinal(tptp_fun_C_1(B))) <=> (~((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))))), ((in(tptp_fun_C_1(B), B) <=> (in(tptp_fun_C_1(B), A!0) & ordinal(tptp_fun_C_1(B)))) <=> (in(tptp_fun_C_1(B), B) <=> (~((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))))))), rewrite((in(tptp_fun_C_1(B), B) <=> (~((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))))) <=> (~(((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B)))), ((in(tptp_fun_C_1(B), B) <=> (in(tptp_fun_C_1(B), A!0) & ordinal(tptp_fun_C_1(B)))) <=> (~(((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B))))), rewrite((~(((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B))) <=> (~(((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B)))), ((in(tptp_fun_C_1(B), B) <=> (in(tptp_fun_C_1(B), A!0) & ordinal(tptp_fun_C_1(B)))) <=> (~(((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B))))), ((~(in(tptp_fun_C_1(B), B) <=> (in(tptp_fun_C_1(B), A!0) & ordinal(tptp_fun_C_1(B))))) <=> (~(~(((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B)))))), rewrite((~(~(((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B)))) <=> (((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B))), ((~(in(tptp_fun_C_1(B), B) <=> (in(tptp_fun_C_1(B), A!0) & ordinal(tptp_fun_C_1(B))))) <=> (((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B))))),
% 0.21/0.58 inference(bind,[status(th)],[])).
% 0.21/0.58 tff(26,plain,
% 0.21/0.58 (![B: $i] : (~(in(tptp_fun_C_1(B), B) <=> (in(tptp_fun_C_1(B), A!0) & ordinal(tptp_fun_C_1(B))))) <=> ![B: $i] : (((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B))),
% 0.21/0.58 inference(quant_intro,[status(thm)],[25])).
% 0.21/0.58 tff(27,plain,
% 0.21/0.58 ((~![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (in(C, A) & ordinal(C)))) <=> (~![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (in(C, A) & ordinal(C))))),
% 0.21/0.58 inference(rewrite,[status(thm)],[])).
% 0.21/0.58 tff(28,axiom,(~![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (in(C, A) & ordinal(C)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','s1_xboole_0__e6_22__wellord2')).
% 0.21/0.58 tff(29,plain,
% 0.21/0.58 (~![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (in(C, A) & ordinal(C)))),
% 0.21/0.58 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.21/0.58 tff(30,plain,
% 0.21/0.58 (~![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (in(C, A) & ordinal(C)))),
% 0.21/0.58 inference(modus_ponens,[status(thm)],[29, 27])).
% 0.21/0.58 tff(31,plain,
% 0.21/0.58 (~![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (in(C, A) & ordinal(C)))),
% 0.21/0.58 inference(modus_ponens,[status(thm)],[30, 27])).
% 0.21/0.58 tff(32,plain,
% 0.21/0.58 (~![A: $i] : ?[B: $i] : ![C: $i] : (in(C, B) <=> (in(C, A) & ordinal(C)))),
% 0.21/0.58 inference(modus_ponens,[status(thm)],[31, 27])).
% 0.21/0.58 tff(33,plain,(
% 0.21/0.58 $oeq((~?[B: $i] : ![C: $i] : (in(C, B) <=> (in(C, A!0) & ordinal(C)))), ![B: $i] : (~(in(tptp_fun_C_1(B), B) <=> (in(tptp_fun_C_1(B), A!0) & ordinal(tptp_fun_C_1(B))))))),
% 0.21/0.58 inference(transitivity,[status(sab)],[32])).
% 0.21/0.58 tff(34,plain,
% 0.21/0.58 (![B: $i] : (((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B))),
% 0.21/0.58 inference(modus_ponens,[status(thm)],[33, 26])).
% 0.21/0.58 tff(35,plain,
% 0.21/0.58 ((~![B: $i] : (((~in(tptp_fun_C_1(B), A!0)) | (~ordinal(tptp_fun_C_1(B)))) <=> in(tptp_fun_C_1(B), B))) | (((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(quant_inst,[status(thm)],[])).
% 0.21/0.58 tff(36,plain,
% 0.21/0.58 (((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[35, 34])).
% 0.21/0.58 tff(37,plain,
% 0.21/0.58 ((~(((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(38,plain,
% 0.21/0.58 ((~((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[37, 36])).
% 0.21/0.58 tff(39,plain,
% 0.21/0.58 (~((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[38, 24])).
% 0.21/0.58 tff(40,plain,
% 0.21/0.58 (((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))) | ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(41,plain,
% 0.21/0.58 (ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[40, 39])).
% 0.21/0.58 tff(42,assumption,(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))), introduced(assumption)).
% 0.21/0.58 tff(43,plain,
% 0.21/0.58 ((~![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))) | (~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))),
% 0.21/0.58 inference(quant_inst,[status(thm)],[])).
% 0.21/0.58 tff(44,plain,
% 0.21/0.58 ($false),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[43, 16, 42])).
% 0.21/0.58 tff(45,plain,(~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.58 tff(46,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) | ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(47,plain,
% 0.21/0.58 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[46, 45])).
% 0.21/0.58 tff(48,plain,
% 0.21/0.58 ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[47, 24])).
% 0.21/0.58 tff(49,plain,
% 0.21/0.58 ((~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(50,plain,
% 0.21/0.58 (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[49, 41, 48])).
% 0.21/0.58 tff(51,assumption,(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), introduced(assumption)).
% 0.21/0.58 tff(52,plain,
% 0.21/0.58 ((~![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))) | (~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(quant_inst,[status(thm)],[])).
% 0.21/0.58 tff(53,plain,
% 0.21/0.58 ($false),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[52, 16, 51])).
% 0.21/0.58 tff(54,plain,(~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.58 tff(55,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) | ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(56,plain,
% 0.21/0.58 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[55, 54])).
% 0.21/0.58 tff(57,plain,
% 0.21/0.58 ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[56, 50])).
% 0.21/0.58 tff(58,plain,
% 0.21/0.58 ((~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(59,plain,
% 0.21/0.58 (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[58, 57, 41])).
% 0.21/0.58 tff(60,assumption,(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))), introduced(assumption)).
% 0.21/0.58 tff(61,plain,
% 0.21/0.58 ((~![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))) | (~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(quant_inst,[status(thm)],[])).
% 0.21/0.58 tff(62,plain,
% 0.21/0.58 ($false),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[61, 16, 60])).
% 0.21/0.58 tff(63,plain,(~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.58 tff(64,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))) | ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(65,plain,
% 0.21/0.58 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[64, 63])).
% 0.21/0.58 tff(66,plain,
% 0.21/0.58 ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[65, 59])).
% 0.21/0.58 tff(67,plain,
% 0.21/0.58 ((~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(68,plain,
% 0.21/0.58 (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[67, 66, 41])).
% 0.21/0.58 tff(69,plain,
% 0.21/0.58 (((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(70,plain,
% 0.21/0.58 (in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[69, 39])).
% 0.21/0.58 tff(71,plain,
% 0.21/0.58 ((~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)))) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(72,plain,
% 0.21/0.58 (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[71, 41, 70])).
% 0.21/0.58 tff(73,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))) | ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(74,plain,
% 0.21/0.58 (in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[73, 72, 23])).
% 0.21/0.58 tff(75,plain,
% 0.21/0.58 ((~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))))) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(76,plain,
% 0.21/0.58 (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[75, 74, 41])).
% 0.21/0.58 tff(77,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))) | ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(78,plain,
% 0.21/0.58 (in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[77, 76, 19])).
% 0.21/0.58 tff(79,plain,
% 0.21/0.58 ((~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))))) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(80,plain,
% 0.21/0.58 (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[79, 78, 41])).
% 0.21/0.58 tff(81,assumption,(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))), introduced(assumption)).
% 0.21/0.58 tff(82,plain,
% 0.21/0.58 ((~![A: $i, C: $i] : (~(((~ordinal(C)) | (~in(C, A))) <=> in(C, tptp_fun_B_3(A))))) | (~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.58 inference(quant_inst,[status(thm)],[])).
% 0.21/0.58 tff(83,plain,
% 0.21/0.58 ($false),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[82, 16, 81])).
% 0.21/0.58 tff(84,plain,(~(((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.58 tff(85,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))) | ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(86,plain,
% 0.21/0.58 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[85, 84])).
% 0.21/0.58 tff(87,plain,
% 0.21/0.58 ($false),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[86, 80, 68])).
% 0.21/0.58 tff(88,plain,(in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.58 tff(89,plain,
% 0.21/0.58 ((~(((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | ((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(90,plain,
% 0.21/0.58 (((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[89, 36])).
% 0.21/0.58 tff(91,plain,
% 0.21/0.58 ((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[90, 88])).
% 0.21/0.58 tff(92,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) | (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(93,plain,
% 0.21/0.58 ((~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[92, 45])).
% 0.21/0.58 tff(94,plain,
% 0.21/0.58 (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[93, 88])).
% 0.21/0.58 tff(95,plain,
% 0.21/0.58 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) | ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(96,plain,
% 0.21/0.58 (ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[95, 94])).
% 0.21/0.58 tff(97,plain,
% 0.21/0.58 ((~((~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)) | (~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(98,plain,
% 0.21/0.58 (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[97, 96, 91])).
% 0.21/0.58 tff(99,plain,
% 0.21/0.58 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(100,plain,
% 0.21/0.58 ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[99, 98])).
% 0.21/0.58 tff(101,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))) | (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), A!0)))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(102,plain,
% 0.21/0.58 (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[101, 100, 23])).
% 0.21/0.58 tff(103,plain,
% 0.21/0.58 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(104,plain,
% 0.21/0.58 ((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[103, 102])).
% 0.21/0.58 tff(105,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0)))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))) | (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(A!0))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(106,plain,
% 0.21/0.58 (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[105, 104, 19])).
% 0.21/0.58 tff(107,plain,
% 0.21/0.58 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(108,plain,
% 0.21/0.58 (in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[107, 94])).
% 0.21/0.58 tff(109,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) | (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(110,plain,
% 0.21/0.58 ((~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[109, 54])).
% 0.21/0.58 tff(111,plain,
% 0.21/0.58 (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[110, 108])).
% 0.21/0.58 tff(112,plain,
% 0.21/0.58 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(113,plain,
% 0.21/0.58 (in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.58 inference(unit_resolution,[status(thm)],[112, 111])).
% 0.21/0.58 tff(114,plain,
% 0.21/0.58 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))) | (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.58 inference(tautology,[status(thm)],[])).
% 0.21/0.58 tff(115,plain,
% 0.21/0.58 ((~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.59 inference(unit_resolution,[status(thm)],[114, 63])).
% 0.21/0.59 tff(116,plain,
% 0.21/0.59 (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))),
% 0.21/0.59 inference(unit_resolution,[status(thm)],[115, 113])).
% 0.21/0.59 tff(117,plain,
% 0.21/0.59 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))),
% 0.21/0.59 inference(tautology,[status(thm)],[])).
% 0.21/0.59 tff(118,plain,
% 0.21/0.59 (in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))),
% 0.21/0.59 inference(unit_resolution,[status(thm)],[117, 116])).
% 0.21/0.59 tff(119,plain,
% 0.21/0.59 ((((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))) <=> in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))) | (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.59 inference(tautology,[status(thm)],[])).
% 0.21/0.59 tff(120,plain,
% 0.21/0.59 ((~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.59 inference(unit_resolution,[status(thm)],[119, 84])).
% 0.21/0.59 tff(121,plain,
% 0.21/0.59 (~((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))))),
% 0.21/0.59 inference(unit_resolution,[status(thm)],[120, 118])).
% 0.21/0.59 tff(122,plain,
% 0.21/0.59 (((~ordinal(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))))) | (~in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0))))) | in(tptp_fun_C_1(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(tptp_fun_B_3(A!0))))))), tptp_fun_B_3(tptp_fun_B_3(A!0)))),
% 0.21/0.59 inference(tautology,[status(thm)],[])).
% 0.21/0.59 tff(123,plain,
% 0.21/0.59 ($false),
% 0.21/0.59 inference(unit_resolution,[status(thm)],[122, 121, 106])).
% 0.21/0.59 % SZS output end Proof
% 0.21/0.59 % E exiting
%------------------------------------------------------------------------------