%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT113+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 : n016.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:25 AM UTC 2026 % Result : Theorem 58.39s 58.54s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.34 % Computer : n016.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:11:47 UTC 2026 % 0.07/0.35 % CPUTime : % 0.25/0.50 start to proof:theBenchmark % 58.39/58.53 %------------------------------------------- % 58.39/58.53 % File :CSE---1.7 % 58.39/58.53 % Problem :theBenchmark % 58.39/58.53 % Transform :cnf % 58.39/58.53 % Format :tptp:raw % 58.39/58.53 % Command :java -jar mcs_scs.jar %d %s % 58.39/58.53 % 58.39/58.53 % Result :Theorem 58.022534s % 58.39/58.53 % Output :CNFRefutation 58.022534s % 58.39/58.53 %------------------------------------------- % 58.39/58.53 %-------------------------------------------------------------------------- % 58.39/58.53 % File : MGT113+1 : TPTP v9.3.0. Released v9.3.0. % 58.39/58.53 % Domain : Management % 58.39/58.53 % Problem : A1-A3+B1: violation triggers norm state change requiring Power % 58.39/58.53 % Version : Especial. % 58.39/58.53 % English : proh(f1) + has_rem(f1) + does(marketplace,distrib,concert_ds). % 58.39/58.53 % B1: violation => NormStateChange. % 58.39/58.53 % A1: NormStateChange => InstEvent. % 58.39/58.53 % A2: InstEvent => competent agent. % 58.39/58.53 % A3: competence => Power+Subjection pair. % 58.39/58.53 % Conjecture: Power+Subjection in fresh rho_R founded via % 58.39/58.53 % founds_rem at e1. % 58.39/58.53 % 58.39/58.53 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL % 58.39/58.53 % Source : [MC+26] % 58.39/58.53 % Names : GRND017-violation-chain-1.p [MC+26] % 58.39/58.53 % 58.39/58.53 % Status : Theorem % 58.39/58.53 % Rating : 0.00 v9.3.0 % 58.39/58.53 % Syntax : Number of formulae : 23 ( 14 unt; 0 def) % 58.39/58.53 % Number of atoms : 86 ( 0 equ) % 58.39/58.53 % Maximal formula atoms : 16 ( 3 avg) % 58.39/58.53 % Number of connectives : 63 ( 0 ~; 0 |; 55 &) % 58.39/58.53 % ( 0 <=>; 8 =>; 0 <=; 0 <~>) % 58.39/58.53 % Maximal formula depth : 19 ( 5 avg) % 58.39/58.53 % Maximal term depth : 2 ( 1 avg) % 58.39/58.53 % Number of predicates : 28 ( 28 usr; 0 prp; 1-5 aty) % 58.39/58.53 % Number of functors : 9 ( 9 usr; 7 con; 0-1 aty) % 58.39/58.53 % Number of variables : 50 ( 35 !; 15 ?) % 58.39/58.53 % SPC : FOF_THM_RFO_NEQ % 58.39/58.53 % 58.39/58.53 % Comments : % 58.39/58.53 %-------------------------------------------------------------------------- % 58.39/58.53 %----Layer 1: Problem-specific axioms (subset of Ax5.1-5.11, A1-A3, B1-B3) % 58.39/58.53 fof(ax_proh_relator_conduct,axiom, % 58.39/58.53 ! [F,X,Y,A,T,E] : % 58.39/58.53 ( ( proh(F) % 58.39/58.53 & aee(F,X) % 58.39/58.53 & aer(F,Y) % 58.39/58.53 & act(F,A) % 58.39/58.53 & tgt(F,T) % 58.39/58.53 & activates(E,F) ) % 58.39/58.53 => ? [Rho,D,C] : % 58.39/58.53 ( founds(E,Rho,F) % 58.39/58.53 & duty(D) % 58.39/58.53 & bearer(D,X) % 58.39/58.53 & cnt(D,rfr(A),T) % 58.39/58.53 & part_of(D,Rho) % 58.39/58.53 & right(C) % 58.39/58.53 & bearer(C,Y) % 58.39/58.53 & cnt(C,rfr(A),T) % 58.39/58.53 & part_of(C,Rho) ) ) ). % 58.39/58.53 % 58.39/58.53 fof(ax_proh_relator_remedy,axiom, % 58.39/58.53 ! [F,X,Y,A,T,E] : % 58.39/58.53 ( ( proh(F) % 58.39/58.53 & has_rem(F) % 58.39/58.53 & aee(F,X) % 58.39/58.53 & aer(F,Y) % 58.39/58.53 & act(F,A) % 58.39/58.53 & tgt(F,T) % 58.39/58.53 & activates(E,F) ) % 58.39/58.53 => ? [RhoR,Pw,S] : % 58.39/58.53 ( founds_rem(E,RhoR,F) % 58.39/58.53 & power(Pw) % 58.39/58.54 & bearer(Pw,Y) % 58.39/58.54 & cnt(Pw,decl(A),T) % 58.39/58.54 & part_of(Pw,RhoR) % 58.39/58.54 & subjection(S) % 58.39/58.54 & bearer(S,X) % 58.39/58.54 & cnt(S,decl(A),T) % 58.39/58.54 & part_of(S,RhoR) ) ) ). % 58.39/58.54 % 58.39/58.54 fof(ax_A1,axiom, % 58.39/58.54 ! [X,A,T,Q] : % 58.39/58.54 ( norm_state_change(X,A,T,Q) % 58.39/58.54 => ? [E] : % 58.39/58.54 ( inst_event(E) % 58.39/58.54 & triggers(E,X,A,T,Q) ) ) ). % 58.39/58.54 % 58.39/58.54 fof(ax_A2,axiom, % 58.39/58.54 ! [E] : % 58.39/58.54 ( inst_event(E) % 58.39/58.54 => ? [Y] : competent_for(Y,E) ) ). % 58.39/58.54 % 58.39/58.54 fof(ax_A3,axiom, % 58.39/58.54 ! [Y,E] : % 58.39/58.54 ( competent_for(Y,E) % 58.39/58.54 => ? [Pw,S,X] : % 58.39/58.54 ( power(Pw) % 58.39/58.54 & bearer(Pw,Y) % 58.39/58.54 & about_event(Pw,E) % 58.39/58.54 & subjection(S) % 58.39/58.54 & bearer(S,X) % 58.39/58.54 & about_event(S,E) ) ) ). % 58.39/58.54 % 58.39/58.54 fof(ax_B1,axiom, % 58.39/58.54 ! [F,X,A,T] : % 58.39/58.54 ( ( proh(F) % 58.39/58.54 & has_rem(F) % 58.39/58.54 & act(F,A) % 58.39/58.54 & tgt(F,T) % 58.39/58.54 & aee(F,X) % 58.39/58.54 & does(X,A,T) ) % 58.39/58.54 => ? [B] : % 58.39/58.54 ( rem_act(F,B) % 58.39/58.54 & norm_state_change(X,B,T,duty_rem) ) ) ). % 58.39/58.54 % 58.39/58.54 fof(ax_B2,axiom, % 58.39/58.54 ! [Pw,A,T,Rho,E,R] : % 58.39/58.54 ( ( power(Pw) % 58.39/58.54 & cnt(Pw,decl(A),T) % 58.39/58.54 & part_of(Pw,Rho) % 58.39/58.54 & founds_rem(E,Rho,R) ) % 58.39/58.54 => about_event(Pw,E) ) ). % 58.39/58.54 % 58.39/58.54 fof(ax_B3,axiom, % 58.39/58.54 ! [S,A,T,Rho,E,R] : % 58.39/58.54 ( ( subjection(S) % 58.39/58.54 & cnt(S,decl(A),T) % 58.39/58.54 & part_of(S,Rho) % 58.39/58.54 & founds_rem(E,Rho,R) ) % 58.39/58.54 => about_event(S,E) ) ). % 58.39/58.54 % 58.39/58.54 %----Ground instance (gamma) % 58.39/58.54 fof(agent_marketplace,axiom, % 58.39/58.54 agent(marketplace) ). % 58.39/58.54 % 58.39/58.54 fof(agent_philharmonie,axiom, % 58.39/58.54 agent(philharmonie) ). % 58.39/58.54 % 58.39/58.54 fof(action_distrib,axiom, % 58.39/58.54 action(distrib) ). % 58.39/58.54 % 58.39/58.54 fof(target_concert,axiom, % 58.39/58.54 target(concert_ds) ). % 58.39/58.54 % 58.39/58.54 fof(rule_f1,axiom, % 58.39/58.54 rule(f1) ). % 58.39/58.54 % 58.39/58.54 fof(event_e1,axiom, % 58.39/58.54 event(e1) ). % 58.39/58.54 % 58.39/58.54 fof(proh_f1,axiom, % 58.39/58.54 proh(f1) ). % 58.39/58.54 % 58.39/58.54 fof(rem_f1,axiom, % 58.39/58.54 has_rem(f1) ). % 58.39/58.54 % 58.39/58.54 fof(aee_f1,axiom, % 58.39/58.54 aee(f1,marketplace) ). % 58.39/58.54 % 58.39/58.54 fof(aer_f1,axiom, % 58.39/58.54 aer(f1,philharmonie) ). % 58.39/58.54 % 58.39/58.54 fof(act_f1,axiom, % 58.39/58.54 act(f1,distrib) ). % 58.39/58.54 % 58.39/58.54 fof(tgt_f1,axiom, % 58.39/58.54 tgt(f1,concert_ds) ). % 58.39/58.54 % 58.39/58.54 fof(act_e1_f1,axiom, % 58.39/58.54 activates(e1,f1) ). % 58.39/58.54 % 58.39/58.54 fof(marketplace_does,axiom, % 58.39/58.54 does(marketplace,distrib,concert_ds) ). % 58.39/58.54 % 58.39/58.54 fof(conjecture,conjecture, % 58.39/58.54 ? [RhoR,Pw,S] : % 58.39/58.54 ( founds_rem(e1,RhoR,f1) % 58.39/58.54 & power(Pw) % 58.39/58.54 & bearer(Pw,philharmonie) % 58.39/58.54 & cnt(Pw,decl(distrib),concert_ds) % 58.39/58.54 & part_of(Pw,RhoR) % 58.39/58.54 & about_event(Pw,e1) % 58.39/58.54 & subjection(S) % 58.39/58.54 & bearer(S,marketplace) % 58.39/58.54 & cnt(S,decl(distrib),concert_ds) % 58.39/58.54 & part_of(S,RhoR) % 58.39/58.54 & about_event(S,e1) ) ). % 58.39/58.54 % 58.39/58.54 %-------------------------------------------------------------------------- % 58.39/58.54 %------------------------------------------- % 58.39/58.54 % Proof found % 58.39/58.54 % SZS status Theorem for theBenchmark % 58.39/58.54 % SZS output start Proof % 58.39/58.54 %ClaNum:46(EqnAxiom:0) % 58.39/58.54 %VarNum:475(SingletonVarNum:152) % 58.39/58.54 %MaxLitNum:11 % 58.39/58.54 %MaxfuncDepth:1 % 58.39/58.54 %SharedTerms:22 % 58.39/58.54 %goalClause: 24 % 58.39/58.54 [1]P1(a1) % 58.39/58.54 [2]P2(a1) % 58.39/58.54 [3]P3(a19) % 58.39/58.54 [4]P3(a20) % 58.39/58.54 [5]P4(a2) % 58.39/58.54 [6]P22(a3) % 58.39/58.54 [7]P23(a1) % 58.39/58.54 [8]P10(a5) % 58.39/58.54 [9]P7(a1,a19) % 58.39/58.54 [10]P9(a1,a20) % 58.39/58.54 [11]P5(a1,a2) % 58.39/58.54 [12]P27(a1,a3) % 58.39/58.54 [13]P8(a5,a1) % 58.39/58.54 [14]P11(a19,a2,a3) % 58.39/58.54 [15]~P18(x151)+P12(f7(x151),x151) % 58.39/58.54 [16]~P12(x161,x162)+P19(f18(x161,x162)) % 58.39/58.54 [17]~P12(x171,x172)+P26(f8(x171,x172)) % 58.39/58.54 [18]~P12(x181,x182)+P13(f18(x181,x182),x181) % 58.39/58.54 [19]~P12(x191,x192)+P6(f18(x191,x192),x192) % 58.39/58.54 [20]~P12(x201,x202)+P6(f8(x201,x202),x202) % 58.39/58.54 [21]~P12(x211,x212)+P13(f8(x211,x212),f9(x211,x212)) % 58.39/58.54 [26]~P21(x261,x262,x263,x264)+P18(f11(x261,x262,x263,x264)) % 58.39/58.54 [28]~P21(x281,x282,x283,x284)+P28(f11(x281,x282,x283,x284),x281,x282,x283,x284) % 58.39/58.54 [22]~P19(x221)+P6(x221,x222)+~P16(x222,x223,x224)+~P20(x221,x223)+~P14(x221,f4(x225),x226) % 58.39/58.54 [23]~P26(x231)+P6(x231,x232)+~P16(x232,x233,x234)+~P20(x231,x233)+~P14(x231,f4(x235),x236) % 58.39/58.54 [25]~P1(x251)+~P2(x251)+~P7(x251,x252)+~P5(x251,x253)+~P27(x251,x254)+~P11(x252,x253,x254)+P24(x251,f10(x251,x252,x253,x254)) % 58.39/58.54 [27]~P1(x272)+~P2(x272)+~P7(x272,x271)+~P5(x272,x273)+~P27(x272,x274)+~P11(x271,x273,x274)+P21(x271,f10(x272,x271,x273,x274),x274,a6) % 58.39/58.54 [29]~P1(x291)+~P7(x291,x292)+~P9(x291,x293)+~P5(x291,x294)+~P27(x291,x295)+~P8(x296,x291)+P15(f12(x291,x292,x293,x294,x295,x296)) % 58.39/58.54 [30]~P1(x301)+~P7(x301,x302)+~P9(x301,x303)+~P5(x301,x304)+~P27(x301,x305)+~P8(x306,x301)+P25(f14(x301,x302,x303,x304,x305,x306)) % 58.39/58.54 [33]~P1(x331)+~P7(x331,x332)+~P9(x331,x333)+~P5(x331,x334)+~P27(x331,x335)+~P8(x336,x331)+P13(f12(x331,x332,x333,x334,x335,x336),x332) % 58.39/58.54 [34]~P1(x341)+~P7(x341,x342)+~P9(x341,x343)+~P5(x341,x344)+~P27(x341,x345)+~P8(x346,x341)+P13(f14(x341,x342,x343,x344,x345,x346),x343) % 58.39/58.54 [37]~P1(x372)+~P7(x372,x373)+~P9(x372,x374)+~P5(x372,x375)+~P27(x372,x376)+~P8(x371,x372)+P17(x371,f13(x372,x373,x374,x375,x376,x371),x372) % 58.39/58.54 [38]~P1(x381)+~P7(x381,x382)+~P9(x381,x383)+~P5(x381,x384)+~P27(x381,x385)+~P8(x386,x381)+P14(f12(x381,x382,x383,x384,x385,x386),f21(x384),x385) % 58.39/58.54 [39]~P1(x391)+~P7(x391,x392)+~P9(x391,x393)+~P5(x391,x394)+~P27(x391,x395)+~P8(x396,x391)+P14(f14(x391,x392,x393,x394,x395,x396),f21(x394),x395) % 58.39/58.54 [43]~P1(x431)+~P7(x431,x432)+~P9(x431,x433)+~P5(x431,x434)+~P27(x431,x435)+~P8(x436,x431)+P20(f12(x431,x432,x433,x434,x435,x436),f13(x431,x432,x433,x434,x435,x436)) % 58.39/58.54 [44]~P1(x441)+~P7(x441,x442)+~P9(x441,x443)+~P5(x441,x444)+~P27(x441,x445)+~P8(x446,x441)+P20(f14(x441,x442,x443,x444,x445,x446),f13(x441,x442,x443,x444,x445,x446)) % 58.39/58.54 [31]~P1(x311)+~P2(x311)+~P7(x311,x312)+~P9(x311,x313)+~P5(x311,x314)+~P27(x311,x315)+~P8(x316,x311)+P19(f15(x311,x312,x313,x314,x315,x316)) % 58.39/58.54 [32]~P1(x321)+~P2(x321)+~P7(x321,x322)+~P9(x321,x323)+~P5(x321,x324)+~P27(x321,x325)+~P8(x326,x321)+P26(f17(x321,x322,x323,x324,x325,x326)) % 58.39/58.54 [35]~P1(x351)+~P2(x351)+~P7(x351,x352)+~P9(x351,x353)+~P5(x351,x354)+~P27(x351,x355)+~P8(x356,x351)+P13(f15(x351,x352,x353,x354,x355,x356),x353) % 58.39/58.54 [36]~P1(x361)+~P2(x361)+~P7(x361,x362)+~P9(x361,x363)+~P5(x361,x364)+~P27(x361,x365)+~P8(x366,x361)+P13(f17(x361,x362,x363,x364,x365,x366),x362) % 58.39/58.54 [40]~P1(x402)+~P2(x402)+~P7(x402,x403)+~P9(x402,x404)+~P5(x402,x405)+~P27(x402,x406)+~P8(x401,x402)+P16(x401,f16(x402,x403,x404,x405,x406,x401),x402) % 58.39/58.54 [41]~P1(x411)+~P2(x411)+~P7(x411,x412)+~P9(x411,x413)+~P5(x411,x414)+~P27(x411,x415)+~P8(x416,x411)+P14(f15(x411,x412,x413,x414,x415,x416),f4(x414),x415) % 58.39/58.54 [42]~P1(x421)+~P2(x421)+~P7(x421,x422)+~P9(x421,x423)+~P5(x421,x424)+~P27(x421,x425)+~P8(x426,x421)+P14(f17(x421,x422,x423,x424,x425,x426),f4(x424),x425) % 58.39/58.54 [45]~P1(x451)+~P2(x451)+~P7(x451,x452)+~P9(x451,x453)+~P5(x451,x454)+~P27(x451,x455)+~P8(x456,x451)+P20(f15(x451,x452,x453,x454,x455,x456),f16(x451,x452,x453,x454,x455,x456)) % 58.39/58.54 [46]~P1(x461)+~P2(x461)+~P7(x461,x462)+~P9(x461,x463)+~P5(x461,x464)+~P27(x461,x465)+~P8(x466,x461)+P20(f17(x461,x462,x463,x464,x465,x466),f16(x461,x462,x463,x464,x465,x466)) % 58.39/58.54 [24]~P20(x241,x243)+~P19(x241)+~P20(x242,x243)+~P26(x242)+~P13(x242,a19)+~P13(x241,a20)+~P6(x242,a5)+~P6(x241,a5)+~P16(a5,x243,a1)+~P14(x242,f4(a2),a3)+~P14(x241,f4(a2),a3) % 58.39/58.54 %EqnAxiom % 58.39/58.54 % 58.39/58.54 %------------------------------------------- % 58.39/58.59 cnf(52954,plain, % 58.39/58.59 (P19(f15(a1,a19,a20,a2,a3,a5))), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31])). % 58.39/58.59 cnf(52956,plain, % 58.39/58.59 (P26(f17(a1,a19,a20,a2,a3,a5))), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31,32])). % 58.39/58.59 cnf(52958,plain, % 58.39/58.59 (P13(f15(a1,a19,a20,a2,a3,a5),a20)), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31,32,35])). % 58.39/58.59 cnf(52960,plain, % 58.39/58.59 (P13(f17(a1,a19,a20,a2,a3,a5),a19)), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31,32,35,36])). % 58.39/58.59 cnf(52962,plain, % 58.39/58.59 (P16(a5,f16(a1,a19,a20,a2,a3,a5),a1)), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31,32,35,36,40])). % 58.39/58.59 cnf(52964,plain, % 58.39/58.59 (P14(f15(a1,a19,a20,a2,a3,a5),f4(a2),a3)), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31,32,35,36,40,41])). % 58.39/58.59 cnf(52966,plain, % 58.39/58.59 (P14(f17(a1,a19,a20,a2,a3,a5),f4(a2),a3)), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31,32,35,36,40,41,42])). % 58.39/58.59 cnf(52968,plain, % 58.39/58.59 (P20(f15(a1,a19,a20,a2,a3,a5),f16(a1,a19,a20,a2,a3,a5))), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31,32,35,36,40,41,42,45])). % 58.39/58.59 cnf(52970,plain, % 58.39/58.59 (P20(f17(a1,a19,a20,a2,a3,a5),f16(a1,a19,a20,a2,a3,a5))), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31,32,35,36,40,41,42,45,46])). % 58.39/58.59 cnf(52972,plain, % 58.39/58.59 (P6(f15(a1,a19,a20,a2,a3,a5),a5)), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31,32,35,36,40,41,42,45,46,22])). % 58.39/58.59 cnf(52974,plain, % 58.39/58.59 (P6(f17(a1,a19,a20,a2,a3,a5),a5)), % 58.39/58.59 inference(scs_inference,[],[1,2,9,10,11,12,13,14,33,34,27,43,44,31,32,35,36,40,41,42,45,46,22,23])). % 58.39/58.59 cnf(52980,plain, % 58.39/58.59 ($false), % 58.39/58.59 inference(scs_inference,[],[52966,52974,52960,52956,52970,52964,52958,52972,52954,52962,52968,24]), % 58.39/58.59 ['proof']). % 58.53/58.61 % SZS output end Proof % 58.53/58.61 % Total time :58.022534s %------------------------------------------------------------------------------