%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB011+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:42:47 EDT 2024
% Result : Unsatisfiable 114.78s 114.96s
% Output : Refutation 114.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWB011+1 : TPTP v8.1.2. Released v5.2.0.
% 0.07/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:13:38 EDT 2024
% 0.15/0.35 % CPUTime :
% 114.78/114.96 % Version: 1.5
% 114.78/114.96 % SZS status Unsatisfiable
% 114.78/114.96 % SZS output start CNFRefutation
% 114.78/114.96 fof(owl_class_classowl_ext,axiom,(![X]:(icext(uri_owl_Class,X)<=>ic(X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', owl_class_classowl_ext)).
% 114.78/114.96 fof(c2256,plain,(![X]:((~icext(uri_owl_Class,X)|ic(X))&(~ic(X)|icext(uri_owl_Class,X)))),inference(fof_nnf,[status(thm)],[owl_class_classowl_ext])).
% 114.78/114.96 fof(c2257,plain,((![X]:(~icext(uri_owl_Class,X)|ic(X)))&(![X]:(~ic(X)|icext(uri_owl_Class,X)))),inference(shift_quantors,[status(thm)],[c2256])).
% 114.78/114.96 fof(c2259,plain,(![X1171]:(![X1172]:((~icext(uri_owl_Class,X1171)|ic(X1171))&(~ic(X1172)|icext(uri_owl_Class,X1172))))),inference(shift_quantors,[status(thm)],[fof(c2258,plain,((![X1171]:(~icext(uri_owl_Class,X1171)|ic(X1171)))&(![X1172]:(~ic(X1172)|icext(uri_owl_Class,X1172)))),inference(variable_rename,[status(thm)],[c2257])).])).
% 114.78/114.96 cnf(c2261,plain,~ic(X1770)|icext(uri_owl_Class,X1770),inference(split_conjunct,[status(thm)],[c2259])).
% 114.78/114.96 fof(rdfs_collection_first_domain,axiom,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', rdfs_collection_first_domain)).
% 114.78/114.96 cnf(c2504,plain,iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain])).
% 114.78/114.96 fof(owl_rdfsext_domain,axiom,(![P]:(![C]:(iext(uri_rdfs_domain,P,C)<=>((ip(P)&ic(C))&(![X]:(![Y]:(iext(P,X,Y)=>icext(C,X)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', owl_rdfsext_domain)).
% 114.78/114.96 fof(c1023,plain,(![P]:(![C]:((~iext(uri_rdfs_domain,P,C)|((ip(P)&ic(C))&(![X]:(![Y]:(~iext(P,X,Y)|icext(C,X))))))&(((~ip(P)|~ic(C))|(?[X]:(?[Y]:(iext(P,X,Y)&~icext(C,X)))))|iext(uri_rdfs_domain,P,C))))),inference(fof_nnf,[status(thm)],[owl_rdfsext_domain])).
% 114.78/114.96 fof(c1024,plain,((![P]:(![C]:(~iext(uri_rdfs_domain,P,C)|((ip(P)&ic(C))&(![X]:((![Y]:~iext(P,X,Y))|icext(C,X)))))))&(![P]:(![C]:(((~ip(P)|~ic(C))|(?[X]:((?[Y]:iext(P,X,Y))&~icext(C,X))))|iext(uri_rdfs_domain,P,C))))),inference(shift_quantors,[status(thm)],[c1023])).
% 114.78/114.96 fof(c1025,plain,((![X498]:(![X499]:(~iext(uri_rdfs_domain,X498,X499)|((ip(X498)&ic(X499))&(![X500]:((![X501]:~iext(X498,X500,X501))|icext(X499,X500)))))))&(![X502]:(![X503]:(((~ip(X502)|~ic(X503))|(?[X504]:((?[X505]:iext(X502,X504,X505))&~icext(X503,X504))))|iext(uri_rdfs_domain,X502,X503))))),inference(variable_rename,[status(thm)],[c1024])).
% 114.78/114.96 fof(c1027,plain,(![X498]:(![X499]:(![X500]:(![X501]:(![X502]:(![X503]:((~iext(uri_rdfs_domain,X498,X499)|((ip(X498)&ic(X499))&(~iext(X498,X500,X501)|icext(X499,X500))))&(((~ip(X502)|~ic(X503))|(iext(X502,skolem0087(X502,X503),skolem0088(X502,X503))&~icext(X503,skolem0087(X502,X503))))|iext(uri_rdfs_domain,X502,X503))))))))),inference(shift_quantors,[status(thm)],[fof(c1026,plain,((![X498]:(![X499]:(~iext(uri_rdfs_domain,X498,X499)|((ip(X498)&ic(X499))&(![X500]:((![X501]:~iext(X498,X500,X501))|icext(X499,X500)))))))&(![X502]:(![X503]:(((~ip(X502)|~ic(X503))|(iext(X502,skolem0087(X502,X503),skolem0088(X502,X503))&~icext(X503,skolem0087(X502,X503))))|iext(uri_rdfs_domain,X502,X503))))),inference(skolemize,[status(esa)],[c1025])).])).
% 114.78/114.96 fof(c1028,plain,(![X498]:(![X499]:(![X500]:(![X501]:(![X502]:(![X503]:((((~iext(uri_rdfs_domain,X498,X499)|ip(X498))&(~iext(uri_rdfs_domain,X498,X499)|ic(X499)))&(~iext(uri_rdfs_domain,X498,X499)|(~iext(X498,X500,X501)|icext(X499,X500))))&((((~ip(X502)|~ic(X503))|iext(X502,skolem0087(X502,X503),skolem0088(X502,X503)))|iext(uri_rdfs_domain,X502,X503))&(((~ip(X502)|~ic(X503))|~icext(X503,skolem0087(X502,X503)))|iext(uri_rdfs_domain,X502,X503)))))))))),inference(distribute,[status(thm)],[c1027])).
% 114.78/114.96 cnf(c1030,plain,~iext(uri_rdfs_domain,X2326,X2325)|ic(X2325),inference(split_conjunct,[status(thm)],[c1028])).
% 114.78/114.96 cnf(c6558,plain,ic(uri_rdf_List),inference(resolution,[status(thm)],[c1030, c2504])).
% 114.78/114.96 cnf(c6576,plain,icext(uri_owl_Class,uri_rdf_List),inference(resolution,[status(thm)],[c6558, c2261])).
% 114.78/114.96 fof(owl_class_objectproperty_ext,axiom,(![X]:(icext(uri_owl_ObjectProperty,X)<=>ip(X))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', owl_class_objectproperty_ext)).
% 114.78/114.96 fof(c2182,plain,(![X]:((~icext(uri_owl_ObjectProperty,X)|ip(X))&(~ip(X)|icext(uri_owl_ObjectProperty,X)))),inference(fof_nnf,[status(thm)],[owl_class_objectproperty_ext])).
% 114.78/114.96 fof(c2183,plain,((![X]:(~icext(uri_owl_ObjectProperty,X)|ip(X)))&(![X]:(~ip(X)|icext(uri_owl_ObjectProperty,X)))),inference(shift_quantors,[status(thm)],[c2182])).
% 114.78/114.96 fof(c2185,plain,(![X1151]:(![X1152]:((~icext(uri_owl_ObjectProperty,X1151)|ip(X1151))&(~ip(X1152)|icext(uri_owl_ObjectProperty,X1152))))),inference(shift_quantors,[status(thm)],[fof(c2184,plain,((![X1151]:(~icext(uri_owl_ObjectProperty,X1151)|ip(X1151)))&(![X1152]:(~ip(X1152)|icext(uri_owl_ObjectProperty,X1152)))),inference(variable_rename,[status(thm)],[c2183])).])).
% 114.78/114.96 cnf(c2187,plain,~ip(X1471)|icext(uri_owl_ObjectProperty,X1471),inference(split_conjunct,[status(thm)],[c2185])).
% 114.78/114.96 fof(rdfs_collection_rest_range,axiom,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', rdfs_collection_rest_range)).
% 114.78/114.96 cnf(c2501,plain,iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range])).
% 114.78/114.96 fof(owl_rdfsext_range,axiom,(![P]:(![C]:(iext(uri_rdfs_range,P,C)<=>((ip(P)&ip(C))&(![X]:(![Y]:(iext(P,X,Y)=>icext(C,Y)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', owl_rdfsext_range)).
% 114.78/114.96 fof(c1012,plain,(![P]:(![C]:((~iext(uri_rdfs_range,P,C)|((ip(P)&ip(C))&(![X]:(![Y]:(~iext(P,X,Y)|icext(C,Y))))))&(((~ip(P)|~ip(C))|(?[X]:(?[Y]:(iext(P,X,Y)&~icext(C,Y)))))|iext(uri_rdfs_range,P,C))))),inference(fof_nnf,[status(thm)],[owl_rdfsext_range])).
% 114.78/114.96 fof(c1013,plain,((![P]:(![C]:(~iext(uri_rdfs_range,P,C)|((ip(P)&ip(C))&(![X]:(![Y]:(~iext(P,X,Y)|icext(C,Y))))))))&(![P]:(![C]:(((~ip(P)|~ip(C))|(?[X]:(?[Y]:(iext(P,X,Y)&~icext(C,Y)))))|iext(uri_rdfs_range,P,C))))),inference(shift_quantors,[status(thm)],[c1012])).
% 114.78/114.96 fof(c1014,plain,((![X490]:(![X491]:(~iext(uri_rdfs_range,X490,X491)|((ip(X490)&ip(X491))&(![X492]:(![X493]:(~iext(X490,X492,X493)|icext(X491,X493))))))))&(![X494]:(![X495]:(((~ip(X494)|~ip(X495))|(?[X496]:(?[X497]:(iext(X494,X496,X497)&~icext(X495,X497)))))|iext(uri_rdfs_range,X494,X495))))),inference(variable_rename,[status(thm)],[c1013])).
% 114.78/114.96 fof(c1016,plain,(![X490]:(![X491]:(![X492]:(![X493]:(![X494]:(![X495]:((~iext(uri_rdfs_range,X490,X491)|((ip(X490)&ip(X491))&(~iext(X490,X492,X493)|icext(X491,X493))))&(((~ip(X494)|~ip(X495))|(iext(X494,skolem0085(X494,X495),skolem0086(X494,X495))&~icext(X495,skolem0086(X494,X495))))|iext(uri_rdfs_range,X494,X495))))))))),inference(shift_quantors,[status(thm)],[fof(c1015,plain,((![X490]:(![X491]:(~iext(uri_rdfs_range,X490,X491)|((ip(X490)&ip(X491))&(![X492]:(![X493]:(~iext(X490,X492,X493)|icext(X491,X493))))))))&(![X494]:(![X495]:(((~ip(X494)|~ip(X495))|(iext(X494,skolem0085(X494,X495),skolem0086(X494,X495))&~icext(X495,skolem0086(X494,X495))))|iext(uri_rdfs_range,X494,X495))))),inference(skolemize,[status(esa)],[c1014])).])).
% 114.78/114.96 fof(c1017,plain,(![X490]:(![X491]:(![X492]:(![X493]:(![X494]:(![X495]:((((~iext(uri_rdfs_range,X490,X491)|ip(X490))&(~iext(uri_rdfs_range,X490,X491)|ip(X491)))&(~iext(uri_rdfs_range,X490,X491)|(~iext(X490,X492,X493)|icext(X491,X493))))&((((~ip(X494)|~ip(X495))|iext(X494,skolem0085(X494,X495),skolem0086(X494,X495)))|iext(uri_rdfs_range,X494,X495))&(((~ip(X494)|~ip(X495))|~icext(X495,skolem0086(X494,X495)))|iext(uri_rdfs_range,X494,X495)))))))))),inference(distribute,[status(thm)],[c1016])).
% 114.78/114.96 cnf(c1019,plain,~iext(uri_rdfs_range,X2255,X2256)|ip(X2256),inference(split_conjunct,[status(thm)],[c1017])).
% 114.78/114.96 cnf(c6401,plain,ip(uri_rdf_List),inference(resolution,[status(thm)],[c1019, c2501])).
% 114.78/114.96 cnf(c6454,plain,icext(uri_owl_ObjectProperty,uri_rdf_List),inference(resolution,[status(thm)],[c6401, c2187])).
% 114.78/114.96 fof(testcase_premise_fullish_011_Entity_Types_as_Classes,axiom,((iext(uri_owl_disjointWith,uri_owl_Class,uri_owl_ObjectProperty)&iext(uri_rdf_type,uri_ex_x,uri_owl_Class))&iext(uri_rdf_type,uri_ex_x,uri_owl_ObjectProperty)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_011_Entity_Types_as_Classes)).
% 114.78/114.96 cnf(c12,plain,iext(uri_owl_disjointWith,uri_owl_Class,uri_owl_ObjectProperty),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_011_Entity_Types_as_Classes])).
% 114.78/114.96 fof(owl_eqdis_disjointwith,axiom,(![C1]:(![C2]:(iext(uri_owl_disjointWith,C1,C2)<=>((ic(C1)&ic(C2))&(![X]:(~(icext(C1,X)&icext(C2,X)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', owl_eqdis_disjointwith)).
% 114.78/114.96 fof(c864,plain,(![C1]:(![C2]:((~iext(uri_owl_disjointWith,C1,C2)|((ic(C1)&ic(C2))&(![X]:(~icext(C1,X)|~icext(C2,X)))))&(((~ic(C1)|~ic(C2))|(?[X]:(icext(C1,X)&icext(C2,X))))|iext(uri_owl_disjointWith,C1,C2))))),inference(fof_nnf,[status(thm)],[owl_eqdis_disjointwith])).
% 114.78/114.96 fof(c865,plain,((![C1]:(![C2]:(~iext(uri_owl_disjointWith,C1,C2)|((ic(C1)&ic(C2))&(![X]:(~icext(C1,X)|~icext(C2,X)))))))&(![C1]:(![C2]:(((~ic(C1)|~ic(C2))|(?[X]:(icext(C1,X)&icext(C2,X))))|iext(uri_owl_disjointWith,C1,C2))))),inference(shift_quantors,[status(thm)],[c864])).
% 114.78/114.96 fof(c866,plain,((![X438]:(![X439]:(~iext(uri_owl_disjointWith,X438,X439)|((ic(X438)&ic(X439))&(![X440]:(~icext(X438,X440)|~icext(X439,X440)))))))&(![X441]:(![X442]:(((~ic(X441)|~ic(X442))|(?[X443]:(icext(X441,X443)&icext(X442,X443))))|iext(uri_owl_disjointWith,X441,X442))))),inference(variable_rename,[status(thm)],[c865])).
% 114.78/114.96 fof(c868,plain,(![X438]:(![X439]:(![X440]:(![X441]:(![X442]:((~iext(uri_owl_disjointWith,X438,X439)|((ic(X438)&ic(X439))&(~icext(X438,X440)|~icext(X439,X440))))&(((~ic(X441)|~ic(X442))|(icext(X441,skolem0077(X441,X442))&icext(X442,skolem0077(X441,X442))))|iext(uri_owl_disjointWith,X441,X442)))))))),inference(shift_quantors,[status(thm)],[fof(c867,plain,((![X438]:(![X439]:(~iext(uri_owl_disjointWith,X438,X439)|((ic(X438)&ic(X439))&(![X440]:(~icext(X438,X440)|~icext(X439,X440)))))))&(![X441]:(![X442]:(((~ic(X441)|~ic(X442))|(icext(X441,skolem0077(X441,X442))&icext(X442,skolem0077(X441,X442))))|iext(uri_owl_disjointWith,X441,X442))))),inference(skolemize,[status(esa)],[c866])).])).
% 114.78/114.96 fof(c869,plain,(![X438]:(![X439]:(![X440]:(![X441]:(![X442]:((((~iext(uri_owl_disjointWith,X438,X439)|ic(X438))&(~iext(uri_owl_disjointWith,X438,X439)|ic(X439)))&(~iext(uri_owl_disjointWith,X438,X439)|(~icext(X438,X440)|~icext(X439,X440))))&((((~ic(X441)|~ic(X442))|icext(X441,skolem0077(X441,X442)))|iext(uri_owl_disjointWith,X441,X442))&(((~ic(X441)|~ic(X442))|icext(X442,skolem0077(X441,X442)))|iext(uri_owl_disjointWith,X441,X442))))))))),inference(distribute,[status(thm)],[c868])).
% 114.78/114.96 cnf(c872,plain,~iext(uri_owl_disjointWith,X2548,X2546)|~icext(X2548,X2547)|~icext(X2546,X2547),inference(split_conjunct,[status(thm)],[c869])).
% 114.78/114.96 cnf(c7266,plain,~icext(uri_owl_Class,X6199)|~icext(uri_owl_ObjectProperty,X6199),inference(resolution,[status(thm)],[c872, c12])).
% 114.78/114.96 cnf(c49539,plain,~icext(uri_owl_Class,uri_rdf_List),inference(resolution,[status(thm)],[c7266, c6454])).
% 114.78/114.96 cnf(c49711,plain,$false,inference(resolution,[status(thm)],[c49539, c6576])).
% 114.78/114.96 % SZS output end CNFRefutation
% 114.78/114.96
% 114.78/114.96 % Initial clauses : 1281
% 114.78/114.96 % Processed clauses : 3714
% 114.78/114.96 % Factors computed : 650
% 114.78/114.96 % Resolvents computed: 46512
% 114.78/114.96 % Tautologies deleted: 60
% 114.78/114.96 % Forward subsumed : 4846
% 114.78/114.96 % Backward subsumed : 31
% 114.78/114.96 % -------- CPU Time ---------
% 114.78/114.96 % User time : 114.460 s
% 114.78/114.96 % System time : 0.129 s
% 114.78/114.96 % Total time : 114.589 s
%------------------------------------------------------------------------------