%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT039-1 : 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 : n016.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 1.46s 1.60s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT039-1 : 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.09/0.36 % Computer : n016.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 12:59:02 UTC 2026 % 0.13/0.36 % CPUTime : % 0.24/0.53 start to proof:theBenchmark % 1.35/1.59 %------------------------------------------- % 1.35/1.59 % File :CSE---1.7 % 1.35/1.59 % Problem :theBenchmark % 1.35/1.59 % Transform :cnf % 1.35/1.59 % Format :tptp:raw % 1.35/1.59 % Command :java -jar mcs_scs.jar %d %s % 1.35/1.59 % 1.35/1.59 % Result :Theorem 1.082557s % 1.35/1.59 % Output :CNFRefutation 1.082557s % 1.35/1.59 %------------------------------------------- % 1.35/1.60 %-------------------------------------------------------------------------- % 1.35/1.60 % File : MGT039-1 : TPTP v9.3.0. Released v2.4.0. % 1.35/1.60 % Domain : Management (Organisation Theory) % 1.35/1.60 % Problem : Selection favours EPs above Fms if change is slow % 1.35/1.60 % Version : [PB+94] axioms : Reduced & Augmented > Complete. % 1.35/1.60 % English : Selection favors efficient producers above first movers if % 1.35/1.60 % environmental change is slow. % 1.35/1.60 % 1.35/1.60 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 1.35/1.60 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 1.35/1.60 % : [Kam95] Kamps (1995), Email to G. Sutcliffe % 1.35/1.60 % Source : [TPTP] % 1.35/1.60 % Names : % 1.35/1.60 % 1.35/1.60 % Status : Unsatisfiable % 1.35/1.60 % Rating : 0.08 v9.3.0, 0.05 v9.0.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.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.05 v5.4.0, 0.10 v5.3.0, 0.06 v5.2.0, 0.00 v4.0.1, 0.09 v4.0.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.35/1.60 % Syntax : Number of clauses : 19 ( 5 unt; 4 nHn; 19 RR) % 1.35/1.60 % Number of literals : 57 ( 2 equ; 35 neg) % 1.35/1.60 % Maximal clause size : 5 ( 3 avg) % 1.35/1.60 % Maximal term depth : 3 ( 1 avg) % 1.35/1.60 % Number of predicates : 9 ( 8 usr; 0 prp; 1-3 aty) % 1.46/1.60 % Number of functors : 8 ( 8 usr; 3 con; 0-2 aty) % 1.46/1.60 % Number of variables : 25 ( 0 sgn) % 1.46/1.60 % SPC : CNF_UNS_RFO_SEQ_NHN % 1.46/1.60 % 1.46/1.60 % Comments : Created with tptp2X -f tptp -t clausify:otter MGT039+1.p % 1.46/1.60 %-------------------------------------------------------------------------- % 1.46/1.60 cnf(mp3_favoured_trategy_20,axiom, % 1.46/1.60 ( ~ observational_period(A) % 1.46/1.60 | ~ propagation_strategy(first_movers) % 1.46/1.60 | ~ propagation_strategy(efficient_producers) % 1.46/1.60 | environment(sk1(A)) % 1.46/1.60 | selection_favors(efficient_producers,first_movers,A) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp3_favoured_trategy_21,axiom, % 1.46/1.60 ( ~ observational_period(A) % 1.46/1.60 | ~ propagation_strategy(first_movers) % 1.46/1.60 | ~ propagation_strategy(efficient_producers) % 1.46/1.60 | in_environment(A,sk1(A)) % 1.46/1.60 | selection_favors(efficient_producers,first_movers,A) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp3_favoured_trategy_22,axiom, % 1.46/1.60 ( ~ observational_period(A) % 1.46/1.60 | ~ propagation_strategy(first_movers) % 1.46/1.60 | ~ propagation_strategy(efficient_producers) % 1.46/1.60 | ~ selection_favors(efficient_producers,first_movers,end_time(sk1(A))) % 1.46/1.60 | selection_favors(efficient_producers,first_movers,A) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp4_critical_point_23,axiom, % 1.46/1.60 ( ~ observational_period(A) % 1.46/1.60 | ~ slow_change(A) % 1.46/1.60 | ~ environment(B) % 1.46/1.60 | ~ in_environment(A,B) % 1.46/1.60 | in_environment(B,sk2(B,A)) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp4_critical_point_24,axiom, % 1.46/1.60 ( ~ observational_period(A) % 1.46/1.60 | ~ slow_change(A) % 1.46/1.60 | ~ environment(B) % 1.46/1.60 | ~ in_environment(A,B) % 1.46/1.60 | greater(sk2(B,A),critical_point(B)) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp_organizational_sets1_25,axiom, % 1.46/1.60 propagation_strategy(first_movers) ). % 1.46/1.60 % 1.46/1.60 cnf(mp_organizational_sets2_26,axiom, % 1.46/1.60 propagation_strategy(efficient_producers) ). % 1.46/1.60 % 1.46/1.60 cnf(mp_time_in_environment_27,axiom, % 1.46/1.60 ( ~ environment(A) % 1.46/1.60 | ~ greater_or_equal(B,start_time(A)) % 1.46/1.60 | ~ greater_or_equal(end_time(A),B) % 1.46/1.60 | in_environment(A,B) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp_environment_end_point_28,axiom, % 1.46/1.60 ( ~ environment(A) % 1.46/1.60 | ~ in_environment(A,B) % 1.46/1.60 | greater_or_equal(end_time(A),B) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp_time_of_critical_point_29,axiom, % 1.46/1.60 ( ~ environment(A) % 1.46/1.60 | greater_or_equal(critical_point(A),start_time(A)) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp_greater_transitivity_30,axiom, % 1.46/1.60 ( ~ greater(A,B) % 1.46/1.60 | ~ greater(B,C) % 1.46/1.60 | greater(A,C) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp_greater_or_equal_31,axiom, % 1.46/1.60 ( ~ greater_or_equal(A,B) % 1.46/1.60 | greater(A,B) % 1.46/1.60 | A = B ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp_greater_or_equal_32,axiom, % 1.46/1.60 ( ~ greater(A,B) % 1.46/1.60 | greater_or_equal(A,B) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp_greater_or_equal_33,axiom, % 1.46/1.60 ( A != B % 1.46/1.60 | greater_or_equal(A,B) ) ). % 1.46/1.60 % 1.46/1.60 cnf(mp_beginning_and_ending_34,axiom, % 1.46/1.60 ( ~ environment(A) % 1.46/1.60 | ~ greater(B,start_time(A)) % 1.46/1.60 | greater(B,end_time(A)) % 1.46/1.60 | greater_or_equal(end_time(A),B) ) ). % 1.46/1.60 % 1.46/1.60 cnf(l8_35,hypothesis, % 1.46/1.60 ( ~ environment(A) % 1.46/1.60 | ~ in_environment(A,B) % 1.46/1.60 | ~ greater(B,critical_point(A)) % 1.46/1.60 | selection_favors(efficient_producers,first_movers,B) ) ). % 1.46/1.60 % 1.46/1.60 cnf(prove_t8_36,negated_conjecture, % 1.46/1.60 observational_period(sk3) ). % 1.46/1.60 % 1.46/1.60 cnf(prove_t8_37,negated_conjecture, % 1.46/1.60 slow_change(sk3) ). % 1.46/1.60 % 1.46/1.60 cnf(prove_t8_38,negated_conjecture, % 1.46/1.60 ~ selection_favors(efficient_producers,first_movers,sk3) ). % 1.46/1.60 % 1.46/1.60 %-------------------------------------------------------------------------- % 1.46/1.60 %------------------------------------------- % 1.46/1.60 % Proof found % 1.46/1.60 % SZS status Theorem for theBenchmark % 1.46/1.60 % SZS output start Proof % 1.46/1.60 %ClaNum:41(EqnAxiom:22) % 1.46/1.60 %VarNum:74(SingletonVarNum:25) % 1.46/1.60 %MaxLitNum:5 % 1.46/1.60 %MaxfuncDepth:2 % 1.46/1.60 %SharedTerms:10 % 1.46/1.60 %goalClause: 23 26 27 % 1.46/1.60 %singleGoalClaCount:3 % 1.46/1.60 [23]P1(a1) % 1.46/1.60 [24]P6(a2) % 1.46/1.60 [25]P6(a3) % 1.46/1.60 [26]P7(a1) % 1.46/1.60 [27]~P8(a3,a2,a1) % 1.46/1.60 [29]~P3(x291)+P2(f4(x291),f8(x291)) % 1.46/1.60 [28]~E(x281,x282)+P2(x281,x282) % 1.46/1.60 [30]~P4(x301,x302)+P2(x301,x302) % 1.46/1.60 [31]P4(x311,x312)+~P2(x311,x312)+E(x311,x312) % 1.46/1.60 [32]~P3(x321)+~P5(x321,x322)+P2(f5(x321),x322) % 1.46/1.60 [33]~P4(x331,x333)+P4(x331,x332)+~P4(x333,x332) % 1.46/1.60 [35]~P3(x352)+~P4(x351,f8(x352))+P4(x351,f5(x352))+P2(f5(x352),x351) % 1.46/1.60 [37]~P3(x371)+P5(x371,x372)+~P2(x372,f8(x371))+~P2(f5(x371),x372) % 1.46/1.60 [40]~P5(x402,x401)+~P3(x402)+~P4(x401,f4(x402))+P8(a3,a2,x401) % 1.46/1.60 [34]~P1(x341)+P8(a3,a2,x341)+P3(f6(x341))+~P6(a2)+~P6(a3) % 1.46/1.60 [38]~P1(x381)+P5(x381,f6(x381))+P8(a3,a2,x381)+~P6(a2)+~P6(a3) % 1.46/1.60 [41]~P1(x411)+P8(a3,a2,x411)+~P6(a2)+~P6(a3)+~P8(a3,a2,f5(f6(x411))) % 1.46/1.60 [36]~P1(x362)+~P3(x361)+~P7(x362)+~P5(x362,x361)+P5(x361,f7(x361,x362)) % 1.46/1.61 [39]~P1(x392)+~P3(x391)+~P7(x392)+~P5(x392,x391)+P4(f7(x391,x392),f4(x391)) % 1.46/1.61 %EqnAxiom % 1.46/1.61 [1]E(x11,x11) % 1.46/1.61 [2]E(x22,x21)+~E(x21,x22) % 1.46/1.61 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.46/1.61 [4]~E(x41,x42)+E(f4(x41),f4(x42)) % 1.46/1.61 [5]~E(x51,x52)+E(f8(x51),f8(x52)) % 1.46/1.61 [6]~E(x61,x62)+E(f5(x61),f5(x62)) % 1.46/1.61 [7]~E(x71,x72)+E(f6(x71),f6(x72)) % 1.46/1.61 [8]~E(x81,x82)+E(f7(x81,x83),f7(x82,x83)) % 1.46/1.61 [9]~E(x91,x92)+E(f7(x93,x91),f7(x93,x92)) % 1.46/1.61 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 1.46/1.61 [11]~P6(x111)+P6(x112)+~E(x111,x112) % 1.46/1.61 [12]P4(x122,x123)+~E(x121,x122)+~P4(x121,x123) % 1.46/1.61 [13]P4(x133,x132)+~E(x131,x132)+~P4(x133,x131) % 1.46/1.61 [14]~P7(x141)+P7(x142)+~E(x141,x142) % 1.46/1.61 [15]P8(x152,x153,x154)+~E(x151,x152)+~P8(x151,x153,x154) % 1.46/1.61 [16]P8(x163,x162,x164)+~E(x161,x162)+~P8(x163,x161,x164) % 1.46/1.61 [17]P8(x173,x174,x172)+~E(x171,x172)+~P8(x173,x174,x171) % 1.46/1.61 [18]P2(x182,x183)+~E(x181,x182)+~P2(x181,x183) % 1.46/1.61 [19]P2(x193,x192)+~E(x191,x192)+~P2(x193,x191) % 1.46/1.61 [20]P5(x202,x203)+~E(x201,x202)+~P5(x201,x203) % 1.46/1.61 [21]P5(x213,x212)+~E(x211,x212)+~P5(x213,x211) % 1.46/1.61 [22]~P3(x221)+P3(x222)+~E(x221,x222) % 1.46/1.61 % 1.46/1.61 %------------------------------------------- % 1.46/1.61 cnf(42,plain, % 1.46/1.61 (P2(x421,x421)), % 1.46/1.61 inference(equality_inference,[],[28])). % 1.46/1.61 cnf(43,plain, % 1.46/1.61 (P5(a1,f6(a1))), % 1.46/1.61 inference(scs_inference,[],[23,27,24,25,38])). % 1.46/1.61 cnf(50,plain, % 1.46/1.61 (~P1(x501)+P8(a3,a2,x501)+P3(f6(x501))), % 1.46/1.61 inference(scs_inference,[],[24,25,34])). % 1.46/1.61 cnf(52,plain, % 1.46/1.61 (~P1(x521)+P8(a3,a2,x521)+~P8(a3,a2,f5(f6(x521)))), % 1.46/1.61 inference(scs_inference,[],[24,25,41])). % 1.46/1.61 cnf(53,plain, % 1.46/1.61 (P3(f6(a1))), % 1.46/1.61 inference(scs_inference,[],[23,27,50])). % 1.46/1.61 cnf(55,plain, % 1.46/1.61 (~P8(a3,a2,f5(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[23,27,50,52])). % 1.46/1.61 cnf(71,plain, % 1.46/1.61 (P2(f4(f6(a1)),f8(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[27,23,29,50])). % 1.46/1.61 cnf(72,plain, % 1.46/1.61 (E(f4(f6(a1)),f8(f6(a1)))+P4(f4(f6(a1)),f8(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[71,31])). % 1.46/1.61 cnf(119,plain, % 1.46/1.61 (~E(x1191,a1)+~P1(a1)+P1(x1191)), % 1.46/1.61 inference(scs_inference,[],[23,10,2])). % 1.46/1.61 cnf(121,plain, % 1.46/1.61 (P1(x1211)+~E(x1211,a1)), % 1.46/1.61 inference(scs_inference,[],[23,119])). % 1.46/1.61 cnf(140,plain, % 1.46/1.61 (P4(x1401,f5(f6(a1)))+P2(f5(f6(a1)),x1401)+~P4(x1401,f8(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[27,23,35,50])). % 1.46/1.61 cnf(141,plain, % 1.46/1.61 (P5(f6(a1),f5(f6(a1)))+~P4(f8(f6(a1)),f8(f6(a1)))+P4(f8(f6(a1)),f5(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[42,53,140,37])). % 1.46/1.61 cnf(142,plain, % 1.46/1.61 (P5(f6(a1),f7(f6(a1),a1))), % 1.46/1.61 inference(scs_inference,[],[26,43,53,121,36])). % 1.46/1.61 cnf(144,plain, % 1.46/1.61 (P5(f6(a1),x1441)+~E(f7(f6(a1),a1),x1441)), % 1.46/1.61 inference(scs_inference,[],[142,20,21])). % 1.46/1.61 cnf(153,plain, % 1.46/1.61 (P4(f7(f6(a1),a1),f4(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[26,43,53,121,39])). % 1.46/1.61 cnf(163,plain, % 1.46/1.61 (~E(f7(f6(a1),a1),f5(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[55,153,53,12,40,144])). % 1.46/1.61 cnf(186,plain, % 1.46/1.61 (~E(x1861,x1862)+E(f6(x1862),f6(x1861))), % 1.46/1.61 inference(scs_inference,[],[2,7])). % 1.46/1.61 cnf(188,plain, % 1.46/1.61 (E(f7(x1881,x1882),f7(x1883,x1882))+~E(x1883,x1881)), % 1.46/1.61 inference(scs_inference,[],[2,8])). % 1.46/1.61 cnf(204,plain, % 1.46/1.61 (~E(x2041,f7(f6(a1),a1))+~E(f5(f6(a1)),x2041)), % 1.46/1.61 inference(scs_inference,[],[163,2,3])). % 1.46/1.61 cnf(205,plain, % 1.46/1.61 (~E(f6(a1),x2051)+~E(f5(f6(a1)),f7(x2051,a1))), % 1.46/1.61 inference(scs_inference,[],[204,188])). % 1.46/1.61 cnf(206,plain, % 1.46/1.61 (~E(f7(x2061,a1),f5(f6(a1)))+~E(f6(a1),x2061)), % 1.46/1.61 inference(scs_inference,[],[205,2])). % 1.46/1.61 cnf(207,plain, % 1.46/1.61 (~E(x2071,a1)+~E(f7(f6(x2071),a1),f5(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[206,186])). % 1.46/1.61 cnf(208,plain, % 1.46/1.61 (~E(f5(f6(a1)),f7(f6(x2081),a1))+~E(x2081,a1)), % 1.46/1.61 inference(scs_inference,[],[207,2])). % 1.46/1.61 cnf(209,plain, % 1.46/1.61 (~P2(f5(f6(a1)),f7(f6(x2091),a1))+P4(f5(f6(a1)),f7(f6(x2091),a1))+~E(x2091,a1)), % 1.46/1.61 inference(scs_inference,[],[208,31])). % 1.46/1.61 cnf(210,plain, % 1.46/1.61 (P4(f5(f6(a1)),f7(f6(a1),a1))+~P2(f5(f6(a1)),f7(f6(a1),a1))), % 1.46/1.61 inference(equality_inference,[],[209])). % 1.46/1.61 cnf(211,plain, % 1.46/1.61 (P4(f5(f6(a1)),f7(f6(a1),a1))), % 1.46/1.61 inference(scs_inference,[],[142,53,210,32])). % 1.46/1.61 cnf(212,plain, % 1.46/1.61 (P4(f5(f6(a1)),f4(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[153,211,33])). % 1.46/1.61 cnf(214,plain, % 1.46/1.61 (~P5(f6(a1),f5(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[153,55,53,211,33,40])). % 1.46/1.61 cnf(218,plain, % 1.46/1.61 (P4(f5(f6(a1)),x2181)+~E(f7(f6(a1),a1),x2181)), % 1.46/1.61 inference(scs_inference,[],[153,55,53,211,33,40,141,12,13])). % 1.46/1.61 cnf(371,plain, % 1.46/1.61 (~P4(f5(f6(a1)),f8(f6(a1)))), % 1.46/1.61 inference(scs_inference,[],[42,214,53,30,37])). % 1.46/1.61 cnf(375,plain, % 1.46/1.61 ($false), % 1.46/1.61 inference(scs_inference,[],[212,371,218,13,72,33]), % 1.46/1.61 ['proof']). % 1.46/1.61 % SZS output end Proof % 1.46/1.61 % Total time :1.082557s %------------------------------------------------------------------------------