%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT036-3 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n031.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 : Unsatisfiable 0.28s 0.53s % 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.4.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.35 % Computer : n031.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:45:56 UTC 2026 % 0.08/0.35 % CPUTime : % 0.28/0.52 start to proof:theBenchmark % 0.28/0.52 %------------------------------------------- % 0.28/0.52 % File :CSE---1.7 % 0.28/0.52 % Problem :theBenchmark % 0.28/0.52 % Transform :cnf % 0.28/0.52 % Format :tptp:raw % 0.28/0.52 % Command :java -jar mcs_scs.jar %d %s % 0.28/0.52 % 0.28/0.52 % Result :Theorem 0.004572s % 0.28/0.52 % Output :CNFRefutation 0.004572s % 0.28/0.52 %------------------------------------------- % 0.28/0.52 %-------------------------------------------------------------------------- % 0.28/0.52 % File : MGT036-3 : TPTP v9.3.0. Released v2.4.0. % 0.28/0.52 % Domain : Management (Organisation Theory) % 0.28/0.52 % Problem : First movers never outcompete efficient producers. % 0.28/0.52 % Version : [PM93] axioms. % 0.28/0.52 % English : % 0.28/0.52 % 0.28/0.52 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 0.28/0.52 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 0.28/0.52 % Source : [TPTP] % 0.28/0.52 % Names : % 0.28/0.52 % 0.28/0.52 % Status : Unsatisfiable % 0.28/0.53 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.00 v2.4.0 % 0.28/0.53 % Syntax : Number of clauses : 9 ( 4 unt; 0 nHn; 9 RR) % 0.28/0.53 % Number of literals : 23 ( 0 equ; 15 neg) % 0.28/0.53 % Maximal clause size : 5 ( 2 avg) % 0.28/0.53 % Maximal term depth : 2 ( 1 avg) % 0.28/0.53 % Number of predicates : 5 ( 5 usr; 0 prp; 1-4 aty) % 0.28/0.53 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty) % 0.28/0.53 % Number of variables : 18 ( 0 sgn) % 0.28/0.53 % SPC : CNF_UNS_RFO_NEQ_HRN % 0.28/0.53 % 0.28/0.53 % Comments : Created with tptp2X -f tptp -t clausify:otter MGT036+3.p % 0.28/0.53 %-------------------------------------------------------------------------- % 0.28/0.53 cnf(mp_symmetry_of_subpopulations_1,axiom, % 0.28/0.53 ( ~ environment(A) % 0.28/0.53 | ~ subpopulations(B,C,A,D) % 0.28/0.53 | subpopulations(C,B,A,D) ) ). % 0.28/0.53 % 0.28/0.53 cnf(d2_2,hypothesis, % 0.28/0.53 ( ~ environment(A) % 0.28/0.53 | ~ subpopulations(B,C,A,D) % 0.28/0.53 | ~ greater_or_equal(growth_rate(C,D),zero) % 0.28/0.53 | ~ greater(zero,growth_rate(B,D)) % 0.28/0.53 | outcompetes(C,B,D) ) ). % 0.28/0.53 % 0.28/0.53 cnf(d2_3,hypothesis, % 0.28/0.53 ( ~ environment(A) % 0.28/0.53 | ~ subpopulations(B,C,A,D) % 0.28/0.53 | ~ outcompetes(C,B,D) % 0.28/0.53 | greater_or_equal(growth_rate(C,D),zero) ) ). % 0.28/0.53 % 0.28/0.53 cnf(d2_4,hypothesis, % 0.28/0.53 ( ~ environment(A) % 0.28/0.53 | ~ subpopulations(B,C,A,D) % 0.28/0.53 | ~ outcompetes(C,B,D) % 0.28/0.53 | greater(zero,growth_rate(B,D)) ) ). % 0.28/0.53 % 0.28/0.53 cnf(a13_star_5,hypothesis, % 0.28/0.53 environment(sk1) ). % 0.28/0.53 % 0.28/0.53 cnf(a13_star_6,hypothesis, % 0.28/0.53 subpopulations(first_movers,efficient_producers,sk1,sk2) ). % 0.28/0.53 % 0.28/0.53 cnf(a13_star_7,hypothesis, % 0.28/0.53 greater_or_equal(growth_rate(first_movers,sk2),zero) ). % 0.28/0.53 % 0.28/0.53 cnf(a13_star_8,hypothesis, % 0.28/0.53 greater(zero,growth_rate(efficient_producers,sk2)) ). % 0.28/0.53 % 0.28/0.53 cnf(prove_t5_star_9,negated_conjecture, % 0.28/0.53 ( ~ environment(A) % 0.28/0.53 | ~ subpopulations(first_movers,efficient_producers,A,B) % 0.28/0.53 | ~ outcompetes(first_movers,efficient_producers,B) ) ). % 0.28/0.53 % 0.28/0.53 %-------------------------------------------------------------------------- % 0.28/0.53 %------------------------------------------- % 0.28/0.53 % Proof found % 0.28/0.53 % SZS status Theorem for theBenchmark % 0.28/0.53 % SZS output start Proof % 0.28/0.53 %ClaNum:9(EqnAxiom:0) % 0.28/0.53 %VarNum:45(SingletonVarNum:18) % 0.28/0.53 %MaxLitNum:5 % 0.28/0.53 %MaxfuncDepth:1 % 0.28/0.53 %SharedTerms:11 % 0.28/0.53 %goalClause: 5 % 0.28/0.53 [1]P1(a1) % 0.28/0.53 [4]P4(a4,a2,a1,a6) % 0.28/0.53 [2]P2(a5,f3(a2,a6)) % 0.28/0.53 [3]P3(f3(a4,a6),a5) % 0.28/0.53 [5]~P1(x51)+~P4(a4,a2,x51,x52)+~P5(a4,a2,x52) % 0.28/0.53 [9]~P1(x93)+~P4(x92,x91,x93,x94)+P4(x91,x92,x93,x94) % 0.28/0.53 [6]~P4(x61,x64,x63,x62)+~P5(x64,x61,x62)+~P1(x63)+P2(a5,f3(x61,x62)) % 0.28/0.53 [7]~P4(x74,x71,x73,x72)+~P5(x71,x74,x72)+~P1(x73)+P3(f3(x71,x72),a5) % 0.28/0.53 [8]~P4(x82,x81,x84,x83)+P5(x81,x82,x83)+~P1(x84)+~P2(a5,f3(x82,x83))+~P3(f3(x81,x83),a5) % 0.28/0.53 %EqnAxiom % 0.28/0.53 % 0.28/0.53 %------------------------------------------- % 0.28/0.53 cnf(12,plain, % 0.28/0.53 (~P4(a2,a4,a1,a6)), % 0.28/0.53 inference(scs_inference,[],[1,4,2,3,8,5])). % 0.28/0.53 cnf(13,plain, % 0.28/0.53 ($false), % 0.28/0.53 inference(scs_inference,[],[1,12,4,9]), % 0.28/0.53 ['proof']). % 0.28/0.53 % SZS output end Proof % 0.28/0.53 % Total time :0.004572s %------------------------------------------------------------------------------