%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB018+1 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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 185.52s 185.71s
% Output : Refutation 185.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SWB018+1 : TPTP v8.1.2. Released v5.2.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n013.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 22:10:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 185.52/185.71 % Version: 1.5
% 185.52/185.71 % SZS status Theorem
% 185.52/185.71 % SZS output start CNFRefutation
% 185.52/185.71 fof(testcase_conclusion_fullish_018_Modified_Logical_Vocabulary_Semantics,conjecture,iext(uri_rdf_type,uri_ex_u,uri_ex_Person),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_conclusion_fullish_018_Modified_Logical_Vocabulary_Semantics)).
% 185.52/185.71 fof(c14,negated_conjecture,(~iext(uri_rdf_type,uri_ex_u,uri_ex_Person)),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_018_Modified_Logical_Vocabulary_Semantics])).
% 185.52/185.71 fof(c15,negated_conjecture,~iext(uri_rdf_type,uri_ex_u,uri_ex_Person),inference(fof_simplification,[status(thm)],[c14])).
% 185.52/185.71 cnf(c16,negated_conjecture,~iext(uri_rdf_type,uri_ex_u,uri_ex_Person),inference(split_conjunct,[status(thm)],[c15])).
% 185.52/185.71 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', rdfs_cext_def)).
% 185.52/185.71 fof(c2510,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])).
% 185.52/185.71 fof(c2511,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)],[c2510])).
% 185.52/185.71 fof(c2513,plain,(![X1256]:(![X1257]:(![X1258]:(![X1259]:((~iext(uri_rdf_type,X1256,X1257)|icext(X1257,X1256))&(~icext(X1259,X1258)|iext(uri_rdf_type,X1258,X1259))))))),inference(shift_quantors,[status(thm)],[fof(c2512,plain,((![X1256]:(![X1257]:(~iext(uri_rdf_type,X1256,X1257)|icext(X1257,X1256))))&(![X1258]:(![X1259]:(~icext(X1259,X1258)|iext(uri_rdf_type,X1258,X1259))))),inference(variable_rename,[status(thm)],[c2511])).])).
% 185.52/185.71 cnf(c2515,plain,~icext(X4958,X4957)|iext(uri_rdf_type,X4957,X4958),inference(split_conjunct,[status(thm)],[c2513])).
% 185.52/185.71 fof(testcase_premise_fullish_018_Modified_Logical_Vocabulary_Semantics,axiom,(iext(uri_rdfs_domain,uri_owl_sameAs,uri_ex_Person)&iext(uri_owl_sameAs,uri_ex_w,uri_ex_u)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_018_Modified_Logical_Vocabulary_Semantics)).
% 185.52/185.71 cnf(c12,plain,iext(uri_rdfs_domain,uri_owl_sameAs,uri_ex_Person),inference(split_conjunct,[status(thm)],[testcase_premise_fullish_018_Modified_Logical_Vocabulary_Semantics])).
% 185.52/185.71 cnf(reflexivity,axiom,X1268=X1268,theory(equality)).
% 185.52/185.71 fof(owl_eqdis_sameas,axiom,(![X]:(![Y]:(iext(uri_owl_sameAs,X,Y)<=>X=Y))),file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax', owl_eqdis_sameas)).
% 185.52/185.71 fof(c825,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])).
% 185.52/185.71 fof(c826,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)],[c825])).
% 185.52/185.71 fof(c828,plain,(![X409]:(![X410]:(![X411]:(![X412]:((~iext(uri_owl_sameAs,X409,X410)|X409=X410)&(X411!=X412|iext(uri_owl_sameAs,X411,X412))))))),inference(shift_quantors,[status(thm)],[fof(c827,plain,((![X409]:(![X410]:(~iext(uri_owl_sameAs,X409,X410)|X409=X410)))&(![X411]:(![X412]:(X411!=X412|iext(uri_owl_sameAs,X411,X412))))),inference(variable_rename,[status(thm)],[c826])).])).
% 185.52/185.71 cnf(c830,plain,X2393!=X2394|iext(uri_owl_sameAs,X2393,X2394),inference(split_conjunct,[status(thm)],[c828])).
% 185.52/185.71 cnf(c6610,plain,iext(uri_owl_sameAs,X2395,X2395),inference(resolution,[status(thm)],[c830, reflexivity])).
% 185.52/185.71 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)).
% 185.52/185.71 fof(c1025,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])).
% 185.52/185.71 fof(c1026,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)],[c1025])).
% 185.52/185.71 fof(c1027,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)],[c1026])).
% 185.52/185.71 fof(c1029,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(c1028,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)],[c1027])).])).
% 185.52/185.71 fof(c1030,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)],[c1029])).
% 185.52/185.71 cnf(c1033,plain,~iext(uri_rdfs_domain,X3141,X3139)|~iext(X3141,X3140,X3138)|icext(X3139,X3140),inference(split_conjunct,[status(thm)],[c1030])).
% 185.52/185.71 cnf(c10784,plain,~iext(uri_rdfs_domain,uri_owl_sameAs,X6750)|icext(X6750,X6749),inference(resolution,[status(thm)],[c1033, c6610])).
% 185.52/185.71 cnf(c67977,plain,icext(uri_ex_Person,X6751),inference(resolution,[status(thm)],[c10784, c12])).
% 185.52/185.71 cnf(c67997,plain,iext(uri_rdf_type,X6752,uri_ex_Person),inference(resolution,[status(thm)],[c67977, c2515])).
% 185.52/185.71 cnf(c68010,plain,$false,inference(resolution,[status(thm)],[c67997, c16])).
% 185.52/185.71 % SZS output end CNFRefutation
% 185.52/185.71
% 185.52/185.71 % Initial clauses : 1281
% 185.52/185.71 % Processed clauses : 4490
% 185.52/185.71 % Factors computed : 646
% 185.52/185.71 % Resolvents computed: 64896
% 185.52/185.71 % Tautologies deleted: 132
% 185.52/185.71 % Forward subsumed : 6514
% 185.52/185.71 % Backward subsumed : 42
% 185.52/185.71 % -------- CPU Time ---------
% 185.52/185.71 % User time : 185.084 s
% 185.52/185.71 % System time : 0.261 s
% 185.52/185.71 % Total time : 185.345 s
%------------------------------------------------------------------------------