%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS112+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:28:44 EDT 2024
% Result : Unsatisfiable 0.49s 0.70s
% Output : Refutation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS112+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n011.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 00:08:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.49/0.70 % Version: 1.5
% 0.49/0.70 % SZS status Unsatisfiable
% 0.49/0.70 % SZS output start CNFRefutation
% 0.49/0.70 fof(axiom_3,axiom,(![X]:(cp(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.49/0.70 fof(c76,plain,(![X]:((~cp(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.49/0.70 fof(c77,plain,((![X]:(~cp(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(shift_quantors,[status(thm)],[c76])).
% 0.49/0.70 fof(c78,plain,((![X39]:(~cp(X39)|(![X40]:~ra_Px1(X39,X40))))&(![X41]:((?[X42]:ra_Px1(X41,X42))|cp(X41)))),inference(variable_rename,[status(thm)],[c77])).
% 0.49/0.70 fof(c80,plain,(![X39]:(![X40]:(![X41]:((~cp(X39)|~ra_Px1(X39,X40))&(ra_Px1(X41,skolem0004(X41))|cp(X41)))))),inference(shift_quantors,[status(thm)],[fof(c79,plain,((![X39]:(~cp(X39)|(![X40]:~ra_Px1(X39,X40))))&(![X41]:(ra_Px1(X41,skolem0004(X41))|cp(X41)))),inference(skolemize,[status(esa)],[c78])).])).
% 0.49/0.70 cnf(c81,plain,~cp(X129)|~ra_Px1(X129,X128),inference(split_conjunct,[status(thm)],[c80])).
% 0.49/0.70 fof(axiom_5,axiom,(![X]:(ca_Ax2(X)<=>(cpxcomp(X)&(![Y]:(rinvF1(X,Y)=>ca_Vx3(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.49/0.70 fof(c59,plain,(![X]:((~ca_Ax2(X)|(cpxcomp(X)&(![Y]:(~rinvF1(X,Y)|ca_Vx3(Y)))))&((~cpxcomp(X)|(?[Y]:(rinvF1(X,Y)&~ca_Vx3(Y))))|ca_Ax2(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.49/0.70 fof(c60,plain,((![X]:(~ca_Ax2(X)|(cpxcomp(X)&(![Y]:(~rinvF1(X,Y)|ca_Vx3(Y))))))&(![X]:((~cpxcomp(X)|(?[Y]:(rinvF1(X,Y)&~ca_Vx3(Y))))|ca_Ax2(X)))),inference(shift_quantors,[status(thm)],[c59])).
% 0.49/0.70 fof(c61,plain,((![X31]:(~ca_Ax2(X31)|(cpxcomp(X31)&(![X32]:(~rinvF1(X31,X32)|ca_Vx3(X32))))))&(![X33]:((~cpxcomp(X33)|(?[X34]:(rinvF1(X33,X34)&~ca_Vx3(X34))))|ca_Ax2(X33)))),inference(variable_rename,[status(thm)],[c60])).
% 0.49/0.70 fof(c63,plain,(![X31]:(![X32]:(![X33]:((~ca_Ax2(X31)|(cpxcomp(X31)&(~rinvF1(X31,X32)|ca_Vx3(X32))))&((~cpxcomp(X33)|(rinvF1(X33,skolem0002(X33))&~ca_Vx3(skolem0002(X33))))|ca_Ax2(X33)))))),inference(shift_quantors,[status(thm)],[fof(c62,plain,((![X31]:(~ca_Ax2(X31)|(cpxcomp(X31)&(![X32]:(~rinvF1(X31,X32)|ca_Vx3(X32))))))&(![X33]:((~cpxcomp(X33)|(rinvF1(X33,skolem0002(X33))&~ca_Vx3(skolem0002(X33))))|ca_Ax2(X33)))),inference(skolemize,[status(esa)],[c61])).])).
% 0.49/0.70 fof(c64,plain,(![X31]:(![X32]:(![X33]:(((~ca_Ax2(X31)|cpxcomp(X31))&(~ca_Ax2(X31)|(~rinvF1(X31,X32)|ca_Vx3(X32))))&(((~cpxcomp(X33)|rinvF1(X33,skolem0002(X33)))|ca_Ax2(X33))&((~cpxcomp(X33)|~ca_Vx3(skolem0002(X33)))|ca_Ax2(X33))))))),inference(distribute,[status(thm)],[c63])).
% 0.49/0.70 cnf(c65,plain,~ca_Ax2(X116)|cpxcomp(X116),inference(split_conjunct,[status(thm)],[c64])).
% 0.49/0.70 fof(axiom_13,axiom,cUnsatisfiable(i2003_11_14_17_21_19256),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_13)).
% 0.49/0.70 cnf(c22,plain,cUnsatisfiable(i2003_11_14_17_21_19256),inference(split_conjunct,[status(thm)],[axiom_13])).
% 0.49/0.70 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((?[Y]:(rf1(X,Y)&ca_Ax2(Y)))&(?[Y]:(rf(X,Y)&cp(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.49/0.70 fof(c83,plain,(![X]:((~cUnsatisfiable(X)|((?[Y]:(rf1(X,Y)&ca_Ax2(Y)))&(?[Y]:(rf(X,Y)&cp(Y)))))&(((![Y]:(~rf1(X,Y)|~ca_Ax2(Y)))|(![Y]:(~rf(X,Y)|~cp(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.49/0.70 fof(c84,plain,((![X]:(~cUnsatisfiable(X)|((?[Y]:(rf1(X,Y)&ca_Ax2(Y)))&(?[Y]:(rf(X,Y)&cp(Y))))))&(![X]:(((![Y]:(~rf1(X,Y)|~ca_Ax2(Y)))|(![Y]:(~rf(X,Y)|~cp(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c83])).
% 0.49/0.70 fof(c85,plain,((![X43]:(~cUnsatisfiable(X43)|((?[X44]:(rf1(X43,X44)&ca_Ax2(X44)))&(?[X45]:(rf(X43,X45)&cp(X45))))))&(![X46]:(((![X47]:(~rf1(X46,X47)|~ca_Ax2(X47)))|(![X48]:(~rf(X46,X48)|~cp(X48))))|cUnsatisfiable(X46)))),inference(variable_rename,[status(thm)],[c84])).
% 0.49/0.70 fof(c87,plain,(![X43]:(![X46]:(![X47]:(![X48]:((~cUnsatisfiable(X43)|((rf1(X43,skolem0005(X43))&ca_Ax2(skolem0005(X43)))&(rf(X43,skolem0006(X43))&cp(skolem0006(X43)))))&(((~rf1(X46,X47)|~ca_Ax2(X47))|(~rf(X46,X48)|~cp(X48)))|cUnsatisfiable(X46))))))),inference(shift_quantors,[status(thm)],[fof(c86,plain,((![X43]:(~cUnsatisfiable(X43)|((rf1(X43,skolem0005(X43))&ca_Ax2(skolem0005(X43)))&(rf(X43,skolem0006(X43))&cp(skolem0006(X43))))))&(![X46]:(((![X47]:(~rf1(X46,X47)|~ca_Ax2(X47)))|(![X48]:(~rf(X46,X48)|~cp(X48))))|cUnsatisfiable(X46)))),inference(skolemize,[status(esa)],[c85])).])).
% 0.49/0.70 fof(c88,plain,(![X43]:(![X46]:(![X47]:(![X48]:((((~cUnsatisfiable(X43)|rf1(X43,skolem0005(X43)))&(~cUnsatisfiable(X43)|ca_Ax2(skolem0005(X43))))&((~cUnsatisfiable(X43)|rf(X43,skolem0006(X43)))&(~cUnsatisfiable(X43)|cp(skolem0006(X43)))))&(((~rf1(X46,X47)|~ca_Ax2(X47))|(~rf(X46,X48)|~cp(X48)))|cUnsatisfiable(X46))))))),inference(distribute,[status(thm)],[c87])).
% 0.49/0.70 cnf(c90,plain,~cUnsatisfiable(X153)|ca_Ax2(skolem0005(X153)),inference(split_conjunct,[status(thm)],[c88])).
% 0.49/0.70 cnf(c182,plain,ca_Ax2(skolem0005(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c90, c22])).
% 0.49/0.70 cnf(c183,plain,cpxcomp(skolem0005(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c182, c65])).
% 0.49/0.70 fof(axiom_4,axiom,(![X]:(cpxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.49/0.70 fof(c69,plain,(![X]:((~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.49/0.70 fof(c70,plain,((![X]:(~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(shift_quantors,[status(thm)],[c69])).
% 0.49/0.70 fof(c71,plain,((![X35]:(~cpxcomp(X35)|(?[X36]:ra_Px1(X35,X36))))&(![X37]:((![X38]:~ra_Px1(X37,X38))|cpxcomp(X37)))),inference(variable_rename,[status(thm)],[c70])).
% 0.49/0.70 fof(c73,plain,(![X35]:(![X37]:(![X38]:((~cpxcomp(X35)|ra_Px1(X35,skolem0003(X35)))&(~ra_Px1(X37,X38)|cpxcomp(X37)))))),inference(shift_quantors,[status(thm)],[fof(c72,plain,((![X35]:(~cpxcomp(X35)|ra_Px1(X35,skolem0003(X35))))&(![X37]:((![X38]:~ra_Px1(X37,X38))|cpxcomp(X37)))),inference(skolemize,[status(esa)],[c71])).])).
% 0.49/0.70 cnf(c74,plain,~cpxcomp(X164)|ra_Px1(X164,skolem0003(X164)),inference(split_conjunct,[status(thm)],[c73])).
% 0.49/0.70 cnf(c186,plain,ra_Px1(skolem0005(i2003_11_14_17_21_19256),skolem0003(skolem0005(i2003_11_14_17_21_19256))),inference(resolution,[status(thm)],[c74, c183])).
% 0.49/0.70 cnf(c263,plain,~cp(skolem0005(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c186, c81])).
% 0.49/0.70 cnf(c5,axiom,X172!=X173|~cp(X172)|cp(X173),theory(equality)).
% 0.49/0.70 cnf(symmetry,axiom,X118!=X117|X117=X118,theory(equality)).
% 0.49/0.70 cnf(c89,plain,~cUnsatisfiable(X170)|rf1(X170,skolem0005(X170)),inference(split_conjunct,[status(thm)],[c88])).
% 0.49/0.70 cnf(c190,plain,rf1(i2003_11_14_17_21_19256,skolem0005(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c89, c22])).
% 0.49/0.70 fof(axiom_15,axiom,(![X]:(![Y]:(rs(X,Y)=>rf1(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_15)).
% 0.49/0.70 fof(c16,plain,(![X]:(![Y]:(~rs(X,Y)|rf1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_15])).
% 0.49/0.70 fof(c17,plain,(![X2]:(![X3]:(~rs(X2,X3)|rf1(X2,X3)))),inference(variable_rename,[status(thm)],[c16])).
% 0.49/0.70 cnf(c18,plain,~rs(X131,X130)|rf1(X131,X130),inference(split_conjunct,[status(thm)],[c17])).
% 0.49/0.70 fof(axiom_6,axiom,(![X]:(ca_Vx3(X)<=>(?[Y]:(rs(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.49/0.70 fof(c50,plain,(![X]:((~ca_Vx3(X)|(?[Y]:(rs(X,Y)&cowlThing(Y))))&((![Y]:(~rs(X,Y)|~cowlThing(Y)))|ca_Vx3(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.49/0.70 fof(c51,plain,((![X]:(~ca_Vx3(X)|(?[Y]:(rs(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~rs(X,Y)|~cowlThing(Y)))|ca_Vx3(X)))),inference(shift_quantors,[status(thm)],[c50])).
% 0.49/0.70 fof(c52,plain,((![X27]:(~ca_Vx3(X27)|(?[X28]:(rs(X27,X28)&cowlThing(X28)))))&(![X29]:((![X30]:(~rs(X29,X30)|~cowlThing(X30)))|ca_Vx3(X29)))),inference(variable_rename,[status(thm)],[c51])).
% 0.49/0.70 fof(c54,plain,(![X27]:(![X29]:(![X30]:((~ca_Vx3(X27)|(rs(X27,skolem0001(X27))&cowlThing(skolem0001(X27))))&((~rs(X29,X30)|~cowlThing(X30))|ca_Vx3(X29)))))),inference(shift_quantors,[status(thm)],[fof(c53,plain,((![X27]:(~ca_Vx3(X27)|(rs(X27,skolem0001(X27))&cowlThing(skolem0001(X27)))))&(![X29]:((![X30]:(~rs(X29,X30)|~cowlThing(X30)))|ca_Vx3(X29)))),inference(skolemize,[status(esa)],[c52])).])).
% 0.49/0.70 fof(c55,plain,(![X27]:(![X29]:(![X30]:(((~ca_Vx3(X27)|rs(X27,skolem0001(X27)))&(~ca_Vx3(X27)|cowlThing(skolem0001(X27))))&((~rs(X29,X30)|~cowlThing(X30))|ca_Vx3(X29)))))),inference(distribute,[status(thm)],[c54])).
% 0.49/0.70 cnf(c56,plain,~ca_Vx3(X163)|rs(X163,skolem0001(X163)),inference(split_conjunct,[status(thm)],[c55])).
% 0.49/0.70 fof(axiom_10,axiom,(![X]:(![Y]:(rinvF1(X,Y)<=>rf1(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_10)).
% 0.49/0.70 fof(c32,plain,(![X]:(![Y]:((~rinvF1(X,Y)|rf1(Y,X))&(~rf1(Y,X)|rinvF1(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.49/0.70 fof(c33,plain,((![X]:(![Y]:(~rinvF1(X,Y)|rf1(Y,X))))&(![X]:(![Y]:(~rf1(Y,X)|rinvF1(X,Y))))),inference(shift_quantors,[status(thm)],[c32])).
% 0.49/0.70 fof(c35,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~rinvF1(X13,X14)|rf1(X14,X13))&(~rf1(X16,X15)|rinvF1(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c34,plain,((![X13]:(![X14]:(~rinvF1(X13,X14)|rf1(X14,X13))))&(![X15]:(![X16]:(~rf1(X16,X15)|rinvF1(X15,X16))))),inference(variable_rename,[status(thm)],[c33])).])).
% 0.49/0.70 cnf(c37,plain,~rf1(X143,X144)|rinvF1(X144,X143),inference(split_conjunct,[status(thm)],[c35])).
% 0.49/0.70 cnf(c191,plain,rinvF1(skolem0005(i2003_11_14_17_21_19256),i2003_11_14_17_21_19256),inference(resolution,[status(thm)],[c190, c37])).
% 0.49/0.70 cnf(c66,plain,~ca_Ax2(X194)|~rinvF1(X194,X193)|ca_Vx3(X193),inference(split_conjunct,[status(thm)],[c64])).
% 0.49/0.70 cnf(c204,plain,~ca_Ax2(skolem0005(i2003_11_14_17_21_19256))|ca_Vx3(i2003_11_14_17_21_19256),inference(resolution,[status(thm)],[c66, c191])).
% 0.49/0.70 cnf(c207,plain,ca_Vx3(i2003_11_14_17_21_19256),inference(resolution,[status(thm)],[c204, c182])).
% 0.49/0.70 cnf(c208,plain,rs(i2003_11_14_17_21_19256,skolem0001(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c207, c56])).
% 0.49/0.70 cnf(c210,plain,rf1(i2003_11_14_17_21_19256,skolem0001(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c208, c18])).
% 0.49/0.70 fof(axiom_8,axiom,(![X]:(![Y]:(![Z]:((rf1(X,Y)&rf1(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.49/0.70 fof(c44,plain,(![X]:(![Y]:(![Z]:((~rf1(X,Y)|~rf1(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.49/0.70 fof(c45,plain,(![X21]:(![X22]:(![X23]:((~rf1(X21,X22)|~rf1(X21,X23))|X22=X23)))),inference(variable_rename,[status(thm)],[c44])).
% 0.49/0.70 cnf(c46,plain,~rf1(X239,X241)|~rf1(X239,X240)|X241=X240,inference(split_conjunct,[status(thm)],[c45])).
% 0.49/0.70 cnf(c229,plain,~rf1(i2003_11_14_17_21_19256,X303)|X303=skolem0001(i2003_11_14_17_21_19256),inference(resolution,[status(thm)],[c46, c210])).
% 0.49/0.70 cnf(c274,plain,skolem0005(i2003_11_14_17_21_19256)=skolem0001(i2003_11_14_17_21_19256),inference(resolution,[status(thm)],[c229, c190])).
% 0.49/0.70 cnf(c282,plain,skolem0001(i2003_11_14_17_21_19256)=skolem0005(i2003_11_14_17_21_19256),inference(resolution,[status(thm)],[c274, symmetry])).
% 0.49/0.70 cnf(c285,plain,~cp(skolem0001(i2003_11_14_17_21_19256))|cp(skolem0005(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c282, c5])).
% 0.49/0.70 cnf(c92,plain,~cUnsatisfiable(X157)|cp(skolem0006(X157)),inference(split_conjunct,[status(thm)],[c88])).
% 0.49/0.70 cnf(c185,plain,cp(skolem0006(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c92, c22])).
% 0.49/0.70 fof(axiom_14,axiom,(![X]:(![Y]:(rs(X,Y)=>rf(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_14)).
% 0.49/0.70 fof(c19,plain,(![X]:(![Y]:(~rs(X,Y)|rf(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_14])).
% 0.49/0.70 fof(c20,plain,(![X4]:(![X5]:(~rs(X4,X5)|rf(X4,X5)))),inference(variable_rename,[status(thm)],[c19])).
% 0.49/0.70 cnf(c21,plain,~rs(X132,X133)|rf(X132,X133),inference(split_conjunct,[status(thm)],[c20])).
% 0.49/0.70 cnf(c213,plain,rf(i2003_11_14_17_21_19256,skolem0001(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c208, c21])).
% 0.49/0.70 cnf(c91,plain,~cUnsatisfiable(X171)|rf(X171,skolem0006(X171)),inference(split_conjunct,[status(thm)],[c88])).
% 0.49/0.70 cnf(c193,plain,rf(i2003_11_14_17_21_19256,skolem0006(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c91, c22])).
% 0.49/0.70 fof(axiom_7,axiom,(![X]:(![Y]:(![Z]:((rf(X,Y)&rf(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.49/0.70 fof(c47,plain,(![X]:(![Y]:(![Z]:((~rf(X,Y)|~rf(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.49/0.70 fof(c48,plain,(![X24]:(![X25]:(![X26]:((~rf(X24,X25)|~rf(X24,X26))|X25=X26)))),inference(variable_rename,[status(thm)],[c47])).
% 0.49/0.70 cnf(c49,plain,~rf(X248,X250)|~rf(X248,X249)|X250=X249,inference(split_conjunct,[status(thm)],[c48])).
% 0.49/0.70 cnf(c233,plain,~rf(i2003_11_14_17_21_19256,X310)|X310=skolem0006(i2003_11_14_17_21_19256),inference(resolution,[status(thm)],[c49, c193])).
% 0.49/0.70 cnf(c298,plain,skolem0001(i2003_11_14_17_21_19256)=skolem0006(i2003_11_14_17_21_19256),inference(resolution,[status(thm)],[c233, c213])).
% 0.49/0.70 cnf(c306,plain,skolem0006(i2003_11_14_17_21_19256)=skolem0001(i2003_11_14_17_21_19256),inference(resolution,[status(thm)],[c298, symmetry])).
% 0.49/0.70 cnf(c308,plain,~cp(skolem0006(i2003_11_14_17_21_19256))|cp(skolem0001(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c306, c5])).
% 0.49/0.70 cnf(c514,plain,cp(skolem0001(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c308, c185])).
% 0.49/0.70 cnf(c518,plain,cp(skolem0005(i2003_11_14_17_21_19256)),inference(resolution,[status(thm)],[c514, c285])).
% 0.49/0.70 cnf(c519,plain,$false,inference(resolution,[status(thm)],[c518, c263])).
% 0.49/0.70 % SZS output end CNFRefutation
% 0.49/0.70
% 0.49/0.70 % Initial clauses : 74
% 0.49/0.70 % Processed clauses : 165
% 0.49/0.70 % Factors computed : 4
% 0.49/0.70 % Resolvents computed: 340
% 0.49/0.70 % Tautologies deleted: 12
% 0.49/0.70 % Forward subsumed : 106
% 0.49/0.70 % Backward subsumed : 7
% 0.49/0.70 % -------- CPU Time ---------
% 0.49/0.70 % User time : 0.328 s
% 0.49/0.70 % System time : 0.012 s
% 0.49/0.70 % Total time : 0.340 s
%------------------------------------------------------------------------------