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