%------------------------------------------------------------------------------
% 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 : n014.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 : Unsatisfiable 13.45s 13.64s
% 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.09/0.34 % Computer : n014.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 13:24:11 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.28/0.51 start to proof:theBenchmark
% 13.45/13.63 %-------------------------------------------
% 13.45/13.63 % File :CSE---1.7
% 13.45/13.63 % Problem :theBenchmark
% 13.45/13.63 % Transform :cnf
% 13.45/13.63 % Format :tptp:raw
% 13.45/13.63 % Command :java -jar mcs_scs.jar %d %s
% 13.45/13.63
% 13.45/13.63 % Result :Theorem 13.134973s
% 13.45/13.63 % Output :CNFRefutation 13.134973s
% 13.45/13.63 %-------------------------------------------
% 13.45/13.63 %--------------------------------------------------------------------------
% 13.45/13.63 % File : MGT053-1 : TPTP v9.3.0. Released v2.4.0.
% 13.45/13.63 % Domain : Management (Organisation Theory)
% 13.45/13.63 % Problem : The dissimilarity relation is symmetric
% 13.45/13.63 % Version : [Han98] axioms.
% 13.45/13.63 % English :
% 13.45/13.63
% 13.45/13.63 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 13.45/13.63 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 13.45/13.63 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 13.45/13.63 % Source : [TPTP]
% 13.45/13.63 % Names :
% 13.45/13.63
% 13.45/13.63 % Status : Unsatisfiable
% 13.45/13.63 % Rating : 0.00 v4.0.1, 0.20 v3.7.0, 0.00 v2.4.0
% 13.45/13.63 % Syntax : Number of clauses : 22 ( 0 unt; 9 nHn; 17 RR)
% 13.45/13.63 % Number of literals : 58 ( 5 equ; 29 neg)
% 13.45/13.63 % Maximal clause size : 4 ( 2 avg)
% 13.45/13.63 % Maximal term depth : 1 ( 1 avg)
% 13.45/13.63 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 13.45/13.63 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% 13.45/13.63 % Number of variables : 44 ( 4 sgn)
% 13.45/13.63 % SPC : CNF_UNS_EPR_SEQ_NHN
% 13.45/13.63
% 13.45/13.63 % Comments : See MGT042+1.p for the mnemonic names.
% 13.45/13.63 % : Created with tptp2X -f tptp -t clausify:otter MGT053+1.p
% 13.45/13.63 %--------------------------------------------------------------------------
% 13.45/13.63 include('Axioms/MGT001-0.ax').
% 13.45/13.63 %--------------------------------------------------------------------------
% 13.45/13.63 cnf(definition_2_29,axiom,
% 13.45/13.63 ( ~ dissimilar(A,B,C)
% 13.45/13.63 | organization(A) ) ).
% 13.45/13.63
% 13.45/13.63 cnf(definition_2_30,axiom,
% 13.45/13.64 ( ~ dissimilar(A,B,C)
% 13.45/13.64 | is_aligned(A,B)
% 13.45/13.64 | is_aligned(A,C) ) ).
% 13.45/13.64
% 13.45/13.64 cnf(definition_2_31,axiom,
% 13.45/13.64 ( ~ dissimilar(A,B,C)
% 13.45/13.64 | ~ is_aligned(A,B)
% 13.45/13.64 | ~ is_aligned(A,C) ) ).
% 13.45/13.64
% 13.45/13.64 cnf(definition_2_32,axiom,
% 13.45/13.64 ( ~ organization(A)
% 13.45/13.64 | ~ is_aligned(A,B)
% 13.45/13.64 | is_aligned(A,B)
% 13.45/13.64 | dissimilar(A,B,C) ) ).
% 13.45/13.64
% 13.45/13.64 cnf(definition_2_33,axiom,
% 13.45/13.64 ( ~ organization(A)
% 13.45/13.64 | ~ is_aligned(A,B)
% 13.45/13.64 | is_aligned(A,C)
% 13.45/13.64 | dissimilar(A,B,C) ) ).
% 13.45/13.64
% 13.45/13.64 cnf(definition_2_34,axiom,
% 13.45/13.64 ( ~ organization(A)
% 13.45/13.64 | ~ is_aligned(A,B)
% 13.45/13.64 | is_aligned(A,C)
% 13.45/13.64 | dissimilar(A,C,B) ) ).
% 13.45/13.64
% 13.45/13.64 cnf(definition_2_35,axiom,
% 13.45/13.64 ( ~ organization(A)
% 13.45/13.64 | ~ is_aligned(A,B)
% 13.45/13.64 | is_aligned(A,B)
% 13.45/13.64 | dissimilar(A,C,B) ) ).
% 13.45/13.64
% 13.45/13.64 cnf(lemma_7_36,negated_conjecture,
% 13.45/13.64 ( dissimilar(sk1,sk2,sk3)
% 13.45/13.64 | dissimilar(sk1,sk3,sk2) ) ).
% 13.45/13.64
% 13.45/13.64 cnf(lemma_7_37,negated_conjecture,
% 13.45/13.64 ( dissimilar(sk1,sk2,sk3)
% 13.45/13.64 | ~ dissimilar(sk1,sk2,sk3) ) ).
% 13.45/13.64
% 13.45/13.64 cnf(lemma_7_38,negated_conjecture,
% 13.45/13.64 ( ~ dissimilar(sk1,sk3,sk2)
% 13.45/13.64 | dissimilar(sk1,sk3,sk2) ) ).
% 13.45/13.64
% 13.45/13.64 cnf(lemma_7_39,negated_conjecture,
% 13.45/13.64 ( ~ dissimilar(sk1,sk3,sk2)
% 13.45/13.64 | ~ dissimilar(sk1,sk2,sk3) ) ).
% 13.45/13.64
% 13.45/13.64 %--------------------------------------------------------------------------
% 13.45/13.64 %-------------------------------------------
% 13.45/13.64 % Proof found
% 13.45/13.64 % SZS status Theorem for theBenchmark
% 13.45/13.64 % SZS output start Proof
% 13.45/13.64 %ClaNum:35(EqnAxiom:17)
% 13.45/13.64 %VarNum:86(SingletonVarNum:38)
% 13.45/13.64 %MaxLitNum:4
% 13.45/13.64 %MaxfuncDepth:0
% 13.45/13.64 %SharedTerms:7
% 13.45/13.64 %goalClause: 32 35
% 13.45/13.64 [32]P4(a1,a2,a3)+P4(a1,a3,a2)
% 13.45/13.64 [35]~P4(a1,a2,a3)+~P4(a1,a3,a2)
% 13.45/13.64 [18]~E(x181,x182)+P1(x181,x182)
% 13.45/13.64 [19]~E(x191,x192)+P2(x191,x192)
% 13.45/13.64 [21]~P5(x211,x212)+P1(x211,x212)
% 13.45/13.64 [22]~P3(x222,x221)+P5(x221,x222)
% 13.45/13.64 [23]~P3(x231,x232)+P2(x231,x232)
% 13.45/13.64 [24]~P5(x242,x241)+P3(x241,x242)
% 13.45/13.64 [27]~P3(x272,x271)+~P3(x271,x272)
% 13.45/13.64 [29]P6(x291)+~P4(x291,x292,x293)
% 13.45/13.64 [20]P5(x201,x202)+P3(x201,x202)+E(x201,x202)
% 13.45/13.64 [25]P5(x251,x252)+~P1(x251,x252)+E(x251,x252)
% 13.45/13.64 [26]P3(x261,x262)+~P2(x261,x262)+E(x261,x262)
% 13.45/13.64 [28]~P3(x281,x283)+P3(x281,x282)+~P3(x283,x282)
% 13.45/13.64 [33]~P4(x331,x333,x332)+P7(x331,x332)+P7(x331,x333)
% 13.45/13.64 [34]~P4(x341,x343,x342)+~P7(x341,x342)+~P7(x341,x343)
% 13.45/13.64 [30]~P6(x301)+~P7(x301,x303)+P7(x301,x302)+P4(x301,x302,x303)
% 13.45/13.64 [31]~P6(x311)+~P7(x311,x313)+P7(x311,x312)+P4(x311,x313,x312)
% 13.45/13.64 %EqnAxiom
% 13.45/13.64 [1]E(x11,x11)
% 13.45/13.64 [2]E(x22,x21)+~E(x21,x22)
% 13.45/13.64 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 13.45/13.64 [4]P1(x42,x43)+~E(x41,x42)+~P1(x41,x43)
% 13.45/13.64 [5]P1(x53,x52)+~E(x51,x52)+~P1(x53,x51)
% 13.45/13.64 [6]P2(x62,x63)+~E(x61,x62)+~P2(x61,x63)
% 13.45/13.64 [7]P2(x73,x72)+~E(x71,x72)+~P2(x73,x71)
% 13.45/13.64 [8]P5(x82,x83)+~E(x81,x82)+~P5(x81,x83)
% 13.45/13.64 [9]P5(x93,x92)+~E(x91,x92)+~P5(x93,x91)
% 13.45/13.64 [10]P3(x102,x103)+~E(x101,x102)+~P3(x101,x103)
% 13.45/13.64 [11]P3(x113,x112)+~E(x111,x112)+~P3(x113,x111)
% 13.45/13.64 [12]P4(x122,x123,x124)+~E(x121,x122)+~P4(x121,x123,x124)
% 13.45/13.64 [13]P4(x133,x132,x134)+~E(x131,x132)+~P4(x133,x131,x134)
% 13.45/13.64 [14]P4(x143,x144,x142)+~E(x141,x142)+~P4(x143,x144,x141)
% 13.45/13.64 [15]P7(x152,x153)+~E(x151,x152)+~P7(x151,x153)
% 13.45/13.64 [16]P7(x163,x162)+~E(x161,x162)+~P7(x163,x161)
% 13.45/13.64 [17]~P6(x171)+P6(x172)+~E(x171,x172)
% 13.45/13.64
% 13.45/13.64 %-------------------------------------------
% 13.45/13.64 cnf(247,plain,
% 13.45/13.64 (P6(a1)+P4(a1,a2,a3)),
% 13.45/13.64 inference(scs_inference,[],[29,32])).
% 13.45/13.64 cnf(248,plain,
% 13.45/13.64 (P6(a1)),
% 13.45/13.64 inference(scs_inference,[],[247,29])).
% 13.45/13.64 cnf(312,plain,
% 13.45/13.64 (P7(a1,a3)+P7(a1,a2)+P4(a1,a3,a2)),
% 13.45/13.64 inference(scs_inference,[],[32,33])).
% 13.45/13.64 cnf(313,plain,
% 13.45/13.64 (P7(a1,a2)+P7(a1,a3)),
% 13.45/13.64 inference(scs_inference,[],[312,33])).
% 13.45/13.64 cnf(321,plain,
% 13.45/13.64 (P4(a1,x3211,a2)+P7(a1,x3211)+P7(a1,a3)),
% 13.45/13.64 inference(scs_inference,[],[248,313,30])).
% 13.45/13.64 cnf(326,plain,
% 13.45/13.64 (P4(a1,a3,x3261)+P7(a1,x3261)+P7(a1,a2)),
% 13.45/13.64 inference(scs_inference,[],[248,313,31])).
% 13.45/13.64 cnf(341,plain,
% 13.45/13.64 (P4(a1,a2,x3411)+P7(a1,x3411)+P7(a1,a3)),
% 13.45/13.64 inference(scs_inference,[],[248,313,31])).
% 13.45/13.64 cnf(345,plain,
% 13.45/13.64 (P4(a1,x3451,a3)+P7(a1,x3451)+P7(a1,a2)),
% 13.45/13.64 inference(scs_inference,[],[248,313,30])).
% 13.45/13.64 cnf(912,plain,
% 13.45/13.64 (~P7(a1,a2)+~P7(a1,a3)+P4(a1,a2,a3)),
% 13.45/13.64 inference(scs_inference,[],[32,34])).
% 13.45/13.64 cnf(913,plain,
% 13.45/13.64 (~P7(a1,a3)+~P7(a1,a2)),
% 13.45/13.64 inference(scs_inference,[],[912,34])).
% 13.45/13.64 cnf(923,plain,
% 13.45/13.64 (~P7(a1,a3)+P4(a1,a3,a2)),
% 13.45/13.64 inference(scs_inference,[],[913,326])).
% 13.45/13.64 cnf(931,plain,
% 13.45/13.64 (~P7(a1,a2)+P4(a1,a3,a2)),
% 13.45/13.64 inference(scs_inference,[],[913,321])).
% 13.45/13.64 cnf(932,plain,
% 13.45/13.64 (~P7(a1,a2)+~P4(a1,a2,a3)),
% 13.45/13.64 inference(scs_inference,[],[931,35])).
% 13.45/13.64 cnf(933,plain,
% 13.45/13.64 (P7(a1,a3)+~P4(a1,a2,a3)),
% 13.45/13.64 inference(scs_inference,[],[932,313])).
% 13.45/13.64 cnf(934,plain,
% 13.45/13.64 (P4(a1,a3,a2)+~P4(a1,a2,a3)),
% 13.45/13.64 inference(scs_inference,[],[933,923])).
% 13.45/13.64 cnf(935,plain,
% 13.45/13.64 (~P4(a1,a2,a3)),
% 13.45/13.64 inference(scs_inference,[],[934,35])).
% 13.45/13.64 cnf(948,plain,
% 13.45/13.64 ($false),
% 13.45/13.64 inference(scs_inference,[],[935,341,345,913]),
% 13.45/13.64 ['proof']).
% 13.45/13.64 % SZS output end Proof
% 13.45/13.64 % Total time :13.134973s
%------------------------------------------------------------------------------