%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS099+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 : n006.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:29 EDT 2024 % Result : Unsatisfiable 0.52s 0.68s % Output : CNFRefutation 0.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS099+1 : TPTP v8.2.0. Released v3.1.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n006.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 : Wed Jun 19 12:34:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.45/0.56 start to proof:theBenchmark % 0.52/0.67 %------------------------------------------- % 0.52/0.67 % File :CSE---1.7 % 0.52/0.67 % Problem :theBenchmark % 0.52/0.67 % Transform :cnf % 0.52/0.67 % Format :tptp:raw % 0.52/0.67 % Command :java -jar mcs_scs.jar %d %s % 0.52/0.67 % 0.52/0.67 % Result :Theorem 0.040000s % 0.52/0.67 % Output :CNFRefutation 0.040000s % 0.52/0.67 %------------------------------------------- % 0.52/0.68 %------------------------------------------------------------------------------ % 0.52/0.68 % File : KRS099+1 : TPTP v8.2.0. Released v3.1.0. % 0.52/0.68 % Domain : Knowledge Representation (Semantic Web) % 0.52/0.68 % Problem : DL Test: heinsohn3c.1 % 0.52/0.68 % Version : Especial. % 0.52/0.68 % English : Tbox tests from [HK+94] % 0.52/0.68 % 0.52/0.68 % Refs : [HK+94] Heinsohn et al. (1994), An Empirical Analysis of Termi % 0.52/0.68 % : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 0.52/0.68 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 0.52/0.68 % Source : [Bec03] % 0.52/0.68 % Names : inconsistent_description-logic-Manifest109 [Bec03] % 0.52/0.68 % 0.52/0.68 % Status : Unsatisfiable % 0.52/0.68 % Rating : 0.00 v3.1.0 % 0.52/0.68 % Syntax : Number of formulae : 16 ( 1 unt; 0 def) % 0.52/0.68 % Number of atoms : 55 ( 15 equ) % 0.52/0.68 % Maximal formula atoms : 15 ( 3 avg) % 0.52/0.68 % Number of connectives : 45 ( 6 ~; 1 |; 21 &) % 0.52/0.68 % ( 2 <=>; 15 =>; 0 <=; 0 <~>) % 0.52/0.68 % Maximal formula depth : 13 ( 5 avg) % 0.52/0.68 % Maximal term depth : 1 ( 1 avg) % 0.52/0.68 % Number of predicates : 10 ( 9 usr; 0 prp; 1-2 aty) % 0.52/0.68 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 0.52/0.68 % Number of variables : 35 ( 32 !; 3 ?) % 0.52/0.68 % SPC : FOF_UNS_RFO_SEQ % 0.52/0.68 % 0.52/0.68 % Comments : Sean Bechhofer says there are some errors in the encoding of % 0.52/0.68 % datatypes, so this problem may not be perfect. At least it's % 0.52/0.68 % still representative of the type of reasoning required for OWL. % 0.52/0.68 % : Tests incoherency caused by number restrictions and role hierarchy % 0.52/0.68 %------------------------------------------------------------------------------ % 0.52/0.68 fof(cUnsatisfiable_substitution_1,axiom, % 0.52/0.68 ! [A,B] : % 0.52/0.68 ( ( A = B % 0.52/0.68 & cUnsatisfiable(A) ) % 0.52/0.68 => cUnsatisfiable(B) ) ). % 0.52/0.68 % 0.52/0.68 fof(ca_substitution_1,axiom, % 0.52/0.68 ! [A,B] : % 0.52/0.68 ( ( A = B % 0.52/0.68 & ca(A) ) % 0.52/0.68 => ca(B) ) ). % 0.52/0.68 % 0.52/0.68 fof(cc_substitution_1,axiom, % 0.52/0.68 ! [A,B] : % 0.52/0.68 ( ( A = B % 0.52/0.68 & cc(A) ) % 0.52/0.68 => cc(B) ) ). % 0.52/0.68 % 0.52/0.68 fof(cd_substitution_1,axiom, % 0.52/0.68 ! [A,B] : % 0.52/0.68 ( ( A = B % 0.52/0.68 & cd(A) ) % 0.52/0.68 => cd(B) ) ). % 0.52/0.68 % 0.52/0.68 fof(cowlNothing_substitution_1,axiom, % 0.52/0.68 ! [A,B] : % 0.52/0.68 ( ( A = B % 0.52/0.68 & cowlNothing(A) ) % 0.52/0.68 => cowlNothing(B) ) ). % 0.52/0.68 % 0.52/0.68 fof(cowlThing_substitution_1,axiom, % 0.52/0.68 ! [A,B] : % 0.52/0.68 ( ( A = B % 0.52/0.68 & cowlThing(A) ) % 0.52/0.68 => cowlThing(B) ) ). % 0.52/0.68 % 0.52/0.68 fof(rtt_substitution_1,axiom, % 0.52/0.68 ! [A,B,C] : % 0.52/0.68 ( ( A = B % 0.52/0.68 & rtt(A,C) ) % 0.52/0.68 => rtt(B,C) ) ). % 0.52/0.68 % 0.52/0.68 fof(rtt_substitution_2,axiom, % 0.52/0.68 ! [A,B,C] : % 0.52/0.68 ( ( A = B % 0.52/0.68 & rtt(C,A) ) % 0.52/0.68 => rtt(C,B) ) ). % 0.52/0.68 % 0.52/0.68 fof(xsd_integer_substitution_1,axiom, % 0.52/0.68 ! [A,B] : % 0.52/0.68 ( ( A = B % 0.52/0.68 & xsd_integer(A) ) % 0.52/0.68 => xsd_integer(B) ) ). % 0.52/0.68 % 0.52/0.68 fof(xsd_string_substitution_1,axiom, % 0.52/0.68 ! [A,B] : % 0.52/0.68 ( ( A = B % 0.52/0.68 & xsd_string(A) ) % 0.52/0.68 => xsd_string(B) ) ). % 0.52/0.68 % 0.52/0.68 %----Thing and Nothing % 0.52/0.68 fof(axiom_0,axiom, % 0.52/0.68 ! [X] : % 0.52/0.68 ( cowlThing(X) % 0.52/0.68 & ~ cowlNothing(X) ) ). % 0.52/0.68 % 0.52/0.68 %----String and Integer disjoint % 0.52/0.68 fof(axiom_1,axiom, % 0.52/0.68 ! [X] : % 0.52/0.68 ( xsd_string(X) % 0.52/0.68 <=> ~ xsd_integer(X) ) ). % 0.52/0.68 % 0.52/0.68 %----Equality cUnsatisfiable % 0.52/0.68 fof(axiom_2,axiom, % 0.52/0.68 ! [X] : % 0.52/0.68 ( cUnsatisfiable(X) % 0.52/0.68 <=> ( ? [Y0,Y1,Y2] : % 0.52/0.68 ( rtt(X,Y0) % 0.52/0.68 & rtt(X,Y1) % 0.52/0.68 & rtt(X,Y2) % 0.52/0.68 & Y0 != Y1 % 0.52/0.68 & Y0 != Y2 % 0.52/0.68 & Y1 != Y2 ) % 0.52/0.68 & ! [Y] : % 0.52/0.68 ( rtt(X,Y) % 0.52/0.68 => ca(Y) ) % 0.52/0.68 & ! [Y0,Y1] : % 0.52/0.68 ( ( rtt(X,Y0) % 0.52/0.68 & rtt(X,Y1) ) % 0.52/0.68 => Y0 = Y1 ) % 0.52/0.68 & ! [Y0,Y1] : % 0.52/0.68 ( ( rtt(X,Y0) % 0.52/0.68 & rtt(X,Y1) ) % 0.52/0.68 => Y0 = Y1 ) ) ) ). % 0.52/0.68 % 0.52/0.68 %----Super ca % 0.52/0.68 fof(axiom_3,axiom, % 0.52/0.68 ! [X] : % 0.52/0.68 ( ca(X) % 0.52/0.68 => ( cd(X) % 0.52/0.68 | cc(X) ) ) ). % 0.52/0.68 % 0.52/0.68 %----Super cc % 0.52/0.68 fof(axiom_4,axiom, % 0.52/0.68 ! [X] : % 0.52/0.68 ( cc(X) % 0.52/0.68 => ~ cd(X) ) ). % 0.52/0.68 % 0.52/0.68 %----i2003_11_14_17_20_29215 % 0.52/0.68 fof(axiom_5,axiom, % 0.52/0.68 cUnsatisfiable(i2003_11_14_17_20_29215) ). % 0.52/0.68 % 0.52/0.68 %------------------------------------------------------------------------------ % 0.52/0.68 %------------------------------------------- % 0.52/0.68 % Proof found % 0.52/0.68 % SZS status Theorem for theBenchmark % 0.52/0.68 % SZS output start Proof % 0.52/0.68 %ClaNum:53(EqnAxiom:20) % 0.52/0.68 %VarNum:372(SingletonVarNum:88) % 0.52/0.68 %MaxLitNum:10 % 0.52/0.68 %MaxfuncDepth:1 % 0.52/0.68 %SharedTerms:2 % 0.52/0.68 [21]P1(a1) % 0.52/0.68 [22]~P2(x221) % 0.52/0.68 [23]P8(x231)+P6(x231) % 0.52/0.68 [24]~P5(x241)+~P3(x241) % 0.52/0.68 [25]~P8(x251)+~P6(x251) % 0.52/0.68 [27]~P1(x271)+~E(f2(x271),f3(x271)) % 0.52/0.68 [28]~P1(x281)+~E(f4(x281),f3(x281)) % 0.52/0.68 [29]~P1(x291)+~E(f4(x291),f2(x291)) % 0.52/0.68 [30]~P1(x301)+P7(x301,f3(x301)) % 0.52/0.69 [31]~P1(x311)+P7(x311,f2(x311)) % 0.52/0.69 [32]~P1(x321)+P7(x321,f4(x321)) % 0.52/0.69 [26]P5(x261)+~P4(x261)+P3(x261) % 0.52/0.69 [33]~P7(x332,x331)+P4(x331)+~P1(x332) % 0.52/0.69 [35]~P7(x353,x352)+~P7(x353,x351)+E(x351,x352)+~P1(x353) % 0.52/0.69 [36]E(x363,x361)+~P7(x364,x362)+~P7(x364,x361)+~P7(x364,x363)+E(x361,x362)+E(x363,x362)+P1(x364)+~E(f5(x364),f6(x364))+~E(f8(x364),f9(x364))+~P4(f7(x364)) % 0.52/0.69 [37]E(x373,x371)+~P7(x374,x372)+~P7(x374,x371)+~P7(x374,x373)+E(x371,x372)+E(x373,x372)+P1(x374)+P7(x374,f7(x374))+~E(f5(x374),f6(x374))+~E(f8(x374),f9(x374)) % 0.52/0.69 [38]E(x383,x381)+~P7(x384,x382)+~P7(x384,x381)+~P7(x384,x383)+E(x381,x382)+E(x383,x382)+P1(x384)+P7(x384,f6(x384))+~E(f8(x384),f9(x384))+~P4(f7(x384)) % 0.52/0.69 [39]E(x393,x391)+~P7(x394,x392)+~P7(x394,x391)+~P7(x394,x393)+E(x391,x392)+E(x393,x392)+P1(x394)+P7(x394,f5(x394))+~E(f8(x394),f9(x394))+~P4(f7(x394)) % 0.52/0.69 [40]E(x403,x401)+~P7(x404,x402)+~P7(x404,x401)+~P7(x404,x403)+E(x401,x402)+E(x403,x402)+P1(x404)+P7(x404,f9(x404))+~E(f5(x404),f6(x404))+~P4(f7(x404)) % 0.52/0.69 [41]E(x413,x411)+~P7(x414,x412)+~P7(x414,x411)+~P7(x414,x413)+E(x411,x412)+E(x413,x412)+P1(x414)+P7(x414,f8(x414))+~E(f5(x414),f6(x414))+~P4(f7(x414)) % 0.52/0.69 [42]E(x423,x421)+~P7(x424,x422)+~P7(x424,x421)+~P7(x424,x423)+E(x421,x422)+E(x423,x422)+P1(x424)+P7(x424,f7(x424))+P7(x424,f6(x424))+~E(f8(x424),f9(x424)) % 0.52/0.69 [43]E(x433,x431)+~P7(x434,x432)+~P7(x434,x431)+~P7(x434,x433)+E(x431,x432)+E(x433,x432)+P1(x434)+P7(x434,f7(x434))+P7(x434,f5(x434))+~E(f8(x434),f9(x434)) % 0.52/0.69 [44]E(x443,x441)+~P7(x444,x442)+~P7(x444,x441)+~P7(x444,x443)+E(x441,x442)+E(x443,x442)+P1(x444)+P7(x444,f7(x444))+P7(x444,f9(x444))+~E(f5(x444),f6(x444)) % 0.52/0.69 [45]E(x453,x451)+~P7(x454,x452)+~P7(x454,x451)+~P7(x454,x453)+E(x451,x452)+E(x453,x452)+P1(x454)+P7(x454,f7(x454))+P7(x454,f8(x454))+~E(f5(x454),f6(x454)) % 0.52/0.69 [46]E(x463,x461)+~P7(x464,x462)+~P7(x464,x461)+~P7(x464,x463)+E(x461,x462)+E(x463,x462)+P1(x464)+P7(x464,f6(x464))+P7(x464,f9(x464))+~P4(f7(x464)) % 0.52/0.69 [47]E(x473,x471)+~P7(x474,x472)+~P7(x474,x471)+~P7(x474,x473)+E(x471,x472)+E(x473,x472)+P1(x474)+P7(x474,f6(x474))+P7(x474,f8(x474))+~P4(f7(x474)) % 0.52/0.69 [48]E(x483,x481)+~P7(x484,x482)+~P7(x484,x481)+~P7(x484,x483)+E(x481,x482)+E(x483,x482)+P1(x484)+P7(x484,f5(x484))+P7(x484,f9(x484))+~P4(f7(x484)) % 0.52/0.69 [49]E(x493,x491)+~P7(x494,x492)+~P7(x494,x491)+~P7(x494,x493)+E(x491,x492)+E(x493,x492)+P1(x494)+P7(x494,f5(x494))+P7(x494,f8(x494))+~P4(f7(x494)) % 0.52/0.69 [50]E(x503,x501)+~P7(x504,x502)+~P7(x504,x501)+~P7(x504,x503)+E(x501,x502)+E(x503,x502)+P1(x504)+P7(x504,f7(x504))+P7(x504,f6(x504))+P7(x504,f9(x504)) % 0.52/0.69 [51]E(x513,x511)+~P7(x514,x512)+~P7(x514,x511)+~P7(x514,x513)+E(x511,x512)+E(x513,x512)+P1(x514)+P7(x514,f7(x514))+P7(x514,f6(x514))+P7(x514,f8(x514)) % 0.52/0.69 [52]E(x523,x521)+~P7(x524,x522)+~P7(x524,x521)+~P7(x524,x523)+E(x521,x522)+E(x523,x522)+P1(x524)+P7(x524,f7(x524))+P7(x524,f5(x524))+P7(x524,f9(x524)) % 0.52/0.69 [53]E(x533,x531)+~P7(x534,x532)+~P7(x534,x531)+~P7(x534,x533)+E(x531,x532)+E(x533,x532)+P1(x534)+P7(x534,f7(x534))+P7(x534,f5(x534))+P7(x534,f8(x534)) % 0.52/0.69 %EqnAxiom % 0.52/0.69 [1]E(x11,x11) % 0.52/0.69 [2]E(x22,x21)+~E(x21,x22) % 0.52/0.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.52/0.69 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.52/0.69 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 0.52/0.69 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 0.52/0.69 [7]~E(x71,x72)+E(f7(x71),f7(x72)) % 0.52/0.69 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 0.52/0.69 [9]~E(x91,x92)+E(f8(x91),f8(x92)) % 0.52/0.69 [10]~E(x101,x102)+E(f9(x101),f9(x102)) % 0.52/0.69 [11]~E(x111,x112)+E(f6(x111),f6(x112)) % 0.52/0.69 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 0.52/0.69 [13]~P2(x131)+P2(x132)+~E(x131,x132) % 0.52/0.69 [14]~P6(x141)+P6(x142)+~E(x141,x142) % 0.52/0.69 [15]~P8(x151)+P8(x152)+~E(x151,x152) % 0.52/0.69 [16]~P3(x161)+P3(x162)+~E(x161,x162) % 0.52/0.69 [17]~P5(x171)+P5(x172)+~E(x171,x172) % 0.52/0.69 [18]P7(x182,x183)+~E(x181,x182)+~P7(x181,x183) % 0.52/0.69 [19]P7(x193,x192)+~E(x191,x192)+~P7(x193,x191) % 0.52/0.69 [20]~P4(x201)+P4(x202)+~E(x201,x202) % 0.52/0.69 % 0.52/0.69 %------------------------------------------- % 0.52/0.69 cnf(59,plain, % 0.52/0.69 (~E(a1,x591)+P7(x591,f3(x591))), % 0.52/0.69 inference(scs_inference,[],[21,30,12])). % 0.52/0.69 cnf(60,plain, % 0.52/0.69 (P7(a1,f3(a1))), % 0.52/0.69 inference(equality_inference,[],[59])). % 0.52/0.69 cnf(65,plain, % 0.52/0.69 (~E(a1,x651)+P7(x651,f2(x651))), % 0.52/0.69 inference(scs_inference,[],[21,31,12])). % 0.52/0.69 cnf(66,plain, % 0.52/0.69 (P7(a1,f2(a1))), % 0.52/0.69 inference(equality_inference,[],[65])). % 0.52/0.69 cnf(77,plain, % 0.52/0.69 (~E(a1,x771)+~E(f2(x771),f3(x771))), % 0.52/0.69 inference(scs_inference,[],[21,27,12])). % 0.52/0.69 cnf(89,plain, % 0.52/0.69 ($false), % 0.52/0.69 inference(scs_inference,[],[21,60,66,77,35]), % 0.52/0.69 ['proof']). % 0.52/0.69 % SZS output end Proof % 0.52/0.69 % Total time :0.040000s %------------------------------------------------------------------------------