%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS113+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:44 EDT 2024
% Result : Unsatisfiable 0.48s 0.72s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : KRS113+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 : n029.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:08:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.48/0.72 % Version: 1.5
% 0.48/0.72 % SZS status Unsatisfiable
% 0.48/0.72 % SZS output start CNFRefutation
% 0.48/0.72 fof(axiom_3,axiom,(![X]:(cp(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.48/0.72 fof(c38,plain,(![X]:((~cp(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.48/0.72 fof(c39,plain,((![X]:(~cp(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cp(X)))),inference(shift_quantors,[status(thm)],[c38])).
% 0.48/0.72 fof(c40,plain,((![X16]:(~cp(X16)|(![X17]:~ra_Px1(X16,X17))))&(![X18]:((?[X19]:ra_Px1(X18,X19))|cp(X18)))),inference(variable_rename,[status(thm)],[c39])).
% 0.48/0.72 fof(c42,plain,(![X16]:(![X17]:(![X18]:((~cp(X16)|~ra_Px1(X16,X17))&(ra_Px1(X18,skolem0003(X18))|cp(X18)))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,((![X16]:(~cp(X16)|(![X17]:~ra_Px1(X16,X17))))&(![X18]:(ra_Px1(X18,skolem0003(X18))|cp(X18)))),inference(skolemize,[status(esa)],[c40])).])).
% 0.48/0.72 cnf(c43,plain,~cp(X89)|~ra_Px1(X89,X90),inference(split_conjunct,[status(thm)],[c42])).
% 0.48/0.72 fof(axiom_7,axiom,cUnsatisfiable(i2003_11_14_17_21_22376),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.48/0.72 cnf(c15,plain,cUnsatisfiable(i2003_11_14_17_21_22376),inference(split_conjunct,[status(thm)],[axiom_7])).
% 0.48/0.72 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((((![Y0]:(![Y1]:((rr(X,Y0)&rr(X,Y1))=>Y0=Y1)))&(?[Y]:(rr(X,Y)&ca_Vx2(Y))))&(?[Y]:(rs(X,Y)&cp(Y))))&cpxcomp(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.48/0.72 fof(c45,plain,(![X]:((~cUnsatisfiable(X)|((((![Y0]:(![Y1]:((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1)))&(?[Y]:(rr(X,Y)&ca_Vx2(Y))))&(?[Y]:(rs(X,Y)&cp(Y))))&cpxcomp(X)))&(((((?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1)))|(![Y]:(~rr(X,Y)|~ca_Vx2(Y))))|(![Y]:(~rs(X,Y)|~cp(Y))))|~cpxcomp(X))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.48/0.72 fof(c46,plain,((![X]:(~cUnsatisfiable(X)|((((![Y0]:(![Y1]:((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1)))&(?[Y]:(rr(X,Y)&ca_Vx2(Y))))&(?[Y]:(rs(X,Y)&cp(Y))))&cpxcomp(X))))&(![X]:(((((?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1)))|(![Y]:(~rr(X,Y)|~ca_Vx2(Y))))|(![Y]:(~rs(X,Y)|~cp(Y))))|~cpxcomp(X))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c45])).
% 0.48/0.72 fof(c47,plain,((![X20]:(~cUnsatisfiable(X20)|((((![X21]:(![X22]:((~rr(X20,X21)|~rr(X20,X22))|X21=X22)))&(?[X23]:(rr(X20,X23)&ca_Vx2(X23))))&(?[X24]:(rs(X20,X24)&cp(X24))))&cpxcomp(X20))))&(![X25]:(((((?[X26]:(?[X27]:((rr(X25,X26)&rr(X25,X27))&X26!=X27)))|(![X28]:(~rr(X25,X28)|~ca_Vx2(X28))))|(![X29]:(~rs(X25,X29)|~cp(X29))))|~cpxcomp(X25))|cUnsatisfiable(X25)))),inference(variable_rename,[status(thm)],[c46])).
% 0.48/0.72 fof(c49,plain,(![X20]:(![X21]:(![X22]:(![X25]:(![X28]:(![X29]:((~cUnsatisfiable(X20)|(((((~rr(X20,X21)|~rr(X20,X22))|X21=X22)&(rr(X20,skolem0004(X20))&ca_Vx2(skolem0004(X20))))&(rs(X20,skolem0005(X20))&cp(skolem0005(X20))))&cpxcomp(X20)))&((((((rr(X25,skolem0006(X25))&rr(X25,skolem0007(X25)))&skolem0006(X25)!=skolem0007(X25))|(~rr(X25,X28)|~ca_Vx2(X28)))|(~rs(X25,X29)|~cp(X29)))|~cpxcomp(X25))|cUnsatisfiable(X25))))))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,((![X20]:(~cUnsatisfiable(X20)|((((![X21]:(![X22]:((~rr(X20,X21)|~rr(X20,X22))|X21=X22)))&(rr(X20,skolem0004(X20))&ca_Vx2(skolem0004(X20))))&(rs(X20,skolem0005(X20))&cp(skolem0005(X20))))&cpxcomp(X20))))&(![X25]:((((((rr(X25,skolem0006(X25))&rr(X25,skolem0007(X25)))&skolem0006(X25)!=skolem0007(X25))|(![X28]:(~rr(X25,X28)|~ca_Vx2(X28))))|(![X29]:(~rs(X25,X29)|~cp(X29))))|~cpxcomp(X25))|cUnsatisfiable(X25)))),inference(skolemize,[status(esa)],[c47])).])).
% 0.48/0.72 fof(c50,plain,(![X20]:(![X21]:(![X22]:(![X25]:(![X28]:(![X29]:(((((~cUnsatisfiable(X20)|((~rr(X20,X21)|~rr(X20,X22))|X21=X22))&((~cUnsatisfiable(X20)|rr(X20,skolem0004(X20)))&(~cUnsatisfiable(X20)|ca_Vx2(skolem0004(X20)))))&((~cUnsatisfiable(X20)|rs(X20,skolem0005(X20)))&(~cUnsatisfiable(X20)|cp(skolem0005(X20)))))&(~cUnsatisfiable(X20)|cpxcomp(X20)))&((((((rr(X25,skolem0006(X25))|(~rr(X25,X28)|~ca_Vx2(X28)))|(~rs(X25,X29)|~cp(X29)))|~cpxcomp(X25))|cUnsatisfiable(X25))&((((rr(X25,skolem0007(X25))|(~rr(X25,X28)|~ca_Vx2(X28)))|(~rs(X25,X29)|~cp(X29)))|~cpxcomp(X25))|cUnsatisfiable(X25)))&((((skolem0006(X25)!=skolem0007(X25)|(~rr(X25,X28)|~ca_Vx2(X28)))|(~rs(X25,X29)|~cp(X29)))|~cpxcomp(X25))|cUnsatisfiable(X25)))))))))),inference(distribute,[status(thm)],[c49])).
% 0.48/0.72 cnf(c56,plain,~cUnsatisfiable(X77)|cpxcomp(X77),inference(split_conjunct,[status(thm)],[c50])).
% 0.48/0.72 cnf(c121,plain,cpxcomp(i2003_11_14_17_21_22376),inference(resolution,[status(thm)],[c56, c15])).
% 0.48/0.72 fof(axiom_4,axiom,(![X]:(cpxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.48/0.72 fof(c31,plain,(![X]:((~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.48/0.72 fof(c32,plain,((![X]:(~cpxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cpxcomp(X)))),inference(shift_quantors,[status(thm)],[c31])).
% 0.48/0.72 fof(c33,plain,((![X12]:(~cpxcomp(X12)|(?[X13]:ra_Px1(X12,X13))))&(![X14]:((![X15]:~ra_Px1(X14,X15))|cpxcomp(X14)))),inference(variable_rename,[status(thm)],[c32])).
% 0.48/0.72 fof(c35,plain,(![X12]:(![X14]:(![X15]:((~cpxcomp(X12)|ra_Px1(X12,skolem0002(X12)))&(~ra_Px1(X14,X15)|cpxcomp(X14)))))),inference(shift_quantors,[status(thm)],[fof(c34,plain,((![X12]:(~cpxcomp(X12)|ra_Px1(X12,skolem0002(X12))))&(![X14]:((![X15]:~ra_Px1(X14,X15))|cpxcomp(X14)))),inference(skolemize,[status(esa)],[c33])).])).
% 0.48/0.72 cnf(c36,plain,~cpxcomp(X112)|ra_Px1(X112,skolem0002(X112)),inference(split_conjunct,[status(thm)],[c35])).
% 0.48/0.72 cnf(c131,plain,ra_Px1(i2003_11_14_17_21_22376,skolem0002(i2003_11_14_17_21_22376)),inference(resolution,[status(thm)],[c36, c121])).
% 0.48/0.72 cnf(c133,plain,~cp(i2003_11_14_17_21_22376),inference(resolution,[status(thm)],[c131, c43])).
% 0.48/0.72 cnf(c53,plain,~cUnsatisfiable(X101)|ca_Vx2(skolem0004(X101)),inference(split_conjunct,[status(thm)],[c50])).
% 0.48/0.72 cnf(c127,plain,ca_Vx2(skolem0004(i2003_11_14_17_21_22376)),inference(resolution,[status(thm)],[c53, c15])).
% 0.48/0.72 fof(axiom_5,axiom,(![X]:(ca_Vx2(X)<=>(![Y]:(rinvS(X,Y)=>cp(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.48/0.72 fof(c22,plain,(![X]:((~ca_Vx2(X)|(![Y]:(~rinvS(X,Y)|cp(Y))))&((?[Y]:(rinvS(X,Y)&~cp(Y)))|ca_Vx2(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.48/0.72 fof(c23,plain,((![X]:(~ca_Vx2(X)|(![Y]:(~rinvS(X,Y)|cp(Y)))))&(![X]:((?[Y]:(rinvS(X,Y)&~cp(Y)))|ca_Vx2(X)))),inference(shift_quantors,[status(thm)],[c22])).
% 0.48/0.72 fof(c24,plain,((![X8]:(~ca_Vx2(X8)|(![X9]:(~rinvS(X8,X9)|cp(X9)))))&(![X10]:((?[X11]:(rinvS(X10,X11)&~cp(X11)))|ca_Vx2(X10)))),inference(variable_rename,[status(thm)],[c23])).
% 0.48/0.72 fof(c26,plain,(![X8]:(![X9]:(![X10]:((~ca_Vx2(X8)|(~rinvS(X8,X9)|cp(X9)))&((rinvS(X10,skolem0001(X10))&~cp(skolem0001(X10)))|ca_Vx2(X10)))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,((![X8]:(~ca_Vx2(X8)|(![X9]:(~rinvS(X8,X9)|cp(X9)))))&(![X10]:((rinvS(X10,skolem0001(X10))&~cp(skolem0001(X10)))|ca_Vx2(X10)))),inference(skolemize,[status(esa)],[c24])).])).
% 0.48/0.72 fof(c27,plain,(![X8]:(![X9]:(![X10]:((~ca_Vx2(X8)|(~rinvS(X8,X9)|cp(X9)))&((rinvS(X10,skolem0001(X10))|ca_Vx2(X10))&(~cp(skolem0001(X10))|ca_Vx2(X10))))))),inference(distribute,[status(thm)],[c26])).
% 0.48/0.72 cnf(c28,plain,~ca_Vx2(X151)|~rinvS(X151,X152)|cp(X152),inference(split_conjunct,[status(thm)],[c27])).
% 0.48/0.72 fof(axiom_6,axiom,(![X]:(![Y]:(rinvS(X,Y)<=>rs(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.48/0.72 fof(c16,plain,(![X]:(![Y]:((~rinvS(X,Y)|rs(Y,X))&(~rs(Y,X)|rinvS(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.48/0.72 fof(c17,plain,((![X]:(![Y]:(~rinvS(X,Y)|rs(Y,X))))&(![X]:(![Y]:(~rs(Y,X)|rinvS(X,Y))))),inference(shift_quantors,[status(thm)],[c16])).
% 0.48/0.72 fof(c19,plain,(![X4]:(![X5]:(![X6]:(![X7]:((~rinvS(X4,X5)|rs(X5,X4))&(~rs(X7,X6)|rinvS(X6,X7))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,((![X4]:(![X5]:(~rinvS(X4,X5)|rs(X5,X4))))&(![X6]:(![X7]:(~rs(X7,X6)|rinvS(X6,X7))))),inference(variable_rename,[status(thm)],[c17])).])).
% 0.48/0.72 cnf(c21,plain,~rs(X96,X95)|rinvS(X95,X96),inference(split_conjunct,[status(thm)],[c19])).
% 0.48/0.72 cnf(c54,plain,~cUnsatisfiable(X126)|rs(X126,skolem0005(X126)),inference(split_conjunct,[status(thm)],[c50])).
% 0.48/0.72 cnf(c147,plain,rs(i2003_11_14_17_21_22376,skolem0005(i2003_11_14_17_21_22376)),inference(resolution,[status(thm)],[c54, c15])).
% 0.48/0.72 cnf(c149,plain,rinvS(skolem0005(i2003_11_14_17_21_22376),i2003_11_14_17_21_22376),inference(resolution,[status(thm)],[c147, c21])).
% 0.48/0.72 fof(rinvS_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rinvS(A,C))=>rinvS(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rinvS_substitution_1)).
% 0.48/0.72 fof(c94,plain,(![A]:(![B]:(![C]:((A!=B|~rinvS(A,C))|rinvS(B,C))))),inference(fof_nnf,[status(thm)],[rinvS_substitution_1])).
% 0.48/0.72 fof(c95,plain,(![X53]:(![X54]:(![X55]:((X53!=X54|~rinvS(X53,X55))|rinvS(X54,X55))))),inference(variable_rename,[status(thm)],[c94])).
% 0.48/0.72 cnf(c96,plain,X198!=X199|~rinvS(X198,X197)|rinvS(X199,X197),inference(split_conjunct,[status(thm)],[c95])).
% 0.48/0.72 cnf(c194,plain,skolem0005(i2003_11_14_17_21_22376)!=X227|rinvS(X227,i2003_11_14_17_21_22376),inference(resolution,[status(thm)],[c96, c149])).
% 0.48/0.72 fof(axiom_8,axiom,(![X]:(![Y]:(rs(X,Y)=>rr(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.48/0.72 fof(c12,plain,(![X]:(![Y]:(~rs(X,Y)|rr(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.48/0.72 fof(c13,plain,(![X2]:(![X3]:(~rs(X2,X3)|rr(X2,X3)))),inference(variable_rename,[status(thm)],[c12])).
% 0.48/0.72 cnf(c14,plain,~rs(X92,X91)|rr(X92,X91),inference(split_conjunct,[status(thm)],[c13])).
% 0.48/0.72 cnf(c148,plain,rr(i2003_11_14_17_21_22376,skolem0005(i2003_11_14_17_21_22376)),inference(resolution,[status(thm)],[c147, c14])).
% 0.48/0.72 cnf(c52,plain,~cUnsatisfiable(X122)|rr(X122,skolem0004(X122)),inference(split_conjunct,[status(thm)],[c50])).
% 0.48/0.72 cnf(c145,plain,rr(i2003_11_14_17_21_22376,skolem0004(i2003_11_14_17_21_22376)),inference(resolution,[status(thm)],[c52, c15])).
% 0.48/0.72 cnf(c51,plain,~cUnsatisfiable(X171)|~rr(X171,X172)|~rr(X171,X173)|X172=X173,inference(split_conjunct,[status(thm)],[c50])).
% 0.48/0.72 cnf(c173,plain,~cUnsatisfiable(i2003_11_14_17_21_22376)|~rr(i2003_11_14_17_21_22376,X299)|X299=skolem0004(i2003_11_14_17_21_22376),inference(resolution,[status(thm)],[c51, c145])).
% 0.48/0.72 cnf(c254,plain,~cUnsatisfiable(i2003_11_14_17_21_22376)|skolem0005(i2003_11_14_17_21_22376)=skolem0004(i2003_11_14_17_21_22376),inference(resolution,[status(thm)],[c173, c148])).
% 0.48/0.72 cnf(c256,plain,skolem0005(i2003_11_14_17_21_22376)=skolem0004(i2003_11_14_17_21_22376),inference(resolution,[status(thm)],[c254, c15])).
% 0.48/0.72 cnf(c266,plain,rinvS(skolem0004(i2003_11_14_17_21_22376),i2003_11_14_17_21_22376),inference(resolution,[status(thm)],[c256, c194])).
% 0.48/0.72 cnf(c288,plain,~ca_Vx2(skolem0004(i2003_11_14_17_21_22376))|cp(i2003_11_14_17_21_22376),inference(resolution,[status(thm)],[c266, c28])).
% 0.48/0.72 cnf(c306,plain,cp(i2003_11_14_17_21_22376),inference(resolution,[status(thm)],[c288, c127])).
% 0.48/0.72 cnf(c313,plain,$false,inference(resolution,[status(thm)],[c306, c133])).
% 0.48/0.72 % SZS output end CNFRefutation
% 0.48/0.72
% 0.48/0.72 % Initial clauses : 55
% 0.48/0.72 % Processed clauses : 108
% 0.48/0.72 % Factors computed : 2
% 0.48/0.72 % Resolvents computed: 191
% 0.48/0.72 % Tautologies deleted: 12
% 0.48/0.72 % Forward subsumed : 64
% 0.48/0.72 % Backward subsumed : 4
% 0.48/0.72 % -------- CPU Time ---------
% 0.48/0.72 % User time : 0.328 s
% 0.48/0.72 % System time : 0.017 s
% 0.48/0.72 % Total time : 0.345 s
%------------------------------------------------------------------------------