%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS143+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 : 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:39 EDT 2024 % Result : Theorem 1.10s 1.19s % Output : CNFRefutation 1.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : KRS143+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 : n005.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:06:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.21/0.57 start to proof:theBenchmark % 1.10/1.18 %------------------------------------------- % 1.10/1.18 % File :CSE---1.7 % 1.10/1.18 % Problem :theBenchmark % 1.10/1.18 % Transform :cnf % 1.10/1.18 % Format :tptp:raw % 1.10/1.18 % Command :java -jar mcs_scs.jar %d %s % 1.10/1.18 % 1.10/1.19 % Result :Theorem 0.560000s % 1.10/1.19 % Output :CNFRefutation 0.560000s % 1.10/1.19 %------------------------------------------- % 1.10/1.19 %------------------------------------------------------------------------------ % 1.10/1.19 % File : KRS143+1 : TPTP v8.2.0. Released v3.1.0. % 1.10/1.19 % Domain : Knowledge Representation (Semantic Web) % 1.10/1.19 % Problem : An owl:cardinality constraint is simply shorthand % 1.10/1.19 % Version : Especial. % 1.10/1.19 % English : An owl:cardinality constraint is simply shorthand for a pair of % 1.10/1.19 % owl:minCardinality and owl:maxCardinality constraints. % 1.10/1.19 % 1.10/1.19 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 1.10/1.19 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 1.10/1.19 % Source : [Bec03] % 1.10/1.19 % Names : positive_cardinality-Manifest002 [Bec03] % 1.10/1.19 % 1.10/1.19 % Status : Theorem % 1.10/1.19 % Rating : 0.03 v7.2.0, 0.00 v6.4.0, 0.04 v6.3.0, 0.00 v6.1.0, 0.03 v6.0.0, 0.04 v5.4.0, 0.07 v5.3.0, 0.15 v5.2.0, 0.00 v4.1.0, 0.04 v4.0.1, 0.09 v4.0.0, 0.08 v3.7.0, 0.00 v3.2.0, 0.11 v3.1.0 % 1.10/1.19 % Syntax : Number of formulae : 12 ( 0 unt; 0 def) % 1.10/1.19 % Number of atoms : 40 ( 9 equ) % 1.10/1.19 % Maximal formula atoms : 9 ( 3 avg) % 1.10/1.19 % Number of connectives : 32 ( 4 ~; 0 |; 14 &) % 1.10/1.19 % ( 2 <=>; 12 =>; 0 <=; 0 <~>) % 1.10/1.19 % Maximal formula depth : 10 ( 6 avg) % 1.10/1.19 % Maximal term depth : 1 ( 1 avg) % 1.10/1.19 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty) % 1.10/1.19 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 1.10/1.19 % Number of variables : 29 ( 27 !; 2 ?) % 1.10/1.19 % SPC : FOF_THM_RFO_SEQ % 1.10/1.19 % 1.10/1.19 % Comments : Sean Bechhofer says there are some errors in the encoding of % 1.10/1.19 % datatypes, so this problem may not be perfect. At least it's % 1.10/1.19 % still representative of the type of reasoning required for OWL. % 1.10/1.19 %------------------------------------------------------------------------------ % 1.10/1.19 fof(cc_substitution_1,axiom, % 1.10/1.19 ! [A,B] : % 1.10/1.19 ( ( A = B % 1.10/1.19 & cc(A) ) % 1.10/1.19 => cc(B) ) ). % 1.10/1.19 % 1.10/1.19 fof(cowlNothing_substitution_1,axiom, % 1.10/1.19 ! [A,B] : % 1.10/1.19 ( ( A = B % 1.10/1.19 & cowlNothing(A) ) % 1.10/1.19 => cowlNothing(B) ) ). % 1.10/1.19 % 1.10/1.19 fof(cowlThing_substitution_1,axiom, % 1.10/1.19 ! [A,B] : % 1.10/1.19 ( ( A = B % 1.10/1.19 & cowlThing(A) ) % 1.10/1.19 => cowlThing(B) ) ). % 1.10/1.19 % 1.10/1.19 fof(rp_substitution_1,axiom, % 1.10/1.19 ! [A,B,C] : % 1.10/1.19 ( ( A = B % 1.10/1.19 & rp(A,C) ) % 1.10/1.19 => rp(B,C) ) ). % 1.10/1.19 % 1.10/1.19 fof(rp_substitution_2,axiom, % 1.10/1.19 ! [A,B,C] : % 1.10/1.19 ( ( A = B % 1.10/1.19 & rp(C,A) ) % 1.10/1.19 => rp(C,B) ) ). % 1.10/1.19 % 1.10/1.19 fof(xsd_integer_substitution_1,axiom, % 1.10/1.19 ! [A,B] : % 1.10/1.19 ( ( A = B % 1.10/1.19 & xsd_integer(A) ) % 1.10/1.19 => xsd_integer(B) ) ). % 1.10/1.19 % 1.10/1.19 fof(xsd_string_substitution_1,axiom, % 1.10/1.19 ! [A,B] : % 1.10/1.19 ( ( A = B % 1.10/1.19 & xsd_string(A) ) % 1.10/1.19 => xsd_string(B) ) ). % 1.10/1.19 % 1.10/1.19 %----Thing and Nothing % 1.10/1.19 fof(axiom_0,axiom, % 1.10/1.19 ! [X] : % 1.10/1.19 ( cowlThing(X) % 1.10/1.19 & ~ cowlNothing(X) ) ). % 1.10/1.19 % 1.10/1.19 %----String and Integer disjoint % 1.10/1.19 fof(axiom_1,axiom, % 1.10/1.19 ! [X] : % 1.10/1.19 ( xsd_string(X) % 1.10/1.19 <=> ~ xsd_integer(X) ) ). % 1.10/1.19 % 1.10/1.19 %----Super cc % 1.10/1.19 fof(axiom_2,axiom, % 1.10/1.19 ! [X] : % 1.10/1.19 ( cc(X) % 1.10/1.19 => ? [Y0] : rp(X,Y0) ) ). % 1.10/1.19 % 1.10/1.19 %----Super cc % 1.10/1.19 fof(axiom_3,axiom, % 1.10/1.19 ! [X] : % 1.10/1.19 ( cc(X) % 1.10/1.19 => ! [Y0,Y1] : % 1.10/1.19 ( ( rp(X,Y0) % 1.10/1.19 & rp(X,Y1) ) % 1.10/1.19 => Y0 = Y1 ) ) ). % 1.10/1.19 % 1.10/1.19 %----Thing and Nothing % 1.10/1.19 %----String and Integer disjoint % 1.10/1.19 %----Super cc % 1.10/1.19 fof(the_axiom,conjecture, % 1.10/1.19 ( ! [X] : % 1.10/1.19 ( cowlThing(X) % 1.10/1.19 & ~ cowlNothing(X) ) % 1.10/1.19 & ! [X] : % 1.10/1.19 ( xsd_string(X) % 1.10/1.19 <=> ~ xsd_integer(X) ) % 1.10/1.19 & ! [X] : % 1.10/1.19 ( cc(X) % 1.10/1.19 => ( ? [Y0] : rp(X,Y0) % 1.10/1.19 & ! [Y0,Y1] : % 1.10/1.19 ( ( rp(X,Y0) % 1.10/1.19 & rp(X,Y1) ) % 1.10/1.19 => Y0 = Y1 ) ) ) ) ). % 1.10/1.19 % 1.10/1.19 %------------------------------------------------------------------------------ % 1.10/1.19 %------------------------------------------- % 1.10/1.19 % Proof found % 1.10/1.19 % SZS status Theorem for theBenchmark % 1.10/1.19 % SZS output start Proof % 1.10/1.19 %ClaNum:23(EqnAxiom:10) % 1.10/1.19 %VarNum:21(SingletonVarNum:13) % 1.10/1.19 %MaxLitNum:5 % 1.10/1.19 %MaxfuncDepth:1 % 1.10/1.19 %SharedTerms:14 % 1.10/1.19 %goalClause: 13 14 17 18 19 20 21 22 % 1.10/1.19 [11]~P1(x111) % 1.10/1.19 [12]P5(x121)+P3(x121) % 1.10/1.19 [15]~P5(x151)+~P3(x151) % 1.10/1.19 [16]~P2(x161)+P4(x161,f3(x161)) % 1.10/1.20 [13]P2(a1)+P1(a2)+P3(a4)+~P5(a4) % 1.10/1.20 [14]P2(a1)+P1(a2)+P5(a4)+~P3(a4) % 1.10/1.20 [23]~P4(x233,x232)+~P4(x233,x231)+E(x231,x232)+~P2(x233) % 1.10/1.20 [17]~P4(a1,x171)+P1(a2)+P3(a4)+~E(a5,a6)+~P5(a4) % 1.10/1.20 [18]~E(a5,a6)+~P4(a1,x181)+P1(a2)+P5(a4)+~P3(a4) % 1.10/1.20 [19]~P4(a1,x191)+P1(a2)+P3(a4)+P4(a1,a6)+~P5(a4) % 1.10/1.20 [20]~P4(a1,x201)+P1(a2)+P3(a4)+P4(a1,a5)+~P5(a4) % 1.10/1.20 [21]P4(a1,a6)+~P4(a1,x211)+P1(a2)+P5(a4)+~P3(a4) % 1.10/1.20 [22]P4(a1,a5)+~P4(a1,x221)+P1(a2)+P5(a4)+~P3(a4) % 1.10/1.20 %EqnAxiom % 1.10/1.20 [1]E(x11,x11) % 1.10/1.20 [2]E(x22,x21)+~E(x21,x22) % 1.10/1.20 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.10/1.20 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 1.10/1.20 [5]~P1(x51)+P1(x52)+~E(x51,x52) % 1.10/1.20 [6]~P3(x61)+P3(x62)+~E(x61,x62) % 1.10/1.20 [7]~P5(x71)+P5(x72)+~E(x71,x72) % 1.10/1.20 [8]~P2(x81)+P2(x82)+~E(x81,x82) % 1.10/1.20 [9]P4(x92,x93)+~E(x91,x92)+~P4(x91,x93) % 1.10/1.20 [10]P4(x103,x102)+~E(x101,x102)+~P4(x103,x101) % 1.10/1.20 % 1.10/1.20 %------------------------------------------- % 1.10/1.20 cnf(28,plain, % 1.10/1.20 (P2(a1)+P3(a4)+~P5(a4)), % 1.10/1.20 inference(scs_inference,[],[11,13])). % 1.10/1.20 cnf(29,plain, % 1.10/1.20 (P2(a1)+P5(a4)+~P3(a4)), % 1.10/1.20 inference(scs_inference,[],[11,14])). % 1.10/1.20 cnf(30,plain, % 1.10/1.20 (~P4(a1,x301)+~E(a5,a6)+P3(a4)+~P5(a4)), % 1.10/1.20 inference(scs_inference,[],[11,17])). % 1.10/1.20 cnf(31,plain, % 1.10/1.20 (~E(a5,a6)+~P4(a1,x311)+P5(a4)+~P3(a4)), % 1.10/1.20 inference(scs_inference,[],[11,18])). % 1.10/1.20 cnf(32,plain, % 1.10/1.20 (~P4(a1,x321)+P4(a1,a6)+P3(a4)+~P5(a4)), % 1.10/1.20 inference(scs_inference,[],[11,19])). % 1.10/1.20 cnf(33,plain, % 1.10/1.20 (~P4(a1,x331)+P4(a1,a5)+P3(a4)+~P5(a4)), % 1.10/1.20 inference(scs_inference,[],[11,20])). % 1.10/1.20 cnf(34,plain, % 1.10/1.20 (P4(a1,a6)+~P4(a1,x341)+P5(a4)+~P3(a4)), % 1.10/1.20 inference(scs_inference,[],[11,21])). % 1.10/1.20 cnf(35,plain, % 1.10/1.20 (P4(a1,a5)+~P4(a1,x351)+P5(a4)+~P3(a4)), % 1.10/1.20 inference(scs_inference,[],[11,22])). % 1.10/1.20 cnf(41,plain, % 1.10/1.20 (P4(a1,f3(a1))+P3(a4)+~P5(a4)), % 1.10/1.20 inference(scs_inference,[],[28,16])). % 1.10/1.20 cnf(42,plain, % 1.10/1.20 (P4(a1,f3(a1))+P5(a4)+~P3(a4)), % 1.10/1.20 inference(scs_inference,[],[29,16])). % 1.10/1.20 cnf(47,plain, % 1.10/1.20 (~E(a5,a6)+P3(a4)+~P5(a4)), % 1.10/1.20 inference(scs_inference,[],[41,30])). % 1.10/1.20 cnf(48,plain, % 1.10/1.20 (~E(a6,a5)+P3(a4)+~P5(a4)), % 1.10/1.20 inference(scs_inference,[],[47,2])). % 1.10/1.20 cnf(49,plain, % 1.10/1.20 (~P5(a4)+~E(a6,a5)), % 1.10/1.20 inference(scs_inference,[],[48,15])). % 1.10/1.20 cnf(50,plain, % 1.10/1.20 (P3(a4)+~E(a6,a5)), % 1.10/1.20 inference(scs_inference,[],[49,12])). % 1.10/1.20 cnf(51,plain, % 1.10/1.20 (~E(a4,x511)+P3(x511)+~E(a6,a5)), % 1.10/1.20 inference(scs_inference,[],[50,6])). % 1.10/1.20 cnf(52,plain, % 1.10/1.20 (~E(a5,a6)+P5(a4)+~P3(a4)), % 1.10/1.20 inference(scs_inference,[],[42,31])). % 1.10/1.20 cnf(53,plain, % 1.10/1.20 (~E(a6,a5)+P5(a4)+~P3(a4)), % 1.10/1.20 inference(scs_inference,[],[52,2])). % 1.10/1.20 cnf(54,plain, % 1.10/1.20 (~P3(a4)+~E(a6,a5)), % 1.10/1.20 inference(scs_inference,[],[53,15])). % 1.10/1.20 cnf(57,plain, % 1.10/1.20 (~E(a6,a5)), % 1.10/1.20 inference(scs_inference,[],[51,54])). % 1.10/1.20 cnf(58,plain, % 1.10/1.20 (~P2(x581)+~P4(x581,a5)+~P4(x581,a6)), % 1.10/1.20 inference(scs_inference,[],[57,23])). % 1.10/1.20 cnf(149,plain, % 1.10/1.20 (P4(x1491,x1492)+~P2(x1491)+~E(f3(x1491),x1492)), % 1.10/1.20 inference(scs_inference,[],[10,16])). % 1.10/1.20 cnf(278,plain, % 1.10/1.20 (P2(a1)+P3(a4)), % 1.10/1.20 inference(scs_inference,[],[12,28])). % 1.10/1.20 cnf(294,plain, % 1.10/1.20 (P4(a1,f3(a1))+P3(a4)), % 1.10/1.20 inference(scs_inference,[],[278,16])). % 1.10/1.20 cnf(310,plain, % 1.10/1.20 (P4(x3101,f3(a1))+~E(a1,x3101)+P3(a4)), % 1.10/1.20 inference(scs_inference,[],[294,9])). % 1.10/1.20 cnf(439,plain, % 1.10/1.20 (P2(a1)+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[12,29])). % 1.10/1.20 cnf(455,plain, % 1.10/1.20 (P4(a1,f3(a1))+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[439,16])). % 1.10/1.20 cnf(471,plain, % 1.10/1.20 (P4(x4711,f3(a1))+~E(a1,x4711)+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[455,9])). % 1.10/1.20 cnf(488,plain, % 1.10/1.20 (~P4(a1,x4881)+P4(a1,a6)+P3(a4)), % 1.10/1.20 inference(scs_inference,[],[12,32])). % 1.10/1.20 cnf(504,plain, % 1.10/1.20 (P4(a1,a6)+P3(a4)), % 1.10/1.20 inference(scs_inference,[],[488,310])). % 1.10/1.20 cnf(520,plain, % 1.10/1.20 (~P2(a1)+~P4(a1,a5)+P3(a4)), % 1.10/1.20 inference(scs_inference,[],[57,504,23])). % 1.10/1.20 cnf(536,plain, % 1.10/1.20 (~P4(a1,a5)+P3(a4)), % 1.10/1.20 inference(scs_inference,[],[520,278])). % 1.10/1.20 cnf(569,plain, % 1.10/1.20 (P4(a1,a6)+~P4(a1,x5691)+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[12,34])). % 1.10/1.20 cnf(585,plain, % 1.10/1.20 (P4(a1,a6)+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[569,455])). % 1.10/1.20 cnf(601,plain, % 1.10/1.20 (~P2(a1)+~P4(a1,a5)+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[585,58])). % 1.10/1.20 cnf(617,plain, % 1.10/1.20 (~P2(a1)+~E(f3(a1),a5)+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[601,149])). % 1.10/1.20 cnf(633,plain, % 1.10/1.20 (~E(a5,f3(a1))+~P2(a1)+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[617,2])). % 1.10/1.20 cnf(649,plain, % 1.10/1.20 (~E(a5,f3(a1))+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[633,439])). % 1.10/1.20 cnf(665,plain, % 1.10/1.20 (~E(f3(a1),a5)+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[649,2])). % 1.10/1.20 cnf(776,plain, % 1.10/1.20 (~P4(a1,x7761)+P4(a1,a5)+P3(a4)), % 1.10/1.20 inference(scs_inference,[],[12,33])). % 1.10/1.20 cnf(792,plain, % 1.10/1.20 (P4(a1,a5)+P3(a4)), % 1.10/1.20 inference(scs_inference,[],[776,310])). % 1.10/1.20 cnf(808,plain, % 1.10/1.20 (P3(a4)), % 1.10/1.20 inference(scs_inference,[],[792,536])). % 1.10/1.20 cnf(809,plain, % 1.10/1.20 (P4(a1,a5)+~P4(a1,x8091)+P5(a4)), % 1.10/1.20 inference(scs_inference,[],[808,35])). % 1.10/1.20 cnf(815,plain, % 1.10/1.20 (~P5(a4)), % 1.10/1.20 inference(scs_inference,[],[808,15])). % 1.10/1.20 cnf(824,plain, % 1.10/1.20 (~P2(a1)), % 1.10/1.20 inference(scs_inference,[],[808,57,15,455,585,649,665,471,809,23])). % 1.10/1.20 cnf(847,plain, % 1.10/1.20 ($false), % 1.10/1.20 inference(scs_inference,[],[824,815,439]), % 1.10/1.20 ['proof']). % 1.10/1.20 % SZS output end Proof % 1.10/1.20 % Total time :0.560000s %------------------------------------------------------------------------------