%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n009.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:26 AM UTC 2026 % Result : Theorem 58.37s 58.53s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.06/0.33 % Computer : n009.cluster.edu % 0.06/0.33 % Model : x86_64 x86_64 % 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.33 % Memory : 8046.5625MB % 0.06/0.33 % OS : Linux 6.8.0-71-generic % 0.06/0.33 % CPULimit : 300 % 0.06/0.33 % WCLimit : 300 % 0.06/0.33 % DateTime : Mon Sep 7 14:09:37 UTC 2026 % 0.06/0.34 % CPUTime : % 0.24/0.50 start to proof:theBenchmark % 58.37/58.52 %------------------------------------------- % 58.37/58.52 % File :CSE---1.7 % 58.37/58.52 % Problem :theBenchmark % 58.37/58.52 % Transform :cnf % 58.37/58.52 % Format :tptp:raw % 58.37/58.52 % Command :java -jar mcs_scs.jar %d %s % 58.37/58.52 % 58.37/58.52 % Result :Theorem 58.009935s % 58.37/58.52 % Output :CNFRefutation 58.009935s % 58.37/58.52 %------------------------------------------- % 58.37/58.52 %-------------------------------------------------------------------------- % 58.37/58.52 % File : MGT117+1 : TPTP v9.3.0. Released v9.3.0. % 58.37/58.52 % Domain : Management % 58.37/58.52 % Problem : Strong perm creates Disability in assigner (positive conjecture) % 58.37/58.52 % Version : Especial. % 58.37/58.52 % English : perm(p1) + strong(p1) + activates(e1,p1). % 58.37/58.52 % Conjecture: exists Disability(museen, read, museum_api) in % 58.37/58.52 % some rho_I. Tests Ax5.2 positive entailment directly. % 58.37/58.52 % 58.37/58.52 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL % 58.37/58.52 % Source : [MC+26] % 58.37/58.52 % Names : GRND034-disability-exists-1.p [MC+26] % 58.37/58.52 % 58.37/58.52 % Status : Theorem % 58.37/58.52 % Rating : 0.00 v9.3.0 % 58.37/58.52 % Syntax : Number of formulae : 15 ( 13 unt; 0 def) % 58.37/58.52 % Number of atoms : 34 ( 0 equ) % 58.37/58.52 % Maximal formula atoms : 16 ( 2 avg) % 58.37/58.52 % Number of connectives : 19 ( 0 ~; 0 |; 18 &) % 58.37/58.52 % ( 0 <=>; 1 =>; 0 <=; 0 <~>) % 58.37/58.52 % Maximal formula depth : 19 ( 3 avg) % 58.37/58.52 % Maximal term depth : 1 ( 1 avg) % 58.37/58.52 % Number of predicates : 18 ( 18 usr; 0 prp; 1-3 aty) % 58.37/58.52 % Number of functors : 6 ( 6 usr; 6 con; 0-0 aty) % 58.37/58.52 % Number of variables : 11 ( 6 !; 5 ?) % 58.37/58.52 % SPC : FOF_THM_RFO_NEQ % 58.37/58.52 % 58.37/58.52 % Comments : % 58.37/58.52 %-------------------------------------------------------------------------- % 58.37/58.52 %----Layer 1: Problem-specific axioms (subset of Ax5.1-5.11, A1-A3, B1-B3) % 58.37/58.52 fof(ax_perm_relator_strong,axiom, % 58.37/58.52 ! [P,X,Y,A,T,E] : % 58.37/58.52 ( ( perm(P) % 58.37/58.52 & strong(P) % 58.37/58.52 & aee(P,X) % 58.37/58.52 & aer(P,Y) % 58.37/58.52 & act(P,A) % 58.37/58.52 & tgt(P,T) % 58.37/58.52 & activates(E,P) ) % 58.37/58.52 => ? [RhoI,Im,Db] : % 58.37/58.52 ( founds_imm(E,RhoI,P) % 58.37/58.52 & immunity(Im) % 58.37/58.52 & bearer(Im,X) % 58.37/58.52 & cnt(Im,A,T) % 58.37/58.52 & part_of(Im,RhoI) % 58.37/58.52 & disability(Db) % 58.37/58.52 & bearer(Db,Y) % 58.37/58.52 & cnt(Db,A,T) % 58.37/58.52 & part_of(Db,RhoI) ) ) ). % 58.37/58.52 % 58.37/58.52 %----Ground instance (gamma) % 58.37/58.52 fof(agent_bibliothek,axiom, % 58.37/58.52 agent(bibliothek) ). % 58.37/58.52 % 58.37/58.52 fof(agent_museen,axiom, % 58.37/58.52 agent(museen) ). % 58.37/58.53 % 58.37/58.53 fof(action_read,axiom, % 58.37/58.53 action(read) ). % 58.37/58.53 % 58.37/58.53 fof(target_museum,axiom, % 58.37/58.53 target(museum_api) ). % 58.37/58.53 % 58.37/58.53 fof(rule_p1,axiom, % 58.37/58.53 rule(p1) ). % 58.37/58.53 % 58.37/58.53 fof(event_e1,axiom, % 58.37/58.53 event(e1) ). % 58.37/58.53 % 58.37/58.53 fof(perm_p1,axiom, % 58.37/58.53 perm(p1) ). % 58.37/58.53 % 58.37/58.53 fof(strong_p1,axiom, % 58.37/58.53 strong(p1) ). % 58.37/58.53 % 58.37/58.53 fof(aee_p1,axiom, % 58.37/58.53 aee(p1,bibliothek) ). % 58.37/58.53 % 58.37/58.53 fof(aer_p1,axiom, % 58.37/58.53 aer(p1,museen) ). % 58.37/58.53 % 58.37/58.53 fof(act_p1,axiom, % 58.37/58.53 act(p1,read) ). % 58.37/58.53 % 58.37/58.53 fof(tgt_p1,axiom, % 58.37/58.53 tgt(p1,museum_api) ). % 58.37/58.53 % 58.37/58.53 fof(act_e1_p1,axiom, % 58.37/58.53 activates(e1,p1) ). % 58.37/58.53 % 58.37/58.53 fof(conjecture,conjecture, % 58.37/58.53 ? [RhoI,Db] : % 58.37/58.53 ( founds_imm(e1,RhoI,p1) % 58.37/58.53 & disability(Db) % 58.37/58.53 & bearer(Db,museen) % 58.37/58.53 & cnt(Db,read,museum_api) % 58.37/58.53 & part_of(Db,RhoI) ) ). % 58.37/58.53 % 58.37/58.53 %-------------------------------------------------------------------------- % 58.37/58.53 %------------------------------------------- % 58.37/58.53 % Proof found % 58.37/58.53 % SZS status Theorem for theBenchmark % 58.37/58.53 % SZS output start Proof % 58.37/58.53 %ClaNum:23(EqnAxiom:0) % 58.37/58.53 %VarNum:188(SingletonVarNum:56) % 58.37/58.53 %MaxLitNum:8 % 58.37/58.53 %MaxfuncDepth:1 % 58.37/58.53 %SharedTerms:19 % 58.37/58.53 %goalClause: 14 % 58.37/58.53 [1]P1(a1) % 58.37/58.53 [2]P15(a1) % 58.37/58.53 [3]P2(a2) % 58.37/58.53 [4]P2(a3) % 58.37/58.53 [5]P3(a9) % 58.37/58.53 [6]P17(a8) % 58.37/58.53 [7]P16(a1) % 58.37/58.53 [8]P8(a4) % 58.37/58.53 [9]P5(a1,a2) % 58.37/58.53 [10]P7(a1,a3) % 58.37/58.53 [11]P4(a1,a9) % 58.37/58.53 [12]P18(a1,a8) % 58.37/58.53 [13]P6(a4,a1) % 58.37/58.53 [14]~P9(x141)+~P12(x141,x142)+~P10(x141,a3)+~P11(x141,a9,a8)+~P13(a4,x142,a1) % 58.37/58.53 [15]~P1(x151)+~P15(x151)+~P5(x151,x152)+~P7(x151,x153)+~P4(x151,x154)+~P18(x151,x155)+~P6(x156,x151)+P14(f5(x151,x152,x153,x154,x155,x156)) % 58.37/58.53 [16]~P1(x161)+~P15(x161)+~P5(x161,x162)+~P7(x161,x163)+~P4(x161,x164)+~P18(x161,x165)+~P6(x166,x161)+P9(f7(x161,x162,x163,x164,x165,x166)) % 58.37/58.53 [17]~P1(x171)+~P15(x171)+~P5(x171,x172)+~P7(x171,x173)+~P4(x171,x174)+~P18(x171,x175)+~P6(x176,x171)+P10(f5(x171,x172,x173,x174,x175,x176),x172) % 58.37/58.53 [18]~P1(x181)+~P15(x181)+~P5(x181,x182)+~P7(x181,x183)+~P4(x181,x184)+~P18(x181,x185)+~P6(x186,x181)+P10(f7(x181,x182,x183,x184,x185,x186),x183) % 58.37/58.53 [19]~P1(x192)+~P15(x192)+~P5(x192,x193)+~P7(x192,x194)+~P4(x192,x195)+~P18(x192,x196)+~P6(x191,x192)+P13(x191,f6(x192,x193,x194,x195,x196,x191),x192) % 58.37/58.53 [20]~P1(x201)+~P15(x201)+~P5(x201,x202)+~P7(x201,x203)+~P4(x201,x204)+~P18(x201,x205)+~P6(x206,x201)+P11(f5(x201,x202,x203,x204,x205,x206),x204,x205) % 58.37/58.53 [21]~P1(x211)+~P15(x211)+~P5(x211,x212)+~P7(x211,x213)+~P4(x211,x214)+~P18(x211,x215)+~P6(x216,x211)+P11(f7(x211,x212,x213,x214,x215,x216),x214,x215) % 58.37/58.53 [22]~P1(x221)+~P15(x221)+~P5(x221,x222)+~P7(x221,x223)+~P4(x221,x224)+~P18(x221,x225)+~P6(x226,x221)+P12(f5(x221,x222,x223,x224,x225,x226),f6(x221,x222,x223,x224,x225,x226)) % 58.37/58.53 [23]~P1(x231)+~P15(x231)+~P5(x231,x232)+~P7(x231,x233)+~P4(x231,x234)+~P18(x231,x235)+~P6(x236,x231)+P12(f7(x231,x232,x233,x234,x235,x236),f6(x231,x232,x233,x234,x235,x236)) % 58.37/58.53 %EqnAxiom % 58.37/58.53 % 58.37/58.53 %------------------------------------------- % 58.37/58.53 cnf(40,plain, % 58.37/58.53 ($false), % 58.37/58.53 inference(scs_inference,[],[1,2,9,10,11,12,13,16,17,18,19,20,21,22,23,14]), % 58.37/58.53 ['proof']). % 58.37/58.53 % SZS output end Proof % 58.37/58.53 % Total time :58.009935s %------------------------------------------------------------------------------