%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS128+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:46 EDT 2024
% Result : Unsatisfiable 0.50s 0.66s
% Output : Refutation 0.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS128+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n009.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 00:11:22 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.50/0.66 % Version: 1.5
% 0.50/0.66 % SZS status Unsatisfiable
% 0.50/0.66 % SZS output start CNFRefutation
% 0.50/0.66 fof(axiom_10,axiom,(![X]:(ca_Cx4xcomp(X)<=>(cd(X)&cexcomp(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_10)).
% 0.50/0.66 fof(c1,plain,(![X]:((~ca_Cx4xcomp(X)|(cd(X)&cexcomp(X)))&((~cd(X)|~cexcomp(X))|ca_Cx4xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.50/0.66 fof(c2,plain,((![X]:(~ca_Cx4xcomp(X)|(cd(X)&cexcomp(X))))&(![X]:((~cd(X)|~cexcomp(X))|ca_Cx4xcomp(X)))),inference(shift_quantors,[status(thm)],[c1])).
% 0.50/0.66 fof(c4,plain,(![X2]:(![X3]:((~ca_Cx4xcomp(X2)|(cd(X2)&cexcomp(X2)))&((~cd(X3)|~cexcomp(X3))|ca_Cx4xcomp(X3))))),inference(shift_quantors,[status(thm)],[fof(c3,plain,((![X2]:(~ca_Cx4xcomp(X2)|(cd(X2)&cexcomp(X2))))&(![X3]:((~cd(X3)|~cexcomp(X3))|ca_Cx4xcomp(X3)))),inference(variable_rename,[status(thm)],[c2])).])).
% 0.50/0.66 fof(c5,plain,(![X2]:(![X3]:(((~ca_Cx4xcomp(X2)|cd(X2))&(~ca_Cx4xcomp(X2)|cexcomp(X2)))&((~cd(X3)|~cexcomp(X3))|ca_Cx4xcomp(X3))))),inference(distribute,[status(thm)],[c4])).
% 0.50/0.66 cnf(c8,plain,~cd(X45)|~cexcomp(X45)|ca_Cx4xcomp(X45),inference(split_conjunct,[status(thm)],[c5])).
% 0.50/0.66 fof(axiom_11,axiom,cUnsatisfiable(i2003_11_14_17_22_31584),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_11)).
% 0.50/0.66 cnf(c0,plain,cUnsatisfiable(i2003_11_14_17_22_31584),inference(split_conjunct,[status(thm)],[axiom_11])).
% 0.50/0.66 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((?[Y]:(rr(X,Y)&cexcomp(Y)))&(![Y]:(rr(X,Y)=>cd(Y))))&(![Y]:(rr(X,Y)=>ca_Cx4(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.50/0.66 fof(c54,plain,(![X]:((~cUnsatisfiable(X)|(((?[Y]:(rr(X,Y)&cexcomp(Y)))&(![Y]:(~rr(X,Y)|cd(Y))))&(![Y]:(~rr(X,Y)|ca_Cx4(Y)))))&((((![Y]:(~rr(X,Y)|~cexcomp(Y)))|(?[Y]:(rr(X,Y)&~cd(Y))))|(?[Y]:(rr(X,Y)&~ca_Cx4(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.50/0.66 fof(c55,plain,((![X]:(~cUnsatisfiable(X)|(((?[Y]:(rr(X,Y)&cexcomp(Y)))&(![Y]:(~rr(X,Y)|cd(Y))))&(![Y]:(~rr(X,Y)|ca_Cx4(Y))))))&(![X]:((((![Y]:(~rr(X,Y)|~cexcomp(Y)))|(?[Y]:(rr(X,Y)&~cd(Y))))|(?[Y]:(rr(X,Y)&~ca_Cx4(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c54])).
% 0.50/0.66 fof(c56,plain,((![X29]:(~cUnsatisfiable(X29)|(((?[X30]:(rr(X29,X30)&cexcomp(X30)))&(![X31]:(~rr(X29,X31)|cd(X31))))&(![X32]:(~rr(X29,X32)|ca_Cx4(X32))))))&(![X33]:((((![X34]:(~rr(X33,X34)|~cexcomp(X34)))|(?[X35]:(rr(X33,X35)&~cd(X35))))|(?[X36]:(rr(X33,X36)&~ca_Cx4(X36))))|cUnsatisfiable(X33)))),inference(variable_rename,[status(thm)],[c55])).
% 0.50/0.66 fof(c58,plain,(![X29]:(![X31]:(![X32]:(![X33]:(![X34]:((~cUnsatisfiable(X29)|(((rr(X29,skolem0007(X29))&cexcomp(skolem0007(X29)))&(~rr(X29,X31)|cd(X31)))&(~rr(X29,X32)|ca_Cx4(X32))))&((((~rr(X33,X34)|~cexcomp(X34))|(rr(X33,skolem0008(X33))&~cd(skolem0008(X33))))|(rr(X33,skolem0009(X33))&~ca_Cx4(skolem0009(X33))))|cUnsatisfiable(X33)))))))),inference(shift_quantors,[status(thm)],[fof(c57,plain,((![X29]:(~cUnsatisfiable(X29)|(((rr(X29,skolem0007(X29))&cexcomp(skolem0007(X29)))&(![X31]:(~rr(X29,X31)|cd(X31))))&(![X32]:(~rr(X29,X32)|ca_Cx4(X32))))))&(![X33]:((((![X34]:(~rr(X33,X34)|~cexcomp(X34)))|(rr(X33,skolem0008(X33))&~cd(skolem0008(X33))))|(rr(X33,skolem0009(X33))&~ca_Cx4(skolem0009(X33))))|cUnsatisfiable(X33)))),inference(skolemize,[status(esa)],[c56])).])).
% 0.50/0.66 fof(c59,plain,(![X29]:(![X31]:(![X32]:(![X33]:(![X34]:(((((~cUnsatisfiable(X29)|rr(X29,skolem0007(X29)))&(~cUnsatisfiable(X29)|cexcomp(skolem0007(X29))))&(~cUnsatisfiable(X29)|(~rr(X29,X31)|cd(X31))))&(~cUnsatisfiable(X29)|(~rr(X29,X32)|ca_Cx4(X32))))&((((((~rr(X33,X34)|~cexcomp(X34))|rr(X33,skolem0008(X33)))|rr(X33,skolem0009(X33)))|cUnsatisfiable(X33))&((((~rr(X33,X34)|~cexcomp(X34))|rr(X33,skolem0008(X33)))|~ca_Cx4(skolem0009(X33)))|cUnsatisfiable(X33)))&(((((~rr(X33,X34)|~cexcomp(X34))|~cd(skolem0008(X33)))|rr(X33,skolem0009(X33)))|cUnsatisfiable(X33))&((((~rr(X33,X34)|~cexcomp(X34))|~cd(skolem0008(X33)))|~ca_Cx4(skolem0009(X33)))|cUnsatisfiable(X33)))))))))),inference(distribute,[status(thm)],[c58])).
% 0.50/0.66 cnf(c61,plain,~cUnsatisfiable(X68)|cexcomp(skolem0007(X68)),inference(split_conjunct,[status(thm)],[c59])).
% 0.50/0.66 cnf(c92,plain,cexcomp(skolem0007(i2003_11_14_17_22_31584)),inference(resolution,[status(thm)],[c61, c0])).
% 0.50/0.66 cnf(c95,plain,~cd(skolem0007(i2003_11_14_17_22_31584))|ca_Cx4xcomp(skolem0007(i2003_11_14_17_22_31584)),inference(resolution,[status(thm)],[c92, c8])).
% 0.50/0.66 cnf(c60,plain,~cUnsatisfiable(X77)|rr(X77,skolem0007(X77)),inference(split_conjunct,[status(thm)],[c59])).
% 0.50/0.66 cnf(c104,plain,rr(i2003_11_14_17_22_31584,skolem0007(i2003_11_14_17_22_31584)),inference(resolution,[status(thm)],[c60, c0])).
% 0.50/0.66 cnf(c62,plain,~cUnsatisfiable(X79)|~rr(X79,X80)|cd(X80),inference(split_conjunct,[status(thm)],[c59])).
% 0.50/0.66 cnf(c108,plain,~cUnsatisfiable(i2003_11_14_17_22_31584)|cd(skolem0007(i2003_11_14_17_22_31584)),inference(resolution,[status(thm)],[c62, c104])).
% 0.50/0.66 cnf(c188,plain,cd(skolem0007(i2003_11_14_17_22_31584)),inference(resolution,[status(thm)],[c108, c0])).
% 0.50/0.66 cnf(c191,plain,ca_Cx4xcomp(skolem0007(i2003_11_14_17_22_31584)),inference(resolution,[status(thm)],[c188, c95])).
% 0.50/0.66 fof(axiom_9,axiom,(![X]:(ca_Cx4xcomp(X)<=>(~(?[Y]:ra_Px4(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.50/0.66 fof(c9,plain,(![X]:((~ca_Cx4xcomp(X)|(![Y]:~ra_Px4(X,Y)))&((?[Y]:ra_Px4(X,Y))|ca_Cx4xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.50/0.66 fof(c10,plain,((![X]:(~ca_Cx4xcomp(X)|(![Y]:~ra_Px4(X,Y))))&(![X]:((?[Y]:ra_Px4(X,Y))|ca_Cx4xcomp(X)))),inference(shift_quantors,[status(thm)],[c9])).
% 0.50/0.66 fof(c11,plain,((![X4]:(~ca_Cx4xcomp(X4)|(![X5]:~ra_Px4(X4,X5))))&(![X6]:((?[X7]:ra_Px4(X6,X7))|ca_Cx4xcomp(X6)))),inference(variable_rename,[status(thm)],[c10])).
% 0.50/0.66 fof(c13,plain,(![X4]:(![X5]:(![X6]:((~ca_Cx4xcomp(X4)|~ra_Px4(X4,X5))&(ra_Px4(X6,skolem0001(X6))|ca_Cx4xcomp(X6)))))),inference(shift_quantors,[status(thm)],[fof(c12,plain,((![X4]:(~ca_Cx4xcomp(X4)|(![X5]:~ra_Px4(X4,X5))))&(![X6]:(ra_Px4(X6,skolem0001(X6))|ca_Cx4xcomp(X6)))),inference(skolemize,[status(esa)],[c11])).])).
% 0.50/0.66 cnf(c14,plain,~ca_Cx4xcomp(X50)|~ra_Px4(X50,X51),inference(split_conjunct,[status(thm)],[c13])).
% 0.50/0.66 fof(axiom_8,axiom,(![X]:(ca_Cx4(X)<=>(?[Y0]:ra_Px4(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.50/0.66 fof(c16,plain,(![X]:((~ca_Cx4(X)|(?[Y0]:ra_Px4(X,Y0)))&((![Y0]:~ra_Px4(X,Y0))|ca_Cx4(X)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.50/0.66 fof(c17,plain,((![X]:(~ca_Cx4(X)|(?[Y0]:ra_Px4(X,Y0))))&(![X]:((![Y0]:~ra_Px4(X,Y0))|ca_Cx4(X)))),inference(shift_quantors,[status(thm)],[c16])).
% 0.50/0.66 fof(c18,plain,((![X8]:(~ca_Cx4(X8)|(?[X9]:ra_Px4(X8,X9))))&(![X10]:((![X11]:~ra_Px4(X10,X11))|ca_Cx4(X10)))),inference(variable_rename,[status(thm)],[c17])).
% 0.50/0.66 fof(c20,plain,(![X8]:(![X10]:(![X11]:((~ca_Cx4(X8)|ra_Px4(X8,skolem0002(X8)))&(~ra_Px4(X10,X11)|ca_Cx4(X10)))))),inference(shift_quantors,[status(thm)],[fof(c19,plain,((![X8]:(~ca_Cx4(X8)|ra_Px4(X8,skolem0002(X8))))&(![X10]:((![X11]:~ra_Px4(X10,X11))|ca_Cx4(X10)))),inference(skolemize,[status(esa)],[c18])).])).
% 0.50/0.66 cnf(c21,plain,~ca_Cx4(X59)|ra_Px4(X59,skolem0002(X59)),inference(split_conjunct,[status(thm)],[c20])).
% 0.50/0.66 cnf(c63,plain,~cUnsatisfiable(X86)|~rr(X86,X87)|ca_Cx4(X87),inference(split_conjunct,[status(thm)],[c59])).
% 0.50/0.66 cnf(c113,plain,~cUnsatisfiable(i2003_11_14_17_22_31584)|ca_Cx4(skolem0007(i2003_11_14_17_22_31584)),inference(resolution,[status(thm)],[c63, c104])).
% 0.50/0.66 cnf(c216,plain,ca_Cx4(skolem0007(i2003_11_14_17_22_31584)),inference(resolution,[status(thm)],[c113, c0])).
% 0.50/0.66 cnf(c217,plain,ra_Px4(skolem0007(i2003_11_14_17_22_31584),skolem0002(skolem0007(i2003_11_14_17_22_31584))),inference(resolution,[status(thm)],[c216, c21])).
% 0.50/0.66 cnf(c277,plain,~ca_Cx4xcomp(skolem0007(i2003_11_14_17_22_31584)),inference(resolution,[status(thm)],[c217, c14])).
% 0.50/0.66 cnf(c279,plain,$false,inference(resolution,[status(thm)],[c277, c191])).
% 0.50/0.66 % SZS output end CNFRefutation
% 0.50/0.66
% 0.50/0.66 % Initial clauses : 29
% 0.50/0.66 % Processed clauses : 89
% 0.50/0.66 % Factors computed : 0
% 0.50/0.66 % Resolvents computed: 203
% 0.50/0.66 % Tautologies deleted: 7
% 0.50/0.66 % Forward subsumed : 93
% 0.50/0.66 % Backward subsumed : 3
% 0.50/0.66 % -------- CPU Time ---------
% 0.50/0.66 % User time : 0.291 s
% 0.50/0.66 % System time : 0.019 s
% 0.50/0.66 % Total time : 0.310 s
%------------------------------------------------------------------------------