%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB018+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:51 EDT 2024
% Result : Theorem 0.38s 0.54s
% Output : Refutation 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SWB018+2 : TPTP v8.1.2. Released v5.2.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n019.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:09:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.38/0.54 % Version: 1.5
% 0.38/0.54 % SZS status Theorem
% 0.38/0.54 % SZS output start CNFRefutation
% 0.38/0.54 fof(testcase_conclusion_fullish_018_Modified_Logical_Vocabulary_Semantics,conjecture,iext(uri_rdf_type,uri_ex_u,uri_ex_Person),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_018_Modified_Logical_Vocabulary_Semantics)).
% 0.38/0.54 fof(c4,negated_conjecture,(~iext(uri_rdf_type,uri_ex_u,uri_ex_Person)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_018_Modified_Logical_Vocabulary_Semantics])).
% 0.38/0.54 fof(c5,negated_conjecture,~iext(uri_rdf_type,uri_ex_u,uri_ex_Person),inference(fof_simplification,[status(thm)],[c4])).
% 0.38/0.54 cnf(c6,negated_conjecture,~iext(uri_rdf_type,uri_ex_u,uri_ex_Person),inference(split_conjunct,[status(thm)],[c5])).
% 0.38/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.38/0.54 fof(c18,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.38/0.54 fof(c19,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)],[c18])).
% 0.38/0.54 fof(c21,plain,(![X10]:(![X11]:(![X12]:(![X13]:((~iext(uri_rdf_type,X10,X11)|icext(X11,X10))&(~icext(X13,X12)|iext(uri_rdf_type,X12,X13))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((![X10]:(![X11]:(~iext(uri_rdf_type,X10,X11)|icext(X11,X10))))&(![X12]:(![X13]:(~icext(X13,X12)|iext(uri_rdf_type,X12,X13))))),inference(variable_rename,[status(thm)],[c19])).])).
% 0.38/0.54 cnf(c23,plain,~icext(X43,X42)|iext(uri_rdf_type,X42,X43),inference(split_conjunct,[status(thm)],[c21])).
% 0.38/0.54 fof(testcase_premise_fullish_018_Modified_Logical_Vocabulary_Semantics,axiom,(iext(uri_rdfs_domain,uri_owl_sameAs,uri_ex_Person)&iext(uri_owl_sameAs,uri_ex_w,uri_ex_u)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_018_Modified_Logical_Vocabulary_Semantics)).
% 0.38/0.54 cnf(c2,plain,iext(uri_rdfs_domain,uri_owl_sameAs,uri_ex_Person),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_018_Modified_Logical_Vocabulary_Semantics])).
% 0.38/0.54 cnf(reflexivity,axiom,X14=X14,theory(equality)).
% 0.38/0.54 fof(owl_eqdis_sameas,axiom,(![X]:(![Y]:(iext(uri_owl_sameAs,X,Y)<=>X=Y))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_eqdis_sameas)).
% 0.38/0.54 fof(c7,plain,(![X]:(![Y]:((~iext(uri_owl_sameAs,X,Y)|X=Y)&(X!=Y|iext(uri_owl_sameAs,X,Y))))),inference(fof_nnf,[status(thm)],[owl_eqdis_sameas])).
% 0.38/0.54 fof(c8,plain,((![X]:(![Y]:(~iext(uri_owl_sameAs,X,Y)|X=Y)))&(![X]:(![Y]:(X!=Y|iext(uri_owl_sameAs,X,Y))))),inference(shift_quantors,[status(thm)],[c7])).
% 0.38/0.54 fof(c10,plain,(![X2]:(![X3]:(![X4]:(![X5]:((~iext(uri_owl_sameAs,X2,X3)|X2=X3)&(X4!=X5|iext(uri_owl_sameAs,X4,X5))))))),inference(shift_quantors,[status(thm)],[fof(c9,plain,((![X2]:(![X3]:(~iext(uri_owl_sameAs,X2,X3)|X2=X3)))&(![X4]:(![X5]:(X4!=X5|iext(uri_owl_sameAs,X4,X5))))),inference(variable_rename,[status(thm)],[c8])).])).
% 0.38/0.54 cnf(c12,plain,X33!=X32|iext(uri_owl_sameAs,X33,X32),inference(split_conjunct,[status(thm)],[c10])).
% 0.38/0.54 cnf(c36,plain,iext(uri_owl_sameAs,X34,X34),inference(resolution,[status(thm)],[c12, reflexivity])).
% 0.38/0.54 fof(rdfs_domain_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_domain,P,C)&iext(P,X,Y))=>icext(C,X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rdfs_domain_main)).
% 0.38/0.54 fof(c13,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_domain,P,C)|~iext(P,X,Y))|icext(C,X)))))),inference(fof_nnf,[status(thm)],[rdfs_domain_main])).
% 0.38/0.54 fof(c14,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c13])).
% 0.38/0.54 fof(c16,plain,(![X6]:(![X7]:(![X8]:(![X9]:((~iext(uri_rdfs_domain,X6,X7)|~iext(X6,X8,X9))|icext(X7,X8)))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,(![X6]:(![X7]:(![X8]:((~iext(uri_rdfs_domain,X6,X7)|(![X9]:~iext(X6,X8,X9)))|icext(X7,X8))))),inference(variable_rename,[status(thm)],[c14])).])).
% 0.38/0.54 cnf(c17,plain,~iext(uri_rdfs_domain,X45,X47)|~iext(X45,X46,X44)|icext(X47,X46),inference(split_conjunct,[status(thm)],[c16])).
% 0.38/0.55 cnf(c43,plain,~iext(uri_rdfs_domain,uri_owl_sameAs,X54)|icext(X54,X53),inference(resolution,[status(thm)],[c17, c36])).
% 0.38/0.55 cnf(c52,plain,icext(uri_ex_Person,X55),inference(resolution,[status(thm)],[c43, c2])).
% 0.38/0.55 cnf(c53,plain,iext(uri_rdf_type,X56,uri_ex_Person),inference(resolution,[status(thm)],[c52, c23])).
% 0.38/0.55 cnf(c57,plain,$false,inference(resolution,[status(thm)],[c53, c6])).
% 0.38/0.55 % SZS output end CNFRefutation
% 0.38/0.55
% 0.38/0.55 % Initial clauses : 13
% 0.38/0.55 % Processed clauses : 23
% 0.38/0.55 % Factors computed : 2
% 0.38/0.55 % Resolvents computed: 33
% 0.38/0.55 % Tautologies deleted: 2
% 0.38/0.55 % Forward subsumed : 9
% 0.38/0.55 % Backward subsumed : 0
% 0.38/0.55 % -------- CPU Time ---------
% 0.38/0.55 % User time : 0.172 s
% 0.38/0.55 % System time : 0.023 s
% 0.38/0.55 % Total time : 0.195 s
%------------------------------------------------------------------------------