%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT070+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n019.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:23 AM UTC 2026
% Result : Theorem 1.44s 1.68s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT070+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 13:54:22 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.52 start to proof:theBenchmark
% 1.44/1.67 %-------------------------------------------
% 1.44/1.67 % File :CSE---1.7
% 1.44/1.67 % Problem :theBenchmark
% 1.44/1.67 % Transform :cnf
% 1.44/1.67 % Format :tptp:raw
% 1.44/1.67 % Command :java -jar mcs_scs.jar %d %s
% 1.44/1.67
% 1.44/1.67 % Result :Theorem 1.162629s
% 1.44/1.67 % Output :CNFRefutation 1.162629s
% 1.44/1.67 %-------------------------------------------
% 1.44/1.67 %--------------------------------------------------------------------------
% 1.44/1.67 % File : MGT070+1 : TPTP v9.3.0. Released v9.3.0.
% 1.44/1.67 % Domain : Management
% 1.44/1.67 % Problem : Sharpness of Unknown in the Compatible direction
% 1.44/1.67 % Version : Especial.
% 1.44/1.67 % English : For every Unknown scenario with domain bounds [ninf, nsup],
% 1.44/1.67 % there exists a value V (namely V=n0) for which a Compatible
% 1.44/1.67 % completion holds. This is thm:unknown-sound (compatible
% 1.44/1.67 % direction): Unknown is sharp - it does not collapse to
% 1.44/1.67 % Conflict, because a Compatible completion always exists.
% 1.44/1.67
% 1.44/1.67 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 1.44/1.67 % Source : [MC+26]
% 1.44/1.67 % Names : HARD002+1.p [MC+26]
% 1.44/1.67
% 1.44/1.67 % Status : Theorem
% 1.44/1.67 % Rating : 0.00 v9.3.0
% 1.44/1.67 % Syntax : Number of formulae : 40 ( 12 unt; 0 def)
% 1.44/1.67 % Number of atoms : 113 ( 24 equ)
% 1.44/1.67 % Maximal formula atoms : 7 ( 2 avg)
% 1.44/1.67 % Number of connectives : 80 ( 7 ~; 9 |; 36 &)
% 1.44/1.67 % ( 8 <=>; 20 =>; 0 <=; 0 <~>)
% 1.44/1.67 % Maximal formula depth : 10 ( 5 avg)
% 1.44/1.67 % Maximal term depth : 2 ( 1 avg)
% 1.44/1.67 % Number of predicates : 13 ( 12 usr; 0 prp; 1-4 aty)
% 1.44/1.67 % Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% 1.44/1.67 % Number of variables : 89 ( 85 !; 4 ?)
% 1.44/1.67 % SPC : FOF_THM_RFO_SEQ
% 1.44/1.67
% 1.44/1.67 % Comments :
% 1.44/1.67 %--------------------------------------------------------------------------
% 1.44/1.67 include('Axioms/MGT002+0.ax').
% 1.44/1.67 include('Axioms/MGT002+1.ax').
% 1.44/1.67 include('Axioms/MGT002+2.ax').
% 1.44/1.67 include('Axioms/MGT002+4.ax').
% 1.44/1.67 %--------------------------------------------------------------------------
% 1.44/1.67 %----Setup: a concrete Unknown scenario.
% 1.44/1.67 %----P1 constrains width with gteq n0 (interval [n0, nsup]).
% 1.44/1.67 %----P2 does not constrain width at all.
% 1.44/1.67 %----The height axis is unconstrained by both policies.
% 1.44/1.67 %----box_verdict = Unknown (both axes unconstrained by at least one policy)
% 1.44/1.67 fof(h_inf_0,hypothesis,
% 1.44/1.67 less(ninf,n0) ).
% 1.44/1.68
% 1.44/1.68 fof(h_0_sup,hypothesis,
% 1.44/1.68 less(n0,nsup) ).
% 1.44/1.68
% 1.44/1.68 fof(h_inf_lb,hypothesis,
% 1.44/1.68 ! [X] : leq(ninf,X) ).
% 1.44/1.68
% 1.44/1.68 fof(h_sup_ub,hypothesis,
% 1.44/1.68 ! [X] : leq(X,nsup) ).
% 1.44/1.68
% 1.44/1.68 %----The box verdict is Unknown (both axes have at least one policy absent).
% 1.44/1.68 fof(h_unknown,hypothesis,
% 1.44/1.68 box_verdict(unknown,unknown) = unknown ).
% 1.44/1.68
% 1.44/1.68 %----Sharpness of Unknown in the Compatible direction.
% 1.44/1.68 %----There exists a value V in [ninf, nsup] for which a Compatible
% 1.44/1.68 %----completion holds. This shows Unknown is NOT uniformly Conflict -
% 1.44/1.68 %----the Compatible direction is reachable.
% 1.44/1.68 fof(unknown_sound_compatible,conjecture,
% 1.44/1.68 ? [V] :
% 1.44/1.68 ( leq(ninf,V)
% 1.44/1.68 & leq(V,nsup)
% 1.44/1.68 & completion_compatible(V,ninf,nsup) ) ).
% 1.44/1.68
% 1.44/1.68 %--------------------------------------------------------------------------
% 1.44/1.68 %-------------------------------------------
% 1.44/1.68 % Proof found
% 1.44/1.68 % SZS status Theorem for theBenchmark
% 1.44/1.68 % SZS output start Proof
% 1.44/1.68 %ClaNum:114(EqnAxiom:55)
% 1.44/1.68 %VarNum:298(SingletonVarNum:131)
% 1.44/1.68 %MaxLitNum:6
% 1.44/1.68 %MaxfuncDepth:1
% 1.44/1.68 %SharedTerms:16
% 1.44/1.68 %goalClause: 100
% 1.44/1.68 [56]P1(a1)
% 1.44/1.68 [57]P1(a2)
% 1.44/1.68 [58]P1(a4)
% 1.44/1.68 [60]P11(a5,a6)
% 1.44/1.68 [61]P11(a6,a11)
% 1.44/1.68 [64]~E(a1,a2)
% 1.44/1.68 [65]~E(a1,a4)
% 1.44/1.68 [66]~E(a4,a2)
% 1.44/1.68 [59]E(f3(a4,a4),a4)
% 1.44/1.68 [62]P12(x621,a11)
% 1.44/1.68 [63]P12(a5,x631)
% 1.44/1.68 [67]~P11(x671,x671)
% 1.44/1.68 [69]~E(x691,x692)+P12(x691,x692)
% 1.44/1.68 [77]~P11(x771,x772)+P12(x771,x772)
% 1.44/1.68 [85]~P11(x851,x852)+P11(x851,f7(x851,x852))
% 1.44/1.68 [86]~P11(x861,x862)+P11(f7(x861,x862),x862)
% 1.44/1.68 [92]P11(x921,x922)+~P8(x922,x921,x923)
% 1.44/1.68 [93]P11(x931,x932)+~P9(x931,x933,x932)
% 1.44/1.68 [94]P11(x941,x942)+~P10(x942,x941,x943)
% 1.44/1.68 [95]P11(x951,x952)+~P10(x951,x953,x952)
% 1.44/1.68 [96]P12(x961,x962)+~P2(x962,x961,x963)
% 1.44/1.68 [97]P12(x971,x972)+~P2(x971,x973,x972)
% 1.44/1.68 [98]P12(x981,x982)+~P8(x981,x983,x982)
% 1.44/1.68 [99]P12(x991,x992)+~P9(x992,x991,x993)
% 1.44/1.68 [108]P6(x1081,x1082,x1083,x1084)+P2(f8(x1081,x1082,x1083,x1084),x1083,x1084)
% 1.44/1.68 [109]P6(x1091,x1092,x1093,x1094)+P2(f8(x1091,x1092,x1093,x1094),x1091,x1092)
% 1.44/1.68 [110]P5(x1101,x1102,x1103,x1104)+P2(f9(x1101,x1102,x1103,x1104),x1101,x1102)
% 1.44/1.68 [111]~P4(x1111,x1112,x1113,x1114)+P2(f10(x1111,x1112,x1113,x1114),x1113,x1114)
% 1.44/1.68 [112]~P4(x1121,x1122,x1123,x1124)+P2(f10(x1121,x1122,x1123,x1124),x1121,x1122)
% 1.44/1.68 [114]P5(x1141,x1142,x1143,x1144)+~P2(f9(x1141,x1142,x1143,x1144),x1143,x1144)
% 1.44/1.68 [100]~P12(a5,x1001)+~P12(x1001,a11)+~P3(x1001,a5,a11)
% 1.44/1.68 [70]P11(x702,x701)+P11(x701,x702)+E(x701,x702)
% 1.44/1.68 [78]P11(x781,x782)+~P12(x781,x782)+E(x781,x782)
% 1.44/1.68 [79]~P12(x792,x791)+~P12(x791,x792)+E(x791,x792)
% 1.44/1.68 [81]~P11(x811,x813)+P11(x811,x812)+~P11(x813,x812)
% 1.44/1.68 [82]~P12(x821,x823)+P11(x821,x822)+~P11(x823,x822)
% 1.44/1.68 [83]~P12(x833,x832)+P11(x831,x832)+~P11(x831,x833)
% 1.44/1.68 [84]~P12(x841,x843)+P12(x841,x842)+~P12(x843,x842)
% 1.44/1.68 [87]~P12(x871,x873)+~P12(x872,x871)+P2(x871,x872,x873)
% 1.44/1.68 [88]~P11(x882,x881)+~P12(x881,x883)+P8(x881,x882,x883)
% 1.44/1.68 [89]~P11(x891,x893)+~P12(x892,x891)+P9(x891,x892,x893)
% 1.44/1.68 [90]~P11(x901,x903)+~P11(x902,x901)+P10(x901,x902,x903)
% 1.44/1.68 [91]~P12(x911,x913)+~P12(x912,x911)+P3(x911,x912,x913)
% 1.44/1.68 [104]~P2(x1045,x1041,x1042)+P4(x1041,x1042,x1043,x1044)+~P2(x1045,x1043,x1044)
% 1.44/1.68 [106]~P5(x1064,x1065,x1062,x1063)+P2(x1061,x1062,x1063)+~P2(x1061,x1064,x1065)
% 1.44/1.68 [107]~P6(x1074,x1075,x1072,x1073)+~P2(x1071,x1072,x1073)+~P2(x1071,x1074,x1075)
% 1.44/1.68 [113]~P5(x1131,x1132,x1135,x1136)+P6(x1131,x1132,x1133,x1134)+~P6(x1135,x1136,x1133,x1134)
% 1.44/1.68 [68]~P1(x681)+E(x681,a2)+E(x681,a4)+E(x681,a1)
% 1.44/1.68 [71]~P1(x711)+~P1(x712)+~E(x712,a1)+E(f3(x711,x712),a1)
% 1.44/1.68 [72]~P1(x722)+~P1(x721)+~E(x721,a1)+E(f3(x721,x722),a1)
% 1.44/1.68 [73]~P1(x732)+~P1(x731)+~E(x732,a2)+~E(x731,a2)+E(f3(x731,x732),a2)
% 1.44/1.68 [80]~P1(x802)+~P1(x801)+E(f3(x801,x802),a1)+E(f3(x801,x802),a2)+E(f3(x801,x802),a4)
% 1.44/1.68 [102]~P11(x1021,x1022)+~P12(x1022,x1024)+~P12(x1021,x1024)+~P12(x1023,x1021)+P7(x1021,x1022,x1023,x1024)
% 1.44/1.68 [74]~P1(x741)+~P1(x742)+~E(x742,a4)+E(x741,a1)+E(x742,a1)+E(f3(x741,x742),a4)
% 1.44/1.68 [75]~P1(x751)+~P1(x752)+~E(x752,a4)+E(x751,a1)+E(x752,a1)+E(f3(x752,x751),a4)
% 1.44/1.68 %EqnAxiom
% 1.44/1.68 [1]E(x11,x11)
% 1.44/1.68 [2]E(x22,x21)+~E(x21,x22)
% 1.44/1.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.44/1.68 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 1.44/1.68 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 1.44/1.68 [6]~E(x61,x62)+E(f9(x61,x63,x64,x65),f9(x62,x63,x64,x65))
% 1.44/1.68 [7]~E(x71,x72)+E(f9(x73,x71,x74,x75),f9(x73,x72,x74,x75))
% 1.44/1.68 [8]~E(x81,x82)+E(f9(x83,x84,x81,x85),f9(x83,x84,x82,x85))
% 1.44/1.68 [9]~E(x91,x92)+E(f9(x93,x94,x95,x91),f9(x93,x94,x95,x92))
% 1.44/1.68 [10]~E(x101,x102)+E(f10(x101,x103,x104,x105),f10(x102,x103,x104,x105))
% 1.44/1.68 [11]~E(x111,x112)+E(f10(x113,x111,x114,x115),f10(x113,x112,x114,x115))
% 1.44/1.68 [12]~E(x121,x122)+E(f10(x123,x124,x121,x125),f10(x123,x124,x122,x125))
% 1.44/1.68 [13]~E(x131,x132)+E(f10(x133,x134,x135,x131),f10(x133,x134,x135,x132))
% 1.44/1.68 [14]~E(x141,x142)+E(f7(x141,x143),f7(x142,x143))
% 1.44/1.68 [15]~E(x151,x152)+E(f7(x153,x151),f7(x153,x152))
% 1.44/1.68 [16]~E(x161,x162)+E(f8(x161,x163,x164,x165),f8(x162,x163,x164,x165))
% 1.44/1.68 [17]~E(x171,x172)+E(f8(x173,x171,x174,x175),f8(x173,x172,x174,x175))
% 1.44/1.68 [18]~E(x181,x182)+E(f8(x183,x184,x181,x185),f8(x183,x184,x182,x185))
% 1.44/1.68 [19]~E(x191,x192)+E(f8(x193,x194,x195,x191),f8(x193,x194,x195,x192))
% 1.44/1.68 [20]~P1(x201)+P1(x202)+~E(x201,x202)
% 1.44/1.68 [21]P2(x212,x213,x214)+~E(x211,x212)+~P2(x211,x213,x214)
% 1.44/1.68 [22]P2(x223,x222,x224)+~E(x221,x222)+~P2(x223,x221,x224)
% 1.44/1.68 [23]P2(x233,x234,x232)+~E(x231,x232)+~P2(x233,x234,x231)
% 1.44/1.68 [24]P5(x242,x243,x244,x245)+~E(x241,x242)+~P5(x241,x243,x244,x245)
% 1.44/1.68 [25]P5(x253,x252,x254,x255)+~E(x251,x252)+~P5(x253,x251,x254,x255)
% 1.44/1.68 [26]P5(x263,x264,x262,x265)+~E(x261,x262)+~P5(x263,x264,x261,x265)
% 1.44/1.68 [27]P5(x273,x274,x275,x272)+~E(x271,x272)+~P5(x273,x274,x275,x271)
% 1.44/1.68 [28]P11(x282,x283)+~E(x281,x282)+~P11(x281,x283)
% 1.44/1.68 [29]P11(x293,x292)+~E(x291,x292)+~P11(x293,x291)
% 1.44/1.68 [30]P12(x302,x303)+~E(x301,x302)+~P12(x301,x303)
% 1.44/1.68 [31]P12(x313,x312)+~E(x311,x312)+~P12(x313,x311)
% 1.44/1.68 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324)
% 1.44/1.68 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334)
% 1.44/1.68 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341)
% 1.44/1.68 [35]P10(x352,x353,x354)+~E(x351,x352)+~P10(x351,x353,x354)
% 1.44/1.68 [36]P10(x363,x362,x364)+~E(x361,x362)+~P10(x363,x361,x364)
% 1.44/1.68 [37]P10(x373,x374,x372)+~E(x371,x372)+~P10(x373,x374,x371)
% 1.44/1.68 [38]P7(x382,x383,x384,x385)+~E(x381,x382)+~P7(x381,x383,x384,x385)
% 1.44/1.68 [39]P7(x393,x392,x394,x395)+~E(x391,x392)+~P7(x393,x391,x394,x395)
% 1.44/1.68 [40]P7(x403,x404,x402,x405)+~E(x401,x402)+~P7(x403,x404,x401,x405)
% 1.44/1.68 [41]P7(x413,x414,x415,x412)+~E(x411,x412)+~P7(x413,x414,x415,x411)
% 1.44/1.68 [42]P8(x422,x423,x424)+~E(x421,x422)+~P8(x421,x423,x424)
% 1.44/1.68 [43]P8(x433,x432,x434)+~E(x431,x432)+~P8(x433,x431,x434)
% 1.44/1.68 [44]P8(x443,x444,x442)+~E(x441,x442)+~P8(x443,x444,x441)
% 1.44/1.68 [45]P9(x452,x453,x454)+~E(x451,x452)+~P9(x451,x453,x454)
% 1.44/1.68 [46]P9(x463,x462,x464)+~E(x461,x462)+~P9(x463,x461,x464)
% 1.44/1.68 [47]P9(x473,x474,x472)+~E(x471,x472)+~P9(x473,x474,x471)
% 1.44/1.68 [48]P6(x482,x483,x484,x485)+~E(x481,x482)+~P6(x481,x483,x484,x485)
% 1.44/1.68 [49]P6(x493,x492,x494,x495)+~E(x491,x492)+~P6(x493,x491,x494,x495)
% 1.44/1.68 [50]P6(x503,x504,x502,x505)+~E(x501,x502)+~P6(x503,x504,x501,x505)
% 1.44/1.68 [51]P6(x513,x514,x515,x512)+~E(x511,x512)+~P6(x513,x514,x515,x511)
% 1.44/1.68 [52]P4(x522,x523,x524,x525)+~E(x521,x522)+~P4(x521,x523,x524,x525)
% 1.44/1.68 [53]P4(x533,x532,x534,x535)+~E(x531,x532)+~P4(x533,x531,x534,x535)
% 1.44/1.68 [54]P4(x543,x544,x542,x545)+~E(x541,x542)+~P4(x543,x544,x541,x545)
% 1.44/1.68 [55]P4(x553,x554,x555,x552)+~E(x551,x552)+~P4(x553,x554,x555,x551)
% 1.44/1.68
% 1.44/1.68 %-------------------------------------------
% 1.44/1.68 cnf(115,plain,
% 1.44/1.68 (P12(x1151,x1151)),
% 1.44/1.68 inference(equality_inference,[],[69])).
% 1.44/1.68 cnf(496,plain,
% 1.44/1.68 ($false),
% 1.44/1.68 inference(scs_inference,[],[62,115,91,100]),
% 1.44/1.68 ['proof']).
% 1.44/1.68 % SZS output end Proof
% 1.44/1.68 % Total time :1.162629s
%------------------------------------------------------------------------------