%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS107+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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.61s 0.79s
% Output : Refutation 0.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : KRS107+1 : TPTP v8.1.2. Released v3.1.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n013.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 00:07:53 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.61/0.79 % Version: 1.5
% 0.61/0.79 % SZS status Unsatisfiable
% 0.61/0.79 % SZS output start CNFRefutation
% 0.61/0.79 fof(axiom_6,axiom,(![X]:(ca_Cx1xcomp(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.61/0.79 fof(c61,plain,(![X]:((~ca_Cx1xcomp(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|ca_Cx1xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.61/0.79 fof(c62,plain,((![X]:(~ca_Cx1xcomp(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|ca_Cx1xcomp(X)))),inference(shift_quantors,[status(thm)],[c61])).
% 0.61/0.79 fof(c63,plain,((![X33]:(~ca_Cx1xcomp(X33)|(![X34]:~ra_Px1(X33,X34))))&(![X35]:((?[X36]:ra_Px1(X35,X36))|ca_Cx1xcomp(X35)))),inference(variable_rename,[status(thm)],[c62])).
% 0.61/0.79 fof(c65,plain,(![X33]:(![X34]:(![X35]:((~ca_Cx1xcomp(X33)|~ra_Px1(X33,X34))&(ra_Px1(X35,skolem0001(X35))|ca_Cx1xcomp(X35)))))),inference(shift_quantors,[status(thm)],[fof(c64,plain,((![X33]:(~ca_Cx1xcomp(X33)|(![X34]:~ra_Px1(X33,X34))))&(![X35]:(ra_Px1(X35,skolem0001(X35))|ca_Cx1xcomp(X35)))),inference(skolemize,[status(esa)],[c63])).])).
% 0.61/0.79 cnf(c66,plain,~ca_Cx1xcomp(X158)|~ra_Px1(X158,X159),inference(split_conjunct,[status(thm)],[c65])).
% 0.61/0.79 fof(axiom_12,axiom,cUnsatisfiable(i2003_11_14_17_21_01226),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_12)).
% 0.61/0.79 cnf(c45,plain,cUnsatisfiable(i2003_11_14_17_21_01226),inference(split_conjunct,[status(thm)],[axiom_12])).
% 0.61/0.79 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((?[Y]:(rrx3(X,Y)&cc1(Y)))&(?[Y]:(rrx4(X,Y)&cc2(Y))))&ca_Cx1(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.61/0.79 fof(c92,plain,(![X]:((~cUnsatisfiable(X)|(((?[Y]:(rrx3(X,Y)&cc1(Y)))&(?[Y]:(rrx4(X,Y)&cc2(Y))))&ca_Cx1(X)))&((((![Y]:(~rrx3(X,Y)|~cc1(Y)))|(![Y]:(~rrx4(X,Y)|~cc2(Y))))|~ca_Cx1(X))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.61/0.79 fof(c93,plain,((![X]:(~cUnsatisfiable(X)|(((?[Y]:(rrx3(X,Y)&cc1(Y)))&(?[Y]:(rrx4(X,Y)&cc2(Y))))&ca_Cx1(X))))&(![X]:((((![Y]:(~rrx3(X,Y)|~cc1(Y)))|(![Y]:(~rrx4(X,Y)|~cc2(Y))))|~ca_Cx1(X))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c92])).
% 0.61/0.79 fof(c94,plain,((![X47]:(~cUnsatisfiable(X47)|(((?[X48]:(rrx3(X47,X48)&cc1(X48)))&(?[X49]:(rrx4(X47,X49)&cc2(X49))))&ca_Cx1(X47))))&(![X50]:((((![X51]:(~rrx3(X50,X51)|~cc1(X51)))|(![X52]:(~rrx4(X50,X52)|~cc2(X52))))|~ca_Cx1(X50))|cUnsatisfiable(X50)))),inference(variable_rename,[status(thm)],[c93])).
% 0.61/0.79 fof(c96,plain,(![X47]:(![X50]:(![X51]:(![X52]:((~cUnsatisfiable(X47)|(((rrx3(X47,skolem0004(X47))&cc1(skolem0004(X47)))&(rrx4(X47,skolem0005(X47))&cc2(skolem0005(X47))))&ca_Cx1(X47)))&((((~rrx3(X50,X51)|~cc1(X51))|(~rrx4(X50,X52)|~cc2(X52)))|~ca_Cx1(X50))|cUnsatisfiable(X50))))))),inference(shift_quantors,[status(thm)],[fof(c95,plain,((![X47]:(~cUnsatisfiable(X47)|(((rrx3(X47,skolem0004(X47))&cc1(skolem0004(X47)))&(rrx4(X47,skolem0005(X47))&cc2(skolem0005(X47))))&ca_Cx1(X47))))&(![X50]:((((![X51]:(~rrx3(X50,X51)|~cc1(X51)))|(![X52]:(~rrx4(X50,X52)|~cc2(X52))))|~ca_Cx1(X50))|cUnsatisfiable(X50)))),inference(skolemize,[status(esa)],[c94])).])).
% 0.61/0.79 fof(c97,plain,(![X47]:(![X50]:(![X51]:(![X52]:(((((~cUnsatisfiable(X47)|rrx3(X47,skolem0004(X47)))&(~cUnsatisfiable(X47)|cc1(skolem0004(X47))))&((~cUnsatisfiable(X47)|rrx4(X47,skolem0005(X47)))&(~cUnsatisfiable(X47)|cc2(skolem0005(X47)))))&(~cUnsatisfiable(X47)|ca_Cx1(X47)))&((((~rrx3(X50,X51)|~cc1(X51))|(~rrx4(X50,X52)|~cc2(X52)))|~ca_Cx1(X50))|cUnsatisfiable(X50))))))),inference(distribute,[status(thm)],[c96])).
% 0.61/0.79 cnf(c102,plain,~cUnsatisfiable(X151)|ca_Cx1(X151),inference(split_conjunct,[status(thm)],[c97])).
% 0.61/0.79 cnf(c214,plain,ca_Cx1(i2003_11_14_17_21_01226),inference(resolution,[status(thm)],[c102, c45])).
% 0.61/0.79 fof(axiom_4,axiom,(![X]:(ca_Cx1(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.61/0.79 fof(c77,plain,(![X]:((~ca_Cx1(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|ca_Cx1(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.61/0.79 fof(c78,plain,((![X]:(~ca_Cx1(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|ca_Cx1(X)))),inference(shift_quantors,[status(thm)],[c77])).
% 0.61/0.79 fof(c79,plain,((![X41]:(~ca_Cx1(X41)|(?[X42]:ra_Px1(X41,X42))))&(![X43]:((![X44]:~ra_Px1(X43,X44))|ca_Cx1(X43)))),inference(variable_rename,[status(thm)],[c78])).
% 0.61/0.79 fof(c81,plain,(![X41]:(![X43]:(![X44]:((~ca_Cx1(X41)|ra_Px1(X41,skolem0003(X41)))&(~ra_Px1(X43,X44)|ca_Cx1(X43)))))),inference(shift_quantors,[status(thm)],[fof(c80,plain,((![X41]:(~ca_Cx1(X41)|ra_Px1(X41,skolem0003(X41))))&(![X43]:((![X44]:~ra_Px1(X43,X44))|ca_Cx1(X43)))),inference(skolemize,[status(esa)],[c79])).])).
% 0.61/0.79 cnf(c82,plain,~ca_Cx1(X209)|ra_Px1(X209,skolem0003(X209)),inference(split_conjunct,[status(thm)],[c81])).
% 0.61/0.79 cnf(c236,plain,ra_Px1(i2003_11_14_17_21_01226,skolem0003(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c82, c214])).
% 0.61/0.79 cnf(c239,plain,~ca_Cx1xcomp(i2003_11_14_17_21_01226),inference(resolution,[status(thm)],[c236, c66])).
% 0.61/0.79 cnf(c98,plain,~cUnsatisfiable(X215)|rrx3(X215,skolem0004(X215)),inference(split_conjunct,[status(thm)],[c97])).
% 0.61/0.79 cnf(c247,plain,rrx3(i2003_11_14_17_21_01226,skolem0004(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c98, c45])).
% 0.61/0.79 fof(axiom_5,axiom,(![X]:(ca_Cx1xcomp(X)<=>(?[Y]:(rrx3(X,Y)&ca_Ax2(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.61/0.79 fof(c68,plain,(![X]:((~ca_Cx1xcomp(X)|(?[Y]:(rrx3(X,Y)&ca_Ax2(Y))))&((![Y]:(~rrx3(X,Y)|~ca_Ax2(Y)))|ca_Cx1xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.61/0.79 fof(c69,plain,((![X]:(~ca_Cx1xcomp(X)|(?[Y]:(rrx3(X,Y)&ca_Ax2(Y)))))&(![X]:((![Y]:(~rrx3(X,Y)|~ca_Ax2(Y)))|ca_Cx1xcomp(X)))),inference(shift_quantors,[status(thm)],[c68])).
% 0.61/0.79 fof(c70,plain,((![X37]:(~ca_Cx1xcomp(X37)|(?[X38]:(rrx3(X37,X38)&ca_Ax2(X38)))))&(![X39]:((![X40]:(~rrx3(X39,X40)|~ca_Ax2(X40)))|ca_Cx1xcomp(X39)))),inference(variable_rename,[status(thm)],[c69])).
% 0.61/0.79 fof(c72,plain,(![X37]:(![X39]:(![X40]:((~ca_Cx1xcomp(X37)|(rrx3(X37,skolem0002(X37))&ca_Ax2(skolem0002(X37))))&((~rrx3(X39,X40)|~ca_Ax2(X40))|ca_Cx1xcomp(X39)))))),inference(shift_quantors,[status(thm)],[fof(c71,plain,((![X37]:(~ca_Cx1xcomp(X37)|(rrx3(X37,skolem0002(X37))&ca_Ax2(skolem0002(X37)))))&(![X39]:((![X40]:(~rrx3(X39,X40)|~ca_Ax2(X40)))|ca_Cx1xcomp(X39)))),inference(skolemize,[status(esa)],[c70])).])).
% 0.61/0.79 fof(c73,plain,(![X37]:(![X39]:(![X40]:(((~ca_Cx1xcomp(X37)|rrx3(X37,skolem0002(X37)))&(~ca_Cx1xcomp(X37)|ca_Ax2(skolem0002(X37))))&((~rrx3(X39,X40)|~ca_Ax2(X40))|ca_Cx1xcomp(X39)))))),inference(distribute,[status(thm)],[c72])).
% 0.61/0.79 cnf(c76,plain,~rrx3(X246,X245)|~ca_Ax2(X245)|ca_Cx1xcomp(X246),inference(split_conjunct,[status(thm)],[c73])).
% 0.61/0.79 cnf(c274,plain,~ca_Ax2(skolem0004(i2003_11_14_17_21_01226))|ca_Cx1xcomp(i2003_11_14_17_21_01226),inference(resolution,[status(thm)],[c76, c247])).
% 0.61/0.79 cnf(c99,plain,~cUnsatisfiable(X188)|cc1(skolem0004(X188)),inference(split_conjunct,[status(thm)],[c97])).
% 0.61/0.79 cnf(c221,plain,cc1(skolem0004(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c99, c45])).
% 0.61/0.79 fof(axiom_3,axiom,(![X]:(ca_Ax2(X)<=>(cc2(X)&cc1(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.61/0.79 fof(c84,plain,(![X]:((~ca_Ax2(X)|(cc2(X)&cc1(X)))&((~cc2(X)|~cc1(X))|ca_Ax2(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.61/0.79 fof(c85,plain,((![X]:(~ca_Ax2(X)|(cc2(X)&cc1(X))))&(![X]:((~cc2(X)|~cc1(X))|ca_Ax2(X)))),inference(shift_quantors,[status(thm)],[c84])).
% 0.61/0.79 fof(c87,plain,(![X45]:(![X46]:((~ca_Ax2(X45)|(cc2(X45)&cc1(X45)))&((~cc2(X46)|~cc1(X46))|ca_Ax2(X46))))),inference(shift_quantors,[status(thm)],[fof(c86,plain,((![X45]:(~ca_Ax2(X45)|(cc2(X45)&cc1(X45))))&(![X46]:((~cc2(X46)|~cc1(X46))|ca_Ax2(X46)))),inference(variable_rename,[status(thm)],[c85])).])).
% 0.61/0.79 fof(c88,plain,(![X45]:(![X46]:(((~ca_Ax2(X45)|cc2(X45))&(~ca_Ax2(X45)|cc1(X45)))&((~cc2(X46)|~cc1(X46))|ca_Ax2(X46))))),inference(distribute,[status(thm)],[c87])).
% 0.61/0.79 cnf(c91,plain,~cc2(X214)|~cc1(X214)|ca_Ax2(X214),inference(split_conjunct,[status(thm)],[c88])).
% 0.61/0.79 cnf(c245,plain,~cc2(skolem0004(i2003_11_14_17_21_01226))|ca_Ax2(skolem0004(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c91, c221])).
% 0.61/0.79 cnf(c101,plain,~cUnsatisfiable(X189)|cc2(skolem0005(X189)),inference(split_conjunct,[status(thm)],[c97])).
% 0.61/0.79 cnf(c222,plain,cc2(skolem0005(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c101, c45])).
% 0.61/0.79 cnf(c5,axiom,X206!=X205|~cc2(X206)|cc2(X205),theory(equality)).
% 0.61/0.79 fof(axiom_17,axiom,(![X]:(![Y]:(rrx4(X,Y)=>rrx(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_17)).
% 0.61/0.79 fof(c30,plain,(![X]:(![Y]:(~rrx4(X,Y)|rrx(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_17])).
% 0.61/0.79 fof(c31,plain,(![X8]:(![X9]:(~rrx4(X8,X9)|rrx(X8,X9)))),inference(variable_rename,[status(thm)],[c30])).
% 0.61/0.79 cnf(c32,plain,~rrx4(X171,X172)|rrx(X171,X172),inference(split_conjunct,[status(thm)],[c31])).
% 0.61/0.79 cnf(c100,plain,~cUnsatisfiable(X220)|rrx4(X220,skolem0005(X220)),inference(split_conjunct,[status(thm)],[c97])).
% 0.61/0.79 cnf(c253,plain,rrx4(i2003_11_14_17_21_01226,skolem0005(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c100, c45])).
% 0.61/0.79 cnf(c255,plain,rrx(i2003_11_14_17_21_01226,skolem0005(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c253, c32])).
% 0.61/0.79 fof(axiom_20,axiom,(![X]:(![Y]:(rrx3(X,Y)=>rrx(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_20)).
% 0.61/0.79 fof(c21,plain,(![X]:(![Y]:(~rrx3(X,Y)|rrx(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_20])).
% 0.61/0.79 fof(c22,plain,(![X2]:(![X3]:(~rrx3(X2,X3)|rrx(X2,X3)))),inference(variable_rename,[status(thm)],[c21])).
% 0.61/0.79 cnf(c23,plain,~rrx3(X162,X163)|rrx(X162,X163),inference(split_conjunct,[status(thm)],[c22])).
% 0.61/0.79 cnf(c249,plain,rrx(i2003_11_14_17_21_01226,skolem0004(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c247, c23])).
% 0.61/0.79 fof(axiom_7,axiom,(![X]:(![Y]:(![Z]:((rrx(X,Y)&rrx(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.61/0.79 fof(c58,plain,(![X]:(![Y]:(![Z]:((~rrx(X,Y)|~rrx(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.61/0.79 fof(c59,plain,(![X30]:(![X31]:(![X32]:((~rrx(X30,X31)|~rrx(X30,X32))|X31=X32)))),inference(variable_rename,[status(thm)],[c58])).
% 0.61/0.79 cnf(c60,plain,~rrx(X343,X344)|~rrx(X343,X345)|X344=X345,inference(split_conjunct,[status(thm)],[c59])).
% 0.61/0.79 cnf(c319,plain,~rrx(i2003_11_14_17_21_01226,X439)|X439=skolem0004(i2003_11_14_17_21_01226),inference(resolution,[status(thm)],[c60, c249])).
% 0.61/0.79 cnf(c416,plain,skolem0005(i2003_11_14_17_21_01226)=skolem0004(i2003_11_14_17_21_01226),inference(resolution,[status(thm)],[c319, c255])).
% 0.61/0.79 cnf(c418,plain,~cc2(skolem0005(i2003_11_14_17_21_01226))|cc2(skolem0004(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c416, c5])).
% 0.61/0.79 cnf(c522,plain,cc2(skolem0004(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c418, c222])).
% 0.61/0.79 cnf(c523,plain,ca_Ax2(skolem0004(i2003_11_14_17_21_01226)),inference(resolution,[status(thm)],[c522, c245])).
% 0.61/0.79 cnf(c525,plain,ca_Cx1xcomp(i2003_11_14_17_21_01226),inference(resolution,[status(thm)],[c523, c274])).
% 0.61/0.79 cnf(c531,plain,$false,inference(resolution,[status(thm)],[c525, c239])).
% 0.61/0.79 % SZS output end CNFRefutation
% 0.61/0.79
% 0.61/0.79 % Initial clauses : 90
% 0.61/0.79 % Processed clauses : 162
% 0.61/0.79 % Factors computed : 6
% 0.61/0.79 % Resolvents computed: 316
% 0.61/0.79 % Tautologies deleted: 13
% 0.61/0.79 % Forward subsumed : 97
% 0.61/0.79 % Backward subsumed : 4
% 0.61/0.79 % -------- CPU Time ---------
% 0.61/0.79 % User time : 0.403 s
% 0.61/0.79 % System time : 0.021 s
% 0.61/0.79 % Total time : 0.424 s
%------------------------------------------------------------------------------