%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB030+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:56 EDT 2024
% Result : Unsatisfiable 0.40s 0.61s
% Output : Refutation 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWB030+2 : TPTP v8.1.2. Released v5.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n010.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 22:05:37 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.40/0.61 % Version: 1.5
% 0.40/0.61 % SZS status Unsatisfiable
% 0.40/0.61 % SZS output start CNFRefutation
% 0.40/0.61 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rdfs_cext_def)).
% 0.40/0.61 fof(c24,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.40/0.61 fof(c25,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)],[c24])).
% 0.40/0.61 fof(c27,plain,(![X12]:(![X13]:(![X14]:(![X15]:((~iext(uri_rdf_type,X12,X13)|icext(X13,X12))&(~icext(X15,X14)|iext(uri_rdf_type,X14,X15))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,((![X12]:(![X13]:(~iext(uri_rdf_type,X12,X13)|icext(X13,X12))))&(![X14]:(![X15]:(~icext(X15,X14)|iext(uri_rdf_type,X14,X15))))),inference(variable_rename,[status(thm)],[c25])).])).
% 0.40/0.61 cnf(c28,plain,~iext(uri_rdf_type,X21,X20)|icext(X20,X21),inference(split_conjunct,[status(thm)],[c27])).
% 0.40/0.61 fof(testcase_premise_fullish_030_Bad_Class,axiom,(?[BNODE_x]:((((iext(uri_rdf_type,uri_ex_c,uri_owl_Class)&iext(uri_owl_complementOf,uri_ex_c,BNODE_x))&iext(uri_rdf_type,BNODE_x,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_x,uri_rdf_type))&iext(uri_owl_hasSelf,BNODE_x,literal_typed(dat_str_true,uri_xsd_boolean)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_030_Bad_Class)).
% 0.40/0.61 fof(c0,plain,(?[X2]:((((iext(uri_rdf_type,uri_ex_c,uri_owl_Class)&iext(uri_owl_complementOf,uri_ex_c,X2))&iext(uri_rdf_type,X2,uri_owl_Restriction))&iext(uri_owl_onProperty,X2,uri_rdf_type))&iext(uri_owl_hasSelf,X2,literal_typed(dat_str_true,uri_xsd_boolean)))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_030_Bad_Class])).
% 0.40/0.61 fof(c1,plain,((((iext(uri_rdf_type,uri_ex_c,uri_owl_Class)&iext(uri_owl_complementOf,uri_ex_c,skolem0001))&iext(uri_rdf_type,skolem0001,uri_owl_Restriction))&iext(uri_owl_onProperty,skolem0001,uri_rdf_type))&iext(uri_owl_hasSelf,skolem0001,literal_typed(dat_str_true,uri_xsd_boolean))),inference(skolemize,[status(esa)],[c0])).
% 0.40/0.61 cnf(c3,plain,iext(uri_owl_complementOf,uri_ex_c,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 0.40/0.61 fof(owl_bool_complementof_class,axiom,(![Z]:(![C]:(iext(uri_owl_complementOf,Z,C)=>((ic(Z)&ic(C))&(![X]:(icext(Z,X)<=>(~icext(C,X)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_bool_complementof_class)).
% 0.40/0.61 fof(c7,plain,(![Z]:(![C]:(iext(uri_owl_complementOf,Z,C)=>((ic(Z)&ic(C))&(![X]:(icext(Z,X)<=>~icext(C,X))))))),inference(fof_simplification,[status(thm)],[owl_bool_complementof_class])).
% 0.40/0.61 fof(c8,plain,(![Z]:(![C]:(~iext(uri_owl_complementOf,Z,C)|((ic(Z)&ic(C))&(![X]:((~icext(Z,X)|~icext(C,X))&(icext(C,X)|icext(Z,X)))))))),inference(fof_nnf,[status(thm)],[c7])).
% 0.40/0.61 fof(c9,plain,(![Z]:(![C]:(~iext(uri_owl_complementOf,Z,C)|((ic(Z)&ic(C))&((![X]:(~icext(Z,X)|~icext(C,X)))&(![X]:(icext(C,X)|icext(Z,X)))))))),inference(shift_quantors,[status(thm)],[c8])).
% 0.40/0.61 fof(c11,plain,(![X3]:(![X4]:(![X5]:(![X6]:(~iext(uri_owl_complementOf,X3,X4)|((ic(X3)&ic(X4))&((~icext(X3,X5)|~icext(X4,X5))&(icext(X4,X6)|icext(X3,X6))))))))),inference(shift_quantors,[status(thm)],[fof(c10,plain,(![X3]:(![X4]:(~iext(uri_owl_complementOf,X3,X4)|((ic(X3)&ic(X4))&((![X5]:(~icext(X3,X5)|~icext(X4,X5)))&(![X6]:(icext(X4,X6)|icext(X3,X6)))))))),inference(variable_rename,[status(thm)],[c9])).])).
% 0.40/0.61 fof(c12,plain,(![X3]:(![X4]:(![X5]:(![X6]:(((~iext(uri_owl_complementOf,X3,X4)|ic(X3))&(~iext(uri_owl_complementOf,X3,X4)|ic(X4)))&((~iext(uri_owl_complementOf,X3,X4)|(~icext(X3,X5)|~icext(X4,X5)))&(~iext(uri_owl_complementOf,X3,X4)|(icext(X4,X6)|icext(X3,X6))))))))),inference(distribute,[status(thm)],[c11])).
% 0.40/0.61 cnf(c16,plain,~iext(uri_owl_complementOf,X28,X29)|icext(X29,X30)|icext(X28,X30),inference(split_conjunct,[status(thm)],[c12])).
% 0.40/0.61 cnf(c37,plain,icext(skolem0001,X31)|icext(uri_ex_c,X31),inference(resolution,[status(thm)],[c16, c3])).
% 0.40/0.61 cnf(c6,plain,iext(uri_owl_hasSelf,skolem0001,literal_typed(dat_str_true,uri_xsd_boolean)),inference(split_conjunct,[status(thm)],[c1])).
% 0.40/0.61 cnf(c5,plain,iext(uri_owl_onProperty,skolem0001,uri_rdf_type),inference(split_conjunct,[status(thm)],[c1])).
% 0.40/0.61 fof(owl_restrict_hasself,axiom,(![Z]:(![P]:(![V]:((iext(uri_owl_hasSelf,Z,V)&iext(uri_owl_onProperty,Z,P))=>(![X]:(icext(Z,X)<=>iext(P,X,X))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_restrict_hasself)).
% 0.40/0.61 fof(c17,plain,(![Z]:(![P]:(![V]:((~iext(uri_owl_hasSelf,Z,V)|~iext(uri_owl_onProperty,Z,P))|(![X]:((~icext(Z,X)|iext(P,X,X))&(~iext(P,X,X)|icext(Z,X)))))))),inference(fof_nnf,[status(thm)],[owl_restrict_hasself])).
% 0.40/0.61 fof(c18,plain,(![Z]:(![P]:(((![V]:~iext(uri_owl_hasSelf,Z,V))|~iext(uri_owl_onProperty,Z,P))|((![X]:(~icext(Z,X)|iext(P,X,X)))&(![X]:(~iext(P,X,X)|icext(Z,X))))))),inference(shift_quantors,[status(thm)],[c17])).
% 0.40/0.61 fof(c20,plain,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:((~iext(uri_owl_hasSelf,X7,X9)|~iext(uri_owl_onProperty,X7,X8))|((~icext(X7,X10)|iext(X8,X10,X10))&(~iext(X8,X11,X11)|icext(X7,X11))))))))),inference(shift_quantors,[status(thm)],[fof(c19,plain,(![X7]:(![X8]:(((![X9]:~iext(uri_owl_hasSelf,X7,X9))|~iext(uri_owl_onProperty,X7,X8))|((![X10]:(~icext(X7,X10)|iext(X8,X10,X10)))&(![X11]:(~iext(X8,X11,X11)|icext(X7,X11))))))),inference(variable_rename,[status(thm)],[c18])).])).
% 0.40/0.61 fof(c21,plain,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(((~iext(uri_owl_hasSelf,X7,X9)|~iext(uri_owl_onProperty,X7,X8))|(~icext(X7,X10)|iext(X8,X10,X10)))&((~iext(uri_owl_hasSelf,X7,X9)|~iext(uri_owl_onProperty,X7,X8))|(~iext(X8,X11,X11)|icext(X7,X11))))))))),inference(distribute,[status(thm)],[c20])).
% 0.40/0.61 cnf(c22,plain,~iext(uri_owl_hasSelf,X36,X37)|~iext(uri_owl_onProperty,X36,X38)|~icext(X36,X39)|iext(X38,X39,X39),inference(split_conjunct,[status(thm)],[c21])).
% 0.40/0.61 cnf(c46,plain,~iext(uri_owl_hasSelf,skolem0001,X52)|~icext(skolem0001,X51)|iext(uri_rdf_type,X51,X51),inference(resolution,[status(thm)],[c22, c5])).
% 0.40/0.61 cnf(c55,plain,~icext(skolem0001,X53)|iext(uri_rdf_type,X53,X53),inference(resolution,[status(thm)],[c46, c6])).
% 0.40/0.61 cnf(c56,plain,iext(uri_rdf_type,X54,X54)|icext(uri_ex_c,X54),inference(resolution,[status(thm)],[c55, c37])).
% 0.40/0.61 cnf(c59,plain,icext(uri_ex_c,X56)|icext(X56,X56),inference(resolution,[status(thm)],[c56, c28])).
% 0.40/0.61 cnf(c61,plain,icext(uri_ex_c,uri_ex_c),inference(factor,[status(thm)],[c59])).
% 0.40/0.61 cnf(c15,plain,~iext(uri_owl_complementOf,X22,X23)|~icext(X22,X24)|~icext(X23,X24),inference(split_conjunct,[status(thm)],[c12])).
% 0.40/0.61 cnf(c34,plain,~icext(uri_ex_c,X27)|~icext(skolem0001,X27),inference(resolution,[status(thm)],[c15, c3])).
% 0.40/0.61 cnf(c29,plain,~icext(X25,X26)|iext(uri_rdf_type,X26,X25),inference(split_conjunct,[status(thm)],[c27])).
% 0.40/0.61 cnf(c40,plain,icext(skolem0001,X35)|iext(uri_rdf_type,X35,uri_ex_c),inference(resolution,[status(thm)],[c37, c29])).
% 0.40/0.61 cnf(c23,plain,~iext(uri_owl_hasSelf,X45,X47)|~iext(uri_owl_onProperty,X45,X48)|~iext(X48,X46,X46)|icext(X45,X46),inference(split_conjunct,[status(thm)],[c21])).
% 0.40/0.61 cnf(c52,plain,~iext(uri_owl_hasSelf,X63,X64)|~iext(uri_owl_onProperty,X63,uri_rdf_type)|icext(X63,uri_ex_c)|icext(skolem0001,uri_ex_c),inference(resolution,[status(thm)],[c23, c40])).
% 0.40/0.61 cnf(c80,plain,~iext(uri_owl_hasSelf,skolem0001,X69)|icext(skolem0001,uri_ex_c),inference(resolution,[status(thm)],[c52, c5])).
% 0.40/0.61 cnf(c81,plain,icext(skolem0001,uri_ex_c),inference(resolution,[status(thm)],[c80, c6])).
% 0.40/0.61 cnf(c85,plain,~icext(uri_ex_c,uri_ex_c),inference(resolution,[status(thm)],[c81, c34])).
% 0.40/0.61 cnf(c92,plain,$false,inference(resolution,[status(thm)],[c85, c61])).
% 0.40/0.61 % SZS output end CNFRefutation
% 0.40/0.61
% 0.40/0.61 % Initial clauses : 13
% 0.40/0.61 % Processed clauses : 38
% 0.40/0.61 % Factors computed : 4
% 0.40/0.61 % Resolvents computed: 59
% 0.40/0.61 % Tautologies deleted: 2
% 0.40/0.61 % Forward subsumed : 16
% 0.40/0.61 % Backward subsumed : 3
% 0.40/0.61 % -------- CPU Time ---------
% 0.40/0.61 % User time : 0.242 s
% 0.40/0.61 % System time : 0.012 s
% 0.40/0.61 % Total time : 0.254 s
%------------------------------------------------------------------------------