%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB011+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:47 EDT 2024
% Result : Unsatisfiable 0.22s 0.54s
% Output : Refutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWB011+2 : TPTP v8.1.2. Released v5.2.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n007.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 22:08:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.22/0.54 % Version: 1.5
% 0.22/0.54 % SZS status Unsatisfiable
% 0.22/0.54 % SZS output start CNFRefutation
% 0.22/0.54 fof(testcase_premise_fullish_011_Entity_Types_as_Classes,axiom,((iext(uri_owl_disjointWith,uri_owl_Class,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_x,uri_owl_Class))&iext(uri_rdf_type,uri_ex_x,uri_owl_ObjectProperty)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_011_Entity_Types_as_Classes)).
% 0.22/0.54 cnf(c1,plain,iext(uri_rdf_type,uri_ex_x,uri_owl_Class),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_011_Entity_Types_as_Classes])).
% 0.22/0.54 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rdfs_cext_def)).
% 0.22/0.54 fof(c14,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.22/0.54 fof(c15,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)],[c14])).
% 0.22/0.54 fof(c17,plain,(![X8]:(![X9]:(![X10]:(![X11]:((~iext(uri_rdf_type,X8,X9)|icext(X9,X8))&(~icext(X11,X10)|iext(uri_rdf_type,X10,X11))))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,((![X8]:(![X9]:(~iext(uri_rdf_type,X8,X9)|icext(X9,X8))))&(![X10]:(![X11]:(~icext(X11,X10)|iext(uri_rdf_type,X10,X11))))),inference(variable_rename,[status(thm)],[c15])).])).
% 0.22/0.54 cnf(c18,plain,~iext(uri_rdf_type,X16,X17)|icext(X17,X16),inference(split_conjunct,[status(thm)],[c17])).
% 0.22/0.54 cnf(c23,plain,icext(uri_owl_Class,uri_ex_x),inference(resolution,[status(thm)],[c18, c1])).
% 0.22/0.54 cnf(c2,plain,iext(uri_rdf_type,uri_ex_x,uri_owl_ObjectProperty),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_011_Entity_Types_as_Classes])).
% 0.22/0.54 cnf(c22,plain,icext(uri_owl_ObjectProperty,uri_ex_x),inference(resolution,[status(thm)],[c18, c2])).
% 0.22/0.54 cnf(c0,plain,iext(uri_owl_disjointWith,uri_owl_Class,uri_owl_ObjectProperty),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_011_Entity_Types_as_Classes])).
% 0.22/0.54 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.22/0.54 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.22/0.54 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.22/0.54 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.22/0.54 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.22/0.54 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.22/0.54 cnf(c11,plain,~iext(uri_owl_disjointWith,X21,X22)|~icext(X21,X20)|~icext(X22,X20),inference(split_conjunct,[status(thm)],[c8])).
% 0.22/0.54 cnf(c26,plain,~icext(uri_owl_Class,X23)|~icext(uri_owl_ObjectProperty,X23),inference(resolution,[status(thm)],[c11, c0])).
% 0.22/0.54 cnf(c27,plain,~icext(uri_owl_Class,uri_ex_x),inference(resolution,[status(thm)],[c26, c22])).
% 0.22/0.54 cnf(c28,plain,$false,inference(resolution,[status(thm)],[c27, c23])).
% 0.22/0.54 % SZS output end CNFRefutation
% 0.22/0.54
% 0.22/0.54 % Initial clauses : 10
% 0.22/0.54 % Processed clauses : 14
% 0.22/0.54 % Factors computed : 0
% 0.22/0.54 % Resolvents computed: 9
% 0.22/0.54 % Tautologies deleted: 0
% 0.22/0.54 % Forward subsumed : 2
% 0.22/0.54 % Backward subsumed : 0
% 0.22/0.54 % -------- CPU Time ---------
% 0.22/0.54 % User time : 0.168 s
% 0.22/0.54 % System time : 0.016 s
% 0.22/0.54 % Total time : 0.184 s
%------------------------------------------------------------------------------