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