%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS119+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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.50s 0.69s
% Output : Refutation 0.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS119+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n012.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:06:52 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.50/0.69 % Version: 1.5
% 0.50/0.69 % SZS status Unsatisfiable
% 0.50/0.69 % SZS output start CNFRefutation
% 0.50/0.69 fof(axiom_11,axiom,cUnsatisfiable(i2003_11_14_17_21_44786),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_11)).
% 0.50/0.69 cnf(c14,plain,cUnsatisfiable(i2003_11_14_17_21_44786),inference(split_conjunct,[status(thm)],[axiom_11])).
% 0.50/0.69 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((?[Y]:(rr(X,Y)&ca_Vx3(Y)))&cp1(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.50/0.69 fof(c67,plain,(![X]:((~cUnsatisfiable(X)|((?[Y]:(rr(X,Y)&ca_Vx3(Y)))&cp1(X)))&(((![Y]:(~rr(X,Y)|~ca_Vx3(Y)))|~cp1(X))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.50/0.69 fof(c68,plain,((![X]:(~cUnsatisfiable(X)|((?[Y]:(rr(X,Y)&ca_Vx3(Y)))&cp1(X))))&(![X]:(((![Y]:(~rr(X,Y)|~ca_Vx3(Y)))|~cp1(X))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c67])).
% 0.50/0.69 fof(c69,plain,((![X32]:(~cUnsatisfiable(X32)|((?[X33]:(rr(X32,X33)&ca_Vx3(X33)))&cp1(X32))))&(![X34]:(((![X35]:(~rr(X34,X35)|~ca_Vx3(X35)))|~cp1(X34))|cUnsatisfiable(X34)))),inference(variable_rename,[status(thm)],[c68])).
% 0.50/0.69 fof(c71,plain,(![X32]:(![X34]:(![X35]:((~cUnsatisfiable(X32)|((rr(X32,skolem0005(X32))&ca_Vx3(skolem0005(X32)))&cp1(X32)))&(((~rr(X34,X35)|~ca_Vx3(X35))|~cp1(X34))|cUnsatisfiable(X34)))))),inference(shift_quantors,[status(thm)],[fof(c70,plain,((![X32]:(~cUnsatisfiable(X32)|((rr(X32,skolem0005(X32))&ca_Vx3(skolem0005(X32)))&cp1(X32))))&(![X34]:(((![X35]:(~rr(X34,X35)|~ca_Vx3(X35)))|~cp1(X34))|cUnsatisfiable(X34)))),inference(skolemize,[status(esa)],[c69])).])).
% 0.50/0.69 fof(c72,plain,(![X32]:(![X34]:(![X35]:((((~cUnsatisfiable(X32)|rr(X32,skolem0005(X32)))&(~cUnsatisfiable(X32)|ca_Vx3(skolem0005(X32))))&(~cUnsatisfiable(X32)|cp1(X32)))&(((~rr(X34,X35)|~ca_Vx3(X35))|~cp1(X34))|cUnsatisfiable(X34)))))),inference(distribute,[status(thm)],[c71])).
% 0.50/0.69 cnf(c75,plain,~cUnsatisfiable(X95)|cp1(X95),inference(split_conjunct,[status(thm)],[c72])).
% 0.50/0.69 cnf(c148,plain,cp1(i2003_11_14_17_21_44786),inference(resolution,[status(thm)],[c75, c14])).
% 0.50/0.69 fof(axiom_3,axiom,(![X]:(cp1(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.50/0.69 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.50/0.69 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.50/0.69 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.50/0.69 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.50/0.69 cnf(c65,plain,~cp1(X105)|~ra_Px1(X105,X104),inference(split_conjunct,[status(thm)],[c64])).
% 0.50/0.69 fof(axiom_4,axiom,(![X]:(cp1xcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.50/0.69 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.50/0.69 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.50/0.69 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.50/0.69 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.50/0.69 cnf(c58,plain,~cp1xcomp(X129)|ra_Px1(X129,skolem0003(X129)),inference(split_conjunct,[status(thm)],[c57])).
% 0.50/0.69 fof(axiom_6,axiom,(![X]:(ca_Vx3(X)<=>(?[Y]:(rr(X,Y)&ca_Ax2(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.50/0.69 fof(c34,plain,(![X]:((~ca_Vx3(X)|(?[Y]:(rr(X,Y)&ca_Ax2(Y))))&((![Y]:(~rr(X,Y)|~ca_Ax2(Y)))|ca_Vx3(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.50/0.69 fof(c35,plain,((![X]:(~ca_Vx3(X)|(?[Y]:(rr(X,Y)&ca_Ax2(Y)))))&(![X]:((![Y]:(~rr(X,Y)|~ca_Ax2(Y)))|ca_Vx3(X)))),inference(shift_quantors,[status(thm)],[c34])).
% 0.50/0.69 fof(c36,plain,((![X16]:(~ca_Vx3(X16)|(?[X17]:(rr(X16,X17)&ca_Ax2(X17)))))&(![X18]:((![X19]:(~rr(X18,X19)|~ca_Ax2(X19)))|ca_Vx3(X18)))),inference(variable_rename,[status(thm)],[c35])).
% 0.50/0.69 fof(c38,plain,(![X16]:(![X18]:(![X19]:((~ca_Vx3(X16)|(rr(X16,skolem0001(X16))&ca_Ax2(skolem0001(X16))))&((~rr(X18,X19)|~ca_Ax2(X19))|ca_Vx3(X18)))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,((![X16]:(~ca_Vx3(X16)|(rr(X16,skolem0001(X16))&ca_Ax2(skolem0001(X16)))))&(![X18]:((![X19]:(~rr(X18,X19)|~ca_Ax2(X19)))|ca_Vx3(X18)))),inference(skolemize,[status(esa)],[c36])).])).
% 0.50/0.69 fof(c39,plain,(![X16]:(![X18]:(![X19]:(((~ca_Vx3(X16)|rr(X16,skolem0001(X16)))&(~ca_Vx3(X16)|ca_Ax2(skolem0001(X16))))&((~rr(X18,X19)|~ca_Ax2(X19))|ca_Vx3(X18)))))),inference(distribute,[status(thm)],[c38])).
% 0.50/0.69 cnf(c41,plain,~ca_Vx3(X117)|ca_Ax2(skolem0001(X117)),inference(split_conjunct,[status(thm)],[c39])).
% 0.50/0.69 cnf(c74,plain,~cUnsatisfiable(X118)|ca_Vx3(skolem0005(X118)),inference(split_conjunct,[status(thm)],[c72])).
% 0.50/0.69 cnf(c153,plain,ca_Vx3(skolem0005(i2003_11_14_17_21_44786)),inference(resolution,[status(thm)],[c74, c14])).
% 0.50/0.69 cnf(c155,plain,ca_Ax2(skolem0001(skolem0005(i2003_11_14_17_21_44786))),inference(resolution,[status(thm)],[c153, c41])).
% 0.50/0.69 cnf(c42,plain,~rr(X157,X158)|~ca_Ax2(X158)|ca_Vx3(X157),inference(split_conjunct,[status(thm)],[c39])).
% 0.50/0.69 cnf(c73,plain,~cUnsatisfiable(X135)|rr(X135,skolem0005(X135)),inference(split_conjunct,[status(thm)],[c72])).
% 0.50/0.69 cnf(c162,plain,rr(i2003_11_14_17_21_44786,skolem0005(i2003_11_14_17_21_44786)),inference(resolution,[status(thm)],[c73, c14])).
% 0.50/0.69 fof(axiom_10,axiom,(![X]:(![Y]:(![Z]:((rr(X,Y)&rr(Y,Z))=>rr(X,Z))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_10)).
% 0.50/0.69 fof(c15,plain,(![X]:(![Y]:(![Z]:((~rr(X,Y)|~rr(Y,Z))|rr(X,Z))))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.50/0.69 fof(c16,plain,(![X2]:(![X3]:(![X4]:((~rr(X2,X3)|~rr(X3,X4))|rr(X2,X4))))),inference(variable_rename,[status(thm)],[c15])).
% 0.50/0.69 cnf(c17,plain,~rr(X201,X200)|~rr(X200,X199)|rr(X201,X199),inference(split_conjunct,[status(thm)],[c16])).
% 0.50/0.69 cnf(c40,plain,~ca_Vx3(X128)|rr(X128,skolem0001(X128)),inference(split_conjunct,[status(thm)],[c39])).
% 0.50/0.69 cnf(c158,plain,rr(skolem0005(i2003_11_14_17_21_44786),skolem0001(skolem0005(i2003_11_14_17_21_44786))),inference(resolution,[status(thm)],[c40, c153])).
% 0.50/0.69 cnf(c216,plain,~rr(X320,skolem0005(i2003_11_14_17_21_44786))|rr(X320,skolem0001(skolem0005(i2003_11_14_17_21_44786))),inference(resolution,[status(thm)],[c158, c17])).
% 0.50/0.69 cnf(c451,plain,rr(i2003_11_14_17_21_44786,skolem0001(skolem0005(i2003_11_14_17_21_44786))),inference(resolution,[status(thm)],[c216, c162])).
% 0.50/0.69 cnf(c454,plain,~ca_Ax2(skolem0001(skolem0005(i2003_11_14_17_21_44786)))|ca_Vx3(i2003_11_14_17_21_44786),inference(resolution,[status(thm)],[c451, c42])).
% 0.50/0.69 cnf(c466,plain,ca_Vx3(i2003_11_14_17_21_44786),inference(resolution,[status(thm)],[c454, c155])).
% 0.50/0.69 cnf(c477,plain,ca_Ax2(skolem0001(i2003_11_14_17_21_44786)),inference(resolution,[status(thm)],[c466, c41])).
% 0.50/0.69 fof(axiom_5,axiom,(![X]:(ca_Ax2(X)<=>(cp1(X)&(![Y]:(rinvR(X,Y)=>cp1xcomp(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.50/0.69 fof(c43,plain,(![X]:((~ca_Ax2(X)|(cp1(X)&(![Y]:(~rinvR(X,Y)|cp1xcomp(Y)))))&((~cp1(X)|(?[Y]:(rinvR(X,Y)&~cp1xcomp(Y))))|ca_Ax2(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.50/0.69 fof(c44,plain,((![X]:(~ca_Ax2(X)|(cp1(X)&(![Y]:(~rinvR(X,Y)|cp1xcomp(Y))))))&(![X]:((~cp1(X)|(?[Y]:(rinvR(X,Y)&~cp1xcomp(Y))))|ca_Ax2(X)))),inference(shift_quantors,[status(thm)],[c43])).
% 0.50/0.69 fof(c45,plain,((![X20]:(~ca_Ax2(X20)|(cp1(X20)&(![X21]:(~rinvR(X20,X21)|cp1xcomp(X21))))))&(![X22]:((~cp1(X22)|(?[X23]:(rinvR(X22,X23)&~cp1xcomp(X23))))|ca_Ax2(X22)))),inference(variable_rename,[status(thm)],[c44])).
% 0.50/0.69 fof(c47,plain,(![X20]:(![X21]:(![X22]:((~ca_Ax2(X20)|(cp1(X20)&(~rinvR(X20,X21)|cp1xcomp(X21))))&((~cp1(X22)|(rinvR(X22,skolem0002(X22))&~cp1xcomp(skolem0002(X22))))|ca_Ax2(X22)))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X20]:(~ca_Ax2(X20)|(cp1(X20)&(![X21]:(~rinvR(X20,X21)|cp1xcomp(X21))))))&(![X22]:((~cp1(X22)|(rinvR(X22,skolem0002(X22))&~cp1xcomp(skolem0002(X22))))|ca_Ax2(X22)))),inference(skolemize,[status(esa)],[c45])).])).
% 0.50/0.69 fof(c48,plain,(![X20]:(![X21]:(![X22]:(((~ca_Ax2(X20)|cp1(X20))&(~ca_Ax2(X20)|(~rinvR(X20,X21)|cp1xcomp(X21))))&(((~cp1(X22)|rinvR(X22,skolem0002(X22)))|ca_Ax2(X22))&((~cp1(X22)|~cp1xcomp(skolem0002(X22)))|ca_Ax2(X22))))))),inference(distribute,[status(thm)],[c47])).
% 0.50/0.69 cnf(c50,plain,~ca_Ax2(X159)|~rinvR(X159,X160)|cp1xcomp(X160),inference(split_conjunct,[status(thm)],[c48])).
% 0.50/0.69 fof(axiom_9,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 0.50/0.69 fof(c18,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.50/0.69 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.50/0.69 fof(c21,plain,(![X5]:(![X6]:(![X7]:(![X8]:((~rinvR(X5,X6)|rr(X6,X5))&(~rr(X8,X7)|rinvR(X7,X8))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((![X5]:(![X6]:(~rinvR(X5,X6)|rr(X6,X5))))&(![X7]:(![X8]:(~rr(X8,X7)|rinvR(X7,X8))))),inference(variable_rename,[status(thm)],[c19])).])).
% 0.50/0.69 cnf(c23,plain,~rr(X109,X108)|rinvR(X108,X109),inference(split_conjunct,[status(thm)],[c21])).
% 0.50/0.69 cnf(c478,plain,rr(i2003_11_14_17_21_44786,skolem0001(i2003_11_14_17_21_44786)),inference(resolution,[status(thm)],[c466, c40])).
% 0.50/0.69 cnf(c490,plain,rinvR(skolem0001(i2003_11_14_17_21_44786),i2003_11_14_17_21_44786),inference(resolution,[status(thm)],[c478, c23])).
% 0.50/0.69 cnf(c494,plain,~ca_Ax2(skolem0001(i2003_11_14_17_21_44786))|cp1xcomp(i2003_11_14_17_21_44786),inference(resolution,[status(thm)],[c490, c50])).
% 0.50/0.69 cnf(c502,plain,cp1xcomp(i2003_11_14_17_21_44786),inference(resolution,[status(thm)],[c494, c477])).
% 0.50/0.69 cnf(c510,plain,ra_Px1(i2003_11_14_17_21_44786,skolem0003(i2003_11_14_17_21_44786)),inference(resolution,[status(thm)],[c502, c58])).
% 0.50/0.69 cnf(c515,plain,~cp1(i2003_11_14_17_21_44786),inference(resolution,[status(thm)],[c510, c65])).
% 0.50/0.69 cnf(c519,plain,$false,inference(resolution,[status(thm)],[c515, c148])).
% 0.50/0.69 % SZS output end CNFRefutation
% 0.50/0.69
% 0.50/0.69 % Initial clauses : 62
% 0.50/0.69 % Processed clauses : 122
% 0.50/0.69 % Factors computed : 3
% 0.50/0.69 % Resolvents computed: 370
% 0.50/0.69 % Tautologies deleted: 17
% 0.50/0.69 % Forward subsumed : 81
% 0.50/0.69 % Backward subsumed : 7
% 0.50/0.69 % -------- CPU Time ---------
% 0.50/0.69 % User time : 0.325 s
% 0.50/0.69 % System time : 0.015 s
% 0.50/0.69 % Total time : 0.340 s
%------------------------------------------------------------------------------