%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT032+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n018.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:17 AM UTC 2026 % Result : Theorem 115.95s 116.10s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT032+2 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.06/0.34 % Computer : n018.cluster.edu % 0.06/0.34 % Model : x86_64 x86_64 % 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.34 % Memory : 8046.5625MB % 0.06/0.34 % OS : Linux 6.8.0-71-generic % 0.06/0.34 % CPULimit : 300 % 0.06/0.34 % WCLimit : 300 % 0.06/0.34 % DateTime : Mon Sep 7 12:24:07 UTC 2026 % 0.06/0.34 % CPUTime : % 0.27/0.51 start to proof:theBenchmark % 115.95/116.10 %------------------------------------------- % 115.95/116.10 % File :CSE---1.7 % 115.95/116.10 % Problem :theBenchmark % 115.95/116.10 % Transform :cnf % 115.95/116.10 % Format :tptp:raw % 115.95/116.10 % Command :java -jar mcs_scs.jar %d %s % 115.95/116.10 % 115.95/116.10 % Result :Theorem 115.599354s % 115.95/116.10 % Output :CNFRefutation 115.599354s % 115.95/116.10 %------------------------------------------- % 115.95/116.10 %-------------------------------------------------------------------------- % 115.95/116.10 % File : MGT032+2 : TPTP v9.3.0. Released v2.0.0. % 115.95/116.10 % Domain : Management (Organisation Theory) % 115.95/116.10 % Problem : Selection favours EPs above FMs % 115.95/116.10 % Version : [PM93] axioms. % 115.95/116.10 % English : In stable environments, selection favors efficient producers % 115.95/116.10 % above first movers past a certain point in time. % 115.95/116.10 % 115.95/116.10 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 115.95/116.10 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 115.95/116.10 % : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing % 115.95/116.10 % : [Kam95] Kamps (1995), Email to G. Sutcliffe % 115.95/116.10 % Source : [PM93] % 115.95/116.10 % Names : THEOREM 1 [PM93] % 115.95/116.10 % : T1 [PB+94] % 115.95/116.10 % 115.95/116.10 % Status : Theorem % 115.95/116.10 % Rating : 0.00 v6.3.0, 0.08 v6.2.0, 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.04 v5.3.0, 0.13 v5.2.0, 0.00 v2.1.0 % 115.95/116.10 % Syntax : Number of formulae : 3 ( 0 unt; 0 def) % 115.95/116.10 % Number of atoms : 16 ( 0 equ) % 115.95/116.10 % Maximal formula atoms : 6 ( 5 avg) % 115.95/116.10 % Number of connectives : 13 ( 0 ~; 0 |; 8 &) % 115.95/116.10 % ( 0 <=>; 5 =>; 0 <=; 0 <~>) % 115.95/116.10 % Maximal formula depth : 8 ( 8 avg) % 115.95/116.10 % Maximal term depth : 2 ( 1 avg) % 115.95/116.10 % Number of predicates : 7 ( 7 usr; 0 prp; 1-4 aty) % 115.95/116.10 % Number of functors : 3 ( 3 usr; 2 con; 0-2 aty) % 115.95/116.10 % Number of variables : 10 ( 8 !; 2 ?) % 115.95/116.10 % SPC : FOF_THM_RFO_NEQ % 115.95/116.10 % 115.95/116.10 % Comments : % 115.95/116.10 %-------------------------------------------------------------------------- % 115.95/116.10 %----MP1. Selection favors subpopulations with higher growth rates. % 115.95/116.10 fof(mp1_high_growth_rates,axiom, % 115.95/116.10 ! [E,S1,S2,T] : % 115.95/116.10 ( ( environment(E) % 115.95/116.10 & subpopulations(S1,S2,E,T) % 115.95/116.10 & greater(growth_rate(S2,T),growth_rate(S1,T)) ) % 115.95/116.10 => selection_favors(S2,S1,T) ) ). % 115.95/116.10 % 115.95/116.10 %----L1. The growth rate of efficient producers exceeds the growth rate of % 115.95/116.10 %----first movers past a certain time in stable environments. % 115.95/116.10 fof(l1,hypothesis, % 115.95/116.10 ! [E] : % 115.95/116.10 ( ( environment(E) % 115.95/116.10 & stable(E) ) % 115.95/116.10 => ? [To] : % 115.95/116.10 ( in_environment(E,To) % 115.95/116.10 & ! [T] : % 115.95/116.10 ( ( subpopulations(first_movers,efficient_producers,E,T) % 115.95/116.10 & greater_or_equal(T,To) ) % 115.95/116.10 => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ) ). % 115.95/116.10 % 115.95/116.10 %----GOAL: T1. Selection favors efficient producers above first movers % 115.95/116.10 %----past a certain time in stable environments. % 115.95/116.10 fof(prove_t1,conjecture, % 115.95/116.10 ! [E] : % 115.95/116.10 ( ( environment(E) % 115.95/116.10 & stable(E) ) % 115.95/116.10 => ? [To] : % 115.95/116.10 ( in_environment(E,To) % 115.95/116.10 & ! [T] : % 115.95/116.10 ( ( subpopulations(first_movers,efficient_producers,E,T) % 115.95/116.10 & greater_or_equal(T,To) ) % 115.95/116.10 => selection_favors(efficient_producers,first_movers,T) ) ) ) ). % 115.95/116.10 % 115.95/116.10 %-------------------------------------------------------------------------- % 115.95/116.10 %------------------------------------------- % 115.95/116.10 % Proof found % 115.95/116.10 % SZS status Theorem for theBenchmark % 115.95/116.10 % SZS output start Proof % 115.95/116.10 %ClaNum:8(EqnAxiom:0) % 115.95/116.10 %VarNum:31(SingletonVarNum:10) % 115.95/116.10 %MaxLitNum:5 % 115.95/116.10 %MaxfuncDepth:1 % 115.95/116.10 %SharedTerms:5 % 115.95/116.10 %goalClause: 1 2 4 5 6 % 115.95/116.10 %singleGoalClaCount:2 % 115.95/116.10 [1]P1(a1) % 115.95/116.10 [2]P2(a1) % 115.95/116.10 [4]~P3(a1,x41)+P4(f4(x41),x41) % 115.95/116.10 [5]~P3(a1,x51)+~P6(a3,a5,f4(x51)) % 115.95/116.10 [6]~P3(a1,x61)+P7(a5,a3,a1,f4(x61)) % 115.95/116.10 [3]~P1(x31)+~P2(x31)+P3(x31,f2(x31)) % 115.95/116.10 [8]~P7(x82,x81,x84,x83)+P6(x81,x82,x83)+~P1(x84)+~P5(f6(x81,x83),f6(x82,x83)) % 115.95/116.10 [7]~P2(x72)+~P1(x72)+~P4(x71,f2(x72))+~P7(a5,a3,x72,x71)+P5(f6(a3,x71),f6(a5,x71)) % 115.95/116.10 %EqnAxiom % 115.95/116.10 % 115.95/116.10 %------------------------------------------- % 115.95/116.11 cnf(9,plain, % 115.95/116.11 (~P7(a5,a3,a1,f4(f2(a1)))+~P3(a1,f2(a1))+P5(f6(a3,f4(f2(a1))),f6(a5,f4(f2(a1))))), % 115.95/116.11 inference(scs_inference,[],[1,2,4,7])). % 115.95/116.11 cnf(11,plain, % 115.95/116.11 (P7(a5,a3,a1,f4(f2(a1)))), % 115.95/116.11 inference(scs_inference,[],[2,1,6,3])). % 115.95/116.11 cnf(12,plain, % 115.95/116.11 (P5(f6(a3,f4(f2(a1))),f6(a5,f4(f2(a1))))+~P3(a1,f2(a1))), % 115.95/116.11 inference(scs_inference,[],[11,9])). % 115.95/116.11 cnf(14,plain, % 115.95/116.11 (~P5(f6(a3,f4(f2(a1))),f6(a5,f4(f2(a1))))+~P3(a1,f2(a1))), % 115.95/116.11 inference(scs_inference,[],[1,11,5,8])). % 115.95/116.11 cnf(18,plain, % 115.95/116.11 (P3(a1,f2(a1))), % 115.95/116.11 inference(scs_inference,[],[1,2,3])). % 115.95/116.11 cnf(20,plain, % 115.95/116.11 (P5(f6(a3,f4(f2(a1))),f6(a5,f4(f2(a1))))), % 115.95/116.11 inference(scs_inference,[],[18,12])). % 115.95/116.11 cnf(21,plain, % 115.95/116.11 (~P5(f6(a3,f4(f2(a1))),f6(a5,f4(f2(a1))))), % 115.95/116.11 inference(scs_inference,[],[18,14])). % 115.95/116.11 cnf(2020,plain, % 115.95/116.11 ($false), % 115.95/116.11 inference(scs_inference,[],[20,21]), % 115.95/116.11 ['proof']). % 115.95/116.11 % SZS output end Proof % 115.95/116.11 % Total time :115.599354s %------------------------------------------------------------------------------