%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS118+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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.90s 1.14s
% Output : Refutation 0.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KRS118+1 : TPTP v8.1.2. Released v3.1.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n004.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 : Thu May 9 00:05:38 EDT 2024
% 0.19/0.34 % CPUTime :
% 0.90/1.14 % Version: 1.5
% 0.90/1.14 % SZS status Unsatisfiable
% 0.90/1.14 % SZS output start CNFRefutation
% 0.90/1.14 fof(axiom_5,axiom,(![X]:(cd(X)<=>((?[Y]:(rf(X,Y)&ccxcomp(Y)))&cc(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.90/1.14 fof(c45,plain,(![X]:((~cd(X)|((?[Y]:(rf(X,Y)&ccxcomp(Y)))&cc(X)))&(((![Y]:(~rf(X,Y)|~ccxcomp(Y)))|~cc(X))|cd(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.90/1.14 fof(c46,plain,((![X]:(~cd(X)|((?[Y]:(rf(X,Y)&ccxcomp(Y)))&cc(X))))&(![X]:(((![Y]:(~rf(X,Y)|~ccxcomp(Y)))|~cc(X))|cd(X)))),inference(shift_quantors,[status(thm)],[c45])).
% 0.90/1.14 fof(c47,plain,((![X22]:(~cd(X22)|((?[X23]:(rf(X22,X23)&ccxcomp(X23)))&cc(X22))))&(![X24]:(((![X25]:(~rf(X24,X25)|~ccxcomp(X25)))|~cc(X24))|cd(X24)))),inference(variable_rename,[status(thm)],[c46])).
% 0.90/1.14 fof(c49,plain,(![X22]:(![X24]:(![X25]:((~cd(X22)|((rf(X22,skolem0002(X22))&ccxcomp(skolem0002(X22)))&cc(X22)))&(((~rf(X24,X25)|~ccxcomp(X25))|~cc(X24))|cd(X24)))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,((![X22]:(~cd(X22)|((rf(X22,skolem0002(X22))&ccxcomp(skolem0002(X22)))&cc(X22))))&(![X24]:(((![X25]:(~rf(X24,X25)|~ccxcomp(X25)))|~cc(X24))|cd(X24)))),inference(skolemize,[status(esa)],[c47])).])).
% 0.90/1.14 fof(c50,plain,(![X22]:(![X24]:(![X25]:((((~cd(X22)|rf(X22,skolem0002(X22)))&(~cd(X22)|ccxcomp(skolem0002(X22))))&(~cd(X22)|cc(X22)))&(((~rf(X24,X25)|~ccxcomp(X25))|~cc(X24))|cd(X24)))))),inference(distribute,[status(thm)],[c49])).
% 0.90/1.14 cnf(c53,plain,~cd(X95)|cc(X95),inference(split_conjunct,[status(thm)],[c50])).
% 0.90/1.14 fof(axiom_11,axiom,cUnsatisfiable(i2003_11_14_17_21_4056),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_11)).
% 0.90/1.14 cnf(c17,plain,cUnsatisfiable(i2003_11_14_17_21_4056),inference(split_conjunct,[status(thm)],[axiom_11])).
% 0.90/1.14 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((![Y]:(rinvR(X,Y)=>ca_Vx3(Y)))&(?[Y]:(rinvF(X,Y)&cd(Y))))&ccxcomp(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.90/1.14 fof(c69,plain,(![X]:((~cUnsatisfiable(X)|(((![Y]:(~rinvR(X,Y)|ca_Vx3(Y)))&(?[Y]:(rinvF(X,Y)&cd(Y))))&ccxcomp(X)))&((((?[Y]:(rinvR(X,Y)&~ca_Vx3(Y)))|(![Y]:(~rinvF(X,Y)|~cd(Y))))|~ccxcomp(X))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.90/1.14 fof(c70,plain,((![X]:(~cUnsatisfiable(X)|(((![Y]:(~rinvR(X,Y)|ca_Vx3(Y)))&(?[Y]:(rinvF(X,Y)&cd(Y))))&ccxcomp(X))))&(![X]:((((?[Y]:(rinvR(X,Y)&~ca_Vx3(Y)))|(![Y]:(~rinvF(X,Y)|~cd(Y))))|~ccxcomp(X))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c69])).
% 0.90/1.14 fof(c71,plain,((![X34]:(~cUnsatisfiable(X34)|(((![X35]:(~rinvR(X34,X35)|ca_Vx3(X35)))&(?[X36]:(rinvF(X34,X36)&cd(X36))))&ccxcomp(X34))))&(![X37]:((((?[X38]:(rinvR(X37,X38)&~ca_Vx3(X38)))|(![X39]:(~rinvF(X37,X39)|~cd(X39))))|~ccxcomp(X37))|cUnsatisfiable(X37)))),inference(variable_rename,[status(thm)],[c70])).
% 0.90/1.14 fof(c73,plain,(![X34]:(![X35]:(![X37]:(![X39]:((~cUnsatisfiable(X34)|(((~rinvR(X34,X35)|ca_Vx3(X35))&(rinvF(X34,skolem0005(X34))&cd(skolem0005(X34))))&ccxcomp(X34)))&((((rinvR(X37,skolem0006(X37))&~ca_Vx3(skolem0006(X37)))|(~rinvF(X37,X39)|~cd(X39)))|~ccxcomp(X37))|cUnsatisfiable(X37))))))),inference(shift_quantors,[status(thm)],[fof(c72,plain,((![X34]:(~cUnsatisfiable(X34)|(((![X35]:(~rinvR(X34,X35)|ca_Vx3(X35)))&(rinvF(X34,skolem0005(X34))&cd(skolem0005(X34))))&ccxcomp(X34))))&(![X37]:((((rinvR(X37,skolem0006(X37))&~ca_Vx3(skolem0006(X37)))|(![X39]:(~rinvF(X37,X39)|~cd(X39))))|~ccxcomp(X37))|cUnsatisfiable(X37)))),inference(skolemize,[status(esa)],[c71])).])).
% 0.90/1.14 fof(c74,plain,(![X34]:(![X35]:(![X37]:(![X39]:((((~cUnsatisfiable(X34)|(~rinvR(X34,X35)|ca_Vx3(X35)))&((~cUnsatisfiable(X34)|rinvF(X34,skolem0005(X34)))&(~cUnsatisfiable(X34)|cd(skolem0005(X34)))))&(~cUnsatisfiable(X34)|ccxcomp(X34)))&((((rinvR(X37,skolem0006(X37))|(~rinvF(X37,X39)|~cd(X39)))|~ccxcomp(X37))|cUnsatisfiable(X37))&(((~ca_Vx3(skolem0006(X37))|(~rinvF(X37,X39)|~cd(X39)))|~ccxcomp(X37))|cUnsatisfiable(X37)))))))),inference(distribute,[status(thm)],[c73])).
% 0.90/1.14 cnf(c77,plain,~cUnsatisfiable(X128)|cd(skolem0005(X128)),inference(split_conjunct,[status(thm)],[c74])).
% 0.90/1.14 cnf(c158,plain,cd(skolem0005(i2003_11_14_17_21_4056)),inference(resolution,[status(thm)],[c77, c17])).
% 0.90/1.14 cnf(c160,plain,cc(skolem0005(i2003_11_14_17_21_4056)),inference(resolution,[status(thm)],[c158, c53])).
% 0.90/1.14 fof(axiom_3,axiom,(![X]:(cc(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.90/1.14 fof(c62,plain,(![X]:((~cc(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cc(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.90/1.14 fof(c63,plain,((![X]:(~cc(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cc(X)))),inference(shift_quantors,[status(thm)],[c62])).
% 0.90/1.14 fof(c64,plain,((![X30]:(~cc(X30)|(![X31]:~ra_Px1(X30,X31))))&(![X32]:((?[X33]:ra_Px1(X32,X33))|cc(X32)))),inference(variable_rename,[status(thm)],[c63])).
% 0.90/1.14 fof(c66,plain,(![X30]:(![X31]:(![X32]:((~cc(X30)|~ra_Px1(X30,X31))&(ra_Px1(X32,skolem0004(X32))|cc(X32)))))),inference(shift_quantors,[status(thm)],[fof(c65,plain,((![X30]:(~cc(X30)|(![X31]:~ra_Px1(X30,X31))))&(![X32]:(ra_Px1(X32,skolem0004(X32))|cc(X32)))),inference(skolemize,[status(esa)],[c64])).])).
% 0.90/1.14 cnf(c67,plain,~cc(X108)|~ra_Px1(X108,X109),inference(split_conjunct,[status(thm)],[c66])).
% 0.90/1.14 fof(axiom_4,axiom,(![X]:(ccxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.90/1.14 fof(c55,plain,(![X]:((~ccxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|ccxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.90/1.14 fof(c56,plain,((![X]:(~ccxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|ccxcomp(X)))),inference(shift_quantors,[status(thm)],[c55])).
% 0.90/1.14 fof(c57,plain,((![X26]:(~ccxcomp(X26)|(?[X27]:ra_Px1(X26,X27))))&(![X28]:((![X29]:~ra_Px1(X28,X29))|ccxcomp(X28)))),inference(variable_rename,[status(thm)],[c56])).
% 0.90/1.14 fof(c59,plain,(![X26]:(![X28]:(![X29]:((~ccxcomp(X26)|ra_Px1(X26,skolem0003(X26)))&(~ra_Px1(X28,X29)|ccxcomp(X28)))))),inference(shift_quantors,[status(thm)],[fof(c58,plain,((![X26]:(~ccxcomp(X26)|ra_Px1(X26,skolem0003(X26))))&(![X28]:((![X29]:~ra_Px1(X28,X29))|ccxcomp(X28)))),inference(skolemize,[status(esa)],[c57])).])).
% 0.90/1.14 cnf(c60,plain,~ccxcomp(X140)|ra_Px1(X140,skolem0003(X140)),inference(split_conjunct,[status(thm)],[c59])).
% 0.90/1.14 cnf(c52,plain,~cd(X127)|ccxcomp(skolem0002(X127)),inference(split_conjunct,[status(thm)],[c50])).
% 0.90/1.14 fof(axiom_6,axiom,(![X]:(ca_Vx3(X)<=>(?[Y]:(rinvF(X,Y)&cd(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.90/1.14 fof(c36,plain,(![X]:((~ca_Vx3(X)|(?[Y]:(rinvF(X,Y)&cd(Y))))&((![Y]:(~rinvF(X,Y)|~cd(Y)))|ca_Vx3(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.90/1.14 fof(c37,plain,((![X]:(~ca_Vx3(X)|(?[Y]:(rinvF(X,Y)&cd(Y)))))&(![X]:((![Y]:(~rinvF(X,Y)|~cd(Y)))|ca_Vx3(X)))),inference(shift_quantors,[status(thm)],[c36])).
% 0.90/1.14 fof(c38,plain,((![X18]:(~ca_Vx3(X18)|(?[X19]:(rinvF(X18,X19)&cd(X19)))))&(![X20]:((![X21]:(~rinvF(X20,X21)|~cd(X21)))|ca_Vx3(X20)))),inference(variable_rename,[status(thm)],[c37])).
% 0.90/1.14 fof(c40,plain,(![X18]:(![X20]:(![X21]:((~ca_Vx3(X18)|(rinvF(X18,skolem0001(X18))&cd(skolem0001(X18))))&((~rinvF(X20,X21)|~cd(X21))|ca_Vx3(X20)))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,((![X18]:(~ca_Vx3(X18)|(rinvF(X18,skolem0001(X18))&cd(skolem0001(X18)))))&(![X20]:((![X21]:(~rinvF(X20,X21)|~cd(X21)))|ca_Vx3(X20)))),inference(skolemize,[status(esa)],[c38])).])).
% 0.90/1.14 fof(c41,plain,(![X18]:(![X20]:(![X21]:(((~ca_Vx3(X18)|rinvF(X18,skolem0001(X18)))&(~ca_Vx3(X18)|cd(skolem0001(X18))))&((~rinvF(X20,X21)|~cd(X21))|ca_Vx3(X20)))))),inference(distribute,[status(thm)],[c40])).
% 0.90/1.14 cnf(c43,plain,~ca_Vx3(X123)|cd(skolem0001(X123)),inference(split_conjunct,[status(thm)],[c41])).
% 0.90/1.14 fof(axiom_9,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 0.90/1.14 fof(c21,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.90/1.14 fof(c22,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c21])).
% 0.90/1.14 fof(c24,plain,(![X7]:(![X8]:(![X9]:(![X10]:((~rinvR(X7,X8)|rr(X8,X7))&(~rr(X10,X9)|rinvR(X9,X10))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X7]:(![X8]:(~rinvR(X7,X8)|rr(X8,X7))))&(![X9]:(![X10]:(~rr(X10,X9)|rinvR(X9,X10))))),inference(variable_rename,[status(thm)],[c22])).])).
% 0.90/1.14 cnf(c26,plain,~rr(X117,X118)|rinvR(X118,X117),inference(split_conjunct,[status(thm)],[c24])).
% 0.90/1.14 fof(axiom_12,axiom,(![X]:(![Y]:(rf(X,Y)=>rr(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_12)).
% 0.90/1.14 fof(c14,plain,(![X]:(![Y]:(~rf(X,Y)|rr(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_12])).
% 0.90/1.14 fof(c15,plain,(![X2]:(![X3]:(~rf(X2,X3)|rr(X2,X3)))),inference(variable_rename,[status(thm)],[c14])).
% 0.90/1.14 cnf(c16,plain,~rf(X111,X110)|rr(X111,X110),inference(split_conjunct,[status(thm)],[c15])).
% 0.90/1.14 fof(axiom_8,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.90/1.14 fof(c27,plain,(![X]:(![Y]:((~rinvF(X,Y)|rf(Y,X))&(~rf(Y,X)|rinvF(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.90/1.14 fof(c28,plain,((![X]:(![Y]:(~rinvF(X,Y)|rf(Y,X))))&(![X]:(![Y]:(~rf(Y,X)|rinvF(X,Y))))),inference(shift_quantors,[status(thm)],[c27])).
% 0.90/1.14 fof(c30,plain,(![X11]:(![X12]:(![X13]:(![X14]:((~rinvF(X11,X12)|rf(X12,X11))&(~rf(X14,X13)|rinvF(X13,X14))))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,((![X11]:(![X12]:(~rinvF(X11,X12)|rf(X12,X11))))&(![X13]:(![X14]:(~rf(X14,X13)|rinvF(X13,X14))))),inference(variable_rename,[status(thm)],[c28])).])).
% 0.90/1.14 cnf(c31,plain,~rinvF(X120,X119)|rf(X119,X120),inference(split_conjunct,[status(thm)],[c30])).
% 0.90/1.14 cnf(c76,plain,~cUnsatisfiable(X149)|rinvF(X149,skolem0005(X149)),inference(split_conjunct,[status(thm)],[c74])).
% 0.90/1.14 cnf(c176,plain,rinvF(i2003_11_14_17_21_4056,skolem0005(i2003_11_14_17_21_4056)),inference(resolution,[status(thm)],[c76, c17])).
% 0.90/1.14 cnf(c177,plain,rf(skolem0005(i2003_11_14_17_21_4056),i2003_11_14_17_21_4056),inference(resolution,[status(thm)],[c176, c31])).
% 0.90/1.14 cnf(c179,plain,rr(skolem0005(i2003_11_14_17_21_4056),i2003_11_14_17_21_4056),inference(resolution,[status(thm)],[c177, c16])).
% 0.90/1.14 cnf(c180,plain,rinvR(i2003_11_14_17_21_4056,skolem0005(i2003_11_14_17_21_4056)),inference(resolution,[status(thm)],[c179, c26])).
% 0.90/1.14 cnf(c75,plain,~cUnsatisfiable(X176)|~rinvR(X176,X175)|ca_Vx3(X175),inference(split_conjunct,[status(thm)],[c74])).
% 0.90/1.14 cnf(c194,plain,~cUnsatisfiable(i2003_11_14_17_21_4056)|ca_Vx3(skolem0005(i2003_11_14_17_21_4056)),inference(resolution,[status(thm)],[c75, c180])).
% 0.90/1.14 cnf(c221,plain,ca_Vx3(skolem0005(i2003_11_14_17_21_4056)),inference(resolution,[status(thm)],[c194, c17])).
% 0.90/1.14 cnf(c223,plain,cd(skolem0001(skolem0005(i2003_11_14_17_21_4056))),inference(resolution,[status(thm)],[c221, c43])).
% 0.90/1.14 cnf(c227,plain,ccxcomp(skolem0002(skolem0001(skolem0005(i2003_11_14_17_21_4056)))),inference(resolution,[status(thm)],[c223, c52])).
% 0.90/1.14 cnf(c3,axiom,X136!=X137|~ccxcomp(X136)|ccxcomp(X137),theory(equality)).
% 0.90/1.14 cnf(c51,plain,~cd(X139)|rf(X139,skolem0002(X139)),inference(split_conjunct,[status(thm)],[c50])).
% 0.90/1.14 cnf(c226,plain,rf(skolem0001(skolem0005(i2003_11_14_17_21_4056)),skolem0002(skolem0001(skolem0005(i2003_11_14_17_21_4056)))),inference(resolution,[status(thm)],[c223, c51])).
% 0.90/1.14 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.90/1.14 fof(c33,plain,(![X]:(![Y]:(![Z]:((~rf(X,Y)|~rf(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.90/1.14 fof(c34,plain,(![X15]:(![X16]:(![X17]:((~rf(X15,X16)|~rf(X15,X17))|X16=X17)))),inference(variable_rename,[status(thm)],[c33])).
% 0.90/1.14 cnf(c35,plain,~rf(X209,X207)|~rf(X209,X208)|X207=X208,inference(split_conjunct,[status(thm)],[c34])).
% 0.90/1.14 cnf(c42,plain,~ca_Vx3(X135)|rinvF(X135,skolem0001(X135)),inference(split_conjunct,[status(thm)],[c41])).
% 0.90/1.14 cnf(c222,plain,rinvF(skolem0005(i2003_11_14_17_21_4056),skolem0001(skolem0005(i2003_11_14_17_21_4056))),inference(resolution,[status(thm)],[c221, c42])).
% 0.90/1.14 cnf(c331,plain,rf(skolem0001(skolem0005(i2003_11_14_17_21_4056)),skolem0005(i2003_11_14_17_21_4056)),inference(resolution,[status(thm)],[c222, c31])).
% 0.90/1.14 cnf(c491,plain,~rf(skolem0001(skolem0005(i2003_11_14_17_21_4056)),X389)|X389=skolem0005(i2003_11_14_17_21_4056),inference(resolution,[status(thm)],[c331, c35])).
% 0.90/1.14 cnf(c904,plain,skolem0002(skolem0001(skolem0005(i2003_11_14_17_21_4056)))=skolem0005(i2003_11_14_17_21_4056),inference(resolution,[status(thm)],[c491, c226])).
% 0.90/1.14 cnf(c912,plain,~ccxcomp(skolem0002(skolem0001(skolem0005(i2003_11_14_17_21_4056))))|ccxcomp(skolem0005(i2003_11_14_17_21_4056)),inference(resolution,[status(thm)],[c904, c3])).
% 0.90/1.14 cnf(c1377,plain,ccxcomp(skolem0005(i2003_11_14_17_21_4056)),inference(resolution,[status(thm)],[c912, c227])).
% 0.90/1.14 cnf(c1380,plain,ra_Px1(skolem0005(i2003_11_14_17_21_4056),skolem0003(skolem0005(i2003_11_14_17_21_4056))),inference(resolution,[status(thm)],[c1377, c60])).
% 0.90/1.14 cnf(c1384,plain,~cc(skolem0005(i2003_11_14_17_21_4056)),inference(resolution,[status(thm)],[c1380, c67])).
% 0.90/1.14 cnf(c1389,plain,$false,inference(resolution,[status(thm)],[c1384, c160])).
% 0.90/1.14 % SZS output end CNFRefutation
% 0.90/1.14
% 0.90/1.14 % Initial clauses : 65
% 0.90/1.14 % Processed clauses : 440
% 0.90/1.14 % Factors computed : 3
% 0.90/1.14 % Resolvents computed: 1236
% 0.90/1.14 % Tautologies deleted: 13
% 0.90/1.14 % Forward subsumed : 445
% 0.90/1.14 % Backward subsumed : 14
% 0.90/1.14 % -------- CPU Time ---------
% 0.90/1.14 % User time : 0.768 s
% 0.90/1.14 % System time : 0.024 s
% 0.90/1.14 % Total time : 0.792 s
%------------------------------------------------------------------------------