%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET800+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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:40:06 EDT 2024
% Result : Theorem 0.92s 1.16s
% Output : Refutation 0.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET800+4 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n017.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 : Wed May 8 18:28:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.92/1.16 % Version: 1.5
% 0.92/1.16 % SZS status Theorem
% 0.92/1.16 % SZS output start CNFRefutation
% 0.92/1.16 fof(thIV12,conjecture,(![R]:(![E]:(order(R,E)=>(![X1]:(![X2]:(((subset(X1,E)&subset(X2,E))&subset(X1,X2))=>(![M1]:(![M2]:((greatest_lower_bound(M1,X1,R,E)&greatest_lower_bound(M2,X2,R,E))=>apply(R,M2,M1)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thIV12)).
% 0.92/1.16 fof(c22,negated_conjecture,(~(![R]:(![E]:(order(R,E)=>(![X1]:(![X2]:(((subset(X1,E)&subset(X2,E))&subset(X1,X2))=>(![M1]:(![M2]:((greatest_lower_bound(M1,X1,R,E)&greatest_lower_bound(M2,X2,R,E))=>apply(R,M2,M1))))))))))),inference(assume_negation,[status(cth)],[thIV12])).
% 0.92/1.16 fof(c23,negated_conjecture,(?[R]:(?[E]:(order(R,E)&(?[X1]:(?[X2]:(((subset(X1,E)&subset(X2,E))&subset(X1,X2))&(?[M1]:(?[M2]:((greatest_lower_bound(M1,X1,R,E)&greatest_lower_bound(M2,X2,R,E))&~apply(R,M2,M1)))))))))),inference(fof_nnf,[status(thm)],[c22])).
% 0.92/1.16 fof(c24,negated_conjecture,(?[X2]:(?[X3]:(order(X2,X3)&(?[X4]:(?[X5]:(((subset(X4,X3)&subset(X5,X3))&subset(X4,X5))&(?[X6]:(?[X7]:((greatest_lower_bound(X6,X4,X2,X3)&greatest_lower_bound(X7,X5,X2,X3))&~apply(X2,X7,X6)))))))))),inference(variable_rename,[status(thm)],[c23])).
% 0.92/1.16 fof(c25,negated_conjecture,(order(skolem0001,skolem0002)&(((subset(skolem0003,skolem0002)&subset(skolem0004,skolem0002))&subset(skolem0003,skolem0004))&((greatest_lower_bound(skolem0005,skolem0003,skolem0001,skolem0002)&greatest_lower_bound(skolem0006,skolem0004,skolem0001,skolem0002))&~apply(skolem0001,skolem0006,skolem0005)))),inference(skolemize,[status(esa)],[c24])).
% 0.92/1.16 cnf(c32,negated_conjecture,~apply(skolem0001,skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c25])).
% 0.92/1.16 cnf(c29,negated_conjecture,subset(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c25])).
% 0.92/1.16 cnf(c30,negated_conjecture,greatest_lower_bound(skolem0005,skolem0003,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c25])).
% 0.92/1.16 fof(greatest_lower_bound,axiom,(![A]:(![X]:(![R]:(![E]:(greatest_lower_bound(A,X,R,E)<=>((member(A,X)&lower_bound(A,R,X))&(![M]:((member(M,E)&lower_bound(M,R,X))=>apply(R,M,A))))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', greatest_lower_bound)).
% 0.92/1.16 fof(c33,plain,(![A]:(![X]:(![R]:(![E]:((~greatest_lower_bound(A,X,R,E)|((member(A,X)&lower_bound(A,R,X))&(![M]:((~member(M,E)|~lower_bound(M,R,X))|apply(R,M,A)))))&(((~member(A,X)|~lower_bound(A,R,X))|(?[M]:((member(M,E)&lower_bound(M,R,X))&~apply(R,M,A))))|greatest_lower_bound(A,X,R,E))))))),inference(fof_nnf,[status(thm)],[greatest_lower_bound])).
% 0.92/1.16 fof(c34,plain,((![A]:(![X]:(![R]:(![E]:(~greatest_lower_bound(A,X,R,E)|((member(A,X)&lower_bound(A,R,X))&(![M]:((~member(M,E)|~lower_bound(M,R,X))|apply(R,M,A)))))))))&(![A]:(![X]:(![R]:(![E]:(((~member(A,X)|~lower_bound(A,R,X))|(?[M]:((member(M,E)&lower_bound(M,R,X))&~apply(R,M,A))))|greatest_lower_bound(A,X,R,E))))))),inference(shift_quantors,[status(thm)],[c33])).
% 0.92/1.16 fof(c35,plain,((![X8]:(![X9]:(![X10]:(![X11]:(~greatest_lower_bound(X8,X9,X10,X11)|((member(X8,X9)&lower_bound(X8,X10,X9))&(![X12]:((~member(X12,X11)|~lower_bound(X12,X10,X9))|apply(X10,X12,X8)))))))))&(![X13]:(![X14]:(![X15]:(![X16]:(((~member(X13,X14)|~lower_bound(X13,X15,X14))|(?[X17]:((member(X17,X16)&lower_bound(X17,X15,X14))&~apply(X15,X17,X13))))|greatest_lower_bound(X13,X14,X15,X16))))))),inference(variable_rename,[status(thm)],[c34])).
% 0.92/1.16 fof(c37,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((~greatest_lower_bound(X8,X9,X10,X11)|((member(X8,X9)&lower_bound(X8,X10,X9))&((~member(X12,X11)|~lower_bound(X12,X10,X9))|apply(X10,X12,X8))))&(((~member(X13,X14)|~lower_bound(X13,X15,X14))|((member(skolem0007(X13,X14,X15,X16),X16)&lower_bound(skolem0007(X13,X14,X15,X16),X15,X14))&~apply(X15,skolem0007(X13,X14,X15,X16),X13)))|greatest_lower_bound(X13,X14,X15,X16)))))))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,((![X8]:(![X9]:(![X10]:(![X11]:(~greatest_lower_bound(X8,X9,X10,X11)|((member(X8,X9)&lower_bound(X8,X10,X9))&(![X12]:((~member(X12,X11)|~lower_bound(X12,X10,X9))|apply(X10,X12,X8)))))))))&(![X13]:(![X14]:(![X15]:(![X16]:(((~member(X13,X14)|~lower_bound(X13,X15,X14))|((member(skolem0007(X13,X14,X15,X16),X16)&lower_bound(skolem0007(X13,X14,X15,X16),X15,X14))&~apply(X15,skolem0007(X13,X14,X15,X16),X13)))|greatest_lower_bound(X13,X14,X15,X16))))))),inference(skolemize,[status(esa)],[c35])).])).
% 0.92/1.16 fof(c38,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((((~greatest_lower_bound(X8,X9,X10,X11)|member(X8,X9))&(~greatest_lower_bound(X8,X9,X10,X11)|lower_bound(X8,X10,X9)))&(~greatest_lower_bound(X8,X9,X10,X11)|((~member(X12,X11)|~lower_bound(X12,X10,X9))|apply(X10,X12,X8))))&(((((~member(X13,X14)|~lower_bound(X13,X15,X14))|member(skolem0007(X13,X14,X15,X16),X16))|greatest_lower_bound(X13,X14,X15,X16))&(((~member(X13,X14)|~lower_bound(X13,X15,X14))|lower_bound(skolem0007(X13,X14,X15,X16),X15,X14))|greatest_lower_bound(X13,X14,X15,X16)))&(((~member(X13,X14)|~lower_bound(X13,X15,X14))|~apply(X15,skolem0007(X13,X14,X15,X16),X13))|greatest_lower_bound(X13,X14,X15,X16))))))))))))),inference(distribute,[status(thm)],[c37])).
% 0.92/1.16 cnf(c39,plain,~greatest_lower_bound(X191,X193,X194,X192)|member(X191,X193),inference(split_conjunct,[status(thm)],[c38])).
% 0.92/1.16 cnf(c287,plain,member(skolem0005,skolem0003),inference(resolution,[status(thm)],[c39, c30])).
% 0.92/1.16 fof(subset,axiom,(![A]:(![B]:(subset(A,B)<=>(![X]:(member(X,A)=>member(X,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', subset)).
% 0.92/1.16 fof(c272,plain,(![A]:(![B]:((~subset(A,B)|(![X]:(~member(X,A)|member(X,B))))&((?[X]:(member(X,A)&~member(X,B)))|subset(A,B))))),inference(fof_nnf,[status(thm)],[subset])).
% 0.92/1.16 fof(c273,plain,((![A]:(![B]:(~subset(A,B)|(![X]:(~member(X,A)|member(X,B))))))&(![A]:(![B]:((?[X]:(member(X,A)&~member(X,B)))|subset(A,B))))),inference(shift_quantors,[status(thm)],[c272])).
% 0.92/1.16 fof(c274,plain,((![X149]:(![X150]:(~subset(X149,X150)|(![X151]:(~member(X151,X149)|member(X151,X150))))))&(![X152]:(![X153]:((?[X154]:(member(X154,X152)&~member(X154,X153)))|subset(X152,X153))))),inference(variable_rename,[status(thm)],[c273])).
% 0.92/1.16 fof(c276,plain,(![X149]:(![X150]:(![X151]:(![X152]:(![X153]:((~subset(X149,X150)|(~member(X151,X149)|member(X151,X150)))&((member(skolem0025(X152,X153),X152)&~member(skolem0025(X152,X153),X153))|subset(X152,X153)))))))),inference(shift_quantors,[status(thm)],[fof(c275,plain,((![X149]:(![X150]:(~subset(X149,X150)|(![X151]:(~member(X151,X149)|member(X151,X150))))))&(![X152]:(![X153]:((member(skolem0025(X152,X153),X152)&~member(skolem0025(X152,X153),X153))|subset(X152,X153))))),inference(skolemize,[status(esa)],[c274])).])).
% 0.92/1.16 fof(c277,plain,(![X149]:(![X150]:(![X151]:(![X152]:(![X153]:((~subset(X149,X150)|(~member(X151,X149)|member(X151,X150)))&((member(skolem0025(X152,X153),X152)|subset(X152,X153))&(~member(skolem0025(X152,X153),X153)|subset(X152,X153))))))))),inference(distribute,[status(thm)],[c276])).
% 0.92/1.16 cnf(c278,plain,~subset(X358,X359)|~member(X357,X358)|member(X357,X359),inference(split_conjunct,[status(thm)],[c277])).
% 0.92/1.16 cnf(c453,plain,~subset(skolem0003,X369)|member(skolem0005,X369),inference(resolution,[status(thm)],[c278, c287])).
% 0.92/1.16 cnf(c477,plain,member(skolem0005,skolem0004),inference(resolution,[status(thm)],[c453, c29])).
% 0.92/1.16 cnf(c31,negated_conjecture,greatest_lower_bound(skolem0006,skolem0004,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c25])).
% 0.92/1.16 cnf(c40,plain,~greatest_lower_bound(X220,X222,X223,X221)|lower_bound(X220,X223,X222),inference(split_conjunct,[status(thm)],[c38])).
% 0.92/1.16 cnf(c303,plain,lower_bound(skolem0006,skolem0001,skolem0004),inference(resolution,[status(thm)],[c40, c31])).
% 0.92/1.16 fof(lower_bound,axiom,(![R]:(![E]:(![M]:(lower_bound(M,R,E)<=>(![X]:(member(X,E)=>apply(R,M,X))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', lower_bound)).
% 0.92/1.16 fof(c99,plain,(![R]:(![E]:(![M]:((~lower_bound(M,R,E)|(![X]:(~member(X,E)|apply(R,M,X))))&((?[X]:(member(X,E)&~apply(R,M,X)))|lower_bound(M,R,E)))))),inference(fof_nnf,[status(thm)],[lower_bound])).
% 0.92/1.16 fof(c100,plain,((![R]:(![E]:(![M]:(~lower_bound(M,R,E)|(![X]:(~member(X,E)|apply(R,M,X)))))))&(![R]:(![E]:(![M]:((?[X]:(member(X,E)&~apply(R,M,X)))|lower_bound(M,R,E)))))),inference(shift_quantors,[status(thm)],[c99])).
% 0.92/1.16 fof(c101,plain,((![X60]:(![X61]:(![X62]:(~lower_bound(X62,X60,X61)|(![X63]:(~member(X63,X61)|apply(X60,X62,X63)))))))&(![X64]:(![X65]:(![X66]:((?[X67]:(member(X67,X65)&~apply(X64,X66,X67)))|lower_bound(X66,X64,X65)))))),inference(variable_rename,[status(thm)],[c100])).
% 0.92/1.16 fof(c103,plain,(![X60]:(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:(![X66]:((~lower_bound(X62,X60,X61)|(~member(X63,X61)|apply(X60,X62,X63)))&((member(skolem0013(X64,X65,X66),X65)&~apply(X64,X66,skolem0013(X64,X65,X66)))|lower_bound(X66,X64,X65)))))))))),inference(shift_quantors,[status(thm)],[fof(c102,plain,((![X60]:(![X61]:(![X62]:(~lower_bound(X62,X60,X61)|(![X63]:(~member(X63,X61)|apply(X60,X62,X63)))))))&(![X64]:(![X65]:(![X66]:((member(skolem0013(X64,X65,X66),X65)&~apply(X64,X66,skolem0013(X64,X65,X66)))|lower_bound(X66,X64,X65)))))),inference(skolemize,[status(esa)],[c101])).])).
% 0.92/1.16 fof(c104,plain,(![X60]:(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:(![X66]:((~lower_bound(X62,X60,X61)|(~member(X63,X61)|apply(X60,X62,X63)))&((member(skolem0013(X64,X65,X66),X65)|lower_bound(X66,X64,X65))&(~apply(X64,X66,skolem0013(X64,X65,X66))|lower_bound(X66,X64,X65))))))))))),inference(distribute,[status(thm)],[c103])).
% 0.92/1.16 cnf(c105,plain,~lower_bound(X671,X673,X670)|~member(X672,X670)|apply(X673,X671,X672),inference(split_conjunct,[status(thm)],[c104])).
% 0.92/1.16 cnf(c1363,plain,~member(X740,skolem0004)|apply(skolem0001,skolem0006,X740),inference(resolution,[status(thm)],[c105, c303])).
% 0.92/1.16 cnf(c1526,plain,apply(skolem0001,skolem0006,skolem0005),inference(resolution,[status(thm)],[c1363, c477])).
% 0.92/1.16 cnf(c1530,plain,$false,inference(resolution,[status(thm)],[c1526, c32])).
% 0.92/1.16 % SZS output end CNFRefutation
% 0.92/1.16
% 0.92/1.16 % Initial clauses : 166
% 0.92/1.16 % Processed clauses : 220
% 0.92/1.16 % Factors computed : 9
% 0.92/1.16 % Resolvents computed: 1243
% 0.92/1.16 % Tautologies deleted: 2
% 0.92/1.16 % Forward subsumed : 105
% 0.92/1.16 % Backward subsumed : 1
% 0.92/1.16 % -------- CPU Time ---------
% 0.92/1.16 % User time : 0.793 s
% 0.92/1.16 % System time : 0.013 s
% 0.92/1.16 % Total time : 0.806 s
%------------------------------------------------------------------------------