%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB008+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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 0.40s 0.61s
% Output : Refutation 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SWB008+2 : TPTP v8.1.2. Released v5.2.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n022.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:04:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.40/0.61 % Version: 1.5
% 0.40/0.61 % SZS status Theorem
% 0.40/0.61 % SZS output start CNFRefutation
% 0.40/0.61 fof(testcase_conclusion_fullish_008_Inverse_Functional_Data_Properties,conjecture,iext(uri_owl_sameAs,uri_ex_bob,uri_ex_robert),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_008_Inverse_Functional_Data_Properties)).
% 0.40/0.61 fof(c8,negated_conjecture,(~iext(uri_owl_sameAs,uri_ex_bob,uri_ex_robert)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_008_Inverse_Functional_Data_Properties])).
% 0.40/0.61 fof(c9,negated_conjecture,~iext(uri_owl_sameAs,uri_ex_bob,uri_ex_robert),inference(fof_simplification,[status(thm)],[c8])).
% 0.40/0.61 cnf(c10,negated_conjecture,~iext(uri_owl_sameAs,uri_ex_bob,uri_ex_robert),inference(split_conjunct,[status(thm)],[c9])).
% 0.40/0.61 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.40/0.61 fof(c22,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.40/0.61 fof(c23,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)],[c22])).
% 0.40/0.61 fof(c25,plain,(![X10]:(![X11]:(![X12]:(![X13]:((~iext(uri_owl_sameAs,X10,X11)|X10=X11)&(X12!=X13|iext(uri_owl_sameAs,X12,X13))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X10]:(![X11]:(~iext(uri_owl_sameAs,X10,X11)|X10=X11)))&(![X12]:(![X13]:(X12!=X13|iext(uri_owl_sameAs,X12,X13))))),inference(variable_rename,[status(thm)],[c23])).])).
% 0.40/0.61 cnf(c27,plain,X43!=X44|iext(uri_owl_sameAs,X43,X44),inference(split_conjunct,[status(thm)],[c25])).
% 0.40/0.61 cnf(symmetry,axiom,X19!=X20|X20=X19,theory(equality)).
% 0.40/0.61 fof(testcase_premise_fullish_008_Inverse_Functional_Data_Properties,axiom,(((iext(uri_rdf_type,uri_foaf_mbox_sha1sum,uri_owl_DatatypeProperty)&iext(uri_rdf_type,uri_foaf_mbox_sha1sum,uri_owl_InverseFunctionalProperty))&iext(uri_foaf_mbox_sha1sum,uri_ex_bob,literal_plain(dat_str_xyz)))&iext(uri_foaf_mbox_sha1sum,uri_ex_robert,literal_plain(dat_str_xyz))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_008_Inverse_Functional_Data_Properties)).
% 0.40/0.61 cnf(c5,plain,iext(uri_rdf_type,uri_foaf_mbox_sha1sum,uri_owl_InverseFunctionalProperty),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_008_Inverse_Functional_Data_Properties])).
% 0.40/0.61 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.40/0.61 fof(c28,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.40/0.61 fof(c29,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)],[c28])).
% 0.40/0.61 fof(c31,plain,(![X14]:(![X15]:(![X16]:(![X17]:((~iext(uri_rdf_type,X14,X15)|icext(X15,X14))&(~icext(X17,X16)|iext(uri_rdf_type,X16,X17))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X14]:(![X15]:(~iext(uri_rdf_type,X14,X15)|icext(X15,X14))))&(![X16]:(![X17]:(~icext(X17,X16)|iext(uri_rdf_type,X16,X17))))),inference(variable_rename,[status(thm)],[c29])).])).
% 0.40/0.61 cnf(c32,plain,~iext(uri_rdf_type,X48,X47)|icext(X47,X48),inference(split_conjunct,[status(thm)],[c31])).
% 0.40/0.61 cnf(c46,plain,icext(uri_owl_InverseFunctionalProperty,uri_foaf_mbox_sha1sum),inference(resolution,[status(thm)],[c32, c5])).
% 0.40/0.61 cnf(c7,plain,iext(uri_foaf_mbox_sha1sum,uri_ex_robert,literal_plain(dat_str_xyz)),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_008_Inverse_Functional_Data_Properties])).
% 0.40/0.61 cnf(c6,plain,iext(uri_foaf_mbox_sha1sum,uri_ex_bob,literal_plain(dat_str_xyz)),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_008_Inverse_Functional_Data_Properties])).
% 0.40/0.61 fof(owl_char_inversefunctional,axiom,(![P]:(icext(uri_owl_InverseFunctionalProperty,P)<=>(ip(P)&(![X1]:(![X2]:(![Y]:((iext(P,X1,Y)&iext(P,X2,Y))=>X1=X2))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_char_inversefunctional)).
% 0.40/0.61 fof(c11,plain,(![P]:((~icext(uri_owl_InverseFunctionalProperty,P)|(ip(P)&(![X1]:(![X2]:(![Y]:((~iext(P,X1,Y)|~iext(P,X2,Y))|X1=X2))))))&((~ip(P)|(?[X1]:(?[X2]:(?[Y]:((iext(P,X1,Y)&iext(P,X2,Y))&X1!=X2)))))|icext(uri_owl_InverseFunctionalProperty,P)))),inference(fof_nnf,[status(thm)],[owl_char_inversefunctional])).
% 0.40/0.61 fof(c12,plain,((![P]:(~icext(uri_owl_InverseFunctionalProperty,P)|(ip(P)&(![X1]:(![X2]:((![Y]:(~iext(P,X1,Y)|~iext(P,X2,Y)))|X1=X2))))))&(![P]:((~ip(P)|(?[X1]:(?[X2]:((?[Y]:(iext(P,X1,Y)&iext(P,X2,Y)))&X1!=X2))))|icext(uri_owl_InverseFunctionalProperty,P)))),inference(shift_quantors,[status(thm)],[c11])).
% 0.40/0.61 fof(c13,plain,((![X2]:(~icext(uri_owl_InverseFunctionalProperty,X2)|(ip(X2)&(![X3]:(![X4]:((![X5]:(~iext(X2,X3,X5)|~iext(X2,X4,X5)))|X3=X4))))))&(![X6]:((~ip(X6)|(?[X7]:(?[X8]:((?[X9]:(iext(X6,X7,X9)&iext(X6,X8,X9)))&X7!=X8))))|icext(uri_owl_InverseFunctionalProperty,X6)))),inference(variable_rename,[status(thm)],[c12])).
% 0.40/0.61 fof(c15,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:((~icext(uri_owl_InverseFunctionalProperty,X2)|(ip(X2)&((~iext(X2,X3,X5)|~iext(X2,X4,X5))|X3=X4)))&((~ip(X6)|((iext(X6,skolem0001(X6),skolem0003(X6))&iext(X6,skolem0002(X6),skolem0003(X6)))&skolem0001(X6)!=skolem0002(X6)))|icext(uri_owl_InverseFunctionalProperty,X6)))))))),inference(shift_quantors,[status(thm)],[fof(c14,plain,((![X2]:(~icext(uri_owl_InverseFunctionalProperty,X2)|(ip(X2)&(![X3]:(![X4]:((![X5]:(~iext(X2,X3,X5)|~iext(X2,X4,X5)))|X3=X4))))))&(![X6]:((~ip(X6)|((iext(X6,skolem0001(X6),skolem0003(X6))&iext(X6,skolem0002(X6),skolem0003(X6)))&skolem0001(X6)!=skolem0002(X6)))|icext(uri_owl_InverseFunctionalProperty,X6)))),inference(skolemize,[status(esa)],[c13])).])).
% 0.40/0.61 fof(c16,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(((~icext(uri_owl_InverseFunctionalProperty,X2)|ip(X2))&(~icext(uri_owl_InverseFunctionalProperty,X2)|((~iext(X2,X3,X5)|~iext(X2,X4,X5))|X3=X4)))&((((~ip(X6)|iext(X6,skolem0001(X6),skolem0003(X6)))|icext(uri_owl_InverseFunctionalProperty,X6))&((~ip(X6)|iext(X6,skolem0002(X6),skolem0003(X6)))|icext(uri_owl_InverseFunctionalProperty,X6)))&((~ip(X6)|skolem0001(X6)!=skolem0002(X6))|icext(uri_owl_InverseFunctionalProperty,X6))))))))),inference(distribute,[status(thm)],[c15])).
% 0.40/0.61 cnf(c18,plain,~icext(uri_owl_InverseFunctionalProperty,X57)|~iext(X57,X56,X55)|~iext(X57,X58,X55)|X56=X58,inference(split_conjunct,[status(thm)],[c16])).
% 0.40/0.61 cnf(c54,plain,~icext(uri_owl_InverseFunctionalProperty,uri_foaf_mbox_sha1sum)|~iext(uri_foaf_mbox_sha1sum,X112,literal_plain(dat_str_xyz))|X112=uri_ex_bob,inference(resolution,[status(thm)],[c18, c6])).
% 0.40/0.61 cnf(c87,plain,~icext(uri_owl_InverseFunctionalProperty,uri_foaf_mbox_sha1sum)|uri_ex_robert=uri_ex_bob,inference(resolution,[status(thm)],[c54, c7])).
% 0.40/0.61 cnf(c88,plain,uri_ex_robert=uri_ex_bob,inference(resolution,[status(thm)],[c87, c46])).
% 0.40/0.61 cnf(c93,plain,uri_ex_bob=uri_ex_robert,inference(resolution,[status(thm)],[c88, symmetry])).
% 0.40/0.61 cnf(c102,plain,iext(uri_owl_sameAs,uri_ex_bob,uri_ex_robert),inference(resolution,[status(thm)],[c93, c27])).
% 0.40/0.61 cnf(c108,plain,$false,inference(resolution,[status(thm)],[c102, c10])).
% 0.40/0.61 % SZS output end CNFRefutation
% 0.40/0.61
% 0.40/0.61 % Initial clauses : 21
% 0.40/0.61 % Processed clauses : 55
% 0.40/0.61 % Factors computed : 7
% 0.40/0.61 % Resolvents computed: 72
% 0.40/0.61 % Tautologies deleted: 3
% 0.40/0.61 % Forward subsumed : 20
% 0.40/0.61 % Backward subsumed : 3
% 0.40/0.61 % -------- CPU Time ---------
% 0.40/0.61 % User time : 0.241 s
% 0.40/0.61 % System time : 0.010 s
% 0.40/0.61 % Total time : 0.251 s
%------------------------------------------------------------------------------