%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU216+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:15 AM UTC 2025
% Result : Theorem 3.08s 3.27s
% Output : Proof 3.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU216+1 : TPTP v9.0.0. Released v3.3.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n003.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 06:18:54 EDT 2025
% 0.12/0.33 % CPUTime :
% 3.08/3.27 % SZS status Theorem
% 3.08/3.27 % SZS output start Proof
% 3.08/3.27 tff(tptp_fun_C_11_type, type, (
% 3.08/3.27 tptp_fun_C_11: $i)).
% 3.08/3.27 tff(apply_type, type, (
% 3.08/3.27 apply: ( $i * $i ) > $i)).
% 3.08/3.27 tff(tptp_fun_B_9_type, type, (
% 3.08/3.27 tptp_fun_B_9: $i)).
% 3.08/3.27 tff(identity_relation_type, type, (
% 3.08/3.27 identity_relation: $i > $i)).
% 3.08/3.27 tff(tptp_fun_A_10_type, type, (
% 3.08/3.27 tptp_fun_A_10: $i)).
% 3.08/3.27 tff(in_type, type, (
% 3.08/3.27 in: ( $i * $i ) > $o)).
% 3.08/3.27 tff(relation_dom_type, type, (
% 3.08/3.27 relation_dom: $i > $i)).
% 3.08/3.27 tff(ordered_pair_type, type, (
% 3.08/3.27 ordered_pair: ( $i * $i ) > $i)).
% 3.08/3.27 tff(function_type, type, (
% 3.08/3.27 function: $i > $o)).
% 3.08/3.27 tff(tptp_fun_D_0_type, type, (
% 3.08/3.27 tptp_fun_D_0: ( $i * $i ) > $i)).
% 3.08/3.27 tff(tptp_fun_C_1_type, type, (
% 3.08/3.27 tptp_fun_C_1: ( $i * $i ) > $i)).
% 3.08/3.27 tff(relation_type, type, (
% 3.08/3.27 relation: $i > $o)).
% 3.08/3.27 tff(relation_rng_type, type, (
% 3.08/3.27 relation_rng: $i > $i)).
% 3.08/3.27 tff(1,plain,
% 3.08/3.27 (((relation(B!9) & function(B!9)) & (((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) & ((~(B!9 = identity_relation(A!10))) | (~(relation_dom(B!9) = A!10)) | (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11)))))) <=> (relation(B!9) & function(B!9) & ((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) & ((~(B!9 = identity_relation(A!10))) | (~(relation_dom(B!9) = A!10)) | (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11)))))),
% 3.08/3.27 inference(rewrite,[status(thm)],[])).
% 3.08/3.27 tff(2,plain,
% 3.08/3.27 ((((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) & ((~(B!9 = identity_relation(A!10))) | ((~(relation_dom(B!9) = A!10)) | (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11)))))) <=> (((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) & ((~(B!9 = identity_relation(A!10))) | (~(relation_dom(B!9) = A!10)) | (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11)))))),
% 3.08/3.27 inference(rewrite,[status(thm)],[])).
% 3.08/3.27 tff(3,plain,
% 3.08/3.27 (((relation(B!9) & function(B!9)) & (((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) & ((~(B!9 = identity_relation(A!10))) | ((~(relation_dom(B!9) = A!10)) | (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11))))))) <=> ((relation(B!9) & function(B!9)) & (((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) & ((~(B!9 = identity_relation(A!10))) | (~(relation_dom(B!9) = A!10)) | (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11))))))),
% 3.08/3.27 inference(monotonicity,[status(thm)],[2])).
% 3.08/3.27 tff(4,plain,
% 3.08/3.27 (((relation(B!9) & function(B!9)) & (((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) & ((~(B!9 = identity_relation(A!10))) | ((~(relation_dom(B!9) = A!10)) | (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11))))))) <=> (relation(B!9) & function(B!9) & ((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) & ((~(B!9 = identity_relation(A!10))) | (~(relation_dom(B!9) = A!10)) | (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11)))))),
% 3.08/3.27 inference(transitivity,[status(thm)],[3, 1])).
% 3.08/3.27 tff(5,plain,
% 3.08/3.27 ((~![A: $i, B: $i] : ((~(relation(B) & function(B))) | ((B = identity_relation(A)) <=> ((relation_dom(B) = A) & ![C: $i] : ((~in(C, A)) | (apply(B, C) = C)))))) <=> (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | ((B = identity_relation(A)) <=> ((relation_dom(B) = A) & ![C: $i] : ((~in(C, A)) | (apply(B, C) = C))))))),
% 3.08/3.27 inference(rewrite,[status(thm)],[])).
% 3.08/3.27 tff(6,plain,
% 3.08/3.27 ((~![A: $i, B: $i] : ((relation(B) & function(B)) => ((B = identity_relation(A)) <=> ((relation_dom(B) = A) & ![C: $i] : (in(C, A) => (apply(B, C) = C)))))) <=> (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | ((B = identity_relation(A)) <=> ((relation_dom(B) = A) & ![C: $i] : ((~in(C, A)) | (apply(B, C) = C))))))),
% 3.08/3.27 inference(rewrite,[status(thm)],[])).
% 3.08/3.27 tff(7,axiom,(~![A: $i, B: $i] : ((relation(B) & function(B)) => ((B = identity_relation(A)) <=> ((relation_dom(B) = A) & ![C: $i] : (in(C, A) => (apply(B, C) = C)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t34_funct_1')).
% 3.08/3.28 tff(8,plain,
% 3.08/3.28 (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | ((B = identity_relation(A)) <=> ((relation_dom(B) = A) & ![C: $i] : ((~in(C, A)) | (apply(B, C) = C)))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[7, 6])).
% 3.08/3.28 tff(9,plain,
% 3.08/3.28 (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | ((B = identity_relation(A)) <=> ((relation_dom(B) = A) & ![C: $i] : ((~in(C, A)) | (apply(B, C) = C)))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[8, 5])).
% 3.08/3.28 tff(10,plain,
% 3.08/3.28 (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | ((B = identity_relation(A)) <=> ((relation_dom(B) = A) & ![C: $i] : ((~in(C, A)) | (apply(B, C) = C)))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[9, 5])).
% 3.08/3.28 tff(11,plain,
% 3.08/3.28 (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | ((B = identity_relation(A)) <=> ((relation_dom(B) = A) & ![C: $i] : ((~in(C, A)) | (apply(B, C) = C)))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[10, 5])).
% 3.08/3.28 tff(12,plain,
% 3.08/3.28 (relation(B!9) & function(B!9) & ((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) & ((~(B!9 = identity_relation(A!10))) | (~(relation_dom(B!9) = A!10)) | (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[11, 4])).
% 3.08/3.28 tff(13,plain,
% 3.08/3.28 (relation(B!9)),
% 3.08/3.28 inference(and_elim,[status(thm)],[12])).
% 3.08/3.28 tff(14,plain,
% 3.08/3.28 (^[A: $i, B: $i] : rewrite(((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B))))))) <=> ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B)))))))))),
% 3.08/3.28 inference(bind,[status(th)],[])).
% 3.08/3.28 tff(15,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B))))))) <=> ![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))),
% 3.08/3.28 inference(quant_intro,[status(thm)],[14])).
% 3.08/3.28 tff(16,plain,
% 3.08/3.28 (^[A: $i, B: $i] : refl(((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B))))))) <=> ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B))))))))),
% 3.08/3.28 inference(bind,[status(th)],[])).
% 3.08/3.28 tff(17,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B))))))) <=> ![A: $i, B: $i] : ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))))))),
% 3.08/3.28 inference(quant_intro,[status(thm)],[16])).
% 3.08/3.28 tff(18,plain,
% 3.08/3.28 (^[A: $i, B: $i] : rewrite(((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B))))))) <=> ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B))))))))),
% 3.08/3.28 inference(bind,[status(th)],[])).
% 3.08/3.28 tff(19,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B))))))) <=> ![A: $i, B: $i] : ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))))))),
% 3.08/3.28 inference(quant_intro,[status(thm)],[18])).
% 3.08/3.28 tff(20,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B))))))) <=> ![A: $i, B: $i] : ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))))))),
% 3.08/3.28 inference(transitivity,[status(thm)],[19, 17])).
% 3.08/3.28 tff(21,plain,
% 3.08/3.28 (^[A: $i, B: $i] : rewrite(((~relation(B)) | (((~(B = identity_relation(A))) | ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))) & ((B = identity_relation(A)) | (~(in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B) <=> (in(tptp_fun_C_1(B, A), A) & (tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))))))) <=> ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B))))))))),
% 3.08/3.28 inference(bind,[status(th)],[])).
% 3.08/3.28 tff(22,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | (((~(B = identity_relation(A))) | ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))) & ((B = identity_relation(A)) | (~(in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B) <=> (in(tptp_fun_C_1(B, A), A) & (tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))))))) <=> ![A: $i, B: $i] : ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))))))),
% 3.08/3.28 inference(quant_intro,[status(thm)],[21])).
% 3.08/3.28 tff(23,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D))))) <=> ![A: $i, B: $i] : ((~relation(B)) | ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))))),
% 3.08/3.28 inference(rewrite,[status(thm)],[])).
% 3.08/3.28 tff(24,plain,
% 3.08/3.28 (^[A: $i, B: $i] : trans(monotonicity(rewrite(((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))) <=> ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D))))), ((relation(B) => ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D))))) <=> (relation(B) => ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D))))))), rewrite((relation(B) => ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D))))) <=> ((~relation(B)) | ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))))), ((relation(B) => ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D))))) <=> ((~relation(B)) | ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))))))),
% 3.08/3.28 inference(bind,[status(th)],[])).
% 3.08/3.28 tff(25,plain,
% 3.08/3.28 (![A: $i, B: $i] : (relation(B) => ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D))))) <=> ![A: $i, B: $i] : ((~relation(B)) | ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))))),
% 3.08/3.28 inference(quant_intro,[status(thm)],[24])).
% 3.08/3.28 tff(26,axiom,(![A: $i, B: $i] : (relation(B) => ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d10_relat_1')).
% 3.08/3.28 tff(27,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[26, 25])).
% 3.08/3.28 tff(28,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | ((B = identity_relation(A)) <=> ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[27, 23])).
% 3.08/3.28 tff(29,plain,(
% 3.08/3.28 ![A: $i, B: $i] : ((~relation(B)) | (((~(B = identity_relation(A))) | ![C: $i, D: $i] : (in(ordered_pair(C, D), B) <=> (in(C, A) & (C = D)))) & ((B = identity_relation(A)) | (~(in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B) <=> (in(tptp_fun_C_1(B, A), A) & (tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A))))))))),
% 3.08/3.28 inference(skolemize,[status(sab)],[28])).
% 3.08/3.28 tff(30,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[29, 22])).
% 3.08/3.28 tff(31,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | (~((~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))) | (~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[30, 20])).
% 3.08/3.28 tff(32,plain,
% 3.08/3.28 (![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[31, 15])).
% 3.08/3.28 tff(33,plain,
% 3.08/3.28 (((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | ((~relation(B!9)) | (~((~((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9))))))))) <=> ((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | (~relation(B!9)) | (~((~((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9))))))))),
% 3.08/3.28 inference(rewrite,[status(thm)],[])).
% 3.08/3.28 tff(34,plain,
% 3.08/3.28 (((~relation(B!9)) | (~((~((B!9 = identity_relation(A!10)) | (((~in(tptp_fun_C_1(B!9, A!10), A!10)) | (~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10)))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9)))))))) <=> ((~relation(B!9)) | (~((~((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9))))))))),
% 3.08/3.28 inference(rewrite,[status(thm)],[])).
% 3.08/3.28 tff(35,plain,
% 3.08/3.28 (((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | ((~relation(B!9)) | (~((~((B!9 = identity_relation(A!10)) | (((~in(tptp_fun_C_1(B!9, A!10), A!10)) | (~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10)))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9))))))))) <=> ((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | ((~relation(B!9)) | (~((~((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9)))))))))),
% 3.08/3.28 inference(monotonicity,[status(thm)],[34])).
% 3.08/3.28 tff(36,plain,
% 3.08/3.28 (((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | ((~relation(B!9)) | (~((~((B!9 = identity_relation(A!10)) | (((~in(tptp_fun_C_1(B!9, A!10), A!10)) | (~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10)))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9))))))))) <=> ((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | (~relation(B!9)) | (~((~((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9))))))))),
% 3.08/3.28 inference(transitivity,[status(thm)],[35, 33])).
% 3.08/3.28 tff(37,plain,
% 3.08/3.28 ((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | ((~relation(B!9)) | (~((~((B!9 = identity_relation(A!10)) | (((~in(tptp_fun_C_1(B!9, A!10), A!10)) | (~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10)))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9))))))))),
% 3.08/3.28 inference(quant_inst,[status(thm)],[])).
% 3.08/3.28 tff(38,plain,
% 3.08/3.28 ((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | (~relation(B!9)) | (~((~((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9)))))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[37, 36])).
% 3.08/3.28 tff(39,plain,
% 3.08/3.28 (~((~((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9))))))),
% 3.08/3.28 inference(unit_resolution,[status(thm)],[38, 32, 13])).
% 3.08/3.28 tff(40,plain,
% 3.08/3.28 (((~((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (~((~(B!9 = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), B!9)))))) | ((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))),
% 3.08/3.28 inference(tautology,[status(thm)],[])).
% 3.08/3.28 tff(41,plain,
% 3.08/3.28 ((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))),
% 3.08/3.28 inference(unit_resolution,[status(thm)],[40, 39])).
% 3.08/3.28 tff(42,assumption,(~(B!9 = identity_relation(A!10))), introduced(assumption)).
% 3.08/3.28 tff(43,plain,
% 3.08/3.28 ((~((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))),
% 3.08/3.28 inference(tautology,[status(thm)],[])).
% 3.08/3.28 tff(44,plain,
% 3.08/3.28 ((~((B!9 = identity_relation(A!10)) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) | (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))),
% 3.08/3.28 inference(unit_resolution,[status(thm)],[43, 42])).
% 3.08/3.28 tff(45,plain,
% 3.08/3.28 (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)),
% 3.08/3.28 inference(unit_resolution,[status(thm)],[44, 41])).
% 3.08/3.28 tff(46,plain,
% 3.08/3.28 (((B!9 = identity_relation(A!10)) | (~((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))))) <=> ((B!9 = identity_relation(A!10)) | (~((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))))))),
% 3.08/3.28 inference(rewrite,[status(thm)],[])).
% 3.08/3.28 tff(47,plain,
% 3.08/3.28 (((B!9 = identity_relation(A!10)) | (~((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))))) <=> ((B!9 = identity_relation(A!10)) | (~((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))))))),
% 3.08/3.28 inference(rewrite,[status(thm)],[])).
% 3.08/3.28 tff(48,plain,
% 3.08/3.28 (((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))) <=> (~((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))))),
% 3.08/3.28 inference(rewrite,[status(thm)],[])).
% 3.08/3.28 tff(49,plain,
% 3.08/3.28 (((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) <=> ((B!9 = identity_relation(A!10)) | (~((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))))))),
% 3.08/3.28 inference(monotonicity,[status(thm)],[48])).
% 3.08/3.28 tff(50,plain,
% 3.08/3.28 (((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) <=> ((B!9 = identity_relation(A!10)) | (~((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))))))),
% 3.08/3.28 inference(transitivity,[status(thm)],[49, 47])).
% 3.08/3.28 tff(51,plain,
% 3.08/3.28 ((B!9 = identity_relation(A!10)) | ((relation_dom(B!9) = A!10) & ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))),
% 3.08/3.28 inference(and_elim,[status(thm)],[12])).
% 3.08/3.28 tff(52,plain,
% 3.08/3.28 ((B!9 = identity_relation(A!10)) | (~((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[51, 50])).
% 3.08/3.28 tff(53,plain,
% 3.08/3.28 ((B!9 = identity_relation(A!10)) | (~((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[52, 46])).
% 3.08/3.28 tff(54,plain,
% 3.08/3.28 (~((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))))),
% 3.08/3.28 inference(unit_resolution,[status(thm)],[53, 42])).
% 3.08/3.28 tff(55,plain,
% 3.08/3.28 (((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) | (relation_dom(B!9) = A!10)),
% 3.08/3.28 inference(tautology,[status(thm)],[])).
% 3.08/3.28 tff(56,plain,
% 3.08/3.28 (relation_dom(B!9) = A!10),
% 3.08/3.28 inference(unit_resolution,[status(thm)],[55, 54])).
% 3.08/3.28 tff(57,plain,
% 3.08/3.28 (((~(relation_dom(B!9) = A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C)))) | ![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))),
% 3.08/3.28 inference(tautology,[status(thm)],[])).
% 3.08/3.28 tff(58,plain,
% 3.08/3.28 (![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))),
% 3.08/3.28 inference(unit_resolution,[status(thm)],[57, 54])).
% 3.08/3.28 tff(59,plain,
% 3.08/3.28 (^[A: $i, B: $i, C: $i] : refl(((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))) <=> ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))))),
% 3.08/3.28 inference(bind,[status(th)],[])).
% 3.08/3.28 tff(60,plain,
% 3.08/3.28 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))) <=> ![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))),
% 3.08/3.28 inference(quant_intro,[status(thm)],[59])).
% 3.08/3.28 tff(61,plain,
% 3.08/3.28 (^[A: $i, B: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((relation(C) & function(C)) <=> (~((~relation(C)) | (~function(C))))), ((~(relation(C) & function(C))) <=> (~(~((~relation(C)) | (~function(C))))))), rewrite((~(~((~relation(C)) | (~function(C))))) <=> ((~relation(C)) | (~function(C)))), ((~(relation(C) & function(C))) <=> ((~relation(C)) | (~function(C))))), trans(trans(monotonicity(rewrite((in(A, relation_dom(C)) & (B = apply(C, A))) <=> (~((~in(A, relation_dom(C))) | (~(B = apply(C, A)))))), ((in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))) <=> (in(ordered_pair(A, B), C) <=> (~((~in(A, relation_dom(C))) | (~(B = apply(C, A)))))))), rewrite((in(ordered_pair(A, B), C) <=> (~((~in(A, relation_dom(C))) | (~(B = apply(C, A)))))) <=> (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))), ((in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))) <=> (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))), rewrite((~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))) <=> (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))), ((in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))) <=> (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))), (((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> (((~relation(C)) | (~function(C))) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))))), rewrite((((~relation(C)) | (~function(C))) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))) <=> ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))), (((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))))),
% 3.08/3.28 inference(bind,[status(th)],[])).
% 3.08/3.28 tff(62,plain,
% 3.08/3.28 (![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> ![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))),
% 3.08/3.28 inference(quant_intro,[status(thm)],[61])).
% 3.08/3.28 tff(63,plain,
% 3.08/3.28 (![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> ![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))),
% 3.08/3.28 inference(rewrite,[status(thm)],[])).
% 3.08/3.28 tff(64,plain,
% 3.08/3.28 (^[A: $i, B: $i, C: $i] : rewrite(((relation(C) & function(C)) => (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))))),
% 3.08/3.28 inference(bind,[status(th)],[])).
% 3.08/3.28 tff(65,plain,
% 3.08/3.28 (![A: $i, B: $i, C: $i] : ((relation(C) & function(C)) => (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> ![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))),
% 3.08/3.28 inference(quant_intro,[status(thm)],[64])).
% 3.08/3.28 tff(66,axiom,(![A: $i, B: $i, C: $i] : ((relation(C) & function(C)) => (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t8_funct_1')).
% 3.08/3.28 tff(67,plain,
% 3.08/3.28 (![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[66, 65])).
% 3.08/3.28 tff(68,plain,
% 3.08/3.28 (![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[67, 63])).
% 3.08/3.28 tff(69,plain,(
% 3.08/3.28 ![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))),
% 3.08/3.28 inference(skolemize,[status(sab)],[68])).
% 3.08/3.28 tff(70,plain,
% 3.08/3.28 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[69, 62])).
% 3.08/3.28 tff(71,plain,
% 3.08/3.28 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[70, 60])).
% 3.08/3.28 tff(72,plain,
% 3.08/3.28 (function(B!9)),
% 3.08/3.28 inference(and_elim,[status(thm)],[12])).
% 3.08/3.28 tff(73,plain,
% 3.08/3.28 (((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | ((~function(B!9)) | (~relation(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))))) <=> ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | (~function(B!9)) | (~relation(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))))),
% 3.08/3.28 inference(rewrite,[status(thm)],[])).
% 3.08/3.28 tff(74,plain,
% 3.08/3.28 (((~relation(B!9)) | (~function(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) <=> ((~function(B!9)) | (~relation(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))))),
% 3.08/3.28 inference(rewrite,[status(thm)],[])).
% 3.08/3.28 tff(75,plain,
% 3.08/3.28 ((~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))) <=> (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))),
% 3.08/3.28 inference(rewrite,[status(thm)],[])).
% 3.08/3.28 tff(76,plain,
% 3.08/3.28 (((~relation(B!9)) | (~function(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) <=> ((~relation(B!9)) | (~function(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))))),
% 3.08/3.28 inference(monotonicity,[status(thm)],[75])).
% 3.08/3.28 tff(77,plain,
% 3.08/3.28 (((~relation(B!9)) | (~function(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))) <=> ((~function(B!9)) | (~relation(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))))),
% 3.08/3.28 inference(transitivity,[status(thm)],[76, 74])).
% 3.08/3.28 tff(78,plain,
% 3.08/3.28 (((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | ((~relation(B!9)) | (~function(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))))) <=> ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | ((~function(B!9)) | (~relation(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))))),
% 3.08/3.28 inference(monotonicity,[status(thm)],[77])).
% 3.08/3.28 tff(79,plain,
% 3.08/3.28 (((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | ((~relation(B!9)) | (~function(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))))) <=> ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | (~function(B!9)) | (~relation(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))))),
% 3.08/3.28 inference(transitivity,[status(thm)],[78, 73])).
% 3.08/3.28 tff(80,plain,
% 3.08/3.28 ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | ((~relation(B!9)) | (~function(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))))),
% 3.08/3.28 inference(quant_inst,[status(thm)],[])).
% 3.08/3.28 tff(81,plain,
% 3.08/3.28 ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | (~function(B!9)) | (~relation(B!9)) | (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))),
% 3.08/3.28 inference(modus_ponens,[status(thm)],[80, 79])).
% 3.08/3.28 tff(82,plain,
% 3.08/3.28 (~(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))),
% 3.08/3.28 inference(unit_resolution,[status(thm)],[81, 13, 72, 71])).
% 3.08/3.28 tff(83,assumption,(((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)), introduced(assumption)).
% 3.08/3.28 tff(84,assumption,(~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))), introduced(assumption)).
% 3.08/3.28 tff(85,plain,
% 3.08/3.28 (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) | (tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))),
% 3.08/3.28 inference(tautology,[status(thm)],[])).
% 3.08/3.28 tff(86,plain,
% 3.08/3.28 ((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))),
% 3.08/3.28 inference(unit_resolution,[status(thm)],[85, 84])).
% 3.08/3.28 tff(87,plain,
% 3.08/3.29 ((~(((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))) | (~((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10)))) | in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)),
% 3.08/3.29 inference(tautology,[status(thm)],[])).
% 3.08/3.29 tff(88,plain,
% 3.08/3.29 (in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[87, 86, 83])).
% 3.08/3.29 tff(89,plain,
% 3.08/3.29 ((((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)) | (~((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10)))))) | (~in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))),
% 3.08/3.29 inference(tautology,[status(thm)],[])).
% 3.08/3.29 tff(90,plain,
% 3.08/3.29 (~((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10)))))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[89, 88, 82])).
% 3.08/3.29 tff(91,plain,
% 3.08/3.29 (((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) | (tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10)))),
% 3.08/3.29 inference(tautology,[status(thm)],[])).
% 3.08/3.29 tff(92,plain,
% 3.08/3.29 (tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[91, 90])).
% 3.08/3.29 tff(93,plain,
% 3.08/3.29 (apply(B!9, tptp_fun_C_1(B!9, A!10)) = tptp_fun_D_0(B!9, A!10)),
% 3.08/3.29 inference(symmetry,[status(thm)],[92])).
% 3.08/3.29 tff(94,assumption,(relation_dom(B!9) = A!10), introduced(assumption)).
% 3.08/3.29 tff(95,plain,
% 3.08/3.29 (in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9)) <=> in(tptp_fun_C_1(B!9, A!10), A!10)),
% 3.08/3.29 inference(monotonicity,[status(thm)],[94])).
% 3.08/3.29 tff(96,plain,
% 3.08/3.29 (((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) | in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))),
% 3.08/3.29 inference(tautology,[status(thm)],[])).
% 3.08/3.29 tff(97,plain,
% 3.08/3.29 (in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[96, 90])).
% 3.08/3.29 tff(98,plain,
% 3.08/3.29 (in(tptp_fun_C_1(B!9, A!10), A!10)),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[97, 95])).
% 3.08/3.29 tff(99,assumption,(![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))), introduced(assumption)).
% 3.08/3.29 tff(100,plain,
% 3.08/3.29 (((~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))) | ((~in(tptp_fun_C_1(B!9, A!10), A!10)) | (apply(B!9, tptp_fun_C_1(B!9, A!10)) = tptp_fun_C_1(B!9, A!10)))) <=> ((~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))) | (~in(tptp_fun_C_1(B!9, A!10), A!10)) | (apply(B!9, tptp_fun_C_1(B!9, A!10)) = tptp_fun_C_1(B!9, A!10)))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(101,plain,
% 3.08/3.29 ((~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))) | ((~in(tptp_fun_C_1(B!9, A!10), A!10)) | (apply(B!9, tptp_fun_C_1(B!9, A!10)) = tptp_fun_C_1(B!9, A!10)))),
% 3.08/3.29 inference(quant_inst,[status(thm)],[])).
% 3.08/3.29 tff(102,plain,
% 3.08/3.29 ((~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))) | (~in(tptp_fun_C_1(B!9, A!10), A!10)) | (apply(B!9, tptp_fun_C_1(B!9, A!10)) = tptp_fun_C_1(B!9, A!10))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[101, 100])).
% 3.08/3.29 tff(103,plain,
% 3.08/3.29 (apply(B!9, tptp_fun_C_1(B!9, A!10)) = tptp_fun_C_1(B!9, A!10)),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[102, 99, 98])).
% 3.08/3.29 tff(104,plain,
% 3.08/3.29 (tptp_fun_C_1(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))),
% 3.08/3.29 inference(symmetry,[status(thm)],[103])).
% 3.08/3.29 tff(105,plain,
% 3.08/3.29 (tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10)),
% 3.08/3.29 inference(transitivity,[status(thm)],[104, 93])).
% 3.08/3.29 tff(106,plain,
% 3.08/3.29 ($false),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[84, 105])).
% 3.08/3.29 tff(107,plain,((tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10)) | (~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))) | (~(relation_dom(B!9) = A!10)) | (~(((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))), inference(lemma,lemma(discharge,[]))).
% 3.08/3.29 tff(108,plain,
% 3.08/3.29 (tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10)),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[107, 58, 56, 45])).
% 3.08/3.29 tff(109,plain,
% 3.08/3.29 (tptp_fun_D_0(B!9, A!10) = tptp_fun_C_1(B!9, A!10)),
% 3.08/3.29 inference(symmetry,[status(thm)],[108])).
% 3.08/3.29 tff(110,plain,
% 3.08/3.29 (in(tptp_fun_D_0(B!9, A!10), A!10) <=> in(tptp_fun_C_1(B!9, A!10), A!10)),
% 3.08/3.29 inference(monotonicity,[status(thm)],[109])).
% 3.08/3.29 tff(111,plain,
% 3.08/3.29 (in(tptp_fun_C_1(B!9, A!10), A!10) <=> in(tptp_fun_D_0(B!9, A!10), A!10)),
% 3.08/3.29 inference(symmetry,[status(thm)],[110])).
% 3.08/3.29 tff(112,assumption,(~((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10)))))), introduced(assumption)).
% 3.08/3.29 tff(113,plain,
% 3.08/3.29 (in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[96, 112])).
% 3.08/3.29 tff(114,plain,
% 3.08/3.29 (in(tptp_fun_C_1(B!9, A!10), A!10)),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[113, 95])).
% 3.08/3.29 tff(115,assumption,(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10)), introduced(assumption)).
% 3.08/3.29 tff(116,plain,
% 3.08/3.29 ((((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)) | ((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) | in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)),
% 3.08/3.29 inference(tautology,[status(thm)],[])).
% 3.08/3.29 tff(117,plain,
% 3.08/3.29 (in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[116, 112, 82])).
% 3.08/3.29 tff(118,plain,
% 3.08/3.29 ((~(((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))) | ((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) | (~in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9))),
% 3.08/3.29 inference(tautology,[status(thm)],[])).
% 3.08/3.29 tff(119,plain,
% 3.08/3.29 ((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[118, 117, 83])).
% 3.08/3.29 tff(120,plain,
% 3.08/3.29 ((~((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10)))) | (~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))),
% 3.08/3.29 inference(tautology,[status(thm)],[])).
% 3.08/3.29 tff(121,plain,
% 3.08/3.29 (~in(tptp_fun_C_1(B!9, A!10), A!10)),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[120, 119, 115])).
% 3.08/3.29 tff(122,plain,
% 3.08/3.29 ($false),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[121, 114])).
% 3.08/3.29 tff(123,plain,(((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))) | (~(relation_dom(B!9) = A!10)) | (~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~(((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) <=> in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)))), inference(lemma,lemma(discharge,[]))).
% 3.08/3.29 tff(124,plain,
% 3.08/3.29 ((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[123, 56, 108, 45])).
% 3.08/3.29 tff(125,plain,
% 3.08/3.29 (~in(ordered_pair(tptp_fun_C_1(B!9, A!10), tptp_fun_D_0(B!9, A!10)), B!9)),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[89, 124, 82])).
% 3.08/3.29 tff(126,plain,
% 3.08/3.29 (~((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10)))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[87, 125, 45])).
% 3.08/3.29 tff(127,plain,
% 3.08/3.29 (((~(tptp_fun_C_1(B!9, A!10) = tptp_fun_D_0(B!9, A!10))) | (~in(tptp_fun_C_1(B!9, A!10), A!10))) | in(tptp_fun_C_1(B!9, A!10), A!10)),
% 3.08/3.29 inference(tautology,[status(thm)],[])).
% 3.08/3.29 tff(128,plain,
% 3.08/3.29 (in(tptp_fun_C_1(B!9, A!10), A!10)),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[127, 126])).
% 3.08/3.29 tff(129,plain,
% 3.08/3.29 (in(tptp_fun_D_0(B!9, A!10), A!10)),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[128, 111])).
% 3.08/3.29 tff(130,plain,
% 3.08/3.29 ((apply(B!9, tptp_fun_C_1(B!9, A!10)) = tptp_fun_D_0(B!9, A!10)) <=> (tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10)))),
% 3.08/3.29 inference(commutativity,[status(thm)],[])).
% 3.08/3.29 tff(131,plain,
% 3.08/3.29 (apply(B!9, tptp_fun_D_0(B!9, A!10)) = apply(B!9, tptp_fun_C_1(B!9, A!10))),
% 3.08/3.29 inference(monotonicity,[status(thm)],[109])).
% 3.08/3.29 tff(132,plain,
% 3.08/3.29 ((apply(B!9, tptp_fun_D_0(B!9, A!10)) = tptp_fun_D_0(B!9, A!10)) <=> (apply(B!9, tptp_fun_C_1(B!9, A!10)) = tptp_fun_D_0(B!9, A!10))),
% 3.08/3.29 inference(monotonicity,[status(thm)],[131])).
% 3.08/3.29 tff(133,plain,
% 3.08/3.29 ((apply(B!9, tptp_fun_D_0(B!9, A!10)) = tptp_fun_D_0(B!9, A!10)) <=> (tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10)))),
% 3.08/3.29 inference(transitivity,[status(thm)],[132, 130])).
% 3.08/3.29 tff(134,plain,
% 3.08/3.29 ((tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))) <=> (apply(B!9, tptp_fun_D_0(B!9, A!10)) = tptp_fun_D_0(B!9, A!10))),
% 3.08/3.29 inference(symmetry,[status(thm)],[133])).
% 3.08/3.29 tff(135,plain,
% 3.08/3.29 ((~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10)))) <=> (~(apply(B!9, tptp_fun_D_0(B!9, A!10)) = tptp_fun_D_0(B!9, A!10)))),
% 3.08/3.29 inference(monotonicity,[status(thm)],[134])).
% 3.08/3.29 tff(136,plain,
% 3.08/3.29 (in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9)) <=> in(tptp_fun_C_1(B!9, A!10), A!10)),
% 3.08/3.29 inference(monotonicity,[status(thm)],[56])).
% 3.08/3.29 tff(137,plain,
% 3.08/3.29 (in(tptp_fun_C_1(B!9, A!10), A!10) <=> in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))),
% 3.08/3.29 inference(symmetry,[status(thm)],[136])).
% 3.08/3.29 tff(138,plain,
% 3.08/3.29 (in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[128, 137])).
% 3.08/3.29 tff(139,plain,
% 3.08/3.29 ((~((~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10)))))) | (~in(tptp_fun_C_1(B!9, A!10), relation_dom(B!9))) | (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10))))),
% 3.08/3.29 inference(tautology,[status(thm)],[])).
% 3.08/3.29 tff(140,plain,
% 3.08/3.29 (~(tptp_fun_D_0(B!9, A!10) = apply(B!9, tptp_fun_C_1(B!9, A!10)))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[139, 138, 124])).
% 3.08/3.29 tff(141,plain,
% 3.08/3.29 (~(apply(B!9, tptp_fun_D_0(B!9, A!10)) = tptp_fun_D_0(B!9, A!10))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[140, 135])).
% 3.08/3.29 tff(142,plain,
% 3.08/3.29 (((~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))) | ((~in(tptp_fun_D_0(B!9, A!10), A!10)) | (apply(B!9, tptp_fun_D_0(B!9, A!10)) = tptp_fun_D_0(B!9, A!10)))) <=> ((~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))) | (~in(tptp_fun_D_0(B!9, A!10), A!10)) | (apply(B!9, tptp_fun_D_0(B!9, A!10)) = tptp_fun_D_0(B!9, A!10)))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(143,plain,
% 3.08/3.29 ((~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))) | ((~in(tptp_fun_D_0(B!9, A!10), A!10)) | (apply(B!9, tptp_fun_D_0(B!9, A!10)) = tptp_fun_D_0(B!9, A!10)))),
% 3.08/3.29 inference(quant_inst,[status(thm)],[])).
% 3.08/3.29 tff(144,plain,
% 3.08/3.29 ((~![C: $i] : ((~in(C, A!10)) | (apply(B!9, C) = C))) | (~in(tptp_fun_D_0(B!9, A!10), A!10)) | (apply(B!9, tptp_fun_D_0(B!9, A!10)) = tptp_fun_D_0(B!9, A!10))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[143, 142])).
% 3.08/3.29 tff(145,plain,
% 3.08/3.29 ((~in(tptp_fun_D_0(B!9, A!10), A!10)) | (apply(B!9, tptp_fun_D_0(B!9, A!10)) = tptp_fun_D_0(B!9, A!10))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[144, 58])).
% 3.08/3.29 tff(146,plain,
% 3.08/3.29 ($false),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[145, 141, 129])).
% 3.08/3.29 tff(147,plain,(B!9 = identity_relation(A!10)), inference(lemma,lemma(discharge,[]))).
% 3.08/3.29 tff(148,plain,
% 3.08/3.29 (identity_relation(A!10) = B!9),
% 3.08/3.29 inference(symmetry,[status(thm)],[147])).
% 3.08/3.29 tff(149,plain,
% 3.08/3.29 (function(identity_relation(A!10)) <=> function(B!9)),
% 3.08/3.29 inference(monotonicity,[status(thm)],[148])).
% 3.08/3.29 tff(150,plain,
% 3.08/3.29 (function(B!9) <=> function(identity_relation(A!10))),
% 3.08/3.29 inference(symmetry,[status(thm)],[149])).
% 3.08/3.29 tff(151,plain,
% 3.08/3.29 (function(identity_relation(A!10))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[72, 150])).
% 3.08/3.29 tff(152,plain,
% 3.08/3.29 (relation(identity_relation(A!10)) <=> relation(B!9)),
% 3.08/3.29 inference(monotonicity,[status(thm)],[148])).
% 3.08/3.29 tff(153,plain,
% 3.08/3.29 (relation(B!9) <=> relation(identity_relation(A!10))),
% 3.08/3.29 inference(symmetry,[status(thm)],[152])).
% 3.08/3.29 tff(154,plain,
% 3.08/3.29 (relation(identity_relation(A!10))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[13, 153])).
% 3.08/3.29 tff(155,plain,
% 3.08/3.29 (((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | ((~relation(identity_relation(A!10))) | (~function(identity_relation(A!10))) | (~(((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11)))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))))) <=> ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | (~relation(identity_relation(A!10))) | (~function(identity_relation(A!10))) | (~(((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11)))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(156,plain,
% 3.08/3.29 ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | ((~relation(identity_relation(A!10))) | (~function(identity_relation(A!10))) | (~(((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11)))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))))),
% 3.08/3.29 inference(quant_inst,[status(thm)],[])).
% 3.08/3.29 tff(157,plain,
% 3.08/3.29 ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | (~relation(identity_relation(A!10))) | (~function(identity_relation(A!10))) | (~(((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11)))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[156, 155])).
% 3.08/3.29 tff(158,plain,
% 3.08/3.29 (~(((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11)))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[157, 71, 154, 151])).
% 3.08/3.29 tff(159,plain,
% 3.08/3.29 (((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | ((~relation(identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10)))))) <=> ((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | (~relation(identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10)))))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(160,plain,
% 3.08/3.29 (((~relation(identity_relation(A!10))) | (~((~((identity_relation(A!10) = identity_relation(A!10)) | (((~in(tptp_fun_C_1(identity_relation(A!10), A!10), A!10)) | (~(tptp_fun_C_1(identity_relation(A!10), A!10) = tptp_fun_D_0(identity_relation(A!10), A!10)))) <=> in(ordered_pair(tptp_fun_C_1(identity_relation(A!10), A!10), tptp_fun_D_0(identity_relation(A!10), A!10)), identity_relation(A!10))))) | (~((~(identity_relation(A!10) = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))))))) <=> ((~relation(identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10)))))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(161,plain,
% 3.08/3.29 (((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | ((~relation(identity_relation(A!10))) | (~((~((identity_relation(A!10) = identity_relation(A!10)) | (((~in(tptp_fun_C_1(identity_relation(A!10), A!10), A!10)) | (~(tptp_fun_C_1(identity_relation(A!10), A!10) = tptp_fun_D_0(identity_relation(A!10), A!10)))) <=> in(ordered_pair(tptp_fun_C_1(identity_relation(A!10), A!10), tptp_fun_D_0(identity_relation(A!10), A!10)), identity_relation(A!10))))) | (~((~(identity_relation(A!10) = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10)))))))))) <=> ((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | ((~relation(identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))))),
% 3.08/3.29 inference(monotonicity,[status(thm)],[160])).
% 3.08/3.29 tff(162,plain,
% 3.08/3.29 (((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | ((~relation(identity_relation(A!10))) | (~((~((identity_relation(A!10) = identity_relation(A!10)) | (((~in(tptp_fun_C_1(identity_relation(A!10), A!10), A!10)) | (~(tptp_fun_C_1(identity_relation(A!10), A!10) = tptp_fun_D_0(identity_relation(A!10), A!10)))) <=> in(ordered_pair(tptp_fun_C_1(identity_relation(A!10), A!10), tptp_fun_D_0(identity_relation(A!10), A!10)), identity_relation(A!10))))) | (~((~(identity_relation(A!10) = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10)))))))))) <=> ((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | (~relation(identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10)))))),
% 3.08/3.29 inference(transitivity,[status(thm)],[161, 159])).
% 3.08/3.29 tff(163,plain,
% 3.08/3.29 ((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | ((~relation(identity_relation(A!10))) | (~((~((identity_relation(A!10) = identity_relation(A!10)) | (((~in(tptp_fun_C_1(identity_relation(A!10), A!10), A!10)) | (~(tptp_fun_C_1(identity_relation(A!10), A!10) = tptp_fun_D_0(identity_relation(A!10), A!10)))) <=> in(ordered_pair(tptp_fun_C_1(identity_relation(A!10), A!10), tptp_fun_D_0(identity_relation(A!10), A!10)), identity_relation(A!10))))) | (~((~(identity_relation(A!10) = identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10)))))))))),
% 3.08/3.29 inference(quant_inst,[status(thm)],[])).
% 3.08/3.29 tff(164,plain,
% 3.08/3.29 ((~![A: $i, B: $i] : ((~relation(B)) | (~((~((B = identity_relation(A)) | (((~in(tptp_fun_C_1(B, A), A)) | (~(tptp_fun_C_1(B, A) = tptp_fun_D_0(B, A)))) <=> in(ordered_pair(tptp_fun_C_1(B, A), tptp_fun_D_0(B, A)), B)))) | (~((~(B = identity_relation(A))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A))) <=> in(ordered_pair(C, D), B))))))))) | (~relation(identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[163, 162])).
% 3.08/3.29 tff(165,plain,
% 3.08/3.29 ((~relation(identity_relation(A!10))) | ![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[164, 32])).
% 3.08/3.29 tff(166,plain,
% 3.08/3.29 (![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[165, 154])).
% 3.08/3.29 tff(167,plain,
% 3.08/3.29 (((~![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))) | (in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))) <=> ((~![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))) | (in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(168,plain,
% 3.08/3.29 ((~(~(in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))) <=> (in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(169,plain,
% 3.08/3.29 ((~(in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))) <=> (~(in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(170,plain,
% 3.08/3.29 (((~in(C!11, A!10)) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))) <=> (~(in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(171,plain,
% 3.08/3.29 (($false | (~in(C!11, A!10))) <=> (~in(C!11, A!10))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(172,plain,
% 3.08/3.29 ((~$true) <=> $false),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(173,plain,
% 3.08/3.29 ((C!11 = C!11) <=> $true),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(174,plain,
% 3.08/3.29 ((~(C!11 = C!11)) <=> (~$true)),
% 3.08/3.29 inference(monotonicity,[status(thm)],[173])).
% 3.08/3.29 tff(175,plain,
% 3.08/3.29 ((~(C!11 = C!11)) <=> $false),
% 3.08/3.29 inference(transitivity,[status(thm)],[174, 172])).
% 3.08/3.29 tff(176,plain,
% 3.08/3.29 (((~(C!11 = C!11)) | (~in(C!11, A!10))) <=> ($false | (~in(C!11, A!10)))),
% 3.08/3.29 inference(monotonicity,[status(thm)],[175])).
% 3.08/3.29 tff(177,plain,
% 3.08/3.29 (((~(C!11 = C!11)) | (~in(C!11, A!10))) <=> (~in(C!11, A!10))),
% 3.08/3.29 inference(transitivity,[status(thm)],[176, 171])).
% 3.08/3.29 tff(178,plain,
% 3.08/3.29 ((((~(C!11 = C!11)) | (~in(C!11, A!10))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))) <=> ((~in(C!11, A!10)) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))),
% 3.08/3.29 inference(monotonicity,[status(thm)],[177])).
% 3.08/3.29 tff(179,plain,
% 3.08/3.29 ((((~(C!11 = C!11)) | (~in(C!11, A!10))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))) <=> (~(in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))),
% 3.08/3.29 inference(transitivity,[status(thm)],[178, 170])).
% 3.08/3.29 tff(180,plain,
% 3.08/3.29 ((((~(C!11 = C!11)) | (~in(C!11, A!10))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))) <=> (~(in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))),
% 3.08/3.29 inference(transitivity,[status(thm)],[179, 169])).
% 3.08/3.29 tff(181,plain,
% 3.08/3.29 ((~(((~(C!11 = C!11)) | (~in(C!11, A!10))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))) <=> (~(~(in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))))),
% 3.08/3.29 inference(monotonicity,[status(thm)],[180])).
% 3.08/3.29 tff(182,plain,
% 3.08/3.29 ((~(((~(C!11 = C!11)) | (~in(C!11, A!10))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))) <=> (in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))),
% 3.08/3.29 inference(transitivity,[status(thm)],[181, 168])).
% 3.08/3.29 tff(183,plain,
% 3.08/3.29 (((~![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))) | (~(((~(C!11 = C!11)) | (~in(C!11, A!10))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))) <=> ((~![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))) | (in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))),
% 3.08/3.29 inference(monotonicity,[status(thm)],[182])).
% 3.08/3.29 tff(184,plain,
% 3.08/3.29 (((~![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))) | (~(((~(C!11 = C!11)) | (~in(C!11, A!10))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))) <=> ((~![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))) | (in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))),
% 3.08/3.29 inference(transitivity,[status(thm)],[183, 167])).
% 3.08/3.29 tff(185,plain,
% 3.08/3.29 ((~![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))) | (~(((~(C!11 = C!11)) | (~in(C!11, A!10))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))))),
% 3.08/3.29 inference(quant_inst,[status(thm)],[])).
% 3.08/3.29 tff(186,plain,
% 3.08/3.29 ((~![C: $i, D: $i] : (~(((~(C = D)) | (~in(C, A!10))) <=> in(ordered_pair(C, D), identity_relation(A!10))))) | (in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[185, 184])).
% 3.08/3.29 tff(187,plain,
% 3.08/3.29 (in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[186, 166])).
% 3.08/3.29 tff(188,plain,
% 3.08/3.29 (^[A: $i] : refl((~((~(relation_dom(identity_relation(A)) = A)) | (~(relation_rng(identity_relation(A)) = A)))) <=> (~((~(relation_dom(identity_relation(A)) = A)) | (~(relation_rng(identity_relation(A)) = A)))))),
% 3.08/3.29 inference(bind,[status(th)],[])).
% 3.08/3.29 tff(189,plain,
% 3.08/3.29 (![A: $i] : (~((~(relation_dom(identity_relation(A)) = A)) | (~(relation_rng(identity_relation(A)) = A)))) <=> ![A: $i] : (~((~(relation_dom(identity_relation(A)) = A)) | (~(relation_rng(identity_relation(A)) = A))))),
% 3.08/3.29 inference(quant_intro,[status(thm)],[188])).
% 3.08/3.29 tff(190,plain,
% 3.08/3.29 (^[A: $i] : rewrite(((relation_dom(identity_relation(A)) = A) & (relation_rng(identity_relation(A)) = A)) <=> (~((~(relation_dom(identity_relation(A)) = A)) | (~(relation_rng(identity_relation(A)) = A)))))),
% 3.08/3.29 inference(bind,[status(th)],[])).
% 3.08/3.29 tff(191,plain,
% 3.08/3.29 (![A: $i] : ((relation_dom(identity_relation(A)) = A) & (relation_rng(identity_relation(A)) = A)) <=> ![A: $i] : (~((~(relation_dom(identity_relation(A)) = A)) | (~(relation_rng(identity_relation(A)) = A))))),
% 3.08/3.29 inference(quant_intro,[status(thm)],[190])).
% 3.08/3.29 tff(192,plain,
% 3.08/3.29 (![A: $i] : ((relation_dom(identity_relation(A)) = A) & (relation_rng(identity_relation(A)) = A)) <=> ![A: $i] : ((relation_dom(identity_relation(A)) = A) & (relation_rng(identity_relation(A)) = A))),
% 3.08/3.29 inference(rewrite,[status(thm)],[])).
% 3.08/3.29 tff(193,axiom,(![A: $i] : ((relation_dom(identity_relation(A)) = A) & (relation_rng(identity_relation(A)) = A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t71_relat_1')).
% 3.08/3.29 tff(194,plain,
% 3.08/3.29 (![A: $i] : ((relation_dom(identity_relation(A)) = A) & (relation_rng(identity_relation(A)) = A))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[193, 192])).
% 3.08/3.29 tff(195,plain,(
% 3.08/3.29 ![A: $i] : ((relation_dom(identity_relation(A)) = A) & (relation_rng(identity_relation(A)) = A))),
% 3.08/3.29 inference(skolemize,[status(sab)],[194])).
% 3.08/3.29 tff(196,plain,
% 3.08/3.29 (![A: $i] : (~((~(relation_dom(identity_relation(A)) = A)) | (~(relation_rng(identity_relation(A)) = A))))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[195, 191])).
% 3.08/3.29 tff(197,plain,
% 3.08/3.29 (![A: $i] : (~((~(relation_dom(identity_relation(A)) = A)) | (~(relation_rng(identity_relation(A)) = A))))),
% 3.08/3.29 inference(modus_ponens,[status(thm)],[196, 189])).
% 3.08/3.29 tff(198,plain,
% 3.08/3.29 ((~![A: $i] : (~((~(relation_dom(identity_relation(A)) = A)) | (~(relation_rng(identity_relation(A)) = A))))) | (~((~(relation_dom(identity_relation(A!10)) = A!10)) | (~(relation_rng(identity_relation(A!10)) = A!10))))),
% 3.08/3.29 inference(quant_inst,[status(thm)],[])).
% 3.08/3.29 tff(199,plain,
% 3.08/3.29 (~((~(relation_dom(identity_relation(A!10)) = A!10)) | (~(relation_rng(identity_relation(A!10)) = A!10)))),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[198, 197])).
% 3.08/3.29 tff(200,plain,
% 3.08/3.29 (((~(relation_dom(identity_relation(A!10)) = A!10)) | (~(relation_rng(identity_relation(A!10)) = A!10))) | (relation_dom(identity_relation(A!10)) = A!10)),
% 3.08/3.29 inference(tautology,[status(thm)],[])).
% 3.08/3.29 tff(201,plain,
% 3.08/3.29 (relation_dom(identity_relation(A!10)) = A!10),
% 3.08/3.29 inference(unit_resolution,[status(thm)],[200, 199])).
% 3.08/3.29 tff(202,plain,
% 3.08/3.29 (relation_dom(B!9) = relation_dom(identity_relation(A!10))),
% 3.08/3.29 inference(monotonicity,[status(thm)],[147])).
% 3.08/3.29 tff(203,plain,
% 3.08/3.29 (relation_dom(B!9) = A!10),
% 3.08/3.29 inference(transitivity,[status(thm)],[202, 201])).
% 3.08/3.29 tff(204,plain,
% 3.08/3.29 ((~(B!9 = identity_relation(A!10))) | (~(relation_dom(B!9) = A!10)) | (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11)))),
% 3.08/3.29 inference(and_elim,[status(thm)],[12])).
% 3.08/3.30 tff(205,plain,
% 3.08/3.30 (~((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11))),
% 3.08/3.30 inference(unit_resolution,[status(thm)],[204, 203, 147])).
% 3.08/3.30 tff(206,plain,
% 3.08/3.30 (((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11)) | in(C!11, A!10)),
% 3.08/3.30 inference(tautology,[status(thm)],[])).
% 3.08/3.30 tff(207,plain,
% 3.08/3.30 (in(C!11, A!10)),
% 3.08/3.30 inference(unit_resolution,[status(thm)],[206, 205])).
% 3.08/3.30 tff(208,plain,
% 3.08/3.30 ((~(in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))) | (~in(C!11, A!10)) | in(ordered_pair(C!11, C!11), identity_relation(A!10))),
% 3.08/3.30 inference(tautology,[status(thm)],[])).
% 3.08/3.30 tff(209,plain,
% 3.08/3.30 ((~(in(C!11, A!10) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10)))) | in(ordered_pair(C!11, C!11), identity_relation(A!10))),
% 3.08/3.30 inference(unit_resolution,[status(thm)],[208, 207])).
% 3.08/3.30 tff(210,plain,
% 3.08/3.30 (in(ordered_pair(C!11, C!11), identity_relation(A!10))),
% 3.08/3.30 inference(unit_resolution,[status(thm)],[209, 187])).
% 3.08/3.30 tff(211,plain,
% 3.08/3.30 ((((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11)))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))) | (~((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11))))) | (~in(ordered_pair(C!11, C!11), identity_relation(A!10)))),
% 3.08/3.30 inference(tautology,[status(thm)],[])).
% 3.08/3.30 tff(212,plain,
% 3.08/3.30 ((((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11)))) <=> in(ordered_pair(C!11, C!11), identity_relation(A!10))) | (~((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11)))))),
% 3.08/3.30 inference(unit_resolution,[status(thm)],[211, 210])).
% 3.08/3.30 tff(213,plain,
% 3.08/3.30 (~((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11))))),
% 3.08/3.30 inference(unit_resolution,[status(thm)],[212, 158])).
% 3.08/3.30 tff(214,plain,
% 3.08/3.30 (((~in(C!11, relation_dom(identity_relation(A!10)))) | (~(C!11 = apply(identity_relation(A!10), C!11)))) | (C!11 = apply(identity_relation(A!10), C!11))),
% 3.08/3.30 inference(tautology,[status(thm)],[])).
% 3.08/3.30 tff(215,plain,
% 3.08/3.30 (C!11 = apply(identity_relation(A!10), C!11)),
% 3.08/3.30 inference(unit_resolution,[status(thm)],[214, 213])).
% 3.08/3.30 tff(216,plain,
% 3.08/3.30 (apply(identity_relation(A!10), C!11) = C!11),
% 3.08/3.30 inference(symmetry,[status(thm)],[215])).
% 3.08/3.30 tff(217,plain,
% 3.08/3.30 (apply(identity_relation(A!10), C!11) = apply(B!9, C!11)),
% 3.08/3.30 inference(monotonicity,[status(thm)],[148])).
% 3.08/3.30 tff(218,plain,
% 3.08/3.30 (apply(B!9, C!11) = apply(identity_relation(A!10), C!11)),
% 3.08/3.30 inference(symmetry,[status(thm)],[217])).
% 3.08/3.30 tff(219,plain,
% 3.08/3.30 (apply(B!9, C!11) = C!11),
% 3.08/3.30 inference(transitivity,[status(thm)],[218, 216])).
% 3.08/3.30 tff(220,plain,
% 3.08/3.30 (((~in(C!11, A!10)) | (apply(B!9, C!11) = C!11)) | (~(apply(B!9, C!11) = C!11))),
% 3.08/3.30 inference(tautology,[status(thm)],[])).
% 3.08/3.30 tff(221,plain,
% 3.08/3.30 (~(apply(B!9, C!11) = C!11)),
% 3.08/3.30 inference(unit_resolution,[status(thm)],[220, 205])).
% 3.08/3.30 tff(222,plain,
% 3.08/3.30 ($false),
% 3.08/3.30 inference(unit_resolution,[status(thm)],[221, 219])).
% 3.08/3.30 % SZS output end Proof
% 3.08/3.30 % E exiting
%------------------------------------------------------------------------------