%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET804+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:07 EDT 2024
% Result : Theorem 0.73s 0.91s
% Output : Refutation 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET804+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 : n022.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 18:56:38 EDT 2024
% 0.14/0.37 % CPUTime :
% 0.73/0.91 % Version: 1.5
% 0.73/0.91 % SZS status Theorem
% 0.73/0.91 % SZS output start CNFRefutation
% 0.73/0.91 fof(thIV16,conjecture,(![R]:(![E]:(order(R,E)=>(![M1]:(![M2]:(((min(M1,R,E)&min(M2,R,E))&M1!=M2)=>(~(?[M]:least(M,R,E))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thIV16)).
% 0.73/0.91 fof(c12,negated_conjecture,(~(![R]:(![E]:(order(R,E)=>(![M1]:(![M2]:(((min(M1,R,E)&min(M2,R,E))&M1!=M2)=>(~(?[M]:least(M,R,E)))))))))),inference(assume_negation,[status(cth)],[thIV16])).
% 0.73/0.91 fof(c13,negated_conjecture,(?[R]:(?[E]:(order(R,E)&(?[M1]:(?[M2]:(((min(M1,R,E)&min(M2,R,E))&M1!=M2)&(?[M]:least(M,R,E)))))))),inference(fof_nnf,[status(thm)],[c12])).
% 0.73/0.91 fof(c14,negated_conjecture,(?[R]:(?[E]:(order(R,E)&((?[M1]:(?[M2]:((min(M1,R,E)&min(M2,R,E))&M1!=M2)))&(?[M]:least(M,R,E)))))),inference(shift_quantors,[status(thm)],[c13])).
% 0.73/0.91 fof(c15,negated_conjecture,(?[X2]:(?[X3]:(order(X2,X3)&((?[X4]:(?[X5]:((min(X4,X2,X3)&min(X5,X2,X3))&X4!=X5)))&(?[X6]:least(X6,X2,X3)))))),inference(variable_rename,[status(thm)],[c14])).
% 0.73/0.91 fof(c16,negated_conjecture,(order(skolem0001,skolem0002)&(((min(skolem0003,skolem0001,skolem0002)&min(skolem0004,skolem0001,skolem0002))&skolem0003!=skolem0004)&least(skolem0005,skolem0001,skolem0002))),inference(skolemize,[status(esa)],[c15])).
% 0.73/0.91 cnf(c20,negated_conjecture,skolem0003!=skolem0004,inference(split_conjunct,[status(thm)],[c16])).
% 0.73/0.91 cnf(transitivity,axiom,X103!=X105|X105!=X104|X103=X104,theory(equality)).
% 0.73/0.91 cnf(symmetry,axiom,X100!=X101|X101=X100,theory(equality)).
% 0.73/0.91 cnf(c21,negated_conjecture,least(skolem0005,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c16])).
% 0.73/0.91 fof(least,axiom,(![R]:(![E]:(![M]:(least(M,R,E)<=>(member(M,E)&(![X]:(member(X,E)=>apply(R,M,X)))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', least)).
% 0.73/0.91 fof(c68,plain,(![R]:(![E]:(![M]:((~least(M,R,E)|(member(M,E)&(![X]:(~member(X,E)|apply(R,M,X)))))&((~member(M,E)|(?[X]:(member(X,E)&~apply(R,M,X))))|least(M,R,E)))))),inference(fof_nnf,[status(thm)],[least])).
% 0.73/0.91 fof(c69,plain,((![R]:(![E]:(![M]:(~least(M,R,E)|(member(M,E)&(![X]:(~member(X,E)|apply(R,M,X))))))))&(![R]:(![E]:(![M]:((~member(M,E)|(?[X]:(member(X,E)&~apply(R,M,X))))|least(M,R,E)))))),inference(shift_quantors,[status(thm)],[c68])).
% 0.73/0.91 fof(c70,plain,((![X43]:(![X44]:(![X45]:(~least(X45,X43,X44)|(member(X45,X44)&(![X46]:(~member(X46,X44)|apply(X43,X45,X46))))))))&(![X47]:(![X48]:(![X49]:((~member(X49,X48)|(?[X50]:(member(X50,X48)&~apply(X47,X49,X50))))|least(X49,X47,X48)))))),inference(variable_rename,[status(thm)],[c69])).
% 0.73/0.91 fof(c72,plain,(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:((~least(X45,X43,X44)|(member(X45,X44)&(~member(X46,X44)|apply(X43,X45,X46))))&((~member(X49,X48)|(member(skolem0010(X47,X48,X49),X48)&~apply(X47,X49,skolem0010(X47,X48,X49))))|least(X49,X47,X48)))))))))),inference(shift_quantors,[status(thm)],[fof(c71,plain,((![X43]:(![X44]:(![X45]:(~least(X45,X43,X44)|(member(X45,X44)&(![X46]:(~member(X46,X44)|apply(X43,X45,X46))))))))&(![X47]:(![X48]:(![X49]:((~member(X49,X48)|(member(skolem0010(X47,X48,X49),X48)&~apply(X47,X49,skolem0010(X47,X48,X49))))|least(X49,X47,X48)))))),inference(skolemize,[status(esa)],[c70])).])).
% 0.73/0.91 fof(c73,plain,(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:(((~least(X45,X43,X44)|member(X45,X44))&(~least(X45,X43,X44)|(~member(X46,X44)|apply(X43,X45,X46))))&(((~member(X49,X48)|member(skolem0010(X47,X48,X49),X48))|least(X49,X47,X48))&((~member(X49,X48)|~apply(X47,X49,skolem0010(X47,X48,X49)))|least(X49,X47,X48))))))))))),inference(distribute,[status(thm)],[c72])).
% 0.73/0.91 cnf(c74,plain,~least(X126,X127,X125)|member(X126,X125),inference(split_conjunct,[status(thm)],[c73])).
% 0.73/0.91 cnf(c195,plain,member(skolem0005,skolem0002),inference(resolution,[status(thm)],[c74, c21])).
% 0.73/0.91 cnf(c19,negated_conjecture,min(skolem0004,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c16])).
% 0.73/0.91 fof(min,axiom,(![R]:(![E]:(![M]:(min(M,R,E)<=>(member(M,E)&(![X]:((member(X,E)&apply(R,X,M))=>M=X))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', min)).
% 0.73/0.91 fof(c46,plain,(![R]:(![E]:(![M]:((~min(M,R,E)|(member(M,E)&(![X]:((~member(X,E)|~apply(R,X,M))|M=X))))&((~member(M,E)|(?[X]:((member(X,E)&apply(R,X,M))&M!=X)))|min(M,R,E)))))),inference(fof_nnf,[status(thm)],[min])).
% 0.73/0.91 fof(c47,plain,((![R]:(![E]:(![M]:(~min(M,R,E)|(member(M,E)&(![X]:((~member(X,E)|~apply(R,X,M))|M=X)))))))&(![R]:(![E]:(![M]:((~member(M,E)|(?[X]:((member(X,E)&apply(R,X,M))&M!=X)))|min(M,R,E)))))),inference(shift_quantors,[status(thm)],[c46])).
% 0.73/0.91 fof(c48,plain,((![X27]:(![X28]:(![X29]:(~min(X29,X27,X28)|(member(X29,X28)&(![X30]:((~member(X30,X28)|~apply(X27,X30,X29))|X29=X30)))))))&(![X31]:(![X32]:(![X33]:((~member(X33,X32)|(?[X34]:((member(X34,X32)&apply(X31,X34,X33))&X33!=X34)))|min(X33,X31,X32)))))),inference(variable_rename,[status(thm)],[c47])).
% 0.73/0.91 fof(c50,plain,(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:((~min(X29,X27,X28)|(member(X29,X28)&((~member(X30,X28)|~apply(X27,X30,X29))|X29=X30)))&((~member(X33,X32)|((member(skolem0008(X31,X32,X33),X32)&apply(X31,skolem0008(X31,X32,X33),X33))&X33!=skolem0008(X31,X32,X33)))|min(X33,X31,X32)))))))))),inference(shift_quantors,[status(thm)],[fof(c49,plain,((![X27]:(![X28]:(![X29]:(~min(X29,X27,X28)|(member(X29,X28)&(![X30]:((~member(X30,X28)|~apply(X27,X30,X29))|X29=X30)))))))&(![X31]:(![X32]:(![X33]:((~member(X33,X32)|((member(skolem0008(X31,X32,X33),X32)&apply(X31,skolem0008(X31,X32,X33),X33))&X33!=skolem0008(X31,X32,X33)))|min(X33,X31,X32)))))),inference(skolemize,[status(esa)],[c48])).])).
% 0.73/0.91 fof(c51,plain,(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(((~min(X29,X27,X28)|member(X29,X28))&(~min(X29,X27,X28)|((~member(X30,X28)|~apply(X27,X30,X29))|X29=X30)))&((((~member(X33,X32)|member(skolem0008(X31,X32,X33),X32))|min(X33,X31,X32))&((~member(X33,X32)|apply(X31,skolem0008(X31,X32,X33),X33))|min(X33,X31,X32)))&((~member(X33,X32)|X33!=skolem0008(X31,X32,X33))|min(X33,X31,X32))))))))))),inference(distribute,[status(thm)],[c50])).
% 0.73/0.91 cnf(c52,plain,~min(X117,X116,X115)|member(X117,X115),inference(split_conjunct,[status(thm)],[c51])).
% 0.73/0.91 cnf(c191,plain,member(skolem0004,skolem0002),inference(resolution,[status(thm)],[c52, c19])).
% 0.73/0.91 cnf(c75,plain,~least(X177,X178,X175)|~member(X176,X175)|apply(X178,X177,X176),inference(split_conjunct,[status(thm)],[c73])).
% 0.73/0.91 cnf(c211,plain,~member(X179,skolem0002)|apply(skolem0001,skolem0005,X179),inference(resolution,[status(thm)],[c75, c21])).
% 0.73/0.91 cnf(c214,plain,apply(skolem0001,skolem0005,skolem0004),inference(resolution,[status(thm)],[c211, c191])).
% 0.73/0.91 cnf(c53,plain,~min(X306,X305,X303)|~member(X304,X303)|~apply(X305,X304,X306)|X306=X304,inference(split_conjunct,[status(thm)],[c51])).
% 0.73/0.91 cnf(c354,plain,~min(skolem0004,skolem0001,X408)|~member(skolem0005,X408)|skolem0004=skolem0005,inference(resolution,[status(thm)],[c53, c214])).
% 0.73/0.91 cnf(c728,plain,~member(skolem0005,skolem0002)|skolem0004=skolem0005,inference(resolution,[status(thm)],[c354, c19])).
% 0.73/0.91 cnf(c730,plain,skolem0004=skolem0005,inference(resolution,[status(thm)],[c728, c195])).
% 0.73/0.91 cnf(c760,plain,skolem0005=skolem0004,inference(resolution,[status(thm)],[c730, symmetry])).
% 0.73/0.91 cnf(c764,plain,X419!=skolem0005|X419=skolem0004,inference(resolution,[status(thm)],[c760, transitivity])).
% 0.73/0.91 cnf(c18,negated_conjecture,min(skolem0003,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c16])).
% 0.73/0.91 cnf(c192,plain,member(skolem0003,skolem0002),inference(resolution,[status(thm)],[c52, c18])).
% 0.73/0.91 cnf(c213,plain,apply(skolem0001,skolem0005,skolem0003),inference(resolution,[status(thm)],[c211, c192])).
% 0.73/0.91 cnf(c363,plain,~min(skolem0003,skolem0001,X427)|~member(skolem0005,X427)|skolem0003=skolem0005,inference(resolution,[status(thm)],[c53, c213])).
% 0.73/0.91 cnf(c842,plain,~member(skolem0005,skolem0002)|skolem0003=skolem0005,inference(resolution,[status(thm)],[c363, c18])).
% 0.73/0.91 cnf(c889,plain,skolem0003=skolem0005,inference(resolution,[status(thm)],[c842, c195])).
% 0.73/0.91 cnf(c892,plain,skolem0003=skolem0004,inference(resolution,[status(thm)],[c889, c764])).
% 0.73/0.91 cnf(c897,plain,$false,inference(resolution,[status(thm)],[c892, c20])).
% 0.73/0.91 % SZS output end CNFRefutation
% 0.73/0.91
% 0.73/0.91 % Initial clauses : 125
% 0.73/0.91 % Processed clauses : 136
% 0.73/0.91 % Factors computed : 4
% 0.73/0.91 % Resolvents computed: 756
% 0.73/0.91 % Tautologies deleted: 2
% 0.73/0.91 % Forward subsumed : 36
% 0.73/0.91 % Backward subsumed : 4
% 0.73/0.91 % -------- CPU Time ---------
% 0.73/0.91 % User time : 0.512 s
% 0.73/0.91 % System time : 0.023 s
% 0.73/0.91 % Total time : 0.535 s
%------------------------------------------------------------------------------