%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS120+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:45 EDT 2024
% Result : Unsatisfiable 0.43s 0.59s
% Output : Refutation 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : KRS120+1 : TPTP v8.1.2. Released v3.1.0.
% 0.00/0.09 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Thu May 9 00:15:37 EDT 2024
% 0.13/0.28 % CPUTime :
% 0.43/0.59 % Version: 1.5
% 0.43/0.59 % SZS status Unsatisfiable
% 0.43/0.59 % SZS output start CNFRefutation
% 0.43/0.59 fof(axiom_3,axiom,(![X]:(cp1(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.43/0.59 fof(c60,plain,(![X]:((~cp1(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cp1(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.43/0.59 fof(c61,plain,((![X]:(~cp1(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cp1(X)))),inference(shift_quantors,[status(thm)],[c60])).
% 0.43/0.59 fof(c62,plain,((![X28]:(~cp1(X28)|(![X29]:~ra_Px1(X28,X29))))&(![X30]:((?[X31]:ra_Px1(X30,X31))|cp1(X30)))),inference(variable_rename,[status(thm)],[c61])).
% 0.43/0.59 fof(c64,plain,(![X28]:(![X29]:(![X30]:((~cp1(X28)|~ra_Px1(X28,X29))&(ra_Px1(X30,skolem0004(X30))|cp1(X30)))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,((![X28]:(~cp1(X28)|(![X29]:~ra_Px1(X28,X29))))&(![X30]:(ra_Px1(X30,skolem0004(X30))|cp1(X30)))),inference(skolemize,[status(esa)],[c62])).])).
% 0.43/0.59 cnf(c65,plain,~cp1(X104)|~ra_Px1(X104,X103),inference(split_conjunct,[status(thm)],[c64])).
% 0.43/0.59 fof(axiom_4,axiom,(![X]:(cp1xcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.43/0.59 fof(c53,plain,(![X]:((~cp1xcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cp1xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.43/0.59 fof(c54,plain,((![X]:(~cp1xcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cp1xcomp(X)))),inference(shift_quantors,[status(thm)],[c53])).
% 0.43/0.59 fof(c55,plain,((![X24]:(~cp1xcomp(X24)|(?[X25]:ra_Px1(X24,X25))))&(![X26]:((![X27]:~ra_Px1(X26,X27))|cp1xcomp(X26)))),inference(variable_rename,[status(thm)],[c54])).
% 0.43/0.59 fof(c57,plain,(![X24]:(![X26]:(![X27]:((~cp1xcomp(X24)|ra_Px1(X24,skolem0003(X24)))&(~ra_Px1(X26,X27)|cp1xcomp(X26)))))),inference(shift_quantors,[status(thm)],[fof(c56,plain,((![X24]:(~cp1xcomp(X24)|ra_Px1(X24,skolem0003(X24))))&(![X26]:((![X27]:~ra_Px1(X26,X27))|cp1xcomp(X26)))),inference(skolemize,[status(esa)],[c55])).])).
% 0.43/0.59 cnf(c58,plain,~cp1xcomp(X130)|ra_Px1(X130,skolem0003(X130)),inference(split_conjunct,[status(thm)],[c57])).
% 0.43/0.59 fof(axiom_6,axiom,(![X]:(ca_Vx3(X)<=>(?[Y]:(rf(X,Y)&cp1xcomp(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.43/0.59 fof(c34,plain,(![X]:((~ca_Vx3(X)|(?[Y]:(rf(X,Y)&cp1xcomp(Y))))&((![Y]:(~rf(X,Y)|~cp1xcomp(Y)))|ca_Vx3(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.43/0.59 fof(c35,plain,((![X]:(~ca_Vx3(X)|(?[Y]:(rf(X,Y)&cp1xcomp(Y)))))&(![X]:((![Y]:(~rf(X,Y)|~cp1xcomp(Y)))|ca_Vx3(X)))),inference(shift_quantors,[status(thm)],[c34])).
% 0.43/0.59 fof(c36,plain,((![X16]:(~ca_Vx3(X16)|(?[X17]:(rf(X16,X17)&cp1xcomp(X17)))))&(![X18]:((![X19]:(~rf(X18,X19)|~cp1xcomp(X19)))|ca_Vx3(X18)))),inference(variable_rename,[status(thm)],[c35])).
% 0.43/0.59 fof(c38,plain,(![X16]:(![X18]:(![X19]:((~ca_Vx3(X16)|(rf(X16,skolem0001(X16))&cp1xcomp(skolem0001(X16))))&((~rf(X18,X19)|~cp1xcomp(X19))|ca_Vx3(X18)))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,((![X16]:(~ca_Vx3(X16)|(rf(X16,skolem0001(X16))&cp1xcomp(skolem0001(X16)))))&(![X18]:((![X19]:(~rf(X18,X19)|~cp1xcomp(X19)))|ca_Vx3(X18)))),inference(skolemize,[status(esa)],[c36])).])).
% 0.43/0.59 fof(c39,plain,(![X16]:(![X18]:(![X19]:(((~ca_Vx3(X16)|rf(X16,skolem0001(X16)))&(~ca_Vx3(X16)|cp1xcomp(skolem0001(X16))))&((~rf(X18,X19)|~cp1xcomp(X19))|ca_Vx3(X18)))))),inference(distribute,[status(thm)],[c38])).
% 0.43/0.59 cnf(c41,plain,~ca_Vx3(X116)|cp1xcomp(skolem0001(X116)),inference(split_conjunct,[status(thm)],[c39])).
% 0.43/0.59 fof(axiom_5,axiom,(![X]:(ca_Ax2(X)<=>((?[Y]:(rinvF(X,Y)&ca_Vx3(Y)))&cp1(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.43/0.59 fof(c43,plain,(![X]:((~ca_Ax2(X)|((?[Y]:(rinvF(X,Y)&ca_Vx3(Y)))&cp1(X)))&(((![Y]:(~rinvF(X,Y)|~ca_Vx3(Y)))|~cp1(X))|ca_Ax2(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.43/0.59 fof(c44,plain,((![X]:(~ca_Ax2(X)|((?[Y]:(rinvF(X,Y)&ca_Vx3(Y)))&cp1(X))))&(![X]:(((![Y]:(~rinvF(X,Y)|~ca_Vx3(Y)))|~cp1(X))|ca_Ax2(X)))),inference(shift_quantors,[status(thm)],[c43])).
% 0.43/0.59 fof(c45,plain,((![X20]:(~ca_Ax2(X20)|((?[X21]:(rinvF(X20,X21)&ca_Vx3(X21)))&cp1(X20))))&(![X22]:(((![X23]:(~rinvF(X22,X23)|~ca_Vx3(X23)))|~cp1(X22))|ca_Ax2(X22)))),inference(variable_rename,[status(thm)],[c44])).
% 0.43/0.59 fof(c47,plain,(![X20]:(![X22]:(![X23]:((~ca_Ax2(X20)|((rinvF(X20,skolem0002(X20))&ca_Vx3(skolem0002(X20)))&cp1(X20)))&(((~rinvF(X22,X23)|~ca_Vx3(X23))|~cp1(X22))|ca_Ax2(X22)))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X20]:(~ca_Ax2(X20)|((rinvF(X20,skolem0002(X20))&ca_Vx3(skolem0002(X20)))&cp1(X20))))&(![X22]:(((![X23]:(~rinvF(X22,X23)|~ca_Vx3(X23)))|~cp1(X22))|ca_Ax2(X22)))),inference(skolemize,[status(esa)],[c45])).])).
% 0.43/0.59 fof(c48,plain,(![X20]:(![X22]:(![X23]:((((~ca_Ax2(X20)|rinvF(X20,skolem0002(X20)))&(~ca_Ax2(X20)|ca_Vx3(skolem0002(X20))))&(~ca_Ax2(X20)|cp1(X20)))&(((~rinvF(X22,X23)|~ca_Vx3(X23))|~cp1(X22))|ca_Ax2(X22)))))),inference(distribute,[status(thm)],[c47])).
% 0.43/0.59 cnf(c50,plain,~ca_Ax2(X117)|ca_Vx3(skolem0002(X117)),inference(split_conjunct,[status(thm)],[c48])).
% 0.43/0.59 fof(axiom_11,axiom,cUnsatisfiable(i2003_11_14_17_21_48796),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_11)).
% 0.43/0.59 cnf(c14,plain,cUnsatisfiable(i2003_11_14_17_21_48796),inference(split_conjunct,[status(thm)],[axiom_11])).
% 0.43/0.59 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(?[Y]:(rf(X,Y)&ca_Ax2(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.43/0.59 fof(c67,plain,(![X]:((~cUnsatisfiable(X)|(?[Y]:(rf(X,Y)&ca_Ax2(Y))))&((![Y]:(~rf(X,Y)|~ca_Ax2(Y)))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.43/0.59 fof(c68,plain,((![X]:(~cUnsatisfiable(X)|(?[Y]:(rf(X,Y)&ca_Ax2(Y)))))&(![X]:((![Y]:(~rf(X,Y)|~ca_Ax2(Y)))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c67])).
% 0.43/0.59 fof(c69,plain,((![X32]:(~cUnsatisfiable(X32)|(?[X33]:(rf(X32,X33)&ca_Ax2(X33)))))&(![X34]:((![X35]:(~rf(X34,X35)|~ca_Ax2(X35)))|cUnsatisfiable(X34)))),inference(variable_rename,[status(thm)],[c68])).
% 0.43/0.59 fof(c71,plain,(![X32]:(![X34]:(![X35]:((~cUnsatisfiable(X32)|(rf(X32,skolem0005(X32))&ca_Ax2(skolem0005(X32))))&((~rf(X34,X35)|~ca_Ax2(X35))|cUnsatisfiable(X34)))))),inference(shift_quantors,[status(thm)],[fof(c70,plain,((![X32]:(~cUnsatisfiable(X32)|(rf(X32,skolem0005(X32))&ca_Ax2(skolem0005(X32)))))&(![X34]:((![X35]:(~rf(X34,X35)|~ca_Ax2(X35)))|cUnsatisfiable(X34)))),inference(skolemize,[status(esa)],[c69])).])).
% 0.43/0.59 fof(c72,plain,(![X32]:(![X34]:(![X35]:(((~cUnsatisfiable(X32)|rf(X32,skolem0005(X32)))&(~cUnsatisfiable(X32)|ca_Ax2(skolem0005(X32))))&((~rf(X34,X35)|~ca_Ax2(X35))|cUnsatisfiable(X34)))))),inference(distribute,[status(thm)],[c71])).
% 0.43/0.59 cnf(c74,plain,~cUnsatisfiable(X118)|ca_Ax2(skolem0005(X118)),inference(split_conjunct,[status(thm)],[c72])).
% 0.43/0.59 cnf(c151,plain,ca_Ax2(skolem0005(i2003_11_14_17_21_48796)),inference(resolution,[status(thm)],[c74, c14])).
% 0.43/0.59 cnf(c153,plain,ca_Vx3(skolem0002(skolem0005(i2003_11_14_17_21_48796))),inference(resolution,[status(thm)],[c151, c50])).
% 0.43/0.59 cnf(c155,plain,cp1xcomp(skolem0001(skolem0002(skolem0005(i2003_11_14_17_21_48796)))),inference(resolution,[status(thm)],[c153, c41])).
% 0.43/0.59 cnf(c42,plain,~rf(X159,X158)|~cp1xcomp(X158)|ca_Vx3(X159),inference(split_conjunct,[status(thm)],[c39])).
% 0.43/0.59 cnf(c73,plain,~cUnsatisfiable(X136)|rf(X136,skolem0005(X136)),inference(split_conjunct,[status(thm)],[c72])).
% 0.43/0.59 cnf(c162,plain,rf(i2003_11_14_17_21_48796,skolem0005(i2003_11_14_17_21_48796)),inference(resolution,[status(thm)],[c73, c14])).
% 0.43/0.59 fof(rf_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rf(C,A))=>rf(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rf_substitution_2)).
% 0.43/0.59 fof(c113,plain,(![A]:(![B]:(![C]:((A!=B|~rf(C,A))|rf(C,B))))),inference(fof_nnf,[status(thm)],[rf_substitution_2])).
% 0.43/0.59 fof(c114,plain,(![X62]:(![X63]:(![X64]:((X62!=X63|~rf(X64,X62))|rf(X64,X63))))),inference(variable_rename,[status(thm)],[c113])).
% 0.43/0.59 cnf(c115,plain,X219!=X218|~rf(X220,X219)|rf(X220,X218),inference(split_conjunct,[status(thm)],[c114])).
% 0.43/0.59 cnf(c182,plain,skolem0005(i2003_11_14_17_21_48796)!=X239|rf(i2003_11_14_17_21_48796,X239),inference(resolution,[status(thm)],[c115, c162])).
% 0.43/0.59 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.43/0.59 fof(c83,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.43/0.60 fof(c84,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c83])).
% 0.43/0.60 fof(c86,plain,(![X38]:(![X39]:(cowlThing(X38)&~cowlNothing(X39)))),inference(shift_quantors,[status(thm)],[fof(c85,plain,((![X38]:cowlThing(X38))&(![X39]:~cowlNothing(X39))),inference(variable_rename,[status(thm)],[c84])).])).
% 0.43/0.60 cnf(c87,plain,cowlThing(X88),inference(split_conjunct,[status(thm)],[c86])).
% 0.43/0.60 fof(axiom_8,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.43/0.60 fof(c24,plain,(![X]:(![Y]:((~rinvF(X,Y)|rf(Y,X))&(~rf(Y,X)|rinvF(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.43/0.60 fof(c25,plain,((![X]:(![Y]:(~rinvF(X,Y)|rf(Y,X))))&(![X]:(![Y]:(~rf(Y,X)|rinvF(X,Y))))),inference(shift_quantors,[status(thm)],[c24])).
% 0.43/0.60 fof(c27,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~rinvF(X9,X10)|rf(X10,X9))&(~rf(X12,X11)|rinvF(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,((![X9]:(![X10]:(~rinvF(X9,X10)|rf(X10,X9))))&(![X11]:(![X12]:(~rf(X12,X11)|rinvF(X11,X12))))),inference(variable_rename,[status(thm)],[c25])).])).
% 0.43/0.60 cnf(c28,plain,~rinvF(X109,X110)|rf(X110,X109),inference(split_conjunct,[status(thm)],[c27])).
% 0.43/0.60 cnf(c49,plain,~ca_Ax2(X129)|rinvF(X129,skolem0002(X129)),inference(split_conjunct,[status(thm)],[c48])).
% 0.43/0.60 cnf(c158,plain,rinvF(skolem0005(i2003_11_14_17_21_48796),skolem0002(skolem0005(i2003_11_14_17_21_48796))),inference(resolution,[status(thm)],[c49, c151])).
% 0.43/0.60 cnf(c191,plain,rf(skolem0002(skolem0005(i2003_11_14_17_21_48796)),skolem0005(i2003_11_14_17_21_48796)),inference(resolution,[status(thm)],[c158, c28])).
% 0.43/0.60 fof(axiom_7,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf(X,Y0)&rf(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.43/0.60 fof(c30,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf(X,Y0)|~rf(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.43/0.60 fof(c32,plain,(![X13]:(![X14]:(![X15]:(~cowlThing(X13)|((~rf(X13,X14)|~rf(X13,X15))|X14=X15))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,(![X13]:(~cowlThing(X13)|(![X14]:(![X15]:((~rf(X13,X14)|~rf(X13,X15))|X14=X15))))),inference(variable_rename,[status(thm)],[c30])).])).
% 0.43/0.60 cnf(c33,plain,~cowlThing(X221)|~rf(X221,X223)|~rf(X221,X222)|X223=X222,inference(split_conjunct,[status(thm)],[c32])).
% 0.43/0.60 cnf(c40,plain,~ca_Vx3(X128)|rf(X128,skolem0001(X128)),inference(split_conjunct,[status(thm)],[c39])).
% 0.43/0.60 cnf(c157,plain,rf(skolem0002(skolem0005(i2003_11_14_17_21_48796)),skolem0001(skolem0002(skolem0005(i2003_11_14_17_21_48796)))),inference(resolution,[status(thm)],[c40, c153])).
% 0.43/0.60 cnf(c204,plain,~cowlThing(skolem0002(skolem0005(i2003_11_14_17_21_48796)))|~rf(skolem0002(skolem0005(i2003_11_14_17_21_48796)),X284)|X284=skolem0001(skolem0002(skolem0005(i2003_11_14_17_21_48796))),inference(resolution,[status(thm)],[c157, c33])).
% 0.43/0.60 cnf(c277,plain,~cowlThing(skolem0002(skolem0005(i2003_11_14_17_21_48796)))|skolem0005(i2003_11_14_17_21_48796)=skolem0001(skolem0002(skolem0005(i2003_11_14_17_21_48796))),inference(resolution,[status(thm)],[c204, c191])).
% 0.43/0.60 cnf(c311,plain,skolem0005(i2003_11_14_17_21_48796)=skolem0001(skolem0002(skolem0005(i2003_11_14_17_21_48796))),inference(resolution,[status(thm)],[c277, c87])).
% 0.43/0.60 cnf(c313,plain,rf(i2003_11_14_17_21_48796,skolem0001(skolem0002(skolem0005(i2003_11_14_17_21_48796)))),inference(resolution,[status(thm)],[c311, c182])).
% 0.43/0.60 cnf(c336,plain,~cp1xcomp(skolem0001(skolem0002(skolem0005(i2003_11_14_17_21_48796))))|ca_Vx3(i2003_11_14_17_21_48796),inference(resolution,[status(thm)],[c313, c42])).
% 0.43/0.60 cnf(c359,plain,ca_Vx3(i2003_11_14_17_21_48796),inference(resolution,[status(thm)],[c336, c155])).
% 0.43/0.60 cnf(c361,plain,cp1xcomp(skolem0001(i2003_11_14_17_21_48796)),inference(resolution,[status(thm)],[c359, c41])).
% 0.43/0.60 cnf(c363,plain,ra_Px1(skolem0001(i2003_11_14_17_21_48796),skolem0003(skolem0001(i2003_11_14_17_21_48796))),inference(resolution,[status(thm)],[c361, c58])).
% 0.43/0.60 cnf(c380,plain,~cp1(skolem0001(i2003_11_14_17_21_48796)),inference(resolution,[status(thm)],[c363, c65])).
% 0.43/0.60 cnf(c51,plain,~ca_Ax2(X91)|cp1(X91),inference(split_conjunct,[status(thm)],[c48])).
% 0.43/0.60 cnf(c152,plain,cp1(skolem0005(i2003_11_14_17_21_48796)),inference(resolution,[status(thm)],[c151, c51])).
% 0.43/0.60 cnf(c5,axiom,X143!=X142|~cp1(X143)|cp1(X142),theory(equality)).
% 0.43/0.60 cnf(symmetry,axiom,X92!=X93|X93=X92,theory(equality)).
% 0.43/0.60 cnf(c184,plain,~cowlThing(i2003_11_14_17_21_48796)|~rf(i2003_11_14_17_21_48796,X269)|X269=skolem0005(i2003_11_14_17_21_48796),inference(resolution,[status(thm)],[c33, c162])).
% 0.43/0.60 cnf(c362,plain,rf(i2003_11_14_17_21_48796,skolem0001(i2003_11_14_17_21_48796)),inference(resolution,[status(thm)],[c359, c40])).
% 0.43/0.60 cnf(c370,plain,~cowlThing(i2003_11_14_17_21_48796)|skolem0001(i2003_11_14_17_21_48796)=skolem0005(i2003_11_14_17_21_48796),inference(resolution,[status(thm)],[c362, c184])).
% 0.43/0.60 cnf(c400,plain,skolem0001(i2003_11_14_17_21_48796)=skolem0005(i2003_11_14_17_21_48796),inference(resolution,[status(thm)],[c370, c87])).
% 0.43/0.60 cnf(c413,plain,skolem0005(i2003_11_14_17_21_48796)=skolem0001(i2003_11_14_17_21_48796),inference(resolution,[status(thm)],[c400, symmetry])).
% 0.43/0.60 cnf(c421,plain,~cp1(skolem0005(i2003_11_14_17_21_48796))|cp1(skolem0001(i2003_11_14_17_21_48796)),inference(resolution,[status(thm)],[c413, c5])).
% 0.43/0.60 cnf(c449,plain,cp1(skolem0001(i2003_11_14_17_21_48796)),inference(resolution,[status(thm)],[c421, c152])).
% 0.43/0.60 cnf(c453,plain,$false,inference(resolution,[status(thm)],[c449, c380])).
% 0.43/0.60 % SZS output end CNFRefutation
% 0.43/0.60
% 0.43/0.60 % Initial clauses : 61
% 0.43/0.60 % Processed clauses : 147
% 0.43/0.60 % Factors computed : 3
% 0.43/0.60 % Resolvents computed: 305
% 0.43/0.60 % Tautologies deleted: 13
% 0.43/0.60 % Forward subsumed : 96
% 0.43/0.60 % Backward subsumed : 7
% 0.43/0.60 % -------- CPU Time ---------
% 0.43/0.60 % User time : 0.287 s
% 0.43/0.60 % System time : 0.011 s
% 0.43/0.60 % Total time : 0.298 s
%------------------------------------------------------------------------------