%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT022+2 : 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 : n003.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 : Theorem 0.29s 0.47s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT022+2 : 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.35 % Computer : n003.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:06:24 UTC 2026 % 0.09/0.35 % CPUTime : % 0.12/0.45 start to proof:theBenchmark % 0.29/0.47 %------------------------------------------- % 0.29/0.47 % File :CSE---1.7 % 0.29/0.47 % Problem :theBenchmark % 0.29/0.47 % Transform :cnf % 0.29/0.47 % Format :tptp:raw % 0.29/0.47 % Command :java -jar mcs_scs.jar %d %s % 0.29/0.47 % 0.29/0.47 % Result :Theorem 0.008866s % 0.29/0.47 % Output :CNFRefutation 0.008866s % 0.29/0.47 %------------------------------------------- % 0.29/0.47 %-------------------------------------------------------------------------- % 0.29/0.47 % File : MGT022+2 : TPTP v9.3.0. Released v2.0.0. % 0.29/0.47 % Domain : Management (Organisation Theory) % 0.29/0.47 % Problem : Decreasing resource availability affects FMS more than EPs % 0.29/0.47 % Version : [PM93] axioms. % 0.29/0.47 % English : Decreasing resource availability affects the disbanding rate % 0.29/0.47 % of first movers more than the disbanding rate of efficient % 0.29/0.47 % producers. % 0.29/0.47 % 0.29/0.47 % Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg % 0.29/0.47 % : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg % 0.29/0.47 % : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing % 0.29/0.47 % Source : [PM93] % 0.29/0.47 % Names : LEMMA 4 [PM93] % 0.29/0.47 % : L4 [PB+94] % 0.29/0.47 % 0.29/0.47 % Status : Theorem % 0.29/0.47 % Rating : 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.04 v5.3.0, 0.13 v5.2.0, 0.00 v2.1.0 % 0.29/0.47 % Syntax : Number of formulae : 4 ( 1 unt; 0 def) % 0.29/0.47 % Number of atoms : 16 ( 0 equ) % 0.29/0.47 % Maximal formula atoms : 7 ( 4 avg) % 0.29/0.47 % Number of connectives : 14 ( 2 ~; 0 |; 5 &) % 0.29/0.47 % ( 0 <=>; 7 =>; 0 <=; 0 <~>) % 0.29/0.47 % Maximal formula depth : 8 ( 5 avg) % 0.29/0.47 % Maximal term depth : 3 ( 1 avg) % 0.29/0.47 % Number of predicates : 6 ( 6 usr; 0 prp; 1-4 aty) % 0.29/0.47 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty) % 0.29/0.47 % Number of variables : 7 ( 7 !; 0 ?) % 0.29/0.47 % SPC : FOF_THM_RFO_NEQ % 0.29/0.47 % 0.29/0.47 % Comments : % 0.29/0.47 %-------------------------------------------------------------------------- % 0.29/0.47 %----MP. If something is constant, then it does not decreases. % 0.29/0.47 fof(mp_constant_not_decrease,axiom, % 0.29/0.47 ! [X] : % 0.29/0.47 ( constant(X) % 0.29/0.47 => ~ decreases(X) ) ). % 0.29/0.47 % 0.29/0.47 %----A6. Less resilient subpopulations are more affected by decreasing % 0.29/0.47 %----resource availability. % 0.29/0.47 fof(a6,hypothesis, % 0.29/0.47 ! [E,S1,S2,T] : % 0.29/0.47 ( ( environment(E) % 0.29/0.47 & subpopulations(S1,S2,E,T) % 0.29/0.47 & greater(resilience(S2),resilience(S1)) ) % 0.29/0.47 => ( ( decreases(resources(E,T)) % 0.29/0.47 => increases(difference(disbanding_rate(S1,T),disbanding_rate(S2,T))) ) % 0.29/0.47 & ( constant(resources(E,T)) % 0.29/0.47 => constant(difference(disbanding_rate(S1,T),disbanding_rate(S2,T))) ) ) ) ). % 0.29/0.47 % 0.29/0.47 %----A2. Efficient producers are more resilient than first movers. % 0.29/0.47 fof(a2,hypothesis, % 0.29/0.47 greater(resilience(efficient_producers),resilience(first_movers)) ). % 0.29/0.47 % 0.29/0.47 %----GOAL: L4. A decreasing resource availability affects the disbanding % 0.29/0.47 %----rate of first movers more than the disbanding rate of efficient % 0.29/0.47 %----producers. % 0.29/0.47 fof(prove_l4,conjecture, % 0.29/0.47 ! [E,T] : % 0.29/0.47 ( ( environment(E) % 0.29/0.47 & subpopulations(first_movers,efficient_producers,E,T) ) % 0.29/0.47 => ( ( decreases(resources(E,T)) % 0.29/0.47 => increases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ) % 0.29/0.47 & ( constant(resources(E,T)) % 0.29/0.47 => ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ) ) ) ). % 0.29/0.47 % 0.29/0.47 %-------------------------------------------------------------------------- % 0.29/0.47 %------------------------------------------- % 0.29/0.47 % Proof found % 0.29/0.47 % SZS status Theorem for theBenchmark % 0.29/0.47 % SZS output start Proof % 0.29/0.47 %ClaNum:10(EqnAxiom:0) % 0.29/0.47 %VarNum:28(SingletonVarNum:9) % 0.29/0.47 %MaxLitNum:5 % 0.29/0.47 %MaxfuncDepth:2 % 0.29/0.47 %SharedTerms:17 % 0.29/0.47 %goalClause: 1 3 5 6 7 8 % 0.29/0.47 %singleGoalClaCount:2 % 0.29/0.47 [1]P1(a1) % 0.29/0.47 [3]P5(a6,a2,a1,a7) % 0.29/0.47 [2]P4(f5(a2),f5(a6)) % 0.29/0.47 [5]P3(f8(a1,a7))+P2(f8(a1,a7)) % 0.29/0.47 [6]P3(f8(a1,a7))+P3(f4(f3(a6,a7),f3(a2,a7))) % 0.29/0.47 [7]~P6(f4(f3(a6,a7),f3(a2,a7)))+P2(f8(a1,a7)) % 0.29/0.47 [8]~P6(f4(f3(a6,a7),f3(a2,a7)))+P3(f4(f3(a6,a7),f3(a2,a7))) % 0.29/0.47 [4]~P3(x41)+~P2(x41) % 0.29/0.47 [9]~P5(x91,x93,x94,x92)+~P1(x94)+~P4(f5(x93),f5(x91))+~P2(f8(x94,x92))+P2(f4(f3(x91,x92),f3(x93,x92))) % 0.29/0.47 [10]~P5(x101,x103,x104,x102)+~P1(x104)+~P4(f5(x103),f5(x101))+~P3(f8(x104,x102))+P6(f4(f3(x101,x102),f3(x103,x102))) % 0.29/0.47 %EqnAxiom % 0.29/0.47 % 0.29/0.47 %------------------------------------------- % 0.29/0.48 cnf(12,plain, % 0.29/0.48 (~P2(f8(a1,a7))+P3(f4(f3(a6,a7),f3(a2,a7)))), % 0.29/0.48 inference(scs_inference,[],[6,4])). % 0.29/0.48 cnf(13,plain, % 0.29/0.48 (~P3(f8(a1,a7))+~P6(f4(f3(a6,a7),f3(a2,a7)))), % 0.29/0.48 inference(scs_inference,[],[7,4])). % 0.29/0.48 cnf(14,plain, % 0.29/0.48 (~P2(f4(f3(a6,a7),f3(a2,a7)))+~P2(f8(a1,a7))), % 0.29/0.48 inference(scs_inference,[],[12,4])). % 0.29/0.48 cnf(15,plain, % 0.29/0.48 (~P3(f8(a1,a7))), % 0.29/0.48 inference(scs_inference,[],[2,1,3,13,10])). % 0.29/0.48 cnf(16,plain, % 0.29/0.48 (P2(f8(a1,a7))), % 0.29/0.48 inference(scs_inference,[],[15,5])). % 0.29/0.48 cnf(19,plain, % 0.29/0.48 (~P2(f4(f3(a6,a7),f3(a2,a7)))), % 0.29/0.48 inference(scs_inference,[],[16,14])). % 0.29/0.48 cnf(20,plain, % 0.29/0.48 ($false), % 0.29/0.48 inference(scs_inference,[],[3,16,1,19,2,9]), % 0.29/0.48 ['proof']). % 0.29/0.48 % SZS output end Proof % 0.29/0.48 % Total time :0.008866s %------------------------------------------------------------------------------