%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS127+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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.41s 0.60s
% Output : Refutation 0.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.13 % Problem : KRS127+1 : TPTP v8.1.2. Released v3.1.0.
% 0.13/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n016.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 00:06:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.41/0.60 % Version: 1.5
% 0.41/0.60 % SZS status Unsatisfiable
% 0.41/0.60 % SZS output start CNFRefutation
% 0.41/0.60 fof(axiom_4,axiom,(![X]:(cd(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.41/0.60 fof(c18,plain,(![X]:((~cd(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cd(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.41/0.60 fof(c19,plain,((![X]:(~cd(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cd(X)))),inference(shift_quantors,[status(thm)],[c18])).
% 0.41/0.60 fof(c20,plain,((![X6]:(~cd(X6)|(![X7]:~ra_Px1(X6,X7))))&(![X8]:((?[X9]:ra_Px1(X8,X9))|cd(X8)))),inference(variable_rename,[status(thm)],[c19])).
% 0.41/0.60 fof(c22,plain,(![X6]:(![X7]:(![X8]:((~cd(X6)|~ra_Px1(X6,X7))&(ra_Px1(X8,skolem0002(X8))|cd(X8)))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,((![X6]:(~cd(X6)|(![X7]:~ra_Px1(X6,X7))))&(![X8]:(ra_Px1(X8,skolem0002(X8))|cd(X8)))),inference(skolemize,[status(esa)],[c20])).])).
% 0.41/0.60 cnf(c23,plain,~cd(X69)|~ra_Px1(X69,X68),inference(split_conjunct,[status(thm)],[c22])).
% 0.41/0.60 fof(axiom_3,axiom,(![X]:(cc(X)=>cdxcomp(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.41/0.60 fof(c25,plain,(![X]:(~cc(X)|cdxcomp(X))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.41/0.60 fof(c26,plain,(![X10]:(~cc(X10)|cdxcomp(X10))),inference(variable_rename,[status(thm)],[c25])).
% 0.41/0.60 cnf(c27,plain,~cc(X56)|cdxcomp(X56),inference(split_conjunct,[status(thm)],[c26])).
% 0.41/0.60 fof(axiom_6,axiom,cUnsatisfiable(i2003_11_14_17_22_27794),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.41/0.60 cnf(c10,plain,cUnsatisfiable(i2003_11_14_17_22_27794),inference(split_conjunct,[status(thm)],[axiom_6])).
% 0.41/0.60 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((?[Y]:(rr(X,Y)&cc(Y)))&(?[Y]:(rr(X,Y)&cd(Y))))&(![Y0]:(![Y1]:((rr(X,Y0)&rr(X,Y1))=>Y0=Y1)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.41/0.60 fof(c28,plain,(![X]:((~cUnsatisfiable(X)|(((?[Y]:(rr(X,Y)&cc(Y)))&(?[Y]:(rr(X,Y)&cd(Y))))&(![Y0]:(![Y1]:((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1)))))&((((![Y]:(~rr(X,Y)|~cc(Y)))|(![Y]:(~rr(X,Y)|~cd(Y))))|(?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.41/0.60 fof(c29,plain,((![X]:(~cUnsatisfiable(X)|(((?[Y]:(rr(X,Y)&cc(Y)))&(?[Y]:(rr(X,Y)&cd(Y))))&(![Y0]:(![Y1]:((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1))))))&(![X]:((((![Y]:(~rr(X,Y)|~cc(Y)))|(![Y]:(~rr(X,Y)|~cd(Y))))|(?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c28])).
% 0.41/0.60 fof(c30,plain,((![X11]:(~cUnsatisfiable(X11)|(((?[X12]:(rr(X11,X12)&cc(X12)))&(?[X13]:(rr(X11,X13)&cd(X13))))&(![X14]:(![X15]:((~rr(X11,X14)|~rr(X11,X15))|X14=X15))))))&(![X16]:((((![X17]:(~rr(X16,X17)|~cc(X17)))|(![X18]:(~rr(X16,X18)|~cd(X18))))|(?[X19]:(?[X20]:((rr(X16,X19)&rr(X16,X20))&X19!=X20))))|cUnsatisfiable(X16)))),inference(variable_rename,[status(thm)],[c29])).
% 0.41/0.60 fof(c32,plain,(![X11]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:((~cUnsatisfiable(X11)|(((rr(X11,skolem0003(X11))&cc(skolem0003(X11)))&(rr(X11,skolem0004(X11))&cd(skolem0004(X11))))&((~rr(X11,X14)|~rr(X11,X15))|X14=X15)))&((((~rr(X16,X17)|~cc(X17))|(~rr(X16,X18)|~cd(X18)))|((rr(X16,skolem0005(X16))&rr(X16,skolem0006(X16)))&skolem0005(X16)!=skolem0006(X16)))|cUnsatisfiable(X16))))))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,((![X11]:(~cUnsatisfiable(X11)|(((rr(X11,skolem0003(X11))&cc(skolem0003(X11)))&(rr(X11,skolem0004(X11))&cd(skolem0004(X11))))&(![X14]:(![X15]:((~rr(X11,X14)|~rr(X11,X15))|X14=X15))))))&(![X16]:((((![X17]:(~rr(X16,X17)|~cc(X17)))|(![X18]:(~rr(X16,X18)|~cd(X18))))|((rr(X16,skolem0005(X16))&rr(X16,skolem0006(X16)))&skolem0005(X16)!=skolem0006(X16)))|cUnsatisfiable(X16)))),inference(skolemize,[status(esa)],[c30])).])).
% 0.41/0.60 fof(c33,plain,(![X11]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(((((~cUnsatisfiable(X11)|rr(X11,skolem0003(X11)))&(~cUnsatisfiable(X11)|cc(skolem0003(X11))))&((~cUnsatisfiable(X11)|rr(X11,skolem0004(X11)))&(~cUnsatisfiable(X11)|cd(skolem0004(X11)))))&(~cUnsatisfiable(X11)|((~rr(X11,X14)|~rr(X11,X15))|X14=X15)))&((((((~rr(X16,X17)|~cc(X17))|(~rr(X16,X18)|~cd(X18)))|rr(X16,skolem0005(X16)))|cUnsatisfiable(X16))&((((~rr(X16,X17)|~cc(X17))|(~rr(X16,X18)|~cd(X18)))|rr(X16,skolem0006(X16)))|cUnsatisfiable(X16)))&((((~rr(X16,X17)|~cc(X17))|(~rr(X16,X18)|~cd(X18)))|skolem0005(X16)!=skolem0006(X16))|cUnsatisfiable(X16)))))))))),inference(distribute,[status(thm)],[c32])).
% 0.41/0.60 cnf(c35,plain,~cUnsatisfiable(X70)|cc(skolem0003(X70)),inference(split_conjunct,[status(thm)],[c33])).
% 0.41/0.60 cnf(c95,plain,cc(skolem0003(i2003_11_14_17_22_27794)),inference(resolution,[status(thm)],[c35, c10])).
% 0.41/0.60 cnf(c96,plain,cdxcomp(skolem0003(i2003_11_14_17_22_27794)),inference(resolution,[status(thm)],[c95, c27])).
% 0.41/0.60 fof(axiom_5,axiom,(![X]:(cdxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.41/0.60 fof(c11,plain,(![X]:((~cdxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cdxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.41/0.60 fof(c12,plain,((![X]:(~cdxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cdxcomp(X)))),inference(shift_quantors,[status(thm)],[c11])).
% 0.41/0.60 fof(c13,plain,((![X2]:(~cdxcomp(X2)|(?[X3]:ra_Px1(X2,X3))))&(![X4]:((![X5]:~ra_Px1(X4,X5))|cdxcomp(X4)))),inference(variable_rename,[status(thm)],[c12])).
% 0.41/0.60 fof(c15,plain,(![X2]:(![X4]:(![X5]:((~cdxcomp(X2)|ra_Px1(X2,skolem0001(X2)))&(~ra_Px1(X4,X5)|cdxcomp(X4)))))),inference(shift_quantors,[status(thm)],[fof(c14,plain,((![X2]:(~cdxcomp(X2)|ra_Px1(X2,skolem0001(X2))))&(![X4]:((![X5]:~ra_Px1(X4,X5))|cdxcomp(X4)))),inference(skolemize,[status(esa)],[c13])).])).
% 0.41/0.60 cnf(c16,plain,~cdxcomp(X78)|ra_Px1(X78,skolem0001(X78)),inference(split_conjunct,[status(thm)],[c15])).
% 0.41/0.60 cnf(c99,plain,ra_Px1(skolem0003(i2003_11_14_17_22_27794),skolem0001(skolem0003(i2003_11_14_17_22_27794))),inference(resolution,[status(thm)],[c16, c96])).
% 0.41/0.60 cnf(c134,plain,~cd(skolem0003(i2003_11_14_17_22_27794)),inference(resolution,[status(thm)],[c99, c23])).
% 0.41/0.60 cnf(c37,plain,~cUnsatisfiable(X71)|cd(skolem0004(X71)),inference(split_conjunct,[status(thm)],[c33])).
% 0.41/0.60 cnf(c97,plain,cd(skolem0004(i2003_11_14_17_22_27794)),inference(resolution,[status(thm)],[c37, c10])).
% 0.41/0.60 cnf(c2,axiom,X87!=X86|~cd(X87)|cd(X86),theory(equality)).
% 0.41/0.60 cnf(symmetry,axiom,X57!=X58|X58=X57,theory(equality)).
% 0.41/0.60 cnf(c34,plain,~cUnsatisfiable(X85)|rr(X85,skolem0003(X85)),inference(split_conjunct,[status(thm)],[c33])).
% 0.41/0.60 cnf(c104,plain,rr(i2003_11_14_17_22_27794,skolem0003(i2003_11_14_17_22_27794)),inference(resolution,[status(thm)],[c34, c10])).
% 0.41/0.60 cnf(c36,plain,~cUnsatisfiable(X89)|rr(X89,skolem0004(X89)),inference(split_conjunct,[status(thm)],[c33])).
% 0.41/0.60 cnf(c106,plain,rr(i2003_11_14_17_22_27794,skolem0004(i2003_11_14_17_22_27794)),inference(resolution,[status(thm)],[c36, c10])).
% 0.41/0.60 cnf(c38,plain,~cUnsatisfiable(X126)|~rr(X126,X127)|~rr(X126,X128)|X127=X128,inference(split_conjunct,[status(thm)],[c33])).
% 0.41/0.60 cnf(c117,plain,~cUnsatisfiable(i2003_11_14_17_22_27794)|~rr(i2003_11_14_17_22_27794,X187)|X187=skolem0004(i2003_11_14_17_22_27794),inference(resolution,[status(thm)],[c38, c106])).
% 0.41/0.60 cnf(c159,plain,~cUnsatisfiable(i2003_11_14_17_22_27794)|skolem0003(i2003_11_14_17_22_27794)=skolem0004(i2003_11_14_17_22_27794),inference(resolution,[status(thm)],[c117, c104])).
% 0.41/0.60 cnf(c160,plain,skolem0003(i2003_11_14_17_22_27794)=skolem0004(i2003_11_14_17_22_27794),inference(resolution,[status(thm)],[c159, c10])).
% 0.41/0.60 cnf(c167,plain,skolem0004(i2003_11_14_17_22_27794)=skolem0003(i2003_11_14_17_22_27794),inference(resolution,[status(thm)],[c160, symmetry])).
% 0.41/0.60 cnf(c185,plain,~cd(skolem0004(i2003_11_14_17_22_27794))|cd(skolem0003(i2003_11_14_17_22_27794)),inference(resolution,[status(thm)],[c167, c2])).
% 0.41/0.60 cnf(c199,plain,cd(skolem0003(i2003_11_14_17_22_27794)),inference(resolution,[status(thm)],[c185, c97])).
% 0.41/0.60 cnf(c202,plain,$false,inference(resolution,[status(thm)],[c199, c134])).
% 0.41/0.60 % SZS output end CNFRefutation
% 0.41/0.60
% 0.41/0.60 % Initial clauses : 43
% 0.41/0.60 % Processed clauses : 74
% 0.41/0.60 % Factors computed : 4
% 0.41/0.60 % Resolvents computed: 109
% 0.41/0.60 % Tautologies deleted: 11
% 0.41/0.60 % Forward subsumed : 41
% 0.41/0.60 % Backward subsumed : 4
% 0.41/0.60 % -------- CPU Time ---------
% 0.41/0.60 % User time : 0.239 s
% 0.41/0.60 % System time : 0.012 s
% 0.41/0.60 % Total time : 0.251 s
%------------------------------------------------------------------------------