%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB023+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:53 EDT 2024
% Result : Theorem 0.49s 0.72s
% Output : Refutation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWB023+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 : 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:03:52 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.49/0.72 % Version: 1.5
% 0.49/0.72 % SZS status Theorem
% 0.49/0.72 % SZS output start CNFRefutation
% 0.49/0.72 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.49/0.72 fof(c16,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.49/0.72 fof(c17,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)],[c16])).
% 0.49/0.72 fof(c19,plain,(![X4]:(![X5]:(![X6]:(![X7]:((~iext(uri_owl_sameAs,X4,X5)|X4=X5)&(X6!=X7|iext(uri_owl_sameAs,X6,X7))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,((![X4]:(![X5]:(~iext(uri_owl_sameAs,X4,X5)|X4=X5)))&(![X6]:(![X7]:(X6!=X7|iext(uri_owl_sameAs,X6,X7))))),inference(variable_rename,[status(thm)],[c17])).])).
% 0.49/0.72 cnf(c21,plain,X56!=X55|iext(uri_owl_sameAs,X56,X55),inference(split_conjunct,[status(thm)],[c19])).
% 0.49/0.72 fof(testcase_premise_fullish_023_Unique_List_Components,axiom,(?[BNODE_o]:(?[BNODE_l]:((((((iext(uri_rdf_type,uri_rdf_first,uri_owl_FunctionalProperty)&iext(uri_rdf_type,uri_ex_w,BNODE_o))&iext(uri_rdf_type,BNODE_o,uri_owl_Class))&iext(uri_owl_oneOf,BNODE_o,BNODE_l))&iext(uri_rdf_first,BNODE_l,uri_ex_u))&iext(uri_rdf_first,BNODE_l,uri_ex_v))&iext(uri_rdf_rest,BNODE_l,uri_rdf_nil)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_023_Unique_List_Components)).
% 0.49/0.72 fof(c4,plain,(?[X2]:(?[X3]:((((((iext(uri_rdf_type,uri_rdf_first,uri_owl_FunctionalProperty)&iext(uri_rdf_type,uri_ex_w,X2))&iext(uri_rdf_type,X2,uri_owl_Class))&iext(uri_owl_oneOf,X2,X3))&iext(uri_rdf_first,X3,uri_ex_u))&iext(uri_rdf_first,X3,uri_ex_v))&iext(uri_rdf_rest,X3,uri_rdf_nil)))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_023_Unique_List_Components])).
% 0.49/0.72 fof(c5,plain,((((((iext(uri_rdf_type,uri_rdf_first,uri_owl_FunctionalProperty)&iext(uri_rdf_type,uri_ex_w,skolem0001))&iext(uri_rdf_type,skolem0001,uri_owl_Class))&iext(uri_owl_oneOf,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,uri_ex_u))&iext(uri_rdf_first,skolem0002,uri_ex_v))&iext(uri_rdf_rest,skolem0002,uri_rdf_nil)),inference(skolemize,[status(esa)],[c4])).
% 0.49/0.72 cnf(c7,plain,iext(uri_rdf_type,uri_ex_w,skolem0001),inference(split_conjunct,[status(thm)],[c5])).
% 0.49/0.72 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.49/0.72 fof(c44,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.49/0.72 fof(c45,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)],[c44])).
% 0.49/0.72 fof(c47,plain,(![X22]:(![X23]:(![X24]:(![X25]:((~iext(uri_rdf_type,X22,X23)|icext(X23,X22))&(~icext(X25,X24)|iext(uri_rdf_type,X24,X25))))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X22]:(![X23]:(~iext(uri_rdf_type,X22,X23)|icext(X23,X22))))&(![X24]:(![X25]:(~icext(X25,X24)|iext(uri_rdf_type,X24,X25))))),inference(variable_rename,[status(thm)],[c45])).])).
% 0.49/0.72 cnf(c48,plain,~iext(uri_rdf_type,X60,X59)|icext(X59,X60),inference(split_conjunct,[status(thm)],[c47])).
% 0.49/0.72 cnf(c67,plain,icext(skolem0001,uri_ex_w),inference(resolution,[status(thm)],[c48, c7])).
% 0.49/0.72 cnf(c10,plain,iext(uri_rdf_first,skolem0002,uri_ex_u),inference(split_conjunct,[status(thm)],[c5])).
% 0.49/0.72 cnf(c12,plain,iext(uri_rdf_rest,skolem0002,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c5])).
% 0.49/0.72 cnf(c9,plain,iext(uri_owl_oneOf,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c5])).
% 0.49/0.72 fof(owl_enum_class_001,axiom,(![Z]:(![S1]:(![A1]:((iext(uri_rdf_first,S1,A1)&iext(uri_rdf_rest,S1,uri_rdf_nil))=>(iext(uri_owl_oneOf,Z,S1)<=>(ic(Z)&(![X]:(icext(Z,X)<=>X=A1)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_enum_class_001)).
% 0.49/0.72 fof(c33,plain,(![Z]:(![S1]:(![A1]:((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&(![X]:((~icext(Z,X)|X=A1)&(X!=A1|icext(Z,X))))))&((~ic(Z)|(?[X]:((~icext(Z,X)|X!=A1)&(icext(Z,X)|X=A1))))|iext(uri_owl_oneOf,Z,S1))))))),inference(fof_nnf,[status(thm)],[owl_enum_class_001])).
% 0.49/0.72 fof(c34,plain,(![Z]:(![S1]:(![A1]:((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]:(~icext(Z,X)|X=A1))&(![X]:(X!=A1|icext(Z,X))))))&((~ic(Z)|(?[X]:((~icext(Z,X)|X!=A1)&(icext(Z,X)|X=A1))))|iext(uri_owl_oneOf,Z,S1))))))),inference(shift_quantors,[status(thm)],[c33])).
% 0.49/0.72 fof(c35,plain,(![X16]:(![X17]:(![X18]:((~iext(uri_rdf_first,X17,X18)|~iext(uri_rdf_rest,X17,uri_rdf_nil))|((~iext(uri_owl_oneOf,X16,X17)|(ic(X16)&((![X19]:(~icext(X16,X19)|X19=X18))&(![X20]:(X20!=X18|icext(X16,X20))))))&((~ic(X16)|(?[X21]:((~icext(X16,X21)|X21!=X18)&(icext(X16,X21)|X21=X18))))|iext(uri_owl_oneOf,X16,X17))))))),inference(variable_rename,[status(thm)],[c34])).
% 0.49/0.72 fof(c37,plain,(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((~iext(uri_rdf_first,X17,X18)|~iext(uri_rdf_rest,X17,uri_rdf_nil))|((~iext(uri_owl_oneOf,X16,X17)|(ic(X16)&((~icext(X16,X19)|X19=X18)&(X20!=X18|icext(X16,X20)))))&((~ic(X16)|((~icext(X16,skolem0006(X16,X17,X18))|skolem0006(X16,X17,X18)!=X18)&(icext(X16,skolem0006(X16,X17,X18))|skolem0006(X16,X17,X18)=X18)))|iext(uri_owl_oneOf,X16,X17))))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,(![X16]:(![X17]:(![X18]:((~iext(uri_rdf_first,X17,X18)|~iext(uri_rdf_rest,X17,uri_rdf_nil))|((~iext(uri_owl_oneOf,X16,X17)|(ic(X16)&((![X19]:(~icext(X16,X19)|X19=X18))&(![X20]:(X20!=X18|icext(X16,X20))))))&((~ic(X16)|((~icext(X16,skolem0006(X16,X17,X18))|skolem0006(X16,X17,X18)!=X18)&(icext(X16,skolem0006(X16,X17,X18))|skolem0006(X16,X17,X18)=X18)))|iext(uri_owl_oneOf,X16,X17))))))),inference(skolemize,[status(esa)],[c35])).])).
% 0.49/0.72 fof(c38,plain,(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((((~iext(uri_rdf_first,X17,X18)|~iext(uri_rdf_rest,X17,uri_rdf_nil))|(~iext(uri_owl_oneOf,X16,X17)|ic(X16)))&(((~iext(uri_rdf_first,X17,X18)|~iext(uri_rdf_rest,X17,uri_rdf_nil))|(~iext(uri_owl_oneOf,X16,X17)|(~icext(X16,X19)|X19=X18)))&((~iext(uri_rdf_first,X17,X18)|~iext(uri_rdf_rest,X17,uri_rdf_nil))|(~iext(uri_owl_oneOf,X16,X17)|(X20!=X18|icext(X16,X20))))))&(((~iext(uri_rdf_first,X17,X18)|~iext(uri_rdf_rest,X17,uri_rdf_nil))|((~ic(X16)|(~icext(X16,skolem0006(X16,X17,X18))|skolem0006(X16,X17,X18)!=X18))|iext(uri_owl_oneOf,X16,X17)))&((~iext(uri_rdf_first,X17,X18)|~iext(uri_rdf_rest,X17,uri_rdf_nil))|((~ic(X16)|(icext(X16,skolem0006(X16,X17,X18))|skolem0006(X16,X17,X18)=X18))|iext(uri_owl_oneOf,X16,X17)))))))))),inference(distribute,[status(thm)],[c37])).
% 0.49/0.72 cnf(c40,plain,~iext(uri_rdf_first,X107,X104)|~iext(uri_rdf_rest,X107,uri_rdf_nil)|~iext(uri_owl_oneOf,X106,X107)|~icext(X106,X105)|X105=X104,inference(split_conjunct,[status(thm)],[c38])).
% 0.49/0.72 cnf(c103,plain,~iext(uri_rdf_first,skolem0002,X192)|~iext(uri_rdf_rest,skolem0002,uri_rdf_nil)|~icext(skolem0001,X193)|X193=X192,inference(resolution,[status(thm)],[c40, c9])).
% 0.49/0.72 cnf(c182,plain,~iext(uri_rdf_first,skolem0002,X194)|~icext(skolem0001,X195)|X195=X194,inference(resolution,[status(thm)],[c103, c12])).
% 0.49/0.72 cnf(c183,plain,~icext(skolem0001,X196)|X196=uri_ex_u,inference(resolution,[status(thm)],[c182, c10])).
% 0.49/0.72 cnf(c185,plain,uri_ex_w=uri_ex_u,inference(resolution,[status(thm)],[c183, c67])).
% 0.49/0.72 cnf(c195,plain,iext(uri_owl_sameAs,uri_ex_w,uri_ex_u),inference(resolution,[status(thm)],[c185, c21])).
% 0.49/0.72 fof(testcase_conclusion_fullish_023_Unique_List_Components,conjecture,(iext(uri_owl_sameAs,uri_ex_w,uri_ex_u)&iext(uri_owl_sameAs,uri_ex_w,uri_ex_v)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_023_Unique_List_Components)).
% 0.49/0.72 fof(c13,negated_conjecture,(~(iext(uri_owl_sameAs,uri_ex_w,uri_ex_u)&iext(uri_owl_sameAs,uri_ex_w,uri_ex_v))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_023_Unique_List_Components])).
% 0.49/0.72 fof(c14,negated_conjecture,(~iext(uri_owl_sameAs,uri_ex_w,uri_ex_u)|~iext(uri_owl_sameAs,uri_ex_w,uri_ex_v)),inference(fof_nnf,[status(thm)],[c13])).
% 0.49/0.72 cnf(c15,negated_conjecture,~iext(uri_owl_sameAs,uri_ex_w,uri_ex_u)|~iext(uri_owl_sameAs,uri_ex_w,uri_ex_v),inference(split_conjunct,[status(thm)],[c14])).
% 0.49/0.72 cnf(transitivity,axiom,X31!=X30|X30!=X32|X31=X32,theory(equality)).
% 0.49/0.72 cnf(symmetry,axiom,X28!=X27|X27=X28,theory(equality)).
% 0.49/0.72 cnf(c6,plain,iext(uri_rdf_type,uri_rdf_first,uri_owl_FunctionalProperty),inference(split_conjunct,[status(thm)],[c5])).
% 0.49/0.72 cnf(c65,plain,icext(uri_owl_FunctionalProperty,uri_rdf_first),inference(resolution,[status(thm)],[c48, c6])).
% 0.49/0.72 cnf(c11,plain,iext(uri_rdf_first,skolem0002,uri_ex_v),inference(split_conjunct,[status(thm)],[c5])).
% 0.49/0.72 fof(owl_char_functional,axiom,(![P]:(icext(uri_owl_FunctionalProperty,P)<=>(ip(P)&(![X]:(![Y1]:(![Y2]:((iext(P,X,Y1)&iext(P,X,Y2))=>Y1=Y2))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_char_functional)).
% 0.49/0.72 fof(c22,plain,(![P]:((~icext(uri_owl_FunctionalProperty,P)|(ip(P)&(![X]:(![Y1]:(![Y2]:((~iext(P,X,Y1)|~iext(P,X,Y2))|Y1=Y2))))))&((~ip(P)|(?[X]:(?[Y1]:(?[Y2]:((iext(P,X,Y1)&iext(P,X,Y2))&Y1!=Y2)))))|icext(uri_owl_FunctionalProperty,P)))),inference(fof_nnf,[status(thm)],[owl_char_functional])).
% 0.49/0.72 fof(c23,plain,((![P]:(~icext(uri_owl_FunctionalProperty,P)|(ip(P)&(![X]:(![Y1]:(![Y2]:((~iext(P,X,Y1)|~iext(P,X,Y2))|Y1=Y2)))))))&(![P]:((~ip(P)|(?[X]:(?[Y1]:(?[Y2]:((iext(P,X,Y1)&iext(P,X,Y2))&Y1!=Y2)))))|icext(uri_owl_FunctionalProperty,P)))),inference(shift_quantors,[status(thm)],[c22])).
% 0.49/0.72 fof(c24,plain,((![X8]:(~icext(uri_owl_FunctionalProperty,X8)|(ip(X8)&(![X9]:(![X10]:(![X11]:((~iext(X8,X9,X10)|~iext(X8,X9,X11))|X10=X11)))))))&(![X12]:((~ip(X12)|(?[X13]:(?[X14]:(?[X15]:((iext(X12,X13,X14)&iext(X12,X13,X15))&X14!=X15)))))|icext(uri_owl_FunctionalProperty,X12)))),inference(variable_rename,[status(thm)],[c23])).
% 0.49/0.72 fof(c26,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((~icext(uri_owl_FunctionalProperty,X8)|(ip(X8)&((~iext(X8,X9,X10)|~iext(X8,X9,X11))|X10=X11)))&((~ip(X12)|((iext(X12,skolem0003(X12),skolem0004(X12))&iext(X12,skolem0003(X12),skolem0005(X12)))&skolem0004(X12)!=skolem0005(X12)))|icext(uri_owl_FunctionalProperty,X12)))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,((![X8]:(~icext(uri_owl_FunctionalProperty,X8)|(ip(X8)&(![X9]:(![X10]:(![X11]:((~iext(X8,X9,X10)|~iext(X8,X9,X11))|X10=X11)))))))&(![X12]:((~ip(X12)|((iext(X12,skolem0003(X12),skolem0004(X12))&iext(X12,skolem0003(X12),skolem0005(X12)))&skolem0004(X12)!=skolem0005(X12)))|icext(uri_owl_FunctionalProperty,X12)))),inference(skolemize,[status(esa)],[c24])).])).
% 0.49/0.72 fof(c27,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(((~icext(uri_owl_FunctionalProperty,X8)|ip(X8))&(~icext(uri_owl_FunctionalProperty,X8)|((~iext(X8,X9,X10)|~iext(X8,X9,X11))|X10=X11)))&((((~ip(X12)|iext(X12,skolem0003(X12),skolem0004(X12)))|icext(uri_owl_FunctionalProperty,X12))&((~ip(X12)|iext(X12,skolem0003(X12),skolem0005(X12)))|icext(uri_owl_FunctionalProperty,X12)))&((~ip(X12)|skolem0004(X12)!=skolem0005(X12))|icext(uri_owl_FunctionalProperty,X12))))))))),inference(distribute,[status(thm)],[c26])).
% 0.49/0.72 cnf(c29,plain,~icext(uri_owl_FunctionalProperty,X63)|~iext(X63,X64,X61)|~iext(X63,X64,X62)|X61=X62,inference(split_conjunct,[status(thm)],[c27])).
% 0.49/0.72 cnf(c72,plain,~icext(uri_owl_FunctionalProperty,uri_rdf_first)|~iext(uri_rdf_first,skolem0002,X117)|X117=uri_ex_u,inference(resolution,[status(thm)],[c29, c10])).
% 0.49/0.72 cnf(c110,plain,~icext(uri_owl_FunctionalProperty,uri_rdf_first)|uri_ex_v=uri_ex_u,inference(resolution,[status(thm)],[c72, c11])).
% 0.49/0.72 cnf(c111,plain,uri_ex_v=uri_ex_u,inference(resolution,[status(thm)],[c110, c65])).
% 0.49/0.72 cnf(c116,plain,uri_ex_u=uri_ex_v,inference(resolution,[status(thm)],[c111, symmetry])).
% 0.49/0.72 cnf(c120,plain,X128!=uri_ex_u|X128=uri_ex_v,inference(resolution,[status(thm)],[c116, transitivity])).
% 0.49/0.72 cnf(c187,plain,uri_ex_w=uri_ex_v,inference(resolution,[status(thm)],[c185, c120])).
% 0.49/0.72 cnf(c205,plain,iext(uri_owl_sameAs,uri_ex_w,uri_ex_v),inference(resolution,[status(thm)],[c187, c21])).
% 0.49/0.72 cnf(c237,plain,~iext(uri_owl_sameAs,uri_ex_w,uri_ex_u),inference(resolution,[status(thm)],[c205, c15])).
% 0.49/0.72 cnf(c253,plain,$false,inference(resolution,[status(thm)],[c237, c195])).
% 0.49/0.72 % SZS output end CNFRefutation
% 0.49/0.72
% 0.49/0.72 % Initial clauses : 29
% 0.49/0.72 % Processed clauses : 122
% 0.49/0.72 % Factors computed : 7
% 0.49/0.72 % Resolvents computed: 197
% 0.49/0.72 % Tautologies deleted: 4
% 0.49/0.72 % Forward subsumed : 63
% 0.49/0.72 % Backward subsumed : 7
% 0.49/0.72 % -------- CPU Time ---------
% 0.49/0.72 % User time : 0.350 s
% 0.49/0.72 % System time : 0.012 s
% 0.49/0.72 % Total time : 0.362 s
%------------------------------------------------------------------------------