%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT030+1 : 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 : n013.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 122.19s 122.37s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT030+1 : 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.07/0.34 % Computer : n013.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Mon Sep 7 12:18:20 UTC 2026 % 0.07/0.34 % CPUTime : % 0.23/0.51 start to proof:theBenchmark % 122.19/122.36 %------------------------------------------- % 122.19/122.36 % File :CSE---1.7 % 122.19/122.36 % Problem :theBenchmark % 122.19/122.36 % Transform :cnf % 122.19/122.36 % Format :tptp:raw % 122.19/122.36 % Command :java -jar mcs_scs.jar %d %s % 122.19/122.36 % 122.19/122.36 % Result :Theorem 121.839306s % 122.19/122.36 % Output :CNFRefutation 121.839306s % 122.19/122.36 %------------------------------------------- % 122.19/122.36 %-------------------------------------------------------------------------- % 122.19/122.36 % File : MGT030+1 : TPTP v9.3.0. Released v2.0.0. % 122.19/122.36 % Domain : Management (Organisation Theory) % 122.19/122.36 % Problem : Earliest time point when FM growth rate exceeds EP growth rate % 122.19/122.36 % Version : [PB+94] axioms : Reduced & Augmented > Complete. % 122.19/122.36 % English : There is an earliest time point, past which FM's growth % 122.19/122.36 % rate exceeds EP's growth rate. % 122.19/122.36 % 122.19/122.37 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 122.19/122.37 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 122.19/122.37 % : [Kam95] Kamps (1995), Email to G. Sutcliffe % 122.19/122.37 % Source : [Kam95] % 122.19/122.37 % Names : % 122.19/122.37 % 122.19/122.37 % Status : Theorem % 122.19/122.37 % Rating : 0.00 v9.1.0, 0.07 v9.0.0, 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.08 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 % 122.19/122.37 % Syntax : Number of formulae : 3 ( 0 unt; 0 def) % 122.19/122.37 % Number of atoms : 23 ( 0 equ) % 122.19/122.37 % Maximal formula atoms : 10 ( 7 avg) % 122.19/122.37 % Number of connectives : 22 ( 2 ~; 0 |; 13 &) % 122.19/122.37 % ( 0 <=>; 7 =>; 0 <=; 0 <~>) % 122.19/122.37 % Maximal formula depth : 9 ( 9 avg) % 122.19/122.37 % Maximal term depth : 2 ( 1 avg) % 122.19/122.37 % Number of predicates : 6 ( 6 usr; 0 prp; 1-4 aty) % 122.19/122.37 % Number of functors : 3 ( 3 usr; 2 con; 0-2 aty) % 122.19/122.37 % Number of variables : 11 ( 7 !; 4 ?) % 122.19/122.37 % SPC : FOF_THM_RFO_NEQ % 122.19/122.37 % 122.19/122.37 % Comments : % 122.19/122.37 %-------------------------------------------------------------------------- % 122.19/122.37 %----MP. If EP's growth rate exceeds FM's growth rate past a certain time, % 122.19/122.37 %----then there is an earliest time point, past which FM's growth rate % 122.19/122.37 %----exceeds EP's growth rate. % 122.19/122.37 fof(mp_earliest_time_growth_rate_exceeds,axiom, % 122.19/122.37 ! [E] : % 122.19/122.37 ( ( environment(E) % 122.19/122.37 & ? [To] : % 122.19/122.37 ( in_environment(E,To) % 122.19/122.37 & ! [T] : % 122.19/122.37 ( ( subpopulations(first_movers,efficient_producers,E,T) % 122.19/122.37 & greater_or_equal(T,To) ) % 122.19/122.37 => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ) % 122.19/122.37 => ? [To] : % 122.19/122.37 ( in_environment(E,To) % 122.19/122.37 & ~ greater(growth_rate(efficient_producers,To),growth_rate(first_movers,To)) % 122.19/122.37 & ! [T] : % 122.19/122.37 ( ( subpopulations(first_movers,efficient_producers,E,T) % 122.19/122.37 & greater(T,To) ) % 122.19/122.37 => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ) ). % 122.19/122.37 % 122.19/122.37 %----L1. The growth rate of efficient producers exceeds the growth rate of % 122.19/122.37 %----first movers past a certain time in stable environments. % 122.19/122.37 fof(l1,hypothesis, % 122.19/122.37 ! [E] : % 122.19/122.37 ( ( environment(E) % 122.19/122.37 & stable(E) ) % 122.19/122.37 => ? [To] : % 122.19/122.37 ( in_environment(E,To) % 122.19/122.37 & ! [T] : % 122.19/122.37 ( ( subpopulations(first_movers,efficient_producers,E,T) % 122.19/122.37 & greater_or_equal(T,To) ) % 122.19/122.37 => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ) ). % 122.19/122.37 % 122.19/122.37 %----GOAL:L12. There is an earliest time point, past which FM's growth % 122.19/122.37 %----rate exceeds EP's growth rate. % 122.19/122.37 fof(prove_l12,conjecture, % 122.19/122.37 ! [E] : % 122.19/122.37 ( ( environment(E) % 122.19/122.37 & stable(E) ) % 122.19/122.37 => ? [To] : % 122.19/122.37 ( in_environment(E,To) % 122.19/122.37 & ~ greater(growth_rate(efficient_producers,To),growth_rate(first_movers,To)) % 122.19/122.37 & ! [T] : % 122.19/122.37 ( ( subpopulations(first_movers,efficient_producers,E,T) % 122.19/122.37 & greater(T,To) ) % 122.19/122.37 => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ) ). % 122.19/122.37 % 122.19/122.37 %-------------------------------------------------------------------------- % 122.19/122.37 %------------------------------------------- % 122.19/122.37 % Proof found % 122.19/122.37 % SZS status Theorem for theBenchmark % 122.19/122.37 % SZS output start Proof % 122.19/122.37 %ClaNum:16(EqnAxiom:0) % 122.19/122.37 %VarNum:113(SingletonVarNum:27) % 122.19/122.37 %MaxLitNum:6 % 122.19/122.37 %MaxfuncDepth:2 % 122.19/122.37 %SharedTerms:5 % 122.19/122.37 %goalClause: 1 2 5 7 10 % 122.19/122.37 %singleGoalClaCount:2 % 122.19/122.37 [1]P1(a1) % 122.19/122.37 [2]P2(a1) % 122.19/122.37 [3]~P1(x31)+~P2(x31)+P3(x31,f2(x31)) % 122.19/122.37 [5]~P3(a1,x51)+P5(f6(x51),x51)+P5(f7(a5,x51),f7(a8,x51)) % 122.19/122.37 [10]~P3(a1,x101)+P5(f7(a5,x101),f7(a8,x101))+P6(a8,a5,a1,f6(x101)) % 122.19/122.37 [7]~P3(a1,x71)+P5(f7(a5,x71),f7(a8,x71))+~P5(f7(a5,f6(x71)),f7(a8,f6(x71))) % 122.19/122.37 [4]~P1(x41)+~P3(x41,x42)+P3(x41,f3(x41))+P4(f4(x41,x42),x42) % 122.19/122.37 [9]~P1(x91)+~P3(x91,x92)+P3(x91,f3(x91))+P6(a8,a5,x91,f4(x91,x92)) % 122.19/122.37 [6]~P1(x61)+~P3(x61,x62)+P4(f4(x61,x62),x62)+~P5(f7(a5,f3(x61)),f7(a8,f3(x61))) % 122.19/122.37 [8]~P1(x81)+~P3(x81,x82)+P3(x81,f3(x81))+~P5(f7(a5,f4(x81,x82)),f7(a8,f4(x81,x82))) % 122.19/122.37 [11]~P1(x111)+~P3(x111,x112)+~P5(f7(a5,f3(x111)),f7(a8,f3(x111)))+~P5(f7(a5,f4(x111,x112)),f7(a8,f4(x111,x112))) % 122.19/122.37 [12]~P1(x121)+~P3(x121,x122)+P6(a8,a5,x121,f4(x121,x122))+~P5(f7(a5,f3(x121)),f7(a8,f3(x121))) % 122.19/122.37 [13]~P2(x132)+~P1(x132)+~P4(x131,f2(x132))+~P6(a8,a5,x132,x131)+P5(f7(a5,x131),f7(a8,x131)) % 122.19/122.37 [14]~P1(x141)+~P3(x141,x142)+~P5(x143,f3(x141))+~P6(a8,a5,x141,x143)+P4(f4(x141,x142),x142)+P5(f7(a5,x143),f7(a8,x143)) % 122.19/122.37 [16]~P1(x161)+~P3(x161,x162)+~P5(x163,f3(x161))+~P6(a8,a5,x161,x163)+P6(a8,a5,x161,f4(x161,x162))+P5(f7(a5,x163),f7(a8,x163)) % 122.19/122.37 [15]~P3(x152,x153)+~P1(x152)+~P5(x151,f3(x152))+~P6(a8,a5,x152,x151)+P5(f7(a5,x151),f7(a8,x151))+~P5(f7(a5,f4(x152,x153)),f7(a8,f4(x152,x153))) % 122.19/122.37 %EqnAxiom % 122.19/122.37 % 122.19/122.37 %------------------------------------------- % 122.41/122.51 cnf(71025,plain, % 122.41/122.51 (P3(a1,f2(a1))), % 122.41/122.51 inference(scs_inference,[],[2,1,3])). % 122.41/122.51 cnf(71032,plain, % 122.41/122.51 (P4(f4(a1,f2(a1)),f2(a1))+~P5(f7(a5,f3(a1)),f7(a8,f3(a1)))), % 122.41/122.51 inference(scs_inference,[],[71025,1,6])). % 122.41/122.51 cnf(71034,plain, % 122.41/122.51 (P6(a8,a5,a1,f4(a1,f2(a1)))+~P5(f7(a5,f3(a1)),f7(a8,f3(a1)))), % 122.41/122.51 inference(scs_inference,[],[71025,1,6,12])). % 122.41/122.51 cnf(71037,plain, % 122.41/122.51 (~P6(a8,a5,a1,x710371)+~P4(x710371,f2(a1))+P5(f7(a5,x710371),f7(a8,x710371))), % 122.41/122.51 inference(scs_inference,[],[2,1,13])). % 122.41/122.51 cnf(71040,plain, % 122.41/122.51 (~P6(a8,a5,a1,x710401)+P4(f4(a1,f2(a1)),f2(a1))+~P5(x710401,f3(a1))+P5(f7(a5,x710401),f7(a8,x710401))), % 122.41/122.51 inference(scs_inference,[],[71025,1,14])). % 122.41/122.51 cnf(71045,plain, % 122.41/122.51 (~P6(a8,a5,a1,x710451)+~P4(f4(a1,f2(a1)),f2(a1))+~P5(x710451,f3(a1))+P5(f7(a5,f4(a1,f2(a1))),f7(a8,f4(a1,f2(a1))))+P5(f7(a5,x710451),f7(a8,x710451))), % 122.41/122.51 inference(scs_inference,[],[2,71025,1,13,16])). % 122.41/122.51 cnf(71046,plain, % 122.41/122.51 (~P6(a8,a5,a1,x710461)+~P5(x710461,f3(a1))+P5(f7(a5,x710461),f7(a8,x710461))+~P5(f7(a5,f4(a1,f2(a1))),f7(a8,f4(a1,f2(a1))))), % 122.41/122.51 inference(scs_inference,[],[71025,1,15])). % 122.41/122.51 cnf(75741,plain, % 122.41/122.51 (~P6(a8,a5,a1,f4(a1,f2(a1)))+~P6(a8,a5,a1,x757411)+~P4(f4(a1,f2(a1)),f2(a1))+~P5(x757411,f3(a1))+P5(f7(a5,x757411),f7(a8,x757411))), % 122.41/122.51 inference(scs_inference,[],[2,71025,1,13,15])). % 122.41/122.51 cnf(123341,plain, % 122.41/122.51 (P3(a1,f3(a1))+~P5(f7(a5,f4(a1,f2(a1))),f7(a8,f4(a1,f2(a1))))), % 122.41/122.51 inference(scs_inference,[],[1,71025,10,5,7,8])). % 122.41/122.51 cnf(123418,plain, % 122.41/122.51 (P3(a1,f3(a1))+~P6(a8,a5,a1,f4(a1,f2(a1)))+~P4(f4(a1,f2(a1)),f2(a1))), % 122.41/122.51 inference(scs_inference,[],[1,2,123341,13])). % 122.41/122.51 cnf(123425,plain, % 122.41/122.51 (~P4(f4(a1,f2(a1)),f2(a1))+P3(a1,f3(a1))), % 122.41/122.51 inference(scs_inference,[],[71025,1,123418,9])). % 122.41/122.51 cnf(123432,plain, % 122.41/122.51 (P3(a1,f3(a1))), % 122.41/122.51 inference(scs_inference,[],[71025,1,123425,4])). % 122.41/122.51 cnf(137337,plain, % 122.41/122.51 (P5(f7(a5,f3(a1)),f7(a8,f3(a1)))+~P5(f7(a5,f6(f3(a1))),f7(a8,f6(f3(a1))))), % 122.41/122.51 inference(scs_inference,[],[123432,7])). % 122.41/122.51 cnf(137343,plain, % 122.41/122.51 (P5(f6(f3(a1)),f3(a1))+P5(f7(a5,f3(a1)),f7(a8,f3(a1)))), % 122.41/122.51 inference(scs_inference,[],[123432,5])). % 122.41/122.51 cnf(137345,plain, % 122.41/122.51 (P5(f7(a5,f3(a1)),f7(a8,f3(a1)))+P6(a8,a5,a1,f6(f3(a1)))), % 122.41/122.51 inference(scs_inference,[],[123432,5,10])). % 122.41/122.51 cnf(137396,plain, % 122.41/122.51 (P4(f4(a1,f2(a1)),f2(a1))+P5(f6(f3(a1)),f3(a1))), % 122.41/122.51 inference(scs_inference,[],[137343,71032])). % 122.41/122.51 cnf(137669,plain, % 122.41/122.51 (P4(f4(a1,f2(a1)),f2(a1))+~P5(f7(a5,f6(f3(a1))),f7(a8,f6(f3(a1))))), % 122.41/122.51 inference(scs_inference,[],[137337,71032])). % 122.41/122.51 cnf(138487,plain, % 122.41/122.51 (P4(f4(a1,f2(a1)),f2(a1))+P5(f7(a5,f6(f3(a1))),f7(a8,f6(f3(a1))))+~P6(a8,a5,a1,f6(f3(a1)))), % 122.41/122.51 inference(scs_inference,[],[137396,71040])). % 122.41/122.51 cnf(138578,plain, % 122.41/122.51 (P4(f4(a1,f2(a1)),f2(a1))+~P6(a8,a5,a1,f6(f3(a1)))), % 122.41/122.51 inference(scs_inference,[],[138487,137669])). % 122.41/122.51 cnf(139667,plain, % 122.41/122.51 (P4(f4(a1,f2(a1)),f2(a1))+P5(f7(a5,f3(a1)),f7(a8,f3(a1)))), % 122.41/122.51 inference(scs_inference,[],[138578,137345])). % 122.41/122.51 cnf(139758,plain, % 122.41/122.51 (P5(f7(a5,f3(a1)),f7(a8,f3(a1)))+~P6(a8,a5,a1,f4(a1,f2(a1)))+P5(f7(a5,f4(a1,f2(a1))),f7(a8,f4(a1,f2(a1))))), % 122.41/122.51 inference(scs_inference,[],[1,2,139667,13])). % 122.41/122.51 cnf(139849,plain, % 122.41/122.51 (~P6(a8,a5,a1,f4(a1,f2(a1)))+P5(f7(a5,f4(a1,f2(a1))),f7(a8,f4(a1,f2(a1))))+P4(f4(a1,f2(a1)),f2(a1))), % 122.41/122.51 inference(scs_inference,[],[139758,71032])). % 122.41/122.51 cnf(139940,plain, % 122.41/122.51 (P5(f7(a5,f4(a1,f2(a1))),f7(a8,f4(a1,f2(a1))))+~P6(a8,a5,a1,f4(a1,f2(a1)))), % 122.41/122.51 inference(scs_inference,[],[139849,71037])). % 122.41/122.51 cnf(140031,plain, % 122.41/122.51 (~P6(a8,a5,a1,f4(a1,f2(a1)))+~P5(f7(a5,f3(a1)),f7(a8,f3(a1)))), % 122.41/122.51 inference(scs_inference,[],[1,71025,139940,11])). % 122.41/122.51 cnf(140122,plain, % 122.41/122.51 (~P5(f7(a5,f3(a1)),f7(a8,f3(a1)))), % 122.41/122.51 inference(scs_inference,[],[140031,71034])). % 122.41/122.51 cnf(140123,plain, % 122.41/122.51 (~P5(f7(a5,f6(f3(a1))),f7(a8,f6(f3(a1))))), % 122.41/122.51 inference(scs_inference,[],[140122,137337])). % 122.41/122.51 cnf(140124,plain, % 122.41/122.51 (P5(f6(f3(a1)),f3(a1))), % 122.41/122.51 inference(scs_inference,[],[140122,137343])). % 122.41/122.51 cnf(140125,plain, % 122.41/122.51 (P6(a8,a5,a1,f6(f3(a1)))), % 122.41/122.51 inference(scs_inference,[],[140122,137345])). % 122.41/122.51 cnf(140126,plain, % 122.41/122.51 (P4(f4(a1,f2(a1)),f2(a1))), % 122.41/122.51 inference(scs_inference,[],[140122,139667])). % 122.41/122.51 cnf(140135,plain, % 122.41/122.51 (P5(f7(a5,f4(a1,f2(a1))),f7(a8,f4(a1,f2(a1))))+~P5(x1401351,f3(a1))+P5(f7(a5,x1401351),f7(a8,x1401351))+~P6(a8,a5,a1,x1401351)), % 122.41/122.51 inference(scs_inference,[],[140126,71045])). % 122.41/122.51 cnf(140136,plain, % 122.41/122.51 (~P6(a8,a5,a1,f4(a1,f2(a1)))+~P5(x1401361,f3(a1))+P5(f7(a5,x1401361),f7(a8,x1401361))+~P6(a8,a5,a1,x1401361)), % 122.41/122.51 inference(scs_inference,[],[140126,75741])). % 122.41/122.51 cnf(140146,plain, % 122.41/122.51 ($false), % 122.41/122.51 inference(scs_inference,[],[140123,140124,140125,71037,140135,140136,71046]), % 122.41/122.51 ['proof']). % 122.41/122.56 % SZS output end Proof % 122.41/122.56 % Total time :121.839306s %------------------------------------------------------------------------------