%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB005+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 : n019.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 58.48s 58.72s % Output : CNFRefutation 58.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SWB005+2 : TPTP v8.2.0. Released v5.2.0. % 0.08/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n019.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Tue Jun 18 18:00:54 EDT 2024 % 0.11/0.33 % CPUTime : % 0.44/0.56 start to proof:theBenchmark % 58.48/58.69 %------------------------------------------- % 58.48/58.69 % File :CSE---1.7 % 58.48/58.69 % Problem :theBenchmark % 58.48/58.69 % Transform :cnf % 58.48/58.69 % Format :tptp:raw % 58.48/58.69 % Command :java -jar mcs_scs.jar %d %s % 58.48/58.69 % 58.48/58.69 % Result :Theorem 58.000000s % 58.48/58.69 % Output :CNFRefutation 58.000000s % 58.48/58.69 %------------------------------------------- % 58.48/58.71 %------------------------------------------------------------------------------ % 58.48/58.71 % File : SWB005+2 : TPTP v8.2.0. Released v5.2.0. % 58.48/58.71 % Domain : Semantic Web % 58.48/58.71 % Problem : Everything is a Resource % 58.48/58.71 % Version : [Sch11] axioms : Reduced > Incomplete. % 58.48/58.71 % English : % 58.48/58.71 % 58.48/58.71 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 58.48/58.71 % Source : [Sch11] % 58.48/58.71 % Names : 005_Everything_is_a_Resource [Sch11] % 58.48/58.72 % 58.48/58.72 % Status : Theorem % 58.48/58.72 % Rating : 0.00 v5.3.0, 0.09 v5.2.0 % 58.48/58.72 % Syntax : Number of formulae : 9 ( 2 unt; 0 def) % 58.48/58.72 % Number of atoms : 22 ( 0 equ) % 58.48/58.72 % Maximal formula atoms : 8 ( 2 avg) % 58.48/58.72 % Number of connectives : 13 ( 0 ~; 0 |; 7 &) % 58.48/58.72 % ( 5 <=>; 1 =>; 0 <=; 0 <~>) % 58.48/58.72 % Maximal formula depth : 8 ( 4 avg) % 58.48/58.72 % Maximal term depth : 1 ( 1 avg) % 58.48/58.72 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty) % 58.48/58.72 % Number of functors : 8 ( 8 usr; 8 con; 0-0 aty) % 58.48/58.72 % Number of variables : 10 ( 10 !; 0 ?) % 58.48/58.72 % SPC : FOF_THM_EPR_NEQ % 58.48/58.72 % 58.48/58.72 % Comments : % 58.48/58.72 %------------------------------------------------------------------------------ % 58.48/58.72 fof(simple_ir,axiom, % 58.48/58.72 ! [X] : ir(X) ). % 58.48/58.72 % 58.48/58.72 fof(simple_iext_property,axiom, % 58.48/58.72 ! [S,P,O] : % 58.48/58.72 ( iext(P,S,O) % 58.48/58.72 => ip(P) ) ). % 58.48/58.72 % 58.48/58.72 fof(rdf_type_ip,axiom, % 58.48/58.72 ! [P] : % 58.48/58.72 ( iext(uri_rdf_type,P,uri_rdf_Property) % 58.48/58.72 <=> ip(P) ) ). % 58.48/58.72 % 58.48/58.72 fof(rdfs_cext_def,axiom, % 58.48/58.72 ! [X,C] : % 58.48/58.72 ( iext(uri_rdf_type,X,C) % 58.48/58.72 <=> icext(C,X) ) ). % 58.48/58.72 % 58.48/58.72 fof(rdfs_ir_def,axiom, % 58.48/58.72 ! [X] : % 58.48/58.72 ( ir(X) % 58.48/58.72 <=> icext(uri_rdfs_Resource,X) ) ). % 58.48/58.72 % 58.48/58.72 fof(owl_class_thing_ext,axiom, % 58.48/58.72 ! [X] : % 58.48/58.72 ( icext(uri_owl_Thing,X) % 58.48/58.72 <=> ir(X) ) ). % 58.48/58.72 % 58.48/58.72 fof(owl_class_objectproperty_ext,axiom, % 58.48/58.72 ! [X] : % 58.48/58.72 ( icext(uri_owl_ObjectProperty,X) % 58.48/58.72 <=> ip(X) ) ). % 58.48/58.72 % 58.48/58.72 fof(testcase_conclusion_fullish_005_Everything_is_a_Resource,conjecture, % 58.48/58.72 ( iext(uri_rdf_type,uri_ex_s,uri_rdfs_Resource) % 58.48/58.72 & iext(uri_rdf_type,uri_ex_s,uri_owl_Thing) % 58.48/58.72 & iext(uri_rdf_type,uri_ex_p,uri_rdfs_Resource) % 58.48/58.72 & iext(uri_rdf_type,uri_ex_p,uri_owl_Thing) % 58.48/58.72 & iext(uri_rdf_type,uri_ex_p,uri_rdf_Property) % 58.48/58.72 & iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty) % 58.48/58.72 & iext(uri_rdf_type,uri_ex_o,uri_rdfs_Resource) % 58.48/58.72 & iext(uri_rdf_type,uri_ex_o,uri_owl_Thing) ) ). % 58.48/58.72 % 58.48/58.72 fof(testcase_premise_fullish_005_Everything_is_a_Resource,axiom, % 58.48/58.72 iext(uri_ex_p,uri_ex_s,uri_ex_o) ). % 58.48/58.72 % 58.48/58.72 %------------------------------------------------------------------------------ % 58.48/58.72 %------------------------------------------- % 58.48/58.72 % Proof found % 58.48/58.72 % SZS status Theorem for theBenchmark % 58.48/58.72 % SZS output start Proof % 58.48/58.73 %ClaNum:11(EqnAxiom:0) % 58.48/58.73 %VarNum:22(SingletonVarNum:13) % 58.48/58.73 %MaxLitNum:8 % 58.48/58.73 %MaxfuncDepth:0 % 58.48/58.73 %SharedTerms:17 % 58.48/58.73 %goalClause: 11 % 58.48/58.73 [3]P2(a3,a5,a4) % 58.48/58.73 [1]P1(a1,x11) % 58.48/58.73 [2]P1(a2,x21) % 58.48/58.73 [4]~P3(x41)+P1(a6,x41) % 58.48/58.73 [5]P3(x51)+~P1(a6,x51) % 58.48/58.73 [6]~P3(x61)+P2(a7,x61,a8) % 58.48/58.73 [8]P3(x81)+~P2(a7,x81,a8) % 58.48/58.73 [7]~P1(x72,x71)+P2(a7,x71,x72) % 58.48/58.73 [10]P1(x101,x102)+~P2(a7,x102,x101) % 58.48/58.73 [9]P3(x91)+~P2(x91,x92,x93) % 58.48/58.73 [11]~P2(a7,a5,a1)+~P2(a7,a5,a2)+~P2(a7,a3,a8)+~P2(a7,a3,a1)+~P2(a7,a3,a2)+~P2(a7,a3,a6)+~P2(a7,a4,a1)+~P2(a7,a4,a2) % 58.48/58.73 %EqnAxiom % 58.48/58.73 % 58.48/58.73 %------------------------------------------- % 58.63/58.74 cnf(12,plain, % 58.63/58.74 (P1(a6,a3)), % 58.63/58.74 inference(scs_inference,[],[3,4,9])). % 58.63/58.74 cnf(13,plain, % 58.63/58.74 (P3(a3)), % 58.63/58.74 inference(scs_inference,[],[12,5])). % 58.63/58.74 cnf(15,plain, % 58.63/58.75 (P2(a7,a3,a8)), % 58.63/58.75 inference(scs_inference,[],[12,6,5])). % 58.63/58.75 cnf(16,plain, % 58.63/58.75 (~P2(a7,a5,a1)+~P2(a7,a5,a2)+~P2(a7,a3,a1)+~P2(a7,a3,a2)+~P2(a7,a3,a6)+~P2(a7,a4,a1)+~P2(a7,a4,a2)), % 58.63/58.75 inference(scs_inference,[],[15,11])). % 58.63/58.75 cnf(19,plain, % 58.63/58.75 (P2(a7,a3,a6)), % 58.63/58.75 inference(scs_inference,[],[13,7,4])). % 58.63/58.75 cnf(20,plain, % 58.63/58.75 (~P2(a7,a5,a1)+~P2(a7,a5,a2)+~P2(a7,a3,a1)+~P2(a7,a3,a2)+~P2(a7,a4,a1)+~P2(a7,a4,a2)), % 58.63/58.75 inference(scs_inference,[],[19,16])). % 58.63/58.75 cnf(28,plain, % 58.63/58.75 (P2(a7,x281,a1)), % 58.63/58.75 inference(scs_inference,[],[1,7])). % 58.63/58.75 cnf(30,plain, % 58.63/58.75 (~P2(a7,a3,a2)+~P2(a7,a4,a2)+~P2(a7,a3,a1)+~P2(a7,a5,a2)+~P2(a7,a5,a1)), % 58.63/58.75 inference(scs_inference,[],[28,20])). % 58.63/58.75 cnf(31,plain, % 58.63/58.75 (P2(a7,x311,a2)), % 58.63/58.75 inference(scs_inference,[],[2,7])). % 58.63/58.75 cnf(34,plain, % 58.63/58.75 (~P2(a7,a4,a2)+~P2(a7,a3,a2)+~P2(a7,a5,a1)), % 58.63/58.75 inference(scs_inference,[],[2,28,7,30])). % 58.63/58.75 cnf(35,plain, % 58.63/58.75 ($false), % 58.63/58.75 inference(scs_inference,[],[31,28,2,34,7]), % 58.63/58.75 ['proof']). % 58.63/58.75 % SZS output end Proof % 58.63/58.75 % Total time :58.000000s %------------------------------------------------------------------------------