%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS129+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n026.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 10:08:36 EDT 2024 % Result : Theorem 0.60s 0.71s % Output : CNFRefutation 0.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : KRS129+1 : TPTP v8.2.0. Released v3.1.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.35 % Computer : n026.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Wed Jun 19 13:59:39 EDT 2024 % 0.14/0.35 % CPUTime : % 0.54/0.60 start to proof:theBenchmark % 0.60/0.70 %------------------------------------------- % 0.60/0.70 % File :CSE---1.7 % 0.60/0.70 % Problem :theBenchmark % 0.60/0.70 % Transform :cnf % 0.60/0.70 % Format :tptp:raw % 0.60/0.70 % Command :java -jar mcs_scs.jar %d %s % 0.60/0.70 % 0.60/0.70 % Result :Theorem 0.060000s % 0.60/0.70 % Output :CNFRefutation 0.060000s % 0.60/0.70 %------------------------------------------- % 0.60/0.70 %------------------------------------------------------------------------------ % 0.60/0.70 % File : KRS129+1 : TPTP v8.2.0. Released v3.1.0. % 0.60/0.70 % Domain : Knowledge Representation (Semantic Web) % 0.60/0.70 % Problem : An example combinging owl:oneOf and owl:inverseOf % 0.60/0.70 % Version : Especial. % 0.60/0.70 % English : % 0.60/0.70 % 0.60/0.70 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 0.60/0.70 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 0.60/0.70 % Source : [Bec03] % 0.60/0.70 % Names : positive_I4.5-Manifest001 [Bec03] % 0.60/0.70 % 0.60/0.70 % Status : Theorem % 0.60/0.70 % Rating : 0.08 v8.1.0, 0.06 v7.4.0, 0.07 v7.2.0, 0.03 v7.1.0, 0.00 v6.1.0, 0.03 v6.0.0, 0.04 v5.4.0, 0.07 v5.3.0, 0.15 v5.2.0, 0.00 v4.1.0, 0.04 v4.0.1, 0.09 v4.0.0, 0.08 v3.7.0, 0.00 v3.2.0, 0.11 v3.1.0 % 0.60/0.70 % Syntax : Number of formulae : 27 ( 8 unt; 0 def) % 0.60/0.70 % Number of atoms : 67 ( 18 equ) % 0.60/0.70 % Maximal formula atoms : 7 ( 2 avg) % 0.60/0.70 % Number of connectives : 44 ( 4 ~; 5 |; 17 &) % 0.60/0.70 % ( 5 <=>; 13 =>; 0 <=; 0 <~>) % 0.60/0.70 % Maximal formula depth : 8 ( 4 avg) % 0.60/0.70 % Maximal term depth : 1 ( 1 avg) % 0.60/0.70 % Number of predicates : 11 ( 10 usr; 0 prp; 1-2 aty) % 0.60/0.70 % Number of functors : 7 ( 7 usr; 7 con; 0-0 aty) % 0.60/0.70 % Number of variables : 39 ( 38 !; 1 ?) % 0.60/0.70 % SPC : FOF_THM_RFO_SEQ % 0.60/0.70 % 0.60/0.70 % Comments : Sean Bechhofer says there are some errors in the encoding of % 0.60/0.70 % datatypes, so this problem may not be perfect. At least it's % 0.60/0.70 % still representative of the type of reasoning required for OWL. % 0.60/0.70 %------------------------------------------------------------------------------ % 0.60/0.70 fof(cEUCountry_substitution_1,axiom, % 0.60/0.70 ! [A,B] : % 0.60/0.70 ( ( A = B % 0.60/0.70 & cEUCountry(A) ) % 0.60/0.70 => cEUCountry(B) ) ). % 0.60/0.70 % 0.60/0.70 fof(cEuroMP_substitution_1,axiom, % 0.60/0.70 ! [A,B] : % 0.60/0.70 ( ( A = B % 0.60/0.70 & cEuroMP(A) ) % 0.60/0.70 => cEuroMP(B) ) ). % 0.60/0.70 % 0.60/0.70 fof(cEuropeanCountry_substitution_1,axiom, % 0.60/0.70 ! [A,B] : % 0.60/0.70 ( ( A = B % 0.60/0.70 & cEuropeanCountry(A) ) % 0.60/0.70 => cEuropeanCountry(B) ) ). % 0.60/0.70 % 0.60/0.70 fof(cPerson_substitution_1,axiom, % 0.60/0.70 ! [A,B] : % 0.60/0.70 ( ( A = B % 0.60/0.70 & cPerson(A) ) % 0.60/0.70 => cPerson(B) ) ). % 0.60/0.70 % 0.60/0.70 fof(cowlNothing_substitution_1,axiom, % 0.60/0.71 ! [A,B] : % 0.60/0.71 ( ( A = B % 0.60/0.71 & cowlNothing(A) ) % 0.60/0.71 => cowlNothing(B) ) ). % 0.60/0.71 % 0.60/0.71 fof(cowlThing_substitution_1,axiom, % 0.60/0.71 ! [A,B] : % 0.60/0.71 ( ( A = B % 0.60/0.71 & cowlThing(A) ) % 0.60/0.71 => cowlThing(B) ) ). % 0.60/0.71 % 0.60/0.71 fof(rhasEuroMP_substitution_1,axiom, % 0.60/0.71 ! [A,B,C] : % 0.60/0.71 ( ( A = B % 0.60/0.71 & rhasEuroMP(A,C) ) % 0.60/0.71 => rhasEuroMP(B,C) ) ). % 0.60/0.71 % 0.60/0.71 fof(rhasEuroMP_substitution_2,axiom, % 0.60/0.71 ! [A,B,C] : % 0.60/0.71 ( ( A = B % 0.60/0.71 & rhasEuroMP(C,A) ) % 0.60/0.71 => rhasEuroMP(C,B) ) ). % 0.60/0.71 % 0.60/0.71 fof(risEuroMPFrom_substitution_1,axiom, % 0.60/0.71 ! [A,B,C] : % 0.60/0.71 ( ( A = B % 0.60/0.71 & risEuroMPFrom(A,C) ) % 0.60/0.71 => risEuroMPFrom(B,C) ) ). % 0.60/0.71 % 0.60/0.71 fof(risEuroMPFrom_substitution_2,axiom, % 0.60/0.71 ! [A,B,C] : % 0.60/0.71 ( ( A = B % 0.60/0.71 & risEuroMPFrom(C,A) ) % 0.60/0.71 => risEuroMPFrom(C,B) ) ). % 0.60/0.71 % 0.60/0.71 fof(xsd_integer_substitution_1,axiom, % 0.60/0.71 ! [A,B] : % 0.60/0.71 ( ( A = B % 0.60/0.71 & xsd_integer(A) ) % 0.60/0.71 => xsd_integer(B) ) ). % 0.60/0.71 % 0.60/0.71 fof(xsd_string_substitution_1,axiom, % 0.60/0.71 ! [A,B] : % 0.60/0.71 ( ( A = B % 0.60/0.71 & xsd_string(A) ) % 0.60/0.71 => xsd_string(B) ) ). % 0.60/0.71 % 0.60/0.71 %----Thing and Nothing % 0.60/0.71 fof(axiom_0,axiom, % 0.60/0.71 ! [X] : % 0.60/0.71 ( cowlThing(X) % 0.60/0.71 & ~ cowlNothing(X) ) ). % 0.60/0.71 % 0.60/0.71 %----String and Integer disjoint % 0.60/0.71 fof(axiom_1,axiom, % 0.60/0.71 ! [X] : % 0.60/0.71 ( xsd_string(X) % 0.60/0.71 <=> ~ xsd_integer(X) ) ). % 0.60/0.71 % 0.60/0.71 %----Enumeration cEUCountry % 0.60/0.71 fof(axiom_2,axiom, % 0.60/0.71 ! [X] : % 0.60/0.71 ( cEUCountry(X) % 0.60/0.71 <=> ( X = iBE % 0.60/0.71 | X = iFR % 0.60/0.71 | X = iES % 0.60/0.71 | X = iUK % 0.60/0.71 | X = iNL % 0.60/0.71 | X = iPT ) ) ). % 0.60/0.71 % 0.60/0.71 %----Equality cEuroMP % 0.60/0.71 fof(axiom_3,axiom, % 0.60/0.71 ! [X] : % 0.60/0.71 ( cEuroMP(X) % 0.60/0.71 <=> ? [Y] : % 0.60/0.71 ( risEuroMPFrom(X,Y) % 0.60/0.71 & cowlThing(Y) ) ) ). % 0.60/0.71 % 0.60/0.71 %----Domain: rhasEuroMP % 0.60/0.71 fof(axiom_4,axiom, % 0.60/0.71 ! [X,Y] : % 0.60/0.71 ( rhasEuroMP(X,Y) % 0.60/0.71 => cEUCountry(X) ) ). % 0.60/0.71 % 0.60/0.71 %----Inverse: risEuroMPFrom % 0.60/0.71 fof(axiom_5,axiom, % 0.60/0.71 ! [X,Y] : % 0.60/0.71 ( risEuroMPFrom(X,Y) % 0.60/0.71 <=> rhasEuroMP(Y,X) ) ). % 0.60/0.71 % 0.60/0.71 %----iBE % 0.60/0.71 fof(axiom_6,axiom, % 0.60/0.71 cEuropeanCountry(iBE) ). % 0.60/0.71 % 0.60/0.71 %----iES % 0.60/0.71 fof(axiom_7,axiom, % 0.60/0.71 cEuropeanCountry(iES) ). % 0.60/0.71 % 0.60/0.71 %----iFR % 0.60/0.71 fof(axiom_8,axiom, % 0.60/0.71 cEuropeanCountry(iFR) ). % 0.60/0.71 % 0.60/0.71 %----iKinnock % 0.60/0.71 fof(axiom_9,axiom, % 0.60/0.71 cPerson(iKinnock) ). % 0.60/0.71 % 0.60/0.71 %----iNL % 0.60/0.71 fof(axiom_10,axiom, % 0.60/0.71 cEuropeanCountry(iNL) ). % 0.60/0.71 % 0.60/0.71 %----iPT % 0.60/0.71 fof(axiom_11,axiom, % 0.60/0.71 cEuropeanCountry(iPT) ). % 0.60/0.71 % 0.60/0.71 %----iUK % 0.60/0.71 fof(axiom_12,axiom, % 0.60/0.71 cEuropeanCountry(iUK) ). % 0.60/0.71 % 0.60/0.71 fof(axiom_13,axiom, % 0.60/0.71 rhasEuroMP(iUK,iKinnock) ). % 0.60/0.71 % 0.60/0.71 %----Thing and Nothing % 0.60/0.71 %----String and Integer disjoint % 0.60/0.71 %----iKinnock % 0.60/0.71 fof(the_axiom,conjecture, % 0.60/0.71 ( ! [X] : % 0.60/0.71 ( cowlThing(X) % 0.60/0.71 & ~ cowlNothing(X) ) % 0.60/0.71 & ! [X] : % 0.60/0.71 ( xsd_string(X) % 0.60/0.71 <=> ~ xsd_integer(X) ) % 0.60/0.71 & cEuroMP(iKinnock) ) ). % 0.60/0.71 % 0.60/0.71 %------------------------------------------------------------------------------ % 0.60/0.71 %------------------------------------------- % 0.60/0.71 % Proof found % 0.60/0.71 % SZS status Theorem for theBenchmark % 0.60/0.71 % SZS output start Proof % 0.60/0.71 %ClaNum:40(EqnAxiom:15) % 0.60/0.71 %VarNum:41(SingletonVarNum:19) % 0.60/0.71 %MaxLitNum:7 % 0.60/0.71 %MaxfuncDepth:1 % 0.60/0.71 %SharedTerms:23 % 0.60/0.71 %goalClause: 33 34 % 0.60/0.71 [16]P1(a1) % 0.60/0.71 [17]P1(a5) % 0.60/0.71 [18]P1(a6) % 0.60/0.71 [19]P1(a7) % 0.60/0.71 [20]P1(a8) % 0.60/0.71 [21]P1(a10) % 0.60/0.71 [22]P4(a9) % 0.60/0.71 [23]P5(a7,a9) % 0.60/0.71 [24]~P6(x241) % 0.60/0.71 [25]P2(x251)+~E(x251,a1) % 0.60/0.71 [26]P2(x261)+~E(x261,a5) % 0.60/0.71 [27]P2(x271)+~E(x271,a6) % 0.60/0.71 [28]P2(x281)+~E(x281,a7) % 0.60/0.71 [29]P2(x291)+~E(x291,a8) % 0.60/0.71 [30]P2(x301)+~E(x301,a10) % 0.60/0.71 [31]P9(x311)+P7(x311) % 0.60/0.71 [32]~P9(x321)+~P7(x321) % 0.60/0.71 [38]~P3(x381)+P8(x381,f3(x381)) % 0.60/0.71 [36]P2(x361)+~P5(x361,x362) % 0.60/0.71 [37]P3(x371)+~P8(x371,x372) % 0.60/0.71 [39]~P8(x392,x391)+P5(x391,x392) % 0.60/0.71 [40]~P5(x402,x401)+P8(x401,x402) % 0.60/0.71 [33]P6(a2)+P7(a4)+~P3(a9)+~P9(a4) % 0.60/0.71 [34]P6(a2)+P9(a4)+~P3(a9)+~P7(a4) % 0.60/0.71 [35]~P2(x351)+E(x351,a5)+E(x351,a6)+E(x351,a7)+E(x351,a8)+E(x351,a10)+E(x351,a1) % 0.60/0.71 %EqnAxiom % 0.60/0.71 [1]E(x11,x11) % 0.60/0.71 [2]E(x22,x21)+~E(x21,x22) % 0.60/0.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.60/0.71 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 0.60/0.71 [5]~P1(x51)+P1(x52)+~E(x51,x52) % 0.60/0.71 [6]P5(x62,x63)+~E(x61,x62)+~P5(x61,x63) % 0.60/0.71 [7]P5(x73,x72)+~E(x71,x72)+~P5(x73,x71) % 0.60/0.71 [8]P8(x82,x83)+~E(x81,x82)+~P8(x81,x83) % 0.60/0.71 [9]P8(x93,x92)+~E(x91,x92)+~P8(x93,x91) % 0.60/0.71 [10]~P3(x101)+P3(x102)+~E(x101,x102) % 0.60/0.71 [11]~P2(x111)+P2(x112)+~E(x111,x112) % 0.60/0.71 [12]~P7(x121)+P7(x122)+~E(x121,x122) % 0.60/0.71 [13]~P4(x131)+P4(x132)+~E(x131,x132) % 0.60/0.71 [14]~P6(x141)+P6(x142)+~E(x141,x142) % 0.60/0.71 [15]~P9(x151)+P9(x152)+~E(x151,x152) % 0.60/0.71 % 0.60/0.71 %------------------------------------------- % 0.60/0.71 cnf(54,plain, % 0.60/0.71 (P7(a4)+~P3(a9)+~P9(a4)), % 0.60/0.71 inference(scs_inference,[],[24,33])). % 0.60/0.71 cnf(55,plain, % 0.60/0.71 (P9(a4)+~P3(a9)+~P7(a4)), % 0.60/0.71 inference(scs_inference,[],[24,34])). % 0.60/0.71 cnf(67,plain, % 0.60/0.71 (~P8(a9,x671)+P7(a4)+~P9(a4)), % 0.60/0.71 inference(scs_inference,[],[54,37])). % 0.60/0.71 cnf(79,plain, % 0.60/0.71 (P7(a4)+~P9(a4)), % 0.60/0.71 inference(scs_inference,[],[23,67,40])). % 0.60/0.71 cnf(80,plain, % 0.60/0.71 (~P9(a4)), % 0.60/0.71 inference(scs_inference,[],[79,32])). % 0.60/0.71 cnf(81,plain, % 0.60/0.71 (~P3(a9)+~P7(a4)), % 0.60/0.71 inference(scs_inference,[],[80,55])). % 0.60/0.71 cnf(82,plain, % 0.60/0.71 (~P8(a9,x821)+~P7(a4)), % 0.60/0.71 inference(scs_inference,[],[81,37])). % 0.60/0.71 cnf(83,plain, % 0.60/0.71 (~P7(a4)), % 0.60/0.71 inference(scs_inference,[],[23,82,40])). % 0.60/0.71 cnf(84,plain, % 0.60/0.71 ($false), % 0.60/0.71 inference(scs_inference,[],[80,83,31]), % 0.60/0.71 ['proof']). % 0.60/0.71 % SZS output end Proof % 0.60/0.71 % Total time :0.060000s %------------------------------------------------------------------------------