%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT089+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n004.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.28s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT089+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.06/0.34 % Computer : n004.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Mon Sep 7 14:00:15 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.28/0.51 start to proof:theBenchmark
% 0.28/0.51 %-------------------------------------------
% 0.28/0.51 % File :CSE---1.7
% 0.28/0.51 % Problem :theBenchmark
% 0.28/0.51 % Transform :cnf
% 0.28/0.51 % Format :tptp:raw
% 0.28/0.51 % Command :java -jar mcs_scs.jar %d %s
% 0.28/0.51
% 0.28/0.51 % Result :Theorem 0.005418s
% 0.28/0.51 % Output :CNFRefutation 0.005418s
% 0.28/0.51 %-------------------------------------------
% 0.28/0.51 %--------------------------------------------------------------------------
% 0.28/0.51 % File : MGT089+1 : TPTP v9.3.0. Released v9.3.0.
% 0.28/0.51 % Domain : Management
% 0.28/0.51 % Problem : prec_oo: leq(U,L) implies prec(U,L,o,o)
% 0.28/0.51 % Version : Especial.
% 0.28/0.51 % English : Criterion prec_oo: leq(v5,v5) => prec(v5,v5,o,o)
% 0.28/0.51 % Both endpoints open: equal value is enough for separation.
% 0.28/0.51
% 0.28/0.51 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 0.28/0.51 % Source : [MC+26]
% 0.28/0.51 % Names : ODRL604-1.p [MC+26]
% 0.28/0.51
% 0.28/0.51 % Status : Theorem
% 0.28/0.51 % Rating : 0.04 v9.3.0
% 0.28/0.51 % Syntax : Number of formulae : 48 ( 22 unt; 0 def)
% 0.28/0.51 % Number of atoms : 106 ( 26 equ)
% 0.28/0.51 % Maximal formula atoms : 7 ( 2 avg)
% 0.28/0.51 % Number of connectives : 66 ( 8 ~; 11 |; 21 &)
% 0.28/0.51 % ( 13 <=>; 13 =>; 0 <=; 0 <~>)
% 0.28/0.51 % Maximal formula depth : 11 ( 4 avg)
% 0.28/0.51 % Maximal term depth : 2 ( 1 avg)
% 0.28/0.51 % Number of predicates : 17 ( 16 usr; 0 prp; 1-8 aty)
% 0.28/0.51 % Number of functors : 12 ( 12 usr; 11 con; 0-2 aty)
% 0.28/0.51 % Number of variables : 74 ( 72 !; 2 ?)
% 0.28/0.51 % SPC : FOF_THM_RFO_SEQ
% 0.28/0.51
% 0.28/0.51 % Comments : Requires MGT002+0.ax + MGT002+2.ax.
% 0.28/0.51 %--------------------------------------------------------------------------
% 0.28/0.51 include('Axioms/MGT002+0.ax').
% 0.28/0.51 include('Axioms/MGT002+2.ax').
% 0.28/0.51 include('Axioms/MGT002+5.ax').
% 0.28/0.51 %--------------------------------------------------------------------------
% 0.28/0.51 %----Named constants and ordering
% 0.28/0.51 fof(val_v5,axiom,
% 0.28/0.51 val(v5) ).
% 0.28/0.51
% 0.28/0.51 fof(odrl604,conjecture,
% 0.28/0.51 prec(v5,v5,o,o) ).
% 0.28/0.51
% 0.28/0.51 %--------------------------------------------------------------------------
% 0.28/0.51 %-------------------------------------------
% 0.28/0.51 % Proof found
% 0.28/0.51 % SZS status Theorem for theBenchmark
% 0.28/0.51 % SZS output start Proof
% 0.28/0.51 %ClaNum:136(EqnAxiom:64)
% 0.28/0.51 %VarNum:327(SingletonVarNum:152)
% 0.28/0.51 %MaxLitNum:6
% 0.28/0.51 %MaxfuncDepth:1
% 0.28/0.51 %SharedTerms:32
% 0.28/0.51 %goalClause: 86
% 0.28/0.51 %singleGoalClaCount:1
% 0.28/0.51 [65]P1(a1)
% 0.28/0.51 [66]P1(a2)
% 0.28/0.51 [67]P1(a5)
% 0.28/0.51 [68]P2(a3)
% 0.28/0.51 [69]P2(a6)
% 0.28/0.51 [70]P11(a15)
% 0.28/0.51 [71]P12(a7,a3)
% 0.28/0.51 [72]P12(a8,a3)
% 0.28/0.51 [73]P12(a9,a3)
% 0.28/0.51 [74]P12(a14,a3)
% 0.28/0.51 [75]P12(a10,a6)
% 0.28/0.51 [76]P15(a7,a3)
% 0.28/0.51 [77]P15(a8,a3)
% 0.28/0.51 [78]P15(a9,a3)
% 0.28/0.51 [79]P15(a14,a6)
% 0.28/0.51 [80]P15(a10,a3)
% 0.28/0.51 [81]~E(a1,a2)
% 0.28/0.51 [82]~E(a1,a5)
% 0.28/0.51 [83]~E(a5,a2)
% 0.28/0.51 [84]~E(a6,a3)
% 0.28/0.51 [86]~P16(a15,a15,a6,a6)
% 0.28/0.51 [85]~P13(x851,x851)
% 0.28/0.51 [89]~E(x891,x892)+P14(x891,x892)
% 0.28/0.51 [97]~P13(x971,x972)+P14(x971,x972)
% 0.28/0.51 [117]~P13(x1171,x1172)+P16(x1171,x1172,a3,a3)
% 0.28/0.51 [118]~P14(x1181,x1182)+P16(x1181,x1182,a3,a6)
% 0.28/0.51 [119]~P14(x1191,x1192)+P16(x1191,x1192,a6,a3)
% 0.28/0.51 [120]~P14(x1201,x1202)+P16(x1201,x1202,a6,a6)
% 0.28/0.51 [121]P13(x1211,x1212)+~P16(x1211,x1212,a3,a3)
% 0.28/0.51 [122]P14(x1221,x1222)+~P16(x1221,x1222,a3,a6)
% 0.28/0.51 [123]P14(x1231,x1232)+~P16(x1231,x1232,a6,a3)
% 0.28/0.51 [124]P14(x1241,x1242)+~P16(x1241,x1242,a6,a6)
% 0.28/0.51 [109]P13(x1091,x1092)+~P8(x1092,x1091,x1093)
% 0.28/0.51 [110]P13(x1101,x1102)+~P9(x1101,x1103,x1102)
% 0.28/0.51 [111]P13(x1111,x1112)+~P10(x1112,x1111,x1113)
% 0.28/0.51 [112]P13(x1121,x1122)+~P10(x1121,x1123,x1122)
% 0.28/0.51 [113]P14(x1131,x1132)+~P3(x1132,x1131,x1133)
% 0.28/0.51 [114]P14(x1141,x1142)+~P3(x1141,x1143,x1142)
% 0.28/0.51 [115]P14(x1151,x1152)+~P8(x1151,x1153,x1152)
% 0.28/0.51 [116]P14(x1161,x1162)+~P9(x1162,x1161,x1163)
% 0.28/0.51 [128]P6(x1281,x1282,x1283,x1284)+P3(f11(x1281,x1282,x1283,x1284),x1283,x1284)
% 0.28/0.51 [129]P6(x1291,x1292,x1293,x1294)+P3(f11(x1291,x1292,x1293,x1294),x1291,x1292)
% 0.28/0.51 [130]P5(x1301,x1302,x1303,x1304)+P3(f12(x1301,x1302,x1303,x1304),x1301,x1302)
% 0.28/0.51 [131]~P4(x1311,x1312,x1313,x1314)+P3(f13(x1311,x1312,x1313,x1314),x1313,x1314)
% 0.28/0.51 [132]~P4(x1321,x1322,x1323,x1324)+P3(f13(x1321,x1322,x1323,x1324),x1321,x1322)
% 0.28/0.51 [133]P5(x1331,x1332,x1333,x1334)+~P3(f12(x1331,x1332,x1333,x1334),x1333,x1334)
% 0.28/0.51 [134]~P16(x1342,x1345,x1344,x1347)+P7(x1341,x1342,x1343,x1344,x1345,x1346,x1347,x1348)
% 0.28/0.51 [135]~P16(x1356,x1351,x1358,x1353)+P7(x1351,x1352,x1353,x1354,x1355,x1356,x1357,x1358)
% 0.28/0.51 [87]~P2(x871)+E(x871,a6)+E(x871,a3)
% 0.28/0.51 [90]P13(x902,x901)+P13(x901,x902)+E(x901,x902)
% 0.28/0.51 [98]P13(x981,x982)+~P14(x981,x982)+E(x981,x982)
% 0.28/0.51 [99]~P14(x992,x991)+~P14(x991,x992)+E(x991,x992)
% 0.28/0.51 [101]~P13(x1011,x1013)+P13(x1011,x1012)+~P13(x1013,x1012)
% 0.28/0.51 [102]~P14(x1021,x1023)+P13(x1021,x1022)+~P13(x1023,x1022)
% 0.28/0.51 [103]~P14(x1033,x1032)+P13(x1031,x1032)+~P13(x1031,x1033)
% 0.28/0.51 [104]~P14(x1041,x1043)+P14(x1041,x1042)+~P14(x1043,x1042)
% 0.28/0.51 [105]~P14(x1051,x1053)+~P14(x1052,x1051)+P3(x1051,x1052,x1053)
% 0.28/0.51 [106]~P13(x1062,x1061)+~P14(x1061,x1063)+P8(x1061,x1062,x1063)
% 0.28/0.51 [107]~P13(x1071,x1073)+~P14(x1072,x1071)+P9(x1071,x1072,x1073)
% 0.28/0.51 [108]~P13(x1081,x1083)+~P13(x1082,x1081)+P10(x1081,x1082,x1083)
% 0.28/0.51 [125]~P3(x1255,x1251,x1252)+P4(x1251,x1252,x1253,x1254)+~P3(x1255,x1253,x1254)
% 0.28/0.51 [126]~P5(x1264,x1265,x1262,x1263)+P3(x1261,x1262,x1263)+~P3(x1261,x1264,x1265)
% 0.28/0.51 [127]~P6(x1274,x1275,x1272,x1273)+~P3(x1271,x1272,x1273)+~P3(x1271,x1274,x1275)
% 0.28/0.51 [136]~P7(x1362,x1365,x1364,x1367,x1366,x1361,x1368,x1363)+P16(x1361,x1362,x1363,x1364)+P16(x1365,x1366,x1367,x1368)
% 0.28/0.51 [88]~P1(x881)+E(x881,a2)+E(x881,a5)+E(x881,a1)
% 0.28/0.52 [91]~P1(x911)+~P1(x912)+~E(x912,a1)+E(f4(x911,x912),a1)
% 0.28/0.52 [92]~P1(x922)+~P1(x921)+~E(x921,a1)+E(f4(x921,x922),a1)
% 0.28/0.52 [93]~P1(x932)+~P1(x931)+~E(x932,a2)+~E(x931,a2)+E(f4(x931,x932),a2)
% 0.28/0.52 [100]~P1(x1002)+~P1(x1001)+E(f4(x1001,x1002),a1)+E(f4(x1001,x1002),a2)+E(f4(x1001,x1002),a5)
% 0.28/0.52 [94]~P1(x941)+~P1(x942)+~E(x942,a5)+E(x941,a1)+E(x942,a1)+E(f4(x941,x942),a5)
% 0.28/0.52 [95]~P1(x951)+~P1(x952)+~E(x952,a5)+E(x951,a1)+E(x952,a1)+E(f4(x952,x951),a5)
% 0.28/0.52 %EqnAxiom
% 0.28/0.52 [1]E(x11,x11)
% 0.28/0.52 [2]E(x22,x21)+~E(x21,x22)
% 0.28/0.52 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.28/0.52 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 0.28/0.52 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 0.28/0.52 [6]~E(x61,x62)+E(f12(x61,x63,x64,x65),f12(x62,x63,x64,x65))
% 0.28/0.52 [7]~E(x71,x72)+E(f12(x73,x71,x74,x75),f12(x73,x72,x74,x75))
% 0.28/0.52 [8]~E(x81,x82)+E(f12(x83,x84,x81,x85),f12(x83,x84,x82,x85))
% 0.28/0.52 [9]~E(x91,x92)+E(f12(x93,x94,x95,x91),f12(x93,x94,x95,x92))
% 0.28/0.52 [10]~E(x101,x102)+E(f13(x101,x103,x104,x105),f13(x102,x103,x104,x105))
% 0.28/0.52 [11]~E(x111,x112)+E(f13(x113,x111,x114,x115),f13(x113,x112,x114,x115))
% 0.28/0.52 [12]~E(x121,x122)+E(f13(x123,x124,x121,x125),f13(x123,x124,x122,x125))
% 0.28/0.52 [13]~E(x131,x132)+E(f13(x133,x134,x135,x131),f13(x133,x134,x135,x132))
% 0.28/0.52 [14]~E(x141,x142)+E(f11(x141,x143,x144,x145),f11(x142,x143,x144,x145))
% 0.28/0.52 [15]~E(x151,x152)+E(f11(x153,x151,x154,x155),f11(x153,x152,x154,x155))
% 0.28/0.52 [16]~E(x161,x162)+E(f11(x163,x164,x161,x165),f11(x163,x164,x162,x165))
% 0.28/0.52 [17]~E(x171,x172)+E(f11(x173,x174,x175,x171),f11(x173,x174,x175,x172))
% 0.28/0.52 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 0.28/0.52 [19]P7(x192,x193,x194,x195,x196,x197,x198,x199)+~E(x191,x192)+~P7(x191,x193,x194,x195,x196,x197,x198,x199)
% 0.28/0.52 [20]P7(x203,x202,x204,x205,x206,x207,x208,x209)+~E(x201,x202)+~P7(x203,x201,x204,x205,x206,x207,x208,x209)
% 0.28/0.52 [21]P7(x213,x214,x212,x215,x216,x217,x218,x219)+~E(x211,x212)+~P7(x213,x214,x211,x215,x216,x217,x218,x219)
% 0.28/0.52 [22]P7(x223,x224,x225,x222,x226,x227,x228,x229)+~E(x221,x222)+~P7(x223,x224,x225,x221,x226,x227,x228,x229)
% 0.28/0.52 [23]P7(x233,x234,x235,x236,x232,x237,x238,x239)+~E(x231,x232)+~P7(x233,x234,x235,x236,x231,x237,x238,x239)
% 0.28/0.52 [24]P7(x243,x244,x245,x246,x247,x242,x248,x249)+~E(x241,x242)+~P7(x243,x244,x245,x246,x247,x241,x248,x249)
% 0.28/0.52 [25]P7(x253,x254,x255,x256,x257,x258,x252,x259)+~E(x251,x252)+~P7(x253,x254,x255,x256,x257,x258,x251,x259)
% 0.28/0.52 [26]P7(x263,x264,x265,x266,x267,x268,x269,x262)+~E(x261,x262)+~P7(x263,x264,x265,x266,x267,x268,x269,x261)
% 0.28/0.52 [27]P16(x272,x273,x274,x275)+~E(x271,x272)+~P16(x271,x273,x274,x275)
% 0.28/0.52 [28]P16(x283,x282,x284,x285)+~E(x281,x282)+~P16(x283,x281,x284,x285)
% 0.28/0.52 [29]P16(x293,x294,x292,x295)+~E(x291,x292)+~P16(x293,x294,x291,x295)
% 0.28/0.52 [30]P16(x303,x304,x305,x302)+~E(x301,x302)+~P16(x303,x304,x305,x301)
% 0.28/0.52 [31]~P2(x311)+P2(x312)+~E(x311,x312)
% 0.28/0.52 [32]P14(x322,x323)+~E(x321,x322)+~P14(x321,x323)
% 0.28/0.52 [33]P14(x333,x332)+~E(x331,x332)+~P14(x333,x331)
% 0.28/0.52 [34]~P11(x341)+P11(x342)+~E(x341,x342)
% 0.28/0.52 [35]P12(x352,x353)+~E(x351,x352)+~P12(x351,x353)
% 0.28/0.52 [36]P12(x363,x362)+~E(x361,x362)+~P12(x363,x361)
% 0.28/0.52 [37]P13(x372,x373)+~E(x371,x372)+~P13(x371,x373)
% 0.28/0.52 [38]P13(x383,x382)+~E(x381,x382)+~P13(x383,x381)
% 0.28/0.52 [39]P9(x392,x393,x394)+~E(x391,x392)+~P9(x391,x393,x394)
% 0.28/0.52 [40]P9(x403,x402,x404)+~E(x401,x402)+~P9(x403,x401,x404)
% 0.28/0.52 [41]P9(x413,x414,x412)+~E(x411,x412)+~P9(x413,x414,x411)
% 0.28/0.52 [42]P10(x422,x423,x424)+~E(x421,x422)+~P10(x421,x423,x424)
% 0.28/0.52 [43]P10(x433,x432,x434)+~E(x431,x432)+~P10(x433,x431,x434)
% 0.28/0.52 [44]P10(x443,x444,x442)+~E(x441,x442)+~P10(x443,x444,x441)
% 0.28/0.52 [45]P8(x452,x453,x454)+~E(x451,x452)+~P8(x451,x453,x454)
% 0.28/0.52 [46]P8(x463,x462,x464)+~E(x461,x462)+~P8(x463,x461,x464)
% 0.28/0.52 [47]P8(x473,x474,x472)+~E(x471,x472)+~P8(x473,x474,x471)
% 0.28/0.52 [48]P15(x482,x483)+~E(x481,x482)+~P15(x481,x483)
% 0.28/0.52 [49]P15(x493,x492)+~E(x491,x492)+~P15(x493,x491)
% 0.28/0.52 [50]P3(x502,x503,x504)+~E(x501,x502)+~P3(x501,x503,x504)
% 0.28/0.52 [51]P3(x513,x512,x514)+~E(x511,x512)+~P3(x513,x511,x514)
% 0.28/0.52 [52]P3(x523,x524,x522)+~E(x521,x522)+~P3(x523,x524,x521)
% 0.28/0.52 [53]P5(x532,x533,x534,x535)+~E(x531,x532)+~P5(x531,x533,x534,x535)
% 0.28/0.52 [54]P5(x543,x542,x544,x545)+~E(x541,x542)+~P5(x543,x541,x544,x545)
% 0.28/0.52 [55]P5(x553,x554,x552,x555)+~E(x551,x552)+~P5(x553,x554,x551,x555)
% 0.28/0.52 [56]P5(x563,x564,x565,x562)+~E(x561,x562)+~P5(x563,x564,x565,x561)
% 0.28/0.52 [57]P4(x572,x573,x574,x575)+~E(x571,x572)+~P4(x571,x573,x574,x575)
% 0.28/0.52 [58]P4(x583,x582,x584,x585)+~E(x581,x582)+~P4(x583,x581,x584,x585)
% 0.28/0.52 [59]P4(x593,x594,x592,x595)+~E(x591,x592)+~P4(x593,x594,x591,x595)
% 0.28/0.52 [60]P4(x603,x604,x605,x602)+~E(x601,x602)+~P4(x603,x604,x605,x601)
% 0.28/0.52 [61]P6(x612,x613,x614,x615)+~E(x611,x612)+~P6(x611,x613,x614,x615)
% 0.28/0.52 [62]P6(x623,x622,x624,x625)+~E(x621,x622)+~P6(x623,x621,x624,x625)
% 0.28/0.52 [63]P6(x633,x634,x632,x635)+~E(x631,x632)+~P6(x633,x634,x631,x635)
% 0.28/0.52 [64]P6(x643,x644,x645,x642)+~E(x641,x642)+~P6(x643,x644,x645,x641)
% 0.28/0.52
% 0.28/0.52 %-------------------------------------------
% 0.28/0.52 cnf(137,plain,
% 0.28/0.52 (P14(x1371,x1371)),
% 0.28/0.52 inference(equality_inference,[],[89])).
% 0.28/0.52 cnf(142,plain,
% 0.28/0.52 ($false),
% 0.28/0.52 inference(scs_inference,[],[137,86,120]),
% 0.28/0.52 ['proof']).
% 0.28/0.52 % SZS output end Proof
% 0.28/0.52 % Total time :0.005418s
%------------------------------------------------------------------------------