%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS089+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 : n005.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:27 EDT 2024 % Result : Unsatisfiable 58.56s 58.68s % Output : CNFRefutation 58.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : KRS089+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.09/0.29 % Computer : n005.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Wed Jun 19 14:30:53 EDT 2024 % 0.09/0.29 % CPUTime : % 0.14/0.50 start to proof:theBenchmark % 58.56/58.67 %------------------------------------------- % 58.56/58.67 % File :CSE---1.7 % 58.56/58.67 % Problem :theBenchmark % 58.56/58.67 % Transform :cnf % 58.56/58.67 % Format :tptp:raw % 58.56/58.67 % Command :java -jar mcs_scs.jar %d %s % 58.56/58.67 % 58.56/58.67 % Result :Theorem 58.140000s % 58.56/58.67 % Output :CNFRefutation 58.140000s % 58.56/58.67 %------------------------------------------- % 58.56/58.67 %------------------------------------------------------------------------------ % 58.56/58.67 % File : KRS089+1 : TPTP v8.2.0. Released v3.1.0. % 58.56/58.67 % Domain : Knowledge Representation (Semantic Web) % 58.56/58.67 % Problem : A test for the interaction of one-of and inverse % 58.56/58.67 % Version : Especial. % 58.56/58.67 % English : A test for the interaction of one-of and inverse using the idea % 58.56/58.67 % of a spy point. Everything is related to the spy via the property % 58.56/58.68 % p and we know that the spy has at most two invP successors, thus % 58.56/58.68 % limiting the cardinality of the domain to being at most 2. % 58.56/58.68 % 58.56/58.68 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 58.56/58.68 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 58.56/58.68 % Source : [Bec03] % 58.56/58.68 % Names : inconsistent_description-logic-Manifest035 [Bec03] % 58.56/58.68 % 58.56/58.68 % Status : Unsatisfiable % 58.56/58.68 % Rating : 0.14 v8.2.0, 0.00 v3.7.0, 0.33 v3.3.0, 0.00 v3.1.0 % 58.56/58.68 % Syntax : Number of formulae : 19 ( 2 unt; 0 def) % 58.56/58.68 % Number of atoms : 57 ( 18 equ) % 58.56/58.68 % Maximal formula atoms : 7 ( 3 avg) % 58.56/58.68 % Number of connectives : 43 ( 5 ~; 2 |; 20 &) % 58.56/58.68 % ( 2 <=>; 14 =>; 0 <=; 0 <~>) % 58.56/58.68 % Maximal formula depth : 12 ( 5 avg) % 58.56/58.68 % Maximal term depth : 1 ( 1 avg) % 58.56/58.68 % Number of predicates : 9 ( 8 usr; 0 prp; 1-2 aty) % 58.56/58.68 % Number of functors : 2 ( 2 usr; 2 con; 0-0 aty) % 58.56/58.68 % Number of variables : 41 ( 37 !; 4 ?) % 58.56/58.68 % SPC : FOF_UNS_RFO_SEQ % 58.56/58.68 % 58.56/58.68 % Comments : Sean Bechhofer says there are some errors in the encoding of % 58.56/58.68 % datatypes, so this problem may not be perfect. At least it's % 58.56/58.68 % still representative of the type of reasoning required for OWL. % 58.56/58.68 %------------------------------------------------------------------------------ % 58.56/58.68 fof(cUnsatisfiable_substitution_1,axiom, % 58.56/58.68 ! [A,B] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & cUnsatisfiable(A) ) % 58.56/58.68 => cUnsatisfiable(B) ) ). % 58.56/58.68 % 58.56/58.68 fof(cowlNothing_substitution_1,axiom, % 58.56/58.68 ! [A,B] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & cowlNothing(A) ) % 58.56/58.68 => cowlNothing(B) ) ). % 58.56/58.68 % 58.56/58.68 fof(cowlThing_substitution_1,axiom, % 58.56/58.68 ! [A,B] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & cowlThing(A) ) % 58.56/58.68 => cowlThing(B) ) ). % 58.56/58.68 % 58.56/58.68 fof(rinvP_substitution_1,axiom, % 58.56/58.68 ! [A,B,C] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & rinvP(A,C) ) % 58.56/58.68 => rinvP(B,C) ) ). % 58.56/58.68 % 58.56/58.68 fof(rinvP_substitution_2,axiom, % 58.56/58.68 ! [A,B,C] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & rinvP(C,A) ) % 58.56/58.68 => rinvP(C,B) ) ). % 58.56/58.68 % 58.56/58.68 fof(rp_substitution_1,axiom, % 58.56/58.68 ! [A,B,C] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & rp(A,C) ) % 58.56/58.68 => rp(B,C) ) ). % 58.56/58.68 % 58.56/58.68 fof(rp_substitution_2,axiom, % 58.56/58.68 ! [A,B,C] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & rp(C,A) ) % 58.56/58.68 => rp(C,B) ) ). % 58.56/58.68 % 58.56/58.68 fof(rr_substitution_1,axiom, % 58.56/58.68 ! [A,B,C] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & rr(A,C) ) % 58.56/58.68 => rr(B,C) ) ). % 58.56/58.68 % 58.56/58.68 fof(rr_substitution_2,axiom, % 58.56/58.68 ! [A,B,C] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & rr(C,A) ) % 58.56/58.68 => rr(C,B) ) ). % 58.56/58.68 % 58.56/58.68 fof(xsd_integer_substitution_1,axiom, % 58.56/58.68 ! [A,B] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & xsd_integer(A) ) % 58.56/58.68 => xsd_integer(B) ) ). % 58.56/58.68 % 58.56/58.68 fof(xsd_string_substitution_1,axiom, % 58.56/58.68 ! [A,B] : % 58.56/58.68 ( ( A = B % 58.56/58.68 & xsd_string(A) ) % 58.56/58.68 => xsd_string(B) ) ). % 58.56/58.68 % 58.56/58.68 %----Thing and Nothing % 58.56/58.68 fof(axiom_0,axiom, % 58.56/58.68 ! [X] : % 58.56/58.68 ( cowlThing(X) % 58.56/58.68 & ~ cowlNothing(X) ) ). % 58.56/58.68 % 58.56/58.68 %----String and Integer disjoint % 58.56/58.68 fof(axiom_1,axiom, % 58.56/58.68 ! [X] : % 58.56/58.68 ( xsd_string(X) % 58.56/58.68 <=> ~ xsd_integer(X) ) ). % 58.56/58.68 % 58.56/58.68 %----Super cUnsatisfiable % 58.56/58.68 fof(axiom_2,axiom, % 58.56/58.68 ! [X] : % 58.56/58.68 ( cUnsatisfiable(X) % 58.56/58.68 => ? [Y0,Y1,Y2] : % 58.56/58.68 ( rr(X,Y0) % 58.56/58.68 & rr(X,Y1) % 58.56/58.68 & rr(X,Y2) % 58.56/58.68 & Y0 != Y1 % 58.56/58.68 & Y0 != Y2 % 58.56/58.68 & Y1 != Y2 ) ) ). % 58.56/58.68 % 58.56/58.68 %----Super cowlThing % 58.56/58.68 fof(axiom_3,axiom, % 58.56/58.68 ! [X] : % 58.56/58.68 ( cowlThing(X) % 58.56/58.68 => ? [Y] : % 58.56/58.68 ( rp(X,Y) % 58.56/58.68 & Y = ispy ) ) ). % 58.56/58.68 % 58.56/58.68 %----Inverse: rp % 58.56/58.68 fof(axiom_4,axiom, % 58.56/58.68 ! [X,Y] : % 58.56/58.68 ( rp(X,Y) % 58.56/58.68 <=> rinvP(Y,X) ) ). % 58.56/58.68 % 58.56/58.68 %----ispy % 58.56/58.68 fof(axiom_5,axiom, % 58.56/58.68 ! [X0,X1,X2] : % 58.56/58.68 ( ( rinvP(ispy,X0) % 58.56/58.68 & rinvP(ispy,X1) % 58.56/58.68 & rinvP(ispy,X2) ) % 58.56/58.68 => ( X0 = X1 % 58.56/58.68 | X0 = X2 % 58.56/58.68 | X1 = X2 ) ) ). % 58.56/58.68 % 58.56/58.68 %----ispy % 58.56/58.68 fof(axiom_6,axiom, % 58.56/58.68 cowlThing(ispy) ). % 58.56/58.68 % 58.56/58.68 %----i2003_11_14_17_19_53168 % 58.56/58.68 fof(axiom_7,axiom, % 58.56/58.68 cUnsatisfiable(i2003_11_14_17_19_53168) ). % 58.56/58.68 % 58.56/58.68 %------------------------------------------------------------------------------ % 58.56/58.68 %------------------------------------------- % 58.56/58.68 % Proof found % 58.56/58.68 % SZS status Theorem for theBenchmark % 58.56/58.68 % SZS output start Proof % 58.56/58.68 %ClaNum:30(EqnAxiom:16) % 58.56/58.68 %VarNum:41(SingletonVarNum:17) % 58.56/58.68 %MaxLitNum:6 % 58.56/58.68 %MaxfuncDepth:1 % 58.56/58.68 %SharedTerms:3 % 58.56/58.68 [17]P1(a1) % 58.56/58.68 [18]P2(x181,a5) % 58.56/58.68 [19]~P3(x191) % 58.56/58.68 [20]P7(x201)+P5(x201) % 58.56/58.68 [21]~P7(x211)+~P5(x211) % 58.56/58.68 [22]~P1(x221)+~E(f2(x221),f3(x221)) % 58.56/58.68 [23]~P1(x231)+~E(f4(x231),f3(x231)) % 58.56/58.68 [24]~P1(x241)+~E(f4(x241),f2(x241)) % 58.56/58.68 [25]~P1(x251)+P6(x251,f3(x251)) % 58.56/58.68 [26]~P1(x261)+P6(x261,f2(x261)) % 58.56/58.68 [27]~P1(x271)+P6(x271,f4(x271)) % 58.56/58.68 [28]~P2(x282,x281)+P4(x281,x282) % 58.56/58.68 [29]~P4(x292,x291)+P2(x291,x292) % 58.56/58.68 [30]E(x303,x301)+E(x301,x302)+E(x303,x302)+~P4(a5,x302)+~P4(a5,x301)+~P4(a5,x303) % 58.56/58.68 %EqnAxiom % 58.56/58.68 [1]E(x11,x11) % 58.56/58.68 [2]E(x22,x21)+~E(x21,x22) % 58.56/58.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.56/58.68 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 58.56/58.68 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 58.56/58.68 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 58.56/58.68 [7]~P1(x71)+P1(x72)+~E(x71,x72) % 58.56/58.68 [8]P2(x82,x83)+~E(x81,x82)+~P2(x81,x83) % 58.56/58.68 [9]P2(x93,x92)+~E(x91,x92)+~P2(x93,x91) % 58.56/58.68 [10]~P3(x101)+P3(x102)+~E(x101,x102) % 58.56/58.68 [11]~P5(x111)+P5(x112)+~E(x111,x112) % 58.56/58.68 [12]~P7(x121)+P7(x122)+~E(x121,x122) % 58.56/58.68 [13]P6(x132,x133)+~E(x131,x132)+~P6(x131,x133) % 58.56/58.68 [14]P6(x143,x142)+~E(x141,x142)+~P6(x143,x141) % 58.56/58.68 [15]P4(x152,x153)+~E(x151,x152)+~P4(x151,x153) % 58.56/58.68 [16]P4(x163,x162)+~E(x161,x162)+~P4(x163,x161) % 58.56/58.68 % 58.56/58.68 %------------------------------------------- % 58.64/58.68 cnf(55,plain, % 58.64/58.68 (P4(x551,x552)+~E(a5,x551)), % 58.64/58.68 inference(scs_inference,[],[18,28,15])). % 58.64/58.68 cnf(56,plain, % 58.64/58.68 (P4(a5,x561)), % 58.64/58.68 inference(equality_inference,[],[55])). % 58.64/58.68 cnf(57,plain, % 58.64/58.68 (~E(a1,x571)+~E(f2(x571),f3(x571))), % 58.64/58.68 inference(scs_inference,[],[17,22,7])). % 58.64/58.68 cnf(58,plain, % 58.64/58.68 (~E(a1,x581)+~E(f4(x581),f3(x581))), % 58.64/58.68 inference(scs_inference,[],[17,23,7])). % 58.64/58.68 cnf(59,plain, % 58.64/58.68 (~E(a1,x591)+~E(f4(x591),f2(x591))), % 58.64/58.68 inference(scs_inference,[],[17,24,7])). % 58.64/58.68 cnf(64,plain, % 58.64/58.68 (~E(f3(x641),f2(x641))+~E(a1,x641)), % 58.64/58.68 inference(scs_inference,[],[57,2])). % 58.64/58.68 cnf(65,plain, % 58.64/58.68 (~E(f3(x651),f4(x651))+~E(a1,x651)), % 58.64/58.68 inference(scs_inference,[],[58,2])). % 58.64/58.68 cnf(66,plain, % 58.64/58.68 (~E(f2(x661),f4(x661))+~E(a1,x661)), % 58.64/58.68 inference(scs_inference,[],[59,2])). % 58.64/58.68 cnf(67,plain, % 58.64/58.68 (~E(x671,f2(x672))+~E(f3(x672),x671)+~E(a1,x672)), % 58.64/58.68 inference(scs_inference,[],[64,3])). % 58.64/58.68 cnf(68,plain, % 58.64/58.68 (~E(x681,f4(x682))+~E(f3(x682),x681)+~E(a1,x682)), % 58.64/58.68 inference(scs_inference,[],[65,3])). % 58.64/58.68 cnf(69,plain, % 58.64/58.68 (~E(x691,f4(x692))+~E(f2(x692),x691)+~E(a1,x692)), % 58.64/58.68 inference(scs_inference,[],[66,3])). % 58.64/58.68 cnf(74,plain, % 58.64/58.68 (~E(f3(a1),x741)+~E(x741,f2(a1))), % 58.64/58.68 inference(scs_inference,[],[56,67,30])). % 58.64/58.68 cnf(75,plain, % 58.64/58.68 (~E(f3(a1),f2(a1))), % 58.64/58.68 inference(scs_inference,[],[56,74,30])). % 58.64/58.68 cnf(76,plain, % 58.64/58.68 (~E(f3(a1),x761)+~E(x761,f4(a1))), % 58.64/58.68 inference(scs_inference,[],[56,68,30])). % 58.64/58.68 cnf(77,plain, % 58.64/58.68 (~E(f3(a1),f4(a1))), % 58.64/58.68 inference(scs_inference,[],[56,76,30])). % 58.64/58.68 cnf(78,plain, % 58.64/58.68 (~E(f2(a1),x781)+~E(x781,f4(a1))), % 58.64/58.68 inference(scs_inference,[],[56,69,30])). % 58.64/58.68 cnf(79,plain, % 58.64/58.68 (~E(f2(a1),f4(a1))), % 58.64/58.68 inference(scs_inference,[],[56,78,30])). % 58.64/58.68 cnf(98,plain, % 58.64/58.68 (~E(x981,f3(a1))+~E(f4(a1),x981)), % 58.64/58.68 inference(scs_inference,[],[77,2,3])). % 58.64/58.68 cnf(99,plain, % 58.64/58.68 (~E(f4(a1),f3(a1))), % 58.64/58.68 inference(scs_inference,[],[56,98,30])). % 58.64/58.68 cnf(104,plain, % 58.64/58.68 (~E(x1041,f2(a1))+~E(f4(a1),x1041)), % 58.64/58.68 inference(scs_inference,[],[79,2,3])). % 58.64/58.68 cnf(105,plain, % 58.64/58.68 (~E(f4(a1),f2(a1))), % 58.64/58.68 inference(scs_inference,[],[56,104,30])). % 58.64/58.68 cnf(909,plain, % 58.64/58.68 (~P4(a5,f3(a1))+~P4(a5,f2(a1))), % 58.64/58.68 inference(scs_inference,[],[99,105,75,56,30])). % 58.64/58.68 cnf(914,plain, % 58.64/58.68 ($false), % 58.64/58.68 inference(scs_inference,[],[56,909,55]), % 58.64/58.68 ['proof']). % 58.64/58.68 % SZS output end Proof % 58.64/58.68 % Total time :58.140000s %------------------------------------------------------------------------------