%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT028-1 : 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 : n015.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 : Unsatisfiable 116.62s 116.78s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT028-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.35 % Computer : n015.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Mon Sep 7 12:18:15 UTC 2026 % 0.08/0.35 % CPUTime : % 0.24/0.51 start to proof:theBenchmark % 116.62/116.77 %------------------------------------------- % 116.62/116.77 % File :CSE---1.7 % 116.62/116.77 % Problem :theBenchmark % 116.62/116.77 % Transform :cnf % 116.62/116.77 % Format :tptp:raw % 116.62/116.77 % Command :java -jar mcs_scs.jar %d %s % 116.62/116.77 % 116.62/116.77 % Result :Theorem 116.259656s % 116.62/116.77 % Output :CNFRefutation 116.259656s % 116.62/116.77 %------------------------------------------- % 116.62/116.77 %-------------------------------------------------------------------------- % 116.62/116.77 % File : MGT028-1 : TPTP v9.3.0. Released v2.4.0. % 116.62/116.77 % Domain : Management (Organisation Theory) % 116.62/116.77 % Problem : FMs have a negative growth rate in stable environments % 116.62/116.77 % Version : [PB+94] axioms : Reduced & Augmented > Complete. % 116.62/116.77 % English : First movers have negative growth rate past a certain point % 116.62/116.77 % of time (also after the appearence of efficient producers) % 116.62/116.77 % in stable environments. % 116.62/116.77 % 116.62/116.77 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 116.62/116.77 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 116.62/116.77 % : [Kam95] Kamps (1995), Email to G. Sutcliffe % 116.62/116.77 % Source : [TPTP] % 116.62/116.77 % Names : % 116.62/116.77 % 116.62/116.78 % Status : Unsatisfiable % 116.62/116.78 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.00 v2.4.0 % 116.62/116.78 % Syntax : Number of clauses : 14 ( 2 unt; 4 nHn; 14 RR) % 116.62/116.78 % Number of literals : 57 ( 0 equ; 40 neg) % 116.62/116.78 % Maximal clause size : 7 ( 4 avg) % 116.62/116.78 % Maximal term depth : 3 ( 1 avg) % 116.62/116.78 % Number of predicates : 6 ( 6 usr; 0 prp; 1-4 aty) % 116.62/116.78 % Number of functors : 10 ( 10 usr; 4 con; 0-2 aty) % 116.62/116.78 % Number of variables : 23 ( 0 sgn) % 116.62/116.78 % SPC : CNF_UNS_RFO_NEQ_NHN % 116.62/116.78 % 116.62/116.78 % Comments : Created with tptp2X -f tptp -t clausify:otter MGT028+1.p % 116.62/116.78 %-------------------------------------------------------------------------- % 116.62/116.78 cnf(mp_first_movers_negative_growth_1,axiom, % 116.62/116.78 ( ~ environment(A) % 116.62/116.78 | ~ stable(A) % 116.62/116.78 | ~ in_environment(A,B) % 116.62/116.78 | subpopulations(first_movers,efficient_producers,A,sk1(B,A)) % 116.62/116.78 | greater(sk2(A),appear(efficient_producers,A)) ) ). % 116.62/116.78 % 116.62/116.78 cnf(mp_first_movers_negative_growth_2,axiom, % 116.62/116.78 ( ~ environment(A) % 116.62/116.78 | ~ stable(A) % 116.62/116.78 | ~ in_environment(A,B) % 116.62/116.78 | greater_or_equal(sk1(B,A),B) % 116.62/116.78 | greater(sk2(A),appear(efficient_producers,A)) ) ). % 116.62/116.78 % 116.62/116.78 cnf(mp_first_movers_negative_growth_3,axiom, % 116.62/116.78 ( ~ environment(A) % 116.62/116.78 | ~ stable(A) % 116.62/116.78 | ~ in_environment(A,B) % 116.62/116.78 | subpopulations(first_movers,efficient_producers,A,sk1(B,A)) % 116.62/116.78 | ~ subpopulations(first_movers,efficient_producers,A,C) % 116.62/116.78 | ~ greater_or_equal(C,sk2(A)) % 116.62/116.78 | greater(zero,growth_rate(first_movers,C)) ) ). % 116.62/116.78 % 116.62/116.78 cnf(mp_first_movers_negative_growth_4,axiom, % 116.62/116.78 ( ~ environment(A) % 116.62/116.78 | ~ stable(A) % 116.62/116.78 | ~ in_environment(A,B) % 116.62/116.78 | greater_or_equal(sk1(B,A),B) % 116.62/116.78 | ~ subpopulations(first_movers,efficient_producers,A,C) % 116.62/116.78 | ~ greater_or_equal(C,sk2(A)) % 116.62/116.78 | greater(zero,growth_rate(first_movers,C)) ) ). % 116.62/116.78 % 116.62/116.78 cnf(mp_first_movers_negative_growth_5,axiom, % 116.62/116.78 ( ~ environment(A) % 116.62/116.78 | ~ stable(A) % 116.62/116.78 | ~ in_environment(A,B) % 116.62/116.78 | ~ greater(zero,growth_rate(first_movers,sk1(B,A))) % 116.62/116.78 | greater(sk2(A),appear(efficient_producers,A)) ) ). % 116.62/116.78 % 116.62/116.78 cnf(mp_first_movers_negative_growth_6,axiom, % 116.62/116.78 ( ~ environment(A) % 116.62/116.78 | ~ stable(A) % 116.62/116.78 | ~ in_environment(A,B) % 116.62/116.78 | ~ greater(zero,growth_rate(first_movers,sk1(B,A))) % 116.62/116.78 | ~ subpopulations(first_movers,efficient_producers,A,C) % 116.62/116.78 | ~ greater_or_equal(C,sk2(A)) % 116.62/116.78 | greater(zero,growth_rate(first_movers,C)) ) ). % 116.62/116.78 % 116.62/116.78 cnf(l11_7,hypothesis, % 116.62/116.78 ( ~ environment(A) % 116.62/116.78 | ~ stable(A) % 116.62/116.78 | in_environment(A,sk3(A)) ) ). % 116.62/116.78 % 116.62/116.78 cnf(l11_8,hypothesis, % 116.62/116.78 ( ~ environment(A) % 116.62/116.78 | ~ stable(A) % 116.62/116.78 | ~ subpopulations(first_movers,efficient_producers,A,B) % 116.62/116.78 | ~ greater_or_equal(B,sk3(A)) % 116.62/116.78 | greater(growth_rate(efficient_producers,B),zero) ) ). % 116.62/116.78 % 116.62/116.78 cnf(l11_9,hypothesis, % 116.62/116.78 ( ~ environment(A) % 116.62/116.78 | ~ stable(A) % 116.62/116.78 | ~ subpopulations(first_movers,efficient_producers,A,B) % 116.62/116.78 | ~ greater_or_equal(B,sk3(A)) % 116.62/116.78 | greater(zero,growth_rate(first_movers,B)) ) ). % 116.62/116.78 % 116.62/116.78 cnf(prove_l10_10,negated_conjecture, % 116.62/116.78 environment(sk4) ). % 116.62/116.78 % 116.62/116.78 cnf(prove_l10_11,negated_conjecture, % 116.62/116.78 stable(sk4) ). % 116.62/116.78 % 116.62/116.78 cnf(prove_l10_12,negated_conjecture, % 116.62/116.78 ( ~ greater(A,appear(efficient_producers,sk4)) % 116.62/116.78 | subpopulations(first_movers,efficient_producers,sk4,sk5(A)) ) ). % 116.62/116.78 % 116.62/116.78 cnf(prove_l10_13,negated_conjecture, % 116.62/116.78 ( ~ greater(A,appear(efficient_producers,sk4)) % 116.62/116.78 | greater_or_equal(sk5(A),A) ) ). % 116.62/116.78 % 116.62/116.78 cnf(prove_l10_14,negated_conjecture, % 116.62/116.78 ( ~ greater(A,appear(efficient_producers,sk4)) % 116.62/116.78 | ~ greater(zero,growth_rate(first_movers,sk5(A))) ) ). % 116.62/116.78 % 116.62/116.78 %-------------------------------------------------------------------------- % 116.62/116.78 %------------------------------------------- % 116.62/116.78 % Proof found % 116.62/116.78 % SZS status Theorem for theBenchmark % 116.62/116.78 % SZS output start Proof % 116.62/116.78 %ClaNum:14(EqnAxiom:0) % 116.62/116.78 %VarNum:86(SingletonVarNum:23) % 116.62/116.78 %MaxLitNum:7 % 116.62/116.78 %MaxfuncDepth:2 % 116.62/116.78 %SharedTerms:7 % 116.62/116.78 %goalClause: 1 2 4 6 8 % 116.62/116.78 %singleGoalClaCount:2 % 116.62/116.78 [1]P1(a1) % 116.62/116.78 [2]P2(a1) % 116.62/116.78 [4]P4(f9(x41),x41)+~P5(x41,f4(a3,a1)) % 116.62/116.78 [8]~P5(x81,f4(a3,a1))+P6(a6,a3,a1,f9(x81)) % 116.62/116.78 [6]~P5(x61,f4(a3,a1))+~P5(a10,f7(a6,f9(x61))) % 116.62/116.78 [3]~P1(x31)+~P2(x31)+P3(x31,f2(x31)) % 116.62/116.78 [5]~P1(x52)+~P2(x52)+~P3(x52,x51)+P4(f5(x51,x52),x51)+P5(f8(x52),f4(a3,x52)) % 116.62/116.78 [9]~P1(x91)+~P2(x91)+~P3(x91,x92)+P5(f8(x91),f4(a3,x91))+P6(a6,a3,x91,f5(x92,x91)) % 116.62/116.78 [10]~P2(x102)+~P1(x102)+~P4(x101,f2(x102))+~P6(a6,a3,x102,x101)+P5(a10,f7(a6,x101)) % 116.62/116.78 [11]~P2(x112)+~P1(x112)+~P4(x111,f2(x112))+~P6(a6,a3,x112,x111)+P5(f7(a3,x111),a10) % 116.62/116.78 [7]~P1(x71)+~P2(x71)+~P3(x71,x72)+P5(f8(x71),f4(a3,x71))+~P5(a10,f7(a6,f5(x72,x71))) % 116.62/116.78 [12]~P1(x122)+~P2(x122)+~P3(x122,x121)+~P4(x123,f8(x122))+~P6(a6,a3,x122,x123)+P4(f5(x121,x122),x121)+P5(a10,f7(a6,x123)) % 116.62/116.78 [14]~P1(x142)+~P2(x142)+~P3(x142,x143)+~P4(x141,f8(x142))+~P6(a6,a3,x142,x141)+P6(a6,a3,x142,f5(x143,x142))+P5(a10,f7(a6,x141)) % 116.62/116.78 [13]~P2(x132)+~P3(x132,x133)+~P1(x132)+~P4(x131,f8(x132))+~P6(a6,a3,x132,x131)+P5(a10,f7(a6,x131))+~P5(a10,f7(a6,f5(x133,x132))) % 116.62/116.78 %EqnAxiom % 116.62/116.78 % 116.62/116.78 %------------------------------------------- % 116.75/116.87 cnf(17,plain, % 116.75/116.87 (~P3(a1,x171)+P6(a6,a3,a1,f9(f8(a1)))+~P5(a10,f7(a6,f5(x171,a1)))), % 116.75/116.87 inference(scs_inference,[],[2,1,8,7])). % 116.75/116.87 cnf(18,plain, % 116.75/116.87 (~P5(a10,f7(a6,f5(f2(a1),a1)))+P6(a6,a3,a1,f9(f8(a1)))), % 116.75/116.87 inference(scs_inference,[],[2,1,3,17])). % 116.75/116.87 cnf(19,plain, % 116.75/116.87 (~P3(a1,x191)+P4(f9(f8(a1)),f8(a1))+P6(a6,a3,a1,f5(x191,a1))), % 116.75/116.87 inference(scs_inference,[],[2,1,4,9])). % 116.75/116.87 cnf(20,plain, % 116.75/116.87 (P4(f9(f8(a1)),f8(a1))+P6(a6,a3,a1,f5(f2(a1),a1))), % 116.75/116.87 inference(scs_inference,[],[2,1,19,3])). % 116.75/116.87 cnf(55661,plain, % 116.75/116.87 (P3(a1,f2(a1))), % 116.75/116.87 inference(scs_inference,[],[1,2,3])). % 116.75/116.87 cnf(55665,plain, % 116.75/116.87 (~P6(a6,a3,a1,f5(f2(a1),a1))+P5(f8(a1),f4(a3,a1))+P5(a10,f7(a6,f5(f2(a1),a1)))), % 116.75/116.87 inference(scs_inference,[],[1,2,3,5,10])). % 116.75/116.87 cnf(55667,plain, % 116.75/116.87 (P5(f8(a1),f4(a3,a1))+P6(a6,a3,a1,f5(f2(a1),a1))), % 116.75/116.87 inference(scs_inference,[],[1,55661,2,9])). % 116.75/116.87 cnf(55671,plain, % 116.75/116.87 (P5(f8(a1),f4(a3,a1))+~P4(f5(f2(a1),a1),f2(a1))+P5(a10,f7(a6,f5(f2(a1),a1)))), % 116.75/116.87 inference(scs_inference,[],[2,1,55667,10])). % 116.75/116.87 cnf(91863,plain, % 116.75/116.87 (P5(f8(a1),f4(a3,a1))+~P5(a10,f7(a6,f5(f2(a1),a1)))), % 116.75/116.87 inference(scs_inference,[],[2,1,55661,7])). % 116.75/116.87 cnf(91865,plain, % 116.75/116.87 (P5(f8(a1),f4(a3,a1))+~P6(a6,a3,a1,f5(f2(a1),a1))), % 116.75/116.87 inference(scs_inference,[],[2,1,55661,7,55665])). % 116.75/116.87 cnf(91868,plain, % 116.75/116.87 (~P5(a10,f7(a6,f5(f2(a1),a1)))+~P5(a10,f7(a6,f9(f8(a1))))), % 116.75/116.87 inference(scs_inference,[],[91863,6])). % 116.75/116.87 cnf(91891,plain, % 116.75/116.87 (~P5(a10,f7(a6,f9(f8(a1))))+~P6(a6,a3,a1,f5(f2(a1),a1))+~P4(f5(f2(a1),a1),f2(a1))), % 116.75/116.87 inference(scs_inference,[],[1,2,91868,10])). % 116.75/116.87 cnf(91955,plain, % 116.75/116.87 (~P4(f5(f2(a1),a1),f2(a1))+~P5(a10,f7(a6,f9(f8(a1))))+P5(f8(a1),f4(a3,a1))), % 116.75/116.87 inference(scs_inference,[],[2,55661,1,91891,9])). % 116.75/116.87 cnf(91971,plain, % 116.75/116.87 (~P4(f5(f2(a1),a1),f2(a1))+~P5(a10,f7(a6,f9(f8(a1))))), % 116.75/116.87 inference(scs_inference,[],[91955,6])). % 116.75/116.87 cnf(91987,plain, % 116.75/116.87 (~P5(a10,f7(a6,f9(f8(a1))))+P5(f8(a1),f4(a3,a1))), % 116.75/116.87 inference(scs_inference,[],[2,1,55661,91971,5])). % 116.75/116.87 cnf(92003,plain, % 116.75/116.87 (~P5(a10,f7(a6,f9(f8(a1))))), % 116.75/116.87 inference(scs_inference,[],[91987,6])). % 116.75/116.87 cnf(92004,plain, % 116.75/116.87 (~P6(a6,a3,a1,f9(f8(a1)))+~P4(f9(f8(a1)),f8(a1))+~P5(a10,f7(a6,f5(f2(a1),a1)))), % 116.75/116.87 inference(scs_inference,[],[2,1,55661,92003,13])). % 116.75/116.87 cnf(92019,plain, % 116.75/116.87 (~P5(a10,f7(a6,f5(f2(a1),a1)))+~P4(f9(f8(a1)),f8(a1))), % 116.75/116.87 inference(scs_inference,[],[92004,18])). % 116.75/116.87 cnf(92035,plain, % 116.75/116.87 (~P4(f9(f8(a1)),f8(a1))+~P6(a6,a3,a1,f5(f2(a1),a1))+~P4(f5(f2(a1),a1),f2(a1))), % 116.75/116.87 inference(scs_inference,[],[1,2,92019,10])). % 116.75/116.87 cnf(92082,plain, % 116.75/116.87 (~P6(a6,a3,a1,f5(f2(a1),a1))+P4(f9(f8(a1)),f8(a1))), % 116.75/116.87 inference(scs_inference,[],[4,91865])). % 116.75/116.87 cnf(92098,plain, % 116.75/116.87 (P4(f9(f8(a1)),f8(a1))), % 116.75/116.87 inference(scs_inference,[],[92082,20])). % 116.75/116.87 cnf(92099,plain, % 116.75/116.87 (~P5(a10,f7(a6,f5(f2(a1),a1)))), % 116.75/116.87 inference(scs_inference,[],[92098,92019])). % 116.75/116.87 cnf(92100,plain, % 116.75/116.87 (~P6(a6,a3,a1,f5(f2(a1),a1))+~P4(f5(f2(a1),a1),f2(a1))), % 116.75/116.87 inference(scs_inference,[],[92098,92035])). % 116.75/116.87 cnf(92101,plain, % 116.75/116.87 (~P6(a6,a3,a1,f9(f8(a1)))+P6(a6,a3,a1,f5(f2(a1),a1))), % 116.75/116.87 inference(scs_inference,[],[2,1,55661,92003,92098,14])). % 116.75/116.87 cnf(92104,plain, % 116.75/116.87 (P5(f8(a1),f4(a3,a1))+~P4(f5(f2(a1),a1),f2(a1))), % 116.75/116.87 inference(scs_inference,[],[92099,55671])). % 116.75/116.87 cnf(92108,plain, % 116.75/116.87 (~P6(a6,a3,a1,f5(f2(a1),a1))+~P6(a6,a3,a1,f9(f8(a1)))), % 116.75/116.87 inference(scs_inference,[],[2,1,55661,92003,92098,12,92104,92100])). % 116.75/116.87 cnf(92146,plain, % 116.75/116.87 (~P6(a6,a3,a1,f9(f8(a1)))), % 116.75/116.87 inference(scs_inference,[],[92108,92101])). % 116.75/116.87 cnf(92155,plain, % 116.75/116.87 ($false), % 116.75/116.87 inference(scs_inference,[],[1,2,55661,92146,8,5,92104]), % 116.75/116.87 ['proof']). % 116.85/116.90 % SZS output end Proof % 116.85/116.90 % Total time :116.259656s %------------------------------------------------------------------------------