%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET799+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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.90s 1.15s
% Output : Refutation 0.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET799+4 : TPTP v8.1.2. Released v3.2.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.37 % Computer : n014.cluster.edu
% 0.14/0.37 % Model : x86_64 x86_64
% 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.37 % Memory : 8042.1875MB
% 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 300
% 0.14/0.37 % DateTime : Wed May 8 19:35:22 EDT 2024
% 0.14/0.37 % CPUTime :
% 0.90/1.15 % Version: 1.5
% 0.90/1.15 % SZS status Theorem
% 0.90/1.15 % SZS output start CNFRefutation
% 0.90/1.15 fof(thIV11,conjecture,(![R]:(![E]:(order(R,E)=>(![X1]:(![X2]:(((subset(X1,E)&subset(X2,E))&subset(X1,X2))=>(![M1]:(![M2]:((least_upper_bound(M1,X1,R,E)&least_upper_bound(M2,X2,R,E))=>apply(R,M1,M2)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thIV11)).
% 0.90/1.15 fof(c22,negated_conjecture,(~(![R]:(![E]:(order(R,E)=>(![X1]:(![X2]:(((subset(X1,E)&subset(X2,E))&subset(X1,X2))=>(![M1]:(![M2]:((least_upper_bound(M1,X1,R,E)&least_upper_bound(M2,X2,R,E))=>apply(R,M1,M2))))))))))),inference(assume_negation,[status(cth)],[thIV11])).
% 0.90/1.15 fof(c23,negated_conjecture,(?[R]:(?[E]:(order(R,E)&(?[X1]:(?[X2]:(((subset(X1,E)&subset(X2,E))&subset(X1,X2))&(?[M1]:(?[M2]:((least_upper_bound(M1,X1,R,E)&least_upper_bound(M2,X2,R,E))&~apply(R,M1,M2)))))))))),inference(fof_nnf,[status(thm)],[c22])).
% 0.90/1.15 fof(c24,negated_conjecture,(?[X2]:(?[X3]:(order(X2,X3)&(?[X4]:(?[X5]:(((subset(X4,X3)&subset(X5,X3))&subset(X4,X5))&(?[X6]:(?[X7]:((least_upper_bound(X6,X4,X2,X3)&least_upper_bound(X7,X5,X2,X3))&~apply(X2,X6,X7)))))))))),inference(variable_rename,[status(thm)],[c23])).
% 0.90/1.15 fof(c25,negated_conjecture,(order(skolem0001,skolem0002)&(((subset(skolem0003,skolem0002)&subset(skolem0004,skolem0002))&subset(skolem0003,skolem0004))&((least_upper_bound(skolem0005,skolem0003,skolem0001,skolem0002)&least_upper_bound(skolem0006,skolem0004,skolem0001,skolem0002))&~apply(skolem0001,skolem0005,skolem0006)))),inference(skolemize,[status(esa)],[c24])).
% 0.90/1.15 cnf(c32,negated_conjecture,~apply(skolem0001,skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c25])).
% 0.90/1.15 cnf(c29,negated_conjecture,subset(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c25])).
% 0.90/1.15 cnf(c30,negated_conjecture,least_upper_bound(skolem0005,skolem0003,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c25])).
% 0.90/1.15 fof(least_upper_bound,axiom,(![A]:(![X]:(![R]:(![E]:(least_upper_bound(A,X,R,E)<=>((member(A,X)&upper_bound(A,R,X))&(![M]:((member(M,E)&upper_bound(M,R,X))=>apply(R,A,M))))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', least_upper_bound)).
% 0.90/1.15 fof(c45,plain,(![A]:(![X]:(![R]:(![E]:((~least_upper_bound(A,X,R,E)|((member(A,X)&upper_bound(A,R,X))&(![M]:((~member(M,E)|~upper_bound(M,R,X))|apply(R,A,M)))))&(((~member(A,X)|~upper_bound(A,R,X))|(?[M]:((member(M,E)&upper_bound(M,R,X))&~apply(R,A,M))))|least_upper_bound(A,X,R,E))))))),inference(fof_nnf,[status(thm)],[least_upper_bound])).
% 0.90/1.15 fof(c46,plain,((![A]:(![X]:(![R]:(![E]:(~least_upper_bound(A,X,R,E)|((member(A,X)&upper_bound(A,R,X))&(![M]:((~member(M,E)|~upper_bound(M,R,X))|apply(R,A,M)))))))))&(![A]:(![X]:(![R]:(![E]:(((~member(A,X)|~upper_bound(A,R,X))|(?[M]:((member(M,E)&upper_bound(M,R,X))&~apply(R,A,M))))|least_upper_bound(A,X,R,E))))))),inference(shift_quantors,[status(thm)],[c45])).
% 0.90/1.15 fof(c47,plain,((![X18]:(![X19]:(![X20]:(![X21]:(~least_upper_bound(X18,X19,X20,X21)|((member(X18,X19)&upper_bound(X18,X20,X19))&(![X22]:((~member(X22,X21)|~upper_bound(X22,X20,X19))|apply(X20,X18,X22)))))))))&(![X23]:(![X24]:(![X25]:(![X26]:(((~member(X23,X24)|~upper_bound(X23,X25,X24))|(?[X27]:((member(X27,X26)&upper_bound(X27,X25,X24))&~apply(X25,X23,X27))))|least_upper_bound(X23,X24,X25,X26))))))),inference(variable_rename,[status(thm)],[c46])).
% 0.90/1.15 fof(c49,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:((~least_upper_bound(X18,X19,X20,X21)|((member(X18,X19)&upper_bound(X18,X20,X19))&((~member(X22,X21)|~upper_bound(X22,X20,X19))|apply(X20,X18,X22))))&(((~member(X23,X24)|~upper_bound(X23,X25,X24))|((member(skolem0008(X23,X24,X25,X26),X26)&upper_bound(skolem0008(X23,X24,X25,X26),X25,X24))&~apply(X25,X23,skolem0008(X23,X24,X25,X26))))|least_upper_bound(X23,X24,X25,X26)))))))))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,((![X18]:(![X19]:(![X20]:(![X21]:(~least_upper_bound(X18,X19,X20,X21)|((member(X18,X19)&upper_bound(X18,X20,X19))&(![X22]:((~member(X22,X21)|~upper_bound(X22,X20,X19))|apply(X20,X18,X22)))))))))&(![X23]:(![X24]:(![X25]:(![X26]:(((~member(X23,X24)|~upper_bound(X23,X25,X24))|((member(skolem0008(X23,X24,X25,X26),X26)&upper_bound(skolem0008(X23,X24,X25,X26),X25,X24))&~apply(X25,X23,skolem0008(X23,X24,X25,X26))))|least_upper_bound(X23,X24,X25,X26))))))),inference(skolemize,[status(esa)],[c47])).])).
% 0.90/1.15 fof(c50,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:((((~least_upper_bound(X18,X19,X20,X21)|member(X18,X19))&(~least_upper_bound(X18,X19,X20,X21)|upper_bound(X18,X20,X19)))&(~least_upper_bound(X18,X19,X20,X21)|((~member(X22,X21)|~upper_bound(X22,X20,X19))|apply(X20,X18,X22))))&(((((~member(X23,X24)|~upper_bound(X23,X25,X24))|member(skolem0008(X23,X24,X25,X26),X26))|least_upper_bound(X23,X24,X25,X26))&(((~member(X23,X24)|~upper_bound(X23,X25,X24))|upper_bound(skolem0008(X23,X24,X25,X26),X25,X24))|least_upper_bound(X23,X24,X25,X26)))&(((~member(X23,X24)|~upper_bound(X23,X25,X24))|~apply(X25,X23,skolem0008(X23,X24,X25,X26)))|least_upper_bound(X23,X24,X25,X26))))))))))))),inference(distribute,[status(thm)],[c49])).
% 0.90/1.15 cnf(c51,plain,~least_upper_bound(X197,X195,X198,X196)|member(X197,X195),inference(split_conjunct,[status(thm)],[c50])).
% 0.90/1.15 cnf(c287,plain,member(skolem0005,skolem0003),inference(resolution,[status(thm)],[c51, c30])).
% 0.90/1.15 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.90/1.15 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.90/1.15 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.90/1.15 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.90/1.15 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.90/1.15 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.90/1.15 cnf(c278,plain,~subset(X358,X359)|~member(X357,X358)|member(X357,X359),inference(split_conjunct,[status(thm)],[c277])).
% 0.90/1.15 cnf(c463,plain,~subset(skolem0003,X381)|member(skolem0005,X381),inference(resolution,[status(thm)],[c278, c287])).
% 0.90/1.15 cnf(c491,plain,member(skolem0005,skolem0004),inference(resolution,[status(thm)],[c463, c29])).
% 0.90/1.15 cnf(c31,negated_conjecture,least_upper_bound(skolem0006,skolem0004,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c25])).
% 0.90/1.15 cnf(c52,plain,~least_upper_bound(X226,X224,X227,X225)|upper_bound(X226,X227,X224),inference(split_conjunct,[status(thm)],[c50])).
% 0.90/1.15 cnf(c303,plain,upper_bound(skolem0006,skolem0001,skolem0004),inference(resolution,[status(thm)],[c52, c31])).
% 0.90/1.15 fof(upper_bound,axiom,(![R]:(![E]:(![M]:(upper_bound(M,R,E)<=>(![X]:(member(X,E)=>apply(R,X,M))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', upper_bound)).
% 0.90/1.15 fof(c108,plain,(![R]:(![E]:(![M]:((~upper_bound(M,R,E)|(![X]:(~member(X,E)|apply(R,X,M))))&((?[X]:(member(X,E)&~apply(R,X,M)))|upper_bound(M,R,E)))))),inference(fof_nnf,[status(thm)],[upper_bound])).
% 0.90/1.15 fof(c109,plain,((![R]:(![E]:(![M]:(~upper_bound(M,R,E)|(![X]:(~member(X,E)|apply(R,X,M)))))))&(![R]:(![E]:(![M]:((?[X]:(member(X,E)&~apply(R,X,M)))|upper_bound(M,R,E)))))),inference(shift_quantors,[status(thm)],[c108])).
% 0.90/1.15 fof(c110,plain,((![X68]:(![X69]:(![X70]:(~upper_bound(X70,X68,X69)|(![X71]:(~member(X71,X69)|apply(X68,X71,X70)))))))&(![X72]:(![X73]:(![X74]:((?[X75]:(member(X75,X73)&~apply(X72,X75,X74)))|upper_bound(X74,X72,X73)))))),inference(variable_rename,[status(thm)],[c109])).
% 0.90/1.15 fof(c112,plain,(![X68]:(![X69]:(![X70]:(![X71]:(![X72]:(![X73]:(![X74]:((~upper_bound(X70,X68,X69)|(~member(X71,X69)|apply(X68,X71,X70)))&((member(skolem0014(X72,X73,X74),X73)&~apply(X72,skolem0014(X72,X73,X74),X74))|upper_bound(X74,X72,X73)))))))))),inference(shift_quantors,[status(thm)],[fof(c111,plain,((![X68]:(![X69]:(![X70]:(~upper_bound(X70,X68,X69)|(![X71]:(~member(X71,X69)|apply(X68,X71,X70)))))))&(![X72]:(![X73]:(![X74]:((member(skolem0014(X72,X73,X74),X73)&~apply(X72,skolem0014(X72,X73,X74),X74))|upper_bound(X74,X72,X73)))))),inference(skolemize,[status(esa)],[c110])).])).
% 0.90/1.15 fof(c113,plain,(![X68]:(![X69]:(![X70]:(![X71]:(![X72]:(![X73]:(![X74]:((~upper_bound(X70,X68,X69)|(~member(X71,X69)|apply(X68,X71,X70)))&((member(skolem0014(X72,X73,X74),X73)|upper_bound(X74,X72,X73))&(~apply(X72,skolem0014(X72,X73,X74),X74)|upper_bound(X74,X72,X73))))))))))),inference(distribute,[status(thm)],[c112])).
% 0.90/1.15 cnf(c114,plain,~upper_bound(X690,X692,X691)|~member(X689,X691)|apply(X692,X689,X690),inference(split_conjunct,[status(thm)],[c113])).
% 0.90/1.15 cnf(c1364,plain,~member(X737,skolem0004)|apply(skolem0001,X737,skolem0006),inference(resolution,[status(thm)],[c114, c303])).
% 0.90/1.15 cnf(c1523,plain,apply(skolem0001,skolem0005,skolem0006),inference(resolution,[status(thm)],[c1364, c491])).
% 0.90/1.15 cnf(c1526,plain,$false,inference(resolution,[status(thm)],[c1523, c32])).
% 0.90/1.15 % SZS output end CNFRefutation
% 0.90/1.15
% 0.90/1.15 % Initial clauses : 166
% 0.90/1.15 % Processed clauses : 219
% 0.90/1.15 % Factors computed : 9
% 0.90/1.15 % Resolvents computed: 1238
% 0.90/1.15 % Tautologies deleted: 2
% 0.90/1.15 % Forward subsumed : 105
% 0.90/1.15 % Backward subsumed : 1
% 0.90/1.15 % -------- CPU Time ---------
% 0.90/1.15 % User time : 0.750 s
% 0.90/1.15 % System time : 0.015 s
% 0.90/1.15 % Total time : 0.765 s
%------------------------------------------------------------------------------