%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS095+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 : n027.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:28 EDT 2024 % Result : Unsatisfiable 0.21s 0.63s % Output : CNFRefutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : KRS095+1 : TPTP v8.2.0. Released v3.1.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n027.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:09:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.21/0.57 start to proof:theBenchmark % 0.21/0.62 %------------------------------------------- % 0.21/0.62 % File :CSE---1.7 % 0.21/0.62 % Problem :theBenchmark % 0.21/0.62 % Transform :cnf % 0.21/0.62 % Format :tptp:raw % 0.21/0.62 % Command :java -jar mcs_scs.jar %d %s % 0.21/0.62 % 0.21/0.62 % Result :Theorem 0.020000s % 0.21/0.62 % Output :CNFRefutation 0.020000s % 0.21/0.62 %------------------------------------------- % 0.21/0.63 %------------------------------------------------------------------------------ % 0.21/0.63 % File : KRS095+1 : TPTP v8.2.0. Released v3.1.0. % 0.21/0.63 % Domain : Knowledge Representation (Semantic Web) % 0.21/0.63 % Problem : DL Test: heinsohn2.1 % 0.21/0.63 % Version : Especial. % 0.21/0.63 % English : Tbox tests from [HK+94] % 0.21/0.63 % 0.21/0.63 % Refs : [HK+94] Heinsohn et al. (1994), An Empirical Analysis of Termi % 0.21/0.63 % : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 0.21/0.63 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 0.21/0.63 % Source : [Bec03] % 0.21/0.63 % Names : inconsistent_description-logic-Manifest105 [Bec03] % 0.21/0.63 % 0.21/0.63 % Status : Unsatisfiable % 0.21/0.63 % Rating : 0.00 v3.1.0 % 0.21/0.63 % Syntax : Number of formulae : 14 ( 1 unt; 0 def) % 0.21/0.63 % Number of atoms : 41 ( 11 equ) % 0.21/0.63 % Maximal formula atoms : 7 ( 2 avg) % 0.21/0.63 % Number of connectives : 31 ( 4 ~; 0 |; 14 &) % 0.21/0.63 % ( 2 <=>; 11 =>; 0 <=; 0 <~>) % 0.21/0.63 % Maximal formula depth : 9 ( 5 avg) % 0.21/0.63 % Maximal term depth : 1 ( 1 avg) % 0.21/0.63 % Number of predicates : 9 ( 8 usr; 0 prp; 1-2 aty) % 0.21/0.63 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 0.21/0.63 % Number of variables : 28 ( 26 !; 2 ?) % 0.21/0.63 % SPC : FOF_UNS_RFO_SEQ % 0.21/0.63 % 0.21/0.63 % Comments : Sean Bechhofer says there are some errors in the encoding of % 0.21/0.63 % datatypes, so this problem may not be perfect. At least it's % 0.21/0.63 % still representative of the type of reasoning required for OWL. % 0.21/0.63 % : Tests incoherency caused by number restrictions % 0.21/0.63 %------------------------------------------------------------------------------ % 0.21/0.63 fof(cUnsatisfiable_substitution_1,axiom, % 0.21/0.63 ! [A,B] : % 0.21/0.63 ( ( A = B % 0.21/0.63 & cUnsatisfiable(A) ) % 0.21/0.63 => cUnsatisfiable(B) ) ). % 0.21/0.63 % 0.21/0.63 fof(cc_substitution_1,axiom, % 0.21/0.63 ! [A,B] : % 0.21/0.63 ( ( A = B % 0.21/0.63 & cc(A) ) % 0.21/0.63 => cc(B) ) ). % 0.21/0.63 % 0.21/0.63 fof(cd_substitution_1,axiom, % 0.21/0.63 ! [A,B] : % 0.21/0.63 ( ( A = B % 0.21/0.63 & cd(A) ) % 0.21/0.63 => cd(B) ) ). % 0.21/0.63 % 0.21/0.63 fof(cowlNothing_substitution_1,axiom, % 0.21/0.63 ! [A,B] : % 0.21/0.63 ( ( A = B % 0.21/0.63 & cowlNothing(A) ) % 0.21/0.63 => cowlNothing(B) ) ). % 0.21/0.63 % 0.21/0.63 fof(cowlThing_substitution_1,axiom, % 0.21/0.63 ! [A,B] : % 0.21/0.63 ( ( A = B % 0.21/0.63 & cowlThing(A) ) % 0.21/0.63 => cowlThing(B) ) ). % 0.21/0.63 % 0.21/0.63 fof(rr_substitution_1,axiom, % 0.21/0.63 ! [A,B,C] : % 0.21/0.63 ( ( A = B % 0.21/0.63 & rr(A,C) ) % 0.21/0.63 => rr(B,C) ) ). % 0.21/0.63 % 0.21/0.63 fof(rr_substitution_2,axiom, % 0.21/0.63 ! [A,B,C] : % 0.21/0.63 ( ( A = B % 0.21/0.63 & rr(C,A) ) % 0.21/0.63 => rr(C,B) ) ). % 0.21/0.63 % 0.21/0.63 fof(xsd_integer_substitution_1,axiom, % 0.21/0.63 ! [A,B] : % 0.21/0.63 ( ( A = B % 0.21/0.63 & xsd_integer(A) ) % 0.21/0.63 => xsd_integer(B) ) ). % 0.21/0.63 % 0.21/0.63 fof(xsd_string_substitution_1,axiom, % 0.21/0.63 ! [A,B] : % 0.21/0.63 ( ( A = B % 0.21/0.63 & xsd_string(A) ) % 0.21/0.63 => xsd_string(B) ) ). % 0.21/0.63 % 0.21/0.63 %----Thing and Nothing % 0.21/0.63 fof(axiom_0,axiom, % 0.21/0.63 ! [X] : % 0.21/0.63 ( cowlThing(X) % 0.21/0.63 & ~ cowlNothing(X) ) ). % 0.21/0.63 % 0.21/0.63 %----String and Integer disjoint % 0.21/0.63 fof(axiom_1,axiom, % 0.21/0.63 ! [X] : % 0.21/0.63 ( xsd_string(X) % 0.21/0.63 <=> ~ xsd_integer(X) ) ). % 0.21/0.63 % 0.21/0.63 %----Equality cUnsatisfiable % 0.21/0.63 fof(axiom_2,axiom, % 0.21/0.63 ! [X] : % 0.21/0.63 ( cUnsatisfiable(X) % 0.21/0.63 <=> ( ? [Y0,Y1] : % 0.21/0.63 ( rr(X,Y0) % 0.21/0.63 & rr(X,Y1) % 0.21/0.63 & Y0 != Y1 ) % 0.21/0.63 & ! [Y0,Y1] : % 0.21/0.63 ( ( rr(X,Y0) % 0.21/0.63 & rr(X,Y1) ) % 0.21/0.63 => Y0 = Y1 ) ) ) ). % 0.21/0.63 % 0.21/0.63 %----Super cc % 0.21/0.63 fof(axiom_3,axiom, % 0.21/0.63 ! [X] : % 0.21/0.63 ( cc(X) % 0.21/0.63 => ~ cd(X) ) ). % 0.21/0.63 % 0.21/0.63 %----i2003_11_14_17_20_14253 % 0.21/0.63 fof(axiom_4,axiom, % 0.21/0.63 cUnsatisfiable(i2003_11_14_17_20_14253) ). % 0.21/0.63 % 0.21/0.63 %------------------------------------------------------------------------------ % 0.21/0.63 %------------------------------------------- % 0.21/0.63 % Proof found % 0.21/0.63 % SZS status Theorem for theBenchmark % 0.21/0.63 % SZS output start Proof % 0.21/0.63 %ClaNum:27(EqnAxiom:15) % 0.21/0.63 %VarNum:50(SingletonVarNum:19) % 0.21/0.63 %MaxLitNum:5 % 0.21/0.63 %MaxfuncDepth:1 % 0.21/0.63 %SharedTerms:2 % 0.21/0.63 [16]P1(a1) % 0.21/0.63 [17]~P2(x171) % 0.21/0.63 [18]P7(x181)+P5(x181) % 0.21/0.63 [19]~P4(x191)+~P3(x191) % 0.21/0.63 [20]~P7(x201)+~P5(x201) % 0.21/0.63 [21]~P1(x211)+~E(f2(x211),f3(x211)) % 0.21/0.63 [22]~P1(x221)+P6(x221,f3(x221)) % 0.21/0.63 [23]~P1(x231)+P6(x231,f2(x231)) % 0.21/0.63 [24]~P6(x243,x242)+~P6(x243,x241)+E(x241,x242)+~P1(x243) % 0.21/0.63 [25]~P6(x253,x252)+~P6(x253,x251)+E(x251,x252)+P1(x253)+~E(f4(x253),f5(x253)) % 0.21/0.63 [26]~P6(x263,x262)+~P6(x263,x261)+E(x261,x262)+P1(x263)+P6(x263,f5(x263)) % 0.21/0.63 [27]~P6(x273,x272)+~P6(x273,x271)+E(x271,x272)+P1(x273)+P6(x273,f4(x273)) % 0.21/0.63 %EqnAxiom % 0.21/0.63 [1]E(x11,x11) % 0.21/0.63 [2]E(x22,x21)+~E(x21,x22) % 0.21/0.63 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.21/0.63 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.21/0.63 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 0.21/0.63 [6]~E(x61,x62)+E(f5(x61),f5(x62)) % 0.21/0.63 [7]~E(x71,x72)+E(f4(x71),f4(x72)) % 0.21/0.63 [8]~P1(x81)+P1(x82)+~E(x81,x82) % 0.21/0.63 [9]~P2(x91)+P2(x92)+~E(x91,x92) % 0.21/0.63 [10]~P5(x101)+P5(x102)+~E(x101,x102) % 0.21/0.63 [11]~P7(x111)+P7(x112)+~E(x111,x112) % 0.21/0.63 [12]~P3(x121)+P3(x122)+~E(x121,x122) % 0.21/0.63 [13]~P4(x131)+P4(x132)+~E(x131,x132) % 0.21/0.63 [14]P6(x142,x143)+~E(x141,x142)+~P6(x141,x143) % 0.21/0.63 [15]P6(x153,x152)+~E(x151,x152)+~P6(x153,x151) % 0.21/0.63 % 0.21/0.63 %------------------------------------------- % 0.21/0.63 cnf(33,plain, % 0.21/0.63 (~E(a1,x331)+P6(x331,f3(x331))), % 0.21/0.63 inference(scs_inference,[],[16,22,8])). % 0.21/0.63 cnf(34,plain, % 0.21/0.63 (P6(a1,f3(a1))), % 0.21/0.63 inference(equality_inference,[],[33])). % 0.21/0.63 cnf(39,plain, % 0.21/0.63 (~E(a1,x391)+P6(x391,f2(x391))), % 0.21/0.63 inference(scs_inference,[],[16,23,8])). % 0.21/0.63 cnf(40,plain, % 0.21/0.63 (P6(a1,f2(a1))), % 0.21/0.63 inference(equality_inference,[],[39])). % 0.21/0.63 cnf(45,plain, % 0.21/0.63 (~E(a1,x451)+~E(f2(x451),f3(x451))), % 0.21/0.63 inference(scs_inference,[],[16,21,8])). % 0.21/0.63 cnf(51,plain, % 0.21/0.63 ($false), % 0.21/0.63 inference(scs_inference,[],[16,34,40,45,24]), % 0.21/0.64 ['proof']). % 0.21/0.64 % SZS output end Proof % 0.21/0.64 % Total time :0.020000s %------------------------------------------------------------------------------