%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB023+2 : TPTP v8.2.0. Released v5.2.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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 16:05:26 EDT 2024 % Result : Theorem 3.83s 3.92s % Output : CNFRefutation 3.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB023+2 : TPTP v8.2.0. Released v5.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 17:45:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 3.83/3.91 %------------------------------------------- % 3.83/3.91 % File :CSE---1.7 % 3.83/3.91 % Problem :theBenchmark % 3.83/3.91 % Transform :cnf % 3.83/3.91 % Format :tptp:raw % 3.83/3.91 % Command :java -jar mcs_scs.jar %d %s % 3.83/3.91 % 3.83/3.91 % Result :Theorem 3.310000s % 3.83/3.91 % Output :CNFRefutation 3.310000s % 3.83/3.91 %------------------------------------------- % 3.83/3.91 %------------------------------------------------------------------------------ % 3.83/3.91 % File : SWB023+2 : TPTP v8.2.0. Released v5.2.0. % 3.83/3.91 % Domain : Semantic Web % 3.83/3.91 % Problem : Unique List Components % 3.83/3.91 % Version : [Sch11] axioms : Reduced > Incomplete. % 3.83/3.91 % English : % 3.83/3.91 % 3.83/3.91 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 3.83/3.91 % Source : [Sch11] % 3.83/3.91 % Names : 023_Unique_List_Components [Sch11] % 3.83/3.91 % 3.83/3.91 % Status : Theorem % 3.83/3.91 % Rating : 0.08 v8.1.0, 0.03 v7.1.0, 0.00 v6.4.0, 0.04 v6.2.0, 0.08 v6.1.0, 0.13 v5.5.0, 0.07 v5.3.0, 0.15 v5.2.0 % 3.83/3.91 % Syntax : Number of formulae : 6 ( 0 unt; 0 def) % 3.83/3.91 % Number of atoms : 24 ( 3 equ) % 3.83/3.91 % Maximal formula atoms : 7 ( 4 avg) % 3.83/3.91 % Number of connectives : 18 ( 0 ~; 0 |; 11 &) % 3.83/3.91 % ( 5 <=>; 2 =>; 0 <=; 0 <~>) % 3.83/3.91 % Maximal formula depth : 9 ( 6 avg) % 3.83/3.91 % Maximal term depth : 1 ( 1 avg) % 3.83/3.91 % Number of predicates : 5 ( 4 usr; 0 prp; 1-3 aty) % 3.83/3.91 % Number of functors : 11 ( 11 usr; 11 con; 0-0 aty) % 3.83/3.91 % Number of variables : 14 ( 12 !; 2 ?) % 3.83/3.91 % SPC : FOF_THM_RFO_SEQ % 3.83/3.91 % 3.83/3.91 % Comments : % 3.83/3.91 %------------------------------------------------------------------------------ % 3.83/3.91 fof(rdfs_cext_def,axiom, % 3.83/3.91 ! [X,C] : % 3.83/3.91 ( iext(uri_rdf_type,X,C) % 3.83/3.91 <=> icext(C,X) ) ). % 3.83/3.91 % 3.83/3.91 fof(owl_enum_class_001,axiom, % 3.83/3.92 ! [Z,S1,A1] : % 3.83/3.92 ( ( iext(uri_rdf_first,S1,A1) % 3.83/3.92 & iext(uri_rdf_rest,S1,uri_rdf_nil) ) % 3.83/3.92 => ( iext(uri_owl_oneOf,Z,S1) % 3.83/3.92 <=> ( ic(Z) % 3.83/3.92 & ! [X] : % 3.83/3.92 ( icext(Z,X) % 3.83/3.92 <=> X = A1 ) ) ) ) ). % 3.83/3.92 % 3.83/3.92 fof(owl_char_functional,axiom, % 3.83/3.92 ! [P] : % 3.83/3.92 ( icext(uri_owl_FunctionalProperty,P) % 3.83/3.92 <=> ( ip(P) % 3.83/3.92 & ! [X,Y1,Y2] : % 3.83/3.92 ( ( iext(P,X,Y1) % 3.83/3.92 & iext(P,X,Y2) ) % 3.83/3.92 => Y1 = Y2 ) ) ) ). % 3.83/3.92 % 3.83/3.92 fof(owl_eqdis_sameas,axiom, % 3.83/3.92 ! [X,Y] : % 3.83/3.92 ( iext(uri_owl_sameAs,X,Y) % 3.83/3.92 <=> X = Y ) ). % 3.83/3.92 % 3.83/3.92 fof(testcase_conclusion_fullish_023_Unique_List_Components,conjecture, % 3.83/3.92 ( iext(uri_owl_sameAs,uri_ex_w,uri_ex_u) % 3.83/3.92 & iext(uri_owl_sameAs,uri_ex_w,uri_ex_v) ) ). % 3.83/3.92 % 3.83/3.92 fof(testcase_premise_fullish_023_Unique_List_Components,axiom, % 3.83/3.92 ? [BNODE_o,BNODE_l] : % 3.83/3.92 ( iext(uri_rdf_type,uri_rdf_first,uri_owl_FunctionalProperty) % 3.83/3.92 & iext(uri_rdf_type,uri_ex_w,BNODE_o) % 3.83/3.92 & iext(uri_rdf_type,BNODE_o,uri_owl_Class) % 3.83/3.92 & iext(uri_owl_oneOf,BNODE_o,BNODE_l) % 3.83/3.92 & iext(uri_rdf_first,BNODE_l,uri_ex_u) % 3.83/3.92 & iext(uri_rdf_first,BNODE_l,uri_ex_v) % 3.83/3.92 & iext(uri_rdf_rest,BNODE_l,uri_rdf_nil) ) ). % 3.83/3.92 % 3.83/3.92 %------------------------------------------------------------------------------ % 3.83/3.92 %------------------------------------------- % 3.83/3.92 % Proof found % 3.83/3.92 % SZS status Theorem for theBenchmark % 3.83/3.92 % SZS output start Proof % 3.83/3.92 %ClaNum:38(EqnAxiom:16) % 3.83/3.92 %VarNum:93(SingletonVarNum:33) % 3.83/3.92 %MaxLitNum:6 % 3.83/3.92 %MaxfuncDepth:1 % 3.83/3.92 %SharedTerms:22 % 3.83/3.92 %goalClause: 32 % 3.83/3.92 [17]P1(a1,a2,a3) % 3.83/3.92 [18]P1(a1,a4,a5) % 3.83/3.92 [19]P1(a1,a5,a13) % 3.83/3.92 [20]P1(a2,a10,a11) % 3.83/3.92 [21]P1(a2,a10,a12) % 3.83/3.92 [22]P1(a16,a10,a17) % 3.83/3.92 [23]P1(a14,a5,a10) % 3.83/3.92 [32]~P1(a15,a4,a11)+~P1(a15,a4,a12) % 3.83/3.92 [24]P4(x241)+~P2(a3,x241) % 3.83/3.92 [26]~E(x261,x262)+P1(a15,x261,x262) % 3.83/3.92 [27]~P2(x272,x271)+P1(a1,x271,x272) % 3.83/3.92 [28]E(x281,x282)+~P1(a15,x281,x282) % 3.83/3.92 [31]P2(x311,x312)+~P1(a1,x312,x311) % 3.83/3.92 [25]~P4(x251)+~E(f6(x251),f7(x251))+P2(a3,x251) % 3.83/3.92 [29]~P4(x291)+P1(x291,f8(x291),f7(x291))+P2(a3,x291) % 3.83/3.92 [30]~P4(x301)+P1(x301,f8(x301),f6(x301))+P2(a3,x301) % 3.83/3.92 [34]P3(x341)+~P1(a14,x341,x342)+~P1(a2,x342,x343)+~P1(a16,x342,a17) % 3.83/3.92 [33]~P1(x333,x334,x331)+E(x331,x332)+~P1(x333,x334,x332)+~P2(a3,x333) % 3.83/3.92 [35]P2(x351,x352)+~E(x352,x353)+~P1(a14,x351,x354)+~P1(a2,x354,x353)+~P1(a16,x354,a17) % 3.83/3.92 [36]E(x361,x362)+~P2(x363,x361)+~P1(a14,x363,x364)+~P1(a2,x364,x362)+~P1(a16,x364,a17) % 3.83/3.92 [37]~P3(x371)+P1(a14,x371,x372)+~P1(a2,x372,x373)+E(f9(x371,x372,x373),x373)+P2(x371,f9(x371,x372,x373))+~P1(a16,x372,a17) % 3.83/3.92 [38]~P3(x381)+~P1(a2,x382,x383)+P1(a14,x381,x382)+~E(f9(x381,x382,x383),x383)+~P2(x381,f9(x381,x382,x383))+~P1(a16,x382,a17) % 3.83/3.92 %EqnAxiom % 3.83/3.92 [1]E(x11,x11) % 3.83/3.92 [2]E(x22,x21)+~E(x21,x22) % 3.83/3.92 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 3.83/3.92 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 3.83/3.92 [5]~E(x51,x52)+E(f7(x51),f7(x52)) % 3.83/3.92 [6]~E(x61,x62)+E(f8(x61),f8(x62)) % 3.83/3.92 [7]~E(x71,x72)+E(f9(x71,x73,x74),f9(x72,x73,x74)) % 3.83/3.92 [8]~E(x81,x82)+E(f9(x83,x81,x84),f9(x83,x82,x84)) % 3.83/3.92 [9]~E(x91,x92)+E(f9(x93,x94,x91),f9(x93,x94,x92)) % 3.83/3.92 [10]P1(x102,x103,x104)+~E(x101,x102)+~P1(x101,x103,x104) % 3.83/3.92 [11]P1(x113,x112,x114)+~E(x111,x112)+~P1(x113,x111,x114) % 3.83/3.92 [12]P1(x123,x124,x122)+~E(x121,x122)+~P1(x123,x124,x121) % 3.83/3.92 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133) % 3.83/3.92 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141) % 3.83/3.92 [15]~P3(x151)+P3(x152)+~E(x151,x152) % 3.83/3.92 [16]~P4(x161)+P4(x162)+~E(x161,x162) % 3.83/3.92 % 3.83/3.92 %------------------------------------------- % 3.83/3.92 cnf(39,plain, % 3.83/3.92 (P1(a15,x391,x391)), % 3.83/3.92 inference(equality_inference,[],[26])). % 3.83/3.92 cnf(40,plain, % 3.83/3.92 (P2(x401,x402)+~P1(a2,x403,x402)+~P1(a14,x401,x403)+~P1(a16,x403,a17)), % 3.83/3.92 inference(equality_inference,[],[35])). % 3.83/3.92 cnf(45,plain, % 3.83/3.92 (P2(a5,a11)), % 3.83/3.92 inference(scs_inference,[],[17,20,22,23,31,34,40])). % 3.83/3.92 cnf(61,plain, % 3.83/3.92 (P2(a5,a4)), % 3.83/3.92 inference(scs_inference,[],[18,31])). % 3.83/3.92 cnf(67,plain, % 3.83/3.92 (E(a12,a11)), % 3.83/3.92 inference(scs_inference,[],[18,21,45,23,22,31,40,36,2])). % 3.83/3.92 cnf(170,plain, % 3.83/3.92 (E(a4,a12)), % 3.83/3.92 inference(scs_inference,[],[22,21,61,23,36])). % 3.83/3.92 cnf(1252,plain, % 3.83/3.92 (P1(a15,a12,a4)), % 3.83/3.92 inference(scs_inference,[],[39,170,11])). % 3.83/3.92 cnf(1253,plain, % 3.83/3.92 (P1(a15,x12531,x12531)), % 3.83/3.92 inference(rename_variables,[],[39])). % 3.83/3.92 cnf(1254,plain, % 3.83/3.92 (P1(a15,a4,a12)), % 3.83/3.92 inference(scs_inference,[],[39,1253,170,11,12])). % 3.83/3.92 cnf(1261,plain, % 3.83/3.92 (~P1(a15,a4,a11)), % 3.83/3.92 inference(scs_inference,[],[1254,32])). % 3.83/3.92 cnf(1263,plain, % 3.83/3.92 (P1(a15,a4,a11)), % 3.83/3.92 inference(scs_inference,[],[1252,1254,67,11,12])). % 3.83/3.92 cnf(1269,plain, % 3.83/3.92 ($false), % 3.83/3.92 inference(scs_inference,[],[1261,1263]), % 3.83/3.92 ['proof']). % 3.83/3.92 % SZS output end Proof % 3.83/3.92 % Total time :3.310000s %------------------------------------------------------------------------------