%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS160+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 : n014.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:44 EDT 2024 % Result : Theorem 0.53s 0.66s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS160+1 : TPTP v8.2.0. Released v3.1.0. % 0.11/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jun 19 12:30:54 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 0.53/0.64 %------------------------------------------- % 0.53/0.64 % File :CSE---1.7 % 0.53/0.64 % Problem :theBenchmark % 0.53/0.64 % Transform :cnf % 0.53/0.64 % Format :tptp:raw % 0.53/0.64 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.64 % 0.53/0.64 % Result :Theorem 0.040000s % 0.53/0.64 % Output :CNFRefutation 0.040000s % 0.53/0.65 %------------------------------------------- % 0.53/0.65 %------------------------------------------------------------------------------ % 0.53/0.65 % File : KRS160+1 : TPTP v8.2.0. Released v3.1.0. % 0.53/0.65 % Domain : Knowledge Representation (Semantic Web) % 0.53/0.65 % Problem : DL Test: k_ph ABox test from DL98 systems comparison % 0.53/0.65 % Version : Especial. % 0.53/0.65 % English : % 0.53/0.65 % 0.53/0.65 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 0.53/0.65 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 0.53/0.65 % Source : [Bec03] % 0.53/0.65 % Names : positive_description-logic-Manifest667 [Bec03] % 0.53/0.65 % 0.53/0.65 % Status : Theorem % 0.53/0.65 % Rating : 0.00 v6.0.0, 0.25 v5.5.0, 0.00 v5.4.0, 0.04 v5.3.0, 0.13 v5.2.0, 0.00 v3.2.0, 0.11 v3.1.0 % 0.53/0.65 % Syntax : Number of formulae : 23 ( 8 unt; 0 def) % 0.53/0.65 % Number of atoms : 49 ( 0 equ) % 0.53/0.65 % Maximal formula atoms : 8 ( 2 avg) % 0.53/0.65 % Number of connectives : 33 ( 7 ~; 0 |; 12 &) % 0.53/0.65 % ( 13 <=>; 1 =>; 0 <=; 0 <~>) % 0.53/0.65 % Maximal formula depth : 6 ( 3 avg) % 0.53/0.65 % Maximal term depth : 1 ( 1 avg) % 0.53/0.65 % Number of predicates : 18 ( 18 usr; 0 prp; 1-2 aty) % 0.53/0.65 % Number of functors : 2 ( 2 usr; 2 con; 0-0 aty) % 0.53/0.65 % Number of variables : 24 ( 16 !; 8 ?) % 0.53/0.65 % SPC : FOF_THM_RFO_NEQ % 0.53/0.65 % 0.53/0.65 % Comments : Sean Bechhofer says there are some errors in the encoding of % 0.53/0.65 % datatypes, so this problem may not be perfect. At least it's % 0.53/0.65 % still representative of the type of reasoning required for OWL. % 0.53/0.65 %------------------------------------------------------------------------------ % 0.53/0.65 %----Thing and Nothing % 0.53/0.65 fof(axiom_0,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cowlThing(X) % 0.53/0.65 & ~ cowlNothing(X) ) ). % 0.53/0.65 % 0.53/0.65 %----String and Integer disjoint % 0.53/0.65 fof(axiom_1,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( xsd_string(X) % 0.53/0.65 <=> ~ xsd_integer(X) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cC10 % 0.53/0.65 fof(axiom_2,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cC10(X) % 0.53/0.65 <=> ( cC4(X) % 0.53/0.65 & cC2(X) ) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cC12 % 0.53/0.65 fof(axiom_3,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cC12(X) % 0.53/0.65 <=> ? [Y] : % 0.53/0.65 ( rR1(X,Y) % 0.53/0.65 & cC10(Y) ) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cC2 % 0.53/0.65 fof(axiom_4,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cC2(X) % 0.53/0.65 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cC2xcomp % 0.53/0.65 fof(axiom_5,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cC2xcomp(X) % 0.53/0.65 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cC6 % 0.53/0.65 fof(axiom_6,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cC6(X) % 0.53/0.65 <=> ( cC2xcomp(X) % 0.53/0.65 & cC4(X) ) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cC6 % 0.53/0.65 fof(axiom_7,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cC6(X) % 0.53/0.65 <=> ~ ? [Y] : ra_Px4(X,Y) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cC6xcomp % 0.53/0.65 fof(axiom_8,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cC6xcomp(X) % 0.53/0.65 <=> ? [Y0] : ra_Px4(X,Y0) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cC8 % 0.53/0.65 fof(axiom_9,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cC8(X) % 0.53/0.65 <=> ? [Y0] : ra_Px2(X,Y0) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cC8 % 0.53/0.65 fof(axiom_10,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cC8(X) % 0.53/0.65 <=> ? [Y] : % 0.53/0.65 ( rR1(X,Y) % 0.53/0.65 & cC6(Y) ) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cC8xcomp % 0.53/0.65 fof(axiom_11,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cC8xcomp(X) % 0.53/0.65 <=> ~ ? [Y] : ra_Px2(X,Y) ) ). % 0.53/0.65 % 0.53/0.65 %----Equality cTEST % 0.53/0.65 fof(axiom_12,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cTEST(X) % 0.53/0.65 <=> ( cC8xcomp(X) % 0.53/0.65 & cC12(X) ) ) ). % 0.53/0.65 % 0.53/0.65 %----iV21080 % 0.53/0.65 fof(axiom_13,axiom, % 0.53/0.65 cTEST(iV21080) ). % 0.53/0.65 % 0.53/0.65 %----iV21080 % 0.53/0.65 fof(axiom_14,axiom, % 0.53/0.65 cC8xcomp(iV21080) ). % 0.53/0.65 % 0.53/0.65 %----iV21080 % 0.53/0.65 fof(axiom_15,axiom, % 0.53/0.65 cowlThing(iV21080) ). % 0.53/0.65 % 0.53/0.65 %----iV21080 % 0.53/0.65 fof(axiom_16,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( rR1(iV21080,X) % 0.53/0.65 => cC6xcomp(X) ) ). % 0.53/0.65 % 0.53/0.65 fof(axiom_17,axiom, % 0.53/0.65 rR1(iV21080,iV21081) ). % 0.53/0.65 % 0.53/0.65 %----iV21081 % 0.53/0.65 fof(axiom_18,axiom, % 0.53/0.65 cC4(iV21081) ). % 0.53/0.65 % 0.53/0.65 %----iV21081 % 0.53/0.65 fof(axiom_19,axiom, % 0.53/0.66 cC6xcomp(iV21081) ). % 0.53/0.66 % 0.53/0.66 %----iV21081 % 0.53/0.66 fof(axiom_20,axiom, % 0.53/0.66 cC2(iV21081) ). % 0.53/0.66 % 0.53/0.66 %----iV21081 % 0.53/0.66 fof(axiom_21,axiom, % 0.53/0.66 cowlThing(iV21081) ). % 0.53/0.66 % 0.53/0.66 %----Thing and Nothing % 0.53/0.66 %----String and Integer disjoint % 0.53/0.66 %----iV21080 % 0.53/0.66 %----iV21080 % 0.53/0.66 %----iV21081 % 0.53/0.66 %----iV21081 % 0.53/0.66 fof(the_axiom,conjecture, % 0.53/0.66 ( ! [X] : % 0.53/0.66 ( cowlThing(X) % 0.53/0.66 & ~ cowlNothing(X) ) % 0.53/0.66 & ! [X] : % 0.53/0.66 ( xsd_string(X) % 0.53/0.66 <=> ~ xsd_integer(X) ) % 0.53/0.66 & cowlThing(iV21080) % 0.53/0.66 & cC12(iV21080) % 0.53/0.66 & cC10(iV21081) % 0.53/0.66 & cowlThing(iV21081) ) ). % 0.53/0.66 % 0.53/0.66 %------------------------------------------------------------------------------ % 0.53/0.66 %------------------------------------------- % 0.53/0.66 % Proof found % 0.53/0.66 % SZS status Theorem for theBenchmark % 0.53/0.66 % SZS output start Proof % 0.53/0.66 %ClaNum:39(EqnAxiom:0) % 0.53/0.66 %VarNum:82(SingletonVarNum:39) % 0.53/0.66 %MaxLitNum:5 % 0.53/0.66 %MaxfuncDepth:1 % 0.53/0.66 %SharedTerms:17 % 0.53/0.66 %goalClause: 21 22 % 0.53/0.66 [1]P1(a1) % 0.53/0.66 [2]P2(a1) % 0.53/0.66 [3]P6(a1) % 0.53/0.66 [4]P8(a2) % 0.53/0.66 [5]P10(a2) % 0.53/0.66 [6]P11(a2,a1) % 0.53/0.66 [7]~P12(x71) % 0.53/0.66 [8]P14(x81)+P13(x81) % 0.53/0.66 [9]~P3(x91)+P1(x91) % 0.53/0.66 [10]~P7(x101)+P1(x101) % 0.53/0.66 [11]~P3(x111)+P2(x111) % 0.53/0.66 [12]~P10(x121)+P4(x121) % 0.53/0.66 [13]~P7(x131)+P5(x131) % 0.53/0.66 [14]~P10(x141)+P8(x141) % 0.53/0.66 [15]~P14(x151)+~P13(x151) % 0.53/0.66 [23]P6(x231)+~P11(a2,x231) % 0.53/0.66 [16]~P4(x161)+P3(f3(x161)) % 0.53/0.66 [17]~P9(x171)+P7(f6(x171)) % 0.53/0.66 [24]P2(x241)+P15(x241,f7(x241)) % 0.53/0.66 [25]P7(x251)+P16(x251,f8(x251)) % 0.53/0.66 [26]P8(x261)+P17(x261,f12(x261)) % 0.53/0.66 [30]~P4(x301)+P11(x301,f3(x301)) % 0.53/0.66 [31]~P9(x311)+P11(x311,f6(x311)) % 0.53/0.66 [32]~P5(x321)+P15(x321,f9(x321)) % 0.53/0.66 [33]~P6(x331)+P16(x331,f10(x331)) % 0.53/0.66 [34]~P9(x341)+P17(x341,f11(x341)) % 0.53/0.66 [27]P5(x271)+~P15(x271,x272) % 0.53/0.66 [28]P6(x281)+~P16(x281,x282) % 0.53/0.66 [29]P9(x291)+~P17(x291,x292) % 0.53/0.66 [35]~P2(x351)+~P15(x351,x352) % 0.53/0.66 [36]~P7(x361)+~P16(x361,x362) % 0.53/0.66 [37]~P8(x371)+~P17(x371,x372) % 0.53/0.66 [18]~P1(x181)+~P2(x181)+P3(x181) % 0.53/0.66 [19]~P1(x191)+~P5(x191)+P7(x191) % 0.53/0.66 [20]~P4(x201)+~P8(x201)+P10(x201) % 0.53/0.66 [38]~P11(x381,x382)+P4(x381)+~P3(x382) % 0.53/0.66 [39]~P11(x391,x392)+P9(x391)+~P7(x392) % 0.53/0.66 [21]P12(a4)+P13(a5)+~P14(a5)+~P3(a1)+~P4(a2) % 0.53/0.66 [22]P12(a4)+P14(a5)+~P13(a5)+~P3(a1)+~P4(a2) % 0.53/0.66 %EqnAxiom % 0.53/0.66 % 0.53/0.66 %------------------------------------------- % 0.53/0.66 cnf(48,plain, % 0.53/0.66 (P3(a1)), % 0.53/0.66 inference(scs_inference,[],[1,2,4,35,32,37,34,18])). % 0.53/0.66 cnf(55,plain, % 0.53/0.66 (P13(a5)+~P14(a5)+~P4(a2)), % 0.53/0.66 inference(scs_inference,[],[7,48,21])). % 0.53/0.66 cnf(56,plain, % 0.53/0.66 (P14(a5)+~P13(a5)+~P4(a2)), % 0.53/0.66 inference(scs_inference,[],[7,48,22])). % 0.53/0.66 cnf(80,plain, % 0.53/0.66 (~P14(a5)+~P4(a2)), % 0.53/0.66 inference(scs_inference,[],[55,15])). % 0.53/0.66 cnf(81,plain, % 0.53/0.66 (P13(a5)+~P4(a2)), % 0.53/0.66 inference(scs_inference,[],[80,8])). % 0.53/0.66 cnf(82,plain, % 0.53/0.66 (P14(a5)+~P4(a2)), % 0.53/0.66 inference(scs_inference,[],[81,56])). % 0.53/0.66 cnf(83,plain, % 0.53/0.66 (~P13(a5)+~P4(a2)), % 0.53/0.66 inference(scs_inference,[],[82,15])). % 0.53/0.66 cnf(84,plain, % 0.53/0.66 (~P4(a2)), % 0.53/0.66 inference(scs_inference,[],[83,81])). % 0.53/0.66 cnf(85,plain, % 0.53/0.66 ($false), % 0.53/0.66 inference(scs_inference,[],[84,5,12]), % 0.53/0.66 ['proof']). % 0.53/0.66 % SZS output end Proof % 0.53/0.66 % Total time :0.040000s %------------------------------------------------------------------------------