%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS150+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:41 EDT 2024 % Result : Theorem 2.01s 2.12s % Output : CNFRefutation 2.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : KRS150+1 : TPTP v8.2.0. Released v3.1.0. % 0.05/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.30 % Computer : n025.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Wed Jun 19 14:05:09 EDT 2024 % 0.10/0.31 % CPUTime : % 0.48/0.54 start to proof:theBenchmark % 2.01/2.11 %------------------------------------------- % 2.01/2.11 % File :CSE---1.7 % 2.01/2.11 % Problem :theBenchmark % 2.01/2.11 % Transform :cnf % 2.01/2.11 % Format :tptp:raw % 2.01/2.11 % Command :java -jar mcs_scs.jar %d %s % 2.01/2.11 % 2.01/2.11 % Result :Theorem 1.520000s % 2.01/2.11 % Output :CNFRefutation 1.520000s % 2.01/2.11 %------------------------------------------- % 2.01/2.11 %------------------------------------------------------------------------------ % 2.01/2.11 % File : KRS150+1 : TPTP v8.2.0. Released v3.1.0. % 2.01/2.11 % Domain : Knowledge Representation (Semantic Web) % 2.01/2.11 % Problem : DL Test: k_lin ABox test from DL98 systems comparison % 2.01/2.11 % Version : Especial. % 2.01/2.11 % English : % 2.01/2.11 % 2.01/2.11 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 2.01/2.11 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 2.01/2.11 % Source : [Bec03] % 2.01/2.11 % Names : positive_description-logic-Manifest205 [Bec03] % 2.01/2.11 % 2.01/2.11 % Status : Theorem % 2.01/2.11 % 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.17 v5.2.0, 0.00 v3.2.0, 0.11 v3.1.0 % 2.01/2.11 % Syntax : Number of formulae : 25 ( 11 unt; 0 def) % 2.01/2.11 % Number of atoms : 59 ( 0 equ) % 2.01/2.11 % Maximal formula atoms : 13 ( 2 avg) % 2.01/2.11 % Number of connectives : 48 ( 14 ~; 0 |; 21 &) % 2.01/2.11 % ( 11 <=>; 2 =>; 0 <=; 0 <~>) % 2.01/2.11 % Maximal formula depth : 11 ( 3 avg) % 2.01/2.11 % Maximal term depth : 1 ( 1 avg) % 2.01/2.11 % Number of predicates : 16 ( 16 usr; 0 prp; 1-2 aty) % 2.01/2.11 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 2.01/2.11 % Number of variables : 19 ( 15 !; 4 ?) % 2.01/2.11 % SPC : FOF_THM_RFO_NEQ % 2.01/2.11 % 2.01/2.11 % Comments : Sean Bechhofer says there are some errors in the encoding of % 2.01/2.11 % datatypes, so this problem may not be perfect. At least it's % 2.01/2.11 % still representative of the type of reasoning required for OWL. % 2.01/2.11 %------------------------------------------------------------------------------ % 2.01/2.11 %----Thing and Nothing % 2.01/2.11 fof(axiom_0,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( cowlThing(X) % 2.01/2.11 & ~ cowlNothing(X) ) ). % 2.01/2.11 % 2.01/2.11 %----String and Integer disjoint % 2.01/2.11 fof(axiom_1,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( xsd_string(X) % 2.01/2.11 <=> ~ xsd_integer(X) ) ). % 2.01/2.11 % 2.01/2.11 %----Equality cC10 % 2.01/2.11 fof(axiom_2,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( cC10(X) % 2.01/2.11 <=> ? [Y] : % 2.01/2.11 ( rR1(X,Y) % 2.01/2.11 & ~ cC2(Y) ) ) ). % 2.01/2.11 % 2.01/2.11 %----Equality cC12 % 2.01/2.11 fof(axiom_3,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( cC12(X) % 2.01/2.11 <=> ( ~ cC2(X) % 2.01/2.11 & ~ cC10(X) ) ) ). % 2.01/2.11 % 2.01/2.11 %----Equality cC14 % 2.01/2.11 fof(axiom_4,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( cC14(X) % 2.01/2.11 <=> ? [Y] : % 2.01/2.11 ( rR1(X,Y) % 2.01/2.11 & cC12(Y) ) ) ). % 2.01/2.11 % 2.01/2.11 %----Equality cC16 % 2.01/2.11 fof(axiom_5,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( cC16(X) % 2.01/2.11 <=> ( cC14(X) % 2.01/2.11 & cC8(X) ) ) ). % 2.01/2.11 % 2.01/2.11 %----Equality cC18 % 2.01/2.11 fof(axiom_6,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( cC18(X) % 2.01/2.11 <=> ( cTOP(X) % 2.01/2.11 & cC16(X) ) ) ). % 2.01/2.11 % 2.01/2.11 %----Equality cC4 % 2.01/2.11 fof(axiom_7,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( cC4(X) % 2.01/2.11 <=> ? [Y] : % 2.01/2.11 ( rR1(X,Y) % 2.01/2.11 & ~ cC2(Y) ) ) ). % 2.01/2.11 % 2.01/2.11 %----Equality cC6 % 2.01/2.11 fof(axiom_8,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( cC6(X) % 2.01/2.11 <=> ( ~ cC2(X) % 2.01/2.11 & ~ cC4(X) ) ) ). % 2.01/2.11 % 2.01/2.11 %----Equality cC8 % 2.01/2.11 fof(axiom_9,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( cC8(X) % 2.01/2.11 <=> ? [Y] : % 2.01/2.11 ( rR1(X,Y) % 2.01/2.11 & cC6(Y) ) ) ). % 2.01/2.11 % 2.01/2.11 %----Equality cTEST % 2.01/2.11 fof(axiom_10,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( cTEST(X) % 2.01/2.11 <=> ( cC18(X) % 2.01/2.11 & cTOP(X) ) ) ). % 2.01/2.11 % 2.01/2.11 %----iV16560 % 2.01/2.11 fof(axiom_11,axiom, % 2.01/2.11 cTOP(iV16560) ). % 2.01/2.11 % 2.01/2.11 %----iV16560 % 2.01/2.11 fof(axiom_12,axiom, % 2.01/2.11 cTEST(iV16560) ). % 2.01/2.11 % 2.01/2.11 %----iV16560 % 2.01/2.11 fof(axiom_13,axiom, % 2.01/2.11 cowlThing(iV16560) ). % 2.01/2.11 % 2.01/2.11 fof(axiom_14,axiom, % 2.01/2.11 rR1(iV16560,iV16562) ). % 2.01/2.11 % 2.01/2.11 fof(axiom_15,axiom, % 2.01/2.11 rR1(iV16560,iV16561) ). % 2.01/2.11 % 2.01/2.11 %----iV16561 % 2.01/2.11 fof(axiom_16,axiom, % 2.01/2.11 ~ cC4(iV16561) ). % 2.01/2.11 % 2.01/2.11 %----iV16561 % 2.01/2.11 fof(axiom_17,axiom, % 2.01/2.11 cowlThing(iV16561) ). % 2.01/2.11 % 2.01/2.11 %----iV16561 % 2.01/2.11 fof(axiom_18,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( rR1(iV16561,X) % 2.01/2.11 => cC2(X) ) ). % 2.01/2.11 % 2.01/2.11 %----iV16561 % 2.01/2.11 fof(axiom_19,axiom, % 2.01/2.11 ~ cC2(iV16561) ). % 2.01/2.11 % 2.01/2.11 %----iV16562 % 2.01/2.11 fof(axiom_20,axiom, % 2.01/2.11 ~ cC10(iV16562) ). % 2.01/2.11 % 2.01/2.11 %----iV16562 % 2.01/2.11 fof(axiom_21,axiom, % 2.01/2.11 ~ cC2(iV16562) ). % 2.01/2.11 % 2.01/2.11 %----iV16562 % 2.01/2.11 fof(axiom_22,axiom, % 2.01/2.11 cowlThing(iV16562) ). % 2.01/2.11 % 2.01/2.11 %----iV16562 % 2.01/2.11 fof(axiom_23,axiom, % 2.01/2.11 ! [X] : % 2.01/2.11 ( rR1(iV16562,X) % 2.01/2.11 => cC2(X) ) ). % 2.01/2.11 % 2.01/2.11 %----Thing and Nothing % 2.01/2.11 %----String and Integer disjoint % 2.01/2.11 %----iV16560 % 2.01/2.11 %----iV16560 % 2.01/2.11 %----iV16560 % 2.01/2.11 %----iV16560 % 2.01/2.12 %----iV16560 % 2.01/2.12 %----iV16561 % 2.01/2.12 %----iV16561 % 2.01/2.12 %----iV16562 % 2.01/2.12 %----iV16562 % 2.01/2.12 fof(the_axiom,conjecture, % 2.01/2.12 ( ! [X] : % 2.01/2.12 ( cowlThing(X) % 2.01/2.12 & ~ cowlNothing(X) ) % 2.01/2.12 & ! [X] : % 2.01/2.12 ( xsd_string(X) % 2.01/2.12 <=> ~ xsd_integer(X) ) % 2.01/2.12 & cC18(iV16560) % 2.01/2.12 & cC16(iV16560) % 2.01/2.12 & cowlThing(iV16560) % 2.01/2.12 & cC14(iV16560) % 2.01/2.12 & cC8(iV16560) % 2.01/2.12 & cowlThing(iV16561) % 2.01/2.12 & cC6(iV16561) % 2.01/2.12 & cowlThing(iV16562) % 2.01/2.12 & cC12(iV16562) ) ). % 2.01/2.12 % 2.01/2.12 %------------------------------------------------------------------------------ % 2.01/2.12 %------------------------------------------- % 2.01/2.12 % Proof found % 2.01/2.12 % SZS status Theorem for theBenchmark % 2.01/2.12 % SZS output start Proof % 2.01/2.12 %ClaNum:42(EqnAxiom:0) % 2.01/2.12 %VarNum:80(SingletonVarNum:36) % 2.01/2.12 %MaxLitNum:9 % 2.01/2.12 %MaxfuncDepth:1 % 2.01/2.12 %SharedTerms:24 % 2.01/2.12 %goalClause: 41 42 % 2.01/2.12 [1]P1(a1) % 2.01/2.12 [2]P2(a1) % 2.01/2.12 [3]P12(a1,a8) % 2.01/2.12 [4]P12(a1,a9) % 2.01/2.12 [5]~P3(a8) % 2.01/2.12 [6]~P4(a8) % 2.01/2.12 [7]~P4(a9) % 2.01/2.12 [8]~P9(a9) % 2.01/2.12 [9]~P13(x91) % 2.01/2.12 [10]P15(x101)+P14(x101) % 2.01/2.12 [11]~P7(x111)+P5(x111) % 2.01/2.12 [12]~P8(x121)+P7(x121) % 2.05/2.12 [13]~P7(x131)+P10(x131) % 2.05/2.12 [14]~P2(x141)+P8(x141) % 2.05/2.12 [15]~P8(x151)+P1(x151) % 2.05/2.12 [16]~P2(x161)+P1(x161) % 2.05/2.12 [19]~P15(x191)+~P14(x191) % 2.05/2.12 [20]~P6(x201)+~P3(x201) % 2.05/2.12 [21]~P6(x211)+~P4(x211) % 2.05/2.12 [22]~P11(x221)+~P4(x221) % 2.05/2.12 [23]~P11(x231)+~P9(x231) % 2.05/2.12 [31]P4(x311)+~P12(a8,x311) % 2.05/2.12 [32]P4(x321)+~P12(a9,x321) % 2.05/2.12 [24]~P5(x241)+P6(f2(x241)) % 2.05/2.12 [25]~P10(x251)+P11(f4(x251)) % 2.05/2.12 [29]~P3(x291)+~P4(f3(x291)) % 2.05/2.12 [30]~P9(x301)+~P4(f5(x301)) % 2.05/2.12 [33]~P3(x331)+P12(x331,f3(x331)) % 2.05/2.12 [34]~P5(x341)+P12(x341,f2(x341)) % 2.05/2.12 [35]~P9(x351)+P12(x351,f5(x351)) % 2.05/2.12 [36]~P10(x361)+P12(x361,f4(x361)) % 2.05/2.12 [17]P4(x171)+P6(x171)+P3(x171) % 2.05/2.12 [18]P9(x181)+P11(x181)+P4(x181) % 2.05/2.12 [26]~P5(x261)+~P10(x261)+P7(x261) % 2.05/2.12 [27]~P7(x271)+~P1(x271)+P8(x271) % 2.05/2.12 [28]~P8(x281)+~P1(x281)+P2(x281) % 2.05/2.12 [37]~P12(x371,x372)+P3(x371)+P4(x372) % 2.05/2.12 [38]~P12(x382,x381)+P4(x381)+P9(x382) % 2.05/2.12 [39]~P12(x391,x392)+P5(x391)+~P6(x392) % 2.05/2.12 [40]~P12(x401,x402)+P10(x401)+~P11(x402) % 2.05/2.12 [41]P13(a6)+P14(a7)+~P15(a7)+~P6(a8)+~P5(a1)+~P7(a1)+~P10(a1)+~P8(a1)+~P11(a9) % 2.05/2.12 [42]P13(a6)+P15(a7)+~P14(a7)+~P6(a8)+~P5(a1)+~P7(a1)+~P10(a1)+~P8(a1)+~P11(a9) % 2.05/2.12 %EqnAxiom % 2.05/2.12 % 2.05/2.12 %------------------------------------------- % 2.05/2.12 cnf(50,plain, % 2.05/2.12 (~P7(a1)+~P15(a7)+~P6(a8)+~P5(a1)+P14(a7)+~P10(a1)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[1,9,6,5,8,37,38,27,41])). % 2.05/2.12 cnf(51,plain, % 2.05/2.12 (P15(a7)+~P14(a7)+~P6(a8)+~P5(a1)+~P7(a1)+~P10(a1)+~P8(a1)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[9,42])). % 2.05/2.12 cnf(230,plain, % 2.05/2.12 (P10(x2301)+~P8(x2301)), % 2.05/2.12 inference(scs_inference,[],[12,13])). % 2.05/2.12 cnf(291,plain, % 2.05/2.12 (P10(a1)), % 2.05/2.12 inference(scs_inference,[],[2,14,230])). % 2.05/2.12 cnf(292,plain, % 2.05/2.12 (~P7(a1)+~P15(a7)+~P6(a8)+~P5(a1)+P14(a7)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[291,50])). % 2.05/2.12 cnf(293,plain, % 2.05/2.12 (P15(a7)+~P14(a7)+~P6(a8)+~P5(a1)+~P7(a1)+~P8(a1)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[291,51])). % 2.05/2.12 cnf(298,plain, % 2.05/2.12 (P7(a1)+~P5(a1)), % 2.05/2.12 inference(scs_inference,[],[291,6,5,8,37,38,26])). % 2.05/2.12 cnf(300,plain, % 2.05/2.12 (P8(a1)+~P5(a1)), % 2.05/2.12 inference(scs_inference,[],[1,291,6,5,8,37,38,26,27])). % 2.05/2.12 cnf(302,plain, % 2.05/2.12 (~P5(a1)+~P6(a8)+~P15(a7)+P14(a7)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[1,291,6,5,8,37,38,26,27,292])). % 2.05/2.12 cnf(3280,plain, % 2.05/2.12 (P5(x32801)+~P8(x32801)), % 2.05/2.12 inference(scs_inference,[],[11,12])). % 2.05/2.12 cnf(3341,plain, % 2.05/2.12 (P5(a1)), % 2.05/2.12 inference(scs_inference,[],[2,3280,14])). % 2.05/2.12 cnf(3342,plain, % 2.05/2.12 (P15(a7)+~P14(a7)+~P6(a8)+~P7(a1)+~P8(a1)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[3341,293])). % 2.05/2.12 cnf(3343,plain, % 2.05/2.12 (P7(a1)), % 2.05/2.12 inference(scs_inference,[],[3341,298])). % 2.05/2.12 cnf(3344,plain, % 2.05/2.12 (P8(a1)), % 2.05/2.12 inference(scs_inference,[],[3341,300])). % 2.05/2.12 cnf(3345,plain, % 2.05/2.12 (~P6(a8)+~P15(a7)+P14(a7)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[3341,302])). % 2.05/2.12 cnf(3358,plain, % 2.05/2.12 (P15(a7)+~P14(a7)+~P6(a8)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[3343,3344,3342])). % 2.05/2.12 cnf(3919,plain, % 2.05/2.12 (~P6(a8)+~P15(a7)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[19,3345])). % 2.05/2.12 cnf(3980,plain, % 2.05/2.12 (~P15(a7)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[5,6,3919,17])). % 2.05/2.12 cnf(4041,plain, % 2.05/2.12 (P14(a7)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[3980,10])). % 2.05/2.12 cnf(4102,plain, % 2.05/2.12 (P15(a7)+~P6(a8)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[4041,3358])). % 2.05/2.12 cnf(4163,plain, % 2.05/2.12 (~P14(a7)+~P6(a8)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[4102,19])). % 2.05/2.12 cnf(4224,plain, % 2.05/2.12 (~P6(a8)+~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[4163,4041])). % 2.05/2.12 cnf(4285,plain, % 2.05/2.12 (~P11(a9)), % 2.05/2.12 inference(scs_inference,[],[5,6,4224,17])). % 2.05/2.12 cnf(4286,plain, % 2.05/2.12 ($false), % 2.05/2.12 inference(scs_inference,[],[4285,7,8,18]), % 2.05/2.12 ['proof']). % 2.05/2.12 % SZS output end Proof % 2.05/2.12 % Total time :1.520000s %------------------------------------------------------------------------------