%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB031+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:57 EDT 2024
% Result : Unsatisfiable 0.19s 0.60s
% Output : Refutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWB031+2 : TPTP v8.1.2. Released v5.2.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n027.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 22:02:08 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.60 % Version: 1.5
% 0.19/0.60 % SZS status Unsatisfiable
% 0.19/0.60 % SZS output start CNFRefutation
% 0.19/0.60 fof(owl_class_nothing_ext,axiom,(![X]:(~icext(uri_owl_Nothing,X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_class_nothing_ext)).
% 0.19/0.60 fof(c33,plain,(![X]:~icext(uri_owl_Nothing,X)),inference(fof_simplification,[status(thm)],[owl_class_nothing_ext])).
% 0.19/0.60 fof(c34,plain,(![X17]:~icext(uri_owl_Nothing,X17)),inference(variable_rename,[status(thm)],[c33])).
% 0.19/0.60 cnf(c35,plain,~icext(uri_owl_Nothing,X23),inference(split_conjunct,[status(thm)],[c34])).
% 0.19/0.60 cnf(reflexivity,axiom,X22=X22,theory(equality)).
% 0.19/0.60 fof(simple_ir,axiom,(![X]:ir(X)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', simple_ir)).
% 0.19/0.60 fof(c42,plain,(![X20]:ir(X20)),inference(variable_rename,[status(thm)],[simple_ir])).
% 0.19/0.60 cnf(c43,plain,ir(X21),inference(split_conjunct,[status(thm)],[c42])).
% 0.19/0.60 fof(owl_class_thing_ext,axiom,(![X]:(icext(uri_owl_Thing,X)<=>ir(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_class_thing_ext)).
% 0.19/0.60 fof(c36,plain,(![X]:((~icext(uri_owl_Thing,X)|ir(X))&(~ir(X)|icext(uri_owl_Thing,X)))),inference(fof_nnf,[status(thm)],[owl_class_thing_ext])).
% 0.19/0.60 fof(c37,plain,((![X]:(~icext(uri_owl_Thing,X)|ir(X)))&(![X]:(~ir(X)|icext(uri_owl_Thing,X)))),inference(shift_quantors,[status(thm)],[c36])).
% 0.19/0.60 fof(c39,plain,(![X18]:(![X19]:((~icext(uri_owl_Thing,X18)|ir(X18))&(~ir(X19)|icext(uri_owl_Thing,X19))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,((![X18]:(~icext(uri_owl_Thing,X18)|ir(X18)))&(![X19]:(~ir(X19)|icext(uri_owl_Thing,X19)))),inference(variable_rename,[status(thm)],[c37])).])).
% 0.19/0.60 cnf(c41,plain,~ir(X33)|icext(uri_owl_Thing,X33),inference(split_conjunct,[status(thm)],[c39])).
% 0.19/0.60 cnf(c47,plain,icext(uri_owl_Thing,X34),inference(resolution,[status(thm)],[c41, c43])).
% 0.19/0.60 cnf(c1,axiom,X40!=X43|X42!=X41|~icext(X40,X42)|icext(X43,X41),theory(equality)).
% 0.19/0.60 cnf(c49,plain,uri_owl_Thing!=X55|X57!=X56|icext(X55,X56),inference(resolution,[status(thm)],[c1, c47])).
% 0.19/0.60 cnf(c57,plain,uri_owl_Thing!=X59|icext(X59,X60),inference(resolution,[status(thm)],[c49, reflexivity])).
% 0.19/0.60 fof(testcase_premise_fullish_031_Large_Universe,axiom,(?[BNODE_x]:(?[BNODE_l]:(((iext(uri_owl_equivalentClass,uri_owl_Thing,BNODE_x)&iext(uri_owl_oneOf,BNODE_x,BNODE_l))&iext(uri_rdf_first,BNODE_l,uri_ex_w))&iext(uri_rdf_rest,BNODE_l,uri_rdf_nil)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_031_Large_Universe)).
% 0.19/0.60 fof(c4,plain,(?[X2]:(?[X3]:(((iext(uri_owl_equivalentClass,uri_owl_Thing,X2)&iext(uri_owl_oneOf,X2,X3))&iext(uri_rdf_first,X3,uri_ex_w))&iext(uri_rdf_rest,X3,uri_rdf_nil)))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_031_Large_Universe])).
% 0.19/0.60 fof(c5,plain,(((iext(uri_owl_equivalentClass,uri_owl_Thing,skolem0001)&iext(uri_owl_oneOf,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,uri_ex_w))&iext(uri_rdf_rest,skolem0002,uri_rdf_nil)),inference(skolemize,[status(esa)],[c4])).
% 0.19/0.60 cnf(c6,plain,iext(uri_owl_equivalentClass,uri_owl_Thing,skolem0001),inference(split_conjunct,[status(thm)],[c5])).
% 0.19/0.60 fof(owl_eqdis_equivalentclass,axiom,(![C1]:(![C2]:(iext(uri_owl_equivalentClass,C1,C2)<=>((ic(C1)&ic(C2))&(![X]:(icext(C1,X)<=>icext(C2,X))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_eqdis_equivalentclass)).
% 0.19/0.60 fof(c10,plain,(![C1]:(![C2]:((~iext(uri_owl_equivalentClass,C1,C2)|((ic(C1)&ic(C2))&(![X]:((~icext(C1,X)|icext(C2,X))&(~icext(C2,X)|icext(C1,X))))))&(((~ic(C1)|~ic(C2))|(?[X]:((~icext(C1,X)|~icext(C2,X))&(icext(C1,X)|icext(C2,X)))))|iext(uri_owl_equivalentClass,C1,C2))))),inference(fof_nnf,[status(thm)],[owl_eqdis_equivalentclass])).
% 0.19/0.60 fof(c11,plain,((![C1]:(![C2]:(~iext(uri_owl_equivalentClass,C1,C2)|((ic(C1)&ic(C2))&((![X]:(~icext(C1,X)|icext(C2,X)))&(![X]:(~icext(C2,X)|icext(C1,X))))))))&(![C1]:(![C2]:(((~ic(C1)|~ic(C2))|(?[X]:((~icext(C1,X)|~icext(C2,X))&(icext(C1,X)|icext(C2,X)))))|iext(uri_owl_equivalentClass,C1,C2))))),inference(shift_quantors,[status(thm)],[c10])).
% 0.19/0.60 fof(c12,plain,((![X4]:(![X5]:(~iext(uri_owl_equivalentClass,X4,X5)|((ic(X4)&ic(X5))&((![X6]:(~icext(X4,X6)|icext(X5,X6)))&(![X7]:(~icext(X5,X7)|icext(X4,X7))))))))&(![X8]:(![X9]:(((~ic(X8)|~ic(X9))|(?[X10]:((~icext(X8,X10)|~icext(X9,X10))&(icext(X8,X10)|icext(X9,X10)))))|iext(uri_owl_equivalentClass,X8,X9))))),inference(variable_rename,[status(thm)],[c11])).
% 0.19/0.60 fof(c14,plain,(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:((~iext(uri_owl_equivalentClass,X4,X5)|((ic(X4)&ic(X5))&((~icext(X4,X6)|icext(X5,X6))&(~icext(X5,X7)|icext(X4,X7)))))&(((~ic(X8)|~ic(X9))|((~icext(X8,skolem0003(X8,X9))|~icext(X9,skolem0003(X8,X9)))&(icext(X8,skolem0003(X8,X9))|icext(X9,skolem0003(X8,X9)))))|iext(uri_owl_equivalentClass,X8,X9))))))))),inference(shift_quantors,[status(thm)],[fof(c13,plain,((![X4]:(![X5]:(~iext(uri_owl_equivalentClass,X4,X5)|((ic(X4)&ic(X5))&((![X6]:(~icext(X4,X6)|icext(X5,X6)))&(![X7]:(~icext(X5,X7)|icext(X4,X7))))))))&(![X8]:(![X9]:(((~ic(X8)|~ic(X9))|((~icext(X8,skolem0003(X8,X9))|~icext(X9,skolem0003(X8,X9)))&(icext(X8,skolem0003(X8,X9))|icext(X9,skolem0003(X8,X9)))))|iext(uri_owl_equivalentClass,X8,X9))))),inference(skolemize,[status(esa)],[c12])).])).
% 0.19/0.60 fof(c15,plain,(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:((((~iext(uri_owl_equivalentClass,X4,X5)|ic(X4))&(~iext(uri_owl_equivalentClass,X4,X5)|ic(X5)))&((~iext(uri_owl_equivalentClass,X4,X5)|(~icext(X4,X6)|icext(X5,X6)))&(~iext(uri_owl_equivalentClass,X4,X5)|(~icext(X5,X7)|icext(X4,X7)))))&((((~ic(X8)|~ic(X9))|(~icext(X8,skolem0003(X8,X9))|~icext(X9,skolem0003(X8,X9))))|iext(uri_owl_equivalentClass,X8,X9))&(((~ic(X8)|~ic(X9))|(icext(X8,skolem0003(X8,X9))|icext(X9,skolem0003(X8,X9))))|iext(uri_owl_equivalentClass,X8,X9)))))))))),inference(distribute,[status(thm)],[c14])).
% 0.19/0.60 cnf(c18,plain,~iext(uri_owl_equivalentClass,X62,X64)|~icext(X62,X63)|icext(X64,X63),inference(split_conjunct,[status(thm)],[c15])).
% 0.19/0.60 cnf(c60,plain,~icext(uri_owl_Thing,X65)|icext(skolem0001,X65),inference(resolution,[status(thm)],[c18, c6])).
% 0.19/0.60 cnf(c61,plain,icext(skolem0001,X66),inference(resolution,[status(thm)],[c60, c47])).
% 0.19/0.60 cnf(c8,plain,iext(uri_rdf_first,skolem0002,uri_ex_w),inference(split_conjunct,[status(thm)],[c5])).
% 0.19/0.60 cnf(c9,plain,iext(uri_rdf_rest,skolem0002,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c5])).
% 0.19/0.60 cnf(c7,plain,iext(uri_owl_oneOf,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c5])).
% 0.19/0.60 fof(owl_enum_class_001,axiom,(![Z]:(![S1]:(![A1]:((iext(uri_rdf_first,S1,A1)&iext(uri_rdf_rest,S1,uri_rdf_nil))=>(iext(uri_owl_oneOf,Z,S1)<=>(ic(Z)&(![X]:(icext(Z,X)<=>X=A1)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_enum_class_001)).
% 0.19/0.60 fof(c22,plain,(![Z]:(![S1]:(![A1]:((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&(![X]:((~icext(Z,X)|X=A1)&(X!=A1|icext(Z,X))))))&((~ic(Z)|(?[X]:((~icext(Z,X)|X!=A1)&(icext(Z,X)|X=A1))))|iext(uri_owl_oneOf,Z,S1))))))),inference(fof_nnf,[status(thm)],[owl_enum_class_001])).
% 0.19/0.60 fof(c23,plain,(![Z]:(![S1]:(![A1]:((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]:(~icext(Z,X)|X=A1))&(![X]:(X!=A1|icext(Z,X))))))&((~ic(Z)|(?[X]:((~icext(Z,X)|X!=A1)&(icext(Z,X)|X=A1))))|iext(uri_owl_oneOf,Z,S1))))))),inference(shift_quantors,[status(thm)],[c22])).
% 0.19/0.60 fof(c24,plain,(![X11]:(![X12]:(![X13]:((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,uri_rdf_nil))|((~iext(uri_owl_oneOf,X11,X12)|(ic(X11)&((![X14]:(~icext(X11,X14)|X14=X13))&(![X15]:(X15!=X13|icext(X11,X15))))))&((~ic(X11)|(?[X16]:((~icext(X11,X16)|X16!=X13)&(icext(X11,X16)|X16=X13))))|iext(uri_owl_oneOf,X11,X12))))))),inference(variable_rename,[status(thm)],[c23])).
% 0.19/0.60 fof(c26,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,uri_rdf_nil))|((~iext(uri_owl_oneOf,X11,X12)|(ic(X11)&((~icext(X11,X14)|X14=X13)&(X15!=X13|icext(X11,X15)))))&((~ic(X11)|((~icext(X11,skolem0004(X11,X12,X13))|skolem0004(X11,X12,X13)!=X13)&(icext(X11,skolem0004(X11,X12,X13))|skolem0004(X11,X12,X13)=X13)))|iext(uri_owl_oneOf,X11,X12))))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,(![X11]:(![X12]:(![X13]:((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,uri_rdf_nil))|((~iext(uri_owl_oneOf,X11,X12)|(ic(X11)&((![X14]:(~icext(X11,X14)|X14=X13))&(![X15]:(X15!=X13|icext(X11,X15))))))&((~ic(X11)|((~icext(X11,skolem0004(X11,X12,X13))|skolem0004(X11,X12,X13)!=X13)&(icext(X11,skolem0004(X11,X12,X13))|skolem0004(X11,X12,X13)=X13)))|iext(uri_owl_oneOf,X11,X12))))))),inference(skolemize,[status(esa)],[c24])).])).
% 0.19/0.60 fof(c27,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,uri_rdf_nil))|(~iext(uri_owl_oneOf,X11,X12)|ic(X11)))&(((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,uri_rdf_nil))|(~iext(uri_owl_oneOf,X11,X12)|(~icext(X11,X14)|X14=X13)))&((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,uri_rdf_nil))|(~iext(uri_owl_oneOf,X11,X12)|(X15!=X13|icext(X11,X15))))))&(((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,uri_rdf_nil))|((~ic(X11)|(~icext(X11,skolem0004(X11,X12,X13))|skolem0004(X11,X12,X13)!=X13))|iext(uri_owl_oneOf,X11,X12)))&((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,uri_rdf_nil))|((~ic(X11)|(icext(X11,skolem0004(X11,X12,X13))|skolem0004(X11,X12,X13)=X13))|iext(uri_owl_oneOf,X11,X12)))))))))),inference(distribute,[status(thm)],[c26])).
% 0.19/0.60 cnf(c29,plain,~iext(uri_rdf_first,X96,X99)|~iext(uri_rdf_rest,X96,uri_rdf_nil)|~iext(uri_owl_oneOf,X98,X96)|~icext(X98,X97)|X97=X99,inference(split_conjunct,[status(thm)],[c27])).
% 0.19/0.60 cnf(c92,plain,~iext(uri_rdf_first,skolem0002,X159)|~iext(uri_rdf_rest,skolem0002,uri_rdf_nil)|~icext(skolem0001,X160)|X160=X159,inference(resolution,[status(thm)],[c29, c7])).
% 0.19/0.60 cnf(c129,plain,~iext(uri_rdf_first,skolem0002,X162)|~icext(skolem0001,X163)|X163=X162,inference(resolution,[status(thm)],[c92, c9])).
% 0.19/0.60 cnf(c131,plain,~icext(skolem0001,X164)|X164=uri_ex_w,inference(resolution,[status(thm)],[c129, c8])).
% 0.19/0.60 cnf(c132,plain,X165=uri_ex_w,inference(resolution,[status(thm)],[c131, c61])).
% 0.19/0.60 cnf(transitivity,axiom,X29!=X27|X27!=X28|X29=X28,theory(equality)).
% 0.19/0.60 cnf(symmetry,axiom,X25!=X24|X24=X25,theory(equality)).
% 0.19/0.60 cnf(c151,plain,uri_ex_w=X168,inference(resolution,[status(thm)],[c132, symmetry])).
% 0.19/0.60 cnf(c162,plain,X182!=uri_ex_w|X182=X183,inference(resolution,[status(thm)],[c151, transitivity])).
% 0.19/0.60 cnf(c195,plain,X185=X186,inference(resolution,[status(thm)],[c162, c132])).
% 0.19/0.60 cnf(c224,plain,icext(X188,X187),inference(resolution,[status(thm)],[c195, c57])).
% 0.19/0.60 cnf(c231,plain,$false,inference(resolution,[status(thm)],[c224, c35])).
% 0.19/0.60 % SZS output end CNFRefutation
% 0.19/0.60
% 0.19/0.60 % Initial clauses : 26
% 0.19/0.60 % Processed clauses : 95
% 0.19/0.60 % Factors computed : 7
% 0.19/0.60 % Resolvents computed: 182
% 0.19/0.60 % Tautologies deleted: 7
% 0.19/0.60 % Forward subsumed : 38
% 0.19/0.60 % Backward subsumed : 42
% 0.19/0.60 % -------- CPU Time ---------
% 0.19/0.60 % User time : 0.255 s
% 0.19/0.60 % System time : 0.011 s
% 0.19/0.60 % Total time : 0.266 s
%------------------------------------------------------------------------------