%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB032+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %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 : Thu May 9 17:42:57 EDT 2024
% Result : Theorem 0.99s 1.22s
% Output : Refutation 0.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SWB032+2 : TPTP v8.1.2. Released v5.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n004.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:07:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.99/1.22 % Version: 1.5
% 0.99/1.22 % SZS status Theorem
% 0.99/1.22 % SZS output start CNFRefutation
% 0.99/1.22 fof(owl_dat_dtype_relation_subtype_string_plainliteral,axiom,(![X]:(icext(uri_xsd_string,X)=>icext(uri_rdf_PlainLiteral,X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_dat_dtype_relation_subtype_string_plainliteral)).
% 0.99/1.22 fof(c37,plain,(![X]:(~icext(uri_xsd_string,X)|icext(uri_rdf_PlainLiteral,X))),inference(fof_nnf,[status(thm)],[owl_dat_dtype_relation_subtype_string_plainliteral])).
% 0.99/1.22 fof(c38,plain,(![X18]:(~icext(uri_xsd_string,X18)|icext(uri_rdf_PlainLiteral,X18))),inference(variable_rename,[status(thm)],[c37])).
% 0.99/1.22 cnf(c39,plain,~icext(uri_xsd_string,X35)|icext(uri_rdf_PlainLiteral,X35),inference(split_conjunct,[status(thm)],[c38])).
% 0.99/1.22 fof(owl_dat_dtype_decimal_type,axiom,idc(uri_xsd_decimal),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_dat_dtype_decimal_type)).
% 0.99/1.22 cnf(c44,plain,idc(uri_xsd_decimal),inference(split_conjunct,[status(thm)],[owl_dat_dtype_decimal_type])).
% 0.99/1.22 fof(owl_parts_idc_cond_set,axiom,(![X]:(idc(X)=>ic(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_parts_idc_cond_set)).
% 0.99/1.22 fof(c25,plain,(![X]:(~idc(X)|ic(X))),inference(fof_nnf,[status(thm)],[owl_parts_idc_cond_set])).
% 0.99/1.22 fof(c26,plain,(![X14]:(~idc(X14)|ic(X14))),inference(variable_rename,[status(thm)],[c25])).
% 0.99/1.22 cnf(c27,plain,~idc(X20)|ic(X20),inference(split_conjunct,[status(thm)],[c26])).
% 0.99/1.22 cnf(c46,plain,ic(uri_xsd_decimal),inference(resolution,[status(thm)],[c27, c44])).
% 0.99/1.22 fof(owl_dat_dtype_string_type,axiom,idc(uri_xsd_string),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_dat_dtype_string_type)).
% 0.99/1.22 cnf(c45,plain,idc(uri_xsd_string),inference(split_conjunct,[status(thm)],[owl_dat_dtype_string_type])).
% 0.99/1.22 cnf(c47,plain,ic(uri_xsd_string),inference(resolution,[status(thm)],[c27, c45])).
% 0.99/1.22 fof(owl_eqdis_disjointwith,axiom,(![C1]:(![C2]:(iext(uri_owl_disjointWith,C1,C2)<=>((ic(C1)&ic(C2))&(![X]:(~(icext(C1,X)&icext(C2,X)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_eqdis_disjointwith)).
% 0.99/1.22 fof(c3,plain,(![C1]:(![C2]:((~iext(uri_owl_disjointWith,C1,C2)|((ic(C1)&ic(C2))&(![X]:(~icext(C1,X)|~icext(C2,X)))))&(((~ic(C1)|~ic(C2))|(?[X]:(icext(C1,X)&icext(C2,X))))|iext(uri_owl_disjointWith,C1,C2))))),inference(fof_nnf,[status(thm)],[owl_eqdis_disjointwith])).
% 0.99/1.22 fof(c4,plain,((![C1]:(![C2]:(~iext(uri_owl_disjointWith,C1,C2)|((ic(C1)&ic(C2))&(![X]:(~icext(C1,X)|~icext(C2,X)))))))&(![C1]:(![C2]:(((~ic(C1)|~ic(C2))|(?[X]:(icext(C1,X)&icext(C2,X))))|iext(uri_owl_disjointWith,C1,C2))))),inference(shift_quantors,[status(thm)],[c3])).
% 0.99/1.22 fof(c5,plain,((![X2]:(![X3]:(~iext(uri_owl_disjointWith,X2,X3)|((ic(X2)&ic(X3))&(![X4]:(~icext(X2,X4)|~icext(X3,X4)))))))&(![X5]:(![X6]:(((~ic(X5)|~ic(X6))|(?[X7]:(icext(X5,X7)&icext(X6,X7))))|iext(uri_owl_disjointWith,X5,X6))))),inference(variable_rename,[status(thm)],[c4])).
% 0.99/1.22 fof(c7,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:((~iext(uri_owl_disjointWith,X2,X3)|((ic(X2)&ic(X3))&(~icext(X2,X4)|~icext(X3,X4))))&(((~ic(X5)|~ic(X6))|(icext(X5,skolem0001(X5,X6))&icext(X6,skolem0001(X5,X6))))|iext(uri_owl_disjointWith,X5,X6)))))))),inference(shift_quantors,[status(thm)],[fof(c6,plain,((![X2]:(![X3]:(~iext(uri_owl_disjointWith,X2,X3)|((ic(X2)&ic(X3))&(![X4]:(~icext(X2,X4)|~icext(X3,X4)))))))&(![X5]:(![X6]:(((~ic(X5)|~ic(X6))|(icext(X5,skolem0001(X5,X6))&icext(X6,skolem0001(X5,X6))))|iext(uri_owl_disjointWith,X5,X6))))),inference(skolemize,[status(esa)],[c5])).])).
% 0.99/1.22 fof(c8,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:((((~iext(uri_owl_disjointWith,X2,X3)|ic(X2))&(~iext(uri_owl_disjointWith,X2,X3)|ic(X3)))&(~iext(uri_owl_disjointWith,X2,X3)|(~icext(X2,X4)|~icext(X3,X4))))&((((~ic(X5)|~ic(X6))|icext(X5,skolem0001(X5,X6)))|iext(uri_owl_disjointWith,X5,X6))&(((~ic(X5)|~ic(X6))|icext(X6,skolem0001(X5,X6)))|iext(uri_owl_disjointWith,X5,X6))))))))),inference(distribute,[status(thm)],[c7])).
% 0.99/1.22 cnf(c13,plain,~ic(X46)|~ic(X45)|icext(X45,skolem0001(X46,X45))|iext(uri_owl_disjointWith,X46,X45),inference(split_conjunct,[status(thm)],[c8])).
% 0.99/1.22 cnf(c63,plain,~ic(X57)|icext(uri_xsd_string,skolem0001(X57,uri_xsd_string))|iext(uri_owl_disjointWith,X57,uri_xsd_string),inference(resolution,[status(thm)],[c13, c47])).
% 0.99/1.22 cnf(c113,plain,icext(uri_xsd_string,skolem0001(uri_xsd_decimal,uri_xsd_string))|iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string),inference(resolution,[status(thm)],[c63, c46])).
% 0.99/1.22 cnf(c257,plain,iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)|icext(uri_rdf_PlainLiteral,skolem0001(uri_xsd_decimal,uri_xsd_string)),inference(resolution,[status(thm)],[c113, c39])).
% 0.99/1.22 fof(testcase_conclusion_fullish_032_Datatype_Relationships,conjecture,(iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)&iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_032_Datatype_Relationships)).
% 0.99/1.22 fof(c0,negated_conjecture,(~(iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)&iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_032_Datatype_Relationships])).
% 0.99/1.22 fof(c1,negated_conjecture,(~iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)|~iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)),inference(fof_nnf,[status(thm)],[c0])).
% 0.99/1.22 cnf(c2,negated_conjecture,~iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)|~iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal),inference(split_conjunct,[status(thm)],[c1])).
% 0.99/1.22 fof(owl_dat_dtype_integer_type,axiom,idc(uri_xsd_integer),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_dat_dtype_integer_type)).
% 0.99/1.22 cnf(c43,plain,idc(uri_xsd_integer),inference(split_conjunct,[status(thm)],[owl_dat_dtype_integer_type])).
% 0.99/1.22 cnf(c48,plain,ic(uri_xsd_integer),inference(resolution,[status(thm)],[c27, c43])).
% 0.99/1.22 fof(owl_rdfsext_subclassof,axiom,(![C1]:(![C2]:(iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]:(icext(C1,X)=>icext(C2,X))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_rdfsext_subclassof)).
% 0.99/1.22 fof(c14,plain,(![C1]:(![C2]:((~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]:(~icext(C1,X)|icext(C2,X)))))&(((~ic(C1)|~ic(C2))|(?[X]:(icext(C1,X)&~icext(C2,X))))|iext(uri_rdfs_subClassOf,C1,C2))))),inference(fof_nnf,[status(thm)],[owl_rdfsext_subclassof])).
% 0.99/1.22 fof(c15,plain,((![C1]:(![C2]:(~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]:(~icext(C1,X)|icext(C2,X)))))))&(![C1]:(![C2]:(((~ic(C1)|~ic(C2))|(?[X]:(icext(C1,X)&~icext(C2,X))))|iext(uri_rdfs_subClassOf,C1,C2))))),inference(shift_quantors,[status(thm)],[c14])).
% 0.99/1.22 fof(c16,plain,((![X8]:(![X9]:(~iext(uri_rdfs_subClassOf,X8,X9)|((ic(X8)&ic(X9))&(![X10]:(~icext(X8,X10)|icext(X9,X10)))))))&(![X11]:(![X12]:(((~ic(X11)|~ic(X12))|(?[X13]:(icext(X11,X13)&~icext(X12,X13))))|iext(uri_rdfs_subClassOf,X11,X12))))),inference(variable_rename,[status(thm)],[c15])).
% 0.99/1.22 fof(c18,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((~iext(uri_rdfs_subClassOf,X8,X9)|((ic(X8)&ic(X9))&(~icext(X8,X10)|icext(X9,X10))))&(((~ic(X11)|~ic(X12))|(icext(X11,skolem0002(X11,X12))&~icext(X12,skolem0002(X11,X12))))|iext(uri_rdfs_subClassOf,X11,X12)))))))),inference(shift_quantors,[status(thm)],[fof(c17,plain,((![X8]:(![X9]:(~iext(uri_rdfs_subClassOf,X8,X9)|((ic(X8)&ic(X9))&(![X10]:(~icext(X8,X10)|icext(X9,X10)))))))&(![X11]:(![X12]:(((~ic(X11)|~ic(X12))|(icext(X11,skolem0002(X11,X12))&~icext(X12,skolem0002(X11,X12))))|iext(uri_rdfs_subClassOf,X11,X12))))),inference(skolemize,[status(esa)],[c16])).])).
% 0.99/1.22 fof(c19,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((((~iext(uri_rdfs_subClassOf,X8,X9)|ic(X8))&(~iext(uri_rdfs_subClassOf,X8,X9)|ic(X9)))&(~iext(uri_rdfs_subClassOf,X8,X9)|(~icext(X8,X10)|icext(X9,X10))))&((((~ic(X11)|~ic(X12))|icext(X11,skolem0002(X11,X12)))|iext(uri_rdfs_subClassOf,X11,X12))&(((~ic(X11)|~ic(X12))|~icext(X12,skolem0002(X11,X12)))|iext(uri_rdfs_subClassOf,X11,X12))))))))),inference(distribute,[status(thm)],[c18])).
% 0.99/1.22 cnf(c24,plain,~ic(X54)|~ic(X53)|~icext(X53,skolem0002(X54,X53))|iext(uri_rdfs_subClassOf,X54,X53),inference(split_conjunct,[status(thm)],[c19])).
% 0.99/1.22 fof(owl_dat_dtype_relation_subtype_integer_decimal,axiom,(![X]:(icext(uri_xsd_integer,X)=>icext(uri_xsd_decimal,X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_dat_dtype_relation_subtype_integer_decimal)).
% 0.99/1.22 fof(c28,plain,(![X]:(~icext(uri_xsd_integer,X)|icext(uri_xsd_decimal,X))),inference(fof_nnf,[status(thm)],[owl_dat_dtype_relation_subtype_integer_decimal])).
% 0.99/1.22 fof(c29,plain,(![X15]:(~icext(uri_xsd_integer,X15)|icext(uri_xsd_decimal,X15))),inference(variable_rename,[status(thm)],[c28])).
% 0.99/1.22 cnf(c30,plain,~icext(uri_xsd_integer,X32)|icext(uri_xsd_decimal,X32),inference(split_conjunct,[status(thm)],[c29])).
% 0.99/1.22 cnf(c23,plain,~ic(X50)|~ic(X49)|icext(X50,skolem0002(X50,X49))|iext(uri_rdfs_subClassOf,X50,X49),inference(split_conjunct,[status(thm)],[c19])).
% 0.99/1.22 cnf(c76,plain,~ic(X63)|icext(X63,skolem0002(X63,uri_xsd_decimal))|iext(uri_rdfs_subClassOf,X63,uri_xsd_decimal),inference(resolution,[status(thm)],[c23, c46])).
% 0.99/1.22 cnf(c143,plain,icext(uri_xsd_integer,skolem0002(uri_xsd_integer,uri_xsd_decimal))|iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal),inference(resolution,[status(thm)],[c76, c48])).
% 0.99/1.22 cnf(c380,plain,iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)|icext(uri_xsd_decimal,skolem0002(uri_xsd_integer,uri_xsd_decimal)),inference(resolution,[status(thm)],[c143, c30])).
% 0.99/1.22 cnf(c813,plain,iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)|~ic(uri_xsd_integer)|~ic(uri_xsd_decimal),inference(resolution,[status(thm)],[c380, c24])).
% 0.99/1.22 cnf(c816,plain,iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)|~ic(uri_xsd_integer),inference(resolution,[status(thm)],[c813, c46])).
% 0.99/1.22 cnf(c817,plain,iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal),inference(resolution,[status(thm)],[c816, c48])).
% 0.99/1.22 cnf(c818,plain,~iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string),inference(resolution,[status(thm)],[c817, c2])).
% 0.99/1.22 cnf(c828,plain,icext(uri_rdf_PlainLiteral,skolem0001(uri_xsd_decimal,uri_xsd_string)),inference(resolution,[status(thm)],[c818, c257])).
% 0.99/1.22 fof(owl_dat_dtype_relation_disjoint_plainliteral_real,axiom,(![X]:(~(icext(uri_rdf_PlainLiteral,X)&icext(uri_owl_real,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_dat_dtype_relation_disjoint_plainliteral_real)).
% 0.99/1.22 fof(c40,plain,(![X]:(~icext(uri_rdf_PlainLiteral,X)|~icext(uri_owl_real,X))),inference(fof_nnf,[status(thm)],[owl_dat_dtype_relation_disjoint_plainliteral_real])).
% 0.99/1.22 fof(c41,plain,(![X19]:(~icext(uri_rdf_PlainLiteral,X19)|~icext(uri_owl_real,X19))),inference(variable_rename,[status(thm)],[c40])).
% 0.99/1.22 cnf(c42,plain,~icext(uri_rdf_PlainLiteral,X38)|~icext(uri_owl_real,X38),inference(split_conjunct,[status(thm)],[c41])).
% 0.99/1.22 fof(owl_dat_dtype_relation_subtype_rational_real,axiom,(![X]:(icext(uri_owl_rational,X)=>icext(uri_owl_real,X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_dat_dtype_relation_subtype_rational_real)).
% 0.99/1.22 fof(c34,plain,(![X]:(~icext(uri_owl_rational,X)|icext(uri_owl_real,X))),inference(fof_nnf,[status(thm)],[owl_dat_dtype_relation_subtype_rational_real])).
% 0.99/1.22 fof(c35,plain,(![X17]:(~icext(uri_owl_rational,X17)|icext(uri_owl_real,X17))),inference(variable_rename,[status(thm)],[c34])).
% 0.99/1.22 cnf(c36,plain,~icext(uri_owl_rational,X34)|icext(uri_owl_real,X34),inference(split_conjunct,[status(thm)],[c35])).
% 0.99/1.22 fof(owl_dat_dtype_relation_subtype_decimal_rational,axiom,(![X]:(icext(uri_xsd_decimal,X)=>icext(uri_owl_rational,X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_dat_dtype_relation_subtype_decimal_rational)).
% 0.99/1.22 fof(c31,plain,(![X]:(~icext(uri_xsd_decimal,X)|icext(uri_owl_rational,X))),inference(fof_nnf,[status(thm)],[owl_dat_dtype_relation_subtype_decimal_rational])).
% 0.99/1.22 fof(c32,plain,(![X16]:(~icext(uri_xsd_decimal,X16)|icext(uri_owl_rational,X16))),inference(variable_rename,[status(thm)],[c31])).
% 0.99/1.22 cnf(c33,plain,~icext(uri_xsd_decimal,X33)|icext(uri_owl_rational,X33),inference(split_conjunct,[status(thm)],[c32])).
% 0.99/1.22 cnf(c12,plain,~ic(X37)|~ic(X36)|icext(X37,skolem0001(X37,X36))|iext(uri_owl_disjointWith,X37,X36),inference(split_conjunct,[status(thm)],[c8])).
% 0.99/1.22 cnf(c50,plain,~ic(X43)|icext(X43,skolem0001(X43,uri_xsd_string))|iext(uri_owl_disjointWith,X43,uri_xsd_string),inference(resolution,[status(thm)],[c12, c47])).
% 0.99/1.22 cnf(c58,plain,icext(uri_xsd_decimal,skolem0001(uri_xsd_decimal,uri_xsd_string))|iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string),inference(resolution,[status(thm)],[c50, c46])).
% 0.99/1.22 cnf(c97,plain,iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)|icext(uri_owl_rational,skolem0001(uri_xsd_decimal,uri_xsd_string)),inference(resolution,[status(thm)],[c58, c33])).
% 0.99/1.22 cnf(c216,plain,iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)|icext(uri_owl_real,skolem0001(uri_xsd_decimal,uri_xsd_string)),inference(resolution,[status(thm)],[c97, c36])).
% 0.99/1.22 cnf(c822,plain,icext(uri_owl_real,skolem0001(uri_xsd_decimal,uri_xsd_string)),inference(resolution,[status(thm)],[c818, c216])).
% 0.99/1.22 cnf(c831,plain,~icext(uri_rdf_PlainLiteral,skolem0001(uri_xsd_decimal,uri_xsd_string)),inference(resolution,[status(thm)],[c822, c42])).
% 0.99/1.22 cnf(c876,plain,$false,inference(resolution,[status(thm)],[c831, c828])).
% 0.99/1.22 % SZS output end CNFRefutation
% 0.99/1.22
% 0.99/1.22 % Initial clauses : 20
% 0.99/1.22 % Processed clauses : 182
% 0.99/1.22 % Factors computed : 3
% 0.99/1.22 % Resolvents computed: 828
% 0.99/1.22 % Tautologies deleted: 8
% 0.99/1.22 % Forward subsumed : 233
% 0.99/1.22 % Backward subsumed : 63
% 0.99/1.22 % -------- CPU Time ---------
% 0.99/1.22 % User time : 0.825 s
% 0.99/1.22 % System time : 0.020 s
% 0.99/1.22 % Total time : 0.845 s
%------------------------------------------------------------------------------