%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU072+1 : TPTP v9.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n007.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:26:51 AM UTC 2025
% Result : Theorem 0.20s 0.49s
% Output : Proof 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU072+1 : TPTP v9.0.0. Released v3.2.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.13/0.33 % Computer : n007.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri Jun 20 06:01:05 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.20/0.49 % SZS status Theorem
% 0.20/0.49 % SZS output start Proof
% 0.20/0.49 tff(subset_type, type, (
% 0.20/0.49 subset: ( $i * $i ) > $o)).
% 0.20/0.49 tff(singleton_type, type, (
% 0.20/0.49 singleton: $i > $i)).
% 0.20/0.49 tff(tptp_fun_C_3_type, type, (
% 0.20/0.49 tptp_fun_C_3: $i > $i)).
% 0.20/0.49 tff(tptp_fun_A_16_type, type, (
% 0.20/0.49 tptp_fun_A_16: $i)).
% 0.20/0.49 tff(tptp_fun_B_4_type, type, (
% 0.20/0.49 tptp_fun_B_4: $i > $i)).
% 0.20/0.49 tff(relation_inverse_image_type, type, (
% 0.20/0.49 relation_inverse_image: ( $i * $i ) > $i)).
% 0.20/0.49 tff(relation_image_type, type, (
% 0.20/0.49 relation_image: ( $i * $i ) > $i)).
% 0.20/0.49 tff(apply_type, type, (
% 0.20/0.49 apply: ( $i * $i ) > $i)).
% 0.20/0.49 tff(in_type, type, (
% 0.20/0.49 in: ( $i * $i ) > $o)).
% 0.20/0.49 tff(relation_dom_type, type, (
% 0.20/0.49 relation_dom: $i > $i)).
% 0.20/0.49 tff(one_to_one_type, type, (
% 0.20/0.49 one_to_one: $i > $o)).
% 0.20/0.49 tff(function_type, type, (
% 0.20/0.49 function: $i > $o)).
% 0.20/0.49 tff(relation_type, type, (
% 0.20/0.49 relation: $i > $o)).
% 0.20/0.49 tff(empty_set_type, type, (
% 0.20/0.49 empty_set: $i)).
% 0.20/0.49 tff(relation_rng_type, type, (
% 0.20/0.49 relation_rng: $i > $i)).
% 0.20/0.49 tff(tptp_fun_D_0_type, type, (
% 0.20/0.49 tptp_fun_D_0: ( $i * $i ) > $i)).
% 0.20/0.49 tff(tptp_fun_C_1_type, type, (
% 0.20/0.49 tptp_fun_C_1: ( $i * $i ) > $i)).
% 0.20/0.49 tff(tptp_fun_D_2_type, type, (
% 0.20/0.49 tptp_fun_D_2: ( $i * $i ) > $i)).
% 0.20/0.49 tff(1,plain,
% 0.20/0.49 (((~one_to_one(A!16)) & (relation(A!16) & function(A!16)) & ![B: $i] : subset(relation_inverse_image(A!16, relation_image(A!16, B)), B)) <=> ((~one_to_one(A!16)) & relation(A!16) & function(A!16) & ![B: $i] : subset(relation_inverse_image(A!16, relation_image(A!16, B)), B))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(2,plain,
% 0.20/0.49 ((~![A: $i] : (one_to_one(A) | (~(relation(A) & function(A))) | (~![B: $i] : subset(relation_inverse_image(A, relation_image(A, B)), B)))) <=> (~![A: $i] : (one_to_one(A) | (~(relation(A) & function(A))) | (~![B: $i] : subset(relation_inverse_image(A, relation_image(A, B)), B))))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(3,plain,
% 0.20/0.49 ((~![A: $i] : ((relation(A) & function(A)) => (![B: $i] : subset(relation_inverse_image(A, relation_image(A, B)), B) => one_to_one(A)))) <=> (~![A: $i] : (one_to_one(A) | (~(relation(A) & function(A))) | (~![B: $i] : subset(relation_inverse_image(A, relation_image(A, B)), B))))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(4,axiom,(~![A: $i] : ((relation(A) & function(A)) => (![B: $i] : subset(relation_inverse_image(A, relation_image(A, B)), B) => one_to_one(A)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t153_funct_1')).
% 0.20/0.49 tff(5,plain,
% 0.20/0.49 (~![A: $i] : (one_to_one(A) | (~(relation(A) & function(A))) | (~![B: $i] : subset(relation_inverse_image(A, relation_image(A, B)), B)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.20/0.49 tff(6,plain,
% 0.20/0.49 (~![A: $i] : (one_to_one(A) | (~(relation(A) & function(A))) | (~![B: $i] : subset(relation_inverse_image(A, relation_image(A, B)), B)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[5, 2])).
% 0.20/0.49 tff(7,plain,
% 0.20/0.49 (~![A: $i] : (one_to_one(A) | (~(relation(A) & function(A))) | (~![B: $i] : subset(relation_inverse_image(A, relation_image(A, B)), B)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.20/0.49 tff(8,plain,
% 0.20/0.49 (~![A: $i] : (one_to_one(A) | (~(relation(A) & function(A))) | (~![B: $i] : subset(relation_inverse_image(A, relation_image(A, B)), B)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[7, 2])).
% 0.20/0.49 tff(9,plain,
% 0.20/0.49 ((~one_to_one(A!16)) & relation(A!16) & function(A!16) & ![B: $i] : subset(relation_inverse_image(A!16, relation_image(A!16, B)), B)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[8, 1])).
% 0.20/0.49 tff(10,plain,
% 0.20/0.49 (function(A!16)),
% 0.20/0.49 inference(and_elim,[status(thm)],[9])).
% 0.20/0.49 tff(11,plain,
% 0.20/0.49 (relation(A!16)),
% 0.20/0.49 inference(and_elim,[status(thm)],[9])).
% 0.20/0.49 tff(12,plain,
% 0.20/0.49 (^[A: $i] : refl(((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))))))))) <=> ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))))))))))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(13,plain,
% 0.20/0.50 (![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[12])).
% 0.20/0.50 tff(14,plain,
% 0.20/0.50 (^[A: $i] : rewrite(((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))))))))) <=> ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))))))))))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(15,plain,
% 0.20/0.50 (![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[14])).
% 0.20/0.50 tff(16,plain,
% 0.20/0.50 (![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))),
% 0.20/0.50 inference(transitivity,[status(thm)],[15, 13])).
% 0.20/0.50 tff(17,plain,
% 0.20/0.50 (^[A: $i] : trans(monotonicity(trans(monotonicity(rewrite((relation(A) & function(A)) <=> (~((~relation(A)) | (~function(A))))), ((~(relation(A) & function(A))) <=> (~(~((~relation(A)) | (~function(A))))))), rewrite((~(~((~relation(A)) | (~function(A))))) <=> ((~relation(A)) | (~function(A)))), ((~(relation(A) & function(A))) <=> ((~relation(A)) | (~function(A))))), trans(monotonicity(rewrite(((~one_to_one(A)) | ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))) <=> ((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))), rewrite((one_to_one(A) | (~((~(in(tptp_fun_B_4(A), relation_dom(A)) & in(tptp_fun_C_3(A), relation_dom(A)) & (apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))) | (tptp_fun_B_4(A) = tptp_fun_C_3(A))))) <=> (one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))), ((((~one_to_one(A)) | ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))) & (one_to_one(A) | (~((~(in(tptp_fun_B_4(A), relation_dom(A)) & in(tptp_fun_C_3(A), relation_dom(A)) & (apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))) | (tptp_fun_B_4(A) = tptp_fun_C_3(A)))))) <=> (((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C))))) & (one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))), rewrite((((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C))))) & (one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))) <=> (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))))))))), ((((~one_to_one(A)) | ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))) & (one_to_one(A) | (~((~(in(tptp_fun_B_4(A), relation_dom(A)) & in(tptp_fun_C_3(A), relation_dom(A)) & (apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))) | (tptp_fun_B_4(A) = tptp_fun_C_3(A)))))) <=> (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))), (((~(relation(A) & function(A))) | (((~one_to_one(A)) | ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))) & (one_to_one(A) | (~((~(in(tptp_fun_B_4(A), relation_dom(A)) & in(tptp_fun_C_3(A), relation_dom(A)) & (apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))) | (tptp_fun_B_4(A) = tptp_fun_C_3(A))))))) <=> (((~relation(A)) | (~function(A))) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))))))))))), rewrite((((~relation(A)) | (~function(A))) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))))))))) <=> ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))), (((~(relation(A) & function(A))) | (((~one_to_one(A)) | ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))) & (one_to_one(A) | (~((~(in(tptp_fun_B_4(A), relation_dom(A)) & in(tptp_fun_C_3(A), relation_dom(A)) & (apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))) | (tptp_fun_B_4(A) = tptp_fun_C_3(A))))))) <=> ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(18,plain,
% 0.20/0.50 (![A: $i] : ((~(relation(A) & function(A))) | (((~one_to_one(A)) | ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))) & (one_to_one(A) | (~((~(in(tptp_fun_B_4(A), relation_dom(A)) & in(tptp_fun_C_3(A), relation_dom(A)) & (apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))) | (tptp_fun_B_4(A) = tptp_fun_C_3(A))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[17])).
% 0.20/0.50 tff(19,plain,
% 0.20/0.50 (![A: $i] : ((~(relation(A) & function(A))) | (one_to_one(A) <=> ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C)))) <=> ![A: $i] : ((~(relation(A) & function(A))) | (one_to_one(A) <=> ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(20,plain,
% 0.20/0.50 (^[A: $i] : trans(monotonicity(rewrite((one_to_one(A) <=> ![B: $i, C: $i] : (((in(B, relation_dom(A)) & in(C, relation_dom(A))) & (apply(A, B) = apply(A, C))) => (B = C))) <=> (one_to_one(A) <=> ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C)))), (((relation(A) & function(A)) => (one_to_one(A) <=> ![B: $i, C: $i] : (((in(B, relation_dom(A)) & in(C, relation_dom(A))) & (apply(A, B) = apply(A, C))) => (B = C)))) <=> ((relation(A) & function(A)) => (one_to_one(A) <=> ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C)))))), rewrite(((relation(A) & function(A)) => (one_to_one(A) <=> ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C)))) <=> ((~(relation(A) & function(A))) | (one_to_one(A) <=> ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))))), (((relation(A) & function(A)) => (one_to_one(A) <=> ![B: $i, C: $i] : (((in(B, relation_dom(A)) & in(C, relation_dom(A))) & (apply(A, B) = apply(A, C))) => (B = C)))) <=> ((~(relation(A) & function(A))) | (one_to_one(A) <=> ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))))))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(21,plain,
% 0.20/0.50 (![A: $i] : ((relation(A) & function(A)) => (one_to_one(A) <=> ![B: $i, C: $i] : (((in(B, relation_dom(A)) & in(C, relation_dom(A))) & (apply(A, B) = apply(A, C))) => (B = C)))) <=> ![A: $i] : ((~(relation(A) & function(A))) | (one_to_one(A) <=> ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[20])).
% 0.20/0.50 tff(22,axiom,(![A: $i] : ((relation(A) & function(A)) => (one_to_one(A) <=> ![B: $i, C: $i] : (((in(B, relation_dom(A)) & in(C, relation_dom(A))) & (apply(A, B) = apply(A, C))) => (B = C))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d8_funct_1')).
% 0.20/0.50 tff(23,plain,
% 0.20/0.50 (![A: $i] : ((~(relation(A) & function(A))) | (one_to_one(A) <=> ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[22, 21])).
% 0.20/0.50 tff(24,plain,
% 0.20/0.50 (![A: $i] : ((~(relation(A) & function(A))) | (one_to_one(A) <=> ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[23, 19])).
% 0.20/0.50 tff(25,plain,(
% 0.20/0.50 ![A: $i] : ((~(relation(A) & function(A))) | (((~one_to_one(A)) | ![B: $i, C: $i] : ((~(in(B, relation_dom(A)) & in(C, relation_dom(A)) & (apply(A, B) = apply(A, C)))) | (B = C))) & (one_to_one(A) | (~((~(in(tptp_fun_B_4(A), relation_dom(A)) & in(tptp_fun_C_3(A), relation_dom(A)) & (apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A))))) | (tptp_fun_B_4(A) = tptp_fun_C_3(A)))))))),
% 0.20/0.50 inference(skolemize,[status(sab)],[24])).
% 0.20/0.50 tff(26,plain,
% 0.20/0.50 (![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[25, 18])).
% 0.20/0.50 tff(27,plain,
% 0.20/0.50 (![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[26, 16])).
% 0.20/0.50 tff(28,plain,
% 0.20/0.50 (((~![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))) | ((~function(A!16)) | (~relation(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))))))))) <=> ((~![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))) | (~function(A!16)) | (~relation(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))))))))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(29,plain,
% 0.20/0.50 (((~relation(A!16)) | (~function(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))))))))) <=> ((~function(A!16)) | (~relation(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))))))))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(30,plain,
% 0.20/0.50 ((~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))))))))) <=> (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))))))))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(31,plain,
% 0.20/0.50 (((~relation(A!16)) | (~function(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16))))))))))) <=> ((~relation(A!16)) | (~function(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))))))))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[30])).
% 0.20/0.50 tff(32,plain,
% 0.20/0.50 (((~relation(A!16)) | (~function(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16))))))))))) <=> ((~function(A!16)) | (~relation(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))))))))),
% 0.20/0.50 inference(transitivity,[status(thm)],[31, 29])).
% 0.20/0.50 tff(33,plain,
% 0.20/0.50 (((~![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))) | ((~relation(A!16)) | (~function(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))))))))))) <=> ((~![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))) | ((~function(A!16)) | (~relation(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))))))))))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[32])).
% 0.20/0.50 tff(34,plain,
% 0.20/0.50 (((~![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))) | ((~relation(A!16)) | (~function(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))))))))))) <=> ((~![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))) | (~function(A!16)) | (~relation(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))))))))),
% 0.20/0.50 inference(transitivity,[status(thm)],[33, 28])).
% 0.20/0.50 tff(35,plain,
% 0.20/0.50 ((~![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))) | ((~relation(A!16)) | (~function(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))))))))))),
% 0.20/0.50 inference(quant_inst,[status(thm)],[])).
% 0.20/0.50 tff(36,plain,
% 0.20/0.50 ((~![A: $i] : ((~relation(A)) | (~function(A)) | (~((~((~one_to_one(A)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A))) | (~in(B, relation_dom(A))) | (~(apply(A, B) = apply(A, C)))))) | (~(one_to_one(A) | (~((tptp_fun_B_4(A) = tptp_fun_C_3(A)) | (~in(tptp_fun_B_4(A), relation_dom(A))) | (~in(tptp_fun_C_3(A), relation_dom(A))) | (~(apply(A, tptp_fun_B_4(A)) = apply(A, tptp_fun_C_3(A)))))))))))) | (~function(A!16)) | (~relation(A!16)) | (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))))))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[35, 34])).
% 0.20/0.50 tff(37,plain,
% 0.20/0.50 (~((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))))))),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[36, 27, 11, 10])).
% 0.20/0.50 tff(38,plain,
% 0.20/0.50 (((~((~one_to_one(A!16)) | ![B: $i, C: $i] : ((B = C) | (~in(C, relation_dom(A!16))) | (~in(B, relation_dom(A!16))) | (~(apply(A!16, B) = apply(A!16, C)))))) | (~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))))))) | (one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))))),
% 0.20/0.50 inference(tautology,[status(thm)],[])).
% 0.20/0.50 tff(39,plain,
% 0.20/0.50 (one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))))),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[38, 37])).
% 0.20/0.50 tff(40,plain,
% 0.20/0.50 (~one_to_one(A!16)),
% 0.20/0.50 inference(and_elim,[status(thm)],[9])).
% 0.20/0.50 tff(41,plain,
% 0.20/0.50 ((~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))))) | one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))))),
% 0.20/0.50 inference(tautology,[status(thm)],[])).
% 0.20/0.50 tff(42,plain,
% 0.20/0.50 ((~(one_to_one(A!16) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))))) | (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))))),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[41, 40])).
% 0.20/0.50 tff(43,plain,
% 0.20/0.50 (~((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[42, 39])).
% 0.20/0.50 tff(44,plain,
% 0.20/0.50 (((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))) | in(tptp_fun_B_4(A!16), relation_dom(A!16))),
% 0.20/0.50 inference(tautology,[status(thm)],[])).
% 0.20/0.50 tff(45,plain,
% 0.20/0.50 (in(tptp_fun_B_4(A!16), relation_dom(A!16))),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[44, 43])).
% 0.20/0.50 tff(46,plain,
% 0.20/0.50 (^[A: $i, B: $i] : refl(((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B))) <=> ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B))))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(47,plain,
% 0.20/0.50 (![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B))) <=> ![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[46])).
% 0.20/0.50 tff(48,plain,
% 0.20/0.50 (^[A: $i, B: $i] : trans(monotonicity(trans(monotonicity(rewrite((relation(B) & function(B)) <=> (~((~relation(B)) | (~function(B))))), ((~(relation(B) & function(B))) <=> (~(~((~relation(B)) | (~function(B))))))), rewrite((~(~((~relation(B)) | (~function(B))))) <=> ((~relation(B)) | (~function(B)))), ((~(relation(B) & function(B))) <=> ((~relation(B)) | (~function(B))))), (((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B)))) <=> ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | ((~relation(B)) | (~function(B))) | (~in(A, relation_dom(B)))))), rewrite(((relation_image(B, singleton(A)) = singleton(apply(B, A))) | ((~relation(B)) | (~function(B))) | (~in(A, relation_dom(B)))) <=> ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))), (((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B)))) <=> ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(49,plain,
% 0.20/0.50 (![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B)))) <=> ![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[48])).
% 0.20/0.50 tff(50,plain,
% 0.20/0.50 (![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B)))) <=> ![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B))))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(51,plain,
% 0.20/0.50 (^[A: $i, B: $i] : trans(monotonicity(rewrite((in(A, relation_dom(B)) => (relation_image(B, singleton(A)) = singleton(apply(B, A)))) <=> ((~in(A, relation_dom(B))) | (relation_image(B, singleton(A)) = singleton(apply(B, A))))), (((relation(B) & function(B)) => (in(A, relation_dom(B)) => (relation_image(B, singleton(A)) = singleton(apply(B, A))))) <=> ((relation(B) & function(B)) => ((~in(A, relation_dom(B))) | (relation_image(B, singleton(A)) = singleton(apply(B, A))))))), rewrite(((relation(B) & function(B)) => ((~in(A, relation_dom(B))) | (relation_image(B, singleton(A)) = singleton(apply(B, A))))) <=> ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B))))), (((relation(B) & function(B)) => (in(A, relation_dom(B)) => (relation_image(B, singleton(A)) = singleton(apply(B, A))))) <=> ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B))))))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(52,plain,
% 0.20/0.50 (![A: $i, B: $i] : ((relation(B) & function(B)) => (in(A, relation_dom(B)) => (relation_image(B, singleton(A)) = singleton(apply(B, A))))) <=> ![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B))))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[51])).
% 0.20/0.51 tff(53,axiom,(![A: $i, B: $i] : ((relation(B) & function(B)) => (in(A, relation_dom(B)) => (relation_image(B, singleton(A)) = singleton(apply(B, A)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t117_funct_1')).
% 0.20/0.51 tff(54,plain,
% 0.20/0.51 (![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[53, 52])).
% 0.20/0.51 tff(55,plain,
% 0.20/0.51 (![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[54, 50])).
% 0.20/0.51 tff(56,plain,(
% 0.20/0.51 ![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~(relation(B) & function(B))) | (~in(A, relation_dom(B))))),
% 0.20/0.51 inference(skolemize,[status(sab)],[55])).
% 0.20/0.51 tff(57,plain,
% 0.20/0.51 (![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[56, 49])).
% 0.20/0.51 tff(58,plain,
% 0.20/0.51 (![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[57, 47])).
% 0.20/0.51 tff(59,plain,
% 0.20/0.51 (((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | ((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16)))))) <=> ((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16)))))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(60,plain,
% 0.20/0.51 (((relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16)))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~relation(A!16)) | (~function(A!16))) <=> ((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16)))))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(61,plain,
% 0.20/0.51 (((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | ((relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16)))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~relation(A!16)) | (~function(A!16)))) <=> ((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | ((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16))))))),
% 0.20/0.51 inference(monotonicity,[status(thm)],[60])).
% 0.20/0.51 tff(62,plain,
% 0.20/0.51 (((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | ((relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16)))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~relation(A!16)) | (~function(A!16)))) <=> ((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16)))))),
% 0.20/0.51 inference(transitivity,[status(thm)],[61, 59])).
% 0.20/0.51 tff(63,plain,
% 0.20/0.51 ((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | ((relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16)))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~relation(A!16)) | (~function(A!16)))),
% 0.20/0.51 inference(quant_inst,[status(thm)],[])).
% 0.20/0.51 tff(64,plain,
% 0.20/0.51 ((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[63, 62])).
% 0.20/0.51 tff(65,plain,
% 0.20/0.51 (relation_image(A!16, singleton(tptp_fun_B_4(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16)))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[64, 58, 11, 10, 45])).
% 0.20/0.51 tff(66,plain,
% 0.20/0.51 (singleton(apply(A!16, tptp_fun_B_4(A!16))) = relation_image(A!16, singleton(tptp_fun_B_4(A!16)))),
% 0.20/0.51 inference(symmetry,[status(thm)],[65])).
% 0.20/0.51 tff(67,plain,
% 0.20/0.51 (((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))) | (apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))),
% 0.20/0.51 inference(tautology,[status(thm)],[])).
% 0.20/0.51 tff(68,plain,
% 0.20/0.51 (apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[67, 43])).
% 0.20/0.51 tff(69,plain,
% 0.20/0.51 (apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16))),
% 0.20/0.51 inference(symmetry,[status(thm)],[68])).
% 0.20/0.51 tff(70,plain,
% 0.20/0.51 (singleton(apply(A!16, tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_B_4(A!16)))),
% 0.20/0.51 inference(monotonicity,[status(thm)],[69])).
% 0.20/0.51 tff(71,plain,
% 0.20/0.51 (((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))) | in(tptp_fun_C_3(A!16), relation_dom(A!16))),
% 0.20/0.51 inference(tautology,[status(thm)],[])).
% 0.20/0.51 tff(72,plain,
% 0.20/0.51 (in(tptp_fun_C_3(A!16), relation_dom(A!16))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[71, 43])).
% 0.20/0.51 tff(73,plain,
% 0.20/0.51 (((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | ((~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16)))))) <=> ((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16)))))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(74,plain,
% 0.20/0.51 (((relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~relation(A!16)) | (~function(A!16))) <=> ((~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16)))))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(75,plain,
% 0.20/0.51 (((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | ((relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~relation(A!16)) | (~function(A!16)))) <=> ((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | ((~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16))))))),
% 0.20/0.51 inference(monotonicity,[status(thm)],[74])).
% 0.20/0.51 tff(76,plain,
% 0.20/0.51 (((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | ((relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~relation(A!16)) | (~function(A!16)))) <=> ((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16)))))),
% 0.20/0.51 inference(transitivity,[status(thm)],[75, 73])).
% 0.20/0.51 tff(77,plain,
% 0.20/0.51 ((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | ((relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~relation(A!16)) | (~function(A!16)))),
% 0.20/0.51 inference(quant_inst,[status(thm)],[])).
% 0.20/0.51 tff(78,plain,
% 0.20/0.51 ((~![A: $i, B: $i] : ((relation_image(B, singleton(A)) = singleton(apply(B, A))) | (~in(A, relation_dom(B))) | (~relation(B)) | (~function(B)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~function(A!16)) | (~relation(A!16)) | (relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[77, 76])).
% 0.20/0.51 tff(79,plain,
% 0.20/0.51 (relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = singleton(apply(A!16, tptp_fun_C_3(A!16)))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[78, 58, 11, 10, 72])).
% 0.20/0.51 tff(80,plain,
% 0.20/0.51 (relation_image(A!16, singleton(tptp_fun_C_3(A!16))) = relation_image(A!16, singleton(tptp_fun_B_4(A!16)))),
% 0.20/0.51 inference(transitivity,[status(thm)],[79, 70, 66])).
% 0.20/0.51 tff(81,plain,
% 0.20/0.51 (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_C_3(A!16)))) = relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16))))),
% 0.20/0.51 inference(monotonicity,[status(thm)],[80])).
% 0.20/0.51 tff(82,plain,
% 0.20/0.51 (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_C_3(A!16))))),
% 0.20/0.51 inference(symmetry,[status(thm)],[81])).
% 0.20/0.51 tff(83,plain,
% 0.20/0.51 (^[A: $i, B: $i] : refl((subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B)))) <=> (subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B)))))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(84,plain,
% 0.20/0.51 (![A: $i, B: $i] : (subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B)))) <=> ![A: $i, B: $i] : (subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B))))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[83])).
% 0.20/0.51 tff(85,plain,
% 0.20/0.51 (![A: $i, B: $i] : (subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B)))) <=> ![A: $i, B: $i] : (subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B))))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(86,axiom,(![A: $i, B: $i] : (subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t39_zfmisc_1')).
% 0.20/0.51 tff(87,plain,
% 0.20/0.51 (![A: $i, B: $i] : (subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[86, 85])).
% 0.20/0.51 tff(88,plain,(
% 0.20/0.51 ![A: $i, B: $i] : (subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B))))),
% 0.20/0.51 inference(skolemize,[status(sab)],[87])).
% 0.20/0.51 tff(89,plain,
% 0.20/0.51 (![A: $i, B: $i] : (subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[88, 84])).
% 0.20/0.51 tff(90,plain,
% 0.20/0.51 ((~![A: $i, B: $i] : (subset(A, singleton(B)) <=> ((A = empty_set) | (A = singleton(B))))) | (subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))), singleton(tptp_fun_B_4(A!16))) <=> ((relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set) | (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = singleton(tptp_fun_B_4(A!16)))))),
% 0.20/0.51 inference(quant_inst,[status(thm)],[])).
% 0.20/0.51 tff(91,plain,
% 0.20/0.51 (subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))), singleton(tptp_fun_B_4(A!16))) <=> ((relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set) | (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = singleton(tptp_fun_B_4(A!16))))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[90, 89])).
% 0.20/0.51 tff(92,plain,
% 0.20/0.51 (^[B: $i] : refl(subset(relation_inverse_image(A!16, relation_image(A!16, B)), B) <=> subset(relation_inverse_image(A!16, relation_image(A!16, B)), B))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(93,plain,
% 0.20/0.51 (![B: $i] : subset(relation_inverse_image(A!16, relation_image(A!16, B)), B) <=> ![B: $i] : subset(relation_inverse_image(A!16, relation_image(A!16, B)), B)),
% 0.20/0.51 inference(quant_intro,[status(thm)],[92])).
% 0.20/0.51 tff(94,plain,
% 0.20/0.51 (![B: $i] : subset(relation_inverse_image(A!16, relation_image(A!16, B)), B)),
% 0.20/0.51 inference(and_elim,[status(thm)],[9])).
% 0.20/0.51 tff(95,plain,
% 0.20/0.51 (![B: $i] : subset(relation_inverse_image(A!16, relation_image(A!16, B)), B)),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[94, 93])).
% 0.20/0.51 tff(96,plain,
% 0.20/0.51 ((~![B: $i] : subset(relation_inverse_image(A!16, relation_image(A!16, B)), B)) | subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))), singleton(tptp_fun_B_4(A!16)))),
% 0.20/0.51 inference(quant_inst,[status(thm)],[])).
% 0.20/0.51 tff(97,plain,
% 0.20/0.51 (subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))), singleton(tptp_fun_B_4(A!16)))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[96, 95])).
% 0.20/0.51 tff(98,plain,
% 0.20/0.51 ((~(subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))), singleton(tptp_fun_B_4(A!16))) <=> ((relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set) | (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = singleton(tptp_fun_B_4(A!16)))))) | (~subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))), singleton(tptp_fun_B_4(A!16)))) | ((relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set) | (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = singleton(tptp_fun_B_4(A!16))))),
% 0.20/0.51 inference(tautology,[status(thm)],[])).
% 0.20/0.51 tff(99,plain,
% 0.20/0.51 ((~(subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))), singleton(tptp_fun_B_4(A!16))) <=> ((relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set) | (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = singleton(tptp_fun_B_4(A!16)))))) | ((relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set) | (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = singleton(tptp_fun_B_4(A!16))))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[98, 97])).
% 0.20/0.51 tff(100,plain,
% 0.20/0.51 ((relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set) | (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = singleton(tptp_fun_B_4(A!16)))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[99, 91])).
% 0.20/0.51 tff(101,plain,
% 0.20/0.51 (singleton(apply(A!16, tptp_fun_C_3(A!16))) = relation_image(A!16, singleton(tptp_fun_B_4(A!16)))),
% 0.20/0.51 inference(transitivity,[status(thm)],[70, 66])).
% 0.20/0.51 tff(102,plain,
% 0.20/0.51 (relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16))))),
% 0.20/0.51 inference(monotonicity,[status(thm)],[101])).
% 0.20/0.51 tff(103,plain,
% 0.20/0.51 ((relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = empty_set) <=> (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set)),
% 0.20/0.51 inference(monotonicity,[status(thm)],[102])).
% 0.20/0.51 tff(104,plain,
% 0.20/0.51 ((~(relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = empty_set)) <=> (~(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set))),
% 0.20/0.51 inference(monotonicity,[status(thm)],[103])).
% 0.20/0.51 tff(105,plain,
% 0.20/0.51 (^[A: $i, B: $i] : refl(((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B))))) <=> ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B))))))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(106,plain,
% 0.20/0.51 (![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B))))) <=> ![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[105])).
% 0.20/0.51 tff(107,plain,
% 0.20/0.51 (![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B))))) <=> ![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(108,plain,
% 0.20/0.51 (^[A: $i, B: $i] : trans(monotonicity(trans(rewrite((in(A, relation_rng(B)) <=> (~(relation_inverse_image(B, singleton(A)) = empty_set))) <=> (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B))))), rewrite((~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))) <=> (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B))))), ((in(A, relation_rng(B)) <=> (~(relation_inverse_image(B, singleton(A)) = empty_set))) <=> (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))), ((relation(B) => (in(A, relation_rng(B)) <=> (~(relation_inverse_image(B, singleton(A)) = empty_set)))) <=> (relation(B) => (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B))))))), rewrite((relation(B) => (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B))))) <=> ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))), ((relation(B) => (in(A, relation_rng(B)) <=> (~(relation_inverse_image(B, singleton(A)) = empty_set)))) <=> ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(109,plain,
% 0.20/0.51 (![A: $i, B: $i] : (relation(B) => (in(A, relation_rng(B)) <=> (~(relation_inverse_image(B, singleton(A)) = empty_set)))) <=> ![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[108])).
% 0.20/0.51 tff(110,axiom,(![A: $i, B: $i] : (relation(B) => (in(A, relation_rng(B)) <=> (~(relation_inverse_image(B, singleton(A)) = empty_set))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t142_funct_1')).
% 0.20/0.51 tff(111,plain,
% 0.20/0.51 (![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[110, 109])).
% 0.20/0.51 tff(112,plain,
% 0.20/0.51 (![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[111, 107])).
% 0.20/0.51 tff(113,plain,(
% 0.20/0.51 ![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))),
% 0.20/0.51 inference(skolemize,[status(sab)],[112])).
% 0.20/0.51 tff(114,plain,
% 0.20/0.51 (![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[113, 106])).
% 0.20/0.51 tff(115,plain,
% 0.20/0.51 (((~![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))) | ((~relation(A!16)) | (~((relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = empty_set) <=> in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)))))) <=> ((~![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))) | (~relation(A!16)) | (~((relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = empty_set) <=> in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)))))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(116,plain,
% 0.20/0.51 ((~![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))) | ((~relation(A!16)) | (~((relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = empty_set) <=> in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)))))),
% 0.20/0.51 inference(quant_inst,[status(thm)],[])).
% 0.20/0.51 tff(117,plain,
% 0.20/0.51 ((~![A: $i, B: $i] : ((~relation(B)) | (~((relation_inverse_image(B, singleton(A)) = empty_set) <=> in(A, relation_rng(B)))))) | (~relation(A!16)) | (~((relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = empty_set) <=> in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[116, 115])).
% 0.20/0.51 tff(118,plain,
% 0.20/0.51 (~((relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = empty_set) <=> in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[117, 114, 11])).
% 0.20/0.51 tff(119,plain,
% 0.20/0.51 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i, D_17: $i, C: $i, D: $i] : rewrite((~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17)))))))))))) <=> (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))), (![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17)))))))))))) <=> ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))), (((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17)))))))))))))), rewrite(((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17)))))))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))), (((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(120,plain,
% 0.20/0.51 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[119])).
% 0.20/0.51 tff(121,plain,
% 0.20/0.51 (^[A: $i] : refl(((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(122,plain,
% 0.20/0.51 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17)))))))))))))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[121])).
% 0.20/0.51 tff(123,plain,
% 0.20/0.51 (^[A: $i] : rewrite(((~relation(A)) | (~function(A)) | ![B: $i] : (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(124,plain,
% 0.20/0.51 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i] : (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17)))))))))))))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[123])).
% 0.20/0.51 tff(125,plain,
% 0.20/0.51 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i] : (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17)))))))))))))),
% 0.20/0.51 inference(transitivity,[status(thm)],[124, 122])).
% 0.20/0.51 tff(126,plain,
% 0.20/0.51 (^[A: $i] : trans(monotonicity(trans(monotonicity(rewrite((relation(A) & function(A)) <=> (~((~relation(A)) | (~function(A))))), ((~(relation(A) & function(A))) <=> (~(~((~relation(A)) | (~function(A))))))), rewrite((~(~((~relation(A)) | (~function(A))))) <=> ((~relation(A)) | (~function(A)))), ((~(relation(A) & function(A))) <=> ((~relation(A)) | (~function(A))))), quant_intro(proof_bind(^[B: $i] : trans(monotonicity(rewrite(((~(B = relation_rng(A))) | ![C: $i] : (((~in(C, B)) | (in(tptp_fun_D_0(C, A), relation_dom(A)) & (C = apply(A, tptp_fun_D_0(C, A))))) & (in(C, B) | ![D: $i] : (~(in(D, relation_dom(A)) & (C = apply(A, D))))))) <=> ((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))), trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))) <=> (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))))), ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) <=> (in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))))))), rewrite((in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))))) <=> (in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))), ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) <=> (in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))))))), rewrite(((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D))))) <=> ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))), (((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D)))))) <=> ((in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))))), rewrite(((in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))) <=> (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))), (((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D)))))) <=> (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))))))), (((B = relation_rng(A)) | ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D))))))) <=> ((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))))), rewrite(((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))) <=> ((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))))))), (((B = relation_rng(A)) | ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D))))))) <=> ((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))))), ((((~(B = relation_rng(A))) | ![C: $i] : (((~in(C, B)) | (in(tptp_fun_D_0(C, A), relation_dom(A)) & (C = apply(A, tptp_fun_D_0(C, A))))) & (in(C, B) | ![D: $i] : (~(in(D, relation_dom(A)) & (C = apply(A, D))))))) & ((B = relation_rng(A)) | ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D)))))))) <=> (((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) & ((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))))))))), rewrite((((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) & ((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))))))) <=> (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))))))), ((((~(B = relation_rng(A))) | ![C: $i] : (((~in(C, B)) | (in(tptp_fun_D_0(C, A), relation_dom(A)) & (C = apply(A, tptp_fun_D_0(C, A))))) & (in(C, B) | ![D: $i] : (~(in(D, relation_dom(A)) & (C = apply(A, D))))))) & ((B = relation_rng(A)) | ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D)))))))) <=> (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))))))))), (![B: $i] : (((~(B = relation_rng(A))) | ![C: $i] : (((~in(C, B)) | (in(tptp_fun_D_0(C, A), relation_dom(A)) & (C = apply(A, tptp_fun_D_0(C, A))))) & (in(C, B) | ![D: $i] : (~(in(D, relation_dom(A)) & (C = apply(A, D))))))) & ((B = relation_rng(A)) | ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D)))))))) <=> ![B: $i] : (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))))))))))), (((~(relation(A) & function(A))) | ![B: $i] : (((~(B = relation_rng(A))) | ![C: $i] : (((~in(C, B)) | (in(tptp_fun_D_0(C, A), relation_dom(A)) & (C = apply(A, tptp_fun_D_0(C, A))))) & (in(C, B) | ![D: $i] : (~(in(D, relation_dom(A)) & (C = apply(A, D))))))) & ((B = relation_rng(A)) | ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D))))))))) <=> (((~relation(A)) | (~function(A))) | ![B: $i] : (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))))))))), rewrite((((~relation(A)) | (~function(A))) | ![B: $i] : (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D))))))))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i] : (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))))))))))), (((~(relation(A) & function(A))) | ![B: $i] : (((~(B = relation_rng(A))) | ![C: $i] : (((~in(C, B)) | (in(tptp_fun_D_0(C, A), relation_dom(A)) & (C = apply(A, tptp_fun_D_0(C, A))))) & (in(C, B) | ![D: $i] : (~(in(D, relation_dom(A)) & (C = apply(A, D))))))) & ((B = relation_rng(A)) | ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D))))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i] : (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))))))))))))),
% 0.20/0.52 inference(bind,[status(th)],[])).
% 0.20/0.52 tff(127,plain,
% 0.20/0.52 (![A: $i] : ((~(relation(A) & function(A))) | ![B: $i] : (((~(B = relation_rng(A))) | ![C: $i] : (((~in(C, B)) | (in(tptp_fun_D_0(C, A), relation_dom(A)) & (C = apply(A, tptp_fun_D_0(C, A))))) & (in(C, B) | ![D: $i] : (~(in(D, relation_dom(A)) & (C = apply(A, D))))))) & ((B = relation_rng(A)) | ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D))))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i] : (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))))))))))),
% 0.20/0.52 inference(quant_intro,[status(thm)],[126])).
% 0.20/0.52 tff(128,plain,
% 0.20/0.52 (![A: $i] : ((~(relation(A) & function(A))) | ![B: $i] : ((B = relation_rng(A)) <=> ![C: $i] : (in(C, B) <=> ?[D: $i] : (in(D, relation_dom(A)) & (C = apply(A, D)))))) <=> ![A: $i] : ((~(relation(A) & function(A))) | ![B: $i] : ((B = relation_rng(A)) <=> ![C: $i] : (in(C, B) <=> ?[D: $i] : (in(D, relation_dom(A)) & (C = apply(A, D))))))),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(129,plain,
% 0.20/0.52 (^[A: $i] : rewrite(((relation(A) & function(A)) => ![B: $i] : ((B = relation_rng(A)) <=> ![C: $i] : (in(C, B) <=> ?[D: $i] : (in(D, relation_dom(A)) & (C = apply(A, D)))))) <=> ((~(relation(A) & function(A))) | ![B: $i] : ((B = relation_rng(A)) <=> ![C: $i] : (in(C, B) <=> ?[D: $i] : (in(D, relation_dom(A)) & (C = apply(A, D)))))))),
% 0.20/0.52 inference(bind,[status(th)],[])).
% 0.20/0.52 tff(130,plain,
% 0.20/0.52 (![A: $i] : ((relation(A) & function(A)) => ![B: $i] : ((B = relation_rng(A)) <=> ![C: $i] : (in(C, B) <=> ?[D: $i] : (in(D, relation_dom(A)) & (C = apply(A, D)))))) <=> ![A: $i] : ((~(relation(A) & function(A))) | ![B: $i] : ((B = relation_rng(A)) <=> ![C: $i] : (in(C, B) <=> ?[D: $i] : (in(D, relation_dom(A)) & (C = apply(A, D))))))),
% 0.20/0.52 inference(quant_intro,[status(thm)],[129])).
% 0.20/0.52 tff(131,axiom,(![A: $i] : ((relation(A) & function(A)) => ![B: $i] : ((B = relation_rng(A)) <=> ![C: $i] : (in(C, B) <=> ?[D: $i] : (in(D, relation_dom(A)) & (C = apply(A, D))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d5_funct_1')).
% 0.20/0.52 tff(132,plain,
% 0.20/0.52 (![A: $i] : ((~(relation(A) & function(A))) | ![B: $i] : ((B = relation_rng(A)) <=> ![C: $i] : (in(C, B) <=> ?[D: $i] : (in(D, relation_dom(A)) & (C = apply(A, D))))))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[131, 130])).
% 0.20/0.52 tff(133,plain,
% 0.20/0.52 (![A: $i] : ((~(relation(A) & function(A))) | ![B: $i] : ((B = relation_rng(A)) <=> ![C: $i] : (in(C, B) <=> ?[D: $i] : (in(D, relation_dom(A)) & (C = apply(A, D))))))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[132, 128])).
% 0.20/0.52 tff(134,plain,(
% 0.20/0.52 ![A: $i] : ((~(relation(A) & function(A))) | ![B: $i] : (((~(B = relation_rng(A))) | ![C: $i] : (((~in(C, B)) | (in(tptp_fun_D_0(C, A), relation_dom(A)) & (C = apply(A, tptp_fun_D_0(C, A))))) & (in(C, B) | ![D: $i] : (~(in(D, relation_dom(A)) & (C = apply(A, D))))))) & ((B = relation_rng(A)) | ((in(tptp_fun_C_1(B, A), B) | (in(tptp_fun_D_2(B, A), relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A))))) & ((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : (~(in(D, relation_dom(A)) & (tptp_fun_C_1(B, A) = apply(A, D)))))))))),
% 0.20/0.52 inference(skolemize,[status(sab)],[133])).
% 0.20/0.52 tff(135,plain,
% 0.20/0.52 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i] : (~((~((~(B = relation_rng(A))) | ![C: $i] : (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ![D: $i] : ((~in(D, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D)))))))))))))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[134, 127])).
% 0.20/0.52 tff(136,plain,
% 0.20/0.52 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | ((~in(D, relation_dom(A))) | (~(C = apply(A, D)))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | ((~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17)))))))))))))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[135, 125])).
% 0.20/0.52 tff(137,plain,
% 0.20/0.52 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[136, 120])).
% 0.20/0.52 tff(138,plain,
% 0.20/0.52 (((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) | ((~function(A!16)) | (~relation(A!16)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17))))))))))))) <=> ((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) | (~function(A!16)) | (~relation(A!16)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17))))))))))))),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(139,plain,
% 0.20/0.52 (((~relation(A!16)) | (~function(A!16)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))) <=> ((~function(A!16)) | (~relation(A!16)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17))))))))))))),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(140,plain,
% 0.20/0.52 (((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) | ((~relation(A!16)) | (~function(A!16)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17))))))))))))) <=> ((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) | ((~function(A!16)) | (~relation(A!16)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))))),
% 0.20/0.52 inference(monotonicity,[status(thm)],[139])).
% 0.20/0.52 tff(141,plain,
% 0.20/0.52 (((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) | ((~relation(A!16)) | (~function(A!16)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17))))))))))))) <=> ((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) | (~function(A!16)) | (~relation(A!16)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17))))))))))))),
% 0.20/0.52 inference(transitivity,[status(thm)],[140, 138])).
% 0.20/0.52 tff(142,plain,
% 0.20/0.52 ((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) | ((~relation(A!16)) | (~function(A!16)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17))))))))))))),
% 0.20/0.52 inference(quant_inst,[status(thm)],[])).
% 0.20/0.52 tff(143,plain,
% 0.20/0.52 ((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A), relation_dom(A))) | (~(C = apply(A, tptp_fun_D_0(C, A)))))))) | (~(in(C, B) | (~in(D, relation_dom(A))) | (~(C = apply(A, D))))))))) | (~((B = relation_rng(A)) | (~((~(in(tptp_fun_C_1(B, A), B) | (~((~in(tptp_fun_D_2(B, A), relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, tptp_fun_D_2(B, A)))))))) | (~((~in(tptp_fun_C_1(B, A), B)) | (~in(D_17, relation_dom(A))) | (~(tptp_fun_C_1(B, A) = apply(A, D_17))))))))))))) | (~function(A!16)) | (~relation(A!16)) | ![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[142, 141])).
% 0.20/0.52 tff(144,plain,
% 0.20/0.52 (![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[143, 137, 11, 10])).
% 0.20/0.52 tff(145,plain,
% 0.20/0.52 (((~![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))) | (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16))))))))) <=> ((~![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))) | (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))))))),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(146,plain,
% 0.20/0.52 ((~((~((~(relation_rng(A!16) = relation_rng(A!16))) | (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~(in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))))))) | (~((relation_rng(A!16) = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(relation_rng(A!16), A!16), relation_rng(A!16)) | (~((~in(tptp_fun_D_2(relation_rng(A!16), A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(relation_rng(A!16), A!16) = apply(A!16, tptp_fun_D_2(relation_rng(A!16), A!16)))))))) | (~((~in(tptp_fun_C_1(relation_rng(A!16), A!16), relation_rng(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(relation_rng(A!16), A!16) = apply(A!16, tptp_fun_B_4(A!16)))))))))))) <=> (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16))))))))),
% 0.20/0.53 inference(rewrite,[status(thm)],[])).
% 0.20/0.53 tff(147,plain,
% 0.20/0.53 (((~![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))) | (~((~((~(relation_rng(A!16) = relation_rng(A!16))) | (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~(in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))))))) | (~((relation_rng(A!16) = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(relation_rng(A!16), A!16), relation_rng(A!16)) | (~((~in(tptp_fun_D_2(relation_rng(A!16), A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(relation_rng(A!16), A!16) = apply(A!16, tptp_fun_D_2(relation_rng(A!16), A!16)))))))) | (~((~in(tptp_fun_C_1(relation_rng(A!16), A!16), relation_rng(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(relation_rng(A!16), A!16) = apply(A!16, tptp_fun_B_4(A!16))))))))))))) <=> ((~![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))) | (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))))))),
% 0.20/0.53 inference(monotonicity,[status(thm)],[146])).
% 0.20/0.53 tff(148,plain,
% 0.20/0.53 (((~![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))) | (~((~((~(relation_rng(A!16) = relation_rng(A!16))) | (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~(in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))))))) | (~((relation_rng(A!16) = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(relation_rng(A!16), A!16), relation_rng(A!16)) | (~((~in(tptp_fun_D_2(relation_rng(A!16), A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(relation_rng(A!16), A!16) = apply(A!16, tptp_fun_D_2(relation_rng(A!16), A!16)))))))) | (~((~in(tptp_fun_C_1(relation_rng(A!16), A!16), relation_rng(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(relation_rng(A!16), A!16) = apply(A!16, tptp_fun_B_4(A!16))))))))))))) <=> ((~![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))) | (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))))))),
% 0.20/0.53 inference(transitivity,[status(thm)],[147, 145])).
% 0.20/0.53 tff(149,plain,
% 0.20/0.53 ((~![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))) | (~((~((~(relation_rng(A!16) = relation_rng(A!16))) | (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~(in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))))))) | (~((relation_rng(A!16) = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(relation_rng(A!16), A!16), relation_rng(A!16)) | (~((~in(tptp_fun_D_2(relation_rng(A!16), A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(relation_rng(A!16), A!16) = apply(A!16, tptp_fun_D_2(relation_rng(A!16), A!16)))))))) | (~((~in(tptp_fun_C_1(relation_rng(A!16), A!16), relation_rng(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(relation_rng(A!16), A!16) = apply(A!16, tptp_fun_B_4(A!16))))))))))))),
% 0.20/0.53 inference(quant_inst,[status(thm)],[])).
% 0.20/0.53 tff(150,plain,
% 0.20/0.53 ((~![B: $i, D_17: $i, C: $i, D: $i] : (~((~((~(B = relation_rng(A!16))) | (~((~((~in(C, B)) | (~((~in(tptp_fun_D_0(C, A!16), relation_dom(A!16))) | (~(C = apply(A!16, tptp_fun_D_0(C, A!16)))))))) | (~(in(C, B) | (~in(D, relation_dom(A!16))) | (~(C = apply(A!16, D))))))))) | (~((B = relation_rng(A!16)) | (~((~(in(tptp_fun_C_1(B, A!16), B) | (~((~in(tptp_fun_D_2(B, A!16), relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, tptp_fun_D_2(B, A!16)))))))) | (~((~in(tptp_fun_C_1(B, A!16), B)) | (~in(D_17, relation_dom(A!16))) | (~(tptp_fun_C_1(B, A!16) = apply(A!16, D_17)))))))))))) | (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16))))))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[149, 148])).
% 0.20/0.53 tff(151,plain,
% 0.20/0.53 (~((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[150, 144])).
% 0.20/0.53 tff(152,plain,
% 0.20/0.53 (((~((~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~((~in(tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16), relation_dom(A!16))) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_D_0(apply(A!16, tptp_fun_C_3(A!16)), A!16)))))))) | (~((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16))))))) | ((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))),
% 0.20/0.53 inference(tautology,[status(thm)],[])).
% 0.20/0.53 tff(153,plain,
% 0.20/0.53 ((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16))))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[152, 151])).
% 0.20/0.53 tff(154,plain,
% 0.20/0.53 ((~((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16))))),
% 0.20/0.53 inference(tautology,[status(thm)],[])).
% 0.20/0.53 tff(155,plain,
% 0.20/0.53 ((~((~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)) | (~(apply(A!16, tptp_fun_C_3(A!16)) = apply(A!16, tptp_fun_B_4(A!16)))))) | in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[154, 45, 69])).
% 0.20/0.53 tff(156,plain,
% 0.20/0.53 (in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[155, 153])).
% 0.20/0.53 tff(157,plain,
% 0.20/0.53 (((relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = empty_set) <=> in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16))) | (~(relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = empty_set)) | (~in(apply(A!16, tptp_fun_C_3(A!16)), relation_rng(A!16)))),
% 0.20/0.53 inference(tautology,[status(thm)],[])).
% 0.20/0.53 tff(158,plain,
% 0.20/0.53 (~(relation_inverse_image(A!16, singleton(apply(A!16, tptp_fun_C_3(A!16)))) = empty_set)),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[157, 156, 118])).
% 0.20/0.53 tff(159,plain,
% 0.20/0.53 (~(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set)),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[158, 104])).
% 0.20/0.53 tff(160,plain,
% 0.20/0.53 ((~((relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set) | (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = singleton(tptp_fun_B_4(A!16))))) | (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = empty_set) | (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = singleton(tptp_fun_B_4(A!16)))),
% 0.20/0.53 inference(tautology,[status(thm)],[])).
% 0.20/0.53 tff(161,plain,
% 0.20/0.53 (relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16)))) = singleton(tptp_fun_B_4(A!16))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[160, 159, 100])).
% 0.20/0.53 tff(162,plain,
% 0.20/0.53 (singleton(tptp_fun_B_4(A!16)) = relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_B_4(A!16))))),
% 0.20/0.53 inference(symmetry,[status(thm)],[161])).
% 0.20/0.53 tff(163,plain,
% 0.20/0.53 (singleton(tptp_fun_B_4(A!16)) = relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_C_3(A!16))))),
% 0.20/0.53 inference(transitivity,[status(thm)],[162, 82])).
% 0.20/0.53 tff(164,plain,
% 0.20/0.53 (subset(singleton(tptp_fun_B_4(A!16)), singleton(tptp_fun_C_3(A!16))) <=> subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_C_3(A!16)))), singleton(tptp_fun_C_3(A!16)))),
% 0.20/0.53 inference(monotonicity,[status(thm)],[163])).
% 0.20/0.53 tff(165,plain,
% 0.20/0.53 (subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_C_3(A!16)))), singleton(tptp_fun_C_3(A!16))) <=> subset(singleton(tptp_fun_B_4(A!16)), singleton(tptp_fun_C_3(A!16)))),
% 0.20/0.53 inference(symmetry,[status(thm)],[164])).
% 0.20/0.53 tff(166,plain,
% 0.20/0.53 ((~![B: $i] : subset(relation_inverse_image(A!16, relation_image(A!16, B)), B)) | subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_C_3(A!16)))), singleton(tptp_fun_C_3(A!16)))),
% 0.20/0.53 inference(quant_inst,[status(thm)],[])).
% 0.20/0.53 tff(167,plain,
% 0.20/0.53 (subset(relation_inverse_image(A!16, relation_image(A!16, singleton(tptp_fun_C_3(A!16)))), singleton(tptp_fun_C_3(A!16)))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[166, 95])).
% 0.20/0.53 tff(168,plain,
% 0.20/0.53 (subset(singleton(tptp_fun_B_4(A!16)), singleton(tptp_fun_C_3(A!16)))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[167, 165])).
% 0.20/0.53 tff(169,plain,
% 0.20/0.53 (((~(apply(A!16, tptp_fun_B_4(A!16)) = apply(A!16, tptp_fun_C_3(A!16)))) | (~in(tptp_fun_C_3(A!16), relation_dom(A!16))) | (~in(tptp_fun_B_4(A!16), relation_dom(A!16))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))) | (~(tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))),
% 0.20/0.53 inference(tautology,[status(thm)],[])).
% 0.20/0.53 tff(170,plain,
% 0.20/0.53 (~(tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[169, 43])).
% 0.20/0.53 tff(171,plain,
% 0.20/0.53 (^[A: $i, B: $i] : refl(((~subset(singleton(A), singleton(B))) | (A = B)) <=> ((~subset(singleton(A), singleton(B))) | (A = B)))),
% 0.20/0.53 inference(bind,[status(th)],[])).
% 0.20/0.53 tff(172,plain,
% 0.20/0.53 (![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B)) <=> ![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[171])).
% 0.20/0.53 tff(173,plain,
% 0.20/0.53 (![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B)) <=> ![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))),
% 0.20/0.53 inference(rewrite,[status(thm)],[])).
% 0.20/0.53 tff(174,plain,
% 0.20/0.53 (^[A: $i, B: $i] : rewrite((subset(singleton(A), singleton(B)) => (A = B)) <=> ((~subset(singleton(A), singleton(B))) | (A = B)))),
% 0.20/0.53 inference(bind,[status(th)],[])).
% 0.20/0.53 tff(175,plain,
% 0.20/0.53 (![A: $i, B: $i] : (subset(singleton(A), singleton(B)) => (A = B)) <=> ![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[174])).
% 0.20/0.53 tff(176,axiom,(![A: $i, B: $i] : (subset(singleton(A), singleton(B)) => (A = B))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t6_zfmisc_1')).
% 0.20/0.53 tff(177,plain,
% 0.20/0.53 (![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[176, 175])).
% 0.20/0.53 tff(178,plain,
% 0.20/0.53 (![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[177, 173])).
% 0.20/0.53 tff(179,plain,(
% 0.20/0.53 ![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))),
% 0.20/0.53 inference(skolemize,[status(sab)],[178])).
% 0.20/0.53 tff(180,plain,
% 0.20/0.53 (![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[179, 172])).
% 0.20/0.53 tff(181,plain,
% 0.20/0.53 (((~![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))) | ((~subset(singleton(tptp_fun_B_4(A!16)), singleton(tptp_fun_C_3(A!16)))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))) <=> ((~![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))) | (~subset(singleton(tptp_fun_B_4(A!16)), singleton(tptp_fun_C_3(A!16)))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))),
% 0.20/0.53 inference(rewrite,[status(thm)],[])).
% 0.20/0.53 tff(182,plain,
% 0.20/0.53 ((~![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))) | ((~subset(singleton(tptp_fun_B_4(A!16)), singleton(tptp_fun_C_3(A!16)))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16)))),
% 0.20/0.53 inference(quant_inst,[status(thm)],[])).
% 0.20/0.53 tff(183,plain,
% 0.20/0.53 ((~![A: $i, B: $i] : ((~subset(singleton(A), singleton(B))) | (A = B))) | (~subset(singleton(tptp_fun_B_4(A!16)), singleton(tptp_fun_C_3(A!16)))) | (tptp_fun_B_4(A!16) = tptp_fun_C_3(A!16))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[182, 181])).
% 0.20/0.53 tff(184,plain,
% 0.20/0.53 (~subset(singleton(tptp_fun_B_4(A!16)), singleton(tptp_fun_C_3(A!16)))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[183, 180, 170])).
% 0.20/0.53 tff(185,plain,
% 0.20/0.53 ($false),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[184, 168])).
% 0.20/0.53 % SZS output end Proof
% 0.20/0.54 % E exiting
%------------------------------------------------------------------------------