%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT036+3 : 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 : n007.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:19 AM UTC 2026 % Result : Theorem 0.23s 0.50s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT036+3 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.34 % Computer : n007.cluster.edu % 0.09/0.34 % Model : x86_64 x86_64 % 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.34 % Memory : 8046.5625MB % 0.09/0.34 % OS : Linux 6.8.0-71-generic % 0.09/0.34 % CPULimit : 300 % 0.09/0.34 % WCLimit : 300 % 0.09/0.34 % DateTime : Mon Sep 7 12:39:56 UTC 2026 % 0.09/0.34 % CPUTime : % 0.23/0.50 start to proof:theBenchmark % 0.23/0.50 %------------------------------------------- % 0.23/0.50 % File :CSE---1.7 % 0.23/0.50 % Problem :theBenchmark % 0.23/0.50 % Transform :cnf % 0.23/0.50 % Format :tptp:raw % 0.23/0.50 % Command :java -jar mcs_scs.jar %d %s % 0.23/0.50 % 0.23/0.50 % Result :Theorem 0.004389s % 0.23/0.50 % Output :CNFRefutation 0.004389s % 0.23/0.50 %------------------------------------------- % 0.23/0.50 %-------------------------------------------------------------------------- % 0.23/0.50 % File : MGT036+3 : TPTP v9.3.0. Released v2.0.0. % 0.23/0.50 % Domain : Management (Organisation Theory) % 0.23/0.50 % Problem : First movers never outcompete efficient producers. % 0.23/0.50 % Version : [PM93] axioms. % 0.23/0.50 % English : % 0.23/0.50 % 0.23/0.50 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 0.23/0.50 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 0.23/0.50 % Source : [PM93] % 0.23/0.50 % Names : THEOREM 5* [PM93] % 0.23/0.50 % 0.23/0.50 % Status : Theorem % 0.23/0.50 % Rating : 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.04 v5.3.0, 0.13 v5.2.0, 0.00 v2.1.0 % 0.23/0.50 % Syntax : Number of formulae : 4 ( 0 unt; 0 def) % 0.23/0.50 % Number of atoms : 15 ( 0 equ) % 0.23/0.50 % Maximal formula atoms : 5 ( 3 avg) % 0.23/0.50 % Number of connectives : 11 ( 0 ~; 0 |; 8 &) % 0.23/0.50 % ( 1 <=>; 2 =>; 0 <=; 0 <~>) % 0.23/0.50 % Maximal formula depth : 8 ( 7 avg) % 0.23/0.50 % Maximal term depth : 2 ( 1 avg) % 0.23/0.50 % Number of predicates : 5 ( 5 usr; 0 prp; 1-4 aty) % 0.23/0.50 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty) % 0.23/0.50 % Number of variables : 12 ( 8 !; 4 ?) % 0.23/0.50 % SPC : FOF_THM_RFO_NEQ % 0.23/0.50 % 0.23/0.50 % Comments : % 0.23/0.50 %-------------------------------------------------------------------------- % 0.23/0.50 %----MP. The "pop" predicate is symmetric: if S1 and S2 are subpopulations, % 0.23/0.50 %----then S2 and S1 are also subpopulations. % 0.23/0.50 fof(mp_symmetry_of_subpopulations,axiom, % 0.23/0.50 ! [E,S1,S2,T] : % 0.23/0.50 ( ( environment(E) % 0.23/0.50 & subpopulations(S1,S2,E,T) ) % 0.23/0.50 => subpopulations(S2,S1,E,T) ) ). % 0.23/0.50 % 0.23/0.50 %----D2. A subpopulation outcompetes an other in an environment at a % 0.23/0.50 %----certain time, if and only if, it has non-negative growth rate while % 0.23/0.50 %----the other subpopulation has negative growth rate. % 0.23/0.50 fof(d2,hypothesis, % 0.23/0.50 ! [E,S1,S2,T] : % 0.23/0.50 ( ( environment(E) % 0.23/0.50 & subpopulations(S1,S2,E,T) ) % 0.23/0.50 => ( ( greater_or_equal(growth_rate(S2,T),zero) % 0.23/0.50 & greater(zero,growth_rate(S1,T)) ) % 0.23/0.50 <=> outcompetes(S2,S1,T) ) ) ). % 0.23/0.50 % 0.23/0.50 %----A13*: Efficient producers may decrease in members even when the first % 0.23/0.50 %----mover subpopulation grows or stagnates. % 0.23/0.50 fof(a13_star,hypothesis, % 0.23/0.50 ? [E,T] : % 0.23/0.50 ( environment(E) % 0.23/0.50 & subpopulations(first_movers,efficient_producers,E,T) % 0.23/0.50 & greater_or_equal(growth_rate(first_movers,T),zero) % 0.23/0.50 & greater(zero,growth_rate(efficient_producers,T)) ) ). % 0.23/0.50 % 0.23/0.50 %----GOAL: T5*. First movers may outcompete efficient producers in some % 0.23/0.50 %----environments. % 0.23/0.50 fof(prove_t5_star,conjecture, % 0.23/0.50 ? [E,T] : % 0.23/0.50 ( environment(E) % 0.23/0.50 & subpopulations(first_movers,efficient_producers,E,T) % 0.23/0.50 & outcompetes(first_movers,efficient_producers,T) ) ). % 0.23/0.50 % 0.23/0.50 %-------------------------------------------------------------------------- % 0.23/0.50 %------------------------------------------- % 0.23/0.50 % Proof found % 0.23/0.50 % SZS status Theorem for theBenchmark % 0.23/0.50 % SZS output start Proof % 0.23/0.50 %ClaNum:9(EqnAxiom:0) % 0.23/0.50 %VarNum:45(SingletonVarNum:18) % 0.23/0.50 %MaxLitNum:5 % 0.23/0.50 %MaxfuncDepth:1 % 0.23/0.50 %SharedTerms:11 % 0.23/0.50 %goalClause: 5 % 0.23/0.50 [1]P1(a1) % 0.23/0.50 [4]P4(a6,a2,a1,a4) % 0.23/0.50 [2]P2(a3,f5(a2,a4)) % 0.23/0.50 [3]P3(f5(a6,a4),a3) % 0.23/0.50 [5]~P1(x51)+~P4(a6,a2,x51,x52)+~P5(a6,a2,x52) % 0.23/0.50 [9]~P1(x93)+~P4(x92,x91,x93,x94)+P4(x91,x92,x93,x94) % 0.23/0.50 [6]~P4(x61,x64,x63,x62)+~P5(x64,x61,x62)+~P1(x63)+P2(a3,f5(x61,x62)) % 0.23/0.50 [7]~P4(x74,x71,x73,x72)+~P5(x71,x74,x72)+~P1(x73)+P3(f5(x71,x72),a3) % 0.23/0.50 [8]~P4(x82,x81,x84,x83)+P5(x81,x82,x83)+~P1(x84)+~P2(a3,f5(x82,x83))+~P3(f5(x81,x83),a3) % 0.23/0.50 %EqnAxiom % 0.23/0.50 % 0.23/0.50 %------------------------------------------- % 0.23/0.50 cnf(12,plain, % 0.23/0.50 (~P4(a2,a6,a1,a4)), % 0.23/0.50 inference(scs_inference,[],[1,4,2,3,8,5])). % 0.23/0.50 cnf(13,plain, % 0.23/0.50 ($false), % 0.23/0.50 inference(scs_inference,[],[1,12,4,9]), % 0.23/0.50 ['proof']). % 0.23/0.50 % SZS output end Proof % 0.23/0.50 % Total time :0.004389s %------------------------------------------------------------------------------