%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWB020+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 : n025.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:24 EDT 2024 % Result : Theorem 0.56s 0.75s % Output : CNFRefutation 0.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB020+2 : TPTP v8.2.0. Released v5.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n025.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Jun 18 18:07:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.56/0.58 start to proof:theBenchmark % 0.56/0.74 %------------------------------------------- % 0.56/0.74 % File :CSE---1.7 % 0.56/0.74 % Problem :theBenchmark % 0.56/0.74 % Transform :cnf % 0.56/0.74 % Format :tptp:raw % 0.56/0.74 % Command :java -jar mcs_scs.jar %d %s % 0.56/0.74 % 0.56/0.74 % Result :Theorem 0.110000s % 0.56/0.74 % Output :CNFRefutation 0.110000s % 0.56/0.74 %------------------------------------------- % 0.56/0.74 %------------------------------------------------------------------------------ % 0.56/0.74 % File : SWB020+2 : TPTP v8.2.0. Released v5.2.0. % 0.56/0.74 % Domain : Semantic Web % 0.56/0.74 % Problem : Logical Complications % 0.56/0.74 % Version : [Sch11] axioms : Reduced > Incomplete. % 0.56/0.74 % English : % 0.56/0.74 % 0.56/0.74 % Refs : [Sch11] Schneider, M. (2011), Email to G. Sutcliffe % 0.56/0.74 % Source : [Sch11] % 0.56/0.74 % Names : 020_Logical_Complications [Sch11] % 0.56/0.74 % 0.56/0.74 % Status : Theorem % 0.56/0.74 % Rating : 0.06 v8.2.0, 0.13 v8.1.0, 0.21 v7.5.0, 0.24 v7.4.0, 0.19 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.29 v6.3.0, 0.23 v6.2.0, 0.36 v6.1.0, 0.44 v6.0.0, 0.50 v5.4.0, 0.52 v5.3.0, 0.65 v5.2.0 % 0.56/0.74 % Syntax : Number of formulae : 8 ( 1 unt; 0 def) % 0.56/0.74 % Number of atoms : 60 ( 0 equ) % 0.56/0.74 % Maximal formula atoms : 15 ( 7 avg) % 0.56/0.74 % Number of connectives : 54 ( 2 ~; 2 |; 38 &) % 0.56/0.74 % ( 7 <=>; 5 =>; 0 <=; 0 <~>) % 0.56/0.74 % Maximal formula depth : 22 ( 11 avg) % 0.56/0.74 % Maximal term depth : 1 ( 1 avg) % 0.56/0.74 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty) % 0.56/0.74 % Number of functors : 13 ( 13 usr; 13 con; 0-0 aty) % 0.56/0.74 % Number of variables : 32 ( 25 !; 7 ?) % 0.56/0.74 % SPC : FOF_THM_RFO_NEQ % 0.56/0.74 % 0.56/0.74 % Comments : % 0.56/0.74 %------------------------------------------------------------------------------ % 0.56/0.74 fof(owl_prop_disjointwith_ext,axiom, % 0.56/0.74 ! [X,Y] : % 0.56/0.74 ( iext(uri_owl_disjointWith,X,Y) % 0.56/0.74 => ( ic(X) % 0.56/0.74 & ic(Y) ) ) ). % 0.56/0.74 % 0.56/0.74 fof(owl_bool_complementof_class,axiom, % 0.56/0.74 ! [Z,C] : % 0.56/0.74 ( iext(uri_owl_complementOf,Z,C) % 0.56/0.74 => ( ic(Z) % 0.56/0.74 & ic(C) % 0.56/0.74 & ! [X] : % 0.56/0.74 ( icext(Z,X) % 0.56/0.74 <=> ~ icext(C,X) ) ) ) ). % 0.56/0.74 % 0.56/0.74 fof(owl_bool_intersectionof_class_002,axiom, % 0.56/0.74 ! [Z,S1,C1,S2,C2] : % 0.56/0.74 ( ( iext(uri_rdf_first,S1,C1) % 0.56/0.74 & iext(uri_rdf_rest,S1,S2) % 0.56/0.74 & iext(uri_rdf_first,S2,C2) % 0.56/0.74 & iext(uri_rdf_rest,S2,uri_rdf_nil) ) % 0.56/0.74 => ( iext(uri_owl_intersectionOf,Z,S1) % 0.56/0.74 <=> ( ic(Z) % 0.56/0.74 & ic(C1) % 0.56/0.74 & ic(C2) % 0.56/0.74 & ! [X] : % 0.56/0.74 ( icext(Z,X) % 0.56/0.74 <=> ( icext(C1,X) % 0.56/0.74 & icext(C2,X) ) ) ) ) ) ). % 0.56/0.74 % 0.56/0.74 fof(owl_bool_unionof_class_003,axiom, % 0.56/0.74 ! [Z,S1,C1,S2,C2,S3,C3] : % 0.56/0.74 ( ( iext(uri_rdf_first,S1,C1) % 0.56/0.74 & iext(uri_rdf_rest,S1,S2) % 0.56/0.74 & iext(uri_rdf_first,S2,C2) % 0.56/0.74 & iext(uri_rdf_rest,S2,S3) % 0.56/0.74 & iext(uri_rdf_first,S3,C3) % 0.56/0.74 & iext(uri_rdf_rest,S3,uri_rdf_nil) ) % 0.56/0.74 => ( iext(uri_owl_unionOf,Z,S1) % 0.56/0.74 <=> ( ic(Z) % 0.56/0.74 & ic(C1) % 0.56/0.74 & ic(C2) % 0.56/0.74 & ic(C3) % 0.56/0.74 & ! [X] : % 0.56/0.74 ( icext(Z,X) % 0.56/0.74 <=> ( icext(C1,X) % 0.56/0.74 | icext(C2,X) % 0.56/0.74 | icext(C3,X) ) ) ) ) ) ). % 0.56/0.74 % 0.56/0.74 fof(owl_rdfsext_subclassof,axiom, % 0.56/0.74 ! [C1,C2] : % 0.56/0.74 ( iext(uri_rdfs_subClassOf,C1,C2) % 0.56/0.74 <=> ( ic(C1) % 0.56/0.74 & ic(C2) % 0.56/0.74 & ! [X] : % 0.56/0.74 ( icext(C1,X) % 0.56/0.74 => icext(C2,X) ) ) ) ). % 0.56/0.74 % 0.56/0.74 fof(owl_eqdis_disjointwith,axiom, % 0.56/0.74 ! [C1,C2] : % 0.56/0.75 ( iext(uri_owl_disjointWith,C1,C2) % 0.56/0.75 <=> ( ic(C1) % 0.56/0.75 & ic(C2) % 0.56/0.75 & ! [X] : % 0.56/0.75 ~ ( icext(C1,X) % 0.56/0.75 & icext(C2,X) ) ) ) ). % 0.56/0.75 % 0.56/0.75 fof(testcase_conclusion_fullish_020_Logical_Complications,conjecture, % 0.56/0.75 iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3) ). % 0.56/0.75 % 0.56/0.75 fof(testcase_premise_fullish_020_Logical_Complications,axiom, % 0.56/0.75 ? [BNODE_xs,BNODE_xc,BNODE_lu1,BNODE_lu2,BNODE_lu3,BNODE_li1,BNODE_li2] : % 0.56/0.75 ( iext(uri_owl_unionOf,uri_ex_c,BNODE_lu1) % 0.56/0.75 & iext(uri_rdf_first,BNODE_lu1,uri_ex_c1) % 0.56/0.75 & iext(uri_rdf_rest,BNODE_lu1,BNODE_lu2) % 0.56/0.75 & iext(uri_rdf_first,BNODE_lu2,uri_ex_c2) % 0.56/0.75 & iext(uri_rdf_rest,BNODE_lu2,BNODE_lu3) % 0.56/0.75 & iext(uri_rdf_first,BNODE_lu3,uri_ex_c3) % 0.56/0.75 & iext(uri_rdf_rest,BNODE_lu3,uri_rdf_nil) % 0.56/0.75 & iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1) % 0.56/0.75 & iext(uri_rdfs_subClassOf,uri_ex_d,BNODE_xs) % 0.56/0.75 & iext(uri_owl_intersectionOf,BNODE_xs,BNODE_li1) % 0.56/0.75 & iext(uri_rdf_first,BNODE_li1,uri_ex_c) % 0.56/0.75 & iext(uri_rdf_rest,BNODE_li1,BNODE_li2) % 0.56/0.75 & iext(uri_rdf_first,BNODE_li2,BNODE_xc) % 0.56/0.75 & iext(uri_rdf_rest,BNODE_li2,uri_rdf_nil) % 0.56/0.75 & iext(uri_owl_complementOf,BNODE_xc,uri_ex_c2) ) ). % 0.56/0.75 % 0.56/0.75 %------------------------------------------------------------------------------ % 0.56/0.75 %------------------------------------------- % 0.56/0.75 % Proof found % 0.56/0.75 % SZS status Theorem for theBenchmark % 0.56/0.75 % SZS output start Proof % 0.56/0.75 %ClaNum:53(EqnAxiom:0) % 0.56/0.75 %VarNum:495(SingletonVarNum:168) % 0.56/0.75 %MaxLitNum:15 % 0.56/0.75 %MaxfuncDepth:1 % 0.56/0.75 %SharedTerms:36 % 0.56/0.75 %goalClause: 16 % 0.56/0.75 %singleGoalClaCount:1 % 0.56/0.75 [1]P1(a1,a2,a3) % 0.56/0.75 [2]P1(a18,a4,a16) % 0.56/0.75 [3]P1(a19,a12,a3) % 0.56/0.75 [4]P1(a19,a13,a16) % 0.56/0.75 [5]P1(a19,a14,a17) % 0.56/0.75 [6]P1(a19,a5,a15) % 0.56/0.75 [7]P1(a19,a6,a4) % 0.56/0.75 [8]P1(a22,a12,a13) % 0.56/0.75 [9]P1(a22,a13,a14) % 0.56/0.75 [10]P1(a22,a14,a23) % 0.56/0.75 [11]P1(a22,a5,a6) % 0.56/0.75 [12]P1(a22,a6,a23) % 0.56/0.75 [13]P1(a20,a7,a5) % 0.56/0.75 [14]P1(a21,a15,a12) % 0.56/0.75 [15]P1(a24,a2,a7) % 0.56/0.75 [16]~P1(a24,a2,a17) % 0.56/0.75 [18]P2(x181)+~P1(a1,x182,x181) % 0.56/0.75 [20]P2(x201)+~P1(a1,x201,x202) % 0.56/0.75 [21]P2(x211)+~P1(a18,x212,x211) % 0.56/0.75 [22]P2(x221)+~P1(a18,x221,x222) % 0.56/0.75 [23]P2(x231)+~P1(a24,x232,x231) % 0.56/0.75 [24]P2(x241)+~P1(a24,x241,x242) % 0.56/0.75 [28]P3(x281,x282)+P3(x283,x282)+~P1(a18,x281,x283) % 0.56/0.75 [29]P3(x291,x292)+~P3(x293,x292)+~P1(a24,x293,x291) % 0.56/0.75 [30]~P3(x301,x302)+~P3(x303,x302)+~P1(a1,x303,x301) % 0.56/0.75 [31]~P3(x311,x312)+~P3(x313,x312)+~P1(a18,x313,x311) % 0.56/0.75 [25]~P2(x251)+~P2(x252)+P1(a1,x251,x252)+P3(x252,f8(x251,x252)) % 0.56/0.75 [26]~P2(x262)+~P2(x261)+P1(a1,x261,x262)+P3(x261,f8(x261,x262)) % 0.56/0.75 [27]~P2(x272)+~P2(x271)+P1(a24,x271,x272)+P3(x271,f9(x271,x272)) % 0.56/0.75 [32]~P2(x321)+~P2(x322)+P1(a24,x321,x322)+~P3(x322,f9(x321,x322)) % 0.56/0.75 [33]P2(x331)+~P1(a22,x333,x332)+~P1(a19,x332,x331)+~P1(a19,x333,x334)+~P1(a20,x335,x333)+~P1(a22,x332,a23) % 0.56/0.75 [34]P2(x341)+~P1(a22,x344,x342)+~P1(a19,x342,x343)+~P1(a19,x344,x341)+~P1(a20,x345,x344)+~P1(a22,x342,a23) % 0.56/0.75 [35]P2(x351)+~P1(a22,x354,x352)+~P1(a20,x351,x354)+~P1(a19,x352,x353)+~P1(a19,x354,x355)+~P1(a22,x352,a23) % 0.56/0.75 [36]P3(x361,x362)+~P3(x363,x362)+~P1(a22,x365,x364)+~P1(a20,x363,x365)+~P1(a19,x364,x361)+~P1(a19,x365,x366)+~P1(a22,x364,a23) % 0.56/0.75 [37]P3(x371,x372)+~P3(x373,x372)+~P1(a22,x376,x374)+~P1(a20,x373,x376)+~P1(a19,x374,x375)+~P1(a19,x376,x371)+~P1(a22,x374,a23) % 0.56/0.75 [38]P3(x381,x382)+~P3(x383,x382)+~P3(x384,x382)+~P1(a22,x386,x385)+~P1(a20,x381,x386)+~P1(a19,x385,x383)+~P1(a19,x386,x384)+~P1(a22,x385,a23) % 0.56/0.75 [39]P2(x391)+~P1(a22,x393,x392)+~P1(a22,x395,x393)+~P1(a19,x392,x391)+~P1(a19,x393,x394)+~P1(a19,x395,x396)+~P1(a21,x397,x395)+~P1(a22,x392,a23) % 0.56/0.75 [40]P2(x401)+~P1(a22,x404,x402)+~P1(a22,x405,x404)+~P1(a19,x402,x403)+~P1(a19,x404,x401)+~P1(a19,x405,x406)+~P1(a21,x407,x405)+~P1(a22,x402,a23) % 0.56/0.75 [41]P2(x411)+~P1(a22,x414,x412)+~P1(a22,x416,x414)+~P1(a19,x412,x413)+~P1(a19,x414,x415)+~P1(a19,x416,x411)+~P1(a21,x417,x416)+~P1(a22,x412,a23) % 0.56/0.75 [42]P2(x421)+~P1(a22,x424,x422)+~P1(a22,x426,x424)+~P1(a21,x421,x426)+~P1(a19,x422,x423)+~P1(a19,x424,x425)+~P1(a19,x426,x427)+~P1(a22,x422,a23) % 0.56/0.75 [43]P3(x431,x432)+~P3(x433,x432)+~P1(a22,x435,x434)+~P1(a22,x437,x435)+~P1(a21,x431,x437)+~P1(a19,x434,x433)+~P1(a19,x435,x436)+~P1(a19,x437,x438)+~P1(a22,x434,a23) % 0.56/0.75 [44]P3(x441,x442)+~P3(x443,x442)+~P1(a22,x446,x444)+~P1(a22,x447,x446)+~P1(a21,x441,x447)+~P1(a19,x444,x445)+~P1(a19,x446,x443)+~P1(a19,x447,x448)+~P1(a22,x444,a23) % 0.56/0.75 [45]P3(x451,x452)+~P3(x453,x452)+~P1(a22,x456,x454)+~P1(a22,x458,x456)+~P1(a21,x451,x458)+~P1(a19,x454,x455)+~P1(a19,x456,x457)+~P1(a19,x458,x453)+~P1(a22,x454,a23) % 0.56/0.75 [47]~P2(x473)+~P2(x471)+~P2(x475)+~P1(a19,x474,x475)+~P1(a19,x472,x473)+~P1(a22,x472,x474)+P1(a20,x471,x472)+P3(x471,f10(x471,x472,x473,x474,x475))+P3(x475,f10(x471,x472,x473,x474,x475))+~P1(a22,x474,a23) % 0.56/0.75 [48]~P2(x485)+~P2(x481)+~P2(x483)+~P1(a19,x484,x485)+~P1(a19,x482,x483)+~P1(a22,x482,x484)+P1(a20,x481,x482)+P3(x481,f10(x481,x482,x483,x484,x485))+P3(x483,f10(x481,x482,x483,x484,x485))+~P1(a22,x484,a23) % 0.56/0.75 [49]~P2(x491)+~P2(x493)+~P2(x494)+~P1(a19,x492,x494)+~P1(a22,x492,x495)+P1(a20,x491,x492)+~P1(a19,x495,x493)+~P3(x493,f10(x491,x492,x494,x495,x493))+~P3(x494,f10(x491,x492,x494,x495,x493))+~P3(x491,f10(x491,x492,x494,x495,x493))+~P1(a22,x495,a23) % 0.56/0.75 [46]P3(x461,x462)+P3(x463,x462)+P3(x464,x462)+~P3(x465,x462)+~P1(a22,x467,x466)+~P1(a22,x468,x467)+~P1(a21,x465,x468)+~P1(a19,x466,x461)+~P1(a19,x467,x463)+~P1(a19,x468,x464)+~P1(a22,x466,a23) % 0.56/0.75 [50]~P2(x501)+~P2(x503)+~P2(x504)+~P2(x505)+~P1(a19,x502,x505)+~P1(a22,x507,x506)+~P1(a22,x502,x507)+P1(a21,x501,x502)+~P1(a19,x506,x503)+~P1(a19,x507,x504)+~P3(x501,f11(x501,x502,x505,x507,x504,x506,x503))+~P3(x505,f11(x501,x502,x505,x507,x504,x506,x503))+~P1(a22,x506,a23) % 0.56/0.75 [51]~P2(x511)+~P2(x513)+~P2(x514)+~P2(x515)+~P1(a19,x512,x514)+~P1(a22,x517,x516)+~P1(a22,x512,x517)+P1(a21,x511,x512)+~P1(a19,x516,x513)+~P1(a19,x517,x515)+~P3(x511,f11(x511,x512,x514,x517,x515,x516,x513))+~P3(x515,f11(x511,x512,x514,x517,x515,x516,x513))+~P1(a22,x516,a23) % 0.56/0.75 [52]~P2(x521)+~P2(x523)+~P2(x524)+~P2(x525)+~P1(a19,x522,x524)+~P1(a22,x527,x526)+~P1(a22,x522,x527)+P1(a21,x521,x522)+~P1(a19,x526,x525)+~P1(a19,x527,x523)+~P3(x521,f11(x521,x522,x524,x527,x523,x526,x525))+~P3(x525,f11(x521,x522,x524,x527,x523,x526,x525))+~P1(a22,x526,a23) % 0.56/0.75 [53]~P2(x533)+~P2(x536)+~P2(x534)+~P2(x531)+~P1(a19,x537,x533)+~P1(a19,x535,x536)+~P1(a19,x532,x534)+~P1(a22,x535,x537)+~P1(a22,x532,x535)+P1(a21,x531,x532)+P3(x533,f11(x531,x532,x534,x535,x536,x537,x533))+P3(x536,f11(x531,x532,x534,x535,x536,x537,x533))+P3(x534,f11(x531,x532,x534,x535,x536,x537,x533))+P3(x531,f11(x531,x532,x534,x535,x536,x537,x533))+~P1(a22,x537,a23) % 0.56/0.75 %EqnAxiom % 0.56/0.75 % 0.56/0.75 %------------------------------------------- % 0.56/0.75 cnf(56,plain, % 0.56/0.75 (P2(a2)), % 0.56/0.75 inference(scs_inference,[],[1,18,20])). % 0.56/0.75 cnf(64,plain, % 0.56/0.75 (P2(a17)), % 0.56/0.75 inference(scs_inference,[],[1,2,3,4,5,8,9,10,14,15,18,20,21,22,23,39])). % 0.56/0.75 cnf(75,plain, % 0.56/0.75 (~P3(a16,x751)+~P3(a4,x751)), % 0.56/0.75 inference(scs_inference,[],[2,31])). % 0.56/0.75 cnf(82,plain, % 0.56/0.75 (~P3(a3,x821)+~P3(a2,x821)), % 0.56/0.75 inference(scs_inference,[],[1,30])). % 0.56/0.75 cnf(87,plain, % 0.56/0.75 (P3(a7,x871)+~P3(a2,x871)), % 0.56/0.75 inference(scs_inference,[],[15,29])). % 0.56/0.75 cnf(98,plain, % 0.56/0.75 (P3(a15,x981)+~P3(a7,x981)), % 0.56/0.75 inference(scs_inference,[],[12,13,11,6,7,37])). % 0.56/0.75 cnf(103,plain, % 0.56/0.75 (P3(a4,x1031)+~P3(a7,x1031)), % 0.56/0.75 inference(scs_inference,[],[12,13,11,6,7,36])). % 0.56/0.75 cnf(132,plain, % 0.56/0.75 (P3(a2,f9(a2,a17))), % 0.56/0.75 inference(scs_inference,[],[15,16,64,24,27])). % 0.56/0.75 cnf(145,plain, % 0.56/0.75 ($false), % 0.56/0.75 inference(scs_inference,[],[16,132,56,64,10,8,14,9,4,3,5,82,87,98,103,75,46,32]), % 0.56/0.75 ['proof']). % 0.56/0.75 % SZS output end Proof % 0.56/0.75 % Total time :0.110000s %------------------------------------------------------------------------------