%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT053+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 : n019.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:21 AM UTC 2026
% Result : Theorem 7.33s 7.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT053+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 13:23:37 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.52 start to proof:theBenchmark
% 7.33/7.58 %-------------------------------------------
% 7.33/7.58 % File :CSE---1.7
% 7.33/7.58 % Problem :theBenchmark
% 7.33/7.58 % Transform :cnf
% 7.33/7.58 % Format :tptp:raw
% 7.33/7.58 % Command :java -jar mcs_scs.jar %d %s
% 7.33/7.58
% 7.33/7.58 % Result :Theorem 7.078269s
% 7.33/7.58 % Output :CNFRefutation 7.078269s
% 7.33/7.58 %-------------------------------------------
% 7.33/7.58 %--------------------------------------------------------------------------
% 7.33/7.58 % File : MGT053+1 : TPTP v9.3.0. Released v2.4.0.
% 7.33/7.58 % Domain : Management (Organisation Theory)
% 7.33/7.58 % Problem : The dissimilarity relation is symmetric
% 7.33/7.58 % Version : [Han98] axioms.
% 7.33/7.58 % English :
% 7.33/7.58
% 7.33/7.58 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 7.33/7.58 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 7.33/7.58 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 7.33/7.58 % Source : [Kam00]
% 7.33/7.58 % Names : LEMMA 7 [Han98]
% 7.33/7.58
% 7.33/7.58 % Status : Theorem
% 7.33/7.58 % Rating : 0.09 v9.3.0, 0.00 v5.3.0, 0.09 v5.2.0, 0.00 v4.1.0, 0.13 v4.0.1, 0.17 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0, 0.17 v2.7.0, 0.00 v2.4.0
% 7.33/7.58 % Syntax : Number of formulae : 8 ( 0 unt; 0 def)
% 7.33/7.58 % Number of atoms : 22 ( 3 equ)
% 7.33/7.58 % Maximal formula atoms : 4 ( 2 avg)
% 7.33/7.58 % Number of connectives : 16 ( 2 ~; 4 |; 3 &)
% 7.33/7.58 % ( 6 <=>; 1 =>; 0 <=; 0 <~>)
% 7.33/7.59 % Maximal formula depth : 8 ( 5 avg)
% 7.33/7.59 % Maximal term depth : 1 ( 1 avg)
% 7.33/7.59 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 7.33/7.59 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 7.33/7.59 % Number of variables : 19 ( 19 !; 0 ?)
% 7.33/7.59 % SPC : FOF_THM_RFO_SEQ
% 7.33/7.59
% 7.33/7.59 % Comments : See MGT042+1.p for the mnemonic names.
% 7.33/7.59 %--------------------------------------------------------------------------
% 7.33/7.59 include('Axioms/MGT001+0.ax').
% 7.33/7.59 %--------------------------------------------------------------------------
% 7.33/7.59 %----Problem Axioms
% 7.33/7.59 %----Two states of the environment are dissimilar for an organization
% 7.33/7.59 %----if and only if the organization cannot be aligned to both.
% 7.33/7.59 %----
% 7.33/7.59 %----Added quantification over X.
% 7.33/7.59 fof(definition_2,axiom,
% 7.33/7.59 ! [X,T0,T] :
% 7.33/7.59 ( dissimilar(X,T0,T)
% 7.33/7.59 <=> ( organization(X)
% 7.33/7.59 & ~ ( is_aligned(X,T0)
% 7.33/7.59 <=> is_aligned(X,T) ) ) ) ).
% 7.33/7.59
% 7.33/7.59 %----Problem theorems
% 7.33/7.59 %----The dissimilarity relation is symmetric.
% 7.33/7.59 %----From D2.
% 7.33/7.59 %----
% 7.33/7.59 %----As stated is incorrect (missing Xs in quantification and second DS).
% 7.33/7.59 %----No inequalities needed.
% 7.33/7.59 fof(lemma_7,conjecture,
% 7.33/7.59 ! [X,T1,T2] :
% 7.33/7.59 ( dissimilar(X,T1,T2)
% 7.33/7.59 <=> dissimilar(X,T2,T1) ) ).
% 7.33/7.59
% 7.33/7.59 %--------------------------------------------------------------------------
% 7.33/7.59 %-------------------------------------------
% 7.33/7.59 % Proof found
% 7.33/7.59 % SZS status Theorem for theBenchmark
% 7.33/7.59 % SZS output start Proof
% 7.33/7.59 %ClaNum:35(EqnAxiom:17)
% 7.33/7.59 %VarNum:86(SingletonVarNum:38)
% 7.33/7.59 %MaxLitNum:4
% 7.33/7.59 %MaxfuncDepth:0
% 7.33/7.59 %SharedTerms:7
% 7.33/7.59 %goalClause: 32 35
% 7.33/7.59 [32]P4(a1,a2,a3)+P4(a1,a3,a2)
% 7.33/7.59 [35]~P4(a1,a2,a3)+~P4(a1,a3,a2)
% 7.33/7.59 [18]~E(x181,x182)+P1(x181,x182)
% 7.33/7.59 [19]~E(x191,x192)+P2(x191,x192)
% 7.33/7.59 [21]~P5(x211,x212)+P1(x211,x212)
% 7.33/7.59 [22]~P3(x222,x221)+P5(x221,x222)
% 7.33/7.59 [23]~P3(x231,x232)+P2(x231,x232)
% 7.33/7.59 [24]~P5(x242,x241)+P3(x241,x242)
% 7.33/7.59 [27]~P3(x272,x271)+~P3(x271,x272)
% 7.33/7.59 [29]P6(x291)+~P4(x291,x292,x293)
% 7.33/7.59 [20]P5(x201,x202)+P3(x201,x202)+E(x201,x202)
% 7.33/7.59 [25]P5(x251,x252)+~P1(x251,x252)+E(x251,x252)
% 7.33/7.59 [26]P3(x261,x262)+~P2(x261,x262)+E(x261,x262)
% 7.33/7.59 [28]~P3(x281,x283)+P3(x281,x282)+~P3(x283,x282)
% 7.33/7.59 [33]~P4(x331,x333,x332)+P7(x331,x332)+P7(x331,x333)
% 7.33/7.59 [34]~P4(x341,x343,x342)+~P7(x341,x342)+~P7(x341,x343)
% 7.33/7.59 [30]~P6(x301)+~P7(x301,x303)+P7(x301,x302)+P4(x301,x302,x303)
% 7.33/7.59 [31]~P6(x311)+~P7(x311,x313)+P7(x311,x312)+P4(x311,x313,x312)
% 7.33/7.59 %EqnAxiom
% 7.33/7.59 [1]E(x11,x11)
% 7.33/7.59 [2]E(x22,x21)+~E(x21,x22)
% 7.33/7.59 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 7.33/7.59 [4]P1(x42,x43)+~E(x41,x42)+~P1(x41,x43)
% 7.33/7.59 [5]P1(x53,x52)+~E(x51,x52)+~P1(x53,x51)
% 7.33/7.59 [6]P2(x62,x63)+~E(x61,x62)+~P2(x61,x63)
% 7.33/7.59 [7]P2(x73,x72)+~E(x71,x72)+~P2(x73,x71)
% 7.33/7.59 [8]P5(x82,x83)+~E(x81,x82)+~P5(x81,x83)
% 7.33/7.59 [9]P5(x93,x92)+~E(x91,x92)+~P5(x93,x91)
% 7.33/7.59 [10]P3(x102,x103)+~E(x101,x102)+~P3(x101,x103)
% 7.33/7.59 [11]P3(x113,x112)+~E(x111,x112)+~P3(x113,x111)
% 7.33/7.59 [12]P4(x122,x123,x124)+~E(x121,x122)+~P4(x121,x123,x124)
% 7.33/7.59 [13]P4(x133,x132,x134)+~E(x131,x132)+~P4(x133,x131,x134)
% 7.33/7.59 [14]P4(x143,x144,x142)+~E(x141,x142)+~P4(x143,x144,x141)
% 7.33/7.59 [15]P7(x152,x153)+~E(x151,x152)+~P7(x151,x153)
% 7.33/7.59 [16]P7(x163,x162)+~E(x161,x162)+~P7(x163,x161)
% 7.33/7.59 [17]~P6(x171)+P6(x172)+~E(x171,x172)
% 7.33/7.59
% 7.33/7.59 %-------------------------------------------
% 7.33/7.59 cnf(247,plain,
% 7.33/7.59 (P6(a1)+P4(a1,a2,a3)),
% 7.33/7.59 inference(scs_inference,[],[29,32])).
% 7.33/7.59 cnf(248,plain,
% 7.33/7.59 (P6(a1)),
% 7.33/7.59 inference(scs_inference,[],[247,29])).
% 7.33/7.59 cnf(312,plain,
% 7.33/7.59 (P7(a1,a3)+P7(a1,a2)+P4(a1,a3,a2)),
% 7.33/7.59 inference(scs_inference,[],[32,33])).
% 7.33/7.59 cnf(313,plain,
% 7.33/7.59 (P7(a1,a2)+P7(a1,a3)),
% 7.33/7.59 inference(scs_inference,[],[312,33])).
% 7.33/7.59 cnf(321,plain,
% 7.33/7.59 (P4(a1,x3211,a2)+P7(a1,x3211)+P7(a1,a3)),
% 7.33/7.59 inference(scs_inference,[],[248,313,30])).
% 7.33/7.59 cnf(326,plain,
% 7.33/7.59 (P4(a1,a3,x3261)+P7(a1,x3261)+P7(a1,a2)),
% 7.33/7.59 inference(scs_inference,[],[248,313,31])).
% 7.33/7.59 cnf(341,plain,
% 7.33/7.59 (P4(a1,a2,x3411)+P7(a1,x3411)+P7(a1,a3)),
% 7.33/7.59 inference(scs_inference,[],[248,313,31])).
% 7.33/7.59 cnf(345,plain,
% 7.33/7.59 (P4(a1,x3451,a3)+P7(a1,x3451)+P7(a1,a2)),
% 7.33/7.59 inference(scs_inference,[],[248,313,30])).
% 7.33/7.59 cnf(912,plain,
% 7.33/7.59 (~P7(a1,a2)+~P7(a1,a3)+P4(a1,a2,a3)),
% 7.33/7.59 inference(scs_inference,[],[32,34])).
% 7.33/7.59 cnf(913,plain,
% 7.33/7.59 (~P7(a1,a3)+~P7(a1,a2)),
% 7.33/7.59 inference(scs_inference,[],[912,34])).
% 7.33/7.59 cnf(923,plain,
% 7.33/7.59 (~P7(a1,a3)+P4(a1,a3,a2)),
% 7.33/7.59 inference(scs_inference,[],[913,326])).
% 7.33/7.59 cnf(931,plain,
% 7.33/7.59 (~P7(a1,a2)+P4(a1,a3,a2)),
% 7.33/7.59 inference(scs_inference,[],[913,321])).
% 7.33/7.59 cnf(932,plain,
% 7.33/7.59 (~P7(a1,a2)+~P4(a1,a2,a3)),
% 7.33/7.59 inference(scs_inference,[],[931,35])).
% 7.33/7.59 cnf(933,plain,
% 7.33/7.59 (P7(a1,a3)+~P4(a1,a2,a3)),
% 7.33/7.59 inference(scs_inference,[],[932,313])).
% 7.33/7.59 cnf(934,plain,
% 7.33/7.59 (P4(a1,a3,a2)+~P4(a1,a2,a3)),
% 7.33/7.59 inference(scs_inference,[],[933,923])).
% 7.33/7.59 cnf(935,plain,
% 7.33/7.59 (~P4(a1,a2,a3)),
% 7.33/7.59 inference(scs_inference,[],[934,35])).
% 7.33/7.59 cnf(948,plain,
% 7.33/7.59 ($false),
% 7.33/7.59 inference(scs_inference,[],[935,341,345,913]),
% 7.33/7.59 ['proof']).
% 7.33/7.59 % SZS output end Proof
% 7.33/7.59 % Total time :7.078269s
%------------------------------------------------------------------------------