%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS127+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 : n019.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:36 EDT 2024 % Result : Unsatisfiable 0.57s 0.66s % Output : CNFRefutation 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : KRS127+1 : TPTP v8.2.0. Released v3.1.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n019.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Wed Jun 19 12:31:54 EDT 2024 % 0.13/0.35 % CPUTime : % 0.46/0.60 start to proof:theBenchmark % 0.57/0.65 %------------------------------------------- % 0.57/0.65 % File :CSE---1.7 % 0.57/0.65 % Problem :theBenchmark % 0.57/0.65 % Transform :cnf % 0.57/0.65 % Format :tptp:raw % 0.57/0.65 % Command :java -jar mcs_scs.jar %d %s % 0.57/0.65 % 0.57/0.65 % Result :Theorem 0.010000s % 0.57/0.65 % Output :CNFRefutation 0.010000s % 0.57/0.65 %------------------------------------------- % 0.57/0.65 %------------------------------------------------------------------------------ % 0.57/0.65 % File : KRS127+1 : TPTP v8.2.0. Released v3.1.0. % 0.57/0.65 % Domain : Knowledge Representation (Semantic Web) % 0.57/0.65 % Problem : DL Test: heinsohn2.2 % 0.57/0.65 % Version : Especial. % 0.57/0.65 % English : Tbox tests from [HK+94] % 0.57/0.65 % 0.57/0.65 % Refs : [HK+94] Heinsohn et al. (1994), An Empirical Analysis of Termi % 0.57/0.65 % : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 0.57/0.65 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 0.57/0.65 % Source : [Bec03] % 0.57/0.65 % Names : inconsistent_description-logic-Manifest646 [Bec03] % 0.57/0.65 % 0.57/0.65 % Status : Unsatisfiable % 0.57/0.65 % Rating : 0.00 v3.1.0 % 0.57/0.65 % Syntax : Number of formulae : 19 ( 1 unt; 0 def) % 0.57/0.65 % Number of atoms : 55 ( 13 equ) % 0.57/0.65 % Maximal formula atoms : 8 ( 2 avg) % 0.57/0.65 % Number of connectives : 39 ( 3 ~; 0 |; 18 &) % 0.57/0.65 % ( 4 <=>; 14 =>; 0 <=; 0 <~>) % 0.57/0.65 % Maximal formula depth : 9 ( 5 avg) % 0.57/0.65 % Maximal term depth : 1 ( 1 avg) % 0.57/0.65 % Number of predicates : 11 ( 10 usr; 0 prp; 1-2 aty) % 0.57/0.65 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 0.57/0.65 % Number of variables : 40 ( 36 !; 4 ?) % 0.57/0.65 % SPC : FOF_UNS_RFO_SEQ % 0.57/0.65 % 0.57/0.65 % Comments : Sean Bechhofer says there are some errors in the encoding of % 0.57/0.65 % datatypes, so this problem may not be perfect. At least it's % 0.57/0.65 % still representative of the type of reasoning required for OWL. % 0.57/0.65 % : Tests incoherency caused by number restrictions % 0.57/0.65 %------------------------------------------------------------------------------ % 0.57/0.65 fof(cUnsatisfiable_substitution_1,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( ( A = B % 0.57/0.65 & cUnsatisfiable(A) ) % 0.57/0.65 => cUnsatisfiable(B) ) ). % 0.57/0.65 % 0.57/0.65 fof(cc_substitution_1,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( ( A = B % 0.57/0.65 & cc(A) ) % 0.57/0.65 => cc(B) ) ). % 0.57/0.65 % 0.57/0.65 fof(cd_substitution_1,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( ( A = B % 0.57/0.65 & cd(A) ) % 0.57/0.65 => cd(B) ) ). % 0.57/0.65 % 0.57/0.65 fof(cdxcomp_substitution_1,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( ( A = B % 0.57/0.66 & cdxcomp(A) ) % 0.57/0.66 => cdxcomp(B) ) ). % 0.57/0.66 % 0.57/0.66 fof(cowlNothing_substitution_1,axiom, % 0.57/0.66 ! [A,B] : % 0.57/0.66 ( ( A = B % 0.57/0.66 & cowlNothing(A) ) % 0.57/0.66 => cowlNothing(B) ) ). % 0.57/0.66 % 0.57/0.66 fof(cowlThing_substitution_1,axiom, % 0.57/0.66 ! [A,B] : % 0.57/0.66 ( ( A = B % 0.57/0.66 & cowlThing(A) ) % 0.57/0.66 => cowlThing(B) ) ). % 0.57/0.66 % 0.57/0.66 fof(ra_Px1_substitution_1,axiom, % 0.57/0.66 ! [A,B,C] : % 0.57/0.66 ( ( A = B % 0.57/0.66 & ra_Px1(A,C) ) % 0.57/0.66 => ra_Px1(B,C) ) ). % 0.57/0.66 % 0.57/0.66 fof(ra_Px1_substitution_2,axiom, % 0.57/0.66 ! [A,B,C] : % 0.57/0.66 ( ( A = B % 0.57/0.66 & ra_Px1(C,A) ) % 0.57/0.66 => ra_Px1(C,B) ) ). % 0.57/0.66 % 0.57/0.66 fof(rr_substitution_1,axiom, % 0.57/0.66 ! [A,B,C] : % 0.57/0.66 ( ( A = B % 0.57/0.66 & rr(A,C) ) % 0.57/0.66 => rr(B,C) ) ). % 0.57/0.66 % 0.57/0.66 fof(rr_substitution_2,axiom, % 0.57/0.66 ! [A,B,C] : % 0.57/0.66 ( ( A = B % 0.57/0.66 & rr(C,A) ) % 0.57/0.66 => rr(C,B) ) ). % 0.57/0.66 % 0.57/0.66 fof(xsd_integer_substitution_1,axiom, % 0.57/0.66 ! [A,B] : % 0.57/0.66 ( ( A = B % 0.57/0.66 & xsd_integer(A) ) % 0.57/0.66 => xsd_integer(B) ) ). % 0.57/0.66 % 0.57/0.66 fof(xsd_string_substitution_1,axiom, % 0.57/0.66 ! [A,B] : % 0.57/0.66 ( ( A = B % 0.57/0.66 & xsd_string(A) ) % 0.57/0.66 => xsd_string(B) ) ). % 0.57/0.66 % 0.57/0.66 %----Thing and Nothing % 0.57/0.66 fof(axiom_0,axiom, % 0.57/0.66 ! [X] : % 0.57/0.66 ( cowlThing(X) % 0.57/0.66 & ~ cowlNothing(X) ) ). % 0.57/0.66 % 0.57/0.66 %----String and Integer disjoint % 0.57/0.66 fof(axiom_1,axiom, % 0.57/0.66 ! [X] : % 0.57/0.66 ( xsd_string(X) % 0.57/0.66 <=> ~ xsd_integer(X) ) ). % 0.57/0.66 % 0.57/0.66 %----Equality cUnsatisfiable % 0.57/0.66 fof(axiom_2,axiom, % 0.57/0.66 ! [X] : % 0.57/0.66 ( cUnsatisfiable(X) % 0.57/0.66 <=> ( ? [Y] : % 0.57/0.66 ( rr(X,Y) % 0.57/0.66 & cc(Y) ) % 0.57/0.66 & ? [Y] : % 0.57/0.66 ( rr(X,Y) % 0.57/0.66 & cd(Y) ) % 0.57/0.66 & ! [Y0,Y1] : % 0.57/0.66 ( ( rr(X,Y0) % 0.57/0.66 & rr(X,Y1) ) % 0.57/0.66 => Y0 = Y1 ) ) ) ). % 0.57/0.66 % 0.57/0.66 %----Super cc % 0.57/0.66 fof(axiom_3,axiom, % 0.57/0.66 ! [X] : % 0.57/0.66 ( cc(X) % 0.57/0.66 => cdxcomp(X) ) ). % 0.57/0.66 % 0.57/0.66 %----Equality cd % 0.57/0.66 fof(axiom_4,axiom, % 0.57/0.66 ! [X] : % 0.57/0.66 ( cd(X) % 0.57/0.66 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 0.57/0.66 % 0.57/0.66 %----Equality cdxcomp % 0.57/0.66 fof(axiom_5,axiom, % 0.57/0.66 ! [X] : % 0.57/0.66 ( cdxcomp(X) % 0.57/0.66 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 0.57/0.66 % 0.57/0.66 %----i2003_11_14_17_22_27794 % 0.57/0.66 fof(axiom_6,axiom, % 0.57/0.66 cUnsatisfiable(i2003_11_14_17_22_27794) ). % 0.57/0.66 % 0.57/0.66 %------------------------------------------------------------------------------ % 0.57/0.66 %------------------------------------------- % 0.57/0.66 % Proof found % 0.57/0.66 % SZS status Theorem for theBenchmark % 0.57/0.66 % SZS output start Proof % 0.57/0.66 %ClaNum:37(EqnAxiom:20) % 0.57/0.66 %VarNum:63(SingletonVarNum:26) % 0.57/0.66 %MaxLitNum:6 % 0.57/0.66 %MaxfuncDepth:1 % 0.57/0.66 %SharedTerms:2 % 0.57/0.66 [21]P1(a1) % 0.57/0.66 [22]~P2(x221) % 0.57/0.66 [23]P9(x231)+P6(x231) % 0.57/0.66 [24]~P4(x241)+P3(x241) % 0.57/0.66 [25]~P9(x251)+~P6(x251) % 0.57/0.66 [26]~P1(x261)+P4(f2(x261)) % 0.57/0.66 [27]~P1(x271)+P5(f3(x271)) % 0.57/0.66 [28]P5(x281)+P7(x281,f4(x281)) % 0.57/0.66 [30]~P3(x301)+P7(x301,f7(x301)) % 0.57/0.66 [31]~P1(x311)+P8(x311,f2(x311)) % 0.57/0.66 [32]~P1(x321)+P8(x321,f3(x321)) % 0.57/0.66 [29]P3(x291)+~P7(x291,x292) % 0.57/0.66 [33]~P5(x331)+~P7(x331,x332) % 0.57/0.66 [34]~P8(x343,x342)+~P8(x343,x341)+E(x341,x342)+~P1(x343) % 0.57/0.66 [35]~P8(x351,x353)+~P8(x351,x352)+P1(x351)+~P4(x352)+~P5(x353)+~E(f5(x351),f6(x351)) % 0.57/0.66 [36]~P8(x361,x363)+~P8(x361,x362)+P1(x361)+~P4(x362)+~P5(x363)+P8(x361,f6(x361)) % 0.57/0.66 [37]~P8(x371,x373)+~P8(x371,x372)+P1(x371)+~P4(x372)+~P5(x373)+P8(x371,f5(x371)) % 0.57/0.66 %EqnAxiom % 0.57/0.66 [1]E(x11,x11) % 0.57/0.66 [2]E(x22,x21)+~E(x21,x22) % 0.57/0.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.57/0.66 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.57/0.66 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 0.57/0.66 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 0.57/0.66 [7]~E(x71,x72)+E(f7(x71),f7(x72)) % 0.57/0.66 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 0.57/0.66 [9]~E(x91,x92)+E(f6(x91),f6(x92)) % 0.57/0.66 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 0.57/0.66 [11]~P2(x111)+P2(x112)+~E(x111,x112) % 0.57/0.66 [12]~P6(x121)+P6(x122)+~E(x121,x122) % 0.57/0.66 [13]~P9(x131)+P9(x132)+~E(x131,x132) % 0.57/0.66 [14]~P3(x141)+P3(x142)+~E(x141,x142) % 0.57/0.66 [15]~P4(x151)+P4(x152)+~E(x151,x152) % 0.57/0.66 [16]~P5(x161)+P5(x162)+~E(x161,x162) % 0.57/0.66 [17]P8(x172,x173)+~E(x171,x172)+~P8(x171,x173) % 0.57/0.66 [18]P8(x183,x182)+~E(x181,x182)+~P8(x183,x181) % 0.57/0.66 [19]P7(x192,x193)+~E(x191,x192)+~P7(x191,x193) % 0.57/0.66 [20]P7(x203,x202)+~E(x201,x202)+~P7(x203,x201) % 0.57/0.66 % 0.57/0.66 %------------------------------------------- % 0.57/0.66 cnf(39,plain, % 0.57/0.66 (~P4(x391)+P7(x391,f7(x391))), % 0.57/0.66 inference(scs_inference,[],[24,30])). % 0.57/0.66 cnf(40,plain, % 0.57/0.66 (~E(a1,x401)+P4(f2(x401))), % 0.57/0.66 inference(scs_inference,[],[21,26,10])). % 0.57/0.66 cnf(41,plain, % 0.57/0.66 (P4(f2(a1))), % 0.57/0.66 inference(equality_inference,[],[40])). % 0.57/0.66 cnf(42,plain, % 0.57/0.66 (~E(a1,x421)+P5(f3(x421))), % 0.57/0.66 inference(scs_inference,[],[21,27,10])). % 0.57/0.66 cnf(43,plain, % 0.57/0.66 (P5(f3(a1))), % 0.57/0.66 inference(equality_inference,[],[42])). % 0.57/0.66 cnf(46,plain, % 0.57/0.66 (~P4(f3(a1))), % 0.57/0.66 inference(scs_inference,[],[43,33,39])). % 0.57/0.66 cnf(56,plain, % 0.57/0.66 (~E(a1,x561)+P8(x561,f2(x561))), % 0.57/0.66 inference(scs_inference,[],[21,31,10])). % 0.57/0.66 cnf(57,plain, % 0.57/0.66 (P8(a1,f2(a1))), % 0.57/0.66 inference(equality_inference,[],[56])). % 0.57/0.66 cnf(62,plain, % 0.57/0.66 (~E(a1,x621)+P8(x621,f3(x621))), % 0.57/0.66 inference(scs_inference,[],[21,32,10])). % 0.57/0.66 cnf(63,plain, % 0.57/0.66 (P8(a1,f3(a1))), % 0.57/0.66 inference(equality_inference,[],[62])). % 0.57/0.66 cnf(77,plain, % 0.57/0.66 (~E(f3(a1),f2(a1))), % 0.57/0.66 inference(scs_inference,[],[41,46,15,2])). % 0.57/0.66 cnf(78,plain, % 0.57/0.66 ($false), % 0.57/0.66 inference(scs_inference,[],[57,63,77,21,34]), % 0.57/0.66 ['proof']). % 0.57/0.66 % SZS output end Proof % 0.57/0.66 % Total time :0.010000s %------------------------------------------------------------------------------