%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT036+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 : n027.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 : Theorem 0.25s 0.52s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT036+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.08/0.35 % Computer : n027.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:42:30 UTC 2026 % 0.08/0.35 % CPUTime : % 0.25/0.52 start to proof:theBenchmark % 0.25/0.52 %------------------------------------------- % 0.25/0.52 % File :CSE---1.7 % 0.25/0.52 % Problem :theBenchmark % 0.25/0.52 % Transform :cnf % 0.25/0.52 % Format :tptp:raw % 0.25/0.52 % Command :java -jar mcs_scs.jar %d %s % 0.25/0.52 % 0.25/0.52 % Result :Theorem 0.013968s % 0.25/0.52 % Output :CNFRefutation 0.013968s % 0.25/0.52 %------------------------------------------- % 0.25/0.52 %-------------------------------------------------------------------------- % 0.25/0.52 % File : MGT036+1 : TPTP v9.3.0. Released v2.0.0. % 0.25/0.52 % Domain : Management (Organisation Theory) % 0.25/0.52 % Problem : First movers never outcompete efficient producers. % 0.25/0.52 % Version : [PB+94] axioms : Reduced & Augmented > Complete. % 0.25/0.52 % English : % 0.25/0.52 % 0.25/0.52 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 0.25/0.52 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 0.25/0.52 % : [Kam95] Kamps (1995), Email to G. Sutcliffe % 0.25/0.52 % Source : [Kam95] % 0.25/0.52 % Names : % 0.25/0.52 % 0.25/0.52 % Status : Theorem % 0.25/0.52 % Rating : 0.00 v9.1.0, 0.07 v9.0.0, 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.12 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 % 0.25/0.52 % Syntax : Number of formulae : 7 ( 1 unt; 0 def) % 0.25/0.52 % Number of atoms : 24 ( 0 equ) % 0.25/0.52 % Maximal formula atoms : 5 ( 3 avg) % 0.25/0.52 % Number of connectives : 21 ( 4 ~; 0 |; 9 &) % 0.25/0.52 % ( 2 <=>; 6 =>; 0 <=; 0 <~>) % 0.25/0.52 % Maximal formula depth : 10 ( 6 avg) % 0.25/0.52 % Maximal term depth : 2 ( 1 avg) % 0.25/0.52 % Number of predicates : 6 ( 6 usr; 0 prp; 1-4 aty) % 0.25/0.52 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty) % 0.25/0.52 % Number of variables : 18 ( 18 !; 0 ?) % 0.25/0.52 % SPC : FOF_THM_RFO_NEQ % 0.25/0.52 % 0.25/0.52 % Comments : % 0.25/0.52 %-------------------------------------------------------------------------- % 0.25/0.52 %----MP. The "pop" predicate is symmetric: if FM and EP are subpopulations, % 0.25/0.52 %----then EP and FM are also subpopulations. % 0.25/0.52 fof(mp_symmetry_of_FM_and_EP,axiom, % 0.25/0.52 ! [E,T] : % 0.25/0.52 ( ( environment(E) % 0.25/0.52 & subpopulations(first_movers,efficient_producers,E,T) ) % 0.25/0.52 => subpopulations(efficient_producers,first_movers,E,T) ) ). % 0.25/0.52 % 0.25/0.52 %----MP. The time points when FM and EP are present in the environment % 0.25/0.52 %----occur during the environment sustains. % 0.25/0.52 fof(mp_time_point_occur,axiom, % 0.25/0.52 ! [E,T] : % 0.25/0.52 ( ( environment(E) % 0.25/0.52 & subpopulations(first_movers,efficient_producers,E,T) ) % 0.25/0.52 => in_environment(E,T) ) ). % 0.25/0.52 % 0.25/0.52 %----MP. on "greater or equal to" % 0.25/0.52 fof(mp_growth_rate_relationships,axiom, % 0.25/0.52 ! [E,S1,S2,T] : % 0.25/0.52 ( ( ( environment(E) % 0.25/0.52 & subpopulations(S1,S2,E,T) ) % 0.25/0.52 => greater_or_equal(growth_rate(S1,T),zero) ) % 0.25/0.52 <=> ~ greater(zero,growth_rate(S1,T)) ) ). % 0.25/0.52 % 0.25/0.52 %----D2. A subpopulation outcompetes an other in an environment at a % 0.25/0.52 %----certain time, if and only if, it has non-negative growth rate while % 0.25/0.52 %----the other subpopulation has negative growth rate. % 0.25/0.52 fof(d2,hypothesis, % 0.25/0.52 ! [E,S1,S2,T] : % 0.25/0.52 ( ( environment(E) % 0.25/0.52 & subpopulations(S1,S2,E,T) ) % 0.25/0.52 => ( ( greater_or_equal(growth_rate(S2,T),zero) % 0.25/0.52 & greater(zero,growth_rate(S1,T)) ) % 0.25/0.52 <=> outcompetes(S2,S1,T) ) ) ). % 0.25/0.52 % 0.25/0.52 %----A12. If a subpopulation does not decrease in members, then a more % 0.25/0.52 %----resilient subpopulation does not decrease either. % 0.25/0.52 fof(a12,hypothesis, % 0.25/0.52 ! [E,S1,S2,T] : % 0.25/0.52 ( ( environment(E) % 0.25/0.52 & in_environment(E,T) % 0.25/0.52 & ~ greater(zero,growth_rate(S1,T)) % 0.25/0.52 & greater(resilience(S2),resilience(S1)) ) % 0.25/0.52 => ~ greater(zero,growth_rate(S2,T)) ) ). % 0.25/0.52 % 0.25/0.52 %----A2. Efficient producers are more resilient than first movers. % 0.25/0.52 fof(a2,hypothesis, % 0.25/0.52 greater(resilience(efficient_producers),resilience(first_movers)) ). % 0.25/0.52 % 0.25/0.52 %----GOAL: T5. First movers never outcompete efficient producers. % 0.25/0.52 fof(prove_t5,conjecture, % 0.25/0.52 ! [E,T] : % 0.25/0.52 ( ( environment(E) % 0.25/0.52 & subpopulations(first_movers,efficient_producers,E,T) ) % 0.25/0.52 => ~ outcompetes(first_movers,efficient_producers,T) ) ). % 0.25/0.52 % 0.25/0.52 %-------------------------------------------------------------------------- % 0.25/0.52 %------------------------------------------- % 0.25/0.52 % Proof found % 0.25/0.52 % SZS status Theorem for theBenchmark % 0.25/0.52 % SZS output start Proof % 0.25/0.52 %ClaNum:14(EqnAxiom:0) % 0.25/0.52 %VarNum:73(SingletonVarNum:33) % 0.25/0.52 %MaxLitNum:5 % 0.25/0.52 %MaxfuncDepth:1 % 0.25/0.52 %SharedTerms:11 % 0.25/0.52 %goalClause: 1 3 4 % 0.25/0.52 %singleGoalClaCount:3 % 0.25/0.52 [1]P1(a1) % 0.25/0.52 [3]P3(a4,a2,a5) % 0.25/0.52 [4]P6(a4,a2,a1,a5) % 0.25/0.52 [2]P2(f3(a2),f3(a4)) % 0.25/0.52 [6]~P2(a7,f6(x61,x62))+~P4(f6(x61,x62),a7) % 0.25/0.52 [5]P1(x51)+~P2(a7,f6(x52,x53)) % 0.25/0.52 [8]P6(x81,x82,x83,x84)+~P2(a7,f6(x81,x84)) % 0.25/0.52 [9]~P1(x91)+P5(x91,x92)+~P6(a4,a2,x91,x92) % 0.25/0.52 [14]~P1(x141)+~P6(a4,a2,x141,x142)+P6(a2,a4,x141,x142) % 0.25/0.53 [10]~P6(x101,x104,x103,x102)+~P1(x103)+P2(a7,f6(x101,x102))+P4(f6(x101,x102),a7) % 0.25/0.53 [11]~P6(x111,x114,x113,x112)+~P3(x114,x111,x112)+~P1(x113)+P2(a7,f6(x111,x112)) % 0.25/0.53 [12]~P6(x124,x121,x123,x122)+~P3(x121,x124,x122)+~P1(x123)+P4(f6(x121,x122),a7) % 0.25/0.53 [7]~P5(x73,x72)+~P1(x73)+~P2(f3(x74),f3(x71))+P2(a7,f6(x71,x72))+~P2(a7,f6(x74,x72)) % 0.25/0.53 [13]~P6(x132,x131,x134,x133)+P3(x131,x132,x133)+~P1(x134)+~P2(a7,f6(x132,x133))+~P4(f6(x131,x133),a7) % 0.25/0.53 %EqnAxiom % 0.25/0.53 % 0.25/0.53 %------------------------------------------- % 0.25/0.53 cnf(15,plain, % 0.25/0.53 (P5(a1,a5)), % 0.25/0.53 inference(scs_inference,[],[1,4,9])). % 0.25/0.53 cnf(22,plain, % 0.25/0.53 (P1(x221)+P4(f6(a4,a5),a7)), % 0.25/0.53 inference(scs_inference,[],[1,4,5,10])). % 0.25/0.53 cnf(23,plain, % 0.25/0.53 (P4(f6(a4,a5),a7)+P6(a2,a4,a1,a5)), % 0.25/0.53 inference(scs_inference,[],[4,22,14])). % 0.25/0.53 cnf(24,plain, % 0.25/0.53 (P4(f6(a4,a5),a7)), % 0.25/0.53 inference(scs_inference,[],[3,1,23,12])). % 0.25/0.53 cnf(25,plain, % 0.25/0.53 (P2(a7,f6(a4,a5))+~P2(a7,f6(a2,a5))+~P2(a7,f6(x251,x252))), % 0.25/0.53 inference(scs_inference,[],[2,15,5,7])). % 0.25/0.53 cnf(26,plain, % 0.25/0.53 (P2(a7,f6(a4,a5))+~P2(a7,f6(a2,a5))), % 0.25/0.53 inference(factoring_inference,[],[25])). % 0.25/0.53 cnf(27,plain, % 0.25/0.53 (~P2(a7,f6(a2,a5))), % 0.25/0.53 inference(scs_inference,[],[24,26,6])). % 0.25/0.53 cnf(30,plain, % 0.25/0.53 ($false), % 0.25/0.53 inference(scs_inference,[],[3,4,1,27,11,14]), % 0.25/0.53 ['proof']). % 0.25/0.53 % SZS output end Proof % 0.25/0.53 % Total time :0.013968s %------------------------------------------------------------------------------