%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT028+1 : 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 : n014.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 116.75s 116.81s % 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.0.0. % 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.35 % Computer : n014.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:14:56 UTC 2026 % 0.08/0.35 % CPUTime : % 0.34/0.52 start to proof:theBenchmark % 116.75/116.80 %------------------------------------------- % 116.75/116.80 % File :CSE---1.7 % 116.75/116.80 % Problem :theBenchmark % 116.75/116.80 % Transform :cnf % 116.75/116.80 % Format :tptp:raw % 116.75/116.80 % Command :java -jar mcs_scs.jar %d %s % 116.75/116.80 % 116.75/116.80 % Result :Theorem 116.284070s % 116.75/116.80 % Output :CNFRefutation 116.284070s % 116.75/116.80 %------------------------------------------- % 116.75/116.80 %-------------------------------------------------------------------------- % 116.75/116.80 % File : MGT028+1 : TPTP v9.3.0. Released v2.0.0. % 116.75/116.80 % Domain : Management (Organisation Theory) % 116.75/116.80 % Problem : FMs have a negative growth rate in stable environments % 116.75/116.80 % Version : [PB+94] axioms : Reduced & Augmented > Complete. % 116.75/116.80 % English : First movers have negative growth rate past a certain point % 116.75/116.80 % of time (also after the appearence of efficient producers) % 116.75/116.80 % in stable environments. % 116.75/116.80 % 116.75/116.80 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 116.75/116.80 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 116.75/116.80 % : [Kam95] Kamps (1995), Email to G. Sutcliffe % 116.75/116.81 % Source : [Kam95] % 116.75/116.81 % Names : % 116.75/116.81 % 116.75/116.81 % Status : Theorem % 116.75/116.81 % Rating : 0.00 v9.3.0, 0.05 v9.1.0, 0.07 v9.0.0, 0.00 v6.3.0, 0.08 v6.2.0, 0.00 v5.5.0, 0.08 v5.4.0, 0.04 v5.3.0, 0.13 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 % 116.75/116.81 % Syntax : Number of formulae : 3 ( 0 unt; 0 def) % 116.75/116.81 % Number of atoms : 23 ( 0 equ) % 116.75/116.81 % Maximal formula atoms : 10 ( 7 avg) % 116.75/116.81 % Number of connectives : 20 ( 0 ~; 0 |; 13 &) % 116.75/116.81 % ( 0 <=>; 7 =>; 0 <=; 0 <~>) % 116.75/116.81 % Maximal formula depth : 10 ( 9 avg) % 116.75/116.81 % Maximal term depth : 2 ( 1 avg) % 116.75/116.81 % Number of predicates : 6 ( 6 usr; 0 prp; 1-4 aty) % 116.75/116.81 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty) % 116.75/116.81 % Number of variables : 11 ( 7 !; 4 ?) % 116.75/116.81 % SPC : FOF_THM_RFO_NEQ % 116.75/116.81 % 116.75/116.81 % Comments : % 116.75/116.81 %-------------------------------------------------------------------------- % 116.75/116.81 %----MP. If first movers have negative growth rate past time t1 in a % 116.75/116.81 %----stable environment, then there is also a time, t2, which is after the % 116.75/116.81 %----appearence of EP, and FM has negative growth rate past t2. % 116.75/116.81 fof(mp_first_movers_negative_growth,axiom, % 116.75/116.81 ! [E] : % 116.75/116.81 ( ( environment(E) % 116.75/116.81 & stable(E) % 116.75/116.81 & ? [T1] : % 116.75/116.81 ( in_environment(E,T1) % 116.75/116.81 & ! [T] : % 116.75/116.81 ( ( subpopulations(first_movers,efficient_producers,E,T) % 116.75/116.81 & greater_or_equal(T,T1) ) % 116.75/116.81 => greater(zero,growth_rate(first_movers,T)) ) ) ) % 116.75/116.81 => ? [T2] : % 116.75/116.81 ( greater(T2,appear(efficient_producers,E)) % 116.75/116.81 & ! [T] : % 116.75/116.81 ( ( subpopulations(first_movers,efficient_producers,E,T) % 116.75/116.81 & greater_or_equal(T,T2) ) % 116.75/116.81 => greater(zero,growth_rate(first_movers,T)) ) ) ) ). % 116.75/116.81 % 116.75/116.81 %----L11. Efficient producers have positive, while first movers have % 116.75/116.81 %----negative growth rate past a certain point of time in stable % 116.75/116.81 %----environments. % 116.75/116.81 fof(l11,hypothesis, % 116.75/116.81 ! [E] : % 116.75/116.81 ( ( environment(E) % 116.75/116.81 & stable(E) ) % 116.75/116.81 => ? [To] : % 116.75/116.81 ( in_environment(E,To) % 116.75/116.81 & ! [T] : % 116.75/116.81 ( ( subpopulations(first_movers,efficient_producers,E,T) % 116.75/116.81 & greater_or_equal(T,To) ) % 116.75/116.81 => ( greater(growth_rate(efficient_producers,T),zero) % 116.75/116.81 & greater(zero,growth_rate(first_movers,T)) ) ) ) ) ). % 116.75/116.81 % 116.75/116.81 %----GOAL:L10. First movers have negative growth rate past a certain point % 116.75/116.81 %----of time (also after the appearence of efficient producers) in stable % 116.75/116.81 %----environments. % 116.75/116.81 fof(prove_l10,conjecture, % 116.75/116.81 ! [E] : % 116.75/116.81 ( ( environment(E) % 116.75/116.81 & stable(E) ) % 116.75/116.81 => ? [To] : % 116.75/116.81 ( greater(To,appear(efficient_producers,E)) % 116.75/116.81 & ! [T] : % 116.75/116.81 ( ( subpopulations(first_movers,efficient_producers,E,T) % 116.75/116.81 & greater_or_equal(T,To) ) % 116.75/116.81 => greater(zero,growth_rate(first_movers,T)) ) ) ) ). % 116.75/116.81 % 116.75/116.81 %-------------------------------------------------------------------------- % 116.75/116.81 %------------------------------------------- % 116.75/116.81 % Proof found % 116.75/116.81 % SZS status Theorem for theBenchmark % 116.75/116.81 % SZS output start Proof % 116.75/116.81 %ClaNum:14(EqnAxiom:0) % 116.75/116.81 %VarNum:86(SingletonVarNum:23) % 116.75/116.81 %MaxLitNum:7 % 116.75/116.81 %MaxfuncDepth:2 % 116.75/116.81 %SharedTerms:7 % 116.75/116.81 %goalClause: 1 2 4 6 8 % 116.75/116.81 %singleGoalClaCount:2 % 116.75/116.81 [1]P1(a1) % 116.75/116.81 [2]P2(a1) % 116.75/116.81 [4]P4(f7(x41),x41)+~P5(x41,f4(a3,a1)) % 116.75/116.81 [8]~P5(x81,f4(a3,a1))+P6(a9,a3,a1,f7(x81)) % 116.75/116.81 [6]~P5(x61,f4(a3,a1))+~P5(a8,f10(a9,f7(x61))) % 116.75/116.81 [3]~P1(x31)+~P2(x31)+P3(x31,f2(x31)) % 116.75/116.81 [5]~P1(x51)+~P2(x51)+~P3(x51,x52)+P4(f5(x51,x52),x52)+P5(f6(x51),f4(a3,x51)) % 116.75/116.81 [9]~P1(x91)+~P2(x91)+~P3(x91,x92)+P5(f6(x91),f4(a3,x91))+P6(a9,a3,x91,f5(x91,x92)) % 116.75/116.81 [10]~P2(x102)+~P1(x102)+~P4(x101,f2(x102))+~P6(a9,a3,x102,x101)+P5(a8,f10(a9,x101)) % 116.75/116.81 [11]~P2(x112)+~P1(x112)+~P4(x111,f2(x112))+~P6(a9,a3,x112,x111)+P5(f10(a3,x111),a8) % 116.75/116.81 [7]~P1(x71)+~P2(x71)+~P3(x71,x72)+P5(f6(x71),f4(a3,x71))+~P5(a8,f10(a9,f5(x71,x72))) % 116.75/116.81 [12]~P1(x121)+~P2(x121)+~P3(x121,x122)+~P4(x123,f6(x121))+~P6(a9,a3,x121,x123)+P4(f5(x121,x122),x122)+P5(a8,f10(a9,x123)) % 116.75/116.81 [14]~P1(x142)+~P2(x142)+~P3(x142,x143)+~P4(x141,f6(x142))+~P6(a9,a3,x142,x141)+P6(a9,a3,x142,f5(x142,x143))+P5(a8,f10(a9,x141)) % 116.75/116.81 [13]~P2(x132)+~P3(x132,x133)+~P1(x132)+~P4(x131,f6(x132))+~P6(a9,a3,x132,x131)+P5(a8,f10(a9,x131))+~P5(a8,f10(a9,f5(x132,x133))) % 116.75/116.81 %EqnAxiom % 116.75/116.81 % 116.75/116.81 %------------------------------------------- % 116.75/116.85 cnf(17,plain, % 116.75/116.85 (~P3(a1,x171)+P6(a9,a3,a1,f7(f6(a1)))+~P5(a8,f10(a9,f5(a1,x171)))), % 116.75/116.85 inference(scs_inference,[],[2,1,8,7])). % 116.75/116.85 cnf(18,plain, % 116.75/116.85 (~P5(a8,f10(a9,f5(a1,f2(a1))))+P6(a9,a3,a1,f7(f6(a1)))), % 116.75/116.85 inference(scs_inference,[],[2,1,3,17])). % 116.75/116.85 cnf(19,plain, % 116.75/116.85 (~P3(a1,x191)+P4(f7(f6(a1)),f6(a1))+P6(a9,a3,a1,f5(a1,x191))), % 116.75/116.85 inference(scs_inference,[],[2,1,4,9])). % 116.75/116.85 cnf(20,plain, % 116.75/116.85 (P4(f7(f6(a1)),f6(a1))+P6(a9,a3,a1,f5(a1,f2(a1)))), % 116.75/116.85 inference(scs_inference,[],[2,1,19,3])). % 116.75/116.85 cnf(54921,plain, % 116.75/116.85 (P3(a1,f2(a1))), % 116.75/116.85 inference(scs_inference,[],[2,1,3])). % 116.75/116.85 cnf(54925,plain, % 116.75/116.85 (~P6(a9,a3,a1,f5(a1,f2(a1)))+P5(f6(a1),f4(a3,a1))+P5(a8,f10(a9,f5(a1,f2(a1))))), % 116.75/116.85 inference(scs_inference,[],[2,1,3,5,10])). % 116.75/116.85 cnf(54927,plain, % 116.75/116.85 (P5(f6(a1),f4(a3,a1))+P6(a9,a3,a1,f5(a1,f2(a1)))), % 116.75/116.85 inference(scs_inference,[],[2,54921,1,9])). % 116.75/116.85 cnf(54931,plain, % 116.75/116.85 (P5(f6(a1),f4(a3,a1))+~P4(f5(a1,f2(a1)),f2(a1))+P5(a8,f10(a9,f5(a1,f2(a1))))), % 116.75/116.85 inference(scs_inference,[],[2,1,54927,10])). % 116.75/116.85 cnf(90372,plain, % 116.75/116.85 (P5(f6(a1),f4(a3,a1))+~P5(a8,f10(a9,f5(a1,f2(a1))))), % 116.75/116.85 inference(scs_inference,[],[2,1,54921,7])). % 116.75/116.85 cnf(90374,plain, % 116.75/116.85 (P5(f6(a1),f4(a3,a1))+~P6(a9,a3,a1,f5(a1,f2(a1)))), % 116.75/116.85 inference(scs_inference,[],[2,1,54921,7,54925])). % 116.75/116.85 cnf(90377,plain, % 116.75/116.85 (~P5(a8,f10(a9,f5(a1,f2(a1))))+~P5(a8,f10(a9,f7(f6(a1))))), % 116.75/116.85 inference(scs_inference,[],[90372,6])). % 116.75/116.85 cnf(90387,plain, % 116.75/116.85 (~P6(a9,a3,a1,f5(a1,f2(a1)))+P6(a9,a3,a1,f7(f6(a1)))), % 116.75/116.85 inference(scs_inference,[],[90374,8])). % 116.75/116.85 cnf(90403,plain, % 116.75/116.85 (~P5(a8,f10(a9,f7(f6(a1))))+~P6(a9,a3,a1,f5(a1,f2(a1)))+~P4(f5(a1,f2(a1)),f2(a1))), % 116.75/116.85 inference(scs_inference,[],[1,2,90377,10])). % 116.75/116.85 cnf(90467,plain, % 116.75/116.85 (~P4(f5(a1,f2(a1)),f2(a1))+~P5(a8,f10(a9,f7(f6(a1))))+P5(f6(a1),f4(a3,a1))), % 116.75/116.85 inference(scs_inference,[],[2,1,54921,90403,9])). % 116.75/116.85 cnf(90483,plain, % 116.75/116.85 (~P5(a8,f10(a9,f7(f6(a1))))+P5(f6(a1),f4(a3,a1))), % 116.75/116.85 inference(scs_inference,[],[2,1,54921,90467,5])). % 116.75/116.85 cnf(90499,plain, % 116.75/116.85 (~P5(a8,f10(a9,f7(f6(a1))))), % 116.75/116.85 inference(scs_inference,[],[90483,6])). % 116.75/116.85 cnf(90500,plain, % 116.75/116.85 (~P6(a9,a3,a1,f7(f6(a1)))+~P4(f7(f6(a1)),f6(a1))+P6(a9,a3,a1,f5(a1,f2(a1)))), % 116.75/116.85 inference(scs_inference,[],[2,1,54921,90499,14])). % 116.75/116.85 cnf(90562,plain, % 116.75/116.85 (~P6(a9,a3,a1,f5(a1,f2(a1)))+P4(f7(f6(a1)),f6(a1))), % 116.75/116.85 inference(scs_inference,[],[4,90374])). % 116.75/116.85 cnf(90578,plain, % 116.75/116.85 (P4(f7(f6(a1)),f6(a1))), % 116.75/116.85 inference(scs_inference,[],[90562,20])). % 116.75/116.85 cnf(90579,plain, % 116.75/116.85 (~P6(a9,a3,a1,f7(f6(a1)))+P6(a9,a3,a1,f5(a1,f2(a1)))), % 116.75/116.85 inference(scs_inference,[],[90578,90500])). % 116.75/116.85 cnf(90585,plain, % 116.75/116.85 (~P5(a8,f10(a9,f5(a1,f2(a1))))), % 116.75/116.85 inference(scs_inference,[],[2,1,54921,90499,90578,13,90387,18])). % 116.75/116.85 cnf(90588,plain, % 116.75/116.85 (P5(f6(a1),f4(a3,a1))+~P4(f5(a1,f2(a1)),f2(a1))), % 116.75/116.85 inference(scs_inference,[],[90585,54931])). % 116.75/116.85 cnf(90589,plain, % 116.75/116.85 (~P6(a9,a3,a1,f7(f6(a1)))+P4(f5(a1,f2(a1)),f2(a1))), % 116.75/116.85 inference(scs_inference,[],[2,1,54921,90499,90578,12])). % 116.75/116.85 cnf(90595,plain, % 116.75/116.85 (~P4(f5(a1,f2(a1)),f2(a1))+P6(a9,a3,a1,f7(f6(a1)))), % 116.75/116.86 inference(scs_inference,[],[90588,8])). % 116.75/116.86 cnf(90597,plain, % 116.75/116.86 (P4(f5(a1,f2(a1)),f2(a1))+~P5(f6(a1),f4(a3,a1))), % 116.75/116.86 inference(scs_inference,[],[90589,8])). % 116.75/116.86 cnf(90612,plain, % 116.75/116.86 (~P5(f6(a1),f4(a3,a1))+~P6(a9,a3,a1,f5(a1,f2(a1)))), % 116.75/116.86 inference(scs_inference,[],[1,2,90585,90597,10])). % 116.75/116.86 cnf(90628,plain, % 116.75/116.86 (~P4(f5(a1,f2(a1)),f2(a1))+P6(a9,a3,a1,f5(a1,f2(a1)))), % 116.75/116.86 inference(scs_inference,[],[90595,90579])). % 116.75/116.86 cnf(90644,plain, % 116.75/116.86 (~P4(f5(a1,f2(a1)),f2(a1))+~P5(f6(a1),f4(a3,a1))), % 116.75/116.86 inference(scs_inference,[],[90612,90628])). % 116.75/116.86 cnf(90660,plain, % 116.75/116.86 (~P6(a9,a3,a1,f7(f6(a1)))+~P5(f6(a1),f4(a3,a1))), % 116.75/116.86 inference(scs_inference,[],[90644,90589])). % 116.75/116.86 cnf(90676,plain, % 116.75/116.86 (~P5(f6(a1),f4(a3,a1))), % 116.75/116.86 inference(scs_inference,[],[90660,8])). % 116.75/116.86 cnf(90678,plain, % 116.75/116.86 (P6(a9,a3,a1,f5(a1,f2(a1)))), % 116.75/116.86 inference(scs_inference,[],[90676,54927])). % 116.75/116.86 cnf(90679,plain, % 116.75/116.86 (~P6(a9,a3,a1,f5(a1,f2(a1)))), % 116.75/116.86 inference(scs_inference,[],[90676,90374])). % 116.75/116.86 cnf(90684,plain, % 116.75/116.86 ($false), % 116.75/116.86 inference(scs_inference,[],[90678,90679]), % 116.75/116.86 ['proof']). % 116.75/116.88 % SZS output end Proof % 116.75/116.88 % Total time :116.284070s %------------------------------------------------------------------------------