%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET794+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 5.55s 5.72s
% Output : Refutation 5.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET794+4 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n024.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 19:43:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 5.55/5.72 % Version: 1.5
% 5.55/5.72 % SZS status Theorem
% 5.55/5.72 % SZS output start CNFRefutation
% 5.55/5.72 fof(thIV6,conjecture,(![R]:(![E]:(![M]:((total_order(R,E)&min(M,R,E))=>least(M,R,E))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thIV6)).
% 5.55/5.72 fof(c12,negated_conjecture,(~(![R]:(![E]:(![M]:((total_order(R,E)&min(M,R,E))=>least(M,R,E)))))),inference(assume_negation,[status(cth)],[thIV6])).
% 5.55/5.72 fof(c13,negated_conjecture,(?[R]:(?[E]:(?[M]:((total_order(R,E)&min(M,R,E))&~least(M,R,E))))),inference(fof_nnf,[status(thm)],[c12])).
% 5.55/5.72 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((total_order(X2,X3)&min(X4,X2,X3))&~least(X4,X2,X3))))),inference(variable_rename,[status(thm)],[c13])).
% 5.55/5.72 fof(c15,negated_conjecture,((total_order(skolem0001,skolem0002)&min(skolem0003,skolem0001,skolem0002))&~least(skolem0003,skolem0001,skolem0002)),inference(skolemize,[status(esa)],[c14])).
% 5.55/5.72 cnf(c18,negated_conjecture,~least(skolem0003,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 5.55/5.72 cnf(c17,negated_conjecture,min(skolem0003,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 5.55/5.72 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/sandbox2/benchmark/Axioms/SET006+3.ax', min)).
% 5.55/5.72 fof(c43,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])).
% 5.55/5.72 fof(c44,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)],[c43])).
% 5.55/5.72 fof(c45,plain,((![X25]:(![X26]:(![X27]:(~min(X27,X25,X26)|(member(X27,X26)&(![X28]:((~member(X28,X26)|~apply(X25,X28,X27))|X27=X28)))))))&(![X29]:(![X30]:(![X31]:((~member(X31,X30)|(?[X32]:((member(X32,X30)&apply(X29,X32,X31))&X31!=X32)))|min(X31,X29,X30)))))),inference(variable_rename,[status(thm)],[c44])).
% 5.55/5.72 fof(c47,plain,(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((~min(X27,X25,X26)|(member(X27,X26)&((~member(X28,X26)|~apply(X25,X28,X27))|X27=X28)))&((~member(X31,X30)|((member(skolem0006(X29,X30,X31),X30)&apply(X29,skolem0006(X29,X30,X31),X31))&X31!=skolem0006(X29,X30,X31)))|min(X31,X29,X30)))))))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X25]:(![X26]:(![X27]:(~min(X27,X25,X26)|(member(X27,X26)&(![X28]:((~member(X28,X26)|~apply(X25,X28,X27))|X27=X28)))))))&(![X29]:(![X30]:(![X31]:((~member(X31,X30)|((member(skolem0006(X29,X30,X31),X30)&apply(X29,skolem0006(X29,X30,X31),X31))&X31!=skolem0006(X29,X30,X31)))|min(X31,X29,X30)))))),inference(skolemize,[status(esa)],[c45])).])).
% 5.55/5.72 fof(c48,plain,(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(((~min(X27,X25,X26)|member(X27,X26))&(~min(X27,X25,X26)|((~member(X28,X26)|~apply(X25,X28,X27))|X27=X28)))&((((~member(X31,X30)|member(skolem0006(X29,X30,X31),X30))|min(X31,X29,X30))&((~member(X31,X30)|apply(X29,skolem0006(X29,X30,X31),X31))|min(X31,X29,X30)))&((~member(X31,X30)|X31!=skolem0006(X29,X30,X31))|min(X31,X29,X30))))))))))),inference(distribute,[status(thm)],[c47])).
% 5.55/5.72 cnf(c49,plain,~min(X113,X114,X115)|member(X113,X115),inference(split_conjunct,[status(thm)],[c48])).
% 5.55/5.72 cnf(c189,plain,member(skolem0003,skolem0002),inference(resolution,[status(thm)],[c49, c17])).
% 5.55/5.72 fof(least,axiom,(![R]:(![E]:(![M]:(least(M,R,E)<=>(member(M,E)&(![X]:(member(X,E)=>apply(R,M,X)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+3.ax', least)).
% 5.55/5.72 fof(c65,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])).
% 5.55/5.72 fof(c66,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)],[c65])).
% 5.55/5.72 fof(c67,plain,((![X41]:(![X42]:(![X43]:(~least(X43,X41,X42)|(member(X43,X42)&(![X44]:(~member(X44,X42)|apply(X41,X43,X44))))))))&(![X45]:(![X46]:(![X47]:((~member(X47,X46)|(?[X48]:(member(X48,X46)&~apply(X45,X47,X48))))|least(X47,X45,X46)))))),inference(variable_rename,[status(thm)],[c66])).
% 5.55/5.72 fof(c69,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:((~least(X43,X41,X42)|(member(X43,X42)&(~member(X44,X42)|apply(X41,X43,X44))))&((~member(X47,X46)|(member(skolem0008(X45,X46,X47),X46)&~apply(X45,X47,skolem0008(X45,X46,X47))))|least(X47,X45,X46)))))))))),inference(shift_quantors,[status(thm)],[fof(c68,plain,((![X41]:(![X42]:(![X43]:(~least(X43,X41,X42)|(member(X43,X42)&(![X44]:(~member(X44,X42)|apply(X41,X43,X44))))))))&(![X45]:(![X46]:(![X47]:((~member(X47,X46)|(member(skolem0008(X45,X46,X47),X46)&~apply(X45,X47,skolem0008(X45,X46,X47))))|least(X47,X45,X46)))))),inference(skolemize,[status(esa)],[c67])).])).
% 5.55/5.72 fof(c70,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(((~least(X43,X41,X42)|member(X43,X42))&(~least(X43,X41,X42)|(~member(X44,X42)|apply(X41,X43,X44))))&(((~member(X47,X46)|member(skolem0008(X45,X46,X47),X46))|least(X47,X45,X46))&((~member(X47,X46)|~apply(X45,X47,skolem0008(X45,X46,X47)))|least(X47,X45,X46))))))))))),inference(distribute,[status(thm)],[c69])).
% 5.55/5.72 cnf(c74,plain,~member(X282,X281)|~apply(X280,X282,skolem0008(X280,X281,X282))|least(X282,X280,X281),inference(split_conjunct,[status(thm)],[c70])).
% 5.55/5.72 cnf(reflexivity,axiom,X97=X97,theory(equality)).
% 5.55/5.72 cnf(c73,plain,~member(X238,X237)|member(skolem0008(X236,X237,X238),X237)|least(X238,X236,X237),inference(split_conjunct,[status(thm)],[c70])).
% 5.55/5.72 cnf(c219,plain,member(skolem0008(X298,skolem0002,skolem0003),skolem0002)|least(skolem0003,X298,skolem0002),inference(resolution,[status(thm)],[c73, c189])).
% 5.55/5.72 cnf(c304,plain,member(skolem0008(skolem0001,skolem0002,skolem0003),skolem0002),inference(resolution,[status(thm)],[c219, c18])).
% 5.55/5.72 cnf(c50,plain,~min(X260,X262,X263)|~member(X261,X263)|~apply(X262,X261,X260)|X260=X261,inference(split_conjunct,[status(thm)],[c48])).
% 5.55/5.72 cnf(c16,negated_conjecture,total_order(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 5.55/5.72 fof(total_order,axiom,(![R]:(![E]:(total_order(R,E)<=>(order(R,E)&(![X]:(![Y]:((member(X,E)&member(Y,E))=>(apply(R,X,Y)|apply(R,Y,X))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+3.ax', total_order)).
% 5.55/5.72 fof(c103,plain,(![R]:(![E]:((~total_order(R,E)|(order(R,E)&(![X]:(![Y]:((~member(X,E)|~member(Y,E))|(apply(R,X,Y)|apply(R,Y,X)))))))&((~order(R,E)|(?[X]:(?[Y]:((member(X,E)&member(Y,E))&(~apply(R,X,Y)&~apply(R,Y,X))))))|total_order(R,E))))),inference(fof_nnf,[status(thm)],[total_order])).
% 5.55/5.72 fof(c104,plain,((![R]:(![E]:(~total_order(R,E)|(order(R,E)&(![X]:(![Y]:((~member(X,E)|~member(Y,E))|(apply(R,X,Y)|apply(R,Y,X)))))))))&(![R]:(![E]:((~order(R,E)|(?[X]:(?[Y]:((member(X,E)&member(Y,E))&(~apply(R,X,Y)&~apply(R,Y,X))))))|total_order(R,E))))),inference(shift_quantors,[status(thm)],[c103])).
% 5.55/5.72 fof(c105,plain,((![X73]:(![X74]:(~total_order(X73,X74)|(order(X73,X74)&(![X75]:(![X76]:((~member(X75,X74)|~member(X76,X74))|(apply(X73,X75,X76)|apply(X73,X76,X75)))))))))&(![X77]:(![X78]:((~order(X77,X78)|(?[X79]:(?[X80]:((member(X79,X78)&member(X80,X78))&(~apply(X77,X79,X80)&~apply(X77,X80,X79))))))|total_order(X77,X78))))),inference(variable_rename,[status(thm)],[c104])).
% 5.55/5.72 fof(c107,plain,(![X73]:(![X74]:(![X75]:(![X76]:(![X77]:(![X78]:((~total_order(X73,X74)|(order(X73,X74)&((~member(X75,X74)|~member(X76,X74))|(apply(X73,X75,X76)|apply(X73,X76,X75)))))&((~order(X77,X78)|((member(skolem0012(X77,X78),X78)&member(skolem0013(X77,X78),X78))&(~apply(X77,skolem0012(X77,X78),skolem0013(X77,X78))&~apply(X77,skolem0013(X77,X78),skolem0012(X77,X78)))))|total_order(X77,X78))))))))),inference(shift_quantors,[status(thm)],[fof(c106,plain,((![X73]:(![X74]:(~total_order(X73,X74)|(order(X73,X74)&(![X75]:(![X76]:((~member(X75,X74)|~member(X76,X74))|(apply(X73,X75,X76)|apply(X73,X76,X75)))))))))&(![X77]:(![X78]:((~order(X77,X78)|((member(skolem0012(X77,X78),X78)&member(skolem0013(X77,X78),X78))&(~apply(X77,skolem0012(X77,X78),skolem0013(X77,X78))&~apply(X77,skolem0013(X77,X78),skolem0012(X77,X78)))))|total_order(X77,X78))))),inference(skolemize,[status(esa)],[c105])).])).
% 5.55/5.72 fof(c108,plain,(![X73]:(![X74]:(![X75]:(![X76]:(![X77]:(![X78]:(((~total_order(X73,X74)|order(X73,X74))&(~total_order(X73,X74)|((~member(X75,X74)|~member(X76,X74))|(apply(X73,X75,X76)|apply(X73,X76,X75)))))&((((~order(X77,X78)|member(skolem0012(X77,X78),X78))|total_order(X77,X78))&((~order(X77,X78)|member(skolem0013(X77,X78),X78))|total_order(X77,X78)))&(((~order(X77,X78)|~apply(X77,skolem0012(X77,X78),skolem0013(X77,X78)))|total_order(X77,X78))&((~order(X77,X78)|~apply(X77,skolem0013(X77,X78),skolem0012(X77,X78)))|total_order(X77,X78))))))))))),inference(distribute,[status(thm)],[c107])).
% 5.55/5.72 cnf(c110,plain,~total_order(X399,X396)|~member(X397,X396)|~member(X398,X396)|apply(X399,X397,X398)|apply(X399,X398,X397),inference(split_conjunct,[status(thm)],[c108])).
% 5.55/5.72 cnf(c390,plain,~total_order(X470,skolem0002)|~member(X469,skolem0002)|apply(X470,X469,skolem0003)|apply(X470,skolem0003,X469),inference(resolution,[status(thm)],[c110, c189])).
% 5.55/5.72 cnf(c701,plain,~total_order(X2249,skolem0002)|apply(X2249,skolem0008(skolem0001,skolem0002,skolem0003),skolem0003)|apply(X2249,skolem0003,skolem0008(skolem0001,skolem0002,skolem0003)),inference(resolution,[status(thm)],[c390, c304])).
% 5.55/5.72 cnf(c13604,plain,apply(skolem0001,skolem0008(skolem0001,skolem0002,skolem0003),skolem0003)|apply(skolem0001,skolem0003,skolem0008(skolem0001,skolem0002,skolem0003)),inference(resolution,[status(thm)],[c701, c16])).
% 5.55/5.72 cnf(c13615,plain,apply(skolem0001,skolem0008(skolem0001,skolem0002,skolem0003),skolem0003)|~member(skolem0003,skolem0002)|least(skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c13604, c74])).
% 5.55/5.72 cnf(c13617,plain,apply(skolem0001,skolem0008(skolem0001,skolem0002,skolem0003),skolem0003)|least(skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c13615, c189])).
% 5.55/5.72 cnf(c13625,plain,apply(skolem0001,skolem0008(skolem0001,skolem0002,skolem0003),skolem0003),inference(resolution,[status(thm)],[c13617, c18])).
% 5.55/5.72 cnf(c13630,plain,~min(skolem0003,skolem0001,X2295)|~member(skolem0008(skolem0001,skolem0002,skolem0003),X2295)|skolem0003=skolem0008(skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c13625, c50])).
% 5.55/5.72 cnf(c14123,plain,~min(skolem0003,skolem0001,skolem0002)|skolem0003=skolem0008(skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c13630, c304])).
% 5.55/5.72 cnf(c14141,plain,skolem0003=skolem0008(skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c14123, c17])).
% 5.55/5.72 cnf(c2,axiom,X151!=X148|X149!=X153|X152!=X150|~apply(X151,X149,X152)|apply(X148,X153,X150),theory(equality)).
% 5.55/5.72 cnf(c13627,plain,skolem0001!=X2259|skolem0008(skolem0001,skolem0002,skolem0003)!=X2258|skolem0003!=X2257|apply(X2259,X2258,X2257),inference(resolution,[status(thm)],[c13625, c2])).
% 5.55/5.72 cnf(symmetry,axiom,X98!=X99|X99=X98,theory(equality)).
% 5.55/5.72 cnf(c14161,plain,skolem0008(skolem0001,skolem0002,skolem0003)=skolem0003,inference(resolution,[status(thm)],[c14141, symmetry])).
% 5.55/5.72 cnf(c14268,plain,skolem0001!=X2305|skolem0003!=X2306|apply(X2305,skolem0003,X2306),inference(resolution,[status(thm)],[c14161, c13627])).
% 5.55/5.72 cnf(c14763,plain,skolem0001!=X2319|apply(X2319,skolem0003,skolem0008(skolem0001,skolem0002,skolem0003)),inference(resolution,[status(thm)],[c14268, c14141])).
% 5.55/5.72 cnf(c15202,plain,apply(skolem0001,skolem0003,skolem0008(skolem0001,skolem0002,skolem0003)),inference(resolution,[status(thm)],[c14763, reflexivity])).
% 5.55/5.72 cnf(c15208,plain,~member(skolem0003,skolem0002)|least(skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c15202, c74])).
% 5.55/5.72 cnf(c15209,plain,least(skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c15208, c189])).
% 5.55/5.72 cnf(c15430,plain,$false,inference(resolution,[status(thm)],[c15209, c18])).
% 5.55/5.72 % SZS output end CNFRefutation
% 5.55/5.72
% 5.55/5.72 % Initial clauses : 123
% 5.55/5.72 % Processed clauses : 665
% 5.55/5.72 % Factors computed : 68
% 5.55/5.72 % Resolvents computed: 15180
% 5.55/5.72 % Tautologies deleted: 6
% 5.55/5.72 % Forward subsumed : 296
% 5.55/5.72 % Backward subsumed : 19
% 5.55/5.72 % -------- CPU Time ---------
% 5.55/5.72 % User time : 5.322 s
% 5.55/5.72 % System time : 0.050 s
% 5.55/5.72 % Total time : 5.372 s
%------------------------------------------------------------------------------