%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS158+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.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:43 EDT 2024 % Result : Theorem 1.77s 1.89s % Output : CNFRefutation 1.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS158+1 : TPTP v8.2.0. Released v3.1.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n022.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Jun 19 13:46:53 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 1.77/1.87 %------------------------------------------- % 1.77/1.87 % File :CSE---1.7 % 1.77/1.87 % Problem :theBenchmark % 1.77/1.87 % Transform :cnf % 1.77/1.87 % Format :tptp:raw % 1.77/1.87 % Command :java -jar mcs_scs.jar %d %s % 1.77/1.87 % 1.77/1.87 % Result :Theorem 1.260000s % 1.77/1.87 % Output :CNFRefutation 1.260000s % 1.77/1.87 %------------------------------------------- % 1.77/1.88 %------------------------------------------------------------------------------ % 1.77/1.88 % File : KRS158+1 : TPTP v8.2.0. Released v3.1.0. % 1.77/1.88 % Domain : Knowledge Representation (Semantic Web) % 1.77/1.88 % Problem : DL Test: k_lin ABox test from DL98 systems comparison % 1.77/1.88 % Version : Especial. % 1.77/1.88 % English : % 1.77/1.88 % 1.77/1.88 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 1.77/1.88 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 1.77/1.88 % Source : [Bec03] % 1.77/1.88 % Names : positive_description-logic-Manifest665 [Bec03] % 1.77/1.88 % 1.77/1.88 % Status : Theorem % 1.77/1.88 % Rating : 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.04 v5.4.0, 0.09 v5.3.0, 0.22 v5.2.0, 0.00 v3.2.0, 0.11 v3.1.0 % 1.77/1.88 % Syntax : Number of formulae : 31 ( 11 unt; 0 def) % 1.77/1.88 % Number of atoms : 71 ( 0 equ) % 1.77/1.88 % Maximal formula atoms : 13 ( 2 avg) % 1.77/1.88 % Number of connectives : 47 ( 7 ~; 0 |; 21 &) % 1.77/1.88 % ( 17 <=>; 2 =>; 0 <=; 0 <~>) % 1.77/1.88 % Maximal formula depth : 11 ( 3 avg) % 1.77/1.88 % Maximal term depth : 1 ( 1 avg) % 1.77/1.88 % Number of predicates : 22 ( 22 usr; 0 prp; 1-2 aty) % 1.77/1.88 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 1.77/1.88 % Number of variables : 31 ( 21 !; 10 ?) % 1.77/1.88 % SPC : FOF_THM_RFO_NEQ % 1.77/1.88 % 1.77/1.88 % Comments : Sean Bechhofer says there are some errors in the encoding of % 1.77/1.88 % datatypes, so this problem may not be perfect. At least it's % 1.77/1.88 % still representative of the type of reasoning required for OWL. % 1.77/1.88 %------------------------------------------------------------------------------ % 1.77/1.88 %----Thing and Nothing % 1.77/1.88 fof(axiom_0,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cowlThing(X) % 1.77/1.88 & ~ cowlNothing(X) ) ). % 1.77/1.88 % 1.77/1.88 %----String and Integer disjoint % 1.77/1.88 fof(axiom_1,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( xsd_string(X) % 1.77/1.88 <=> ~ xsd_integer(X) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC10 % 1.77/1.88 fof(axiom_2,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC10(X) % 1.77/1.88 <=> ? [Y0] : ra_Px3(X,Y0) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC10 % 1.77/1.88 fof(axiom_3,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC10(X) % 1.77/1.88 <=> ? [Y] : % 1.77/1.88 ( rR1(X,Y) % 1.77/1.88 & cC2xcomp(Y) ) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC10xcomp % 1.77/1.88 fof(axiom_4,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC10xcomp(X) % 1.77/1.88 <=> ~ ? [Y] : ra_Px3(X,Y) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC12 % 1.77/1.88 fof(axiom_5,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC12(X) % 1.77/1.88 <=> ( cC10xcomp(X) % 1.77/1.88 & cC2xcomp(X) ) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC14 % 1.77/1.88 fof(axiom_6,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC14(X) % 1.77/1.88 <=> ? [Y] : % 1.77/1.88 ( rR1(X,Y) % 1.77/1.88 & cC12(Y) ) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC16 % 1.77/1.88 fof(axiom_7,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC16(X) % 1.77/1.88 <=> ( cC14(X) % 1.77/1.88 & cC8(X) ) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC18 % 1.77/1.88 fof(axiom_8,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC18(X) % 1.77/1.88 <=> ( cTOP(X) % 1.77/1.88 & cC16(X) ) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC2 % 1.77/1.88 fof(axiom_9,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC2(X) % 1.77/1.88 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC2xcomp % 1.77/1.88 fof(axiom_10,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC2xcomp(X) % 1.77/1.88 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC4 % 1.77/1.88 fof(axiom_11,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC4(X) % 1.77/1.88 <=> ? [Y0] : ra_Px6(X,Y0) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC4 % 1.77/1.88 fof(axiom_12,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC4(X) % 1.77/1.88 <=> ? [Y] : % 1.77/1.88 ( rR1(X,Y) % 1.77/1.88 & cC2xcomp(Y) ) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC4xcomp % 1.77/1.88 fof(axiom_13,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC4xcomp(X) % 1.77/1.88 <=> ~ ? [Y] : ra_Px6(X,Y) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC6 % 1.77/1.88 fof(axiom_14,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC6(X) % 1.77/1.88 <=> ( cC4xcomp(X) % 1.77/1.88 & cC2xcomp(X) ) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cC8 % 1.77/1.88 fof(axiom_15,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cC8(X) % 1.77/1.88 <=> ? [Y] : % 1.77/1.88 ( rR1(X,Y) % 1.77/1.88 & cC6(Y) ) ) ). % 1.77/1.88 % 1.77/1.88 %----Equality cTEST % 1.77/1.88 fof(axiom_16,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( cTEST(X) % 1.77/1.88 <=> ( cTOP(X) % 1.77/1.88 & cC18(X) ) ) ). % 1.77/1.88 % 1.77/1.88 %----iV16560 % 1.77/1.88 fof(axiom_17,axiom, % 1.77/1.88 cowlThing(iV16560) ). % 1.77/1.88 % 1.77/1.88 %----iV16560 % 1.77/1.88 fof(axiom_18,axiom, % 1.77/1.88 cTEST(iV16560) ). % 1.77/1.88 % 1.77/1.88 %----iV16560 % 1.77/1.88 fof(axiom_19,axiom, % 1.77/1.88 cTOP(iV16560) ). % 1.77/1.88 % 1.77/1.88 fof(axiom_20,axiom, % 1.77/1.88 rR1(iV16560,iV16562) ). % 1.77/1.88 % 1.77/1.88 fof(axiom_21,axiom, % 1.77/1.88 rR1(iV16560,iV16561) ). % 1.77/1.88 % 1.77/1.88 %----iV16561 % 1.77/1.88 fof(axiom_22,axiom, % 1.77/1.88 cowlThing(iV16561) ). % 1.77/1.88 % 1.77/1.88 %----iV16561 % 1.77/1.88 fof(axiom_23,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( rR1(iV16561,X) % 1.77/1.88 => cC2(X) ) ). % 1.77/1.88 % 1.77/1.88 %----iV16561 % 1.77/1.88 fof(axiom_24,axiom, % 1.77/1.88 cC4xcomp(iV16561) ). % 1.77/1.88 % 1.77/1.88 %----iV16561 % 1.77/1.88 fof(axiom_25,axiom, % 1.77/1.88 cC2xcomp(iV16561) ). % 1.77/1.88 % 1.77/1.88 %----iV16562 % 1.77/1.88 fof(axiom_26,axiom, % 1.77/1.88 cowlThing(iV16562) ). % 1.77/1.88 % 1.77/1.88 %----iV16562 % 1.77/1.88 fof(axiom_27,axiom, % 1.77/1.88 ! [X] : % 1.77/1.88 ( rR1(iV16562,X) % 1.77/1.88 => cC2(X) ) ). % 1.77/1.88 % 1.77/1.88 %----iV16562 % 1.77/1.88 fof(axiom_28,axiom, % 1.77/1.88 cC10xcomp(iV16562) ). % 1.77/1.88 % 1.77/1.88 %----iV16562 % 1.77/1.88 fof(axiom_29,axiom, % 1.77/1.88 cC2xcomp(iV16562) ). % 1.77/1.88 % 1.77/1.88 %----Thing and Nothing % 1.77/1.88 %----String and Integer disjoint % 1.77/1.88 %----iV16560 % 1.77/1.88 %----iV16560 % 1.77/1.88 %----iV16560 % 1.77/1.88 %----iV16560 % 1.77/1.88 %----iV16560 % 1.77/1.88 %----iV16561 % 1.77/1.88 %----iV16561 % 1.77/1.88 %----iV16562 % 1.77/1.88 %----iV16562 % 1.77/1.88 fof(the_axiom,conjecture, % 1.77/1.88 ( ! [X] : % 1.77/1.88 ( cowlThing(X) % 1.77/1.88 & ~ cowlNothing(X) ) % 1.77/1.88 & ! [X] : % 1.77/1.88 ( xsd_string(X) % 1.77/1.88 <=> ~ xsd_integer(X) ) % 1.77/1.88 & cC18(iV16560) % 1.77/1.88 & cC14(iV16560) % 1.77/1.88 & cC8(iV16560) % 1.77/1.88 & cC16(iV16560) % 1.77/1.88 & cowlThing(iV16560) % 1.77/1.88 & cC6(iV16561) % 1.77/1.88 & cowlThing(iV16561) % 1.77/1.88 & cC12(iV16562) % 1.77/1.89 & cowlThing(iV16562) ) ). % 1.77/1.89 % 1.77/1.89 %------------------------------------------------------------------------------ % 1.77/1.89 %------------------------------------------- % 1.77/1.89 % Proof found % 1.77/1.89 % SZS status Theorem for theBenchmark % 1.77/1.89 % SZS output start Proof % 1.77/1.89 %ClaNum:54(EqnAxiom:0) % 1.77/1.89 %VarNum:116(SingletonVarNum:54) % 1.77/1.89 %MaxLitNum:9 % 1.77/1.89 %MaxfuncDepth:1 % 1.77/1.89 %SharedTerms:24 % 1.77/1.89 %goalClause: 53 54 % 1.77/1.89 [1]P1(a1) % 1.77/1.89 [2]P1(a2) % 1.77/1.89 [3]P2(a1) % 1.77/1.89 [4]P9(a3) % 1.77/1.89 [5]P10(a2) % 1.77/1.89 [6]P12(a3) % 1.77/1.89 [7]P15(a3,a1) % 1.77/1.89 [8]P15(a3,a2) % 1.77/1.89 [9]~P16(x91) % 1.77/1.89 [10]P18(x101)+P17(x101) % 1.77/1.89 [11]~P4(x111)+P1(x111) % 1.77/1.89 [12]~P13(x121)+P1(x121) % 1.77/1.89 [13]~P4(x131)+P2(x131) % 1.77/1.89 [14]~P6(x141)+P5(x141) % 1.77/1.89 [15]~P7(x151)+P6(x151) % 1.77/1.89 [16]~P6(x161)+P14(x161) % 1.77/1.89 [17]~P12(x171)+P7(x171) % 1.77/1.89 [18]~P7(x181)+P9(x181) % 1.77/1.89 [19]~P12(x191)+P9(x191) % 1.77/1.89 [20]~P13(x201)+P10(x201) % 1.77/1.89 [21]~P18(x211)+~P17(x211) % 1.77/1.89 [31]P8(x311)+~P15(a1,x311) % 1.77/1.89 [32]P8(x321)+~P15(a2,x321) % 1.77/1.89 [22]~P3(x221)+P1(f4(x221)) % 1.77/1.89 [23]~P11(x231)+P1(f9(x231)) % 1.77/1.89 [24]~P5(x241)+P4(f10(x241)) % 1.77/1.89 [25]~P14(x251)+P13(f5(x251)) % 1.77/1.89 [33]P2(x331)+P19(x331,f11(x331)) % 1.77/1.89 [34]P8(x341)+P20(x341,f12(x341)) % 1.77/1.89 [35]P10(x351)+P21(x351,f15(x351)) % 1.77/1.89 [39]~P3(x391)+P19(x391,f6(x391)) % 1.77/1.89 [40]~P3(x401)+P15(x401,f4(x401)) % 1.77/1.89 [41]~P5(x411)+P15(x411,f10(x411)) % 1.77/1.89 [42]~P11(x421)+P15(x421,f9(x421)) % 1.77/1.89 [43]~P14(x431)+P15(x431,f5(x431)) % 1.77/1.89 [44]~P1(x441)+P20(x441,f13(x441)) % 1.77/1.89 [45]~P11(x451)+P21(x451,f14(x451)) % 1.77/1.89 [36]P3(x361)+~P19(x361,x362) % 1.77/1.89 [37]P1(x371)+~P20(x371,x372) % 1.77/1.89 [38]P11(x381)+~P21(x381,x382) % 1.77/1.89 [46]~P2(x461)+~P19(x461,x462) % 1.77/1.89 [47]~P8(x471)+~P20(x471,x472) % 1.77/1.89 [48]~P10(x481)+~P21(x481,x482) % 1.77/1.89 [26]~P1(x261)+~P2(x261)+P4(x261) % 1.77/1.89 [27]~P5(x271)+~P14(x271)+P6(x271) % 1.77/1.89 [28]~P6(x281)+~P9(x281)+P7(x281) % 1.77/1.89 [29]~P1(x291)+~P10(x291)+P13(x291) % 1.77/1.89 [30]~P7(x301)+~P9(x301)+P12(x301) % 1.77/1.89 [49]~P15(x491,x492)+P3(x491)+~P1(x492) % 1.77/1.89 [50]~P15(x501,x502)+P5(x501)+~P4(x502) % 1.77/1.89 [51]~P15(x511,x512)+P14(x511)+~P13(x512) % 1.77/1.89 [52]~P15(x521,x522)+P11(x521)+~P1(x522) % 1.77/1.89 [53]P16(a7)+P17(a8)+~P18(a8)+~P4(a1)+~P5(a3)+~P6(a3)+~P14(a3)+~P7(a3)+~P13(a2) % 1.77/1.89 [54]P16(a7)+P18(a8)+~P17(a8)+~P4(a1)+~P5(a3)+~P6(a3)+~P14(a3)+~P7(a3)+~P13(a2) % 1.77/1.89 %EqnAxiom % 1.77/1.89 % 1.77/1.89 %------------------------------------------- % 1.77/1.89 cnf(59,plain, % 1.77/1.89 (P4(a1)), % 1.77/1.89 inference(scs_inference,[],[1,3,5,46,48,26])). % 1.77/1.89 cnf(61,plain, % 1.77/1.89 (P13(a2)), % 1.77/1.89 inference(scs_inference,[],[1,2,3,5,46,48,26,29])). % 1.77/1.89 cnf(63,plain, % 1.77/1.89 (~P3(a1)), % 1.77/1.89 inference(scs_inference,[],[1,2,3,5,46,48,26,29,39])). % 1.77/1.89 cnf(65,plain, % 1.77/1.89 (~P11(a2)), % 1.77/1.89 inference(scs_inference,[],[1,2,3,5,46,48,26,29,39,45])). % 1.77/1.89 cnf(76,plain, % 1.77/1.89 (P17(a8)+~P18(a8)+~P5(a3)+~P6(a3)+~P14(a3)+~P7(a3)), % 1.77/1.89 inference(scs_inference,[],[9,59,61,53])). % 1.77/1.89 cnf(77,plain, % 1.77/1.89 (P18(a8)+~P17(a8)+~P5(a3)+~P6(a3)+~P14(a3)+~P7(a3)), % 1.77/1.89 inference(scs_inference,[],[9,59,61,54])). % 1.77/1.89 cnf(434,plain, % 1.77/1.89 (P14(x4341)+~P7(x4341)), % 1.77/1.89 inference(scs_inference,[],[15,16])). % 1.77/1.89 cnf(495,plain, % 1.77/1.89 (P14(a3)), % 1.77/1.89 inference(scs_inference,[],[6,17,434])). % 1.77/1.89 cnf(496,plain, % 1.77/1.89 (P17(a8)+~P18(a8)+~P5(a3)+~P6(a3)+~P7(a3)), % 1.77/1.89 inference(scs_inference,[],[495,76])). % 1.77/1.89 cnf(497,plain, % 1.77/1.89 (P18(a8)+~P17(a8)+~P5(a3)+~P6(a3)+~P7(a3)), % 1.77/1.89 inference(scs_inference,[],[495,77])). % 1.77/1.89 cnf(504,plain, % 1.77/1.89 (P7(a3)+~P5(a3)), % 1.77/1.89 inference(scs_inference,[],[1,495,4,63,65,52,49,27,28])). % 1.77/1.89 cnf(924,plain, % 1.77/1.89 (P7(a3)), % 1.77/1.89 inference(scs_inference,[],[59,7,504,50])). % 1.77/1.89 cnf(925,plain, % 1.77/1.89 (P17(a8)+~P18(a8)+~P5(a3)+~P6(a3)), % 1.77/1.89 inference(scs_inference,[],[924,496])). % 1.77/1.89 cnf(926,plain, % 1.77/1.89 (P18(a8)+~P17(a8)+~P5(a3)+~P6(a3)), % 1.77/1.89 inference(scs_inference,[],[924,497])). % 1.77/1.89 cnf(3656,plain, % 1.77/1.89 (P18(a8)+~P5(a3)+~P6(a3)), % 1.77/1.89 inference(scs_inference,[],[10,926])). % 1.77/1.89 cnf(3717,plain, % 1.77/1.89 (~P17(a8)+~P5(a3)+~P6(a3)), % 1.77/1.89 inference(scs_inference,[],[3656,21])). % 1.77/1.89 cnf(3778,plain, % 1.77/1.89 (~P18(a8)+~P5(a3)+~P6(a3)), % 1.77/1.89 inference(scs_inference,[],[3717,925])). % 1.77/1.89 cnf(3839,plain, % 1.77/1.89 (P17(a8)+~P5(a3)+~P6(a3)), % 1.77/1.89 inference(scs_inference,[],[3778,10])). % 1.77/1.89 cnf(3900,plain, % 1.77/1.89 (~P5(a3)+~P6(a3)), % 1.77/1.89 inference(scs_inference,[],[3839,3717])). % 1.77/1.89 cnf(3961,plain, % 1.77/1.89 (~P6(a3)), % 1.77/1.89 inference(scs_inference,[],[59,7,3900,50])). % 1.77/1.89 cnf(3963,plain, % 1.77/1.89 ($false), % 1.77/1.89 inference(scs_inference,[],[3961,924,15]), % 1.77/1.89 ['proof']). % 1.77/1.89 % SZS output end Proof % 1.77/1.89 % Total time :1.260000s %------------------------------------------------------------------------------