%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU374+1 : 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:44 AM UTC 2025
% Result : Theorem 0.20s 0.45s
% Output : Proof 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU374+1 : TPTP v9.0.0. Released v3.3.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n001.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 07:00:20 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.20/0.45 % SZS status Theorem
% 0.20/0.45 % SZS output start Proof
% 0.20/0.45 tff(related_type, type, (
% 0.20/0.45 related: ( $i * $i * $i ) > $o)).
% 0.20/0.45 tff(tptp_fun_D_20_type, type, (
% 0.20/0.45 tptp_fun_D_20: $i)).
% 0.20/0.45 tff(tptp_fun_C_19_type, type, (
% 0.20/0.45 tptp_fun_C_19: $i)).
% 0.20/0.45 tff(tptp_fun_B_18_type, type, (
% 0.20/0.45 tptp_fun_B_18: $i)).
% 0.20/0.45 tff(element_type, type, (
% 0.20/0.45 element: ( $i * $i ) > $o)).
% 0.20/0.45 tff(the_carrier_type, type, (
% 0.20/0.45 the_carrier: $i > $i)).
% 0.20/0.45 tff(subrelstr_type, type, (
% 0.20/0.45 subrelstr: ( $i * $i ) > $o)).
% 0.20/0.45 tff(relation_dom_restr_as_relation_of_type, type, (
% 0.20/0.45 relation_dom_restr_as_relation_of: ( $i * $i * $i * $i ) > $i)).
% 0.20/0.45 tff(the_mapping_type, type, (
% 0.20/0.45 the_mapping: ( $i * $i ) > $i)).
% 0.20/0.45 tff(tptp_fun_A_17_type, type, (
% 0.20/0.45 tptp_fun_A_17: $i)).
% 0.20/0.45 tff(subnetstr_type, type, (
% 0.20/0.45 subnetstr: ( $i * $i * $i ) > $o)).
% 0.20/0.45 tff(net_str_type, type, (
% 0.20/0.45 net_str: ( $i * $i ) > $o)).
% 0.20/0.45 tff(tptp_fun_E_21_type, type, (
% 0.20/0.45 tptp_fun_E_21: $i)).
% 0.20/0.45 tff(one_sorted_str_type, type, (
% 0.20/0.45 one_sorted_str: $i > $o)).
% 0.20/0.45 tff(rel_str_type, type, (
% 0.20/0.45 rel_str: $i > $o)).
% 0.20/0.45 tff(1,plain,
% 0.20/0.45 ((one_sorted_str(A!17) & (net_str(B!18, A!17) & subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))) <=> (one_sorted_str(A!17) & net_str(B!18, A!17) & subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(2,plain,
% 0.20/0.45 ((net_str(B!18, A!17) & (subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))) <=> (net_str(B!18, A!17) & subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(3,plain,
% 0.20/0.45 ((subnetstr(C!19, A!17, B!18) & (element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))) <=> (subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(4,plain,
% 0.20/0.45 ((element(D!20, the_carrier(B!18)) & (~((~element(E!21, the_carrier(B!18))) | (~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21))))) <=> (element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(5,plain,
% 0.20/0.45 ((subnetstr(C!19, A!17, B!18) & (element(D!20, the_carrier(B!18)) & (~((~element(E!21, the_carrier(B!18))) | (~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))) <=> (subnetstr(C!19, A!17, B!18) & (element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21))))))),
% 0.20/0.45 inference(monotonicity,[status(thm)],[4])).
% 0.20/0.45 tff(6,plain,
% 0.20/0.45 ((subnetstr(C!19, A!17, B!18) & (element(D!20, the_carrier(B!18)) & (~((~element(E!21, the_carrier(B!18))) | (~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))) <=> (subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))),
% 0.20/0.45 inference(transitivity,[status(thm)],[5, 3])).
% 0.20/0.45 tff(7,plain,
% 0.20/0.45 ((net_str(B!18, A!17) & (subnetstr(C!19, A!17, B!18) & (element(D!20, the_carrier(B!18)) & (~((~element(E!21, the_carrier(B!18))) | (~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21))))))) <=> (net_str(B!18, A!17) & (subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21))))))),
% 0.20/0.45 inference(monotonicity,[status(thm)],[6])).
% 0.20/0.45 tff(8,plain,
% 0.20/0.45 ((net_str(B!18, A!17) & (subnetstr(C!19, A!17, B!18) & (element(D!20, the_carrier(B!18)) & (~((~element(E!21, the_carrier(B!18))) | (~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21))))))) <=> (net_str(B!18, A!17) & subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))),
% 0.20/0.45 inference(transitivity,[status(thm)],[7, 2])).
% 0.20/0.45 tff(9,plain,
% 0.20/0.45 ((one_sorted_str(A!17) & (net_str(B!18, A!17) & (subnetstr(C!19, A!17, B!18) & (element(D!20, the_carrier(B!18)) & (~((~element(E!21, the_carrier(B!18))) | (~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))))) <=> (one_sorted_str(A!17) & (net_str(B!18, A!17) & subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21))))))),
% 0.20/0.45 inference(monotonicity,[status(thm)],[8])).
% 0.20/0.45 tff(10,plain,
% 0.20/0.45 ((one_sorted_str(A!17) & (net_str(B!18, A!17) & (subnetstr(C!19, A!17, B!18) & (element(D!20, the_carrier(B!18)) & (~((~element(E!21, the_carrier(B!18))) | (~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))))) <=> (one_sorted_str(A!17) & net_str(B!18, A!17) & subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))))),
% 0.20/0.45 inference(transitivity,[status(thm)],[9, 1])).
% 0.20/0.45 tff(11,plain,
% 0.20/0.45 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | ![D: $i] : ((~element(D, the_carrier(B))) | ![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(C))) | (~element(E, the_carrier(C))) | related(B, D, E) | (~related(C, D, E)))))))) <=> (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | ![D: $i] : ((~element(D, the_carrier(B))) | ![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(C))) | (~element(E, the_carrier(C))) | related(B, D, E) | (~related(C, D, E))))))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(12,plain,
% 0.20/0.45 ((~![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => ![D: $i] : (element(D, the_carrier(B)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(C)) => ![G: $i] : (element(G, the_carrier(C)) => ((((D = F) & (E = G)) & related(C, F, G)) => related(B, D, E)))))))))) <=> (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | ![D: $i] : ((~element(D, the_carrier(B))) | ![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(C))) | (~element(E, the_carrier(C))) | related(B, D, E) | (~related(C, D, E))))))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(13,axiom,(~![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => ![D: $i] : (element(D, the_carrier(B)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(C)) => ![G: $i] : (element(G, the_carrier(C)) => ((((D = F) & (E = G)) & related(C, F, G)) => related(B, D, E)))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t20_yellow_6')).
% 0.20/0.45 tff(14,plain,
% 0.20/0.45 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | ![D: $i] : ((~element(D, the_carrier(B))) | ![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(C))) | (~element(E, the_carrier(C))) | related(B, D, E) | (~related(C, D, E)))))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[13, 12])).
% 0.20/0.45 tff(15,plain,
% 0.20/0.45 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | ![D: $i] : ((~element(D, the_carrier(B))) | ![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(C))) | (~element(E, the_carrier(C))) | related(B, D, E) | (~related(C, D, E)))))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[14, 11])).
% 0.20/0.45 tff(16,plain,
% 0.20/0.45 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | ![D: $i] : ((~element(D, the_carrier(B))) | ![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(C))) | (~element(E, the_carrier(C))) | related(B, D, E) | (~related(C, D, E)))))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[15, 11])).
% 0.20/0.45 tff(17,plain,
% 0.20/0.45 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | ![D: $i] : ((~element(D, the_carrier(B))) | ![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(C))) | (~element(E, the_carrier(C))) | related(B, D, E) | (~related(C, D, E)))))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[16, 11])).
% 0.20/0.45 tff(18,plain,
% 0.20/0.46 (one_sorted_str(A!17) & net_str(B!18, A!17) & subnetstr(C!19, A!17, B!18) & element(D!20, the_carrier(B!18)) & (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21))))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[17, 10])).
% 0.20/0.46 tff(19,plain,
% 0.20/0.46 (net_str(B!18, A!17)),
% 0.20/0.46 inference(and_elim,[status(thm)],[18])).
% 0.20/0.46 tff(20,plain,
% 0.20/0.46 (one_sorted_str(A!17)),
% 0.20/0.46 inference(and_elim,[status(thm)],[18])).
% 0.20/0.46 tff(21,plain,
% 0.20/0.46 (^[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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(22,plain,
% 0.20/0.46 (![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.20/0.46 inference(quant_intro,[status(thm)],[21])).
% 0.20/0.46 tff(23,plain,
% 0.20/0.46 (^[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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(24,plain,
% 0.20/0.46 (![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.20/0.46 inference(quant_intro,[status(thm)],[23])).
% 0.20/0.46 tff(25,plain,
% 0.20/0.46 (^[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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(26,plain,
% 0.20/0.46 (![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.20/0.46 inference(quant_intro,[status(thm)],[25])).
% 0.20/0.46 tff(27,plain,
% 0.20/0.46 (![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.20/0.46 inference(transitivity,[status(thm)],[26, 24])).
% 0.20/0.46 tff(28,plain,
% 0.20/0.46 (^[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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(29,plain,
% 0.20/0.46 (![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.20/0.46 inference(quant_intro,[status(thm)],[28])).
% 0.20/0.46 tff(30,plain,
% 0.20/0.46 (![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.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(31,plain,
% 0.20/0.46 (^[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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(32,plain,
% 0.20/0.46 (![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.20/0.46 inference(quant_intro,[status(thm)],[31])).
% 0.20/0.46 tff(33,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/sandbox2/benchmark/theBenchmark.p','dt_m1_yellow_6')).
% 0.20/0.46 tff(34,plain,
% 0.20/0.46 (![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[33, 32])).
% 0.20/0.46 tff(35,plain,
% 0.20/0.46 (![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[34, 30])).
% 0.20/0.46 tff(36,plain,(
% 0.20/0.46 ![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.20/0.46 inference(skolemize,[status(sab)],[35])).
% 0.20/0.46 tff(37,plain,
% 0.20/0.46 (![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[36, 29])).
% 0.20/0.46 tff(38,plain,
% 0.20/0.46 (![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[37, 27])).
% 0.20/0.46 tff(39,plain,
% 0.20/0.46 (![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[38, 22])).
% 0.20/0.46 tff(40,plain,
% 0.20/0.46 (((~![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.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(41,plain,
% 0.20/0.46 (((~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.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(42,plain,
% 0.20/0.46 (((~![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.20/0.46 inference(monotonicity,[status(thm)],[41])).
% 0.20/0.46 tff(43,plain,
% 0.20/0.46 (((~![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.20/0.46 inference(transitivity,[status(thm)],[42, 40])).
% 0.20/0.46 tff(44,plain,
% 0.20/0.46 ((~![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.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(45,plain,
% 0.20/0.46 ((~![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.20/0.46 inference(modus_ponens,[status(thm)],[44, 43])).
% 0.20/0.46 tff(46,plain,
% 0.20/0.46 (![C: $i] : ((~subnetstr(C, A!17, B!18)) | net_str(C, A!17))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[45, 39, 20, 19])).
% 0.20/0.46 tff(47,plain,
% 0.20/0.46 (subnetstr(C!19, A!17, B!18)),
% 0.20/0.46 inference(and_elim,[status(thm)],[18])).
% 0.20/0.46 tff(48,plain,
% 0.20/0.46 (((~![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.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(49,plain,
% 0.20/0.46 ((~![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.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(50,plain,
% 0.20/0.46 ((~![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.20/0.46 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.20/0.46 tff(51,plain,
% 0.20/0.46 (net_str(C!19, A!17)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[50, 47, 46])).
% 0.20/0.46 tff(52,plain,
% 0.20/0.46 (^[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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(53,plain,
% 0.20/0.46 (![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.20/0.46 inference(quant_intro,[status(thm)],[52])).
% 0.20/0.46 tff(54,plain,
% 0.20/0.46 (^[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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(55,plain,
% 0.20/0.46 (![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.20/0.46 inference(quant_intro,[status(thm)],[54])).
% 0.20/0.46 tff(56,plain,
% 0.20/0.46 (![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.20/0.46 inference(transitivity,[status(thm)],[55, 53])).
% 0.20/0.46 tff(57,plain,
% 0.20/0.46 (^[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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(58,plain,
% 0.20/0.46 (![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.20/0.46 inference(quant_intro,[status(thm)],[57])).
% 0.20/0.46 tff(59,plain,
% 0.20/0.46 (![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.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(60,plain,
% 0.20/0.46 (^[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.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(61,plain,
% 0.20/0.46 (![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.20/0.46 inference(quant_intro,[status(thm)],[60])).
% 0.20/0.46 tff(62,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/sandbox2/benchmark/theBenchmark.p','d8_yellow_6')).
% 0.20/0.46 tff(63,plain,
% 0.20/0.46 (![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.20/0.46 inference(modus_ponens,[status(thm)],[62, 61])).
% 0.20/0.46 tff(64,plain,
% 0.20/0.46 (![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.20/0.46 inference(modus_ponens,[status(thm)],[63, 59])).
% 0.20/0.46 tff(65,plain,(
% 0.20/0.46 ![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.20/0.46 inference(skolemize,[status(sab)],[64])).
% 0.20/0.46 tff(66,plain,
% 0.20/0.46 (![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.20/0.46 inference(modus_ponens,[status(thm)],[65, 58])).
% 0.20/0.46 tff(67,plain,
% 0.20/0.46 (![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.20/0.46 inference(modus_ponens,[status(thm)],[66, 56])).
% 0.20/0.46 tff(68,plain,
% 0.20/0.46 (((~![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.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(69,plain,
% 0.20/0.46 ((~![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.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(70,plain,
% 0.20/0.46 ((~![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.20/0.46 inference(modus_ponens,[status(thm)],[69, 68])).
% 0.20/0.46 tff(71,plain,
% 0.20/0.46 (![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.20/0.46 inference(unit_resolution,[status(thm)],[70, 67, 20])).
% 0.20/0.46 tff(72,plain,
% 0.20/0.46 (((~![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.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(73,plain,
% 0.20/0.46 ((~![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.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(74,plain,
% 0.20/0.46 ((~![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.20/0.46 inference(modus_ponens,[status(thm)],[73, 72])).
% 0.20/0.46 tff(75,plain,
% 0.20/0.46 (![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.20/0.46 inference(unit_resolution,[status(thm)],[74, 19, 71])).
% 0.20/0.46 tff(76,plain,
% 0.20/0.46 (((~![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.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(77,plain,
% 0.20/0.46 ((~![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.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(78,plain,
% 0.20/0.46 ((~![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.20/0.46 inference(modus_ponens,[status(thm)],[77, 76])).
% 0.20/0.46 tff(79,plain,
% 0.20/0.46 (~(((~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.20/0.46 inference(unit_resolution,[status(thm)],[78, 75, 51])).
% 0.20/0.46 tff(80,plain,
% 0.20/0.46 ((((~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.20/0.46 inference(tautology,[status(thm)],[])).
% 0.20/0.46 tff(81,plain,
% 0.20/0.46 ((((~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.20/0.47 inference(unit_resolution,[status(thm)],[80, 47])).
% 0.20/0.47 tff(82,plain,
% 0.20/0.47 (~((~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.20/0.47 inference(unit_resolution,[status(thm)],[81, 79])).
% 0.20/0.47 tff(83,plain,
% 0.20/0.47 (((~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.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(84,plain,
% 0.20/0.47 (subrelstr(C!19, B!18)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[83, 82])).
% 0.20/0.47 tff(85,plain,
% 0.20/0.47 (^[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.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(86,plain,
% 0.20/0.47 (![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.20/0.47 inference(quant_intro,[status(thm)],[85])).
% 0.20/0.47 tff(87,plain,
% 0.20/0.47 (^[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.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(88,plain,
% 0.20/0.47 (![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.20/0.47 inference(quant_intro,[status(thm)],[87])).
% 0.20/0.47 tff(89,plain,
% 0.20/0.47 (![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.20/0.47 inference(transitivity,[status(thm)],[88, 86])).
% 0.20/0.47 tff(90,plain,
% 0.20/0.47 (![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.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(91,plain,
% 0.20/0.47 (^[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.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(92,plain,
% 0.20/0.47 (![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.20/0.47 inference(quant_intro,[status(thm)],[91])).
% 0.20/0.47 tff(93,axiom,(![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => rel_str(B)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dt_l1_waybel_0')).
% 0.20/0.47 tff(94,plain,
% 0.20/0.47 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[93, 92])).
% 0.20/0.47 tff(95,plain,
% 0.20/0.47 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[94, 90])).
% 0.20/0.47 tff(96,plain,(
% 0.20/0.47 ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.20/0.47 inference(skolemize,[status(sab)],[95])).
% 0.20/0.47 tff(97,plain,
% 0.20/0.47 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[96, 89])).
% 0.20/0.47 tff(98,plain,
% 0.20/0.47 (((~![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.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(99,plain,
% 0.20/0.47 ((~![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.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(100,plain,
% 0.20/0.47 ((~![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.20/0.47 inference(modus_ponens,[status(thm)],[99, 98])).
% 0.20/0.47 tff(101,plain,
% 0.20/0.47 (![B: $i] : (rel_str(B) | (~net_str(B, A!17)))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[100, 97, 20])).
% 0.20/0.47 tff(102,plain,
% 0.20/0.47 (((~![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.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(103,plain,
% 0.20/0.47 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!17)))) | (rel_str(B!18) | (~net_str(B!18, A!17)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(104,plain,
% 0.20/0.47 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!17)))) | rel_str(B!18) | (~net_str(B!18, A!17))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.20/0.47 tff(105,plain,
% 0.20/0.47 (rel_str(B!18)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[104, 19, 101])).
% 0.20/0.47 tff(106,plain,
% 0.20/0.47 (^[A: $i] : refl(((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))) <=> ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(107,plain,
% 0.20/0.47 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[106])).
% 0.20/0.47 tff(108,plain,
% 0.20/0.47 (^[A: $i] : rewrite(((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))) <=> ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(109,plain,
% 0.20/0.47 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[108])).
% 0.20/0.47 tff(110,plain,
% 0.20/0.47 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))),
% 0.20/0.47 inference(transitivity,[status(thm)],[109, 107])).
% 0.20/0.47 tff(111,plain,
% 0.20/0.47 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(112,plain,
% 0.20/0.47 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : trans(monotonicity(quant_intro(proof_bind(^[D: $i] : trans(monotonicity(trans(quant_intro(proof_bind(^[E: $i] : trans(monotonicity(trans(quant_intro(proof_bind(^[F: $i] : trans(monotonicity(trans(monotonicity(rewrite((((E = C) & (F = D)) & related(B, E, F)) <=> ((E = C) & (F = D) & related(B, E, F))), (((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)) <=> (((E = C) & (F = D) & related(B, E, F)) => related(A, C, D)))), rewrite((((E = C) & (F = D) & related(B, E, F)) => related(A, C, D)) <=> ((~((E = C) & (F = D) & related(B, E, F))) | related(A, C, D))), (((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)) <=> ((~((E = C) & (F = D) & related(B, E, F))) | related(A, C, D)))), ((element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))) <=> (element(F, the_carrier(B)) => ((~((E = C) & (F = D) & related(B, E, F))) | related(A, C, D))))), rewrite((element(F, the_carrier(B)) => ((~((E = C) & (F = D) & related(B, E, F))) | related(A, C, D))) <=> (related(A, C, D) | (~((E = C) & (F = D) & related(B, E, F))) | (~element(F, the_carrier(B))))), ((element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))) <=> (related(A, C, D) | (~((E = C) & (F = D) & related(B, E, F))) | (~element(F, the_carrier(B))))))), (![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))) <=> ![F: $i] : (related(A, C, D) | (~((E = C) & (F = D) & related(B, E, F))) | (~element(F, the_carrier(B)))))), trans(der(![F: $i] : (related(A, C, D) | (~((E = C) & (F = D) & related(B, E, F))) | (~element(F, the_carrier(B)))) <=> ![F: $i] : ((~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C)))), elim_unused(![F: $i] : ((~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C))) <=> ((~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C)))), (![F: $i] : (related(A, C, D) | (~((E = C) & (F = D) & related(B, E, F))) | (~element(F, the_carrier(B)))) <=> ((~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C))))), (![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))) <=> ((~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C))))), ((element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)))) <=> (element(E, the_carrier(B)) => ((~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C)))))), rewrite((element(E, the_carrier(B)) => ((~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C)))) <=> ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C)))), ((element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)))) <=> ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C)))))), (![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)))) <=> ![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C))))), trans(der(![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C))) <=> ![E: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))), elim_unused(![E: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))) <=> ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))), (![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, E, D)) | (~(E = C))) <=> ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))), (![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)))) <=> ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))), ((element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))))) <=> (element(D, the_carrier(A)) => ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))), rewrite((element(D, the_carrier(A)) => ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))) <=> ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))), ((element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))))) <=> ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))), (![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))))) <=> ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))), ((element(C, the_carrier(A)) => ![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)))))) <=> (element(C, the_carrier(A)) => ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))), rewrite((element(C, the_carrier(A)) => ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))) <=> ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))), ((element(C, the_carrier(A)) => ![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)))))) <=> ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))), (![C: $i] : (element(C, the_carrier(A)) => ![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)))))) <=> ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))), ((subrelstr(B, A) => ![C: $i] : (element(C, the_carrier(A)) => ![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))))))) <=> (subrelstr(B, A) => ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))), rewrite((subrelstr(B, A) => ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))) <=> ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))), ((subrelstr(B, A) => ![C: $i] : (element(C, the_carrier(A)) => ![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))))))) <=> ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))))), (![B: $i] : (subrelstr(B, A) => ![C: $i] : (element(C, the_carrier(A)) => ![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))))))) <=> ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))), ((rel_str(A) => ![B: $i] : (subrelstr(B, A) => ![C: $i] : (element(C, the_carrier(A)) => ![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)))))))) <=> (rel_str(A) => ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))))), rewrite((rel_str(A) => ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D)))))) <=> ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))), ((rel_str(A) => ![B: $i] : (subrelstr(B, A) => ![C: $i] : (element(C, the_carrier(A)) => ![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)))))))) <=> ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(113,plain,
% 0.20/0.47 (![A: $i] : (rel_str(A) => ![B: $i] : (subrelstr(B, A) => ![C: $i] : (element(C, the_carrier(A)) => ![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D)))))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[112])).
% 0.20/0.47 tff(114,axiom,(![A: $i] : (rel_str(A) => ![B: $i] : (subrelstr(B, A) => ![C: $i] : (element(C, the_carrier(A)) => ![D: $i] : (element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((E = C) & (F = D)) & related(B, E, F)) => related(A, C, D))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t60_yellow_0')).
% 0.20/0.47 tff(115,plain,
% 0.20/0.47 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[114, 113])).
% 0.20/0.47 tff(116,plain,
% 0.20/0.47 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[115, 111])).
% 0.20/0.47 tff(117,plain,(
% 0.20/0.47 ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))),
% 0.20/0.47 inference(skolemize,[status(sab)],[116])).
% 0.20/0.47 tff(118,plain,
% 0.20/0.47 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[117, 110])).
% 0.20/0.47 tff(119,plain,
% 0.20/0.47 (((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))) | ((~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D)))))) <=> ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))) | (~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D)))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(120,plain,
% 0.20/0.47 (((~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B!18, C, D) | (~related(B, C, D)))))) <=> ((~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D)))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(121,plain,
% 0.20/0.47 (((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))) | ((~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B!18, C, D) | (~related(B, C, D))))))) <=> ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))) | ((~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[120])).
% 0.20/0.47 tff(122,plain,
% 0.20/0.47 (((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))) | ((~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B!18, C, D) | (~related(B, C, D))))))) <=> ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))) | (~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D)))))),
% 0.20/0.47 inference(transitivity,[status(thm)],[121, 119])).
% 0.20/0.47 tff(123,plain,
% 0.20/0.47 ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))) | ((~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B!18, C, D) | (~related(B, C, D))))))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(124,plain,
% 0.20/0.47 ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | ![C: $i] : ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(A, C, D) | (~related(B, C, D))))))) | (~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[123, 122])).
% 0.20/0.47 tff(125,plain,
% 0.20/0.47 ((~rel_str(B!18)) | ![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[124, 118])).
% 0.20/0.47 tff(126,plain,
% 0.20/0.47 (![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[125, 105])).
% 0.20/0.47 tff(127,plain,
% 0.20/0.47 (((~![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))) | ((~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D)))))) <=> ((~![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))) | (~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D)))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(128,plain,
% 0.20/0.47 (((~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D)))) <=> ((~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D)))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(129,plain,
% 0.20/0.47 (((~![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))) | ((~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))) <=> ((~![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))) | ((~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[128])).
% 0.20/0.47 tff(130,plain,
% 0.20/0.47 (((~![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))) | ((~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))) <=> ((~![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))) | (~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D)))))),
% 0.20/0.47 inference(transitivity,[status(thm)],[129, 127])).
% 0.20/0.47 tff(131,plain,
% 0.20/0.47 ((~![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))) | ((~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(132,plain,
% 0.20/0.47 ((~![B: $i] : ((~subrelstr(B, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | (~related(B, C, D)) | (~element(D, the_carrier(B!18))) | related(B!18, C, D))))) | (~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[131, 130])).
% 0.20/0.48 tff(133,plain,
% 0.20/0.48 ((~subrelstr(C!19, B!18)) | ![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[132, 126])).
% 0.20/0.48 tff(134,plain,
% 0.20/0.48 (![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[133, 84])).
% 0.20/0.48 tff(135,plain,
% 0.20/0.48 (element(D!20, the_carrier(B!18))),
% 0.20/0.48 inference(and_elim,[status(thm)],[18])).
% 0.20/0.48 tff(136,plain,
% 0.20/0.48 (((~![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))) | ((~element(D!20, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D))))) <=> ((~![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))) | (~element(D!20, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(137,plain,
% 0.20/0.48 (((~element(D!20, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, D!20, D) | (~element(D!20, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, D!20, D)))) <=> ((~element(D!20, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(138,plain,
% 0.20/0.48 (((~![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))) | ((~element(D!20, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, D!20, D) | (~element(D!20, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, D!20, D))))) <=> ((~![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))) | ((~element(D!20, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[137])).
% 0.20/0.48 tff(139,plain,
% 0.20/0.48 (((~![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))) | ((~element(D!20, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, D!20, D) | (~element(D!20, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, D!20, D))))) <=> ((~![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))) | (~element(D!20, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D))))),
% 0.20/0.48 inference(transitivity,[status(thm)],[138, 136])).
% 0.20/0.48 tff(140,plain,
% 0.20/0.48 ((~![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))) | ((~element(D!20, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, D!20, D) | (~element(D!20, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, D!20, D))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(141,plain,
% 0.20/0.48 ((~![C: $i] : ((~element(C, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | related(B!18, C, D) | (~element(C, the_carrier(C!19))) | (~element(D, the_carrier(C!19))) | (~related(C!19, C, D))))) | (~element(D!20, the_carrier(B!18))) | ![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[140, 139])).
% 0.20/0.48 tff(142,plain,
% 0.20/0.48 (![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[141, 135, 134])).
% 0.20/0.48 tff(143,plain,
% 0.20/0.48 (~((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))),
% 0.20/0.48 inference(and_elim,[status(thm)],[18])).
% 0.20/0.48 tff(144,plain,
% 0.20/0.48 (related(C!19, D!20, E!21)),
% 0.20/0.48 inference(or_elim,[status(thm)],[143])).
% 0.20/0.48 tff(145,plain,
% 0.20/0.48 (~related(B!18, D!20, E!21)),
% 0.20/0.48 inference(or_elim,[status(thm)],[143])).
% 0.20/0.48 tff(146,plain,
% 0.20/0.48 (element(E!21, the_carrier(C!19))),
% 0.20/0.48 inference(or_elim,[status(thm)],[143])).
% 0.20/0.48 tff(147,plain,
% 0.20/0.48 (element(E!21, the_carrier(B!18))),
% 0.20/0.48 inference(or_elim,[status(thm)],[143])).
% 0.20/0.48 tff(148,plain,
% 0.20/0.48 (element(D!20, the_carrier(C!19))),
% 0.20/0.48 inference(or_elim,[status(thm)],[143])).
% 0.20/0.48 tff(149,plain,
% 0.20/0.48 (((~![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))) | ((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))) <=> ((~![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))) | (~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(150,plain,
% 0.20/0.48 (((~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21))) <=> ((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(151,plain,
% 0.20/0.48 (((~![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))) | ((~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))) <=> ((~![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))) | ((~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21))))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[150])).
% 0.20/0.48 tff(152,plain,
% 0.20/0.48 (((~![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))) | ((~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))) <=> ((~![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))) | (~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))),
% 0.20/0.48 inference(transitivity,[status(thm)],[151, 149])).
% 0.20/0.48 tff(153,plain,
% 0.20/0.48 ((~![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))) | ((~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(154,plain,
% 0.20/0.48 ((~![D: $i] : ((~element(D, the_carrier(B!18))) | (~element(D, the_carrier(C!19))) | (~element(D!20, the_carrier(C!19))) | related(B!18, D!20, D) | (~related(C!19, D!20, D)))) | (~element(D!20, the_carrier(C!19))) | (~element(E!21, the_carrier(B!18))) | (~element(E!21, the_carrier(C!19))) | related(B!18, D!20, E!21) | (~related(C!19, D!20, E!21))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[153, 152])).
% 0.20/0.48 tff(155,plain,
% 0.20/0.48 ($false),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[154, 148, 147, 146, 145, 144, 142])).
% 0.20/0.48 % SZS output end Proof
% 0.20/0.48 % E exiting
%------------------------------------------------------------------------------