%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS131+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 : n009.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:37 EDT 2024 % Result : Theorem 0.52s 0.69s % Output : CNFRefutation 0.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS131+1 : TPTP v8.2.0. Released v3.1.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n009.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:32:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.45/0.56 start to proof:theBenchmark % 0.51/0.68 %------------------------------------------- % 0.51/0.68 % File :CSE---1.7 % 0.51/0.68 % Problem :theBenchmark % 0.51/0.68 % Transform :cnf % 0.51/0.68 % Format :tptp:raw % 0.51/0.68 % Command :java -jar mcs_scs.jar %d %s % 0.51/0.68 % 0.51/0.69 % Result :Theorem 0.080000s % 0.51/0.69 % Output :CNFRefutation 0.080000s % 0.51/0.69 %------------------------------------------- % 0.51/0.69 %------------------------------------------------------------------------------ % 0.51/0.69 % File : KRS131+1 : TPTP v8.2.0. Released v3.1.0. % 0.51/0.69 % Domain : Knowledge Representation (Semantic Web) % 0.51/0.69 % Problem : The complement of a class can be defined % 0.51/0.69 % Version : Especial. % 0.51/0.69 % English : The complement of a class can be defined using OWL Lite % 0.51/0.69 % restrictions. % 0.51/0.69 % 0.51/0.69 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 0.51/0.69 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 0.51/0.69 % Source : [Bec03] % 0.51/0.69 % Names : positive_I5.2-Manifest004 [Bec03] % 0.51/0.69 % 0.51/0.69 % Status : Theorem % 0.51/0.69 % Rating : 0.00 v8.2.0, 0.07 v8.1.0, 0.00 v6.3.0, 0.08 v6.2.0, 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.12 v5.4.0, 0.13 v5.2.0, 0.07 v5.0.0, 0.05 v4.1.0, 0.06 v4.0.1, 0.05 v3.7.0, 0.33 v3.5.0, 0.12 v3.4.0, 0.08 v3.3.0, 0.00 v3.2.0, 0.22 v3.1.0 % 0.51/0.69 % Syntax : Number of formulae : 7 ( 0 unt; 0 def) % 0.51/0.69 % Number of atoms : 20 ( 0 equ) % 0.51/0.69 % Maximal formula atoms : 6 ( 2 avg) % 0.51/0.69 % Number of connectives : 19 ( 6 ~; 0 |; 5 &) % 0.51/0.69 % ( 5 <=>; 3 =>; 0 <=; 0 <~>) % 0.51/0.69 % Maximal formula depth : 6 ( 5 avg) % 0.51/0.69 % Maximal term depth : 1 ( 1 avg) % 0.51/0.69 % Number of predicates : 9 ( 9 usr; 0 prp; 1-2 aty) % 0.51/0.69 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 0.51/0.69 % Number of variables : 13 ( 10 !; 3 ?) % 0.51/0.69 % SPC : FOF_THM_RFO_NEQ % 0.51/0.69 % 0.51/0.69 % Comments : Sean Bechhofer says there are some errors in the encoding of % 0.51/0.69 % datatypes, so this problem may not be perfect. At least it's % 0.51/0.69 % still representative of the type of reasoning required for OWL. % 0.51/0.69 %------------------------------------------------------------------------------ % 0.51/0.69 %----Thing and Nothing % 0.51/0.69 fof(axiom_0,axiom, % 0.51/0.69 ! [X] : % 0.51/0.69 ( cowlThing(X) % 0.51/0.69 & ~ cowlNothing(X) ) ). % 0.51/0.69 % 0.51/0.69 %----String and Integer disjoint % 0.51/0.69 fof(axiom_1,axiom, % 0.51/0.69 ! [X] : % 0.51/0.69 ( xsd_string(X) % 0.51/0.69 <=> ~ xsd_integer(X) ) ). % 0.51/0.69 % 0.51/0.69 %----Equality cA % 0.51/0.69 fof(axiom_2,axiom, % 0.52/0.69 ! [X] : % 0.52/0.69 ( cA(X) % 0.52/0.69 <=> ? [Y] : % 0.52/0.69 ( rq(X,Y) % 0.52/0.69 & cowlThing(Y) ) ) ). % 0.52/0.69 % 0.52/0.69 %----Super cNothing % 0.52/0.69 fof(axiom_3,axiom, % 0.52/0.69 ! [X] : % 0.52/0.69 ( cNothing(X) % 0.52/0.69 => ~ ? [Y] : rp(X,Y) ) ). % 0.52/0.69 % 0.52/0.69 %----Super cNothing % 0.52/0.69 fof(axiom_4,axiom, % 0.52/0.69 ! [X] : % 0.52/0.69 ( cNothing(X) % 0.52/0.69 => ? [Y0] : rp(X,Y0) ) ). % 0.52/0.69 % 0.52/0.69 %----Equality cnotA % 0.52/0.69 fof(axiom_5,axiom, % 0.52/0.69 ! [X] : % 0.52/0.69 ( cnotA(X) % 0.52/0.69 <=> ! [Y] : % 0.52/0.69 ( rq(X,Y) % 0.52/0.69 => cNothing(Y) ) ) ). % 0.52/0.69 % 0.52/0.69 %----Thing and Nothing % 0.52/0.69 %----String and Integer disjoint % 0.52/0.69 %----Equality cnotA % 0.52/0.69 fof(the_axiom,conjecture, % 0.52/0.69 ( ! [X] : % 0.52/0.69 ( cowlThing(X) % 0.52/0.69 & ~ cowlNothing(X) ) % 0.52/0.69 & ! [X] : % 0.52/0.69 ( xsd_string(X) % 0.52/0.69 <=> ~ xsd_integer(X) ) % 0.52/0.69 & ! [X] : % 0.52/0.69 ( cnotA(X) % 0.52/0.69 <=> ~ cA(X) ) ) ). % 0.52/0.69 % 0.52/0.69 %------------------------------------------------------------------------------ % 0.52/0.69 %------------------------------------------- % 0.52/0.69 % Proof found % 0.52/0.69 % SZS status Theorem for theBenchmark % 0.52/0.69 % SZS output start Proof % 0.52/0.69 %ClaNum:14(EqnAxiom:0) % 0.52/0.69 %VarNum:26(SingletonVarNum:13) % 0.52/0.69 %MaxLitNum:5 % 0.52/0.69 %MaxfuncDepth:1 % 0.52/0.69 %SharedTerms:12 % 0.52/0.69 %goalClause: 4 5 6 7 % 0.52/0.69 [1]~P1(x11) % 0.52/0.69 [2]P6(x21)+P5(x21) % 0.52/0.69 [3]~P6(x31)+~P5(x31) % 0.52/0.69 [8]P3(x81)+~P4(f2(x81)) % 0.52/0.69 [9]P3(x91)+P7(x91,f2(x91)) % 0.52/0.69 [11]~P2(x111)+P7(x111,f3(x111)) % 0.52/0.69 [12]~P4(x121)+P8(x121,f4(x121)) % 0.52/0.69 [10]P2(x101)+~P7(x101,x102) % 0.52/0.69 [13]~P4(x131)+~P8(x131,x132) % 0.52/0.69 [14]~P7(x142,x141)+P4(x141)+~P3(x142) % 0.52/0.69 [4]P1(a1)+P5(a5)+P2(a6)+~P6(a5)+~P3(a6) % 0.52/0.69 [5]P1(a1)+P5(a5)+P3(a6)+~P6(a5)+~P2(a6) % 0.52/0.69 [6]P1(a1)+P6(a5)+P2(a6)+~P5(a5)+~P3(a6) % 0.52/0.69 [7]P1(a1)+P6(a5)+P3(a6)+~P5(a5)+~P2(a6) % 0.52/0.69 %EqnAxiom % 0.52/0.69 % 0.52/0.69 %------------------------------------------- % 0.52/0.70 cnf(15,plain, % 0.52/0.70 (~P1(x151)), % 0.52/0.70 inference(rename_variables,[],[1])). % 0.52/0.70 cnf(17,plain, % 0.52/0.70 (P5(a5)+~P2(a6)+~P6(a5)+P3(a6)), % 0.52/0.70 inference(scs_inference,[],[1,15,5])). % 0.52/0.70 cnf(18,plain, % 0.52/0.70 (P5(a5)+P2(a6)+~P6(a5)+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[1,4])). % 0.52/0.70 cnf(19,plain, % 0.52/0.70 (P6(a5)+P2(a6)+~P5(a5)+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[1,6])). % 0.52/0.70 cnf(20,plain, % 0.52/0.70 (P6(a5)+P3(a6)+~P5(a5)+~P2(a6)), % 0.52/0.70 inference(scs_inference,[],[1,7])). % 0.52/0.70 cnf(30,plain, % 0.52/0.70 (P6(a5)+P2(a6)+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[2,19])). % 0.52/0.70 cnf(31,plain, % 0.52/0.70 (~P5(a5)+P2(a6)+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[30,3])). % 0.52/0.70 cnf(32,plain, % 0.52/0.70 (P2(a6)+~P6(a5)+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[31,18])). % 0.52/0.70 cnf(33,plain, % 0.52/0.70 (P7(a6,f3(a6))+~P3(a6)+~P6(a5)), % 0.52/0.70 inference(scs_inference,[],[32,11])). % 0.52/0.70 cnf(34,plain, % 0.52/0.70 (P4(f3(a6))+~P3(a6)+~P6(a5)), % 0.52/0.70 inference(scs_inference,[],[33,14])). % 0.52/0.70 cnf(35,plain, % 0.52/0.70 (P8(f3(a6),f4(f3(a6)))+~P3(a6)+~P6(a5)), % 0.52/0.70 inference(scs_inference,[],[34,12])). % 0.52/0.70 cnf(36,plain, % 0.52/0.70 (~P4(f3(a6))+~P3(a6)+~P6(a5)), % 0.52/0.70 inference(scs_inference,[],[35,13])). % 0.52/0.70 cnf(37,plain, % 0.52/0.70 (~P3(a6)+~P6(a5)), % 0.52/0.70 inference(scs_inference,[],[36,34])). % 0.52/0.70 cnf(40,plain, % 0.52/0.70 (P5(a5)+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[2,37])). % 0.52/0.70 cnf(41,plain, % 0.52/0.70 (P2(a6)+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[40,31])). % 0.52/0.70 cnf(42,plain, % 0.52/0.70 (P7(a6,f3(a6))+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[41,11])). % 0.52/0.70 cnf(43,plain, % 0.52/0.70 (P4(f3(a6))+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[42,14])). % 0.52/0.70 cnf(44,plain, % 0.52/0.70 (P8(f3(a6),f4(f3(a6)))+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[43,12])). % 0.52/0.70 cnf(45,plain, % 0.52/0.70 (~P4(f3(a6))+~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[44,13])). % 0.52/0.70 cnf(46,plain, % 0.52/0.70 (~P3(a6)), % 0.52/0.70 inference(scs_inference,[],[45,43])). % 0.52/0.70 cnf(47,plain, % 0.52/0.70 (P5(a5)+~P2(a6)+~P6(a5)), % 0.52/0.70 inference(scs_inference,[],[46,17])). % 0.52/0.70 cnf(48,plain, % 0.52/0.70 (P6(a5)+~P5(a5)+~P2(a6)), % 0.52/0.70 inference(scs_inference,[],[46,20])). % 0.52/0.70 cnf(49,plain, % 0.52/0.70 (~P6(a5)+~P2(a6)), % 0.52/0.70 inference(scs_inference,[],[47,3])). % 0.52/0.70 cnf(50,plain, % 0.52/0.70 (P5(a5)+~P2(a6)), % 0.52/0.70 inference(scs_inference,[],[49,2])). % 0.52/0.70 cnf(51,plain, % 0.52/0.70 (P6(a5)+~P2(a6)), % 0.52/0.70 inference(scs_inference,[],[50,48])). % 0.52/0.70 cnf(59,plain, % 0.52/0.70 (~P5(a5)+~P2(a6)), % 0.52/0.70 inference(scs_inference,[],[3,51])). % 0.52/0.70 cnf(60,plain, % 0.52/0.70 (~P2(a6)), % 0.52/0.70 inference(scs_inference,[],[59,50])). % 0.52/0.70 cnf(63,plain, % 0.52/0.70 ($false), % 0.52/0.70 inference(scs_inference,[],[46,60,10,9]), % 0.52/0.70 ['proof']). % 0.52/0.70 % SZS output end Proof % 0.52/0.70 % Total time :0.080000s %------------------------------------------------------------------------------