%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB004+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 : n007.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:14 EDT 2024 % Result : Theorem 44.04s 44.13s % Output : CNFRefutation 44.04s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB004+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.33 % Computer : n007.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 18:32:53 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.56 start to proof:theBenchmark % 44.04/44.12 %------------------------------------------- % 44.04/44.12 % File :CSE---1.7 % 44.04/44.12 % Problem :theBenchmark % 44.04/44.12 % Transform :cnf % 44.04/44.12 % Format :tptp:raw % 44.04/44.12 % Command :java -jar mcs_scs.jar %d %s % 44.04/44.12 % 44.04/44.12 % Result :Theorem 43.530000s % 44.04/44.12 % Output :CNFRefutation 43.530000s % 44.04/44.12 %------------------------------------------- % 44.04/44.13 %------------------------------------------------------------------------------ % 44.04/44.13 % File : SWB004+2 : TPTP v8.2.0. Released v5.2.0. % 44.04/44.13 % Domain : Semantic Web % 44.04/44.13 % Problem : Axiomatic Triples % 44.04/44.13 % Version : [Sch11] axioms : Reduced > Incomplete. % 44.04/44.13 % English : % 44.04/44.13 % 44.04/44.13 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 44.04/44.13 % Source : [Sch11] % 44.04/44.13 % Names : 004_Axiomatic_Triples [Sch11] % 44.04/44.13 % 44.04/44.13 % Status : Theorem % 44.04/44.13 % Rating : 0.00 v6.3.0, 0.08 v6.2.0, 0.00 v5.5.0, 0.04 v5.3.0, 0.09 v5.2.0 % 44.04/44.13 % Syntax : Number of formulae : 14 ( 5 unt; 0 def) % 44.04/44.13 % Number of atoms : 32 ( 0 equ) % 44.04/44.13 % Maximal formula atoms : 5 ( 2 avg) % 44.04/44.13 % Number of connectives : 18 ( 0 ~; 0 |; 8 &) % 44.04/44.13 % ( 8 <=>; 2 =>; 0 <=; 0 <~>) % 44.04/44.13 % Maximal formula depth : 8 ( 3 avg) % 44.04/44.13 % Maximal term depth : 1 ( 1 avg) % 44.04/44.13 % Number of predicates : 5 ( 5 usr; 0 prp; 1-3 aty) % 44.04/44.13 % Number of functors : 7 ( 7 usr; 7 con; 0-0 aty) % 44.04/44.13 % Number of variables : 14 ( 14 !; 0 ?) % 44.04/44.13 % SPC : FOF_THM_RFO_NEQ % 44.04/44.13 % 44.04/44.13 % Comments : % 44.04/44.13 %------------------------------------------------------------------------------ % 44.04/44.13 fof(simple_ir,axiom, % 44.04/44.13 ! [X] : ir(X) ). % 44.04/44.13 % 44.04/44.13 fof(rdfs_cext_def,axiom, % 44.04/44.13 ! [X,C] : % 44.04/44.13 ( iext(uri_rdf_type,X,C) % 44.04/44.13 <=> icext(C,X) ) ). % 44.04/44.13 % 44.04/44.13 fof(owl_parts_idc_cond_set,axiom, % 44.04/44.13 ! [X] : % 44.04/44.13 ( idc(X) % 44.04/44.13 => ic(X) ) ). % 44.04/44.13 % 44.04/44.13 fof(owl_class_classowl_type,axiom, % 44.04/44.13 ic(uri_owl_Class) ). % 44.04/44.13 % 44.04/44.13 fof(owl_class_classowl_ext,axiom, % 44.04/44.13 ! [X] : % 44.04/44.13 ( icext(uri_owl_Class,X) % 44.04/44.13 <=> ic(X) ) ). % 44.04/44.13 % 44.04/44.13 fof(owl_class_classrdfs_type,axiom, % 44.04/44.13 ic(uri_rdfs_Class) ). % 44.04/44.13 % 44.04/44.13 fof(owl_class_classrdfs_ext,axiom, % 44.04/44.13 ! [X] : % 44.04/44.13 ( icext(uri_rdfs_Class,X) % 44.04/44.13 <=> ic(X) ) ). % 44.04/44.13 % 44.04/44.13 fof(owl_class_datatype_type,axiom, % 44.04/44.13 ic(uri_rdfs_Datatype) ). % 44.04/44.13 % 44.04/44.13 fof(owl_class_datatype_ext,axiom, % 44.04/44.13 ! [X] : % 44.04/44.13 ( icext(uri_rdfs_Datatype,X) % 44.04/44.13 <=> idc(X) ) ). % 44.04/44.13 % 44.04/44.13 fof(owl_class_thing_type,axiom, % 44.04/44.13 ic(uri_owl_Thing) ). % 44.04/44.13 % 44.04/44.13 fof(owl_class_thing_ext,axiom, % 44.04/44.13 ! [X] : % 44.04/44.13 ( icext(uri_owl_Thing,X) % 44.04/44.13 <=> ir(X) ) ). % 44.04/44.13 % 44.04/44.13 fof(owl_rdfsext_subclassof,axiom, % 44.04/44.13 ! [C1,C2] : % 44.04/44.13 ( iext(uri_rdfs_subClassOf,C1,C2) % 44.04/44.13 <=> ( ic(C1) % 44.04/44.13 & ic(C2) % 44.04/44.13 & ! [X] : % 44.04/44.13 ( icext(C1,X) % 44.04/44.13 => icext(C2,X) ) ) ) ). % 44.04/44.13 % 44.04/44.13 fof(owl_eqdis_equivalentclass,axiom, % 44.04/44.13 ! [C1,C2] : % 44.04/44.13 ( iext(uri_owl_equivalentClass,C1,C2) % 44.04/44.13 <=> ( ic(C1) % 44.04/44.13 & ic(C2) % 44.04/44.13 & ! [X] : % 44.04/44.13 ( icext(C1,X) % 44.04/44.13 <=> icext(C2,X) ) ) ) ). % 44.04/44.13 % 44.04/44.13 fof(testcase_conclusion_fullish_004_Axiomatic_Triples,conjecture, % 44.04/44.13 ( iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) % 44.04/44.13 & iext(uri_rdf_type,uri_owl_Class,uri_owl_Class) % 44.04/44.13 & iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing) % 44.04/44.13 & iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) % 44.04/44.13 & iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class) ) ). % 44.04/44.13 % 44.04/44.13 %------------------------------------------------------------------------------ % 44.04/44.13 %------------------------------------------- % 44.04/44.13 % Proof found % 44.04/44.13 % SZS status Theorem for theBenchmark % 44.04/44.13 % SZS output start Proof % 44.04/44.13 %ClaNum:26(EqnAxiom:0) % 44.04/44.13 %VarNum:87(SingletonVarNum:37) % 44.04/44.13 %MaxLitNum:5 % 44.04/44.13 %MaxfuncDepth:1 % 44.04/44.13 %SharedTerms:16 % 44.04/44.13 %goalClause: 26 % 44.04/44.13 [1]P1(a1) % 44.04/44.13 [2]P1(a4) % 44.04/44.13 [3]P1(a8) % 44.04/44.13 [4]P1(a5) % 44.04/44.13 [5]P2(a5,x51) % 44.04/44.13 [6]~P3(x61)+P1(x61) % 44.04/44.13 [7]~P1(x71)+P2(a1,x71) % 44.04/44.13 [8]~P1(x81)+P2(a4,x81) % 44.04/44.13 [9]~P3(x91)+P2(a8,x91) % 44.04/44.13 [10]P3(x101)+~P2(a8,x101) % 44.04/44.13 [11]P1(x111)+~P2(a1,x111) % 44.04/44.13 [12]P1(x121)+~P2(a4,x121) % 44.04/44.13 [13]~P2(x132,x131)+P4(a6,x131,x132) % 44.04/44.13 [14]P1(x141)+~P4(a9,x142,x141) % 44.04/44.13 [15]P1(x151)+~P4(a9,x151,x152) % 44.04/44.13 [16]P1(x161)+~P4(a7,x162,x161) % 44.04/44.13 [17]P1(x171)+~P4(a7,x171,x172) % 44.04/44.13 [18]P2(x181,x182)+~P4(a6,x182,x181) % 44.04/44.13 [20]P2(x201,x202)+~P2(x203,x202)+~P4(a9,x203,x201) % 44.04/44.13 [21]P2(x211,x212)+~P2(x213,x212)+~P4(a7,x211,x213) % 44.04/44.13 [22]P2(x221,x222)+~P2(x223,x222)+~P4(a7,x223,x221) % 44.04/44.13 [19]~P1(x192)+~P1(x191)+P4(a9,x191,x192)+P2(x191,f2(x191,x192)) % 44.04/44.13 [23]~P1(x231)+~P1(x232)+P4(a9,x231,x232)+~P2(x232,f2(x231,x232)) % 44.04/44.13 [26]~P4(a6,a1,a1)+~P4(a6,a1,a5)+~P4(a9,a1,a5)+~P4(a9,a8,a1)+~P4(a7,a1,a4) % 44.04/44.13 [24]~P1(x242)+~P1(x241)+P4(a7,x241,x242)+P2(x242,f3(x241,x242))+P2(x241,f3(x241,x242)) % 44.04/44.13 [25]~P1(x252)+~P1(x251)+P4(a7,x251,x252)+~P2(x252,f3(x251,x252))+~P2(x251,f3(x251,x252)) % 44.04/44.13 %EqnAxiom % 44.04/44.13 % 44.04/44.13 %------------------------------------------- % 44.04/44.13 cnf(27,plain, % 44.04/44.13 (P4(a9,a1,a5)), % 44.04/44.13 inference(scs_inference,[],[1,5,4,23])). % 44.04/44.13 cnf(34,plain, % 44.04/44.13 (~P4(a6,a1,a1)+~P4(a6,a1,a5)+~P4(a9,a8,a1)+~P4(a7,a1,a4)), % 44.04/44.13 inference(scs_inference,[],[27,26])). % 44.04/44.13 cnf(35,plain, % 44.04/44.13 (P1(x351)+~P2(a8,x351)), % 44.04/44.13 inference(scs_inference,[],[6,10])). % 44.04/44.13 cnf(47,plain, % 44.04/44.13 (P2(a1,a1)), % 44.04/44.13 inference(scs_inference,[],[27,15,7])). % 44.04/44.13 cnf(55,plain, % 44.04/44.13 (P2(a1,x551)+~P2(a8,x551)), % 44.04/44.13 inference(scs_inference,[],[7,35])). % 44.04/44.13 cnf(56,plain, % 44.04/44.13 (~P3(x561)+P2(a1,x561)), % 44.04/44.13 inference(scs_inference,[],[55,9])). % 44.04/44.13 cnf(57,plain, % 44.04/44.14 (~P3(x571)+P4(a6,x571,a1)), % 44.04/44.14 inference(scs_inference,[],[56,13])). % 44.04/44.14 cnf(58,plain, % 44.04/44.14 (~P2(a8,x581)+P4(a6,x581,a1)), % 44.04/44.14 inference(scs_inference,[],[57,10])). % 44.04/44.14 cnf(59,plain, % 44.04/44.14 (~P4(a6,x591,a8)+P4(a6,x591,a1)), % 44.04/44.14 inference(scs_inference,[],[58,18])). % 44.04/44.14 cnf(60,plain, % 44.04/44.14 (P2(a1,x601)+~P4(a6,x601,a8)), % 44.04/44.14 inference(scs_inference,[],[59,18])). % 44.04/44.14 cnf(61,plain, % 44.04/44.14 (P4(a9,a8,a1)+~P4(a6,f2(a8,a1),a8)), % 44.04/44.14 inference(scs_inference,[],[3,1,60,23])). % 44.04/44.14 cnf(62,plain, % 44.04/44.14 (~P2(a8,f2(a8,a1))+P4(a9,a8,a1)), % 44.04/44.14 inference(scs_inference,[],[61,13])). % 44.04/44.14 cnf(264,plain, % 44.04/44.14 (~P3(x2641)+P4(a6,x2641,a8)), % 44.04/44.14 inference(scs_inference,[],[9,13])). % 44.04/44.14 cnf(721,plain, % 44.04/44.14 (P3(f2(a8,a1))+P4(a9,a8,a1)), % 44.04/44.14 inference(scs_inference,[],[1,3,10,19])). % 44.04/44.14 cnf(785,plain, % 44.04/44.14 (P1(f3(a1,a4))+P4(a7,a1,a4)+P2(a1,f3(a1,a4))), % 44.04/44.14 inference(scs_inference,[],[2,1,12,24])). % 44.04/44.14 cnf(1282,plain, % 44.04/44.14 (P4(a9,a8,a1)+P4(a6,f2(a8,a1),a8)), % 44.04/44.14 inference(scs_inference,[],[264,721])). % 44.04/44.14 cnf(1283,plain, % 44.04/44.14 (P2(a8,f2(a8,a1))+P4(a9,a8,a1)), % 44.04/44.14 inference(scs_inference,[],[1282,18])). % 44.04/44.14 cnf(1284,plain, % 44.04/44.14 (P4(a9,a8,a1)), % 44.04/44.14 inference(scs_inference,[],[1283,62])). % 44.04/44.14 cnf(1285,plain, % 44.04/44.14 (~P4(a7,a1,a4)+~P4(a6,a1,a1)+~P4(a6,a1,a5)), % 44.04/44.14 inference(scs_inference,[],[1284,34])). % 44.04/44.14 cnf(1286,plain, % 44.04/44.14 (~P4(a7,a1,a4)+~P4(a6,a1,a5)), % 44.04/44.14 inference(scs_inference,[],[47,1285,13])). % 44.04/44.14 cnf(1287,plain, % 44.04/44.14 (P2(a1,f3(a1,a4))+P1(f3(a1,a4))+~P4(a6,a1,a5)), % 44.04/44.14 inference(scs_inference,[],[1286,785])). % 44.04/44.14 cnf(1288,plain, % 44.04/44.14 (P1(f3(a1,a4))+~P4(a6,a1,a5)), % 44.04/44.14 inference(scs_inference,[],[1287,11])). % 44.04/44.14 cnf(1289,plain, % 44.04/44.14 (P2(a1,f3(a1,a4))+~P4(a6,a1,a5)), % 44.04/44.14 inference(scs_inference,[],[1288,7])). % 44.04/44.14 cnf(1290,plain, % 44.04/44.14 (P4(a6,f3(a1,a4),a1)+~P4(a6,a1,a5)), % 44.04/44.14 inference(scs_inference,[],[1289,13])). % 44.04/44.14 cnf(1291,plain, % 44.04/44.14 (P4(a6,f3(a1,a4),a1)), % 44.04/44.14 inference(scs_inference,[],[5,1290,13])). % 44.04/44.14 cnf(1292,plain, % 44.04/44.14 (P2(a1,f3(a1,a4))), % 44.04/44.14 inference(scs_inference,[],[1291,18])). % 44.04/44.14 cnf(1294,plain, % 44.04/44.14 (P1(f3(a1,a4))), % 44.04/44.14 inference(scs_inference,[],[1291,18,11])). % 44.04/44.14 cnf(2240,plain, % 44.04/44.14 (~P4(a7,a1,a4)), % 44.04/44.14 inference(scs_inference,[],[5,13,1286])). % 44.04/44.14 cnf(2241,plain, % 44.04/44.14 (P4(a6,f3(a1,a4),a4)), % 44.04/44.14 inference(scs_inference,[],[1294,13,8])). % 44.04/44.14 cnf(2244,plain, % 44.04/44.14 ($false), % 44.04/44.14 inference(scs_inference,[],[2240,2241,1292,1,2,18,25]), % 44.04/44.14 ['proof']). % 44.04/44.14 % SZS output end Proof % 44.04/44.14 % Total time :43.530000s %------------------------------------------------------------------------------