%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB014+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:49 EDT 2024
% Result : Theorem 0.48s 0.63s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SWB014+2 : TPTP v8.1.2. Released v5.2.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n005.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Wed May 8 22:09:08 EDT 2024
% 0.15/0.35 % CPUTime :
% 0.48/0.63 % Version: 1.5
% 0.48/0.63 % SZS status Theorem
% 0.48/0.63 % SZS output start CNFRefutation
% 0.48/0.63 fof(testcase_premise_fullish_014_Harry_belongs_to_some_Species,axiom,(?[BNODE_u]:(?[BNODE_l1]:(?[BNODE_l2]:(((((((iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)&iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species))&iext(uri_rdf_type,uri_ex_harry,BNODE_u))&iext(uri_owl_unionOf,BNODE_u,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_ex_Eagle))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,uri_ex_Falcon))&iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_014_Harry_belongs_to_some_Species)).
% 0.48/0.63 fof(c0,plain,(?[X2]:(?[X3]:(?[X4]:(((((((iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)&iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species))&iext(uri_rdf_type,uri_ex_harry,X2))&iext(uri_owl_unionOf,X2,X3))&iext(uri_rdf_first,X3,uri_ex_Eagle))&iext(uri_rdf_rest,X3,X4))&iext(uri_rdf_first,X4,uri_ex_Falcon))&iext(uri_rdf_rest,X4,uri_rdf_nil))))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_014_Harry_belongs_to_some_Species])).
% 0.48/0.63 fof(c1,plain,(((((((iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)&iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species))&iext(uri_rdf_type,uri_ex_harry,skolem0001))&iext(uri_owl_unionOf,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,uri_ex_Eagle))&iext(uri_rdf_rest,skolem0002,skolem0003))&iext(uri_rdf_first,skolem0003,uri_ex_Falcon))&iext(uri_rdf_rest,skolem0003,uri_rdf_nil)),inference(skolemize,[status(esa)],[c0])).
% 0.48/0.63 cnf(c3,plain,iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species),inference(split_conjunct,[status(thm)],[c1])).
% 0.48/0.63 fof(testcase_conclusion_fullish_014_Harry_belongs_to_some_Species,conjecture,(?[BNODE_x]:(iext(uri_rdf_type,uri_ex_harry,BNODE_x)&iext(uri_rdf_type,BNODE_x,uri_ex_Species))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_conclusion_fullish_014_Harry_belongs_to_some_Species)).
% 0.48/0.63 fof(c10,negated_conjecture,(~(?[BNODE_x]:(iext(uri_rdf_type,uri_ex_harry,BNODE_x)&iext(uri_rdf_type,BNODE_x,uri_ex_Species)))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_014_Harry_belongs_to_some_Species])).
% 0.48/0.63 fof(c11,negated_conjecture,(![BNODE_x]:(~iext(uri_rdf_type,uri_ex_harry,BNODE_x)|~iext(uri_rdf_type,BNODE_x,uri_ex_Species))),inference(fof_nnf,[status(thm)],[c10])).
% 0.48/0.63 fof(c12,negated_conjecture,(![X5]:(~iext(uri_rdf_type,uri_ex_harry,X5)|~iext(uri_rdf_type,X5,uri_ex_Species))),inference(variable_rename,[status(thm)],[c11])).
% 0.48/0.63 cnf(c13,negated_conjecture,~iext(uri_rdf_type,uri_ex_harry,X20)|~iext(uri_rdf_type,X20,uri_ex_Species),inference(split_conjunct,[status(thm)],[c12])).
% 0.48/0.63 cnf(c39,plain,~iext(uri_rdf_type,uri_ex_harry,uri_ex_Falcon),inference(resolution,[status(thm)],[c13, c3])).
% 0.48/0.63 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rdfs_cext_def)).
% 0.48/0.63 fof(c29,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.48/0.63 fof(c30,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)],[c29])).
% 0.48/0.63 fof(c32,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(c31,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)],[c30])).])).
% 0.48/0.63 cnf(c34,plain,~icext(X22,X21)|iext(uri_rdf_type,X21,X22),inference(split_conjunct,[status(thm)],[c32])).
% 0.48/0.63 cnf(c2,plain,iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species),inference(split_conjunct,[status(thm)],[c1])).
% 0.48/0.63 cnf(c38,plain,~iext(uri_rdf_type,uri_ex_harry,uri_ex_Eagle),inference(resolution,[status(thm)],[c13, c2])).
% 0.48/0.63 cnf(c4,plain,iext(uri_rdf_type,uri_ex_harry,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 0.48/0.63 cnf(c33,plain,~iext(uri_rdf_type,X18,X19)|icext(X19,X18),inference(split_conjunct,[status(thm)],[c32])).
% 0.48/0.63 cnf(c36,plain,icext(skolem0001,uri_ex_harry),inference(resolution,[status(thm)],[c33, c4])).
% 0.48/0.63 cnf(c6,plain,iext(uri_rdf_first,skolem0002,uri_ex_Eagle),inference(split_conjunct,[status(thm)],[c1])).
% 0.48/0.63 cnf(c7,plain,iext(uri_rdf_rest,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c1])).
% 0.48/0.63 cnf(c8,plain,iext(uri_rdf_first,skolem0003,uri_ex_Falcon),inference(split_conjunct,[status(thm)],[c1])).
% 0.48/0.63 cnf(c9,plain,iext(uri_rdf_rest,skolem0003,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 0.48/0.63 cnf(c5,plain,iext(uri_owl_unionOf,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c1])).
% 0.48/0.63 fof(owl_bool_unionof_class_002,axiom,(![Z]:(![S1]:(![C1]:(![S2]:(![C2]:((((iext(uri_rdf_first,S1,C1)&iext(uri_rdf_rest,S1,S2))&iext(uri_rdf_first,S2,C2))&iext(uri_rdf_rest,S2,uri_rdf_nil))=>(iext(uri_owl_unionOf,Z,S1)<=>(((ic(Z)&ic(C1))&ic(C2))&(![X]:(icext(Z,X)<=>(icext(C1,X)|icext(C2,X)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_bool_unionof_class_002)).
% 0.48/0.63 fof(c14,plain,(![Z]:(![S1]:(![C1]:(![S2]:(![C2]:((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|((~iext(uri_owl_unionOf,Z,S1)|(((ic(Z)&ic(C1))&ic(C2))&(![X]:((~icext(Z,X)|(icext(C1,X)|icext(C2,X)))&((~icext(C1,X)&~icext(C2,X))|icext(Z,X))))))&((((~ic(Z)|~ic(C1))|~ic(C2))|(?[X]:((~icext(Z,X)|(~icext(C1,X)&~icext(C2,X)))&(icext(Z,X)|(icext(C1,X)|icext(C2,X))))))|iext(uri_owl_unionOf,Z,S1))))))))),inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_002])).
% 0.48/0.63 fof(c15,plain,(![Z]:(![S1]:(![C1]:(![S2]:(![C2]:((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|((~iext(uri_owl_unionOf,Z,S1)|(((ic(Z)&ic(C1))&ic(C2))&((![X]:(~icext(Z,X)|(icext(C1,X)|icext(C2,X))))&(![X]:((~icext(C1,X)&~icext(C2,X))|icext(Z,X))))))&((((~ic(Z)|~ic(C1))|~ic(C2))|(?[X]:((~icext(Z,X)|(~icext(C1,X)&~icext(C2,X)))&(icext(Z,X)|(icext(C1,X)|icext(C2,X))))))|iext(uri_owl_unionOf,Z,S1))))))))),inference(shift_quantors,[status(thm)],[c14])).
% 0.48/0.63 fof(c16,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((~iext(uri_owl_unionOf,X6,X7)|(((ic(X6)&ic(X8))&ic(X10))&((![X11]:(~icext(X6,X11)|(icext(X8,X11)|icext(X10,X11))))&(![X12]:((~icext(X8,X12)&~icext(X10,X12))|icext(X6,X12))))))&((((~ic(X6)|~ic(X8))|~ic(X10))|(?[X13]:((~icext(X6,X13)|(~icext(X8,X13)&~icext(X10,X13)))&(icext(X6,X13)|(icext(X8,X13)|icext(X10,X13))))))|iext(uri_owl_unionOf,X6,X7))))))))),inference(variable_rename,[status(thm)],[c15])).
% 0.48/0.63 fof(c18,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((~iext(uri_owl_unionOf,X6,X7)|(((ic(X6)&ic(X8))&ic(X10))&((~icext(X6,X11)|(icext(X8,X11)|icext(X10,X11)))&((~icext(X8,X12)&~icext(X10,X12))|icext(X6,X12)))))&((((~ic(X6)|~ic(X8))|~ic(X10))|((~icext(X6,skolem0004(X6,X7,X8,X9,X10))|(~icext(X8,skolem0004(X6,X7,X8,X9,X10))&~icext(X10,skolem0004(X6,X7,X8,X9,X10))))&(icext(X6,skolem0004(X6,X7,X8,X9,X10))|(icext(X8,skolem0004(X6,X7,X8,X9,X10))|icext(X10,skolem0004(X6,X7,X8,X9,X10))))))|iext(uri_owl_unionOf,X6,X7))))))))))),inference(shift_quantors,[status(thm)],[fof(c17,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((~iext(uri_owl_unionOf,X6,X7)|(((ic(X6)&ic(X8))&ic(X10))&((![X11]:(~icext(X6,X11)|(icext(X8,X11)|icext(X10,X11))))&(![X12]:((~icext(X8,X12)&~icext(X10,X12))|icext(X6,X12))))))&((((~ic(X6)|~ic(X8))|~ic(X10))|((~icext(X6,skolem0004(X6,X7,X8,X9,X10))|(~icext(X8,skolem0004(X6,X7,X8,X9,X10))&~icext(X10,skolem0004(X6,X7,X8,X9,X10))))&(icext(X6,skolem0004(X6,X7,X8,X9,X10))|(icext(X8,skolem0004(X6,X7,X8,X9,X10))|icext(X10,skolem0004(X6,X7,X8,X9,X10))))))|iext(uri_owl_unionOf,X6,X7))))))))),inference(skolemize,[status(esa)],[c16])).])).
% 0.48/0.63 fof(c19,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((((((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_unionOf,X6,X7)|ic(X6)))&((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_unionOf,X6,X7)|ic(X8))))&((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_unionOf,X6,X7)|ic(X10))))&(((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_unionOf,X6,X7)|(~icext(X6,X11)|(icext(X8,X11)|icext(X10,X11)))))&(((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_unionOf,X6,X7)|(~icext(X8,X12)|icext(X6,X12))))&((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_unionOf,X6,X7)|(~icext(X10,X12)|icext(X6,X12)))))))&((((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((((~ic(X6)|~ic(X8))|~ic(X10))|(~icext(X6,skolem0004(X6,X7,X8,X9,X10))|~icext(X8,skolem0004(X6,X7,X8,X9,X10))))|iext(uri_owl_unionOf,X6,X7)))&((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((((~ic(X6)|~ic(X8))|~ic(X10))|(~icext(X6,skolem0004(X6,X7,X8,X9,X10))|~icext(X10,skolem0004(X6,X7,X8,X9,X10))))|iext(uri_owl_unionOf,X6,X7))))&((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((((~ic(X6)|~ic(X8))|~ic(X10))|(icext(X6,skolem0004(X6,X7,X8,X9,X10))|(icext(X8,skolem0004(X6,X7,X8,X9,X10))|icext(X10,skolem0004(X6,X7,X8,X9,X10)))))|iext(uri_owl_unionOf,X6,X7)))))))))))),inference(distribute,[status(thm)],[c18])).
% 0.48/0.63 cnf(c23,plain,~iext(uri_rdf_first,X58,X59)|~iext(uri_rdf_rest,X58,X61)|~iext(uri_rdf_first,X61,X63)|~iext(uri_rdf_rest,X61,uri_rdf_nil)|~iext(uri_owl_unionOf,X62,X58)|~icext(X62,X60)|icext(X59,X60)|icext(X63,X60),inference(split_conjunct,[status(thm)],[c19])).
% 0.48/0.63 cnf(c57,plain,~iext(uri_rdf_first,skolem0002,X109)|~iext(uri_rdf_rest,skolem0002,X106)|~iext(uri_rdf_first,X106,X108)|~iext(uri_rdf_rest,X106,uri_rdf_nil)|~icext(skolem0001,X107)|icext(X109,X107)|icext(X108,X107),inference(resolution,[status(thm)],[c23, c5])).
% 0.48/0.63 cnf(c70,plain,~iext(uri_rdf_first,skolem0002,X111)|~iext(uri_rdf_rest,skolem0002,skolem0003)|~iext(uri_rdf_first,skolem0003,X110)|~icext(skolem0001,X112)|icext(X111,X112)|icext(X110,X112),inference(resolution,[status(thm)],[c57, c9])).
% 0.48/0.63 cnf(c71,plain,~iext(uri_rdf_first,skolem0002,X119)|~iext(uri_rdf_rest,skolem0002,skolem0003)|~icext(skolem0001,X118)|icext(X119,X118)|icext(uri_ex_Falcon,X118),inference(resolution,[status(thm)],[c70, c8])).
% 0.48/0.63 cnf(c73,plain,~iext(uri_rdf_first,skolem0002,X120)|~icext(skolem0001,X121)|icext(X120,X121)|icext(uri_ex_Falcon,X121),inference(resolution,[status(thm)],[c71, c7])).
% 0.48/0.63 cnf(c74,plain,~icext(skolem0001,X122)|icext(uri_ex_Eagle,X122)|icext(uri_ex_Falcon,X122),inference(resolution,[status(thm)],[c73, c6])).
% 0.48/0.63 cnf(c75,plain,icext(uri_ex_Eagle,uri_ex_harry)|icext(uri_ex_Falcon,uri_ex_harry),inference(resolution,[status(thm)],[c74, c36])).
% 0.48/0.63 cnf(c77,plain,icext(uri_ex_Falcon,uri_ex_harry)|iext(uri_rdf_type,uri_ex_harry,uri_ex_Eagle),inference(resolution,[status(thm)],[c75, c34])).
% 0.48/0.63 cnf(c85,plain,icext(uri_ex_Falcon,uri_ex_harry),inference(resolution,[status(thm)],[c77, c38])).
% 0.48/0.63 cnf(c86,plain,iext(uri_rdf_type,uri_ex_harry,uri_ex_Falcon),inference(resolution,[status(thm)],[c85, c34])).
% 0.48/0.63 cnf(c88,plain,$false,inference(resolution,[status(thm)],[c86, c39])).
% 0.48/0.63 % SZS output end CNFRefutation
% 0.48/0.63
% 0.48/0.63 % Initial clauses : 20
% 0.48/0.63 % Processed clauses : 60
% 0.48/0.63 % Factors computed : 3
% 0.48/0.63 % Resolvents computed: 52
% 0.48/0.63 % Tautologies deleted: 0
% 0.48/0.63 % Forward subsumed : 6
% 0.48/0.63 % Backward subsumed : 17
% 0.48/0.63 % -------- CPU Time ---------
% 0.48/0.63 % User time : 0.260 s
% 0.48/0.63 % System time : 0.021 s
% 0.48/0.63 % Total time : 0.281 s
%------------------------------------------------------------------------------