%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS121+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 : 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:34 EDT 2024 % Result : Unsatisfiable 0.56s 0.72s % Output : CNFRefutation 0.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : KRS121+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.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:20:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.42/0.60 start to proof:theBenchmark % 0.56/0.71 %------------------------------------------- % 0.56/0.71 % File :CSE---1.7 % 0.56/0.71 % Problem :theBenchmark % 0.56/0.71 % Transform :cnf % 0.56/0.71 % Format :tptp:raw % 0.56/0.71 % Command :java -jar mcs_scs.jar %d %s % 0.56/0.71 % 0.56/0.71 % Result :Theorem 0.050000s % 0.56/0.71 % Output :CNFRefutation 0.050000s % 0.56/0.71 %------------------------------------------- % 0.56/0.71 %------------------------------------------------------------------------------ % 0.56/0.71 % File : KRS121+1 : TPTP v8.2.0. Released v3.1.0. % 0.56/0.71 % Domain : Knowledge Representation (Semantic Web) % 0.56/0.71 % Problem : DL Test: t7f.2 % 0.56/0.71 % Version : Especial. % 0.56/0.71 % English : % 0.56/0.71 % 0.56/0.71 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 0.56/0.71 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 0.56/0.71 % Source : [Bec03] % 0.56/0.71 % Names : inconsistent_description-logic-Manifest632 [Bec03] % 0.56/0.71 % 0.56/0.71 % Status : Unsatisfiable % 0.56/0.71 % Rating : 0.00 v3.1.0 % 0.56/0.71 % Syntax : Number of formulae : 31 ( 1 unt; 0 def) % 0.56/0.71 % Number of atoms : 87 ( 20 equ) % 0.56/0.71 % Maximal formula atoms : 4 ( 2 avg) % 0.56/0.71 % Number of connectives : 59 ( 3 ~; 0 |; 26 &) % 0.56/0.71 % ( 8 <=>; 22 =>; 0 <=; 0 <~>) % 0.56/0.71 % Maximal formula depth : 6 ( 5 avg) % 0.56/0.71 % Maximal term depth : 1 ( 1 avg) % 0.56/0.71 % Number of predicates : 15 ( 14 usr; 0 prp; 1-2 aty) % 0.56/0.71 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 0.56/0.71 % Number of variables : 70 ( 66 !; 4 ?) % 0.56/0.71 % SPC : FOF_UNS_RFO_SEQ % 0.56/0.71 % 0.56/0.71 % Comments : Sean Bechhofer says there are some errors in the encoding of % 0.56/0.71 % datatypes, so this problem may not be perfect. At least it's % 0.56/0.71 % still representative of the type of reasoning required for OWL. % 0.56/0.71 %------------------------------------------------------------------------------ % 0.56/0.71 fof(cUnsatisfiable_substitution_1,axiom, % 0.56/0.71 ! [A,B] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & cUnsatisfiable(A) ) % 0.56/0.71 => cUnsatisfiable(B) ) ). % 0.56/0.71 % 0.56/0.71 fof(ca_Ax2_substitution_1,axiom, % 0.56/0.71 ! [A,B] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & ca_Ax2(A) ) % 0.56/0.71 => ca_Ax2(B) ) ). % 0.56/0.71 % 0.56/0.71 fof(ca_Vx3_substitution_1,axiom, % 0.56/0.71 ! [A,B] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & ca_Vx3(A) ) % 0.56/0.71 => ca_Vx3(B) ) ). % 0.56/0.71 % 0.56/0.71 fof(cowlNothing_substitution_1,axiom, % 0.56/0.71 ! [A,B] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & cowlNothing(A) ) % 0.56/0.71 => cowlNothing(B) ) ). % 0.56/0.71 % 0.56/0.71 fof(cowlThing_substitution_1,axiom, % 0.56/0.71 ! [A,B] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & cowlThing(A) ) % 0.56/0.71 => cowlThing(B) ) ). % 0.56/0.71 % 0.56/0.71 fof(cp1_substitution_1,axiom, % 0.56/0.71 ! [A,B] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & cp1(A) ) % 0.56/0.71 => cp1(B) ) ). % 0.56/0.71 % 0.56/0.71 fof(cp1xcomp_substitution_1,axiom, % 0.56/0.71 ! [A,B] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & cp1xcomp(A) ) % 0.56/0.71 => cp1xcomp(B) ) ). % 0.56/0.71 % 0.56/0.71 fof(ra_Px1_substitution_1,axiom, % 0.56/0.71 ! [A,B,C] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & ra_Px1(A,C) ) % 0.56/0.71 => ra_Px1(B,C) ) ). % 0.56/0.71 % 0.56/0.71 fof(ra_Px1_substitution_2,axiom, % 0.56/0.71 ! [A,B,C] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & ra_Px1(C,A) ) % 0.56/0.71 => ra_Px1(C,B) ) ). % 0.56/0.71 % 0.56/0.71 fof(rf_substitution_1,axiom, % 0.56/0.71 ! [A,B,C] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & rf(A,C) ) % 0.56/0.71 => rf(B,C) ) ). % 0.56/0.71 % 0.56/0.71 fof(rf_substitution_2,axiom, % 0.56/0.71 ! [A,B,C] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & rf(C,A) ) % 0.56/0.71 => rf(C,B) ) ). % 0.56/0.71 % 0.56/0.71 fof(rinvF_substitution_1,axiom, % 0.56/0.71 ! [A,B,C] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & rinvF(A,C) ) % 0.56/0.71 => rinvF(B,C) ) ). % 0.56/0.71 % 0.56/0.71 fof(rinvF_substitution_2,axiom, % 0.56/0.71 ! [A,B,C] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & rinvF(C,A) ) % 0.56/0.71 => rinvF(C,B) ) ). % 0.56/0.71 % 0.56/0.71 fof(rinvR_substitution_1,axiom, % 0.56/0.71 ! [A,B,C] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & rinvR(A,C) ) % 0.56/0.71 => rinvR(B,C) ) ). % 0.56/0.71 % 0.56/0.71 fof(rinvR_substitution_2,axiom, % 0.56/0.71 ! [A,B,C] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & rinvR(C,A) ) % 0.56/0.71 => rinvR(C,B) ) ). % 0.56/0.71 % 0.56/0.71 fof(rr_substitution_1,axiom, % 0.56/0.71 ! [A,B,C] : % 0.56/0.71 ( ( A = B % 0.56/0.71 & rr(A,C) ) % 0.56/0.71 => rr(B,C) ) ). % 0.56/0.71 % 0.56/0.71 fof(rr_substitution_2,axiom, % 0.56/0.71 ! [A,B,C] : % 0.56/0.72 ( ( A = B % 0.56/0.72 & rr(C,A) ) % 0.56/0.72 => rr(C,B) ) ). % 0.56/0.72 % 0.56/0.72 fof(xsd_integer_substitution_1,axiom, % 0.56/0.72 ! [A,B] : % 0.56/0.72 ( ( A = B % 0.56/0.72 & xsd_integer(A) ) % 0.56/0.72 => xsd_integer(B) ) ). % 0.56/0.72 % 0.56/0.72 fof(xsd_string_substitution_1,axiom, % 0.56/0.72 ! [A,B] : % 0.56/0.72 ( ( A = B % 0.56/0.72 & xsd_string(A) ) % 0.56/0.72 => xsd_string(B) ) ). % 0.56/0.72 % 0.56/0.72 %----Thing and Nothing % 0.56/0.72 fof(axiom_0,axiom, % 0.56/0.72 ! [X] : % 0.56/0.72 ( cowlThing(X) % 0.56/0.72 & ~ cowlNothing(X) ) ). % 0.56/0.72 % 0.56/0.72 %----String and Integer disjoint % 0.56/0.72 fof(axiom_1,axiom, % 0.56/0.72 ! [X] : % 0.56/0.72 ( xsd_string(X) % 0.56/0.72 <=> ~ xsd_integer(X) ) ). % 0.56/0.72 % 0.56/0.72 %----Equality cUnsatisfiable % 0.56/0.72 fof(axiom_2,axiom, % 0.56/0.72 ! [X] : % 0.56/0.72 ( cUnsatisfiable(X) % 0.56/0.72 <=> ( ? [Y] : % 0.56/0.72 ( rr(X,Y) % 0.56/0.72 & ca_Vx3(Y) ) % 0.56/0.72 & cp1(X) ) ) ). % 0.56/0.72 % 0.56/0.72 %----Equality cp1 % 0.56/0.72 fof(axiom_3,axiom, % 0.56/0.72 ! [X] : % 0.56/0.72 ( cp1(X) % 0.56/0.72 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 0.56/0.72 % 0.56/0.72 %----Equality cp1xcomp % 0.56/0.72 fof(axiom_4,axiom, % 0.56/0.72 ! [X] : % 0.56/0.72 ( cp1xcomp(X) % 0.56/0.72 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 0.56/0.72 % 0.56/0.72 %----Equality ca_Ax2 % 0.56/0.72 fof(axiom_5,axiom, % 0.56/0.72 ! [X] : % 0.56/0.72 ( ca_Ax2(X) % 0.56/0.72 <=> ( cp1(X) % 0.56/0.72 & ! [Y] : % 0.56/0.72 ( rinvR(X,Y) % 0.56/0.72 => cp1xcomp(Y) ) ) ) ). % 0.56/0.72 % 0.56/0.72 %----Equality ca_Vx3 % 0.56/0.72 fof(axiom_6,axiom, % 0.56/0.72 ! [X] : % 0.56/0.72 ( ca_Vx3(X) % 0.56/0.72 <=> ? [Y] : % 0.56/0.72 ( rr(X,Y) % 0.56/0.72 & ca_Ax2(Y) ) ) ). % 0.56/0.72 % 0.56/0.72 %----Functional: rf % 0.56/0.72 fof(axiom_7,axiom, % 0.56/0.72 ! [X,Y,Z] : % 0.56/0.72 ( ( rf(X,Y) % 0.56/0.72 & rf(X,Z) ) % 0.56/0.72 => Y = Z ) ). % 0.56/0.72 % 0.56/0.72 %----Inverse: rinvF % 0.56/0.72 fof(axiom_8,axiom, % 0.56/0.72 ! [X,Y] : % 0.56/0.72 ( rinvF(X,Y) % 0.56/0.72 <=> rf(Y,X) ) ). % 0.56/0.72 % 0.56/0.72 %----Inverse: rinvR % 0.56/0.72 fof(axiom_9,axiom, % 0.56/0.72 ! [X,Y] : % 0.56/0.72 ( rinvR(X,Y) % 0.56/0.72 <=> rr(Y,X) ) ). % 0.56/0.72 % 0.56/0.72 %----Transitive: rr % 0.56/0.72 fof(axiom_10,axiom, % 0.56/0.72 ! [X,Y,Z] : % 0.56/0.72 ( ( rr(X,Y) % 0.56/0.72 & rr(Y,Z) ) % 0.56/0.72 => rr(X,Z) ) ). % 0.56/0.72 % 0.56/0.72 %----i2003_11_14_17_21_5199 % 0.56/0.72 fof(axiom_11,axiom, % 0.56/0.72 cUnsatisfiable(i2003_11_14_17_21_5199) ). % 0.56/0.72 % 0.56/0.72 %------------------------------------------------------------------------------ % 0.56/0.72 %------------------------------------------- % 0.56/0.72 % Proof found % 0.56/0.72 % SZS status Theorem for theBenchmark % 0.56/0.72 % SZS output start Proof % 0.56/0.72 %ClaNum:51(EqnAxiom:26) % 0.56/0.72 %VarNum:79(SingletonVarNum:37) % 0.56/0.72 %MaxLitNum:4 % 0.56/0.72 %MaxfuncDepth:1 % 0.56/0.72 %SharedTerms:2 % 0.56/0.72 [27]P1(a1) % 0.56/0.72 [28]~P2(x281) % 0.56/0.72 [29]P13(x291)+P5(x291) % 0.56/0.72 [30]~P1(x301)+P6(x301) % 0.56/0.72 [31]~P3(x311)+P6(x311) % 0.56/0.72 [32]~P13(x321)+~P5(x321) % 0.56/0.72 [33]~P4(x331)+P3(f2(x331)) % 0.56/0.72 [34]~P1(x341)+P4(f3(x341)) % 0.56/0.72 [35]P6(x351)+P7(x351,f4(x351)) % 0.56/0.72 [37]~P8(x371)+P7(x371,f5(x371)) % 0.56/0.72 [38]~P1(x381)+P9(x381,f3(x381)) % 0.56/0.72 [39]~P4(x391)+P9(x391,f2(x391)) % 0.56/0.72 [36]P8(x361)+~P7(x361,x362) % 0.56/0.72 [41]~P6(x411)+~P7(x411,x412) % 0.56/0.72 [45]~P12(x452,x451)+P11(x451,x452) % 0.56/0.72 [46]~P11(x462,x461)+P12(x461,x462) % 0.56/0.72 [47]~P9(x472,x471)+P10(x471,x472) % 0.56/0.72 [48]~P10(x482,x481)+P9(x481,x482) % 0.56/0.72 [40]~P6(x401)+P3(x401)+~P8(f6(x401)) % 0.56/0.72 [42]~P6(x421)+P3(x421)+P10(x421,f6(x421)) % 0.56/0.72 [43]~P9(x431,x432)+P4(x431)+~P3(x432) % 0.56/0.72 [44]~P10(x442,x441)+P8(x441)+~P3(x442) % 0.56/0.72 [50]~P11(x503,x501)+E(x501,x502)+~P11(x503,x502) % 0.56/0.72 [51]~P9(x511,x513)+P9(x511,x512)+~P9(x513,x512) % 0.56/0.72 [49]~P6(x491)+~P9(x491,x492)+P1(x491)+~P4(x492) % 0.56/0.72 %EqnAxiom % 0.56/0.72 [1]E(x11,x11) % 0.56/0.72 [2]E(x22,x21)+~E(x21,x22) % 0.56/0.72 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.56/0.72 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.56/0.72 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 0.56/0.72 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 0.56/0.72 [7]~E(x71,x72)+E(f5(x71),f5(x72)) % 0.56/0.72 [8]~E(x81,x82)+E(f6(x81),f6(x82)) % 0.56/0.72 [9]~P1(x91)+P1(x92)+~E(x91,x92) % 0.56/0.72 [10]~P2(x101)+P2(x102)+~E(x101,x102) % 0.56/0.72 [11]~P5(x111)+P5(x112)+~E(x111,x112) % 0.56/0.72 [12]~P13(x121)+P13(x122)+~E(x121,x122) % 0.56/0.72 [13]~P6(x131)+P6(x132)+~E(x131,x132) % 0.56/0.72 [14]P9(x142,x143)+~E(x141,x142)+~P9(x141,x143) % 0.56/0.72 [15]P9(x153,x152)+~E(x151,x152)+~P9(x153,x151) % 0.56/0.72 [16]~P4(x161)+P4(x162)+~E(x161,x162) % 0.56/0.72 [17]~P3(x171)+P3(x172)+~E(x171,x172) % 0.56/0.72 [18]P11(x182,x183)+~E(x181,x182)+~P11(x181,x183) % 0.56/0.72 [19]P11(x193,x192)+~E(x191,x192)+~P11(x193,x191) % 0.56/0.72 [20]P10(x202,x203)+~E(x201,x202)+~P10(x201,x203) % 0.56/0.72 [21]P10(x213,x212)+~E(x211,x212)+~P10(x213,x211) % 0.56/0.72 [22]P12(x222,x223)+~E(x221,x222)+~P12(x221,x223) % 0.56/0.72 [23]P12(x233,x232)+~E(x231,x232)+~P12(x233,x231) % 0.56/0.72 [24]~P8(x241)+P8(x242)+~E(x241,x242) % 0.56/0.72 [25]P7(x252,x253)+~E(x251,x252)+~P7(x251,x253) % 0.56/0.72 [26]P7(x263,x262)+~E(x261,x262)+~P7(x263,x261) % 0.56/0.72 % 0.56/0.72 %------------------------------------------- % 0.56/0.72 cnf(53,plain, % 0.56/0.72 (~P7(a1,x531)), % 0.56/0.72 inference(scs_inference,[],[27,30,41])). % 0.56/0.72 cnf(55,plain, % 0.56/0.72 (~P7(a1,x551)), % 0.56/0.72 inference(rename_variables,[],[53])). % 0.56/0.72 cnf(62,plain, % 0.56/0.72 (~P4(x621)+~P10(f2(x621),a1)), % 0.56/0.72 inference(scs_inference,[],[53,55,35,37,44,33])). % 0.56/0.72 cnf(72,plain, % 0.56/0.72 (~E(a1,x721)+P9(x721,f3(x721))), % 0.56/0.72 inference(scs_inference,[],[27,38,9])). % 0.56/0.72 cnf(73,plain, % 0.56/0.72 (P9(a1,f3(a1))), % 0.56/0.72 inference(equality_inference,[],[72])). % 0.56/0.72 cnf(77,plain, % 0.56/0.72 (P9(f3(a1),f2(f3(a1)))), % 0.56/0.72 inference(scs_inference,[],[27,39,34])). % 0.56/0.72 cnf(78,plain, % 0.56/0.72 (P9(a1,f2(f3(a1)))), % 0.56/0.72 inference(scs_inference,[],[77,73,51])). % 0.56/0.72 cnf(104,plain, % 0.56/0.72 (~P4(f3(a1))), % 0.56/0.72 inference(scs_inference,[],[78,47,62])). % 0.56/0.72 cnf(105,plain, % 0.56/0.72 ($false), % 0.56/0.72 inference(scs_inference,[],[104,27,34]), % 0.56/0.72 ['proof']). % 0.56/0.72 % SZS output end Proof % 0.56/0.72 % Total time :0.050000s %------------------------------------------------------------------------------