%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS071+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:37 EDT 2024
% Result : Unsatisfiable 0.61s 0.80s
% Output : Refutation 0.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS071+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 00:10:38 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.61/0.80 % Version: 1.5
% 0.61/0.80 % SZS status Unsatisfiable
% 0.61/0.80 % SZS output start CNFRefutation
% 0.61/0.80 fof(axiom_8,axiom,cUnsatisfiable(i2003_11_14_17_18_39380),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.61/0.80 cnf(c12,plain,cUnsatisfiable(i2003_11_14_17_18_39380),inference(split_conjunct,[status(thm)],[axiom_8])).
% 0.61/0.80 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((((?[Y]:(rr(X,Y)&cp1(Y)))&(?[Y]:(rr(X,Y)&cp2(Y))))&(?[Y]:(rr(X,Y)&cp3(Y))))&(![Y0]:(![Y1]:(![Y2]:(((rr(X,Y0)&rr(X,Y1))&rr(X,Y2))=>((Y0=Y1|Y0=Y2)|Y1=Y2)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.61/0.80 fof(c41,plain,(![X]:((~cUnsatisfiable(X)|((((?[Y]:(rr(X,Y)&cp1(Y)))&(?[Y]:(rr(X,Y)&cp2(Y))))&(?[Y]:(rr(X,Y)&cp3(Y))))&(![Y0]:(![Y1]:(![Y2]:(((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|((Y0=Y1|Y0=Y2)|Y1=Y2)))))))&(((((![Y]:(~rr(X,Y)|~cp1(Y)))|(![Y]:(~rr(X,Y)|~cp2(Y))))|(![Y]:(~rr(X,Y)|~cp3(Y))))|(?[Y0]:(?[Y1]:(?[Y2]:(((rr(X,Y0)&rr(X,Y1))&rr(X,Y2))&((Y0!=Y1&Y0!=Y2)&Y1!=Y2))))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.61/0.80 fof(c42,plain,((![X]:(~cUnsatisfiable(X)|((((?[Y]:(rr(X,Y)&cp1(Y)))&(?[Y]:(rr(X,Y)&cp2(Y))))&(?[Y]:(rr(X,Y)&cp3(Y))))&(![Y0]:(![Y1]:(![Y2]:(((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|((Y0=Y1|Y0=Y2)|Y1=Y2))))))))&(![X]:(((((![Y]:(~rr(X,Y)|~cp1(Y)))|(![Y]:(~rr(X,Y)|~cp2(Y))))|(![Y]:(~rr(X,Y)|~cp3(Y))))|(?[Y0]:(?[Y1]:(?[Y2]:(((rr(X,Y0)&rr(X,Y1))&rr(X,Y2))&((Y0!=Y1&Y0!=Y2)&Y1!=Y2))))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c41])).
% 0.61/0.80 fof(c43,plain,((![X10]:(~cUnsatisfiable(X10)|((((?[X11]:(rr(X10,X11)&cp1(X11)))&(?[X12]:(rr(X10,X12)&cp2(X12))))&(?[X13]:(rr(X10,X13)&cp3(X13))))&(![X14]:(![X15]:(![X16]:(((~rr(X10,X14)|~rr(X10,X15))|~rr(X10,X16))|((X14=X15|X14=X16)|X15=X16))))))))&(![X17]:(((((![X18]:(~rr(X17,X18)|~cp1(X18)))|(![X19]:(~rr(X17,X19)|~cp2(X19))))|(![X20]:(~rr(X17,X20)|~cp3(X20))))|(?[X21]:(?[X22]:(?[X23]:(((rr(X17,X21)&rr(X17,X22))&rr(X17,X23))&((X21!=X22&X21!=X23)&X22!=X23))))))|cUnsatisfiable(X17)))),inference(variable_rename,[status(thm)],[c42])).
% 0.61/0.80 fof(c45,plain,(![X10]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((~cUnsatisfiable(X10)|((((rr(X10,skolem0001(X10))&cp1(skolem0001(X10)))&(rr(X10,skolem0002(X10))&cp2(skolem0002(X10))))&(rr(X10,skolem0003(X10))&cp3(skolem0003(X10))))&(((~rr(X10,X14)|~rr(X10,X15))|~rr(X10,X16))|((X14=X15|X14=X16)|X15=X16))))&(((((~rr(X17,X18)|~cp1(X18))|(~rr(X17,X19)|~cp2(X19)))|(~rr(X17,X20)|~cp3(X20)))|(((rr(X17,skolem0004(X17))&rr(X17,skolem0005(X17)))&rr(X17,skolem0006(X17)))&((skolem0004(X17)!=skolem0005(X17)&skolem0004(X17)!=skolem0006(X17))&skolem0005(X17)!=skolem0006(X17))))|cUnsatisfiable(X17))))))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,((![X10]:(~cUnsatisfiable(X10)|((((rr(X10,skolem0001(X10))&cp1(skolem0001(X10)))&(rr(X10,skolem0002(X10))&cp2(skolem0002(X10))))&(rr(X10,skolem0003(X10))&cp3(skolem0003(X10))))&(![X14]:(![X15]:(![X16]:(((~rr(X10,X14)|~rr(X10,X15))|~rr(X10,X16))|((X14=X15|X14=X16)|X15=X16))))))))&(![X17]:(((((![X18]:(~rr(X17,X18)|~cp1(X18)))|(![X19]:(~rr(X17,X19)|~cp2(X19))))|(![X20]:(~rr(X17,X20)|~cp3(X20))))|(((rr(X17,skolem0004(X17))&rr(X17,skolem0005(X17)))&rr(X17,skolem0006(X17)))&((skolem0004(X17)!=skolem0005(X17)&skolem0004(X17)!=skolem0006(X17))&skolem0005(X17)!=skolem0006(X17))))|cUnsatisfiable(X17)))),inference(skolemize,[status(esa)],[c43])).])).
% 0.61/0.80 fof(c46,plain,(![X10]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((((((~cUnsatisfiable(X10)|rr(X10,skolem0001(X10)))&(~cUnsatisfiable(X10)|cp1(skolem0001(X10))))&((~cUnsatisfiable(X10)|rr(X10,skolem0002(X10)))&(~cUnsatisfiable(X10)|cp2(skolem0002(X10)))))&((~cUnsatisfiable(X10)|rr(X10,skolem0003(X10)))&(~cUnsatisfiable(X10)|cp3(skolem0003(X10)))))&(~cUnsatisfiable(X10)|(((~rr(X10,X14)|~rr(X10,X15))|~rr(X10,X16))|((X14=X15|X14=X16)|X15=X16))))&((((((((~rr(X17,X18)|~cp1(X18))|(~rr(X17,X19)|~cp2(X19)))|(~rr(X17,X20)|~cp3(X20)))|rr(X17,skolem0004(X17)))|cUnsatisfiable(X17))&(((((~rr(X17,X18)|~cp1(X18))|(~rr(X17,X19)|~cp2(X19)))|(~rr(X17,X20)|~cp3(X20)))|rr(X17,skolem0005(X17)))|cUnsatisfiable(X17)))&(((((~rr(X17,X18)|~cp1(X18))|(~rr(X17,X19)|~cp2(X19)))|(~rr(X17,X20)|~cp3(X20)))|rr(X17,skolem0006(X17)))|cUnsatisfiable(X17)))&(((((((~rr(X17,X18)|~cp1(X18))|(~rr(X17,X19)|~cp2(X19)))|(~rr(X17,X20)|~cp3(X20)))|skolem0004(X17)!=skolem0005(X17))|cUnsatisfiable(X17))&(((((~rr(X17,X18)|~cp1(X18))|(~rr(X17,X19)|~cp2(X19)))|(~rr(X17,X20)|~cp3(X20)))|skolem0004(X17)!=skolem0006(X17))|cUnsatisfiable(X17)))&(((((~rr(X17,X18)|~cp1(X18))|(~rr(X17,X19)|~cp2(X19)))|(~rr(X17,X20)|~cp3(X20)))|skolem0005(X17)!=skolem0006(X17))|cUnsatisfiable(X17))))))))))))),inference(distribute,[status(thm)],[c45])).
% 0.61/0.80 cnf(c50,plain,~cUnsatisfiable(X92)|cp2(skolem0002(X92)),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.80 cnf(c121,plain,cp2(skolem0002(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c50, c12])).
% 0.61/0.80 fof(axiom_4,axiom,(![X]:(cp2(X)=>(~((cp4(X)|cp3(X))|cp5(X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.61/0.80 fof(c28,plain,(![X]:(~cp2(X)|((~cp4(X)&~cp3(X))&~cp5(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.61/0.80 fof(c29,plain,(![X8]:(~cp2(X8)|((~cp4(X8)&~cp3(X8))&~cp5(X8)))),inference(variable_rename,[status(thm)],[c28])).
% 0.61/0.80 fof(c30,plain,(![X8]:(((~cp2(X8)|~cp4(X8))&(~cp2(X8)|~cp3(X8)))&(~cp2(X8)|~cp5(X8)))),inference(distribute,[status(thm)],[c29])).
% 0.61/0.80 cnf(c32,plain,~cp2(X70)|~cp3(X70),inference(split_conjunct,[status(thm)],[c30])).
% 0.61/0.80 cnf(c52,plain,~cUnsatisfiable(X95)|cp3(skolem0003(X95)),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.80 cnf(c123,plain,cp3(skolem0003(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c52, c12])).
% 0.61/0.80 cnf(c5,axiom,X108!=X107|~cp3(X108)|cp3(X107),theory(equality)).
% 0.61/0.80 fof(axiom_3,axiom,(![X]:(cp1(X)=>(~(((cp4(X)|cp2(X))|cp3(X))|cp5(X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.61/0.80 fof(c34,plain,(![X]:(~cp1(X)|(((~cp4(X)&~cp2(X))&~cp3(X))&~cp5(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.61/0.80 fof(c35,plain,(![X9]:(~cp1(X9)|(((~cp4(X9)&~cp2(X9))&~cp3(X9))&~cp5(X9)))),inference(variable_rename,[status(thm)],[c34])).
% 0.61/0.80 fof(c36,plain,(![X9]:((((~cp1(X9)|~cp4(X9))&(~cp1(X9)|~cp2(X9)))&(~cp1(X9)|~cp3(X9)))&(~cp1(X9)|~cp5(X9)))),inference(distribute,[status(thm)],[c35])).
% 0.61/0.80 cnf(c38,plain,~cp1(X76)|~cp2(X76),inference(split_conjunct,[status(thm)],[c36])).
% 0.61/0.80 cnf(c122,plain,~cp1(skolem0002(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c121, c38])).
% 0.61/0.80 cnf(c48,plain,~cUnsatisfiable(X91)|cp1(skolem0001(X91)),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.80 cnf(c120,plain,cp1(skolem0001(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c48, c12])).
% 0.61/0.80 cnf(c3,axiom,X97!=X96|~cp1(X97)|cp1(X96),theory(equality)).
% 0.61/0.80 cnf(c39,plain,~cp1(X77)|~cp3(X77),inference(split_conjunct,[status(thm)],[c36])).
% 0.61/0.80 cnf(c125,plain,~cp1(skolem0003(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c123, c39])).
% 0.61/0.80 cnf(c47,plain,~cUnsatisfiable(X102)|rr(X102,skolem0001(X102)),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.80 cnf(c127,plain,rr(i2003_11_14_17_18_39380,skolem0001(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c47, c12])).
% 0.61/0.80 cnf(c51,plain,~cUnsatisfiable(X110)|rr(X110,skolem0003(X110)),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.80 cnf(c135,plain,rr(i2003_11_14_17_18_39380,skolem0003(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c51, c12])).
% 0.61/0.80 cnf(c49,plain,~cUnsatisfiable(X106)|rr(X106,skolem0002(X106)),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.80 cnf(c131,plain,rr(i2003_11_14_17_18_39380,skolem0002(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c49, c12])).
% 0.61/0.80 cnf(c53,plain,~cUnsatisfiable(X146)|~rr(X146,X145)|~rr(X146,X143)|~rr(X146,X144)|X145=X143|X145=X144|X143=X144,inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.80 cnf(c150,plain,~cUnsatisfiable(i2003_11_14_17_18_39380)|~rr(i2003_11_14_17_18_39380,X231)|~rr(i2003_11_14_17_18_39380,X230)|X231=X230|X231=skolem0002(i2003_11_14_17_18_39380)|X230=skolem0002(i2003_11_14_17_18_39380),inference(resolution,[status(thm)],[c53, c131])).
% 0.61/0.80 cnf(c200,plain,~cUnsatisfiable(i2003_11_14_17_18_39380)|~rr(i2003_11_14_17_18_39380,X259)|X259=skolem0003(i2003_11_14_17_18_39380)|X259=skolem0002(i2003_11_14_17_18_39380)|skolem0003(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380),inference(resolution,[status(thm)],[c150, c135])).
% 0.61/0.80 cnf(c212,plain,~cUnsatisfiable(i2003_11_14_17_18_39380)|skolem0001(i2003_11_14_17_18_39380)=skolem0003(i2003_11_14_17_18_39380)|skolem0001(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380)|skolem0003(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380),inference(resolution,[status(thm)],[c200, c127])).
% 0.61/0.80 cnf(c228,plain,skolem0001(i2003_11_14_17_18_39380)=skolem0003(i2003_11_14_17_18_39380)|skolem0001(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380)|skolem0003(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380),inference(resolution,[status(thm)],[c212, c12])).
% 0.61/0.80 cnf(c233,plain,skolem0001(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380)|skolem0003(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380)|~cp1(skolem0001(i2003_11_14_17_18_39380))|cp1(skolem0003(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c228, c3])).
% 0.61/0.80 cnf(c569,plain,skolem0001(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380)|skolem0003(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380)|cp1(skolem0003(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c233, c120])).
% 0.61/0.80 cnf(c598,plain,skolem0001(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380)|skolem0003(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380),inference(resolution,[status(thm)],[c569, c125])).
% 0.61/0.80 cnf(c603,plain,skolem0003(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380)|~cp1(skolem0001(i2003_11_14_17_18_39380))|cp1(skolem0002(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c598, c3])).
% 0.61/0.80 cnf(c712,plain,skolem0003(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380)|cp1(skolem0002(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c603, c120])).
% 0.61/0.80 cnf(c727,plain,skolem0003(i2003_11_14_17_18_39380)=skolem0002(i2003_11_14_17_18_39380),inference(resolution,[status(thm)],[c712, c122])).
% 0.61/0.80 cnf(c729,plain,~cp3(skolem0003(i2003_11_14_17_18_39380))|cp3(skolem0002(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c727, c5])).
% 0.61/0.80 cnf(c756,plain,cp3(skolem0002(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c729, c123])).
% 0.61/0.80 cnf(c757,plain,~cp2(skolem0002(i2003_11_14_17_18_39380)),inference(resolution,[status(thm)],[c756, c32])).
% 0.61/0.80 cnf(c759,plain,$false,inference(resolution,[status(thm)],[c757, c121])).
% 0.61/0.80 % SZS output end CNFRefutation
% 0.61/0.80
% 0.61/0.80 % Initial clauses : 59
% 0.61/0.80 % Processed clauses : 117
% 0.61/0.80 % Factors computed : 12
% 0.61/0.80 % Resolvents computed: 633
% 0.61/0.80 % Tautologies deleted: 11
% 0.61/0.80 % Forward subsumed : 176
% 0.61/0.80 % Backward subsumed : 29
% 0.61/0.80 % -------- CPU Time ---------
% 0.61/0.80 % User time : 0.440 s
% 0.61/0.80 % System time : 0.015 s
% 0.61/0.80 % Total time : 0.455 s
%------------------------------------------------------------------------------