%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB006+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:45 EDT 2024
% Result : Theorem 0.16s 0.48s
% Output : Refutation 0.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : SWB006+2 : TPTP v8.1.2. Released v5.2.0.
% 0.00/0.10 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.30 % Computer : n032.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Wed May 8 22:07:07 EDT 2024
% 0.09/0.31 % CPUTime :
% 0.16/0.48 % Version: 1.5
% 0.16/0.48 % SZS status Theorem
% 0.16/0.48 % SZS output start CNFRefutation
% 0.16/0.48 fof(testcase_conclusion_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes,conjecture,iext(uri_owl_sameAs,uri_ex_u,uri_ex_w),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes)).
% 0.16/0.48 fof(c7,negated_conjecture,(~iext(uri_owl_sameAs,uri_ex_u,uri_ex_w)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes])).
% 0.16/0.48 fof(c8,negated_conjecture,~iext(uri_owl_sameAs,uri_ex_u,uri_ex_w),inference(fof_simplification,[status(thm)],[c7])).
% 0.16/0.48 cnf(c9,negated_conjecture,~iext(uri_owl_sameAs,uri_ex_u,uri_ex_w),inference(split_conjunct,[status(thm)],[c8])).
% 0.16/0.48 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.16/0.48 fof(c10,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.16/0.48 fof(c11,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)],[c10])).
% 0.16/0.48 fof(c13,plain,(![X3]:(![X4]:(![X5]:(![X6]:((~iext(uri_owl_sameAs,X3,X4)|X3=X4)&(X5!=X6|iext(uri_owl_sameAs,X5,X6))))))),inference(shift_quantors,[status(thm)],[fof(c12,plain,((![X3]:(![X4]:(~iext(uri_owl_sameAs,X3,X4)|X3=X4)))&(![X5]:(![X6]:(X5!=X6|iext(uri_owl_sameAs,X5,X6))))),inference(variable_rename,[status(thm)],[c11])).])).
% 0.16/0.48 cnf(c15,plain,X29!=X28|iext(uri_owl_sameAs,X29,X28),inference(split_conjunct,[status(thm)],[c13])).
% 0.16/0.48 cnf(transitivity,axiom,X12!=X13|X13!=X11|X12=X11,theory(equality)).
% 0.16/0.48 fof(testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes,axiom,(?[BNODE_x]:((iext(uri_owl_sameAs,uri_ex_u,literal_plain(dat_str_abc))&iext(uri_owl_sameAs,BNODE_x,literal_plain(dat_str_abc)))&iext(uri_owl_sameAs,BNODE_x,uri_ex_w))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes)).
% 0.16/0.48 fof(c2,plain,(?[X2]:((iext(uri_owl_sameAs,uri_ex_u,literal_plain(dat_str_abc))&iext(uri_owl_sameAs,X2,literal_plain(dat_str_abc)))&iext(uri_owl_sameAs,X2,uri_ex_w))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes])).
% 0.16/0.48 fof(c3,plain,((iext(uri_owl_sameAs,uri_ex_u,literal_plain(dat_str_abc))&iext(uri_owl_sameAs,skolem0001,literal_plain(dat_str_abc)))&iext(uri_owl_sameAs,skolem0001,uri_ex_w)),inference(skolemize,[status(esa)],[c2])).
% 0.16/0.48 cnf(c6,plain,iext(uri_owl_sameAs,skolem0001,uri_ex_w),inference(split_conjunct,[status(thm)],[c3])).
% 0.16/0.48 cnf(c14,plain,~iext(uri_owl_sameAs,X17,X18)|X17=X18,inference(split_conjunct,[status(thm)],[c13])).
% 0.16/0.48 cnf(c19,plain,skolem0001=uri_ex_w,inference(resolution,[status(thm)],[c14, c6])).
% 0.16/0.48 cnf(c24,plain,X32!=skolem0001|X32=uri_ex_w,inference(resolution,[status(thm)],[c19, transitivity])).
% 0.16/0.48 cnf(c4,plain,iext(uri_owl_sameAs,uri_ex_u,literal_plain(dat_str_abc)),inference(split_conjunct,[status(thm)],[c3])).
% 0.16/0.48 cnf(c21,plain,uri_ex_u=literal_plain(dat_str_abc),inference(resolution,[status(thm)],[c14, c4])).
% 0.16/0.48 cnf(symmetry,axiom,X8!=X9|X9=X8,theory(equality)).
% 0.16/0.48 cnf(c5,plain,iext(uri_owl_sameAs,skolem0001,literal_plain(dat_str_abc)),inference(split_conjunct,[status(thm)],[c3])).
% 0.16/0.48 cnf(c20,plain,skolem0001=literal_plain(dat_str_abc),inference(resolution,[status(thm)],[c14, c5])).
% 0.16/0.48 cnf(c29,plain,literal_plain(dat_str_abc)=skolem0001,inference(resolution,[status(thm)],[c20, symmetry])).
% 0.16/0.48 cnf(c39,plain,X36!=literal_plain(dat_str_abc)|X36=skolem0001,inference(resolution,[status(thm)],[c29, transitivity])).
% 0.16/0.48 cnf(c100,plain,uri_ex_u=skolem0001,inference(resolution,[status(thm)],[c39, c21])).
% 0.16/0.48 cnf(c103,plain,uri_ex_u=uri_ex_w,inference(resolution,[status(thm)],[c100, c24])).
% 0.16/0.48 cnf(c118,plain,iext(uri_owl_sameAs,uri_ex_u,uri_ex_w),inference(resolution,[status(thm)],[c103, c15])).
% 0.16/0.48 cnf(c140,plain,$false,inference(resolution,[status(thm)],[c118, c9])).
% 0.16/0.48 % SZS output end CNFRefutation
% 0.16/0.48
% 0.16/0.48 % Initial clauses : 11
% 0.16/0.48 % Processed clauses : 45
% 0.16/0.48 % Factors computed : 1
% 0.16/0.48 % Resolvents computed: 129
% 0.16/0.48 % Tautologies deleted: 2
% 0.16/0.48 % Forward subsumed : 37
% 0.16/0.48 % Backward subsumed : 0
% 0.16/0.48 % -------- CPU Time ---------
% 0.16/0.48 % User time : 0.157 s
% 0.16/0.48 % System time : 0.018 s
% 0.16/0.48 % Total time : 0.175 s
%------------------------------------------------------------------------------