%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS077+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 : n012.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:25 EDT 2024 % Result : Unsatisfiable 0.53s 0.66s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : KRS077+1 : TPTP v8.2.0. Released v3.1.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n012.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jun 19 13:37:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 0.53/0.65 %------------------------------------------- % 0.53/0.65 % File :CSE---1.7 % 0.53/0.65 % Problem :theBenchmark % 0.53/0.65 % Transform :cnf % 0.53/0.65 % Format :tptp:raw % 0.53/0.65 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.65 % 0.53/0.65 % Result :Theorem 0.010000s % 0.53/0.65 % Output :CNFRefutation 0.010000s % 0.53/0.65 %------------------------------------------- % 0.53/0.65 %------------------------------------------------------------------------------ % 0.53/0.65 % File : KRS077+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: t11.1 % 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 : inconsistent_description-logic-Manifest014 [Bec03] % 0.53/0.65 % 0.53/0.65 % Status : Unsatisfiable % 0.53/0.65 % Rating : 0.00 v3.1.0 % 0.53/0.65 % Syntax : Number of formulae : 18 ( 1 unt; 0 def) % 0.53/0.65 % Number of atoms : 55 ( 13 equ) % 0.53/0.65 % Maximal formula atoms : 10 ( 3 avg) % 0.53/0.65 % Number of connectives : 40 ( 3 ~; 0 |; 19 &) % 0.53/0.65 % ( 3 <=>; 15 =>; 0 <=; 0 <~>) % 0.53/0.65 % Maximal formula depth : 9 ( 5 avg) % 0.53/0.65 % Maximal term depth : 1 ( 1 avg) % 0.53/0.65 % Number of predicates : 10 ( 9 usr; 0 prp; 1-2 aty) % 0.53/0.65 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 0.53/0.65 % Number of variables : 42 ( 40 !; 2 ?) % 0.53/0.65 % SPC : FOF_UNS_RFO_SEQ % 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 fof(cUnsatisfiable_substitution_1,axiom, % 0.53/0.65 ! [A,B] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & cUnsatisfiable(A) ) % 0.53/0.65 => cUnsatisfiable(B) ) ). % 0.53/0.65 % 0.53/0.65 fof(cowlNothing_substitution_1,axiom, % 0.53/0.65 ! [A,B] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & cowlNothing(A) ) % 0.53/0.65 => cowlNothing(B) ) ). % 0.53/0.65 % 0.53/0.65 fof(cowlThing_substitution_1,axiom, % 0.53/0.65 ! [A,B] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & cowlThing(A) ) % 0.53/0.65 => cowlThing(B) ) ). % 0.53/0.65 % 0.53/0.65 fof(cp_substitution_1,axiom, % 0.53/0.65 ! [A,B] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & cp(A) ) % 0.53/0.65 => cp(B) ) ). % 0.53/0.65 % 0.53/0.65 fof(rinvS_substitution_1,axiom, % 0.53/0.65 ! [A,B,C] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & rinvS(A,C) ) % 0.53/0.65 => rinvS(B,C) ) ). % 0.53/0.65 % 0.53/0.65 fof(rinvS_substitution_2,axiom, % 0.53/0.65 ! [A,B,C] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & rinvS(C,A) ) % 0.53/0.65 => rinvS(C,B) ) ). % 0.53/0.65 % 0.53/0.65 fof(rr_substitution_1,axiom, % 0.53/0.65 ! [A,B,C] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & rr(A,C) ) % 0.53/0.65 => rr(B,C) ) ). % 0.53/0.65 % 0.53/0.65 fof(rr_substitution_2,axiom, % 0.53/0.65 ! [A,B,C] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & rr(C,A) ) % 0.53/0.65 => rr(C,B) ) ). % 0.53/0.65 % 0.53/0.65 fof(rs_substitution_1,axiom, % 0.53/0.65 ! [A,B,C] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & rs(A,C) ) % 0.53/0.65 => rs(B,C) ) ). % 0.53/0.65 % 0.53/0.65 fof(rs_substitution_2,axiom, % 0.53/0.65 ! [A,B,C] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & rs(C,A) ) % 0.53/0.65 => rs(C,B) ) ). % 0.53/0.65 % 0.53/0.65 fof(xsd_integer_substitution_1,axiom, % 0.53/0.65 ! [A,B] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & xsd_integer(A) ) % 0.53/0.65 => xsd_integer(B) ) ). % 0.53/0.65 % 0.53/0.65 fof(xsd_string_substitution_1,axiom, % 0.53/0.65 ! [A,B] : % 0.53/0.65 ( ( A = B % 0.53/0.65 & xsd_string(A) ) % 0.53/0.65 => xsd_string(B) ) ). % 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 cUnsatisfiable % 0.53/0.65 fof(axiom_2,axiom, % 0.53/0.65 ! [X] : % 0.53/0.65 ( cUnsatisfiable(X) % 0.53/0.65 <=> ( ! [Y0,Y1] : % 0.53/0.65 ( ( rr(X,Y0) % 0.53/0.65 & rr(X,Y1) ) % 0.53/0.65 => Y0 = Y1 ) % 0.53/0.65 & ? [Y] : % 0.53/0.65 ( rr(X,Y) % 0.53/0.65 & ! [Z] : % 0.53/0.65 ( rinvS(Y,Z) % 0.53/0.65 => cp(Z) ) ) % 0.53/0.65 & ~ cp(X) % 0.53/0.65 & ? [Y] : % 0.53/0.65 ( rs(X,Y) % 0.53/0.66 & cp(Y) ) ) ) ). % 0.53/0.66 % 0.53/0.66 %----Inverse: rinvS % 0.53/0.66 fof(axiom_3,axiom, % 0.53/0.66 ! [X,Y] : % 0.53/0.66 ( rinvS(X,Y) % 0.53/0.66 <=> rs(Y,X) ) ). % 0.53/0.66 % 0.53/0.66 %----i2003_11_14_17_19_09372 % 0.53/0.66 fof(axiom_4,axiom, % 0.53/0.66 cUnsatisfiable(i2003_11_14_17_19_09372) ). % 0.53/0.66 % 0.53/0.66 fof(axiom_5,axiom, % 0.53/0.66 ! [X,Y] : % 0.53/0.66 ( rs(X,Y) % 0.53/0.66 => rr(X,Y) ) ). % 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:20) % 0.53/0.66 %VarNum:107(SingletonVarNum:36) % 0.53/0.66 %MaxLitNum:7 % 0.53/0.66 %MaxfuncDepth:1 % 0.53/0.66 %SharedTerms:2 % 0.53/0.66 [21]P1(a1) % 0.53/0.66 [22]~P2(x221) % 0.53/0.66 [23]P8(x231)+P3(x231) % 0.53/0.66 [24]~P4(x241)+~P1(x241) % 0.53/0.66 [25]~P8(x251)+~P3(x251) % 0.53/0.66 [26]~P1(x261)+P4(f2(x261)) % 0.53/0.66 [27]~P1(x271)+P5(x271,f3(x271)) % 0.53/0.66 [28]~P1(x281)+P7(x281,f2(x281)) % 0.53/0.66 [29]~P7(x292,x291)+P6(x291,x292) % 0.53/0.66 [30]~P7(x301,x302)+P5(x301,x302) % 0.53/0.66 [31]~P6(x312,x311)+P7(x311,x312) % 0.53/0.66 [32]P4(x321)+~P1(x322)+~P6(f3(x322),x321) % 0.53/0.66 [33]~P5(x333,x332)+~P5(x333,x331)+E(x331,x332)+~P1(x333) % 0.53/0.66 [34]P4(x341)+~P5(x341,x342)+~P7(x341,x343)+P1(x341)+~P4(x343)+~E(f5(x341),f6(x341))+P6(x342,f4(x341,x342)) % 0.53/0.66 [35]P4(x351)+~P5(x351,x352)+~P7(x351,x353)+P1(x351)+~P4(x353)+P5(x351,f6(x351))+P6(x352,f4(x351,x352)) % 0.53/0.66 [36]P4(x361)+~P5(x361,x362)+~P7(x361,x363)+P1(x361)+~P4(x363)+P5(x361,f5(x361))+P6(x362,f4(x361,x362)) % 0.53/0.66 [37]P4(x371)+~P7(x371,x372)+P1(x371)+~P5(x371,x373)+~P4(x372)+~E(f5(x371),f6(x371))+~P4(f4(x371,x373)) % 0.53/0.66 [38]P4(x381)+~P7(x381,x382)+P1(x381)+~P5(x381,x383)+~P4(x382)+P5(x381,f6(x381))+~P4(f4(x381,x383)) % 0.53/0.66 [39]P4(x391)+~P7(x391,x392)+P1(x391)+~P5(x391,x393)+~P4(x392)+P5(x391,f5(x391))+~P4(f4(x391,x393)) % 0.53/0.66 %EqnAxiom % 0.53/0.66 [1]E(x11,x11) % 0.53/0.66 [2]E(x22,x21)+~E(x21,x22) % 0.53/0.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.53/0.66 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.53/0.66 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 0.53/0.66 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63)) % 0.53/0.66 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72)) % 0.53/0.66 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 0.53/0.66 [9]~E(x91,x92)+E(f6(x91),f6(x92)) % 0.53/0.66 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 0.53/0.66 [11]~P2(x111)+P2(x112)+~E(x111,x112) % 0.53/0.66 [12]~P3(x121)+P3(x122)+~E(x121,x122) % 0.53/0.66 [13]~P8(x131)+P8(x132)+~E(x131,x132) % 0.53/0.66 [14]~P4(x141)+P4(x142)+~E(x141,x142) % 0.53/0.66 [15]P7(x152,x153)+~E(x151,x152)+~P7(x151,x153) % 0.53/0.66 [16]P7(x163,x162)+~E(x161,x162)+~P7(x163,x161) % 0.53/0.66 [17]P5(x172,x173)+~E(x171,x172)+~P5(x171,x173) % 0.53/0.66 [18]P5(x183,x182)+~E(x181,x182)+~P5(x183,x181) % 0.53/0.66 [19]P6(x192,x193)+~E(x191,x192)+~P6(x191,x193) % 0.53/0.66 [20]P6(x203,x202)+~E(x201,x202)+~P6(x203,x201) % 0.53/0.66 % 0.53/0.66 %------------------------------------------- % 0.53/0.66 cnf(40,plain, % 0.53/0.66 (~P4(a1)), % 0.53/0.66 inference(scs_inference,[],[21,24])). % 0.53/0.66 cnf(47,plain, % 0.53/0.66 (~E(a1,x471)+P5(x471,f3(x471))), % 0.53/0.66 inference(scs_inference,[],[21,27,10])). % 0.53/0.66 cnf(48,plain, % 0.53/0.66 (P5(a1,f3(a1))), % 0.53/0.66 inference(equality_inference,[],[47])). % 0.53/0.66 cnf(53,plain, % 0.53/0.66 (~E(a1,x531)+P7(x531,f2(x531))), % 0.53/0.66 inference(scs_inference,[],[21,28,10])). % 0.53/0.66 cnf(54,plain, % 0.53/0.66 (P7(a1,f2(a1))), % 0.53/0.66 inference(equality_inference,[],[53])). % 0.53/0.66 cnf(56,plain, % 0.53/0.66 (P7(a1,x561)+~E(f2(a1),x561)), % 0.53/0.66 inference(scs_inference,[],[54,15,16])). % 0.53/0.66 cnf(59,plain, % 0.53/0.66 (~P7(a1,f3(a1))), % 0.53/0.66 inference(scs_inference,[],[40,21,29,32])). % 0.53/0.66 cnf(65,plain, % 0.53/0.66 ($false), % 0.53/0.66 inference(scs_inference,[],[48,21,59,54,31,56,33,30]), % 0.53/0.66 ['proof']). % 0.53/0.66 % SZS output end Proof % 0.53/0.66 % Total time :0.010000s %------------------------------------------------------------------------------