%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB009+3 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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 40.06s 40.26s
% Output : Refutation 40.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SWB009+3 : TPTP v8.1.2. Released v5.2.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % 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:13:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 40.06/40.26 % Version: 1.5
% 40.06/40.26 % SZS status Theorem
% 40.06/40.26 % SZS output start CNFRefutation
% 40.06/40.26 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/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_009_Existential_Restriction_Entailments)).
% 40.06/40.26 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])).
% 40.06/40.26 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])).
% 40.06/40.26 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])).
% 40.06/40.26 cnf(c11,negated_conjecture,~iext(uri_ex_p,uri_ex_s,X231)|~iext(uri_rdf_type,X231,uri_ex_c),inference(split_conjunct,[status(thm)],[c10])).
% 40.06/40.26 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax', rdfs_cext_def)).
% 40.06/40.26 fof(c124,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])).
% 40.06/40.26 fof(c125,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)],[c124])).
% 40.06/40.26 fof(c127,plain,(![X41]:(![X42]:(![X43]:(![X44]:((~iext(uri_rdf_type,X41,X42)|icext(X42,X41))&(~icext(X44,X43)|iext(uri_rdf_type,X43,X44))))))),inference(shift_quantors,[status(thm)],[fof(c126,plain,((![X41]:(![X42]:(~iext(uri_rdf_type,X41,X42)|icext(X42,X41))))&(![X43]:(![X44]:(~icext(X44,X43)|iext(uri_rdf_type,X43,X44))))),inference(variable_rename,[status(thm)],[c125])).])).
% 40.06/40.26 cnf(c129,plain,~icext(X275,X276)|iext(uri_rdf_type,X276,X275),inference(split_conjunct,[status(thm)],[c127])).
% 40.06/40.26 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/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_009_Existential_Restriction_Entailments)).
% 40.06/40.26 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])).
% 40.06/40.26 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])).
% 40.06/40.26 cnf(c4,plain,iext(uri_rdf_type,uri_ex_s,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 40.06/40.26 cnf(c128,plain,~iext(uri_rdf_type,X273,X274)|icext(X274,X273),inference(split_conjunct,[status(thm)],[c127])).
% 40.06/40.26 cnf(c797,plain,icext(skolem0001,uri_ex_s),inference(resolution,[status(thm)],[c128, c4])).
% 40.06/40.26 cnf(c7,plain,iext(uri_owl_someValuesFrom,skolem0001,uri_ex_c),inference(split_conjunct,[status(thm)],[c1])).
% 40.06/40.26 cnf(c6,plain,iext(uri_owl_onProperty,skolem0001,uri_ex_p),inference(split_conjunct,[status(thm)],[c1])).
% 40.06/40.26 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/sandbox/benchmark/Axioms/SWB002+0.ax', owl_restrict_somevaluesfrom)).
% 40.06/40.26 fof(c156,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])).
% 40.06/40.26 fof(c157,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)],[c156])).
% 40.06/40.26 fof(c158,plain,(![X47]:(![X48]:(![X49]:((~iext(uri_owl_someValuesFrom,X47,X49)|~iext(uri_owl_onProperty,X47,X48))|((![X50]:(~icext(X47,X50)|(?[X51]:(iext(X48,X50,X51)&icext(X49,X51)))))&(![X52]:((![X53]:(~iext(X48,X52,X53)|~icext(X49,X53)))|icext(X47,X52)))))))),inference(variable_rename,[status(thm)],[c157])).
% 40.06/40.26 fof(c160,plain,(![X47]:(![X48]:(![X49]:(![X50]:(![X52]:(![X53]:((~iext(uri_owl_someValuesFrom,X47,X49)|~iext(uri_owl_onProperty,X47,X48))|((~icext(X47,X50)|(iext(X48,X50,skolem0002(X47,X48,X49,X50))&icext(X49,skolem0002(X47,X48,X49,X50))))&((~iext(X48,X52,X53)|~icext(X49,X53))|icext(X47,X52)))))))))),inference(shift_quantors,[status(thm)],[fof(c159,plain,(![X47]:(![X48]:(![X49]:((~iext(uri_owl_someValuesFrom,X47,X49)|~iext(uri_owl_onProperty,X47,X48))|((![X50]:(~icext(X47,X50)|(iext(X48,X50,skolem0002(X47,X48,X49,X50))&icext(X49,skolem0002(X47,X48,X49,X50)))))&(![X52]:((![X53]:(~iext(X48,X52,X53)|~icext(X49,X53)))|icext(X47,X52)))))))),inference(skolemize,[status(esa)],[c158])).])).
% 40.06/40.26 fof(c161,plain,(![X47]:(![X48]:(![X49]:(![X50]:(![X52]:(![X53]:((((~iext(uri_owl_someValuesFrom,X47,X49)|~iext(uri_owl_onProperty,X47,X48))|(~icext(X47,X50)|iext(X48,X50,skolem0002(X47,X48,X49,X50))))&((~iext(uri_owl_someValuesFrom,X47,X49)|~iext(uri_owl_onProperty,X47,X48))|(~icext(X47,X50)|icext(X49,skolem0002(X47,X48,X49,X50)))))&((~iext(uri_owl_someValuesFrom,X47,X49)|~iext(uri_owl_onProperty,X47,X48))|((~iext(X48,X52,X53)|~icext(X49,X53))|icext(X47,X52)))))))))),inference(distribute,[status(thm)],[c160])).
% 40.06/40.26 cnf(c163,plain,~iext(uri_owl_someValuesFrom,X293,X292)|~iext(uri_owl_onProperty,X293,X291)|~icext(X293,X290)|icext(X292,skolem0002(X293,X291,X292,X290)),inference(split_conjunct,[status(thm)],[c161])).
% 40.06/40.26 cnf(c973,plain,~iext(uri_owl_someValuesFrom,skolem0001,X1067)|~icext(skolem0001,X1066)|icext(X1067,skolem0002(skolem0001,uri_ex_p,X1067,X1066)),inference(resolution,[status(thm)],[c163, c6])).
% 40.06/40.26 cnf(c3497,plain,~icext(skolem0001,X2901)|icext(uri_ex_c,skolem0002(skolem0001,uri_ex_p,uri_ex_c,X2901)),inference(resolution,[status(thm)],[c973, c7])).
% 40.06/40.26 cnf(c10142,plain,icext(uri_ex_c,skolem0002(skolem0001,uri_ex_p,uri_ex_c,uri_ex_s)),inference(resolution,[status(thm)],[c3497, c797])).
% 40.06/40.26 cnf(c10144,plain,iext(uri_rdf_type,skolem0002(skolem0001,uri_ex_p,uri_ex_c,uri_ex_s),uri_ex_c),inference(resolution,[status(thm)],[c10142, c129])).
% 40.06/40.26 cnf(c10170,plain,~iext(uri_ex_p,uri_ex_s,skolem0002(skolem0001,uri_ex_p,uri_ex_c,uri_ex_s)),inference(resolution,[status(thm)],[c10144, c11])).
% 40.06/40.26 cnf(c162,plain,~iext(uri_owl_someValuesFrom,X285,X284)|~iext(uri_owl_onProperty,X285,X283)|~icext(X285,X282)|iext(X283,X282,skolem0002(X285,X283,X284,X282)),inference(split_conjunct,[status(thm)],[c161])).
% 40.06/40.26 cnf(c965,plain,~iext(uri_owl_someValuesFrom,skolem0001,X1056)|~icext(skolem0001,X1057)|iext(uri_ex_p,X1057,skolem0002(skolem0001,uri_ex_p,X1056,X1057)),inference(resolution,[status(thm)],[c162, c6])).
% 40.06/40.26 cnf(c3490,plain,~icext(skolem0001,X3189)|iext(uri_ex_p,X3189,skolem0002(skolem0001,uri_ex_p,uri_ex_c,X3189)),inference(resolution,[status(thm)],[c965, c7])).
% 40.06/40.26 cnf(c12005,plain,iext(uri_ex_p,uri_ex_s,skolem0002(skolem0001,uri_ex_p,uri_ex_c,uri_ex_s)),inference(resolution,[status(thm)],[c3490, c797])).
% 40.06/40.26 cnf(c12019,plain,$false,inference(resolution,[status(thm)],[c12005, c10170])).
% 40.06/40.26 % SZS output end CNFRefutation
% 40.06/40.26
% 40.06/40.26 % Initial clauses : 253
% 40.06/40.26 % Processed clauses : 2350
% 40.06/40.26 % Factors computed : 73
% 40.06/40.26 % Resolvents computed: 11435
% 40.06/40.26 % Tautologies deleted: 76
% 40.06/40.26 % Forward subsumed : 3926
% 40.06/40.26 % Backward subsumed : 44
% 40.06/40.26 % -------- CPU Time ---------
% 40.06/40.26 % User time : 39.877 s
% 40.06/40.26 % System time : 0.029 s
% 40.06/40.26 % Total time : 39.906 s
%------------------------------------------------------------------------------