%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT005+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:23:54 AM UTC 2026
% Result : Theorem 0.66s 0.90s
% Output : Proof 0.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT005+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.07/0.34 % Computer : n028.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 7 11:39:33 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.66/0.90 % SZS status Theorem
% 0.66/0.90 % SZS output start Proof
% 0.66/0.90 tff(greater_type, type, (
% 0.66/0.90 greater: ( $i * $i ) > $o)).
% 0.66/0.90 tff(tptp_fun_Tc_1_type, type, (
% 0.66/0.90 tptp_fun_Tc_1: $i)).
% 0.66/0.90 tff(tptp_fun_P2_6_type, type, (
% 0.66/0.90 tptp_fun_P2_6: $i)).
% 0.66/0.90 tff(tptp_fun_P_0_type, type, (
% 0.66/0.90 tptp_fun_P_0: ( $i * $i ) > $i)).
% 0.66/0.90 tff(tptp_fun_Y_11_type, type, (
% 0.66/0.90 tptp_fun_Y_11: $i)).
% 0.66/0.90 tff(tptp_fun_Tb_2_type, type, (
% 0.66/0.90 tptp_fun_Tb_2: $i)).
% 0.66/0.90 tff(tptp_fun_X_12_type, type, (
% 0.66/0.90 tptp_fun_X_12: $i)).
% 0.66/0.90 tff(tptp_fun_P1_7_type, type, (
% 0.66/0.90 tptp_fun_P1_7: $i)).
% 0.66/0.90 tff(survival_chance_type, type, (
% 0.66/0.90 survival_chance: ( $i * $i * $i ) > $o)).
% 0.66/0.90 tff(organization_type, type, (
% 0.66/0.90 organization: ( $i * $i ) > $o)).
% 0.66/0.90 tff(tptp_fun_C1_5_type, type, (
% 0.66/0.90 tptp_fun_C1_5: $i)).
% 0.66/0.90 tff(tptp_fun_C2_4_type, type, (
% 0.66/0.90 tptp_fun_C2_4: $i)).
% 0.66/0.90 tff(complexity_type, type, (
% 0.66/0.90 complexity: ( $i * $i * $i ) > $o)).
% 0.66/0.90 tff(tptp_fun_Ta_3_type, type, (
% 0.66/0.90 tptp_fun_Ta_3: $i)).
% 0.66/0.90 tff(reorganization_free_type, type, (
% 0.66/0.90 reorganization_free: ( $i * $i * $i ) > $o)).
% 0.66/0.90 tff(reorganization_type_type, type, (
% 0.66/0.90 reorganization_type: ( $i * $i * $i ) > $o)).
% 0.66/0.90 tff(tptp_fun_Re_10_type, type, (
% 0.66/0.90 tptp_fun_Re_10: $i)).
% 0.66/0.90 tff(reorganization_type, type, (
% 0.66/0.90 reorganization: ( $i * $i * $i ) > $o)).
% 0.66/0.90 tff(tptp_fun_P_8_type, type, (
% 0.66/0.90 tptp_fun_P_8: $i)).
% 0.66/0.90 tff(class_type, type, (
% 0.66/0.90 class: ( $i * $i * $i ) > $o)).
% 0.66/0.90 tff(tptp_fun_C_9_type, type, (
% 0.66/0.90 tptp_fun_C_9: $i)).
% 0.66/0.90 tff(1,assumption,(greater(tptp_fun_P_0(Tb!2, X!12), P2!6)), introduced(assumption)).
% 0.66/0.90 tff(2,assumption,(~organization(X!12, Tb!2)), introduced(assumption)).
% 0.66/0.90 tff(3,plain,
% 0.66/0.90 ((~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tc) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & reorganization_free(X, Tb, Tc) & survival_chance(X, P1, Tc) & survival_chance(Y, P2, Tc) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(P1, P2))) <=> (~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tc) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & reorganization_free(X, Tb, Tc) & survival_chance(X, P1, Tc) & survival_chance(Y, P2, Tc) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(P1, P2)))),
% 0.66/0.90 inference(rewrite,[status(thm)],[])).
% 0.66/0.90 tff(4,plain,
% 0.66/0.90 ((~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((((((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tc)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & reorganization_free(X, Tb, Tc)) & survival_chance(X, P1, Tc)) & survival_chance(Y, P2, Tc)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) => greater(P1, P2))) <=> (~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tc) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & reorganization_free(X, Tb, Tc) & survival_chance(X, P1, Tc) & survival_chance(Y, P2, Tc) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(P1, P2)))),
% 0.66/0.90 inference(rewrite,[status(thm)],[])).
% 0.66/0.90 tff(5,axiom,(~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((((((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tc)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & reorganization_free(X, Tb, Tc)) & survival_chance(X, P1, Tc)) & survival_chance(Y, P2, Tc)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) => greater(P1, P2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t5_FOL')).
% 0.66/0.90 tff(6,plain,
% 0.66/0.90 (~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tc) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & reorganization_free(X, Tb, Tc) & survival_chance(X, P1, Tc) & survival_chance(Y, P2, Tc) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(P1, P2))),
% 0.66/0.90 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.66/0.90 tff(7,plain,
% 0.66/0.90 (~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tc) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & reorganization_free(X, Tb, Tc) & survival_chance(X, P1, Tc) & survival_chance(Y, P2, Tc) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(P1, P2))),
% 0.66/0.90 inference(modus_ponens,[status(thm)],[6, 3])).
% 0.66/0.90 tff(8,plain,
% 0.66/0.90 (~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tc) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & reorganization_free(X, Tb, Tc) & survival_chance(X, P1, Tc) & survival_chance(Y, P2, Tc) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(P1, P2))),
% 0.66/0.90 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.66/0.90 tff(9,plain,
% 0.66/0.90 (~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tc) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & reorganization_free(X, Tb, Tc) & survival_chance(X, P1, Tc) & survival_chance(Y, P2, Tc) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(P1, P2))),
% 0.66/0.90 inference(modus_ponens,[status(thm)],[8, 3])).
% 0.66/0.90 tff(10,plain,(
% 0.66/0.90 ~((~(organization(X!12, Ta!3) & organization(Y!11, Ta!3) & organization(X!12, Tc!1) & organization(Y!11, Tc!1) & class(X!12, C!9, Ta!3) & class(Y!11, C!9, Ta!3) & survival_chance(X!12, P!8, Ta!3) & survival_chance(Y!11, P!8, Ta!3) & reorganization(X!12, Ta!3, Tb!2) & reorganization(Y!11, Ta!3, Tc!1) & reorganization_type(X!12, Re!10, Ta!3) & reorganization_type(Y!11, Re!10, Ta!3) & reorganization_free(X!12, Tb!2, Tc!1) & survival_chance(X!12, P1!7, Tc!1) & survival_chance(Y!11, P2!6, Tc!1) & complexity(X!12, C1!5, Ta!3) & complexity(Y!11, C2!4, Ta!3) & greater(C2!4, C1!5))) | greater(P1!7, P2!6))),
% 0.66/0.90 inference(skolemize,[status(sab)],[9])).
% 0.66/0.90 tff(11,plain,
% 0.66/0.90 (organization(X!12, Ta!3) & organization(Y!11, Ta!3) & organization(X!12, Tc!1) & organization(Y!11, Tc!1) & class(X!12, C!9, Ta!3) & class(Y!11, C!9, Ta!3) & survival_chance(X!12, P!8, Ta!3) & survival_chance(Y!11, P!8, Ta!3) & reorganization(X!12, Ta!3, Tb!2) & reorganization(Y!11, Ta!3, Tc!1) & reorganization_type(X!12, Re!10, Ta!3) & reorganization_type(Y!11, Re!10, Ta!3) & reorganization_free(X!12, Tb!2, Tc!1) & survival_chance(X!12, P1!7, Tc!1) & survival_chance(Y!11, P2!6, Tc!1) & complexity(X!12, C1!5, Ta!3) & complexity(Y!11, C2!4, Ta!3) & greater(C2!4, C1!5)),
% 0.66/0.90 inference(or_elim,[status(thm)],[10])).
% 0.66/0.90 tff(12,plain,
% 0.66/0.90 (greater(C2!4, C1!5)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(13,plain,
% 0.66/0.90 (complexity(Y!11, C2!4, Ta!3)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(14,plain,
% 0.66/0.90 (complexity(X!12, C1!5, Ta!3)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(15,plain,
% 0.66/0.90 (reorganization_type(Y!11, Re!10, Ta!3)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(16,plain,
% 0.66/0.90 (reorganization_type(X!12, Re!10, Ta!3)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(17,plain,
% 0.66/0.90 (reorganization(Y!11, Ta!3, Tc!1)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(18,plain,
% 0.66/0.90 (reorganization(X!12, Ta!3, Tb!2)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(19,plain,
% 0.66/0.90 (class(Y!11, C!9, Ta!3)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(20,plain,
% 0.66/0.90 (class(X!12, C!9, Ta!3)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(21,plain,
% 0.66/0.90 (organization(Y!11, Tc!1)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(22,plain,
% 0.66/0.90 (organization(Y!11, Ta!3)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(23,plain,
% 0.66/0.90 (organization(X!12, Ta!3)),
% 0.66/0.90 inference(and_elim,[status(thm)],[11])).
% 0.66/0.90 tff(24,plain,
% 0.66/0.90 (^[X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : refl((greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1))) <=> (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1))))),
% 0.66/0.90 inference(bind,[status(th)],[])).
% 0.66/0.90 tff(25,plain,
% 0.66/0.90 (![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1))) <=> ![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))),
% 0.66/0.90 inference(quant_intro,[status(thm)],[24])).
% 0.66/0.90 tff(26,plain,
% 0.66/0.90 (^[X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : trans(monotonicity(trans(monotonicity(rewrite((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)) <=> (~((~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1))))), ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) <=> (~(~((~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1))))))), rewrite((~(~((~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1))))) <=> ((~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))), ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) <=> ((~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1))))), (((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb)) <=> (((~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1))) | greater(Tc, Tb)))), rewrite((((~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1))) | greater(Tc, Tb)) <=> (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))), (((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb)) <=> (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))))),
% 0.66/0.90 inference(bind,[status(th)],[])).
% 0.66/0.90 tff(27,plain,
% 0.66/0.90 (![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb)) <=> ![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))),
% 0.66/0.90 inference(quant_intro,[status(thm)],[26])).
% 0.66/0.90 tff(28,plain,
% 0.66/0.90 (![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb)) <=> ![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb))),
% 0.66/0.90 inference(rewrite,[status(thm)],[])).
% 0.66/0.90 tff(29,plain,
% 0.66/0.90 (^[X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc))), ((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc)) & class(X, C, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc)) & class(X, C, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta))), ((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta)))), (((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta)) & class(Y, C, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta)) & class(Y, C, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta))), (((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta)))), ((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb))), ((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb)))), (((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc))), (((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc)))), ((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta))), ((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta)))), (((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta))), (((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta)))), ((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta))), ((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta)))), (((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta))), (((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta)))), ((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta)) & greater(C2, C1)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta)) & greater(C2, C1)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))), ((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)))), (((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) => greater(Tc, Tb)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)) => greater(Tc, Tb)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)) => greater(Tc, Tb)) <=> ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb))), (((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) => greater(Tc, Tb)) <=> ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb))))),
% 0.66/0.91 inference(bind,[status(th)],[])).
% 0.66/0.91 tff(30,plain,
% 0.66/0.91 (![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) => greater(Tc, Tb)) <=> ![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb))),
% 0.66/0.91 inference(quant_intro,[status(thm)],[29])).
% 0.66/0.91 tff(31,axiom,(![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(Y, Tc)) & class(X, C, Ta)) & class(Y, C, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) => greater(Tc, Tb))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','a10_FOL')).
% 0.66/0.91 tff(32,plain,
% 0.66/0.91 (![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb))),
% 0.66/0.91 inference(modus_ponens,[status(thm)],[31, 30])).
% 0.66/0.91 tff(33,plain,
% 0.66/0.91 (![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb))),
% 0.66/0.91 inference(modus_ponens,[status(thm)],[32, 28])).
% 0.66/0.91 tff(34,plain,(
% 0.66/0.91 ![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((~(organization(X, Ta) & organization(Y, Ta) & organization(Y, Tc) & class(X, C, Ta) & class(Y, C, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) | greater(Tc, Tb))),
% 0.66/0.91 inference(skolemize,[status(sab)],[33])).
% 0.66/0.91 tff(35,plain,
% 0.66/0.91 (![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))),
% 0.66/0.91 inference(modus_ponens,[status(thm)],[34, 27])).
% 0.66/0.91 tff(36,plain,
% 0.66/0.91 (![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))),
% 0.66/0.91 inference(modus_ponens,[status(thm)],[35, 25])).
% 0.66/0.91 tff(37,plain,
% 0.66/0.91 (((~![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))) | ((~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~reorganization(X!12, Ta!3, Tb!2)) | greater(Tc!1, Tb!2) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)))) <=> ((~![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))) | (~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~reorganization(X!12, Ta!3, Tb!2)) | greater(Tc!1, Tb!2) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)))),
% 0.66/0.91 inference(rewrite,[status(thm)],[])).
% 0.66/0.91 tff(38,plain,
% 0.66/0.91 ((greater(Tc!1, Tb!2) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~class(X!12, C!9, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)) | (~greater(C2!4, C1!5))) <=> ((~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~reorganization(X!12, Ta!3, Tb!2)) | greater(Tc!1, Tb!2) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)))),
% 0.66/0.91 inference(rewrite,[status(thm)],[])).
% 0.66/0.91 tff(39,plain,
% 0.66/0.91 (((~![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))) | (greater(Tc!1, Tb!2) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~class(X!12, C!9, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)) | (~greater(C2!4, C1!5)))) <=> ((~![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))) | ((~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~reorganization(X!12, Ta!3, Tb!2)) | greater(Tc!1, Tb!2) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3))))),
% 0.66/0.91 inference(monotonicity,[status(thm)],[38])).
% 0.66/0.91 tff(40,plain,
% 0.66/0.91 (((~![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))) | (greater(Tc!1, Tb!2) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~class(X!12, C!9, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)) | (~greater(C2!4, C1!5)))) <=> ((~![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))) | (~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~reorganization(X!12, Ta!3, Tb!2)) | greater(Tc!1, Tb!2) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)))),
% 0.66/0.92 inference(transitivity,[status(thm)],[39, 37])).
% 0.66/0.92 tff(41,plain,
% 0.66/0.92 ((~![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))) | (greater(Tc!1, Tb!2) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~class(X!12, C!9, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)) | (~greater(C2!4, C1!5)))),
% 0.66/0.92 inference(quant_inst,[status(thm)],[])).
% 0.66/0.92 tff(42,plain,
% 0.66/0.92 ((~![X: $i, Y: $i, Re: $i, C: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (greater(Tc, Tb) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(Y, Tc)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)) | (~greater(C2, C1)))) | (~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~reorganization(X!12, Ta!3, Tb!2)) | greater(Tc!1, Tb!2) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.66/0.92 tff(43,plain,
% 0.66/0.92 (greater(Tc!1, Tb!2)),
% 0.66/0.92 inference(unit_resolution,[status(thm)],[42, 36, 23, 22, 21, 20, 19, 18, 17, 16, 15, 14, 13, 12])).
% 0.66/0.92 tff(44,plain,
% 0.66/0.92 (^[X: $i, Ta: $i, Tb: $i] : refl(((~reorganization(X, Ta, Tb)) | greater(Tb, Ta)) <=> ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta)))),
% 0.66/0.92 inference(bind,[status(th)],[])).
% 0.66/0.92 tff(45,plain,
% 0.66/0.92 (![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta)) <=> ![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))),
% 0.66/0.92 inference(quant_intro,[status(thm)],[44])).
% 0.66/0.92 tff(46,plain,
% 0.66/0.92 (![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta)) <=> ![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))),
% 0.66/0.92 inference(rewrite,[status(thm)],[])).
% 0.66/0.92 tff(47,plain,
% 0.66/0.92 (^[X: $i, Ta: $i, Tb: $i] : rewrite((reorganization(X, Ta, Tb) => greater(Tb, Ta)) <=> ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta)))),
% 0.66/0.92 inference(bind,[status(th)],[])).
% 0.66/0.92 tff(48,plain,
% 0.66/0.92 (![X: $i, Ta: $i, Tb: $i] : (reorganization(X, Ta, Tb) => greater(Tb, Ta)) <=> ![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))),
% 0.66/0.92 inference(quant_intro,[status(thm)],[47])).
% 0.66/0.92 tff(49,axiom,(![X: $i, Ta: $i, Tb: $i] : (reorganization(X, Ta, Tb) => greater(Tb, Ta))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp7')).
% 0.66/0.92 tff(50,plain,
% 0.66/0.92 (![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.66/0.92 tff(51,plain,
% 0.66/0.92 (![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[50, 46])).
% 0.66/0.92 tff(52,plain,(
% 0.66/0.92 ![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))),
% 0.66/0.92 inference(skolemize,[status(sab)],[51])).
% 0.66/0.92 tff(53,plain,
% 0.66/0.92 (![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[52, 45])).
% 0.66/0.92 tff(54,plain,
% 0.66/0.92 (((~![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))) | ((~reorganization(X!12, Ta!3, Tb!2)) | greater(Tb!2, Ta!3))) <=> ((~![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))) | (~reorganization(X!12, Ta!3, Tb!2)) | greater(Tb!2, Ta!3))),
% 0.66/0.92 inference(rewrite,[status(thm)],[])).
% 0.66/0.92 tff(55,plain,
% 0.66/0.92 ((~![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))) | ((~reorganization(X!12, Ta!3, Tb!2)) | greater(Tb!2, Ta!3))),
% 0.66/0.92 inference(quant_inst,[status(thm)],[])).
% 0.66/0.92 tff(56,plain,
% 0.66/0.92 ((~![X: $i, Ta: $i, Tb: $i] : ((~reorganization(X, Ta, Tb)) | greater(Tb, Ta))) | (~reorganization(X!12, Ta!3, Tb!2)) | greater(Tb!2, Ta!3)),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.66/0.92 tff(57,plain,
% 0.66/0.92 (greater(Tb!2, Ta!3)),
% 0.66/0.92 inference(unit_resolution,[status(thm)],[56, 53, 18])).
% 0.66/0.92 tff(58,plain,
% 0.66/0.92 (organization(X!12, Tc!1)),
% 0.66/0.92 inference(and_elim,[status(thm)],[11])).
% 0.66/0.92 tff(59,plain,
% 0.66/0.92 (^[X: $i, T: $i, T1: $i, T2: $i] : refl((organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T))) <=> (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T))))),
% 0.66/0.92 inference(bind,[status(th)],[])).
% 0.66/0.92 tff(60,plain,
% 0.66/0.92 (![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T))) <=> ![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))),
% 0.66/0.92 inference(quant_intro,[status(thm)],[59])).
% 0.66/0.92 tff(61,plain,
% 0.66/0.92 (^[X: $i, T: $i, T1: $i, T2: $i] : trans(monotonicity(trans(monotonicity(rewrite((organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T)) <=> (~((~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T))))), ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) <=> (~(~((~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T))))))), rewrite((~(~((~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T))))) <=> ((~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))), ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) <=> ((~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T))))), (((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T)) <=> (((~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T))) | organization(X, T)))), rewrite((((~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T))) | organization(X, T)) <=> (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))), (((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T)) <=> (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))))),
% 0.66/0.92 inference(bind,[status(th)],[])).
% 0.66/0.92 tff(62,plain,
% 0.66/0.92 (![X: $i, T: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T)) <=> ![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))),
% 0.66/0.92 inference(quant_intro,[status(thm)],[61])).
% 0.66/0.92 tff(63,plain,
% 0.66/0.92 (![X: $i, T: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T)) <=> ![X: $i, T: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T))),
% 0.66/0.92 inference(rewrite,[status(thm)],[])).
% 0.66/0.92 tff(64,plain,
% 0.66/0.92 (^[X: $i, T: $i, T1: $i, T2: $i] : trans(monotonicity(trans(monotonicity(rewrite(((organization(X, T1) & organization(X, T2)) & greater(T, T1)) <=> (organization(X, T1) & organization(X, T2) & greater(T, T1))), ((((organization(X, T1) & organization(X, T2)) & greater(T, T1)) & greater(T2, T)) <=> ((organization(X, T1) & organization(X, T2) & greater(T, T1)) & greater(T2, T)))), rewrite(((organization(X, T1) & organization(X, T2) & greater(T, T1)) & greater(T2, T)) <=> (organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))), ((((organization(X, T1) & organization(X, T2)) & greater(T, T1)) & greater(T2, T)) <=> (organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T)))), (((((organization(X, T1) & organization(X, T2)) & greater(T, T1)) & greater(T2, T)) => organization(X, T)) <=> ((organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T)) => organization(X, T)))), rewrite(((organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T)) => organization(X, T)) <=> ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T))), (((((organization(X, T1) & organization(X, T2)) & greater(T, T1)) & greater(T2, T)) => organization(X, T)) <=> ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T))))),
% 0.66/0.92 inference(bind,[status(th)],[])).
% 0.66/0.92 tff(65,plain,
% 0.66/0.92 (![X: $i, T: $i, T1: $i, T2: $i] : ((((organization(X, T1) & organization(X, T2)) & greater(T, T1)) & greater(T2, T)) => organization(X, T)) <=> ![X: $i, T: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T))),
% 0.66/0.92 inference(quant_intro,[status(thm)],[64])).
% 0.66/0.92 tff(66,axiom,(![X: $i, T: $i, T1: $i, T2: $i] : ((((organization(X, T1) & organization(X, T2)) & greater(T, T1)) & greater(T2, T)) => organization(X, T))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp13')).
% 0.66/0.92 tff(67,plain,
% 0.66/0.92 (![X: $i, T: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.66/0.92 tff(68,plain,
% 0.66/0.92 (![X: $i, T: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[67, 63])).
% 0.66/0.92 tff(69,plain,(
% 0.66/0.92 ![X: $i, T: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & greater(T, T1) & greater(T2, T))) | organization(X, T))),
% 0.66/0.92 inference(skolemize,[status(sab)],[68])).
% 0.66/0.92 tff(70,plain,
% 0.66/0.92 (![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[69, 62])).
% 0.66/0.92 tff(71,plain,
% 0.66/0.92 (![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[70, 60])).
% 0.66/0.92 tff(72,plain,
% 0.66/0.92 (((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | ((~organization(X!12, Ta!3)) | (~organization(X!12, Tc!1)) | organization(X!12, Tb!2) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2)))) <=> ((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (~organization(X!12, Ta!3)) | (~organization(X!12, Tc!1)) | organization(X!12, Tb!2) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2)))),
% 0.66/0.92 inference(rewrite,[status(thm)],[])).
% 0.66/0.92 tff(73,plain,
% 0.66/0.92 ((organization(X!12, Tb!2) | (~greater(Tb!2, Ta!3)) | (~organization(X!12, Ta!3)) | (~organization(X!12, Tc!1)) | (~greater(Tc!1, Tb!2))) <=> ((~organization(X!12, Ta!3)) | (~organization(X!12, Tc!1)) | organization(X!12, Tb!2) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2)))),
% 0.66/0.92 inference(rewrite,[status(thm)],[])).
% 0.66/0.92 tff(74,plain,
% 0.66/0.92 (((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (organization(X!12, Tb!2) | (~greater(Tb!2, Ta!3)) | (~organization(X!12, Ta!3)) | (~organization(X!12, Tc!1)) | (~greater(Tc!1, Tb!2)))) <=> ((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | ((~organization(X!12, Ta!3)) | (~organization(X!12, Tc!1)) | organization(X!12, Tb!2) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2))))),
% 0.66/0.92 inference(monotonicity,[status(thm)],[73])).
% 0.66/0.92 tff(75,plain,
% 0.66/0.92 (((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (organization(X!12, Tb!2) | (~greater(Tb!2, Ta!3)) | (~organization(X!12, Ta!3)) | (~organization(X!12, Tc!1)) | (~greater(Tc!1, Tb!2)))) <=> ((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (~organization(X!12, Ta!3)) | (~organization(X!12, Tc!1)) | organization(X!12, Tb!2) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2)))),
% 0.66/0.92 inference(transitivity,[status(thm)],[74, 72])).
% 0.66/0.92 tff(76,plain,
% 0.66/0.92 ((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (organization(X!12, Tb!2) | (~greater(Tb!2, Ta!3)) | (~organization(X!12, Ta!3)) | (~organization(X!12, Tc!1)) | (~greater(Tc!1, Tb!2)))),
% 0.66/0.92 inference(quant_inst,[status(thm)],[])).
% 0.66/0.92 tff(77,plain,
% 0.66/0.92 ((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (~organization(X!12, Ta!3)) | (~organization(X!12, Tc!1)) | organization(X!12, Tb!2) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[76, 75])).
% 0.66/0.92 tff(78,plain,
% 0.66/0.92 ($false),
% 0.66/0.92 inference(unit_resolution,[status(thm)],[77, 71, 23, 58, 57, 43, 2])).
% 0.66/0.92 tff(79,plain,(organization(X!12, Tb!2)), inference(lemma,lemma(discharge,[]))).
% 0.66/0.92 tff(80,plain,
% 0.66/0.92 (^[X: $i, T: $i] : refl(((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T)) <=> ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T)))),
% 0.66/0.92 inference(bind,[status(th)],[])).
% 0.66/0.92 tff(81,plain,
% 0.66/0.92 (![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T)) <=> ![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))),
% 0.66/0.92 inference(quant_intro,[status(thm)],[80])).
% 0.66/0.92 tff(82,plain,
% 0.66/0.92 (![X: $i, T: $i] : ((~organization(X, T)) | ?[P: $i] : survival_chance(X, P, T)) <=> ![X: $i, T: $i] : ((~organization(X, T)) | ?[P: $i] : survival_chance(X, P, T))),
% 0.66/0.92 inference(rewrite,[status(thm)],[])).
% 0.66/0.92 tff(83,plain,
% 0.66/0.92 (^[X: $i, T: $i] : rewrite((organization(X, T) => ?[P: $i] : survival_chance(X, P, T)) <=> ((~organization(X, T)) | ?[P: $i] : survival_chance(X, P, T)))),
% 0.66/0.92 inference(bind,[status(th)],[])).
% 0.66/0.92 tff(84,plain,
% 0.66/0.92 (![X: $i, T: $i] : (organization(X, T) => ?[P: $i] : survival_chance(X, P, T)) <=> ![X: $i, T: $i] : ((~organization(X, T)) | ?[P: $i] : survival_chance(X, P, T))),
% 0.66/0.92 inference(quant_intro,[status(thm)],[83])).
% 0.66/0.92 tff(85,axiom,(![X: $i, T: $i] : (organization(X, T) => ?[P: $i] : survival_chance(X, P, T))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp12')).
% 0.66/0.92 tff(86,plain,
% 0.66/0.92 (![X: $i, T: $i] : ((~organization(X, T)) | ?[P: $i] : survival_chance(X, P, T))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[85, 84])).
% 0.66/0.92 tff(87,plain,
% 0.66/0.92 (![X: $i, T: $i] : ((~organization(X, T)) | ?[P: $i] : survival_chance(X, P, T))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[86, 82])).
% 0.66/0.92 tff(88,plain,(
% 0.66/0.92 ![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))),
% 0.66/0.92 inference(skolemize,[status(sab)],[87])).
% 0.66/0.92 tff(89,plain,
% 0.66/0.92 (![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[88, 81])).
% 0.66/0.92 tff(90,plain,
% 0.66/0.92 (((~![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))) | ((~organization(X!12, Tb!2)) | survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2))) <=> ((~![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))) | (~organization(X!12, Tb!2)) | survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2))),
% 0.66/0.92 inference(rewrite,[status(thm)],[])).
% 0.66/0.92 tff(91,plain,
% 0.66/0.92 ((~![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))) | ((~organization(X!12, Tb!2)) | survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2))),
% 0.66/0.92 inference(quant_inst,[status(thm)],[])).
% 0.66/0.92 tff(92,plain,
% 0.66/0.92 ((~![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))) | (~organization(X!12, Tb!2)) | survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)),
% 0.66/0.92 inference(modus_ponens,[status(thm)],[91, 90])).
% 0.66/0.92 tff(93,plain,
% 0.66/0.92 (survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)),
% 0.66/0.92 inference(unit_resolution,[status(thm)],[92, 89, 79])).
% 0.66/0.92 tff(94,plain,
% 0.66/0.92 (survival_chance(X!12, P1!7, Tc!1)),
% 0.66/0.92 inference(and_elim,[status(thm)],[11])).
% 0.66/0.92 tff(95,plain,
% 0.66/0.92 (reorganization_free(X!12, Tb!2, Tc!1)),
% 0.66/0.92 inference(and_elim,[status(thm)],[11])).
% 0.66/0.92 tff(96,plain,
% 0.66/0.92 (^[X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : refl((greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2))) <=> (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2))))),
% 0.66/0.92 inference(bind,[status(th)],[])).
% 0.66/0.92 tff(97,plain,
% 0.66/0.92 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2))) <=> ![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))),
% 0.66/0.92 inference(quant_intro,[status(thm)],[96])).
% 0.66/0.92 tff(98,plain,
% 0.66/0.92 (^[X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : trans(monotonicity(trans(monotonicity(rewrite((organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1)) <=> (~((~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2))))), ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) <=> (~(~((~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2))))))), rewrite((~(~((~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2))))) <=> ((~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))), ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) <=> ((~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2))))), (((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1)) <=> (((~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2))) | greater(P2, P1)))), rewrite((((~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2))) | greater(P2, P1)) <=> (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))), (((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1)) <=> (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))))),
% 0.66/0.92 inference(bind,[status(th)],[])).
% 0.66/0.92 tff(99,plain,
% 0.66/0.92 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1)) <=> ![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))),
% 0.66/0.92 inference(quant_intro,[status(thm)],[98])).
% 0.66/0.92 tff(100,plain,
% 0.66/0.92 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1)) <=> ![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1))),
% 0.66/0.92 inference(rewrite,[status(thm)],[])).
% 0.66/0.92 tff(101,plain,
% 0.66/0.92 (^[X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) <=> (organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2))), ((((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) <=> ((organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)))), rewrite(((organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) <=> (organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1))), ((((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) <=> (organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1)))), (((((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) <=> ((organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)))), rewrite(((organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) <=> (organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2))), (((((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) <=> (organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2)))), ((((((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & greater(T2, T1)) <=> ((organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2)) & greater(T2, T1)))), rewrite(((organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2)) & greater(T2, T1)) <=> (organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))), ((((((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & greater(T2, T1)) <=> (organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1)))), (((((((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & greater(T2, T1)) => greater(P2, P1)) <=> ((organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1)) => greater(P2, P1)))), rewrite(((organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1)) => greater(P2, P1)) <=> ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1))), (((((((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & greater(T2, T1)) => greater(P2, P1)) <=> ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1))))),
% 0.66/0.93 inference(bind,[status(th)],[])).
% 0.66/0.93 tff(102,plain,
% 0.66/0.93 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : ((((((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & greater(T2, T1)) => greater(P2, P1)) <=> ![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1))),
% 0.66/0.93 inference(quant_intro,[status(thm)],[101])).
% 0.66/0.93 tff(103,axiom,(![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : ((((((organization(X, T1) & organization(X, T2)) & reorganization_free(X, T1, T2)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & greater(T2, T1)) => greater(P2, P1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t3_FOL')).
% 0.66/0.93 tff(104,plain,
% 0.66/0.93 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1))),
% 0.66/0.93 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.66/0.93 tff(105,plain,
% 0.66/0.93 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1))),
% 0.66/0.93 inference(modus_ponens,[status(thm)],[104, 100])).
% 0.66/0.93 tff(106,plain,(
% 0.66/0.93 ![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization_free(X, T1, T2) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & greater(T2, T1))) | greater(P2, P1))),
% 0.66/0.93 inference(skolemize,[status(sab)],[105])).
% 0.66/0.93 tff(107,plain,
% 0.66/0.93 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))),
% 0.66/0.93 inference(modus_ponens,[status(thm)],[106, 99])).
% 0.66/0.93 tff(108,plain,
% 0.66/0.93 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))),
% 0.66/0.93 inference(modus_ponens,[status(thm)],[107, 97])).
% 0.66/0.93 tff(109,plain,
% 0.66/0.93 (((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))) | ((~organization(X!12, Tc!1)) | (~survival_chance(X!12, P1!7, Tc!1)) | (~organization(X!12, Tb!2)) | (~greater(Tc!1, Tb!2)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | greater(P1!7, tptp_fun_P_0(Tb!2, X!12)) | (~reorganization_free(X!12, Tb!2, Tc!1)))) <=> ((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))) | (~organization(X!12, Tc!1)) | (~survival_chance(X!12, P1!7, Tc!1)) | (~organization(X!12, Tb!2)) | (~greater(Tc!1, Tb!2)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | greater(P1!7, tptp_fun_P_0(Tb!2, X!12)) | (~reorganization_free(X!12, Tb!2, Tc!1)))),
% 0.66/0.93 inference(rewrite,[status(thm)],[])).
% 0.66/0.93 tff(110,plain,
% 0.66/0.93 ((greater(P1!7, tptp_fun_P_0(Tb!2, X!12)) | (~greater(Tc!1, Tb!2)) | (~organization(X!12, Tb!2)) | (~organization(X!12, Tc!1)) | (~reorganization_free(X!12, Tb!2, Tc!1)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~survival_chance(X!12, P1!7, Tc!1))) <=> ((~organization(X!12, Tc!1)) | (~survival_chance(X!12, P1!7, Tc!1)) | (~organization(X!12, Tb!2)) | (~greater(Tc!1, Tb!2)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | greater(P1!7, tptp_fun_P_0(Tb!2, X!12)) | (~reorganization_free(X!12, Tb!2, Tc!1)))),
% 0.66/0.93 inference(rewrite,[status(thm)],[])).
% 0.66/0.93 tff(111,plain,
% 0.66/0.93 (((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))) | (greater(P1!7, tptp_fun_P_0(Tb!2, X!12)) | (~greater(Tc!1, Tb!2)) | (~organization(X!12, Tb!2)) | (~organization(X!12, Tc!1)) | (~reorganization_free(X!12, Tb!2, Tc!1)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~survival_chance(X!12, P1!7, Tc!1)))) <=> ((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))) | ((~organization(X!12, Tc!1)) | (~survival_chance(X!12, P1!7, Tc!1)) | (~organization(X!12, Tb!2)) | (~greater(Tc!1, Tb!2)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | greater(P1!7, tptp_fun_P_0(Tb!2, X!12)) | (~reorganization_free(X!12, Tb!2, Tc!1))))),
% 0.66/0.93 inference(monotonicity,[status(thm)],[110])).
% 0.66/0.93 tff(112,plain,
% 0.66/0.93 (((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))) | (greater(P1!7, tptp_fun_P_0(Tb!2, X!12)) | (~greater(Tc!1, Tb!2)) | (~organization(X!12, Tb!2)) | (~organization(X!12, Tc!1)) | (~reorganization_free(X!12, Tb!2, Tc!1)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~survival_chance(X!12, P1!7, Tc!1)))) <=> ((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))) | (~organization(X!12, Tc!1)) | (~survival_chance(X!12, P1!7, Tc!1)) | (~organization(X!12, Tb!2)) | (~greater(Tc!1, Tb!2)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | greater(P1!7, tptp_fun_P_0(Tb!2, X!12)) | (~reorganization_free(X!12, Tb!2, Tc!1)))),
% 0.66/0.93 inference(transitivity,[status(thm)],[111, 109])).
% 0.66/0.93 tff(113,plain,
% 0.66/0.93 ((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))) | (greater(P1!7, tptp_fun_P_0(Tb!2, X!12)) | (~greater(Tc!1, Tb!2)) | (~organization(X!12, Tb!2)) | (~organization(X!12, Tc!1)) | (~reorganization_free(X!12, Tb!2, Tc!1)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~survival_chance(X!12, P1!7, Tc!1)))),
% 0.66/0.93 inference(quant_inst,[status(thm)],[])).
% 0.66/0.93 tff(114,plain,
% 0.66/0.93 ((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i] : (greater(P2, P1) | (~greater(T2, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization_free(X, T1, T2)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)))) | (~organization(X!12, Tc!1)) | (~survival_chance(X!12, P1!7, Tc!1)) | (~organization(X!12, Tb!2)) | (~greater(Tc!1, Tb!2)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | greater(P1!7, tptp_fun_P_0(Tb!2, X!12)) | (~reorganization_free(X!12, Tb!2, Tc!1))),
% 0.66/0.93 inference(modus_ponens,[status(thm)],[113, 112])).
% 0.66/0.93 tff(115,plain,
% 0.66/0.93 (greater(P1!7, tptp_fun_P_0(Tb!2, X!12))),
% 0.66/0.93 inference(unit_resolution,[status(thm)],[114, 108, 58, 95, 94, 43, 79, 93])).
% 0.66/0.93 tff(116,plain,
% 0.66/0.93 (~greater(P1!7, P2!6)),
% 0.66/0.93 inference(or_elim,[status(thm)],[10])).
% 0.66/0.93 tff(117,plain,
% 0.66/0.93 (![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y))) <=> ![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))),
% 0.66/0.93 inference(rewrite,[status(thm)],[])).
% 0.66/0.93 tff(118,plain,
% 0.66/0.93 (^[X: $i, Y: $i, Z: $i] : trans(monotonicity(trans(monotonicity(rewrite((greater(X, Y) & greater(Y, Z)) <=> (~((~greater(Y, Z)) | (~greater(X, Y))))), ((~(greater(X, Y) & greater(Y, Z))) <=> (~(~((~greater(Y, Z)) | (~greater(X, Y))))))), rewrite((~(~((~greater(Y, Z)) | (~greater(X, Y))))) <=> ((~greater(Y, Z)) | (~greater(X, Y)))), ((~(greater(X, Y) & greater(Y, Z))) <=> ((~greater(Y, Z)) | (~greater(X, Y))))), (((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z)) <=> (((~greater(Y, Z)) | (~greater(X, Y))) | greater(X, Z)))), rewrite((((~greater(Y, Z)) | (~greater(X, Y))) | greater(X, Z)) <=> (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))), (((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z)) <=> (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))))),
% 0.66/0.93 inference(bind,[status(th)],[])).
% 0.66/0.93 tff(119,plain,
% 0.66/0.93 (![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))),
% 0.66/0.93 inference(quant_intro,[status(thm)],[118])).
% 0.66/0.93 tff(120,plain,
% 0.66/0.93 (![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z))),
% 0.66/0.93 inference(rewrite,[status(thm)],[])).
% 0.66/0.93 tff(121,plain,
% 0.66/0.93 (^[X: $i, Y: $i, Z: $i] : rewrite(((greater(X, Y) & greater(Y, Z)) => greater(X, Z)) <=> ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z)))),
% 0.66/0.93 inference(bind,[status(th)],[])).
% 0.66/0.93 tff(122,plain,
% 0.66/0.93 (![X: $i, Y: $i, Z: $i] : ((greater(X, Y) & greater(Y, Z)) => greater(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z))),
% 0.66/0.93 inference(quant_intro,[status(thm)],[121])).
% 0.66/0.93 tff(123,axiom,(![X: $i, Y: $i, Z: $i] : ((greater(X, Y) & greater(Y, Z)) => greater(X, Z))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp11')).
% 0.66/0.93 tff(124,plain,
% 0.66/0.93 (![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z))),
% 0.66/0.93 inference(modus_ponens,[status(thm)],[123, 122])).
% 0.66/0.93 tff(125,plain,
% 0.66/0.93 (![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z))),
% 0.66/0.93 inference(modus_ponens,[status(thm)],[124, 120])).
% 0.66/0.93 tff(126,plain,(
% 0.66/0.93 ![X: $i, Y: $i, Z: $i] : ((~(greater(X, Y) & greater(Y, Z))) | greater(X, Z))),
% 0.66/0.93 inference(skolemize,[status(sab)],[125])).
% 0.66/0.93 tff(127,plain,
% 0.66/0.93 (![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))),
% 0.66/0.93 inference(modus_ponens,[status(thm)],[126, 119])).
% 0.66/0.93 tff(128,plain,
% 0.66/0.93 (![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))),
% 0.66/0.93 inference(modus_ponens,[status(thm)],[127, 117])).
% 0.66/0.93 tff(129,plain,
% 0.66/0.93 (((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | (greater(P1!7, P2!6) | (~greater(P1!7, tptp_fun_P_0(Tb!2, X!12))) | (~greater(tptp_fun_P_0(Tb!2, X!12), P2!6)))) <=> ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | greater(P1!7, P2!6) | (~greater(P1!7, tptp_fun_P_0(Tb!2, X!12))) | (~greater(tptp_fun_P_0(Tb!2, X!12), P2!6)))),
% 0.66/0.93 inference(rewrite,[status(thm)],[])).
% 0.66/0.93 tff(130,plain,
% 0.66/0.93 ((greater(P1!7, P2!6) | (~greater(tptp_fun_P_0(Tb!2, X!12), P2!6)) | (~greater(P1!7, tptp_fun_P_0(Tb!2, X!12)))) <=> (greater(P1!7, P2!6) | (~greater(P1!7, tptp_fun_P_0(Tb!2, X!12))) | (~greater(tptp_fun_P_0(Tb!2, X!12), P2!6)))),
% 0.66/0.93 inference(rewrite,[status(thm)],[])).
% 0.66/0.93 tff(131,plain,
% 0.66/0.93 (((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | (greater(P1!7, P2!6) | (~greater(tptp_fun_P_0(Tb!2, X!12), P2!6)) | (~greater(P1!7, tptp_fun_P_0(Tb!2, X!12))))) <=> ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | (greater(P1!7, P2!6) | (~greater(P1!7, tptp_fun_P_0(Tb!2, X!12))) | (~greater(tptp_fun_P_0(Tb!2, X!12), P2!6))))),
% 0.66/0.93 inference(monotonicity,[status(thm)],[130])).
% 0.66/0.93 tff(132,plain,
% 0.66/0.93 (((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | (greater(P1!7, P2!6) | (~greater(tptp_fun_P_0(Tb!2, X!12), P2!6)) | (~greater(P1!7, tptp_fun_P_0(Tb!2, X!12))))) <=> ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | greater(P1!7, P2!6) | (~greater(P1!7, tptp_fun_P_0(Tb!2, X!12))) | (~greater(tptp_fun_P_0(Tb!2, X!12), P2!6)))),
% 0.66/0.93 inference(transitivity,[status(thm)],[131, 129])).
% 0.66/0.93 tff(133,plain,
% 0.66/0.93 ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | (greater(P1!7, P2!6) | (~greater(tptp_fun_P_0(Tb!2, X!12), P2!6)) | (~greater(P1!7, tptp_fun_P_0(Tb!2, X!12))))),
% 0.66/0.93 inference(quant_inst,[status(thm)],[])).
% 0.66/0.93 tff(134,plain,
% 0.66/0.93 ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | greater(P1!7, P2!6) | (~greater(P1!7, tptp_fun_P_0(Tb!2, X!12))) | (~greater(tptp_fun_P_0(Tb!2, X!12), P2!6))),
% 0.66/0.93 inference(modus_ponens,[status(thm)],[133, 132])).
% 0.66/0.93 tff(135,plain,
% 0.66/0.93 ($false),
% 0.66/0.93 inference(unit_resolution,[status(thm)],[134, 128, 116, 115, 1])).
% 0.66/0.93 tff(136,plain,(~greater(tptp_fun_P_0(Tb!2, X!12), P2!6)), inference(lemma,lemma(discharge,[]))).
% 0.66/0.93 tff(137,assumption,(greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)), introduced(assumption)).
% 0.66/0.93 tff(138,assumption,(~greater(tptp_fun_P_0(Tb!2, X!12), P2!6)), introduced(assumption)).
% 0.66/0.93 tff(139,assumption,(greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))), introduced(assumption)).
% 0.66/0.93 tff(140,plain,
% 0.66/0.93 (((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | (greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)))) <=> ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)))),
% 0.66/0.93 inference(rewrite,[status(thm)],[])).
% 0.66/0.93 tff(141,plain,
% 0.66/0.93 ((greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)) | (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11)))) <=> (greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)))),
% 0.66/0.93 inference(rewrite,[status(thm)],[])).
% 0.66/0.93 tff(142,plain,
% 0.66/0.93 (((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | (greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)) | (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))))) <=> ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | (greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6))))),
% 0.66/0.93 inference(monotonicity,[status(thm)],[141])).
% 0.66/0.93 tff(143,plain,
% 0.66/0.93 (((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | (greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)) | (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))))) <=> ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)))),
% 0.66/0.94 inference(transitivity,[status(thm)],[142, 140])).
% 0.66/0.94 tff(144,plain,
% 0.66/0.94 ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | (greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)) | (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))))),
% 0.66/0.94 inference(quant_inst,[status(thm)],[])).
% 0.66/0.94 tff(145,plain,
% 0.66/0.94 ((~![X: $i, Y: $i, Z: $i] : (greater(X, Z) | (~greater(Y, Z)) | (~greater(X, Y)))) | greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6))),
% 0.66/0.94 inference(modus_ponens,[status(thm)],[144, 143])).
% 0.66/0.94 tff(146,plain,
% 0.66/0.94 ($false),
% 0.66/0.94 inference(unit_resolution,[status(thm)],[145, 128, 138, 139, 137])).
% 0.66/0.94 tff(147,plain,((~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))) | greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6))), inference(lemma,lemma(discharge,[]))).
% 0.66/0.94 tff(148,plain,
% 0.66/0.94 (~greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))),
% 0.66/0.94 inference(unit_resolution,[status(thm)],[147, 138, 137])).
% 0.66/0.94 tff(149,plain,
% 0.66/0.94 (((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | ((~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2)) | organization(Y!11, Tb!2))) <=> ((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2)) | organization(Y!11, Tb!2))),
% 0.66/0.94 inference(rewrite,[status(thm)],[])).
% 0.66/0.94 tff(150,plain,
% 0.66/0.94 ((organization(Y!11, Tb!2) | (~greater(Tb!2, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~greater(Tc!1, Tb!2))) <=> ((~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2)) | organization(Y!11, Tb!2))),
% 0.66/0.94 inference(rewrite,[status(thm)],[])).
% 0.66/0.94 tff(151,plain,
% 0.66/0.94 (((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (organization(Y!11, Tb!2) | (~greater(Tb!2, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~greater(Tc!1, Tb!2)))) <=> ((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | ((~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2)) | organization(Y!11, Tb!2)))),
% 0.66/0.94 inference(monotonicity,[status(thm)],[150])).
% 0.66/0.94 tff(152,plain,
% 0.66/0.94 (((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (organization(Y!11, Tb!2) | (~greater(Tb!2, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~greater(Tc!1, Tb!2)))) <=> ((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2)) | organization(Y!11, Tb!2))),
% 0.66/0.94 inference(transitivity,[status(thm)],[151, 149])).
% 0.66/0.94 tff(153,plain,
% 0.66/0.94 ((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (organization(Y!11, Tb!2) | (~greater(Tb!2, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~greater(Tc!1, Tb!2)))),
% 0.66/0.94 inference(quant_inst,[status(thm)],[])).
% 0.66/0.94 tff(154,plain,
% 0.66/0.94 ((~![X: $i, T: $i, T1: $i, T2: $i] : (organization(X, T) | (~greater(T, T1)) | (~organization(X, T1)) | (~organization(X, T2)) | (~greater(T2, T)))) | (~organization(Y!11, Ta!3)) | (~organization(Y!11, Tc!1)) | (~greater(Tb!2, Ta!3)) | (~greater(Tc!1, Tb!2)) | organization(Y!11, Tb!2)),
% 0.66/0.94 inference(modus_ponens,[status(thm)],[153, 152])).
% 0.66/0.94 tff(155,plain,
% 0.66/0.94 (organization(Y!11, Tb!2)),
% 0.66/0.94 inference(unit_resolution,[status(thm)],[154, 71, 22, 21, 57, 43])).
% 0.66/0.94 tff(156,plain,
% 0.66/0.94 (((~![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))) | ((~organization(Y!11, Tb!2)) | survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2))) <=> ((~![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))) | (~organization(Y!11, Tb!2)) | survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2))),
% 0.66/0.94 inference(rewrite,[status(thm)],[])).
% 0.66/0.94 tff(157,plain,
% 0.66/0.94 ((~![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))) | ((~organization(Y!11, Tb!2)) | survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2))),
% 0.66/0.94 inference(quant_inst,[status(thm)],[])).
% 0.66/0.94 tff(158,plain,
% 0.66/0.94 ((~![X: $i, T: $i] : ((~organization(X, T)) | survival_chance(X, tptp_fun_P_0(T, X), T))) | (~organization(Y!11, Tb!2)) | survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)),
% 0.66/0.94 inference(modus_ponens,[status(thm)],[157, 156])).
% 0.66/0.94 tff(159,plain,
% 0.66/0.94 (survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)),
% 0.66/0.94 inference(unit_resolution,[status(thm)],[158, 89, 155])).
% 0.66/0.94 tff(160,plain,
% 0.66/0.94 (survival_chance(Y!11, P!8, Ta!3)),
% 0.66/0.94 inference(and_elim,[status(thm)],[11])).
% 0.66/0.94 tff(161,plain,
% 0.66/0.94 (survival_chance(X!12, P!8, Ta!3)),
% 0.66/0.94 inference(and_elim,[status(thm)],[11])).
% 0.66/0.94 tff(162,plain,
% 0.66/0.94 (^[X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : refl(((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta))) <=> ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta))))),
% 0.66/0.94 inference(bind,[status(th)],[])).
% 0.66/0.94 tff(163,plain,
% 0.66/0.94 (![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta))) <=> ![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))),
% 0.66/0.94 inference(quant_intro,[status(thm)],[162])).
% 0.66/0.94 tff(164,plain,
% 0.66/0.94 (^[X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : trans(monotonicity(trans(monotonicity(rewrite((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)) <=> (~((~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta))))), ((~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) <=> (~(~((~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta))))))), rewrite((~(~((~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta))))) <=> ((~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))), ((~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))) <=> ((~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta))))), (((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)))) <=> ((P1 = P2) | greater(P1, P2) | ((~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))))), rewrite(((P1 = P2) | greater(P1, P2) | ((~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))) <=> ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))), (((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)))) <=> ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))))),
% 0.66/0.94 inference(bind,[status(th)],[])).
% 0.66/0.94 tff(165,plain,
% 0.66/0.94 (![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)))) <=> ![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))),
% 0.66/0.94 inference(quant_intro,[status(thm)],[164])).
% 0.66/0.94 tff(166,plain,
% 0.66/0.94 (![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)))) <=> ![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))))),
% 0.66/0.94 inference(rewrite,[status(thm)],[])).
% 0.66/0.94 tff(167,plain,
% 0.66/0.94 (^[X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb))), ((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb)) & organization(Y, Tb)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb)) & organization(Y, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb))), ((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb)))), (((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb)) & class(X, C, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb)) & class(X, C, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta))), (((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta)))), ((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta)) & class(Y, C, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta)) & class(Y, C, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta))), ((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta)))), (((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta)) & survival_chance(X, P, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta))), (((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta)))), ((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta))), ((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta)))), (((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb))), (((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb)))), ((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc))), ((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc)))), (((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta))), (((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta)))), ((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta))), ((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta)))), (((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb))), (((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb)))), ((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb))), ((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb)))), (((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta))), (((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta)))), ((((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta))), ((((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta)))), (((((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta)) & greater(C2, C1)))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta)) & greater(C2, C1)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))), (((((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) <=> (organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)))), rewrite((greater(P1, P2) | (P1 = P2)) <=> ((P1 = P2) | greater(P1, P2))), ((((((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) => (greater(P1, P2) | (P1 = P2))) <=> ((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)) => ((P1 = P2) | greater(P1, P2))))), rewrite(((organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1)) => ((P1 = P2) | greater(P1, P2))) <=> ((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))))), ((((((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) => (greater(P1, P2) | (P1 = P2))) <=> ((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))))))),
% 0.66/0.95 inference(bind,[status(th)],[])).
% 0.66/0.95 tff(168,plain,
% 0.66/0.95 (![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (((((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) => (greater(P1, P2) | (P1 = P2))) <=> ![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))))),
% 0.66/0.95 inference(quant_intro,[status(thm)],[167])).
% 0.66/0.95 tff(169,axiom,(![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : (((((((((((((((((organization(X, Ta) & organization(Y, Ta)) & organization(X, Tb)) & organization(Y, Tb)) & class(X, C, Ta)) & class(Y, C, Ta)) & survival_chance(X, P, Ta)) & survival_chance(Y, P, Ta)) & reorganization(X, Ta, Tb)) & reorganization(Y, Ta, Tc)) & reorganization_type(X, Re, Ta)) & reorganization_type(Y, Re, Ta)) & survival_chance(X, P1, Tb)) & survival_chance(Y, P2, Tb)) & complexity(X, C1, Ta)) & complexity(Y, C2, Ta)) & greater(C2, C1)) => (greater(P1, P2) | (P1 = P2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','a11_FOL')).
% 0.66/0.95 tff(170,plain,
% 0.66/0.95 (![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))))),
% 0.66/0.95 inference(modus_ponens,[status(thm)],[169, 168])).
% 0.66/0.95 tff(171,plain,
% 0.66/0.95 (![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))))),
% 0.66/0.95 inference(modus_ponens,[status(thm)],[170, 166])).
% 0.66/0.95 tff(172,plain,(
% 0.66/0.95 ![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~(organization(X, Ta) & organization(Y, Ta) & organization(X, Tb) & organization(Y, Tb) & class(X, C, Ta) & class(Y, C, Ta) & survival_chance(X, P, Ta) & survival_chance(Y, P, Ta) & reorganization(X, Ta, Tb) & reorganization(Y, Ta, Tc) & reorganization_type(X, Re, Ta) & reorganization_type(Y, Re, Ta) & survival_chance(X, P1, Tb) & survival_chance(Y, P2, Tb) & complexity(X, C1, Ta) & complexity(Y, C2, Ta) & greater(C2, C1))))),
% 0.66/0.95 inference(skolemize,[status(sab)],[171])).
% 0.66/0.95 tff(173,plain,
% 0.66/0.95 (![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))),
% 0.66/0.95 inference(modus_ponens,[status(thm)],[172, 165])).
% 0.66/0.95 tff(174,plain,
% 0.66/0.95 (![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))),
% 0.66/0.95 inference(modus_ponens,[status(thm)],[173, 163])).
% 0.66/0.95 tff(175,plain,
% 0.66/0.95 (((~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))) | ((~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~survival_chance(X!12, P!8, Ta!3)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P!8, Ta!3)) | (~organization(X!12, Tb!2)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11)))) <=> ((~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))) | (~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~survival_chance(X!12, P!8, Ta!3)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P!8, Ta!3)) | (~organization(X!12, Tb!2)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11)))),
% 0.66/0.95 inference(rewrite,[status(thm)],[])).
% 0.66/0.95 tff(176,plain,
% 0.66/0.95 (((tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11)) | (~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(X!12, Tb!2)) | (~organization(Y!11, Tb!2)) | (~class(X!12, C!9, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~survival_chance(X!12, P!8, Ta!3)) | (~survival_chance(Y!11, P!8, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (~complexity(X!12, C1!5, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3))) <=> ((~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~survival_chance(X!12, P!8, Ta!3)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P!8, Ta!3)) | (~organization(X!12, Tb!2)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11)))),
% 0.66/0.95 inference(rewrite,[status(thm)],[])).
% 0.66/0.95 tff(177,plain,
% 0.66/0.95 (((~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))) | ((tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11)) | (~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(X!12, Tb!2)) | (~organization(Y!11, Tb!2)) | (~class(X!12, C!9, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~survival_chance(X!12, P!8, Ta!3)) | (~survival_chance(Y!11, P!8, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (~complexity(X!12, C1!5, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)))) <=> ((~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))) | ((~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~survival_chance(X!12, P!8, Ta!3)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P!8, Ta!3)) | (~organization(X!12, Tb!2)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))))),
% 0.66/0.96 inference(monotonicity,[status(thm)],[176])).
% 0.66/0.96 tff(178,plain,
% 0.66/0.96 (((~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))) | ((tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11)) | (~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(X!12, Tb!2)) | (~organization(Y!11, Tb!2)) | (~class(X!12, C!9, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~survival_chance(X!12, P!8, Ta!3)) | (~survival_chance(Y!11, P!8, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (~complexity(X!12, C1!5, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)))) <=> ((~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))) | (~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~survival_chance(X!12, P!8, Ta!3)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P!8, Ta!3)) | (~organization(X!12, Tb!2)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11)))),
% 0.66/0.96 inference(transitivity,[status(thm)],[177, 175])).
% 0.66/0.96 tff(179,plain,
% 0.66/0.96 ((~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))) | ((tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11)) | (~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~organization(X!12, Tb!2)) | (~organization(Y!11, Tb!2)) | (~class(X!12, C!9, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~survival_chance(X!12, P!8, Ta!3)) | (~survival_chance(Y!11, P!8, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (~complexity(X!12, C1!5, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)))),
% 0.66/0.96 inference(quant_inst,[status(thm)],[])).
% 0.66/0.96 tff(180,plain,
% 0.66/0.96 ((~![X: $i, Y: $i, Re: $i, C: $i, P: $i, P1: $i, P2: $i, C1: $i, C2: $i, Ta: $i, Tb: $i, Tc: $i] : ((P1 = P2) | greater(P1, P2) | (~greater(C2, C1)) | (~organization(X, Ta)) | (~organization(Y, Ta)) | (~organization(X, Tb)) | (~organization(Y, Tb)) | (~class(X, C, Ta)) | (~class(Y, C, Ta)) | (~survival_chance(X, P, Ta)) | (~survival_chance(Y, P, Ta)) | (~reorganization(X, Ta, Tb)) | (~reorganization(Y, Ta, Tc)) | (~reorganization_type(X, Re, Ta)) | (~reorganization_type(Y, Re, Ta)) | (~survival_chance(X, P1, Tb)) | (~survival_chance(Y, P2, Tb)) | (~complexity(X, C1, Ta)) | (~complexity(Y, C2, Ta)))) | (~greater(C2!4, C1!5)) | (~organization(X!12, Ta!3)) | (~organization(Y!11, Ta!3)) | (~reorganization(X!12, Ta!3, Tb!2)) | (~survival_chance(X!12, P!8, Ta!3)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P!8, Ta!3)) | (~organization(X!12, Tb!2)) | (~class(X!12, C!9, Ta!3)) | (~reorganization_type(X!12, Re!10, Ta!3)) | (~complexity(X!12, C1!5, Ta!3)) | (~class(Y!11, C!9, Ta!3)) | (~reorganization_type(Y!11, Re!10, Ta!3)) | (~complexity(Y!11, C2!4, Ta!3)) | (~survival_chance(X!12, tptp_fun_P_0(Tb!2, X!12), Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))),
% 0.66/0.96 inference(modus_ponens,[status(thm)],[179, 178])).
% 0.66/0.96 tff(181,plain,
% 0.66/0.96 ((tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)) | greater(tptp_fun_P_0(Tb!2, X!12), tptp_fun_P_0(Tb!2, Y!11))),
% 0.66/0.96 inference(unit_resolution,[status(thm)],[180, 174, 23, 22, 20, 19, 161, 160, 18, 17, 16, 15, 14, 13, 12, 79, 93, 155, 159])).
% 0.66/0.96 tff(182,plain,
% 0.66/0.96 (tptp_fun_P_0(Tb!2, X!12) = tptp_fun_P_0(Tb!2, Y!11)),
% 0.66/0.96 inference(unit_resolution,[status(thm)],[181, 148])).
% 0.66/0.96 tff(183,plain,
% 0.66/0.96 (greater(tptp_fun_P_0(Tb!2, X!12), P2!6) <=> greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)),
% 0.66/0.96 inference(monotonicity,[status(thm)],[182])).
% 0.66/0.96 tff(184,plain,
% 0.66/0.96 (greater(tptp_fun_P_0(Tb!2, Y!11), P2!6) <=> greater(tptp_fun_P_0(Tb!2, X!12), P2!6)),
% 0.66/0.96 inference(symmetry,[status(thm)],[183])).
% 0.66/0.96 tff(185,plain,
% 0.66/0.96 (greater(tptp_fun_P_0(Tb!2, X!12), P2!6)),
% 0.66/0.96 inference(modus_ponens,[status(thm)],[137, 184])).
% 0.66/0.96 tff(186,plain,
% 0.66/0.96 ($false),
% 0.66/0.96 inference(unit_resolution,[status(thm)],[138, 185])).
% 0.66/0.96 tff(187,plain,(greater(tptp_fun_P_0(Tb!2, X!12), P2!6) | (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6))), inference(lemma,lemma(discharge,[]))).
% 0.66/0.96 tff(188,plain,
% 0.66/0.96 (~greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)),
% 0.66/0.96 inference(unit_resolution,[status(thm)],[187, 136])).
% 0.66/0.96 tff(189,plain,
% 0.66/0.96 (^[X: $i, Y: $i] : refl(((~greater(X, Y)) | (~greater(Y, X))) <=> ((~greater(X, Y)) | (~greater(Y, X))))),
% 0.66/0.96 inference(bind,[status(th)],[])).
% 0.66/0.96 tff(190,plain,
% 0.66/0.96 (![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X))) <=> ![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))),
% 0.66/0.96 inference(quant_intro,[status(thm)],[189])).
% 0.66/0.96 tff(191,plain,
% 0.66/0.96 (^[X: $i, Y: $i] : trans(monotonicity(rewrite((greater(X, Y) & greater(Y, X)) <=> (~((~greater(X, Y)) | (~greater(Y, X))))), ((~(greater(X, Y) & greater(Y, X))) <=> (~(~((~greater(X, Y)) | (~greater(Y, X))))))), rewrite((~(~((~greater(X, Y)) | (~greater(Y, X))))) <=> ((~greater(X, Y)) | (~greater(Y, X)))), ((~(greater(X, Y) & greater(Y, X))) <=> ((~greater(X, Y)) | (~greater(Y, X)))))),
% 0.66/0.96 inference(bind,[status(th)],[])).
% 0.66/0.96 tff(192,plain,
% 0.66/0.96 (![X: $i, Y: $i] : (~(greater(X, Y) & greater(Y, X))) <=> ![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))),
% 0.66/0.96 inference(quant_intro,[status(thm)],[191])).
% 0.66/0.96 tff(193,plain,
% 0.66/0.96 (![X: $i, Y: $i] : (~(greater(X, Y) & greater(Y, X))) <=> ![X: $i, Y: $i] : (~(greater(X, Y) & greater(Y, X)))),
% 0.66/0.96 inference(rewrite,[status(thm)],[])).
% 0.66/0.96 tff(194,axiom,(![X: $i, Y: $i] : (~(greater(X, Y) & greater(Y, X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mp6_2')).
% 0.66/0.96 tff(195,plain,
% 0.66/0.96 (![X: $i, Y: $i] : (~(greater(X, Y) & greater(Y, X)))),
% 0.66/0.96 inference(modus_ponens,[status(thm)],[194, 193])).
% 0.66/0.96 tff(196,plain,(
% 0.66/0.96 ![X: $i, Y: $i] : (~(greater(X, Y) & greater(Y, X)))),
% 0.66/0.96 inference(skolemize,[status(sab)],[195])).
% 0.66/0.96 tff(197,plain,
% 0.66/0.96 (![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))),
% 0.66/0.96 inference(modus_ponens,[status(thm)],[196, 192])).
% 0.66/0.96 tff(198,plain,
% 0.66/0.96 (![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))),
% 0.66/0.96 inference(modus_ponens,[status(thm)],[197, 190])).
% 0.66/0.96 tff(199,plain,
% 0.66/0.96 (((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | ((~greater(Ta!3, Tb!2)) | (~greater(Tb!2, Ta!3)))) <=> ((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | (~greater(Ta!3, Tb!2)) | (~greater(Tb!2, Ta!3)))),
% 0.66/0.96 inference(rewrite,[status(thm)],[])).
% 0.66/0.96 tff(200,plain,
% 0.66/0.96 ((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | ((~greater(Ta!3, Tb!2)) | (~greater(Tb!2, Ta!3)))),
% 0.66/0.96 inference(quant_inst,[status(thm)],[])).
% 0.66/0.96 tff(201,plain,
% 0.66/0.96 ((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | (~greater(Ta!3, Tb!2)) | (~greater(Tb!2, Ta!3))),
% 0.66/0.96 inference(modus_ponens,[status(thm)],[200, 199])).
% 0.66/0.96 tff(202,plain,
% 0.66/0.96 (~greater(Ta!3, Tb!2)),
% 0.66/0.96 inference(unit_resolution,[status(thm)],[201, 198, 57])).
% 0.66/0.96 tff(203,plain,
% 0.66/0.96 (survival_chance(Y!11, P2!6, Tc!1)),
% 0.66/0.96 inference(and_elim,[status(thm)],[11])).
% 0.66/0.96 tff(204,plain,
% 0.66/0.96 (^[X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : refl((greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1))) <=> (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1))))),
% 0.66/0.96 inference(bind,[status(th)],[])).
% 0.66/0.96 tff(205,plain,
% 0.66/0.96 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1))) <=> ![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))),
% 0.66/0.96 inference(quant_intro,[status(thm)],[204])).
% 0.66/0.96 tff(206,plain,
% 0.66/0.96 (^[X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : trans(monotonicity(trans(monotonicity(rewrite((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb))) <=> (~(greater(T2, Tb) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1))))), ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) <=> (~(~(greater(T2, Tb) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1))))))), rewrite((~(~(greater(T2, Tb) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1))))) <=> (greater(T2, Tb) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))), ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) <=> (greater(T2, Tb) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1))))), (((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2)) <=> ((greater(T2, Tb) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1))) | greater(P1, P2)))), rewrite(((greater(T2, Tb) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1))) | greater(P1, P2)) <=> (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))), (((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2)) <=> (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))))),
% 0.66/0.96 inference(bind,[status(th)],[])).
% 0.66/0.96 tff(207,plain,
% 0.66/0.96 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2)) <=> ![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))),
% 0.66/0.97 inference(quant_intro,[status(thm)],[206])).
% 0.66/0.97 tff(208,plain,
% 0.66/0.97 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2)) <=> ![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2))),
% 0.66/0.97 inference(rewrite,[status(thm)],[])).
% 0.66/0.97 tff(209,plain,
% 0.66/0.97 (^[X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb))), ((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) <=> ((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)))), rewrite(((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1))), ((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1)))), (((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) <=> ((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)))), rewrite(((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2))), (((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2)))), ((((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) <=> ((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))))), rewrite(((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)))), ((((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1))))), (((((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) & greater(T2, T1)) <=> ((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1))) & greater(T2, T1)))), rewrite(((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1))) & greater(T2, T1)) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1))), (((((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) & greater(T2, T1)) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1)))), ((((((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) & greater(T2, T1)) & (~greater(T2, Tb))) <=> ((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1)) & (~greater(T2, Tb))))), rewrite(((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1)) & (~greater(T2, Tb))) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))), ((((((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) & greater(T2, T1)) & (~greater(T2, Tb))) <=> (organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb))))), (((((((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) & greater(T2, T1)) & (~greater(T2, Tb))) => greater(P1, P2)) <=> ((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb))) => greater(P1, P2)))), rewrite(((organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb))) => greater(P1, P2)) <=> ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2))), (((((((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) & greater(T2, T1)) & (~greater(T2, Tb))) => greater(P1, P2)) <=> ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2))))),
% 0.66/0.97 inference(bind,[status(th)],[])).
% 0.66/0.97 tff(210,plain,
% 0.66/0.97 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : ((((((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) & greater(T2, T1)) & (~greater(T2, Tb))) => greater(P1, P2)) <=> ![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2))),
% 0.66/0.97 inference(quant_intro,[status(thm)],[209])).
% 0.66/0.97 tff(211,axiom,(![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : ((((((((organization(X, T1) & organization(X, T2)) & reorganization(X, Ta, Tb)) & survival_chance(X, P1, T1)) & survival_chance(X, P2, T2)) & (~greater(Ta, T1))) & greater(T2, T1)) & (~greater(T2, Tb))) => greater(P1, P2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t4_FOL')).
% 0.66/0.97 tff(212,plain,
% 0.66/0.97 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2))),
% 0.66/0.97 inference(modus_ponens,[status(thm)],[211, 210])).
% 0.66/0.97 tff(213,plain,
% 0.66/0.97 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2))),
% 0.66/0.97 inference(modus_ponens,[status(thm)],[212, 208])).
% 0.66/0.97 tff(214,plain,(
% 0.66/0.97 ![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : ((~(organization(X, T1) & organization(X, T2) & reorganization(X, Ta, Tb) & survival_chance(X, P1, T1) & survival_chance(X, P2, T2) & (~greater(Ta, T1)) & greater(T2, T1) & (~greater(T2, Tb)))) | greater(P1, P2))),
% 0.66/0.97 inference(skolemize,[status(sab)],[213])).
% 0.66/0.97 tff(215,plain,
% 0.66/0.97 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))),
% 0.66/0.97 inference(modus_ponens,[status(thm)],[214, 207])).
% 0.66/0.97 tff(216,plain,
% 0.66/0.97 (![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))),
% 0.66/0.97 inference(modus_ponens,[status(thm)],[215, 205])).
% 0.66/0.97 tff(217,plain,
% 0.66/0.97 (((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))) | ((~organization(Y!11, Tc!1)) | greater(Ta!3, Tb!2) | greater(Tc!1, Tc!1) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P2!6, Tc!1)) | (~greater(Tc!1, Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6))) <=> ((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))) | (~organization(Y!11, Tc!1)) | greater(Ta!3, Tb!2) | greater(Tc!1, Tc!1) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P2!6, Tc!1)) | (~greater(Tc!1, Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6))),
% 0.66/0.97 inference(rewrite,[status(thm)],[])).
% 0.66/0.97 tff(218,plain,
% 0.66/0.97 ((greater(Tc!1, Tc!1) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6) | greater(Ta!3, Tb!2) | (~organization(Y!11, Tb!2)) | (~organization(Y!11, Tc!1)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (~survival_chance(Y!11, P2!6, Tc!1)) | (~greater(Tc!1, Tb!2))) <=> ((~organization(Y!11, Tc!1)) | greater(Ta!3, Tb!2) | greater(Tc!1, Tc!1) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P2!6, Tc!1)) | (~greater(Tc!1, Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6))),
% 0.66/0.97 inference(rewrite,[status(thm)],[])).
% 0.66/0.97 tff(219,plain,
% 0.66/0.97 (((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))) | (greater(Tc!1, Tc!1) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6) | greater(Ta!3, Tb!2) | (~organization(Y!11, Tb!2)) | (~organization(Y!11, Tc!1)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (~survival_chance(Y!11, P2!6, Tc!1)) | (~greater(Tc!1, Tb!2)))) <=> ((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))) | ((~organization(Y!11, Tc!1)) | greater(Ta!3, Tb!2) | greater(Tc!1, Tc!1) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P2!6, Tc!1)) | (~greater(Tc!1, Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)))),
% 0.66/0.97 inference(monotonicity,[status(thm)],[218])).
% 0.66/0.97 tff(220,plain,
% 0.66/0.97 (((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))) | (greater(Tc!1, Tc!1) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6) | greater(Ta!3, Tb!2) | (~organization(Y!11, Tb!2)) | (~organization(Y!11, Tc!1)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (~survival_chance(Y!11, P2!6, Tc!1)) | (~greater(Tc!1, Tb!2)))) <=> ((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))) | (~organization(Y!11, Tc!1)) | greater(Ta!3, Tb!2) | greater(Tc!1, Tc!1) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P2!6, Tc!1)) | (~greater(Tc!1, Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6))),
% 0.66/0.97 inference(transitivity,[status(thm)],[219, 217])).
% 0.66/0.97 tff(221,plain,
% 0.66/0.97 ((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))) | (greater(Tc!1, Tc!1) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6) | greater(Ta!3, Tb!2) | (~organization(Y!11, Tb!2)) | (~organization(Y!11, Tc!1)) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | (~survival_chance(Y!11, P2!6, Tc!1)) | (~greater(Tc!1, Tb!2)))),
% 0.66/0.97 inference(quant_inst,[status(thm)],[])).
% 0.66/0.97 tff(222,plain,
% 0.66/0.97 ((~![X: $i, P1: $i, P2: $i, T1: $i, T2: $i, Ta: $i, Tb: $i] : (greater(T2, Tb) | greater(P1, P2) | greater(Ta, T1) | (~organization(X, T1)) | (~organization(X, T2)) | (~reorganization(X, Ta, Tb)) | (~survival_chance(X, P1, T1)) | (~survival_chance(X, P2, T2)) | (~greater(T2, T1)))) | (~organization(Y!11, Tc!1)) | greater(Ta!3, Tb!2) | greater(Tc!1, Tc!1) | (~reorganization(Y!11, Ta!3, Tc!1)) | (~survival_chance(Y!11, P2!6, Tc!1)) | (~greater(Tc!1, Tb!2)) | (~organization(Y!11, Tb!2)) | (~survival_chance(Y!11, tptp_fun_P_0(Tb!2, Y!11), Tb!2)) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)),
% 0.66/0.97 inference(modus_ponens,[status(thm)],[221, 220])).
% 0.66/0.97 tff(223,plain,
% 0.66/0.97 (greater(Tc!1, Tc!1) | greater(tptp_fun_P_0(Tb!2, Y!11), P2!6)),
% 0.66/0.97 inference(unit_resolution,[status(thm)],[222, 216, 21, 17, 203, 43, 202, 155, 159])).
% 0.66/0.97 tff(224,plain,
% 0.66/0.97 (greater(Tc!1, Tc!1)),
% 0.66/0.97 inference(unit_resolution,[status(thm)],[223, 188])).
% 0.66/0.97 tff(225,plain,
% 0.66/0.97 (((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | (~greater(Tc!1, Tc!1))) <=> ((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | (~greater(Tc!1, Tc!1)))),
% 0.66/0.97 inference(rewrite,[status(thm)],[])).
% 0.66/0.98 tff(226,plain,
% 0.66/0.98 (((~greater(Tc!1, Tc!1)) | (~greater(Tc!1, Tc!1))) <=> (~greater(Tc!1, Tc!1))),
% 0.66/0.98 inference(rewrite,[status(thm)],[])).
% 0.66/0.98 tff(227,plain,
% 0.66/0.98 (((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | ((~greater(Tc!1, Tc!1)) | (~greater(Tc!1, Tc!1)))) <=> ((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | (~greater(Tc!1, Tc!1)))),
% 0.66/0.98 inference(monotonicity,[status(thm)],[226])).
% 0.66/0.98 tff(228,plain,
% 0.66/0.98 (((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | ((~greater(Tc!1, Tc!1)) | (~greater(Tc!1, Tc!1)))) <=> ((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | (~greater(Tc!1, Tc!1)))),
% 0.66/0.98 inference(transitivity,[status(thm)],[227, 225])).
% 0.66/0.98 tff(229,plain,
% 0.66/0.98 ((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | ((~greater(Tc!1, Tc!1)) | (~greater(Tc!1, Tc!1)))),
% 0.66/0.98 inference(quant_inst,[status(thm)],[])).
% 0.66/0.98 tff(230,plain,
% 0.66/0.98 ((~![X: $i, Y: $i] : ((~greater(X, Y)) | (~greater(Y, X)))) | (~greater(Tc!1, Tc!1))),
% 0.66/0.98 inference(modus_ponens,[status(thm)],[229, 228])).
% 0.66/0.98 tff(231,plain,
% 0.66/0.98 ($false),
% 0.66/0.98 inference(unit_resolution,[status(thm)],[230, 198, 224])).
% 0.66/0.98 % SZS output end Proof
% 0.66/0.98 % E exiting
%------------------------------------------------------------------------------