%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT062+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:24:09 AM UTC 2026
% Result : Theorem 0.14s 0.43s
% Output : Proof 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT062+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.07/0.34 % Computer : n028.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 7 13:40:51 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.14/0.43 % SZS status Theorem
% 0.14/0.43 % SZS output start Proof
% 0.14/0.43 tff(smaller_type, type, (
% 0.14/0.43 smaller: ( $i * $i ) > $o)).
% 0.14/0.43 tff(hazard_of_mortality_type, type, (
% 0.14/0.43 hazard_of_mortality: ( $i * $i ) > $i)).
% 0.14/0.43 tff(tptp_fun_T1_2_type, type, (
% 0.14/0.43 tptp_fun_T1_2: $i)).
% 0.14/0.43 tff(tptp_fun_X_4_type, type, (
% 0.14/0.43 tptp_fun_X_4: $i)).
% 0.14/0.43 tff(tptp_fun_T2_1_type, type, (
% 0.14/0.43 tptp_fun_T2_1: $i)).
% 0.14/0.43 tff(mod2_type, type, (
% 0.14/0.43 mod2: $i)).
% 0.14/0.43 tff(mod1_type, type, (
% 0.14/0.43 mod1: $i)).
% 0.14/0.43 tff(is_aligned_type, type, (
% 0.14/0.43 is_aligned: ( $i * $i ) > $o)).
% 0.14/0.43 tff(tptp_fun_T0_3_type, type, (
% 0.14/0.43 tptp_fun_T0_3: $i)).
% 0.14/0.43 tff(organization_type, type, (
% 0.14/0.43 organization: $i > $o)).
% 0.14/0.43 tff(dissimilar_type, type, (
% 0.14/0.43 dissimilar: ( $i * $i * $i ) > $o)).
% 0.14/0.43 tff(greater_type, type, (
% 0.14/0.43 greater: ( $i * $i ) > $o)).
% 0.14/0.43 tff(sigma_type, type, (
% 0.14/0.43 sigma: $i)).
% 0.14/0.43 tff(age_type, type, (
% 0.14/0.43 age: ( $i * $i ) > $i)).
% 0.14/0.43 tff(zero_type, type, (
% 0.14/0.43 zero: $i)).
% 0.14/0.43 tff(smaller_or_equal_type, type, (
% 0.14/0.43 smaller_or_equal: ( $i * $i ) > $o)).
% 0.14/0.43 tff(tau_type, type, (
% 0.14/0.43 tau: $i)).
% 0.14/0.43 tff(has_endowment_type, type, (
% 0.14/0.43 has_endowment: $i > $o)).
% 0.14/0.43 tff(robust_position_type, type, (
% 0.14/0.43 robust_position: $i > $o)).
% 0.14/0.43 tff(positional_advantage_type, type, (
% 0.14/0.43 positional_advantage: ( $i * $i ) > $o)).
% 0.14/0.43 tff(tptp_fun_T_0_type, type, (
% 0.14/0.43 tptp_fun_T_0: $i > $i)).
% 0.14/0.43 tff(high_type, type, (
% 0.14/0.43 high: $i)).
% 0.14/0.43 tff(low_type, type, (
% 0.14/0.43 low: $i)).
% 0.14/0.43 tff(has_immunity_type, type, (
% 0.14/0.43 has_immunity: ( $i * $i ) > $o)).
% 0.14/0.43 tff(very_low_type, type, (
% 0.14/0.43 very_low: $i)).
% 0.14/0.43 tff(1,plain,
% 0.14/0.43 (^[X: $i, T0: $i, T: $i] : refl((~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T))) <=> (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T))))),
% 0.14/0.43 inference(bind,[status(th)],[])).
% 0.14/0.43 tff(2,plain,
% 0.14/0.43 (![X: $i, T0: $i, T: $i] : (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T))) <=> ![X: $i, T0: $i, T: $i] : (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T)))),
% 0.14/0.43 inference(quant_intro,[status(thm)],[1])).
% 0.14/0.43 tff(3,plain,
% 0.14/0.43 (^[X: $i, T0: $i, T: $i] : trans(trans(monotonicity(trans(monotonicity(rewrite((~(is_aligned(X, T0) <=> is_aligned(X, T))) <=> (~(is_aligned(X, T0) <=> is_aligned(X, T)))), ((organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T)))) <=> (organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T)))))), rewrite((organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T)))) <=> (~((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))))), ((organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T)))) <=> (~((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T)))))), ((dissimilar(X, T0, T) <=> (organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T))))) <=> (dissimilar(X, T0, T) <=> (~((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))))))), rewrite((dissimilar(X, T0, T) <=> (~((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))))) <=> (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T)))), ((dissimilar(X, T0, T) <=> (organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T))))) <=> (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T))))), rewrite((~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T))) <=> (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T)))), ((dissimilar(X, T0, T) <=> (organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T))))) <=> (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T)))))),
% 0.14/0.43 inference(bind,[status(th)],[])).
% 0.14/0.43 tff(4,plain,
% 0.14/0.43 (![X: $i, T0: $i, T: $i] : (dissimilar(X, T0, T) <=> (organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T))))) <=> ![X: $i, T0: $i, T: $i] : (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T)))),
% 0.14/0.43 inference(quant_intro,[status(thm)],[3])).
% 0.14/0.43 tff(5,plain,
% 0.14/0.43 (![X: $i, T0: $i, T: $i] : (dissimilar(X, T0, T) <=> (organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T))))) <=> ![X: $i, T0: $i, T: $i] : (dissimilar(X, T0, T) <=> (organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T)))))),
% 0.14/0.43 inference(rewrite,[status(thm)],[])).
% 0.14/0.43 tff(6,axiom,(![X: $i, T0: $i, T: $i] : (dissimilar(X, T0, T) <=> (organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','definition_2')).
% 0.14/0.43 tff(7,plain,
% 0.14/0.43 (![X: $i, T0: $i, T: $i] : (dissimilar(X, T0, T) <=> (organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T)))))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.14/0.43 tff(8,plain,(
% 0.14/0.43 ![X: $i, T0: $i, T: $i] : (dissimilar(X, T0, T) <=> (organization(X) & (~(is_aligned(X, T0) <=> is_aligned(X, T)))))),
% 0.14/0.43 inference(skolemize,[status(sab)],[7])).
% 0.14/0.43 tff(9,plain,
% 0.14/0.43 (![X: $i, T0: $i, T: $i] : (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T)))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[8, 4])).
% 0.14/0.43 tff(10,plain,
% 0.14/0.43 (![X: $i, T0: $i, T: $i] : (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T)))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[9, 2])).
% 0.14/0.43 tff(11,plain,
% 0.14/0.43 ((~![X: $i, T0: $i, T: $i] : (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T)))) | (~(((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2))) <=> dissimilar(X!4, T0!3, T1!2)))),
% 0.14/0.43 inference(quant_inst,[status(thm)],[])).
% 0.14/0.43 tff(12,plain,
% 0.14/0.43 (~(((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2))) <=> dissimilar(X!4, T0!3, T1!2))),
% 0.14/0.43 inference(unit_resolution,[status(thm)],[11, 10])).
% 0.14/0.43 tff(13,plain,
% 0.14/0.43 ((~![X: $i, T0: $i, T1: $i, T2: $i] : ((~(organization(X) & robust_position(X) & (~has_endowment(X)) & (age(X, T0) = zero) & greater(sigma, zero) & greater(tau, zero) & (sigma = tau) & smaller_or_equal(age(X, T1), sigma) & greater(age(X, T2), sigma))) | (smaller(hazard_of_mortality(X, T2), hazard_of_mortality(X, T1)) & (hazard_of_mortality(X, T1) = hazard_of_mortality(X, T0))))) <=> (~![X: $i, T0: $i, T1: $i, T2: $i] : ((~(organization(X) & robust_position(X) & (~has_endowment(X)) & (age(X, T0) = zero) & greater(sigma, zero) & greater(tau, zero) & (sigma = tau) & smaller_or_equal(age(X, T1), sigma) & greater(age(X, T2), sigma))) | (smaller(hazard_of_mortality(X, T2), hazard_of_mortality(X, T1)) & (hazard_of_mortality(X, T1) = hazard_of_mortality(X, T0)))))),
% 0.14/0.43 inference(rewrite,[status(thm)],[])).
% 0.14/0.43 tff(14,plain,
% 0.14/0.43 ((~![X: $i, T0: $i, T1: $i, T2: $i] : (((((((((organization(X) & robust_position(X)) & (~has_endowment(X))) & (age(X, T0) = zero)) & greater(sigma, zero)) & greater(tau, zero)) & (sigma = tau)) & smaller_or_equal(age(X, T1), sigma)) & greater(age(X, T2), sigma)) => (smaller(hazard_of_mortality(X, T2), hazard_of_mortality(X, T1)) & (hazard_of_mortality(X, T1) = hazard_of_mortality(X, T0))))) <=> (~![X: $i, T0: $i, T1: $i, T2: $i] : ((~(organization(X) & robust_position(X) & (~has_endowment(X)) & (age(X, T0) = zero) & greater(sigma, zero) & greater(tau, zero) & (sigma = tau) & smaller_or_equal(age(X, T1), sigma) & greater(age(X, T2), sigma))) | (smaller(hazard_of_mortality(X, T2), hazard_of_mortality(X, T1)) & (hazard_of_mortality(X, T1) = hazard_of_mortality(X, T0)))))),
% 0.14/0.43 inference(rewrite,[status(thm)],[])).
% 0.14/0.43 tff(15,axiom,(~![X: $i, T0: $i, T1: $i, T2: $i] : (((((((((organization(X) & robust_position(X)) & (~has_endowment(X))) & (age(X, T0) = zero)) & greater(sigma, zero)) & greater(tau, zero)) & (sigma = tau)) & smaller_or_equal(age(X, T1), sigma)) & greater(age(X, T2), sigma)) => (smaller(hazard_of_mortality(X, T2), hazard_of_mortality(X, T1)) & (hazard_of_mortality(X, T1) = hazard_of_mortality(X, T0))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','theorem_8')).
% 0.14/0.43 tff(16,plain,
% 0.14/0.43 (~![X: $i, T0: $i, T1: $i, T2: $i] : ((~(organization(X) & robust_position(X) & (~has_endowment(X)) & (age(X, T0) = zero) & greater(sigma, zero) & greater(tau, zero) & (sigma = tau) & smaller_or_equal(age(X, T1), sigma) & greater(age(X, T2), sigma))) | (smaller(hazard_of_mortality(X, T2), hazard_of_mortality(X, T1)) & (hazard_of_mortality(X, T1) = hazard_of_mortality(X, T0))))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.14/0.43 tff(17,plain,
% 0.14/0.43 (~![X: $i, T0: $i, T1: $i, T2: $i] : ((~(organization(X) & robust_position(X) & (~has_endowment(X)) & (age(X, T0) = zero) & greater(sigma, zero) & greater(tau, zero) & (sigma = tau) & smaller_or_equal(age(X, T1), sigma) & greater(age(X, T2), sigma))) | (smaller(hazard_of_mortality(X, T2), hazard_of_mortality(X, T1)) & (hazard_of_mortality(X, T1) = hazard_of_mortality(X, T0))))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[16, 13])).
% 0.14/0.43 tff(18,plain,
% 0.14/0.43 (~![X: $i, T0: $i, T1: $i, T2: $i] : ((~(organization(X) & robust_position(X) & (~has_endowment(X)) & (age(X, T0) = zero) & greater(sigma, zero) & greater(tau, zero) & (sigma = tau) & smaller_or_equal(age(X, T1), sigma) & greater(age(X, T2), sigma))) | (smaller(hazard_of_mortality(X, T2), hazard_of_mortality(X, T1)) & (hazard_of_mortality(X, T1) = hazard_of_mortality(X, T0))))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[17, 13])).
% 0.14/0.43 tff(19,plain,
% 0.14/0.43 (~![X: $i, T0: $i, T1: $i, T2: $i] : ((~(organization(X) & robust_position(X) & (~has_endowment(X)) & (age(X, T0) = zero) & greater(sigma, zero) & greater(tau, zero) & (sigma = tau) & smaller_or_equal(age(X, T1), sigma) & greater(age(X, T2), sigma))) | (smaller(hazard_of_mortality(X, T2), hazard_of_mortality(X, T1)) & (hazard_of_mortality(X, T1) = hazard_of_mortality(X, T0))))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[18, 13])).
% 0.14/0.43 tff(20,plain,(
% 0.14/0.43 ~((~(organization(X!4) & robust_position(X!4) & (~has_endowment(X!4)) & (age(X!4, T0!3) = zero) & greater(sigma, zero) & greater(tau, zero) & (sigma = tau) & smaller_or_equal(age(X!4, T1!2), sigma) & greater(age(X!4, T2!1), sigma))) | (smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2)) & (hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3))))),
% 0.14/0.43 inference(skolemize,[status(sab)],[19])).
% 0.14/0.43 tff(21,plain,
% 0.14/0.43 (organization(X!4) & robust_position(X!4) & (~has_endowment(X!4)) & (age(X!4, T0!3) = zero) & greater(sigma, zero) & greater(tau, zero) & (sigma = tau) & smaller_or_equal(age(X!4, T1!2), sigma) & greater(age(X!4, T2!1), sigma)),
% 0.14/0.43 inference(or_elim,[status(thm)],[20])).
% 0.14/0.43 tff(22,plain,
% 0.14/0.43 (age(X!4, T0!3) = zero),
% 0.14/0.43 inference(and_elim,[status(thm)],[21])).
% 0.14/0.43 tff(23,plain,
% 0.14/0.43 (organization(X!4)),
% 0.14/0.43 inference(and_elim,[status(thm)],[21])).
% 0.14/0.43 tff(24,plain,
% 0.14/0.43 (^[X: $i, T0: $i, T: $i] : refl(((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero))) <=> ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero))))),
% 0.14/0.43 inference(bind,[status(th)],[])).
% 0.14/0.43 tff(25,plain,
% 0.14/0.43 (![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero))) <=> ![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))),
% 0.14/0.43 inference(quant_intro,[status(thm)],[24])).
% 0.14/0.43 tff(26,plain,
% 0.14/0.43 (^[X: $i, T0: $i, T: $i] : trans(monotonicity(trans(monotonicity(rewrite((organization(X) & (age(X, T0) = zero)) <=> (~((~organization(X)) | (~(age(X, T0) = zero))))), ((~(organization(X) & (age(X, T0) = zero))) <=> (~(~((~organization(X)) | (~(age(X, T0) = zero))))))), rewrite((~(~((~organization(X)) | (~(age(X, T0) = zero))))) <=> ((~organization(X)) | (~(age(X, T0) = zero)))), ((~(organization(X) & (age(X, T0) = zero))) <=> ((~organization(X)) | (~(age(X, T0) = zero))))), (((~(organization(X) & (age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T))) <=> (((~organization(X)) | (~(age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T))))), rewrite((((~organization(X)) | (~(age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T))) <=> ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))), (((~(organization(X) & (age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T))) <=> ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))))),
% 0.14/0.44 inference(bind,[status(th)],[])).
% 0.14/0.44 tff(27,plain,
% 0.14/0.44 (![X: $i, T0: $i, T: $i] : ((~(organization(X) & (age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T))) <=> ![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))),
% 0.14/0.44 inference(quant_intro,[status(thm)],[26])).
% 0.14/0.44 tff(28,plain,
% 0.14/0.44 (![X: $i, T0: $i, T: $i] : ((~(organization(X) & (age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T))) <=> ![X: $i, T0: $i, T: $i] : ((~(organization(X) & (age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T)))),
% 0.14/0.44 inference(rewrite,[status(thm)],[])).
% 0.14/0.44 tff(29,plain,
% 0.14/0.44 (^[X: $i, T0: $i, T: $i] : rewrite(((organization(X) & (age(X, T0) = zero)) => (greater(age(X, T), sigma) <=> dissimilar(X, T0, T))) <=> ((~(organization(X) & (age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T))))),
% 0.14/0.44 inference(bind,[status(th)],[])).
% 0.14/0.44 tff(30,plain,
% 0.14/0.44 (![X: $i, T0: $i, T: $i] : ((organization(X) & (age(X, T0) = zero)) => (greater(age(X, T), sigma) <=> dissimilar(X, T0, T))) <=> ![X: $i, T0: $i, T: $i] : ((~(organization(X) & (age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T)))),
% 0.14/0.44 inference(quant_intro,[status(thm)],[29])).
% 0.14/0.44 tff(31,axiom,(![X: $i, T0: $i, T: $i] : ((organization(X) & (age(X, T0) = zero)) => (greater(age(X, T), sigma) <=> dissimilar(X, T0, T)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_15')).
% 0.14/0.44 tff(32,plain,
% 0.14/0.44 (![X: $i, T0: $i, T: $i] : ((~(organization(X) & (age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T)))),
% 0.14/0.44 inference(modus_ponens,[status(thm)],[31, 30])).
% 0.14/0.44 tff(33,plain,
% 0.14/0.44 (![X: $i, T0: $i, T: $i] : ((~(organization(X) & (age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T)))),
% 0.14/0.44 inference(modus_ponens,[status(thm)],[32, 28])).
% 0.14/0.44 tff(34,plain,(
% 0.14/0.44 ![X: $i, T0: $i, T: $i] : ((~(organization(X) & (age(X, T0) = zero))) | (greater(age(X, T), sigma) <=> dissimilar(X, T0, T)))),
% 0.14/0.44 inference(skolemize,[status(sab)],[33])).
% 0.14/0.44 tff(35,plain,
% 0.14/0.44 (![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))),
% 0.14/0.44 inference(modus_ponens,[status(thm)],[34, 27])).
% 0.14/0.44 tff(36,plain,
% 0.14/0.44 (![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))),
% 0.14/0.44 inference(modus_ponens,[status(thm)],[35, 25])).
% 0.14/0.44 tff(37,plain,
% 0.14/0.44 (((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | ((~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2)))) <=> ((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2)))),
% 0.14/0.44 inference(rewrite,[status(thm)],[])).
% 0.14/0.44 tff(38,plain,
% 0.14/0.44 (((greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2)) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero))) <=> ((~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2)))),
% 0.14/0.44 inference(rewrite,[status(thm)],[])).
% 0.14/0.44 tff(39,plain,
% 0.14/0.44 (((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | ((greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2)) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)))) <=> ((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | ((~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2))))),
% 0.14/0.44 inference(monotonicity,[status(thm)],[38])).
% 0.14/0.44 tff(40,plain,
% 0.14/0.44 (((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | ((greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2)) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)))) <=> ((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2)))),
% 0.14/0.44 inference(transitivity,[status(thm)],[39, 37])).
% 0.14/0.44 tff(41,plain,
% 0.14/0.44 ((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | ((greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2)) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)))),
% 0.14/0.44 inference(quant_inst,[status(thm)],[])).
% 0.14/0.44 tff(42,plain,
% 0.14/0.44 ((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2))),
% 0.14/0.44 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.14/0.44 tff(43,plain,
% 0.14/0.44 (greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2)),
% 0.14/0.44 inference(unit_resolution,[status(thm)],[42, 36, 23, 22])).
% 0.14/0.44 tff(44,plain,
% 0.14/0.44 (sigma = tau),
% 0.14/0.44 inference(and_elim,[status(thm)],[21])).
% 0.14/0.44 tff(45,plain,
% 0.14/0.44 (greater(age(X!4, T1!2), sigma) <=> greater(age(X!4, T1!2), tau)),
% 0.14/0.44 inference(monotonicity,[status(thm)],[44])).
% 0.14/0.44 tff(46,plain,
% 0.14/0.44 (greater(age(X!4, T1!2), tau) <=> greater(age(X!4, T1!2), sigma)),
% 0.14/0.44 inference(symmetry,[status(thm)],[45])).
% 0.14/0.44 tff(47,plain,
% 0.14/0.44 ((~greater(age(X!4, T1!2), tau)) <=> (~greater(age(X!4, T1!2), sigma))),
% 0.14/0.44 inference(monotonicity,[status(thm)],[46])).
% 0.14/0.44 tff(48,plain,
% 0.14/0.44 (^[X: $i] : rewrite((~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))) <=> (~((~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))) | (~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))))))),
% 0.14/0.44 inference(bind,[status(th)],[])).
% 0.14/0.44 tff(49,plain,
% 0.14/0.44 (![X: $i] : (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))) <=> ![X: $i] : (~((~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))) | (~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T)))))))))),
% 0.14/0.44 inference(quant_intro,[status(thm)],[48])).
% 0.14/0.44 tff(50,plain,
% 0.14/0.44 (^[X: $i] : refl((~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))) <=> (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))))),
% 0.14/0.44 inference(bind,[status(th)],[])).
% 0.14/0.44 tff(51,plain,
% 0.14/0.44 (![X: $i] : (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))) <=> ![X: $i] : (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))))),
% 0.14/0.44 inference(quant_intro,[status(thm)],[50])).
% 0.14/0.44 tff(52,plain,
% 0.14/0.44 (^[X: $i] : rewrite((~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))) <=> (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))))),
% 0.14/0.44 inference(bind,[status(th)],[])).
% 0.14/0.44 tff(53,plain,
% 0.14/0.44 (![X: $i] : (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))) <=> ![X: $i] : (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))))),
% 0.14/0.44 inference(quant_intro,[status(thm)],[52])).
% 0.14/0.44 tff(54,plain,
% 0.14/0.44 (![X: $i] : (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))) <=> ![X: $i] : (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))))),
% 0.14/0.44 inference(transitivity,[status(thm)],[53, 51])).
% 0.14/0.44 tff(55,plain,
% 0.14/0.44 (^[X: $i] : trans(monotonicity(rewrite(((~robust_position(X)) | ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T)))) <=> ((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))), trans(monotonicity(trans(monotonicity(rewrite((((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau))) & ((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))) <=> (~((~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))), ((~(((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau))) & ((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))) <=> (~(~((~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))))), rewrite((~(~((~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))) <=> ((~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))), ((~(((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau))) & ((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))) <=> ((~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))), ((robust_position(X) | (~(((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau))) & ((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))) <=> (robust_position(X) | ((~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))), rewrite((robust_position(X) | ((~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))) <=> (robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))), ((robust_position(X) | (~(((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau))) & ((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))) <=> (robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))), ((((~robust_position(X)) | ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T)))) & (robust_position(X) | (~(((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau))) & ((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))) <=> (((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T)))))) & (robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))), rewrite((((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T)))))) & (robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))) <=> (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))))), ((((~robust_position(X)) | ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T)))) & (robust_position(X) | (~(((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau))) & ((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))) <=> (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))))))),
% 0.14/0.44 inference(bind,[status(th)],[])).
% 0.14/0.44 tff(56,plain,
% 0.14/0.44 (![X: $i] : (((~robust_position(X)) | ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T)))) & (robust_position(X) | (~(((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau))) & ((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))) <=> ![X: $i] : (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))))),
% 0.14/0.44 inference(quant_intro,[status(thm)],[55])).
% 0.14/0.44 tff(57,plain,
% 0.14/0.44 (![X: $i] : (robust_position(X) <=> ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T)))) <=> ![X: $i] : (robust_position(X) <=> ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T))))),
% 0.14/0.44 inference(rewrite,[status(thm)],[])).
% 0.14/0.44 tff(58,plain,
% 0.14/0.44 (^[X: $i] : rewrite((robust_position(X) <=> ![T: $i] : ((smaller_or_equal(age(X, T), tau) => (~positional_advantage(X, T))) & (greater(age(X, T), tau) => positional_advantage(X, T)))) <=> (robust_position(X) <=> ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T)))))),
% 0.14/0.44 inference(bind,[status(th)],[])).
% 0.14/0.44 tff(59,plain,
% 0.14/0.44 (![X: $i] : (robust_position(X) <=> ![T: $i] : ((smaller_or_equal(age(X, T), tau) => (~positional_advantage(X, T))) & (greater(age(X, T), tau) => positional_advantage(X, T)))) <=> ![X: $i] : (robust_position(X) <=> ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T))))),
% 0.14/0.44 inference(quant_intro,[status(thm)],[58])).
% 0.14/0.44 tff(60,axiom,(![X: $i] : (robust_position(X) <=> ![T: $i] : ((smaller_or_equal(age(X, T), tau) => (~positional_advantage(X, T))) & (greater(age(X, T), tau) => positional_advantage(X, T))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','definition_4')).
% 0.14/0.44 tff(61,plain,
% 0.14/0.44 (![X: $i] : (robust_position(X) <=> ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T))))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[60, 59])).
% 0.14/0.45 tff(62,plain,
% 0.14/0.45 (![X: $i] : (robust_position(X) <=> ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T))))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[61, 57])).
% 0.14/0.45 tff(63,plain,(
% 0.14/0.45 ![X: $i] : (((~robust_position(X)) | ![T: $i] : (((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau))) & ((~greater(age(X, T), tau)) | positional_advantage(X, T)))) & (robust_position(X) | (~(((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau))) & ((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))))),
% 0.14/0.45 inference(skolemize,[status(sab)],[62])).
% 0.14/0.45 tff(64,plain,
% 0.14/0.45 (![X: $i] : (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[63, 56])).
% 0.14/0.45 tff(65,plain,
% 0.14/0.45 (![X: $i] : (~((~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T))))))) | (~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X))))))))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[64, 54])).
% 0.14/0.45 tff(66,plain,
% 0.14/0.45 (![X: $i] : (~((~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))) | (~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T)))))))))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[65, 49])).
% 0.14/0.45 tff(67,plain,
% 0.14/0.45 ((~![X: $i] : (~((~(robust_position(X) | (~((~positional_advantage(X, tptp_fun_T_0(X))) | (~smaller_or_equal(age(X, tptp_fun_T_0(X)), tau)))) | (~((~greater(age(X, tptp_fun_T_0(X)), tau)) | positional_advantage(X, tptp_fun_T_0(X)))))) | (~((~robust_position(X)) | ![T: $i] : (~((~((~positional_advantage(X, T)) | (~smaller_or_equal(age(X, T), tau)))) | (~((~greater(age(X, T), tau)) | positional_advantage(X, T)))))))))) | (~((~(robust_position(X!4) | (~((~positional_advantage(X!4, tptp_fun_T_0(X!4))) | (~smaller_or_equal(age(X!4, tptp_fun_T_0(X!4)), tau)))) | (~((~greater(age(X!4, tptp_fun_T_0(X!4)), tau)) | positional_advantage(X!4, tptp_fun_T_0(X!4)))))) | (~((~robust_position(X!4)) | ![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T)))))))))),
% 0.14/0.45 inference(quant_inst,[status(thm)],[])).
% 0.14/0.45 tff(68,plain,
% 0.14/0.45 (~((~(robust_position(X!4) | (~((~positional_advantage(X!4, tptp_fun_T_0(X!4))) | (~smaller_or_equal(age(X!4, tptp_fun_T_0(X!4)), tau)))) | (~((~greater(age(X!4, tptp_fun_T_0(X!4)), tau)) | positional_advantage(X!4, tptp_fun_T_0(X!4)))))) | (~((~robust_position(X!4)) | ![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T))))))))),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[67, 66])).
% 0.14/0.45 tff(69,plain,
% 0.14/0.45 (((~(robust_position(X!4) | (~((~positional_advantage(X!4, tptp_fun_T_0(X!4))) | (~smaller_or_equal(age(X!4, tptp_fun_T_0(X!4)), tau)))) | (~((~greater(age(X!4, tptp_fun_T_0(X!4)), tau)) | positional_advantage(X!4, tptp_fun_T_0(X!4)))))) | (~((~robust_position(X!4)) | ![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T)))))))) | ((~robust_position(X!4)) | ![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T))))))),
% 0.14/0.45 inference(tautology,[status(thm)],[])).
% 0.14/0.45 tff(70,plain,
% 0.14/0.45 ((~robust_position(X!4)) | ![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T)))))),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[69, 68])).
% 0.14/0.45 tff(71,plain,
% 0.14/0.45 (robust_position(X!4)),
% 0.14/0.45 inference(and_elim,[status(thm)],[21])).
% 0.14/0.45 tff(72,plain,
% 0.14/0.45 ((~((~robust_position(X!4)) | ![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T))))))) | (~robust_position(X!4)) | ![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T)))))),
% 0.14/0.45 inference(tautology,[status(thm)],[])).
% 0.14/0.45 tff(73,plain,
% 0.14/0.45 ((~((~robust_position(X!4)) | ![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T))))))) | ![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T)))))),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[72, 71])).
% 0.14/0.45 tff(74,plain,
% 0.14/0.45 (![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T)))))),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[73, 70])).
% 0.14/0.45 tff(75,plain,
% 0.14/0.45 ((~![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T)))))) | (~((~((~positional_advantage(X!4, T1!2)) | (~smaller_or_equal(age(X!4, T1!2), tau)))) | (~((~greater(age(X!4, T1!2), tau)) | positional_advantage(X!4, T1!2)))))),
% 0.14/0.45 inference(quant_inst,[status(thm)],[])).
% 0.14/0.45 tff(76,plain,
% 0.14/0.45 (~((~((~positional_advantage(X!4, T1!2)) | (~smaller_or_equal(age(X!4, T1!2), tau)))) | (~((~greater(age(X!4, T1!2), tau)) | positional_advantage(X!4, T1!2))))),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[75, 74])).
% 0.14/0.45 tff(77,plain,
% 0.14/0.45 (((~((~positional_advantage(X!4, T1!2)) | (~smaller_or_equal(age(X!4, T1!2), tau)))) | (~((~greater(age(X!4, T1!2), tau)) | positional_advantage(X!4, T1!2)))) | ((~greater(age(X!4, T1!2), tau)) | positional_advantage(X!4, T1!2))),
% 0.14/0.45 inference(tautology,[status(thm)],[])).
% 0.14/0.45 tff(78,plain,
% 0.14/0.45 ((~greater(age(X!4, T1!2), tau)) | positional_advantage(X!4, T1!2)),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[77, 76])).
% 0.14/0.45 tff(79,plain,
% 0.14/0.45 (((~((~positional_advantage(X!4, T1!2)) | (~smaller_or_equal(age(X!4, T1!2), tau)))) | (~((~greater(age(X!4, T1!2), tau)) | positional_advantage(X!4, T1!2)))) | ((~positional_advantage(X!4, T1!2)) | (~smaller_or_equal(age(X!4, T1!2), tau)))),
% 0.14/0.45 inference(tautology,[status(thm)],[])).
% 0.14/0.45 tff(80,plain,
% 0.14/0.45 ((~positional_advantage(X!4, T1!2)) | (~smaller_or_equal(age(X!4, T1!2), tau))),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[79, 76])).
% 0.14/0.45 tff(81,plain,
% 0.14/0.45 (tau = sigma),
% 0.14/0.45 inference(symmetry,[status(thm)],[44])).
% 0.14/0.45 tff(82,plain,
% 0.14/0.45 (smaller_or_equal(age(X!4, T1!2), tau) <=> smaller_or_equal(age(X!4, T1!2), sigma)),
% 0.14/0.45 inference(monotonicity,[status(thm)],[81])).
% 0.14/0.45 tff(83,plain,
% 0.14/0.45 (smaller_or_equal(age(X!4, T1!2), sigma) <=> smaller_or_equal(age(X!4, T1!2), tau)),
% 0.14/0.45 inference(symmetry,[status(thm)],[82])).
% 0.14/0.45 tff(84,plain,
% 0.14/0.45 (smaller_or_equal(age(X!4, T1!2), sigma)),
% 0.14/0.45 inference(and_elim,[status(thm)],[21])).
% 0.14/0.45 tff(85,plain,
% 0.14/0.45 (smaller_or_equal(age(X!4, T1!2), tau)),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[84, 83])).
% 0.14/0.45 tff(86,plain,
% 0.14/0.45 ((~((~positional_advantage(X!4, T1!2)) | (~smaller_or_equal(age(X!4, T1!2), tau)))) | (~positional_advantage(X!4, T1!2)) | (~smaller_or_equal(age(X!4, T1!2), tau))),
% 0.14/0.45 inference(tautology,[status(thm)],[])).
% 0.14/0.45 tff(87,plain,
% 0.14/0.45 ((~((~positional_advantage(X!4, T1!2)) | (~smaller_or_equal(age(X!4, T1!2), tau)))) | (~positional_advantage(X!4, T1!2))),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[86, 85])).
% 0.14/0.45 tff(88,plain,
% 0.14/0.45 (~positional_advantage(X!4, T1!2)),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[87, 80])).
% 0.14/0.45 tff(89,plain,
% 0.14/0.45 ((~((~greater(age(X!4, T1!2), tau)) | positional_advantage(X!4, T1!2))) | (~greater(age(X!4, T1!2), tau)) | positional_advantage(X!4, T1!2)),
% 0.14/0.45 inference(tautology,[status(thm)],[])).
% 0.14/0.45 tff(90,plain,
% 0.14/0.45 (~greater(age(X!4, T1!2), tau)),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[89, 88, 78])).
% 0.14/0.45 tff(91,plain,
% 0.14/0.45 (~greater(age(X!4, T1!2), sigma)),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[90, 47])).
% 0.14/0.45 tff(92,plain,
% 0.14/0.45 ((~(greater(age(X!4, T1!2), sigma) <=> dissimilar(X!4, T0!3, T1!2))) | greater(age(X!4, T1!2), sigma) | (~dissimilar(X!4, T0!3, T1!2))),
% 0.14/0.45 inference(tautology,[status(thm)],[])).
% 0.14/0.45 tff(93,plain,
% 0.14/0.45 (~dissimilar(X!4, T0!3, T1!2)),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[92, 91, 43])).
% 0.14/0.45 tff(94,plain,
% 0.14/0.45 ((((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2))) <=> dissimilar(X!4, T0!3, T1!2)) | ((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2))) | dissimilar(X!4, T0!3, T1!2)),
% 0.14/0.45 inference(tautology,[status(thm)],[])).
% 0.14/0.45 tff(95,plain,
% 0.14/0.45 ((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2))),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[94, 93, 12])).
% 0.14/0.45 tff(96,plain,
% 0.14/0.45 ((~((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2)))) | (~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2))),
% 0.14/0.45 inference(tautology,[status(thm)],[])).
% 0.14/0.45 tff(97,plain,
% 0.14/0.45 ((~((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2)))) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2))),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[96, 23])).
% 0.14/0.45 tff(98,plain,
% 0.14/0.45 (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2)),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[97, 95])).
% 0.14/0.45 tff(99,plain,
% 0.14/0.45 (^[X: $i, T: $i] : refl((is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero))) <=> (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero))))),
% 0.14/0.45 inference(bind,[status(th)],[])).
% 0.14/0.45 tff(100,plain,
% 0.14/0.45 (![X: $i, T: $i] : (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero))) <=> ![X: $i, T: $i] : (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero)))),
% 0.14/0.45 inference(quant_intro,[status(thm)],[99])).
% 0.14/0.45 tff(101,plain,
% 0.14/0.45 (^[X: $i, T: $i] : trans(monotonicity(trans(monotonicity(rewrite((organization(X) & (age(X, T) = zero)) <=> (~((~organization(X)) | (~(age(X, T) = zero))))), ((~(organization(X) & (age(X, T) = zero))) <=> (~(~((~organization(X)) | (~(age(X, T) = zero))))))), rewrite((~(~((~organization(X)) | (~(age(X, T) = zero))))) <=> ((~organization(X)) | (~(age(X, T) = zero)))), ((~(organization(X) & (age(X, T) = zero))) <=> ((~organization(X)) | (~(age(X, T) = zero))))), (((~(organization(X) & (age(X, T) = zero))) | is_aligned(X, T)) <=> (((~organization(X)) | (~(age(X, T) = zero))) | is_aligned(X, T)))), rewrite((((~organization(X)) | (~(age(X, T) = zero))) | is_aligned(X, T)) <=> (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero)))), (((~(organization(X) & (age(X, T) = zero))) | is_aligned(X, T)) <=> (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero)))))),
% 0.14/0.45 inference(bind,[status(th)],[])).
% 0.14/0.45 tff(102,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~(organization(X) & (age(X, T) = zero))) | is_aligned(X, T)) <=> ![X: $i, T: $i] : (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero)))),
% 0.14/0.45 inference(quant_intro,[status(thm)],[101])).
% 0.14/0.45 tff(103,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~(organization(X) & (age(X, T) = zero))) | is_aligned(X, T)) <=> ![X: $i, T: $i] : ((~(organization(X) & (age(X, T) = zero))) | is_aligned(X, T))),
% 0.14/0.45 inference(rewrite,[status(thm)],[])).
% 0.14/0.45 tff(104,plain,
% 0.14/0.45 (^[X: $i, T: $i] : rewrite(((organization(X) & (age(X, T) = zero)) => is_aligned(X, T)) <=> ((~(organization(X) & (age(X, T) = zero))) | is_aligned(X, T)))),
% 0.14/0.45 inference(bind,[status(th)],[])).
% 0.14/0.45 tff(105,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((organization(X) & (age(X, T) = zero)) => is_aligned(X, T)) <=> ![X: $i, T: $i] : ((~(organization(X) & (age(X, T) = zero))) | is_aligned(X, T))),
% 0.14/0.45 inference(quant_intro,[status(thm)],[104])).
% 0.14/0.45 tff(106,axiom,(![X: $i, T: $i] : ((organization(X) & (age(X, T) = zero)) => is_aligned(X, T))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_13')).
% 0.14/0.45 tff(107,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~(organization(X) & (age(X, T) = zero))) | is_aligned(X, T))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[106, 105])).
% 0.14/0.45 tff(108,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~(organization(X) & (age(X, T) = zero))) | is_aligned(X, T))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[107, 103])).
% 0.14/0.45 tff(109,plain,(
% 0.14/0.45 ![X: $i, T: $i] : ((~(organization(X) & (age(X, T) = zero))) | is_aligned(X, T))),
% 0.14/0.45 inference(skolemize,[status(sab)],[108])).
% 0.14/0.45 tff(110,plain,
% 0.14/0.45 (![X: $i, T: $i] : (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero)))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[109, 102])).
% 0.14/0.45 tff(111,plain,
% 0.14/0.45 (![X: $i, T: $i] : (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero)))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[110, 100])).
% 0.14/0.45 tff(112,plain,
% 0.14/0.45 (((~![X: $i, T: $i] : (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero)))) | (is_aligned(X!4, T0!3) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)))) <=> ((~![X: $i, T: $i] : (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero)))) | is_aligned(X!4, T0!3) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)))),
% 0.14/0.45 inference(rewrite,[status(thm)],[])).
% 0.14/0.45 tff(113,plain,
% 0.14/0.45 ((~![X: $i, T: $i] : (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero)))) | (is_aligned(X!4, T0!3) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)))),
% 0.14/0.45 inference(quant_inst,[status(thm)],[])).
% 0.14/0.45 tff(114,plain,
% 0.14/0.45 ((~![X: $i, T: $i] : (is_aligned(X, T) | (~organization(X)) | (~(age(X, T) = zero)))) | is_aligned(X!4, T0!3) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[113, 112])).
% 0.14/0.45 tff(115,plain,
% 0.14/0.45 (is_aligned(X!4, T0!3)),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[114, 111, 23, 22])).
% 0.14/0.45 tff(116,plain,
% 0.14/0.45 ((~(is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2))) | (~is_aligned(X!4, T0!3)) | is_aligned(X!4, T1!2)),
% 0.14/0.45 inference(tautology,[status(thm)],[])).
% 0.14/0.45 tff(117,plain,
% 0.14/0.45 ((~(is_aligned(X!4, T0!3) <=> is_aligned(X!4, T1!2))) | is_aligned(X!4, T1!2)),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[116, 115])).
% 0.14/0.45 tff(118,plain,
% 0.14/0.45 (is_aligned(X!4, T1!2)),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[117, 98])).
% 0.14/0.45 tff(119,assumption,(has_immunity(X!4, T1!2)), introduced(assumption)).
% 0.14/0.45 tff(120,plain,
% 0.14/0.45 (~has_endowment(X!4)),
% 0.14/0.45 inference(and_elim,[status(thm)],[21])).
% 0.14/0.45 tff(121,plain,
% 0.14/0.45 (^[X: $i, T: $i] : refl(((~has_immunity(X, T)) | has_endowment(X) | (~organization(X))) <=> ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X))))),
% 0.14/0.45 inference(bind,[status(th)],[])).
% 0.14/0.45 tff(122,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X))) <=> ![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))),
% 0.14/0.45 inference(quant_intro,[status(thm)],[121])).
% 0.14/0.45 tff(123,plain,
% 0.14/0.45 (^[X: $i, T: $i] : trans(monotonicity(trans(monotonicity(rewrite((organization(X) & (~has_endowment(X))) <=> (~(has_endowment(X) | (~organization(X))))), ((~(organization(X) & (~has_endowment(X)))) <=> (~(~(has_endowment(X) | (~organization(X))))))), rewrite((~(~(has_endowment(X) | (~organization(X))))) <=> (has_endowment(X) | (~organization(X)))), ((~(organization(X) & (~has_endowment(X)))) <=> (has_endowment(X) | (~organization(X))))), (((~has_immunity(X, T)) | (~(organization(X) & (~has_endowment(X))))) <=> ((~has_immunity(X, T)) | (has_endowment(X) | (~organization(X)))))), rewrite(((~has_immunity(X, T)) | (has_endowment(X) | (~organization(X)))) <=> ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))), (((~has_immunity(X, T)) | (~(organization(X) & (~has_endowment(X))))) <=> ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))))),
% 0.14/0.45 inference(bind,[status(th)],[])).
% 0.14/0.45 tff(124,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~has_immunity(X, T)) | (~(organization(X) & (~has_endowment(X))))) <=> ![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))),
% 0.14/0.45 inference(quant_intro,[status(thm)],[123])).
% 0.14/0.45 tff(125,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~has_immunity(X, T)) | (~(organization(X) & (~has_endowment(X))))) <=> ![X: $i, T: $i] : ((~has_immunity(X, T)) | (~(organization(X) & (~has_endowment(X)))))),
% 0.14/0.45 inference(rewrite,[status(thm)],[])).
% 0.14/0.45 tff(126,plain,
% 0.14/0.45 (^[X: $i, T: $i] : rewrite(((organization(X) & (~has_endowment(X))) => (~has_immunity(X, T))) <=> ((~has_immunity(X, T)) | (~(organization(X) & (~has_endowment(X))))))),
% 0.14/0.45 inference(bind,[status(th)],[])).
% 0.14/0.45 tff(127,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((organization(X) & (~has_endowment(X))) => (~has_immunity(X, T))) <=> ![X: $i, T: $i] : ((~has_immunity(X, T)) | (~(organization(X) & (~has_endowment(X)))))),
% 0.14/0.45 inference(quant_intro,[status(thm)],[126])).
% 0.14/0.45 tff(128,axiom,(![X: $i, T: $i] : ((organization(X) & (~has_endowment(X))) => (~has_immunity(X, T)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_1')).
% 0.14/0.45 tff(129,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~has_immunity(X, T)) | (~(organization(X) & (~has_endowment(X)))))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[128, 127])).
% 0.14/0.45 tff(130,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~has_immunity(X, T)) | (~(organization(X) & (~has_endowment(X)))))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[129, 125])).
% 0.14/0.45 tff(131,plain,(
% 0.14/0.45 ![X: $i, T: $i] : ((~has_immunity(X, T)) | (~(organization(X) & (~has_endowment(X)))))),
% 0.14/0.45 inference(skolemize,[status(sab)],[130])).
% 0.14/0.45 tff(132,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[131, 124])).
% 0.14/0.45 tff(133,plain,
% 0.14/0.45 (![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[132, 122])).
% 0.14/0.45 tff(134,plain,
% 0.14/0.45 (((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | (has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T1!2)))) <=> ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T1!2)))),
% 0.14/0.45 inference(rewrite,[status(thm)],[])).
% 0.14/0.45 tff(135,plain,
% 0.14/0.45 (((~has_immunity(X!4, T1!2)) | has_endowment(X!4) | (~organization(X!4))) <=> (has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T1!2)))),
% 0.14/0.45 inference(rewrite,[status(thm)],[])).
% 0.14/0.45 tff(136,plain,
% 0.14/0.45 (((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | ((~has_immunity(X!4, T1!2)) | has_endowment(X!4) | (~organization(X!4)))) <=> ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | (has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T1!2))))),
% 0.14/0.45 inference(monotonicity,[status(thm)],[135])).
% 0.14/0.45 tff(137,plain,
% 0.14/0.45 (((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | ((~has_immunity(X!4, T1!2)) | has_endowment(X!4) | (~organization(X!4)))) <=> ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T1!2)))),
% 0.14/0.45 inference(transitivity,[status(thm)],[136, 134])).
% 0.14/0.45 tff(138,plain,
% 0.14/0.45 ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | ((~has_immunity(X!4, T1!2)) | has_endowment(X!4) | (~organization(X!4)))),
% 0.14/0.45 inference(quant_inst,[status(thm)],[])).
% 0.14/0.45 tff(139,plain,
% 0.14/0.45 ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T1!2))),
% 0.14/0.45 inference(modus_ponens,[status(thm)],[138, 137])).
% 0.14/0.45 tff(140,plain,
% 0.14/0.45 ($false),
% 0.14/0.45 inference(unit_resolution,[status(thm)],[139, 133, 23, 120, 119])).
% 0.14/0.45 tff(141,plain,(~has_immunity(X!4, T1!2)), inference(lemma,lemma(discharge,[]))).
% 0.14/0.46 tff(142,plain,
% 0.14/0.46 (^[X: $i, T: $i] : refl(((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high)))))))))) <=> ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high)))))))))))),
% 0.14/0.46 inference(bind,[status(th)],[])).
% 0.14/0.46 tff(143,plain,
% 0.14/0.46 (![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high)))))))))) <=> ![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))),
% 0.14/0.46 inference(quant_intro,[status(thm)],[142])).
% 0.14/0.46 tff(144,plain,
% 0.14/0.46 (^[X: $i, T: $i] : rewrite(((~organization(X)) | (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high)))))) <=> ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high)))))))))))),
% 0.14/0.46 inference(bind,[status(th)],[])).
% 0.14/0.46 tff(145,plain,
% 0.14/0.46 (![X: $i, T: $i] : ((~organization(X)) | (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high)))))) <=> ![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))),
% 0.14/0.46 inference(quant_intro,[status(thm)],[144])).
% 0.14/0.46 tff(146,plain,
% 0.14/0.46 (![X: $i, T: $i] : ((~organization(X)) | (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high)))))) <=> ![X: $i, T: $i] : ((~organization(X)) | (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high))))))),
% 0.14/0.46 inference(rewrite,[status(thm)],[])).
% 0.14/0.46 tff(147,plain,
% 0.14/0.46 (^[X: $i, T: $i] : trans(monotonicity(rewrite(((has_immunity(X, T) => (hazard_of_mortality(X, T) = very_low)) & ((~has_immunity(X, T)) => (((((is_aligned(X, T) & positional_advantage(X, T)) => (hazard_of_mortality(X, T) = low)) & (((~is_aligned(X, T)) & positional_advantage(X, T)) => (hazard_of_mortality(X, T) = mod1))) & ((is_aligned(X, T) & (~positional_advantage(X, T))) => (hazard_of_mortality(X, T) = mod2))) & (((~is_aligned(X, T)) & (~positional_advantage(X, T))) => (hazard_of_mortality(X, T) = high))))) <=> (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high)))))), ((organization(X) => ((has_immunity(X, T) => (hazard_of_mortality(X, T) = very_low)) & ((~has_immunity(X, T)) => (((((is_aligned(X, T) & positional_advantage(X, T)) => (hazard_of_mortality(X, T) = low)) & (((~is_aligned(X, T)) & positional_advantage(X, T)) => (hazard_of_mortality(X, T) = mod1))) & ((is_aligned(X, T) & (~positional_advantage(X, T))) => (hazard_of_mortality(X, T) = mod2))) & (((~is_aligned(X, T)) & (~positional_advantage(X, T))) => (hazard_of_mortality(X, T) = high)))))) <=> (organization(X) => (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high)))))))), rewrite((organization(X) => (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high)))))) <=> ((~organization(X)) | (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high))))))), ((organization(X) => ((has_immunity(X, T) => (hazard_of_mortality(X, T) = very_low)) & ((~has_immunity(X, T)) => (((((is_aligned(X, T) & positional_advantage(X, T)) => (hazard_of_mortality(X, T) = low)) & (((~is_aligned(X, T)) & positional_advantage(X, T)) => (hazard_of_mortality(X, T) = mod1))) & ((is_aligned(X, T) & (~positional_advantage(X, T))) => (hazard_of_mortality(X, T) = mod2))) & (((~is_aligned(X, T)) & (~positional_advantage(X, T))) => (hazard_of_mortality(X, T) = high)))))) <=> ((~organization(X)) | (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high))))))))),
% 0.23/0.46 inference(bind,[status(th)],[])).
% 0.23/0.46 tff(148,plain,
% 0.23/0.46 (![X: $i, T: $i] : (organization(X) => ((has_immunity(X, T) => (hazard_of_mortality(X, T) = very_low)) & ((~has_immunity(X, T)) => (((((is_aligned(X, T) & positional_advantage(X, T)) => (hazard_of_mortality(X, T) = low)) & (((~is_aligned(X, T)) & positional_advantage(X, T)) => (hazard_of_mortality(X, T) = mod1))) & ((is_aligned(X, T) & (~positional_advantage(X, T))) => (hazard_of_mortality(X, T) = mod2))) & (((~is_aligned(X, T)) & (~positional_advantage(X, T))) => (hazard_of_mortality(X, T) = high)))))) <=> ![X: $i, T: $i] : ((~organization(X)) | (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high))))))),
% 0.23/0.46 inference(quant_intro,[status(thm)],[147])).
% 0.23/0.46 tff(149,axiom,(![X: $i, T: $i] : (organization(X) => ((has_immunity(X, T) => (hazard_of_mortality(X, T) = very_low)) & ((~has_immunity(X, T)) => (((((is_aligned(X, T) & positional_advantage(X, T)) => (hazard_of_mortality(X, T) = low)) & (((~is_aligned(X, T)) & positional_advantage(X, T)) => (hazard_of_mortality(X, T) = mod1))) & ((is_aligned(X, T) & (~positional_advantage(X, T))) => (hazard_of_mortality(X, T) = mod2))) & (((~is_aligned(X, T)) & (~positional_advantage(X, T))) => (hazard_of_mortality(X, T) = high))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_17')).
% 0.23/0.46 tff(150,plain,
% 0.23/0.46 (![X: $i, T: $i] : ((~organization(X)) | (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high))))))),
% 0.23/0.46 inference(modus_ponens,[status(thm)],[149, 148])).
% 0.23/0.46 tff(151,plain,
% 0.23/0.46 (![X: $i, T: $i] : ((~organization(X)) | (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high))))))),
% 0.23/0.46 inference(modus_ponens,[status(thm)],[150, 146])).
% 0.23/0.46 tff(152,plain,(
% 0.23/0.46 ![X: $i, T: $i] : ((~organization(X)) | (((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low)) & (has_immunity(X, T) | (((~(is_aligned(X, T) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = low)) & ((~((~is_aligned(X, T)) & positional_advantage(X, T))) | (hazard_of_mortality(X, T) = mod1)) & ((~(is_aligned(X, T) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = mod2)) & ((~((~is_aligned(X, T)) & (~positional_advantage(X, T)))) | (hazard_of_mortality(X, T) = high))))))),
% 0.23/0.46 inference(skolemize,[status(sab)],[151])).
% 0.23/0.46 tff(153,plain,
% 0.23/0.46 (![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))),
% 0.23/0.46 inference(modus_ponens,[status(thm)],[152, 145])).
% 0.23/0.46 tff(154,plain,
% 0.23/0.46 (![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))),
% 0.23/0.46 inference(modus_ponens,[status(thm)],[153, 143])).
% 0.23/0.46 tff(155,plain,
% 0.23/0.46 (((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))))))))) <=> ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | (~organization(X!4)) | (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))))))))),
% 0.23/0.46 inference(rewrite,[status(thm)],[])).
% 0.23/0.46 tff(156,plain,
% 0.23/0.46 (((~organization(X!4)) | (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(positional_advantage(X!4, T1!2) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high)))))))))) <=> ((~organization(X!4)) | (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))))))))),
% 0.23/0.46 inference(rewrite,[status(thm)],[])).
% 0.23/0.46 tff(157,plain,
% 0.23/0.46 (((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(positional_advantage(X!4, T1!2) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))))))))) <=> ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high)))))))))))),
% 0.23/0.46 inference(monotonicity,[status(thm)],[156])).
% 0.23/0.46 tff(158,plain,
% 0.23/0.46 (((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(positional_advantage(X!4, T1!2) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))))))))) <=> ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | (~organization(X!4)) | (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))))))))),
% 0.23/0.47 inference(transitivity,[status(thm)],[157, 155])).
% 0.23/0.47 tff(159,plain,
% 0.23/0.47 ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(positional_advantage(X!4, T1!2) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))))))))),
% 0.23/0.47 inference(quant_inst,[status(thm)],[])).
% 0.23/0.47 tff(160,plain,
% 0.23/0.47 ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | (~organization(X!4)) | (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high)))))))))),
% 0.23/0.47 inference(modus_ponens,[status(thm)],[159, 158])).
% 0.23/0.47 tff(161,plain,
% 0.23/0.47 (~((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))))))),
% 0.23/0.47 inference(unit_resolution,[status(thm)],[160, 154, 23])).
% 0.23/0.47 tff(162,plain,
% 0.23/0.47 (((~((~has_immunity(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = very_low))) | (~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high)))))))) | (has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))))),
% 0.23/0.47 inference(tautology,[status(thm)],[])).
% 0.23/0.47 tff(163,plain,
% 0.23/0.47 (has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high)))))),
% 0.23/0.47 inference(unit_resolution,[status(thm)],[162, 161])).
% 0.23/0.47 tff(164,plain,
% 0.23/0.47 ((~(has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))))) | has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high)))))),
% 0.23/0.47 inference(tautology,[status(thm)],[])).
% 0.23/0.47 tff(165,plain,
% 0.23/0.47 (has_immunity(X!4, T1!2) | (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high)))))),
% 0.23/0.47 inference(unit_resolution,[status(thm)],[164, 163])).
% 0.23/0.47 tff(166,plain,
% 0.23/0.47 (~((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high))))),
% 0.23/0.47 inference(unit_resolution,[status(thm)],[165, 141])).
% 0.23/0.47 tff(167,plain,
% 0.23/0.47 (((~((~positional_advantage(X!4, T1!2)) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = low))) | (~((~positional_advantage(X!4, T1!2)) | is_aligned(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = mod1))) | (~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~(is_aligned(X!4, T1!2) | positional_advantage(X!4, T1!2) | (hazard_of_mortality(X!4, T1!2) = high)))) | (positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))),
% 0.23/0.47 inference(tautology,[status(thm)],[])).
% 0.23/0.47 tff(168,plain,
% 0.23/0.47 (positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2)),
% 0.23/0.47 inference(unit_resolution,[status(thm)],[167, 166])).
% 0.23/0.47 tff(169,plain,
% 0.23/0.47 ((~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2)),
% 0.23/0.47 inference(tautology,[status(thm)],[])).
% 0.23/0.47 tff(170,plain,
% 0.23/0.47 ((~(positional_advantage(X!4, T1!2) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2))) | (~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2)),
% 0.23/0.47 inference(unit_resolution,[status(thm)],[169, 88])).
% 0.23/0.47 tff(171,plain,
% 0.23/0.47 ((~is_aligned(X!4, T1!2)) | (hazard_of_mortality(X!4, T1!2) = mod2)),
% 0.23/0.47 inference(unit_resolution,[status(thm)],[170, 168])).
% 0.23/0.47 tff(172,plain,
% 0.23/0.47 (hazard_of_mortality(X!4, T1!2) = mod2),
% 0.23/0.47 inference(unit_resolution,[status(thm)],[171, 118])).
% 0.23/0.47 tff(173,plain,
% 0.23/0.47 ((~![X: $i, T0: $i, T: $i] : (~(((~organization(X)) | (is_aligned(X, T0) <=> is_aligned(X, T))) <=> dissimilar(X, T0, T)))) | (~(((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1))) <=> dissimilar(X!4, T0!3, T2!1)))),
% 0.23/0.47 inference(quant_inst,[status(thm)],[])).
% 0.23/0.47 tff(174,plain,
% 0.23/0.47 (~(((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1))) <=> dissimilar(X!4, T0!3, T2!1))),
% 0.23/0.47 inference(unit_resolution,[status(thm)],[173, 10])).
% 0.23/0.47 tff(175,plain,
% 0.23/0.47 (((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | ((~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1)))) <=> ((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1)))),
% 0.23/0.47 inference(rewrite,[status(thm)],[])).
% 0.23/0.47 tff(176,plain,
% 0.23/0.47 (((greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1)) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero))) <=> ((~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1)))),
% 0.23/0.47 inference(rewrite,[status(thm)],[])).
% 0.23/0.47 tff(177,plain,
% 0.23/0.47 (((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | ((greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1)) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)))) <=> ((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | ((~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1))))),
% 0.23/0.47 inference(monotonicity,[status(thm)],[176])).
% 0.23/0.47 tff(178,plain,
% 0.23/0.47 (((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | ((greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1)) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)))) <=> ((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1)))),
% 0.23/0.48 inference(transitivity,[status(thm)],[177, 175])).
% 0.23/0.48 tff(179,plain,
% 0.23/0.48 ((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | ((greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1)) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)))),
% 0.23/0.48 inference(quant_inst,[status(thm)],[])).
% 0.23/0.48 tff(180,plain,
% 0.23/0.48 ((~![X: $i, T0: $i, T: $i] : ((greater(age(X, T), sigma) <=> dissimilar(X, T0, T)) | (~organization(X)) | (~(age(X, T0) = zero)))) | (~organization(X!4)) | (~(age(X!4, T0!3) = zero)) | (greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1))),
% 0.23/0.48 inference(modus_ponens,[status(thm)],[179, 178])).
% 0.23/0.48 tff(181,plain,
% 0.23/0.48 (greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1)),
% 0.23/0.48 inference(unit_resolution,[status(thm)],[180, 36, 23, 22])).
% 0.23/0.48 tff(182,plain,
% 0.23/0.48 (greater(age(X!4, T2!1), sigma)),
% 0.23/0.48 inference(and_elim,[status(thm)],[21])).
% 0.23/0.48 tff(183,plain,
% 0.23/0.48 ((~(greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1))) | (~greater(age(X!4, T2!1), sigma)) | dissimilar(X!4, T0!3, T2!1)),
% 0.23/0.48 inference(tautology,[status(thm)],[])).
% 0.23/0.48 tff(184,plain,
% 0.23/0.48 ((~(greater(age(X!4, T2!1), sigma) <=> dissimilar(X!4, T0!3, T2!1))) | dissimilar(X!4, T0!3, T2!1)),
% 0.23/0.48 inference(unit_resolution,[status(thm)],[183, 182])).
% 0.23/0.48 tff(185,plain,
% 0.23/0.48 (dissimilar(X!4, T0!3, T2!1)),
% 0.23/0.48 inference(unit_resolution,[status(thm)],[184, 181])).
% 0.23/0.48 tff(186,plain,
% 0.23/0.48 ((((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1))) <=> dissimilar(X!4, T0!3, T2!1)) | (~((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1)))) | (~dissimilar(X!4, T0!3, T2!1))),
% 0.23/0.48 inference(tautology,[status(thm)],[])).
% 0.23/0.48 tff(187,plain,
% 0.23/0.48 ((((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1))) <=> dissimilar(X!4, T0!3, T2!1)) | (~((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1))))),
% 0.23/0.48 inference(unit_resolution,[status(thm)],[186, 185])).
% 0.23/0.48 tff(188,plain,
% 0.23/0.48 (~((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1)))),
% 0.23/0.48 inference(unit_resolution,[status(thm)],[187, 174])).
% 0.23/0.48 tff(189,plain,
% 0.23/0.48 (((~organization(X!4)) | (is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1))) | (~(is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1)))),
% 0.23/0.48 inference(tautology,[status(thm)],[])).
% 0.23/0.48 tff(190,plain,
% 0.23/0.48 (~(is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1))),
% 0.23/0.48 inference(unit_resolution,[status(thm)],[189, 188])).
% 0.23/0.48 tff(191,plain,
% 0.23/0.48 ((is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1)) | (~is_aligned(X!4, T0!3)) | (~is_aligned(X!4, T2!1))),
% 0.23/0.48 inference(tautology,[status(thm)],[])).
% 0.23/0.48 tff(192,plain,
% 0.23/0.48 ((is_aligned(X!4, T0!3) <=> is_aligned(X!4, T2!1)) | (~is_aligned(X!4, T2!1))),
% 0.23/0.48 inference(unit_resolution,[status(thm)],[191, 115])).
% 0.23/0.48 tff(193,plain,
% 0.23/0.48 (~is_aligned(X!4, T2!1)),
% 0.23/0.48 inference(unit_resolution,[status(thm)],[192, 190])).
% 0.23/0.48 tff(194,assumption,(has_immunity(X!4, T2!1)), introduced(assumption)).
% 0.23/0.48 tff(195,plain,
% 0.23/0.48 (((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | (has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T2!1)))) <=> ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T2!1)))),
% 0.23/0.48 inference(rewrite,[status(thm)],[])).
% 0.23/0.48 tff(196,plain,
% 0.23/0.48 (((~has_immunity(X!4, T2!1)) | has_endowment(X!4) | (~organization(X!4))) <=> (has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T2!1)))),
% 0.23/0.48 inference(rewrite,[status(thm)],[])).
% 0.23/0.48 tff(197,plain,
% 0.23/0.48 (((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | ((~has_immunity(X!4, T2!1)) | has_endowment(X!4) | (~organization(X!4)))) <=> ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | (has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T2!1))))),
% 0.23/0.48 inference(monotonicity,[status(thm)],[196])).
% 0.23/0.48 tff(198,plain,
% 0.23/0.48 (((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | ((~has_immunity(X!4, T2!1)) | has_endowment(X!4) | (~organization(X!4)))) <=> ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T2!1)))),
% 0.23/0.48 inference(transitivity,[status(thm)],[197, 195])).
% 0.23/0.48 tff(199,plain,
% 0.23/0.48 ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | ((~has_immunity(X!4, T2!1)) | has_endowment(X!4) | (~organization(X!4)))),
% 0.23/0.48 inference(quant_inst,[status(thm)],[])).
% 0.23/0.48 tff(200,plain,
% 0.23/0.48 ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T2!1))),
% 0.23/0.48 inference(modus_ponens,[status(thm)],[199, 198])).
% 0.23/0.48 tff(201,plain,
% 0.23/0.48 ($false),
% 0.23/0.48 inference(unit_resolution,[status(thm)],[200, 133, 23, 120, 194])).
% 0.23/0.48 tff(202,plain,(~has_immunity(X!4, T2!1)), inference(lemma,lemma(discharge,[]))).
% 0.23/0.48 tff(203,plain,
% 0.23/0.48 (((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))))))))) <=> ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | (~organization(X!4)) | (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))))))))),
% 0.23/0.48 inference(rewrite,[status(thm)],[])).
% 0.23/0.48 tff(204,plain,
% 0.23/0.48 (((~organization(X!4)) | (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(positional_advantage(X!4, T2!1) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high)))))))))) <=> ((~organization(X!4)) | (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))))))))),
% 0.23/0.48 inference(rewrite,[status(thm)],[])).
% 0.23/0.48 tff(205,plain,
% 0.23/0.48 (((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(positional_advantage(X!4, T2!1) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))))))))) <=> ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high)))))))))))),
% 0.23/0.48 inference(monotonicity,[status(thm)],[204])).
% 0.23/0.48 tff(206,plain,
% 0.23/0.48 (((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(positional_advantage(X!4, T2!1) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))))))))) <=> ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | (~organization(X!4)) | (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))))))))),
% 0.23/0.48 inference(transitivity,[status(thm)],[205, 203])).
% 0.23/0.48 tff(207,plain,
% 0.23/0.48 ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(positional_advantage(X!4, T2!1) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))))))))),
% 0.23/0.48 inference(quant_inst,[status(thm)],[])).
% 0.23/0.48 tff(208,plain,
% 0.23/0.48 ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | (~organization(X!4)) | (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high)))))))))),
% 0.23/0.48 inference(modus_ponens,[status(thm)],[207, 206])).
% 0.23/0.48 tff(209,plain,
% 0.23/0.48 (~((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))))))),
% 0.23/0.48 inference(unit_resolution,[status(thm)],[208, 154, 23])).
% 0.23/0.48 tff(210,plain,
% 0.23/0.48 (((~((~has_immunity(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = very_low))) | (~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high)))))))) | (has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))))),
% 0.23/0.49 inference(tautology,[status(thm)],[])).
% 0.23/0.49 tff(211,plain,
% 0.23/0.49 (has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high)))))),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[210, 209])).
% 0.23/0.49 tff(212,plain,
% 0.23/0.49 ((~(has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))))) | has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high)))))),
% 0.23/0.49 inference(tautology,[status(thm)],[])).
% 0.23/0.49 tff(213,plain,
% 0.23/0.49 (has_immunity(X!4, T2!1) | (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high)))))),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[212, 211])).
% 0.23/0.49 tff(214,plain,
% 0.23/0.49 (~((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high))))),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[213, 202])).
% 0.23/0.49 tff(215,plain,
% 0.23/0.49 (((~((~positional_advantage(X!4, T2!1)) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = low))) | (~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~(positional_advantage(X!4, T2!1) | (~is_aligned(X!4, T2!1)) | (hazard_of_mortality(X!4, T2!1) = mod2))) | (~(is_aligned(X!4, T2!1) | positional_advantage(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = high)))) | ((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))),
% 0.23/0.49 inference(tautology,[status(thm)],[])).
% 0.23/0.49 tff(216,plain,
% 0.23/0.49 ((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1)),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[215, 214])).
% 0.23/0.49 tff(217,plain,
% 0.23/0.49 ((~![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T)))))) | (~((~((~positional_advantage(X!4, T2!1)) | (~smaller_or_equal(age(X!4, T2!1), tau)))) | (~((~greater(age(X!4, T2!1), tau)) | positional_advantage(X!4, T2!1)))))),
% 0.23/0.49 inference(quant_inst,[status(thm)],[])).
% 0.23/0.49 tff(218,plain,
% 0.23/0.49 (~((~((~positional_advantage(X!4, T2!1)) | (~smaller_or_equal(age(X!4, T2!1), tau)))) | (~((~greater(age(X!4, T2!1), tau)) | positional_advantage(X!4, T2!1))))),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[217, 74])).
% 0.23/0.49 tff(219,plain,
% 0.23/0.49 (((~((~positional_advantage(X!4, T2!1)) | (~smaller_or_equal(age(X!4, T2!1), tau)))) | (~((~greater(age(X!4, T2!1), tau)) | positional_advantage(X!4, T2!1)))) | ((~greater(age(X!4, T2!1), tau)) | positional_advantage(X!4, T2!1))),
% 0.23/0.49 inference(tautology,[status(thm)],[])).
% 0.23/0.49 tff(220,plain,
% 0.23/0.49 ((~greater(age(X!4, T2!1), tau)) | positional_advantage(X!4, T2!1)),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[219, 218])).
% 0.23/0.49 tff(221,plain,
% 0.23/0.49 (greater(age(X!4, T2!1), tau) <=> greater(age(X!4, T2!1), sigma)),
% 0.23/0.49 inference(monotonicity,[status(thm)],[81])).
% 0.23/0.49 tff(222,plain,
% 0.23/0.49 (greater(age(X!4, T2!1), sigma) <=> greater(age(X!4, T2!1), tau)),
% 0.23/0.49 inference(symmetry,[status(thm)],[221])).
% 0.23/0.49 tff(223,plain,
% 0.23/0.49 (greater(age(X!4, T2!1), tau)),
% 0.23/0.49 inference(modus_ponens,[status(thm)],[182, 222])).
% 0.23/0.49 tff(224,plain,
% 0.23/0.49 ((~((~greater(age(X!4, T2!1), tau)) | positional_advantage(X!4, T2!1))) | (~greater(age(X!4, T2!1), tau)) | positional_advantage(X!4, T2!1)),
% 0.23/0.49 inference(tautology,[status(thm)],[])).
% 0.23/0.49 tff(225,plain,
% 0.23/0.49 ((~((~greater(age(X!4, T2!1), tau)) | positional_advantage(X!4, T2!1))) | positional_advantage(X!4, T2!1)),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[224, 223])).
% 0.23/0.49 tff(226,plain,
% 0.23/0.49 (positional_advantage(X!4, T2!1)),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[225, 220])).
% 0.23/0.49 tff(227,plain,
% 0.23/0.49 ((~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | (~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1)),
% 0.23/0.49 inference(tautology,[status(thm)],[])).
% 0.23/0.49 tff(228,plain,
% 0.23/0.49 ((~((~positional_advantage(X!4, T2!1)) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1))) | is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1)),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[227, 226])).
% 0.23/0.49 tff(229,plain,
% 0.23/0.49 (is_aligned(X!4, T2!1) | (hazard_of_mortality(X!4, T2!1) = mod1)),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[228, 216])).
% 0.23/0.49 tff(230,plain,
% 0.23/0.49 (hazard_of_mortality(X!4, T2!1) = mod1),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[229, 193])).
% 0.23/0.49 tff(231,plain,
% 0.23/0.49 (smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2)) <=> smaller(mod1, mod2)),
% 0.23/0.49 inference(monotonicity,[status(thm)],[230, 172])).
% 0.23/0.49 tff(232,plain,
% 0.23/0.49 (smaller(mod1, mod2) <=> smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2))),
% 0.23/0.49 inference(symmetry,[status(thm)],[231])).
% 0.23/0.49 tff(233,plain,
% 0.23/0.49 (^[X: $i, Y: $i] : refl((smaller(X, Y) <=> greater(Y, X)) <=> (smaller(X, Y) <=> greater(Y, X)))),
% 0.23/0.49 inference(bind,[status(th)],[])).
% 0.23/0.49 tff(234,plain,
% 0.23/0.49 (![X: $i, Y: $i] : (smaller(X, Y) <=> greater(Y, X)) <=> ![X: $i, Y: $i] : (smaller(X, Y) <=> greater(Y, X))),
% 0.23/0.49 inference(quant_intro,[status(thm)],[233])).
% 0.23/0.49 tff(235,plain,
% 0.23/0.49 (![X: $i, Y: $i] : (smaller(X, Y) <=> greater(Y, X)) <=> ![X: $i, Y: $i] : (smaller(X, Y) <=> greater(Y, X))),
% 0.23/0.49 inference(rewrite,[status(thm)],[])).
% 0.23/0.49 tff(236,axiom,(![X: $i, Y: $i] : (smaller(X, Y) <=> greater(Y, X))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax','definition_smaller')).
% 0.23/0.49 tff(237,plain,
% 0.23/0.49 (![X: $i, Y: $i] : (smaller(X, Y) <=> greater(Y, X))),
% 0.23/0.49 inference(modus_ponens,[status(thm)],[236, 235])).
% 0.23/0.49 tff(238,plain,(
% 0.23/0.49 ![X: $i, Y: $i] : (smaller(X, Y) <=> greater(Y, X))),
% 0.23/0.49 inference(skolemize,[status(sab)],[237])).
% 0.23/0.49 tff(239,plain,
% 0.23/0.49 (![X: $i, Y: $i] : (smaller(X, Y) <=> greater(Y, X))),
% 0.23/0.49 inference(modus_ponens,[status(thm)],[238, 234])).
% 0.23/0.49 tff(240,plain,
% 0.23/0.49 ((~![X: $i, Y: $i] : (smaller(X, Y) <=> greater(Y, X))) | (smaller(mod1, mod2) <=> greater(mod2, mod1))),
% 0.23/0.49 inference(quant_inst,[status(thm)],[])).
% 0.23/0.49 tff(241,plain,
% 0.23/0.49 (smaller(mod1, mod2) <=> greater(mod2, mod1)),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[240, 239])).
% 0.23/0.49 tff(242,plain,
% 0.23/0.49 (greater(mod2, mod1) <=> greater(mod2, mod1)),
% 0.23/0.49 inference(rewrite,[status(thm)],[])).
% 0.23/0.49 tff(243,axiom,(greater(mod2, mod1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_19')).
% 0.23/0.49 tff(244,plain,
% 0.23/0.49 (greater(mod2, mod1)),
% 0.23/0.49 inference(modus_ponens,[status(thm)],[243, 242])).
% 0.23/0.49 tff(245,plain,
% 0.23/0.49 ((~(smaller(mod1, mod2) <=> greater(mod2, mod1))) | smaller(mod1, mod2) | (~greater(mod2, mod1))),
% 0.23/0.49 inference(tautology,[status(thm)],[])).
% 0.23/0.49 tff(246,plain,
% 0.23/0.49 ((~(smaller(mod1, mod2) <=> greater(mod2, mod1))) | smaller(mod1, mod2)),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[245, 244])).
% 0.23/0.49 tff(247,plain,
% 0.23/0.49 (smaller(mod1, mod2)),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[246, 241])).
% 0.23/0.49 tff(248,plain,
% 0.23/0.49 (smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2))),
% 0.23/0.49 inference(modus_ponens,[status(thm)],[247, 232])).
% 0.23/0.49 tff(249,assumption,(has_immunity(X!4, T0!3)), introduced(assumption)).
% 0.23/0.49 tff(250,plain,
% 0.23/0.49 (((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | (has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T0!3)))) <=> ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T0!3)))),
% 0.23/0.49 inference(rewrite,[status(thm)],[])).
% 0.23/0.49 tff(251,plain,
% 0.23/0.49 (((~has_immunity(X!4, T0!3)) | has_endowment(X!4) | (~organization(X!4))) <=> (has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T0!3)))),
% 0.23/0.49 inference(rewrite,[status(thm)],[])).
% 0.23/0.49 tff(252,plain,
% 0.23/0.49 (((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | ((~has_immunity(X!4, T0!3)) | has_endowment(X!4) | (~organization(X!4)))) <=> ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | (has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T0!3))))),
% 0.23/0.49 inference(monotonicity,[status(thm)],[251])).
% 0.23/0.49 tff(253,plain,
% 0.23/0.49 (((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | ((~has_immunity(X!4, T0!3)) | has_endowment(X!4) | (~organization(X!4)))) <=> ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T0!3)))),
% 0.23/0.49 inference(transitivity,[status(thm)],[252, 250])).
% 0.23/0.49 tff(254,plain,
% 0.23/0.49 ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | ((~has_immunity(X!4, T0!3)) | has_endowment(X!4) | (~organization(X!4)))),
% 0.23/0.49 inference(quant_inst,[status(thm)],[])).
% 0.23/0.49 tff(255,plain,
% 0.23/0.49 ((~![X: $i, T: $i] : ((~has_immunity(X, T)) | has_endowment(X) | (~organization(X)))) | has_endowment(X!4) | (~organization(X!4)) | (~has_immunity(X!4, T0!3))),
% 0.23/0.49 inference(modus_ponens,[status(thm)],[254, 253])).
% 0.23/0.49 tff(256,plain,
% 0.23/0.49 ($false),
% 0.23/0.49 inference(unit_resolution,[status(thm)],[255, 133, 23, 120, 249])).
% 0.23/0.49 tff(257,plain,(~has_immunity(X!4, T0!3)), inference(lemma,lemma(discharge,[]))).
% 0.23/0.49 tff(258,plain,
% 0.23/0.49 (((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))))))))) <=> ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | (~organization(X!4)) | (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))))))))),
% 0.23/0.50 inference(rewrite,[status(thm)],[])).
% 0.23/0.50 tff(259,plain,
% 0.23/0.50 (((~organization(X!4)) | (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(positional_advantage(X!4, T0!3) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high)))))))))) <=> ((~organization(X!4)) | (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))))))))),
% 0.23/0.50 inference(rewrite,[status(thm)],[])).
% 0.23/0.50 tff(260,plain,
% 0.23/0.50 (((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(positional_advantage(X!4, T0!3) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))))))))) <=> ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high)))))))))))),
% 0.23/0.50 inference(monotonicity,[status(thm)],[259])).
% 0.23/0.50 tff(261,plain,
% 0.23/0.50 (((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(positional_advantage(X!4, T0!3) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))))))))) <=> ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | (~organization(X!4)) | (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))))))))),
% 0.23/0.50 inference(transitivity,[status(thm)],[260, 258])).
% 0.23/0.50 tff(262,plain,
% 0.23/0.50 ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | ((~organization(X!4)) | (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(positional_advantage(X!4, T0!3) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))))))))),
% 0.23/0.50 inference(quant_inst,[status(thm)],[])).
% 0.23/0.50 tff(263,plain,
% 0.23/0.50 ((~![X: $i, T: $i] : ((~organization(X)) | (~((~((~has_immunity(X, T)) | (hazard_of_mortality(X, T) = very_low))) | (~(has_immunity(X, T) | (~((~((~positional_advantage(X, T)) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = low))) | (~((~positional_advantage(X, T)) | is_aligned(X, T) | (hazard_of_mortality(X, T) = mod1))) | (~(positional_advantage(X, T) | (~is_aligned(X, T)) | (hazard_of_mortality(X, T) = mod2))) | (~(positional_advantage(X, T) | is_aligned(X, T) | (hazard_of_mortality(X, T) = high))))))))))) | (~organization(X!4)) | (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high)))))))))),
% 0.23/0.50 inference(modus_ponens,[status(thm)],[262, 261])).
% 0.23/0.50 tff(264,plain,
% 0.23/0.50 (~((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))))))),
% 0.23/0.50 inference(unit_resolution,[status(thm)],[263, 154, 23])).
% 0.23/0.50 tff(265,plain,
% 0.23/0.50 (((~((~has_immunity(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = very_low))) | (~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high)))))))) | (has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))))),
% 0.23/0.50 inference(tautology,[status(thm)],[])).
% 0.23/0.50 tff(266,plain,
% 0.23/0.50 (has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high)))))),
% 0.23/0.50 inference(unit_resolution,[status(thm)],[265, 264])).
% 0.23/0.50 tff(267,plain,
% 0.23/0.50 ((~(has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))))) | has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high)))))),
% 0.23/0.50 inference(tautology,[status(thm)],[])).
% 0.23/0.50 tff(268,plain,
% 0.23/0.50 (has_immunity(X!4, T0!3) | (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high)))))),
% 0.23/0.50 inference(unit_resolution,[status(thm)],[267, 266])).
% 0.23/0.50 tff(269,plain,
% 0.23/0.50 (~((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high))))),
% 0.23/0.50 inference(unit_resolution,[status(thm)],[268, 257])).
% 0.23/0.50 tff(270,plain,
% 0.23/0.50 (((~((~positional_advantage(X!4, T0!3)) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = low))) | (~((~positional_advantage(X!4, T0!3)) | is_aligned(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod1))) | (~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (~(is_aligned(X!4, T0!3) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = high)))) | (positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))),
% 0.23/0.50 inference(tautology,[status(thm)],[])).
% 0.23/0.50 tff(271,plain,
% 0.23/0.50 (positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2)),
% 0.23/0.50 inference(unit_resolution,[status(thm)],[270, 269])).
% 0.23/0.50 tff(272,plain,
% 0.23/0.50 ((~![T: $i] : (~((~((~positional_advantage(X!4, T)) | (~smaller_or_equal(age(X!4, T), tau)))) | (~((~greater(age(X!4, T), tau)) | positional_advantage(X!4, T)))))) | (~((~((~positional_advantage(X!4, T0!3)) | (~smaller_or_equal(age(X!4, T0!3), tau)))) | (~((~greater(age(X!4, T0!3), tau)) | positional_advantage(X!4, T0!3)))))),
% 0.23/0.50 inference(quant_inst,[status(thm)],[])).
% 0.23/0.50 tff(273,plain,
% 0.23/0.50 (~((~((~positional_advantage(X!4, T0!3)) | (~smaller_or_equal(age(X!4, T0!3), tau)))) | (~((~greater(age(X!4, T0!3), tau)) | positional_advantage(X!4, T0!3))))),
% 0.23/0.50 inference(unit_resolution,[status(thm)],[272, 74])).
% 0.23/0.50 tff(274,plain,
% 0.23/0.50 (((~((~positional_advantage(X!4, T0!3)) | (~smaller_or_equal(age(X!4, T0!3), tau)))) | (~((~greater(age(X!4, T0!3), tau)) | positional_advantage(X!4, T0!3)))) | ((~positional_advantage(X!4, T0!3)) | (~smaller_or_equal(age(X!4, T0!3), tau)))),
% 0.23/0.50 inference(tautology,[status(thm)],[])).
% 0.23/0.50 tff(275,plain,
% 0.23/0.50 ((~positional_advantage(X!4, T0!3)) | (~smaller_or_equal(age(X!4, T0!3), tau))),
% 0.23/0.50 inference(unit_resolution,[status(thm)],[274, 273])).
% 0.23/0.50 tff(276,plain,
% 0.23/0.50 (smaller_or_equal(age(X!4, T0!3), tau) <=> smaller_or_equal(zero, tau)),
% 0.23/0.50 inference(monotonicity,[status(thm)],[22])).
% 0.23/0.50 tff(277,plain,
% 0.23/0.50 (smaller_or_equal(zero, tau) <=> smaller_or_equal(age(X!4, T0!3), tau)),
% 0.23/0.50 inference(symmetry,[status(thm)],[276])).
% 0.23/0.50 tff(278,plain,
% 0.23/0.50 (^[X: $i, Y: $i] : refl((smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y))) <=> (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y))))),
% 0.23/0.50 inference(bind,[status(th)],[])).
% 0.23/0.50 tff(279,plain,
% 0.23/0.50 (![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y))) <=> ![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y)))),
% 0.23/0.51 inference(quant_intro,[status(thm)],[278])).
% 0.23/0.51 tff(280,plain,
% 0.23/0.51 (![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y))) <=> ![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y)))),
% 0.23/0.51 inference(rewrite,[status(thm)],[])).
% 0.23/0.51 tff(281,plain,
% 0.23/0.51 (^[X: $i, Y: $i] : rewrite((smaller_or_equal(X, Y) <=> (smaller(X, Y) | (X = Y))) <=> (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y))))),
% 0.23/0.51 inference(bind,[status(th)],[])).
% 0.23/0.51 tff(282,plain,
% 0.23/0.51 (![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> (smaller(X, Y) | (X = Y))) <=> ![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y)))),
% 0.23/0.51 inference(quant_intro,[status(thm)],[281])).
% 0.23/0.51 tff(283,axiom,(![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> (smaller(X, Y) | (X = Y)))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax','definition_smaller_or_equal')).
% 0.23/0.51 tff(284,plain,
% 0.23/0.51 (![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y)))),
% 0.23/0.51 inference(modus_ponens,[status(thm)],[283, 282])).
% 0.23/0.51 tff(285,plain,
% 0.23/0.51 (![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y)))),
% 0.23/0.51 inference(modus_ponens,[status(thm)],[284, 280])).
% 0.23/0.51 tff(286,plain,(
% 0.23/0.51 ![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y)))),
% 0.23/0.51 inference(skolemize,[status(sab)],[285])).
% 0.23/0.51 tff(287,plain,
% 0.23/0.51 (![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y)))),
% 0.23/0.51 inference(modus_ponens,[status(thm)],[286, 279])).
% 0.23/0.51 tff(288,plain,
% 0.23/0.51 ((~![X: $i, Y: $i] : (smaller_or_equal(X, Y) <=> ((X = Y) | smaller(X, Y)))) | (smaller_or_equal(zero, tau) <=> ((zero = tau) | smaller(zero, tau)))),
% 0.23/0.51 inference(quant_inst,[status(thm)],[])).
% 0.23/0.51 tff(289,plain,
% 0.23/0.51 (smaller_or_equal(zero, tau) <=> ((zero = tau) | smaller(zero, tau))),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[288, 287])).
% 0.23/0.51 tff(290,plain,
% 0.23/0.51 ((~![X: $i, Y: $i] : (smaller(X, Y) <=> greater(Y, X))) | (smaller(zero, tau) <=> greater(tau, zero))),
% 0.23/0.51 inference(quant_inst,[status(thm)],[])).
% 0.23/0.51 tff(291,plain,
% 0.23/0.51 (smaller(zero, tau) <=> greater(tau, zero)),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[290, 239])).
% 0.23/0.51 tff(292,plain,
% 0.23/0.51 (greater(tau, zero)),
% 0.23/0.51 inference(and_elim,[status(thm)],[21])).
% 0.23/0.51 tff(293,plain,
% 0.23/0.51 ((~(smaller(zero, tau) <=> greater(tau, zero))) | smaller(zero, tau) | (~greater(tau, zero))),
% 0.23/0.51 inference(tautology,[status(thm)],[])).
% 0.23/0.51 tff(294,plain,
% 0.23/0.51 ((~(smaller(zero, tau) <=> greater(tau, zero))) | smaller(zero, tau)),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[293, 292])).
% 0.23/0.51 tff(295,plain,
% 0.23/0.51 (smaller(zero, tau)),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[294, 291])).
% 0.23/0.51 tff(296,plain,
% 0.23/0.51 (((zero = tau) | smaller(zero, tau)) | (~smaller(zero, tau))),
% 0.23/0.51 inference(tautology,[status(thm)],[])).
% 0.23/0.51 tff(297,plain,
% 0.23/0.51 ((zero = tau) | smaller(zero, tau)),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[296, 295])).
% 0.23/0.51 tff(298,plain,
% 0.23/0.51 ((~(smaller_or_equal(zero, tau) <=> ((zero = tau) | smaller(zero, tau)))) | smaller_or_equal(zero, tau) | (~((zero = tau) | smaller(zero, tau)))),
% 0.23/0.51 inference(tautology,[status(thm)],[])).
% 0.23/0.51 tff(299,plain,
% 0.23/0.51 ((~(smaller_or_equal(zero, tau) <=> ((zero = tau) | smaller(zero, tau)))) | smaller_or_equal(zero, tau)),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[298, 297])).
% 0.23/0.51 tff(300,plain,
% 0.23/0.51 (smaller_or_equal(zero, tau)),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[299, 289])).
% 0.23/0.51 tff(301,plain,
% 0.23/0.51 (smaller_or_equal(age(X!4, T0!3), tau)),
% 0.23/0.51 inference(modus_ponens,[status(thm)],[300, 277])).
% 0.23/0.51 tff(302,plain,
% 0.23/0.51 ((~((~positional_advantage(X!4, T0!3)) | (~smaller_or_equal(age(X!4, T0!3), tau)))) | (~positional_advantage(X!4, T0!3)) | (~smaller_or_equal(age(X!4, T0!3), tau))),
% 0.23/0.51 inference(tautology,[status(thm)],[])).
% 0.23/0.51 tff(303,plain,
% 0.23/0.51 (~positional_advantage(X!4, T0!3)),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[302, 301, 275])).
% 0.23/0.51 tff(304,plain,
% 0.23/0.51 ((~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2)),
% 0.23/0.51 inference(tautology,[status(thm)],[])).
% 0.23/0.51 tff(305,plain,
% 0.23/0.51 ((~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | positional_advantage(X!4, T0!3) | (hazard_of_mortality(X!4, T0!3) = mod2)),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[304, 115])).
% 0.23/0.51 tff(306,plain,
% 0.23/0.51 ((~(positional_advantage(X!4, T0!3) | (~is_aligned(X!4, T0!3)) | (hazard_of_mortality(X!4, T0!3) = mod2))) | (hazard_of_mortality(X!4, T0!3) = mod2)),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[305, 303])).
% 0.23/0.51 tff(307,plain,
% 0.23/0.51 (hazard_of_mortality(X!4, T0!3) = mod2),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[306, 271])).
% 0.23/0.51 tff(308,plain,
% 0.23/0.51 ((hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3)) <=> (hazard_of_mortality(X!4, T1!2) = mod2)),
% 0.23/0.51 inference(monotonicity,[status(thm)],[307])).
% 0.23/0.51 tff(309,plain,
% 0.23/0.51 ((hazard_of_mortality(X!4, T1!2) = mod2) <=> (hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3))),
% 0.23/0.51 inference(symmetry,[status(thm)],[308])).
% 0.23/0.51 tff(310,assumption,(hazard_of_mortality(X!4, T1!2) = mod2), introduced(assumption)).
% 0.23/0.51 tff(311,plain,
% 0.23/0.51 (hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3)),
% 0.23/0.51 inference(modus_ponens,[status(thm)],[310, 309])).
% 0.23/0.51 tff(312,assumption,(~(hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3))), introduced(assumption)).
% 0.23/0.51 tff(313,plain,
% 0.23/0.51 ($false),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[312, 311])).
% 0.23/0.51 tff(314,plain,((~(hazard_of_mortality(X!4, T1!2) = mod2)) | (hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3))), inference(lemma,lemma(discharge,[]))).
% 0.23/0.51 tff(315,plain,
% 0.23/0.51 (hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3)),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[314, 172])).
% 0.23/0.51 tff(316,plain,
% 0.23/0.51 ((~(~((~smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2))) | (~(hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3)))))) <=> ((~smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2))) | (~(hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3))))),
% 0.23/0.51 inference(rewrite,[status(thm)],[])).
% 0.23/0.51 tff(317,plain,
% 0.23/0.51 ((smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2)) & (hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3))) <=> (~((~smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2))) | (~(hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3)))))),
% 0.23/0.51 inference(rewrite,[status(thm)],[])).
% 0.23/0.51 tff(318,plain,
% 0.23/0.51 ((~(smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2)) & (hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3)))) <=> (~(~((~smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2))) | (~(hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3))))))),
% 0.23/0.51 inference(monotonicity,[status(thm)],[317])).
% 0.23/0.51 tff(319,plain,
% 0.23/0.51 ((~(smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2)) & (hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3)))) <=> ((~smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2))) | (~(hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3))))),
% 0.23/0.51 inference(transitivity,[status(thm)],[318, 316])).
% 0.23/0.51 tff(320,plain,
% 0.23/0.51 (~(smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2)) & (hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3)))),
% 0.23/0.51 inference(or_elim,[status(thm)],[20])).
% 0.23/0.51 tff(321,plain,
% 0.23/0.51 ((~smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2))) | (~(hazard_of_mortality(X!4, T1!2) = hazard_of_mortality(X!4, T0!3)))),
% 0.23/0.51 inference(modus_ponens,[status(thm)],[320, 319])).
% 0.23/0.51 tff(322,plain,
% 0.23/0.51 (~smaller(hazard_of_mortality(X!4, T2!1), hazard_of_mortality(X!4, T1!2))),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[321, 315])).
% 0.23/0.51 tff(323,plain,
% 0.23/0.51 ($false),
% 0.23/0.51 inference(unit_resolution,[status(thm)],[322, 248])).
% 0.23/0.51 % SZS output end Proof
% 0.23/0.51 % E exiting
%------------------------------------------------------------------------------