%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT055-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n027.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:08 AM UTC 2026
% Result : Unsatisfiable 0.67s 0.99s
% Output : Proof 0.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT055-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.10/0.37 % Computer : n027.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 7 13:30:48 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.67/0.99 % SZS status Unsatisfiable
% 0.67/0.99 % SZS output start Proof
% 0.67/0.99 tff(greater_type, type, (
% 0.67/0.99 greater: ( $i * $i ) > $o)).
% 0.67/0.99 tff(age_type, type, (
% 0.67/0.99 age: ( $i * $i ) > $i)).
% 0.67/0.99 tff(sk5_type, type, (
% 0.67/0.99 sk5: $i)).
% 0.67/0.99 tff(sk2_type, type, (
% 0.67/0.99 sk2: $i)).
% 0.67/0.99 tff(sigma_type, type, (
% 0.67/0.99 sigma: $i)).
% 0.67/0.99 tff(smaller_type, type, (
% 0.67/0.99 smaller: ( $i * $i ) > $o)).
% 0.67/0.99 tff(dissimilar_type, type, (
% 0.67/0.99 dissimilar: ( $i * $i * $i ) > $o)).
% 0.67/0.99 tff(sk3_type, type, (
% 0.67/0.99 sk3: $i)).
% 0.67/0.99 tff(is_aligned_type, type, (
% 0.67/0.99 is_aligned: ( $i * $i ) > $o)).
% 0.67/0.99 tff(sk6_type, type, (
% 0.67/0.99 sk6: $i)).
% 0.67/0.99 tff(zero_type, type, (
% 0.67/0.99 zero: $i)).
% 0.67/0.99 tff(organization_type, type, (
% 0.67/0.99 organization: $i > $o)).
% 0.67/0.99 tff(capability_type, type, (
% 0.67/0.99 capability: ( $i * $i ) > $i)).
% 0.67/0.99 tff(has_immunity_type, type, (
% 0.67/0.99 has_immunity: ( $i * $i ) > $o)).
% 0.67/0.99 tff(eta_type, type, (
% 0.67/0.99 eta: $i)).
% 0.67/0.99 tff(has_endowment_type, type, (
% 0.67/0.99 has_endowment: $i > $o)).
% 0.67/0.99 tff(hazard_of_mortality_type, type, (
% 0.67/0.99 hazard_of_mortality: ( $i * $i ) > $i)).
% 0.67/0.99 tff(sk4_type, type, (
% 0.67/0.99 sk4: $i)).
% 0.67/0.99 tff(smaller_or_equal_type, type, (
% 0.67/0.99 smaller_or_equal: ( $i * $i ) > $o)).
% 0.67/0.99 tff(1,assumption,(~dissimilar(sk2, sk3, sk5)), introduced(assumption)).
% 0.67/0.99 tff(2,plain,
% 0.67/0.99 (greater(age(sk2, sk6), sigma) <=> greater(age(sk2, sk6), sigma)),
% 0.67/0.99 inference(rewrite,[status(thm)],[])).
% 0.67/0.99 tff(3,axiom,(greater(age(sk2, sk6), sigma)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma_8_65')).
% 0.67/0.99 tff(4,plain,
% 0.67/0.99 (greater(age(sk2, sk6), sigma)),
% 0.67/0.99 inference(modus_ponens,[status(thm)],[3, 2])).
% 0.67/0.99 tff(5,plain,
% 0.67/0.99 ((age(sk2, sk3) = zero) <=> (age(sk2, sk3) = zero)),
% 0.67/0.99 inference(rewrite,[status(thm)],[])).
% 0.67/0.99 tff(6,axiom,(age(sk2, sk3) = zero), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma_8_61')).
% 0.67/0.99 tff(7,plain,
% 0.67/0.99 (age(sk2, sk3) = zero),
% 0.67/0.99 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.67/0.99 tff(8,plain,
% 0.67/0.99 (organization(sk2) <=> organization(sk2)),
% 0.67/0.99 inference(rewrite,[status(thm)],[])).
% 0.67/0.99 tff(9,axiom,(organization(sk2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma_8_59')).
% 0.67/0.99 tff(10,plain,
% 0.67/0.99 (organization(sk2)),
% 0.67/0.99 inference(modus_ponens,[status(thm)],[9, 8])).
% 0.67/0.99 tff(11,plain,
% 0.67/0.99 (^[B: $i, A: $i, C: $i] : refl((dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero))) <=> (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero))))),
% 0.67/0.99 inference(bind,[status(th)],[])).
% 0.67/0.99 tff(12,plain,
% 0.67/0.99 (![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero))) <=> ![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))),
% 0.67/0.99 inference(quant_intro,[status(thm)],[11])).
% 0.67/0.99 tff(13,plain,
% 0.67/0.99 (![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero))) <=> ![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))),
% 0.67/0.99 inference(rewrite,[status(thm)],[])).
% 0.67/0.99 tff(14,plain,
% 0.67/0.99 (^[B: $i, A: $i, C: $i] : trans(monotonicity(rewrite((((~organization(A)) | (~(age(A, B) = zero))) | (~greater(age(A, C), sigma))) <=> ((~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))), (((((~organization(A)) | (~(age(A, B) = zero))) | (~greater(age(A, C), sigma))) | dissimilar(A, B, C)) <=> (((~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero))) | dissimilar(A, B, C)))), rewrite((((~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero))) | dissimilar(A, B, C)) <=> (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))), (((((~organization(A)) | (~(age(A, B) = zero))) | (~greater(age(A, C), sigma))) | dissimilar(A, B, C)) <=> (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))))),
% 0.67/0.99 inference(bind,[status(th)],[])).
% 0.67/0.99 tff(15,plain,
% 0.67/0.99 (![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~(age(A, B) = zero))) | (~greater(age(A, C), sigma))) | dissimilar(A, B, C)) <=> ![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))),
% 0.67/0.99 inference(quant_intro,[status(thm)],[14])).
% 0.67/0.99 tff(16,axiom,(![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~(age(A, B) = zero))) | (~greater(age(A, C), sigma))) | dissimilar(A, B, C))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_15_56')).
% 0.67/0.99 tff(17,plain,
% 0.67/0.99 (![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))),
% 0.67/0.99 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.67/0.99 tff(18,plain,
% 0.67/0.99 (![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))),
% 0.67/0.99 inference(modus_ponens,[status(thm)],[17, 13])).
% 0.67/0.99 tff(19,plain,(
% 0.67/0.99 ![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))),
% 0.67/0.99 inference(skolemize,[status(sab)],[18])).
% 0.67/0.99 tff(20,plain,
% 0.67/0.99 (![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))),
% 0.67/0.99 inference(modus_ponens,[status(thm)],[19, 12])).
% 0.67/0.99 tff(21,plain,
% 0.67/0.99 (((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))) | ((~greater(age(sk2, sk6), sigma)) | (~organization(sk2)) | (~(age(sk2, sk3) = zero)) | dissimilar(sk2, sk3, sk6))) <=> ((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))) | (~greater(age(sk2, sk6), sigma)) | (~organization(sk2)) | (~(age(sk2, sk3) = zero)) | dissimilar(sk2, sk3, sk6))),
% 0.67/0.99 inference(rewrite,[status(thm)],[])).
% 0.67/0.99 tff(22,plain,
% 0.67/0.99 ((dissimilar(sk2, sk3, sk6) | (~organization(sk2)) | (~greater(age(sk2, sk6), sigma)) | (~(age(sk2, sk3) = zero))) <=> ((~greater(age(sk2, sk6), sigma)) | (~organization(sk2)) | (~(age(sk2, sk3) = zero)) | dissimilar(sk2, sk3, sk6))),
% 0.67/0.99 inference(rewrite,[status(thm)],[])).
% 0.67/0.99 tff(23,plain,
% 0.67/0.99 (((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))) | (dissimilar(sk2, sk3, sk6) | (~organization(sk2)) | (~greater(age(sk2, sk6), sigma)) | (~(age(sk2, sk3) = zero)))) <=> ((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))) | ((~greater(age(sk2, sk6), sigma)) | (~organization(sk2)) | (~(age(sk2, sk3) = zero)) | dissimilar(sk2, sk3, sk6)))),
% 0.67/0.99 inference(monotonicity,[status(thm)],[22])).
% 0.67/0.99 tff(24,plain,
% 0.67/0.99 (((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))) | (dissimilar(sk2, sk3, sk6) | (~organization(sk2)) | (~greater(age(sk2, sk6), sigma)) | (~(age(sk2, sk3) = zero)))) <=> ((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))) | (~greater(age(sk2, sk6), sigma)) | (~organization(sk2)) | (~(age(sk2, sk3) = zero)) | dissimilar(sk2, sk3, sk6))),
% 0.67/0.99 inference(transitivity,[status(thm)],[23, 21])).
% 0.67/0.99 tff(25,plain,
% 0.67/0.99 ((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))) | (dissimilar(sk2, sk3, sk6) | (~organization(sk2)) | (~greater(age(sk2, sk6), sigma)) | (~(age(sk2, sk3) = zero)))),
% 0.67/0.99 inference(quant_inst,[status(thm)],[])).
% 0.67/0.99 tff(26,plain,
% 0.67/0.99 ((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | (~organization(A)) | (~greater(age(A, C), sigma)) | (~(age(A, B) = zero)))) | (~greater(age(sk2, sk6), sigma)) | (~organization(sk2)) | (~(age(sk2, sk3) = zero)) | dissimilar(sk2, sk3, sk6)),
% 0.67/0.99 inference(modus_ponens,[status(thm)],[25, 24])).
% 0.67/0.99 tff(27,plain,
% 0.67/0.99 (dissimilar(sk2, sk3, sk6)),
% 0.67/0.99 inference(unit_resolution,[status(thm)],[26, 20, 10, 7, 4])).
% 0.67/0.99 tff(28,plain,
% 0.67/0.99 (^[B: $i, A: $i] : refl(((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero))) <=> ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero))))),
% 0.67/0.99 inference(bind,[status(th)],[])).
% 0.67/0.99 tff(29,plain,
% 0.67/0.99 (![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero))) <=> ![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))),
% 0.67/1.00 inference(quant_intro,[status(thm)],[28])).
% 0.67/1.00 tff(30,plain,
% 0.67/1.00 (![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero))) <=> ![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))),
% 0.67/1.00 inference(rewrite,[status(thm)],[])).
% 0.67/1.00 tff(31,plain,
% 0.67/1.00 (^[B: $i, A: $i] : rewrite((((~organization(A)) | (~(age(A, B) = zero))) | is_aligned(A, B)) <=> ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero))))),
% 0.67/1.00 inference(bind,[status(th)],[])).
% 0.67/1.00 tff(32,plain,
% 0.67/1.00 (![B: $i, A: $i] : (((~organization(A)) | (~(age(A, B) = zero))) | is_aligned(A, B)) <=> ![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))),
% 0.67/1.00 inference(quant_intro,[status(thm)],[31])).
% 0.67/1.00 tff(33,axiom,(![B: $i, A: $i] : (((~organization(A)) | (~(age(A, B) = zero))) | is_aligned(A, B))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_13_54')).
% 0.67/1.00 tff(34,plain,
% 0.67/1.00 (![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))),
% 0.67/1.00 inference(modus_ponens,[status(thm)],[33, 32])).
% 0.67/1.00 tff(35,plain,
% 0.67/1.00 (![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))),
% 0.67/1.00 inference(modus_ponens,[status(thm)],[34, 30])).
% 0.67/1.00 tff(36,plain,(
% 0.67/1.00 ![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))),
% 0.67/1.00 inference(skolemize,[status(sab)],[35])).
% 0.67/1.00 tff(37,plain,
% 0.67/1.00 (![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))),
% 0.67/1.00 inference(modus_ponens,[status(thm)],[36, 29])).
% 0.67/1.00 tff(38,plain,
% 0.67/1.00 (((~![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))) | ((~organization(sk2)) | is_aligned(sk2, sk3) | (~(age(sk2, sk3) = zero)))) <=> ((~![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))) | (~organization(sk2)) | is_aligned(sk2, sk3) | (~(age(sk2, sk3) = zero)))),
% 0.67/1.00 inference(rewrite,[status(thm)],[])).
% 0.67/1.00 tff(39,plain,
% 0.67/1.00 ((~![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))) | ((~organization(sk2)) | is_aligned(sk2, sk3) | (~(age(sk2, sk3) = zero)))),
% 0.67/1.00 inference(quant_inst,[status(thm)],[])).
% 0.67/1.00 tff(40,plain,
% 0.67/1.00 ((~![B: $i, A: $i] : ((~organization(A)) | is_aligned(A, B) | (~(age(A, B) = zero)))) | (~organization(sk2)) | is_aligned(sk2, sk3) | (~(age(sk2, sk3) = zero))),
% 0.67/1.00 inference(modus_ponens,[status(thm)],[39, 38])).
% 0.67/1.00 tff(41,plain,
% 0.67/1.00 (is_aligned(sk2, sk3)),
% 0.67/1.00 inference(unit_resolution,[status(thm)],[40, 37, 10, 7])).
% 0.67/1.00 tff(42,plain,
% 0.67/1.00 (^[B: $i, A: $i, C: $i] : refl(((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B))) <=> ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B))))),
% 0.67/1.00 inference(bind,[status(th)],[])).
% 0.67/1.00 tff(43,plain,
% 0.67/1.00 (![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B))) <=> ![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))),
% 0.67/1.00 inference(quant_intro,[status(thm)],[42])).
% 0.67/1.00 tff(44,plain,
% 0.67/1.00 (![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B))) <=> ![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))),
% 0.67/1.00 inference(rewrite,[status(thm)],[])).
% 0.67/1.00 tff(45,plain,
% 0.67/1.00 (^[B: $i, A: $i, C: $i] : trans(monotonicity(rewrite(((~dissimilar(A, B, C)) | (~is_aligned(A, B))) <=> ((~dissimilar(A, B, C)) | (~is_aligned(A, B)))), ((((~dissimilar(A, B, C)) | (~is_aligned(A, B))) | (~is_aligned(A, C))) <=> (((~dissimilar(A, B, C)) | (~is_aligned(A, B))) | (~is_aligned(A, C))))), rewrite((((~dissimilar(A, B, C)) | (~is_aligned(A, B))) | (~is_aligned(A, C))) <=> ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))), ((((~dissimilar(A, B, C)) | (~is_aligned(A, B))) | (~is_aligned(A, C))) <=> ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))))),
% 0.67/1.00 inference(bind,[status(th)],[])).
% 0.67/1.00 tff(46,plain,
% 0.67/1.00 (![B: $i, A: $i, C: $i] : (((~dissimilar(A, B, C)) | (~is_aligned(A, B))) | (~is_aligned(A, C))) <=> ![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))),
% 0.67/1.00 inference(quant_intro,[status(thm)],[45])).
% 0.67/1.00 tff(47,axiom,(![B: $i, A: $i, C: $i] : (((~dissimilar(A, B, C)) | (~is_aligned(A, B))) | (~is_aligned(A, C)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','definition_2_49')).
% 0.67/1.00 tff(48,plain,
% 0.67/1.00 (![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))),
% 0.67/1.00 inference(modus_ponens,[status(thm)],[47, 46])).
% 0.67/1.00 tff(49,plain,
% 0.67/1.00 (![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))),
% 0.67/1.00 inference(modus_ponens,[status(thm)],[48, 44])).
% 0.67/1.00 tff(50,plain,(
% 0.67/1.00 ![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))),
% 0.67/1.00 inference(skolemize,[status(sab)],[49])).
% 0.67/1.00 tff(51,plain,
% 0.67/1.00 (![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))),
% 0.67/1.00 inference(modus_ponens,[status(thm)],[50, 43])).
% 0.67/1.00 tff(52,plain,
% 0.67/1.00 (((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))) | ((~is_aligned(sk2, sk3)) | (~is_aligned(sk2, sk6)) | (~dissimilar(sk2, sk3, sk6)))) <=> ((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))) | (~is_aligned(sk2, sk3)) | (~is_aligned(sk2, sk6)) | (~dissimilar(sk2, sk3, sk6)))),
% 0.67/1.00 inference(rewrite,[status(thm)],[])).
% 0.67/1.00 tff(53,plain,
% 0.67/1.00 (((~dissimilar(sk2, sk3, sk6)) | (~is_aligned(sk2, sk6)) | (~is_aligned(sk2, sk3))) <=> ((~is_aligned(sk2, sk3)) | (~is_aligned(sk2, sk6)) | (~dissimilar(sk2, sk3, sk6)))),
% 0.67/1.00 inference(rewrite,[status(thm)],[])).
% 0.67/1.00 tff(54,plain,
% 0.67/1.00 (((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))) | ((~dissimilar(sk2, sk3, sk6)) | (~is_aligned(sk2, sk6)) | (~is_aligned(sk2, sk3)))) <=> ((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))) | ((~is_aligned(sk2, sk3)) | (~is_aligned(sk2, sk6)) | (~dissimilar(sk2, sk3, sk6))))),
% 0.67/1.00 inference(monotonicity,[status(thm)],[53])).
% 0.67/1.00 tff(55,plain,
% 0.67/1.00 (((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))) | ((~dissimilar(sk2, sk3, sk6)) | (~is_aligned(sk2, sk6)) | (~is_aligned(sk2, sk3)))) <=> ((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))) | (~is_aligned(sk2, sk3)) | (~is_aligned(sk2, sk6)) | (~dissimilar(sk2, sk3, sk6)))),
% 0.67/1.00 inference(transitivity,[status(thm)],[54, 52])).
% 0.67/1.00 tff(56,plain,
% 0.67/1.00 ((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))) | ((~dissimilar(sk2, sk3, sk6)) | (~is_aligned(sk2, sk6)) | (~is_aligned(sk2, sk3)))),
% 0.67/1.00 inference(quant_inst,[status(thm)],[])).
% 0.67/1.00 tff(57,plain,
% 0.67/1.00 ((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~is_aligned(A, C)) | (~is_aligned(A, B)))) | (~is_aligned(sk2, sk3)) | (~is_aligned(sk2, sk6)) | (~dissimilar(sk2, sk3, sk6))),
% 0.67/1.00 inference(modus_ponens,[status(thm)],[56, 55])).
% 0.67/1.00 tff(58,plain,
% 0.67/1.00 (~is_aligned(sk2, sk6)),
% 0.67/1.00 inference(unit_resolution,[status(thm)],[57, 51, 41, 27])).
% 0.67/1.00 tff(59,plain,
% 0.67/1.00 (greater(sigma, eta) <=> greater(sigma, eta)),
% 0.67/1.00 inference(rewrite,[status(thm)],[])).
% 0.67/1.00 tff(60,axiom,(greater(sigma, eta)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma_8_66')).
% 0.67/1.00 tff(61,plain,
% 0.67/1.00 (greater(sigma, eta)),
% 0.67/1.00 inference(modus_ponens,[status(thm)],[60, 59])).
% 0.67/1.00 tff(62,plain,
% 0.67/1.00 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B))) <=> ![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.67/1.00 inference(rewrite,[status(thm)],[])).
% 0.67/1.00 tff(63,plain,
% 0.67/1.00 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B))) <=> ![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.67/1.00 inference(rewrite,[status(thm)],[])).
% 0.67/1.00 tff(64,plain,
% 0.67/1.00 (^[B: $i, A: $i, C: $i] : rewrite((((~greater(A, B)) | (~greater(B, C))) | greater(A, C)) <=> (greater(A, C) | (~greater(B, C)) | (~greater(A, B))))),
% 0.67/1.01 inference(bind,[status(th)],[])).
% 0.67/1.01 tff(65,plain,
% 0.67/1.01 (![B: $i, A: $i, C: $i] : (((~greater(A, B)) | (~greater(B, C))) | greater(A, C)) <=> ![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.67/1.01 inference(quant_intro,[status(thm)],[64])).
% 0.67/1.01 tff(66,axiom,(![B: $i, A: $i, C: $i] : (((~greater(A, B)) | (~greater(B, C))) | greater(A, C))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax','meaning_postulate_greater_transitive_10')).
% 0.67/1.01 tff(67,plain,
% 0.67/1.01 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.67/1.01 tff(68,plain,
% 0.67/1.01 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[67, 63])).
% 0.67/1.01 tff(69,plain,(
% 0.67/1.01 ![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.67/1.01 inference(skolemize,[status(sab)],[68])).
% 0.67/1.01 tff(70,plain,
% 0.67/1.01 (![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[69, 62])).
% 0.67/1.01 tff(71,plain,
% 0.67/1.01 (((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(age(sk2, sk6), eta) | (~greater(sigma, eta)) | (~greater(age(sk2, sk6), sigma)))) <=> ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(age(sk2, sk6), eta) | (~greater(sigma, eta)) | (~greater(age(sk2, sk6), sigma)))),
% 0.67/1.01 inference(rewrite,[status(thm)],[])).
% 0.67/1.01 tff(72,plain,
% 0.67/1.01 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | (greater(age(sk2, sk6), eta) | (~greater(sigma, eta)) | (~greater(age(sk2, sk6), sigma)))),
% 0.67/1.01 inference(quant_inst,[status(thm)],[])).
% 0.67/1.01 tff(73,plain,
% 0.67/1.01 ((~![B: $i, A: $i, C: $i] : (greater(A, C) | (~greater(B, C)) | (~greater(A, B)))) | greater(age(sk2, sk6), eta) | (~greater(sigma, eta)) | (~greater(age(sk2, sk6), sigma))),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[72, 71])).
% 0.67/1.01 tff(74,plain,
% 0.67/1.01 (greater(age(sk2, sk6), eta)),
% 0.67/1.01 inference(unit_resolution,[status(thm)],[73, 70, 4, 61])).
% 0.67/1.01 tff(75,plain,
% 0.67/1.01 (has_endowment(sk2) <=> has_endowment(sk2)),
% 0.67/1.01 inference(rewrite,[status(thm)],[])).
% 0.67/1.01 tff(76,axiom,(has_endowment(sk2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma_8_60')).
% 0.67/1.01 tff(77,plain,
% 0.67/1.01 (has_endowment(sk2)),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[76, 75])).
% 0.67/1.01 tff(78,plain,
% 0.67/1.01 (^[B: $i, A: $i] : refl(((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta))) <=> ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta))))),
% 0.67/1.01 inference(bind,[status(th)],[])).
% 0.67/1.01 tff(79,plain,
% 0.67/1.01 (![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta))) <=> ![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))),
% 0.67/1.01 inference(quant_intro,[status(thm)],[78])).
% 0.67/1.01 tff(80,plain,
% 0.67/1.01 (![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta))) <=> ![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))),
% 0.67/1.01 inference(rewrite,[status(thm)],[])).
% 0.67/1.01 tff(81,plain,
% 0.67/1.01 (^[B: $i, A: $i] : rewrite((((~has_endowment(A)) | (~greater(age(A, B), eta))) | (~has_immunity(A, B))) <=> ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta))))),
% 0.67/1.01 inference(bind,[status(th)],[])).
% 0.67/1.01 tff(82,plain,
% 0.67/1.01 (![B: $i, A: $i] : (((~has_endowment(A)) | (~greater(age(A, B), eta))) | (~has_immunity(A, B))) <=> ![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))),
% 0.67/1.01 inference(quant_intro,[status(thm)],[81])).
% 0.67/1.01 tff(83,axiom,(![B: $i, A: $i] : (((~has_endowment(A)) | (~greater(age(A, B), eta))) | (~has_immunity(A, B)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','definition_1_40')).
% 0.67/1.01 tff(84,plain,
% 0.67/1.01 (![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.67/1.01 tff(85,plain,
% 0.67/1.01 (![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[84, 80])).
% 0.67/1.01 tff(86,plain,(
% 0.67/1.01 ![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))),
% 0.67/1.01 inference(skolemize,[status(sab)],[85])).
% 0.67/1.01 tff(87,plain,
% 0.67/1.01 (![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[86, 79])).
% 0.67/1.01 tff(88,plain,
% 0.67/1.01 (((~![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))) | ((~has_endowment(sk2)) | (~has_immunity(sk2, sk6)) | (~greater(age(sk2, sk6), eta)))) <=> ((~![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))) | (~has_endowment(sk2)) | (~has_immunity(sk2, sk6)) | (~greater(age(sk2, sk6), eta)))),
% 0.67/1.01 inference(rewrite,[status(thm)],[])).
% 0.67/1.01 tff(89,plain,
% 0.67/1.01 ((~![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))) | ((~has_endowment(sk2)) | (~has_immunity(sk2, sk6)) | (~greater(age(sk2, sk6), eta)))),
% 0.67/1.01 inference(quant_inst,[status(thm)],[])).
% 0.67/1.01 tff(90,plain,
% 0.67/1.01 ((~![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))) | (~has_endowment(sk2)) | (~has_immunity(sk2, sk6)) | (~greater(age(sk2, sk6), eta))),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[89, 88])).
% 0.67/1.01 tff(91,plain,
% 0.67/1.01 (~has_immunity(sk2, sk6)),
% 0.67/1.01 inference(unit_resolution,[status(thm)],[90, 87, 77, 74])).
% 0.67/1.01 tff(92,plain,
% 0.67/1.01 (greater(age(sk2, sk5), eta) <=> greater(age(sk2, sk5), eta)),
% 0.67/1.01 inference(rewrite,[status(thm)],[])).
% 0.67/1.01 tff(93,axiom,(greater(age(sk2, sk5), eta)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma_8_63')).
% 0.67/1.01 tff(94,plain,
% 0.67/1.01 (greater(age(sk2, sk5), eta)),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[93, 92])).
% 0.67/1.01 tff(95,plain,
% 0.67/1.01 (((~![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))) | ((~has_endowment(sk2)) | (~has_immunity(sk2, sk5)) | (~greater(age(sk2, sk5), eta)))) <=> ((~![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))) | (~has_endowment(sk2)) | (~has_immunity(sk2, sk5)) | (~greater(age(sk2, sk5), eta)))),
% 0.67/1.01 inference(rewrite,[status(thm)],[])).
% 0.67/1.01 tff(96,plain,
% 0.67/1.01 ((~![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))) | ((~has_endowment(sk2)) | (~has_immunity(sk2, sk5)) | (~greater(age(sk2, sk5), eta)))),
% 0.67/1.01 inference(quant_inst,[status(thm)],[])).
% 0.67/1.01 tff(97,plain,
% 0.67/1.01 ((~![B: $i, A: $i] : ((~has_endowment(A)) | (~has_immunity(A, B)) | (~greater(age(A, B), eta)))) | (~has_endowment(sk2)) | (~has_immunity(sk2, sk5)) | (~greater(age(sk2, sk5), eta))),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[96, 95])).
% 0.67/1.01 tff(98,plain,
% 0.67/1.01 (~has_immunity(sk2, sk5)),
% 0.67/1.01 inference(unit_resolution,[status(thm)],[97, 87, 77, 94])).
% 0.67/1.01 tff(99,plain,
% 0.67/1.01 (smaller_or_equal(age(sk2, sk4), eta) <=> smaller_or_equal(age(sk2, sk4), eta)),
% 0.67/1.01 inference(rewrite,[status(thm)],[])).
% 0.67/1.01 tff(100,axiom,(smaller_or_equal(age(sk2, sk4), eta)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma_8_62')).
% 0.67/1.01 tff(101,plain,
% 0.67/1.01 (smaller_or_equal(age(sk2, sk4), eta)),
% 0.67/1.01 inference(modus_ponens,[status(thm)],[100, 99])).
% 0.67/1.01 tff(102,plain,
% 0.67/1.01 (^[B: $i, A: $i] : refl(((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta))) <=> ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta))))),
% 0.67/1.01 inference(bind,[status(th)],[])).
% 0.67/1.01 tff(103,plain,
% 0.67/1.01 (![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta))) <=> ![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))),
% 0.67/1.01 inference(quant_intro,[status(thm)],[102])).
% 0.67/1.01 tff(104,plain,
% 0.67/1.01 (![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta))) <=> ![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))),
% 0.67/1.01 inference(rewrite,[status(thm)],[])).
% 0.67/1.01 tff(105,plain,
% 0.67/1.02 (^[B: $i, A: $i] : rewrite((((~has_endowment(A)) | (~smaller_or_equal(age(A, B), eta))) | has_immunity(A, B)) <=> ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta))))),
% 0.67/1.02 inference(bind,[status(th)],[])).
% 0.67/1.02 tff(106,plain,
% 0.67/1.02 (![B: $i, A: $i] : (((~has_endowment(A)) | (~smaller_or_equal(age(A, B), eta))) | has_immunity(A, B)) <=> ![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))),
% 0.67/1.02 inference(quant_intro,[status(thm)],[105])).
% 0.67/1.02 tff(107,axiom,(![B: $i, A: $i] : (((~has_endowment(A)) | (~smaller_or_equal(age(A, B), eta))) | has_immunity(A, B))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','definition_1_39')).
% 0.67/1.02 tff(108,plain,
% 0.67/1.02 (![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))),
% 0.67/1.02 inference(modus_ponens,[status(thm)],[107, 106])).
% 0.67/1.02 tff(109,plain,
% 0.67/1.02 (![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))),
% 0.67/1.02 inference(modus_ponens,[status(thm)],[108, 104])).
% 0.67/1.02 tff(110,plain,(
% 0.67/1.02 ![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))),
% 0.67/1.02 inference(skolemize,[status(sab)],[109])).
% 0.67/1.02 tff(111,plain,
% 0.67/1.02 (![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))),
% 0.67/1.02 inference(modus_ponens,[status(thm)],[110, 103])).
% 0.67/1.02 tff(112,plain,
% 0.67/1.02 (((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | ((~smaller_or_equal(age(sk2, sk4), eta)) | (~has_endowment(sk2)) | has_immunity(sk2, sk4))) <=> ((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | (~smaller_or_equal(age(sk2, sk4), eta)) | (~has_endowment(sk2)) | has_immunity(sk2, sk4))),
% 0.67/1.02 inference(rewrite,[status(thm)],[])).
% 0.67/1.02 tff(113,plain,
% 0.67/1.02 (((~has_endowment(sk2)) | has_immunity(sk2, sk4) | (~smaller_or_equal(age(sk2, sk4), eta))) <=> ((~smaller_or_equal(age(sk2, sk4), eta)) | (~has_endowment(sk2)) | has_immunity(sk2, sk4))),
% 0.67/1.02 inference(rewrite,[status(thm)],[])).
% 0.67/1.02 tff(114,plain,
% 0.67/1.02 (((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | ((~has_endowment(sk2)) | has_immunity(sk2, sk4) | (~smaller_or_equal(age(sk2, sk4), eta)))) <=> ((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | ((~smaller_or_equal(age(sk2, sk4), eta)) | (~has_endowment(sk2)) | has_immunity(sk2, sk4)))),
% 0.67/1.02 inference(monotonicity,[status(thm)],[113])).
% 0.67/1.02 tff(115,plain,
% 0.67/1.02 (((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | ((~has_endowment(sk2)) | has_immunity(sk2, sk4) | (~smaller_or_equal(age(sk2, sk4), eta)))) <=> ((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | (~smaller_or_equal(age(sk2, sk4), eta)) | (~has_endowment(sk2)) | has_immunity(sk2, sk4))),
% 0.67/1.02 inference(transitivity,[status(thm)],[114, 112])).
% 0.67/1.02 tff(116,plain,
% 0.67/1.02 ((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | ((~has_endowment(sk2)) | has_immunity(sk2, sk4) | (~smaller_or_equal(age(sk2, sk4), eta)))),
% 0.67/1.02 inference(quant_inst,[status(thm)],[])).
% 0.67/1.02 tff(117,plain,
% 0.67/1.02 ((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | (~smaller_or_equal(age(sk2, sk4), eta)) | (~has_endowment(sk2)) | has_immunity(sk2, sk4)),
% 0.67/1.02 inference(modus_ponens,[status(thm)],[116, 115])).
% 0.67/1.02 tff(118,plain,
% 0.67/1.02 (has_immunity(sk2, sk4)),
% 0.67/1.02 inference(unit_resolution,[status(thm)],[117, 111, 77, 101])).
% 0.67/1.02 tff(119,assumption,(~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))), introduced(assumption)).
% 0.67/1.02 tff(120,plain,
% 0.67/1.02 (^[B: $i, A: $i, C: $i] : refl((greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A))) <=> (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A))))),
% 0.67/1.02 inference(bind,[status(th)],[])).
% 0.67/1.02 tff(121,plain,
% 0.67/1.02 (![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A))) <=> ![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.02 inference(quant_intro,[status(thm)],[120])).
% 0.67/1.02 tff(122,plain,
% 0.67/1.02 (![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A))) <=> ![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.02 inference(rewrite,[status(thm)],[])).
% 0.67/1.02 tff(123,plain,
% 0.67/1.02 (^[B: $i, A: $i, C: $i] : trans(monotonicity(rewrite((((~organization(A)) | (~has_immunity(A, B))) | has_immunity(A, C)) <=> (has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))), (((((~organization(A)) | (~has_immunity(A, B))) | has_immunity(A, C)) | greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B))) <=> ((has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A))) | greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B))))), rewrite(((has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A))) | greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B))) <=> (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))), (((((~organization(A)) | (~has_immunity(A, B))) | has_immunity(A, C)) | greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B))) <=> (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))))),
% 0.67/1.02 inference(bind,[status(th)],[])).
% 0.67/1.02 tff(124,plain,
% 0.67/1.02 (![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~has_immunity(A, B))) | has_immunity(A, C)) | greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B))) <=> ![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.02 inference(quant_intro,[status(thm)],[123])).
% 0.67/1.02 tff(125,axiom,(![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~has_immunity(A, B))) | has_immunity(A, C)) | greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_3_46')).
% 0.67/1.02 tff(126,plain,
% 0.67/1.02 (![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.02 inference(modus_ponens,[status(thm)],[125, 124])).
% 0.67/1.02 tff(127,plain,
% 0.67/1.02 (![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.02 inference(modus_ponens,[status(thm)],[126, 122])).
% 0.67/1.02 tff(128,plain,(
% 0.67/1.02 ![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.02 inference(skolemize,[status(sab)],[127])).
% 0.67/1.02 tff(129,plain,
% 0.67/1.02 (![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.02 inference(modus_ponens,[status(thm)],[128, 121])).
% 0.67/1.02 tff(130,plain,
% 0.67/1.02 (((~![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))) | (greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | has_immunity(sk2, sk5))) <=> ((~![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))) | greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | has_immunity(sk2, sk5))),
% 0.67/1.02 inference(rewrite,[status(thm)],[])).
% 0.67/1.02 tff(131,plain,
% 0.67/1.02 ((greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)) | has_immunity(sk2, sk5) | (~has_immunity(sk2, sk4)) | (~organization(sk2))) <=> (greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | has_immunity(sk2, sk5))),
% 0.67/1.02 inference(rewrite,[status(thm)],[])).
% 0.67/1.02 tff(132,plain,
% 0.67/1.02 (((~![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))) | (greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)) | has_immunity(sk2, sk5) | (~has_immunity(sk2, sk4)) | (~organization(sk2)))) <=> ((~![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))) | (greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | has_immunity(sk2, sk5)))),
% 0.67/1.02 inference(monotonicity,[status(thm)],[131])).
% 0.67/1.02 tff(133,plain,
% 0.67/1.02 (((~![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))) | (greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)) | has_immunity(sk2, sk5) | (~has_immunity(sk2, sk4)) | (~organization(sk2)))) <=> ((~![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))) | greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | has_immunity(sk2, sk5))),
% 0.67/1.02 inference(transitivity,[status(thm)],[132, 130])).
% 0.67/1.02 tff(134,plain,
% 0.67/1.02 ((~![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))) | (greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)) | has_immunity(sk2, sk5) | (~has_immunity(sk2, sk4)) | (~organization(sk2)))),
% 0.67/1.02 inference(quant_inst,[status(thm)],[])).
% 0.67/1.02 tff(135,plain,
% 0.67/1.02 ((~![B: $i, A: $i, C: $i] : (greater(hazard_of_mortality(A, C), hazard_of_mortality(A, B)) | has_immunity(A, C) | (~has_immunity(A, B)) | (~organization(A)))) | greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | has_immunity(sk2, sk5)),
% 0.67/1.02 inference(modus_ponens,[status(thm)],[134, 133])).
% 0.67/1.02 tff(136,plain,
% 0.67/1.02 ($false),
% 0.67/1.02 inference(unit_resolution,[status(thm)],[135, 129, 10, 119, 118, 98])).
% 0.67/1.02 tff(137,plain,(greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))), inference(lemma,lemma(discharge,[]))).
% 0.67/1.02 tff(138,plain,
% 0.67/1.02 (zero = age(sk2, sk3)),
% 0.67/1.02 inference(symmetry,[status(thm)],[7])).
% 0.67/1.02 tff(139,plain,
% 0.67/1.02 (smaller_or_equal(zero, eta) <=> smaller_or_equal(age(sk2, sk3), eta)),
% 0.67/1.02 inference(monotonicity,[status(thm)],[138])).
% 0.67/1.02 tff(140,plain,
% 0.67/1.02 (greater(eta, zero) <=> greater(eta, zero)),
% 0.67/1.02 inference(rewrite,[status(thm)],[])).
% 0.67/1.02 tff(141,axiom,(greater(eta, zero)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma_8_67')).
% 0.67/1.02 tff(142,plain,
% 0.67/1.02 (greater(eta, zero)),
% 0.67/1.02 inference(modus_ponens,[status(thm)],[141, 140])).
% 0.67/1.02 tff(143,plain,
% 0.67/1.02 (^[B: $i, A: $i] : refl(((~greater(A, B)) | smaller(B, A)) <=> ((~greater(A, B)) | smaller(B, A)))),
% 0.67/1.02 inference(bind,[status(th)],[])).
% 0.67/1.02 tff(144,plain,
% 0.67/1.02 (![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A)) <=> ![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A))),
% 0.67/1.02 inference(quant_intro,[status(thm)],[143])).
% 0.67/1.02 tff(145,plain,
% 0.67/1.02 (![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A)) <=> ![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A))),
% 0.67/1.02 inference(rewrite,[status(thm)],[])).
% 0.67/1.02 tff(146,axiom,(![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax','definition_smaller_8')).
% 0.67/1.02 tff(147,plain,
% 0.67/1.02 (![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A))),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[146, 145])).
% 0.67/1.03 tff(148,plain,(
% 0.67/1.03 ![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A))),
% 0.67/1.03 inference(skolemize,[status(sab)],[147])).
% 0.67/1.03 tff(149,plain,
% 0.67/1.03 (![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A))),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[148, 144])).
% 0.67/1.03 tff(150,plain,
% 0.67/1.03 (((~![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A))) | ((~greater(eta, zero)) | smaller(zero, eta))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A))) | (~greater(eta, zero)) | smaller(zero, eta))),
% 0.67/1.03 inference(rewrite,[status(thm)],[])).
% 0.67/1.03 tff(151,plain,
% 0.67/1.03 ((~![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A))) | ((~greater(eta, zero)) | smaller(zero, eta))),
% 0.67/1.03 inference(quant_inst,[status(thm)],[])).
% 0.67/1.03 tff(152,plain,
% 0.67/1.03 ((~![B: $i, A: $i] : ((~greater(A, B)) | smaller(B, A))) | (~greater(eta, zero)) | smaller(zero, eta)),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[151, 150])).
% 0.67/1.03 tff(153,plain,
% 0.67/1.03 (smaller(zero, eta)),
% 0.67/1.03 inference(unit_resolution,[status(thm)],[152, 149, 142])).
% 0.67/1.03 tff(154,plain,
% 0.67/1.03 (^[B: $i, A: $i] : refl(((~smaller(A, B)) | smaller_or_equal(A, B)) <=> ((~smaller(A, B)) | smaller_or_equal(A, B)))),
% 0.67/1.03 inference(bind,[status(th)],[])).
% 0.67/1.03 tff(155,plain,
% 0.67/1.03 (![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B)) <=> ![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B))),
% 0.67/1.03 inference(quant_intro,[status(thm)],[154])).
% 0.67/1.03 tff(156,plain,
% 0.67/1.03 (![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B)) <=> ![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B))),
% 0.67/1.03 inference(rewrite,[status(thm)],[])).
% 0.67/1.03 tff(157,axiom,(![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax','definition_smaller_or_equal_2')).
% 0.67/1.03 tff(158,plain,
% 0.67/1.03 (![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B))),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[157, 156])).
% 0.67/1.03 tff(159,plain,(
% 0.67/1.03 ![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B))),
% 0.67/1.03 inference(skolemize,[status(sab)],[158])).
% 0.67/1.03 tff(160,plain,
% 0.67/1.03 (![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B))),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[159, 155])).
% 0.67/1.03 tff(161,plain,
% 0.67/1.03 (((~![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B))) | ((~smaller(zero, eta)) | smaller_or_equal(zero, eta))) <=> ((~![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B))) | (~smaller(zero, eta)) | smaller_or_equal(zero, eta))),
% 0.67/1.03 inference(rewrite,[status(thm)],[])).
% 0.67/1.03 tff(162,plain,
% 0.67/1.03 ((~![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B))) | ((~smaller(zero, eta)) | smaller_or_equal(zero, eta))),
% 0.67/1.03 inference(quant_inst,[status(thm)],[])).
% 0.67/1.03 tff(163,plain,
% 0.67/1.03 ((~![B: $i, A: $i] : ((~smaller(A, B)) | smaller_or_equal(A, B))) | (~smaller(zero, eta)) | smaller_or_equal(zero, eta)),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[162, 161])).
% 0.67/1.03 tff(164,plain,
% 0.67/1.03 (smaller_or_equal(zero, eta)),
% 0.67/1.03 inference(unit_resolution,[status(thm)],[163, 160, 153])).
% 0.67/1.03 tff(165,plain,
% 0.67/1.03 (smaller_or_equal(age(sk2, sk3), eta)),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[164, 139])).
% 0.67/1.03 tff(166,plain,
% 0.67/1.03 (((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | ((~has_endowment(sk2)) | has_immunity(sk2, sk3) | (~smaller_or_equal(age(sk2, sk3), eta)))) <=> ((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | (~has_endowment(sk2)) | has_immunity(sk2, sk3) | (~smaller_or_equal(age(sk2, sk3), eta)))),
% 0.67/1.03 inference(rewrite,[status(thm)],[])).
% 0.67/1.03 tff(167,plain,
% 0.67/1.03 ((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | ((~has_endowment(sk2)) | has_immunity(sk2, sk3) | (~smaller_or_equal(age(sk2, sk3), eta)))),
% 0.67/1.03 inference(quant_inst,[status(thm)],[])).
% 0.67/1.03 tff(168,plain,
% 0.67/1.03 ((~![B: $i, A: $i] : ((~has_endowment(A)) | has_immunity(A, B) | (~smaller_or_equal(age(A, B), eta)))) | (~has_endowment(sk2)) | has_immunity(sk2, sk3) | (~smaller_or_equal(age(sk2, sk3), eta))),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[167, 166])).
% 0.67/1.03 tff(169,plain,
% 0.67/1.03 (has_immunity(sk2, sk3) | (~smaller_or_equal(age(sk2, sk3), eta))),
% 0.67/1.03 inference(unit_resolution,[status(thm)],[168, 111, 77])).
% 0.67/1.03 tff(170,plain,
% 0.67/1.03 (has_immunity(sk2, sk3)),
% 0.67/1.03 inference(unit_resolution,[status(thm)],[169, 165])).
% 0.67/1.03 tff(171,assumption,(~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3))), introduced(assumption)).
% 0.67/1.03 tff(172,plain,
% 0.67/1.03 (^[B: $i, A: $i, C: $i] : refl(((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A))) <=> ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A))))),
% 0.67/1.03 inference(bind,[status(th)],[])).
% 0.67/1.03 tff(173,plain,
% 0.67/1.03 (![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A))) <=> ![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.03 inference(quant_intro,[status(thm)],[172])).
% 0.67/1.03 tff(174,plain,
% 0.67/1.03 (![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A))) <=> ![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.03 inference(rewrite,[status(thm)],[])).
% 0.67/1.03 tff(175,plain,
% 0.67/1.03 (^[B: $i, A: $i, C: $i] : trans(monotonicity(rewrite((((~organization(A)) | (~has_immunity(A, B))) | (~has_immunity(A, C))) <=> ((~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))), (((((~organization(A)) | (~has_immunity(A, B))) | (~has_immunity(A, C))) | (hazard_of_mortality(A, B) = hazard_of_mortality(A, C))) <=> (((~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A))) | (hazard_of_mortality(A, B) = hazard_of_mortality(A, C))))), rewrite((((~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A))) | (hazard_of_mortality(A, B) = hazard_of_mortality(A, C))) <=> ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))), (((((~organization(A)) | (~has_immunity(A, B))) | (~has_immunity(A, C))) | (hazard_of_mortality(A, B) = hazard_of_mortality(A, C))) <=> ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))))),
% 0.67/1.03 inference(bind,[status(th)],[])).
% 0.67/1.03 tff(176,plain,
% 0.67/1.03 (![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~has_immunity(A, B))) | (~has_immunity(A, C))) | (hazard_of_mortality(A, B) = hazard_of_mortality(A, C))) <=> ![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.03 inference(quant_intro,[status(thm)],[175])).
% 0.67/1.03 tff(177,axiom,(![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~has_immunity(A, B))) | (~has_immunity(A, C))) | (hazard_of_mortality(A, B) = hazard_of_mortality(A, C)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_2_45')).
% 0.67/1.03 tff(178,plain,
% 0.67/1.03 (![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[177, 176])).
% 0.67/1.03 tff(179,plain,
% 0.67/1.03 (![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[178, 174])).
% 0.67/1.03 tff(180,plain,(
% 0.67/1.03 ![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.03 inference(skolemize,[status(sab)],[179])).
% 0.67/1.03 tff(181,plain,
% 0.67/1.03 (![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))),
% 0.67/1.03 inference(modus_ponens,[status(thm)],[180, 173])).
% 0.67/1.03 tff(182,plain,
% 0.67/1.03 (((~![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))) | ((hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | (~has_immunity(sk2, sk3)))) <=> ((~![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))) | (hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | (~has_immunity(sk2, sk3)))),
% 0.80/1.03 inference(rewrite,[status(thm)],[])).
% 0.80/1.03 tff(183,plain,
% 0.80/1.03 (((hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)) | (~has_immunity(sk2, sk3)) | (~has_immunity(sk2, sk4)) | (~organization(sk2))) <=> ((hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | (~has_immunity(sk2, sk3)))),
% 0.80/1.03 inference(rewrite,[status(thm)],[])).
% 0.80/1.03 tff(184,plain,
% 0.80/1.03 (((~![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))) | ((hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)) | (~has_immunity(sk2, sk3)) | (~has_immunity(sk2, sk4)) | (~organization(sk2)))) <=> ((~![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))) | ((hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | (~has_immunity(sk2, sk3))))),
% 0.80/1.03 inference(monotonicity,[status(thm)],[183])).
% 0.80/1.03 tff(185,plain,
% 0.80/1.03 (((~![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))) | ((hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)) | (~has_immunity(sk2, sk3)) | (~has_immunity(sk2, sk4)) | (~organization(sk2)))) <=> ((~![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))) | (hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | (~has_immunity(sk2, sk3)))),
% 0.80/1.03 inference(transitivity,[status(thm)],[184, 182])).
% 0.80/1.03 tff(186,plain,
% 0.80/1.03 ((~![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))) | ((hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)) | (~has_immunity(sk2, sk3)) | (~has_immunity(sk2, sk4)) | (~organization(sk2)))),
% 0.80/1.03 inference(quant_inst,[status(thm)],[])).
% 0.80/1.03 tff(187,plain,
% 0.80/1.03 ((~![B: $i, A: $i, C: $i] : ((hazard_of_mortality(A, B) = hazard_of_mortality(A, C)) | (~has_immunity(A, C)) | (~has_immunity(A, B)) | (~organization(A)))) | (hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)) | (~organization(sk2)) | (~has_immunity(sk2, sk4)) | (~has_immunity(sk2, sk3))),
% 0.80/1.03 inference(modus_ponens,[status(thm)],[186, 185])).
% 0.80/1.03 tff(188,plain,
% 0.80/1.03 ($false),
% 0.80/1.03 inference(unit_resolution,[status(thm)],[187, 181, 10, 171, 170, 118])).
% 0.80/1.03 tff(189,plain,(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)), inference(lemma,lemma(discharge,[]))).
% 0.80/1.03 tff(190,plain,
% 0.80/1.03 (((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)))) <=> ((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3))))),
% 0.80/1.03 inference(rewrite,[status(thm)],[])).
% 0.80/1.03 tff(191,plain,
% 0.80/1.03 ((((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)))) <=> ((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3))))),
% 0.80/1.04 inference(rewrite,[status(thm)],[])).
% 0.80/1.04 tff(192,plain,
% 0.80/1.04 (((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)))) <=> ((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))))),
% 0.80/1.04 inference(rewrite,[status(thm)],[])).
% 0.80/1.04 tff(193,plain,
% 0.80/1.04 ((((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)))) <=> (((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3))))),
% 0.80/1.04 inference(monotonicity,[status(thm)],[192])).
% 0.80/1.04 tff(194,plain,
% 0.80/1.04 ((((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)))) <=> ((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3))))),
% 0.80/1.04 inference(transitivity,[status(thm)],[193, 191])).
% 0.80/1.04 tff(195,axiom,(((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma_8_68')).
% 0.80/1.04 tff(196,plain,
% 0.80/1.04 ((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)))),
% 0.80/1.04 inference(modus_ponens,[status(thm)],[195, 194])).
% 0.80/1.04 tff(197,plain,
% 0.80/1.04 ((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)))),
% 0.80/1.04 inference(modus_ponens,[status(thm)],[196, 190])).
% 0.80/1.04 tff(198,plain,
% 0.80/1.04 ((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)))),
% 0.80/1.04 inference(modus_ponens,[status(thm)],[197, 190])).
% 0.80/1.04 tff(199,plain,
% 0.80/1.04 ((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)))),
% 0.80/1.04 inference(modus_ponens,[status(thm)],[198, 190])).
% 0.80/1.04 tff(200,plain,
% 0.80/1.04 ((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4))) | (~(hazard_of_mortality(sk2, sk4) = hazard_of_mortality(sk2, sk3)))),
% 0.80/1.04 inference(modus_ponens,[status(thm)],[199, 190])).
% 0.80/1.04 tff(201,plain,
% 0.80/1.04 ((~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))) | (~greater(hazard_of_mortality(sk2, sk5), hazard_of_mortality(sk2, sk4)))),
% 0.80/1.04 inference(unit_resolution,[status(thm)],[200, 189])).
% 0.80/1.04 tff(202,plain,
% 0.80/1.04 (~greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5))),
% 0.80/1.04 inference(unit_resolution,[status(thm)],[201, 137])).
% 0.80/1.04 tff(203,plain,
% 0.80/1.04 (^[B: $i, A: $i, C: $i] : refl((has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B)))) <=> (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B)))))),
% 0.80/1.04 inference(bind,[status(th)],[])).
% 0.80/1.04 tff(204,plain,
% 0.80/1.04 (![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B)))) <=> ![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))),
% 0.80/1.04 inference(quant_intro,[status(thm)],[203])).
% 0.80/1.04 tff(205,plain,
% 0.80/1.04 (![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B)))) <=> ![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))),
% 0.80/1.04 inference(rewrite,[status(thm)],[])).
% 0.80/1.04 tff(206,plain,
% 0.80/1.04 (^[B: $i, A: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((((~organization(A)) | has_immunity(A, B)) | has_immunity(A, C)) <=> (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)))), (((((~organization(A)) | has_immunity(A, B)) | has_immunity(A, C)) | (~greater(capability(A, C), capability(A, B)))) <=> ((has_immunity(A, C) | has_immunity(A, B) | (~organization(A))) | (~greater(capability(A, C), capability(A, B)))))), rewrite(((has_immunity(A, C) | has_immunity(A, B) | (~organization(A))) | (~greater(capability(A, C), capability(A, B)))) <=> (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | (~greater(capability(A, C), capability(A, B))))), (((((~organization(A)) | has_immunity(A, B)) | has_immunity(A, C)) | (~greater(capability(A, C), capability(A, B)))) <=> (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | (~greater(capability(A, C), capability(A, B)))))), ((((((~organization(A)) | has_immunity(A, B)) | has_immunity(A, C)) | (~greater(capability(A, C), capability(A, B)))) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C))) <=> ((has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | (~greater(capability(A, C), capability(A, B)))) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C))))), rewrite(((has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | (~greater(capability(A, C), capability(A, B)))) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C))) <=> (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))), ((((((~organization(A)) | has_immunity(A, B)) | has_immunity(A, C)) | (~greater(capability(A, C), capability(A, B)))) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C))) <=> (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))))),
% 0.80/1.04 inference(bind,[status(th)],[])).
% 0.80/1.04 tff(207,plain,
% 0.80/1.04 (![B: $i, A: $i, C: $i] : (((((~organization(A)) | has_immunity(A, B)) | has_immunity(A, C)) | (~greater(capability(A, C), capability(A, B)))) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C))) <=> ![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))),
% 0.80/1.04 inference(quant_intro,[status(thm)],[206])).
% 0.80/1.04 tff(208,axiom,(![B: $i, A: $i, C: $i] : (((((~organization(A)) | has_immunity(A, B)) | has_immunity(A, C)) | (~greater(capability(A, C), capability(A, B)))) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_16_58')).
% 0.80/1.04 tff(209,plain,
% 0.80/1.04 (![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))),
% 0.80/1.05 inference(modus_ponens,[status(thm)],[208, 207])).
% 0.80/1.05 tff(210,plain,
% 0.80/1.05 (![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))),
% 0.80/1.05 inference(modus_ponens,[status(thm)],[209, 205])).
% 0.80/1.05 tff(211,plain,(
% 0.80/1.05 ![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))),
% 0.80/1.05 inference(skolemize,[status(sab)],[210])).
% 0.80/1.05 tff(212,plain,
% 0.80/1.05 (![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))),
% 0.80/1.05 inference(modus_ponens,[status(thm)],[211, 204])).
% 0.80/1.05 tff(213,plain,
% 0.80/1.05 (((~![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))) | (greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5)) | (~organization(sk2)) | has_immunity(sk2, sk5) | has_immunity(sk2, sk6) | (~greater(capability(sk2, sk5), capability(sk2, sk6))))) <=> ((~![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))) | greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5)) | (~organization(sk2)) | has_immunity(sk2, sk5) | has_immunity(sk2, sk6) | (~greater(capability(sk2, sk5), capability(sk2, sk6))))),
% 0.80/1.05 inference(rewrite,[status(thm)],[])).
% 0.80/1.05 tff(214,plain,
% 0.80/1.05 ((has_immunity(sk2, sk5) | has_immunity(sk2, sk6) | (~organization(sk2)) | greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5)) | (~greater(capability(sk2, sk5), capability(sk2, sk6)))) <=> (greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5)) | (~organization(sk2)) | has_immunity(sk2, sk5) | has_immunity(sk2, sk6) | (~greater(capability(sk2, sk5), capability(sk2, sk6))))),
% 0.80/1.05 inference(rewrite,[status(thm)],[])).
% 0.80/1.05 tff(215,plain,
% 0.80/1.05 (((~![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))) | (has_immunity(sk2, sk5) | has_immunity(sk2, sk6) | (~organization(sk2)) | greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5)) | (~greater(capability(sk2, sk5), capability(sk2, sk6))))) <=> ((~![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))) | (greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5)) | (~organization(sk2)) | has_immunity(sk2, sk5) | has_immunity(sk2, sk6) | (~greater(capability(sk2, sk5), capability(sk2, sk6)))))),
% 0.80/1.05 inference(monotonicity,[status(thm)],[214])).
% 0.80/1.05 tff(216,plain,
% 0.80/1.05 (((~![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))) | (has_immunity(sk2, sk5) | has_immunity(sk2, sk6) | (~organization(sk2)) | greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5)) | (~greater(capability(sk2, sk5), capability(sk2, sk6))))) <=> ((~![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))) | greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5)) | (~organization(sk2)) | has_immunity(sk2, sk5) | has_immunity(sk2, sk6) | (~greater(capability(sk2, sk5), capability(sk2, sk6))))),
% 0.80/1.05 inference(transitivity,[status(thm)],[215, 213])).
% 0.80/1.05 tff(217,plain,
% 0.80/1.05 ((~![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))) | (has_immunity(sk2, sk5) | has_immunity(sk2, sk6) | (~organization(sk2)) | greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5)) | (~greater(capability(sk2, sk5), capability(sk2, sk6))))),
% 0.80/1.05 inference(quant_inst,[status(thm)],[])).
% 0.80/1.05 tff(218,plain,
% 0.80/1.05 ((~![B: $i, A: $i, C: $i] : (has_immunity(A, C) | has_immunity(A, B) | (~organization(A)) | greater(hazard_of_mortality(A, B), hazard_of_mortality(A, C)) | (~greater(capability(A, C), capability(A, B))))) | greater(hazard_of_mortality(sk2, sk6), hazard_of_mortality(sk2, sk5)) | (~organization(sk2)) | has_immunity(sk2, sk5) | has_immunity(sk2, sk6) | (~greater(capability(sk2, sk5), capability(sk2, sk6)))),
% 0.80/1.05 inference(modus_ponens,[status(thm)],[217, 216])).
% 0.80/1.05 tff(219,plain,
% 0.80/1.05 (~greater(capability(sk2, sk5), capability(sk2, sk6))),
% 0.80/1.05 inference(unit_resolution,[status(thm)],[218, 212, 10, 202, 98, 91])).
% 0.80/1.05 tff(220,plain,
% 0.80/1.05 (^[B: $i, A: $i, C: $i] : refl((is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C))) <=> (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C))))),
% 0.80/1.05 inference(bind,[status(th)],[])).
% 0.80/1.05 tff(221,plain,
% 0.80/1.05 (![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C))) <=> ![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))),
% 0.80/1.05 inference(quant_intro,[status(thm)],[220])).
% 0.80/1.05 tff(222,plain,
% 0.80/1.05 (![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C))) <=> ![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))),
% 0.80/1.05 inference(rewrite,[status(thm)],[])).
% 0.80/1.05 tff(223,plain,
% 0.80/1.05 (^[B: $i, A: $i, C: $i] : trans(monotonicity(rewrite((((~organization(A)) | (~is_aligned(A, B))) | is_aligned(A, C)) <=> (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))), (((((~organization(A)) | (~is_aligned(A, B))) | is_aligned(A, C)) | greater(capability(A, B), capability(A, C))) <=> ((is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B))) | greater(capability(A, B), capability(A, C))))), rewrite(((is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B))) | greater(capability(A, B), capability(A, C))) <=> (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))), (((((~organization(A)) | (~is_aligned(A, B))) | is_aligned(A, C)) | greater(capability(A, B), capability(A, C))) <=> (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))))),
% 0.80/1.05 inference(bind,[status(th)],[])).
% 0.80/1.05 tff(224,plain,
% 0.80/1.05 (![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~is_aligned(A, B))) | is_aligned(A, C)) | greater(capability(A, B), capability(A, C))) <=> ![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))),
% 0.80/1.05 inference(quant_intro,[status(thm)],[223])).
% 0.80/1.05 tff(225,axiom,(![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~is_aligned(A, B))) | is_aligned(A, C)) | greater(capability(A, B), capability(A, C)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_14_55')).
% 0.80/1.05 tff(226,plain,
% 0.80/1.05 (![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))),
% 0.80/1.05 inference(modus_ponens,[status(thm)],[225, 224])).
% 0.80/1.05 tff(227,plain,
% 0.80/1.05 (![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))),
% 0.80/1.05 inference(modus_ponens,[status(thm)],[226, 222])).
% 0.80/1.05 tff(228,plain,(
% 0.80/1.05 ![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))),
% 0.80/1.05 inference(skolemize,[status(sab)],[227])).
% 0.80/1.05 tff(229,plain,
% 0.80/1.05 (![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))),
% 0.80/1.05 inference(modus_ponens,[status(thm)],[228, 221])).
% 0.80/1.05 tff(230,plain,
% 0.80/1.05 (((~![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))) | ((~organization(sk2)) | is_aligned(sk2, sk6) | greater(capability(sk2, sk5), capability(sk2, sk6)) | (~is_aligned(sk2, sk5)))) <=> ((~![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))) | (~organization(sk2)) | is_aligned(sk2, sk6) | greater(capability(sk2, sk5), capability(sk2, sk6)) | (~is_aligned(sk2, sk5)))),
% 0.80/1.05 inference(rewrite,[status(thm)],[])).
% 0.80/1.05 tff(231,plain,
% 0.80/1.05 ((is_aligned(sk2, sk6) | (~organization(sk2)) | (~is_aligned(sk2, sk5)) | greater(capability(sk2, sk5), capability(sk2, sk6))) <=> ((~organization(sk2)) | is_aligned(sk2, sk6) | greater(capability(sk2, sk5), capability(sk2, sk6)) | (~is_aligned(sk2, sk5)))),
% 0.80/1.05 inference(rewrite,[status(thm)],[])).
% 0.80/1.05 tff(232,plain,
% 0.80/1.05 (((~![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))) | (is_aligned(sk2, sk6) | (~organization(sk2)) | (~is_aligned(sk2, sk5)) | greater(capability(sk2, sk5), capability(sk2, sk6)))) <=> ((~![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))) | ((~organization(sk2)) | is_aligned(sk2, sk6) | greater(capability(sk2, sk5), capability(sk2, sk6)) | (~is_aligned(sk2, sk5))))),
% 0.80/1.05 inference(monotonicity,[status(thm)],[231])).
% 0.80/1.05 tff(233,plain,
% 0.80/1.05 (((~![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))) | (is_aligned(sk2, sk6) | (~organization(sk2)) | (~is_aligned(sk2, sk5)) | greater(capability(sk2, sk5), capability(sk2, sk6)))) <=> ((~![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))) | (~organization(sk2)) | is_aligned(sk2, sk6) | greater(capability(sk2, sk5), capability(sk2, sk6)) | (~is_aligned(sk2, sk5)))),
% 0.80/1.05 inference(transitivity,[status(thm)],[232, 230])).
% 0.80/1.05 tff(234,plain,
% 0.80/1.05 ((~![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))) | (is_aligned(sk2, sk6) | (~organization(sk2)) | (~is_aligned(sk2, sk5)) | greater(capability(sk2, sk5), capability(sk2, sk6)))),
% 0.80/1.05 inference(quant_inst,[status(thm)],[])).
% 0.80/1.05 tff(235,plain,
% 0.80/1.05 ((~![B: $i, A: $i, C: $i] : (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)) | greater(capability(A, B), capability(A, C)))) | (~organization(sk2)) | is_aligned(sk2, sk6) | greater(capability(sk2, sk5), capability(sk2, sk6)) | (~is_aligned(sk2, sk5))),
% 0.80/1.05 inference(modus_ponens,[status(thm)],[234, 233])).
% 0.80/1.05 tff(236,plain,
% 0.80/1.05 (is_aligned(sk2, sk6) | (~is_aligned(sk2, sk5))),
% 0.80/1.05 inference(unit_resolution,[status(thm)],[235, 229, 10, 219])).
% 0.80/1.05 tff(237,plain,
% 0.80/1.05 (~is_aligned(sk2, sk5)),
% 0.80/1.05 inference(unit_resolution,[status(thm)],[236, 58])).
% 0.80/1.05 tff(238,plain,
% 0.80/1.05 (^[B: $i, A: $i, C: $i] : refl((dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B))) <=> (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B))))),
% 0.80/1.05 inference(bind,[status(th)],[])).
% 0.80/1.05 tff(239,plain,
% 0.80/1.05 (![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B))) <=> ![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))),
% 0.80/1.05 inference(quant_intro,[status(thm)],[238])).
% 0.80/1.05 tff(240,plain,
% 0.80/1.05 (![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B))) <=> ![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))),
% 0.80/1.06 inference(rewrite,[status(thm)],[])).
% 0.80/1.06 tff(241,plain,
% 0.80/1.06 (^[B: $i, A: $i, C: $i] : trans(monotonicity(rewrite((((~organization(A)) | (~is_aligned(A, B))) | is_aligned(A, C)) <=> (is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))), (((((~organization(A)) | (~is_aligned(A, B))) | is_aligned(A, C)) | dissimilar(A, B, C)) <=> ((is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B))) | dissimilar(A, B, C)))), rewrite(((is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B))) | dissimilar(A, B, C)) <=> (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))), (((((~organization(A)) | (~is_aligned(A, B))) | is_aligned(A, C)) | dissimilar(A, B, C)) <=> (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))))),
% 0.80/1.06 inference(bind,[status(th)],[])).
% 0.80/1.06 tff(242,plain,
% 0.80/1.06 (![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~is_aligned(A, B))) | is_aligned(A, C)) | dissimilar(A, B, C)) <=> ![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))),
% 0.80/1.06 inference(quant_intro,[status(thm)],[241])).
% 0.80/1.06 tff(243,axiom,(![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~is_aligned(A, B))) | is_aligned(A, C)) | dissimilar(A, B, C))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','definition_2_51')).
% 0.80/1.06 tff(244,plain,
% 0.80/1.06 (![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))),
% 0.80/1.06 inference(modus_ponens,[status(thm)],[243, 242])).
% 0.80/1.06 tff(245,plain,
% 0.80/1.06 (![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))),
% 0.80/1.06 inference(modus_ponens,[status(thm)],[244, 240])).
% 0.80/1.06 tff(246,plain,(
% 0.80/1.06 ![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))),
% 0.80/1.06 inference(skolemize,[status(sab)],[245])).
% 0.80/1.06 tff(247,plain,
% 0.80/1.06 (![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))),
% 0.80/1.06 inference(modus_ponens,[status(thm)],[246, 239])).
% 0.80/1.06 tff(248,plain,
% 0.80/1.06 (((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))) | ((~organization(sk2)) | is_aligned(sk2, sk5) | (~is_aligned(sk2, sk3)) | dissimilar(sk2, sk3, sk5))) <=> ((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))) | (~organization(sk2)) | is_aligned(sk2, sk5) | (~is_aligned(sk2, sk3)) | dissimilar(sk2, sk3, sk5))),
% 0.80/1.06 inference(rewrite,[status(thm)],[])).
% 0.80/1.06 tff(249,plain,
% 0.80/1.06 ((dissimilar(sk2, sk3, sk5) | is_aligned(sk2, sk5) | (~organization(sk2)) | (~is_aligned(sk2, sk3))) <=> ((~organization(sk2)) | is_aligned(sk2, sk5) | (~is_aligned(sk2, sk3)) | dissimilar(sk2, sk3, sk5))),
% 0.80/1.06 inference(rewrite,[status(thm)],[])).
% 0.80/1.06 tff(250,plain,
% 0.80/1.06 (((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))) | (dissimilar(sk2, sk3, sk5) | is_aligned(sk2, sk5) | (~organization(sk2)) | (~is_aligned(sk2, sk3)))) <=> ((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))) | ((~organization(sk2)) | is_aligned(sk2, sk5) | (~is_aligned(sk2, sk3)) | dissimilar(sk2, sk3, sk5)))),
% 0.80/1.06 inference(monotonicity,[status(thm)],[249])).
% 0.80/1.06 tff(251,plain,
% 0.80/1.06 (((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))) | (dissimilar(sk2, sk3, sk5) | is_aligned(sk2, sk5) | (~organization(sk2)) | (~is_aligned(sk2, sk3)))) <=> ((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))) | (~organization(sk2)) | is_aligned(sk2, sk5) | (~is_aligned(sk2, sk3)) | dissimilar(sk2, sk3, sk5))),
% 0.80/1.06 inference(transitivity,[status(thm)],[250, 248])).
% 0.80/1.06 tff(252,plain,
% 0.80/1.06 ((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))) | (dissimilar(sk2, sk3, sk5) | is_aligned(sk2, sk5) | (~organization(sk2)) | (~is_aligned(sk2, sk3)))),
% 0.80/1.06 inference(quant_inst,[status(thm)],[])).
% 0.80/1.06 tff(253,plain,
% 0.80/1.06 ((~![B: $i, A: $i, C: $i] : (dissimilar(A, B, C) | is_aligned(A, C) | (~organization(A)) | (~is_aligned(A, B)))) | (~organization(sk2)) | is_aligned(sk2, sk5) | (~is_aligned(sk2, sk3)) | dissimilar(sk2, sk3, sk5)),
% 0.80/1.06 inference(modus_ponens,[status(thm)],[252, 251])).
% 0.80/1.06 tff(254,plain,
% 0.80/1.06 ($false),
% 0.80/1.06 inference(unit_resolution,[status(thm)],[253, 247, 10, 41, 237, 1])).
% 0.80/1.06 tff(255,plain,(dissimilar(sk2, sk3, sk5)), inference(lemma,lemma(discharge,[]))).
% 0.80/1.06 tff(256,plain,
% 0.80/1.06 (^[B: $i, A: $i, C: $i] : refl(((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero))) <=> ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero))))),
% 0.80/1.06 inference(bind,[status(th)],[])).
% 0.80/1.06 tff(257,plain,
% 0.80/1.06 (![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero))) <=> ![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))),
% 0.80/1.06 inference(quant_intro,[status(thm)],[256])).
% 0.80/1.06 tff(258,plain,
% 0.80/1.06 (![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero))) <=> ![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))),
% 0.80/1.06 inference(rewrite,[status(thm)],[])).
% 0.80/1.06 tff(259,plain,
% 0.80/1.06 (^[B: $i, A: $i, C: $i] : trans(monotonicity(rewrite((((~organization(A)) | (~(age(A, B) = zero))) | (~dissimilar(A, B, C))) <=> ((~dissimilar(A, B, C)) | (~organization(A)) | (~(age(A, B) = zero)))), (((((~organization(A)) | (~(age(A, B) = zero))) | (~dissimilar(A, B, C))) | greater(age(A, C), sigma)) <=> (((~dissimilar(A, B, C)) | (~organization(A)) | (~(age(A, B) = zero))) | greater(age(A, C), sigma)))), rewrite((((~dissimilar(A, B, C)) | (~organization(A)) | (~(age(A, B) = zero))) | greater(age(A, C), sigma)) <=> ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))), (((((~organization(A)) | (~(age(A, B) = zero))) | (~dissimilar(A, B, C))) | greater(age(A, C), sigma)) <=> ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))))),
% 0.80/1.06 inference(bind,[status(th)],[])).
% 0.80/1.06 tff(260,plain,
% 0.80/1.06 (![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~(age(A, B) = zero))) | (~dissimilar(A, B, C))) | greater(age(A, C), sigma)) <=> ![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))),
% 0.80/1.06 inference(quant_intro,[status(thm)],[259])).
% 0.80/1.06 tff(261,axiom,(![B: $i, A: $i, C: $i] : ((((~organization(A)) | (~(age(A, B) = zero))) | (~dissimilar(A, B, C))) | greater(age(A, C), sigma))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','assumption_15_57')).
% 0.80/1.06 tff(262,plain,
% 0.80/1.06 (![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))),
% 0.80/1.06 inference(modus_ponens,[status(thm)],[261, 260])).
% 0.80/1.06 tff(263,plain,
% 0.80/1.06 (![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))),
% 0.80/1.06 inference(modus_ponens,[status(thm)],[262, 258])).
% 0.80/1.06 tff(264,plain,(
% 0.80/1.06 ![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))),
% 0.80/1.06 inference(skolemize,[status(sab)],[263])).
% 0.80/1.06 tff(265,plain,
% 0.80/1.06 (![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))),
% 0.80/1.06 inference(modus_ponens,[status(thm)],[264, 257])).
% 0.80/1.06 tff(266,plain,
% 0.80/1.06 (((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))) | ((~organization(sk2)) | (~(age(sk2, sk3) = zero)) | greater(age(sk2, sk5), sigma) | (~dissimilar(sk2, sk3, sk5)))) <=> ((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))) | (~organization(sk2)) | (~(age(sk2, sk3) = zero)) | greater(age(sk2, sk5), sigma) | (~dissimilar(sk2, sk3, sk5)))),
% 0.80/1.07 inference(rewrite,[status(thm)],[])).
% 0.80/1.07 tff(267,plain,
% 0.80/1.07 (((~dissimilar(sk2, sk3, sk5)) | (~organization(sk2)) | greater(age(sk2, sk5), sigma) | (~(age(sk2, sk3) = zero))) <=> ((~organization(sk2)) | (~(age(sk2, sk3) = zero)) | greater(age(sk2, sk5), sigma) | (~dissimilar(sk2, sk3, sk5)))),
% 0.80/1.07 inference(rewrite,[status(thm)],[])).
% 0.80/1.07 tff(268,plain,
% 0.80/1.07 (((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))) | ((~dissimilar(sk2, sk3, sk5)) | (~organization(sk2)) | greater(age(sk2, sk5), sigma) | (~(age(sk2, sk3) = zero)))) <=> ((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))) | ((~organization(sk2)) | (~(age(sk2, sk3) = zero)) | greater(age(sk2, sk5), sigma) | (~dissimilar(sk2, sk3, sk5))))),
% 0.80/1.07 inference(monotonicity,[status(thm)],[267])).
% 0.80/1.07 tff(269,plain,
% 0.80/1.07 (((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))) | ((~dissimilar(sk2, sk3, sk5)) | (~organization(sk2)) | greater(age(sk2, sk5), sigma) | (~(age(sk2, sk3) = zero)))) <=> ((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))) | (~organization(sk2)) | (~(age(sk2, sk3) = zero)) | greater(age(sk2, sk5), sigma) | (~dissimilar(sk2, sk3, sk5)))),
% 0.80/1.07 inference(transitivity,[status(thm)],[268, 266])).
% 0.80/1.07 tff(270,plain,
% 0.80/1.07 ((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))) | ((~dissimilar(sk2, sk3, sk5)) | (~organization(sk2)) | greater(age(sk2, sk5), sigma) | (~(age(sk2, sk3) = zero)))),
% 0.80/1.07 inference(quant_inst,[status(thm)],[])).
% 0.80/1.07 tff(271,plain,
% 0.80/1.07 ((~![B: $i, A: $i, C: $i] : ((~dissimilar(A, B, C)) | (~organization(A)) | greater(age(A, C), sigma) | (~(age(A, B) = zero)))) | (~organization(sk2)) | (~(age(sk2, sk3) = zero)) | greater(age(sk2, sk5), sigma) | (~dissimilar(sk2, sk3, sk5))),
% 0.80/1.07 inference(modus_ponens,[status(thm)],[270, 269])).
% 0.80/1.07 tff(272,plain,
% 0.80/1.07 (greater(age(sk2, sk5), sigma) | (~dissimilar(sk2, sk3, sk5))),
% 0.80/1.07 inference(unit_resolution,[status(thm)],[271, 265, 10, 7])).
% 0.80/1.07 tff(273,plain,
% 0.80/1.07 (greater(age(sk2, sk5), sigma)),
% 0.80/1.07 inference(unit_resolution,[status(thm)],[272, 255])).
% 0.80/1.07 tff(274,plain,
% 0.80/1.07 (^[B: $i, A: $i] : refl(((~greater(A, B)) | (~greater(B, A))) <=> ((~greater(A, B)) | (~greater(B, A))))),
% 0.80/1.07 inference(bind,[status(th)],[])).
% 0.80/1.07 tff(275,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A))) <=> ![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A)))),
% 0.80/1.07 inference(quant_intro,[status(thm)],[274])).
% 0.80/1.07 tff(276,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A))) <=> ![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A)))),
% 0.80/1.07 inference(rewrite,[status(thm)],[])).
% 0.80/1.07 tff(277,axiom,(![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A)))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax','meaning_postulate_greater_strict_9')).
% 0.80/1.07 tff(278,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A)))),
% 0.80/1.07 inference(modus_ponens,[status(thm)],[277, 276])).
% 0.80/1.07 tff(279,plain,(
% 0.80/1.07 ![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A)))),
% 0.80/1.07 inference(skolemize,[status(sab)],[278])).
% 0.80/1.07 tff(280,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A)))),
% 0.80/1.07 inference(modus_ponens,[status(thm)],[279, 275])).
% 0.80/1.07 tff(281,plain,
% 0.80/1.07 (((~![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A)))) | ((~greater(sigma, age(sk2, sk5))) | (~greater(age(sk2, sk5), sigma)))) <=> ((~![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A)))) | (~greater(sigma, age(sk2, sk5))) | (~greater(age(sk2, sk5), sigma)))),
% 0.80/1.07 inference(rewrite,[status(thm)],[])).
% 0.80/1.07 tff(282,plain,
% 0.80/1.07 ((~![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A)))) | ((~greater(sigma, age(sk2, sk5))) | (~greater(age(sk2, sk5), sigma)))),
% 0.80/1.07 inference(quant_inst,[status(thm)],[])).
% 0.80/1.07 tff(283,plain,
% 0.80/1.07 ((~![B: $i, A: $i] : ((~greater(A, B)) | (~greater(B, A)))) | (~greater(sigma, age(sk2, sk5))) | (~greater(age(sk2, sk5), sigma))),
% 0.80/1.07 inference(modus_ponens,[status(thm)],[282, 281])).
% 0.80/1.07 tff(284,plain,
% 0.80/1.07 (~greater(sigma, age(sk2, sk5))),
% 0.80/1.07 inference(unit_resolution,[status(thm)],[283, 280, 273])).
% 0.80/1.07 tff(285,plain,
% 0.80/1.07 (^[B: $i, A: $i] : refl(((~smaller(A, B)) | greater(B, A)) <=> ((~smaller(A, B)) | greater(B, A)))),
% 0.80/1.07 inference(bind,[status(th)],[])).
% 0.80/1.07 tff(286,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A)) <=> ![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A))),
% 0.80/1.07 inference(quant_intro,[status(thm)],[285])).
% 0.80/1.07 tff(287,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A)) <=> ![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A))),
% 0.80/1.07 inference(rewrite,[status(thm)],[])).
% 0.80/1.07 tff(288,axiom,(![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax','definition_smaller_7')).
% 0.80/1.07 tff(289,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A))),
% 0.80/1.07 inference(modus_ponens,[status(thm)],[288, 287])).
% 0.80/1.07 tff(290,plain,(
% 0.80/1.07 ![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A))),
% 0.80/1.07 inference(skolemize,[status(sab)],[289])).
% 0.80/1.07 tff(291,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A))),
% 0.80/1.07 inference(modus_ponens,[status(thm)],[290, 286])).
% 0.80/1.07 tff(292,plain,
% 0.80/1.07 (((~![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A))) | ((~smaller(age(sk2, sk5), sigma)) | greater(sigma, age(sk2, sk5)))) <=> ((~![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A))) | (~smaller(age(sk2, sk5), sigma)) | greater(sigma, age(sk2, sk5)))),
% 0.80/1.07 inference(rewrite,[status(thm)],[])).
% 0.80/1.07 tff(293,plain,
% 0.80/1.07 ((~![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A))) | ((~smaller(age(sk2, sk5), sigma)) | greater(sigma, age(sk2, sk5)))),
% 0.80/1.07 inference(quant_inst,[status(thm)],[])).
% 0.80/1.07 tff(294,plain,
% 0.80/1.07 ((~![B: $i, A: $i] : ((~smaller(A, B)) | greater(B, A))) | (~smaller(age(sk2, sk5), sigma)) | greater(sigma, age(sk2, sk5))),
% 0.80/1.07 inference(modus_ponens,[status(thm)],[293, 292])).
% 0.80/1.07 tff(295,plain,
% 0.80/1.07 (~smaller(age(sk2, sk5), sigma)),
% 0.80/1.07 inference(unit_resolution,[status(thm)],[294, 291, 284])).
% 0.80/1.07 tff(296,plain,
% 0.80/1.07 (smaller_or_equal(age(sk2, sk5), sigma) <=> smaller_or_equal(age(sk2, sk5), sigma)),
% 0.80/1.07 inference(rewrite,[status(thm)],[])).
% 0.80/1.07 tff(297,axiom,(smaller_or_equal(age(sk2, sk5), sigma)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma_8_64')).
% 0.80/1.07 tff(298,plain,
% 0.80/1.07 (smaller_or_equal(age(sk2, sk5), sigma)),
% 0.80/1.07 inference(modus_ponens,[status(thm)],[297, 296])).
% 0.80/1.07 tff(299,plain,
% 0.80/1.07 (^[B: $i, A: $i] : refl(((A = B) | smaller(A, B) | (~smaller_or_equal(A, B))) <=> ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B))))),
% 0.80/1.07 inference(bind,[status(th)],[])).
% 0.80/1.07 tff(300,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B))) <=> ![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))),
% 0.80/1.07 inference(quant_intro,[status(thm)],[299])).
% 0.80/1.07 tff(301,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B))) <=> ![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))),
% 0.80/1.07 inference(rewrite,[status(thm)],[])).
% 0.80/1.07 tff(302,plain,
% 0.80/1.07 (^[B: $i, A: $i] : rewrite((((~smaller_or_equal(A, B)) | smaller(A, B)) | (A = B)) <=> ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B))))),
% 0.80/1.07 inference(bind,[status(th)],[])).
% 0.80/1.07 tff(303,plain,
% 0.80/1.07 (![B: $i, A: $i] : (((~smaller_or_equal(A, B)) | smaller(A, B)) | (A = B)) <=> ![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))),
% 0.80/1.07 inference(quant_intro,[status(thm)],[302])).
% 0.80/1.07 tff(304,axiom,(![B: $i, A: $i] : (((~smaller_or_equal(A, B)) | smaller(A, B)) | (A = B))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax','definition_smaller_or_equal_1')).
% 0.80/1.07 tff(305,plain,
% 0.80/1.07 (![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))),
% 0.80/1.07 inference(modus_ponens,[status(thm)],[304, 303])).
% 0.80/1.08 tff(306,plain,
% 0.80/1.08 (![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))),
% 0.80/1.08 inference(modus_ponens,[status(thm)],[305, 301])).
% 0.80/1.08 tff(307,plain,(
% 0.80/1.08 ![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))),
% 0.80/1.08 inference(skolemize,[status(sab)],[306])).
% 0.80/1.08 tff(308,plain,
% 0.80/1.08 (![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))),
% 0.80/1.08 inference(modus_ponens,[status(thm)],[307, 300])).
% 0.80/1.08 tff(309,plain,
% 0.80/1.08 (((~![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))) | ((age(sk2, sk5) = sigma) | smaller(age(sk2, sk5), sigma) | (~smaller_or_equal(age(sk2, sk5), sigma)))) <=> ((~![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))) | (age(sk2, sk5) = sigma) | smaller(age(sk2, sk5), sigma) | (~smaller_or_equal(age(sk2, sk5), sigma)))),
% 0.80/1.08 inference(rewrite,[status(thm)],[])).
% 0.80/1.08 tff(310,plain,
% 0.80/1.08 ((~![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))) | ((age(sk2, sk5) = sigma) | smaller(age(sk2, sk5), sigma) | (~smaller_or_equal(age(sk2, sk5), sigma)))),
% 0.80/1.08 inference(quant_inst,[status(thm)],[])).
% 0.80/1.08 tff(311,plain,
% 0.80/1.08 ((~![B: $i, A: $i] : ((A = B) | smaller(A, B) | (~smaller_or_equal(A, B)))) | (age(sk2, sk5) = sigma) | smaller(age(sk2, sk5), sigma) | (~smaller_or_equal(age(sk2, sk5), sigma))),
% 0.80/1.08 inference(modus_ponens,[status(thm)],[310, 309])).
% 0.80/1.08 tff(312,plain,
% 0.80/1.08 ((age(sk2, sk5) = sigma) | smaller(age(sk2, sk5), sigma)),
% 0.80/1.08 inference(unit_resolution,[status(thm)],[311, 308, 298])).
% 0.80/1.08 tff(313,plain,
% 0.80/1.08 (age(sk2, sk5) = sigma),
% 0.80/1.08 inference(unit_resolution,[status(thm)],[312, 295])).
% 0.80/1.08 tff(314,plain,
% 0.80/1.08 (sigma = age(sk2, sk5)),
% 0.80/1.08 inference(symmetry,[status(thm)],[313])).
% 0.80/1.08 tff(315,plain,
% 0.80/1.08 (greater(sigma, age(sk2, sk5)) <=> greater(age(sk2, sk5), sigma)),
% 0.80/1.08 inference(monotonicity,[status(thm)],[314, 313])).
% 0.80/1.08 tff(316,plain,
% 0.80/1.08 (greater(age(sk2, sk5), sigma) <=> greater(sigma, age(sk2, sk5))),
% 0.80/1.08 inference(symmetry,[status(thm)],[315])).
% 0.80/1.08 tff(317,plain,
% 0.80/1.08 (greater(sigma, age(sk2, sk5))),
% 0.80/1.08 inference(modus_ponens,[status(thm)],[273, 316])).
% 0.80/1.08 tff(318,plain,
% 0.80/1.08 ($false),
% 0.80/1.08 inference(unit_resolution,[status(thm)],[284, 317])).
% 0.80/1.08 % SZS output end Proof
% 0.80/1.09 % E exiting
%------------------------------------------------------------------------------