%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT032-2 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 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:04:18 AM UTC 2026 % Result : Unsatisfiable 115.93s 116.11s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT032-2 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.09/0.35 % Computer : n028.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 12:25:17 UTC 2026 % 0.13/0.36 % CPUTime : % 0.24/0.52 start to proof:theBenchmark % 115.93/116.10 %------------------------------------------- % 115.93/116.10 % File :CSE---1.7 % 115.93/116.10 % Problem :theBenchmark % 115.93/116.10 % Transform :cnf % 115.93/116.10 % Format :tptp:raw % 115.93/116.10 % Command :java -jar mcs_scs.jar %d %s % 115.93/116.10 % 115.93/116.10 % Result :Theorem 115.598892s % 115.93/116.10 % Output :CNFRefutation 115.598892s % 115.93/116.10 %------------------------------------------- % 115.93/116.10 %-------------------------------------------------------------------------- % 115.93/116.10 % File : MGT032-2 : TPTP v9.3.0. Released v2.4.0. % 115.93/116.10 % Domain : Management (Organisation Theory) % 115.93/116.10 % Problem : Selection favours EPs above FMs % 115.93/116.10 % Version : [PM93] axioms. % 115.93/116.10 % English : In stable environments, selection favors efficient producers % 115.93/116.10 % above first movers past a certain point in time. % 115.93/116.10 % 115.93/116.10 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 115.93/116.10 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 115.93/116.10 % : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing % 115.93/116.10 % : [Kam95] Kamps (1995), Email to G. Sutcliffe % 115.93/116.10 % Source : [TPTP] % 115.93/116.10 % Names : % 115.93/116.10 % 115.93/116.10 % Status : Unsatisfiable % 115.93/116.10 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.00 v2.4.0 % 115.93/116.10 % Syntax : Number of clauses : 8 ( 2 unt; 0 nHn; 8 RR) % 115.93/116.10 % Number of literals : 20 ( 0 equ; 13 neg) % 115.93/116.10 % Maximal clause size : 5 ( 2 avg) % 115.93/116.10 % Maximal term depth : 2 ( 1 avg) % 115.93/116.10 % Number of predicates : 7 ( 7 usr; 0 prp; 1-4 aty) % 115.93/116.10 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty) % 115.93/116.10 % Number of variables : 10 ( 0 sgn) % 115.93/116.10 % SPC : CNF_UNS_RFO_NEQ_HRN % 115.93/116.10 % 115.93/116.10 % Comments : Created with tptp2X -f tptp -t clausify:otter MGT032+2.p % 115.93/116.10 %-------------------------------------------------------------------------- % 115.93/116.10 cnf(mp1_high_growth_rates_1,axiom, % 115.93/116.10 ( ~ environment(A) % 115.93/116.10 | ~ subpopulations(B,C,A,D) % 115.93/116.10 | ~ greater(growth_rate(C,D),growth_rate(B,D)) % 115.93/116.10 | selection_favors(C,B,D) ) ). % 115.93/116.10 % 115.93/116.10 cnf(l1_2,hypothesis, % 115.93/116.10 ( ~ environment(A) % 115.93/116.10 | ~ stable(A) % 115.93/116.10 | in_environment(A,sk1(A)) ) ). % 115.93/116.10 % 115.93/116.10 cnf(l1_3,hypothesis, % 115.93/116.10 ( ~ environment(A) % 115.93/116.10 | ~ stable(A) % 115.93/116.10 | ~ subpopulations(first_movers,efficient_producers,A,B) % 115.93/116.11 | ~ greater_or_equal(B,sk1(A)) % 115.93/116.11 | greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B)) ) ). % 115.93/116.11 % 115.93/116.11 cnf(prove_t1_4,negated_conjecture, % 115.93/116.11 environment(sk2) ). % 115.93/116.11 % 115.93/116.11 cnf(prove_t1_5,negated_conjecture, % 115.93/116.11 stable(sk2) ). % 115.93/116.11 % 115.93/116.11 cnf(prove_t1_6,negated_conjecture, % 115.93/116.11 ( ~ in_environment(sk2,A) % 115.93/116.11 | subpopulations(first_movers,efficient_producers,sk2,sk3(A)) ) ). % 115.93/116.11 % 115.93/116.11 cnf(prove_t1_7,negated_conjecture, % 115.93/116.11 ( ~ in_environment(sk2,A) % 115.93/116.11 | greater_or_equal(sk3(A),A) ) ). % 115.93/116.11 % 115.93/116.11 cnf(prove_t1_8,negated_conjecture, % 115.93/116.11 ( ~ in_environment(sk2,A) % 115.93/116.11 | ~ selection_favors(efficient_producers,first_movers,sk3(A)) ) ). % 115.93/116.11 % 115.93/116.11 %-------------------------------------------------------------------------- % 115.93/116.11 %------------------------------------------- % 115.93/116.11 % Proof found % 115.93/116.11 % SZS status Theorem for theBenchmark % 115.93/116.11 % SZS output start Proof % 115.93/116.11 %ClaNum:8(EqnAxiom:0) % 115.93/116.11 %VarNum:31(SingletonVarNum:10) % 115.93/116.11 %MaxLitNum:5 % 115.93/116.11 %MaxfuncDepth:1 % 115.93/116.11 %SharedTerms:5 % 115.93/116.11 %goalClause: 1 2 4 5 6 % 115.93/116.11 %singleGoalClaCount:2 % 115.93/116.11 [1]P1(a1) % 115.93/116.11 [2]P2(a1) % 115.93/116.11 [4]~P3(a1,x41)+P4(f6(x41),x41) % 115.93/116.11 [5]~P3(a1,x51)+~P6(a3,a4,f6(x51)) % 115.93/116.11 [6]~P3(a1,x61)+P7(a4,a3,a1,f6(x61)) % 115.93/116.11 [3]~P1(x31)+~P2(x31)+P3(x31,f2(x31)) % 115.93/116.11 [8]~P7(x82,x81,x84,x83)+P6(x81,x82,x83)+~P1(x84)+~P5(f5(x81,x83),f5(x82,x83)) % 115.93/116.11 [7]~P2(x72)+~P1(x72)+~P4(x71,f2(x72))+~P7(a4,a3,x72,x71)+P5(f5(a3,x71),f5(a4,x71)) % 115.93/116.11 %EqnAxiom % 115.93/116.11 % 115.93/116.11 %------------------------------------------- % 115.93/116.11 cnf(9,plain, % 115.93/116.11 (~P7(a4,a3,a1,f6(f2(a1)))+~P3(a1,f2(a1))+P5(f5(a3,f6(f2(a1))),f5(a4,f6(f2(a1))))), % 115.93/116.11 inference(scs_inference,[],[1,2,4,7])). % 115.93/116.11 cnf(11,plain, % 115.93/116.11 (P7(a4,a3,a1,f6(f2(a1)))), % 115.93/116.11 inference(scs_inference,[],[2,1,6,3])). % 115.93/116.11 cnf(12,plain, % 115.93/116.11 (P5(f5(a3,f6(f2(a1))),f5(a4,f6(f2(a1))))+~P3(a1,f2(a1))), % 115.93/116.11 inference(scs_inference,[],[11,9])). % 115.93/116.11 cnf(14,plain, % 115.93/116.11 (~P5(f5(a3,f6(f2(a1))),f5(a4,f6(f2(a1))))+~P3(a1,f2(a1))), % 115.93/116.11 inference(scs_inference,[],[1,11,5,8])). % 115.93/116.11 cnf(18,plain, % 115.93/116.11 (P3(a1,f2(a1))), % 115.93/116.11 inference(scs_inference,[],[1,2,3])). % 115.93/116.11 cnf(20,plain, % 115.93/116.11 (P5(f5(a3,f6(f2(a1))),f5(a4,f6(f2(a1))))), % 115.93/116.11 inference(scs_inference,[],[18,12])). % 115.93/116.11 cnf(21,plain, % 115.93/116.11 (~P5(f5(a3,f6(f2(a1))),f5(a4,f6(f2(a1))))), % 115.93/116.11 inference(scs_inference,[],[18,14])). % 115.93/116.11 cnf(2262,plain, % 115.93/116.11 ($false), % 115.93/116.11 inference(scs_inference,[],[20,21]), % 115.93/116.11 ['proof']). % 115.93/116.11 % SZS output end Proof % 115.93/116.11 % Total time :115.598892s %------------------------------------------------------------------------------