%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT021-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 : 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:16 AM UTC 2026 % Result : Unsatisfiable 0.24s 0.56s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT021-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.08/0.34 % Computer : n028.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.34 % WCLimit : 300 % 0.08/0.34 % DateTime : Mon Sep 7 12:05:32 UTC 2026 % 0.08/0.34 % CPUTime : % 0.24/0.51 start to proof:theBenchmark % 0.24/0.55 %------------------------------------------- % 0.24/0.55 % File :CSE---1.7 % 0.24/0.55 % Problem :theBenchmark % 0.24/0.55 % Transform :cnf % 0.24/0.55 % Format :tptp:raw % 0.24/0.55 % Command :java -jar mcs_scs.jar %d %s % 0.24/0.55 % 0.24/0.55 % Result :Theorem 0.047714s % 0.24/0.55 % Output :CNFRefutation 0.047714s % 0.24/0.55 %------------------------------------------- % 0.24/0.55 %-------------------------------------------------------------------------- % 0.24/0.55 % File : MGT021-1 : TPTP v9.3.0. Released v2.4.0. % 0.24/0.55 % Domain : Management (Organisation Theory) % 0.24/0.55 % Problem : Difference between disbanding rates does not decrease % 0.24/0.55 % Version : [PB+94] axioms. % 0.24/0.55 % English : The difference between the disbanding rates of first movers % 0.24/0.55 % and efficient producers does not decrease with time. % 0.24/0.55 % 0.24/0.55 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 0.24/0.55 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 0.24/0.55 % : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing % 0.24/0.55 % : [Kam95] Kamps (1995), Email to G. Sutcliffe % 0.24/0.55 % Source : [TPTP] % 0.24/0.55 % Names : % 0.24/0.55 % 0.24/0.55 % Status : Unsatisfiable % 0.24/0.55 % Rating : 0.17 v9.3.0, 0.09 v9.1.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.09 v6.2.0, 0.00 v5.5.0, 0.05 v5.4.0, 0.10 v5.3.0, 0.06 v5.2.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.4.0 % 0.24/0.55 % Syntax : Number of clauses : 11 ( 3 unt; 2 nHn; 11 RR) % 0.24/0.55 % Number of literals : 32 ( 1 equ; 21 neg) % 0.24/0.55 % Maximal clause size : 5 ( 2 avg) % 0.24/0.55 % Maximal term depth : 3 ( 1 avg) % 0.24/0.55 % Number of predicates : 9 ( 8 usr; 0 prp; 1-4 aty) % 0.24/0.55 % Number of functors : 10 ( 10 usr; 5 con; 0-2 aty) % 0.24/0.55 % Number of variables : 15 ( 0 sgn) % 0.24/0.55 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.24/0.55 % 0.24/0.55 % Comments : Same as version with [PM93] axioms. % 0.24/0.55 % : Created with tptp2X -f tptp -t clausify:otter MGT021+1.p % 0.24/0.55 %-------------------------------------------------------------------------- % 0.24/0.55 cnf(mp_time_point_in_environment_27,axiom, % 0.24/0.55 ( ~ environment(A) % 0.24/0.56 | ~ subpopulations(first_movers,efficient_producers,A,B) % 0.24/0.56 | in_environment(A,B) ) ). % 0.24/0.56 % 0.24/0.56 cnf(mp_environment_not_empty_28,axiom, % 0.24/0.56 ( ~ environment(A) % 0.24/0.56 | ~ subpopulations(first_movers,efficient_producers,A,B) % 0.24/0.56 | greater(number_of_organizations(A,B),zero) ) ). % 0.24/0.56 % 0.24/0.56 cnf(mp_increase_not_decrease_29,axiom, % 0.24/0.56 ( ~ increases(A) % 0.24/0.56 | ~ decreases(A) ) ). % 0.24/0.56 % 0.24/0.56 cnf(mp_greater_or_equal_30,axiom, % 0.24/0.56 ( ~ greater_or_equal(A,B) % 0.24/0.56 | greater(A,B) % 0.24/0.56 | A = B ) ). % 0.24/0.56 % 0.24/0.56 cnf(a3_31,hypothesis, % 0.24/0.56 ( ~ environment(A) % 0.24/0.56 | ~ in_environment(A,B) % 0.24/0.56 | ~ greater(number_of_organizations(A,B),zero) % 0.24/0.56 | ~ greater(equilibrium(A),B) % 0.24/0.56 | decreases(resources(A,B)) ) ). % 0.24/0.56 % 0.24/0.56 cnf(a3_32,hypothesis, % 0.24/0.56 ( ~ environment(A) % 0.24/0.56 | ~ in_environment(A,B) % 0.24/0.56 | ~ greater(number_of_organizations(A,B),zero) % 0.24/0.56 | greater(equilibrium(A),B) % 0.24/0.56 | constant(resources(A,B)) ) ). % 0.24/0.56 % 0.24/0.56 cnf(l4_33,hypothesis, % 0.24/0.56 ( ~ environment(A) % 0.24/0.56 | ~ subpopulations(first_movers,efficient_producers,A,B) % 0.24/0.56 | ~ decreases(resources(A,B)) % 0.24/0.56 | increases(difference(disbanding_rate(first_movers,B),disbanding_rate(efficient_producers,B))) ) ). % 0.24/0.56 % 0.24/0.56 cnf(l4_34,hypothesis, % 0.24/0.56 ( ~ environment(A) % 0.24/0.56 | ~ subpopulations(first_movers,efficient_producers,A,B) % 0.24/0.56 | ~ constant(resources(A,B)) % 0.24/0.56 | ~ decreases(difference(disbanding_rate(first_movers,B),disbanding_rate(efficient_producers,B))) ) ). % 0.24/0.56 % 0.24/0.56 cnf(prove_l3_35,negated_conjecture, % 0.24/0.56 environment(sk1) ). % 0.24/0.56 % 0.24/0.56 cnf(prove_l3_36,negated_conjecture, % 0.24/0.56 subpopulations(first_movers,efficient_producers,sk1,sk2) ). % 0.24/0.56 % 0.24/0.56 cnf(prove_l3_37,negated_conjecture, % 0.24/0.56 decreases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))) ). % 0.24/0.56 % 0.24/0.56 %-------------------------------------------------------------------------- % 0.24/0.56 %------------------------------------------- % 0.24/0.56 % Proof found % 0.24/0.56 % SZS status Theorem for theBenchmark % 0.24/0.56 % SZS output start Proof % 0.24/0.56 %ClaNum:37(EqnAxiom:26) % 0.24/0.56 %VarNum:50(SingletonVarNum:15) % 0.24/0.56 %MaxLitNum:5 % 0.24/0.56 %MaxfuncDepth:2 % 0.24/0.56 %SharedTerms:11 % 0.24/0.56 %goalClause: 27 28 29 % 0.24/0.56 %singleGoalClaCount:3 % 0.24/0.56 [27]P1(a1) % 0.24/0.56 [29]P4(a2,a5,a1,a9) % 0.24/0.56 [28]P2(f4(f3(a2,a9),f3(a5,a9))) % 0.24/0.56 [30]~P2(x301)+~P5(x301) % 0.24/0.56 [31]P6(x311,x312)+~P7(x311,x312)+E(x311,x312) % 0.24/0.56 [34]~P1(x341)+P8(x341,x342)+~P4(a2,a5,x341,x342) % 0.24/0.56 [35]~P1(x351)+~P4(a2,a5,x351,x352)+P6(f8(x351,x352),a10) % 0.24/0.56 [36]~P1(x362)+~P4(a2,a5,x362,x361)+~P2(f7(x362,x361))+P5(f4(f3(a2,x361),f3(a5,x361))) % 0.24/0.56 [37]~P1(x371)+~P4(a2,a5,x371,x372)+~P3(f7(x371,x372))+~P2(f4(f3(a2,x372),f3(a5,x372))) % 0.24/0.56 [32]~P1(x321)+~P8(x321,x322)+P6(f6(x321),x322)+~P6(f8(x321,x322),a10)+P3(f7(x321,x322)) % 0.24/0.56 [33]~P1(x331)+~P8(x331,x332)+~P6(f6(x331),x332)+~P6(f8(x331,x332),a10)+P2(f7(x331,x332)) % 0.24/0.56 %EqnAxiom % 0.24/0.56 [1]E(x11,x11) % 0.24/0.56 [2]E(x22,x21)+~E(x21,x22) % 0.24/0.56 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.24/0.56 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43)) % 0.24/0.56 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52)) % 0.24/0.56 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63)) % 0.24/0.56 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72)) % 0.24/0.56 [8]~E(x81,x82)+E(f7(x81,x83),f7(x82,x83)) % 0.24/0.56 [9]~E(x91,x92)+E(f7(x93,x91),f7(x93,x92)) % 0.24/0.56 [10]~E(x101,x102)+E(f8(x101,x103),f8(x102,x103)) % 0.24/0.56 [11]~E(x111,x112)+E(f8(x113,x111),f8(x113,x112)) % 0.24/0.56 [12]~E(x121,x122)+E(f6(x121),f6(x122)) % 0.24/0.56 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 0.24/0.56 [14]~P2(x141)+P2(x142)+~E(x141,x142) % 0.24/0.56 [15]P4(x152,x153,x154,x155)+~E(x151,x152)+~P4(x151,x153,x154,x155) % 0.24/0.56 [16]P4(x163,x162,x164,x165)+~E(x161,x162)+~P4(x163,x161,x164,x165) % 0.24/0.56 [17]P4(x173,x174,x172,x175)+~E(x171,x172)+~P4(x173,x174,x171,x175) % 0.24/0.56 [18]P4(x183,x184,x185,x182)+~E(x181,x182)+~P4(x183,x184,x185,x181) % 0.24/0.56 [19]~P5(x191)+P5(x192)+~E(x191,x192) % 0.24/0.56 [20]P6(x202,x203)+~E(x201,x202)+~P6(x201,x203) % 0.24/0.56 [21]P6(x213,x212)+~E(x211,x212)+~P6(x213,x211) % 0.24/0.56 [22]P8(x222,x223)+~E(x221,x222)+~P8(x221,x223) % 0.24/0.56 [23]P8(x233,x232)+~E(x231,x232)+~P8(x233,x231) % 0.24/0.56 [24]P7(x242,x243)+~E(x241,x242)+~P7(x241,x243) % 0.24/0.56 [25]P7(x253,x252)+~E(x251,x252)+~P7(x253,x251) % 0.24/0.56 [26]~P3(x261)+P3(x262)+~E(x261,x262) % 0.24/0.56 % 0.24/0.56 %------------------------------------------- % 0.24/0.56 cnf(38,plain, % 0.24/0.56 (P8(a1,a9)), % 0.24/0.56 inference(scs_inference,[],[27,29,34])). % 0.24/0.56 cnf(40,plain, % 0.24/0.56 (~P3(f7(a1,a9))), % 0.24/0.56 inference(scs_inference,[],[27,29,28,34,37])). % 0.24/0.56 cnf(54,plain, % 0.24/0.56 (~P2(f7(a1,a9))), % 0.24/0.56 inference(scs_inference,[],[28,29,27,30,36])). % 0.24/0.56 cnf(65,plain, % 0.24/0.56 (~E(x651,a1)+P1(x651)), % 0.24/0.56 inference(scs_inference,[],[27,13,2])). % 0.24/0.56 cnf(84,plain, % 0.24/0.56 (P6(f8(a1,a9),a10)), % 0.24/0.56 inference(scs_inference,[],[29,35,65])). % 0.24/0.56 cnf(87,plain, % 0.24/0.56 ($false), % 0.24/0.56 inference(scs_inference,[],[27,38,84,54,40,32,33]), % 0.24/0.56 ['proof']). % 0.24/0.56 % SZS output end Proof % 0.24/0.56 % Total time :0.047714s %------------------------------------------------------------------------------