%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB012+2 : TPTP v8.2.0. Released v5.2.0. % 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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 16:05:19 EDT 2024 % Result : Theorem 0.58s 0.73s % Output : CNFRefutation 0.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB012+2 : TPTP v8.2.0. Released v5.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n018.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Jun 18 17:55:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.49/0.62 start to proof:theBenchmark % 0.58/0.72 %------------------------------------------- % 0.58/0.72 % File :CSE---1.7 % 0.58/0.72 % Problem :theBenchmark % 0.58/0.72 % Transform :cnf % 0.58/0.72 % Format :tptp:raw % 0.58/0.72 % Command :java -jar mcs_scs.jar %d %s % 0.58/0.72 % 0.58/0.72 % Result :Theorem 0.050000s % 0.58/0.72 % Output :CNFRefutation 0.050000s % 0.58/0.72 %------------------------------------------- % 0.58/0.72 %------------------------------------------------------------------------------ % 0.58/0.72 % File : SWB012+2 : TPTP v8.2.0. Released v5.2.0. % 0.58/0.72 % Domain : Semantic Web % 0.58/0.72 % Problem : Template Class % 0.58/0.73 % Version : [Sch11] axioms : Reduced > Incomplete. % 0.58/0.73 % English : % 0.58/0.73 % 0.58/0.73 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 0.58/0.73 % Source : [Sch11] % 0.58/0.73 % Names : 012_Template_Class [Sch11] % 0.58/0.73 % 0.58/0.73 % Status : Theorem % 0.58/0.73 % Rating : 0.06 v8.2.0, 0.13 v8.1.0, 0.07 v7.5.0, 0.14 v7.4.0, 0.06 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.07 v6.4.0, 0.00 v6.3.0, 0.08 v6.2.0, 0.18 v6.1.0, 0.16 v6.0.0, 0.50 v5.5.0, 0.21 v5.4.0, 0.13 v5.3.0, 0.22 v5.2.0 % 0.58/0.73 % Syntax : Number of formulae : 6 ( 0 unt; 0 def) % 0.58/0.73 % Number of atoms : 39 ( 0 equ) % 0.58/0.73 % Maximal formula atoms : 15 ( 6 avg) % 0.58/0.73 % Number of connectives : 33 ( 0 ~; 0 |; 26 &) % 0.58/0.73 % ( 4 <=>; 3 =>; 0 <=; 0 <~>) % 0.58/0.73 % Maximal formula depth : 18 ( 9 avg) % 0.58/0.73 % Maximal term depth : 2 ( 1 avg) % 0.58/0.73 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 0.58/0.73 % Number of functors : 18 ( 18 usr; 17 con; 0-1 aty) % 0.58/0.73 % Number of variables : 22 ( 18 !; 4 ?) % 0.58/0.73 % SPC : FOF_THM_RFO_NEQ % 0.58/0.73 % 0.58/0.73 % Comments : % 0.58/0.73 %------------------------------------------------------------------------------ % 0.58/0.73 fof(rdfs_cext_def,axiom, % 0.58/0.73 ! [X,C] : % 0.58/0.73 ( iext(uri_rdf_type,X,C) % 0.58/0.73 <=> icext(C,X) ) ). % 0.58/0.73 % 0.58/0.73 fof(rdfs_domain_main,axiom, % 0.58/0.73 ! [P,C,X,Y] : % 0.58/0.73 ( ( iext(uri_rdfs_domain,P,C) % 0.58/0.73 & iext(P,X,Y) ) % 0.58/0.73 => icext(C,X) ) ). % 0.58/0.73 % 0.58/0.73 fof(owl_bool_intersectionof_class_003,axiom, % 0.58/0.73 ! [Z,S1,C1,S2,C2,S3,C3] : % 0.58/0.73 ( ( iext(uri_rdf_first,S1,C1) % 0.58/0.73 & iext(uri_rdf_rest,S1,S2) % 0.58/0.73 & iext(uri_rdf_first,S2,C2) % 0.58/0.73 & iext(uri_rdf_rest,S2,S3) % 0.58/0.73 & iext(uri_rdf_first,S3,C3) % 0.58/0.73 & iext(uri_rdf_rest,S3,uri_rdf_nil) ) % 0.58/0.73 => ( iext(uri_owl_intersectionOf,Z,S1) % 0.58/0.73 <=> ( ic(Z) % 0.58/0.73 & ic(C1) % 0.58/0.73 & ic(C2) % 0.58/0.73 & ic(C3) % 0.58/0.73 & ! [X] : % 0.58/0.73 ( icext(Z,X) % 0.58/0.73 <=> ( icext(C1,X) % 0.58/0.73 & icext(C2,X) % 0.58/0.73 & icext(C3,X) ) ) ) ) ) ). % 0.58/0.73 % 0.58/0.73 fof(owl_restrict_hasvalue,axiom, % 0.58/0.73 ! [Z,P,A] : % 0.58/0.73 ( ( iext(uri_owl_hasValue,Z,A) % 0.58/0.73 & iext(uri_owl_onProperty,Z,P) ) % 0.58/0.73 => ! [X] : % 0.58/0.73 ( icext(Z,X) % 0.58/0.73 <=> iext(P,X,A) ) ) ). % 0.58/0.73 % 0.58/0.73 fof(testcase_conclusion_fullish_012_Template_Class,conjecture, % 0.58/0.73 ( iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty) % 0.58/0.73 & iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person) ) ). % 0.58/0.73 % 0.58/0.73 fof(testcase_premise_fullish_012_Template_Class,axiom, % 0.58/0.73 ? [BNODE_l1,BNODE_l2,BNODE_l3,BNODE_r] : % 0.58/0.73 ( iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class) % 0.58/0.73 & iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1) % 0.58/0.73 & iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty) % 0.58/0.73 & iext(uri_rdf_rest,BNODE_l1,BNODE_l2) % 0.58/0.73 & iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty) % 0.58/0.73 & iext(uri_rdf_rest,BNODE_l2,BNODE_l3) % 0.58/0.73 & iext(uri_rdf_first,BNODE_l3,BNODE_r) % 0.58/0.73 & iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil) % 0.58/0.73 & iext(uri_rdf_type,BNODE_r,uri_owl_Restriction) % 0.58/0.73 & iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain) % 0.58/0.73 & iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person) % 0.58/0.73 & iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute) % 0.58/0.73 & iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice)) ) ). % 0.58/0.73 % 0.58/0.73 %------------------------------------------------------------------------------ % 0.58/0.73 %------------------------------------------- % 0.58/0.73 % Proof found % 0.58/0.73 % SZS status Theorem for theBenchmark % 0.58/0.73 % SZS output start Proof % 0.58/0.73 %ClaNum:31(EqnAxiom:0) % 0.58/0.73 %VarNum:309(SingletonVarNum:104) % 0.58/0.73 %MaxLitNum:15 % 0.58/0.73 %MaxfuncDepth:1 % 0.58/0.73 %SharedTerms:37 % 0.58/0.73 %goalClause: 16 % 0.58/0.73 [1]P1(a1,a2,a3) % 0.58/0.73 [2]P1(a1,a12,a13) % 0.58/0.73 [3]P1(a1,a4,a14) % 0.58/0.73 [4]P1(a17,a5,a15) % 0.58/0.73 [5]P1(a17,a8,a16) % 0.58/0.73 [6]P1(a17,a9,a4) % 0.58/0.73 [7]P1(a21,a5,a8) % 0.58/0.73 [8]P1(a21,a8,a9) % 0.58/0.73 [9]P1(a21,a9,a22) % 0.58/0.73 [10]P1(a18,a3,a5) % 0.58/0.73 [11]P1(a19,a4,a12) % 0.58/0.73 [12]P1(a20,a4,a23) % 0.58/0.73 [13]P1(a2,a11,f10(a6)) % 0.58/0.73 [16]~P1(a1,a2,a16)+~P1(a1,a11,a12) % 0.58/0.73 [14]~P2(x142,x141)+P1(a1,x141,x142) % 0.58/0.73 [15]P2(x151,x152)+~P1(a1,x152,x151) % 0.58/0.73 [17]P2(x171,x172)+~P1(x173,x172,x174)+~P1(a23,x173,x171) % 0.58/0.73 [18]P1(x181,x182,x183)+~P2(x184,x182)+~P1(a19,x184,x183)+~P1(a20,x184,x181) % 0.58/0.73 [19]P2(x191,x192)+~P1(x193,x192,x194)+~P1(a19,x191,x194)+~P1(a20,x191,x193) % 0.58/0.73 [20]P3(x201)+~P1(a21,x203,x202)+~P1(a21,x205,x203)+~P1(a17,x202,x201)+~P1(a17,x203,x204)+~P1(a17,x205,x206)+~P1(a18,x207,x205)+~P1(a21,x202,a22) % 0.58/0.73 [21]P3(x211)+~P1(a21,x214,x212)+~P1(a21,x215,x214)+~P1(a17,x212,x213)+~P1(a17,x214,x211)+~P1(a17,x215,x216)+~P1(a18,x217,x215)+~P1(a21,x212,a22) % 0.58/0.73 [22]P3(x221)+~P1(a21,x224,x222)+~P1(a21,x226,x224)+~P1(a17,x222,x223)+~P1(a17,x224,x225)+~P1(a17,x226,x221)+~P1(a18,x227,x226)+~P1(a21,x222,a22) % 0.58/0.73 [23]P3(x231)+~P1(a21,x234,x232)+~P1(a21,x236,x234)+~P1(a18,x231,x236)+~P1(a17,x232,x233)+~P1(a17,x234,x235)+~P1(a17,x236,x237)+~P1(a21,x232,a22) % 0.58/0.73 [24]P2(x241,x242)+~P2(x243,x242)+~P1(a21,x245,x244)+~P1(a21,x247,x245)+~P1(a18,x243,x247)+~P1(a17,x244,x241)+~P1(a17,x245,x246)+~P1(a17,x247,x248)+~P1(a21,x244,a22) % 0.58/0.73 [25]P2(x251,x252)+~P2(x253,x252)+~P1(a21,x256,x254)+~P1(a21,x257,x256)+~P1(a18,x253,x257)+~P1(a17,x254,x255)+~P1(a17,x256,x251)+~P1(a17,x257,x258)+~P1(a21,x254,a22) % 0.58/0.73 [26]P2(x261,x262)+~P2(x263,x262)+~P1(a21,x266,x264)+~P1(a21,x268,x266)+~P1(a18,x263,x268)+~P1(a17,x264,x265)+~P1(a17,x266,x267)+~P1(a17,x268,x261)+~P1(a21,x264,a22) % 0.58/0.73 [27]P2(x271,x272)+~P2(x273,x272)+~P2(x274,x272)+~P2(x275,x272)+~P1(a21,x277,x276)+~P1(a21,x278,x277)+~P1(a18,x271,x278)+~P1(a17,x276,x273)+~P1(a17,x277,x274)+~P1(a17,x278,x275)+~P1(a21,x276,a22) % 0.58/0.73 [28]~P3(x285)+~P3(x283)+~P3(x281)+~P3(x287)+~P1(a17,x286,x287)+~P1(a17,x284,x285)+~P1(a17,x282,x283)+~P1(a21,x284,x286)+~P1(a21,x282,x284)+P1(a18,x281,x282)+P2(x281,f7(x281,x282,x283,x284,x285,x286,x287))+P2(x287,f7(x281,x282,x283,x284,x285,x286,x287))+~P1(a21,x286,a22) % 0.58/0.73 [29]~P3(x297)+~P3(x293)+~P3(x291)+~P3(x295)+~P1(a17,x296,x297)+~P1(a17,x294,x295)+~P1(a17,x292,x293)+~P1(a21,x294,x296)+~P1(a21,x292,x294)+P1(a18,x291,x292)+P2(x291,f7(x291,x292,x293,x294,x295,x296,x297))+P2(x295,f7(x291,x292,x293,x294,x295,x296,x297))+~P1(a21,x296,a22) % 0.58/0.73 [30]~P3(x307)+~P3(x305)+~P3(x301)+~P3(x303)+~P1(a17,x306,x307)+~P1(a17,x304,x305)+~P1(a17,x302,x303)+~P1(a21,x304,x306)+~P1(a21,x302,x304)+P1(a18,x301,x302)+P2(x301,f7(x301,x302,x303,x304,x305,x306,x307))+P2(x303,f7(x301,x302,x303,x304,x305,x306,x307))+~P1(a21,x306,a22) % 0.58/0.73 [31]~P3(x311)+~P3(x313)+~P3(x314)+~P3(x315)+~P1(a17,x312,x315)+~P1(a21,x317,x316)+~P1(a21,x312,x317)+P1(a18,x311,x312)+~P1(a17,x316,x313)+~P1(a17,x317,x314)+~P2(x313,f7(x311,x312,x315,x317,x314,x316,x313))+~P2(x314,f7(x311,x312,x315,x317,x314,x316,x313))+~P2(x315,f7(x311,x312,x315,x317,x314,x316,x313))+~P2(x311,f7(x311,x312,x315,x317,x314,x316,x313))+~P1(a21,x316,a22) % 0.58/0.73 %EqnAxiom % 0.58/0.73 % 0.58/0.73 %------------------------------------------- % 0.58/0.73 cnf(32,plain, % 0.58/0.73 (P2(a3,a2)), % 0.58/0.73 inference(scs_inference,[],[1,15])). % 0.58/0.73 cnf(44,plain, % 0.58/0.73 (P1(a23,a2,a12)), % 0.58/0.73 inference(scs_inference,[],[1,4,5,6,7,8,9,10,11,12,15,20,22,23,24,26,18])). % 0.58/0.73 cnf(53,plain, % 0.58/0.73 (P2(a16,a2)), % 0.58/0.73 inference(scs_inference,[],[32,2,5,7,8,6,9,10,4,15,21,25])). % 0.58/0.73 cnf(72,plain, % 0.58/0.73 (P1(a1,a11,a12)), % 0.58/0.73 inference(scs_inference,[],[44,13,14,17])). % 0.58/0.73 cnf(73,plain, % 0.58/0.73 (~P1(a1,a2,a16)), % 0.58/0.73 inference(scs_inference,[],[72,16])). % 0.58/0.73 cnf(75,plain, % 0.58/0.73 ($false), % 0.58/0.73 inference(scs_inference,[],[73,53,14]), % 0.58/0.73 ['proof']). % 0.58/0.73 % SZS output end Proof % 0.58/0.73 % Total time :0.050000s %------------------------------------------------------------------------------