%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT039+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/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 10.63s 10.81s % 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.0.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/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:51:26 UTC 2026 % 0.09/0.34 % CPUTime : % 0.12/0.45 start to proof:theBenchmark % 10.52/10.80 %------------------------------------------- % 10.52/10.80 % File :CSE---1.7 % 10.52/10.80 % Problem :theBenchmark % 10.52/10.80 % Transform :cnf % 10.52/10.80 % Format :tptp:raw % 10.52/10.80 % Command :java -jar mcs_scs.jar %d %s % 10.52/10.80 % 10.52/10.80 % Result :Theorem 10.340788s % 10.52/10.80 % Output :CNFRefutation 10.340788s % 10.52/10.80 %------------------------------------------- % 10.63/10.80 %-------------------------------------------------------------------------- % 10.63/10.80 % File : MGT039+1 : TPTP v9.3.0. Released v2.0.0. % 10.63/10.80 % Domain : Management (Organisation Theory) % 10.63/10.80 % Problem : Selection favours EPs above Fms if change is slow % 10.63/10.80 % Version : [PB+94] axioms : Reduced & Augmented > Complete. % 10.63/10.80 % English : Selection favors efficient producers above first movers if % 10.63/10.80 % environmental change is slow. % 10.63/10.80 % 10.63/10.80 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 10.63/10.80 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 10.63/10.80 % : [Kam95] Kamps (1995), Email to G. Sutcliffe % 10.63/10.80 % Source : [Kam95] % 10.63/10.80 % Names : % 10.63/10.80 % 10.63/10.80 % Status : Theorem % 10.63/10.80 % Rating : 0.13 v9.3.0, 0.15 v9.1.0, 0.12 v9.0.0, 0.17 v8.2.0, 0.11 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.3.0, 0.07 v7.2.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.13 v6.0.0, 0.04 v5.3.0, 0.11 v5.2.0, 0.00 v5.0.0, 0.04 v4.0.1, 0.13 v4.0.0, 0.12 v3.7.0, 0.10 v3.5.0, 0.11 v3.3.0, 0.14 v3.2.0, 0.18 v3.1.0, 0.22 v2.7.0, 0.33 v2.6.0, 0.43 v2.5.0, 0.38 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1, 0.00 v2.1.0 % 10.63/10.80 % Syntax : Number of formulae : 12 ( 2 unt; 0 def) % 10.63/10.80 % Number of atoms : 41 ( 1 equ) % 10.63/10.80 % Maximal formula atoms : 7 ( 3 avg) % 10.63/10.80 % Number of connectives : 30 ( 1 ~; 1 |; 16 &) % 10.63/10.80 % ( 1 <=>; 11 =>; 0 <=; 0 <~>) % 10.63/10.80 % Maximal formula depth : 9 ( 5 avg) % 10.63/10.80 % Maximal term depth : 2 ( 1 avg) % 10.63/10.80 % Number of predicates : 9 ( 8 usr; 0 prp; 1-3 aty) % 10.63/10.80 % Number of functors : 5 ( 5 usr; 2 con; 0-1 aty) % 10.63/10.80 % Number of variables : 20 ( 19 !; 1 ?) % 10.63/10.80 % SPC : FOF_THM_RFO_SEQ % 10.63/10.80 % 10.63/10.80 % Comments : % 10.63/10.80 %-------------------------------------------------------------------------- % 10.63/10.80 %----Subsitution axioms % 10.63/10.80 %----Problem axioms % 10.63/10.80 %----MP3. If selection favors organizations of a certain propagation % 10.63/10.80 %----strategy, s1, above an other, s2, at the endpoints of all % 10.63/10.80 %----environments in the observational period, then it favors s1 above % 10.63/10.80 %----s2 during the whole observational period. % 10.63/10.80 %----Instantiation: EP = s1 ; FM = s2 % 10.63/10.80 fof(mp3_favoured_trategy,axiom, % 10.63/10.80 ! [P] : % 10.63/10.80 ( ( observational_period(P) % 10.63/10.80 & propagation_strategy(first_movers) % 10.63/10.80 & propagation_strategy(efficient_producers) % 10.63/10.80 & ! [E] : % 10.63/10.80 ( ( environment(E) % 10.63/10.80 & in_environment(P,E) ) % 10.63/10.80 => selection_favors(efficient_producers,first_movers,end_time(E)) ) ) % 10.63/10.80 => selection_favors(efficient_producers,first_movers,P) ) ). % 10.63/10.80 % 10.63/10.80 %----MP4. If environmental change is slow during an observational period, % 10.63/10.80 %----then all the environments in the observational period contain a % 10.63/10.80 %----critical point. % 10.63/10.80 fof(mp4_critical_point,axiom, % 10.63/10.80 ! [P] : % 10.63/10.80 ( ( observational_period(P) % 10.63/10.80 & slow_change(P) ) % 10.63/10.80 => ! [E] : % 10.63/10.80 ( ( environment(E) % 10.63/10.80 & in_environment(P,E) ) % 10.63/10.80 => ? [T] : % 10.63/10.80 ( in_environment(E,T) % 10.63/10.80 & greater(T,critical_point(E)) ) ) ) ). % 10.63/10.80 % 10.63/10.80 %----MP. First movers and efficient producers are organizational sets of a % 10.63/10.80 %----certain propagation strategy. % 10.63/10.80 fof(mp_organizational_sets1,axiom, % 10.63/10.80 propagation_strategy(first_movers) ). % 10.63/10.80 % 10.63/10.80 fof(mp_organizational_sets2,axiom, % 10.63/10.80 propagation_strategy(efficient_producers) ). % 10.63/10.80 % 10.63/10.80 %----MP. If a time point occurs between the beginning and the end of the % 10.63/10.80 %----environment, then it belongs to the environment. % 10.63/10.80 fof(mp_time_in_environment,axiom, % 10.63/10.80 ! [E,T] : % 10.63/10.80 ( ( environment(E) % 10.63/10.80 & greater_or_equal(T,start_time(E)) % 10.63/10.80 & greater_or_equal(end_time(E),T) ) % 10.63/10.80 => in_environment(E,T) ) ). % 10.63/10.80 % 10.63/10.80 %----MP. If a time point belongs to the environment, then the end-point of % 10.63/10.80 %----the environment cannot precede it. % 10.63/10.80 fof(mp_environment_end_point,axiom, % 10.63/10.80 ! [E,T] : % 10.63/10.80 ( ( environment(E) % 10.63/10.80 & in_environment(E,T) ) % 10.63/10.80 => greater_or_equal(end_time(E),T) ) ). % 10.63/10.80 % 10.63/10.80 %----MP. The critical point of an environment cannot precede the % 10.63/10.80 %----environment's opening time. % 10.63/10.80 fof(mp_time_of_critical_point,axiom, % 10.63/10.80 ! [E] : % 10.63/10.80 ( environment(E) % 10.63/10.80 => greater_or_equal(critical_point(E),start_time(E)) ) ). % 10.63/10.80 % 10.63/10.80 %----MP. inequality % 10.63/10.80 fof(mp_greater_transitivity,axiom, % 10.63/10.80 ! [X,Y,Z] : % 10.63/10.80 ( ( greater(X,Y) % 10.63/10.80 & greater(Y,Z) ) % 10.63/10.80 => greater(X,Z) ) ). % 10.63/10.80 % 10.63/10.80 %----MP. on "greater or equal to" % 10.63/10.80 fof(mp_greater_or_equal,axiom, % 10.63/10.80 ! [X,Y] : % 10.63/10.80 ( greater_or_equal(X,Y) % 10.63/10.80 <=> ( greater(X,Y) % 10.63/10.80 | X = Y ) ) ). % 10.63/10.80 % 10.63/10.80 %----MP. on beginning and ending times % 10.63/10.80 fof(mp_beginning_and_ending,axiom, % 10.63/10.80 ! [E,T] : % 10.63/10.80 ( ( environment(E) % 10.63/10.80 & greater(T,start_time(E)) % 10.63/10.80 & ~ greater(T,end_time(E)) ) % 10.63/10.80 => greater_or_equal(end_time(E),T) ) ). % 10.63/10.80 % 10.63/10.80 %----L8. Selection favors efficient producers above first movers past the % 10.63/10.80 %----critical point. % 10.63/10.80 fof(l8,hypothesis, % 10.63/10.80 ! [E,T] : % 10.63/10.80 ( ( environment(E) % 10.63/10.80 & in_environment(E,T) % 10.63/10.80 & greater(T,critical_point(E)) ) % 10.63/10.80 => selection_favors(efficient_producers,first_movers,T) ) ). % 10.63/10.80 % 10.63/10.80 %----GOAL: T8. Selection favors efficient producers above first movers if % 10.63/10.81 %----environmental change is slow. % 10.63/10.81 fof(prove_t8,conjecture, % 10.63/10.81 ! [P] : % 10.63/10.81 ( ( observational_period(P) % 10.63/10.81 & slow_change(P) ) % 10.63/10.81 => selection_favors(efficient_producers,first_movers,P) ) ). % 10.63/10.81 % 10.63/10.81 %-------------------------------------------------------------------------- % 10.63/10.81 %------------------------------------------- % 10.63/10.81 % Proof found % 10.63/10.81 % SZS status Theorem for theBenchmark % 10.63/10.81 % SZS output start Proof % 10.63/10.81 %ClaNum:41(EqnAxiom:22) % 10.63/10.81 %VarNum:74(SingletonVarNum:25) % 10.63/10.81 %MaxLitNum:5 % 10.63/10.81 %MaxfuncDepth:2 % 10.63/10.81 %SharedTerms:10 % 10.63/10.81 %goalClause: 23 26 27 % 10.63/10.81 %singleGoalClaCount:3 % 10.63/10.81 [23]P1(a1) % 10.63/10.81 [24]P6(a7) % 10.63/10.81 [25]P6(a2) % 10.63/10.81 [26]P7(a1) % 10.63/10.81 [27]~P8(a2,a7,a1) % 10.63/10.81 [29]~P3(x291)+P2(f3(x291),f8(x291)) % 10.63/10.81 [28]~E(x281,x282)+P2(x281,x282) % 10.63/10.81 [30]~P4(x301,x302)+P2(x301,x302) % 10.63/10.81 [31]P4(x311,x312)+~P2(x311,x312)+E(x311,x312) % 10.63/10.81 [32]~P3(x321)+~P5(x321,x322)+P2(f4(x321),x322) % 10.63/10.81 [33]~P4(x331,x333)+P4(x331,x332)+~P4(x333,x332) % 10.63/10.81 [35]~P3(x352)+~P4(x351,f8(x352))+P4(x351,f4(x352))+P2(f4(x352),x351) % 10.63/10.81 [37]~P3(x371)+P5(x371,x372)+~P2(x372,f8(x371))+~P2(f4(x371),x372) % 10.63/10.81 [40]~P5(x402,x401)+~P3(x402)+~P4(x401,f3(x402))+P8(a2,a7,x401) % 10.63/10.81 [34]~P1(x341)+P8(a2,a7,x341)+P3(f5(x341))+~P6(a7)+~P6(a2) % 10.63/10.81 [38]~P1(x381)+P5(x381,f5(x381))+P8(a2,a7,x381)+~P6(a7)+~P6(a2) % 10.63/10.81 [41]~P1(x411)+P8(a2,a7,x411)+~P6(a7)+~P6(a2)+~P8(a2,a7,f4(f5(x411))) % 10.63/10.81 [36]~P1(x362)+~P3(x361)+~P7(x362)+~P5(x362,x361)+P5(x361,f6(x362,x361)) % 10.63/10.81 [39]~P1(x391)+~P3(x392)+~P7(x391)+~P5(x391,x392)+P4(f6(x391,x392),f3(x392)) % 10.63/10.81 %EqnAxiom % 10.63/10.81 [1]E(x11,x11) % 10.63/10.81 [2]E(x22,x21)+~E(x21,x22) % 10.63/10.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 10.63/10.81 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 10.63/10.81 [5]~E(x51,x52)+E(f8(x51),f8(x52)) % 10.63/10.81 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 10.63/10.81 [7]~E(x71,x72)+E(f5(x71),f5(x72)) % 10.63/10.81 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83)) % 10.63/10.81 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92)) % 10.63/10.81 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 10.63/10.81 [11]~P6(x111)+P6(x112)+~E(x111,x112) % 10.63/10.81 [12]P4(x122,x123)+~E(x121,x122)+~P4(x121,x123) % 10.63/10.81 [13]P4(x133,x132)+~E(x131,x132)+~P4(x133,x131) % 10.63/10.81 [14]~P7(x141)+P7(x142)+~E(x141,x142) % 10.63/10.81 [15]P8(x152,x153,x154)+~E(x151,x152)+~P8(x151,x153,x154) % 10.63/10.81 [16]P8(x163,x162,x164)+~E(x161,x162)+~P8(x163,x161,x164) % 10.63/10.81 [17]P8(x173,x174,x172)+~E(x171,x172)+~P8(x173,x174,x171) % 10.63/10.81 [18]P2(x182,x183)+~E(x181,x182)+~P2(x181,x183) % 10.63/10.81 [19]P2(x193,x192)+~E(x191,x192)+~P2(x193,x191) % 10.63/10.81 [20]P5(x202,x203)+~E(x201,x202)+~P5(x201,x203) % 10.63/10.81 [21]P5(x213,x212)+~E(x211,x212)+~P5(x213,x211) % 10.63/10.81 [22]~P3(x221)+P3(x222)+~E(x221,x222) % 10.63/10.81 % 10.63/10.81 %------------------------------------------- % 10.63/10.81 cnf(42,plain, % 10.63/10.81 (P2(x421,x421)), % 10.63/10.81 inference(equality_inference,[],[28])). % 10.63/10.81 cnf(43,plain, % 10.63/10.81 (P5(a1,f5(a1))), % 10.63/10.81 inference(scs_inference,[],[23,27,24,25,38])). % 10.63/10.81 cnf(50,plain, % 10.63/10.81 (~P1(x501)+P8(a2,a7,x501)+P3(f5(x501))), % 10.63/10.81 inference(scs_inference,[],[24,25,34])). % 10.63/10.81 cnf(52,plain, % 10.63/10.81 (~P1(x521)+P8(a2,a7,x521)+~P8(a2,a7,f4(f5(x521)))), % 10.63/10.81 inference(scs_inference,[],[24,25,41])). % 10.63/10.81 cnf(53,plain, % 10.63/10.81 (P3(f5(a1))), % 10.63/10.81 inference(scs_inference,[],[23,27,50])). % 10.63/10.81 cnf(55,plain, % 10.63/10.81 (~P8(a2,a7,f4(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[23,27,50,52])). % 10.63/10.81 cnf(66,plain, % 10.63/10.81 (~P5(f5(a1),f4(f5(a1)))+~P4(f4(f5(a1)),f3(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[53,55,40])). % 10.63/10.81 cnf(71,plain, % 10.63/10.81 (P2(f3(f5(a1)),f8(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[27,23,29,50])). % 10.63/10.81 cnf(72,plain, % 10.63/10.81 (E(f3(f5(a1)),f8(f5(a1)))+P4(f3(f5(a1)),f8(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[71,31])). % 10.63/10.81 cnf(106,plain, % 10.63/10.81 (~P4(x1061,f3(f5(a1)))+~E(x1061,f4(f5(a1)))+~P5(f5(a1),f4(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[66,12])). % 10.63/10.81 cnf(119,plain, % 10.63/10.81 (~E(x1191,a1)+~P1(a1)+P1(x1191)), % 10.63/10.81 inference(scs_inference,[],[23,10,2])). % 10.63/10.81 cnf(121,plain, % 10.63/10.81 (P1(x1211)+~E(x1211,a1)), % 10.63/10.81 inference(scs_inference,[],[23,119])). % 10.63/10.81 cnf(140,plain, % 10.63/10.81 (P4(x1401,f4(f5(a1)))+P2(f4(f5(a1)),x1401)+~P4(x1401,f8(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[27,23,35,50])). % 10.63/10.81 cnf(141,plain, % 10.63/10.81 (P5(f5(a1),f4(f5(a1)))+~P4(f8(f5(a1)),f8(f5(a1)))+P4(f8(f5(a1)),f4(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[42,53,140,37])). % 10.63/10.81 cnf(142,plain, % 10.63/10.81 (P5(f5(a1),f6(a1,f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[26,43,53,121,36])). % 10.63/10.81 cnf(143,plain, % 10.63/10.81 (P5(f5(a1),x1431)+~E(f6(a1,f5(a1)),x1431)), % 10.63/10.81 inference(scs_inference,[],[142,21])). % 10.63/10.81 cnf(157,plain, % 10.63/10.81 (P4(f6(a1,f5(a1)),f3(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[26,43,53,121,39])). % 10.63/10.81 cnf(242,plain, % 10.63/10.81 (~E(x2421,f6(a1,f5(a1)))+P5(f5(a1),x2421)), % 10.63/10.81 inference(scs_inference,[],[2,143])). % 10.63/10.81 cnf(288,plain, % 10.63/10.81 (~E(f4(f5(a1)),f6(a1,f5(a1)))+~P5(f5(a1),f4(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[157,2,106])). % 10.63/10.81 cnf(289,plain, % 10.63/10.81 (~E(f4(f5(a1)),f6(a1,f5(a1)))+~E(f6(a1,f5(a1)),f4(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[288,143])). % 10.63/10.81 cnf(290,plain, % 10.63/10.81 (~E(f6(a1,f5(a1)),f4(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[289,2])). % 10.63/10.81 cnf(299,plain, % 10.63/10.81 (~P2(f4(f5(a1)),f6(a1,f5(a1)))+P4(f4(f5(a1)),f6(a1,f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[290,2,31])). % 10.63/10.81 cnf(300,plain, % 10.63/10.81 (P4(f4(f5(a1)),f6(a1,f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[142,53,299,32])). % 10.63/10.81 cnf(301,plain, % 10.63/10.81 (P4(f4(f5(a1)),f3(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[157,300,33])). % 10.63/10.81 cnf(303,plain, % 10.63/10.81 (~P5(f5(a1),f4(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[157,55,53,300,33,40])). % 10.63/10.81 cnf(308,plain, % 10.63/10.81 (P4(f4(f5(a1)),x3081)+~E(f6(a1,f5(a1)),x3081)), % 10.63/10.81 inference(scs_inference,[],[157,55,53,300,33,40,242,141,12,13])). % 10.63/10.81 cnf(330,plain, % 10.63/10.81 (P4(f4(f5(a1)),x3301)+~E(f3(f5(a1)),x3301)), % 10.63/10.81 inference(scs_inference,[],[301,13])). % 10.63/10.81 cnf(386,plain, % 10.63/10.81 (~E(x3861,f6(a1,f5(a1)))+P4(f4(f5(a1)),x3861)), % 10.63/10.81 inference(scs_inference,[],[2,308])). % 10.63/10.81 cnf(397,plain, % 10.63/10.81 (~E(x3971,f3(f5(a1)))+P4(f4(f5(a1)),x3971)), % 10.63/10.81 inference(scs_inference,[],[2,330])). % 10.63/10.81 cnf(538,plain, % 10.63/10.81 (~P4(f4(f5(a1)),f8(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[42,303,53,30,37])). % 10.63/10.81 cnf(552,plain, % 10.63/10.81 (P4(f6(a1,f5(a1)),f8(f5(a1)))), % 10.63/10.81 inference(scs_inference,[],[157,301,538,308,386,397,13,72,33])). % 10.63/10.81 cnf(560,plain, % 10.63/10.81 ($false), % 10.63/10.81 inference(scs_inference,[],[300,552,538,33]), % 10.63/10.81 ['proof']). % 10.63/10.81 % SZS output end Proof % 10.63/10.81 % Total time :10.340788s %------------------------------------------------------------------------------