%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT081+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 : 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 4.62s 4.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT081+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.34 % Computer : n013.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:15:50 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.12/0.45 start to proof:theBenchmark
% 4.62/4.80 %-------------------------------------------
% 4.62/4.80 % File :CSE---1.7
% 4.62/4.80 % Problem :theBenchmark
% 4.62/4.80 % Transform :cnf
% 4.62/4.80 % Format :tptp:raw
% 4.62/4.80 % Command :java -jar mcs_scs.jar %d %s
% 4.62/4.80
% 4.62/4.80 % Result :Theorem 4.341647s
% 4.62/4.80 % Output :CNFRefutation 4.341647s
% 4.62/4.80 %-------------------------------------------
% 4.62/4.81 %--------------------------------------------------------------------------
% 4.62/4.81 % File : MGT081+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 4.62/4.81 % Domain : Management
% 4.62/4.81 % Problem : 2D Conflict via width (5 constants)
% 4.62/4.81 % Version : Especial.
% 4.62/4.81 % English : Width: lteq 400 intersection gteq 800 = null Conflict
% 4.62/4.81 % Height: lteq 600 intersection gteq 200 = [200,600] != null
% 4.62/4.81 % Compatible. Box: Conflict kills box.
% 4.62/4.81
% 4.62/4.81 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 4.62/4.81 % Source : [MC+26]
% 4.62/4.81 % Names : ODRL402-1.p [MC+26]
% 4.62/4.81
% 4.62/4.81 % Status : Theorem
% 4.62/4.81 % Rating : ? v9.3.1
% 4.62/4.81 % Syntax : Number of formulae : 44 ( 22 unt; 0 def)
% 4.62/4.81 % Number of atoms : 106 ( 33 equ)
% 4.62/4.81 % Maximal formula atoms : 10 ( 2 avg)
% 4.62/4.81 % Number of connectives : 80 ( 18 ~; 9 |; 33 &)
% 4.62/4.81 % ( 8 <=>; 12 =>; 0 <=; 0 <~>)
% 4.62/4.81 % Maximal formula depth : 11 ( 4 avg)
% 4.62/4.81 % Maximal term depth : 2 ( 1 avg)
% 4.62/4.81 % Number of predicates : 12 ( 11 usr; 0 prp; 1-4 aty)
% 4.62/4.81 % Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% 4.62/4.81 % Number of variables : 59 ( 55 !; 4 ?)
% 4.62/4.81 % SPC : FOF_THM_RFO_SEQ
% 4.62/4.81
% 4.62/4.81 % Comments : Requires MGT002+0.ax + MGT002+2.ax.
% 4.62/4.81 % Bugfixes : v9.3.1 - $distinct expanded to inequalities.
% 4.62/4.81 %--------------------------------------------------------------------------
% 4.62/4.81 include('Axioms/MGT002+0.ax').
% 4.62/4.81 include('Axioms/MGT002+2.ax').
% 4.62/4.81 %--------------------------------------------------------------------------
% 4.62/4.81 %----Named constants and ordering
% 4.62/4.81 fof(val_v0,axiom,
% 4.62/4.81 val(v0) ).
% 4.62/4.81
% 4.62/4.81 fof(val_v200,axiom,
% 4.62/4.81 val(v200) ).
% 4.62/4.81
% 4.62/4.81 fof(val_v400,axiom,
% 4.62/4.81 val(v400) ).
% 4.62/4.81
% 4.62/4.81 fof(val_v600,axiom,
% 4.62/4.81 val(v600) ).
% 4.62/4.81
% 4.62/4.81 fof(val_v800,axiom,
% 4.62/4.81 val(v800) ).
% 4.62/4.81
% 4.62/4.81 fof(ord_v0_v200,axiom,
% 4.62/4.81 less(v0,v200) ).
% 4.62/4.81
% 4.62/4.81 fof(ord_v0_v400,axiom,
% 4.62/4.81 less(v0,v400) ).
% 4.62/4.81
% 4.62/4.81 fof(ord_v0_v600,axiom,
% 4.62/4.81 less(v0,v600) ).
% 4.62/4.81
% 4.62/4.81 fof(ord_v0_v800,axiom,
% 4.62/4.81 less(v0,v800) ).
% 4.62/4.81
% 4.62/4.81 fof(ord_v200_v400,axiom,
% 4.62/4.81 less(v200,v400) ).
% 4.62/4.81
% 4.62/4.81 fof(ord_v200_v600,axiom,
% 4.62/4.81 less(v200,v600) ).
% 4.62/4.81
% 4.62/4.81 fof(ord_v200_v800,axiom,
% 4.62/4.81 less(v200,v800) ).
% 4.62/4.81
% 4.62/4.81 fof(ord_v400_v600,axiom,
% 4.62/4.81 less(v400,v600) ).
% 4.62/4.81
% 4.62/4.81 fof(ord_v400_v800,axiom,
% 4.62/4.81 less(v400,v800) ).
% 4.62/4.81
% 4.62/4.81 fof(ord_v600_v800,axiom,
% 4.62/4.81 less(v600,v800) ).
% 4.62/4.81
% 4.62/4.81 fof(distinct,axiom,
% 4.62/4.81 ( v0 != v200
% 4.62/4.81 & v0 != v400
% 4.62/4.81 & v0 != v600
% 4.62/4.81 & v0 != v800
% 4.62/4.81 & v200 != v400
% 4.62/4.81 & v200 != v600
% 4.62/4.81 & v200 != v800
% 4.62/4.81 & v400 != v600
% 4.62/4.81 & v400 != v800
% 4.62/4.81 & v600 != v800 ) ).
% 4.62/4.81
% 4.62/4.81 fof(odrl402,conjecture,
% 4.62/4.81 ~ ? [X,Y] :
% 4.62/4.81 ( in_lopen(X,v0,v400)
% 4.62/4.81 & leq(v800,X)
% 4.62/4.81 & in_lopen(Y,v0,v600)
% 4.62/4.81 & leq(v200,Y) ) ).
% 4.62/4.81
% 4.62/4.81 %--------------------------------------------------------------------------
% 4.62/4.81 %-------------------------------------------
% 4.62/4.81 % Proof found
% 4.62/4.81 % SZS status Theorem for theBenchmark
% 4.62/4.81 % SZS output start Proof
% 4.62/4.81 %ClaNum:121(EqnAxiom:47)
% 4.62/4.81 %VarNum:252(SingletonVarNum:111)
% 4.62/4.81 %MaxLitNum:6
% 4.62/4.81 %MaxfuncDepth:1
% 4.62/4.81 %SharedTerms:45
% 4.62/4.81 %goalClause: 66 67 68 69
% 4.62/4.81 %singleGoalClaCount:4
% 4.62/4.81 [48]P1(a1)
% 4.62/4.81 [49]P1(a2)
% 4.62/4.81 [50]P1(a4)
% 4.62/4.81 [51]P9(a10)
% 4.62/4.81 [52]P9(a11)
% 4.62/4.81 [53]P9(a12)
% 4.62/4.81 [54]P9(a13)
% 4.62/4.81 [55]P9(a14)
% 4.62/4.81 [56]P10(a10,a11)
% 4.62/4.81 [57]P10(a10,a12)
% 4.62/4.81 [58]P10(a10,a13)
% 4.62/4.81 [59]P10(a10,a14)
% 4.62/4.81 [60]P10(a11,a12)
% 4.62/4.81 [61]P10(a11,a13)
% 4.62/4.81 [62]P10(a11,a14)
% 4.62/4.81 [63]P10(a12,a13)
% 4.62/4.81 [64]P10(a12,a14)
% 4.62/4.81 [65]P10(a13,a14)
% 4.62/4.81 [66]P11(a11,a5)
% 4.62/4.81 [67]P11(a14,a6)
% 4.62/4.81 [68]P2(a6,a10,a12)
% 4.62/4.81 [69]P2(a5,a10,a13)
% 4.62/4.81 [70]~E(a1,a2)
% 4.62/4.81 [71]~E(a1,a4)
% 4.62/4.81 [72]~E(a4,a2)
% 4.62/4.81 [73]~E(a11,a10)
% 4.62/4.81 [74]~E(a12,a10)
% 4.62/4.81 [75]~E(a12,a11)
% 4.62/4.81 [76]~E(a13,a10)
% 4.62/4.81 [77]~E(a13,a11)
% 4.62/4.81 [78]~E(a13,a12)
% 4.62/4.81 [79]~E(a14,a10)
% 4.62/4.81 [80]~E(a14,a11)
% 4.62/4.81 [81]~E(a14,a12)
% 4.62/4.81 [82]~E(a14,a13)
% 4.62/4.81 [83]~P10(x831,x831)
% 4.62/4.81 [85]~E(x851,x852)+P11(x851,x852)
% 4.62/4.81 [93]~P10(x931,x932)+P11(x931,x932)
% 4.62/4.81 [105]P10(x1051,x1052)+~P2(x1052,x1051,x1053)
% 4.62/4.81 [106]P10(x1061,x1062)+~P7(x1061,x1063,x1062)
% 4.62/4.81 [107]P10(x1071,x1072)+~P8(x1072,x1071,x1073)
% 4.62/4.81 [108]P10(x1081,x1082)+~P8(x1081,x1083,x1082)
% 4.62/4.81 [109]P11(x1091,x1092)+~P3(x1092,x1091,x1093)
% 4.62/4.81 [110]P11(x1101,x1102)+~P3(x1101,x1103,x1102)
% 4.62/4.81 [111]P11(x1111,x1112)+~P2(x1111,x1113,x1112)
% 4.62/4.81 [112]P11(x1121,x1122)+~P7(x1122,x1121,x1123)
% 4.62/4.81 [116]P6(x1161,x1162,x1163,x1164)+P3(f7(x1161,x1162,x1163,x1164),x1163,x1164)
% 4.62/4.81 [117]P6(x1171,x1172,x1173,x1174)+P3(f7(x1171,x1172,x1173,x1174),x1171,x1172)
% 4.62/4.81 [118]P5(x1181,x1182,x1183,x1184)+P3(f8(x1181,x1182,x1183,x1184),x1181,x1182)
% 4.62/4.81 [119]~P4(x1191,x1192,x1193,x1194)+P3(f9(x1191,x1192,x1193,x1194),x1193,x1194)
% 4.62/4.81 [120]~P4(x1201,x1202,x1203,x1204)+P3(f9(x1201,x1202,x1203,x1204),x1201,x1202)
% 4.62/4.81 [121]P5(x1211,x1212,x1213,x1214)+~P3(f8(x1211,x1212,x1213,x1214),x1213,x1214)
% 4.62/4.81 [86]P10(x862,x861)+P10(x861,x862)+E(x861,x862)
% 4.62/4.81 [94]P10(x941,x942)+~P11(x941,x942)+E(x941,x942)
% 4.62/4.81 [95]~P11(x952,x951)+~P11(x951,x952)+E(x951,x952)
% 4.62/4.81 [97]~P10(x971,x973)+P10(x971,x972)+~P10(x973,x972)
% 4.62/4.81 [98]~P11(x981,x983)+P10(x981,x982)+~P10(x983,x982)
% 4.62/4.81 [99]~P11(x993,x992)+P10(x991,x992)+~P10(x991,x993)
% 4.62/4.81 [100]~P11(x1001,x1003)+P11(x1001,x1002)+~P11(x1003,x1002)
% 4.62/4.81 [101]~P11(x1011,x1013)+~P11(x1012,x1011)+P3(x1011,x1012,x1013)
% 4.62/4.81 [102]~P10(x1022,x1021)+~P11(x1021,x1023)+P2(x1021,x1022,x1023)
% 4.62/4.81 [103]~P10(x1031,x1033)+~P11(x1032,x1031)+P7(x1031,x1032,x1033)
% 4.62/4.81 [104]~P10(x1041,x1043)+~P10(x1042,x1041)+P8(x1041,x1042,x1043)
% 4.62/4.81 [113]~P3(x1135,x1131,x1132)+P4(x1131,x1132,x1133,x1134)+~P3(x1135,x1133,x1134)
% 4.62/4.81 [114]~P5(x1144,x1145,x1142,x1143)+P3(x1141,x1142,x1143)+~P3(x1141,x1144,x1145)
% 4.62/4.81 [115]~P6(x1154,x1155,x1152,x1153)+~P3(x1151,x1152,x1153)+~P3(x1151,x1154,x1155)
% 4.62/4.81 [84]~P1(x841)+E(x841,a2)+E(x841,a4)+E(x841,a1)
% 4.62/4.81 [87]~P1(x871)+~P1(x872)+~E(x872,a1)+E(f3(x871,x872),a1)
% 4.62/4.81 [88]~P1(x882)+~P1(x881)+~E(x881,a1)+E(f3(x881,x882),a1)
% 4.62/4.81 [89]~P1(x892)+~P1(x891)+~E(x892,a2)+~E(x891,a2)+E(f3(x891,x892),a2)
% 4.62/4.81 [96]~P1(x962)+~P1(x961)+E(f3(x961,x962),a1)+E(f3(x961,x962),a2)+E(f3(x961,x962),a4)
% 4.62/4.81 [90]~P1(x901)+~P1(x902)+~E(x902,a4)+E(x901,a1)+E(x902,a1)+E(f3(x901,x902),a4)
% 4.62/4.81 [91]~P1(x911)+~P1(x912)+~E(x912,a4)+E(x911,a1)+E(x912,a1)+E(f3(x912,x911),a4)
% 4.62/4.81 %EqnAxiom
% 4.62/4.81 [1]E(x11,x11)
% 4.62/4.81 [2]E(x22,x21)+~E(x21,x22)
% 4.62/4.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 4.62/4.81 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 4.62/4.81 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 4.62/4.81 [6]~E(x61,x62)+E(f8(x61,x63,x64,x65),f8(x62,x63,x64,x65))
% 4.62/4.81 [7]~E(x71,x72)+E(f8(x73,x71,x74,x75),f8(x73,x72,x74,x75))
% 4.62/4.81 [8]~E(x81,x82)+E(f8(x83,x84,x81,x85),f8(x83,x84,x82,x85))
% 4.62/4.81 [9]~E(x91,x92)+E(f8(x93,x94,x95,x91),f8(x93,x94,x95,x92))
% 4.62/4.81 [10]~E(x101,x102)+E(f9(x101,x103,x104,x105),f9(x102,x103,x104,x105))
% 4.62/4.81 [11]~E(x111,x112)+E(f9(x113,x111,x114,x115),f9(x113,x112,x114,x115))
% 4.62/4.81 [12]~E(x121,x122)+E(f9(x123,x124,x121,x125),f9(x123,x124,x122,x125))
% 4.62/4.81 [13]~E(x131,x132)+E(f9(x133,x134,x135,x131),f9(x133,x134,x135,x132))
% 4.62/4.81 [14]~E(x141,x142)+E(f7(x141,x143,x144,x145),f7(x142,x143,x144,x145))
% 4.62/4.81 [15]~E(x151,x152)+E(f7(x153,x151,x154,x155),f7(x153,x152,x154,x155))
% 4.62/4.81 [16]~E(x161,x162)+E(f7(x163,x164,x161,x165),f7(x163,x164,x162,x165))
% 4.62/4.81 [17]~E(x171,x172)+E(f7(x173,x174,x175,x171),f7(x173,x174,x175,x172))
% 4.62/4.81 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 4.62/4.81 [19]P3(x192,x193,x194)+~E(x191,x192)+~P3(x191,x193,x194)
% 4.62/4.81 [20]P3(x203,x202,x204)+~E(x201,x202)+~P3(x203,x201,x204)
% 4.62/4.81 [21]P3(x213,x214,x212)+~E(x211,x212)+~P3(x213,x214,x211)
% 4.62/4.81 [22]P5(x222,x223,x224,x225)+~E(x221,x222)+~P5(x221,x223,x224,x225)
% 4.62/4.81 [23]P5(x233,x232,x234,x235)+~E(x231,x232)+~P5(x233,x231,x234,x235)
% 4.62/4.81 [24]P5(x243,x244,x242,x245)+~E(x241,x242)+~P5(x243,x244,x241,x245)
% 4.62/4.81 [25]P5(x253,x254,x255,x252)+~E(x251,x252)+~P5(x253,x254,x255,x251)
% 4.62/4.81 [26]~P9(x261)+P9(x262)+~E(x261,x262)
% 4.62/4.81 [27]P8(x272,x273,x274)+~E(x271,x272)+~P8(x271,x273,x274)
% 4.62/4.81 [28]P8(x283,x282,x284)+~E(x281,x282)+~P8(x283,x281,x284)
% 4.62/4.81 [29]P8(x293,x294,x292)+~E(x291,x292)+~P8(x293,x294,x291)
% 4.62/4.81 [30]P10(x302,x303)+~E(x301,x302)+~P10(x301,x303)
% 4.62/4.81 [31]P10(x313,x312)+~E(x311,x312)+~P10(x313,x311)
% 4.62/4.81 [32]P7(x322,x323,x324)+~E(x321,x322)+~P7(x321,x323,x324)
% 4.62/4.81 [33]P7(x333,x332,x334)+~E(x331,x332)+~P7(x333,x331,x334)
% 4.62/4.81 [34]P7(x343,x344,x342)+~E(x341,x342)+~P7(x343,x344,x341)
% 4.62/4.81 [35]P11(x352,x353)+~E(x351,x352)+~P11(x351,x353)
% 4.62/4.81 [36]P11(x363,x362)+~E(x361,x362)+~P11(x363,x361)
% 4.62/4.81 [37]P6(x372,x373,x374,x375)+~E(x371,x372)+~P6(x371,x373,x374,x375)
% 4.62/4.81 [38]P6(x383,x382,x384,x385)+~E(x381,x382)+~P6(x383,x381,x384,x385)
% 4.62/4.81 [39]P6(x393,x394,x392,x395)+~E(x391,x392)+~P6(x393,x394,x391,x395)
% 4.62/4.81 [40]P6(x403,x404,x405,x402)+~E(x401,x402)+~P6(x403,x404,x405,x401)
% 4.62/4.81 [41]P2(x412,x413,x414)+~E(x411,x412)+~P2(x411,x413,x414)
% 4.62/4.81 [42]P2(x423,x422,x424)+~E(x421,x422)+~P2(x423,x421,x424)
% 4.62/4.81 [43]P2(x433,x434,x432)+~E(x431,x432)+~P2(x433,x434,x431)
% 4.62/4.81 [44]P4(x442,x443,x444,x445)+~E(x441,x442)+~P4(x441,x443,x444,x445)
% 4.62/4.81 [45]P4(x453,x452,x454,x455)+~E(x451,x452)+~P4(x453,x451,x454,x455)
% 4.62/4.81 [46]P4(x463,x464,x462,x465)+~E(x461,x462)+~P4(x463,x464,x461,x465)
% 4.62/4.81 [47]P4(x473,x474,x475,x472)+~E(x471,x472)+~P4(x473,x474,x475,x471)
% 4.62/4.81
% 4.62/4.81 %-------------------------------------------
% 4.62/4.81 cnf(215,plain,
% 4.62/4.81 (P10(a12,a6)),
% 4.62/4.81 inference(scs_inference,[],[67,83,57,64,97,99])).
% 4.62/4.81 cnf(715,plain,
% 4.62/4.81 ($false),
% 4.62/4.81 inference(scs_inference,[],[68,215,83,99,93,111]),
% 4.62/4.81 ['proof']).
% 4.62/4.81 % SZS output end Proof
% 4.62/4.81 % Total time :4.341647s
%------------------------------------------------------------------------------