%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB028+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 : n025.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:30 EDT 2024 % Result : Theorem 116.26s 116.39s % Output : CNFRefutation 116.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB028+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 : n025.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:41:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.54/0.59 start to proof:theBenchmark % 116.26/116.37 %------------------------------------------- % 116.26/116.37 % File :CSE---1.7 % 116.26/116.37 % Problem :theBenchmark % 116.26/116.37 % Transform :cnf % 116.26/116.37 % Format :tptp:raw % 116.26/116.37 % Command :java -jar mcs_scs.jar %d %s % 116.26/116.37 % 116.26/116.37 % Result :Theorem 115.620000s % 116.26/116.37 % Output :CNFRefutation 115.620000s % 116.26/116.37 %------------------------------------------- % 116.26/116.38 %------------------------------------------------------------------------------ % 116.26/116.38 % File : SWB028+2 : TPTP v8.2.0. Released v5.2.0. % 116.26/116.38 % Domain : Semantic Web % 116.26/116.38 % Problem : Inferred Property Characteristics III % 116.26/116.38 % Version : [Sch11] axioms : Reduced > Incomplete. % 116.26/116.38 % English : % 116.26/116.38 % 116.26/116.38 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 116.26/116.38 % Source : [Sch11] % 116.26/116.38 % Names : 028_Inferred_Property_Characteristics_III [Sch11] % 116.26/116.38 % 116.26/116.38 % Status : Theorem % 116.26/116.38 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.22 v7.4.0, 0.17 v7.3.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.25 v5.3.0, 0.26 v5.2.0 % 116.26/116.38 % Syntax : Number of formulae : 11 ( 2 unt; 0 def) % 116.26/116.38 % Number of atoms : 42 ( 2 equ) % 116.26/116.38 % Maximal formula atoms : 5 ( 3 avg) % 116.26/116.38 % Number of connectives : 31 ( 0 ~; 0 |; 17 &) % 116.26/116.38 % ( 8 <=>; 6 =>; 0 <=; 0 <~>) % 116.26/116.38 % Maximal formula depth : 9 ( 6 avg) % 116.26/116.38 % Maximal term depth : 1 ( 1 avg) % 116.26/116.38 % Number of predicates : 5 ( 4 usr; 0 prp; 1-3 aty) % 116.26/116.38 % Number of functors : 10 ( 10 usr; 10 con; 0-0 aty) % 116.26/116.38 % Number of variables : 28 ( 26 !; 2 ?) % 116.26/116.38 % SPC : FOF_THM_RFO_SEQ % 116.26/116.38 % 116.26/116.38 % Comments : % 116.26/116.38 %------------------------------------------------------------------------------ % 116.26/116.38 fof(owl_class_inversefunctionalproperty_type,axiom, % 116.26/116.38 ic(uri_owl_InverseFunctionalProperty) ). % 116.26/116.38 % 116.26/116.38 fof(owl_prop_inverseof_ext,axiom, % 116.26/116.38 ! [X,Y] : % 116.26/116.38 ( iext(uri_owl_inverseOf,X,Y) % 116.26/116.38 => ( ip(X) % 116.26/116.38 & ip(Y) ) ) ). % 116.26/116.38 % 116.26/116.38 fof(owl_prop_equivalentclass_ext,axiom, % 116.26/116.38 ! [X,Y] : % 116.26/116.38 ( iext(uri_owl_equivalentClass,X,Y) % 116.26/116.38 => ( ic(X) % 116.26/116.38 & ic(Y) ) ) ). % 116.26/116.38 % 116.26/116.38 fof(owl_char_functional,axiom, % 116.26/116.38 ! [P] : % 116.26/116.38 ( icext(uri_owl_FunctionalProperty,P) % 116.26/116.38 <=> ( ip(P) % 116.26/116.38 & ! [X,Y1,Y2] : % 116.26/116.38 ( ( iext(P,X,Y1) % 116.26/116.38 & iext(P,X,Y2) ) % 116.26/116.38 => Y1 = Y2 ) ) ) ). % 116.26/116.38 % 116.26/116.38 fof(owl_char_inversefunctional,axiom, % 116.26/116.38 ! [P] : % 116.26/116.38 ( icext(uri_owl_InverseFunctionalProperty,P) % 116.26/116.38 <=> ( ip(P) % 116.26/116.38 & ! [X1,X2,Y] : % 116.26/116.38 ( ( iext(P,X1,Y) % 116.26/116.38 & iext(P,X2,Y) ) % 116.26/116.38 => X1 = X2 ) ) ) ). % 116.26/116.38 % 116.26/116.38 fof(owl_rdfsext_subclassof,axiom, % 116.26/116.38 ! [C1,C2] : % 116.26/116.38 ( iext(uri_rdfs_subClassOf,C1,C2) % 116.26/116.38 <=> ( ic(C1) % 116.26/116.38 & ic(C2) % 116.26/116.38 & ! [X] : % 116.26/116.38 ( icext(C1,X) % 116.26/116.38 => icext(C2,X) ) ) ) ). % 116.26/116.38 % 116.26/116.38 fof(owl_eqdis_equivalentclass,axiom, % 116.26/116.38 ! [C1,C2] : % 116.26/116.38 ( iext(uri_owl_equivalentClass,C1,C2) % 116.26/116.38 <=> ( ic(C1) % 116.26/116.38 & ic(C2) % 116.26/116.38 & ! [X] : % 116.26/116.38 ( icext(C1,X) % 116.26/116.38 <=> icext(C2,X) ) ) ) ). % 116.26/116.38 % 116.26/116.38 fof(owl_restrict_somevaluesfrom,axiom, % 116.26/116.38 ! [Z,P,C] : % 116.26/116.38 ( ( iext(uri_owl_someValuesFrom,Z,C) % 116.26/116.39 & iext(uri_owl_onProperty,Z,P) ) % 116.26/116.39 => ! [X] : % 116.26/116.39 ( icext(Z,X) % 116.26/116.39 <=> ? [Y] : % 116.26/116.39 ( iext(P,X,Y) % 116.26/116.39 & icext(C,Y) ) ) ) ). % 116.26/116.39 % 116.26/116.39 fof(owl_inv,axiom, % 116.26/116.39 ! [P1,P2] : % 116.26/116.39 ( iext(uri_owl_inverseOf,P1,P2) % 116.26/116.39 <=> ( ip(P1) % 116.26/116.39 & ip(P2) % 116.26/116.39 & ! [X,Y] : % 116.26/116.39 ( iext(P1,X,Y) % 116.26/116.39 <=> iext(P2,Y,X) ) ) ) ). % 116.26/116.39 % 116.26/116.39 fof(testcase_conclusion_fullish_028_Inferred_Property_Characteristics_III,conjecture, % 116.26/116.39 iext(uri_rdfs_subClassOf,uri_ex_InversesOfFunctionalProperties,uri_owl_InverseFunctionalProperty) ). % 116.26/116.39 % 116.26/116.39 fof(testcase_premise_fullish_028_Inferred_Property_Characteristics_III,axiom, % 116.26/116.39 ? [BNODE_z] : % 116.26/116.39 ( iext(uri_owl_equivalentClass,uri_ex_InversesOfFunctionalProperties,BNODE_z) % 116.26/116.39 & iext(uri_rdf_type,BNODE_z,uri_owl_Restriction) % 116.26/116.39 & iext(uri_owl_onProperty,BNODE_z,uri_owl_inverseOf) % 116.26/116.39 & iext(uri_owl_someValuesFrom,BNODE_z,uri_owl_FunctionalProperty) ) ). % 116.26/116.39 % 116.26/116.39 %------------------------------------------------------------------------------ % 116.26/116.39 %------------------------------------------- % 116.26/116.39 % Proof found % 116.26/116.39 % SZS status Theorem for theBenchmark % 116.26/116.39 % SZS output start Proof % 116.26/116.39 %ClaNum:68(EqnAxiom:28) % 116.26/116.39 %VarNum:198(SingletonVarNum:70) % 116.26/116.39 %MaxLitNum:5 % 116.26/116.39 %MaxfuncDepth:1 % 116.26/116.39 %SharedTerms:17 % 116.26/116.39 %goalClause: 34 % 116.26/116.39 %singleGoalClaCount:1 % 116.26/116.39 [29]P1(a1) % 116.26/116.39 [30]P2(a16,a2,a3) % 116.26/116.39 [31]P2(a18,a3,a15) % 116.26/116.39 [32]P2(a19,a3,a20) % 116.26/116.39 [33]P2(a21,a3,a17) % 116.26/116.39 [34]~P2(a22,a2,a1) % 116.26/116.39 [35]P4(x351)+~P3(a1,x351) % 116.26/116.39 [36]P4(x361)+~P3(a15,x361) % 116.26/116.39 [44]P1(x441)+~P2(a16,x442,x441) % 116.26/116.39 [46]P1(x461)+~P2(a16,x461,x462) % 116.26/116.39 [47]P1(x471)+~P2(a22,x472,x471) % 116.26/116.39 [48]P1(x481)+~P2(a22,x481,x482) % 116.26/116.39 [50]P4(x501)+~P2(a20,x502,x501) % 116.26/116.39 [52]P4(x521)+~P2(a20,x521,x522) % 116.26/116.39 [37]~P4(x371)+~E(f6(x371),f7(x371))+P3(a1,x371) % 116.26/116.39 [38]~P4(x381)+~E(f8(x381),f10(x381))+P3(a15,x381) % 116.26/116.39 [39]~P4(x391)+P2(x391,f7(x391),f11(x391))+P3(a1,x391) % 116.26/116.39 [40]~P4(x401)+P2(x401,f6(x401),f11(x401))+P3(a1,x401) % 116.26/116.39 [41]~P4(x411)+P2(x411,f9(x411),f8(x411))+P3(a15,x411) % 116.26/116.39 [42]~P4(x421)+P2(x421,f9(x421),f10(x421))+P3(a15,x421) % 116.26/116.39 [54]P3(x541,x542)+~P3(x543,x542)+~P2(a16,x541,x543) % 116.26/116.39 [55]P3(x551,x552)+~P3(x553,x552)+~P2(a16,x553,x551) % 116.26/116.39 [56]P3(x561,x562)+~P3(x563,x562)+~P2(a22,x563,x561) % 116.26/116.39 [62]P2(x621,x622,x623)+~P2(x624,x623,x622)+~P2(a20,x621,x624) % 116.26/116.39 [63]P2(x631,x632,x633)+~P2(x634,x633,x632)+~P2(a20,x634,x631) % 116.26/116.39 [53]~P1(x532)+~P1(x531)+P2(a22,x531,x532)+P3(x531,f12(x531,x532)) % 116.26/116.39 [57]~P1(x571)+~P1(x572)+P2(a22,x571,x572)+~P3(x572,f12(x571,x572)) % 116.26/116.39 [60]~P2(x603,x604,x601)+E(x601,x602)+~P2(x603,x604,x602)+~P3(a15,x603) % 116.26/116.39 [61]~P2(x613,x611,x614)+E(x611,x612)+~P2(x613,x612,x614)+~P3(a1,x613) % 116.26/116.39 [67]~P3(x672,x674)+~P2(a18,x672,x671)+~P2(a19,x672,x673)+P3(x671,f14(x672,x673,x671,x674)) % 116.26/116.39 [68]~P3(x683,x682)+~P2(a18,x683,x684)+~P2(a19,x683,x681)+P2(x681,x682,f14(x683,x681,x684,x682)) % 116.26/116.39 [58]~P1(x582)+~P1(x581)+P2(a16,x581,x582)+P3(x582,f13(x581,x582))+P3(x581,f13(x581,x582)) % 116.26/116.39 [59]~P1(x592)+~P1(x591)+P2(a16,x591,x592)+~P3(x592,f13(x591,x592))+~P3(x591,f13(x591,x592)) % 116.26/116.39 [64]~P4(x642)+~P4(x641)+P2(x642,f4(x641,x642),f5(x641,x642))+P2(x641,f5(x641,x642),f4(x641,x642))+P2(a20,x641,x642) % 116.26/116.39 [66]~P4(x662)+~P4(x661)+~P2(x662,f4(x661,x662),f5(x661,x662))+~P2(x661,f5(x661,x662),f4(x661,x662))+P2(a20,x661,x662) % 116.26/116.39 [65]P3(x651,x652)+~P2(x655,x652,x654)+~P3(x653,x654)+~P2(a18,x651,x653)+~P2(a19,x651,x655) % 116.26/116.39 %EqnAxiom % 116.26/116.39 [1]E(x11,x11) % 116.26/116.39 [2]E(x22,x21)+~E(x21,x22) % 116.26/116.39 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.26/116.39 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 116.26/116.39 [5]~E(x51,x52)+E(f7(x51),f7(x52)) % 116.26/116.39 [6]~E(x61,x62)+E(f8(x61),f8(x62)) % 116.26/116.39 [7]~E(x71,x72)+E(f10(x71),f10(x72)) % 116.26/116.39 [8]~E(x81,x82)+E(f14(x81,x83,x84,x85),f14(x82,x83,x84,x85)) % 116.26/116.39 [9]~E(x91,x92)+E(f14(x93,x91,x94,x95),f14(x93,x92,x94,x95)) % 116.26/116.39 [10]~E(x101,x102)+E(f14(x103,x104,x101,x105),f14(x103,x104,x102,x105)) % 116.26/116.39 [11]~E(x111,x112)+E(f14(x113,x114,x115,x111),f14(x113,x114,x115,x112)) % 116.26/116.39 [12]~E(x121,x122)+E(f11(x121),f11(x122)) % 116.26/116.39 [13]~E(x131,x132)+E(f5(x131,x133),f5(x132,x133)) % 116.26/116.39 [14]~E(x141,x142)+E(f5(x143,x141),f5(x143,x142)) % 116.26/116.39 [15]~E(x151,x152)+E(f4(x151,x153),f4(x152,x153)) % 116.26/116.39 [16]~E(x161,x162)+E(f4(x163,x161),f4(x163,x162)) % 116.26/116.39 [17]~E(x171,x172)+E(f9(x171),f9(x172)) % 116.26/116.39 [18]~E(x181,x182)+E(f13(x181,x183),f13(x182,x183)) % 116.26/116.39 [19]~E(x191,x192)+E(f13(x193,x191),f13(x193,x192)) % 116.26/116.39 [20]~E(x201,x202)+E(f12(x201,x203),f12(x202,x203)) % 116.26/116.39 [21]~E(x211,x212)+E(f12(x213,x211),f12(x213,x212)) % 116.26/116.39 [22]~P1(x221)+P1(x222)+~E(x221,x222) % 116.26/116.39 [23]P2(x232,x233,x234)+~E(x231,x232)+~P2(x231,x233,x234) % 116.26/116.39 [24]P2(x243,x242,x244)+~E(x241,x242)+~P2(x243,x241,x244) % 116.26/116.39 [25]P2(x253,x254,x252)+~E(x251,x252)+~P2(x253,x254,x251) % 116.26/116.39 [26]P3(x262,x263)+~E(x261,x262)+~P3(x261,x263) % 116.26/116.39 [27]P3(x273,x272)+~E(x271,x272)+~P3(x273,x271) % 116.26/116.39 [28]~P4(x281)+P4(x282)+~E(x281,x282) % 116.26/116.39 % 116.26/116.39 %------------------------------------------- % 116.26/116.40 cnf(71,plain, % 116.26/116.40 (P1(a2)), % 116.26/116.40 inference(scs_inference,[],[30,44,46])). % 116.26/116.40 cnf(79,plain, % 116.26/116.40 (P3(a2,x791)+~P3(a3,x791)), % 116.26/116.40 inference(scs_inference,[],[31,30,25,54])). % 116.26/116.40 cnf(93,plain, % 116.26/116.40 (P3(a3,x931)+~P3(a2,x931)), % 116.26/116.40 inference(scs_inference,[],[30,32,25,55])). % 116.26/116.40 cnf(329,plain, % 116.26/116.40 (P3(a3,f12(a2,a1))), % 116.26/116.40 inference(scs_inference,[],[34,29,71,93,53])). % 116.26/116.40 cnf(331,plain, % 116.26/116.40 (P3(a2,f12(a2,a1))), % 116.26/116.40 inference(scs_inference,[],[329,79])). % 116.26/116.40 cnf(3679,plain, % 116.26/116.40 (~E(a2,x36791)+P1(x36791)), % 116.26/116.40 inference(scs_inference,[],[71,22])). % 116.26/116.40 cnf(3904,plain, % 116.26/116.40 (~P3(a1,f12(a2,a1))), % 116.26/116.40 inference(scs_inference,[],[34,29,3679,57])). % 116.26/116.40 cnf(6256,plain, % 116.26/116.40 (~P2(a20,f12(a2,a1),x62561)+~E(f6(f12(a2,a1)),f7(f12(a2,a1)))), % 116.26/116.40 inference(scs_inference,[],[3904,52,37])). % 116.26/116.40 cnf(6321,plain, % 116.26/116.40 (P2(f12(a2,a1),f7(f12(a2,a1)),f11(f12(a2,a1)))+~P2(a20,f12(a2,a1),x63211)), % 116.26/116.40 inference(scs_inference,[],[3904,52,39])). % 116.26/116.40 cnf(6352,plain, % 116.26/116.40 (P2(f12(a2,a1),f6(f12(a2,a1)),f11(f12(a2,a1)))+~P2(a20,f12(a2,a1),x63521)), % 116.26/116.40 inference(scs_inference,[],[3904,52,40])). % 116.26/116.40 cnf(6894,plain, % 116.26/116.40 (P2(a20,f12(a2,a1),f14(a3,a20,a15,f12(a2,a1)))), % 116.26/116.40 inference(scs_inference,[],[331,31,32,93,68])). % 116.26/116.40 cnf(6895,plain, % 116.26/116.40 (~E(f6(f12(a2,a1)),f7(f12(a2,a1)))), % 116.26/116.40 inference(scs_inference,[],[6894,6256])). % 116.26/116.40 cnf(6896,plain, % 116.26/116.40 (P2(f12(a2,a1),f7(f12(a2,a1)),f11(f12(a2,a1)))), % 116.26/116.40 inference(scs_inference,[],[6894,6321])). % 116.26/116.40 cnf(6897,plain, % 116.26/116.40 (P2(f12(a2,a1),f6(f12(a2,a1)),f11(f12(a2,a1)))), % 116.26/116.40 inference(scs_inference,[],[6894,6352])). % 116.26/116.40 cnf(6903,plain, % 116.26/116.40 (P2(f14(a3,a20,a15,f12(a2,a1)),x69031,x69032)+~P2(f12(a2,a1),x69032,x69031)), % 116.26/116.40 inference(scs_inference,[],[6894,63])). % 116.26/116.40 cnf(6937,plain, % 116.26/116.40 (P3(a15,f14(a3,a20,a15,f12(a2,a1)))), % 116.26/116.40 inference(scs_inference,[],[331,31,32,93,67])). % 116.26/116.40 cnf(12492,plain, % 116.26/116.40 (~P2(f14(a3,a20,a15,f12(a2,a1)),f11(f12(a2,a1)),f6(f12(a2,a1)))), % 116.26/116.40 inference(scs_inference,[],[6895,6896,6937,6903,2,60])). % 116.26/116.40 cnf(12507,plain, % 116.26/116.40 ($false), % 116.26/116.40 inference(scs_inference,[],[12492,6897,6903]), % 116.26/116.40 ['proof']). % 116.26/116.40 % SZS output end Proof % 116.26/116.40 % Total time :115.620000s %------------------------------------------------------------------------------