%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU376+1 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n014.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.19s 0.48s
% Output : Proof 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SEU376+1 : TPTP v9.0.0. Released v3.3.0.
% 0.04/0.12 % Command : run_E %s %d THM
% 0.11/0.33 % Computer : n014.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri Jun 20 06:56:54 EDT 2025
% 0.11/0.33 % CPUTime :
% 0.19/0.48 % SZS status Theorem
% 0.19/0.48 % SZS output start Proof
% 0.19/0.48 tff(in_type, type, (
% 0.19/0.48 in: ( $i * $i ) > $o)).
% 0.19/0.48 tff(tptp_fun_C_26_type, type, (
% 0.19/0.48 tptp_fun_C_26: $i)).
% 0.19/0.48 tff(apply_netmap_type, type, (
% 0.19/0.48 apply_netmap: ( $i * $i * $i ) > $i)).
% 0.19/0.48 tff(tptp_fun_D_4_type, type, (
% 0.19/0.48 tptp_fun_D_4: ( $i * $i * $i ) > $i)).
% 0.19/0.48 tff(tptp_fun_B_25_type, type, (
% 0.19/0.48 tptp_fun_B_25: $i)).
% 0.19/0.48 tff(tptp_fun_D_3_type, type, (
% 0.19/0.48 tptp_fun_D_3: ( $i * $i * $i ) > $i)).
% 0.19/0.48 tff(tptp_fun_A_24_type, type, (
% 0.19/0.48 tptp_fun_A_24: $i)).
% 0.19/0.48 tff(tptp_fun_D_0_type, type, (
% 0.19/0.48 tptp_fun_D_0: ( $i * $i * $i ) > $i)).
% 0.19/0.48 tff(related_type, type, (
% 0.19/0.48 related: ( $i * $i * $i ) > $o)).
% 0.19/0.48 tff(element_type, type, (
% 0.19/0.48 element: ( $i * $i ) > $o)).
% 0.19/0.48 tff(the_carrier_type, type, (
% 0.19/0.48 the_carrier: $i > $i)).
% 0.19/0.48 tff(is_often_in_type, type, (
% 0.19/0.48 is_often_in: ( $i * $i * $i ) > $o)).
% 0.19/0.48 tff(tptp_fun_E_2_type, type, (
% 0.19/0.48 tptp_fun_E_2: ( $i * $i * $i * $i ) > $i)).
% 0.19/0.48 tff(net_str_type, type, (
% 0.19/0.48 net_str: ( $i * $i ) > $o)).
% 0.19/0.48 tff(empty_carrier_type, type, (
% 0.19/0.48 empty_carrier: $i > $o)).
% 0.19/0.48 tff(one_sorted_str_type, type, (
% 0.19/0.48 one_sorted_str: $i > $o)).
% 0.19/0.48 tff(is_eventually_in_type, type, (
% 0.19/0.48 is_eventually_in: ( $i * $i * $i ) > $o)).
% 0.19/0.48 tff(directed_relstr_type, type, (
% 0.19/0.48 directed_relstr: $i > $o)).
% 0.19/0.48 tff(transitive_relstr_type, type, (
% 0.19/0.48 transitive_relstr: $i > $o)).
% 0.19/0.48 tff(tptp_fun_C_6_type, type, (
% 0.19/0.48 tptp_fun_C_6: $i > $i)).
% 0.19/0.48 tff(tptp_fun_B_5_type, type, (
% 0.19/0.48 tptp_fun_B_5: $i > $i)).
% 0.19/0.48 tff(rel_str_type, type, (
% 0.19/0.48 rel_str: $i > $o)).
% 0.19/0.48 tff(tptp_fun_E_1_type, type, (
% 0.19/0.48 tptp_fun_E_1: ( $i * $i * $i * $i ) > $i)).
% 0.19/0.48 tff(1,plain,
% 0.19/0.48 ((((~empty_carrier(A!24)) & one_sorted_str(A!24)) & ((~empty_carrier(B!25)) & transitive_relstr(B!25) & directed_relstr(B!25) & net_str(B!25, A!24) & (~((~is_eventually_in(A!24, B!25, C!26)) | is_often_in(A!24, B!25, C!26))))) <=> ((~empty_carrier(A!24)) & one_sorted_str(A!24) & (~empty_carrier(B!25)) & transitive_relstr(B!25) & directed_relstr(B!25) & net_str(B!25, A!24) & (~((~is_eventually_in(A!24, B!25, C!26)) | is_often_in(A!24, B!25, C!26))))),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(2,plain,
% 0.19/0.48 ((((~empty_carrier(B!25)) & transitive_relstr(B!25) & directed_relstr(B!25) & net_str(B!25, A!24)) & (~((~is_eventually_in(A!24, B!25, C!26)) | is_often_in(A!24, B!25, C!26)))) <=> ((~empty_carrier(B!25)) & transitive_relstr(B!25) & directed_relstr(B!25) & net_str(B!25, A!24) & (~((~is_eventually_in(A!24, B!25, C!26)) | is_often_in(A!24, B!25, C!26))))),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(3,plain,
% 0.19/0.48 ((((~empty_carrier(A!24)) & one_sorted_str(A!24)) & (((~empty_carrier(B!25)) & transitive_relstr(B!25) & directed_relstr(B!25) & net_str(B!25, A!24)) & (~((~is_eventually_in(A!24, B!25, C!26)) | is_often_in(A!24, B!25, C!26))))) <=> (((~empty_carrier(A!24)) & one_sorted_str(A!24)) & ((~empty_carrier(B!25)) & transitive_relstr(B!25) & directed_relstr(B!25) & net_str(B!25, A!24) & (~((~is_eventually_in(A!24, B!25, C!26)) | is_often_in(A!24, B!25, C!26)))))),
% 0.19/0.48 inference(monotonicity,[status(thm)],[2])).
% 0.19/0.48 tff(4,plain,
% 0.19/0.48 ((((~empty_carrier(A!24)) & one_sorted_str(A!24)) & (((~empty_carrier(B!25)) & transitive_relstr(B!25) & directed_relstr(B!25) & net_str(B!25, A!24)) & (~((~is_eventually_in(A!24, B!25, C!26)) | is_often_in(A!24, B!25, C!26))))) <=> ((~empty_carrier(A!24)) & one_sorted_str(A!24) & (~empty_carrier(B!25)) & transitive_relstr(B!25) & directed_relstr(B!25) & net_str(B!25, A!24) & (~((~is_eventually_in(A!24, B!25, C!26)) | is_often_in(A!24, B!25, C!26))))),
% 0.19/0.48 inference(transitivity,[status(thm)],[3, 1])).
% 0.19/0.48 tff(5,plain,
% 0.19/0.48 ((~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & transitive_relstr(B) & directed_relstr(B) & net_str(B, A))) | ![C: $i] : ((~is_eventually_in(A, B, C)) | is_often_in(A, B, C))))) <=> (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & transitive_relstr(B) & directed_relstr(B) & net_str(B, A))) | ![C: $i] : ((~is_eventually_in(A, B, C)) | is_often_in(A, B, C)))))),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(6,plain,
% 0.19/0.48 ((~![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((((~empty_carrier(B)) & transitive_relstr(B)) & directed_relstr(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) => is_often_in(A, B, C))))) <=> (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & transitive_relstr(B) & directed_relstr(B) & net_str(B, A))) | ![C: $i] : ((~is_eventually_in(A, B, C)) | is_often_in(A, B, C)))))),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(7,axiom,(~![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((((~empty_carrier(B)) & transitive_relstr(B)) & directed_relstr(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) => is_often_in(A, B, C))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t28_yellow_6')).
% 0.19/0.48 tff(8,plain,
% 0.19/0.48 (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & transitive_relstr(B) & directed_relstr(B) & net_str(B, A))) | ![C: $i] : ((~is_eventually_in(A, B, C)) | is_often_in(A, B, C))))),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[7, 6])).
% 0.19/0.48 tff(9,plain,
% 0.19/0.48 (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & transitive_relstr(B) & directed_relstr(B) & net_str(B, A))) | ![C: $i] : ((~is_eventually_in(A, B, C)) | is_often_in(A, B, C))))),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[8, 5])).
% 0.19/0.48 tff(10,plain,
% 0.19/0.48 (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & transitive_relstr(B) & directed_relstr(B) & net_str(B, A))) | ![C: $i] : ((~is_eventually_in(A, B, C)) | is_often_in(A, B, C))))),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.19/0.48 tff(11,plain,
% 0.19/0.48 (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & transitive_relstr(B) & directed_relstr(B) & net_str(B, A))) | ![C: $i] : ((~is_eventually_in(A, B, C)) | is_often_in(A, B, C))))),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[10, 5])).
% 0.19/0.48 tff(12,plain,
% 0.19/0.48 ((~empty_carrier(A!24)) & one_sorted_str(A!24) & (~empty_carrier(B!25)) & transitive_relstr(B!25) & directed_relstr(B!25) & net_str(B!25, A!24) & (~((~is_eventually_in(A!24, B!25, C!26)) | is_often_in(A!24, B!25, C!26)))),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[11, 4])).
% 0.19/0.48 tff(13,plain,
% 0.19/0.48 (one_sorted_str(A!24)),
% 0.19/0.48 inference(and_elim,[status(thm)],[12])).
% 0.19/0.48 tff(14,plain,
% 0.19/0.48 (~empty_carrier(A!24)),
% 0.19/0.48 inference(and_elim,[status(thm)],[12])).
% 0.19/0.48 tff(15,plain,
% 0.19/0.48 (^[A: $i] : refl((empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))))),
% 0.19/0.48 inference(bind,[status(th)],[])).
% 0.19/0.48 tff(16,plain,
% 0.19/0.48 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))),
% 0.19/0.48 inference(quant_intro,[status(thm)],[15])).
% 0.19/0.48 tff(17,plain,
% 0.19/0.48 (^[A: $i] : rewrite((empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))))),
% 0.19/0.48 inference(bind,[status(th)],[])).
% 0.19/0.48 tff(18,plain,
% 0.19/0.48 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))),
% 0.19/0.48 inference(quant_intro,[status(thm)],[17])).
% 0.19/0.48 tff(19,plain,
% 0.19/0.48 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))),
% 0.19/0.48 inference(transitivity,[status(thm)],[18, 16])).
% 0.19/0.48 tff(20,plain,
% 0.19/0.48 (^[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))))), quant_intro(proof_bind(^[B: $i] : trans(monotonicity(trans(monotonicity(rewrite(((~empty_carrier(B)) & net_str(B, A)) <=> (~(empty_carrier(B) | (~net_str(B, A))))), ((~((~empty_carrier(B)) & net_str(B, A))) <=> (~(~(empty_carrier(B) | (~net_str(B, A))))))), rewrite((~(~(empty_carrier(B) | (~net_str(B, A))))) <=> (empty_carrier(B) | (~net_str(B, A)))), ((~((~empty_carrier(B)) & net_str(B, A))) <=> (empty_carrier(B) | (~net_str(B, A))))), quant_intro(proof_bind(^[C: $i] : trans(monotonicity(rewrite(((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) <=> ((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))), trans(monotonicity(trans(monotonicity(quant_intro(proof_bind(^[E: $i] : trans(monotonicity(rewrite((element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C)) <=> (~((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))), ((~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C))) <=> (~(~((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))), rewrite((~(~((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))) <=> ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))), ((~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C))) <=> ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))), (![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C))) <=> ![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))), ((element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C)))) <=> (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))), rewrite((element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))) <=> (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))), ((element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C)))) <=> (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))), ((is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C))))) <=> (is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))), rewrite((is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))) <=> (is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))), ((is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C))))) <=> (is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))), ((((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) & (is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C)))))) <=> (((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))))) & (is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))), rewrite((((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))))) & (is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))) <=> (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))), ((((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) & (is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C)))))) <=> (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))), (![C: $i] : (((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) & (is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C)))))) <=> ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))), (((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) & (is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C))))))) <=> ((empty_carrier(B) | (~net_str(B, A))) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))), rewrite(((empty_carrier(B) | (~net_str(B, A))) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))) <=> (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))), (((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) & (is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C))))))) <=> (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))))), (![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) & (is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C))))))) <=> ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))), (((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) & (is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C)))))))) <=> ((empty_carrier(A) | (~one_sorted_str(A))) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))))), rewrite(((empty_carrier(A) | (~one_sorted_str(A))) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C)))))))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))), (((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) & (is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C)))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))))),
% 0.19/0.48 inference(bind,[status(th)],[])).
% 0.19/0.48 tff(21,plain,
% 0.19/0.48 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) & (is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C)))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))),
% 0.19/0.48 inference(quant_intro,[status(thm)],[20])).
% 0.19/0.48 tff(22,plain,
% 0.19/0.48 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C)))))) <=> ![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C))))))),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(23,plain,
% 0.19/0.48 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : rewrite((is_often_in(A, B, C) <=> ![D: $i] : (element(D, the_carrier(B)) => ?[E: $i] : ((element(E, the_carrier(B)) & related(B, D, E)) & in(apply_netmap(A, B, E), C)))) <=> (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C)))))), (![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : (element(D, the_carrier(B)) => ?[E: $i] : ((element(E, the_carrier(B)) & related(B, D, E)) & in(apply_netmap(A, B, E), C)))) <=> ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C)))))), ((((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : (element(D, the_carrier(B)) => ?[E: $i] : ((element(E, the_carrier(B)) & related(B, D, E)) & in(apply_netmap(A, B, E), C))))) <=> (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C))))))), rewrite((((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C))))) <=> ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C)))))), ((((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : (element(D, the_carrier(B)) => ?[E: $i] : ((element(E, the_carrier(B)) & related(B, D, E)) & in(apply_netmap(A, B, E), C))))) <=> ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C)))))))), (![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : (element(D, the_carrier(B)) => ?[E: $i] : ((element(E, the_carrier(B)) & related(B, D, E)) & in(apply_netmap(A, B, E), C))))) <=> ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C))))))), ((((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : (element(D, the_carrier(B)) => ?[E: $i] : ((element(E, the_carrier(B)) & related(B, D, E)) & in(apply_netmap(A, B, E), C)))))) <=> (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C)))))))), rewrite((((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C)))))) <=> ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C))))))), ((((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : (element(D, the_carrier(B)) => ?[E: $i] : ((element(E, the_carrier(B)) & related(B, D, E)) & in(apply_netmap(A, B, E), C)))))) <=> ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C))))))))),
% 0.19/0.48 inference(bind,[status(th)],[])).
% 0.19/0.48 tff(24,plain,
% 0.19/0.48 (![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : (element(D, the_carrier(B)) => ?[E: $i] : ((element(E, the_carrier(B)) & related(B, D, E)) & in(apply_netmap(A, B, E), C)))))) <=> ![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C))))))),
% 0.19/0.48 inference(quant_intro,[status(thm)],[23])).
% 0.19/0.48 tff(25,axiom,(![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : (element(D, the_carrier(B)) => ?[E: $i] : ((element(E, the_carrier(B)) & related(B, D, E)) & in(apply_netmap(A, B, E), C))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d12_waybel_0')).
% 0.19/0.48 tff(26,plain,
% 0.19/0.48 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C))))))),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[25, 24])).
% 0.19/0.48 tff(27,plain,
% 0.19/0.48 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_often_in(A, B, C) <=> ![D: $i] : ((~element(D, the_carrier(B))) | ?[E: $i] : (element(E, the_carrier(B)) & related(B, D, E) & in(apply_netmap(A, B, E), C))))))),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[26, 22])).
% 0.19/0.48 tff(28,plain,(
% 0.19/0.48 ![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (element(tptp_fun_E_2(D, C, B, A), the_carrier(B)) & related(B, D, tptp_fun_E_2(D, C, B, A)) & in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C)))) & (is_often_in(A, B, C) | (element(tptp_fun_D_3(C, B, A), the_carrier(B)) & ![E: $i] : (~(element(E, the_carrier(B)) & related(B, tptp_fun_D_3(C, B, A), E) & in(apply_netmap(A, B, E), C))))))))),
% 0.19/0.48 inference(skolemize,[status(sab)],[27])).
% 0.19/0.49 tff(29,plain,
% 0.19/0.49 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[28, 21])).
% 0.19/0.49 tff(30,plain,
% 0.19/0.49 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[29, 19])).
% 0.19/0.49 tff(31,plain,
% 0.19/0.49 (((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))) | (empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A!24), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A!24))) | (~in(apply_netmap(A!24, B, tptp_fun_E_2(D, C, B, A!24)), C))))))) | (~(is_often_in(A!24, B, C) | (~((~element(tptp_fun_D_3(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A!24), E)) | (~in(apply_netmap(A!24, B, E), C))))))))))))) <=> ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))) | empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A!24), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A!24))) | (~in(apply_netmap(A!24, B, tptp_fun_E_2(D, C, B, A!24)), C))))))) | (~(is_often_in(A!24, B, C) | (~((~element(tptp_fun_D_3(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A!24), E)) | (~in(apply_netmap(A!24, B, E), C))))))))))))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(32,plain,
% 0.19/0.49 ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))) | (empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A!24), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A!24))) | (~in(apply_netmap(A!24, B, tptp_fun_E_2(D, C, B, A!24)), C))))))) | (~(is_often_in(A!24, B, C) | (~((~element(tptp_fun_D_3(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A!24), E)) | (~in(apply_netmap(A!24, B, E), C))))))))))))),
% 0.19/0.49 inference(quant_inst,[status(thm)],[])).
% 0.19/0.49 tff(33,plain,
% 0.19/0.49 ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_often_in(A, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A))) | (~in(apply_netmap(A, B, tptp_fun_E_2(D, C, B, A)), C))))))) | (~(is_often_in(A, B, C) | (~((~element(tptp_fun_D_3(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A), E)) | (~in(apply_netmap(A, B, E), C))))))))))))) | empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A!24), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A!24))) | (~in(apply_netmap(A!24, B, tptp_fun_E_2(D, C, B, A!24)), C))))))) | (~(is_often_in(A!24, B, C) | (~((~element(tptp_fun_D_3(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A!24), E)) | (~in(apply_netmap(A!24, B, E), C)))))))))))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[32, 31])).
% 0.19/0.49 tff(34,plain,
% 0.19/0.49 (![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A!24), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A!24))) | (~in(apply_netmap(A!24, B, tptp_fun_E_2(D, C, B, A!24)), C))))))) | (~(is_often_in(A!24, B, C) | (~((~element(tptp_fun_D_3(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A!24), E)) | (~in(apply_netmap(A!24, B, E), C)))))))))))),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[33, 30, 14, 13])).
% 0.19/0.49 tff(35,plain,
% 0.19/0.49 (net_str(B!25, A!24)),
% 0.19/0.49 inference(and_elim,[status(thm)],[12])).
% 0.19/0.49 tff(36,plain,
% 0.19/0.49 (~empty_carrier(B!25)),
% 0.19/0.49 inference(and_elim,[status(thm)],[12])).
% 0.19/0.49 tff(37,plain,
% 0.19/0.49 (((~![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A!24), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A!24))) | (~in(apply_netmap(A!24, B, tptp_fun_E_2(D, C, B, A!24)), C))))))) | (~(is_often_in(A!24, B, C) | (~((~element(tptp_fun_D_3(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A!24), E)) | (~in(apply_netmap(A!24, B, E), C)))))))))))) | (empty_carrier(B!25) | (~net_str(B!25, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B!25, C)) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~((~element(tptp_fun_E_2(D, C, B!25, A!24), the_carrier(B!25))) | (~related(B!25, D, tptp_fun_E_2(D, C, B!25, A!24))) | (~in(apply_netmap(A!24, B!25, tptp_fun_E_2(D, C, B!25, A!24)), C))))))) | (~(is_often_in(A!24, B!25, C) | (~((~element(tptp_fun_D_3(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C)))))))))))) <=> ((~![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A!24), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A!24))) | (~in(apply_netmap(A!24, B, tptp_fun_E_2(D, C, B, A!24)), C))))))) | (~(is_often_in(A!24, B, C) | (~((~element(tptp_fun_D_3(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A!24), E)) | (~in(apply_netmap(A!24, B, E), C)))))))))))) | empty_carrier(B!25) | (~net_str(B!25, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B!25, C)) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~((~element(tptp_fun_E_2(D, C, B!25, A!24), the_carrier(B!25))) | (~related(B!25, D, tptp_fun_E_2(D, C, B!25, A!24))) | (~in(apply_netmap(A!24, B!25, tptp_fun_E_2(D, C, B!25, A!24)), C))))))) | (~(is_often_in(A!24, B!25, C) | (~((~element(tptp_fun_D_3(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C)))))))))))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(38,plain,
% 0.19/0.49 ((~![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A!24), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A!24))) | (~in(apply_netmap(A!24, B, tptp_fun_E_2(D, C, B, A!24)), C))))))) | (~(is_often_in(A!24, B, C) | (~((~element(tptp_fun_D_3(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A!24), E)) | (~in(apply_netmap(A!24, B, E), C)))))))))))) | (empty_carrier(B!25) | (~net_str(B!25, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B!25, C)) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~((~element(tptp_fun_E_2(D, C, B!25, A!24), the_carrier(B!25))) | (~related(B!25, D, tptp_fun_E_2(D, C, B!25, A!24))) | (~in(apply_netmap(A!24, B!25, tptp_fun_E_2(D, C, B!25, A!24)), C))))))) | (~(is_often_in(A!24, B!25, C) | (~((~element(tptp_fun_D_3(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C)))))))))))),
% 0.19/0.49 inference(quant_inst,[status(thm)],[])).
% 0.19/0.49 tff(39,plain,
% 0.19/0.49 ((~![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B, C)) | ![D: $i] : ((~element(D, the_carrier(B))) | (~((~element(tptp_fun_E_2(D, C, B, A!24), the_carrier(B))) | (~related(B, D, tptp_fun_E_2(D, C, B, A!24))) | (~in(apply_netmap(A!24, B, tptp_fun_E_2(D, C, B, A!24)), C))))))) | (~(is_often_in(A!24, B, C) | (~((~element(tptp_fun_D_3(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | (~related(B, tptp_fun_D_3(C, B, A!24), E)) | (~in(apply_netmap(A!24, B, E), C)))))))))))) | empty_carrier(B!25) | (~net_str(B!25, A!24)) | ![C: $i] : (~((~((~is_often_in(A!24, B!25, C)) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~((~element(tptp_fun_E_2(D, C, B!25, A!24), the_carrier(B!25))) | (~related(B!25, D, tptp_fun_E_2(D, C, B!25, A!24))) | (~in(apply_netmap(A!24, B!25, tptp_fun_E_2(D, C, B!25, A!24)), C))))))) | (~(is_often_in(A!24, B!25, C) | (~((~element(tptp_fun_D_3(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C))))))))))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[38, 37])).
% 0.19/0.49 tff(40,plain,
% 0.19/0.49 (![C: $i] : (~((~((~is_often_in(A!24, B!25, C)) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~((~element(tptp_fun_E_2(D, C, B!25, A!24), the_carrier(B!25))) | (~related(B!25, D, tptp_fun_E_2(D, C, B!25, A!24))) | (~in(apply_netmap(A!24, B!25, tptp_fun_E_2(D, C, B!25, A!24)), C))))))) | (~(is_often_in(A!24, B!25, C) | (~((~element(tptp_fun_D_3(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C))))))))))),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[39, 36, 35, 34])).
% 0.19/0.49 tff(41,plain,
% 0.19/0.49 ((~![C: $i] : (~((~((~is_often_in(A!24, B!25, C)) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~((~element(tptp_fun_E_2(D, C, B!25, A!24), the_carrier(B!25))) | (~related(B!25, D, tptp_fun_E_2(D, C, B!25, A!24))) | (~in(apply_netmap(A!24, B!25, tptp_fun_E_2(D, C, B!25, A!24)), C))))))) | (~(is_often_in(A!24, B!25, C) | (~((~element(tptp_fun_D_3(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C))))))))))) | (~((~((~is_often_in(A!24, B!25, C!26)) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~((~element(tptp_fun_E_2(D, C!26, B!25, A!24), the_carrier(B!25))) | (~related(B!25, D, tptp_fun_E_2(D, C!26, B!25, A!24))) | (~in(apply_netmap(A!24, B!25, tptp_fun_E_2(D, C!26, B!25, A!24)), C!26))))))) | (~(is_often_in(A!24, B!25, C!26) | (~((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26))))))))))),
% 0.19/0.49 inference(quant_inst,[status(thm)],[])).
% 0.19/0.49 tff(42,plain,
% 0.19/0.49 (~((~((~is_often_in(A!24, B!25, C!26)) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~((~element(tptp_fun_E_2(D, C!26, B!25, A!24), the_carrier(B!25))) | (~related(B!25, D, tptp_fun_E_2(D, C!26, B!25, A!24))) | (~in(apply_netmap(A!24, B!25, tptp_fun_E_2(D, C!26, B!25, A!24)), C!26))))))) | (~(is_often_in(A!24, B!25, C!26) | (~((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))))))))),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[41, 40])).
% 0.19/0.49 tff(43,plain,
% 0.19/0.49 (((~((~is_often_in(A!24, B!25, C!26)) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~((~element(tptp_fun_E_2(D, C!26, B!25, A!24), the_carrier(B!25))) | (~related(B!25, D, tptp_fun_E_2(D, C!26, B!25, A!24))) | (~in(apply_netmap(A!24, B!25, tptp_fun_E_2(D, C!26, B!25, A!24)), C!26))))))) | (~(is_often_in(A!24, B!25, C!26) | (~((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26))))))))) | (is_often_in(A!24, B!25, C!26) | (~((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))))))),
% 0.19/0.49 inference(tautology,[status(thm)],[])).
% 0.19/0.49 tff(44,plain,
% 0.19/0.49 (is_often_in(A!24, B!25, C!26) | (~((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26))))))),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[43, 42])).
% 0.19/0.49 tff(45,plain,
% 0.19/0.49 (~((~is_eventually_in(A!24, B!25, C!26)) | is_often_in(A!24, B!25, C!26))),
% 0.19/0.49 inference(and_elim,[status(thm)],[12])).
% 0.19/0.49 tff(46,plain,
% 0.19/0.49 (~is_often_in(A!24, B!25, C!26)),
% 0.19/0.49 inference(or_elim,[status(thm)],[45])).
% 0.19/0.49 tff(47,plain,
% 0.19/0.49 ((~(is_often_in(A!24, B!25, C!26) | (~((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))))))) | is_often_in(A!24, B!25, C!26) | (~((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26))))))),
% 0.19/0.49 inference(tautology,[status(thm)],[])).
% 0.19/0.49 tff(48,plain,
% 0.19/0.49 ((~(is_often_in(A!24, B!25, C!26) | (~((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))))))) | (~((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26))))))),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[47, 46])).
% 0.19/0.49 tff(49,plain,
% 0.19/0.49 (~((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))))),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[48, 44])).
% 0.19/0.49 tff(50,plain,
% 0.19/0.49 (((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26))))) | element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))),
% 0.19/0.49 inference(tautology,[status(thm)],[])).
% 0.19/0.49 tff(51,plain,
% 0.19/0.49 (element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[50, 49])).
% 0.19/0.49 tff(52,plain,
% 0.19/0.49 (^[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.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(53,plain,
% 0.19/0.49 (![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.19/0.49 inference(quant_intro,[status(thm)],[52])).
% 0.19/0.49 tff(54,plain,
% 0.19/0.49 (^[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.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(55,plain,
% 0.19/0.49 (![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.19/0.49 inference(quant_intro,[status(thm)],[54])).
% 0.19/0.49 tff(56,plain,
% 0.19/0.49 (![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.19/0.49 inference(transitivity,[status(thm)],[55, 53])).
% 0.19/0.49 tff(57,plain,
% 0.19/0.49 (![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.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(58,plain,
% 0.19/0.49 (^[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.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(59,plain,
% 0.19/0.49 (![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.19/0.49 inference(quant_intro,[status(thm)],[58])).
% 0.19/0.49 tff(60,axiom,(![A: $i] : (one_sorted_str(A) => ![B: $i] : (net_str(B, A) => rel_str(B)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dt_l1_waybel_0')).
% 0.19/0.49 tff(61,plain,
% 0.19/0.49 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[60, 59])).
% 0.19/0.49 tff(62,plain,
% 0.19/0.49 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[61, 57])).
% 0.19/0.49 tff(63,plain,(
% 0.19/0.49 ![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.19/0.49 inference(skolemize,[status(sab)],[62])).
% 0.19/0.49 tff(64,plain,
% 0.19/0.49 (![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[63, 56])).
% 0.19/0.49 tff(65,plain,
% 0.19/0.49 (((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | ((~one_sorted_str(A!24)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!24))))) <=> ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | (~one_sorted_str(A!24)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!24))))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(66,plain,
% 0.19/0.49 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | ((~one_sorted_str(A!24)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!24))))),
% 0.19/0.49 inference(quant_inst,[status(thm)],[])).
% 0.19/0.49 tff(67,plain,
% 0.19/0.49 ((~![A: $i] : ((~one_sorted_str(A)) | ![B: $i] : (rel_str(B) | (~net_str(B, A))))) | (~one_sorted_str(A!24)) | ![B: $i] : (rel_str(B) | (~net_str(B, A!24)))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.19/0.49 tff(68,plain,
% 0.19/0.49 (![B: $i] : (rel_str(B) | (~net_str(B, A!24)))),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[67, 64, 13])).
% 0.19/0.49 tff(69,plain,
% 0.19/0.49 (((~![B: $i] : (rel_str(B) | (~net_str(B, A!24)))) | (rel_str(B!25) | (~net_str(B!25, A!24)))) <=> ((~![B: $i] : (rel_str(B) | (~net_str(B, A!24)))) | rel_str(B!25) | (~net_str(B!25, A!24)))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(70,plain,
% 0.19/0.49 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!24)))) | (rel_str(B!25) | (~net_str(B!25, A!24)))),
% 0.19/0.49 inference(quant_inst,[status(thm)],[])).
% 0.19/0.49 tff(71,plain,
% 0.19/0.49 ((~![B: $i] : (rel_str(B) | (~net_str(B, A!24)))) | rel_str(B!25) | (~net_str(B!25, A!24))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[70, 69])).
% 0.19/0.49 tff(72,plain,
% 0.19/0.49 (rel_str(B!25)),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[71, 35, 68])).
% 0.19/0.49 tff(73,plain,
% 0.19/0.49 (^[A: $i] : refl((empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D))))))))))) <=> (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D))))))))))))),
% 0.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(74,plain,
% 0.19/0.49 (![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D))))))))))) <=> ![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))),
% 0.19/0.49 inference(quant_intro,[status(thm)],[73])).
% 0.19/0.49 tff(75,plain,
% 0.19/0.49 (^[A: $i] : rewrite((empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D))))))))))) <=> (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D))))))))))))),
% 0.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(76,plain,
% 0.19/0.49 (![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D))))))))))) <=> ![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))),
% 0.19/0.49 inference(quant_intro,[status(thm)],[75])).
% 0.19/0.49 tff(77,plain,
% 0.19/0.49 (![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D))))))))))) <=> ![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))),
% 0.19/0.49 inference(transitivity,[status(thm)],[76, 74])).
% 0.19/0.49 tff(78,plain,
% 0.19/0.49 (^[A: $i] : trans(monotonicity(trans(monotonicity(rewrite(((~empty_carrier(A)) & rel_str(A)) <=> (~(empty_carrier(A) | (~rel_str(A))))), ((~((~empty_carrier(A)) & rel_str(A))) <=> (~(~(empty_carrier(A) | (~rel_str(A))))))), rewrite((~(~(empty_carrier(A) | (~rel_str(A))))) <=> (empty_carrier(A) | (~rel_str(A)))), ((~((~empty_carrier(A)) & rel_str(A))) <=> (empty_carrier(A) | (~rel_str(A))))), trans(monotonicity(rewrite(((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) <=> ((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))), rewrite((directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D))))) <=> (directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))), ((((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D)))))) <=> (((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A)))))))) & (directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))), rewrite((((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A)))))))) & (directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))) <=> (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D))))))))))), ((((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D)))))) <=> (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))), (((~((~empty_carrier(A)) & rel_str(A))) | (((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D))))))) <=> ((empty_carrier(A) | (~rel_str(A))) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D))))))))))))), rewrite(((empty_carrier(A) | (~rel_str(A))) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D))))))))))) <=> (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))), (((~((~empty_carrier(A)) & rel_str(A))) | (((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D))))))) <=> (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))))),
% 0.19/0.50 inference(bind,[status(th)],[])).
% 0.19/0.50 tff(79,plain,
% 0.19/0.50 (![A: $i] : ((~((~empty_carrier(A)) & rel_str(A))) | (((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D))))))) <=> ![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))),
% 0.19/0.50 inference(quant_intro,[status(thm)],[78])).
% 0.19/0.50 tff(80,plain,
% 0.19/0.50 (^[A: $i] : rewrite(((~((~empty_carrier(A)) & rel_str(A))) | (((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & (element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D)))))))) <=> ((~((~empty_carrier(A)) & rel_str(A))) | (((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D))))))))),
% 0.19/0.50 inference(bind,[status(th)],[])).
% 0.19/0.50 tff(81,plain,
% 0.19/0.50 (![A: $i] : ((~((~empty_carrier(A)) & rel_str(A))) | (((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & (element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D)))))))) <=> ![A: $i] : ((~((~empty_carrier(A)) & rel_str(A))) | (((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D)))))))),
% 0.19/0.50 inference(quant_intro,[status(thm)],[80])).
% 0.19/0.50 tff(82,plain,
% 0.19/0.50 (![A: $i] : ((~((~empty_carrier(A)) & rel_str(A))) | (directed_relstr(A) <=> ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | ?[D: $i] : (element(D, the_carrier(A)) & related(A, B, D) & related(A, C, D)))))) <=> ![A: $i] : ((~((~empty_carrier(A)) & rel_str(A))) | (directed_relstr(A) <=> ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | ?[D: $i] : (element(D, the_carrier(A)) & related(A, B, D) & related(A, C, D))))))),
% 0.19/0.50 inference(rewrite,[status(thm)],[])).
% 0.19/0.50 tff(83,plain,
% 0.19/0.50 (^[A: $i] : trans(monotonicity(rewrite((directed_relstr(A) <=> ![B: $i] : (element(B, the_carrier(A)) => ![C: $i] : (element(C, the_carrier(A)) => ?[D: $i] : ((element(D, the_carrier(A)) & related(A, B, D)) & related(A, C, D))))) <=> (directed_relstr(A) <=> ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | ?[D: $i] : (element(D, the_carrier(A)) & related(A, B, D) & related(A, C, D)))))), ((((~empty_carrier(A)) & rel_str(A)) => (directed_relstr(A) <=> ![B: $i] : (element(B, the_carrier(A)) => ![C: $i] : (element(C, the_carrier(A)) => ?[D: $i] : ((element(D, the_carrier(A)) & related(A, B, D)) & related(A, C, D)))))) <=> (((~empty_carrier(A)) & rel_str(A)) => (directed_relstr(A) <=> ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | ?[D: $i] : (element(D, the_carrier(A)) & related(A, B, D) & related(A, C, D)))))))), rewrite((((~empty_carrier(A)) & rel_str(A)) => (directed_relstr(A) <=> ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | ?[D: $i] : (element(D, the_carrier(A)) & related(A, B, D) & related(A, C, D)))))) <=> ((~((~empty_carrier(A)) & rel_str(A))) | (directed_relstr(A) <=> ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | ?[D: $i] : (element(D, the_carrier(A)) & related(A, B, D) & related(A, C, D))))))), ((((~empty_carrier(A)) & rel_str(A)) => (directed_relstr(A) <=> ![B: $i] : (element(B, the_carrier(A)) => ![C: $i] : (element(C, the_carrier(A)) => ?[D: $i] : ((element(D, the_carrier(A)) & related(A, B, D)) & related(A, C, D)))))) <=> ((~((~empty_carrier(A)) & rel_str(A))) | (directed_relstr(A) <=> ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | ?[D: $i] : (element(D, the_carrier(A)) & related(A, B, D) & related(A, C, D))))))))),
% 0.19/0.50 inference(bind,[status(th)],[])).
% 0.19/0.50 tff(84,plain,
% 0.19/0.50 (![A: $i] : (((~empty_carrier(A)) & rel_str(A)) => (directed_relstr(A) <=> ![B: $i] : (element(B, the_carrier(A)) => ![C: $i] : (element(C, the_carrier(A)) => ?[D: $i] : ((element(D, the_carrier(A)) & related(A, B, D)) & related(A, C, D)))))) <=> ![A: $i] : ((~((~empty_carrier(A)) & rel_str(A))) | (directed_relstr(A) <=> ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | ?[D: $i] : (element(D, the_carrier(A)) & related(A, B, D) & related(A, C, D))))))),
% 0.19/0.50 inference(quant_intro,[status(thm)],[83])).
% 0.19/0.50 tff(85,axiom,(![A: $i] : (((~empty_carrier(A)) & rel_str(A)) => (directed_relstr(A) <=> ![B: $i] : (element(B, the_carrier(A)) => ![C: $i] : (element(C, the_carrier(A)) => ?[D: $i] : ((element(D, the_carrier(A)) & related(A, B, D)) & related(A, C, D))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d5_yellow_6')).
% 0.19/0.50 tff(86,plain,
% 0.19/0.50 (![A: $i] : ((~((~empty_carrier(A)) & rel_str(A))) | (directed_relstr(A) <=> ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | ?[D: $i] : (element(D, the_carrier(A)) & related(A, B, D) & related(A, C, D))))))),
% 0.19/0.50 inference(modus_ponens,[status(thm)],[85, 84])).
% 0.19/0.50 tff(87,plain,
% 0.19/0.50 (![A: $i] : ((~((~empty_carrier(A)) & rel_str(A))) | (directed_relstr(A) <=> ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | ?[D: $i] : (element(D, the_carrier(A)) & related(A, B, D) & related(A, C, D))))))),
% 0.19/0.50 inference(modus_ponens,[status(thm)],[86, 82])).
% 0.19/0.50 tff(88,plain,(
% 0.19/0.50 ![A: $i] : ((~((~empty_carrier(A)) & rel_str(A))) | (((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & (element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D))))))))),
% 0.19/0.50 inference(skolemize,[status(sab)],[87])).
% 0.19/0.50 tff(89,plain,
% 0.19/0.50 (![A: $i] : ((~((~empty_carrier(A)) & rel_str(A))) | (((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (element(tptp_fun_D_4(C, B, A), the_carrier(A)) & related(A, B, tptp_fun_D_4(C, B, A)) & related(A, C, tptp_fun_D_4(C, B, A)))))) & (directed_relstr(A) | (element(tptp_fun_B_5(A), the_carrier(A)) & element(tptp_fun_C_6(A), the_carrier(A)) & ![D: $i] : (~(element(D, the_carrier(A)) & related(A, tptp_fun_B_5(A), D) & related(A, tptp_fun_C_6(A), D)))))))),
% 0.19/0.50 inference(modus_ponens,[status(thm)],[88, 81])).
% 0.19/0.50 tff(90,plain,
% 0.19/0.50 (![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))),
% 0.19/0.50 inference(modus_ponens,[status(thm)],[89, 79])).
% 0.19/0.50 tff(91,plain,
% 0.19/0.50 (![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))),
% 0.19/0.50 inference(modus_ponens,[status(thm)],[90, 77])).
% 0.19/0.50 tff(92,plain,
% 0.19/0.50 (((~![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))) | (empty_carrier(B!25) | (~rel_str(B!25)) | (~((~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))) | (~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))))))))))))) <=> ((~![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))) | empty_carrier(B!25) | (~rel_str(B!25)) | (~((~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))) | (~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))))))))))))),
% 0.19/0.50 inference(rewrite,[status(thm)],[])).
% 0.19/0.50 tff(93,plain,
% 0.19/0.50 ((empty_carrier(B!25) | (~rel_str(B!25)) | (~((~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))))))))) | (~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D))))))))))) <=> (empty_carrier(B!25) | (~rel_str(B!25)) | (~((~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))) | (~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))))))))))))),
% 0.19/0.50 inference(rewrite,[status(thm)],[])).
% 0.19/0.50 tff(94,plain,
% 0.19/0.50 (((~![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))) | (empty_carrier(B!25) | (~rel_str(B!25)) | (~((~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))))))))) | (~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))))))) <=> ((~![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))) | (empty_carrier(B!25) | (~rel_str(B!25)) | (~((~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))) | (~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))))))))),
% 0.19/0.50 inference(monotonicity,[status(thm)],[93])).
% 0.19/0.50 tff(95,plain,
% 0.19/0.50 (((~![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))) | (empty_carrier(B!25) | (~rel_str(B!25)) | (~((~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))))))))) | (~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))))))) <=> ((~![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))) | empty_carrier(B!25) | (~rel_str(B!25)) | (~((~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))) | (~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))))))))))))),
% 0.19/0.50 inference(transitivity,[status(thm)],[94, 92])).
% 0.19/0.50 tff(96,plain,
% 0.19/0.50 ((~![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))) | (empty_carrier(B!25) | (~rel_str(B!25)) | (~((~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))))))))) | (~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))))))),
% 0.19/0.50 inference(quant_inst,[status(thm)],[])).
% 0.19/0.50 tff(97,plain,
% 0.19/0.50 ((~![A: $i] : (empty_carrier(A) | (~rel_str(A)) | (~((~((~directed_relstr(A)) | ![B: $i] : ((~element(B, the_carrier(A))) | ![C: $i] : ((~element(C, the_carrier(A))) | (~((~element(tptp_fun_D_4(C, B, A), the_carrier(A))) | (~related(A, B, tptp_fun_D_4(C, B, A))) | (~related(A, C, tptp_fun_D_4(C, B, A))))))))) | (~(directed_relstr(A) | (~((~element(tptp_fun_B_5(A), the_carrier(A))) | (~element(tptp_fun_C_6(A), the_carrier(A))) | (~![D: $i] : ((~element(D, the_carrier(A))) | (~related(A, tptp_fun_B_5(A), D)) | (~related(A, tptp_fun_C_6(A), D)))))))))))) | empty_carrier(B!25) | (~rel_str(B!25)) | (~((~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))) | (~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))))))),
% 0.19/0.50 inference(modus_ponens,[status(thm)],[96, 95])).
% 0.19/0.50 tff(98,plain,
% 0.19/0.50 ((~rel_str(B!25)) | (~((~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))) | (~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))))))),
% 0.19/0.50 inference(unit_resolution,[status(thm)],[97, 91, 36])).
% 0.19/0.50 tff(99,plain,
% 0.19/0.50 (~((~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))) | (~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))))))))))),
% 0.19/0.50 inference(unit_resolution,[status(thm)],[98, 72])).
% 0.19/0.50 tff(100,plain,
% 0.19/0.50 (((~(directed_relstr(B!25) | (~((~element(tptp_fun_B_5(B!25), the_carrier(B!25))) | (~element(tptp_fun_C_6(B!25), the_carrier(B!25))) | (~![D: $i] : ((~element(D, the_carrier(B!25))) | (~related(B!25, tptp_fun_B_5(B!25), D)) | (~related(B!25, tptp_fun_C_6(B!25), D)))))))) | (~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))))) | ((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))))))))),
% 0.19/0.50 inference(tautology,[status(thm)],[])).
% 0.19/0.50 tff(101,plain,
% 0.19/0.50 ((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))),
% 0.19/0.50 inference(unit_resolution,[status(thm)],[100, 99])).
% 0.19/0.50 tff(102,plain,
% 0.19/0.50 (directed_relstr(B!25)),
% 0.19/0.50 inference(and_elim,[status(thm)],[12])).
% 0.19/0.50 tff(103,plain,
% 0.19/0.50 ((~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))))))))) | (~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))),
% 0.19/0.50 inference(tautology,[status(thm)],[])).
% 0.19/0.50 tff(104,plain,
% 0.19/0.50 ((~((~directed_relstr(B!25)) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25))))))))) | ![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))),
% 0.19/0.50 inference(unit_resolution,[status(thm)],[103, 102])).
% 0.19/0.50 tff(105,plain,
% 0.19/0.50 (![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))),
% 0.19/0.50 inference(unit_resolution,[status(thm)],[104, 101])).
% 0.19/0.50 tff(106,plain,
% 0.19/0.50 (((~![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))) | ((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25)))))))) <=> ((~![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))) | (~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25)))))))),
% 0.19/0.51 inference(rewrite,[status(thm)],[])).
% 0.19/0.51 tff(107,plain,
% 0.19/0.51 ((~![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))) | ((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25)))))))),
% 0.19/0.51 inference(quant_inst,[status(thm)],[])).
% 0.19/0.51 tff(108,plain,
% 0.19/0.51 ((~![B: $i] : ((~element(B, the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, B, B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, B, B!25))) | (~related(B!25, B, tptp_fun_D_4(C, B, B!25)))))))) | (~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | ![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))))))),
% 0.19/0.51 inference(modus_ponens,[status(thm)],[107, 106])).
% 0.19/0.51 tff(109,plain,
% 0.19/0.51 (![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))))))),
% 0.19/0.51 inference(unit_resolution,[status(thm)],[108, 105, 51])).
% 0.19/0.51 tff(110,plain,
% 0.19/0.51 (^[A: $i] : refl((empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))))),
% 0.19/0.51 inference(bind,[status(th)],[])).
% 0.19/0.51 tff(111,plain,
% 0.19/0.51 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))),
% 0.19/0.51 inference(quant_intro,[status(thm)],[110])).
% 0.19/0.51 tff(112,plain,
% 0.19/0.51 (^[A: $i] : rewrite((empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))))),
% 0.19/0.51 inference(bind,[status(th)],[])).
% 0.19/0.51 tff(113,plain,
% 0.19/0.51 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))),
% 0.19/0.51 inference(quant_intro,[status(thm)],[112])).
% 0.19/0.51 tff(114,plain,
% 0.19/0.51 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))),
% 0.19/0.51 inference(transitivity,[status(thm)],[113, 111])).
% 0.19/0.51 tff(115,plain,
% 0.19/0.51 (^[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))))), quant_intro(proof_bind(^[B: $i] : trans(monotonicity(trans(monotonicity(rewrite(((~empty_carrier(B)) & net_str(B, A)) <=> (~(empty_carrier(B) | (~net_str(B, A))))), ((~((~empty_carrier(B)) & net_str(B, A))) <=> (~(~(empty_carrier(B) | (~net_str(B, A))))))), rewrite((~(~(empty_carrier(B) | (~net_str(B, A))))) <=> (empty_carrier(B) | (~net_str(B, A)))), ((~((~empty_carrier(B)) & net_str(B, A))) <=> (empty_carrier(B) | (~net_str(B, A))))), quant_intro(proof_bind(^[C: $i] : trans(monotonicity(rewrite(((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) <=> ((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))), rewrite((is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))) <=> (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))), ((((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))) <=> (((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))), rewrite((((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))) <=> (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))), ((((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))) <=> (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))), (![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))) <=> ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))), (((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))) <=> ((empty_carrier(B) | (~net_str(B, A))) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))), rewrite(((empty_carrier(B) | (~net_str(B, A))) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))) <=> (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))), (((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))) <=> (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))))), (![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))) <=> ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))), (((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))) <=> ((empty_carrier(A) | (~one_sorted_str(A))) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))))), rewrite(((empty_carrier(A) | (~one_sorted_str(A))) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))), (((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))))),
% 0.19/0.51 inference(bind,[status(th)],[])).
% 0.19/0.51 tff(116,plain,
% 0.19/0.51 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))),
% 0.19/0.51 inference(quant_intro,[status(thm)],[115])).
% 0.19/0.51 tff(117,plain,
% 0.19/0.51 (^[A: $i] : rewrite(((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)) | (~element(E, the_carrier(B)))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))) <=> ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))))),
% 0.19/0.51 inference(bind,[status(th)],[])).
% 0.19/0.51 tff(118,plain,
% 0.19/0.51 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)) | (~element(E, the_carrier(B)))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B)))))))))) <=> ![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))),
% 0.19/0.51 inference(quant_intro,[status(thm)],[117])).
% 0.19/0.51 tff(119,plain,
% 0.19/0.51 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B)))))))) <=> ![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B))))))))),
% 0.19/0.51 inference(rewrite,[status(thm)],[])).
% 0.19/0.51 tff(120,plain,
% 0.19/0.51 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : rewrite((is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (element(E, the_carrier(B)) => (related(B, D, E) => in(apply_netmap(A, B, E), C))))) <=> (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B)))))))), (![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (element(E, the_carrier(B)) => (related(B, D, E) => in(apply_netmap(A, B, E), C))))) <=> ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B)))))))), ((((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (element(E, the_carrier(B)) => (related(B, D, E) => in(apply_netmap(A, B, E), C)))))) <=> (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B))))))))), rewrite((((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B))))))) <=> ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B)))))))), ((((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (element(E, the_carrier(B)) => (related(B, D, E) => in(apply_netmap(A, B, E), C)))))) <=> ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B)))))))))), (![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (element(E, the_carrier(B)) => (related(B, D, E) => in(apply_netmap(A, B, E), C)))))) <=> ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B))))))))), ((((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (element(E, the_carrier(B)) => (related(B, D, E) => in(apply_netmap(A, B, E), C))))))) <=> (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B)))))))))), rewrite((((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B)))))))) <=> ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B))))))))), ((((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (element(E, the_carrier(B)) => (related(B, D, E) => in(apply_netmap(A, B, E), C))))))) <=> ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B))))))))))),
% 0.19/0.51 inference(bind,[status(th)],[])).
% 0.19/0.51 tff(121,plain,
% 0.19/0.51 (![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (element(E, the_carrier(B)) => (related(B, D, E) => in(apply_netmap(A, B, E), C))))))) <=> ![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B))))))))),
% 0.19/0.51 inference(quant_intro,[status(thm)],[120])).
% 0.19/0.51 tff(122,axiom,(![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((~empty_carrier(B)) & net_str(B, A)) => ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (element(E, the_carrier(B)) => (related(B, D, E) => in(apply_netmap(A, B, E), C)))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d11_waybel_0')).
% 0.19/0.51 tff(123,plain,
% 0.19/0.51 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B))))))))),
% 0.19/0.51 inference(modus_ponens,[status(thm)],[122, 121])).
% 0.19/0.51 tff(124,plain,
% 0.19/0.51 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (is_eventually_in(A, B, C) <=> ?[D: $i] : (element(D, the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, D, E)) | (~element(E, the_carrier(B))))))))),
% 0.19/0.51 inference(modus_ponens,[status(thm)],[123, 119])).
% 0.19/0.51 tff(125,plain,(
% 0.19/0.51 ![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : (in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)) | (~element(E, the_carrier(B)))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))),
% 0.19/0.51 inference(skolemize,[status(sab)],[124])).
% 0.19/0.51 tff(126,plain,
% 0.19/0.51 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty_carrier(B)) & net_str(B, A))) | ![C: $i] : (((~is_eventually_in(A, B, C)) | (element(tptp_fun_D_0(C, B, A), the_carrier(B)) & ![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E))))) & (is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))),
% 0.19/0.51 inference(modus_ponens,[status(thm)],[125, 118])).
% 0.19/0.51 tff(127,plain,
% 0.19/0.51 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))),
% 0.19/0.51 inference(modus_ponens,[status(thm)],[126, 116])).
% 0.19/0.51 tff(128,plain,
% 0.19/0.51 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))),
% 0.19/0.51 inference(modus_ponens,[status(thm)],[127, 114])).
% 0.19/0.51 tff(129,plain,
% 0.19/0.51 (((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))) | (empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E))))))))))))) <=> ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))) | empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E))))))))))))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(130,plain,
% 0.19/0.52 ((empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))) | (~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))))))) <=> (empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E))))))))))))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(131,plain,
% 0.19/0.52 (((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))) | (empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))) | (~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B))))))))))))) <=> ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))) | (empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))))))))),
% 0.19/0.52 inference(monotonicity,[status(thm)],[130])).
% 0.19/0.52 tff(132,plain,
% 0.19/0.52 (((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))) | (empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))) | (~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B))))))))))))) <=> ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))) | empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E))))))))))))),
% 0.19/0.52 inference(transitivity,[status(thm)],[131, 129])).
% 0.19/0.52 tff(133,plain,
% 0.19/0.52 ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))) | (empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))) | (~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B))))))))))))),
% 0.19/0.52 inference(quant_inst,[status(thm)],[])).
% 0.19/0.52 tff(134,plain,
% 0.19/0.52 ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A)) | ![C: $i] : (~((~((~is_eventually_in(A, B, C)) | (~((~element(tptp_fun_D_0(C, B, A), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A), E)))))))) | (~(is_eventually_in(A, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A, B, tptp_fun_E_1(D, C, B, A)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A))) | (~element(tptp_fun_E_1(D, C, B, A), the_carrier(B))))))))))))) | empty_carrier(A!24) | (~one_sorted_str(A!24)) | ![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[133, 132])).
% 0.19/0.52 tff(135,plain,
% 0.19/0.52 (![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))))))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[134, 128, 14, 13])).
% 0.19/0.52 tff(136,plain,
% 0.19/0.52 (((~![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))))))) | (empty_carrier(B!25) | (~net_str(B!25, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B!25, C) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~(in(apply_netmap(A!24, B!25, tptp_fun_E_1(D, C, B!25, A!24)), C) | (~related(B!25, D, tptp_fun_E_1(D, C, B!25, A!24))) | (~element(tptp_fun_E_1(D, C, B!25, A!24), the_carrier(B!25)))))))) | (~((~is_eventually_in(A!24, B!25, C)) | (~((~element(tptp_fun_D_0(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C) | (~related(B!25, tptp_fun_D_0(C, B!25, A!24), E)))))))))))) <=> ((~![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))))))) | empty_carrier(B!25) | (~net_str(B!25, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B!25, C) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~(in(apply_netmap(A!24, B!25, tptp_fun_E_1(D, C, B!25, A!24)), C) | (~related(B!25, D, tptp_fun_E_1(D, C, B!25, A!24))) | (~element(tptp_fun_E_1(D, C, B!25, A!24), the_carrier(B!25)))))))) | (~((~is_eventually_in(A!24, B!25, C)) | (~((~element(tptp_fun_D_0(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C) | (~related(B!25, tptp_fun_D_0(C, B!25, A!24), E)))))))))))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(137,plain,
% 0.19/0.52 ((~![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))))))) | (empty_carrier(B!25) | (~net_str(B!25, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B!25, C) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~(in(apply_netmap(A!24, B!25, tptp_fun_E_1(D, C, B!25, A!24)), C) | (~related(B!25, D, tptp_fun_E_1(D, C, B!25, A!24))) | (~element(tptp_fun_E_1(D, C, B!25, A!24), the_carrier(B!25)))))))) | (~((~is_eventually_in(A!24, B!25, C)) | (~((~element(tptp_fun_D_0(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C) | (~related(B!25, tptp_fun_D_0(C, B!25, A!24), E)))))))))))),
% 0.19/0.52 inference(quant_inst,[status(thm)],[])).
% 0.19/0.52 tff(138,plain,
% 0.19/0.52 ((~![B: $i] : (empty_carrier(B) | (~net_str(B, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B, C) | ![D: $i] : ((~element(D, the_carrier(B))) | (~(in(apply_netmap(A!24, B, tptp_fun_E_1(D, C, B, A!24)), C) | (~related(B, D, tptp_fun_E_1(D, C, B, A!24))) | (~element(tptp_fun_E_1(D, C, B, A!24), the_carrier(B)))))))) | (~((~is_eventually_in(A!24, B, C)) | (~((~element(tptp_fun_D_0(C, B, A!24), the_carrier(B))) | (~![E: $i] : ((~element(E, the_carrier(B))) | in(apply_netmap(A!24, B, E), C) | (~related(B, tptp_fun_D_0(C, B, A!24), E)))))))))))) | empty_carrier(B!25) | (~net_str(B!25, A!24)) | ![C: $i] : (~((~(is_eventually_in(A!24, B!25, C) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~(in(apply_netmap(A!24, B!25, tptp_fun_E_1(D, C, B!25, A!24)), C) | (~related(B!25, D, tptp_fun_E_1(D, C, B!25, A!24))) | (~element(tptp_fun_E_1(D, C, B!25, A!24), the_carrier(B!25)))))))) | (~((~is_eventually_in(A!24, B!25, C)) | (~((~element(tptp_fun_D_0(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C) | (~related(B!25, tptp_fun_D_0(C, B!25, A!24), E))))))))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[137, 136])).
% 0.19/0.52 tff(139,plain,
% 0.19/0.52 (![C: $i] : (~((~(is_eventually_in(A!24, B!25, C) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~(in(apply_netmap(A!24, B!25, tptp_fun_E_1(D, C, B!25, A!24)), C) | (~related(B!25, D, tptp_fun_E_1(D, C, B!25, A!24))) | (~element(tptp_fun_E_1(D, C, B!25, A!24), the_carrier(B!25)))))))) | (~((~is_eventually_in(A!24, B!25, C)) | (~((~element(tptp_fun_D_0(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C) | (~related(B!25, tptp_fun_D_0(C, B!25, A!24), E))))))))))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[138, 36, 35, 135])).
% 0.19/0.52 tff(140,plain,
% 0.19/0.52 ((~![C: $i] : (~((~(is_eventually_in(A!24, B!25, C) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~(in(apply_netmap(A!24, B!25, tptp_fun_E_1(D, C, B!25, A!24)), C) | (~related(B!25, D, tptp_fun_E_1(D, C, B!25, A!24))) | (~element(tptp_fun_E_1(D, C, B!25, A!24), the_carrier(B!25)))))))) | (~((~is_eventually_in(A!24, B!25, C)) | (~((~element(tptp_fun_D_0(C, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C) | (~related(B!25, tptp_fun_D_0(C, B!25, A!24), E))))))))))) | (~((~(is_eventually_in(A!24, B!25, C!26) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~(in(apply_netmap(A!24, B!25, tptp_fun_E_1(D, C!26, B!25, A!24)), C!26) | (~related(B!25, D, tptp_fun_E_1(D, C!26, B!25, A!24))) | (~element(tptp_fun_E_1(D, C!26, B!25, A!24), the_carrier(B!25)))))))) | (~((~is_eventually_in(A!24, B!25, C!26)) | (~((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E))))))))))),
% 0.19/0.52 inference(quant_inst,[status(thm)],[])).
% 0.19/0.52 tff(141,plain,
% 0.19/0.52 (~((~(is_eventually_in(A!24, B!25, C!26) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~(in(apply_netmap(A!24, B!25, tptp_fun_E_1(D, C!26, B!25, A!24)), C!26) | (~related(B!25, D, tptp_fun_E_1(D, C!26, B!25, A!24))) | (~element(tptp_fun_E_1(D, C!26, B!25, A!24), the_carrier(B!25)))))))) | (~((~is_eventually_in(A!24, B!25, C!26)) | (~((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))))))))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[140, 139])).
% 0.19/0.52 tff(142,plain,
% 0.19/0.52 (((~(is_eventually_in(A!24, B!25, C!26) | ![D: $i] : ((~element(D, the_carrier(B!25))) | (~(in(apply_netmap(A!24, B!25, tptp_fun_E_1(D, C!26, B!25, A!24)), C!26) | (~related(B!25, D, tptp_fun_E_1(D, C!26, B!25, A!24))) | (~element(tptp_fun_E_1(D, C!26, B!25, A!24), the_carrier(B!25)))))))) | (~((~is_eventually_in(A!24, B!25, C!26)) | (~((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E))))))))) | ((~is_eventually_in(A!24, B!25, C!26)) | (~((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))))))),
% 0.19/0.52 inference(tautology,[status(thm)],[])).
% 0.19/0.52 tff(143,plain,
% 0.19/0.52 ((~is_eventually_in(A!24, B!25, C!26)) | (~((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E))))))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[142, 141])).
% 0.19/0.52 tff(144,plain,
% 0.19/0.52 (is_eventually_in(A!24, B!25, C!26)),
% 0.19/0.52 inference(or_elim,[status(thm)],[45])).
% 0.19/0.52 tff(145,plain,
% 0.19/0.52 ((~((~is_eventually_in(A!24, B!25, C!26)) | (~((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))))))) | (~is_eventually_in(A!24, B!25, C!26)) | (~((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E))))))),
% 0.19/0.52 inference(tautology,[status(thm)],[])).
% 0.19/0.52 tff(146,plain,
% 0.19/0.52 ((~((~is_eventually_in(A!24, B!25, C!26)) | (~((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))))))) | (~((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E))))))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[145, 144])).
% 0.19/0.52 tff(147,plain,
% 0.19/0.52 (~((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[146, 143])).
% 0.19/0.52 tff(148,plain,
% 0.19/0.52 (((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E))))) | element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))),
% 0.19/0.52 inference(tautology,[status(thm)],[])).
% 0.19/0.52 tff(149,plain,
% 0.19/0.52 (element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[148, 147])).
% 0.19/0.52 tff(150,plain,
% 0.19/0.52 (((~![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))))))) | ((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))))))) <=> ((~![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))))))) | (~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))))))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(151,plain,
% 0.19/0.53 ((~![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))))))) | ((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))))))),
% 0.19/0.53 inference(quant_inst,[status(thm)],[])).
% 0.19/0.53 tff(152,plain,
% 0.19/0.53 ((~![C: $i] : ((~element(C, the_carrier(B!25))) | (~((~element(tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, C, tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(C, tptp_fun_D_3(C!26, B!25, A!24), B!25))))))) | (~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)))))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[151, 150])).
% 0.19/0.53 tff(153,plain,
% 0.19/0.53 (~((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[152, 149, 109])).
% 0.19/0.53 tff(154,plain,
% 0.19/0.53 (((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)))) | related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(155,plain,
% 0.19/0.53 (related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[154, 153])).
% 0.19/0.53 tff(156,plain,
% 0.19/0.53 (((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)))) | element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(157,plain,
% 0.19/0.53 (element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[156, 153])).
% 0.19/0.53 tff(158,plain,
% 0.19/0.53 (((~element(tptp_fun_D_3(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26))))) | ![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(159,plain,
% 0.19/0.53 (![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[158, 49])).
% 0.19/0.53 tff(160,plain,
% 0.19/0.53 (((~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))) | ((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26)))) <=> ((~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))) | (~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26)))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(161,plain,
% 0.19/0.53 ((~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))) | ((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26)))),
% 0.19/0.53 inference(quant_inst,[status(thm)],[])).
% 0.19/0.53 tff(162,plain,
% 0.19/0.53 ((~![E: $i] : ((~element(E, the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), E)) | (~in(apply_netmap(A!24, B!25, E), C!26)))) | (~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[161, 160])).
% 0.19/0.53 tff(163,plain,
% 0.19/0.53 (~in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26)),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[162, 159, 157, 155])).
% 0.19/0.53 tff(164,plain,
% 0.19/0.53 (((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | (~related(B!25, tptp_fun_D_3(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)))) | related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(165,plain,
% 0.19/0.53 (related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[164, 153])).
% 0.19/0.53 tff(166,plain,
% 0.19/0.53 (((~element(tptp_fun_D_0(C!26, B!25, A!24), the_carrier(B!25))) | (~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E))))) | ![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(167,plain,
% 0.19/0.53 (![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[166, 147])).
% 0.19/0.53 tff(168,plain,
% 0.19/0.53 (((~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))) | ((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26))) <=> ((~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))) | (~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(169,plain,
% 0.19/0.53 (((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)))) <=> ((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(170,plain,
% 0.19/0.53 (((~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))) | ((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))))) <=> ((~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))) | ((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26)))),
% 0.19/0.53 inference(monotonicity,[status(thm)],[169])).
% 0.19/0.53 tff(171,plain,
% 0.19/0.53 (((~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))) | ((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))))) <=> ((~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))) | (~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26))),
% 0.19/0.53 inference(transitivity,[status(thm)],[170, 168])).
% 0.19/0.53 tff(172,plain,
% 0.19/0.53 ((~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))) | ((~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))))),
% 0.19/0.53 inference(quant_inst,[status(thm)],[])).
% 0.19/0.53 tff(173,plain,
% 0.19/0.53 ((~![E: $i] : ((~element(E, the_carrier(B!25))) | in(apply_netmap(A!24, B!25, E), C!26) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), E)))) | (~element(tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25), the_carrier(B!25))) | (~related(B!25, tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25))) | in(apply_netmap(A!24, B!25, tptp_fun_D_4(tptp_fun_D_0(C!26, B!25, A!24), tptp_fun_D_3(C!26, B!25, A!24), B!25)), C!26)),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[172, 171])).
% 0.19/0.53 tff(174,plain,
% 0.19/0.53 ($false),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[173, 167, 157, 165, 163])).
% 0.19/0.53 % SZS output end Proof
% 0.19/0.54 % E exiting
%------------------------------------------------------------------------------