%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB017+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:50 EDT 2024
% Result : Theorem 0.57s 0.73s
% Output : Refutation 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : SWB017+2 : TPTP v8.1.2. Released v5.2.0.
% 0.10/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.32 % Computer : n032.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Wed May 8 22:12:37 EDT 2024
% 0.12/0.32 % CPUTime :
% 0.57/0.73 % Version: 1.5
% 0.57/0.73 % SZS status Theorem
% 0.57/0.73 % SZS output start CNFRefutation
% 0.57/0.73 fof(testcase_premise_fullish_017_Built_in_Based_Definitions,axiom,((iext(uri_owl_propertyDisjointWith,uri_ex_notInstanceOf,uri_rdf_type)&iext(uri_rdf_type,uri_ex_w,uri_ex_c))&iext(uri_ex_notInstanceOf,uri_ex_u,uri_ex_c)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_017_Built_in_Based_Definitions)).
% 0.57/0.73 cnf(c2,plain,iext(uri_owl_propertyDisjointWith,uri_ex_notInstanceOf,uri_rdf_type),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_017_Built_in_Based_Definitions])).
% 0.57/0.73 cnf(c3,plain,iext(uri_rdf_type,uri_ex_w,uri_ex_c),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_017_Built_in_Based_Definitions])).
% 0.57/0.73 fof(owl_eqdis_propertydisjointwith,axiom,(![P1]:(![P2]:(iext(uri_owl_propertyDisjointWith,P1,P2)<=>((ip(P1)&ip(P2))&(![X]:(![Y]:(~(iext(P1,X,Y)&iext(P2,X,Y))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_eqdis_propertydisjointwith)).
% 0.57/0.73 fof(c8,plain,(![P1]:(![P2]:((~iext(uri_owl_propertyDisjointWith,P1,P2)|((ip(P1)&ip(P2))&(![X]:(![Y]:(~iext(P1,X,Y)|~iext(P2,X,Y))))))&(((~ip(P1)|~ip(P2))|(?[X]:(?[Y]:(iext(P1,X,Y)&iext(P2,X,Y)))))|iext(uri_owl_propertyDisjointWith,P1,P2))))),inference(fof_nnf,[status(thm)],[owl_eqdis_propertydisjointwith])).
% 0.57/0.73 fof(c9,plain,((![P1]:(![P2]:(~iext(uri_owl_propertyDisjointWith,P1,P2)|((ip(P1)&ip(P2))&(![X]:(![Y]:(~iext(P1,X,Y)|~iext(P2,X,Y))))))))&(![P1]:(![P2]:(((~ip(P1)|~ip(P2))|(?[X]:(?[Y]:(iext(P1,X,Y)&iext(P2,X,Y)))))|iext(uri_owl_propertyDisjointWith,P1,P2))))),inference(shift_quantors,[status(thm)],[c8])).
% 0.57/0.73 fof(c10,plain,((![X2]:(![X3]:(~iext(uri_owl_propertyDisjointWith,X2,X3)|((ip(X2)&ip(X3))&(![X4]:(![X5]:(~iext(X2,X4,X5)|~iext(X3,X4,X5))))))))&(![X6]:(![X7]:(((~ip(X6)|~ip(X7))|(?[X8]:(?[X9]:(iext(X6,X8,X9)&iext(X7,X8,X9)))))|iext(uri_owl_propertyDisjointWith,X6,X7))))),inference(variable_rename,[status(thm)],[c9])).
% 0.57/0.73 fof(c12,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((~iext(uri_owl_propertyDisjointWith,X2,X3)|((ip(X2)&ip(X3))&(~iext(X2,X4,X5)|~iext(X3,X4,X5))))&(((~ip(X6)|~ip(X7))|(iext(X6,skolem0001(X6,X7),skolem0002(X6,X7))&iext(X7,skolem0001(X6,X7),skolem0002(X6,X7))))|iext(uri_owl_propertyDisjointWith,X6,X7))))))))),inference(shift_quantors,[status(thm)],[fof(c11,plain,((![X2]:(![X3]:(~iext(uri_owl_propertyDisjointWith,X2,X3)|((ip(X2)&ip(X3))&(![X4]:(![X5]:(~iext(X2,X4,X5)|~iext(X3,X4,X5))))))))&(![X6]:(![X7]:(((~ip(X6)|~ip(X7))|(iext(X6,skolem0001(X6,X7),skolem0002(X6,X7))&iext(X7,skolem0001(X6,X7),skolem0002(X6,X7))))|iext(uri_owl_propertyDisjointWith,X6,X7))))),inference(skolemize,[status(esa)],[c10])).])).
% 0.57/0.73 fof(c13,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((((~iext(uri_owl_propertyDisjointWith,X2,X3)|ip(X2))&(~iext(uri_owl_propertyDisjointWith,X2,X3)|ip(X3)))&(~iext(uri_owl_propertyDisjointWith,X2,X3)|(~iext(X2,X4,X5)|~iext(X3,X4,X5))))&((((~ip(X6)|~ip(X7))|iext(X6,skolem0001(X6,X7),skolem0002(X6,X7)))|iext(uri_owl_propertyDisjointWith,X6,X7))&(((~ip(X6)|~ip(X7))|iext(X7,skolem0001(X6,X7),skolem0002(X6,X7)))|iext(uri_owl_propertyDisjointWith,X6,X7)))))))))),inference(distribute,[status(thm)],[c12])).
% 0.57/0.73 cnf(c16,plain,~iext(uri_owl_propertyDisjointWith,X37,X38)|~iext(X37,X39,X40)|~iext(X38,X39,X40),inference(split_conjunct,[status(thm)],[c13])).
% 0.57/0.73 cnf(c36,plain,~iext(uri_owl_propertyDisjointWith,X81,uri_rdf_type)|~iext(X81,uri_ex_w,uri_ex_c),inference(resolution,[status(thm)],[c16, c3])).
% 0.57/0.73 cnf(reflexivity,axiom,X14=X14,theory(equality)).
% 0.57/0.73 cnf(symmetry,axiom,X16!=X15|X15=X16,theory(equality)).
% 0.57/0.73 fof(testcase_conclusion_fullish_017_Built_in_Based_Definitions,conjecture,iext(uri_owl_differentFrom,uri_ex_w,uri_ex_u),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_017_Built_in_Based_Definitions)).
% 0.57/0.73 fof(c5,negated_conjecture,(~iext(uri_owl_differentFrom,uri_ex_w,uri_ex_u)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_017_Built_in_Based_Definitions])).
% 0.57/0.73 fof(c6,negated_conjecture,~iext(uri_owl_differentFrom,uri_ex_w,uri_ex_u),inference(fof_simplification,[status(thm)],[c5])).
% 0.57/0.73 cnf(c7,negated_conjecture,~iext(uri_owl_differentFrom,uri_ex_w,uri_ex_u),inference(split_conjunct,[status(thm)],[c6])).
% 0.57/0.73 fof(owl_eqdis_differentfrom,axiom,(![X]:(![Y]:(iext(uri_owl_differentFrom,X,Y)<=>X!=Y))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_eqdis_differentfrom)).
% 0.57/0.73 fof(c19,plain,(![X]:(![Y]:((~iext(uri_owl_differentFrom,X,Y)|X!=Y)&(X=Y|iext(uri_owl_differentFrom,X,Y))))),inference(fof_nnf,[status(thm)],[owl_eqdis_differentfrom])).
% 0.57/0.73 fof(c20,plain,((![X]:(![Y]:(~iext(uri_owl_differentFrom,X,Y)|X!=Y)))&(![X]:(![Y]:(X=Y|iext(uri_owl_differentFrom,X,Y))))),inference(shift_quantors,[status(thm)],[c19])).
% 0.57/0.73 fof(c22,plain,(![X10]:(![X11]:(![X12]:(![X13]:((~iext(uri_owl_differentFrom,X10,X11)|X10!=X11)&(X12=X13|iext(uri_owl_differentFrom,X12,X13))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,((![X10]:(![X11]:(~iext(uri_owl_differentFrom,X10,X11)|X10!=X11)))&(![X12]:(![X13]:(X12=X13|iext(uri_owl_differentFrom,X12,X13))))),inference(variable_rename,[status(thm)],[c20])).])).
% 0.57/0.73 cnf(c24,plain,X44=X43|iext(uri_owl_differentFrom,X44,X43),inference(split_conjunct,[status(thm)],[c22])).
% 0.57/0.73 cnf(c42,plain,uri_ex_w=uri_ex_u,inference(resolution,[status(thm)],[c24, c7])).
% 0.57/0.73 cnf(c47,plain,uri_ex_u=uri_ex_w,inference(resolution,[status(thm)],[c42, symmetry])).
% 0.57/0.73 cnf(c4,plain,iext(uri_ex_notInstanceOf,uri_ex_u,uri_ex_c),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_017_Built_in_Based_Definitions])).
% 0.57/0.73 cnf(c0,axiom,X31!=X27|X29!=X30|X28!=X26|~iext(X31,X29,X28)|iext(X27,X30,X26),theory(equality)).
% 0.57/0.73 cnf(c30,plain,uri_ex_notInstanceOf!=X65|uri_ex_u!=X67|uri_ex_c!=X66|iext(X65,X67,X66),inference(resolution,[status(thm)],[c0, c4])).
% 0.57/0.73 cnf(c83,plain,uri_ex_notInstanceOf!=X174|uri_ex_u!=X175|iext(X174,X175,uri_ex_c),inference(resolution,[status(thm)],[c30, reflexivity])).
% 0.57/0.73 cnf(c644,plain,uri_ex_notInstanceOf!=X246|iext(X246,uri_ex_w,uri_ex_c),inference(resolution,[status(thm)],[c83, c47])).
% 0.57/0.73 cnf(c928,plain,iext(uri_ex_notInstanceOf,uri_ex_w,uri_ex_c),inference(resolution,[status(thm)],[c644, reflexivity])).
% 0.57/0.73 cnf(c933,plain,~iext(uri_owl_propertyDisjointWith,uri_ex_notInstanceOf,uri_rdf_type),inference(resolution,[status(thm)],[c928, c36])).
% 0.57/0.73 cnf(c954,plain,$false,inference(resolution,[status(thm)],[c933, c2])).
% 0.57/0.73 % SZS output end CNFRefutation
% 0.57/0.73
% 0.57/0.73 % Initial clauses : 16
% 0.57/0.73 % Processed clauses : 119
% 0.57/0.73 % Factors computed : 20
% 0.57/0.73 % Resolvents computed: 910
% 0.57/0.73 % Tautologies deleted: 4
% 0.57/0.73 % Forward subsumed : 160
% 0.57/0.73 % Backward subsumed : 0
% 0.57/0.73 % -------- CPU Time ---------
% 0.57/0.73 % User time : 0.396 s
% 0.57/0.73 % System time : 0.014 s
% 0.57/0.73 % Total time : 0.410 s
%------------------------------------------------------------------------------