%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU373+1 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n011.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:44 AM UTC 2025
% Result : Theorem 0.21s 0.41s
% Output : Proof 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SEU373+1 : TPTP v9.0.0. Released v3.3.0.
% 0.03/0.13 % Command : run_E %s %d THM
% 0.13/0.35 % Computer : n011.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Fri Jun 20 06:55:56 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.21/0.41 % SZS status Theorem
% 0.21/0.41 % SZS output start Proof
% 0.21/0.41 tff(relation_dom_restr_as_relation_of_type, type, (
% 0.21/0.41 relation_dom_restr_as_relation_of: ( $i * $i * $i * $i ) > $i)).
% 0.21/0.41 tff(the_carrier_type, type, (
% 0.21/0.41 the_carrier: $i > $i)).
% 0.21/0.41 tff(tptp_fun_C_19_type, type, (
% 0.21/0.41 tptp_fun_C_19: $i)).
% 0.21/0.41 tff(the_mapping_type, type, (
% 0.21/0.41 the_mapping: ( $i * $i ) > $i)).
% 0.21/0.41 tff(tptp_fun_B_18_type, type, (
% 0.21/0.41 tptp_fun_B_18: $i)).
% 0.21/0.41 tff(tptp_fun_A_17_type, type, (
% 0.21/0.41 tptp_fun_A_17: $i)).
% 0.21/0.41 tff(subrelstr_type, type, (
% 0.21/0.41 subrelstr: ( $i * $i ) > $o)).
% 0.21/0.41 tff(subnetstr_type, type, (
% 0.21/0.41 subnetstr: ( $i * $i * $i ) > $o)).
% 0.21/0.41 tff(net_str_type, type, (
% 0.21/0.41 net_str: ( $i * $i ) > $o)).
% 0.21/0.41 tff(subset_type, type, (
% 0.21/0.41 subset: ( $i * $i ) > $o)).
% 0.21/0.41 tff(one_sorted_str_type, type, (
% 0.21/0.41 one_sorted_str: $i > $o)).
% 0.21/0.41 tff(the_InternalRel_type, type, (
% 0.21/0.41 the_InternalRel: $i > $i)).
% 0.21/0.41 tff(rel_str_type, type, (
% 0.21/0.41 rel_str: $i > $o)).
% 0.21/0.41 tff(1,plain,
% 0.21/0.41 ((one_sorted_str(A!17) & (net_str(B!18, A!17) & (~((~subnetstr(C!19, A!17, B!18)) | subset(the_carrier(C!19), the_carrier(B!18)))))) <=> (one_sorted_str(A!17) & net_str(B!18, A!17) & (~((~subnetstr(C!19, A!17, B!18)) | subset(the_carrier(C!19), the_carrier(B!18)))))),
% 0.21/0.41 inference(rewrite,[status(thm)],[])).
% 0.21/0.41 tff(2,plain,
% 0.21/0.41 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | subset(the_carrier(C), the_carrier(B)))))) <=> (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | subset(the_carrier(C), the_carrier(B))))))),
% 0.21/0.41 inference(rewrite,[status(thm)],[])).
% 0.21/0.41 tff(3,plain,
% 0.21/0.41 ((~![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => subset(the_carrier(C), the_carrier(B)))))) <=> (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | subset(the_carrier(C), the_carrier(B))))))),
% 0.21/0.41 inference(rewrite,[status(thm)],[])).
% 0.21/0.41 tff(4,axiom,(~![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => subset(the_carrier(C), the_carrier(B)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t19_yellow_6')).
% 0.21/0.41 tff(5,plain,
% 0.21/0.41 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | subset(the_carrier(C), the_carrier(B)))))),
% 0.21/0.41 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.21/0.41 tff(6,plain,
% 0.21/0.41 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | subset(the_carrier(C), the_carrier(B)))))),
% 0.21/0.41 inference(modus_ponens,[status(thm)],[5, 2])).
% 0.21/0.41 tff(7,plain,
% 0.21/0.41 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | subset(the_carrier(C), the_carrier(B)))))),
% 0.21/0.41 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.21/0.41 tff(8,plain,
% 0.21/0.41 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | subset(the_carrier(C), the_carrier(B)))))),
% 0.21/0.41 inference(modus_ponens,[status(thm)],[7, 2])).
% 0.21/0.41 tff(9,plain,
% 0.21/0.41 (one_sorted_str(A!17) & net_str(B!18, A!17) & (~((~subnetstr(C!19, A!17, B!18)) | subset(the_carrier(C!19), the_carrier(B!18))))),
% 0.21/0.41 inference(modus_ponens,[status(thm)],[8, 1])).
% 0.21/0.41 tff(10,plain,
% 0.21/0.41 (net_str(B!18, A!17)),
% 0.21/0.41 inference(and_elim,[status(thm)],[9])).
% 0.21/0.41 tff(11,plain,
% 0.21/0.41 (one_sorted_str(A!17)),
% 0.21/0.41 inference(and_elim,[status(thm)],[9])).
% 0.21/0.41 tff(12,plain,
% 0.21/0.41 (^[A: $i, B: $i] : rewrite(((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A))) <=> ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A))))),
% 0.21/0.41 inference(bind,[status(th)],[])).
% 0.21/0.41 tff(13,plain,
% 0.21/0.41 (![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A))) <=> ![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.21/0.41 inference(quant_intro,[status(thm)],[12])).
% 0.21/0.41 tff(14,plain,
% 0.21/0.41 (^[A: $i, B: $i] : refl(((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A))) <=> ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A))))),
% 0.21/0.41 inference(bind,[status(th)],[])).
% 0.21/0.41 tff(15,plain,
% 0.21/0.41 (![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A))) <=> ![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))),
% 0.21/0.41 inference(quant_intro,[status(thm)],[14])).
% 0.21/0.41 tff(16,plain,
% 0.21/0.41 (^[A: $i, B: $i] : rewrite(((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A))) <=> ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A))))),
% 0.21/0.41 inference(bind,[status(th)],[])).
% 0.21/0.41 tff(17,plain,
% 0.21/0.41 (![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A))) <=> ![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))),
% 0.21/0.41 inference(quant_intro,[status(thm)],[16])).
% 0.21/0.41 tff(18,plain,
% 0.21/0.41 (![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A))) <=> ![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))),
% 0.21/0.41 inference(transitivity,[status(thm)],[17, 15])).
% 0.21/0.41 tff(19,plain,
% 0.21/0.41 (^[A: $i, B: $i] : trans(monotonicity(trans(monotonicity(rewrite((one_sorted_str(A) & net_str(B, A)) <=> (~((~one_sorted_str(A)) | (~net_str(B, A))))), ((~(one_sorted_str(A) & net_str(B, A))) <=> (~(~((~one_sorted_str(A)) | (~net_str(B, A))))))), rewrite((~(~((~one_sorted_str(A)) | (~net_str(B, A))))) <=> ((~one_sorted_str(A)) | (~net_str(B, A)))), ((~(one_sorted_str(A) & net_str(B, A))) <=> ((~one_sorted_str(A)) | (~net_str(B, A))))), (((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A))) <=> (((~one_sorted_str(A)) | (~net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A))))), rewrite((((~one_sorted_str(A)) | (~net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A))) <=> ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))), (((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A))) <=> ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))))),
% 0.21/0.41 inference(bind,[status(th)],[])).
% 0.21/0.41 tff(20,plain,
% 0.21/0.41 (![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A))) <=> ![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))),
% 0.21/0.41 inference(quant_intro,[status(thm)],[19])).
% 0.21/0.41 tff(21,plain,
% 0.21/0.41 (![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A))) <=> ![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.21/0.41 inference(rewrite,[status(thm)],[])).
% 0.21/0.41 tff(22,plain,
% 0.21/0.41 (^[A: $i, B: $i] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : rewrite((subnetstr(C, A, B) => net_str(C, A)) <=> ((~subnetstr(C, A, B)) | net_str(C, A)))), (![C: $i] : (subnetstr(C, A, B) => net_str(C, A)) <=> ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))), (((one_sorted_str(A) & net_str(B, A)) => ![C: $i] : (subnetstr(C, A, B) => net_str(C, A))) <=> ((one_sorted_str(A) & net_str(B, A)) => ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A))))), rewrite(((one_sorted_str(A) & net_str(B, A)) => ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A))) <=> ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))), (((one_sorted_str(A) & net_str(B, A)) => ![C: $i] : (subnetstr(C, A, B) => net_str(C, A))) <=> ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))))),
% 0.21/0.41 inference(bind,[status(th)],[])).
% 0.21/0.41 tff(23,plain,
% 0.21/0.41 (![A: $i, B: $i] : ((one_sorted_str(A) & net_str(B, A)) => ![C: $i] : (subnetstr(C, A, B) => net_str(C, A))) <=> ![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.21/0.42 inference(quant_intro,[status(thm)],[22])).
% 0.21/0.42 tff(24,axiom,(![A: $i, B: $i] : ((one_sorted_str(A) & net_str(B, A)) => ![C: $i] : (subnetstr(C, A, B) => net_str(C, A)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dt_m1_yellow_6')).
% 0.21/0.42 tff(25,plain,
% 0.21/0.42 (![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[24, 23])).
% 0.21/0.42 tff(26,plain,
% 0.21/0.42 (![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[25, 21])).
% 0.21/0.42 tff(27,plain,(
% 0.21/0.42 ![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.21/0.42 inference(skolemize,[status(sab)],[26])).
% 0.21/0.42 tff(28,plain,
% 0.21/0.42 (![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[27, 20])).
% 0.21/0.42 tff(29,plain,
% 0.21/0.42 (![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[28, 18])).
% 0.21/0.42 tff(30,plain,
% 0.21/0.42 (![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[29, 13])).
% 0.21/0.42 tff(31,plain,
% 0.21/0.42 (((~![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))) | ((~one_sorted_str(A!17)) | (~net_str(B!18, A!17)) | ![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17)))) <=> ((~![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))) | (~one_sorted_str(A!17)) | (~net_str(B!18, A!17)) | ![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17)))),
% 0.21/0.42 inference(rewrite,[status(thm)],[])).
% 0.21/0.42 tff(32,plain,
% 0.21/0.42 (((~net_str(B!18, A!17)) | (~one_sorted_str(A!17)) | ![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17))) <=> ((~one_sorted_str(A!17)) | (~net_str(B!18, A!17)) | ![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17)))),
% 0.21/0.42 inference(rewrite,[status(thm)],[])).
% 0.21/0.42 tff(33,plain,
% 0.21/0.42 (((~![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))) | ((~net_str(B!18, A!17)) | (~one_sorted_str(A!17)) | ![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17)))) <=> ((~![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))) | ((~one_sorted_str(A!17)) | (~net_str(B!18, A!17)) | ![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17))))),
% 0.21/0.42 inference(monotonicity,[status(thm)],[32])).
% 0.21/0.42 tff(34,plain,
% 0.21/0.42 (((~![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))) | ((~net_str(B!18, A!17)) | (~one_sorted_str(A!17)) | ![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17)))) <=> ((~![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))) | (~one_sorted_str(A!17)) | (~net_str(B!18, A!17)) | ![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17)))),
% 0.21/0.42 inference(transitivity,[status(thm)],[33, 31])).
% 0.21/0.42 tff(35,plain,
% 0.21/0.42 ((~![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))) | ((~net_str(B!18, A!17)) | (~one_sorted_str(A!17)) | ![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17)))),
% 0.21/0.42 inference(quant_inst,[status(thm)],[])).
% 0.21/0.42 tff(36,plain,
% 0.21/0.42 ((~![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))) | (~one_sorted_str(A!17)) | (~net_str(B!18, A!17)) | ![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[35, 34])).
% 0.21/0.42 tff(37,plain,
% 0.21/0.42 (![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17))),
% 0.21/0.42 inference(unit_resolution,[status(thm)],[36, 30, 11, 10])).
% 0.21/0.42 tff(38,plain,
% 0.21/0.42 (~((~subnetstr(C!19, A!17, B!18)) | subset(the_carrier(C!19), the_carrier(B!18)))),
% 0.21/0.42 inference(and_elim,[status(thm)],[9])).
% 0.21/0.42 tff(39,plain,
% 0.21/0.42 (subnetstr(C!19, A!17, B!18)),
% 0.21/0.42 inference(or_elim,[status(thm)],[38])).
% 0.21/0.42 tff(40,plain,
% 0.21/0.42 (((~![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17))) | ((~subnetstr(C!19, A!17, B!18)) | net_str(C!19, A!17))) <=> ((~![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17))) | (~subnetstr(C!19, A!17, B!18)) | net_str(C!19, A!17))),
% 0.21/0.42 inference(rewrite,[status(thm)],[])).
% 0.21/0.42 tff(41,plain,
% 0.21/0.42 ((~![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17))) | ((~subnetstr(C!19, A!17, B!18)) | net_str(C!19, A!17))),
% 0.21/0.42 inference(quant_inst,[status(thm)],[])).
% 0.21/0.42 tff(42,plain,
% 0.21/0.42 ((~![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17))) | (~subnetstr(C!19, A!17, B!18)) | net_str(C!19, A!17)),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.21/0.42 tff(43,plain,
% 0.21/0.42 (net_str(C!19, A!17)),
% 0.21/0.42 inference(unit_resolution,[status(thm)],[42, 39, 37])).
% 0.21/0.42 tff(44,plain,
% 0.21/0.42 (^[A: $i] : refl(((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B)))))) <=> ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B)))))))),
% 0.21/0.42 inference(bind,[status(th)],[])).
% 0.21/0.42 tff(45,plain,
% 0.21/0.42 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B)))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B))))))),
% 0.21/0.42 inference(quant_intro,[status(thm)],[44])).
% 0.21/0.42 tff(46,plain,
% 0.21/0.42 (^[A: $i] : rewrite(((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B)))))) <=> ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B)))))))),
% 0.21/0.42 inference(bind,[status(th)],[])).
% 0.21/0.42 tff(47,plain,
% 0.21/0.42 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B)))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B))))))),
% 0.21/0.42 inference(quant_intro,[status(thm)],[46])).
% 0.21/0.42 tff(48,plain,
% 0.21/0.42 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B)))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B))))))),
% 0.21/0.42 inference(transitivity,[status(thm)],[47, 45])).
% 0.21/0.42 tff(49,plain,
% 0.21/0.42 (^[A: $i] : rewrite(((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))) <=> ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B)))))))),
% 0.21/0.42 inference(bind,[status(th)],[])).
% 0.21/0.42 tff(50,plain,
% 0.21/0.42 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B))))))),
% 0.21/0.42 inference(quant_intro,[status(thm)],[49])).
% 0.21/0.42 tff(51,plain,
% 0.21/0.42 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))))),
% 0.21/0.42 inference(rewrite,[status(thm)],[])).
% 0.21/0.42 tff(52,plain,
% 0.21/0.42 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : rewrite((net_str(C, A) => (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))) <=> ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))), (![C: $i] : (net_str(C, A) => (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))) <=> ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))), ((net_str(B, A) => ![C: $i] : (net_str(C, A) => (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))) <=> (net_str(B, A) => ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))))), rewrite((net_str(B, A) => ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))) <=> ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))), ((net_str(B, A) => ![C: $i] : (net_str(C, A) => (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))) <=> ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))))), (![B: $i] : (net_str(B, A) => ![C: $i] : (net_str(C, A) => (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))) <=> ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))))), ((one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (net_str(C, A) => (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))) <=> (one_sorted_str(A) => ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))))), rewrite((one_sorted_str(A) => ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))) <=> ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))))), ((one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (net_str(C, A) => (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))) <=> ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))))))),
% 0.21/0.42 inference(bind,[status(th)],[])).
% 0.21/0.42 tff(53,plain,
% 0.21/0.42 (![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (net_str(C, A) => (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C)))))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))))),
% 0.21/0.42 inference(quant_intro,[status(thm)],[52])).
% 0.21/0.42 tff(54,axiom,(![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (net_str(C, A) => (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d8_yellow_6')).
% 0.21/0.42 tff(55,plain,
% 0.21/0.42 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[54, 53])).
% 0.21/0.42 tff(56,plain,
% 0.21/0.42 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[55, 51])).
% 0.21/0.42 tff(57,plain,(
% 0.21/0.42 ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (subnetstr(C, A, B) <=> (subrelstr(C, B) & (the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))))))),
% 0.21/0.42 inference(skolemize,[status(sab)],[56])).
% 0.21/0.42 tff(58,plain,
% 0.21/0.42 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B))))))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[57, 50])).
% 0.21/0.42 tff(59,plain,
% 0.21/0.42 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B))))))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[58, 48])).
% 0.21/0.42 tff(60,plain,
% 0.21/0.42 (((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B))))))) | ((~one_sorted_str(A!17)) | ![B: $i] : ((~net_str(B, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A!17), the_mapping(A!17, B), the_carrier(C))))) <=> subnetstr(C, A!17, B))))))) <=> ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B))))))) | (~one_sorted_str(A!17)) | ![B: $i] : ((~net_str(B, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A!17), the_mapping(A!17, B), the_carrier(C))))) <=> subnetstr(C, A!17, B))))))),
% 0.21/0.42 inference(rewrite,[status(thm)],[])).
% 0.21/0.42 tff(61,plain,
% 0.21/0.42 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B))))))) | ((~one_sorted_str(A!17)) | ![B: $i] : ((~net_str(B, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A!17), the_mapping(A!17, B), the_carrier(C))))) <=> subnetstr(C, A!17, B))))))),
% 0.21/0.42 inference(quant_inst,[status(thm)],[])).
% 0.21/0.42 tff(62,plain,
% 0.21/0.42 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~net_str(C, A)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A), the_mapping(A, B), the_carrier(C))))) <=> subnetstr(C, A, B))))))) | (~one_sorted_str(A!17)) | ![B: $i] : ((~net_str(B, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A!17), the_mapping(A!17, B), the_carrier(C))))) <=> subnetstr(C, A!17, B)))))),
% 0.21/0.42 inference(modus_ponens,[status(thm)],[61, 60])).
% 0.21/0.42 tff(63,plain,
% 0.21/0.42 (![B: $i] : ((~net_str(B, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A!17), the_mapping(A!17, B), the_carrier(C))))) <=> subnetstr(C, A!17, B)))))),
% 0.21/0.42 inference(unit_resolution,[status(thm)],[62, 59, 11])).
% 0.21/0.42 tff(64,plain,
% 0.21/0.42 (((~![B: $i] : ((~net_str(B, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A!17), the_mapping(A!17, B), the_carrier(C))))) <=> subnetstr(C, A!17, B)))))) | ((~net_str(B!18, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B!18)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C))))) <=> subnetstr(C, A!17, B!18)))))) <=> ((~![B: $i] : ((~net_str(B, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A!17), the_mapping(A!17, B), the_carrier(C))))) <=> subnetstr(C, A!17, B)))))) | (~net_str(B!18, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B!18)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C))))) <=> subnetstr(C, A!17, B!18)))))),
% 0.21/0.43 inference(rewrite,[status(thm)],[])).
% 0.21/0.43 tff(65,plain,
% 0.21/0.43 ((~![B: $i] : ((~net_str(B, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A!17), the_mapping(A!17, B), the_carrier(C))))) <=> subnetstr(C, A!17, B)))))) | ((~net_str(B!18, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B!18)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C))))) <=> subnetstr(C, A!17, B!18)))))),
% 0.21/0.43 inference(quant_inst,[status(thm)],[])).
% 0.21/0.43 tff(66,plain,
% 0.21/0.43 ((~![B: $i] : ((~net_str(B, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B), the_carrier(A!17), the_mapping(A!17, B), the_carrier(C))))) <=> subnetstr(C, A!17, B)))))) | (~net_str(B!18, A!17)) | ![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B!18)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C))))) <=> subnetstr(C, A!17, B!18))))),
% 0.21/0.43 inference(modus_ponens,[status(thm)],[65, 64])).
% 0.21/0.43 tff(67,plain,
% 0.21/0.43 (![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B!18)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C))))) <=> subnetstr(C, A!17, B!18))))),
% 0.21/0.43 inference(unit_resolution,[status(thm)],[66, 10, 63])).
% 0.21/0.43 tff(68,plain,
% 0.21/0.43 (((~![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B!18)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C))))) <=> subnetstr(C, A!17, B!18))))) | ((~net_str(C!19, A!17)) | (~(((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19))))) <=> subnetstr(C!19, A!17, B!18))))) <=> ((~![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B!18)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C))))) <=> subnetstr(C, A!17, B!18))))) | (~net_str(C!19, A!17)) | (~(((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19))))) <=> subnetstr(C!19, A!17, B!18))))),
% 0.21/0.43 inference(rewrite,[status(thm)],[])).
% 0.21/0.43 tff(69,plain,
% 0.21/0.43 ((~![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B!18)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C))))) <=> subnetstr(C, A!17, B!18))))) | ((~net_str(C!19, A!17)) | (~(((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19))))) <=> subnetstr(C!19, A!17, B!18))))),
% 0.21/0.43 inference(quant_inst,[status(thm)],[])).
% 0.21/0.43 tff(70,plain,
% 0.21/0.43 ((~![C: $i] : ((~net_str(C, A!17)) | (~(((~subrelstr(C, B!18)) | (~(the_mapping(A!17, C) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C))))) <=> subnetstr(C, A!17, B!18))))) | (~net_str(C!19, A!17)) | (~(((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19))))) <=> subnetstr(C!19, A!17, B!18)))),
% 0.21/0.43 inference(modus_ponens,[status(thm)],[69, 68])).
% 0.21/0.43 tff(71,plain,
% 0.21/0.43 (~(((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19))))) <=> subnetstr(C!19, A!17, B!18))),
% 0.21/0.43 inference(unit_resolution,[status(thm)],[70, 67, 43])).
% 0.21/0.43 tff(72,plain,
% 0.21/0.43 ((((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19))))) <=> subnetstr(C!19, A!17, B!18)) | (~((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19)))))) | (~subnetstr(C!19, A!17, B!18))),
% 0.21/0.43 inference(tautology,[status(thm)],[])).
% 0.21/0.43 tff(73,plain,
% 0.21/0.43 ((((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19))))) <=> subnetstr(C!19, A!17, B!18)) | (~((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19))))))),
% 0.21/0.43 inference(unit_resolution,[status(thm)],[72, 39])).
% 0.21/0.43 tff(74,plain,
% 0.21/0.43 (~((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19)))))),
% 0.21/0.43 inference(unit_resolution,[status(thm)],[73, 71])).
% 0.21/0.43 tff(75,plain,
% 0.21/0.43 (^[A: $i] : refl(((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A)))) <=> ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A)))))),
% 0.21/0.43 inference(bind,[status(th)],[])).
% 0.21/0.43 tff(76,plain,
% 0.21/0.43 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A)))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.21/0.43 inference(quant_intro,[status(thm)],[75])).
% 0.21/0.43 tff(77,plain,
% 0.21/0.43 (^[A: $i] : rewrite(((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A)))) <=> ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A)))))),
% 0.21/0.43 inference(bind,[status(th)],[])).
% 0.21/0.43 tff(78,plain,
% 0.21/0.43 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A)))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.21/0.43 inference(quant_intro,[status(thm)],[77])).
% 0.21/0.43 tff(79,plain,
% 0.21/0.43 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A)))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.21/0.43 inference(transitivity,[status(thm)],[78, 76])).
% 0.21/0.43 tff(80,plain,
% 0.21/0.43 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A)))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.21/0.43 inference(rewrite,[status(thm)],[])).
% 0.21/0.43 tff(81,plain,
% 0.21/0.43 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : rewrite((net_str(B, A) => rel_str(B)) <=> (rel_str(B) | (~net_str(B, A))))), (![B: $i] : (net_str(B, A) => rel_str(B)) <=> ![B: $i] : (rel_str(B) | (~net_str(B, A))))), ((one_sorted_str(A) => ![B: $i] : (net_str(B, A) => rel_str(B))) <=> (one_sorted_str(A) => ![B: $i] : (rel_str(B) | (~net_str(B, A)))))), rewrite((one_sorted_str(A) => ![B: $i] : (rel_str(B) | (~net_str(B, A)))) <=> ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))), ((one_sorted_str(A) => ![B: $i] : (net_str(B, A) => rel_str(B))) <=> ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))))),
% 0.21/0.43 inference(bind,[status(th)],[])).
% 0.21/0.43 tff(82,plain,
% 0.21/0.43 (![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => rel_str(B))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.21/0.43 inference(quant_intro,[status(thm)],[81])).
% 0.21/0.43 tff(83,axiom,(![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => rel_str(B)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dt_l1_waybel_0')).
% 0.21/0.43 tff(84,plain,
% 0.21/0.43 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.21/0.43 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.21/0.43 tff(85,plain,
% 0.21/0.43 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.21/0.43 inference(modus_ponens,[status(thm)],[84, 80])).
% 0.21/0.43 tff(86,plain,(
% 0.21/0.43 ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.21/0.43 inference(skolemize,[status(sab)],[85])).
% 0.21/0.43 tff(87,plain,
% 0.21/0.43 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.21/0.43 inference(modus_ponens,[status(thm)],[86, 79])).
% 0.21/0.43 tff(88,plain,
% 0.21/0.43 (((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | ((~one_sorted_str(A!17)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!17))))) <=> ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | (~one_sorted_str(A!17)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!17))))),
% 0.21/0.43 inference(rewrite,[status(thm)],[])).
% 0.21/0.43 tff(89,plain,
% 0.21/0.43 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | ((~one_sorted_str(A!17)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!17))))),
% 0.21/0.43 inference(quant_inst,[status(thm)],[])).
% 0.21/0.43 tff(90,plain,
% 0.21/0.43 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | (~one_sorted_str(A!17)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!17)))),
% 0.21/0.43 inference(modus_ponens,[status(thm)],[89, 88])).
% 0.21/0.43 tff(91,plain,
% 0.21/0.43 (![B: $i] : (rel_str(B) | (~net_str(B, A!17)))),
% 0.21/0.43 inference(unit_resolution,[status(thm)],[90, 87, 11])).
% 0.21/0.43 tff(92,plain,
% 0.21/0.43 (((~![B: $i] : (rel_str(B) | (~net_str(B, A!17)))) | (rel_str(B!18) | (~net_str(B!18, A!17)))) <=> ((~![B: $i] : (rel_str(B) | (~net_str(B, A!17)))) | rel_str(B!18) | (~net_str(B!18, A!17)))),
% 0.21/0.43 inference(rewrite,[status(thm)],[])).
% 0.21/0.43 tff(93,plain,
% 0.21/0.43 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!17)))) | (rel_str(B!18) | (~net_str(B!18, A!17)))),
% 0.21/0.43 inference(quant_inst,[status(thm)],[])).
% 0.21/0.43 tff(94,plain,
% 0.21/0.43 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!17)))) | rel_str(B!18) | (~net_str(B!18, A!17))),
% 0.21/0.43 inference(modus_ponens,[status(thm)],[93, 92])).
% 0.21/0.43 tff(95,plain,
% 0.21/0.43 (rel_str(B!18)),
% 0.21/0.43 inference(unit_resolution,[status(thm)],[94, 10, 91])).
% 0.21/0.43 tff(96,plain,
% 0.21/0.43 (^[A: $i] : refl(((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A))))) <=> ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A))))))),
% 0.21/0.43 inference(bind,[status(th)],[])).
% 0.21/0.43 tff(97,plain,
% 0.21/0.43 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A)))))),
% 0.21/0.43 inference(quant_intro,[status(thm)],[96])).
% 0.21/0.43 tff(98,plain,
% 0.21/0.43 (^[A: $i] : rewrite(((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A))))) <=> ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A))))))),
% 0.21/0.43 inference(bind,[status(th)],[])).
% 0.21/0.43 tff(99,plain,
% 0.21/0.43 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A)))))),
% 0.21/0.43 inference(quant_intro,[status(thm)],[98])).
% 0.21/0.43 tff(100,plain,
% 0.21/0.43 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A)))))),
% 0.21/0.43 inference(transitivity,[status(thm)],[99, 97])).
% 0.21/0.43 tff(101,plain,
% 0.21/0.43 (^[A: $i] : rewrite(((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A)))))) <=> ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A))))))),
% 0.21/0.43 inference(bind,[status(th)],[])).
% 0.21/0.43 tff(102,plain,
% 0.21/0.43 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A)))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A)))))),
% 0.21/0.43 inference(quant_intro,[status(thm)],[101])).
% 0.21/0.43 tff(103,plain,
% 0.21/0.43 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A)))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))))),
% 0.21/0.43 inference(rewrite,[status(thm)],[])).
% 0.21/0.43 tff(104,plain,
% 0.21/0.43 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : rewrite((rel_str(B) => (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))) <=> ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))))), (![B: $i] : (rel_str(B) => (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))) <=> ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))))), ((rel_str(A) => ![B: $i] : (rel_str(B) => (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A)))))) <=> (rel_str(A) => ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A)))))))), rewrite((rel_str(A) => ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A)))))) <=> ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))))), ((rel_str(A) => ![B: $i] : (rel_str(B) => (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A)))))) <=> ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))))))),
% 0.21/0.43 inference(bind,[status(th)],[])).
% 0.21/0.43 tff(105,plain,
% 0.21/0.43 (![A: $i] : (rel_str(A) => ![B: $i] : (rel_str(B) => (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A)))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))))),
% 0.21/0.43 inference(quant_intro,[status(thm)],[104])).
% 0.21/0.43 tff(106,axiom,(![A: $i] : (rel_str(A) => ![B: $i] : (rel_str(B) => (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d13_yellow_0')).
% 0.21/0.43 tff(107,plain,
% 0.21/0.43 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))))),
% 0.21/0.43 inference(modus_ponens,[status(thm)],[106, 105])).
% 0.21/0.43 tff(108,plain,
% 0.21/0.43 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))))),
% 0.21/0.44 inference(modus_ponens,[status(thm)],[107, 103])).
% 0.21/0.44 tff(109,plain,(
% 0.21/0.44 ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (subrelstr(B, A) <=> (subset(the_carrier(B), the_carrier(A)) & subset(the_InternalRel(B), the_InternalRel(A))))))),
% 0.21/0.44 inference(skolemize,[status(sab)],[108])).
% 0.21/0.44 tff(110,plain,
% 0.21/0.44 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A)))))),
% 0.21/0.44 inference(modus_ponens,[status(thm)],[109, 102])).
% 0.21/0.44 tff(111,plain,
% 0.21/0.44 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A)))))),
% 0.21/0.44 inference(modus_ponens,[status(thm)],[110, 100])).
% 0.21/0.44 tff(112,plain,
% 0.21/0.44 (((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A)))))) | ((~rel_str(B!18)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(B!18))) | (~subset(the_InternalRel(B), the_InternalRel(B!18)))) <=> subrelstr(B, B!18)))))) <=> ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A)))))) | (~rel_str(B!18)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(B!18))) | (~subset(the_InternalRel(B), the_InternalRel(B!18)))) <=> subrelstr(B, B!18)))))),
% 0.21/0.44 inference(rewrite,[status(thm)],[])).
% 0.21/0.44 tff(113,plain,
% 0.21/0.44 ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A)))))) | ((~rel_str(B!18)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(B!18))) | (~subset(the_InternalRel(B), the_InternalRel(B!18)))) <=> subrelstr(B, B!18)))))),
% 0.21/0.44 inference(quant_inst,[status(thm)],[])).
% 0.21/0.44 tff(114,plain,
% 0.21/0.44 ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(A))) | (~subset(the_InternalRel(B), the_InternalRel(A)))) <=> subrelstr(B, A)))))) | (~rel_str(B!18)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(B!18))) | (~subset(the_InternalRel(B), the_InternalRel(B!18)))) <=> subrelstr(B, B!18))))),
% 0.21/0.44 inference(modus_ponens,[status(thm)],[113, 112])).
% 0.21/0.44 tff(115,plain,
% 0.21/0.44 ((~rel_str(B!18)) | ![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(B!18))) | (~subset(the_InternalRel(B), the_InternalRel(B!18)))) <=> subrelstr(B, B!18))))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[114, 111])).
% 0.21/0.44 tff(116,plain,
% 0.21/0.44 (![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(B!18))) | (~subset(the_InternalRel(B), the_InternalRel(B!18)))) <=> subrelstr(B, B!18))))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[115, 95])).
% 0.21/0.44 tff(117,plain,
% 0.21/0.44 (((~![B: $i] : (rel_str(B) | (~net_str(B, A!17)))) | (rel_str(C!19) | (~net_str(C!19, A!17)))) <=> ((~![B: $i] : (rel_str(B) | (~net_str(B, A!17)))) | rel_str(C!19) | (~net_str(C!19, A!17)))),
% 0.21/0.44 inference(rewrite,[status(thm)],[])).
% 0.21/0.44 tff(118,plain,
% 0.21/0.44 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!17)))) | (rel_str(C!19) | (~net_str(C!19, A!17)))),
% 0.21/0.44 inference(quant_inst,[status(thm)],[])).
% 0.21/0.44 tff(119,plain,
% 0.21/0.44 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!17)))) | rel_str(C!19) | (~net_str(C!19, A!17))),
% 0.21/0.44 inference(modus_ponens,[status(thm)],[118, 117])).
% 0.21/0.44 tff(120,plain,
% 0.21/0.44 (rel_str(C!19)),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[119, 91, 43])).
% 0.21/0.44 tff(121,plain,
% 0.21/0.44 (((~![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(B!18))) | (~subset(the_InternalRel(B), the_InternalRel(B!18)))) <=> subrelstr(B, B!18))))) | ((~rel_str(C!19)) | (~(((~subset(the_carrier(C!19), the_carrier(B!18))) | (~subset(the_InternalRel(C!19), the_InternalRel(B!18)))) <=> subrelstr(C!19, B!18))))) <=> ((~![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(B!18))) | (~subset(the_InternalRel(B), the_InternalRel(B!18)))) <=> subrelstr(B, B!18))))) | (~rel_str(C!19)) | (~(((~subset(the_carrier(C!19), the_carrier(B!18))) | (~subset(the_InternalRel(C!19), the_InternalRel(B!18)))) <=> subrelstr(C!19, B!18))))),
% 0.21/0.44 inference(rewrite,[status(thm)],[])).
% 0.21/0.44 tff(122,plain,
% 0.21/0.44 ((~![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(B!18))) | (~subset(the_InternalRel(B), the_InternalRel(B!18)))) <=> subrelstr(B, B!18))))) | ((~rel_str(C!19)) | (~(((~subset(the_carrier(C!19), the_carrier(B!18))) | (~subset(the_InternalRel(C!19), the_InternalRel(B!18)))) <=> subrelstr(C!19, B!18))))),
% 0.21/0.44 inference(quant_inst,[status(thm)],[])).
% 0.21/0.44 tff(123,plain,
% 0.21/0.44 ((~![B: $i] : ((~rel_str(B)) | (~(((~subset(the_carrier(B), the_carrier(B!18))) | (~subset(the_InternalRel(B), the_InternalRel(B!18)))) <=> subrelstr(B, B!18))))) | (~rel_str(C!19)) | (~(((~subset(the_carrier(C!19), the_carrier(B!18))) | (~subset(the_InternalRel(C!19), the_InternalRel(B!18)))) <=> subrelstr(C!19, B!18)))),
% 0.21/0.44 inference(modus_ponens,[status(thm)],[122, 121])).
% 0.21/0.44 tff(124,plain,
% 0.21/0.44 (~(((~subset(the_carrier(C!19), the_carrier(B!18))) | (~subset(the_InternalRel(C!19), the_InternalRel(B!18)))) <=> subrelstr(C!19, B!18))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[123, 120, 116])).
% 0.21/0.44 tff(125,plain,
% 0.21/0.44 (~subset(the_carrier(C!19), the_carrier(B!18))),
% 0.21/0.44 inference(or_elim,[status(thm)],[38])).
% 0.21/0.44 tff(126,plain,
% 0.21/0.44 (((~subset(the_carrier(C!19), the_carrier(B!18))) | (~subset(the_InternalRel(C!19), the_InternalRel(B!18)))) | subset(the_carrier(C!19), the_carrier(B!18))),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(127,plain,
% 0.21/0.44 ((~subset(the_carrier(C!19), the_carrier(B!18))) | (~subset(the_InternalRel(C!19), the_InternalRel(B!18)))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[126, 125])).
% 0.21/0.44 tff(128,plain,
% 0.21/0.44 ((((~subset(the_carrier(C!19), the_carrier(B!18))) | (~subset(the_InternalRel(C!19), the_InternalRel(B!18)))) <=> subrelstr(C!19, B!18)) | (~((~subset(the_carrier(C!19), the_carrier(B!18))) | (~subset(the_InternalRel(C!19), the_InternalRel(B!18))))) | (~subrelstr(C!19, B!18))),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(129,plain,
% 0.21/0.44 ((((~subset(the_carrier(C!19), the_carrier(B!18))) | (~subset(the_InternalRel(C!19), the_InternalRel(B!18)))) <=> subrelstr(C!19, B!18)) | (~subrelstr(C!19, B!18))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[128, 127])).
% 0.21/0.44 tff(130,plain,
% 0.21/0.44 (~subrelstr(C!19, B!18)),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[129, 124])).
% 0.21/0.44 tff(131,plain,
% 0.21/0.44 (((~subrelstr(C!19, B!18)) | (~(the_mapping(A!17, C!19) = relation_dom_restr_as_relation_of(the_carrier(B!18), the_carrier(A!17), the_mapping(A!17, B!18), the_carrier(C!19))))) | subrelstr(C!19, B!18)),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(132,plain,
% 0.21/0.44 ($false),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[131, 130, 74])).
% 0.21/0.44 % SZS output end Proof
% 0.21/0.44 % E exiting
%------------------------------------------------------------------------------