%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT104+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n007.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:25 AM UTC 2026
% Result : Unsatisfiable 0.28s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT104+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n007.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 7 14:37:56 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.28/0.50 start to proof:theBenchmark
% 0.28/0.50 %-------------------------------------------
% 0.28/0.50 % File :CSE---1.7
% 0.28/0.50 % Problem :theBenchmark
% 0.28/0.50 % Transform :cnf
% 0.28/0.50 % Format :tptp:raw
% 0.28/0.50 % Command :java -jar mcs_scs.jar %d %s
% 0.28/0.50
% 0.28/0.50 % Result :Theorem 0.007069s
% 0.28/0.50 % Output :CNFRefutation 0.007069s
% 0.28/0.51 %-------------------------------------------
% 0.28/0.51 %--------------------------------------------------------------------------
% 0.28/0.51 % File : MGT104+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.28/0.51 % Domain : Management
% 0.28/0.51 % Problem : lt InfD violates wf condition (ii) - empty denotation
% 0.28/0.51 % Version : Especial.
% 0.28/0.51 % English : Intra-policy self-contradiction via wf_lt condition (ii).
% 0.28/0.51 % width lt v0 (infimum): [infD, v0) with v0=InfD => empty.
% 0.28/0.51 % def:profile condition (ii): op=lt => V != InfD.
% 0.28/0.51 % Violated: denotation is empty, policy is ill-formed.
% 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 : ODRL762-1.p [MC+26]
% 0.28/0.51
% 0.28/0.51 % Status : Unsatisfiable
% 0.28/0.51 % Rating : ? v9.3.1
% 0.28/0.51 % Syntax : Number of formulae : 58 ( 27 unt; 0 def)
% 0.28/0.51 % Number of atoms : 130 ( 41 equ)
% 0.28/0.51 % Maximal formula atoms : 7 ( 2 avg)
% 0.28/0.51 % Number of connectives : 92 ( 20 ~; 13 |; 28 &)
% 0.28/0.51 % ( 13 <=>; 18 =>; 0 <=; 0 <~>)
% 0.28/0.51 % Maximal formula depth : 9 ( 4 avg)
% 0.28/0.51 % Maximal term depth : 2 ( 1 avg)
% 0.28/0.51 % Number of predicates : 15 ( 14 usr; 0 prp; 1-4 aty)
% 0.28/0.51 % Number of functors : 11 ( 11 usr; 10 con; 0-2 aty)
% 0.28/0.51 % Number of variables : 88 ( 86 !; 2 ?)
% 0.28/0.51 % SPC : FOF_UNS_RFO_SEQ
% 0.28/0.51
% 0.28/0.51 % Comments : Intra-policy self-contradiction.
% 0.28/0.51 % Bugfixes : v9.3.1 - $distinct expanded to inequalities.
% 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+8.ax').
% 0.28/0.51 %--------------------------------------------------------------------------
% 0.28/0.51 %----Named constants and ordering
% 0.28/0.51 fof(val_v0,axiom,
% 0.28/0.51 val(v0) ).
% 0.28/0.51
% 0.28/0.51 fof(val_v1200,axiom,
% 0.28/0.51 val(v1200) ).
% 0.28/0.51
% 0.28/0.51 fof(ord_v0_v1200,axiom,
% 0.28/0.51 less(v0,v1200) ).
% 0.28/0.51
% 0.28/0.51 fof(distinct,axiom,
% 0.28/0.51 v0 != v1200 ).
% 0.28/0.51
% 0.28/0.51 fof(contradiction,axiom,
% 0.28/0.51 less(v0,v0) ).
% 0.28/0.51
% 0.28/0.51 %----No conjecture - contradiction in axioms
% 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:144(EqnAxiom:56)
% 0.28/0.51 %VarNum:387(SingletonVarNum:178)
% 0.28/0.51 %MaxLitNum:6
% 0.28/0.51 %MaxfuncDepth:1
% 0.28/0.51 %SharedTerms:36
% 0.28/0.51 [57]P1(a1)
% 0.28/0.51 [58]P1(a2)
% 0.28/0.51 [59]P1(a4)
% 0.28/0.51 [60]P2(a5)
% 0.28/0.51 [61]P2(a6)
% 0.28/0.51 [62]P2(a7)
% 0.28/0.51 [63]P2(a12)
% 0.28/0.51 [64]P2(a8)
% 0.28/0.51 [65]P10(a13)
% 0.28/0.51 [66]P10(a14)
% 0.28/0.51 [67]P11(a13,a13)
% 0.28/0.51 [68]P11(a13,a14)
% 0.28/0.51 [69]~E(a1,a2)
% 0.28/0.51 [70]~E(a1,a4)
% 0.28/0.51 [71]~E(a4,a2)
% 0.28/0.51 [72]~E(a6,a5)
% 0.28/0.51 [73]~E(a7,a5)
% 0.28/0.51 [74]~E(a7,a6)
% 0.28/0.51 [75]~E(a12,a5)
% 0.28/0.51 [76]~E(a12,a6)
% 0.28/0.51 [77]~E(a12,a7)
% 0.28/0.51 [78]~E(a8,a5)
% 0.28/0.51 [79]~E(a8,a6)
% 0.28/0.51 [80]~E(a8,a7)
% 0.28/0.51 [81]~E(a8,a12)
% 0.28/0.51 [82]~E(a14,a13)
% 0.28/0.51 [83]~P11(x831,x831)
% 0.28/0.51 [86]~E(x861,x862)+P12(x861,x862)
% 0.28/0.51 [94]~P11(x941,x942)+P12(x941,x942)
% 0.28/0.51 [106]P11(x1061,x1062)+~P7(x1062,x1061,x1063)
% 0.28/0.51 [107]P11(x1071,x1072)+~P8(x1071,x1073,x1072)
% 0.28/0.51 [108]P11(x1081,x1082)+~P9(x1082,x1081,x1083)
% 0.28/0.51 [109]P11(x1091,x1092)+~P9(x1091,x1093,x1092)
% 0.28/0.51 [110]P12(x1101,x1102)+~P3(x1102,x1101,x1103)
% 0.28/0.51 [111]P12(x1111,x1112)+~P3(x1111,x1113,x1112)
% 0.28/0.51 [112]P12(x1121,x1122)+~P7(x1121,x1123,x1122)
% 0.28/0.51 [113]P12(x1131,x1132)+~P8(x1132,x1131,x1133)
% 0.28/0.51 [119]~E(x1191,x1192)+~P14(a12,x1191,x1192,x1193)
% 0.28/0.51 [120]~E(x1201,x1202)+~P14(a8,x1201,x1203,x1202)
% 0.28/0.51 [121]P12(x1211,x1212)+~P14(a5,x1212,x1211,x1213)
% 0.28/0.51 [122]P12(x1221,x1222)+~P14(a5,x1221,x1223,x1222)
% 0.28/0.51 [123]P12(x1231,x1232)+~P14(a6,x1232,x1231,x1233)
% 0.28/0.51 [124]P12(x1241,x1242)+~P14(a6,x1241,x1243,x1242)
% 0.28/0.51 [125]P12(x1251,x1252)+~P14(a7,x1252,x1251,x1253)
% 0.28/0.51 [126]P12(x1261,x1262)+~P14(a7,x1261,x1263,x1262)
% 0.28/0.51 [127]P12(x1271,x1272)+~P14(a12,x1272,x1271,x1273)
% 0.28/0.51 [128]P12(x1281,x1282)+~P14(a12,x1281,x1283,x1282)
% 0.28/0.51 [129]P12(x1291,x1292)+~P14(a8,x1292,x1291,x1293)
% 0.28/0.51 [130]P12(x1301,x1302)+~P14(a8,x1301,x1303,x1302)
% 0.28/0.51 [134]~P14(a5,x1341,x1342,x1343)+P13(a5,x1341,x1342,x1343)
% 0.28/0.51 [135]~P14(a6,x1351,x1352,x1353)+P13(a6,x1351,x1352,x1353)
% 0.28/0.51 [136]~P14(a7,x1361,x1362,x1363)+P13(a7,x1361,x1362,x1363)
% 0.28/0.51 [137]~P14(a12,x1371,x1372,x1373)+P13(a12,x1371,x1372,x1373)
% 0.28/0.51 [138]~P14(a8,x1381,x1382,x1383)+P13(a8,x1381,x1382,x1383)
% 0.28/0.51 [139]P6(x1391,x1392,x1393,x1394)+P3(f9(x1391,x1392,x1393,x1394),x1393,x1394)
% 0.28/0.51 [140]P6(x1401,x1402,x1403,x1404)+P3(f9(x1401,x1402,x1403,x1404),x1401,x1402)
% 0.28/0.51 [141]P5(x1411,x1412,x1413,x1414)+P3(f10(x1411,x1412,x1413,x1414),x1411,x1412)
% 0.28/0.51 [142]~P4(x1421,x1422,x1423,x1424)+P3(f11(x1421,x1422,x1423,x1424),x1423,x1424)
% 0.28/0.51 [143]~P4(x1431,x1432,x1433,x1434)+P3(f11(x1431,x1432,x1433,x1434),x1431,x1432)
% 0.28/0.51 [144]P5(x1441,x1442,x1443,x1444)+~P3(f10(x1441,x1442,x1443,x1444),x1443,x1444)
% 0.28/0.51 [87]P11(x872,x871)+P11(x871,x872)+E(x871,x872)
% 0.28/0.51 [95]P11(x951,x952)+~P12(x951,x952)+E(x951,x952)
% 0.28/0.51 [96]~P12(x962,x961)+~P12(x961,x962)+E(x961,x962)
% 0.28/0.51 [98]~P11(x981,x983)+P11(x981,x982)+~P11(x983,x982)
% 0.28/0.51 [99]~P12(x991,x993)+P11(x991,x992)+~P11(x993,x992)
% 0.28/0.51 [100]~P12(x1003,x1002)+P11(x1001,x1002)+~P11(x1001,x1003)
% 0.28/0.51 [101]~P12(x1011,x1013)+P12(x1011,x1012)+~P12(x1013,x1012)
% 0.28/0.51 [102]~P12(x1021,x1023)+~P12(x1022,x1021)+P3(x1021,x1022,x1023)
% 0.28/0.51 [103]~P11(x1032,x1031)+~P12(x1031,x1033)+P7(x1031,x1032,x1033)
% 0.28/0.51 [104]~P11(x1041,x1043)+~P12(x1042,x1041)+P8(x1041,x1042,x1043)
% 0.28/0.51 [105]~P11(x1051,x1053)+~P11(x1052,x1051)+P9(x1051,x1052,x1053)
% 0.28/0.52 [114]~P12(x1141,x1143)+~P12(x1142,x1141)+P14(a5,x1141,x1142,x1143)
% 0.28/0.52 [115]~P12(x1151,x1153)+~P12(x1152,x1151)+P14(a6,x1151,x1152,x1153)
% 0.28/0.52 [116]~P12(x1161,x1163)+~P12(x1162,x1161)+P14(a7,x1161,x1162,x1163)
% 0.28/0.52 [131]~P3(x1315,x1311,x1312)+P4(x1311,x1312,x1313,x1314)+~P3(x1315,x1313,x1314)
% 0.28/0.52 [132]~P5(x1324,x1325,x1322,x1323)+P3(x1321,x1322,x1323)+~P3(x1321,x1324,x1325)
% 0.28/0.52 [133]~P6(x1334,x1335,x1332,x1333)+~P3(x1331,x1332,x1333)+~P3(x1331,x1334,x1335)
% 0.28/0.52 [84]~P1(x841)+E(x841,a2)+E(x841,a4)+E(x841,a1)
% 0.28/0.52 [88]~P1(x881)+~P1(x882)+~E(x882,a1)+E(f3(x881,x882),a1)
% 0.28/0.52 [89]~P1(x892)+~P1(x891)+~E(x891,a1)+E(f3(x891,x892),a1)
% 0.28/0.52 [117]~P12(x1171,x1172)+~P12(x1173,x1171)+E(x1171,x1172)+P14(a8,x1171,x1173,x1172)
% 0.28/0.52 [118]~P12(x1182,x1183)+~P12(x1181,x1182)+E(x1181,x1182)+P14(a12,x1182,x1181,x1183)
% 0.28/0.52 [90]~P1(x902)+~P1(x901)+~E(x902,a2)+~E(x901,a2)+E(f3(x901,x902),a2)
% 0.28/0.52 [97]~P1(x972)+~P1(x971)+E(f3(x971,x972),a1)+E(f3(x971,x972),a2)+E(f3(x971,x972),a4)
% 0.28/0.52 [85]~P2(x851)+E(x851,a6)+E(x851,a7)+E(x851,a12)+E(x851,a8)+E(x851,a5)
% 0.28/0.52 [91]~P1(x911)+~P1(x912)+~E(x912,a4)+E(x911,a1)+E(x912,a1)+E(f3(x911,x912),a4)
% 0.28/0.52 [92]~P1(x921)+~P1(x922)+~E(x922,a4)+E(x921,a1)+E(x922,a1)+E(f3(x922,x921),a4)
% 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(f3(x41,x43),f3(x42,x43))
% 0.28/0.52 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 0.28/0.52 [6]~E(x61,x62)+E(f10(x61,x63,x64,x65),f10(x62,x63,x64,x65))
% 0.28/0.52 [7]~E(x71,x72)+E(f10(x73,x71,x74,x75),f10(x73,x72,x74,x75))
% 0.28/0.52 [8]~E(x81,x82)+E(f10(x83,x84,x81,x85),f10(x83,x84,x82,x85))
% 0.28/0.52 [9]~E(x91,x92)+E(f10(x93,x94,x95,x91),f10(x93,x94,x95,x92))
% 0.28/0.52 [10]~E(x101,x102)+E(f11(x101,x103,x104,x105),f11(x102,x103,x104,x105))
% 0.28/0.52 [11]~E(x111,x112)+E(f11(x113,x111,x114,x115),f11(x113,x112,x114,x115))
% 0.28/0.52 [12]~E(x121,x122)+E(f11(x123,x124,x121,x125),f11(x123,x124,x122,x125))
% 0.28/0.52 [13]~E(x131,x132)+E(f11(x133,x134,x135,x131),f11(x133,x134,x135,x132))
% 0.28/0.52 [14]~E(x141,x142)+E(f9(x141,x143,x144,x145),f9(x142,x143,x144,x145))
% 0.28/0.52 [15]~E(x151,x152)+E(f9(x153,x151,x154,x155),f9(x153,x152,x154,x155))
% 0.28/0.52 [16]~E(x161,x162)+E(f9(x163,x164,x161,x165),f9(x163,x164,x162,x165))
% 0.28/0.52 [17]~E(x171,x172)+E(f9(x173,x174,x175,x171),f9(x173,x174,x175,x172))
% 0.28/0.52 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 0.28/0.52 [19]P3(x192,x193,x194)+~E(x191,x192)+~P3(x191,x193,x194)
% 0.28/0.52 [20]P3(x203,x202,x204)+~E(x201,x202)+~P3(x203,x201,x204)
% 0.28/0.52 [21]P3(x213,x214,x212)+~E(x211,x212)+~P3(x213,x214,x211)
% 0.28/0.52 [22]P5(x222,x223,x224,x225)+~E(x221,x222)+~P5(x221,x223,x224,x225)
% 0.28/0.52 [23]P5(x233,x232,x234,x235)+~E(x231,x232)+~P5(x233,x231,x234,x235)
% 0.28/0.52 [24]P5(x243,x244,x242,x245)+~E(x241,x242)+~P5(x243,x244,x241,x245)
% 0.28/0.52 [25]P5(x253,x254,x255,x252)+~E(x251,x252)+~P5(x253,x254,x255,x251)
% 0.28/0.52 [26]~P2(x261)+P2(x262)+~E(x261,x262)
% 0.28/0.52 [27]P14(x272,x273,x274,x275)+~E(x271,x272)+~P14(x271,x273,x274,x275)
% 0.28/0.52 [28]P14(x283,x282,x284,x285)+~E(x281,x282)+~P14(x283,x281,x284,x285)
% 0.28/0.52 [29]P14(x293,x294,x292,x295)+~E(x291,x292)+~P14(x293,x294,x291,x295)
% 0.28/0.52 [30]P14(x303,x304,x305,x302)+~E(x301,x302)+~P14(x303,x304,x305,x301)
% 0.28/0.52 [31]P12(x312,x313)+~E(x311,x312)+~P12(x311,x313)
% 0.28/0.52 [32]P12(x323,x322)+~E(x321,x322)+~P12(x323,x321)
% 0.28/0.52 [33]P8(x332,x333,x334)+~E(x331,x332)+~P8(x331,x333,x334)
% 0.28/0.52 [34]P8(x343,x342,x344)+~E(x341,x342)+~P8(x343,x341,x344)
% 0.28/0.52 [35]P8(x353,x354,x352)+~E(x351,x352)+~P8(x353,x354,x351)
% 0.28/0.52 [36]P7(x362,x363,x364)+~E(x361,x362)+~P7(x361,x363,x364)
% 0.28/0.52 [37]P7(x373,x372,x374)+~E(x371,x372)+~P7(x373,x371,x374)
% 0.28/0.52 [38]P7(x383,x384,x382)+~E(x381,x382)+~P7(x383,x384,x381)
% 0.28/0.52 [39]~P10(x391)+P10(x392)+~E(x391,x392)
% 0.28/0.52 [40]P9(x402,x403,x404)+~E(x401,x402)+~P9(x401,x403,x404)
% 0.28/0.52 [41]P9(x413,x412,x414)+~E(x411,x412)+~P9(x413,x411,x414)
% 0.28/0.52 [42]P9(x423,x424,x422)+~E(x421,x422)+~P9(x423,x424,x421)
% 0.28/0.52 [43]P11(x432,x433)+~E(x431,x432)+~P11(x431,x433)
% 0.28/0.52 [44]P11(x443,x442)+~E(x441,x442)+~P11(x443,x441)
% 0.28/0.52 [45]P13(x452,x453,x454,x455)+~E(x451,x452)+~P13(x451,x453,x454,x455)
% 0.28/0.52 [46]P13(x463,x462,x464,x465)+~E(x461,x462)+~P13(x463,x461,x464,x465)
% 0.28/0.52 [47]P13(x473,x474,x472,x475)+~E(x471,x472)+~P13(x473,x474,x471,x475)
% 0.28/0.52 [48]P13(x483,x484,x485,x482)+~E(x481,x482)+~P13(x483,x484,x485,x481)
% 0.28/0.52 [49]P6(x492,x493,x494,x495)+~E(x491,x492)+~P6(x491,x493,x494,x495)
% 0.28/0.52 [50]P6(x503,x502,x504,x505)+~E(x501,x502)+~P6(x503,x501,x504,x505)
% 0.28/0.52 [51]P6(x513,x514,x512,x515)+~E(x511,x512)+~P6(x513,x514,x511,x515)
% 0.28/0.52 [52]P6(x523,x524,x525,x522)+~E(x521,x522)+~P6(x523,x524,x525,x521)
% 0.28/0.52 [53]P4(x532,x533,x534,x535)+~E(x531,x532)+~P4(x531,x533,x534,x535)
% 0.28/0.52 [54]P4(x543,x542,x544,x545)+~E(x541,x542)+~P4(x543,x541,x544,x545)
% 0.28/0.52 [55]P4(x553,x554,x552,x555)+~E(x551,x552)+~P4(x553,x554,x551,x555)
% 0.28/0.52 [56]P4(x563,x564,x565,x562)+~E(x561,x562)+~P4(x563,x564,x565,x561)
% 0.28/0.52
% 0.28/0.52 %-------------------------------------------
% 0.28/0.52 cnf(152,plain,
% 0.28/0.52 ($false),
% 0.28/0.52 inference(scs_inference,[],[83,67]),
% 0.28/0.52 ['proof']).
% 0.28/0.52 % SZS output end Proof
% 0.28/0.52 % Total time :0.007069s
%------------------------------------------------------------------------------