%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS116+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 : n025.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:33 EDT 2024 % Result : Unsatisfiable 24.40s 24.52s % Output : CNFRefutation 24.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : KRS116+1 : TPTP v8.2.0. Released v3.1.0. % 0.00/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.09/0.29 % Computer : n025.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Wed Jun 19 14:21:53 EDT 2024 % 0.09/0.29 % CPUTime : % 0.45/0.52 start to proof:theBenchmark % 24.40/24.51 %------------------------------------------- % 24.40/24.51 % File :CSE---1.7 % 24.40/24.51 % Problem :theBenchmark % 24.40/24.51 % Transform :cnf % 24.40/24.51 % Format :tptp:raw % 24.40/24.51 % Command :java -jar mcs_scs.jar %d %s % 24.40/24.51 % 24.40/24.51 % Result :Theorem 23.940000s % 24.40/24.51 % Output :CNFRefutation 23.940000s % 24.40/24.51 %------------------------------------------- % 24.40/24.52 %------------------------------------------------------------------------------ % 24.40/24.52 % File : KRS116+1 : TPTP v8.2.0. Released v3.1.0. % 24.40/24.52 % Domain : Knowledge Representation (Semantic Web) % 24.40/24.52 % Problem : DL Test: t4.1 Dynamic blocking example % 24.40/24.52 % Version : Especial. % 24.40/24.52 % English : % 24.40/24.52 % 24.40/24.52 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 24.40/24.52 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 24.40/24.52 % Source : [Bec03] % 24.40/24.52 % Names : inconsistent_description-logic-Manifest623 [Bec03] % 24.40/24.52 % 24.40/24.52 % Status : Unsatisfiable % 24.40/24.52 % Rating : 0.00 v6.4.0, 0.25 v6.3.0, 0.00 v3.1.0 % 24.40/24.52 % Syntax : Number of formulae : 18 ( 1 unt; 0 def) % 24.40/24.52 % Number of atoms : 54 ( 0 equ) % 24.40/24.52 % Maximal formula atoms : 13 ( 3 avg) % 24.40/24.52 % Number of connectives : 39 ( 3 ~; 0 |; 12 &) % 24.40/24.52 % ( 13 <=>; 11 =>; 0 <=; 0 <~>) % 24.40/24.52 % Maximal formula depth : 10 ( 5 avg) % 24.40/24.52 % Maximal term depth : 1 ( 1 avg) % 24.40/24.52 % Number of predicates : 21 ( 21 usr; 0 prp; 1-2 aty) % 24.40/24.52 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 24.40/24.52 % Number of variables : 37 ( 30 !; 7 ?) % 24.40/24.52 % SPC : FOF_UNS_RFO_NEQ % 24.40/24.52 % 24.40/24.52 % Comments : Sean Bechhofer says there are some errors in the encoding of % 24.40/24.52 % datatypes, so this problem may not be perfect. At least it's % 24.40/24.52 % still representative of the type of reasoning required for OWL. % 24.40/24.52 %------------------------------------------------------------------------------ % 24.40/24.52 %----Thing and Nothing % 24.40/24.52 fof(axiom_0,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( cowlThing(X) % 24.40/24.52 & ~ cowlNothing(X) ) ). % 24.40/24.52 % 24.40/24.52 %----String and Integer disjoint % 24.40/24.52 fof(axiom_1,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( xsd_string(X) % 24.40/24.52 <=> ~ xsd_integer(X) ) ). % 24.40/24.52 % 24.40/24.52 %----Super cUnsatisfiable % 24.40/24.52 fof(axiom_2,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( cUnsatisfiable(X) % 24.40/24.52 => ca(X) ) ). % 24.40/24.52 % 24.40/24.52 %----Super cUnsatisfiable % 24.40/24.52 fof(axiom_3,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( cUnsatisfiable(X) % 24.40/24.52 => ? [Y] : % 24.40/24.52 ( rs(X,Y) % 24.40/24.52 & ca_Ax2(Y) ) ) ). % 24.40/24.52 % 24.40/24.52 %----Equality ca % 24.40/24.52 fof(axiom_4,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( ca(X) % 24.40/24.52 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 24.40/24.52 % 24.40/24.52 %----Equality caxcomp % 24.40/24.52 fof(axiom_5,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( caxcomp(X) % 24.40/24.52 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 24.40/24.52 % 24.40/24.52 %----Equality cc % 24.40/24.52 fof(axiom_6,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( cc(X) % 24.40/24.52 <=> ! [Y] : % 24.40/24.52 ( rinvR(X,Y) % 24.40/24.52 => ca_Vx7(Y) ) ) ). % 24.40/24.52 % 24.40/24.52 %----Equality ca_Ax2 % 24.40/24.52 fof(axiom_7,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( ca_Ax2(X) % 24.40/24.52 <=> ( ! [Y] : % 24.40/24.52 ( rp(X,Y) % 24.40/24.52 => ca_Vx3(Y) ) % 24.40/24.52 & ! [Y] : % 24.40/24.52 ( rp(X,Y) % 24.40/24.52 => ca_Vx5(Y) ) % 24.40/24.52 & ! [Y] : % 24.40/24.52 ( rr(X,Y) % 24.40/24.52 => cc(Y) ) % 24.40/24.52 & ? [Y] : % 24.40/24.52 ( rr(X,Y) % 24.40/24.52 & cowlThing(Y) ) % 24.40/24.52 & ? [Y] : % 24.40/24.52 ( rp(X,Y) % 24.40/24.52 & cowlThing(Y) ) % 24.40/24.52 & ! [Y] : % 24.40/24.52 ( rp(X,Y) % 24.40/24.52 => ca_Vx4(Y) ) ) ) ). % 24.40/24.52 % 24.40/24.52 %----Equality ca_Vx3 % 24.40/24.52 fof(axiom_8,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( ca_Vx3(X) % 24.40/24.52 <=> ? [Y] : % 24.40/24.52 ( rr(X,Y) % 24.40/24.52 & cowlThing(Y) ) ) ). % 24.40/24.52 % 24.40/24.52 %----Equality ca_Vx4 % 24.40/24.52 fof(axiom_9,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( ca_Vx4(X) % 24.40/24.52 <=> ? [Y] : % 24.40/24.52 ( rp(X,Y) % 24.40/24.52 & cowlThing(Y) ) ) ). % 24.40/24.52 % 24.40/24.52 %----Equality ca_Vx5 % 24.40/24.52 fof(axiom_10,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( ca_Vx5(X) % 24.40/24.52 <=> ! [Y] : % 24.40/24.52 ( rr(X,Y) % 24.40/24.52 => cc(Y) ) ) ). % 24.40/24.52 % 24.40/24.52 %----Equality ca_Vx6 % 24.40/24.52 fof(axiom_11,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( ca_Vx6(X) % 24.40/24.52 <=> ! [Y] : % 24.40/24.52 ( rinvS(X,Y) % 24.40/24.52 => caxcomp(Y) ) ) ). % 24.40/24.52 % 24.40/24.52 %----Equality ca_Vx7 % 24.40/24.52 fof(axiom_12,axiom, % 24.40/24.52 ! [X] : % 24.40/24.52 ( ca_Vx7(X) % 24.40/24.52 <=> ! [Y] : % 24.40/24.52 ( rinvP(X,Y) % 24.40/24.52 => ca_Vx6(Y) ) ) ). % 24.40/24.52 % 24.40/24.52 %----Inverse: rinvP % 24.40/24.52 fof(axiom_13,axiom, % 24.40/24.52 ! [X,Y] : % 24.40/24.52 ( rinvP(X,Y) % 24.40/24.52 <=> rp(Y,X) ) ). % 24.40/24.52 % 24.40/24.52 %----Inverse: rinvR % 24.40/24.52 fof(axiom_14,axiom, % 24.40/24.52 ! [X,Y] : % 24.40/24.52 ( rinvR(X,Y) % 24.40/24.52 <=> rr(Y,X) ) ). % 24.40/24.52 % 24.40/24.52 %----Inverse: rinvS % 24.40/24.52 fof(axiom_15,axiom, % 24.40/24.52 ! [X,Y] : % 24.40/24.52 ( rinvS(X,Y) % 24.40/24.52 <=> rs(Y,X) ) ). % 24.40/24.52 % 24.40/24.52 %----Transitive: rp % 24.40/24.52 fof(axiom_16,axiom, % 24.40/24.52 ! [X,Y,Z] : % 24.40/24.52 ( ( rp(X,Y) % 24.40/24.52 & rp(Y,Z) ) % 24.40/24.52 => rp(X,Z) ) ). % 24.40/24.52 % 24.40/24.52 %----i2003_11_14_17_21_33997 % 24.40/24.52 fof(axiom_17,axiom, % 24.40/24.52 cUnsatisfiable(i2003_11_14_17_21_33997) ). % 24.40/24.52 % 24.40/24.52 %------------------------------------------------------------------------------ % 24.40/24.52 %------------------------------------------- % 24.40/24.52 % Proof found % 24.40/24.52 % SZS status Theorem for theBenchmark % 24.40/24.52 % SZS output start Proof % 24.40/24.52 %ClaNum:56(EqnAxiom:0) % 24.40/24.52 %VarNum:300(SingletonVarNum:107) % 24.40/24.52 %MaxLitNum:7 % 24.40/24.52 %MaxfuncDepth:1 % 24.40/24.52 %SharedTerms:2 % 24.40/24.52 [1]P1(a1) % 24.40/24.52 [2]~P2(x21) % 24.40/24.52 [3]P13(x31)+P12(x31) % 24.40/24.52 [4]~P1(x41)+P3(x41) % 24.40/24.52 [5]~P13(x51)+~P12(x51) % 24.40/24.52 [6]~P1(x61)+P4(f2(x61)) % 24.40/24.52 [7]P5(x71)+~P6(f9(x71)) % 24.40/24.52 [8]P6(x81)+~P7(f3(x81)) % 24.40/24.52 [9]P8(x91)+~P5(f4(x91)) % 24.40/24.52 [10]P7(x101)+~P11(f8(x101)) % 24.40/24.52 [11]P3(x111)+P14(x111,f10(x111)) % 24.40/24.52 [12]P5(x121)+P15(x121,f9(x121)) % 24.40/24.52 [13]P6(x131)+P16(x131,f3(x131)) % 24.40/24.52 [14]P8(x141)+P17(x141,f4(x141)) % 24.40/24.52 [15]P7(x151)+P18(x151,f8(x151)) % 24.40/24.52 [19]~P1(x191)+P20(x191,f2(x191)) % 24.40/24.52 [20]~P11(x201)+P14(x201,f11(x201)) % 24.40/24.52 [21]~P4(x211)+P19(x211,f12(x211)) % 24.40/24.52 [22]~P10(x221)+P19(x221,f5(x221)) % 24.40/24.52 [23]~P4(x231)+P17(x231,f13(x231)) % 24.40/24.52 [24]~P9(x241)+P17(x241,f6(x241)) % 24.40/24.52 [16]P11(x161)+~P14(x161,x162) % 24.40/24.52 [17]P9(x171)+~P17(x171,x172) % 24.40/24.52 [18]P10(x181)+~P19(x181,x182) % 24.40/24.52 [25]~P3(x251)+~P14(x251,x252) % 24.40/24.52 [34]~P18(x342,x341)+P20(x341,x342) % 24.40/24.52 [35]~P17(x352,x351)+P15(x351,x352) % 24.40/24.52 [36]~P16(x362,x361)+P19(x361,x362) % 24.40/24.52 [37]~P15(x372,x371)+P17(x371,x372) % 24.40/24.52 [38]~P20(x382,x381)+P18(x381,x382) % 24.40/24.52 [39]~P19(x392,x391)+P16(x391,x392) % 24.40/24.52 [26]~P18(x262,x261)+P11(x261)+~P7(x262) % 24.40/24.52 [27]~P17(x272,x271)+P5(x271)+~P4(x272) % 24.40/24.52 [28]~P17(x282,x281)+P5(x281)+~P8(x282) % 24.40/24.52 [29]~P15(x292,x291)+P6(x291)+~P5(x292) % 24.40/24.52 [30]~P19(x302,x301)+P9(x301)+~P4(x302) % 24.40/24.52 [31]~P19(x312,x311)+P8(x311)+~P4(x312) % 24.40/24.52 [32]~P19(x322,x321)+P10(x321)+~P4(x322) % 24.40/24.52 [33]~P16(x332,x331)+P7(x331)+~P6(x332) % 24.40/24.52 [40]~P19(x401,x403)+P19(x401,x402)+~P19(x403,x402) % 24.40/24.52 [41]P4(x411)+~P19(x411,x412)+~P17(x411,x413)+~P5(f14(x411))+~P9(f15(x411))+~P8(f16(x411))+~P10(f7(x411)) % 24.40/24.52 [42]P4(x421)+~P19(x421,x422)+~P17(x421,x423)+P19(x421,f15(x421))+~P5(f14(x421))+~P8(f16(x421))+~P10(f7(x421)) % 24.40/24.52 [43]P4(x431)+~P19(x431,x432)+~P17(x431,x433)+P19(x431,f16(x431))+~P5(f14(x431))+~P9(f15(x431))+~P10(f7(x431)) % 24.40/24.52 [44]P4(x441)+~P19(x441,x442)+~P17(x441,x443)+P19(x441,f7(x441))+~P5(f14(x441))+~P9(f15(x441))+~P8(f16(x441)) % 24.40/24.52 [45]P4(x451)+~P19(x451,x452)+~P17(x451,x453)+P17(x451,f14(x451))+~P9(f15(x451))+~P8(f16(x451))+~P10(f7(x451)) % 24.40/24.52 [46]P4(x461)+~P19(x461,x462)+~P17(x461,x463)+P19(x461,f15(x461))+P19(x461,f16(x461))+~P5(f14(x461))+~P10(f7(x461)) % 24.40/24.52 [47]P4(x471)+~P19(x471,x472)+~P17(x471,x473)+P19(x471,f15(x471))+P19(x471,f7(x471))+~P5(f14(x471))+~P8(f16(x471)) % 24.40/24.52 [48]P4(x481)+~P19(x481,x482)+~P17(x481,x483)+P19(x481,f15(x481))+P17(x481,f14(x481))+~P8(f16(x481))+~P10(f7(x481)) % 24.40/24.52 [49]P4(x491)+~P19(x491,x492)+~P17(x491,x493)+P19(x491,f16(x491))+P19(x491,f7(x491))+~P5(f14(x491))+~P9(f15(x491)) % 24.40/24.52 [50]P4(x501)+~P19(x501,x502)+~P17(x501,x503)+P19(x501,f16(x501))+P17(x501,f14(x501))+~P9(f15(x501))+~P10(f7(x501)) % 24.40/24.52 [51]P4(x511)+~P19(x511,x512)+~P17(x511,x513)+P19(x511,f7(x511))+P17(x511,f14(x511))+~P9(f15(x511))+~P8(f16(x511)) % 24.40/24.52 [52]P4(x521)+~P19(x521,x522)+~P17(x521,x523)+P19(x521,f15(x521))+P19(x521,f16(x521))+P19(x521,f7(x521))+~P5(f14(x521)) % 24.40/24.52 [53]P4(x531)+~P19(x531,x532)+~P17(x531,x533)+P19(x531,f15(x531))+P19(x531,f16(x531))+P17(x531,f14(x531))+~P10(f7(x531)) % 24.40/24.52 [54]P4(x541)+~P19(x541,x542)+~P17(x541,x543)+P19(x541,f15(x541))+P19(x541,f7(x541))+P17(x541,f14(x541))+~P8(f16(x541)) % 24.40/24.52 [55]P4(x551)+~P19(x551,x552)+~P17(x551,x553)+P19(x551,f16(x551))+P19(x551,f7(x551))+P17(x551,f14(x551))+~P9(f15(x551)) % 24.40/24.52 [56]P4(x561)+~P19(x561,x562)+~P17(x561,x563)+P19(x561,f15(x561))+P19(x561,f16(x561))+P19(x561,f7(x561))+P17(x561,f14(x561)) % 24.40/24.52 %EqnAxiom % 24.40/24.52 % 24.40/24.52 %------------------------------------------- % 24.40/24.52 cnf(58,plain, % 24.40/24.52 (~P14(a1,x581)), % 24.40/24.52 inference(scs_inference,[],[1,4,25])). % 24.40/24.52 cnf(60,plain, % 24.40/24.52 (~P14(a1,x601)), % 24.40/24.53 inference(rename_variables,[],[58])). % 24.40/24.53 cnf(65,plain, % 24.40/24.53 (~P7(x651)+~P18(x651,a1)), % 24.40/24.53 inference(scs_inference,[],[58,60,11,20,26])). % 24.40/24.53 cnf(67,plain, % 24.40/24.53 (~P6(x671)+~P18(x672,a1)+~P16(x671,x672)), % 24.40/24.53 inference(scs_inference,[],[58,60,11,20,26,33])). % 24.40/24.53 cnf(68,plain, % 24.40/24.53 (P19(f2(a1),f12(f2(a1)))), % 24.40/24.53 inference(scs_inference,[],[1,6,21])). % 24.40/24.53 cnf(73,plain, % 24.40/24.53 (~P18(x731,a1)+~P11(f8(x731))), % 24.40/24.53 inference(scs_inference,[],[10,65])). % 24.40/24.53 cnf(74,plain, % 24.40/24.53 (~P14(f8(x741),x742)+~P18(x741,a1)), % 24.40/24.53 inference(scs_inference,[],[16,73])). % 24.40/24.53 cnf(83,plain, % 24.40/24.53 (P18(f2(a1),a1)), % 24.40/24.53 inference(scs_inference,[],[1,19,38])). % 24.40/24.53 cnf(92,plain, % 24.40/24.53 (~P16(x921,f2(a1))+~P6(x921)), % 24.40/24.53 inference(scs_inference,[],[83,65,73,74,11,67])). % 24.40/24.53 cnf(130,plain, % 24.40/24.53 (~P4(f2(a1))+~P19(f2(a1),f12(f2(a1)))+P17(f12(f2(a1)),f6(f12(f2(a1))))), % 24.40/24.53 inference(scs_inference,[],[68,30,24])). % 24.40/24.53 cnf(131,plain, % 24.40/24.53 (P17(f12(f2(a1)),f6(f12(f2(a1))))+~P4(f2(a1))), % 24.40/24.53 inference(scs_inference,[],[68,130])). % 24.40/24.53 cnf(132,plain, % 24.40/24.53 (P8(f12(f2(a1)))), % 24.40/24.53 inference(scs_inference,[],[68,1,31,6])). % 24.40/24.53 cnf(282,plain, % 24.40/24.53 (P16(f12(x2821),x2821)+~P4(x2821)), % 24.40/24.53 inference(scs_inference,[],[21,39])). % 24.40/24.53 cnf(283,plain, % 24.40/24.53 (P16(f12(f2(a1)),f2(a1))), % 24.40/24.53 inference(scs_inference,[],[1,282,6])). % 24.40/24.53 cnf(284,plain, % 24.40/24.53 (~P6(f12(f2(a1)))), % 24.40/24.53 inference(scs_inference,[],[283,92])). % 24.40/24.53 cnf(1184,plain, % 24.40/24.53 (~P17(f12(f2(a1)),x11841)+~P15(x11841,f12(f2(a1)))), % 24.40/24.53 inference(scs_inference,[],[132,284,28,29])). % 24.40/24.53 cnf(1185,plain, % 24.40/24.53 (~P17(f12(f2(a1)),x11851)), % 24.40/24.53 inference(scs_inference,[],[1184,35])). % 24.40/24.53 cnf(1186,plain, % 24.40/24.53 (~P4(f2(a1))), % 24.40/24.53 inference(scs_inference,[],[1185,131])). % 24.40/24.53 cnf(1189,plain, % 24.40/24.53 ($false), % 24.40/24.53 inference(scs_inference,[],[1186,1,6]), % 24.40/24.53 ['proof']). % 24.40/24.53 % SZS output end Proof % 24.40/24.53 % Total time :23.940000s %------------------------------------------------------------------------------