%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT026-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n028.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 : Unsatisfiable 1.22s 1.46s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT026-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.09/0.35 % Computer : n028.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 12:14:46 UTC 2026 % 0.09/0.35 % CPUTime : % 0.23/0.52 start to proof:theBenchmark % 1.22/1.45 %------------------------------------------- % 1.22/1.45 % File :CSE---1.7 % 1.22/1.45 % Problem :theBenchmark % 1.22/1.45 % Transform :cnf % 1.22/1.45 % Format :tptp:raw % 1.22/1.45 % Command :java -jar mcs_scs.jar %d %s % 1.22/1.45 % 1.22/1.45 % Result :Theorem 0.956374s % 1.22/1.45 % Output :CNFRefutation 0.956374s % 1.22/1.45 %------------------------------------------- % 1.22/1.45 %-------------------------------------------------------------------------- % 1.22/1.45 % File : MGT026-1 : TPTP v9.3.0. Released v2.4.0. % 1.22/1.45 % Domain : Management (Organisation Theory) % 1.22/1.45 % Problem : Selection favors efficient producers past the critical point % 1.22/1.45 % Version : [PB+94] axioms : Reduced & Augmented > Complete. % 1.22/1.45 % English : % 1.22/1.45 % 1.22/1.45 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 1.22/1.45 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 1.22/1.45 % : [Kam95] Kamps (1995), Email to G. Sutcliffe % 1.22/1.45 % Source : [TPTP] % 1.22/1.45 % Names : % 1.22/1.45 % 1.22/1.45 % Status : Unsatisfiable % 1.22/1.45 % Rating : 0.08 v9.3.0, 0.09 v9.1.0, 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.4.0, 0.15 v5.3.0, 0.11 v5.2.0, 0.06 v5.0.0, 0.07 v4.1.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.14 v3.2.0, 0.15 v3.1.0, 0.18 v2.7.0, 0.17 v2.6.0, 0.11 v2.5.0, 0.22 v2.4.0 % 1.22/1.45 % Syntax : Number of clauses : 18 ( 4 unt; 1 nHn; 18 RR) % 1.22/1.45 % Number of literals : 52 ( 5 equ; 35 neg) % 1.22/1.45 % Maximal clause size : 6 ( 2 avg) % 1.22/1.45 % Maximal term depth : 2 ( 1 avg) % 1.22/1.45 % Number of predicates : 8 ( 7 usr; 0 prp; 1-4 aty) % 1.22/1.45 % Number of functors : 9 ( 9 usr; 5 con; 0-2 aty) % 1.22/1.45 % Number of variables : 33 ( 0 sgn) % 1.22/1.45 % SPC : CNF_UNS_RFO_SEQ_NHN % 1.22/1.45 % 1.22/1.45 % Comments : Created with tptp2X -f tptp -t clausify:otter MGT026+1.p % 1.22/1.45 %-------------------------------------------------------------------------- % 1.22/1.45 cnf(mp1_high_growth_rates_28,axiom, % 1.22/1.45 ( ~ environment(A) % 1.22/1.45 | ~ subpopulations(B,C,A,D) % 1.22/1.45 | ~ greater(growth_rate(C,D),growth_rate(B,D)) % 1.22/1.45 | selection_favors(C,B,D) ) ). % 1.22/1.45 % 1.22/1.45 cnf(mp2_favour_members_29,axiom, % 1.22/1.45 ( ~ environment(A) % 1.22/1.45 | ~ subpopulation(B,A,C) % 1.22/1.45 | ~ subpopulation(D,A,C) % 1.22/1.45 | ~ greater(cardinality_at_time(B,C),zero) % 1.22/1.45 | cardinality_at_time(D,C) != zero % 1.22/1.45 | selection_favors(B,D,C) ) ). % 1.22/1.45 % 1.22/1.45 cnf(mp_non_empty_fm_and_ep_30,axiom, % 1.22/1.45 ( ~ environment(A) % 1.22/1.45 | ~ in_environment(A,B) % 1.22/1.45 | ~ greater(cardinality_at_time(first_movers,B),zero) % 1.22/1.46 | ~ greater(cardinality_at_time(efficient_producers,B),zero) % 1.22/1.46 | subpopulations(first_movers,efficient_producers,A,B) ) ). % 1.22/1.46 % 1.22/1.46 cnf(mp_first_movers_exist_31,axiom, % 1.22/1.46 ( ~ environment(A) % 1.22/1.46 | ~ in_environment(A,B) % 1.22/1.46 | greater_or_equal(cardinality_at_time(first_movers,B),zero) ) ). % 1.22/1.46 % 1.22/1.46 cnf(mp_subpopulations_32,axiom, % 1.22/1.46 ( ~ environment(A) % 1.22/1.46 | ~ in_environment(A,B) % 1.22/1.46 | subpopulation(first_movers,A,B) ) ). % 1.22/1.46 % 1.22/1.46 cnf(mp_subpopulations_33,axiom, % 1.22/1.46 ( ~ environment(A) % 1.22/1.46 | ~ in_environment(A,B) % 1.22/1.46 | subpopulation(efficient_producers,A,B) ) ). % 1.22/1.46 % 1.22/1.46 cnf(mp_critical_point_after_EP_34,axiom, % 1.22/1.46 ( ~ environment(A) % 1.22/1.46 | greater_or_equal(critical_point(A),appear(efficient_producers,A)) ) ). % 1.22/1.46 % 1.22/1.46 cnf(mp_greater_transitivity_35,axiom, % 1.22/1.46 ( ~ greater(A,B) % 1.22/1.46 | ~ greater(B,C) % 1.22/1.46 | greater(A,C) ) ). % 1.22/1.46 % 1.22/1.46 cnf(mp_greater_or_equal_36,axiom, % 1.22/1.46 ( ~ greater_or_equal(A,B) % 1.22/1.46 | greater(A,B) % 1.22/1.46 | A = B ) ). % 1.22/1.46 % 1.22/1.46 cnf(mp_greater_or_equal_37,axiom, % 1.22/1.46 ( ~ greater(A,B) % 1.22/1.46 | greater_or_equal(A,B) ) ). % 1.22/1.46 % 1.22/1.46 cnf(mp_greater_or_equal_38,axiom, % 1.22/1.46 ( A != B % 1.22/1.46 | greater_or_equal(A,B) ) ). % 1.22/1.46 % 1.22/1.46 cnf(d1_39,hypothesis, % 1.22/1.46 ( ~ environment(A) % 1.22/1.46 | B != critical_point(A) % 1.22/1.46 | ~ greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B)) ) ). % 1.22/1.46 % 1.22/1.46 cnf(d1_40,hypothesis, % 1.22/1.46 ( ~ environment(A) % 1.22/1.46 | B != critical_point(A) % 1.22/1.46 | ~ subpopulations(first_movers,efficient_producers,A,C) % 1.22/1.46 | ~ greater(C,B) % 1.22/1.46 | greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C)) ) ). % 1.22/1.46 % 1.22/1.46 cnf(t6_41,hypothesis, % 1.22/1.46 ( ~ environment(A) % 1.22/1.46 | ~ in_environment(A,B) % 1.22/1.46 | ~ greater_or_equal(B,appear(efficient_producers,A)) % 1.22/1.46 | greater(cardinality_at_time(efficient_producers,B),zero) ) ). % 1.22/1.46 % 1.22/1.46 cnf(prove_l8_42,negated_conjecture, % 1.22/1.46 environment(sk1) ). % 1.22/1.46 % 1.22/1.46 cnf(prove_l8_43,negated_conjecture, % 1.22/1.46 in_environment(sk1,sk2) ). % 1.22/1.46 % 1.22/1.46 cnf(prove_l8_44,negated_conjecture, % 1.22/1.46 greater(sk2,critical_point(sk1)) ). % 1.22/1.46 % 1.22/1.46 cnf(prove_l8_45,negated_conjecture, % 1.22/1.46 ~ selection_favors(efficient_producers,first_movers,sk2) ). % 1.22/1.46 % 1.22/1.46 %-------------------------------------------------------------------------- % 1.22/1.46 %------------------------------------------- % 1.22/1.46 % Proof found % 1.22/1.46 % SZS status Theorem for theBenchmark % 1.22/1.46 % SZS output start Proof % 1.22/1.46 %ClaNum:45(EqnAxiom:27) % 1.22/1.46 %VarNum:90(SingletonVarNum:33) % 1.22/1.46 %MaxLitNum:6 % 1.22/1.46 %MaxfuncDepth:1 % 1.22/1.46 %SharedTerms:10 % 1.22/1.46 %goalClause: 28 29 30 31 % 1.22/1.46 %singleGoalClaCount:4 % 1.22/1.46 [28]P1(a1) % 1.22/1.46 [29]P2(a1,a8) % 1.22/1.46 [31]~P5(a5,a6,a8) % 1.22/1.46 [30]P3(a8,f2(a1)) % 1.22/1.46 [35]~P1(x351)+P4(f2(x351),f3(a5,x351)) % 1.22/1.46 [32]~E(x321,x322)+P4(x321,x322) % 1.22/1.46 [33]~P3(x331,x332)+P4(x331,x332) % 1.22/1.46 [34]P3(x341,x342)+~P4(x341,x342)+E(x341,x342) % 1.22/1.46 [38]~P1(x381)+~P2(x381,x382)+P6(a6,x381,x382) % 1.22/1.46 [39]~P1(x391)+~P2(x391,x392)+P6(a5,x391,x392) % 1.22/1.46 [37]~P2(x372,x371)+~P1(x372)+P4(f4(a6,x371),a9) % 1.22/1.46 [40]~P1(x402)+~E(x401,f2(x402))+~P3(f7(a5,x401),f7(a6,x401)) % 1.22/1.46 [36]~P3(x361,x363)+P3(x361,x362)+~P3(x363,x362) % 1.22/1.46 [41]~P2(x412,x411)+~P1(x412)+~P4(x411,f3(a5,x412))+P3(f4(a5,x411),a9) % 1.22/1.46 [45]~P7(x452,x451,x454,x453)+P5(x451,x452,x453)+~P1(x454)+~P3(f7(x451,x453),f7(x452,x453)) % 1.22/1.46 [43]~P1(x431)+~P2(x431,x432)+P7(a6,a5,x431,x432)+~P3(f4(a6,x432),a9)+~P3(f4(a5,x432),a9) % 1.22/1.46 [44]~P1(x443)+~P3(x441,x442)+~P7(a6,a5,x443,x441)+~E(x442,f2(x443))+P3(f7(a5,x441),f7(a6,x441)) % 1.22/1.46 [42]~P6(x422,x424,x423)+~P6(x421,x424,x423)+P5(x421,x422,x423)+~P1(x424)+~E(f4(x422,x423),a9)+~P3(f4(x421,x423),a9) % 1.22/1.46 %EqnAxiom % 1.22/1.46 [1]E(x11,x11) % 1.22/1.46 [2]E(x22,x21)+~E(x21,x22) % 1.22/1.46 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.22/1.46 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 1.22/1.46 [5]~E(x51,x52)+E(f7(x51,x53),f7(x52,x53)) % 1.22/1.46 [6]~E(x61,x62)+E(f7(x63,x61),f7(x63,x62)) % 1.22/1.46 [7]~E(x71,x72)+E(f3(x71,x73),f3(x72,x73)) % 1.22/1.46 [8]~E(x81,x82)+E(f3(x83,x81),f3(x83,x82)) % 1.22/1.46 [9]~E(x91,x92)+E(f4(x91,x93),f4(x92,x93)) % 1.22/1.46 [10]~E(x101,x102)+E(f4(x103,x101),f4(x103,x102)) % 1.22/1.46 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 1.22/1.46 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123) % 1.22/1.46 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131) % 1.22/1.46 [14]P3(x142,x143)+~E(x141,x142)+~P3(x141,x143) % 1.22/1.46 [15]P3(x153,x152)+~E(x151,x152)+~P3(x153,x151) % 1.22/1.46 [16]P5(x162,x163,x164)+~E(x161,x162)+~P5(x161,x163,x164) % 1.22/1.46 [17]P5(x173,x172,x174)+~E(x171,x172)+~P5(x173,x171,x174) % 1.22/1.46 [18]P5(x183,x184,x182)+~E(x181,x182)+~P5(x183,x184,x181) % 1.22/1.46 [19]P4(x192,x193)+~E(x191,x192)+~P4(x191,x193) % 1.22/1.46 [20]P4(x203,x202)+~E(x201,x202)+~P4(x203,x201) % 1.22/1.46 [21]P7(x212,x213,x214,x215)+~E(x211,x212)+~P7(x211,x213,x214,x215) % 1.22/1.46 [22]P7(x223,x222,x224,x225)+~E(x221,x222)+~P7(x223,x221,x224,x225) % 1.22/1.46 [23]P7(x233,x234,x232,x235)+~E(x231,x232)+~P7(x233,x234,x231,x235) % 1.22/1.46 [24]P7(x243,x244,x245,x242)+~E(x241,x242)+~P7(x243,x244,x245,x241) % 1.22/1.46 [25]P6(x252,x253,x254)+~E(x251,x252)+~P6(x251,x253,x254) % 1.22/1.46 [26]P6(x263,x262,x264)+~E(x261,x262)+~P6(x263,x261,x264) % 1.22/1.46 [27]P6(x273,x274,x272)+~E(x271,x272)+~P6(x273,x274,x271) % 1.22/1.46 % 1.22/1.46 %------------------------------------------- % 1.22/1.46 cnf(48,plain, % 1.22/1.46 (~P1(x481)+~P3(x482,f2(x481))+~P7(a6,a5,x481,x482)+P3(f7(a5,x482),f7(a6,x482))), % 1.22/1.46 inference(equality_inference,[],[44])). % 1.22/1.46 cnf(63,plain, % 1.22/1.46 (P4(x631,f2(a1))+~E(a8,x631)), % 1.22/1.46 inference(scs_inference,[],[30,33,19])). % 1.22/1.46 cnf(64,plain, % 1.22/1.46 (P4(a8,f2(a1))), % 1.22/1.46 inference(equality_inference,[],[63])). % 1.22/1.46 cnf(72,plain, % 1.22/1.46 (~E(a1,x721)+P4(f2(x721),f3(a5,x721))), % 1.22/1.46 inference(scs_inference,[],[28,35,11])). % 1.22/1.46 cnf(73,plain, % 1.22/1.46 (P4(f2(a1),f3(a5,a1))), % 1.22/1.46 inference(equality_inference,[],[72])). % 1.22/1.46 cnf(76,plain, % 1.22/1.46 (P4(a8,f3(a5,a1))+P3(f2(a1),f3(a5,a1))), % 1.22/1.46 inference(scs_inference,[],[73,64,34,20])). % 1.22/1.46 cnf(99,plain, % 1.22/1.46 (P3(a8,f3(a5,a1))+P4(a8,f3(a5,a1))), % 1.22/1.46 inference(scs_inference,[],[30,76,36])). % 1.22/1.46 cnf(100,plain, % 1.22/1.46 (P4(a8,f3(a5,a1))), % 1.22/1.46 inference(scs_inference,[],[99,33])). % 1.22/1.46 cnf(143,plain, % 1.22/1.46 (P6(a6,a1,a8)), % 1.22/1.46 inference(scs_inference,[],[29,28,38,11])). % 1.22/1.46 cnf(150,plain, % 1.22/1.46 (P6(a5,a1,a8)), % 1.22/1.46 inference(scs_inference,[],[29,28,39,11])). % 1.22/1.46 cnf(157,plain, % 1.22/1.46 (P4(f4(a6,a8),a9)), % 1.22/1.46 inference(scs_inference,[],[29,28,37,11])). % 1.22/1.46 cnf(158,plain, % 1.22/1.46 (E(f4(a6,a8),a9)+P3(f4(a6,a8),a9)), % 1.22/1.46 inference(scs_inference,[],[157,34])). % 1.22/1.46 cnf(257,plain, % 1.22/1.46 (~E(x2571,a1)+P1(x2571)), % 1.22/1.46 inference(scs_inference,[],[28,2,11])). % 1.22/1.46 cnf(259,plain, % 1.22/1.46 (~E(f4(a6,a8),a9)+~P3(f4(a5,a8),a9)), % 1.22/1.46 inference(scs_inference,[],[31,143,150,257,42])). % 1.22/1.46 cnf(260,plain, % 1.22/1.46 (~E(f4(a6,a8),a9)), % 1.22/1.46 inference(scs_inference,[],[100,28,29,259,41])). % 1.22/1.46 cnf(261,plain, % 1.22/1.46 (P3(f4(a6,a8),a9)), % 1.22/1.46 inference(scs_inference,[],[260,158])). % 1.22/1.46 cnf(286,plain, % 1.22/1.46 (P7(a6,a5,a1,a8)), % 1.22/1.46 inference(scs_inference,[],[29,28,100,261,43,41])). % 1.22/1.46 cnf(287,plain, % 1.22/1.46 (P3(f7(a5,a8),f7(a6,a8))), % 1.22/1.46 inference(scs_inference,[],[30,28,286,48])). % 1.22/1.46 cnf(306,plain, % 1.22/1.46 ($false), % 1.22/1.46 inference(scs_inference,[],[31,28,287,286,45]), % 1.22/1.46 ['proof']). % 1.22/1.46 % SZS output end Proof % 1.22/1.46 % Total time :0.956374s %------------------------------------------------------------------------------