%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS174+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 : n032.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:47 EDT 2024 % Result : Theorem 0.53s 0.68s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : KRS174+1 : TPTP v8.2.0. Released v3.1.0. % 0.00/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Wed Jun 19 13:33:53 EDT 2024 % 0.08/0.28 % CPUTime : % 0.13/0.47 start to proof:theBenchmark % 0.53/0.67 %------------------------------------------- % 0.53/0.67 % File :CSE---1.7 % 0.53/0.67 % Problem :theBenchmark % 0.53/0.67 % Transform :cnf % 0.53/0.67 % Format :tptp:raw % 0.53/0.67 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.67 % 0.53/0.67 % Result :Theorem 0.160000s % 0.53/0.67 % Output :CNFRefutation 0.160000s % 0.53/0.67 %------------------------------------------- % 0.53/0.67 %------------------------------------------------------------------------------ % 0.53/0.67 % File : KRS174+1 : TPTP v8.2.0. Released v3.1.0. % 0.53/0.67 % Domain : Knowledge Representation (Semantic Web) % 0.53/0.67 % Problem : Sets with appropriate extensions are related by unionOf % 0.53/0.68 % Version : Especial. % 0.53/0.68 % English : % 0.53/0.68 % 0.53/0.68 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 0.53/0.68 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 0.53/0.68 % Source : [Bec03] % 0.53/0.68 % Names : positive_unionOf-Manifest003 [Bec03] % 0.53/0.68 % 0.53/0.68 % Status : Theorem % 0.53/0.68 % Rating : 0.00 v5.3.0, 0.09 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.4.0, 0.08 v3.3.0, 0.00 v3.1.0 % 0.53/0.68 % Syntax : Number of formulae : 15 ( 2 unt; 0 def) % 0.53/0.68 % Number of atoms : 41 ( 11 equ) % 0.53/0.68 % Maximal formula atoms : 7 ( 2 avg) % 0.53/0.68 % Number of connectives : 30 ( 4 ~; 2 |; 11 &) % 0.53/0.68 % ( 6 <=>; 7 =>; 0 <=; 0 <~>) % 0.53/0.68 % Maximal formula depth : 6 ( 4 avg) % 0.53/0.68 % Maximal term depth : 1 ( 1 avg) % 0.53/0.68 % Number of predicates : 8 ( 7 usr; 0 prp; 1-2 aty) % 0.53/0.68 % Number of functors : 2 ( 2 usr; 2 con; 0-0 aty) % 0.53/0.68 % Number of variables : 22 ( 22 !; 0 ?) % 0.53/0.68 % SPC : FOF_THM_EPR_SEQ % 0.53/0.68 % 0.53/0.68 % Comments : Sean Bechhofer says there are some errors in the encoding of % 0.53/0.68 % datatypes, so this problem may not be perfect. At least it's % 0.53/0.68 % still representative of the type of reasoning required for OWL. % 0.53/0.68 %------------------------------------------------------------------------------ % 0.53/0.68 fof(cA_substitution_1,axiom, % 0.53/0.68 ! [A,B] : % 0.53/0.68 ( ( A = B % 0.53/0.68 & cA(A) ) % 0.53/0.68 => cA(B) ) ). % 0.53/0.68 % 0.53/0.68 fof(cA_and_B_substitution_1,axiom, % 0.53/0.68 ! [A,B] : % 0.53/0.68 ( ( A = B % 0.53/0.68 & cA_and_B(A) ) % 0.53/0.68 => cA_and_B(B) ) ). % 0.53/0.68 % 0.53/0.68 fof(cB_substitution_1,axiom, % 0.53/0.68 ! [A,B] : % 0.53/0.68 ( ( A = B % 0.53/0.68 & cB(A) ) % 0.53/0.68 => cB(B) ) ). % 0.53/0.68 % 0.53/0.68 fof(cowlNothing_substitution_1,axiom, % 0.53/0.68 ! [A,B] : % 0.53/0.68 ( ( A = B % 0.53/0.68 & cowlNothing(A) ) % 0.53/0.68 => cowlNothing(B) ) ). % 0.53/0.68 % 0.53/0.68 fof(cowlThing_substitution_1,axiom, % 0.53/0.68 ! [A,B] : % 0.53/0.68 ( ( A = B % 0.53/0.68 & cowlThing(A) ) % 0.53/0.68 => cowlThing(B) ) ). % 0.53/0.68 % 0.53/0.68 fof(xsd_integer_substitution_1,axiom, % 0.53/0.68 ! [A,B] : % 0.53/0.68 ( ( A = B % 0.53/0.68 & xsd_integer(A) ) % 0.53/0.68 => xsd_integer(B) ) ). % 0.53/0.68 % 0.53/0.68 fof(xsd_string_substitution_1,axiom, % 0.53/0.68 ! [A,B] : % 0.53/0.68 ( ( A = B % 0.53/0.68 & xsd_string(A) ) % 0.53/0.68 => xsd_string(B) ) ). % 0.53/0.68 % 0.53/0.68 %----Thing and Nothing % 0.53/0.68 fof(axiom_0,axiom, % 0.53/0.68 ! [X] : % 0.53/0.68 ( cowlThing(X) % 0.53/0.68 & ~ cowlNothing(X) ) ). % 0.53/0.68 % 0.53/0.68 %----String and Integer disjoint % 0.53/0.68 fof(axiom_1,axiom, % 0.53/0.68 ! [X] : % 0.53/0.68 ( xsd_string(X) % 0.53/0.68 <=> ~ xsd_integer(X) ) ). % 0.53/0.68 % 0.53/0.68 %----Enumeration cA % 0.53/0.68 fof(axiom_2,axiom, % 0.53/0.68 ! [X] : % 0.53/0.68 ( cA(X) % 0.53/0.68 <=> X = ia ) ). % 0.53/0.68 % 0.53/0.68 %----Enumeration cA_and_B % 0.53/0.68 fof(axiom_3,axiom, % 0.53/0.68 ! [X] : % 0.53/0.68 ( cA_and_B(X) % 0.53/0.68 <=> ( X = ib % 0.53/0.68 | X = ia ) ) ). % 0.53/0.68 % 0.53/0.68 %----Enumeration cB % 0.53/0.68 fof(axiom_4,axiom, % 0.53/0.68 ! [X] : % 0.53/0.68 ( cB(X) % 0.53/0.68 <=> X = ib ) ). % 0.53/0.68 % 0.53/0.68 %----ia % 0.53/0.68 fof(axiom_5,axiom, % 0.53/0.68 cowlThing(ia) ). % 0.53/0.68 % 0.53/0.68 %----ib % 0.53/0.68 fof(axiom_6,axiom, % 0.53/0.68 cowlThing(ib) ). % 0.53/0.68 % 0.53/0.68 %----Thing and Nothing % 0.53/0.68 %----String and Integer disjoint % 0.53/0.68 %----Equality cA_and_B % 0.53/0.68 fof(the_axiom,conjecture, % 0.53/0.68 ( ! [X] : % 0.53/0.68 ( cowlThing(X) % 0.53/0.68 & ~ cowlNothing(X) ) % 0.53/0.68 & ! [X] : % 0.53/0.68 ( xsd_string(X) % 0.53/0.68 <=> ~ xsd_integer(X) ) % 0.53/0.68 & ! [X] : % 0.53/0.68 ( cA_and_B(X) % 0.53/0.68 <=> ( cB(X) % 0.53/0.68 | cA(X) ) ) ) ). % 0.53/0.68 % 0.53/0.68 %------------------------------------------------------------------------------ % 0.53/0.68 %------------------------------------------- % 0.53/0.68 % Proof found % 0.53/0.68 % SZS status Theorem for theBenchmark % 0.53/0.68 % SZS output start Proof % 0.53/0.68 %ClaNum:25(EqnAxiom:9) % 0.53/0.68 %VarNum:20(SingletonVarNum:10) % 0.53/0.68 %MaxLitNum:6 % 0.53/0.68 %MaxfuncDepth:0 % 0.53/0.68 %SharedTerms:16 % 0.53/0.68 %goalClause: 20 21 22 23 24 25 % 0.53/0.68 [10]~P1(x101) % 0.53/0.68 [11]P2(x111)+~E(x111,a1) % 0.53/0.68 [12]P3(x121)+~E(x121,a1) % 0.53/0.68 [13]P3(x131)+~E(x131,a5) % 0.53/0.68 [14]P4(x141)+~E(x141,a5) % 0.53/0.68 [15]~P2(x151)+E(x151,a1) % 0.53/0.68 [16]~P4(x161)+E(x161,a5) % 0.53/0.68 [17]P6(x171)+P5(x171) % 0.53/0.68 [19]~P6(x191)+~P5(x191) % 0.53/0.68 [18]~P3(x181)+E(x181,a5)+E(x181,a1) % 0.53/0.68 [22]P1(a3)+P5(a4)+~P2(a2)+~P3(a2)+~P6(a4) % 0.53/0.68 [23]P1(a3)+P5(a4)+~P3(a2)+~P4(a2)+~P6(a4) % 0.53/0.68 [24]P1(a3)+P6(a4)+~P2(a2)+~P3(a2)+~P5(a4) % 0.53/0.68 [25]P1(a3)+P6(a4)+~P3(a2)+~P4(a2)+~P5(a4) % 0.53/0.68 [20]P2(a2)+P3(a2)+P4(a2)+P1(a3)+P5(a4)+~P6(a4) % 0.53/0.68 [21]P2(a2)+P3(a2)+P4(a2)+P1(a3)+P6(a4)+~P5(a4) % 0.53/0.68 %EqnAxiom % 0.53/0.68 [1]E(x11,x11) % 0.53/0.68 [2]E(x22,x21)+~E(x21,x22) % 0.53/0.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.53/0.68 [4]~P1(x41)+P1(x42)+~E(x41,x42) % 0.53/0.68 [5]~P2(x51)+P2(x52)+~E(x51,x52) % 0.53/0.68 [6]~P3(x61)+P3(x62)+~E(x61,x62) % 0.53/0.68 [7]~P4(x71)+P4(x72)+~E(x71,x72) % 0.53/0.68 [8]~P5(x81)+P5(x82)+~E(x81,x82) % 0.53/0.68 [9]~P6(x91)+P6(x92)+~E(x91,x92) % 0.53/0.68 % 0.53/0.68 %------------------------------------------- % 0.53/0.68 cnf(27,plain, % 0.53/0.68 (P3(a1)), % 0.53/0.68 inference(equality_inference,[],[12])). % 0.53/0.68 cnf(29,plain, % 0.53/0.68 (P4(a5)), % 0.53/0.68 inference(equality_inference,[],[14])). % 0.53/0.68 cnf(30,plain, % 0.53/0.68 (~P1(x301)), % 0.53/0.68 inference(rename_variables,[],[10])). % 0.53/0.68 cnf(32,plain, % 0.53/0.68 (P5(a4)+~P6(a4)+~P4(a2)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[10,30,23])). % 0.53/0.68 cnf(33,plain, % 0.53/0.68 (P2(a2)+P3(a2)+P4(a2)+P5(a4)+~P6(a4)), % 0.53/0.68 inference(scs_inference,[],[10,20])). % 0.53/0.68 cnf(34,plain, % 0.53/0.68 (P2(a2)+P3(a2)+P4(a2)+P6(a4)+~P5(a4)), % 0.53/0.68 inference(scs_inference,[],[10,21])). % 0.53/0.68 cnf(35,plain, % 0.53/0.68 (P5(a4)+~P2(a2)+~P3(a2)+~P6(a4)), % 0.53/0.68 inference(scs_inference,[],[10,22])). % 0.53/0.68 cnf(36,plain, % 0.53/0.68 (P6(a4)+~P2(a2)+~P3(a2)+~P5(a4)), % 0.53/0.68 inference(scs_inference,[],[10,24])). % 0.53/0.68 cnf(37,plain, % 0.53/0.68 (P6(a4)+~P3(a2)+~P4(a2)+~P5(a4)), % 0.53/0.68 inference(scs_inference,[],[10,25])). % 0.53/0.68 cnf(41,plain, % 0.53/0.68 (~E(x411,x412)+E(x412,x413)+~E(x413,x411)), % 0.53/0.68 inference(scs_inference,[],[2,3])). % 0.53/0.68 cnf(43,plain, % 0.53/0.68 (~E(x431,x432)+~E(x432,a1)+P3(x431)), % 0.53/0.68 inference(scs_inference,[],[27,6,41])). % 0.53/0.68 cnf(44,plain, % 0.53/0.68 (~E(x441,x442)+~E(x442,a5)+P4(x441)), % 0.53/0.68 inference(scs_inference,[],[29,7,41])). % 0.53/0.68 cnf(50,plain, % 0.53/0.68 (~E(x501,x502)+P6(x501)+P5(x502)), % 0.53/0.68 inference(scs_inference,[],[17,8])). % 0.53/0.68 cnf(54,plain, % 0.53/0.68 (P6(a4)+~P2(a2)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[17,36])). % 0.53/0.68 cnf(55,plain, % 0.53/0.68 (~P5(a4)+~P2(a2)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[54,19])). % 0.53/0.68 cnf(56,plain, % 0.53/0.68 (~P2(a2)+~P3(a2)+~P6(a4)), % 0.53/0.68 inference(scs_inference,[],[55,35])). % 0.53/0.68 cnf(57,plain, % 0.53/0.68 (~E(a2,a1)+~P3(a2)+~P6(a4)), % 0.53/0.68 inference(scs_inference,[],[56,11])). % 0.53/0.68 cnf(58,plain, % 0.53/0.68 (~P3(a2)+E(a2,a5)+~P6(a4)), % 0.53/0.68 inference(scs_inference,[],[57,18])). % 0.53/0.68 cnf(63,plain, % 0.53/0.68 (P5(a4)+~P2(a2)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[17,56])). % 0.53/0.68 cnf(64,plain, % 0.53/0.68 (~P2(a2)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[63,55])). % 0.53/0.68 cnf(65,plain, % 0.53/0.68 (~E(a2,a1)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[64,11])). % 0.53/0.68 cnf(71,plain, % 0.53/0.68 (P6(a4)+~P3(a2)+~P4(a2)), % 0.53/0.68 inference(scs_inference,[],[17,37])). % 0.53/0.68 cnf(72,plain, % 0.53/0.68 (P5(a4)+~P4(a2)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[71,32])). % 0.53/0.68 cnf(85,plain, % 0.53/0.68 (~P5(a4)+~P3(a2)+~P4(a2)), % 0.53/0.68 inference(scs_inference,[],[19,71])). % 0.53/0.68 cnf(86,plain, % 0.53/0.68 (~P4(a2)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[85,72])). % 0.53/0.68 cnf(87,plain, % 0.53/0.68 (~E(a2,a5)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[86,14])). % 0.53/0.68 cnf(88,plain, % 0.53/0.68 (~E(a5,a2)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[87,2])). % 0.53/0.68 cnf(89,plain, % 0.53/0.68 (~E(x891,a2)+~E(a5,x891)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[88,3])). % 0.53/0.68 cnf(90,plain, % 0.53/0.68 (~E(x901,a5)+~E(x901,a2)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[89,2])). % 0.53/0.68 cnf(91,plain, % 0.53/0.68 (~E(a2,x911)+~E(x911,a5)+~P3(a2)), % 0.53/0.68 inference(scs_inference,[],[90,2])). % 0.53/0.68 cnf(92,plain, % 0.53/0.68 (~P3(a2)+~P6(a4)), % 0.53/0.68 inference(scs_inference,[],[91,58])). % 0.53/0.68 cnf(119,plain, % 0.53/0.68 (~E(a2,x1191)+~E(x1191,a1)+~P2(a2)), % 0.53/0.68 inference(scs_inference,[],[64,43])). % 0.53/0.68 cnf(120,plain, % 0.53/0.68 (~E(a1,x1201)+~E(a2,x1201)+~P2(a2)), % 0.53/0.68 inference(scs_inference,[],[119,2])). % 0.53/0.68 cnf(121,plain, % 0.53/0.68 (~P2(a2)), % 0.53/0.68 inference(scs_inference,[],[120,15])). % 0.53/0.68 cnf(122,plain, % 0.53/0.68 (P3(a2)+P4(a2)+P5(a4)+~P6(a4)), % 0.53/0.68 inference(scs_inference,[],[121,33])). % 0.53/0.68 cnf(123,plain, % 0.53/0.68 (P3(a2)+P4(a2)+P6(a4)+~P5(a4)), % 0.53/0.68 inference(scs_inference,[],[121,34])). % 0.53/0.68 cnf(134,plain, % 0.53/0.68 (~E(a2,a5)+~P4(a2)), % 0.53/0.68 inference(scs_inference,[],[86,13])). % 0.53/0.68 cnf(135,plain, % 0.53/0.68 (~E(a5,a2)+~P4(a2)), % 0.53/0.68 inference(scs_inference,[],[134,2])). % 0.53/0.68 cnf(136,plain, % 0.53/0.68 (~E(x1361,a2)+~E(a5,x1361)+~P4(a2)), % 0.53/0.68 inference(scs_inference,[],[135,3])). % 0.53/0.68 cnf(137,plain, % 0.53/0.68 (~E(x1371,a5)+~E(x1371,a2)+~P4(a2)), % 0.53/0.68 inference(scs_inference,[],[136,2])). % 0.53/0.68 cnf(138,plain, % 0.53/0.68 (~E(a2,x1381)+~E(x1381,a5)+~P4(a2)), % 0.53/0.68 inference(scs_inference,[],[137,2])). % 0.53/0.68 cnf(139,plain, % 0.53/0.68 (~E(a5,x1391)+~E(a2,x1391)+~P4(a2)), % 0.53/0.68 inference(scs_inference,[],[138,2])). % 0.53/0.68 cnf(140,plain, % 0.53/0.68 (~P4(a2)), % 0.53/0.68 inference(scs_inference,[],[139,16])). % 0.53/0.68 cnf(141,plain, % 0.53/0.68 (P3(a2)+P5(a4)+~P6(a4)), % 0.53/0.68 inference(scs_inference,[],[140,122])). % 0.53/0.68 cnf(142,plain, % 0.53/0.68 (P3(a2)+P6(a4)+~P5(a4)), % 0.53/0.68 inference(scs_inference,[],[140,123])). % 0.53/0.68 cnf(144,plain, % 0.53/0.68 (~E(a2,a1)+P6(a4)+~P5(a4)), % 0.53/0.68 inference(scs_inference,[],[142,65])). % 0.53/0.68 cnf(146,plain, % 0.53/0.68 (~E(a1,a2)+P6(a4)+~P5(a4)), % 0.53/0.69 inference(scs_inference,[],[144,2])). % 0.53/0.69 cnf(149,plain, % 0.53/0.69 (~P5(a4)+~E(a1,a2)), % 0.53/0.69 inference(scs_inference,[],[146,19])). % 0.53/0.69 cnf(150,plain, % 0.53/0.69 (~E(a2,a1)+~P5(a4)), % 0.53/0.69 inference(scs_inference,[],[149,2])). % 0.53/0.69 cnf(151,plain, % 0.53/0.69 (~P3(a2)+E(a2,a5)+~P5(a4)), % 0.53/0.69 inference(scs_inference,[],[150,18])). % 0.53/0.69 cnf(157,plain, % 0.53/0.69 (~P3(a2)+~P5(a4)), % 0.53/0.69 inference(scs_inference,[],[140,151,44])). % 0.53/0.69 cnf(161,plain, % 0.53/0.69 (P5(a4)+~P3(a2)), % 0.53/0.69 inference(scs_inference,[],[92,17])). % 0.53/0.69 cnf(162,plain, % 0.53/0.69 (~P3(a2)), % 0.53/0.69 inference(scs_inference,[],[161,157])). % 0.53/0.69 cnf(163,plain, % 0.53/0.69 (P5(a4)+~P6(a4)), % 0.53/0.69 inference(scs_inference,[],[162,141])). % 0.53/0.69 cnf(164,plain, % 0.53/0.69 (P6(a4)+~P5(a4)), % 0.53/0.69 inference(scs_inference,[],[162,142])). % 0.53/0.69 cnf(165,plain, % 0.53/0.69 (~P6(a4)), % 0.53/0.69 inference(scs_inference,[],[163,19])). % 0.53/0.69 cnf(166,plain, % 0.53/0.69 (~P5(a4)), % 0.53/0.69 inference(scs_inference,[],[165,164])). % 0.53/0.69 cnf(167,plain, % 0.53/0.69 (P5(x1671)+~E(a4,x1671)), % 0.53/0.69 inference(scs_inference,[],[165,50])). % 0.53/0.69 cnf(177,plain, % 0.53/0.69 (P5(a4)), % 0.53/0.69 inference(equality_inference,[],[167])). % 0.53/0.69 cnf(179,plain, % 0.53/0.69 ($false), % 0.53/0.69 inference(scs_inference,[],[166,177]), % 0.53/0.69 ['proof']). % 0.53/0.69 % SZS output end Proof % 0.53/0.69 % Total time :0.160000s %------------------------------------------------------------------------------