%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS109+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:43 EDT 2024
% Result : Unsatisfiable 0.48s 0.65s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : KRS109+1 : TPTP v8.1.2. Released v3.1.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n003.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:11:07 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.48/0.65 % Version: 1.5
% 0.48/0.65 % SZS status Unsatisfiable
% 0.48/0.65 % SZS output start CNFRefutation
% 0.48/0.65 fof(axiom_3,axiom,(![X]:(cp(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.48/0.65 fof(c78,plain,(![X]:((~cp(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.48/0.65 fof(c79,plain,((![X]:(~cp(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(shift_quantors,[status(thm)],[c78])).
% 0.48/0.65 fof(c80,plain,((![X41]:(~cp(X41)|(![X42]:~ra_Px1(X41,X42))))&(![X43]:((?[X44]:ra_Px1(X43,X44))|cp(X43)))),inference(variable_rename,[status(thm)],[c79])).
% 0.48/0.65 fof(c82,plain,(![X41]:(![X42]:(![X43]:((~cp(X41)|~ra_Px1(X41,X42))&(ra_Px1(X43,skolem0005(X43))|cp(X43)))))),inference(shift_quantors,[status(thm)],[fof(c81,plain,((![X41]:(~cp(X41)|(![X42]:~ra_Px1(X41,X42))))&(![X43]:(ra_Px1(X43,skolem0005(X43))|cp(X43)))),inference(skolemize,[status(esa)],[c80])).])).
% 0.48/0.65 cnf(c83,plain,~cp(X128)|~ra_Px1(X128,X129),inference(split_conjunct,[status(thm)],[c82])).
% 0.48/0.65 fof(axiom_13,axiom,cUnsatisfiable(i2003_11_14_17_21_08508),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_13)).
% 0.48/0.65 cnf(c22,plain,cUnsatisfiable(i2003_11_14_17_21_08508),inference(split_conjunct,[status(thm)],[axiom_13])).
% 0.48/0.65 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(cpxcomp(X)&(?[Y]:(rf(X,Y)&ca_Ax2(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.48/0.65 fof(c85,plain,(![X]:((~cUnsatisfiable(X)|(cpxcomp(X)&(?[Y]:(rf(X,Y)&ca_Ax2(Y)))))&((~cpxcomp(X)|(![Y]:(~rf(X,Y)|~ca_Ax2(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.48/0.65 fof(c86,plain,((![X]:(~cUnsatisfiable(X)|(cpxcomp(X)&(?[Y]:(rf(X,Y)&ca_Ax2(Y))))))&(![X]:((~cpxcomp(X)|(![Y]:(~rf(X,Y)|~ca_Ax2(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c85])).
% 0.48/0.65 fof(c87,plain,((![X45]:(~cUnsatisfiable(X45)|(cpxcomp(X45)&(?[X46]:(rf(X45,X46)&ca_Ax2(X46))))))&(![X47]:((~cpxcomp(X47)|(![X48]:(~rf(X47,X48)|~ca_Ax2(X48))))|cUnsatisfiable(X47)))),inference(variable_rename,[status(thm)],[c86])).
% 0.48/0.65 fof(c89,plain,(![X45]:(![X47]:(![X48]:((~cUnsatisfiable(X45)|(cpxcomp(X45)&(rf(X45,skolem0006(X45))&ca_Ax2(skolem0006(X45)))))&((~cpxcomp(X47)|(~rf(X47,X48)|~ca_Ax2(X48)))|cUnsatisfiable(X47)))))),inference(shift_quantors,[status(thm)],[fof(c88,plain,((![X45]:(~cUnsatisfiable(X45)|(cpxcomp(X45)&(rf(X45,skolem0006(X45))&ca_Ax2(skolem0006(X45))))))&(![X47]:((~cpxcomp(X47)|(![X48]:(~rf(X47,X48)|~ca_Ax2(X48))))|cUnsatisfiable(X47)))),inference(skolemize,[status(esa)],[c87])).])).
% 0.48/0.65 fof(c90,plain,(![X45]:(![X47]:(![X48]:(((~cUnsatisfiable(X45)|cpxcomp(X45))&((~cUnsatisfiable(X45)|rf(X45,skolem0006(X45)))&(~cUnsatisfiable(X45)|ca_Ax2(skolem0006(X45)))))&((~cpxcomp(X47)|(~rf(X47,X48)|~ca_Ax2(X48)))|cUnsatisfiable(X47)))))),inference(distribute,[status(thm)],[c89])).
% 0.48/0.65 cnf(c91,plain,~cUnsatisfiable(X116)|cpxcomp(X116),inference(split_conjunct,[status(thm)],[c90])).
% 0.48/0.65 cnf(c177,plain,cpxcomp(i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c91, c22])).
% 0.48/0.65 fof(axiom_4,axiom,(![X]:(cpxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.48/0.65 fof(c71,plain,(![X]:((~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.48/0.65 fof(c72,plain,((![X]:(~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(shift_quantors,[status(thm)],[c71])).
% 0.48/0.65 fof(c73,plain,((![X37]:(~cpxcomp(X37)|(?[X38]:ra_Px1(X37,X38))))&(![X39]:((![X40]:~ra_Px1(X39,X40))|cpxcomp(X39)))),inference(variable_rename,[status(thm)],[c72])).
% 0.48/0.65 fof(c75,plain,(![X37]:(![X39]:(![X40]:((~cpxcomp(X37)|ra_Px1(X37,skolem0004(X37)))&(~ra_Px1(X39,X40)|cpxcomp(X39)))))),inference(shift_quantors,[status(thm)],[fof(c74,plain,((![X37]:(~cpxcomp(X37)|ra_Px1(X37,skolem0004(X37))))&(![X39]:((![X40]:~ra_Px1(X39,X40))|cpxcomp(X39)))),inference(skolemize,[status(esa)],[c73])).])).
% 0.48/0.65 cnf(c76,plain,~cpxcomp(X161)|ra_Px1(X161,skolem0004(X161)),inference(split_conjunct,[status(thm)],[c75])).
% 0.48/0.65 cnf(c186,plain,ra_Px1(i2003_11_14_17_21_08508,skolem0004(i2003_11_14_17_21_08508)),inference(resolution,[status(thm)],[c76, c177])).
% 0.48/0.65 cnf(c188,plain,~cp(i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c186, c83])).
% 0.48/0.65 cnf(c93,plain,~cUnsatisfiable(X153)|ca_Ax2(skolem0006(X153)),inference(split_conjunct,[status(thm)],[c90])).
% 0.48/0.65 cnf(c184,plain,ca_Ax2(skolem0006(i2003_11_14_17_21_08508)),inference(resolution,[status(thm)],[c93, c22])).
% 0.48/0.65 fof(axiom_5,axiom,(![X]:(ca_Ax2(X)<=>((![Y]:(rinvS(X,Y)=>cp(Y)))&(![Y]:(rinvF(X,Y)=>ca_Vx3(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.48/0.65 fof(c59,plain,(![X]:((~ca_Ax2(X)|((![Y]:(~rinvS(X,Y)|cp(Y)))&(![Y]:(~rinvF(X,Y)|ca_Vx3(Y)))))&(((?[Y]:(rinvS(X,Y)&~cp(Y)))|(?[Y]:(rinvF(X,Y)&~ca_Vx3(Y))))|ca_Ax2(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.48/0.65 fof(c60,plain,((![X]:(~ca_Ax2(X)|((![Y]:(~rinvS(X,Y)|cp(Y)))&(![Y]:(~rinvF(X,Y)|ca_Vx3(Y))))))&(![X]:(((?[Y]:(rinvS(X,Y)&~cp(Y)))|(?[Y]:(rinvF(X,Y)&~ca_Vx3(Y))))|ca_Ax2(X)))),inference(shift_quantors,[status(thm)],[c59])).
% 0.48/0.65 fof(c61,plain,((![X31]:(~ca_Ax2(X31)|((![X32]:(~rinvS(X31,X32)|cp(X32)))&(![X33]:(~rinvF(X31,X33)|ca_Vx3(X33))))))&(![X34]:(((?[X35]:(rinvS(X34,X35)&~cp(X35)))|(?[X36]:(rinvF(X34,X36)&~ca_Vx3(X36))))|ca_Ax2(X34)))),inference(variable_rename,[status(thm)],[c60])).
% 0.48/0.65 fof(c63,plain,(![X31]:(![X32]:(![X33]:(![X34]:((~ca_Ax2(X31)|((~rinvS(X31,X32)|cp(X32))&(~rinvF(X31,X33)|ca_Vx3(X33))))&(((rinvS(X34,skolem0002(X34))&~cp(skolem0002(X34)))|(rinvF(X34,skolem0003(X34))&~ca_Vx3(skolem0003(X34))))|ca_Ax2(X34))))))),inference(shift_quantors,[status(thm)],[fof(c62,plain,((![X31]:(~ca_Ax2(X31)|((![X32]:(~rinvS(X31,X32)|cp(X32)))&(![X33]:(~rinvF(X31,X33)|ca_Vx3(X33))))))&(![X34]:(((rinvS(X34,skolem0002(X34))&~cp(skolem0002(X34)))|(rinvF(X34,skolem0003(X34))&~ca_Vx3(skolem0003(X34))))|ca_Ax2(X34)))),inference(skolemize,[status(esa)],[c61])).])).
% 0.48/0.65 fof(c64,plain,(![X31]:(![X32]:(![X33]:(![X34]:(((~ca_Ax2(X31)|(~rinvS(X31,X32)|cp(X32)))&(~ca_Ax2(X31)|(~rinvF(X31,X33)|ca_Vx3(X33))))&((((rinvS(X34,skolem0002(X34))|rinvF(X34,skolem0003(X34)))|ca_Ax2(X34))&((rinvS(X34,skolem0002(X34))|~ca_Vx3(skolem0003(X34)))|ca_Ax2(X34)))&(((~cp(skolem0002(X34))|rinvF(X34,skolem0003(X34)))|ca_Ax2(X34))&((~cp(skolem0002(X34))|~ca_Vx3(skolem0003(X34)))|ca_Ax2(X34))))))))),inference(distribute,[status(thm)],[c63])).
% 0.48/0.65 cnf(c65,plain,~ca_Ax2(X196)|~rinvS(X196,X195)|cp(X195),inference(split_conjunct,[status(thm)],[c64])).
% 0.48/0.65 fof(axiom_11,axiom,(![X]:(![Y]:(rinvS(X,Y)<=>rs(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_11)).
% 0.48/0.65 fof(c26,plain,(![X]:(![Y]:((~rinvS(X,Y)|rs(Y,X))&(~rs(Y,X)|rinvS(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_11])).
% 0.48/0.65 fof(c27,plain,((![X]:(![Y]:(~rinvS(X,Y)|rs(Y,X))))&(![X]:(![Y]:(~rs(Y,X)|rinvS(X,Y))))),inference(shift_quantors,[status(thm)],[c26])).
% 0.48/0.65 fof(c29,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~rinvS(X9,X10)|rs(X10,X9))&(~rs(X12,X11)|rinvS(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c28,plain,((![X9]:(![X10]:(~rinvS(X9,X10)|rs(X10,X9))))&(![X11]:(![X12]:(~rs(X12,X11)|rinvS(X11,X12))))),inference(variable_rename,[status(thm)],[c27])).])).
% 0.48/0.65 cnf(c31,plain,~rs(X140,X139)|rinvS(X139,X140),inference(split_conjunct,[status(thm)],[c29])).
% 0.48/0.65 cnf(symmetry,axiom,X117!=X118|X118=X117,theory(equality)).
% 0.48/0.65 cnf(c92,plain,~cUnsatisfiable(X172)|rf(X172,skolem0006(X172)),inference(split_conjunct,[status(thm)],[c90])).
% 0.48/0.65 cnf(c197,plain,rf(i2003_11_14_17_21_08508,skolem0006(i2003_11_14_17_21_08508)),inference(resolution,[status(thm)],[c92, c22])).
% 0.48/0.65 fof(axiom_14,axiom,(![X]:(![Y]:(rs(X,Y)=>rf(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_14)).
% 0.48/0.65 fof(c19,plain,(![X]:(![Y]:(~rs(X,Y)|rf(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_14])).
% 0.48/0.65 fof(c20,plain,(![X4]:(![X5]:(~rs(X4,X5)|rf(X4,X5)))),inference(variable_rename,[status(thm)],[c19])).
% 0.48/0.65 cnf(c21,plain,~rs(X133,X132)|rf(X133,X132),inference(split_conjunct,[status(thm)],[c20])).
% 0.48/0.65 fof(axiom_6,axiom,(![X]:(ca_Vx3(X)<=>(?[Y]:(rs(X,Y)&cp(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.48/0.65 fof(c50,plain,(![X]:((~ca_Vx3(X)|(?[Y]:(rs(X,Y)&cp(Y))))&((![Y]:(~rs(X,Y)|~cp(Y)))|ca_Vx3(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.48/0.65 fof(c51,plain,((![X]:(~ca_Vx3(X)|(?[Y]:(rs(X,Y)&cp(Y)))))&(![X]:((![Y]:(~rs(X,Y)|~cp(Y)))|ca_Vx3(X)))),inference(shift_quantors,[status(thm)],[c50])).
% 0.48/0.65 fof(c52,plain,((![X27]:(~ca_Vx3(X27)|(?[X28]:(rs(X27,X28)&cp(X28)))))&(![X29]:((![X30]:(~rs(X29,X30)|~cp(X30)))|ca_Vx3(X29)))),inference(variable_rename,[status(thm)],[c51])).
% 0.48/0.65 fof(c54,plain,(![X27]:(![X29]:(![X30]:((~ca_Vx3(X27)|(rs(X27,skolem0001(X27))&cp(skolem0001(X27))))&((~rs(X29,X30)|~cp(X30))|ca_Vx3(X29)))))),inference(shift_quantors,[status(thm)],[fof(c53,plain,((![X27]:(~ca_Vx3(X27)|(rs(X27,skolem0001(X27))&cp(skolem0001(X27)))))&(![X29]:((![X30]:(~rs(X29,X30)|~cp(X30)))|ca_Vx3(X29)))),inference(skolemize,[status(esa)],[c52])).])).
% 0.48/0.65 fof(c55,plain,(![X27]:(![X29]:(![X30]:(((~ca_Vx3(X27)|rs(X27,skolem0001(X27)))&(~ca_Vx3(X27)|cp(skolem0001(X27))))&((~rs(X29,X30)|~cp(X30))|ca_Vx3(X29)))))),inference(distribute,[status(thm)],[c54])).
% 0.48/0.65 cnf(c56,plain,~ca_Vx3(X160)|rs(X160,skolem0001(X160)),inference(split_conjunct,[status(thm)],[c55])).
% 0.48/0.65 fof(axiom_9,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.48/0.65 fof(c38,plain,(![X]:(![Y]:((~rinvF(X,Y)|rf(Y,X))&(~rf(Y,X)|rinvF(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.48/0.65 fof(c39,plain,((![X]:(![Y]:(~rinvF(X,Y)|rf(Y,X))))&(![X]:(![Y]:(~rf(Y,X)|rinvF(X,Y))))),inference(shift_quantors,[status(thm)],[c38])).
% 0.48/0.65 fof(c41,plain,(![X17]:(![X18]:(![X19]:(![X20]:((~rinvF(X17,X18)|rf(X18,X17))&(~rf(X20,X19)|rinvF(X19,X20))))))),inference(shift_quantors,[status(thm)],[fof(c40,plain,((![X17]:(![X18]:(~rinvF(X17,X18)|rf(X18,X17))))&(![X19]:(![X20]:(~rf(X20,X19)|rinvF(X19,X20))))),inference(variable_rename,[status(thm)],[c39])).])).
% 0.48/0.65 cnf(c43,plain,~rf(X151,X150)|rinvF(X150,X151),inference(split_conjunct,[status(thm)],[c41])).
% 0.48/0.65 cnf(c198,plain,rinvF(skolem0006(i2003_11_14_17_21_08508),i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c197, c43])).
% 0.48/0.65 cnf(c66,plain,~ca_Ax2(X198)|~rinvF(X198,X197)|ca_Vx3(X197),inference(split_conjunct,[status(thm)],[c64])).
% 0.48/0.65 cnf(c211,plain,~ca_Ax2(skolem0006(i2003_11_14_17_21_08508))|ca_Vx3(i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c66, c198])).
% 0.48/0.65 cnf(c213,plain,ca_Vx3(i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c211, c184])).
% 0.48/0.65 cnf(c214,plain,rs(i2003_11_14_17_21_08508,skolem0001(i2003_11_14_17_21_08508)),inference(resolution,[status(thm)],[c213, c56])).
% 0.48/0.65 cnf(c217,plain,rf(i2003_11_14_17_21_08508,skolem0001(i2003_11_14_17_21_08508)),inference(resolution,[status(thm)],[c214, c21])).
% 0.48/0.65 fof(axiom_7,axiom,(![X]:(![Y]:(![Z]:((rf(X,Y)&rf(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.48/0.65 fof(c47,plain,(![X]:(![Y]:(![Z]:((~rf(X,Y)|~rf(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.48/0.65 fof(c48,plain,(![X24]:(![X25]:(![X26]:((~rf(X24,X25)|~rf(X24,X26))|X25=X26)))),inference(variable_rename,[status(thm)],[c47])).
% 0.48/0.65 cnf(c49,plain,~rf(X249,X248)|~rf(X249,X247)|X248=X247,inference(split_conjunct,[status(thm)],[c48])).
% 0.48/0.65 cnf(c238,plain,~rf(i2003_11_14_17_21_08508,X299)|X299=skolem0001(i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c49, c217])).
% 0.48/0.65 cnf(c281,plain,skolem0006(i2003_11_14_17_21_08508)=skolem0001(i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c238, c197])).
% 0.48/0.65 cnf(c289,plain,skolem0001(i2003_11_14_17_21_08508)=skolem0006(i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c281, symmetry])).
% 0.48/0.65 fof(rs_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rs(C,A))=>rs(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rs_substitution_2)).
% 0.48/0.65 fof(c114,plain,(![A]:(![B]:(![C]:((A!=B|~rs(C,A))|rs(C,B))))),inference(fof_nnf,[status(thm)],[rs_substitution_2])).
% 0.48/0.65 fof(c115,plain,(![X57]:(![X58]:(![X59]:((X57!=X58|~rs(X59,X57))|rs(X59,X58))))),inference(variable_rename,[status(thm)],[c114])).
% 0.48/0.65 cnf(c116,plain,X252!=X253|~rs(X254,X252)|rs(X254,X253),inference(split_conjunct,[status(thm)],[c115])).
% 0.48/0.65 cnf(c240,plain,skolem0001(i2003_11_14_17_21_08508)!=X304|rs(i2003_11_14_17_21_08508,X304),inference(resolution,[status(thm)],[c116, c214])).
% 0.48/0.65 cnf(c304,plain,rs(i2003_11_14_17_21_08508,skolem0006(i2003_11_14_17_21_08508)),inference(resolution,[status(thm)],[c240, c289])).
% 0.48/0.65 cnf(c308,plain,rinvS(skolem0006(i2003_11_14_17_21_08508),i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c304, c31])).
% 0.48/0.65 cnf(c319,plain,~ca_Ax2(skolem0006(i2003_11_14_17_21_08508))|cp(i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c308, c65])).
% 0.48/0.65 cnf(c332,plain,cp(i2003_11_14_17_21_08508),inference(resolution,[status(thm)],[c319, c184])).
% 0.48/0.65 cnf(c334,plain,$false,inference(resolution,[status(thm)],[c332, c188])).
% 0.48/0.65 % SZS output end CNFRefutation
% 0.48/0.65
% 0.48/0.65 % Initial clauses : 75
% 0.48/0.65 % Processed clauses : 99
% 0.48/0.65 % Factors computed : 4
% 0.48/0.65 % Resolvents computed: 155
% 0.48/0.65 % Tautologies deleted: 12
% 0.48/0.65 % Forward subsumed : 39
% 0.48/0.65 % Backward subsumed : 3
% 0.48/0.65 % -------- CPU Time ---------
% 0.48/0.65 % User time : 0.273 s
% 0.48/0.65 % System time : 0.018 s
% 0.48/0.65 % Total time : 0.291 s
%------------------------------------------------------------------------------