%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU226+2 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:27:18 AM UTC 2025
% Result : Theorem 244.10s 244.33s
% Output : Proof 244.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SEU226+2 : TPTP v9.0.0. Released v3.3.0.
% 0.04/0.13 % Command : run_E %s %d THM
% 0.14/0.35 % Computer : n001.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Fri Jun 20 06:27:05 EDT 2025
% 0.14/0.35 % CPUTime :
% 244.10/244.33 % SZS status Theorem
% 244.10/244.33 % SZS output start Proof
% 244.10/244.33 tff(in_type, type, (
% 244.10/244.33 in: ( $i * $i ) > $o)).
% 244.10/244.33 tff(tptp_fun_A_71_type, type, (
% 244.10/244.33 tptp_fun_A_71: $i)).
% 244.10/244.33 tff(apply_type, type, (
% 244.10/244.33 apply: ( $i * $i ) > $i)).
% 244.10/244.33 tff(tptp_fun_D_69_type, type, (
% 244.10/244.33 tptp_fun_D_69: ( $i * $i * $i ) > $i)).
% 244.10/244.33 tff(tptp_fun_C_36_type, type, (
% 244.10/244.33 tptp_fun_C_36: ( $i * $i ) > $i)).
% 244.10/244.33 tff(relation_image_type, type, (
% 244.10/244.33 relation_image: ( $i * $i ) > $i)).
% 244.10/244.33 tff(relation_inverse_image_type, type, (
% 244.10/244.33 relation_inverse_image: ( $i * $i ) > $i)).
% 244.10/244.33 tff(tptp_fun_B_70_type, type, (
% 244.10/244.33 tptp_fun_B_70: $i)).
% 244.10/244.33 tff(relation_dom_type, type, (
% 244.10/244.33 relation_dom: $i > $i)).
% 244.10/244.33 tff(ordered_pair_type, type, (
% 244.10/244.33 ordered_pair: ( $i * $i ) > $i)).
% 244.10/244.33 tff(function_type, type, (
% 244.10/244.33 function: $i > $o)).
% 244.10/244.33 tff(relation_type, type, (
% 244.10/244.33 relation: $i > $o)).
% 244.10/244.33 tff(subset_type, type, (
% 244.10/244.33 subset: ( $i * $i ) > $o)).
% 244.10/244.33 tff(tptp_fun_D_9_type, type, (
% 244.10/244.33 tptp_fun_D_9: ( $i * $i * $i ) > $i)).
% 244.10/244.33 tff(1,plain,
% 244.10/244.33 (^[A: $i, B: $i, C: $i] : refl(((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))) <=> ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))))),
% 244.10/244.33 inference(bind,[status(th)],[])).
% 244.10/244.33 tff(2,plain,
% 244.10/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))) <=> ![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))),
% 244.10/244.33 inference(quant_intro,[status(thm)],[1])).
% 244.10/244.33 tff(3,plain,
% 244.10/244.33 (^[A: $i, B: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((relation(C) & function(C)) <=> (~((~relation(C)) | (~function(C))))), ((~(relation(C) & function(C))) <=> (~(~((~relation(C)) | (~function(C))))))), rewrite((~(~((~relation(C)) | (~function(C))))) <=> ((~relation(C)) | (~function(C)))), ((~(relation(C) & function(C))) <=> ((~relation(C)) | (~function(C))))), trans(trans(monotonicity(rewrite((in(A, relation_dom(C)) & (B = apply(C, A))) <=> (~((~in(A, relation_dom(C))) | (~(B = apply(C, A)))))), ((in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))) <=> (in(ordered_pair(A, B), C) <=> (~((~in(A, relation_dom(C))) | (~(B = apply(C, A)))))))), rewrite((in(ordered_pair(A, B), C) <=> (~((~in(A, relation_dom(C))) | (~(B = apply(C, A)))))) <=> (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))), ((in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))) <=> (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))), rewrite((~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))) <=> (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))), ((in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))) <=> (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))), (((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> (((~relation(C)) | (~function(C))) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))))), rewrite((((~relation(C)) | (~function(C))) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C)))) <=> ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))), (((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))))),
% 244.10/244.33 inference(bind,[status(th)],[])).
% 244.10/244.33 tff(4,plain,
% 244.10/244.33 (![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> ![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))),
% 244.10/244.33 inference(quant_intro,[status(thm)],[3])).
% 244.10/244.33 tff(5,plain,
% 244.10/244.33 (![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> ![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))),
% 244.10/244.33 inference(rewrite,[status(thm)],[])).
% 244.10/244.33 tff(6,plain,
% 244.10/244.33 (^[A: $i, B: $i, C: $i] : rewrite(((relation(C) & function(C)) => (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))))),
% 244.10/244.33 inference(bind,[status(th)],[])).
% 244.10/244.33 tff(7,plain,
% 244.10/244.33 (![A: $i, B: $i, C: $i] : ((relation(C) & function(C)) => (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A))))) <=> ![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))),
% 244.16/244.33 inference(quant_intro,[status(thm)],[6])).
% 244.16/244.33 tff(8,axiom,(![A: $i, B: $i, C: $i] : ((relation(C) & function(C)) => (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t8_funct_1')).
% 244.16/244.33 tff(9,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[8, 7])).
% 244.16/244.33 tff(10,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[9, 5])).
% 244.16/244.33 tff(11,plain,(
% 244.16/244.33 ![A: $i, B: $i, C: $i] : ((~(relation(C) & function(C))) | (in(ordered_pair(A, B), C) <=> (in(A, relation_dom(C)) & (B = apply(C, A)))))),
% 244.16/244.33 inference(skolemize,[status(sab)],[10])).
% 244.16/244.33 tff(12,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[11, 4])).
% 244.16/244.33 tff(13,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[12, 2])).
% 244.16/244.33 tff(14,plain,
% 244.16/244.33 ((~![A: $i, B: $i] : ((~(relation(B) & function(B))) | subset(relation_image(B, relation_inverse_image(B, A)), A))) <=> (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | subset(relation_image(B, relation_inverse_image(B, A)), A)))),
% 244.16/244.33 inference(rewrite,[status(thm)],[])).
% 244.16/244.33 tff(15,plain,
% 244.16/244.33 ((~![A: $i, B: $i] : ((relation(B) & function(B)) => subset(relation_image(B, relation_inverse_image(B, A)), A))) <=> (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | subset(relation_image(B, relation_inverse_image(B, A)), A)))),
% 244.16/244.33 inference(rewrite,[status(thm)],[])).
% 244.16/244.33 tff(16,axiom,(~![A: $i, B: $i] : ((relation(B) & function(B)) => subset(relation_image(B, relation_inverse_image(B, A)), A))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t145_funct_1')).
% 244.16/244.33 tff(17,plain,
% 244.16/244.33 (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | subset(relation_image(B, relation_inverse_image(B, A)), A))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[16, 15])).
% 244.16/244.33 tff(18,plain,
% 244.16/244.33 (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | subset(relation_image(B, relation_inverse_image(B, A)), A))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[17, 14])).
% 244.16/244.33 tff(19,plain,
% 244.16/244.33 (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | subset(relation_image(B, relation_inverse_image(B, A)), A))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[18, 14])).
% 244.16/244.33 tff(20,plain,
% 244.16/244.33 (~![A: $i, B: $i] : ((~(relation(B) & function(B))) | subset(relation_image(B, relation_inverse_image(B, A)), A))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[19, 14])).
% 244.16/244.33 tff(21,plain,(
% 244.16/244.33 ~((~(relation(B!70) & function(B!70))) | subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71))),
% 244.16/244.33 inference(skolemize,[status(sab)],[20])).
% 244.16/244.33 tff(22,plain,
% 244.16/244.33 (relation(B!70) & function(B!70)),
% 244.16/244.33 inference(or_elim,[status(thm)],[21])).
% 244.16/244.33 tff(23,plain,
% 244.16/244.33 (function(B!70)),
% 244.16/244.33 inference(and_elim,[status(thm)],[22])).
% 244.16/244.33 tff(24,plain,
% 244.16/244.33 (relation(B!70)),
% 244.16/244.33 inference(and_elim,[status(thm)],[22])).
% 244.16/244.33 tff(25,plain,
% 244.16/244.33 (((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | ((~relation(B!70)) | (~function(B!70)) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))))))) <=> in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))) <=> ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | (~relation(B!70)) | (~function(B!70)) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))))))) <=> in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))),
% 244.16/244.33 inference(rewrite,[status(thm)],[])).
% 244.16/244.33 tff(26,plain,
% 244.16/244.33 ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | ((~relation(B!70)) | (~function(B!70)) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))))))) <=> in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))),
% 244.16/244.33 inference(quant_inst,[status(thm)],[])).
% 244.16/244.33 tff(27,plain,
% 244.16/244.33 ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~function(C)) | (~(((~in(A, relation_dom(C))) | (~(B = apply(C, A)))) <=> in(ordered_pair(A, B), C))))) | (~relation(B!70)) | (~function(B!70)) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))))))) <=> in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[26, 25])).
% 244.16/244.33 tff(28,plain,
% 244.16/244.33 (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))))))) <=> in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))),
% 244.16/244.33 inference(unit_resolution,[status(thm)],[27, 24, 23, 13])).
% 244.16/244.33 tff(29,plain,
% 244.16/244.33 (^[A: $i, B: $i, C: $i] : refl(((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C)))))))) <=> ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C)))))))))),
% 244.16/244.33 inference(bind,[status(th)],[])).
% 244.16/244.33 tff(30,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C)))))))) <=> ![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))),
% 244.16/244.33 inference(quant_intro,[status(thm)],[29])).
% 244.16/244.33 tff(31,plain,
% 244.16/244.33 (^[A: $i, B: $i, C: $i] : rewrite(((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C)))))))) <=> ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C)))))))))),
% 244.16/244.33 inference(bind,[status(th)],[])).
% 244.16/244.33 tff(32,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C)))))))) <=> ![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))),
% 244.16/244.33 inference(quant_intro,[status(thm)],[31])).
% 244.16/244.33 tff(33,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C)))))))) <=> ![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))),
% 244.16/244.33 inference(transitivity,[status(thm)],[32, 30])).
% 244.16/244.33 tff(34,plain,
% 244.16/244.33 (^[A: $i, B: $i, C: $i] : rewrite(((~relation(C)) | (((~in(A, relation_image(C, B))) | (in(tptp_fun_D_69(C, B, A), relation_dom(C)) & in(ordered_pair(tptp_fun_D_69(C, B, A), A), C) & in(tptp_fun_D_69(C, B, A), B))) & (in(A, relation_image(C, B)) | ![D: $i] : (~(in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B)))))) <=> ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C)))))))))),
% 244.16/244.33 inference(bind,[status(th)],[])).
% 244.16/244.33 tff(35,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (((~in(A, relation_image(C, B))) | (in(tptp_fun_D_69(C, B, A), relation_dom(C)) & in(ordered_pair(tptp_fun_D_69(C, B, A), A), C) & in(tptp_fun_D_69(C, B, A), B))) & (in(A, relation_image(C, B)) | ![D: $i] : (~(in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B)))))) <=> ![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))),
% 244.16/244.33 inference(quant_intro,[status(thm)],[34])).
% 244.16/244.33 tff(36,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (in(A, relation_image(C, B)) <=> ?[D: $i] : (in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B)))) <=> ![A: $i, B: $i, C: $i] : ((~relation(C)) | (in(A, relation_image(C, B)) <=> ?[D: $i] : (in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B))))),
% 244.16/244.33 inference(rewrite,[status(thm)],[])).
% 244.16/244.33 tff(37,plain,
% 244.16/244.33 (^[A: $i, B: $i, C: $i] : trans(monotonicity(rewrite((in(A, relation_image(C, B)) <=> ?[D: $i] : ((in(D, relation_dom(C)) & in(ordered_pair(D, A), C)) & in(D, B))) <=> (in(A, relation_image(C, B)) <=> ?[D: $i] : (in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B)))), ((relation(C) => (in(A, relation_image(C, B)) <=> ?[D: $i] : ((in(D, relation_dom(C)) & in(ordered_pair(D, A), C)) & in(D, B)))) <=> (relation(C) => (in(A, relation_image(C, B)) <=> ?[D: $i] : (in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B)))))), rewrite((relation(C) => (in(A, relation_image(C, B)) <=> ?[D: $i] : (in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B)))) <=> ((~relation(C)) | (in(A, relation_image(C, B)) <=> ?[D: $i] : (in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B))))), ((relation(C) => (in(A, relation_image(C, B)) <=> ?[D: $i] : ((in(D, relation_dom(C)) & in(ordered_pair(D, A), C)) & in(D, B)))) <=> ((~relation(C)) | (in(A, relation_image(C, B)) <=> ?[D: $i] : (in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B))))))),
% 244.16/244.33 inference(bind,[status(th)],[])).
% 244.16/244.33 tff(38,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : (relation(C) => (in(A, relation_image(C, B)) <=> ?[D: $i] : ((in(D, relation_dom(C)) & in(ordered_pair(D, A), C)) & in(D, B)))) <=> ![A: $i, B: $i, C: $i] : ((~relation(C)) | (in(A, relation_image(C, B)) <=> ?[D: $i] : (in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B))))),
% 244.16/244.33 inference(quant_intro,[status(thm)],[37])).
% 244.16/244.33 tff(39,axiom,(![A: $i, B: $i, C: $i] : (relation(C) => (in(A, relation_image(C, B)) <=> ?[D: $i] : ((in(D, relation_dom(C)) & in(ordered_pair(D, A), C)) & in(D, B))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t143_relat_1')).
% 244.16/244.33 tff(40,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (in(A, relation_image(C, B)) <=> ?[D: $i] : (in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B))))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[39, 38])).
% 244.16/244.33 tff(41,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (in(A, relation_image(C, B)) <=> ?[D: $i] : (in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B))))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[40, 36])).
% 244.16/244.33 tff(42,plain,(
% 244.16/244.33 ![A: $i, B: $i, C: $i] : ((~relation(C)) | (((~in(A, relation_image(C, B))) | (in(tptp_fun_D_69(C, B, A), relation_dom(C)) & in(ordered_pair(tptp_fun_D_69(C, B, A), A), C) & in(tptp_fun_D_69(C, B, A), B))) & (in(A, relation_image(C, B)) | ![D: $i] : (~(in(D, relation_dom(C)) & in(ordered_pair(D, A), C) & in(D, B))))))),
% 244.16/244.33 inference(skolemize,[status(sab)],[41])).
% 244.16/244.33 tff(43,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[42, 35])).
% 244.16/244.33 tff(44,plain,
% 244.16/244.33 (![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))),
% 244.16/244.33 inference(modus_ponens,[status(thm)],[43, 33])).
% 244.16/244.33 tff(45,plain,
% 244.16/244.33 (((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))) | ((~relation(B!70)) | (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_dom(B!70))) | (~in(D, relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))))))) <=> ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))) | (~relation(B!70)) | (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_dom(B!70))) | (~in(D, relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))))))),
% 244.16/244.34 inference(rewrite,[status(thm)],[])).
% 244.16/244.34 tff(46,plain,
% 244.16/244.34 (((~relation(B!70)) | (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_inverse_image(B!70, A!71))) | (~in(D, relation_dom(B!70))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)))))))) <=> ((~relation(B!70)) | (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_dom(B!70))) | (~in(D, relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))))))),
% 244.16/244.34 inference(rewrite,[status(thm)],[])).
% 244.16/244.34 tff(47,plain,
% 244.16/244.34 (((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))) | ((~relation(B!70)) | (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_inverse_image(B!70, A!71))) | (~in(D, relation_dom(B!70))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))))))) <=> ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))) | ((~relation(B!70)) | (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_dom(B!70))) | (~in(D, relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)))))))))),
% 244.16/244.34 inference(monotonicity,[status(thm)],[46])).
% 244.16/244.34 tff(48,plain,
% 244.16/244.34 (((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))) | ((~relation(B!70)) | (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_inverse_image(B!70, A!71))) | (~in(D, relation_dom(B!70))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))))))) <=> ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))) | (~relation(B!70)) | (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_dom(B!70))) | (~in(D, relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))))))),
% 244.16/244.34 inference(transitivity,[status(thm)],[47, 45])).
% 244.16/244.34 tff(49,plain,
% 244.16/244.34 ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))) | ((~relation(B!70)) | (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_inverse_image(B!70, A!71))) | (~in(D, relation_dom(B!70))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))))))),
% 244.16/244.34 inference(quant_inst,[status(thm)],[])).
% 244.16/244.34 tff(50,plain,
% 244.16/244.34 ((~![A: $i, B: $i, C: $i] : ((~relation(C)) | (~((~((~in(A, relation_image(C, B))) | (~((~in(tptp_fun_D_69(C, B, A), relation_dom(C))) | (~in(ordered_pair(tptp_fun_D_69(C, B, A), A), C)) | (~in(tptp_fun_D_69(C, B, A), B)))))) | (~(in(A, relation_image(C, B)) | ![D: $i] : ((~in(D, B)) | (~in(D, relation_dom(C))) | (~in(ordered_pair(D, A), C))))))))) | (~relation(B!70)) | (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_dom(B!70))) | (~in(D, relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)))))))),
% 244.16/244.34 inference(modus_ponens,[status(thm)],[49, 48])).
% 244.16/244.34 tff(51,plain,
% 244.16/244.34 (~((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_dom(B!70))) | (~in(D, relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))))))),
% 244.16/244.34 inference(unit_resolution,[status(thm)],[50, 44, 24])).
% 244.16/244.34 tff(52,plain,
% 244.16/244.34 (((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))) | (~(in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71))) | ![D: $i] : ((~in(D, relation_dom(B!70))) | (~in(D, relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(D, tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)))))) | ((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))),
% 244.16/244.34 inference(tautology,[status(thm)],[])).
% 244.16/244.34 tff(53,plain,
% 244.16/244.34 ((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70)))))),
% 244.16/244.34 inference(unit_resolution,[status(thm)],[52, 51])).
% 244.16/244.34 tff(54,plain,
% 244.16/244.34 (^[A: $i, B: $i] : refl((~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))))) <=> (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))))))),
% 244.16/244.34 inference(bind,[status(th)],[])).
% 244.16/244.34 tff(55,plain,
% 244.16/244.34 (![A: $i, B: $i] : (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))))) <=> ![A: $i, B: $i] : (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))))))),
% 244.16/244.34 inference(quant_intro,[status(thm)],[54])).
% 244.16/244.34 tff(56,plain,
% 244.16/244.34 (^[A: $i, B: $i] : rewrite((~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))))) <=> (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))))))),
% 244.16/244.34 inference(bind,[status(th)],[])).
% 244.16/244.34 tff(57,plain,
% 244.16/244.34 (![A: $i, B: $i] : (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))))) <=> ![A: $i, B: $i] : (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))))))),
% 244.16/244.34 inference(quant_intro,[status(thm)],[56])).
% 244.16/244.34 tff(58,plain,
% 244.16/244.34 (![A: $i, B: $i] : (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))))) <=> ![A: $i, B: $i] : (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))))))),
% 244.16/244.34 inference(transitivity,[status(thm)],[57, 55])).
% 244.16/244.34 tff(59,plain,
% 244.16/244.34 (^[A: $i, B: $i] : trans(monotonicity(rewrite(((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B))) <=> ((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))), rewrite((subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))) <=> (subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))), ((((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B))) & (subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))) <=> (((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B))) & (subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))))), rewrite((((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B))) & (subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))) <=> (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))))))), ((((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B))) & (subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))) <=> (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))))))))),
% 244.16/244.34 inference(bind,[status(th)],[])).
% 244.16/244.34 tff(60,plain,
% 244.16/244.34 (![A: $i, B: $i] : (((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B))) & (subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B))))) <=> ![A: $i, B: $i] : (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))))))),
% 244.16/244.34 inference(quant_intro,[status(thm)],[59])).
% 244.16/244.34 tff(61,plain,
% 244.16/244.34 (![A: $i, B: $i] : (subset(A, B) <=> ![C: $i] : ((~in(C, A)) | in(C, B))) <=> ![A: $i, B: $i] : (subset(A, B) <=> ![C: $i] : ((~in(C, A)) | in(C, B)))),
% 244.16/244.34 inference(rewrite,[status(thm)],[])).
% 244.16/244.34 tff(62,plain,
% 244.16/244.34 (^[A: $i, B: $i] : rewrite((subset(A, B) <=> ![C: $i] : (in(C, A) => in(C, B))) <=> (subset(A, B) <=> ![C: $i] : ((~in(C, A)) | in(C, B))))),
% 244.16/244.34 inference(bind,[status(th)],[])).
% 244.16/244.34 tff(63,plain,
% 244.16/244.34 (![A: $i, B: $i] : (subset(A, B) <=> ![C: $i] : (in(C, A) => in(C, B))) <=> ![A: $i, B: $i] : (subset(A, B) <=> ![C: $i] : ((~in(C, A)) | in(C, B)))),
% 244.16/244.34 inference(quant_intro,[status(thm)],[62])).
% 244.16/244.34 tff(64,axiom,(![A: $i, B: $i] : (subset(A, B) <=> ![C: $i] : (in(C, A) => in(C, B)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','d3_tarski')).
% 244.16/244.34 tff(65,plain,
% 244.16/244.34 (![A: $i, B: $i] : (subset(A, B) <=> ![C: $i] : ((~in(C, A)) | in(C, B)))),
% 244.16/244.34 inference(modus_ponens,[status(thm)],[64, 63])).
% 244.16/244.34 tff(66,plain,
% 244.16/244.34 (![A: $i, B: $i] : (subset(A, B) <=> ![C: $i] : ((~in(C, A)) | in(C, B)))),
% 244.16/244.34 inference(modus_ponens,[status(thm)],[65, 61])).
% 244.16/244.34 tff(67,plain,(
% 244.16/244.34 ![A: $i, B: $i] : (((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B))) & (subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))))),
% 244.16/244.34 inference(skolemize,[status(sab)],[66])).
% 244.16/244.34 tff(68,plain,
% 244.16/244.34 (![A: $i, B: $i] : (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))))))),
% 244.16/244.34 inference(modus_ponens,[status(thm)],[67, 60])).
% 244.16/244.34 tff(69,plain,
% 244.16/244.34 (![A: $i, B: $i] : (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))))))),
% 244.16/244.34 inference(modus_ponens,[status(thm)],[68, 58])).
% 244.16/244.34 tff(70,plain,
% 244.16/244.34 ((~![A: $i, B: $i] : (~((~((~subset(A, B)) | ![C: $i] : ((~in(C, A)) | in(C, B)))) | (~(subset(A, B) | (~((~in(tptp_fun_C_36(B, A), A)) | in(tptp_fun_C_36(B, A), B)))))))) | (~((~((~subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71)) | ![C: $i] : ((~in(C, relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(C, A!71)))) | (~(subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71) | (~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71)))))))),
% 244.16/244.34 inference(quant_inst,[status(thm)],[])).
% 244.16/244.34 tff(71,plain,
% 244.16/244.34 (~((~((~subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71)) | ![C: $i] : ((~in(C, relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(C, A!71)))) | (~(subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71) | (~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71))))))),
% 244.16/244.34 inference(unit_resolution,[status(thm)],[70, 69])).
% 244.16/244.34 tff(72,plain,
% 244.16/244.34 (((~((~subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71)) | ![C: $i] : ((~in(C, relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(C, A!71)))) | (~(subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71) | (~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71)))))) | (subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71) | (~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71))))),
% 244.16/244.34 inference(tautology,[status(thm)],[])).
% 244.16/244.34 tff(73,plain,
% 244.16/244.34 (subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71) | (~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71)))),
% 244.16/244.34 inference(unit_resolution,[status(thm)],[72, 71])).
% 244.16/244.34 tff(74,plain,
% 244.16/244.34 (~subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71)),
% 244.16/244.34 inference(or_elim,[status(thm)],[21])).
% 244.16/244.34 tff(75,plain,
% 244.16/244.34 ((~(subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71) | (~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71))))) | subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71) | (~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71)))),
% 244.16/244.34 inference(tautology,[status(thm)],[])).
% 244.16/244.34 tff(76,plain,
% 244.16/244.34 ((~(subset(relation_image(B!70, relation_inverse_image(B!70, A!71)), A!71) | (~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71))))) | (~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71)))),
% 244.16/244.34 inference(unit_resolution,[status(thm)],[75, 74])).
% 244.16/244.34 tff(77,plain,
% 244.16/244.34 (~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71))),
% 244.16/244.34 inference(unit_resolution,[status(thm)],[76, 73])).
% 244.16/244.34 tff(78,plain,
% 244.16/244.34 (((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71)) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))),
% 244.16/244.34 inference(tautology,[status(thm)],[])).
% 244.16/244.34 tff(79,plain,
% 244.16/244.34 (in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))),
% 244.16/244.34 inference(unit_resolution,[status(thm)],[78, 77])).
% 244.16/244.34 tff(80,plain,
% 244.16/244.34 ((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))) | (~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70)))))),
% 244.16/244.34 inference(tautology,[status(thm)],[])).
% 244.16/244.34 tff(81,plain,
% 244.16/244.34 ((~((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70)))))),
% 244.16/244.35 inference(unit_resolution,[status(thm)],[80, 79])).
% 244.16/244.35 tff(82,plain,
% 244.16/244.35 (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))))),
% 244.16/244.35 inference(unit_resolution,[status(thm)],[81, 53])).
% 244.16/244.35 tff(83,plain,
% 244.16/244.35 (((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70)))) | in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)),
% 244.16/244.35 inference(tautology,[status(thm)],[])).
% 244.16/244.35 tff(84,plain,
% 244.16/244.35 (in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)),
% 244.16/244.35 inference(unit_resolution,[status(thm)],[83, 82])).
% 244.16/244.35 tff(85,plain,
% 244.16/244.35 ((((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))))))) <=> in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))))))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70))),
% 244.16/244.35 inference(tautology,[status(thm)],[])).
% 244.16/244.35 tff(86,plain,
% 244.16/244.35 ((((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))))))) <=> in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))))))))),
% 244.16/244.35 inference(unit_resolution,[status(thm)],[85, 84])).
% 244.16/244.35 tff(87,plain,
% 244.16/244.35 (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))))))),
% 244.16/244.35 inference(unit_resolution,[status(thm)],[86, 28])).
% 244.16/244.35 tff(88,plain,
% 244.16/244.35 (((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))))))) | (tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))))),
% 244.16/244.35 inference(tautology,[status(thm)],[])).
% 244.16/244.35 tff(89,plain,
% 244.16/244.35 (tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))) = apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))))),
% 244.16/244.35 inference(unit_resolution,[status(thm)],[88, 87])).
% 244.16/244.35 tff(90,plain,
% 244.16/244.35 (apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))) = tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))),
% 244.16/244.35 inference(symmetry,[status(thm)],[89])).
% 244.16/244.35 tff(91,plain,
% 244.16/244.35 (in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71) <=> in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71)),
% 244.16/244.35 inference(monotonicity,[status(thm)],[90])).
% 244.16/244.35 tff(92,plain,
% 244.16/244.35 (in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71) <=> in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71)),
% 244.16/244.35 inference(symmetry,[status(thm)],[91])).
% 244.16/244.35 tff(93,plain,
% 244.16/244.35 ((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71)) <=> (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))),
% 244.16/244.35 inference(monotonicity,[status(thm)],[92])).
% 244.16/244.35 tff(94,plain,
% 244.16/244.35 (((~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), relation_image(B!70, relation_inverse_image(B!70, A!71)))) | in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71)) | (~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71))),
% 244.16/244.35 inference(tautology,[status(thm)],[])).
% 244.16/244.35 tff(95,plain,
% 244.16/244.35 (~in(tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))), A!71)),
% 244.16/244.35 inference(unit_resolution,[status(thm)],[94, 77])).
% 244.16/244.35 tff(96,plain,
% 244.16/244.35 (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71)),
% 244.16/244.35 inference(modus_ponens,[status(thm)],[95, 93])).
% 244.16/244.35 tff(97,plain,
% 244.16/244.35 (^[A: $i] : refl(((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))))),
% 244.16/244.35 inference(bind,[status(th)],[])).
% 244.16/244.35 tff(98,plain,
% 244.16/244.35 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))),
% 244.16/244.35 inference(quant_intro,[status(thm)],[97])).
% 244.16/244.35 tff(99,plain,
% 244.16/244.35 (^[A: $i] : rewrite(((~relation(A)) | (~function(A)) | ![B: $i, C: $i] : (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))))),
% 244.16/244.35 inference(bind,[status(th)],[])).
% 244.16/244.35 tff(100,plain,
% 244.16/244.35 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i] : (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))),
% 244.16/244.35 inference(quant_intro,[status(thm)],[99])).
% 244.16/244.35 tff(101,plain,
% 244.16/244.35 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i] : (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))),
% 244.16/244.35 inference(transitivity,[status(thm)],[100, 98])).
% 244.16/244.35 tff(102,plain,
% 244.16/244.35 (^[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, C: $i] : trans(monotonicity(rewrite(((~(C = relation_inverse_image(A, B))) | ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))) <=> ((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))), rewrite(((C = relation_inverse_image(A, B)) | (~(in(tptp_fun_D_9(C, B, A), C) <=> (in(tptp_fun_D_9(C, B, A), relation_dom(A)) & in(apply(A, tptp_fun_D_9(C, B, A)), B))))) <=> ((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))), ((((~(C = relation_inverse_image(A, B))) | ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))) & ((C = relation_inverse_image(A, B)) | (~(in(tptp_fun_D_9(C, B, A), C) <=> (in(tptp_fun_D_9(C, B, A), relation_dom(A)) & in(apply(A, tptp_fun_D_9(C, B, A)), B)))))) <=> (((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C)))) & ((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))), rewrite((((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C)))) & ((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))) <=> (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))), ((((~(C = relation_inverse_image(A, B))) | ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))) & ((C = relation_inverse_image(A, B)) | (~(in(tptp_fun_D_9(C, B, A), C) <=> (in(tptp_fun_D_9(C, B, A), relation_dom(A)) & in(apply(A, tptp_fun_D_9(C, B, A)), B)))))) <=> (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))))), (![B: $i, C: $i] : (((~(C = relation_inverse_image(A, B))) | ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))) & ((C = relation_inverse_image(A, B)) | (~(in(tptp_fun_D_9(C, B, A), C) <=> (in(tptp_fun_D_9(C, B, A), relation_dom(A)) & in(apply(A, tptp_fun_D_9(C, B, A)), B)))))) <=> ![B: $i, C: $i] : (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))), (((~(relation(A) & function(A))) | ![B: $i, C: $i] : (((~(C = relation_inverse_image(A, B))) | ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))) & ((C = relation_inverse_image(A, B)) | (~(in(tptp_fun_D_9(C, B, A), C) <=> (in(tptp_fun_D_9(C, B, A), relation_dom(A)) & in(apply(A, tptp_fun_D_9(C, B, A)), B))))))) <=> (((~relation(A)) | (~function(A))) | ![B: $i, C: $i] : (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))))), rewrite((((~relation(A)) | (~function(A))) | ![B: $i, C: $i] : (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i, C: $i] : (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))), (((~(relation(A) & function(A))) | ![B: $i, C: $i] : (((~(C = relation_inverse_image(A, B))) | ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))) & ((C = relation_inverse_image(A, B)) | (~(in(tptp_fun_D_9(C, B, A), C) <=> (in(tptp_fun_D_9(C, B, A), relation_dom(A)) & in(apply(A, tptp_fun_D_9(C, B, A)), B))))))) <=> ((~relation(A)) | (~function(A)) | ![B: $i, C: $i] : (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))))),
% 244.16/244.35 inference(bind,[status(th)],[])).
% 244.16/244.35 tff(103,plain,
% 244.16/244.35 (![A: $i] : ((~(relation(A) & function(A))) | ![B: $i, C: $i] : (((~(C = relation_inverse_image(A, B))) | ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))) & ((C = relation_inverse_image(A, B)) | (~(in(tptp_fun_D_9(C, B, A), C) <=> (in(tptp_fun_D_9(C, B, A), relation_dom(A)) & in(apply(A, tptp_fun_D_9(C, B, A)), B))))))) <=> ![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i] : (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))),
% 244.16/244.35 inference(quant_intro,[status(thm)],[102])).
% 244.16/244.35 tff(104,plain,
% 244.16/244.35 (![A: $i] : ((~(relation(A) & function(A))) | ![B: $i, C: $i] : ((C = relation_inverse_image(A, B)) <=> ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B))))) <=> ![A: $i] : ((~(relation(A) & function(A))) | ![B: $i, C: $i] : ((C = relation_inverse_image(A, B)) <=> ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))))),
% 244.16/244.35 inference(rewrite,[status(thm)],[])).
% 244.16/244.35 tff(105,plain,
% 244.16/244.35 (^[A: $i] : rewrite(((relation(A) & function(A)) => ![B: $i, C: $i] : ((C = relation_inverse_image(A, B)) <=> ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B))))) <=> ((~(relation(A) & function(A))) | ![B: $i, C: $i] : ((C = relation_inverse_image(A, B)) <=> ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B))))))),
% 244.16/244.35 inference(bind,[status(th)],[])).
% 244.16/244.35 tff(106,plain,
% 244.16/244.35 (![A: $i] : ((relation(A) & function(A)) => ![B: $i, C: $i] : ((C = relation_inverse_image(A, B)) <=> ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B))))) <=> ![A: $i] : ((~(relation(A) & function(A))) | ![B: $i, C: $i] : ((C = relation_inverse_image(A, B)) <=> ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))))),
% 244.16/244.35 inference(quant_intro,[status(thm)],[105])).
% 244.16/244.35 tff(107,axiom,(![A: $i] : ((relation(A) & function(A)) => ![B: $i, C: $i] : ((C = relation_inverse_image(A, B)) <=> ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','d13_funct_1')).
% 244.16/244.35 tff(108,plain,
% 244.16/244.35 (![A: $i] : ((~(relation(A) & function(A))) | ![B: $i, C: $i] : ((C = relation_inverse_image(A, B)) <=> ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))))),
% 244.16/244.35 inference(modus_ponens,[status(thm)],[107, 106])).
% 244.16/244.35 tff(109,plain,
% 244.16/244.35 (![A: $i] : ((~(relation(A) & function(A))) | ![B: $i, C: $i] : ((C = relation_inverse_image(A, B)) <=> ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))))),
% 244.16/244.35 inference(modus_ponens,[status(thm)],[108, 104])).
% 244.16/244.35 tff(110,plain,(
% 244.16/244.35 ![A: $i] : ((~(relation(A) & function(A))) | ![B: $i, C: $i] : (((~(C = relation_inverse_image(A, B))) | ![D: $i] : (in(D, C) <=> (in(D, relation_dom(A)) & in(apply(A, D), B)))) & ((C = relation_inverse_image(A, B)) | (~(in(tptp_fun_D_9(C, B, A), C) <=> (in(tptp_fun_D_9(C, B, A), relation_dom(A)) & in(apply(A, tptp_fun_D_9(C, B, A)), B)))))))),
% 244.16/244.35 inference(skolemize,[status(sab)],[109])).
% 244.16/244.35 tff(111,plain,
% 244.16/244.35 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i] : (~((~((~(C = relation_inverse_image(A, B))) | ![D: $i] : (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))),
% 244.16/244.35 inference(modus_ponens,[status(thm)],[110, 103])).
% 244.16/244.35 tff(112,plain,
% 244.16/244.35 (![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))),
% 244.16/244.35 inference(modus_ponens,[status(thm)],[111, 101])).
% 244.16/244.35 tff(113,plain,
% 244.16/244.35 (((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))) | ((~relation(B!70)) | (~function(B!70)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C)))))))) <=> ((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))) | (~relation(B!70)) | (~function(B!70)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C)))))))),
% 244.16/244.35 inference(rewrite,[status(thm)],[])).
% 244.16/244.35 tff(114,plain,
% 244.16/244.35 ((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))) | ((~relation(B!70)) | (~function(B!70)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C)))))))),
% 244.16/244.35 inference(quant_inst,[status(thm)],[])).
% 244.16/244.35 tff(115,plain,
% 244.16/244.35 ((~![A: $i] : ((~relation(A)) | (~function(A)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(A, B))) | (~(((~in(D, relation_dom(A))) | (~in(apply(A, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(A, B)) | (((~in(tptp_fun_D_9(C, B, A), relation_dom(A))) | (~in(apply(A, tptp_fun_D_9(C, B, A)), B))) <=> in(tptp_fun_D_9(C, B, A), C)))))))) | (~relation(B!70)) | (~function(B!70)) | ![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C))))))),
% 244.16/244.35 inference(modus_ponens,[status(thm)],[114, 113])).
% 244.16/244.35 tff(116,plain,
% 244.16/244.35 (![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C))))))),
% 244.16/244.35 inference(unit_resolution,[status(thm)],[115, 112, 24, 23])).
% 244.16/244.35 tff(117,plain,
% 244.16/244.35 (((~![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C))))))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))) <=> ((~![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C))))))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))),
% 244.16/244.35 inference(rewrite,[status(thm)],[])).
% 244.16/244.35 tff(118,plain,
% 244.16/244.35 ((~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))) <=> (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))),
% 244.16/244.35 inference(rewrite,[status(thm)],[])).
% 244.16/244.35 tff(119,plain,
% 244.16/244.35 (((((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | $false) <=> (((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))),
% 244.16/244.35 inference(rewrite,[status(thm)],[])).
% 244.16/244.35 tff(120,plain,
% 244.16/244.35 ((~$true) <=> $false),
% 244.16/244.35 inference(rewrite,[status(thm)],[])).
% 244.16/244.35 tff(121,plain,
% 244.16/244.35 (($true | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71)))) <=> $true),
% 244.16/244.35 inference(rewrite,[status(thm)],[])).
% 244.16/244.35 tff(122,plain,
% 244.16/244.35 ((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) <=> $true),
% 244.16/244.35 inference(rewrite,[status(thm)],[])).
% 244.16/244.35 tff(123,plain,
% 244.16/244.35 (((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71)))) <=> ($true | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71))))),
% 244.16/244.35 inference(monotonicity,[status(thm)],[122])).
% 244.16/244.35 tff(124,plain,
% 244.16/244.35 (((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71)))) <=> $true),
% 244.16/244.35 inference(transitivity,[status(thm)],[123, 121])).
% 244.16/244.35 tff(125,plain,
% 244.16/244.35 ((~((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71))))) <=> (~$true)),
% 244.16/244.35 inference(monotonicity,[status(thm)],[124])).
% 244.16/244.35 tff(126,plain,
% 244.16/244.35 ((~((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71))))) <=> $false),
% 244.16/244.35 inference(transitivity,[status(thm)],[125, 120])).
% 244.16/244.35 tff(127,plain,
% 244.16/244.35 ((~(~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))) <=> (((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))),
% 244.16/244.36 inference(rewrite,[status(thm)],[])).
% 244.16/244.36 tff(128,plain,
% 244.16/244.36 (($false | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))) <=> (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))),
% 244.16/244.36 inference(rewrite,[status(thm)],[])).
% 244.16/244.36 tff(129,plain,
% 244.16/244.36 ((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) <=> (~$true)),
% 244.16/244.36 inference(monotonicity,[status(thm)],[122])).
% 244.16/244.36 tff(130,plain,
% 244.16/244.36 ((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) <=> $false),
% 244.16/244.36 inference(transitivity,[status(thm)],[129, 120])).
% 244.16/244.36 tff(131,plain,
% 244.16/244.36 (((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))) <=> ($false | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))),
% 244.16/244.36 inference(monotonicity,[status(thm)],[130, 118])).
% 244.16/244.36 tff(132,plain,
% 244.16/244.36 (((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))) <=> (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))),
% 244.16/244.36 inference(transitivity,[status(thm)],[131, 128])).
% 244.16/244.36 tff(133,plain,
% 244.16/244.36 ((~((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))) <=> (~(~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))),
% 244.16/244.36 inference(monotonicity,[status(thm)],[132])).
% 244.16/244.36 tff(134,plain,
% 244.16/244.36 ((~((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))) <=> (((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))),
% 244.16/244.36 inference(transitivity,[status(thm)],[133, 127])).
% 244.16/244.36 tff(135,plain,
% 244.16/244.36 (((~((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))) | (~((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71)))))) <=> ((((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | $false)),
% 244.16/244.36 inference(monotonicity,[status(thm)],[134, 126])).
% 244.16/244.36 tff(136,plain,
% 244.16/244.36 (((~((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))) | (~((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71)))))) <=> (((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))),
% 244.16/244.36 inference(transitivity,[status(thm)],[135, 119])).
% 244.16/244.36 tff(137,plain,
% 244.16/244.36 ((~((~((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))) | (~((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71))))))) <=> (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))),
% 244.16/244.36 inference(monotonicity,[status(thm)],[136])).
% 244.16/244.36 tff(138,plain,
% 244.16/244.36 ((~((~((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))) | (~((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71))))))) <=> (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))),
% 244.19/244.36 inference(transitivity,[status(thm)],[137, 118])).
% 244.19/244.36 tff(139,plain,
% 244.19/244.36 (((~![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C))))))) | (~((~((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))) | (~((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71)))))))) <=> ((~![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C))))))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))),
% 244.19/244.36 inference(monotonicity,[status(thm)],[138])).
% 244.19/244.36 tff(140,plain,
% 244.19/244.36 (((~![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C))))))) | (~((~((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))) | (~((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71)))))))) <=> ((~![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C))))))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))),
% 244.19/244.36 inference(transitivity,[status(thm)],[139, 117])).
% 244.19/244.36 tff(141,plain,
% 244.19/244.36 ((~![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C))))))) | (~((~((~(relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))))) | (~((relation_inverse_image(B!70, A!71) = relation_inverse_image(B!70, A!71)) | (((~in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70)), A!71))) <=> in(tptp_fun_D_9(relation_inverse_image(B!70, A!71), A!71, B!70), relation_inverse_image(B!70, A!71)))))))),
% 244.19/244.36 inference(quant_inst,[status(thm)],[])).
% 244.19/244.36 tff(142,plain,
% 244.19/244.36 ((~![B: $i, C: $i, D: $i] : (~((~((~(C = relation_inverse_image(B!70, B))) | (~(((~in(D, relation_dom(B!70))) | (~in(apply(B!70, D), B))) <=> in(D, C))))) | (~((C = relation_inverse_image(B!70, B)) | (((~in(tptp_fun_D_9(C, B, B!70), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_9(C, B, B!70)), B))) <=> in(tptp_fun_D_9(C, B, B!70), C))))))) | (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))))),
% 244.19/244.36 inference(modus_ponens,[status(thm)],[141, 140])).
% 244.19/244.36 tff(143,plain,
% 244.19/244.36 (~(((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))),
% 244.19/244.36 inference(unit_resolution,[status(thm)],[142, 116])).
% 244.19/244.36 tff(144,plain,
% 244.19/244.36 (((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~in(ordered_pair(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), B!70)) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70)))) | in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))),
% 244.19/244.36 inference(tautology,[status(thm)],[])).
% 244.19/244.36 tff(145,plain,
% 244.19/244.36 (in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))),
% 244.19/244.36 inference(unit_resolution,[status(thm)],[144, 82])).
% 244.19/244.36 tff(146,plain,
% 244.19/244.36 ((((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71)))) | (~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71)))),
% 244.19/244.36 inference(tautology,[status(thm)],[])).
% 244.19/244.36 tff(147,plain,
% 244.19/244.36 ((((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) <=> in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_inverse_image(B!70, A!71))) | (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))))),
% 244.19/244.36 inference(unit_resolution,[status(thm)],[146, 145])).
% 244.19/244.36 tff(148,plain,
% 244.19/244.36 (~((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71)))),
% 244.19/244.36 inference(unit_resolution,[status(thm)],[147, 143])).
% 244.19/244.36 tff(149,plain,
% 244.19/244.36 (((~in(tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71)))), relation_dom(B!70))) | (~in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71))) | in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71)),
% 244.19/244.36 inference(tautology,[status(thm)],[])).
% 244.19/244.36 tff(150,plain,
% 244.19/244.36 (in(apply(B!70, tptp_fun_D_69(B!70, relation_inverse_image(B!70, A!71), tptp_fun_C_36(A!71, relation_image(B!70, relation_inverse_image(B!70, A!71))))), A!71)),
% 244.36/244.54 inference(unit_resolution,[status(thm)],[149, 148])).
% 244.36/244.54 tff(151,plain,
% 244.36/244.54 ($false),
% 244.36/244.54 inference(unit_resolution,[status(thm)],[150, 96])).
% 244.36/244.54 % SZS output end Proof
% 244.71/244.88 % E exiting
%------------------------------------------------------------------------------