%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS099+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:42 EDT 2024
% Result : Unsatisfiable 0.52s 0.68s
% Output : Refutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : KRS099+1 : TPTP v8.1.2. Released v3.1.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n013.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 00:07:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.52/0.68 % Version: 1.5
% 0.52/0.68 % SZS status Unsatisfiable
% 0.52/0.68 % SZS output start CNFRefutation
% 0.52/0.68 fof(axiom_5,axiom,cUnsatisfiable(i2003_11_14_17_20_29215),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.52/0.68 cnf(c9,plain,cUnsatisfiable(i2003_11_14_17_20_29215),inference(split_conjunct,[status(thm)],[axiom_5])).
% 0.52/0.68 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((((?[Y0]:(?[Y1]:(?[Y2]:(((((rtt(X,Y0)&rtt(X,Y1))&rtt(X,Y2))&Y0!=Y1)&Y0!=Y2)&Y1!=Y2))))&(![Y]:(rtt(X,Y)=>ca(Y))))&(![Y0]:(![Y1]:((rtt(X,Y0)&rtt(X,Y1))=>Y0=Y1))))&(![Y0]:(![Y1]:((rtt(X,Y0)&rtt(X,Y1))=>Y0=Y1)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.52/0.68 fof(c17,plain,(![X]:((~cUnsatisfiable(X)|((((?[Y0]:(?[Y1]:(?[Y2]:(((((rtt(X,Y0)&rtt(X,Y1))&rtt(X,Y2))&Y0!=Y1)&Y0!=Y2)&Y1!=Y2))))&(![Y]:(~rtt(X,Y)|ca(Y))))&(![Y0]:(![Y1]:((~rtt(X,Y0)|~rtt(X,Y1))|Y0=Y1))))&(![Y0]:(![Y1]:((~rtt(X,Y0)|~rtt(X,Y1))|Y0=Y1)))))&(((((![Y0]:(![Y1]:(![Y2]:(((((~rtt(X,Y0)|~rtt(X,Y1))|~rtt(X,Y2))|Y0=Y1)|Y0=Y2)|Y1=Y2))))|(?[Y]:(rtt(X,Y)&~ca(Y))))|(?[Y0]:(?[Y1]:((rtt(X,Y0)&rtt(X,Y1))&Y0!=Y1))))|(?[Y0]:(?[Y1]:((rtt(X,Y0)&rtt(X,Y1))&Y0!=Y1))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.52/0.68 fof(c18,plain,((![X]:(~cUnsatisfiable(X)|((((?[Y0]:(?[Y1]:(?[Y2]:(((((rtt(X,Y0)&rtt(X,Y1))&rtt(X,Y2))&Y0!=Y1)&Y0!=Y2)&Y1!=Y2))))&(![Y]:(~rtt(X,Y)|ca(Y))))&(![Y0]:(![Y1]:((~rtt(X,Y0)|~rtt(X,Y1))|Y0=Y1))))&(![Y0]:(![Y1]:((~rtt(X,Y0)|~rtt(X,Y1))|Y0=Y1))))))&(![X]:(((((![Y0]:(![Y1]:(![Y2]:(((((~rtt(X,Y0)|~rtt(X,Y1))|~rtt(X,Y2))|Y0=Y1)|Y0=Y2)|Y1=Y2))))|(?[Y]:(rtt(X,Y)&~ca(Y))))|(?[Y0]:(?[Y1]:((rtt(X,Y0)&rtt(X,Y1))&Y0!=Y1))))|(?[Y0]:(?[Y1]:((rtt(X,Y0)&rtt(X,Y1))&Y0!=Y1))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c17])).
% 0.52/0.68 fof(c19,plain,((![X4]:(~cUnsatisfiable(X4)|((((?[X5]:(?[X6]:(?[X7]:(((((rtt(X4,X5)&rtt(X4,X6))&rtt(X4,X7))&X5!=X6)&X5!=X7)&X6!=X7))))&(![X8]:(~rtt(X4,X8)|ca(X8))))&(![X9]:(![X10]:((~rtt(X4,X9)|~rtt(X4,X10))|X9=X10))))&(![X11]:(![X12]:((~rtt(X4,X11)|~rtt(X4,X12))|X11=X12))))))&(![X13]:(((((![X14]:(![X15]:(![X16]:(((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16))))|(?[X17]:(rtt(X13,X17)&~ca(X17))))|(?[X18]:(?[X19]:((rtt(X13,X18)&rtt(X13,X19))&X18!=X19))))|(?[X20]:(?[X21]:((rtt(X13,X20)&rtt(X13,X21))&X20!=X21))))|cUnsatisfiable(X13)))),inference(variable_rename,[status(thm)],[c18])).
% 0.52/0.68 fof(c21,plain,(![X4]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((~cUnsatisfiable(X4)|((((((((rtt(X4,skolem0001(X4))&rtt(X4,skolem0002(X4)))&rtt(X4,skolem0003(X4)))&skolem0001(X4)!=skolem0002(X4))&skolem0001(X4)!=skolem0003(X4))&skolem0002(X4)!=skolem0003(X4))&(~rtt(X4,X8)|ca(X8)))&((~rtt(X4,X9)|~rtt(X4,X10))|X9=X10))&((~rtt(X4,X11)|~rtt(X4,X12))|X11=X12)))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|(rtt(X13,skolem0004(X13))&~ca(skolem0004(X13))))|((rtt(X13,skolem0005(X13))&rtt(X13,skolem0006(X13)))&skolem0005(X13)!=skolem0006(X13)))|((rtt(X13,skolem0007(X13))&rtt(X13,skolem0008(X13)))&skolem0007(X13)!=skolem0008(X13)))|cUnsatisfiable(X13))))))))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((![X4]:(~cUnsatisfiable(X4)|((((((((rtt(X4,skolem0001(X4))&rtt(X4,skolem0002(X4)))&rtt(X4,skolem0003(X4)))&skolem0001(X4)!=skolem0002(X4))&skolem0001(X4)!=skolem0003(X4))&skolem0002(X4)!=skolem0003(X4))&(![X8]:(~rtt(X4,X8)|ca(X8))))&(![X9]:(![X10]:((~rtt(X4,X9)|~rtt(X4,X10))|X9=X10))))&(![X11]:(![X12]:((~rtt(X4,X11)|~rtt(X4,X12))|X11=X12))))))&(![X13]:(((((![X14]:(![X15]:(![X16]:(((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16))))|(rtt(X13,skolem0004(X13))&~ca(skolem0004(X13))))|((rtt(X13,skolem0005(X13))&rtt(X13,skolem0006(X13)))&skolem0005(X13)!=skolem0006(X13)))|((rtt(X13,skolem0007(X13))&rtt(X13,skolem0008(X13)))&skolem0007(X13)!=skolem0008(X13)))|cUnsatisfiable(X13)))),inference(skolemize,[status(esa)],[c19])).])).
% 0.52/0.68 fof(c22,plain,(![X4]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((((((((((~cUnsatisfiable(X4)|rtt(X4,skolem0001(X4)))&(~cUnsatisfiable(X4)|rtt(X4,skolem0002(X4))))&(~cUnsatisfiable(X4)|rtt(X4,skolem0003(X4))))&(~cUnsatisfiable(X4)|skolem0001(X4)!=skolem0002(X4)))&(~cUnsatisfiable(X4)|skolem0001(X4)!=skolem0003(X4)))&(~cUnsatisfiable(X4)|skolem0002(X4)!=skolem0003(X4)))&(~cUnsatisfiable(X4)|(~rtt(X4,X8)|ca(X8))))&(~cUnsatisfiable(X4)|((~rtt(X4,X9)|~rtt(X4,X10))|X9=X10)))&(~cUnsatisfiable(X4)|((~rtt(X4,X11)|~rtt(X4,X12))|X11=X12)))&((((((((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|rtt(X13,skolem0004(X13)))|rtt(X13,skolem0005(X13)))|rtt(X13,skolem0007(X13)))|cUnsatisfiable(X13))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|rtt(X13,skolem0004(X13)))|rtt(X13,skolem0005(X13)))|rtt(X13,skolem0008(X13)))|cUnsatisfiable(X13)))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|rtt(X13,skolem0004(X13)))|rtt(X13,skolem0005(X13)))|skolem0007(X13)!=skolem0008(X13))|cUnsatisfiable(X13)))&(((((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|rtt(X13,skolem0004(X13)))|rtt(X13,skolem0006(X13)))|rtt(X13,skolem0007(X13)))|cUnsatisfiable(X13))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|rtt(X13,skolem0004(X13)))|rtt(X13,skolem0006(X13)))|rtt(X13,skolem0008(X13)))|cUnsatisfiable(X13)))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|rtt(X13,skolem0004(X13)))|rtt(X13,skolem0006(X13)))|skolem0007(X13)!=skolem0008(X13))|cUnsatisfiable(X13))))&(((((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|rtt(X13,skolem0004(X13)))|skolem0005(X13)!=skolem0006(X13))|rtt(X13,skolem0007(X13)))|cUnsatisfiable(X13))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|rtt(X13,skolem0004(X13)))|skolem0005(X13)!=skolem0006(X13))|rtt(X13,skolem0008(X13)))|cUnsatisfiable(X13)))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|rtt(X13,skolem0004(X13)))|skolem0005(X13)!=skolem0006(X13))|skolem0007(X13)!=skolem0008(X13))|cUnsatisfiable(X13))))&(((((((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|~ca(skolem0004(X13)))|rtt(X13,skolem0005(X13)))|rtt(X13,skolem0007(X13)))|cUnsatisfiable(X13))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|~ca(skolem0004(X13)))|rtt(X13,skolem0005(X13)))|rtt(X13,skolem0008(X13)))|cUnsatisfiable(X13)))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|~ca(skolem0004(X13)))|rtt(X13,skolem0005(X13)))|skolem0007(X13)!=skolem0008(X13))|cUnsatisfiable(X13)))&(((((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|~ca(skolem0004(X13)))|rtt(X13,skolem0006(X13)))|rtt(X13,skolem0007(X13)))|cUnsatisfiable(X13))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|~ca(skolem0004(X13)))|rtt(X13,skolem0006(X13)))|rtt(X13,skolem0008(X13)))|cUnsatisfiable(X13)))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|~ca(skolem0004(X13)))|rtt(X13,skolem0006(X13)))|skolem0007(X13)!=skolem0008(X13))|cUnsatisfiable(X13))))&(((((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|~ca(skolem0004(X13)))|skolem0005(X13)!=skolem0006(X13))|rtt(X13,skolem0007(X13)))|cUnsatisfiable(X13))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|~ca(skolem0004(X13)))|skolem0005(X13)!=skolem0006(X13))|rtt(X13,skolem0008(X13)))|cUnsatisfiable(X13)))&(((((((((~rtt(X13,X14)|~rtt(X13,X15))|~rtt(X13,X16))|X14=X15)|X14=X16)|X15=X16)|~ca(skolem0004(X13)))|skolem0005(X13)!=skolem0006(X13))|skolem0007(X13)!=skolem0008(X13))|cUnsatisfiable(X13)))))))))))))))),inference(distribute,[status(thm)],[c21])).
% 0.52/0.68 cnf(c27,plain,~cUnsatisfiable(X113)|skolem0001(X113)!=skolem0003(X113),inference(split_conjunct,[status(thm)],[c22])).
% 0.52/0.68 cnf(symmetry,axiom,X52!=X53|X53=X52,theory(equality)).
% 0.52/0.68 cnf(c25,plain,~cUnsatisfiable(X70)|rtt(X70,skolem0003(X70)),inference(split_conjunct,[status(thm)],[c22])).
% 0.52/0.68 cnf(c100,plain,rtt(i2003_11_14_17_20_29215,skolem0003(i2003_11_14_17_20_29215)),inference(resolution,[status(thm)],[c25, c9])).
% 0.52/0.68 cnf(c23,plain,~cUnsatisfiable(X65)|rtt(X65,skolem0001(X65)),inference(split_conjunct,[status(thm)],[c22])).
% 0.52/0.68 cnf(c97,plain,rtt(i2003_11_14_17_20_29215,skolem0001(i2003_11_14_17_20_29215)),inference(resolution,[status(thm)],[c23, c9])).
% 0.52/0.68 cnf(c30,plain,~cUnsatisfiable(X116)|~rtt(X116,X115)|~rtt(X116,X117)|X115=X117,inference(split_conjunct,[status(thm)],[c22])).
% 0.52/0.68 cnf(c119,plain,~cUnsatisfiable(i2003_11_14_17_20_29215)|~rtt(i2003_11_14_17_20_29215,X160)|X160=skolem0001(i2003_11_14_17_20_29215),inference(resolution,[status(thm)],[c30, c97])).
% 0.52/0.68 cnf(c156,plain,~cUnsatisfiable(i2003_11_14_17_20_29215)|skolem0003(i2003_11_14_17_20_29215)=skolem0001(i2003_11_14_17_20_29215),inference(resolution,[status(thm)],[c119, c100])).
% 0.52/0.68 cnf(c158,plain,skolem0003(i2003_11_14_17_20_29215)=skolem0001(i2003_11_14_17_20_29215),inference(resolution,[status(thm)],[c156, c9])).
% 0.52/0.68 cnf(c171,plain,skolem0001(i2003_11_14_17_20_29215)=skolem0003(i2003_11_14_17_20_29215),inference(resolution,[status(thm)],[c158, symmetry])).
% 0.52/0.68 cnf(c179,plain,~cUnsatisfiable(i2003_11_14_17_20_29215),inference(resolution,[status(thm)],[c171, c27])).
% 0.52/0.68 cnf(c185,plain,$false,inference(resolution,[status(thm)],[c179, c9])).
% 0.52/0.68 % SZS output end CNFRefutation
% 0.52/0.68
% 0.52/0.68 % Initial clauses : 56
% 0.52/0.68 % Processed clauses : 58
% 0.52/0.68 % Factors computed : 10
% 0.52/0.68 % Resolvents computed: 83
% 0.52/0.68 % Tautologies deleted: 12
% 0.52/0.68 % Forward subsumed : 24
% 0.52/0.68 % Backward subsumed : 5
% 0.52/0.68 % -------- CPU Time ---------
% 0.52/0.68 % User time : 0.291 s
% 0.52/0.68 % System time : 0.025 s
% 0.52/0.68 % Total time : 0.316 s
%------------------------------------------------------------------------------