%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS114+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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.61s 0.77s
% Output : Refutation 0.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS114+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n020.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 00:06:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.61/0.77 % Version: 1.5
% 0.61/0.77 % SZS status Unsatisfiable
% 0.61/0.77 % SZS output start CNFRefutation
% 0.61/0.77 fof(axiom_3,axiom,(![X]:(cp(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.61/0.77 fof(c74,plain,(![X]:((~cp(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.61/0.77 fof(c75,plain,((![X]:(~cp(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(shift_quantors,[status(thm)],[c74])).
% 0.61/0.77 fof(c76,plain,((![X32]:(~cp(X32)|(![X33]:~ra_Px1(X32,X33))))&(![X34]:((?[X35]:ra_Px1(X34,X35))|cp(X34)))),inference(variable_rename,[status(thm)],[c75])).
% 0.61/0.77 fof(c78,plain,(![X32]:(![X33]:(![X34]:((~cp(X32)|~ra_Px1(X32,X33))&(ra_Px1(X34,skolem0008(X34))|cp(X34)))))),inference(shift_quantors,[status(thm)],[fof(c77,plain,((![X32]:(~cp(X32)|(![X33]:~ra_Px1(X32,X33))))&(![X34]:(ra_Px1(X34,skolem0008(X34))|cp(X34)))),inference(skolemize,[status(esa)],[c76])).])).
% 0.61/0.77 cnf(c79,plain,~cp(X121)|~ra_Px1(X121,X120),inference(split_conjunct,[status(thm)],[c78])).
% 0.61/0.77 fof(axiom_4,axiom,(![X]:(cpxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.61/0.77 fof(c67,plain,(![X]:((~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.61/0.77 fof(c68,plain,((![X]:(~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(shift_quantors,[status(thm)],[c67])).
% 0.61/0.77 fof(c69,plain,((![X28]:(~cpxcomp(X28)|(?[X29]:ra_Px1(X28,X29))))&(![X30]:((![X31]:~ra_Px1(X30,X31))|cpxcomp(X30)))),inference(variable_rename,[status(thm)],[c68])).
% 0.61/0.77 fof(c71,plain,(![X28]:(![X30]:(![X31]:((~cpxcomp(X28)|ra_Px1(X28,skolem0007(X28)))&(~ra_Px1(X30,X31)|cpxcomp(X30)))))),inference(shift_quantors,[status(thm)],[fof(c70,plain,((![X28]:(~cpxcomp(X28)|ra_Px1(X28,skolem0007(X28))))&(![X30]:((![X31]:~ra_Px1(X30,X31))|cpxcomp(X30)))),inference(skolemize,[status(esa)],[c69])).])).
% 0.61/0.77 cnf(c72,plain,~cpxcomp(X154)|ra_Px1(X154,skolem0007(X154)),inference(split_conjunct,[status(thm)],[c71])).
% 0.61/0.77 fof(axiom_7,axiom,(![X]:(ca_Ax3(X)<=>(cqxcomp(X)&cpxcomp(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.61/0.77 fof(c45,plain,(![X]:((~ca_Ax3(X)|(cqxcomp(X)&cpxcomp(X)))&((~cqxcomp(X)|~cpxcomp(X))|ca_Ax3(X)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.61/0.77 fof(c46,plain,((![X]:(~ca_Ax3(X)|(cqxcomp(X)&cpxcomp(X))))&(![X]:((~cqxcomp(X)|~cpxcomp(X))|ca_Ax3(X)))),inference(shift_quantors,[status(thm)],[c45])).
% 0.61/0.77 fof(c48,plain,(![X18]:(![X19]:((~ca_Ax3(X18)|(cqxcomp(X18)&cpxcomp(X18)))&((~cqxcomp(X19)|~cpxcomp(X19))|ca_Ax3(X19))))),inference(shift_quantors,[status(thm)],[fof(c47,plain,((![X18]:(~ca_Ax3(X18)|(cqxcomp(X18)&cpxcomp(X18))))&(![X19]:((~cqxcomp(X19)|~cpxcomp(X19))|ca_Ax3(X19)))),inference(variable_rename,[status(thm)],[c46])).])).
% 0.61/0.77 fof(c49,plain,(![X18]:(![X19]:(((~ca_Ax3(X18)|cqxcomp(X18))&(~ca_Ax3(X18)|cpxcomp(X18)))&((~cqxcomp(X19)|~cpxcomp(X19))|ca_Ax3(X19))))),inference(distribute,[status(thm)],[c48])).
% 0.61/0.77 cnf(c51,plain,~ca_Ax3(X107)|cpxcomp(X107),inference(split_conjunct,[status(thm)],[c49])).
% 0.61/0.77 fof(axiom_11,axiom,cUnsatisfiable(i2003_11_14_17_21_262),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_11)).
% 0.61/0.77 cnf(c17,plain,cUnsatisfiable(i2003_11_14_17_21_262),inference(split_conjunct,[status(thm)],[axiom_11])).
% 0.61/0.77 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((?[Y]:(rr(X,Y)&ca_Ax4(Y)))&(?[Y]:(rs(X,Y)&ca_Ax3(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.61/0.77 fof(c81,plain,(![X]:((~cUnsatisfiable(X)|((?[Y]:(rr(X,Y)&ca_Ax4(Y)))&(?[Y]:(rs(X,Y)&ca_Ax3(Y)))))&(((![Y]:(~rr(X,Y)|~ca_Ax4(Y)))|(![Y]:(~rs(X,Y)|~ca_Ax3(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.61/0.77 fof(c82,plain,((![X]:(~cUnsatisfiable(X)|((?[Y]:(rr(X,Y)&ca_Ax4(Y)))&(?[Y]:(rs(X,Y)&ca_Ax3(Y))))))&(![X]:(((![Y]:(~rr(X,Y)|~ca_Ax4(Y)))|(![Y]:(~rs(X,Y)|~ca_Ax3(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c81])).
% 0.61/0.77 fof(c83,plain,((![X36]:(~cUnsatisfiable(X36)|((?[X37]:(rr(X36,X37)&ca_Ax4(X37)))&(?[X38]:(rs(X36,X38)&ca_Ax3(X38))))))&(![X39]:(((![X40]:(~rr(X39,X40)|~ca_Ax4(X40)))|(![X41]:(~rs(X39,X41)|~ca_Ax3(X41))))|cUnsatisfiable(X39)))),inference(variable_rename,[status(thm)],[c82])).
% 0.61/0.77 fof(c85,plain,(![X36]:(![X39]:(![X40]:(![X41]:((~cUnsatisfiable(X36)|((rr(X36,skolem0009(X36))&ca_Ax4(skolem0009(X36)))&(rs(X36,skolem0010(X36))&ca_Ax3(skolem0010(X36)))))&(((~rr(X39,X40)|~ca_Ax4(X40))|(~rs(X39,X41)|~ca_Ax3(X41)))|cUnsatisfiable(X39))))))),inference(shift_quantors,[status(thm)],[fof(c84,plain,((![X36]:(~cUnsatisfiable(X36)|((rr(X36,skolem0009(X36))&ca_Ax4(skolem0009(X36)))&(rs(X36,skolem0010(X36))&ca_Ax3(skolem0010(X36))))))&(![X39]:(((![X40]:(~rr(X39,X40)|~ca_Ax4(X40)))|(![X41]:(~rs(X39,X41)|~ca_Ax3(X41))))|cUnsatisfiable(X39)))),inference(skolemize,[status(esa)],[c83])).])).
% 0.61/0.77 fof(c86,plain,(![X36]:(![X39]:(![X40]:(![X41]:((((~cUnsatisfiable(X36)|rr(X36,skolem0009(X36)))&(~cUnsatisfiable(X36)|ca_Ax4(skolem0009(X36))))&((~cUnsatisfiable(X36)|rs(X36,skolem0010(X36)))&(~cUnsatisfiable(X36)|ca_Ax3(skolem0010(X36)))))&(((~rr(X39,X40)|~ca_Ax4(X40))|(~rs(X39,X41)|~ca_Ax3(X41)))|cUnsatisfiable(X39))))))),inference(distribute,[status(thm)],[c85])).
% 0.61/0.77 cnf(c90,plain,~cUnsatisfiable(X135)|ca_Ax3(skolem0010(X135)),inference(split_conjunct,[status(thm)],[c86])).
% 0.61/0.77 cnf(c179,plain,ca_Ax3(skolem0010(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c90, c17])).
% 0.61/0.77 cnf(c180,plain,cpxcomp(skolem0010(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c179, c51])).
% 0.61/0.77 cnf(c189,plain,ra_Px1(skolem0010(i2003_11_14_17_21_262),skolem0007(skolem0010(i2003_11_14_17_21_262))),inference(resolution,[status(thm)],[c72, c180])).
% 0.61/0.77 cnf(c258,plain,~cp(skolem0010(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c189, c79])).
% 0.61/0.77 fof(axiom_9,axiom,(![X]:(ca_Vx5(X)<=>(![Y]:(rs(X,Y)=>cp(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.61/0.77 fof(c24,plain,(![X]:((~ca_Vx5(X)|(![Y]:(~rs(X,Y)|cp(Y))))&((?[Y]:(rs(X,Y)&~cp(Y)))|ca_Vx5(X)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.61/0.77 fof(c25,plain,((![X]:(~ca_Vx5(X)|(![Y]:(~rs(X,Y)|cp(Y)))))&(![X]:((?[Y]:(rs(X,Y)&~cp(Y)))|ca_Vx5(X)))),inference(shift_quantors,[status(thm)],[c24])).
% 0.61/0.77 fof(c26,plain,((![X6]:(~ca_Vx5(X6)|(![X7]:(~rs(X6,X7)|cp(X7)))))&(![X8]:((?[X9]:(rs(X8,X9)&~cp(X9)))|ca_Vx5(X8)))),inference(variable_rename,[status(thm)],[c25])).
% 0.61/0.77 fof(c28,plain,(![X6]:(![X7]:(![X8]:((~ca_Vx5(X6)|(~rs(X6,X7)|cp(X7)))&((rs(X8,skolem0001(X8))&~cp(skolem0001(X8)))|ca_Vx5(X8)))))),inference(shift_quantors,[status(thm)],[fof(c27,plain,((![X6]:(~ca_Vx5(X6)|(![X7]:(~rs(X6,X7)|cp(X7)))))&(![X8]:((rs(X8,skolem0001(X8))&~cp(skolem0001(X8)))|ca_Vx5(X8)))),inference(skolemize,[status(esa)],[c26])).])).
% 0.61/0.77 fof(c29,plain,(![X6]:(![X7]:(![X8]:((~ca_Vx5(X6)|(~rs(X6,X7)|cp(X7)))&((rs(X8,skolem0001(X8))|ca_Vx5(X8))&(~cp(skolem0001(X8))|ca_Vx5(X8))))))),inference(distribute,[status(thm)],[c28])).
% 0.61/0.77 cnf(c32,plain,~cp(skolem0001(X129))|ca_Vx5(X129),inference(split_conjunct,[status(thm)],[c29])).
% 0.61/0.77 cnf(c73,plain,~ra_Px1(X119,X118)|cpxcomp(X119),inference(split_conjunct,[status(thm)],[c71])).
% 0.61/0.77 cnf(c80,plain,ra_Px1(X155,skolem0008(X155))|cp(X155),inference(split_conjunct,[status(thm)],[c78])).
% 0.61/0.77 cnf(c190,plain,cp(X158)|cpxcomp(X158),inference(resolution,[status(thm)],[c80, c73])).
% 0.61/0.77 cnf(c193,plain,cpxcomp(skolem0001(X160))|ca_Vx5(X160),inference(resolution,[status(thm)],[c190, c32])).
% 0.61/0.77 cnf(c89,plain,~cUnsatisfiable(X165)|rs(X165,skolem0010(X165)),inference(split_conjunct,[status(thm)],[c86])).
% 0.61/0.77 cnf(c202,plain,rs(i2003_11_14_17_21_262,skolem0010(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c89, c17])).
% 0.61/0.77 cnf(c30,plain,~ca_Vx5(X195)|~rs(X195,X196)|cp(X196),inference(split_conjunct,[status(thm)],[c29])).
% 0.61/0.77 cnf(c224,plain,~ca_Vx5(i2003_11_14_17_21_262)|cp(skolem0010(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c30, c202])).
% 0.61/0.77 cnf(c229,plain,cp(skolem0010(i2003_11_14_17_21_262))|cpxcomp(skolem0001(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c224, c193])).
% 0.61/0.77 cnf(c287,plain,cpxcomp(skolem0001(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c229, c258])).
% 0.61/0.77 cnf(c290,plain,ra_Px1(skolem0001(i2003_11_14_17_21_262),skolem0007(skolem0001(i2003_11_14_17_21_262))),inference(resolution,[status(thm)],[c287, c72])).
% 0.61/0.77 cnf(c328,plain,~cp(skolem0001(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c290, c79])).
% 0.61/0.77 cnf(c31,plain,rs(X145,skolem0001(X145))|ca_Vx5(X145),inference(split_conjunct,[status(thm)],[c29])).
% 0.61/0.77 cnf(c230,plain,cp(skolem0010(i2003_11_14_17_21_262))|rs(i2003_11_14_17_21_262,skolem0001(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c224, c31])).
% 0.61/0.77 cnf(c366,plain,rs(i2003_11_14_17_21_262,skolem0001(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c230, c258])).
% 0.61/0.77 cnf(c372,plain,~ca_Vx5(i2003_11_14_17_21_262)|cp(skolem0001(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c366, c30])).
% 0.61/0.77 fof(axiom_8,axiom,(![X]:(ca_Ax4(X)<=>((![Y0]:(![Y1]:((rinvR(X,Y0)&rinvR(X,Y1))=>Y0=Y1)))&(?[Y]:(rinvR(X,Y)&ca_Vx5(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.61/0.77 fof(c33,plain,(![X]:((~ca_Ax4(X)|((![Y0]:(![Y1]:((~rinvR(X,Y0)|~rinvR(X,Y1))|Y0=Y1)))&(?[Y]:(rinvR(X,Y)&ca_Vx5(Y)))))&(((?[Y0]:(?[Y1]:((rinvR(X,Y0)&rinvR(X,Y1))&Y0!=Y1)))|(![Y]:(~rinvR(X,Y)|~ca_Vx5(Y))))|ca_Ax4(X)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.61/0.77 fof(c34,plain,((![X]:(~ca_Ax4(X)|((![Y0]:(![Y1]:((~rinvR(X,Y0)|~rinvR(X,Y1))|Y0=Y1)))&(?[Y]:(rinvR(X,Y)&ca_Vx5(Y))))))&(![X]:(((?[Y0]:(?[Y1]:((rinvR(X,Y0)&rinvR(X,Y1))&Y0!=Y1)))|(![Y]:(~rinvR(X,Y)|~ca_Vx5(Y))))|ca_Ax4(X)))),inference(shift_quantors,[status(thm)],[c33])).
% 0.61/0.77 fof(c35,plain,((![X10]:(~ca_Ax4(X10)|((![X11]:(![X12]:((~rinvR(X10,X11)|~rinvR(X10,X12))|X11=X12)))&(?[X13]:(rinvR(X10,X13)&ca_Vx5(X13))))))&(![X14]:(((?[X15]:(?[X16]:((rinvR(X14,X15)&rinvR(X14,X16))&X15!=X16)))|(![X17]:(~rinvR(X14,X17)|~ca_Vx5(X17))))|ca_Ax4(X14)))),inference(variable_rename,[status(thm)],[c34])).
% 0.61/0.77 fof(c37,plain,(![X10]:(![X11]:(![X12]:(![X14]:(![X17]:((~ca_Ax4(X10)|(((~rinvR(X10,X11)|~rinvR(X10,X12))|X11=X12)&(rinvR(X10,skolem0002(X10))&ca_Vx5(skolem0002(X10)))))&((((rinvR(X14,skolem0003(X14))&rinvR(X14,skolem0004(X14)))&skolem0003(X14)!=skolem0004(X14))|(~rinvR(X14,X17)|~ca_Vx5(X17)))|ca_Ax4(X14)))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,((![X10]:(~ca_Ax4(X10)|((![X11]:(![X12]:((~rinvR(X10,X11)|~rinvR(X10,X12))|X11=X12)))&(rinvR(X10,skolem0002(X10))&ca_Vx5(skolem0002(X10))))))&(![X14]:((((rinvR(X14,skolem0003(X14))&rinvR(X14,skolem0004(X14)))&skolem0003(X14)!=skolem0004(X14))|(![X17]:(~rinvR(X14,X17)|~ca_Vx5(X17))))|ca_Ax4(X14)))),inference(skolemize,[status(esa)],[c35])).])).
% 0.61/0.77 fof(c38,plain,(![X10]:(![X11]:(![X12]:(![X14]:(![X17]:(((~ca_Ax4(X10)|((~rinvR(X10,X11)|~rinvR(X10,X12))|X11=X12))&((~ca_Ax4(X10)|rinvR(X10,skolem0002(X10)))&(~ca_Ax4(X10)|ca_Vx5(skolem0002(X10)))))&((((rinvR(X14,skolem0003(X14))|(~rinvR(X14,X17)|~ca_Vx5(X17)))|ca_Ax4(X14))&((rinvR(X14,skolem0004(X14))|(~rinvR(X14,X17)|~ca_Vx5(X17)))|ca_Ax4(X14)))&((skolem0003(X14)!=skolem0004(X14)|(~rinvR(X14,X17)|~ca_Vx5(X17)))|ca_Ax4(X14))))))))),inference(distribute,[status(thm)],[c37])).
% 0.61/0.77 cnf(c41,plain,~ca_Ax4(X130)|ca_Vx5(skolem0002(X130)),inference(split_conjunct,[status(thm)],[c38])).
% 0.61/0.77 cnf(c88,plain,~cUnsatisfiable(X131)|ca_Ax4(skolem0009(X131)),inference(split_conjunct,[status(thm)],[c86])).
% 0.61/0.77 cnf(c176,plain,ca_Ax4(skolem0009(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c88, c17])).
% 0.61/0.77 cnf(c178,plain,ca_Vx5(skolem0002(skolem0009(i2003_11_14_17_21_262))),inference(resolution,[status(thm)],[c176, c41])).
% 0.61/0.77 cnf(c3,axiom,X142!=X143|~ca_Vx5(X142)|ca_Vx5(X143),theory(equality)).
% 0.61/0.77 cnf(c40,plain,~ca_Ax4(X146)|rinvR(X146,skolem0002(X146)),inference(split_conjunct,[status(thm)],[c38])).
% 0.61/0.77 cnf(c184,plain,rinvR(skolem0009(i2003_11_14_17_21_262),skolem0002(skolem0009(i2003_11_14_17_21_262))),inference(resolution,[status(thm)],[c40, c176])).
% 0.61/0.77 fof(axiom_10,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_10)).
% 0.61/0.77 fof(c18,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.61/0.77 fof(c19,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c18])).
% 0.61/0.77 fof(c21,plain,(![X2]:(![X3]:(![X4]:(![X5]:((~rinvR(X2,X3)|rr(X3,X2))&(~rr(X5,X4)|rinvR(X4,X5))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((![X2]:(![X3]:(~rinvR(X2,X3)|rr(X3,X2))))&(![X4]:(![X5]:(~rr(X5,X4)|rinvR(X4,X5))))),inference(variable_rename,[status(thm)],[c19])).])).
% 0.61/0.77 cnf(c23,plain,~rr(X127,X128)|rinvR(X128,X127),inference(split_conjunct,[status(thm)],[c21])).
% 0.61/0.77 cnf(c87,plain,~cUnsatisfiable(X161)|rr(X161,skolem0009(X161)),inference(split_conjunct,[status(thm)],[c86])).
% 0.61/0.77 cnf(c198,plain,rr(i2003_11_14_17_21_262,skolem0009(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c87, c17])).
% 0.61/0.77 cnf(c199,plain,rinvR(skolem0009(i2003_11_14_17_21_262),i2003_11_14_17_21_262),inference(resolution,[status(thm)],[c198, c23])).
% 0.61/0.77 cnf(c39,plain,~ca_Ax4(X264)|~rinvR(X264,X263)|~rinvR(X264,X262)|X263=X262,inference(split_conjunct,[status(thm)],[c38])).
% 0.61/0.77 cnf(c246,plain,~ca_Ax4(skolem0009(i2003_11_14_17_21_262))|~rinvR(skolem0009(i2003_11_14_17_21_262),X373)|X373=i2003_11_14_17_21_262,inference(resolution,[status(thm)],[c39, c199])).
% 0.61/0.77 cnf(c387,plain,~ca_Ax4(skolem0009(i2003_11_14_17_21_262))|skolem0002(skolem0009(i2003_11_14_17_21_262))=i2003_11_14_17_21_262,inference(resolution,[status(thm)],[c246, c184])).
% 0.61/0.77 cnf(c419,plain,skolem0002(skolem0009(i2003_11_14_17_21_262))=i2003_11_14_17_21_262,inference(resolution,[status(thm)],[c387, c176])).
% 0.61/0.77 cnf(c430,plain,~ca_Vx5(skolem0002(skolem0009(i2003_11_14_17_21_262)))|ca_Vx5(i2003_11_14_17_21_262),inference(resolution,[status(thm)],[c419, c3])).
% 0.61/0.77 cnf(c478,plain,ca_Vx5(i2003_11_14_17_21_262),inference(resolution,[status(thm)],[c430, c178])).
% 0.61/0.77 cnf(c484,plain,cp(skolem0001(i2003_11_14_17_21_262)),inference(resolution,[status(thm)],[c478, c372])).
% 0.61/0.77 cnf(c486,plain,$false,inference(resolution,[status(thm)],[c484, c328])).
% 0.61/0.77 % SZS output end CNFRefutation
% 0.61/0.77
% 0.61/0.77 % Initial clauses : 74
% 0.61/0.77 % Processed clauses : 156
% 0.61/0.77 % Factors computed : 2
% 0.61/0.77 % Resolvents computed: 315
% 0.61/0.77 % Tautologies deleted: 18
% 0.61/0.77 % Forward subsumed : 114
% 0.61/0.77 % Backward subsumed : 5
% 0.61/0.77 % -------- CPU Time ---------
% 0.61/0.77 % User time : 0.397 s
% 0.61/0.77 % System time : 0.016 s
% 0.61/0.77 % Total time : 0.413 s
%------------------------------------------------------------------------------