%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB029+2 : TPTP v8.2.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n004.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 16:05:30 EDT 2024 % Result : Theorem 0.50s 0.60s % Output : CNFRefutation 0.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWB029+2 : TPTP v8.2.0. Released v5.2.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.34 % Computer : n004.cluster.edu % 0.11/0.34 % Model : x86_64 x86_64 % 0.11/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.34 % Memory : 8042.1875MB % 0.11/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.34 % CPULimit : 300 % 0.11/0.34 % WCLimit : 300 % 0.11/0.34 % DateTime : Tue Jun 18 17:57:38 EDT 2024 % 0.11/0.35 % CPUTime : % 0.47/0.56 start to proof:theBenchmark % 0.50/0.60 %------------------------------------------- % 0.50/0.60 % File :CSE---1.7 % 0.50/0.60 % Problem :theBenchmark % 0.50/0.60 % Transform :cnf % 0.50/0.60 % Format :tptp:raw % 0.50/0.60 % Command :java -jar mcs_scs.jar %d %s % 0.50/0.60 % 0.50/0.60 % Result :Theorem 0.000000s % 0.50/0.60 % Output :CNFRefutation 0.000000s % 0.50/0.60 %------------------------------------------- % 0.50/0.60 %------------------------------------------------------------------------------ % 0.50/0.60 % File : SWB029+2 : TPTP v8.2.0. Released v5.2.0. % 0.50/0.60 % Domain : Semantic Web % 0.50/0.60 % Problem : Ex Falso Quodlibet % 0.50/0.60 % Version : [Sch11] axioms : Reduced > Incomplete. % 0.50/0.60 % English : % 0.50/0.60 % 0.50/0.60 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 0.50/0.60 % Source : [Sch11] % 0.50/0.60 % Names : 029_Ex_Falso_Quodlibet [Sch11] % 0.50/0.60 % 0.50/0.60 % Status : ContradictoryAxioms % 0.50/0.60 % Rating : 0.06 v8.2.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v6.1.0, 0.08 v6.0.0, 0.50 v5.5.0, 0.08 v5.4.0, 0.09 v5.3.0, 0.17 v5.2.0 % 0.50/0.60 % Syntax : Number of formulae : 5 ( 1 unt; 0 def) % 0.50/0.60 % Number of atoms : 28 ( 0 equ) % 0.50/0.60 % Maximal formula atoms : 11 ( 5 avg) % 0.50/0.60 % Number of connectives : 24 ( 1 ~; 0 |; 17 &) % 0.50/0.60 % ( 4 <=>; 2 =>; 0 <=; 0 <~>) % 0.50/0.60 % Maximal formula depth : 14 ( 8 avg) % 0.50/0.60 % Maximal term depth : 1 ( 1 avg) % 0.50/0.60 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 0.50/0.60 % Number of functors : 10 ( 10 usr; 10 con; 0-0 aty) % 0.50/0.60 % Number of variables : 15 ( 11 !; 4 ?) % 0.50/0.60 % SPC : FOF_CAX_RFO_NEQ % 0.50/0.60 % 0.50/0.60 % Comments : % 0.50/0.60 %------------------------------------------------------------------------------ % 0.50/0.60 fof(rdfs_cext_def,axiom, % 0.50/0.60 ! [X,C] : % 0.50/0.60 ( iext(uri_rdf_type,X,C) % 0.50/0.60 <=> icext(C,X) ) ). % 0.50/0.60 % 0.50/0.60 fof(owl_bool_complementof_class,axiom, % 0.50/0.60 ! [Z,C] : % 0.50/0.60 ( iext(uri_owl_complementOf,Z,C) % 0.50/0.60 => ( ic(Z) % 0.50/0.60 & ic(C) % 0.50/0.60 & ! [X] : % 0.50/0.60 ( icext(Z,X) % 0.50/0.60 <=> ~ icext(C,X) ) ) ) ). % 0.50/0.60 % 0.50/0.60 fof(owl_bool_intersectionof_class_002,axiom, % 0.50/0.60 ! [Z,S1,C1,S2,C2] : % 0.50/0.60 ( ( iext(uri_rdf_first,S1,C1) % 0.50/0.60 & iext(uri_rdf_rest,S1,S2) % 0.50/0.60 & iext(uri_rdf_first,S2,C2) % 0.50/0.60 & iext(uri_rdf_rest,S2,uri_rdf_nil) ) % 0.50/0.60 => ( iext(uri_owl_intersectionOf,Z,S1) % 0.50/0.60 <=> ( ic(Z) % 0.50/0.60 & ic(C1) % 0.50/0.60 & ic(C2) % 0.50/0.60 & ! [X] : % 0.50/0.60 ( icext(Z,X) % 0.50/0.60 <=> ( icext(C1,X) % 0.50/0.60 & icext(C2,X) ) ) ) ) ) ). % 0.50/0.60 % 0.50/0.60 fof(testcase_conclusion_fullish_029_Ex_Falso_Quodlibet,conjecture, % 0.50/0.60 iext(uri_rdf_type,uri_ex_w,uri_ex_B) ). % 0.50/0.60 % 0.50/0.60 fof(testcase_premise_fullish_029_Ex_Falso_Quodlibet,axiom, % 0.50/0.60 ? [BNODE_x,BNODE_y,BNODE_l1,BNODE_l2] : % 0.50/0.60 ( iext(uri_rdf_type,uri_ex_A,uri_owl_Class) % 0.50/0.60 & iext(uri_rdf_type,uri_ex_B,uri_owl_Class) % 0.50/0.60 & iext(uri_rdf_type,uri_ex_w,BNODE_x) % 0.50/0.60 & iext(uri_owl_intersectionOf,BNODE_x,BNODE_l1) % 0.50/0.60 & iext(uri_rdf_first,BNODE_l1,uri_ex_A) % 0.50/0.60 & iext(uri_rdf_rest,BNODE_l1,BNODE_l2) % 0.50/0.60 & iext(uri_rdf_first,BNODE_l2,BNODE_y) % 0.50/0.60 & iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil) % 0.50/0.60 & iext(uri_owl_complementOf,BNODE_y,uri_ex_A) ) ). % 0.50/0.60 % 0.50/0.60 %------------------------------------------------------------------------------ % 0.50/0.60 %------------------------------------------- % 0.50/0.60 % Proof found % 0.50/0.60 % SZS status Theorem for theBenchmark % 0.50/0.60 % SZS output start Proof % 0.50/0.60 %ClaNum:25(EqnAxiom:0) % 0.50/0.60 %VarNum:175(SingletonVarNum:62) % 0.50/0.60 %MaxLitNum:11 % 0.50/0.60 %MaxfuncDepth:1 % 0.50/0.60 %SharedTerms:24 % 0.50/0.60 %goalClause: 10 % 0.50/0.60 %singleGoalClaCount:1 % 0.50/0.61 [1]P1(a1,a2,a3) % 0.50/0.61 [2]P1(a1,a5,a10) % 0.50/0.61 [3]P1(a1,a6,a10) % 0.50/0.61 [4]P1(a11,a7,a6) % 0.50/0.61 [5]P1(a12,a8,a6) % 0.50/0.61 [6]P1(a12,a9,a7) % 0.50/0.61 [7]P1(a14,a8,a9) % 0.50/0.61 [8]P1(a14,a9,a15) % 0.50/0.61 [9]P1(a13,a3,a8) % 0.50/0.61 [10]~P1(a1,a2,a5) % 0.50/0.61 [11]~P2(x112,x111)+P1(a1,x111,x112) % 0.50/0.61 [12]P3(x121)+~P1(a11,x122,x121) % 0.50/0.61 [13]P3(x131)+~P1(a11,x131,x132) % 0.50/0.61 [14]P2(x141,x142)+~P1(a1,x142,x141) % 0.50/0.61 [15]P2(x151,x152)+P2(x153,x152)+~P1(a11,x151,x153) % 0.50/0.61 [16]~P2(x161,x162)+~P2(x163,x162)+~P1(a11,x163,x161) % 0.50/0.61 [17]P3(x171)+~P1(a14,x173,x172)+~P1(a12,x172,x171)+~P1(a12,x173,x174)+~P1(a13,x175,x173)+~P1(a14,x172,a15) % 0.50/0.61 [18]P3(x181)+~P1(a14,x184,x182)+~P1(a12,x182,x183)+~P1(a12,x184,x181)+~P1(a13,x185,x184)+~P1(a14,x182,a15) % 0.50/0.61 [19]P3(x191)+~P1(a14,x194,x192)+~P1(a13,x191,x194)+~P1(a12,x192,x193)+~P1(a12,x194,x195)+~P1(a14,x192,a15) % 0.50/0.61 [20]P2(x201,x202)+~P2(x203,x202)+~P1(a14,x205,x204)+~P1(a13,x203,x205)+~P1(a12,x204,x201)+~P1(a12,x205,x206)+~P1(a14,x204,a15) % 0.50/0.61 [21]P2(x211,x212)+~P2(x213,x212)+~P1(a14,x216,x214)+~P1(a13,x213,x216)+~P1(a12,x214,x215)+~P1(a12,x216,x211)+~P1(a14,x214,a15) % 0.50/0.61 [22]P2(x221,x222)+~P2(x223,x222)+~P2(x224,x222)+~P1(a14,x226,x225)+~P1(a13,x221,x226)+~P1(a12,x225,x223)+~P1(a12,x226,x224)+~P1(a14,x225,a15) % 0.50/0.61 [23]~P3(x233)+~P3(x231)+~P3(x235)+~P1(a12,x234,x235)+~P1(a12,x232,x233)+~P1(a14,x232,x234)+P1(a13,x231,x232)+P2(x231,f4(x231,x232,x233,x234,x235))+P2(x235,f4(x231,x232,x233,x234,x235))+~P1(a14,x234,a15) % 0.50/0.61 [24]~P3(x245)+~P3(x241)+~P3(x243)+~P1(a12,x244,x245)+~P1(a12,x242,x243)+~P1(a14,x242,x244)+P1(a13,x241,x242)+P2(x241,f4(x241,x242,x243,x244,x245))+P2(x243,f4(x241,x242,x243,x244,x245))+~P1(a14,x244,a15) % 0.50/0.61 [25]~P3(x251)+~P3(x253)+~P3(x254)+~P1(a12,x252,x254)+~P1(a14,x252,x255)+P1(a13,x251,x252)+~P1(a12,x255,x253)+~P2(x253,f4(x251,x252,x254,x255,x253))+~P2(x254,f4(x251,x252,x254,x255,x253))+~P2(x251,f4(x251,x252,x254,x255,x253))+~P1(a14,x255,a15) % 0.50/0.61 %EqnAxiom % 0.50/0.61 % 0.50/0.61 %------------------------------------------- % 0.50/0.61 cnf(36,plain, % 0.50/0.61 (P2(a7,a2)), % 0.50/0.61 inference(scs_inference,[],[10,1,4,5,6,7,8,9,11,14,12,13,19,20])). % 0.50/0.61 cnf(38,plain, % 0.50/0.61 (P2(a6,a2)), % 0.50/0.61 inference(scs_inference,[],[10,1,4,5,6,7,8,9,11,14,12,13,19,20,21])). % 0.50/0.61 cnf(47,plain, % 0.50/0.61 ($false), % 0.50/0.61 inference(scs_inference,[],[36,38,2,4,14,16]), % 0.50/0.61 ['proof']). % 0.50/0.61 % SZS output end Proof % 0.50/0.61 % Total time :0.000000s %------------------------------------------------------------------------------