%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU375+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:45 AM UTC 2025
% Result : Theorem 0.12s 0.37s
% Output : Proof 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU375+1 : TPTP v9.0.0. Released v3.3.0.
% 0.11/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:05 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.37 % SZS status Theorem
% 0.12/0.37 % SZS output start Proof
% 0.12/0.37 tff(in_type, type, (
% 0.12/0.37 in: ( $i * $i ) > $o)).
% 0.12/0.37 tff(the_carrier_type, type, (
% 0.12/0.37 the_carrier: $i > $i)).
% 0.12/0.37 tff(tptp_fun_C_16_type, type, (
% 0.12/0.37 tptp_fun_C_16: $i)).
% 0.12/0.37 tff(tptp_fun_D_17_type, type, (
% 0.12/0.37 tptp_fun_D_17: $i)).
% 0.12/0.37 tff(related_type, type, (
% 0.12/0.37 related: ( $i * $i * $i ) > $o)).
% 0.12/0.37 tff(tptp_fun_B_15_type, type, (
% 0.12/0.37 tptp_fun_B_15: $i)).
% 0.12/0.37 tff(element_type, type, (
% 0.12/0.37 element: ( $i * $i ) > $o)).
% 0.12/0.37 tff(full_subrelstr_type, type, (
% 0.12/0.37 full_subrelstr: ( $i * $i ) > $o)).
% 0.12/0.37 tff(subrelstr_type, type, (
% 0.12/0.37 subrelstr: ( $i * $i ) > $o)).
% 0.12/0.37 tff(full_subnetstr_type, type, (
% 0.12/0.37 full_subnetstr: ( $i * $i * $i ) > $o)).
% 0.12/0.37 tff(tptp_fun_A_14_type, type, (
% 0.12/0.37 tptp_fun_A_14: $i)).
% 0.12/0.37 tff(subnetstr_type, type, (
% 0.12/0.37 subnetstr: ( $i * $i * $i ) > $o)).
% 0.12/0.37 tff(net_str_type, type, (
% 0.12/0.37 net_str: ( $i * $i ) > $o)).
% 0.12/0.37 tff(one_sorted_str_type, type, (
% 0.12/0.37 one_sorted_str: $i > $o)).
% 0.12/0.37 tff(tptp_fun_E_18_type, type, (
% 0.12/0.37 tptp_fun_E_18: $i)).
% 0.12/0.37 tff(empty_carrier_type, type, (
% 0.12/0.37 empty_carrier: $i > $o)).
% 0.12/0.37 tff(rel_str_type, type, (
% 0.12/0.37 rel_str: $i > $o)).
% 0.12/0.37 tff(empty_type, type, (
% 0.12/0.37 empty: $i > $o)).
% 0.12/0.37 tff(1,plain,
% 0.12/0.37 ((one_sorted_str(A!14) & ((~empty_carrier(B!15)) & net_str(B!15, A!14) & (~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))) <=> (one_sorted_str(A!14) & (~empty_carrier(B!15)) & net_str(B!15, A!14) & (~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(2,plain,
% 0.12/0.37 ((((~empty_carrier(B!15)) & net_str(B!15, A!14)) & ((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))) <=> ((~empty_carrier(B!15)) & net_str(B!15, A!14) & (~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(3,plain,
% 0.12/0.37 ((((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15)) & (element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))) <=> ((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(4,plain,
% 0.12/0.37 ((element(D!17, the_carrier(B!15)) & (~((~element(E!18, the_carrier(B!15))) | (~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18))))) <=> (element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(5,plain,
% 0.12/0.37 ((((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15)) & (element(D!17, the_carrier(B!15)) & (~((~element(E!18, the_carrier(B!15))) | (~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))) <=> (((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15)) & (element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18))))))),
% 0.12/0.37 inference(monotonicity,[status(thm)],[4])).
% 0.12/0.37 tff(6,plain,
% 0.12/0.37 ((((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15)) & (element(D!17, the_carrier(B!15)) & (~((~element(E!18, the_carrier(B!15))) | (~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))) <=> ((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))),
% 0.12/0.37 inference(transitivity,[status(thm)],[5, 3])).
% 0.12/0.37 tff(7,plain,
% 0.12/0.37 ((((~empty_carrier(B!15)) & net_str(B!15, A!14)) & (((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15)) & (element(D!17, the_carrier(B!15)) & (~((~element(E!18, the_carrier(B!15))) | (~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18))))))) <=> (((~empty_carrier(B!15)) & net_str(B!15, A!14)) & ((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18))))))),
% 0.12/0.37 inference(monotonicity,[status(thm)],[6])).
% 0.12/0.37 tff(8,plain,
% 0.12/0.37 ((((~empty_carrier(B!15)) & net_str(B!15, A!14)) & (((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15)) & (element(D!17, the_carrier(B!15)) & (~((~element(E!18, the_carrier(B!15))) | (~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18))))))) <=> ((~empty_carrier(B!15)) & net_str(B!15, A!14) & (~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))),
% 0.12/0.37 inference(transitivity,[status(thm)],[7, 2])).
% 0.12/0.37 tff(9,plain,
% 0.12/0.37 ((one_sorted_str(A!14) & (((~empty_carrier(B!15)) & net_str(B!15, A!14)) & (((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15)) & (element(D!17, the_carrier(B!15)) & (~((~element(E!18, the_carrier(B!15))) | (~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))))) <=> (one_sorted_str(A!14) & ((~empty_carrier(B!15)) & net_str(B!15, A!14) & (~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18))))))),
% 0.12/0.37 inference(monotonicity,[status(thm)],[8])).
% 0.12/0.37 tff(10,plain,
% 0.12/0.37 ((one_sorted_str(A!14) & (((~empty_carrier(B!15)) & net_str(B!15, A!14)) & (((~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15)) & (element(D!17, the_carrier(B!15)) & (~((~element(E!18, the_carrier(B!15))) | (~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))))) <=> (one_sorted_str(A!14) & (~empty_carrier(B!15)) & net_str(B!15, A!14) & (~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))))),
% 0.12/0.38 inference(transitivity,[status(thm)],[9, 1])).
% 0.12/0.38 tff(11,plain,
% 0.12/0.38 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : ((~((~empty_carrier(C)) & full_subnetstr(C, A, B) & 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(C, D, E) | (~related(B, D, E)))))))) <=> (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : ((~((~empty_carrier(C)) & full_subnetstr(C, A, B) & 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(C, D, E) | (~related(B, D, E))))))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(12,plain,
% 0.12/0.38 ((~![A: $i] : (one_sorted_str(A) => ![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : ((((~empty_carrier(C)) & full_subnetstr(C, A, B)) & 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(B, D, E)) => related(C, F, G)))))))))) <=> (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : ((~((~empty_carrier(C)) & full_subnetstr(C, A, B) & 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(C, D, E) | (~related(B, D, E))))))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(13,axiom,(~![A: $i] : (one_sorted_str(A) => ![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : ((((~empty_carrier(C)) & full_subnetstr(C, A, B)) & 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(B, D, E)) => related(C, F, G)))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t21_yellow_6')).
% 0.12/0.38 tff(14,plain,
% 0.12/0.38 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : ((~((~empty_carrier(C)) & full_subnetstr(C, A, B) & 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(C, D, E) | (~related(B, D, E)))))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[13, 12])).
% 0.12/0.38 tff(15,plain,
% 0.12/0.38 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : ((~((~empty_carrier(C)) & full_subnetstr(C, A, B) & 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(C, D, E) | (~related(B, D, E)))))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[14, 11])).
% 0.12/0.38 tff(16,plain,
% 0.12/0.38 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : ((~((~empty_carrier(C)) & full_subnetstr(C, A, B) & 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(C, D, E) | (~related(B, D, E)))))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[15, 11])).
% 0.12/0.38 tff(17,plain,
% 0.12/0.38 (~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : ((~((~empty_carrier(C)) & full_subnetstr(C, A, B) & 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(C, D, E) | (~related(B, D, E)))))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[16, 11])).
% 0.12/0.38 tff(18,plain,
% 0.12/0.38 (one_sorted_str(A!14) & (~empty_carrier(B!15)) & net_str(B!15, A!14) & (~empty_carrier(C!16)) & full_subnetstr(C!16, A!14, B!15) & subnetstr(C!16, A!14, B!15) & element(D!17, the_carrier(B!15)) & (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[17, 10])).
% 0.12/0.38 tff(19,plain,
% 0.12/0.38 (one_sorted_str(A!14)),
% 0.12/0.38 inference(and_elim,[status(thm)],[18])).
% 0.12/0.38 tff(20,plain,
% 0.12/0.38 (^[A: $i] : refl(((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B)))))) <=> ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B)))))))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(21,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B)))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B))))))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[20])).
% 0.12/0.38 tff(22,plain,
% 0.12/0.38 (^[A: $i] : rewrite(((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B)))))) <=> ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B)))))))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(23,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B)))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B))))))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[22])).
% 0.12/0.38 tff(24,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B)))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B))))))),
% 0.12/0.38 inference(transitivity,[status(thm)],[23, 21])).
% 0.12/0.38 tff(25,plain,
% 0.12/0.38 (^[A: $i] : rewrite(((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))) <=> ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B)))))))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(26,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B))))))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[25])).
% 0.12/0.38 tff(27,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(28,plain,
% 0.12/0.38 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : rewrite((subnetstr(C, A, B) => (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))) <=> ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))), (![C: $i] : (subnetstr(C, A, B) => (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))) <=> ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))), ((net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))) <=> (net_str(B, A) => ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))))), rewrite((net_str(B, A) => ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))) <=> ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))), ((net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))) <=> ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))))), (![B: $i] : (net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))) <=> ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))))), ((one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))) <=> (one_sorted_str(A) => ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))))), rewrite((one_sorted_str(A) => ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))) <=> ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))))), ((one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))) <=> ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))))))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(29,plain,
% 0.12/0.38 (![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B)))))) <=> ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[28])).
% 0.12/0.38 tff(30,axiom,(![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => ![C: $i] : (subnetstr(C, A, B) => (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','d9_yellow_6')).
% 0.12/0.38 tff(31,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[30, 29])).
% 0.12/0.38 tff(32,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[31, 27])).
% 0.12/0.38 tff(33,plain,(
% 0.12/0.38 ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (full_subnetstr(C, A, B) <=> (full_subrelstr(C, B) & subrelstr(C, B))))))),
% 0.12/0.38 inference(skolemize,[status(sab)],[32])).
% 0.12/0.38 tff(34,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B))))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[33, 26])).
% 0.12/0.38 tff(35,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B))))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[34, 24])).
% 0.12/0.38 tff(36,plain,
% 0.12/0.38 (((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B))))))) | ((~one_sorted_str(A!14)) | ![B: $i] : ((~net_str(B, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A!14, B))))))) <=> ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B))))))) | (~one_sorted_str(A!14)) | ![B: $i] : ((~net_str(B, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A!14, B))))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(37,plain,
% 0.12/0.38 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B))))))) | ((~one_sorted_str(A!14)) | ![B: $i] : ((~net_str(B, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A!14, B))))))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(38,plain,
% 0.12/0.38 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A, B))))))) | (~one_sorted_str(A!14)) | ![B: $i] : ((~net_str(B, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A!14, B)))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.12/0.38 tff(39,plain,
% 0.12/0.38 (![B: $i] : ((~net_str(B, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A!14, B)))))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[38, 35, 19])).
% 0.12/0.38 tff(40,plain,
% 0.12/0.38 (net_str(B!15, A!14)),
% 0.12/0.38 inference(and_elim,[status(thm)],[18])).
% 0.12/0.38 tff(41,plain,
% 0.12/0.38 (((~![B: $i] : ((~net_str(B, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A!14, B)))))) | ((~net_str(B!15, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | (~(((~full_subrelstr(C, B!15)) | (~subrelstr(C, B!15))) <=> full_subnetstr(C, A!14, B!15)))))) <=> ((~![B: $i] : ((~net_str(B, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A!14, B)))))) | (~net_str(B!15, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | (~(((~full_subrelstr(C, B!15)) | (~subrelstr(C, B!15))) <=> full_subnetstr(C, A!14, B!15)))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(42,plain,
% 0.12/0.38 ((~![B: $i] : ((~net_str(B, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A!14, B)))))) | ((~net_str(B!15, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | (~(((~full_subrelstr(C, B!15)) | (~subrelstr(C, B!15))) <=> full_subnetstr(C, A!14, B!15)))))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(43,plain,
% 0.12/0.38 ((~![B: $i] : ((~net_str(B, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B)) | (~(((~full_subrelstr(C, B)) | (~subrelstr(C, B))) <=> full_subnetstr(C, A!14, B)))))) | (~net_str(B!15, A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | (~(((~full_subrelstr(C, B!15)) | (~subrelstr(C, B!15))) <=> full_subnetstr(C, A!14, B!15))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[42, 41])).
% 0.12/0.38 tff(44,plain,
% 0.12/0.38 (![C: $i] : ((~subnetstr(C, A!14, B!15)) | (~(((~full_subrelstr(C, B!15)) | (~subrelstr(C, B!15))) <=> full_subnetstr(C, A!14, B!15))))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[43, 40, 39])).
% 0.12/0.38 tff(45,plain,
% 0.12/0.38 (subnetstr(C!16, A!14, B!15)),
% 0.12/0.38 inference(and_elim,[status(thm)],[18])).
% 0.12/0.38 tff(46,plain,
% 0.12/0.38 (((~![C: $i] : ((~subnetstr(C, A!14, B!15)) | (~(((~full_subrelstr(C, B!15)) | (~subrelstr(C, B!15))) <=> full_subnetstr(C, A!14, B!15))))) | ((~subnetstr(C!16, A!14, B!15)) | (~(((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15))) <=> full_subnetstr(C!16, A!14, B!15))))) <=> ((~![C: $i] : ((~subnetstr(C, A!14, B!15)) | (~(((~full_subrelstr(C, B!15)) | (~subrelstr(C, B!15))) <=> full_subnetstr(C, A!14, B!15))))) | (~subnetstr(C!16, A!14, B!15)) | (~(((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15))) <=> full_subnetstr(C!16, A!14, B!15))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(47,plain,
% 0.12/0.38 ((~![C: $i] : ((~subnetstr(C, A!14, B!15)) | (~(((~full_subrelstr(C, B!15)) | (~subrelstr(C, B!15))) <=> full_subnetstr(C, A!14, B!15))))) | ((~subnetstr(C!16, A!14, B!15)) | (~(((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15))) <=> full_subnetstr(C!16, A!14, B!15))))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(48,plain,
% 0.12/0.38 ((~![C: $i] : ((~subnetstr(C, A!14, B!15)) | (~(((~full_subrelstr(C, B!15)) | (~subrelstr(C, B!15))) <=> full_subnetstr(C, A!14, B!15))))) | (~subnetstr(C!16, A!14, B!15)) | (~(((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15))) <=> full_subnetstr(C!16, A!14, B!15)))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[47, 46])).
% 0.12/0.38 tff(49,plain,
% 0.12/0.38 (~(((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15))) <=> full_subnetstr(C!16, A!14, B!15))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[48, 45, 44])).
% 0.12/0.38 tff(50,plain,
% 0.12/0.38 (full_subnetstr(C!16, A!14, B!15)),
% 0.12/0.38 inference(and_elim,[status(thm)],[18])).
% 0.12/0.38 tff(51,plain,
% 0.12/0.38 ((((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15))) <=> full_subnetstr(C!16, A!14, B!15)) | (~((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)))) | (~full_subnetstr(C!16, A!14, B!15))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(52,plain,
% 0.12/0.38 ((((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15))) <=> full_subnetstr(C!16, A!14, B!15)) | (~((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15))))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[51, 50])).
% 0.12/0.38 tff(53,plain,
% 0.12/0.38 (~((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[52, 49])).
% 0.12/0.38 tff(54,plain,
% 0.12/0.38 (((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15))) | full_subrelstr(C!16, B!15)),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(55,plain,
% 0.12/0.38 (full_subrelstr(C!16, B!15)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[54, 53])).
% 0.12/0.38 tff(56,plain,
% 0.12/0.38 (((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15))) | subrelstr(C!16, B!15)),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(57,plain,
% 0.12/0.38 (subrelstr(C!16, B!15)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[56, 53])).
% 0.12/0.38 tff(58,plain,
% 0.12/0.38 (^[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.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(59,plain,
% 0.12/0.38 (![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.12/0.38 inference(quant_intro,[status(thm)],[58])).
% 0.12/0.38 tff(60,plain,
% 0.12/0.38 (^[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.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(61,plain,
% 0.12/0.38 (![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.12/0.38 inference(quant_intro,[status(thm)],[60])).
% 0.12/0.38 tff(62,plain,
% 0.12/0.38 (![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.12/0.38 inference(transitivity,[status(thm)],[61, 59])).
% 0.12/0.38 tff(63,plain,
% 0.12/0.38 (![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.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(64,plain,
% 0.12/0.38 (^[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.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(65,plain,
% 0.12/0.38 (![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.12/0.38 inference(quant_intro,[status(thm)],[64])).
% 0.12/0.38 tff(66,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.12/0.38 tff(67,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.12/0.38 tff(68,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[67, 63])).
% 0.12/0.38 tff(69,plain,(
% 0.12/0.38 ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.12/0.38 inference(skolemize,[status(sab)],[68])).
% 0.12/0.38 tff(70,plain,
% 0.12/0.38 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[69, 62])).
% 0.12/0.38 tff(71,plain,
% 0.12/0.38 (((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | ((~one_sorted_str(A!14)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!14))))) <=> ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | (~one_sorted_str(A!14)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!14))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(72,plain,
% 0.12/0.38 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | ((~one_sorted_str(A!14)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!14))))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(73,plain,
% 0.12/0.38 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | (~one_sorted_str(A!14)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!14)))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[72, 71])).
% 0.12/0.38 tff(74,plain,
% 0.12/0.38 (![B: $i] : (rel_str(B) | (~net_str(B, A!14)))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[73, 70, 19])).
% 0.12/0.38 tff(75,plain,
% 0.12/0.38 (((~![B: $i] : (rel_str(B) | (~net_str(B, A!14)))) | (rel_str(B!15) | (~net_str(B!15, A!14)))) <=> ((~![B: $i] : (rel_str(B) | (~net_str(B, A!14)))) | rel_str(B!15) | (~net_str(B!15, A!14)))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(76,plain,
% 0.12/0.38 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!14)))) | (rel_str(B!15) | (~net_str(B!15, A!14)))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(77,plain,
% 0.12/0.38 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!14)))) | rel_str(B!15) | (~net_str(B!15, A!14))),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[76, 75])).
% 0.12/0.38 tff(78,plain,
% 0.12/0.38 (rel_str(B!15)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[77, 40, 74])).
% 0.12/0.38 tff(79,plain,
% 0.12/0.38 (^[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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A)))) <=> ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(80,plain,
% 0.12/0.38 (![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A)))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[79])).
% 0.12/0.38 tff(81,plain,
% 0.12/0.38 (^[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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A)))) <=> ((~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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A)))))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(82,plain,
% 0.12/0.38 (![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A)))) <=> ![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A))))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[81])).
% 0.12/0.38 tff(83,plain,
% 0.12/0.38 (^[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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A)))) <=> ((~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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A)))))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(84,plain,
% 0.12/0.38 (![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A)))) <=> ![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A))))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[83])).
% 0.12/0.38 tff(85,plain,
% 0.12/0.38 (![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A)))) <=> ![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A))))),
% 0.12/0.38 inference(transitivity,[status(thm)],[84, 82])).
% 0.12/0.38 tff(86,plain,
% 0.12/0.38 (^[A: $i] : rewrite(((~rel_str(A)) | ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))) <=> ((~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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A)))))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(87,plain,
% 0.12/0.38 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))) <=> ![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A))))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[86])).
% 0.12/0.38 tff(88,plain,
% 0.12/0.38 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(89,plain,
% 0.12/0.38 (^[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(trans(monotonicity(trans(monotonicity(rewrite((((E = C) & (F = D)) & related(A, C, D)) <=> ((E = C) & (F = D) & related(A, C, D))), (((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) <=> (((E = C) & (F = D) & related(A, C, D)) & in(E, the_carrier(B))))), rewrite((((E = C) & (F = D) & related(A, C, D)) & in(E, the_carrier(B))) <=> ((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)))), (((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) <=> ((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B))))), ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) <=> (((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B))) & in(F, the_carrier(B))))), rewrite((((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B))) & in(F, the_carrier(B))) <=> ((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B)))), ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) <=> ((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B))))), (((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)) <=> (((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B))) => related(B, E, F)))), rewrite((((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B))) => related(B, E, F)) <=> ((~((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B)))) | related(B, E, F))), (((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)) <=> ((~((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B)))) | related(B, E, F)))), ((element(F, the_carrier(B)) => ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))) <=> (element(F, the_carrier(B)) => ((~((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B)))) | related(B, E, F))))), rewrite((element(F, the_carrier(B)) => ((~((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B)))) | related(B, E, F))) <=> (related(B, E, F) | (~((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B)))) | (~element(F, the_carrier(B))))), ((element(F, the_carrier(B)) => ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))) <=> (related(B, E, F) | (~((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B)))) | (~element(F, the_carrier(B))))))), (![F: $i] : (element(F, the_carrier(B)) => ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))) <=> ![F: $i] : (related(B, E, F) | (~((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B)))) | (~element(F, the_carrier(B)))))), trans(der(![F: $i] : (related(B, E, F) | (~((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B)))) | (~element(F, the_carrier(B)))) <=> ![F: $i] : ((~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B))))), elim_unused(![F: $i] : ((~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B)))) <=> ((~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B))))), (![F: $i] : (related(B, E, F) | (~((E = C) & (F = D) & related(A, C, D) & in(E, the_carrier(B)) & in(F, the_carrier(B)))) | (~element(F, the_carrier(B)))) <=> ((~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B)))))), (![F: $i] : (element(F, the_carrier(B)) => ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))) <=> ((~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B)))))), ((element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)))) <=> (element(E, the_carrier(B)) => ((~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B))))))), rewrite((element(E, the_carrier(B)) => ((~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B))))) <=> ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B))))), ((element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)))) <=> ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B))))))), (![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)))) <=> ![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B)))))), trans(trans(der(![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B)))) <=> ![E: $i] : ((~in(C, the_carrier(B))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(D, the_carrier(B))) | (~related(A, C, D)))), elim_unused(![E: $i] : ((~in(C, the_carrier(B))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(D, the_carrier(B))) | (~related(A, C, D))) <=> ((~in(C, the_carrier(B))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(D, the_carrier(B))) | (~related(A, C, D)))), (![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B)))) <=> ((~in(C, the_carrier(B))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(D, the_carrier(B))) | (~related(A, C, D))))), rewrite(((~in(C, the_carrier(B))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(D, the_carrier(B))) | (~related(A, C, D))) <=> ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))), (![E: $i] : ((~element(E, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, E, D) | (~in(D, the_carrier(B))) | (~(E = C)) | (~related(A, C, D)) | (~in(E, the_carrier(B)))) <=> ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))), (![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)))) <=> ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))), ((element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))))) <=> (element(D, the_carrier(A)) => ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))), rewrite((element(D, the_carrier(A)) => ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) <=> ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))), ((element(D, the_carrier(A)) => ![E: $i] : (element(E, the_carrier(B)) => ![F: $i] : (element(F, the_carrier(B)) => ((((((E = C) & (F = D)) & related(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))))) <=> ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))), (![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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))))) <=> ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))), ((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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)))))) <=> (element(C, the_carrier(A)) => ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))), rewrite((element(C, the_carrier(A)) => ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) <=> ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))), ((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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)))))) <=> ((~element(C, the_carrier(A))) | ![D: $i] : ((~element(D, the_carrier(A))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))), (![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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)))))) <=> ![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))), (((full_subrelstr(B, A) & 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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))))))) <=> ((full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))), rewrite(((full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))) <=> ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))), (((full_subrelstr(B, A) & 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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))))))) <=> ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))))), (![B: $i] : ((full_subrelstr(B, A) & 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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))))))) <=> ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))), ((rel_str(A) => ![B: $i] : ((full_subrelstr(B, A) & 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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)))))))) <=> (rel_str(A) => ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))))), rewrite((rel_str(A) => ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))) <=> ((~rel_str(A)) | ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))), ((rel_str(A) => ![B: $i] : ((full_subrelstr(B, A) & 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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)))))))) <=> ((~rel_str(A)) | ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(90,plain,
% 0.12/0.38 (![A: $i] : (rel_str(A) => ![B: $i] : ((full_subrelstr(B, A) & 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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F)))))))) <=> ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[89])).
% 0.12/0.38 tff(91,axiom,(![A: $i] : (rel_str(A) => ![B: $i] : ((full_subrelstr(B, A) & 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(A, C, D)) & in(E, the_carrier(B))) & in(F, the_carrier(B))) => related(B, E, F))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t61_yellow_0')).
% 0.12/0.39 tff(92,plain,
% 0.12/0.39 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[91, 90])).
% 0.12/0.39 tff(93,plain,
% 0.12/0.39 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[92, 88])).
% 0.12/0.39 tff(94,plain,(
% 0.12/0.39 ![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~(full_subrelstr(B, A) & 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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))),
% 0.12/0.39 inference(skolemize,[status(sab)],[93])).
% 0.12/0.39 tff(95,plain,
% 0.12/0.39 (![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[94, 87])).
% 0.12/0.39 tff(96,plain,
% 0.12/0.39 (![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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))) | (~full_subrelstr(B, A))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[95, 85])).
% 0.12/0.39 tff(97,plain,
% 0.12/0.39 (![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[96, 80])).
% 0.12/0.39 tff(98,plain,
% 0.12/0.39 (((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))) | ((~rel_str(B!15)) | ![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D))))))) <=> ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))) | (~rel_str(B!15)) | ![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(99,plain,
% 0.12/0.39 (((~rel_str(B!15)) | ![B: $i] : ((~subrelstr(B, B!15)) | (~full_subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(B!15, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))))))) <=> ((~rel_str(B!15)) | ![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(100,plain,
% 0.12/0.39 (((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))) | ((~rel_str(B!15)) | ![B: $i] : ((~subrelstr(B, B!15)) | (~full_subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(B!15, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))) <=> ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))) | ((~rel_str(B!15)) | ![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))))),
% 0.12/0.39 inference(monotonicity,[status(thm)],[99])).
% 0.12/0.39 tff(101,plain,
% 0.12/0.39 (((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))) | ((~rel_str(B!15)) | ![B: $i] : ((~subrelstr(B, B!15)) | (~full_subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(B!15, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))) <=> ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))) | (~rel_str(B!15)) | ![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D))))))),
% 0.12/0.39 inference(transitivity,[status(thm)],[100, 98])).
% 0.12/0.39 tff(102,plain,
% 0.12/0.39 ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))) | ((~rel_str(B!15)) | ![B: $i] : ((~subrelstr(B, B!15)) | (~full_subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~related(B!15, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(103,plain,
% 0.12/0.39 ((~![A: $i] : ((~rel_str(A)) | ![B: $i] : ((~subrelstr(B, A)) | (~full_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(B, C, D) | (~related(A, C, D)) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B)))))))) | (~rel_str(B!15)) | ![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[102, 101])).
% 0.12/0.39 tff(104,plain,
% 0.12/0.39 ((~rel_str(B!15)) | ![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[103, 97])).
% 0.12/0.39 tff(105,plain,
% 0.12/0.39 (![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[104, 78])).
% 0.12/0.39 tff(106,plain,
% 0.12/0.39 (((~![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))) | ((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16))))))) <=> ((~![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))) | (~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(107,plain,
% 0.12/0.39 (((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D))))) <=> ((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(108,plain,
% 0.12/0.39 (((~![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))) | ((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))) <=> ((~![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))) | ((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))))),
% 0.12/0.39 inference(monotonicity,[status(thm)],[107])).
% 0.12/0.39 tff(109,plain,
% 0.12/0.39 (((~![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))) | ((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))) <=> ((~![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))) | (~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16))))))),
% 0.12/0.39 inference(transitivity,[status(thm)],[108, 106])).
% 0.12/0.39 tff(110,plain,
% 0.12/0.39 ((~![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))) | ((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(111,plain,
% 0.12/0.39 ((~![B: $i] : ((~full_subrelstr(B, B!15)) | (~subrelstr(B, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(C, the_carrier(B))) | (~element(D, the_carrier(B))) | related(B, C, D) | (~in(C, the_carrier(B))) | (~in(D, the_carrier(B))) | (~element(D, the_carrier(B!15))) | (~related(B!15, C, D)))))) | (~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[110, 109])).
% 0.12/0.39 tff(112,plain,
% 0.12/0.39 ((~full_subrelstr(C!16, B!15)) | (~subrelstr(C!16, B!15)) | ![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[111, 105])).
% 0.12/0.39 tff(113,plain,
% 0.12/0.39 (![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[112, 57, 55])).
% 0.12/0.39 tff(114,plain,
% 0.12/0.39 (element(D!17, the_carrier(B!15))),
% 0.12/0.39 inference(and_elim,[status(thm)],[18])).
% 0.12/0.39 tff(115,plain,
% 0.12/0.39 (((~![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))) | ((~element(D!17, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16)))))) <=> ((~![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))) | (~element(D!17, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16)))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(116,plain,
% 0.12/0.39 (((~element(D!17, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, D!17, D)) | (~element(D!17, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, D!17, D) | (~in(D!17, the_carrier(C!16))) | (~in(D, the_carrier(C!16))))) <=> ((~element(D!17, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16)))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(117,plain,
% 0.12/0.39 (((~![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))) | ((~element(D!17, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, D!17, D)) | (~element(D!17, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, D!17, D) | (~in(D!17, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))) <=> ((~![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))) | ((~element(D!17, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))))),
% 0.12/0.39 inference(monotonicity,[status(thm)],[116])).
% 0.12/0.39 tff(118,plain,
% 0.12/0.39 (((~![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))) | ((~element(D!17, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, D!17, D)) | (~element(D!17, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, D!17, D) | (~in(D!17, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))) <=> ((~![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))) | (~element(D!17, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16)))))),
% 0.12/0.39 inference(transitivity,[status(thm)],[117, 115])).
% 0.12/0.39 tff(119,plain,
% 0.12/0.39 ((~![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))) | ((~element(D!17, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, D!17, D)) | (~element(D!17, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, D!17, D) | (~in(D!17, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(120,plain,
% 0.12/0.39 ((~![C: $i] : ((~element(C, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~related(B!15, C, D)) | (~element(C, the_carrier(C!16))) | (~element(D, the_carrier(C!16))) | related(C!16, C, D) | (~in(C, the_carrier(C!16))) | (~in(D, the_carrier(C!16)))))) | (~element(D!17, the_carrier(B!15))) | ![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[119, 118])).
% 0.12/0.39 tff(121,plain,
% 0.12/0.39 (![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[120, 114, 113])).
% 0.12/0.39 tff(122,plain,
% 0.12/0.39 (^[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.12/0.39 inference(bind,[status(th)],[])).
% 0.12/0.39 tff(123,plain,
% 0.12/0.39 (![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.12/0.39 inference(quant_intro,[status(thm)],[122])).
% 0.12/0.39 tff(124,plain,
% 0.12/0.39 (^[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.12/0.39 inference(bind,[status(th)],[])).
% 0.12/0.39 tff(125,plain,
% 0.12/0.39 (![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.12/0.39 inference(quant_intro,[status(thm)],[124])).
% 0.12/0.39 tff(126,plain,
% 0.12/0.39 (^[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.12/0.39 inference(bind,[status(th)],[])).
% 0.12/0.39 tff(127,plain,
% 0.12/0.39 (![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.12/0.39 inference(quant_intro,[status(thm)],[126])).
% 0.12/0.39 tff(128,plain,
% 0.12/0.39 (![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.12/0.39 inference(transitivity,[status(thm)],[127, 125])).
% 0.12/0.39 tff(129,plain,
% 0.12/0.39 (^[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.12/0.39 inference(bind,[status(th)],[])).
% 0.12/0.39 tff(130,plain,
% 0.12/0.39 (![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.12/0.39 inference(quant_intro,[status(thm)],[129])).
% 0.12/0.39 tff(131,plain,
% 0.12/0.39 (![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.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(132,plain,
% 0.12/0.39 (^[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.12/0.39 inference(bind,[status(th)],[])).
% 0.12/0.39 tff(133,plain,
% 0.12/0.39 (![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.12/0.39 inference(quant_intro,[status(thm)],[132])).
% 0.12/0.39 tff(134,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.12/0.39 tff(135,plain,
% 0.12/0.39 (![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[134, 133])).
% 0.12/0.39 tff(136,plain,
% 0.12/0.39 (![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[135, 131])).
% 0.12/0.39 tff(137,plain,(
% 0.12/0.39 ![A: $i, B: $i] : ((~(one_sorted_str(A) & net_str(B, A))) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.12/0.39 inference(skolemize,[status(sab)],[136])).
% 0.12/0.39 tff(138,plain,
% 0.12/0.39 (![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[137, 130])).
% 0.12/0.39 tff(139,plain,
% 0.12/0.39 (![A: $i, B: $i] : ((~net_str(B, A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)) | (~one_sorted_str(A)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[138, 128])).
% 0.12/0.39 tff(140,plain,
% 0.12/0.39 (![A: $i, B: $i] : ((~net_str(B, A)) | (~one_sorted_str(A)) | ![C: $i] : ((~subnetstr(C, A, B)) | net_str(C, A)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[139, 123])).
% 0.12/0.39 tff(141,plain,
% 0.12/0.39 (((~![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!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14)) | (~net_str(B!15, A!14)))) <=> ((~![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!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14)) | (~net_str(B!15, A!14)))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(142,plain,
% 0.12/0.39 (((~net_str(B!15, A!14)) | (~one_sorted_str(A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14))) <=> ((~one_sorted_str(A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14)) | (~net_str(B!15, A!14)))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(143,plain,
% 0.12/0.39 (((~![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!15, A!14)) | (~one_sorted_str(A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14)))) <=> ((~![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!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14)) | (~net_str(B!15, A!14))))),
% 0.12/0.39 inference(monotonicity,[status(thm)],[142])).
% 0.12/0.39 tff(144,plain,
% 0.12/0.39 (((~![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!15, A!14)) | (~one_sorted_str(A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14)))) <=> ((~![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!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14)) | (~net_str(B!15, A!14)))),
% 0.12/0.39 inference(transitivity,[status(thm)],[143, 141])).
% 0.12/0.39 tff(145,plain,
% 0.12/0.39 ((~![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!15, A!14)) | (~one_sorted_str(A!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14)))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(146,plain,
% 0.12/0.39 ((~![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!14)) | ![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14)) | (~net_str(B!15, A!14))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[145, 144])).
% 0.12/0.39 tff(147,plain,
% 0.12/0.39 (![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[146, 140, 19, 40])).
% 0.12/0.39 tff(148,plain,
% 0.12/0.39 (((~![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14))) | ((~subnetstr(C!16, A!14, B!15)) | net_str(C!16, A!14))) <=> ((~![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14))) | (~subnetstr(C!16, A!14, B!15)) | net_str(C!16, A!14))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(149,plain,
% 0.12/0.39 ((~![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14))) | ((~subnetstr(C!16, A!14, B!15)) | net_str(C!16, A!14))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(150,plain,
% 0.12/0.39 ((~![C: $i] : ((~subnetstr(C, A!14, B!15)) | net_str(C, A!14))) | (~subnetstr(C!16, A!14, B!15)) | net_str(C!16, A!14)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[149, 148])).
% 0.12/0.39 tff(151,plain,
% 0.12/0.39 (net_str(C!16, A!14)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[150, 45, 147])).
% 0.12/0.40 tff(152,plain,
% 0.12/0.40 (((~![B: $i] : (rel_str(B) | (~net_str(B, A!14)))) | (rel_str(C!16) | (~net_str(C!16, A!14)))) <=> ((~![B: $i] : (rel_str(B) | (~net_str(B, A!14)))) | rel_str(C!16) | (~net_str(C!16, A!14)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(153,plain,
% 0.12/0.40 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!14)))) | (rel_str(C!16) | (~net_str(C!16, A!14)))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(154,plain,
% 0.12/0.40 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!14)))) | rel_str(C!16) | (~net_str(C!16, A!14))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[153, 152])).
% 0.12/0.40 tff(155,plain,
% 0.12/0.40 (rel_str(C!16)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[154, 74, 151])).
% 0.12/0.40 tff(156,plain,
% 0.12/0.40 (^[A: $i] : refl((one_sorted_str(A) | (~rel_str(A))) <=> (one_sorted_str(A) | (~rel_str(A))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(157,plain,
% 0.12/0.40 (![A: $i] : (one_sorted_str(A) | (~rel_str(A))) <=> ![A: $i] : (one_sorted_str(A) | (~rel_str(A)))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[156])).
% 0.12/0.40 tff(158,plain,
% 0.12/0.40 (![A: $i] : (one_sorted_str(A) | (~rel_str(A))) <=> ![A: $i] : (one_sorted_str(A) | (~rel_str(A)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(159,plain,
% 0.12/0.40 (^[A: $i] : rewrite((rel_str(A) => one_sorted_str(A)) <=> (one_sorted_str(A) | (~rel_str(A))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(160,plain,
% 0.12/0.40 (![A: $i] : (rel_str(A) => one_sorted_str(A)) <=> ![A: $i] : (one_sorted_str(A) | (~rel_str(A)))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[159])).
% 0.12/0.40 tff(161,axiom,(![A: $i] : (rel_str(A) => one_sorted_str(A))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dt_l1_orders_2')).
% 0.12/0.40 tff(162,plain,
% 0.12/0.40 (![A: $i] : (one_sorted_str(A) | (~rel_str(A)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[161, 160])).
% 0.12/0.40 tff(163,plain,
% 0.12/0.40 (![A: $i] : (one_sorted_str(A) | (~rel_str(A)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[162, 158])).
% 0.12/0.40 tff(164,plain,(
% 0.12/0.40 ![A: $i] : (one_sorted_str(A) | (~rel_str(A)))),
% 0.12/0.40 inference(skolemize,[status(sab)],[163])).
% 0.12/0.40 tff(165,plain,
% 0.12/0.40 (![A: $i] : (one_sorted_str(A) | (~rel_str(A)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[164, 157])).
% 0.12/0.40 tff(166,plain,
% 0.12/0.40 (((~![A: $i] : (one_sorted_str(A) | (~rel_str(A)))) | (one_sorted_str(C!16) | (~rel_str(C!16)))) <=> ((~![A: $i] : (one_sorted_str(A) | (~rel_str(A)))) | one_sorted_str(C!16) | (~rel_str(C!16)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(167,plain,
% 0.12/0.40 ((~![A: $i] : (one_sorted_str(A) | (~rel_str(A)))) | (one_sorted_str(C!16) | (~rel_str(C!16)))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(168,plain,
% 0.12/0.40 ((~![A: $i] : (one_sorted_str(A) | (~rel_str(A)))) | one_sorted_str(C!16) | (~rel_str(C!16))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[167, 166])).
% 0.12/0.40 tff(169,plain,
% 0.12/0.40 (one_sorted_str(C!16)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[168, 165, 155])).
% 0.12/0.40 tff(170,plain,
% 0.12/0.40 (~empty_carrier(C!16)),
% 0.12/0.40 inference(and_elim,[status(thm)],[18])).
% 0.12/0.40 tff(171,plain,
% 0.12/0.40 (^[A: $i] : refl((empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A))) <=> (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(172,plain,
% 0.12/0.40 (![A: $i] : (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A))) <=> ![A: $i] : (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A)))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[171])).
% 0.12/0.40 tff(173,plain,
% 0.12/0.40 (^[A: $i] : trans(monotonicity(trans(monotonicity(rewrite(((~empty_carrier(A)) & one_sorted_str(A)) <=> (~(empty_carrier(A) | (~one_sorted_str(A))))), ((~((~empty_carrier(A)) & one_sorted_str(A))) <=> (~(~(empty_carrier(A) | (~one_sorted_str(A))))))), rewrite((~(~(empty_carrier(A) | (~one_sorted_str(A))))) <=> (empty_carrier(A) | (~one_sorted_str(A)))), ((~((~empty_carrier(A)) & one_sorted_str(A))) <=> (empty_carrier(A) | (~one_sorted_str(A))))), (((~empty(the_carrier(A))) | (~((~empty_carrier(A)) & one_sorted_str(A)))) <=> ((~empty(the_carrier(A))) | (empty_carrier(A) | (~one_sorted_str(A)))))), rewrite(((~empty(the_carrier(A))) | (empty_carrier(A) | (~one_sorted_str(A)))) <=> (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A)))), (((~empty(the_carrier(A))) | (~((~empty_carrier(A)) & one_sorted_str(A)))) <=> (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A)))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(174,plain,
% 0.12/0.40 (![A: $i] : ((~empty(the_carrier(A))) | (~((~empty_carrier(A)) & one_sorted_str(A)))) <=> ![A: $i] : (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A)))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[173])).
% 0.12/0.40 tff(175,plain,
% 0.12/0.40 (![A: $i] : ((~empty(the_carrier(A))) | (~((~empty_carrier(A)) & one_sorted_str(A)))) <=> ![A: $i] : ((~empty(the_carrier(A))) | (~((~empty_carrier(A)) & one_sorted_str(A))))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(176,plain,
% 0.12/0.40 (^[A: $i] : rewrite((((~empty_carrier(A)) & one_sorted_str(A)) => (~empty(the_carrier(A)))) <=> ((~empty(the_carrier(A))) | (~((~empty_carrier(A)) & one_sorted_str(A)))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(177,plain,
% 0.12/0.40 (![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => (~empty(the_carrier(A)))) <=> ![A: $i] : ((~empty(the_carrier(A))) | (~((~empty_carrier(A)) & one_sorted_str(A))))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[176])).
% 0.12/0.40 tff(178,axiom,(![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => (~empty(the_carrier(A))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fc1_struct_0')).
% 0.12/0.40 tff(179,plain,
% 0.12/0.40 (![A: $i] : ((~empty(the_carrier(A))) | (~((~empty_carrier(A)) & one_sorted_str(A))))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[178, 177])).
% 0.12/0.40 tff(180,plain,
% 0.12/0.40 (![A: $i] : ((~empty(the_carrier(A))) | (~((~empty_carrier(A)) & one_sorted_str(A))))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[179, 175])).
% 0.12/0.40 tff(181,plain,(
% 0.12/0.40 ![A: $i] : ((~empty(the_carrier(A))) | (~((~empty_carrier(A)) & one_sorted_str(A))))),
% 0.12/0.40 inference(skolemize,[status(sab)],[180])).
% 0.12/0.40 tff(182,plain,
% 0.12/0.40 (![A: $i] : (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[181, 174])).
% 0.12/0.40 tff(183,plain,
% 0.12/0.40 (![A: $i] : (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[182, 172])).
% 0.12/0.40 tff(184,plain,
% 0.12/0.40 (((~![A: $i] : (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A)))) | (empty_carrier(C!16) | (~empty(the_carrier(C!16))) | (~one_sorted_str(C!16)))) <=> ((~![A: $i] : (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A)))) | empty_carrier(C!16) | (~empty(the_carrier(C!16))) | (~one_sorted_str(C!16)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(185,plain,
% 0.12/0.40 ((~![A: $i] : (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A)))) | (empty_carrier(C!16) | (~empty(the_carrier(C!16))) | (~one_sorted_str(C!16)))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(186,plain,
% 0.12/0.40 ((~![A: $i] : (empty_carrier(A) | (~empty(the_carrier(A))) | (~one_sorted_str(A)))) | empty_carrier(C!16) | (~empty(the_carrier(C!16))) | (~one_sorted_str(C!16))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[185, 184])).
% 0.12/0.40 tff(187,plain,
% 0.12/0.40 ((~empty(the_carrier(C!16))) | (~one_sorted_str(C!16))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[186, 183, 170])).
% 0.12/0.40 tff(188,plain,
% 0.12/0.40 (~empty(the_carrier(C!16))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[187, 169])).
% 0.12/0.40 tff(189,plain,
% 0.12/0.40 (^[A: $i, B: $i] : refl((empty(B) | in(A, B) | (~element(A, B))) <=> (empty(B) | in(A, B) | (~element(A, B))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(190,plain,
% 0.12/0.40 (![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B))) <=> ![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[189])).
% 0.12/0.40 tff(191,plain,
% 0.12/0.40 (![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B))) <=> ![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(192,plain,
% 0.12/0.40 (^[A: $i, B: $i] : rewrite((element(A, B) => (empty(B) | in(A, B))) <=> (empty(B) | in(A, B) | (~element(A, B))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(193,plain,
% 0.12/0.40 (![A: $i, B: $i] : (element(A, B) => (empty(B) | in(A, B))) <=> ![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[192])).
% 0.12/0.40 tff(194,axiom,(![A: $i, B: $i] : (element(A, B) => (empty(B) | in(A, B)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t2_subset')).
% 0.12/0.40 tff(195,plain,
% 0.12/0.40 (![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[194, 193])).
% 0.12/0.40 tff(196,plain,
% 0.12/0.40 (![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[195, 191])).
% 0.12/0.40 tff(197,plain,(
% 0.12/0.40 ![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))),
% 0.12/0.40 inference(skolemize,[status(sab)],[196])).
% 0.12/0.40 tff(198,plain,
% 0.12/0.40 (![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[197, 190])).
% 0.12/0.40 tff(199,plain,
% 0.12/0.40 (~((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)))),
% 0.12/0.40 inference(and_elim,[status(thm)],[18])).
% 0.12/0.40 tff(200,plain,
% 0.12/0.40 (element(E!18, the_carrier(C!16))),
% 0.12/0.40 inference(or_elim,[status(thm)],[199])).
% 0.12/0.40 tff(201,plain,
% 0.12/0.40 (((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | ((~element(E!18, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16)))) <=> ((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (~element(E!18, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(202,plain,
% 0.12/0.40 ((empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16)) | (~element(E!18, the_carrier(C!16)))) <=> ((~element(E!18, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(203,plain,
% 0.12/0.40 (((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16)) | (~element(E!18, the_carrier(C!16))))) <=> ((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | ((~element(E!18, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16))))),
% 0.12/0.40 inference(monotonicity,[status(thm)],[202])).
% 0.12/0.40 tff(204,plain,
% 0.12/0.40 (((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16)) | (~element(E!18, the_carrier(C!16))))) <=> ((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (~element(E!18, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16)))),
% 0.12/0.40 inference(transitivity,[status(thm)],[203, 201])).
% 0.12/0.40 tff(205,plain,
% 0.12/0.40 ((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16)) | (~element(E!18, the_carrier(C!16))))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(206,plain,
% 0.12/0.40 ((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (~element(E!18, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[205, 204])).
% 0.12/0.40 tff(207,plain,
% 0.12/0.40 (empty(the_carrier(C!16)) | in(E!18, the_carrier(C!16))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[206, 200, 198])).
% 0.12/0.40 tff(208,plain,
% 0.12/0.40 (in(E!18, the_carrier(C!16))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[207, 188])).
% 0.12/0.40 tff(209,plain,
% 0.12/0.40 (element(D!17, the_carrier(C!16))),
% 0.12/0.40 inference(or_elim,[status(thm)],[199])).
% 0.12/0.40 tff(210,plain,
% 0.12/0.40 (((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | ((~element(D!17, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16)))) <=> ((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (~element(D!17, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(211,plain,
% 0.12/0.40 ((empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16)) | (~element(D!17, the_carrier(C!16)))) <=> ((~element(D!17, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(212,plain,
% 0.12/0.40 (((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16)) | (~element(D!17, the_carrier(C!16))))) <=> ((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | ((~element(D!17, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16))))),
% 0.12/0.40 inference(monotonicity,[status(thm)],[211])).
% 0.12/0.40 tff(213,plain,
% 0.12/0.40 (((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16)) | (~element(D!17, the_carrier(C!16))))) <=> ((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (~element(D!17, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16)))),
% 0.12/0.40 inference(transitivity,[status(thm)],[212, 210])).
% 0.12/0.40 tff(214,plain,
% 0.12/0.40 ((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16)) | (~element(D!17, the_carrier(C!16))))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(215,plain,
% 0.12/0.40 ((~![A: $i, B: $i] : (empty(B) | in(A, B) | (~element(A, B)))) | (~element(D!17, the_carrier(C!16))) | empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[214, 213])).
% 0.12/0.40 tff(216,plain,
% 0.12/0.40 (empty(the_carrier(C!16)) | in(D!17, the_carrier(C!16))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[215, 209, 198])).
% 0.12/0.40 tff(217,plain,
% 0.12/0.40 (in(D!17, the_carrier(C!16))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[216, 188])).
% 0.12/0.40 tff(218,plain,
% 0.12/0.40 (related(B!15, D!17, E!18)),
% 0.12/0.40 inference(or_elim,[status(thm)],[199])).
% 0.12/0.40 tff(219,plain,
% 0.12/0.40 (~related(C!16, D!17, E!18)),
% 0.12/0.40 inference(or_elim,[status(thm)],[199])).
% 0.12/0.40 tff(220,plain,
% 0.12/0.40 (element(E!18, the_carrier(B!15))),
% 0.12/0.40 inference(or_elim,[status(thm)],[199])).
% 0.12/0.40 tff(221,plain,
% 0.12/0.40 (((~![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))) | ((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)) | (~in(D!17, the_carrier(C!16))) | (~in(E!18, the_carrier(C!16))))) <=> ((~![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))) | (~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)) | (~in(D!17, the_carrier(C!16))) | (~in(E!18, the_carrier(C!16))))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(222,plain,
% 0.12/0.40 (((~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)) | (~in(E!18, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16)))) <=> ((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)) | (~in(D!17, the_carrier(C!16))) | (~in(E!18, the_carrier(C!16))))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(223,plain,
% 0.12/0.40 (((~![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))) | ((~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)) | (~in(E!18, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))) <=> ((~![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))) | ((~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)) | (~in(D!17, the_carrier(C!16))) | (~in(E!18, the_carrier(C!16)))))),
% 0.12/0.40 inference(monotonicity,[status(thm)],[222])).
% 0.12/0.40 tff(224,plain,
% 0.12/0.40 (((~![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))) | ((~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)) | (~in(E!18, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))) <=> ((~![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))) | (~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)) | (~in(D!17, the_carrier(C!16))) | (~in(E!18, the_carrier(C!16))))),
% 0.12/0.40 inference(transitivity,[status(thm)],[223, 221])).
% 0.12/0.40 tff(225,plain,
% 0.12/0.40 ((~![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))) | ((~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)) | (~in(E!18, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(226,plain,
% 0.12/0.40 ((~![D: $i] : ((~element(D, the_carrier(B!15))) | (~element(D, the_carrier(C!16))) | (~element(D!17, the_carrier(C!16))) | related(C!16, D!17, D) | (~related(B!15, D!17, D)) | (~in(D, the_carrier(C!16))) | (~in(D!17, the_carrier(C!16))))) | (~element(D!17, the_carrier(C!16))) | (~element(E!18, the_carrier(B!15))) | (~element(E!18, the_carrier(C!16))) | related(C!16, D!17, E!18) | (~related(B!15, D!17, E!18)) | (~in(D!17, the_carrier(C!16))) | (~in(E!18, the_carrier(C!16)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[225, 224])).
% 0.12/0.40 tff(227,plain,
% 0.12/0.40 ($false),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[226, 209, 220, 200, 219, 218, 217, 208, 121])).
% 0.12/0.40 % SZS output end Proof
% 0.12/0.40 % E exiting
%------------------------------------------------------------------------------