%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB016+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 : n010.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:22 EDT 2024 % Result : Theorem 58.61s 58.82s % Output : CNFRefutation 58.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.14 % Problem : SWB016+2 : TPTP v8.2.0. Released v5.2.0. % 0.03/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.38 % Computer : n010.cluster.edu % 0.14/0.38 % Model : x86_64 x86_64 % 0.14/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.38 % Memory : 8042.1875MB % 0.14/0.38 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.38 % CPULimit : 300 % 0.14/0.38 % WCLimit : 300 % 0.14/0.38 % DateTime : Tue Jun 18 17:43:54 EDT 2024 % 0.14/0.38 % CPUTime : % 0.46/0.63 start to proof:theBenchmark % 58.61/58.81 %------------------------------------------- % 58.61/58.81 % File :CSE---1.7 % 58.61/58.81 % Problem :theBenchmark % 58.61/58.81 % Transform :cnf % 58.61/58.81 % Format :tptp:raw % 58.61/58.81 % Command :java -jar mcs_scs.jar %d %s % 58.61/58.81 % 58.61/58.81 % Result :Theorem 58.010000s % 58.61/58.81 % Output :CNFRefutation 58.010000s % 58.61/58.81 %------------------------------------------- % 58.61/58.82 %------------------------------------------------------------------------------ % 58.61/58.82 % File : SWB016+2 : TPTP v8.2.0. Released v5.2.0. % 58.61/58.82 % Domain : Semantic Web % 58.61/58.82 % Problem : Reflective Tautologies II % 58.61/58.82 % Version : [Sch11] axioms : Reduced > Incomplete. % 58.61/58.82 % English : % 58.61/58.82 % 58.61/58.82 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 58.61/58.82 % Source : [Sch11] % 58.61/58.82 % Names : 016_Reflective_Tautologies_II [Sch11] % 58.61/58.82 % 58.61/58.82 % Status : Theorem % 58.61/58.82 % Rating : 0.06 v8.2.0, 0.07 v8.1.0, 0.14 v7.5.0, 0.10 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.07 v6.3.0, 0.00 v6.1.0, 0.12 v6.0.0, 0.25 v5.5.0, 0.08 v5.4.0, 0.09 v5.3.0, 0.17 v5.2.0 % 58.61/58.82 % Syntax : Number of formulae : 11 ( 4 unt; 0 def) % 58.61/58.82 % Number of atoms : 29 ( 0 equ) % 58.61/58.82 % Maximal formula atoms : 5 ( 2 avg) % 58.61/58.82 % Number of connectives : 18 ( 0 ~; 0 |; 8 &) % 58.61/58.82 % ( 6 <=>; 4 =>; 0 <=; 0 <~>) % 58.61/58.82 % Maximal formula depth : 9 ( 4 avg) % 58.61/58.82 % Maximal term depth : 1 ( 1 avg) % 58.61/58.82 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty) % 58.61/58.82 % Number of functors : 7 ( 7 usr; 7 con; 0-0 aty) % 58.61/58.82 % Number of variables : 19 ( 19 !; 0 ?) % 58.61/58.82 % SPC : FOF_THM_RFO_NEQ % 58.61/58.82 % 58.61/58.82 % Comments : % 58.61/58.82 %------------------------------------------------------------------------------ % 58.61/58.82 fof(rdf_type_ip,axiom, % 58.61/58.82 ! [P] : % 58.61/58.82 ( iext(uri_rdf_type,P,uri_rdf_Property) % 58.61/58.82 <=> ip(P) ) ). % 58.61/58.82 % 58.61/58.82 fof(rdfs_cext_def,axiom, % 58.61/58.82 ! [X,C] : % 58.61/58.82 ( iext(uri_rdf_type,X,C) % 58.61/58.82 <=> icext(C,X) ) ). % 58.61/58.82 % 58.61/58.82 fof(rdfs_domain_main,axiom, % 58.61/58.82 ! [P,C,X,Y] : % 58.61/58.82 ( ( iext(uri_rdfs_domain,P,C) % 58.61/58.82 & iext(P,X,Y) ) % 58.61/58.82 => icext(C,X) ) ). % 58.61/58.82 % 58.61/58.82 fof(rdfs_domain_domain,axiom, % 58.61/58.82 iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) ). % 58.61/58.82 % 58.61/58.82 fof(rdfs_subclassof_domain,axiom, % 58.61/58.82 iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class) ). % 58.61/58.82 % 58.61/58.82 fof(owl_prop_equivalentclass_type,axiom, % 58.61/58.82 ip(uri_owl_equivalentClass) ). % 58.61/58.82 % 58.61/58.82 fof(owl_prop_equivalentclass_ext,axiom, % 58.61/58.82 ! [X,Y] : % 58.61/58.82 ( iext(uri_owl_equivalentClass,X,Y) % 58.61/58.82 => ( ic(X) % 58.61/58.82 & ic(Y) ) ) ). % 58.61/58.82 % 58.61/58.82 fof(owl_rdfsext_subclassof,axiom, % 58.61/58.82 ! [C1,C2] : % 58.61/58.82 ( iext(uri_rdfs_subClassOf,C1,C2) % 58.61/58.82 <=> ( ic(C1) % 58.61/58.82 & ic(C2) % 58.61/58.82 & ! [X] : % 58.61/58.82 ( icext(C1,X) % 58.61/58.82 => icext(C2,X) ) ) ) ). % 58.61/58.82 % 58.61/58.82 fof(owl_rdfsext_subpropertyof,axiom, % 58.61/58.82 ! [P1,P2] : % 58.61/58.82 ( iext(uri_rdfs_subPropertyOf,P1,P2) % 58.61/58.82 <=> ( ip(P1) % 58.61/58.82 & ip(P2) % 58.61/58.82 & ! [X,Y] : % 58.61/58.82 ( iext(P1,X,Y) % 58.61/58.82 => iext(P2,X,Y) ) ) ) ). % 58.61/58.82 % 58.61/58.82 fof(owl_eqdis_equivalentclass,axiom, % 58.61/58.82 ! [C1,C2] : % 58.61/58.82 ( iext(uri_owl_equivalentClass,C1,C2) % 58.61/58.82 <=> ( ic(C1) % 58.61/58.82 & ic(C2) % 58.61/58.82 & ! [X] : % 58.61/58.82 ( icext(C1,X) % 58.61/58.82 <=> icext(C2,X) ) ) ) ). % 58.61/58.82 % 58.61/58.82 fof(testcase_conclusion_fullish_016_Reflective_Tautologies_II,conjecture, % 58.61/58.82 iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_rdfs_subClassOf) ). % 58.61/58.82 % 58.61/58.82 %------------------------------------------------------------------------------ % 58.61/58.82 %------------------------------------------- % 58.61/58.82 % Proof found % 58.61/58.82 % SZS status Theorem for theBenchmark % 58.61/58.82 % SZS output start Proof % 58.61/58.82 %ClaNum:27(EqnAxiom:0) % 58.61/58.82 %VarNum:115(SingletonVarNum:47) % 58.61/58.82 %MaxLitNum:5 % 58.61/58.82 %MaxfuncDepth:1 % 58.61/58.82 %SharedTerms:11 % 58.61/58.82 %goalClause: 4 % 58.61/58.82 %singleGoalClaCount:1 % 58.61/58.82 [1]P1(a1) % 58.61/58.82 [2]P2(a6,a6,a7) % 58.61/58.82 [3]P2(a6,a10,a8) % 58.61/58.82 [4]~P2(a11,a1,a10) % 58.61/58.82 [5]~P1(x51)+P2(a9,x51,a7) % 58.61/58.82 [7]P1(x71)+~P2(a9,x71,a7) % 58.61/58.82 [6]~P3(x62,x61)+P2(a9,x61,x62) % 58.61/58.82 [8]P1(x81)+~P2(a11,x82,x81) % 58.61/58.82 [9]P1(x91)+~P2(a11,x91,x92) % 58.61/58.82 [10]P4(x101)+~P2(a10,x102,x101) % 58.61/58.82 [11]P4(x111)+~P2(a10,x111,x112) % 58.61/58.82 [13]P4(x131)+~P2(a1,x132,x131) % 58.61/58.82 [15]P4(x151)+~P2(a1,x151,x152) % 58.61/58.82 [16]P3(x161,x162)+~P2(a9,x162,x161) % 58.61/58.82 [18]P3(x181,x182)+~P3(x183,x182)+~P2(a10,x183,x181) % 58.61/58.82 [19]P3(x191,x192)+~P3(x193,x192)+~P2(a1,x191,x193) % 58.61/58.82 [20]P3(x201,x202)+~P3(x203,x202)+~P2(a1,x203,x201) % 58.61/58.82 [24]P3(x241,x242)+~P2(x243,x242,x244)+~P2(a6,x243,x241) % 58.61/58.82 [26]P2(x261,x262,x263)+~P2(x264,x262,x263)+~P2(a11,x264,x261) % 58.61/58.82 [17]~P4(x172)+~P4(x171)+P2(a10,x171,x172)+P3(x171,f2(x171,x172)) % 58.61/58.82 [21]~P4(x211)+~P4(x212)+P2(a10,x211,x212)+~P3(x212,f2(x211,x212)) % 58.61/58.82 [23]~P1(x232)+~P1(x231)+P2(x231,f4(x231,x232),f5(x231,x232))+P2(a11,x231,x232) % 58.61/58.82 [27]~P1(x271)+~P1(x272)+~P2(x272,f4(x271,x272),f5(x271,x272))+P2(a11,x271,x272) % 58.61/58.82 [22]~P4(x222)+~P4(x221)+P2(a1,x221,x222)+P3(x222,f3(x221,x222))+P3(x221,f3(x221,x222)) % 58.61/58.82 [25]~P4(x252)+~P4(x251)+P2(a1,x251,x252)+~P3(x252,f3(x251,x252))+~P3(x251,f3(x251,x252)) % 58.61/58.82 %EqnAxiom % 58.61/58.82 % 58.61/58.82 %------------------------------------------- % 58.61/58.83 cnf(93,plain, % 58.61/58.83 (~P1(a10)+~P2(a10,f4(a1,a10),f5(a1,a10))+~P2(a9,a1,a7)), % 58.61/58.83 inference(scs_inference,[],[4,7,27])). % 58.61/58.83 cnf(94,plain, % 58.61/58.83 (~P2(a10,f4(a1,a10),f5(a1,a10))+~P1(a10)), % 58.61/58.83 inference(scs_inference,[],[1,93,5])). % 58.61/58.83 cnf(99,plain, % 58.61/58.83 (P2(a1,f4(a1,a10),f5(a1,a10))+~P2(a9,a10,a7)), % 58.61/58.83 inference(scs_inference,[],[4,1,7,23])). % 58.61/58.83 cnf(100,plain, % 58.61/58.83 (P4(f5(a1,a10))+~P2(a9,a10,a7)), % 58.61/58.83 inference(scs_inference,[],[99,13])). % 58.61/58.83 cnf(101,plain, % 58.61/58.83 (P2(a10,f5(a1,a10),f5(a1,a10))+P3(f5(a1,a10),f2(f5(a1,a10),f5(a1,a10)))+~P2(a9,a10,a7)), % 58.61/58.83 inference(scs_inference,[],[100,17])). % 58.61/58.83 cnf(102,plain, % 58.61/58.83 (~P4(f5(a1,a10))+P2(a10,f5(a1,a10),f5(a1,a10))+~P2(a9,a10,a7)), % 58.61/58.83 inference(scs_inference,[],[101,21])). % 58.61/58.83 cnf(109,plain, % 58.61/58.83 (~P2(a9,a10,a7)+~P2(a10,f4(a1,a10),f5(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[7,94])). % 58.61/58.83 cnf(110,plain, % 58.61/58.83 (~P3(a7,a10)+~P2(a10,f4(a1,a10),f5(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[109,6])). % 58.61/58.83 cnf(111,plain, % 58.61/58.83 (~P2(a10,f4(a1,a10),f5(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[2,3,110,24])). % 58.61/58.83 cnf(160,plain, % 58.61/58.83 (P4(f4(a1,a10))+~P2(a9,a10,a7)), % 58.61/58.83 inference(scs_inference,[],[15,99])). % 58.61/58.83 cnf(161,plain, % 58.61/58.83 (~P2(a9,a10,a7)+P2(a10,f4(a1,a10),f4(a1,a10))+P3(f4(a1,a10),f2(f4(a1,a10),f4(a1,a10)))), % 58.61/58.83 inference(scs_inference,[],[160,17])). % 58.61/58.83 cnf(162,plain, % 58.61/58.83 (~P4(f4(a1,a10))+~P2(a9,a10,a7)+P2(a10,f4(a1,a10),f4(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[161,21])). % 58.61/58.83 cnf(440,plain, % 58.61/58.83 (~P3(a7,a10)+P2(a1,f4(a1,a10),f5(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[6,99])). % 58.61/58.83 cnf(441,plain, % 58.61/58.83 (P4(f5(a1,a10))+~P3(a7,a10)), % 58.61/58.83 inference(scs_inference,[],[440,13])). % 58.61/58.83 cnf(442,plain, % 58.61/58.83 (~P2(a9,a10,a7)+P2(a10,f5(a1,a10),f5(a1,a10))+~P3(a7,a10)), % 58.61/58.83 inference(scs_inference,[],[441,102])). % 58.61/58.83 cnf(455,plain, % 58.61/58.83 (~P3(a7,a10)+P4(f4(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[6,160])). % 58.61/58.83 cnf(456,plain, % 58.61/58.83 (~P2(a9,a10,a7)+P2(a10,f4(a1,a10),f4(a1,a10))+~P3(a7,a10)), % 58.61/58.83 inference(scs_inference,[],[455,162])). % 58.61/58.83 cnf(723,plain, % 58.61/58.83 (~P3(a7,a10)+P2(a10,f5(a1,a10),f5(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[6,442])). % 58.61/58.83 cnf(724,plain, % 58.61/58.83 (P2(a10,f5(a1,a10),f5(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[2,3,723,24])). % 58.61/58.83 cnf(725,plain, % 58.61/58.83 (P4(f5(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[724,10])). % 58.61/58.83 cnf(737,plain, % 58.61/58.83 (~P4(f4(a1,a10))+P2(a9,f2(f4(a1,a10),f5(a1,a10)),f4(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[111,725,6,17])). % 58.61/58.83 cnf(738,plain, % 58.61/58.83 (P3(f4(a1,a10),f2(f4(a1,a10),f5(a1,a10)))+~P4(f4(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[737,16])). % 58.61/58.83 cnf(739,plain, % 58.61/58.83 (P3(x7391,f2(f4(a1,a10),f5(a1,a10)))+~P4(f4(a1,a10))+~P2(a10,f4(a1,a10),x7391)), % 58.61/58.83 inference(scs_inference,[],[738,18])). % 58.61/58.83 cnf(740,plain, % 58.61/58.83 (P3(x7401,f2(f4(a1,a10),f5(a1,a10)))+~P2(a10,x7402,f4(a1,a10))+~P2(a10,f4(a1,a10),x7401)), % 58.61/58.83 inference(scs_inference,[],[739,10])). % 58.61/58.83 cnf(742,plain, % 58.61/58.83 (~P3(a7,a10)+P2(a10,f4(a1,a10),f4(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[6,456])). % 58.61/58.83 cnf(743,plain, % 58.61/58.83 (P2(a10,f4(a1,a10),f4(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[2,3,742,24])). % 58.61/58.83 cnf(748,plain, % 58.61/58.83 (P3(x7481,f2(f4(a1,a10),f5(a1,a10)))+~P2(a10,f4(a1,a10),x7481)), % 58.61/58.83 inference(scs_inference,[],[743,740])). % 58.61/58.83 cnf(751,plain, % 58.61/58.83 (P4(f4(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[743,748,11])). % 58.61/58.83 cnf(753,plain, % 58.61/58.83 (P2(a9,f2(f4(a1,a10),f5(a1,a10)),f4(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[743,748,11,737])). % 58.61/58.83 cnf(780,plain, % 58.61/58.83 (~P2(a9,f2(f4(a1,a10),f5(a1,a10)),f5(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[111,751,725,16,21])). % 58.61/58.83 cnf(781,plain, % 58.61/58.83 (~P3(f5(a1,a10),f2(f4(a1,a10),f5(a1,a10)))), % 58.61/58.83 inference(scs_inference,[],[780,6])). % 58.61/58.83 cnf(821,plain, % 58.61/58.83 (~P2(a1,f4(a1,a10),f5(a1,a10))), % 58.61/58.83 inference(scs_inference,[],[753,781,16,20])). % 58.61/58.83 cnf(825,plain, % 58.61/58.83 (~P3(a7,a10)), % 58.61/58.83 inference(scs_inference,[],[821,440])). % 58.61/58.83 cnf(2806,plain, % 58.61/58.83 ($false), % 58.61/58.83 inference(scs_inference,[],[825,3,2,24]), % 58.61/58.83 ['proof']). % 58.61/58.83 % SZS output end Proof % 58.61/58.83 % Total time :58.010000s %------------------------------------------------------------------------------