%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS071+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 : n024.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:23 EDT 2024 % Result : Unsatisfiable 0.66s 0.90s % Output : CNFRefutation 0.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : KRS071+1 : TPTP v8.2.0. Released v3.1.0. % 0.04/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.15/0.36 % Computer : n024.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 300 % 0.15/0.36 % DateTime : Wed Jun 19 13:34:09 EDT 2024 % 0.15/0.36 % CPUTime : % 0.61/0.66 start to proof:theBenchmark % 0.66/0.89 %------------------------------------------- % 0.66/0.89 % File :CSE---1.7 % 0.66/0.89 % Problem :theBenchmark % 0.66/0.89 % Transform :cnf % 0.66/0.89 % Format :tptp:raw % 0.66/0.89 % Command :java -jar mcs_scs.jar %d %s % 0.66/0.89 % 0.66/0.89 % Result :Theorem 0.180000s % 0.66/0.89 % Output :CNFRefutation 0.180000s % 0.66/0.89 %------------------------------------------- % 0.66/0.89 %------------------------------------------------------------------------------ % 0.66/0.89 % File : KRS071+1 : TPTP v8.2.0. Released v3.1.0. % 0.66/0.89 % Domain : Knowledge Representation (Semantic Web) % 0.66/0.89 % Problem : DL Test: t1.2 % 0.66/0.89 % Version : Especial. % 0.66/0.89 % English : % 0.66/0.89 % 0.66/0.89 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 0.66/0.89 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 0.66/0.89 % Source : [Bec03] % 0.66/0.89 % Names : inconsistent_description-logic-Manifest007 [Bec03] % 0.66/0.89 % 0.66/0.89 % Status : Unsatisfiable % 0.66/0.89 % Rating : 0.00 v3.1.0 % 0.66/0.89 % Syntax : Number of formulae : 23 ( 1 unt; 0 def) % 0.66/0.89 % Number of atoms : 76 ( 17 equ) % 0.66/0.89 % Maximal formula atoms : 13 ( 3 avg) % 0.66/0.89 % Number of connectives : 59 ( 6 ~; 8 |; 23 &) % 0.66/0.89 % ( 3 <=>; 19 =>; 0 <=; 0 <~>) % 0.66/0.89 % Maximal formula depth : 12 ( 5 avg) % 0.66/0.89 % Maximal term depth : 1 ( 1 avg) % 0.66/0.89 % Number of predicates : 13 ( 12 usr; 0 prp; 1-2 aty) % 0.66/0.89 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 0.66/0.89 % Number of variables : 47 ( 44 !; 3 ?) % 0.66/0.89 % SPC : FOF_UNS_RFO_SEQ % 0.66/0.89 % 0.66/0.89 % Comments : Sean Bechhofer says there are some errors in the encoding of % 0.66/0.89 % datatypes, so this problem may not be perfect. At least it's % 0.66/0.89 % still representative of the type of reasoning required for OWL. % 0.66/0.89 %------------------------------------------------------------------------------ % 0.66/0.89 fof(cUnsatisfiable_substitution_1,axiom, % 0.66/0.89 ! [A,B] : % 0.66/0.89 ( ( A = B % 0.66/0.89 & cUnsatisfiable(A) ) % 0.66/0.89 => cUnsatisfiable(B) ) ). % 0.66/0.89 % 0.66/0.89 fof(cowlNothing_substitution_1,axiom, % 0.66/0.89 ! [A,B] : % 0.66/0.89 ( ( A = B % 0.66/0.89 & cowlNothing(A) ) % 0.66/0.89 => cowlNothing(B) ) ). % 0.66/0.89 % 0.66/0.89 fof(cowlThing_substitution_1,axiom, % 0.66/0.89 ! [A,B] : % 0.66/0.89 ( ( A = B % 0.66/0.89 & cowlThing(A) ) % 0.66/0.89 => cowlThing(B) ) ). % 0.66/0.89 % 0.66/0.89 fof(cp1_substitution_1,axiom, % 0.66/0.89 ! [A,B] : % 0.66/0.89 ( ( A = B % 0.66/0.89 & cp1(A) ) % 0.66/0.89 => cp1(B) ) ). % 0.66/0.89 % 0.66/0.89 fof(cp2_substitution_1,axiom, % 0.66/0.89 ! [A,B] : % 0.66/0.89 ( ( A = B % 0.66/0.89 & cp2(A) ) % 0.66/0.90 => cp2(B) ) ). % 0.66/0.90 % 0.66/0.90 fof(cp3_substitution_1,axiom, % 0.66/0.90 ! [A,B] : % 0.66/0.90 ( ( A = B % 0.66/0.90 & cp3(A) ) % 0.66/0.90 => cp3(B) ) ). % 0.66/0.90 % 0.66/0.90 fof(cp4_substitution_1,axiom, % 0.66/0.90 ! [A,B] : % 0.66/0.90 ( ( A = B % 0.66/0.90 & cp4(A) ) % 0.66/0.90 => cp4(B) ) ). % 0.66/0.90 % 0.66/0.90 fof(cp5_substitution_1,axiom, % 0.66/0.90 ! [A,B] : % 0.66/0.90 ( ( A = B % 0.66/0.90 & cp5(A) ) % 0.66/0.90 => cp5(B) ) ). % 0.66/0.90 % 0.66/0.90 fof(rinvR_substitution_1,axiom, % 0.66/0.90 ! [A,B,C] : % 0.66/0.90 ( ( A = B % 0.66/0.90 & rinvR(A,C) ) % 0.66/0.90 => rinvR(B,C) ) ). % 0.66/0.90 % 0.66/0.90 fof(rinvR_substitution_2,axiom, % 0.66/0.90 ! [A,B,C] : % 0.66/0.90 ( ( A = B % 0.66/0.90 & rinvR(C,A) ) % 0.66/0.90 => rinvR(C,B) ) ). % 0.66/0.90 % 0.66/0.90 fof(rr_substitution_1,axiom, % 0.66/0.90 ! [A,B,C] : % 0.66/0.90 ( ( A = B % 0.66/0.90 & rr(A,C) ) % 0.66/0.90 => rr(B,C) ) ). % 0.66/0.90 % 0.66/0.90 fof(rr_substitution_2,axiom, % 0.66/0.90 ! [A,B,C] : % 0.66/0.90 ( ( A = B % 0.66/0.90 & rr(C,A) ) % 0.66/0.90 => rr(C,B) ) ). % 0.66/0.90 % 0.66/0.90 fof(xsd_integer_substitution_1,axiom, % 0.66/0.90 ! [A,B] : % 0.66/0.90 ( ( A = B % 0.66/0.90 & xsd_integer(A) ) % 0.66/0.90 => xsd_integer(B) ) ). % 0.66/0.90 % 0.66/0.90 fof(xsd_string_substitution_1,axiom, % 0.66/0.90 ! [A,B] : % 0.66/0.90 ( ( A = B % 0.66/0.90 & xsd_string(A) ) % 0.66/0.90 => xsd_string(B) ) ). % 0.66/0.90 % 0.66/0.90 %----Thing and Nothing % 0.66/0.90 fof(axiom_0,axiom, % 0.66/0.90 ! [X] : % 0.66/0.90 ( cowlThing(X) % 0.66/0.90 & ~ cowlNothing(X) ) ). % 0.66/0.90 % 0.66/0.90 %----String and Integer disjoint % 0.66/0.90 fof(axiom_1,axiom, % 0.66/0.90 ! [X] : % 0.66/0.90 ( xsd_string(X) % 0.66/0.90 <=> ~ xsd_integer(X) ) ). % 0.66/0.90 % 0.66/0.90 %----Equality cUnsatisfiable % 0.66/0.90 fof(axiom_2,axiom, % 0.66/0.90 ! [X] : % 0.66/0.90 ( cUnsatisfiable(X) % 0.66/0.90 <=> ( ? [Y] : % 0.66/0.90 ( rr(X,Y) % 0.66/0.90 & cp1(Y) ) % 0.66/0.90 & ? [Y] : % 0.66/0.90 ( rr(X,Y) % 0.66/0.90 & cp2(Y) ) % 0.66/0.90 & ? [Y] : % 0.66/0.90 ( rr(X,Y) % 0.66/0.90 & cp3(Y) ) % 0.66/0.90 & ! [Y0,Y1,Y2] : % 0.66/0.90 ( ( rr(X,Y0) % 0.66/0.90 & rr(X,Y1) % 0.66/0.90 & rr(X,Y2) ) % 0.66/0.90 => ( Y0 = Y1 % 0.66/0.90 | Y0 = Y2 % 0.66/0.90 | Y1 = Y2 ) ) ) ) ). % 0.66/0.90 % 0.66/0.90 %----Super cp1 % 0.66/0.90 fof(axiom_3,axiom, % 0.66/0.90 ! [X] : % 0.66/0.90 ( cp1(X) % 0.66/0.90 => ~ ( cp4(X) % 0.66/0.90 | cp2(X) % 0.66/0.90 | cp3(X) % 0.66/0.90 | cp5(X) ) ) ). % 0.66/0.90 % 0.66/0.90 %----Super cp2 % 0.66/0.90 fof(axiom_4,axiom, % 0.66/0.90 ! [X] : % 0.66/0.90 ( cp2(X) % 0.66/0.90 => ~ ( cp4(X) % 0.66/0.90 | cp3(X) % 0.66/0.90 | cp5(X) ) ) ). % 0.66/0.90 % 0.66/0.90 %----Super cp3 % 0.66/0.90 fof(axiom_5,axiom, % 0.66/0.90 ! [X] : % 0.66/0.90 ( cp3(X) % 0.66/0.90 => ~ ( cp4(X) % 0.66/0.90 | cp5(X) ) ) ). % 0.66/0.90 % 0.66/0.90 %----Super cp4 % 0.66/0.90 fof(axiom_6,axiom, % 0.66/0.90 ! [X] : % 0.66/0.90 ( cp4(X) % 0.66/0.90 => ~ cp5(X) ) ). % 0.66/0.90 % 0.66/0.90 %----Inverse: rinvR % 0.66/0.90 fof(axiom_7,axiom, % 0.66/0.90 ! [X,Y] : % 0.66/0.90 ( rinvR(X,Y) % 0.66/0.90 <=> rr(Y,X) ) ). % 0.66/0.90 % 0.66/0.90 %----i2003_11_14_17_18_39380 % 0.66/0.90 fof(axiom_8,axiom, % 0.66/0.90 cUnsatisfiable(i2003_11_14_17_18_39380) ). % 0.66/0.90 % 0.66/0.90 %------------------------------------------------------------------------------ % 0.66/0.90 %------------------------------------------- % 0.66/0.90 % Proof found % 0.66/0.90 % SZS status Theorem for theBenchmark % 0.66/0.90 % SZS output start Proof % 0.66/0.90 %ClaNum:51(EqnAxiom:22) % 0.66/0.90 %VarNum:133(SingletonVarNum:51) % 0.66/0.90 %MaxLitNum:8 % 0.66/0.90 %MaxfuncDepth:1 % 0.66/0.90 %SharedTerms:2 % 0.66/0.90 [23]P1(a1) % 0.66/0.90 [24]~P2(x241) % 0.66/0.90 [25]P11(x251)+P3(x251) % 0.66/0.90 [26]~P5(x261)+~P4(x261) % 0.66/0.90 [27]~P6(x271)+~P4(x271) % 0.66/0.90 [28]~P7(x281)+~P4(x281) % 0.66/0.90 [29]~P8(x291)+~P4(x291) % 0.66/0.90 [30]~P6(x301)+~P5(x301) % 0.66/0.90 [31]~P7(x311)+~P5(x311) % 0.66/0.90 [32]~P8(x321)+~P5(x321) % 0.66/0.90 [33]~P7(x331)+~P6(x331) % 0.66/0.90 [34]~P8(x341)+~P6(x341) % 0.66/0.90 [35]~P8(x351)+~P7(x351) % 0.66/0.90 [36]~P11(x361)+~P3(x361) % 0.66/0.90 [37]~P1(x371)+P4(f2(x371)) % 0.66/0.90 [38]~P1(x381)+P5(f3(x381)) % 0.66/0.90 [39]~P1(x391)+P6(f4(x391)) % 0.66/0.90 [40]~P1(x401)+P9(x401,f2(x401)) % 0.66/0.90 [41]~P1(x411)+P9(x411,f3(x411)) % 0.66/0.90 [42]~P1(x421)+P9(x421,f4(x421)) % 0.66/0.90 [43]~P9(x432,x431)+P10(x431,x432) % 0.66/0.90 [44]~P10(x442,x441)+P9(x441,x442) % 0.66/0.90 [45]E(x453,x451)+~P9(x454,x452)+~P9(x454,x451)+~P9(x454,x453)+E(x451,x452)+E(x453,x452)+~P1(x454) % 0.66/0.90 [46]~P9(x461,x464)+~P9(x461,x463)+~P9(x461,x462)+P1(x461)+~P4(x462)+~P5(x463)+~P6(x464)+~E(f5(x461),f6(x461)) % 0.66/0.90 [47]~P9(x471,x474)+~P9(x471,x473)+~P9(x471,x472)+P1(x471)+~P4(x472)+~P5(x473)+~P6(x474)+~E(f7(x471),f6(x471)) % 0.66/0.90 [48]~P9(x481,x484)+~P9(x481,x483)+~P9(x481,x482)+P1(x481)+~P4(x482)+~P5(x483)+~P6(x484)+~E(f7(x481),f5(x481)) % 0.66/0.90 [49]~P9(x491,x494)+~P9(x491,x493)+~P9(x491,x492)+P1(x491)+~P4(x492)+~P5(x493)+~P6(x494)+P9(x491,f6(x491)) % 0.66/0.90 [50]~P9(x501,x504)+~P9(x501,x503)+~P9(x501,x502)+P1(x501)+~P4(x502)+~P5(x503)+~P6(x504)+P9(x501,f5(x501)) % 0.66/0.90 [51]~P9(x511,x514)+~P9(x511,x513)+~P9(x511,x512)+P1(x511)+~P4(x512)+~P5(x513)+~P6(x514)+P9(x511,f7(x511)) % 0.66/0.90 %EqnAxiom % 0.66/0.90 [1]E(x11,x11) % 0.66/0.90 [2]E(x22,x21)+~E(x21,x22) % 0.66/0.90 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.66/0.90 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.66/0.90 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 0.66/0.90 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 0.66/0.90 [7]~E(x71,x72)+E(f7(x71),f7(x72)) % 0.66/0.90 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 0.66/0.90 [9]~E(x91,x92)+E(f6(x91),f6(x92)) % 0.66/0.90 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 0.66/0.90 [11]~P2(x111)+P2(x112)+~E(x111,x112) % 0.66/0.90 [12]~P3(x121)+P3(x122)+~E(x121,x122) % 0.66/0.90 [13]~P11(x131)+P11(x132)+~E(x131,x132) % 0.66/0.90 [14]~P4(x141)+P4(x142)+~E(x141,x142) % 0.66/0.90 [15]~P5(x151)+P5(x152)+~E(x151,x152) % 0.66/0.90 [16]P9(x162,x163)+~E(x161,x162)+~P9(x161,x163) % 0.66/0.90 [17]P9(x173,x172)+~E(x171,x172)+~P9(x173,x171) % 0.66/0.90 [18]~P6(x181)+P6(x182)+~E(x181,x182) % 0.66/0.90 [19]P10(x192,x193)+~E(x191,x192)+~P10(x191,x193) % 0.66/0.90 [20]P10(x203,x202)+~E(x201,x202)+~P10(x203,x201) % 0.66/0.90 [21]~P7(x211)+P7(x212)+~E(x211,x212) % 0.66/0.90 [22]~P8(x221)+P8(x222)+~E(x221,x222) % 0.66/0.90 % 0.66/0.90 %------------------------------------------- % 0.66/0.90 cnf(57,plain, % 0.66/0.90 (~P6(f3(a1))), % 0.66/0.90 inference(scs_inference,[],[23,30,38])). % 0.66/0.90 cnf(66,plain, % 0.66/0.90 (~E(a1,x661)+P9(x661,f2(x661))), % 0.66/0.90 inference(scs_inference,[],[23,40,10])). % 0.66/0.90 cnf(67,plain, % 0.66/0.90 (P9(a1,f2(a1))), % 0.66/0.90 inference(equality_inference,[],[66])). % 0.66/0.90 cnf(72,plain, % 0.66/0.90 (~E(a1,x721)+P9(x721,f3(x721))), % 0.66/0.90 inference(scs_inference,[],[23,41,10])). % 0.66/0.90 cnf(73,plain, % 0.66/0.90 (P9(a1,f3(a1))), % 0.66/0.90 inference(equality_inference,[],[72])). % 0.66/0.90 cnf(78,plain, % 0.66/0.90 (~E(a1,x781)+P9(x781,f4(x781))), % 0.66/0.90 inference(scs_inference,[],[23,42,10])). % 0.66/0.90 cnf(79,plain, % 0.66/0.90 (P9(a1,f4(a1))), % 0.66/0.90 inference(equality_inference,[],[78])). % 0.66/0.90 cnf(107,plain, % 0.66/0.90 (~E(x1071,x1072)+P11(x1071)+P3(x1072)), % 0.66/0.90 inference(scs_inference,[],[25,12])). % 0.66/0.90 cnf(111,plain, % 0.66/0.90 (~P4(f3(a1))), % 0.66/0.90 inference(scs_inference,[],[23,26,38])). % 0.66/0.90 cnf(116,plain, % 0.66/0.90 (~P4(f4(a1))), % 0.66/0.90 inference(scs_inference,[],[23,27,39])). % 0.66/0.90 cnf(129,plain, % 0.66/0.90 (~P5(f4(a1))), % 0.66/0.90 inference(scs_inference,[],[23,30,39])). % 0.66/0.90 cnf(156,plain, % 0.66/0.90 (P11(x1561)+~P11(x1562)+~E(x1561,x1562)), % 0.66/0.90 inference(scs_inference,[],[36,107])). % 0.66/0.90 cnf(160,plain, % 0.66/0.90 (~E(f2(a1),f3(a1))), % 0.66/0.90 inference(scs_inference,[],[23,111,37,14])). % 0.66/0.90 cnf(161,plain, % 0.66/0.90 (~E(f2(a1),f4(a1))), % 0.66/0.90 inference(scs_inference,[],[23,116,37,14])). % 0.66/0.90 cnf(168,plain, % 0.66/0.90 (~P6(f4(a1))), % 0.66/0.90 inference(scs_inference,[],[79,67,73,57,129,160,161,23,45,2,156,15,18])). % 0.66/0.90 cnf(174,plain, % 0.66/0.90 ($false), % 0.66/0.90 inference(scs_inference,[],[168,23,39]), % 0.66/0.90 ['proof']). % 0.66/0.90 % SZS output end Proof % 0.66/0.90 % Total time :0.180000s %------------------------------------------------------------------------------