%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB010+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 : n009.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:18 EDT 2024 % Result : Theorem 6.61s 6.71s % Output : CNFRefutation 6.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB010+2 : TPTP v8.2.0. Released v5.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n009.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Jun 18 18:54:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.41/0.61 start to proof:theBenchmark % 6.61/6.70 %------------------------------------------- % 6.61/6.70 % File :CSE---1.7 % 6.61/6.70 % Problem :theBenchmark % 6.61/6.70 % Transform :cnf % 6.61/6.70 % Format :tptp:raw % 6.61/6.70 % Command :java -jar mcs_scs.jar %d %s % 6.61/6.70 % 6.61/6.70 % Result :Theorem 6.040000s % 6.61/6.70 % Output :CNFRefutation 6.040000s % 6.61/6.70 %------------------------------------------- % 6.61/6.70 %------------------------------------------------------------------------------ % 6.61/6.70 % File : SWB010+2 : TPTP v8.2.0. Released v5.2.0. % 6.61/6.70 % Domain : Semantic Web % 6.61/6.70 % Problem : Negative Property Assertions % 6.61/6.70 % Version : [Sch11] axioms : Reduced > Incomplete. % 6.61/6.70 % English : % 6.61/6.70 % 6.61/6.70 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 6.61/6.70 % Source : [Sch11] % 6.61/6.70 % Names : 010_Negative_Property_Assertions [Sch11] % 6.61/6.70 % 6.61/6.70 % Status : Theorem % 6.61/6.70 % Rating : 0.31 v8.1.0, 0.33 v7.5.0, 0.34 v7.4.0, 0.30 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.17 v6.2.0, 0.28 v6.1.0, 0.23 v6.0.0, 0.26 v5.5.0, 0.22 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0 % 6.61/6.70 % Syntax : Number of formulae : 10 ( 1 unt; 0 def) % 6.61/6.70 % Number of atoms : 44 ( 1 equ) % 6.61/6.70 % Maximal formula atoms : 8 ( 4 avg) % 6.61/6.70 % Number of connectives : 36 ( 2 ~; 0 |; 22 &) % 6.61/6.70 % ( 5 <=>; 7 =>; 0 <=; 0 <~>) % 6.61/6.70 % Maximal formula depth : 12 ( 7 avg) % 6.61/6.70 % Maximal term depth : 1 ( 1 avg) % 6.61/6.70 % Number of predicates : 6 ( 5 usr; 0 prp; 1-3 aty) % 6.61/6.70 % Number of functors : 17 ( 17 usr; 17 con; 0-0 aty) % 6.61/6.70 % Number of variables : 28 ( 22 !; 6 ?) % 6.61/6.70 % SPC : FOF_THM_RFO_SEQ % 6.61/6.70 % 6.61/6.70 % Comments : % 6.61/6.70 %------------------------------------------------------------------------------ % 6.61/6.70 fof(simple_ir,axiom, % 6.61/6.71 ! [X] : ir(X) ). % 6.61/6.71 % 6.61/6.71 fof(rdfs_cext_def,axiom, % 6.61/6.71 ! [X,C] : % 6.61/6.71 ( iext(uri_rdf_type,X,C) % 6.61/6.71 <=> icext(C,X) ) ). % 6.61/6.71 % 6.61/6.71 fof(owl_prop_sourceindividual_ext,axiom, % 6.61/6.71 ! [X,Y] : % 6.61/6.71 ( iext(uri_owl_sourceIndividual,X,Y) % 6.61/6.71 => ( icext(uri_owl_NegativePropertyAssertion,X) % 6.61/6.71 & ir(Y) ) ) ). % 6.61/6.71 % 6.61/6.71 fof(owl_prop_onproperty_ext,axiom, % 6.61/6.71 ! [X,Y] : % 6.61/6.71 ( iext(uri_owl_onProperty,X,Y) % 6.61/6.71 => ( icext(uri_owl_Restriction,X) % 6.61/6.71 & ip(Y) ) ) ). % 6.61/6.71 % 6.61/6.71 fof(owl_bool_complementof_class,axiom, % 6.61/6.71 ! [Z,C] : % 6.61/6.71 ( iext(uri_owl_complementOf,Z,C) % 6.61/6.71 => ( ic(Z) % 6.61/6.71 & ic(C) % 6.61/6.71 & ! [X] : % 6.61/6.71 ( icext(Z,X) % 6.61/6.71 <=> ~ icext(C,X) ) ) ) ). % 6.61/6.71 % 6.61/6.71 fof(owl_enum_class_001,axiom, % 6.61/6.71 ! [Z,S1,A1] : % 6.61/6.71 ( ( iext(uri_rdf_first,S1,A1) % 6.61/6.71 & iext(uri_rdf_rest,S1,uri_rdf_nil) ) % 6.61/6.71 => ( iext(uri_owl_oneOf,Z,S1) % 6.61/6.71 <=> ( ic(Z) % 6.61/6.71 & ! [X] : % 6.61/6.71 ( icext(Z,X) % 6.61/6.71 <=> X = A1 ) ) ) ) ). % 6.61/6.71 % 6.61/6.71 fof(owl_restrict_allvaluesfrom,axiom, % 6.61/6.71 ! [Z,P,C] : % 6.61/6.71 ( ( iext(uri_owl_allValuesFrom,Z,C) % 6.61/6.71 & iext(uri_owl_onProperty,Z,P) ) % 6.61/6.71 => ! [X] : % 6.61/6.71 ( icext(Z,X) % 6.61/6.71 <=> ! [Y] : % 6.61/6.71 ( iext(P,X,Y) % 6.61/6.71 => icext(C,Y) ) ) ) ). % 6.61/6.71 % 6.61/6.71 fof(owl_npa_object_fi,axiom, % 6.61/6.71 ! [P,A1,A2] : % 6.61/6.71 ( ( ir(A1) % 6.61/6.71 & ip(P) % 6.61/6.71 & ir(A2) % 6.61/6.71 & ~ iext(P,A1,A2) ) % 6.61/6.71 => ? [Z] : % 6.61/6.71 ( iext(uri_owl_sourceIndividual,Z,A1) % 6.61/6.71 & iext(uri_owl_assertionProperty,Z,P) % 6.61/6.71 & iext(uri_owl_targetIndividual,Z,A2) ) ) ). % 6.61/6.71 % 6.61/6.71 fof(testcase_conclusion_fullish_010_Negative_Property_Assertions,conjecture, % 6.61/6.71 ? [BNODE_z] : % 6.61/6.71 ( iext(uri_rdf_type,BNODE_z,uri_owl_NegativePropertyAssertion) % 6.61/6.71 & iext(uri_owl_sourceIndividual,BNODE_z,uri_ex_s) % 6.61/6.71 & iext(uri_owl_assertionProperty,BNODE_z,uri_ex_p) % 6.61/6.71 & iext(uri_owl_targetIndividual,BNODE_z,uri_ex_o) ) ). % 6.61/6.71 % 6.61/6.71 fof(testcase_premise_fullish_010_Negative_Property_Assertions,axiom, % 6.61/6.71 ? [BNODE_x1,BNODE_x2,BNODE_x3,BNODE_x4] : % 6.61/6.71 ( iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty) % 6.61/6.71 & iext(uri_rdf_type,uri_ex_s,BNODE_x1) % 6.61/6.71 & iext(uri_owl_onProperty,BNODE_x1,uri_ex_p) % 6.61/6.71 & iext(uri_owl_allValuesFrom,BNODE_x1,BNODE_x2) % 6.61/6.71 & iext(uri_owl_complementOf,BNODE_x2,BNODE_x3) % 6.61/6.71 & iext(uri_owl_oneOf,BNODE_x3,BNODE_x4) % 6.61/6.71 & iext(uri_rdf_first,BNODE_x4,uri_ex_o) % 6.61/6.71 & iext(uri_rdf_rest,BNODE_x4,uri_rdf_nil) ) ). % 6.61/6.71 % 6.61/6.71 %------------------------------------------------------------------------------ % 6.61/6.71 %------------------------------------------- % 6.61/6.71 % Proof found % 6.61/6.71 % SZS status Theorem for theBenchmark % 6.61/6.71 % SZS output start Proof % 6.61/6.71 %ClaNum:49(EqnAxiom:20) % 6.61/6.71 %VarNum:149(SingletonVarNum:60) % 6.61/6.71 %MaxLitNum:6 % 6.61/6.71 %MaxfuncDepth:1 % 6.61/6.71 %SharedTerms:29 % 6.61/6.71 %goalClause: 45 % 6.61/6.71 [21]P1(a1,a2,a3) % 6.61/6.71 [22]P1(a1,a7,a12) % 6.61/6.71 [23]P1(a14,a3,a7) % 6.61/6.71 [24]P1(a15,a8,a9) % 6.61/6.71 [25]P1(a19,a10,a11) % 6.61/6.71 [26]P1(a23,a10,a24) % 6.61/6.71 [27]P1(a20,a9,a10) % 6.61/6.71 [28]P1(a16,a3,a8) % 6.61/6.71 [29]~P2(x292,x291)+P1(a1,x291,x292) % 6.61/6.71 [30]P4(x301)+~P1(a14,x302,x301) % 6.61/6.71 [31]P3(x311)+~P1(a15,x312,x311) % 6.61/6.71 [32]P3(x321)+~P1(a15,x321,x322) % 6.61/6.71 [33]~P1(a21,x331,x332)+P2(a13,x331) % 6.61/6.71 [34]~P1(a14,x341,x342)+P2(a17,x341) % 6.61/6.71 [35]P2(x351,x352)+~P1(a1,x352,x351) % 6.61/6.71 [36]P2(x361,x362)+P2(x363,x362)+~P1(a15,x361,x363) % 6.61/6.71 [37]~P2(x371,x372)+~P2(x373,x372)+~P1(a15,x373,x371) % 6.61/6.71 [38]~P4(x381)+P1(x381,x382,x383)+P1(a21,f4(x381,x382,x383),x382) % 6.61/6.71 [39]~P4(x391)+P1(x391,x392,x393)+P1(a18,f4(x391,x392,x393),x391) % 6.61/6.71 [40]~P4(x401)+P1(x401,x402,x403)+P1(a22,f4(x401,x402,x403),x403) % 6.61/6.71 [45]~P1(a21,x451,a2)+~P1(a18,x451,a7)+~P1(a22,x451,a11)+~P1(a1,x451,a13) % 6.61/6.71 [41]P3(x411)+~P1(a20,x411,x412)+~P1(a19,x412,x413)+~P1(a23,x412,a24) % 6.61/6.71 [48]P2(x481,x482)+~P1(a14,x481,x483)+~P1(a16,x481,x484)+P1(x483,x482,f6(x481,x483,x484,x482)) % 6.61/6.71 [49]P2(x491,x492)+~P1(a14,x491,x493)+~P1(a16,x491,x494)+~P2(x494,f6(x491,x493,x494,x492)) % 6.61/6.71 [42]P2(x421,x422)+~E(x422,x423)+~P1(a20,x421,x424)+~P1(a19,x424,x423)+~P1(a23,x424,a24) % 6.61/6.71 [43]E(x431,x432)+~P2(x433,x431)+~P1(a20,x433,x434)+~P1(a19,x434,x432)+~P1(a23,x434,a24) % 6.61/6.71 [44]P2(x441,x442)+~P1(x445,x444,x442)+~P2(x443,x444)+~P1(a14,x443,x445)+~P1(a16,x443,x441) % 6.61/6.71 [46]~P3(x461)+P1(a20,x461,x462)+~P1(a19,x462,x463)+E(f5(x461,x462,x463),x463)+P2(x461,f5(x461,x462,x463))+~P1(a23,x462,a24) % 6.61/6.71 [47]~P3(x471)+~P1(a19,x472,x473)+P1(a20,x471,x472)+~E(f5(x471,x472,x473),x473)+~P2(x471,f5(x471,x472,x473))+~P1(a23,x472,a24) % 6.61/6.71 %EqnAxiom % 6.61/6.71 [1]E(x11,x11) % 6.61/6.71 [2]E(x22,x21)+~E(x21,x22) % 6.61/6.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 6.61/6.71 [4]~E(x41,x42)+E(f4(x41,x43,x44),f4(x42,x43,x44)) % 6.61/6.71 [5]~E(x51,x52)+E(f4(x53,x51,x54),f4(x53,x52,x54)) % 6.61/6.71 [6]~E(x61,x62)+E(f4(x63,x64,x61),f4(x63,x64,x62)) % 6.61/6.71 [7]~E(x71,x72)+E(f6(x71,x73,x74,x75),f6(x72,x73,x74,x75)) % 6.61/6.71 [8]~E(x81,x82)+E(f6(x83,x81,x84,x85),f6(x83,x82,x84,x85)) % 6.61/6.71 [9]~E(x91,x92)+E(f6(x93,x94,x91,x95),f6(x93,x94,x92,x95)) % 6.61/6.71 [10]~E(x101,x102)+E(f6(x103,x104,x105,x101),f6(x103,x104,x105,x102)) % 6.61/6.71 [11]~E(x111,x112)+E(f5(x111,x113,x114),f5(x112,x113,x114)) % 6.61/6.71 [12]~E(x121,x122)+E(f5(x123,x121,x124),f5(x123,x122,x124)) % 6.61/6.71 [13]~E(x131,x132)+E(f5(x133,x134,x131),f5(x133,x134,x132)) % 6.61/6.71 [14]P1(x142,x143,x144)+~E(x141,x142)+~P1(x141,x143,x144) % 6.61/6.71 [15]P1(x153,x152,x154)+~E(x151,x152)+~P1(x153,x151,x154) % 6.61/6.71 [16]P1(x163,x164,x162)+~E(x161,x162)+~P1(x163,x164,x161) % 6.61/6.71 [17]P2(x172,x173)+~E(x171,x172)+~P2(x171,x173) % 6.61/6.71 [18]P2(x183,x182)+~E(x181,x182)+~P2(x183,x181) % 6.61/6.71 [19]~P4(x191)+P4(x192)+~E(x191,x192) % 6.61/6.71 [20]~P3(x201)+P3(x202)+~E(x201,x202) % 6.61/6.71 % 6.61/6.71 %------------------------------------------- % 6.61/6.71 cnf(50,plain, % 6.61/6.71 (P2(x501,x502)+~P1(a19,x503,x502)+~P1(a20,x501,x503)+~P1(a23,x503,a24)), % 6.61/6.71 inference(equality_inference,[],[42])). % 6.61/6.71 cnf(51,plain, % 6.61/6.71 (P4(a7)), % 6.61/6.71 inference(scs_inference,[],[23,30])). % 6.61/6.71 cnf(65,plain, % 6.61/6.71 (~P1(a7,a2,a11)), % 6.61/6.71 inference(scs_inference,[],[21,23,24,25,26,27,28,30,31,32,35,50,14,37,17,44])). % 6.61/6.71 cnf(556,plain, % 6.61/6.71 (P2(a13,f4(a7,a2,a11))), % 6.61/6.71 inference(scs_inference,[],[51,65,33,38])). % 6.61/6.71 cnf(1511,plain, % 6.61/6.71 (P1(a18,f4(a7,a2,a11),a7)), % 6.61/6.71 inference(scs_inference,[],[65,23,39,30])). % 6.61/6.71 cnf(1516,plain, % 6.61/6.71 (~P1(a22,f4(a7,a2,a11),a11)+~P1(a1,f4(a7,a2,a11),a13)+~P1(a21,f4(a7,a2,a11),a2)), % 6.61/6.71 inference(scs_inference,[],[1511,45])). % 6.61/6.71 cnf(1534,plain, % 6.61/6.71 (P1(a22,f4(a7,a2,a11),a11)), % 6.61/6.71 inference(scs_inference,[],[65,23,40,30])). % 6.61/6.71 cnf(1535,plain, % 6.61/6.71 (~P1(a1,f4(a7,a2,a11),a13)+~P1(a21,f4(a7,a2,a11),a2)), % 6.61/6.71 inference(scs_inference,[],[1534,1516])). % 6.61/6.71 cnf(1557,plain, % 6.61/6.71 (~P1(a21,f4(a7,a2,a11),a2)), % 6.61/6.71 inference(scs_inference,[],[556,1535,29])). % 6.61/6.71 cnf(1558,plain, % 6.61/6.71 ($false), % 6.61/6.71 inference(scs_inference,[],[1557,51,65,38]), % 6.61/6.71 ['proof']). % 6.61/6.71 % SZS output end Proof % 6.61/6.71 % Total time :6.040000s %------------------------------------------------------------------------------