%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB074+1 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:43:00 EDT 2024
% Result : Theorem 107.30s 107.54s
% Output : Refutation 107.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : SWB074+1 : TPTP v8.1.2. Released v5.2.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n015.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:06:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 107.30/107.54 % Version: 1.5
% 107.30/107.54 % SZS status Theorem
% 107.30/107.54 % SZS output start CNFRefutation
% 107.30/107.54 fof(conclusion_rdfbased_sem_prop_topdataproperty_ext_lo,conjecture,iext(uri_owl_topDataProperty,uri_ex_x,uri_ex_y),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conclusion_rdfbased_sem_prop_topdataproperty_ext_lo)).
% 107.30/107.54 fof(c14,negated_conjecture,(~iext(uri_owl_topDataProperty,uri_ex_x,uri_ex_y)),inference(assume_negation,[status(cth)],[conclusion_rdfbased_sem_prop_topdataproperty_ext_lo])).
% 107.30/107.54 fof(c15,negated_conjecture,~iext(uri_owl_topDataProperty,uri_ex_x,uri_ex_y),inference(fof_simplification,[status(thm)],[c14])).
% 107.30/107.54 cnf(c16,negated_conjecture,~iext(uri_owl_topDataProperty,uri_ex_x,uri_ex_y),inference(split_conjunct,[status(thm)],[c15])).
% 107.30/107.54 fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', simple_ir)).
% 107.30/107.54 fof(c2545,plain,(![X1263]:ir(X1263)),inference(variable_rename,[status(thm)],[simple_ir])).
% 107.30/107.54 cnf(c2546,plain,ir(X1267),inference(split_conjunct,[status(thm)],[c2545])).
% 107.30/107.54 fof(premise_rdfbased_sem_prop_topdataproperty_ext_lo,axiom,(iext(uri_rdf_type,uri_ex_y,uri_rdfs_Literal)&iext(uri_rdf_type,uri_ex_x,uri_owl_Thing)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', premise_rdfbased_sem_prop_topdataproperty_ext_lo)).
% 107.30/107.54 cnf(c12,plain,iext(uri_rdf_type,uri_ex_y,uri_rdfs_Literal),inference(split_conjunct,[status(thm)],[premise_rdfbased_sem_prop_topdataproperty_ext_lo])).
% 107.30/107.54 fof(owl_parts_lv_def,axiom,(![X]:(lv(X)<=>iext(uri_rdf_type,X,uri_rdfs_Literal))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', owl_parts_lv_def)).
% 107.30/107.54 fof(c2295,plain,(![X]:((~lv(X)|iext(uri_rdf_type,X,uri_rdfs_Literal))&(~iext(uri_rdf_type,X,uri_rdfs_Literal)|lv(X)))),inference(fof_nnf,[status(thm)],[owl_parts_lv_def])).
% 107.30/107.54 fof(c2296,plain,((![X]:(~lv(X)|iext(uri_rdf_type,X,uri_rdfs_Literal)))&(![X]:(~iext(uri_rdf_type,X,uri_rdfs_Literal)|lv(X)))),inference(shift_quantors,[status(thm)],[c2295])).
% 107.30/107.54 fof(c2298,plain,(![X1181]:(![X1182]:((~lv(X1181)|iext(uri_rdf_type,X1181,uri_rdfs_Literal))&(~iext(uri_rdf_type,X1182,uri_rdfs_Literal)|lv(X1182))))),inference(shift_quantors,[status(thm)],[fof(c2297,plain,((![X1181]:(~lv(X1181)|iext(uri_rdf_type,X1181,uri_rdfs_Literal)))&(![X1182]:(~iext(uri_rdf_type,X1182,uri_rdfs_Literal)|lv(X1182)))),inference(variable_rename,[status(thm)],[c2296])).])).
% 107.30/107.54 cnf(c2300,plain,~iext(uri_rdf_type,X3382,uri_rdfs_Literal)|lv(X3382),inference(split_conjunct,[status(thm)],[c2298])).
% 107.30/107.54 cnf(c13058,plain,lv(uri_ex_y),inference(resolution,[status(thm)],[c2300, c12])).
% 107.30/107.54 fof(owl_prop_topdataproperty_ext,axiom,(![X]:(![Y]:(iext(uri_owl_topDataProperty,X,Y)<=>(ir(X)&lv(Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', owl_prop_topdataproperty_ext)).
% 107.30/107.54 fof(c1837,plain,(![X]:(![Y]:((~iext(uri_owl_topDataProperty,X,Y)|(ir(X)&lv(Y)))&((~ir(X)|~lv(Y))|iext(uri_owl_topDataProperty,X,Y))))),inference(fof_nnf,[status(thm)],[owl_prop_topdataproperty_ext])).
% 107.30/107.54 fof(c1838,plain,((![X]:(![Y]:(~iext(uri_owl_topDataProperty,X,Y)|(ir(X)&lv(Y)))))&(![X]:(![Y]:((~ir(X)|~lv(Y))|iext(uri_owl_topDataProperty,X,Y))))),inference(shift_quantors,[status(thm)],[c1837])).
% 107.30/107.54 fof(c1840,plain,(![X1037]:(![X1038]:(![X1039]:(![X1040]:((~iext(uri_owl_topDataProperty,X1037,X1038)|(ir(X1037)&lv(X1038)))&((~ir(X1039)|~lv(X1040))|iext(uri_owl_topDataProperty,X1039,X1040))))))),inference(shift_quantors,[status(thm)],[fof(c1839,plain,((![X1037]:(![X1038]:(~iext(uri_owl_topDataProperty,X1037,X1038)|(ir(X1037)&lv(X1038)))))&(![X1039]:(![X1040]:((~ir(X1039)|~lv(X1040))|iext(uri_owl_topDataProperty,X1039,X1040))))),inference(variable_rename,[status(thm)],[c1838])).])).
% 107.30/107.54 fof(c1841,plain,(![X1037]:(![X1038]:(![X1039]:(![X1040]:(((~iext(uri_owl_topDataProperty,X1037,X1038)|ir(X1037))&(~iext(uri_owl_topDataProperty,X1037,X1038)|lv(X1038)))&((~ir(X1039)|~lv(X1040))|iext(uri_owl_topDataProperty,X1039,X1040))))))),inference(distribute,[status(thm)],[c1840])).
% 107.30/107.54 cnf(c1844,plain,~ir(X5110)|~lv(X5109)|iext(uri_owl_topDataProperty,X5110,X5109),inference(split_conjunct,[status(thm)],[c1841])).
% 107.30/107.54 cnf(c25579,plain,~ir(X6343)|iext(uri_owl_topDataProperty,X6343,uri_ex_y),inference(resolution,[status(thm)],[c1844, c13058])).
% 107.30/107.54 cnf(c50005,plain,iext(uri_owl_topDataProperty,X6344,uri_ex_y),inference(resolution,[status(thm)],[c25579, c2546])).
% 107.30/107.54 cnf(c50009,plain,$false,inference(resolution,[status(thm)],[c50005, c16])).
% 107.30/107.54 % SZS output end CNFRefutation
% 107.30/107.54
% 107.30/107.54 % Initial clauses : 1281
% 107.30/107.54 % Processed clauses : 3714
% 107.30/107.54 % Factors computed : 644
% 107.30/107.54 % Resolvents computed: 46851
% 107.30/107.54 % Tautologies deleted: 131
% 107.30/107.54 % Forward subsumed : 4919
% 107.30/107.54 % Backward subsumed : 33
% 107.30/107.54 % -------- CPU Time ---------
% 107.30/107.54 % User time : 106.996 s
% 107.30/107.54 % System time : 0.129 s
% 107.30/107.54 % Total time : 107.125 s
%------------------------------------------------------------------------------