%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB022+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 : n002.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:25 EDT 2024 % Result : Theorem 58.82s 58.91s % Output : CNFRefutation 58.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB022+2 : TPTP v8.2.0. Released v5.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n002.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 18:30:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.42/0.61 start to proof:theBenchmark % 58.82/58.90 %------------------------------------------- % 58.82/58.90 % File :CSE---1.7 % 58.82/58.90 % Problem :theBenchmark % 58.82/58.90 % Transform :cnf % 58.82/58.90 % Format :tptp:raw % 58.82/58.90 % Command :java -jar mcs_scs.jar %d %s % 58.82/58.90 % 58.82/58.90 % Result :Theorem 58.210000s % 58.82/58.90 % Output :CNFRefutation 58.210000s % 58.82/58.90 %------------------------------------------- % 58.82/58.91 %------------------------------------------------------------------------------ % 58.82/58.91 % File : SWB022+2 : TPTP v8.2.0. Released v5.2.0. % 58.82/58.91 % Domain : Semantic Web % 58.82/58.91 % Problem : List Member Access % 58.82/58.91 % Version : [Sch11] axioms : Reduced > Incomplete. % 58.82/58.91 % English : % 58.82/58.91 % 58.82/58.91 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 58.82/58.91 % Source : [Sch11] % 58.82/58.91 % Names : 022_List_Member_Access [Sch11] % 58.82/58.91 % 58.82/58.91 % Status : Theorem % 58.82/58.91 % Rating : 0.06 v8.2.0, 0.13 v8.1.0, 0.14 v7.5.0, 0.10 v7.4.0, 0.12 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.21 v6.3.0, 0.15 v6.2.0, 0.18 v6.1.0, 0.16 v6.0.0, 0.50 v5.5.0, 0.21 v5.4.0, 0.13 v5.3.0, 0.22 v5.2.0 % 58.82/58.91 % Syntax : Number of formulae : 4 ( 0 unt; 0 def) % 58.82/58.91 % Number of atoms : 38 ( 0 equ) % 58.82/58.91 % Maximal formula atoms : 19 ( 9 avg) % 58.82/58.91 % Number of connectives : 34 ( 0 ~; 0 |; 29 &) % 58.82/58.91 % ( 1 <=>; 4 =>; 0 <=; 0 <~>) % 58.82/58.91 % Maximal formula depth : 27 ( 14 avg) % 58.82/58.91 % Maximal term depth : 1 ( 1 avg) % 58.82/58.91 % Number of predicates : 2 ( 2 usr; 0 prp; 1-3 aty) % 58.82/58.91 % Number of functors : 13 ( 13 usr; 13 con; 0-0 aty) % 58.82/58.91 % Number of variables : 20 ( 12 !; 8 ?) % 58.82/58.91 % SPC : FOF_THM_RFO_NEQ % 58.82/58.91 % 58.82/58.91 % Comments : % 58.82/58.91 %------------------------------------------------------------------------------ % 58.82/58.91 fof(rdfs_subpropertyof_main,axiom, % 58.82/58.91 ! [P,Q] : % 58.82/58.91 ( iext(uri_rdfs_subPropertyOf,P,Q) % 58.82/58.91 => ( ip(P) % 58.82/58.91 & ip(Q) % 58.82/58.91 & ! [X,Y] : % 58.82/58.91 ( iext(P,X,Y) % 58.82/58.91 => iext(Q,X,Y) ) ) ) ). % 58.82/58.91 % 58.82/58.91 fof(owl_chain_002,axiom, % 58.82/58.91 ! [P,S1,P1,S2,P2] : % 58.82/58.91 ( ( iext(uri_rdf_first,S1,P1) % 58.82/58.91 & iext(uri_rdf_rest,S1,S2) % 58.82/58.91 & iext(uri_rdf_first,S2,P2) % 58.82/58.91 & iext(uri_rdf_rest,S2,uri_rdf_nil) ) % 58.82/58.91 => ( iext(uri_owl_propertyChainAxiom,P,S1) % 58.82/58.91 <=> ( ip(P) % 58.82/58.91 & ip(P1) % 58.82/58.91 & ip(P2) % 58.82/58.91 & ! [Y0,Y1,Y2] : % 58.82/58.91 ( ( iext(P1,Y0,Y1) % 58.82/58.91 & iext(P2,Y1,Y2) ) % 58.82/58.91 => iext(P,Y0,Y2) ) ) ) ) ). % 58.82/58.91 % 58.82/58.91 fof(testcase_conclusion_fullish_022_List_Member_Access,conjecture, % 58.82/58.91 ( iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X) % 58.82/58.91 & iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y) % 58.82/58.91 & iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z) ) ). % 58.82/58.91 % 58.82/58.91 fof(testcase_premise_fullish_022_List_Member_Access,axiom, % 58.82/58.91 ? [BNODE_pL,BNODE_l11,BNODE_l12,BNODE_l21,BNODE_l22,BNODE_l31,BNODE_l32,BNODE_l33] : % 58.82/58.91 ( iext(uri_rdfs_subPropertyOf,uri_skos_memberList,BNODE_pL) % 58.82/58.91 & iext(uri_owl_propertyChainAxiom,uri_skos_member,BNODE_l11) % 58.82/58.91 & iext(uri_rdf_first,BNODE_l11,BNODE_pL) % 58.82/58.91 & iext(uri_rdf_rest,BNODE_l11,BNODE_l12) % 58.82/58.91 & iext(uri_rdf_first,BNODE_l12,uri_rdf_first) % 58.82/58.91 & iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil) % 58.82/58.91 & iext(uri_owl_propertyChainAxiom,BNODE_pL,BNODE_l21) % 58.82/58.91 & iext(uri_rdf_first,BNODE_l21,BNODE_pL) % 58.82/58.91 & iext(uri_rdf_rest,BNODE_l21,BNODE_l22) % 58.82/58.91 & iext(uri_rdf_first,BNODE_l22,uri_rdf_rest) % 58.82/58.91 & iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil) % 58.82/58.91 & iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection) % 58.82/58.91 & iext(uri_skos_memberList,uri_ex_MyOrderedCollection,BNODE_l31) % 58.82/58.91 & iext(uri_rdf_first,BNODE_l31,uri_ex_X) % 58.82/58.91 & iext(uri_rdf_rest,BNODE_l31,BNODE_l32) % 58.82/58.91 & iext(uri_rdf_first,BNODE_l32,uri_ex_Y) % 58.82/58.91 & iext(uri_rdf_rest,BNODE_l32,BNODE_l33) % 58.82/58.91 & iext(uri_rdf_first,BNODE_l33,uri_ex_Z) % 58.82/58.91 & iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil) ) ). % 58.82/58.91 % 58.82/58.91 %------------------------------------------------------------------------------ % 58.82/58.91 %------------------------------------------- % 58.82/58.91 % Proof found % 58.82/58.91 % SZS status Theorem for theBenchmark % 58.82/58.91 % SZS output start Proof % 58.82/58.92 %ClaNum:30(EqnAxiom:0) % 58.82/58.92 %VarNum:131(SingletonVarNum:46) % 58.82/58.92 %MaxLitNum:9 % 58.82/58.92 %MaxfuncDepth:1 % 58.82/58.92 %SharedTerms:43 % 58.82/58.92 %goalClause: 23 % 58.82/58.92 [1]P1(a1,a22,a2) % 58.82/58.92 [2]P1(a8,a9,a2) % 58.82/58.92 [3]P1(a8,a10,a8) % 58.82/58.92 [4]P1(a8,a11,a2) % 58.82/58.92 [5]P1(a8,a12,a19) % 58.82/58.92 [6]P1(a8,a13,a14) % 58.82/58.92 [7]P1(a8,a3,a16) % 58.82/58.92 [8]P1(a8,a4,a17) % 58.82/58.92 [9]P1(a19,a9,a10) % 58.82/58.92 [10]P1(a19,a10,a20) % 58.82/58.92 [11]P1(a19,a11,a12) % 58.82/58.92 [12]P1(a19,a12,a20) % 58.82/58.92 [13]P1(a19,a13,a3) % 58.82/58.92 [14]P1(a19,a3,a4) % 58.82/58.92 [15]P1(a19,a4,a20) % 58.82/58.92 [16]P1(a18,a23,a9) % 58.82/58.92 [17]P1(a18,a2,a11) % 58.82/58.92 [18]P1(a22,a15,a13) % 58.82/58.92 [19]P1(a21,a15,a24) % 58.82/58.92 [20]P2(x201)+~P1(a1,x202,x201) % 58.82/58.92 [21]P2(x211)+~P1(a1,x211,x212) % 58.82/58.92 [23]~P1(a23,a15,a14)+~P1(a23,a15,a16)+~P1(a23,a15,a17) % 58.82/58.92 [22]P1(x221,x222,x223)+~P1(x224,x222,x223)+~P1(a1,x224,x221) % 58.82/58.92 [24]P2(x241)+~P1(a19,x243,x242)+~P1(a8,x242,x241)+~P1(a8,x243,x244)+~P1(a18,x245,x243)+~P1(a19,x242,a20) % 58.82/58.92 [25]P2(x251)+~P1(a19,x254,x252)+~P1(a8,x252,x253)+~P1(a8,x254,x251)+~P1(a18,x255,x254)+~P1(a19,x252,a20) % 58.82/58.92 [26]P2(x261)+~P1(a19,x264,x262)+~P1(a18,x261,x264)+~P1(a8,x262,x263)+~P1(a8,x264,x265)+~P1(a19,x262,a20) % 58.82/58.92 [27]P1(x271,x272,x273)+~P1(x274,x275,x273)+~P1(x276,x272,x275)+~P1(a19,x278,x277)+~P1(a18,x271,x278)+~P1(a8,x277,x274)+~P1(a8,x278,x276)+~P1(a19,x277,a20) % 58.82/58.92 [28]~P2(x285)+~P2(x281)+~P2(x283)+~P1(a8,x284,x285)+~P1(a8,x282,x283)+~P1(a19,x282,x284)+P1(x283,f5(x281,x282,x283,x284,x285),f6(x281,x282,x283,x284,x285))+P1(a18,x281,x282)+~P1(a19,x284,a20) % 58.82/58.92 [29]~P2(x294)+~P2(x291)+~P2(x293)+~P1(a8,x295,x293)+~P1(a8,x292,x294)+~P1(a19,x292,x295)+P1(x293,f6(x291,x292,x294,x295,x293),f7(x291,x292,x294,x295,x293))+P1(a18,x291,x292)+~P1(a19,x295,a20) % 58.82/58.92 [30]~P2(x301)+~P2(x303)+~P2(x304)+~P1(a8,x302,x304)+~P1(a19,x302,x305)+~P1(x301,f5(x301,x302,x304,x305,x303),f7(x301,x302,x304,x305,x303))+P1(a18,x301,x302)+~P1(a8,x305,x303)+~P1(a19,x305,a20) % 58.82/58.92 %EqnAxiom % 58.82/58.92 % 58.82/58.92 %------------------------------------------- % 58.82/58.92 cnf(35,plain, % 58.82/58.92 (P1(a2,a15,a13)), % 58.82/58.92 inference(scs_inference,[],[1,18,20,21,22])). % 58.82/58.92 cnf(70,plain, % 58.82/58.92 (~P1(a23,a15,a16)+~P1(a23,a15,a17)), % 58.82/58.92 inference(scs_inference,[],[35,10,16,6,9,2,3,27,23])). % 58.82/58.92 cnf(77,plain, % 58.82/58.92 (P1(a23,x771,a16)+~P1(a2,x771,a3)), % 58.82/58.92 inference(scs_inference,[],[10,16,7,9,2,3,27])). % 58.82/58.92 cnf(387,plain, % 58.82/58.92 (P1(a2,a15,a3)), % 58.82/58.92 inference(scs_inference,[],[35,12,13,11,5,17,4,27])). % 58.82/58.92 cnf(391,plain, % 58.82/58.92 (~P1(a23,a15,a17)), % 58.82/58.92 inference(scs_inference,[],[35,12,13,11,5,17,4,27,77,70])). % 58.82/58.92 cnf(14303,plain, % 58.82/58.92 (P1(a2,a15,a4)), % 58.82/58.92 inference(scs_inference,[],[387,4,17,12,14,5,11,27])). % 58.82/58.92 cnf(14365,plain, % 58.82/58.92 ($false), % 58.82/58.92 inference(scs_inference,[],[2,14303,391,8,16,3,10,9,27]), % 58.82/58.92 ['proof']). % 58.82/58.92 % SZS output end Proof % 58.82/58.92 % Total time :58.210000s %------------------------------------------------------------------------------