%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET798+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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 174.29s 174.65s
% Output : Refutation 174.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.11 % Problem : SET798+4 : TPTP v8.1.2. Released v3.2.0.
% 0.12/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n024.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 : Wed May 8 19:24:23 EDT 2024
% 0.12/0.33 % CPUTime :
% 174.29/174.65 % Version: 1.5
% 174.29/174.65 % SZS status Theorem
% 174.29/174.65 % SZS output start CNFRefutation
% 174.29/174.65 fof(thIV10,conjecture,(![R]:(![E]:(order(R,E)=>(![X]:(![Y]:(((subset(X,E)&subset(Y,E))&subset(X,Y))=>(![M]:(lower_bound(M,R,Y)=>lower_bound(M,R,X))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thIV10)).
% 174.29/174.65 fof(c22,negated_conjecture,(~(![R]:(![E]:(order(R,E)=>(![X]:(![Y]:(((subset(X,E)&subset(Y,E))&subset(X,Y))=>(![M]:(lower_bound(M,R,Y)=>lower_bound(M,R,X)))))))))),inference(assume_negation,[status(cth)],[thIV10])).
% 174.29/174.65 fof(c23,negated_conjecture,(?[R]:(?[E]:(order(R,E)&(?[X]:(?[Y]:(((subset(X,E)&subset(Y,E))&subset(X,Y))&(?[M]:(lower_bound(M,R,Y)&~lower_bound(M,R,X))))))))),inference(fof_nnf,[status(thm)],[c22])).
% 174.29/174.65 fof(c24,negated_conjecture,(?[X2]:(?[X3]:(order(X2,X3)&(?[X4]:(?[X5]:(((subset(X4,X3)&subset(X5,X3))&subset(X4,X5))&(?[X6]:(lower_bound(X6,X2,X5)&~lower_bound(X6,X2,X4))))))))),inference(variable_rename,[status(thm)],[c23])).
% 174.29/174.65 fof(c25,negated_conjecture,(order(skolem0001,skolem0002)&(((subset(skolem0003,skolem0002)&subset(skolem0004,skolem0002))&subset(skolem0003,skolem0004))&(lower_bound(skolem0005,skolem0001,skolem0004)&~lower_bound(skolem0005,skolem0001,skolem0003)))),inference(skolemize,[status(esa)],[c24])).
% 174.29/174.65 cnf(c31,negated_conjecture,~lower_bound(skolem0005,skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c25])).
% 174.29/174.65 fof(lower_bound,axiom,(![R]:(![E]:(![M]:(lower_bound(M,R,E)<=>(![X]:(member(X,E)=>apply(R,M,X))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+3.ax', lower_bound)).
% 174.29/174.65 fof(c98,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])).
% 174.29/174.65 fof(c99,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)],[c98])).
% 174.29/174.65 fof(c100,plain,((![X59]:(![X60]:(![X61]:(~lower_bound(X61,X59,X60)|(![X62]:(~member(X62,X60)|apply(X59,X61,X62)))))))&(![X63]:(![X64]:(![X65]:((?[X66]:(member(X66,X64)&~apply(X63,X65,X66)))|lower_bound(X65,X63,X64)))))),inference(variable_rename,[status(thm)],[c99])).
% 174.29/174.65 fof(c102,plain,(![X59]:(![X60]:(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:((~lower_bound(X61,X59,X60)|(~member(X62,X60)|apply(X59,X61,X62)))&((member(skolem0012(X63,X64,X65),X64)&~apply(X63,X65,skolem0012(X63,X64,X65)))|lower_bound(X65,X63,X64)))))))))),inference(shift_quantors,[status(thm)],[fof(c101,plain,((![X59]:(![X60]:(![X61]:(~lower_bound(X61,X59,X60)|(![X62]:(~member(X62,X60)|apply(X59,X61,X62)))))))&(![X63]:(![X64]:(![X65]:((member(skolem0012(X63,X64,X65),X64)&~apply(X63,X65,skolem0012(X63,X64,X65)))|lower_bound(X65,X63,X64)))))),inference(skolemize,[status(esa)],[c100])).])).
% 174.29/174.65 fof(c103,plain,(![X59]:(![X60]:(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:((~lower_bound(X61,X59,X60)|(~member(X62,X60)|apply(X59,X61,X62)))&((member(skolem0012(X63,X64,X65),X64)|lower_bound(X65,X63,X64))&(~apply(X63,X65,skolem0012(X63,X64,X65))|lower_bound(X65,X63,X64))))))))))),inference(distribute,[status(thm)],[c102])).
% 174.29/174.65 cnf(c106,plain,~apply(X746,X745,skolem0012(X746,X744,X745))|lower_bound(X745,X746,X744),inference(split_conjunct,[status(thm)],[c103])).
% 174.29/174.65 cnf(c30,negated_conjecture,lower_bound(skolem0005,skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c25])).
% 174.29/174.65 cnf(c104,plain,~lower_bound(X730,X731,X733)|~member(X732,X733)|apply(X731,X730,X732),inference(split_conjunct,[status(thm)],[c103])).
% 174.29/174.65 cnf(c1176,plain,~member(X737,skolem0004)|apply(skolem0001,skolem0005,X737),inference(resolution,[status(thm)],[c104, c30])).
% 174.29/174.65 cnf(c29,negated_conjecture,subset(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c25])).
% 174.29/174.65 fof(subset,axiom,(![A]:(![B]:(subset(A,B)<=>(![X]:(member(X,A)=>member(X,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax', subset)).
% 174.29/174.65 fof(c271,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])).
% 174.29/174.65 fof(c272,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)],[c271])).
% 174.29/174.65 fof(c273,plain,((![X148]:(![X149]:(~subset(X148,X149)|(![X150]:(~member(X150,X148)|member(X150,X149))))))&(![X151]:(![X152]:((?[X153]:(member(X153,X151)&~member(X153,X152)))|subset(X151,X152))))),inference(variable_rename,[status(thm)],[c272])).
% 174.29/174.65 fof(c275,plain,(![X148]:(![X149]:(![X150]:(![X151]:(![X152]:((~subset(X148,X149)|(~member(X150,X148)|member(X150,X149)))&((member(skolem0024(X151,X152),X151)&~member(skolem0024(X151,X152),X152))|subset(X151,X152)))))))),inference(shift_quantors,[status(thm)],[fof(c274,plain,((![X148]:(![X149]:(~subset(X148,X149)|(![X150]:(~member(X150,X148)|member(X150,X149))))))&(![X151]:(![X152]:((member(skolem0024(X151,X152),X151)&~member(skolem0024(X151,X152),X152))|subset(X151,X152))))),inference(skolemize,[status(esa)],[c273])).])).
% 174.29/174.65 fof(c276,plain,(![X148]:(![X149]:(![X150]:(![X151]:(![X152]:((~subset(X148,X149)|(~member(X150,X148)|member(X150,X149)))&((member(skolem0024(X151,X152),X151)|subset(X151,X152))&(~member(skolem0024(X151,X152),X152)|subset(X151,X152))))))))),inference(distribute,[status(thm)],[c275])).
% 174.29/174.65 cnf(c277,plain,~subset(X342,X341)|~member(X340,X342)|member(X340,X341),inference(split_conjunct,[status(thm)],[c276])).
% 174.29/174.65 cnf(c105,plain,member(skolem0012(X451,X449,X450),X449)|lower_bound(X450,X451,X449),inference(split_conjunct,[status(thm)],[c103])).
% 174.29/174.65 cnf(c510,plain,member(skolem0012(skolem0001,skolem0003,skolem0005),skolem0003),inference(resolution,[status(thm)],[c105, c31])).
% 174.29/174.65 cnf(c516,plain,~subset(skolem0003,X2887)|member(skolem0012(skolem0001,skolem0003,skolem0005),X2887),inference(resolution,[status(thm)],[c510, c277])).
% 174.29/174.65 cnf(c9842,plain,member(skolem0012(skolem0001,skolem0003,skolem0005),skolem0004),inference(resolution,[status(thm)],[c516, c29])).
% 174.29/174.65 cnf(c10194,plain,apply(skolem0001,skolem0005,skolem0012(skolem0001,skolem0003,skolem0005)),inference(resolution,[status(thm)],[c9842, c1176])).
% 174.29/174.65 cnf(c162681,plain,lower_bound(skolem0005,skolem0001,skolem0003),inference(resolution,[status(thm)],[c10194, c106])).
% 174.29/174.65 cnf(c162687,plain,$false,inference(resolution,[status(thm)],[c162681, c31])).
% 174.29/174.65 % SZS output end CNFRefutation
% 174.29/174.65
% 174.29/174.65 % Initial clauses : 165
% 174.29/174.65 % Processed clauses : 2068
% 174.29/174.65 % Factors computed : 55
% 174.29/174.65 % Resolvents computed: 162355
% 174.29/174.65 % Tautologies deleted: 8
% 174.29/174.65 % Forward subsumed : 5764
% 174.29/174.65 % Backward subsumed : 6
% 174.29/174.65 % -------- CPU Time ---------
% 174.29/174.65 % User time : 173.848 s
% 174.29/174.65 % System time : 0.351 s
% 174.29/174.65 % Total time : 174.199 s
%------------------------------------------------------------------------------