%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT093+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n013.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:24 AM UTC 2026
% Result : Theorem 0.25s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT093+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n013.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 14:00:35 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.25/0.52 start to proof:theBenchmark
% 0.25/0.53 %-------------------------------------------
% 0.25/0.53 % File :CSE---1.7
% 0.25/0.53 % Problem :theBenchmark
% 0.25/0.53 % Transform :cnf
% 0.25/0.53 % Format :tptp:raw
% 0.25/0.53 % Command :java -jar mcs_scs.jar %d %s
% 0.25/0.53
% 0.25/0.53 % Result :Theorem 0.023696s
% 0.25/0.53 % Output :CNFRefutation 0.023696s
% 0.25/0.53 %-------------------------------------------
% 0.25/0.53 %--------------------------------------------------------------------------
% 0.25/0.53 % File : MGT093+1 : TPTP v9.3.0. Released v9.3.0.
% 0.25/0.53 % Domain : Management
% 0.25/0.53 % Problem : One match compatible rest conflict => xone=compatible
% 0.25/0.53 % Version : Especial.
% 0.25/0.53 % English : composition xone_compat: xone_verdict(compatible, conflict) =
% 0.25/0.53 % compatible. Exactly one branch pair overlaps, rest conflict
% 0.25/0.53 % (Vr=MAX of rest=conflict).
% 0.25/0.53
% 0.25/0.53 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 0.25/0.53 % Source : [MC+26]
% 0.25/0.53 % Names : ODRL644-1.p [MC+26]
% 0.25/0.53
% 0.25/0.53 % Status : Theorem
% 0.25/0.53 % Rating : 0.00 v9.3.0
% 0.25/0.53 % Syntax : Number of formulae : 37 ( 8 unt; 0 def)
% 0.25/0.53 % Number of atoms : 130 ( 52 equ)
% 0.25/0.53 % Maximal formula atoms : 8 ( 3 avg)
% 0.25/0.53 % Number of connectives : 106 ( 13 ~; 16 |; 48 &)
% 0.25/0.53 % ( 8 <=>; 21 =>; 0 <=; 0 <~>)
% 0.25/0.53 % Maximal formula depth : 14 ( 6 avg)
% 0.25/0.53 % Maximal term depth : 2 ( 1 avg)
% 0.25/0.53 % Number of predicates : 11 ( 10 usr; 0 prp; 1-4 aty)
% 0.25/0.53 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% 0.25/0.53 % Number of variables : 82 ( 79 !; 3 ?)
% 0.25/0.53 % SPC : FOF_THM_RFO_SEQ
% 0.25/0.53
% 0.25/0.53 % Comments : Requires MGT002+0.ax + MGT002+2.ax.
% 0.25/0.53 %--------------------------------------------------------------------------
% 0.25/0.53 include('Axioms/MGT002+0.ax').
% 0.25/0.53 include('Axioms/MGT002+3.ax').
% 0.25/0.53 include('Axioms/MGT002+2.ax').
% 0.25/0.53 %--------------------------------------------------------------------------
% 0.25/0.53 %----Named constants and ordering
% 0.25/0.53 fof(odrl644,conjecture,
% 0.25/0.53 xone_verdict(compatible,conflict) = compatible ).
% 0.25/0.53
% 0.25/0.53 %--------------------------------------------------------------------------
% 0.25/0.53 %-------------------------------------------
% 0.25/0.53 % Proof found
% 0.25/0.53 % SZS status Theorem for theBenchmark
% 0.25/0.53 % SZS output start Proof
% 0.25/0.53 %ClaNum:113(EqnAxiom:50)
% 0.25/0.53 %VarNum:321(SingletonVarNum:133)
% 0.25/0.53 %MaxLitNum:6
% 0.25/0.53 %MaxfuncDepth:1
% 0.25/0.53 %SharedTerms:11
% 0.25/0.53 %goalClause: 57
% 0.25/0.53 %singleGoalClaCount:1
% 0.25/0.53 [51]P1(a1)
% 0.25/0.53 [52]P1(a3)
% 0.25/0.53 [53]P1(a4)
% 0.25/0.53 [54]~E(a1,a3)
% 0.25/0.53 [55]~E(a1,a4)
% 0.25/0.53 [56]~E(a4,a3)
% 0.25/0.53 [57]~E(f9(a1,a3),a1)
% 0.25/0.53 [58]~P9(x581,x581)
% 0.25/0.53 [60]~E(x601,x602)+P10(x601,x602)
% 0.25/0.53 [79]~P9(x791,x792)+P10(x791,x792)
% 0.25/0.53 [93]P9(x931,x932)+~P6(x932,x931,x933)
% 0.25/0.53 [94]P9(x941,x942)+~P7(x941,x943,x942)
% 0.25/0.53 [95]P9(x951,x952)+~P8(x952,x951,x953)
% 0.25/0.53 [96]P9(x961,x962)+~P8(x961,x963,x962)
% 0.25/0.53 [97]P10(x971,x972)+~P2(x972,x971,x973)
% 0.25/0.53 [98]P10(x981,x982)+~P2(x981,x983,x982)
% 0.25/0.53 [99]P10(x991,x992)+~P6(x991,x993,x992)
% 0.25/0.53 [100]P10(x1001,x1002)+~P7(x1002,x1001,x1003)
% 0.25/0.53 [104]P5(x1041,x1042,x1043,x1044)+P2(f6(x1041,x1042,x1043,x1044),x1043,x1044)
% 0.25/0.53 [105]P5(x1051,x1052,x1053,x1054)+P2(f6(x1051,x1052,x1053,x1054),x1051,x1052)
% 0.25/0.53 [106]P4(x1061,x1062,x1063,x1064)+P2(f7(x1061,x1062,x1063,x1064),x1061,x1062)
% 0.25/0.53 [107]~P3(x1071,x1072,x1073,x1074)+P2(f8(x1071,x1072,x1073,x1074),x1073,x1074)
% 0.25/0.53 [108]~P3(x1081,x1082,x1083,x1084)+P2(f8(x1081,x1082,x1083,x1084),x1081,x1082)
% 0.25/0.53 [109]P4(x1091,x1092,x1093,x1094)+~P2(f7(x1091,x1092,x1093,x1094),x1093,x1094)
% 0.25/0.53 [62]P9(x622,x621)+P9(x621,x622)+E(x621,x622)
% 0.25/0.53 [80]P9(x801,x802)+~P10(x801,x802)+E(x801,x802)
% 0.25/0.53 [81]~P10(x812,x811)+~P10(x811,x812)+E(x811,x812)
% 0.25/0.53 [85]~P9(x851,x853)+P9(x851,x852)+~P9(x853,x852)
% 0.25/0.53 [86]~P10(x861,x863)+P9(x861,x862)+~P9(x863,x862)
% 0.25/0.53 [87]~P10(x873,x872)+P9(x871,x872)+~P9(x871,x873)
% 0.25/0.53 [88]~P10(x881,x883)+P10(x881,x882)+~P10(x883,x882)
% 0.25/0.53 [89]~P10(x891,x893)+~P10(x892,x891)+P2(x891,x892,x893)
% 0.25/0.53 [90]~P9(x902,x901)+~P10(x901,x903)+P6(x901,x902,x903)
% 0.25/0.53 [91]~P9(x911,x913)+~P10(x912,x911)+P7(x911,x912,x913)
% 0.25/0.53 [92]~P9(x921,x923)+~P9(x922,x921)+P8(x921,x922,x923)
% 0.25/0.53 [101]~P2(x1015,x1011,x1012)+P3(x1011,x1012,x1013,x1014)+~P2(x1015,x1013,x1014)
% 0.25/0.54 [102]~P4(x1024,x1025,x1022,x1023)+P2(x1021,x1022,x1023)+~P2(x1021,x1024,x1025)
% 0.25/0.54 [103]~P5(x1034,x1035,x1032,x1033)+~P2(x1031,x1032,x1033)+~P2(x1031,x1034,x1035)
% 0.25/0.54 [59]~P1(x591)+E(x591,a3)+E(x591,a4)+E(x591,a1)
% 0.25/0.54 [61]~P1(x612)+~P1(x611)+E(x611,a3)+E(f9(x612,x611),a4)
% 0.25/0.54 [63]~P1(x631)+~P1(x632)+~E(x632,a1)+E(f5(x631,x632),a1)
% 0.25/0.54 [64]~P1(x642)+~P1(x641)+~E(x641,a1)+E(f5(x641,x642),a1)
% 0.25/0.54 [65]~P1(x651)+~P1(x652)+~E(x652,a3)+E(f2(x651,x652),a3)
% 0.25/0.54 [66]~P1(x662)+~P1(x661)+~E(x661,a3)+E(f2(x661,x662),a3)
% 0.25/0.54 [69]~P1(x692)+~P1(x691)+E(x691,a3)+E(x691,a1)+E(f9(x691,x692),a4)
% 0.25/0.54 [72]~P1(x722)+~P1(x721)+~E(x722,a3)+~E(x721,a3)+E(f5(x721,x722),a3)
% 0.25/0.54 [73]~P1(x732)+~P1(x731)+~E(x732,a3)+~E(x731,a1)+E(f9(x731,x732),a1)
% 0.25/0.54 [74]~P1(x742)+~P1(x741)+~E(x742,a3)+~E(x741,a3)+E(f9(x741,x742),a3)
% 0.25/0.54 [75]~P1(x752)+~P1(x751)+~E(x752,a1)+~E(x751,a1)+E(f2(x751,x752),a1)
% 0.25/0.54 [82]~P1(x822)+~P1(x821)+E(f5(x821,x822),a1)+E(f5(x821,x822),a3)+E(f5(x821,x822),a4)
% 0.25/0.54 [83]~P1(x832)+~P1(x831)+E(f9(x831,x832),a1)+E(f9(x831,x832),a3)+E(f9(x831,x832),a4)
% 0.25/0.54 [84]~P1(x842)+~P1(x841)+E(f2(x841,x842),a1)+E(f2(x841,x842),a3)+E(f2(x841,x842),a4)
% 0.25/0.54 [70]~P1(x701)+~P1(x702)+E(x702,a3)+E(x701,a1)+E(x702,a1)+E(f5(x701,x702),a4)
% 0.25/0.54 [71]~P1(x711)+~P1(x712)+E(x712,a3)+E(x711,a1)+E(x712,a1)+E(f5(x712,x711),a4)
% 0.25/0.54 [76]~P1(x761)+~P1(x762)+~E(x762,a4)+E(x761,a3)+E(x762,a3)+E(f2(x761,x762),a4)
% 0.25/0.54 [77]~P1(x771)+~P1(x772)+~E(x772,a4)+E(x771,a3)+E(x772,a3)+E(f2(x772,x771),a4)
% 0.25/0.54 %EqnAxiom
% 0.25/0.54 [1]E(x11,x11)
% 0.25/0.54 [2]E(x22,x21)+~E(x21,x22)
% 0.25/0.54 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.25/0.54 [4]~E(x41,x42)+E(f9(x41,x43),f9(x42,x43))
% 0.25/0.54 [5]~E(x51,x52)+E(f9(x53,x51),f9(x53,x52))
% 0.25/0.54 [6]~E(x61,x62)+E(f7(x61,x63,x64,x65),f7(x62,x63,x64,x65))
% 0.25/0.54 [7]~E(x71,x72)+E(f7(x73,x71,x74,x75),f7(x73,x72,x74,x75))
% 0.25/0.54 [8]~E(x81,x82)+E(f7(x83,x84,x81,x85),f7(x83,x84,x82,x85))
% 0.25/0.54 [9]~E(x91,x92)+E(f7(x93,x94,x95,x91),f7(x93,x94,x95,x92))
% 0.25/0.54 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103))
% 0.25/0.54 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112))
% 0.25/0.54 [12]~E(x121,x122)+E(f2(x121,x123),f2(x122,x123))
% 0.25/0.54 [13]~E(x131,x132)+E(f2(x133,x131),f2(x133,x132))
% 0.25/0.54 [14]~E(x141,x142)+E(f6(x141,x143,x144,x145),f6(x142,x143,x144,x145))
% 0.25/0.54 [15]~E(x151,x152)+E(f6(x153,x151,x154,x155),f6(x153,x152,x154,x155))
% 0.25/0.54 [16]~E(x161,x162)+E(f6(x163,x164,x161,x165),f6(x163,x164,x162,x165))
% 0.25/0.54 [17]~E(x171,x172)+E(f6(x173,x174,x175,x171),f6(x173,x174,x175,x172))
% 0.25/0.54 [18]~E(x181,x182)+E(f8(x181,x183,x184,x185),f8(x182,x183,x184,x185))
% 0.25/0.54 [19]~E(x191,x192)+E(f8(x193,x191,x194,x195),f8(x193,x192,x194,x195))
% 0.25/0.54 [20]~E(x201,x202)+E(f8(x203,x204,x201,x205),f8(x203,x204,x202,x205))
% 0.25/0.54 [21]~E(x211,x212)+E(f8(x213,x214,x215,x211),f8(x213,x214,x215,x212))
% 0.25/0.54 [22]~P1(x221)+P1(x222)+~E(x221,x222)
% 0.25/0.54 [23]P5(x232,x233,x234,x235)+~E(x231,x232)+~P5(x231,x233,x234,x235)
% 0.25/0.54 [24]P5(x243,x242,x244,x245)+~E(x241,x242)+~P5(x243,x241,x244,x245)
% 0.25/0.54 [25]P5(x253,x254,x252,x255)+~E(x251,x252)+~P5(x253,x254,x251,x255)
% 0.25/0.54 [26]P5(x263,x264,x265,x262)+~E(x261,x262)+~P5(x263,x264,x265,x261)
% 0.25/0.54 [27]P2(x272,x273,x274)+~E(x271,x272)+~P2(x271,x273,x274)
% 0.25/0.54 [28]P2(x283,x282,x284)+~E(x281,x282)+~P2(x283,x281,x284)
% 0.25/0.54 [29]P2(x293,x294,x292)+~E(x291,x292)+~P2(x293,x294,x291)
% 0.25/0.54 [30]P9(x302,x303)+~E(x301,x302)+~P9(x301,x303)
% 0.25/0.54 [31]P9(x313,x312)+~E(x311,x312)+~P9(x313,x311)
% 0.25/0.54 [32]P6(x322,x323,x324)+~E(x321,x322)+~P6(x321,x323,x324)
% 0.25/0.54 [33]P6(x333,x332,x334)+~E(x331,x332)+~P6(x333,x331,x334)
% 0.25/0.54 [34]P6(x343,x344,x342)+~E(x341,x342)+~P6(x343,x344,x341)
% 0.25/0.54 [35]P10(x352,x353)+~E(x351,x352)+~P10(x351,x353)
% 0.25/0.54 [36]P10(x363,x362)+~E(x361,x362)+~P10(x363,x361)
% 0.25/0.54 [37]P4(x372,x373,x374,x375)+~E(x371,x372)+~P4(x371,x373,x374,x375)
% 0.25/0.54 [38]P4(x383,x382,x384,x385)+~E(x381,x382)+~P4(x383,x381,x384,x385)
% 0.25/0.54 [39]P4(x393,x394,x392,x395)+~E(x391,x392)+~P4(x393,x394,x391,x395)
% 0.25/0.54 [40]P4(x403,x404,x405,x402)+~E(x401,x402)+~P4(x403,x404,x405,x401)
% 0.25/0.54 [41]P3(x412,x413,x414,x415)+~E(x411,x412)+~P3(x411,x413,x414,x415)
% 0.25/0.54 [42]P3(x423,x422,x424,x425)+~E(x421,x422)+~P3(x423,x421,x424,x425)
% 0.25/0.54 [43]P3(x433,x434,x432,x435)+~E(x431,x432)+~P3(x433,x434,x431,x435)
% 0.25/0.54 [44]P3(x443,x444,x445,x442)+~E(x441,x442)+~P3(x443,x444,x445,x441)
% 0.25/0.54 [45]P7(x452,x453,x454)+~E(x451,x452)+~P7(x451,x453,x454)
% 0.25/0.54 [46]P7(x463,x462,x464)+~E(x461,x462)+~P7(x463,x461,x464)
% 0.25/0.54 [47]P7(x473,x474,x472)+~E(x471,x472)+~P7(x473,x474,x471)
% 0.25/0.54 [48]P8(x482,x483,x484)+~E(x481,x482)+~P8(x481,x483,x484)
% 0.25/0.54 [49]P8(x493,x492,x494)+~E(x491,x492)+~P8(x493,x491,x494)
% 0.25/0.54 [50]P8(x503,x504,x502)+~E(x501,x502)+~P8(x503,x504,x501)
% 0.25/0.54
% 0.25/0.54 %-------------------------------------------
% 0.25/0.54 cnf(153,plain,
% 0.25/0.54 ($false),
% 0.25/0.54 inference(scs_inference,[],[57,51,52,73]),
% 0.25/0.54 ['proof']).
% 0.25/0.54 % SZS output end Proof
% 0.25/0.54 % Total time :0.023696s
%------------------------------------------------------------------------------