%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB029+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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 : Theorem 0.51s 0.67s
% Output : Refutation 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWB029+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 : n022.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:04:22 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.51/0.67 % Version: 1.5
% 0.51/0.67 % SZS status Theorem
% 0.51/0.67 % SZS output start CNFRefutation
% 0.51/0.67 fof(testcase_premise_fullish_029_Ex_Falso_Quodlibet,axiom,(?[BNODE_x]:(?[BNODE_y]:(?[BNODE_l1]:(?[BNODE_l2]:((((((((iext(uri_rdf_type,uri_ex_A,uri_owl_Class)&iext(uri_rdf_type,uri_ex_B,uri_owl_Class))&iext(uri_rdf_type,uri_ex_w,BNODE_x))&iext(uri_owl_intersectionOf,BNODE_x,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_ex_A))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,BNODE_y))&iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil))&iext(uri_owl_complementOf,BNODE_y,uri_ex_A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_029_Ex_Falso_Quodlibet)).
% 0.51/0.67 fof(c0,plain,(?[BNODE_x]:(?[BNODE_y]:((?[BNODE_l1]:(?[BNODE_l2]:(((((((iext(uri_rdf_type,uri_ex_A,uri_owl_Class)&iext(uri_rdf_type,uri_ex_B,uri_owl_Class))&iext(uri_rdf_type,uri_ex_w,BNODE_x))&iext(uri_owl_intersectionOf,BNODE_x,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_ex_A))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,BNODE_y))&iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil))))&iext(uri_owl_complementOf,BNODE_y,uri_ex_A)))),inference(shift_quantors,[status(thm)],[testcase_premise_fullish_029_Ex_Falso_Quodlibet])).
% 0.51/0.67 fof(c1,plain,(?[X2]:(?[X3]:((?[X4]:(?[X5]:(((((((iext(uri_rdf_type,uri_ex_A,uri_owl_Class)&iext(uri_rdf_type,uri_ex_B,uri_owl_Class))&iext(uri_rdf_type,uri_ex_w,X2))&iext(uri_owl_intersectionOf,X2,X4))&iext(uri_rdf_first,X4,uri_ex_A))&iext(uri_rdf_rest,X4,X5))&iext(uri_rdf_first,X5,X3))&iext(uri_rdf_rest,X5,uri_rdf_nil))))&iext(uri_owl_complementOf,X3,uri_ex_A)))),inference(variable_rename,[status(thm)],[c0])).
% 0.51/0.67 fof(c2,plain,((((((((iext(uri_rdf_type,uri_ex_A,uri_owl_Class)&iext(uri_rdf_type,uri_ex_B,uri_owl_Class))&iext(uri_rdf_type,uri_ex_w,skolem0001))&iext(uri_owl_intersectionOf,skolem0001,skolem0003))&iext(uri_rdf_first,skolem0003,uri_ex_A))&iext(uri_rdf_rest,skolem0003,skolem0004))&iext(uri_rdf_first,skolem0004,skolem0002))&iext(uri_rdf_rest,skolem0004,uri_rdf_nil))&iext(uri_owl_complementOf,skolem0002,uri_ex_A)),inference(skolemize,[status(esa)],[c1])).
% 0.51/0.67 cnf(c11,plain,iext(uri_owl_complementOf,skolem0002,uri_ex_A),inference(split_conjunct,[status(thm)],[c2])).
% 0.51/0.67 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.51/0.67 fof(c30,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.51/0.67 fof(c31,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)],[c30])).
% 0.51/0.67 fof(c32,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)],[c31])).
% 0.51/0.67 fof(c34,plain,(![X14]:(![X15]:(![X16]:(![X17]:(~iext(uri_owl_complementOf,X14,X15)|((ic(X14)&ic(X15))&((~icext(X14,X16)|~icext(X15,X16))&(icext(X15,X17)|icext(X14,X17))))))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,(![X14]:(![X15]:(~iext(uri_owl_complementOf,X14,X15)|((ic(X14)&ic(X15))&((![X16]:(~icext(X14,X16)|~icext(X15,X16)))&(![X17]:(icext(X15,X17)|icext(X14,X17)))))))),inference(variable_rename,[status(thm)],[c32])).])).
% 0.51/0.67 fof(c35,plain,(![X14]:(![X15]:(![X16]:(![X17]:(((~iext(uri_owl_complementOf,X14,X15)|ic(X14))&(~iext(uri_owl_complementOf,X14,X15)|ic(X15)))&((~iext(uri_owl_complementOf,X14,X15)|(~icext(X14,X16)|~icext(X15,X16)))&(~iext(uri_owl_complementOf,X14,X15)|(icext(X15,X17)|icext(X14,X17))))))))),inference(distribute,[status(thm)],[c34])).
% 0.51/0.67 cnf(c38,plain,~iext(uri_owl_complementOf,X45,X46)|~icext(X45,X47)|~icext(X46,X47),inference(split_conjunct,[status(thm)],[c35])).
% 0.51/0.67 cnf(c57,plain,~icext(skolem0002,X48)|~icext(uri_ex_A,X48),inference(resolution,[status(thm)],[c38, c11])).
% 0.51/0.67 cnf(c5,plain,iext(uri_rdf_type,uri_ex_w,skolem0001),inference(split_conjunct,[status(thm)],[c2])).
% 0.51/0.67 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.51/0.67 fof(c40,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.51/0.67 fof(c41,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)],[c40])).
% 0.51/0.67 fof(c43,plain,(![X18]:(![X19]:(![X20]:(![X21]:((~iext(uri_rdf_type,X18,X19)|icext(X19,X18))&(~icext(X21,X20)|iext(uri_rdf_type,X20,X21))))))),inference(shift_quantors,[status(thm)],[fof(c42,plain,((![X18]:(![X19]:(~iext(uri_rdf_type,X18,X19)|icext(X19,X18))))&(![X20]:(![X21]:(~icext(X21,X20)|iext(uri_rdf_type,X20,X21))))),inference(variable_rename,[status(thm)],[c41])).])).
% 0.51/0.67 cnf(c44,plain,~iext(uri_rdf_type,X31,X32)|icext(X32,X31),inference(split_conjunct,[status(thm)],[c43])).
% 0.51/0.67 cnf(c49,plain,icext(skolem0001,uri_ex_w),inference(resolution,[status(thm)],[c44, c5])).
% 0.51/0.67 cnf(c7,plain,iext(uri_rdf_first,skolem0003,uri_ex_A),inference(split_conjunct,[status(thm)],[c2])).
% 0.51/0.67 cnf(c8,plain,iext(uri_rdf_rest,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c2])).
% 0.51/0.67 cnf(c9,plain,iext(uri_rdf_first,skolem0004,skolem0002),inference(split_conjunct,[status(thm)],[c2])).
% 0.51/0.67 cnf(c10,plain,iext(uri_rdf_rest,skolem0004,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c2])).
% 0.51/0.67 cnf(c6,plain,iext(uri_owl_intersectionOf,skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c2])).
% 0.51/0.67 fof(owl_bool_intersectionof_class_002,axiom,(![Z]:(![S1]:(![C1]:(![S2]:(![C2]:((((iext(uri_rdf_first,S1,C1)&iext(uri_rdf_rest,S1,S2))&iext(uri_rdf_first,S2,C2))&iext(uri_rdf_rest,S2,uri_rdf_nil))=>(iext(uri_owl_intersectionOf,Z,S1)<=>(((ic(Z)&ic(C1))&ic(C2))&(![X]:(icext(Z,X)<=>(icext(C1,X)&icext(C2,X)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_bool_intersectionof_class_002)).
% 0.51/0.67 fof(c15,plain,(![Z]:(![S1]:(![C1]:(![S2]:(![C2]:((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,Z,S1)|(((ic(Z)&ic(C1))&ic(C2))&(![X]:((~icext(Z,X)|(icext(C1,X)&icext(C2,X)))&((~icext(C1,X)|~icext(C2,X))|icext(Z,X))))))&((((~ic(Z)|~ic(C1))|~ic(C2))|(?[X]:((~icext(Z,X)|(~icext(C1,X)|~icext(C2,X)))&(icext(Z,X)|(icext(C1,X)&icext(C2,X))))))|iext(uri_owl_intersectionOf,Z,S1))))))))),inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_002])).
% 0.51/0.67 fof(c16,plain,(![Z]:(![S1]:(![C1]:(![S2]:(![C2]:((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,Z,S1)|(((ic(Z)&ic(C1))&ic(C2))&((![X]:(~icext(Z,X)|(icext(C1,X)&icext(C2,X))))&(![X]:((~icext(C1,X)|~icext(C2,X))|icext(Z,X))))))&((((~ic(Z)|~ic(C1))|~ic(C2))|(?[X]:((~icext(Z,X)|(~icext(C1,X)|~icext(C2,X)))&(icext(Z,X)|(icext(C1,X)&icext(C2,X))))))|iext(uri_owl_intersectionOf,Z,S1))))))))),inference(shift_quantors,[status(thm)],[c15])).
% 0.51/0.67 fof(c17,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,X6,X7)|(((ic(X6)&ic(X8))&ic(X10))&((![X11]:(~icext(X6,X11)|(icext(X8,X11)&icext(X10,X11))))&(![X12]:((~icext(X8,X12)|~icext(X10,X12))|icext(X6,X12))))))&((((~ic(X6)|~ic(X8))|~ic(X10))|(?[X13]:((~icext(X6,X13)|(~icext(X8,X13)|~icext(X10,X13)))&(icext(X6,X13)|(icext(X8,X13)&icext(X10,X13))))))|iext(uri_owl_intersectionOf,X6,X7))))))))),inference(variable_rename,[status(thm)],[c16])).
% 0.51/0.67 fof(c19,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,X6,X7)|(((ic(X6)&ic(X8))&ic(X10))&((~icext(X6,X11)|(icext(X8,X11)&icext(X10,X11)))&((~icext(X8,X12)|~icext(X10,X12))|icext(X6,X12)))))&((((~ic(X6)|~ic(X8))|~ic(X10))|((~icext(X6,skolem0005(X6,X7,X8,X9,X10))|(~icext(X8,skolem0005(X6,X7,X8,X9,X10))|~icext(X10,skolem0005(X6,X7,X8,X9,X10))))&(icext(X6,skolem0005(X6,X7,X8,X9,X10))|(icext(X8,skolem0005(X6,X7,X8,X9,X10))&icext(X10,skolem0005(X6,X7,X8,X9,X10))))))|iext(uri_owl_intersectionOf,X6,X7))))))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,X6,X7)|(((ic(X6)&ic(X8))&ic(X10))&((![X11]:(~icext(X6,X11)|(icext(X8,X11)&icext(X10,X11))))&(![X12]:((~icext(X8,X12)|~icext(X10,X12))|icext(X6,X12))))))&((((~ic(X6)|~ic(X8))|~ic(X10))|((~icext(X6,skolem0005(X6,X7,X8,X9,X10))|(~icext(X8,skolem0005(X6,X7,X8,X9,X10))|~icext(X10,skolem0005(X6,X7,X8,X9,X10))))&(icext(X6,skolem0005(X6,X7,X8,X9,X10))|(icext(X8,skolem0005(X6,X7,X8,X9,X10))&icext(X10,skolem0005(X6,X7,X8,X9,X10))))))|iext(uri_owl_intersectionOf,X6,X7))))))))),inference(skolemize,[status(esa)],[c17])).])).
% 0.51/0.67 fof(c20,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((((((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X6,X7)|ic(X6)))&((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X6,X7)|ic(X8))))&((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X6,X7)|ic(X10))))&((((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X6,X7)|(~icext(X6,X11)|icext(X8,X11))))&((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X6,X7)|(~icext(X6,X11)|icext(X10,X11)))))&((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X6,X7)|((~icext(X8,X12)|~icext(X10,X12))|icext(X6,X12))))))&(((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((((~ic(X6)|~ic(X8))|~ic(X10))|(~icext(X6,skolem0005(X6,X7,X8,X9,X10))|(~icext(X8,skolem0005(X6,X7,X8,X9,X10))|~icext(X10,skolem0005(X6,X7,X8,X9,X10)))))|iext(uri_owl_intersectionOf,X6,X7)))&(((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((((~ic(X6)|~ic(X8))|~ic(X10))|(icext(X6,skolem0005(X6,X7,X8,X9,X10))|icext(X8,skolem0005(X6,X7,X8,X9,X10))))|iext(uri_owl_intersectionOf,X6,X7)))&((((~iext(uri_rdf_first,X7,X8)|~iext(uri_rdf_rest,X7,X9))|~iext(uri_rdf_first,X9,X10))|~iext(uri_rdf_rest,X9,uri_rdf_nil))|((((~ic(X6)|~ic(X8))|~ic(X10))|(icext(X6,skolem0005(X6,X7,X8,X9,X10))|icext(X10,skolem0005(X6,X7,X8,X9,X10))))|iext(uri_owl_intersectionOf,X6,X7))))))))))))),inference(distribute,[status(thm)],[c19])).
% 0.51/0.67 cnf(c24,plain,~iext(uri_rdf_first,X53,X56)|~iext(uri_rdf_rest,X53,X54)|~iext(uri_rdf_first,X54,X58)|~iext(uri_rdf_rest,X54,uri_rdf_nil)|~iext(uri_owl_intersectionOf,X57,X53)|~icext(X57,X55)|icext(X56,X55),inference(split_conjunct,[status(thm)],[c20])).
% 0.51/0.67 cnf(c62,plain,~iext(uri_rdf_first,skolem0003,X114)|~iext(uri_rdf_rest,skolem0003,X112)|~iext(uri_rdf_first,X112,X113)|~iext(uri_rdf_rest,X112,uri_rdf_nil)|~icext(skolem0001,X111)|icext(X114,X111),inference(resolution,[status(thm)],[c24, c6])).
% 0.51/0.67 cnf(c90,plain,~iext(uri_rdf_first,skolem0003,X115)|~iext(uri_rdf_rest,skolem0003,skolem0004)|~iext(uri_rdf_first,skolem0004,X117)|~icext(skolem0001,X116)|icext(X115,X116),inference(resolution,[status(thm)],[c62, c10])).
% 0.51/0.67 cnf(c91,plain,~iext(uri_rdf_first,skolem0003,X123)|~iext(uri_rdf_rest,skolem0003,skolem0004)|~icext(skolem0001,X124)|icext(X123,X124),inference(resolution,[status(thm)],[c90, c9])).
% 0.51/0.67 cnf(c94,plain,~iext(uri_rdf_first,skolem0003,X126)|~icext(skolem0001,X125)|icext(X126,X125),inference(resolution,[status(thm)],[c91, c8])).
% 0.51/0.67 cnf(c95,plain,~icext(skolem0001,X127)|icext(uri_ex_A,X127),inference(resolution,[status(thm)],[c94, c7])).
% 0.51/0.67 cnf(c96,plain,icext(uri_ex_A,uri_ex_w),inference(resolution,[status(thm)],[c95, c49])).
% 0.51/0.67 cnf(c97,plain,~icext(skolem0002,uri_ex_w),inference(resolution,[status(thm)],[c96, c57])).
% 0.51/0.67 cnf(c25,plain,~iext(uri_rdf_first,X64,X67)|~iext(uri_rdf_rest,X64,X65)|~iext(uri_rdf_first,X65,X69)|~iext(uri_rdf_rest,X65,uri_rdf_nil)|~iext(uri_owl_intersectionOf,X68,X64)|~icext(X68,X66)|icext(X69,X66),inference(split_conjunct,[status(thm)],[c20])).
% 0.51/0.67 cnf(c68,plain,~iext(uri_rdf_first,skolem0003,X131)|~iext(uri_rdf_rest,skolem0003,X130)|~iext(uri_rdf_first,X130,X129)|~iext(uri_rdf_rest,X130,uri_rdf_nil)|~icext(skolem0001,X128)|icext(X129,X128),inference(resolution,[status(thm)],[c25, c6])).
% 0.51/0.67 cnf(c101,plain,~iext(uri_rdf_first,skolem0003,X133)|~iext(uri_rdf_rest,skolem0003,skolem0004)|~iext(uri_rdf_first,skolem0004,X132)|~icext(skolem0001,X134)|icext(X132,X134),inference(resolution,[status(thm)],[c68, c10])).
% 0.51/0.67 cnf(c103,plain,~iext(uri_rdf_first,skolem0003,X139)|~iext(uri_rdf_rest,skolem0003,skolem0004)|~icext(skolem0001,X140)|icext(skolem0002,X140),inference(resolution,[status(thm)],[c101, c9])).
% 0.51/0.67 cnf(c105,plain,~iext(uri_rdf_first,skolem0003,X141)|~icext(skolem0001,X142)|icext(skolem0002,X142),inference(resolution,[status(thm)],[c103, c8])).
% 0.51/0.67 cnf(c106,plain,~icext(skolem0001,X143)|icext(skolem0002,X143),inference(resolution,[status(thm)],[c105, c7])).
% 0.51/0.67 cnf(c107,plain,icext(skolem0002,uri_ex_w),inference(resolution,[status(thm)],[c106, c49])).
% 0.51/0.67 cnf(c109,plain,$false,inference(resolution,[status(thm)],[c107, c97])).
% 0.51/0.67 % SZS output end CNFRefutation
% 0.51/0.67
% 0.51/0.67 % Initial clauses : 25
% 0.51/0.67 % Processed clauses : 61
% 0.51/0.67 % Factors computed : 4
% 0.51/0.67 % Resolvents computed: 60
% 0.51/0.67 % Tautologies deleted: 1
% 0.51/0.67 % Forward subsumed : 14
% 0.51/0.67 % Backward subsumed : 12
% 0.51/0.67 % -------- CPU Time ---------
% 0.51/0.67 % User time : 0.301 s
% 0.51/0.67 % System time : 0.026 s
% 0.51/0.67 % Total time : 0.327 s
%------------------------------------------------------------------------------