%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB009+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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 : Thu May 9 17:42:46 EDT 2024
% Result : Theorem 0.21s 0.55s
% Output : Refutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWB009+2 : TPTP v8.1.2. Released v5.2.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n028.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 22:09:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.21/0.55 % Version: 1.5
% 0.21/0.55 % SZS status Theorem
% 0.21/0.55 % SZS output start CNFRefutation
% 0.21/0.55 fof(testcase_conclusion_fullish_009_Existential_Restriction_Entailments,conjecture,(?[BNODE_x]:(iext(uri_ex_p,uri_ex_s,BNODE_x)&iext(uri_rdf_type,BNODE_x,uri_ex_c))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_conclusion_fullish_009_Existential_Restriction_Entailments)).
% 0.21/0.55 fof(c8,negated_conjecture,(~(?[BNODE_x]:(iext(uri_ex_p,uri_ex_s,BNODE_x)&iext(uri_rdf_type,BNODE_x,uri_ex_c)))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_009_Existential_Restriction_Entailments])).
% 0.21/0.55 fof(c9,negated_conjecture,(![BNODE_x]:(~iext(uri_ex_p,uri_ex_s,BNODE_x)|~iext(uri_rdf_type,BNODE_x,uri_ex_c))),inference(fof_nnf,[status(thm)],[c8])).
% 0.21/0.55 fof(c10,negated_conjecture,(![X3]:(~iext(uri_ex_p,uri_ex_s,X3)|~iext(uri_rdf_type,X3,uri_ex_c))),inference(variable_rename,[status(thm)],[c9])).
% 0.21/0.55 cnf(c11,negated_conjecture,~iext(uri_ex_p,uri_ex_s,X17)|~iext(uri_rdf_type,X17,uri_ex_c),inference(split_conjunct,[status(thm)],[c10])).
% 0.21/0.55 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rdfs_cext_def)).
% 0.21/0.55 fof(c21,plain,(![X]:(![C]:((~iext(uri_rdf_type,X,C)|icext(C,X))&(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(fof_nnf,[status(thm)],[rdfs_cext_def])).
% 0.21/0.55 fof(c22,plain,((![X]:(![C]:(~iext(uri_rdf_type,X,C)|icext(C,X))))&(![X]:(![C]:(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(shift_quantors,[status(thm)],[c21])).
% 0.21/0.55 fof(c24,plain,(![X11]:(![X12]:(![X13]:(![X14]:((~iext(uri_rdf_type,X11,X12)|icext(X12,X11))&(~icext(X14,X13)|iext(uri_rdf_type,X13,X14))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X11]:(![X12]:(~iext(uri_rdf_type,X11,X12)|icext(X12,X11))))&(![X13]:(![X14]:(~icext(X14,X13)|iext(uri_rdf_type,X13,X14))))),inference(variable_rename,[status(thm)],[c22])).])).
% 0.21/0.55 cnf(c26,plain,~icext(X19,X18)|iext(uri_rdf_type,X18,X19),inference(split_conjunct,[status(thm)],[c24])).
% 0.21/0.55 fof(testcase_premise_fullish_009_Existential_Restriction_Entailments,axiom,(?[BNODE_z]:(((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_c,uri_owl_Class))&iext(uri_rdf_type,uri_ex_s,BNODE_z))&iext(uri_rdf_type,BNODE_z,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_z,uri_ex_p))&iext(uri_owl_someValuesFrom,BNODE_z,uri_ex_c))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_009_Existential_Restriction_Entailments)).
% 0.21/0.55 fof(c0,plain,(?[X2]:(((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_c,uri_owl_Class))&iext(uri_rdf_type,uri_ex_s,X2))&iext(uri_rdf_type,X2,uri_owl_Restriction))&iext(uri_owl_onProperty,X2,uri_ex_p))&iext(uri_owl_someValuesFrom,X2,uri_ex_c))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_009_Existential_Restriction_Entailments])).
% 0.21/0.55 fof(c1,plain,(((((iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_c,uri_owl_Class))&iext(uri_rdf_type,uri_ex_s,skolem0001))&iext(uri_rdf_type,skolem0001,uri_owl_Restriction))&iext(uri_owl_onProperty,skolem0001,uri_ex_p))&iext(uri_owl_someValuesFrom,skolem0001,uri_ex_c)),inference(skolemize,[status(esa)],[c0])).
% 0.21/0.55 cnf(c4,plain,iext(uri_rdf_type,uri_ex_s,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 0.21/0.55 cnf(c25,plain,~iext(uri_rdf_type,X16,X15)|icext(X15,X16),inference(split_conjunct,[status(thm)],[c24])).
% 0.21/0.55 cnf(c28,plain,icext(skolem0001,uri_ex_s),inference(resolution,[status(thm)],[c25, c4])).
% 0.21/0.55 cnf(c7,plain,iext(uri_owl_someValuesFrom,skolem0001,uri_ex_c),inference(split_conjunct,[status(thm)],[c1])).
% 0.21/0.55 cnf(c6,plain,iext(uri_owl_onProperty,skolem0001,uri_ex_p),inference(split_conjunct,[status(thm)],[c1])).
% 0.21/0.55 fof(owl_restrict_somevaluesfrom,axiom,(![Z]:(![P]:(![C]:((iext(uri_owl_someValuesFrom,Z,C)&iext(uri_owl_onProperty,Z,P))=>(![X]:(icext(Z,X)<=>(?[Y]:(iext(P,X,Y)&icext(C,Y))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_restrict_somevaluesfrom)).
% 0.21/0.55 fof(c12,plain,(![Z]:(![P]:(![C]:((~iext(uri_owl_someValuesFrom,Z,C)|~iext(uri_owl_onProperty,Z,P))|(![X]:((~icext(Z,X)|(?[Y]:(iext(P,X,Y)&icext(C,Y))))&((![Y]:(~iext(P,X,Y)|~icext(C,Y)))|icext(Z,X)))))))),inference(fof_nnf,[status(thm)],[owl_restrict_somevaluesfrom])).
% 0.21/0.55 fof(c13,plain,(![Z]:(![P]:(![C]:((~iext(uri_owl_someValuesFrom,Z,C)|~iext(uri_owl_onProperty,Z,P))|((![X]:(~icext(Z,X)|(?[Y]:(iext(P,X,Y)&icext(C,Y)))))&(![X]:((![Y]:(~iext(P,X,Y)|~icext(C,Y)))|icext(Z,X)))))))),inference(shift_quantors,[status(thm)],[c12])).
% 0.21/0.55 fof(c14,plain,(![X4]:(![X5]:(![X6]:((~iext(uri_owl_someValuesFrom,X4,X6)|~iext(uri_owl_onProperty,X4,X5))|((![X7]:(~icext(X4,X7)|(?[X8]:(iext(X5,X7,X8)&icext(X6,X8)))))&(![X9]:((![X10]:(~iext(X5,X9,X10)|~icext(X6,X10)))|icext(X4,X9)))))))),inference(variable_rename,[status(thm)],[c13])).
% 0.21/0.55 fof(c16,plain,(![X4]:(![X5]:(![X6]:(![X7]:(![X9]:(![X10]:((~iext(uri_owl_someValuesFrom,X4,X6)|~iext(uri_owl_onProperty,X4,X5))|((~icext(X4,X7)|(iext(X5,X7,skolem0002(X4,X5,X6,X7))&icext(X6,skolem0002(X4,X5,X6,X7))))&((~iext(X5,X9,X10)|~icext(X6,X10))|icext(X4,X9)))))))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,(![X4]:(![X5]:(![X6]:((~iext(uri_owl_someValuesFrom,X4,X6)|~iext(uri_owl_onProperty,X4,X5))|((![X7]:(~icext(X4,X7)|(iext(X5,X7,skolem0002(X4,X5,X6,X7))&icext(X6,skolem0002(X4,X5,X6,X7)))))&(![X9]:((![X10]:(~iext(X5,X9,X10)|~icext(X6,X10)))|icext(X4,X9)))))))),inference(skolemize,[status(esa)],[c14])).])).
% 0.21/0.55 fof(c17,plain,(![X4]:(![X5]:(![X6]:(![X7]:(![X9]:(![X10]:((((~iext(uri_owl_someValuesFrom,X4,X6)|~iext(uri_owl_onProperty,X4,X5))|(~icext(X4,X7)|iext(X5,X7,skolem0002(X4,X5,X6,X7))))&((~iext(uri_owl_someValuesFrom,X4,X6)|~iext(uri_owl_onProperty,X4,X5))|(~icext(X4,X7)|icext(X6,skolem0002(X4,X5,X6,X7)))))&((~iext(uri_owl_someValuesFrom,X4,X6)|~iext(uri_owl_onProperty,X4,X5))|((~iext(X5,X9,X10)|~icext(X6,X10))|icext(X4,X9)))))))))),inference(distribute,[status(thm)],[c16])).
% 0.21/0.55 cnf(c19,plain,~iext(uri_owl_someValuesFrom,X27,X24)|~iext(uri_owl_onProperty,X27,X26)|~icext(X27,X25)|icext(X24,skolem0002(X27,X26,X24,X25)),inference(split_conjunct,[status(thm)],[c17])).
% 0.21/0.55 cnf(c36,plain,~iext(uri_owl_someValuesFrom,skolem0001,X29)|~icext(skolem0001,X28)|icext(X29,skolem0002(skolem0001,uri_ex_p,X29,X28)),inference(resolution,[status(thm)],[c19, c6])).
% 0.21/0.55 cnf(c37,plain,~icext(skolem0001,X30)|icext(uri_ex_c,skolem0002(skolem0001,uri_ex_p,uri_ex_c,X30)),inference(resolution,[status(thm)],[c36, c7])).
% 0.21/0.55 cnf(c38,plain,icext(uri_ex_c,skolem0002(skolem0001,uri_ex_p,uri_ex_c,uri_ex_s)),inference(resolution,[status(thm)],[c37, c28])).
% 0.21/0.55 cnf(c39,plain,iext(uri_rdf_type,skolem0002(skolem0001,uri_ex_p,uri_ex_c,uri_ex_s),uri_ex_c),inference(resolution,[status(thm)],[c38, c26])).
% 0.21/0.55 cnf(c40,plain,~iext(uri_ex_p,uri_ex_s,skolem0002(skolem0001,uri_ex_p,uri_ex_c,uri_ex_s)),inference(resolution,[status(thm)],[c39, c11])).
% 0.21/0.55 cnf(c18,plain,~iext(uri_owl_someValuesFrom,X23,X20)|~iext(uri_owl_onProperty,X23,X22)|~icext(X23,X21)|iext(X22,X21,skolem0002(X23,X22,X20,X21)),inference(split_conjunct,[status(thm)],[c17])).
% 0.21/0.55 cnf(c35,plain,~iext(uri_owl_someValuesFrom,skolem0001,X43)|~icext(skolem0001,X42)|iext(uri_ex_p,X42,skolem0002(skolem0001,uri_ex_p,X43,X42)),inference(resolution,[status(thm)],[c18, c6])).
% 0.21/0.55 cnf(c51,plain,~icext(skolem0001,X44)|iext(uri_ex_p,X44,skolem0002(skolem0001,uri_ex_p,uri_ex_c,X44)),inference(resolution,[status(thm)],[c35, c7])).
% 0.21/0.55 cnf(c52,plain,iext(uri_ex_p,uri_ex_s,skolem0002(skolem0001,uri_ex_p,uri_ex_c,uri_ex_s)),inference(resolution,[status(thm)],[c51, c28])).
% 0.21/0.55 cnf(c54,plain,$false,inference(resolution,[status(thm)],[c52, c40])).
% 0.21/0.55 % SZS output end CNFRefutation
% 0.21/0.55
% 0.21/0.55 % Initial clauses : 12
% 0.21/0.55 % Processed clauses : 27
% 0.21/0.55 % Factors computed : 2
% 0.21/0.55 % Resolvents computed: 26
% 0.21/0.55 % Tautologies deleted: 0
% 0.21/0.55 % Forward subsumed : 5
% 0.21/0.55 % Backward subsumed : 0
% 0.21/0.55 % -------- CPU Time ---------
% 0.21/0.55 % User time : 0.176 s
% 0.21/0.55 % System time : 0.018 s
% 0.21/0.55 % Total time : 0.193 s
%------------------------------------------------------------------------------