%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT036+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n011.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:04:18 AM UTC 2026 % Result : Theorem 0.28s 0.47s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT036+2 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.33 % Computer : n011.cluster.edu % 0.08/0.33 % Model : x86_64 x86_64 % 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.33 % Memory : 8046.5625MB % 0.08/0.33 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.34 % WCLimit : 300 % 0.08/0.34 % DateTime : Mon Sep 7 12:41:00 UTC 2026 % 0.08/0.34 % CPUTime : % 0.12/0.44 start to proof:theBenchmark % 0.12/0.47 %------------------------------------------- % 0.12/0.47 % File :CSE---1.7 % 0.12/0.47 % Problem :theBenchmark % 0.12/0.47 % Transform :cnf % 0.12/0.47 % Format :tptp:raw % 0.12/0.47 % Command :java -jar mcs_scs.jar %d %s % 0.12/0.47 % 0.12/0.47 % Result :Theorem 0.014165s % 0.12/0.47 % Output :CNFRefutation 0.014165s % 0.12/0.47 %------------------------------------------- % 0.28/0.47 %-------------------------------------------------------------------------- % 0.28/0.47 % File : MGT036+2 : TPTP v9.3.0. Released v2.0.0. % 0.28/0.47 % Domain : Management (Organisation Theory) % 0.28/0.47 % Problem : First movers never outcompete efficient producers. % 0.28/0.47 % Version : [PM93] axioms. % 0.28/0.47 % English : % 0.28/0.47 % 0.28/0.47 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 0.28/0.47 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 0.28/0.47 % : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing % 0.28/0.47 % Source : [PM93] % 0.28/0.47 % Names : THEOREM 5 [PM93] % 0.28/0.47 % : T5 [PB+94] % 0.28/0.47 % 0.28/0.47 % Status : Theorem % 0.28/0.47 % Rating : 0.00 v9.1.0, 0.07 v9.0.0, 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.12 v5.4.0, 0.09 v5.3.0, 0.17 v5.2.0, 0.07 v5.0.0, 0.05 v4.1.0, 0.06 v4.0.1, 0.05 v3.7.0, 0.00 v2.1.0 % 0.28/0.47 % Syntax : Number of formulae : 7 ( 1 unt; 0 def) % 0.28/0.47 % Number of atoms : 24 ( 0 equ) % 0.28/0.47 % Maximal formula atoms : 5 ( 3 avg) % 0.28/0.47 % Number of connectives : 21 ( 4 ~; 0 |; 9 &) % 0.28/0.47 % ( 2 <=>; 6 =>; 0 <=; 0 <~>) % 0.28/0.47 % Maximal formula depth : 10 ( 6 avg) % 0.28/0.47 % Maximal term depth : 2 ( 1 avg) % 0.28/0.47 % Number of predicates : 6 ( 6 usr; 0 prp; 1-4 aty) % 0.28/0.47 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty) % 0.28/0.47 % Number of variables : 20 ( 20 !; 0 ?) % 0.28/0.47 % SPC : FOF_THM_RFO_NEQ % 0.28/0.47 % 0.28/0.47 % Comments : % 0.28/0.47 %-------------------------------------------------------------------------- % 0.28/0.47 %----MP. The "pop" predicate is symmetric: if S1 and S2 are subpopulations, % 0.28/0.47 %----then S2 and S1 are also subpopulations. % 0.28/0.47 fof(mp_symmetry_of_subpopulations,axiom, % 0.28/0.47 ! [E,S1,S2,T] : % 0.28/0.47 ( ( environment(E) % 0.28/0.47 & subpopulations(S1,S2,E,T) ) % 0.28/0.47 => subpopulations(S2,S1,E,T) ) ). % 0.28/0.47 % 0.28/0.47 %----MP. The time points when FM and EP are present in the environment % 0.28/0.47 %----occur during the environment sustains. % 0.28/0.47 fof(mp_time_point_occur,axiom, % 0.28/0.47 ! [E,T] : % 0.28/0.47 ( ( environment(E) % 0.28/0.47 & subpopulations(first_movers,efficient_producers,E,T) ) % 0.28/0.47 => in_environment(E,T) ) ). % 0.28/0.47 % 0.28/0.47 %----MP. on "greater or equal to" % 0.28/0.47 fof(mp_growth_rate_relationships,axiom, % 0.28/0.47 ! [E,S1,S2,T] : % 0.28/0.47 ( ( ( environment(E) % 0.28/0.47 & subpopulations(S1,S2,E,T) ) % 0.28/0.47 => greater_or_equal(growth_rate(S1,T),zero) ) % 0.28/0.47 <=> ~ greater(zero,growth_rate(S1,T)) ) ). % 0.28/0.47 % 0.28/0.47 %----D2. A subpopulation outcompetes an other in an environment at a % 0.28/0.47 %----certain time, if and only if, it has non-negative growth rate while % 0.28/0.47 %----the other subpopulation has negative growth rate. % 0.28/0.47 fof(d2,hypothesis, % 0.28/0.47 ! [E,S1,S2,T] : % 0.28/0.47 ( ( environment(E) % 0.28/0.47 & subpopulations(S1,S2,E,T) ) % 0.28/0.47 => ( ( greater_or_equal(growth_rate(S2,T),zero) % 0.28/0.47 & greater(zero,growth_rate(S1,T)) ) % 0.28/0.47 <=> outcompetes(S2,S1,T) ) ) ). % 0.28/0.47 % 0.28/0.47 %----A2. Efficient producers are more resilient than first movers. % 0.28/0.47 fof(a2,hypothesis, % 0.28/0.47 greater(resilience(efficient_producers),resilience(first_movers)) ). % 0.28/0.47 % 0.28/0.47 %----A13. If a less resilient organizational group does not decrease in a % 0.28/0.47 %----given environment, then a more resilient organizational group does not % 0.28/0.47 %----decrease either in the same environment. % 0.28/0.47 fof(a13,hypothesis, % 0.28/0.47 ! [E,S1,S2,T] : % 0.28/0.47 ( ( environment(E) % 0.28/0.47 & in_environment(E,T) % 0.28/0.47 & ~ greater(zero,growth_rate(S1,T)) % 0.28/0.47 & greater(resilience(S2),resilience(S1)) ) % 0.28/0.47 => ~ greater(zero,growth_rate(S2,T)) ) ). % 0.28/0.47 % 0.28/0.47 %----GOAL: T5. First movers never outcompete efficient producers. % 0.28/0.47 fof(prove_t5,conjecture, % 0.28/0.47 ! [E,T] : % 0.28/0.47 ( ( environment(E) % 0.28/0.47 & subpopulations(first_movers,efficient_producers,E,T) ) % 0.28/0.47 => ~ outcompetes(first_movers,efficient_producers,T) ) ). % 0.28/0.47 % 0.28/0.47 %-------------------------------------------------------------------------- % 0.28/0.47 %------------------------------------------- % 0.28/0.47 % Proof found % 0.28/0.47 % SZS status Theorem for theBenchmark % 0.28/0.47 % SZS output start Proof % 0.28/0.47 %ClaNum:14(EqnAxiom:0) % 0.28/0.47 %VarNum:77(SingletonVarNum:35) % 0.28/0.47 %MaxLitNum:5 % 0.28/0.47 %MaxfuncDepth:1 % 0.28/0.47 %SharedTerms:11 % 0.28/0.47 %goalClause: 1 3 4 % 0.28/0.47 %singleGoalClaCount:3 % 0.28/0.47 [1]P1(a1) % 0.28/0.47 [3]P3(a4,a2,a5) % 0.28/0.47 [4]P6(a4,a2,a1,a5) % 0.28/0.47 [2]P2(f3(a2),f3(a4)) % 0.28/0.47 [6]~P2(a7,f6(x61,x62))+~P4(f6(x61,x62),a7) % 0.28/0.47 [5]P1(x51)+~P2(a7,f6(x52,x53)) % 0.28/0.47 [8]P6(x81,x82,x83,x84)+~P2(a7,f6(x81,x84)) % 0.28/0.47 [9]~P1(x91)+P5(x91,x92)+~P6(a4,a2,x91,x92) % 0.28/0.47 [14]~P1(x143)+~P6(x142,x141,x143,x144)+P6(x141,x142,x143,x144) % 0.28/0.47 [10]~P6(x101,x104,x103,x102)+~P1(x103)+P2(a7,f6(x101,x102))+P4(f6(x101,x102),a7) % 0.28/0.47 [11]~P6(x111,x114,x113,x112)+~P3(x114,x111,x112)+~P1(x113)+P2(a7,f6(x111,x112)) % 0.28/0.47 [12]~P6(x124,x121,x123,x122)+~P3(x121,x124,x122)+~P1(x123)+P4(f6(x121,x122),a7) % 0.28/0.47 [7]~P5(x73,x72)+~P1(x73)+~P2(f3(x74),f3(x71))+P2(a7,f6(x71,x72))+~P2(a7,f6(x74,x72)) % 0.28/0.47 [13]~P6(x132,x131,x134,x133)+P3(x131,x132,x133)+~P1(x134)+~P2(a7,f6(x132,x133))+~P4(f6(x131,x133),a7) % 0.28/0.47 %EqnAxiom % 0.28/0.47 % 0.28/0.47 %------------------------------------------- % 0.28/0.48 cnf(15,plain, % 0.28/0.48 (P5(a1,a5)), % 0.28/0.48 inference(scs_inference,[],[1,4,9])). % 0.28/0.48 cnf(22,plain, % 0.28/0.48 (P1(x221)+P4(f6(a4,a5),a7)), % 0.28/0.48 inference(scs_inference,[],[1,4,5,10])). % 0.28/0.48 cnf(23,plain, % 0.28/0.48 (P6(a2,a4,a1,a5)+P4(f6(a4,a5),a7)), % 0.28/0.48 inference(scs_inference,[],[4,22,14])). % 0.28/0.48 cnf(24,plain, % 0.28/0.48 (P4(f6(a4,a5),a7)), % 0.28/0.48 inference(scs_inference,[],[3,1,23,12])). % 0.28/0.48 cnf(25,plain, % 0.28/0.48 (P2(a7,f6(a4,a5))+~P2(a7,f6(a2,a5))+~P2(a7,f6(x251,x252))), % 0.28/0.48 inference(scs_inference,[],[2,15,5,7])). % 0.28/0.48 cnf(26,plain, % 0.28/0.48 (P2(a7,f6(a4,a5))+~P2(a7,f6(a2,a5))), % 0.28/0.48 inference(factoring_inference,[],[25])). % 0.28/0.48 cnf(27,plain, % 0.28/0.48 (~P2(a7,f6(a2,a5))), % 0.28/0.48 inference(scs_inference,[],[24,26,6])). % 0.28/0.48 cnf(30,plain, % 0.28/0.48 ($false), % 0.28/0.48 inference(scs_inference,[],[3,4,1,27,11,14]), % 0.28/0.48 ['proof']). % 0.28/0.48 % SZS output end Proof % 0.28/0.48 % Total time :0.014165s %------------------------------------------------------------------------------