%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB007+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 : n029.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:16 EDT 2024 % Result : Theorem 0.55s 0.63s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB007+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 : n029.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:40:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.55/0.58 start to proof:theBenchmark % 0.55/0.62 %------------------------------------------- % 0.55/0.62 % File :CSE---1.7 % 0.55/0.62 % Problem :theBenchmark % 0.55/0.62 % Transform :cnf % 0.55/0.62 % Format :tptp:raw % 0.55/0.62 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.62 % 0.55/0.62 % Result :Theorem 0.000000s % 0.55/0.62 % Output :CNFRefutation 0.000000s % 0.55/0.62 %------------------------------------------- % 0.55/0.62 %------------------------------------------------------------------------------ % 0.55/0.62 % File : SWB007+2 : TPTP v8.2.0. Released v5.2.0. % 0.55/0.62 % Domain : Semantic Web % 0.55/0.62 % Problem : Equal Classes % 0.55/0.62 % Version : [Sch11] axioms : Reduced > Incomplete. % 0.55/0.62 % English : % 0.55/0.62 % 0.55/0.62 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 0.55/0.62 % Source : [Sch11] % 0.55/0.62 % Names : 007_Equal_Classes [Sch11] % 0.55/0.62 % 0.55/0.62 % Status : Theorem % 0.55/0.62 % Rating : 0.00 v5.3.0, 0.09 v5.2.0 % 0.55/0.62 % Syntax : Number of formulae : 3 ( 0 unt; 0 def) % 0.55/0.62 % Number of atoms : 9 ( 1 equ) % 0.55/0.62 % Maximal formula atoms : 4 ( 3 avg) % 0.55/0.62 % Number of connectives : 6 ( 0 ~; 0 |; 5 &) % 0.55/0.62 % ( 1 <=>; 0 =>; 0 <=; 0 <~>) % 0.55/0.62 % Maximal formula depth : 4 ( 4 avg) % 0.55/0.62 % Maximal term depth : 1 ( 1 avg) % 0.55/0.62 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty) % 0.55/0.62 % Number of functors : 9 ( 9 usr; 9 con; 0-0 aty) % 0.55/0.62 % Number of variables : 2 ( 2 !; 0 ?) % 0.55/0.62 % SPC : FOF_THM_EPR_SEQ % 0.55/0.62 % 0.55/0.62 % Comments : % 0.55/0.62 %------------------------------------------------------------------------------ % 0.55/0.62 fof(owl_eqdis_sameas,axiom, % 0.55/0.62 ! [X,Y] : % 0.55/0.62 ( iext(uri_owl_sameAs,X,Y) % 0.55/0.62 <=> X = Y ) ). % 0.55/0.62 % 0.55/0.62 fof(testcase_conclusion_fullish_007_Equal_Classes,conjecture, % 0.55/0.63 ( iext(uri_rdf_type,uri_ex_w,uri_ex_c2) % 0.55/0.63 & iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_c2) % 0.55/0.63 & iext(uri_rdfs_range,uri_ex_p,uri_ex_c2) ) ). % 0.55/0.63 % 0.55/0.63 fof(testcase_premise_fullish_007_Equal_Classes,axiom, % 0.55/0.63 ( iext(uri_owl_sameAs,uri_ex_c1,uri_ex_c2) % 0.55/0.63 & iext(uri_rdf_type,uri_ex_w,uri_ex_c1) % 0.55/0.63 & iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_c1) % 0.55/0.63 & iext(uri_rdfs_range,uri_ex_p,uri_ex_c1) ) ). % 0.55/0.63 % 0.55/0.63 %------------------------------------------------------------------------------ % 0.55/0.63 %------------------------------------------- % 0.55/0.63 % Proof found % 0.55/0.63 % SZS status Theorem for theBenchmark % 0.55/0.63 % SZS output start Proof % 0.55/0.63 %ClaNum:13(EqnAxiom:6) % 0.55/0.63 %VarNum:8(SingletonVarNum:4) % 0.55/0.63 %MaxLitNum:3 % 0.55/0.63 %MaxfuncDepth:0 % 0.55/0.63 %SharedTerms:16 % 0.55/0.63 %goalClause: 13 % 0.55/0.63 [7]P1(a1,a2,a4) % 0.55/0.63 [8]P1(a7,a5,a2) % 0.55/0.63 [9]P1(a8,a3,a2) % 0.55/0.63 [10]P1(a9,a6,a2) % 0.55/0.63 [11]~E(x111,x112)+P1(a1,x111,x112) % 0.55/0.63 [12]E(x121,x122)+~P1(a1,x121,x122) % 0.55/0.63 [13]~P1(a7,a5,a4)+~P1(a8,a3,a4)+~P1(a9,a6,a4) % 0.55/0.63 %EqnAxiom % 0.55/0.63 [1]E(x11,x11) % 0.55/0.63 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.63 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.63 [4]P1(x42,x43,x44)+~E(x41,x42)+~P1(x41,x43,x44) % 0.55/0.63 [5]P1(x53,x52,x54)+~E(x51,x52)+~P1(x53,x51,x54) % 0.55/0.63 [6]P1(x63,x64,x62)+~E(x61,x62)+~P1(x63,x64,x61) % 0.55/0.63 % 0.55/0.63 %------------------------------------------- % 0.55/0.63 cnf(14,plain, % 0.55/0.63 (P1(a1,x141,x141)), % 0.55/0.63 inference(equality_inference,[],[11])). % 0.55/0.63 cnf(15,plain, % 0.55/0.63 (E(a2,a4)), % 0.55/0.63 inference(scs_inference,[],[7,12])). % 0.55/0.63 cnf(21,plain, % 0.55/0.63 (~P1(a8,a3,a4)+~P1(a9,a6,a4)), % 0.55/0.63 inference(scs_inference,[],[7,14,8,12,2,5,6,13])). % 0.55/0.63 cnf(25,plain, % 0.55/0.63 (~P1(a9,a6,a4)), % 0.55/0.63 inference(scs_inference,[],[15,9,6,21])). % 0.55/0.63 cnf(30,plain, % 0.55/0.63 ($false), % 0.55/0.63 inference(scs_inference,[],[25,15,10,6]), % 0.55/0.63 ['proof']). % 0.55/0.63 % SZS output end Proof % 0.55/0.63 % Total time :0.000000s %------------------------------------------------------------------------------