%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET793+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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.10s 5.33s
% Output : Refutation 5.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SET793+4 : TPTP v8.1.2. Released v3.2.0.
% 0.14/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n015.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 18:34:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 5.10/5.33 % Version: 1.5
% 5.10/5.33 % SZS status Theorem
% 5.10/5.33 % SZS output start CNFRefutation
% 5.10/5.33 fof(thIV5,conjecture,(![R]:(![E]:(![M]:((total_order(R,E)&max(M,R,E))=>greatest(M,R,E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thIV5)).
% 5.10/5.33 fof(c12,negated_conjecture,(~(![R]:(![E]:(![M]:((total_order(R,E)&max(M,R,E))=>greatest(M,R,E)))))),inference(assume_negation,[status(cth)],[thIV5])).
% 5.10/5.33 fof(c13,negated_conjecture,(?[R]:(?[E]:(?[M]:((total_order(R,E)&max(M,R,E))&~greatest(M,R,E))))),inference(fof_nnf,[status(thm)],[c12])).
% 5.10/5.33 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((total_order(X2,X3)&max(X4,X2,X3))&~greatest(X4,X2,X3))))),inference(variable_rename,[status(thm)],[c13])).
% 5.10/5.33 fof(c15,negated_conjecture,((total_order(skolem0001,skolem0002)&max(skolem0003,skolem0001,skolem0002))&~greatest(skolem0003,skolem0001,skolem0002)),inference(skolemize,[status(esa)],[c14])).
% 5.10/5.33 cnf(c18,negated_conjecture,~greatest(skolem0003,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 5.10/5.33 cnf(c17,negated_conjecture,max(skolem0003,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 5.10/5.33 fof(max,axiom,(![R]:(![E]:(![M]:(max(M,R,E)<=>(member(M,E)&(![X]:((member(X,E)&apply(R,M,X))=>M=X))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', max)).
% 5.10/5.33 fof(c54,plain,(![R]:(![E]:(![M]:((~max(M,R,E)|(member(M,E)&(![X]:((~member(X,E)|~apply(R,M,X))|M=X))))&((~member(M,E)|(?[X]:((member(X,E)&apply(R,M,X))&M!=X)))|max(M,R,E)))))),inference(fof_nnf,[status(thm)],[max])).
% 5.10/5.33 fof(c55,plain,((![R]:(![E]:(![M]:(~max(M,R,E)|(member(M,E)&(![X]:((~member(X,E)|~apply(R,M,X))|M=X)))))))&(![R]:(![E]:(![M]:((~member(M,E)|(?[X]:((member(X,E)&apply(R,M,X))&M!=X)))|max(M,R,E)))))),inference(shift_quantors,[status(thm)],[c54])).
% 5.10/5.33 fof(c56,plain,((![X33]:(![X34]:(![X35]:(~max(X35,X33,X34)|(member(X35,X34)&(![X36]:((~member(X36,X34)|~apply(X33,X35,X36))|X35=X36)))))))&(![X37]:(![X38]:(![X39]:((~member(X39,X38)|(?[X40]:((member(X40,X38)&apply(X37,X39,X40))&X39!=X40)))|max(X39,X37,X38)))))),inference(variable_rename,[status(thm)],[c55])).
% 5.10/5.33 fof(c58,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:((~max(X35,X33,X34)|(member(X35,X34)&((~member(X36,X34)|~apply(X33,X35,X36))|X35=X36)))&((~member(X39,X38)|((member(skolem0007(X37,X38,X39),X38)&apply(X37,X39,skolem0007(X37,X38,X39)))&X39!=skolem0007(X37,X38,X39)))|max(X39,X37,X38)))))))))),inference(shift_quantors,[status(thm)],[fof(c57,plain,((![X33]:(![X34]:(![X35]:(~max(X35,X33,X34)|(member(X35,X34)&(![X36]:((~member(X36,X34)|~apply(X33,X35,X36))|X35=X36)))))))&(![X37]:(![X38]:(![X39]:((~member(X39,X38)|((member(skolem0007(X37,X38,X39),X38)&apply(X37,X39,skolem0007(X37,X38,X39)))&X39!=skolem0007(X37,X38,X39)))|max(X39,X37,X38)))))),inference(skolemize,[status(esa)],[c56])).])).
% 5.10/5.33 fof(c59,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(((~max(X35,X33,X34)|member(X35,X34))&(~max(X35,X33,X34)|((~member(X36,X34)|~apply(X33,X35,X36))|X35=X36)))&((((~member(X39,X38)|member(skolem0007(X37,X38,X39),X38))|max(X39,X37,X38))&((~member(X39,X38)|apply(X37,X39,skolem0007(X37,X38,X39)))|max(X39,X37,X38)))&((~member(X39,X38)|X39!=skolem0007(X37,X38,X39))|max(X39,X37,X38))))))))))),inference(distribute,[status(thm)],[c58])).
% 5.10/5.33 cnf(c60,plain,~max(X116,X117,X118)|member(X116,X118),inference(split_conjunct,[status(thm)],[c59])).
% 5.10/5.33 cnf(c189,plain,member(skolem0003,skolem0002),inference(resolution,[status(thm)],[c60, c17])).
% 5.10/5.33 fof(greatest,axiom,(![R]:(![E]:(![M]:(greatest(M,R,E)<=>(member(M,E)&(![X]:(member(X,E)=>apply(R,X,M)))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', greatest)).
% 5.10/5.33 fof(c75,plain,(![R]:(![E]:(![M]:((~greatest(M,R,E)|(member(M,E)&(![X]:(~member(X,E)|apply(R,X,M)))))&((~member(M,E)|(?[X]:(member(X,E)&~apply(R,X,M))))|greatest(M,R,E)))))),inference(fof_nnf,[status(thm)],[greatest])).
% 5.10/5.33 fof(c76,plain,((![R]:(![E]:(![M]:(~greatest(M,R,E)|(member(M,E)&(![X]:(~member(X,E)|apply(R,X,M))))))))&(![R]:(![E]:(![M]:((~member(M,E)|(?[X]:(member(X,E)&~apply(R,X,M))))|greatest(M,R,E)))))),inference(shift_quantors,[status(thm)],[c75])).
% 5.10/5.33 fof(c77,plain,((![X49]:(![X50]:(![X51]:(~greatest(X51,X49,X50)|(member(X51,X50)&(![X52]:(~member(X52,X50)|apply(X49,X52,X51))))))))&(![X53]:(![X54]:(![X55]:((~member(X55,X54)|(?[X56]:(member(X56,X54)&~apply(X53,X56,X55))))|greatest(X55,X53,X54)))))),inference(variable_rename,[status(thm)],[c76])).
% 5.10/5.33 fof(c79,plain,(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:((~greatest(X51,X49,X50)|(member(X51,X50)&(~member(X52,X50)|apply(X49,X52,X51))))&((~member(X55,X54)|(member(skolem0009(X53,X54,X55),X54)&~apply(X53,skolem0009(X53,X54,X55),X55)))|greatest(X55,X53,X54)))))))))),inference(shift_quantors,[status(thm)],[fof(c78,plain,((![X49]:(![X50]:(![X51]:(~greatest(X51,X49,X50)|(member(X51,X50)&(![X52]:(~member(X52,X50)|apply(X49,X52,X51))))))))&(![X53]:(![X54]:(![X55]:((~member(X55,X54)|(member(skolem0009(X53,X54,X55),X54)&~apply(X53,skolem0009(X53,X54,X55),X55)))|greatest(X55,X53,X54)))))),inference(skolemize,[status(esa)],[c77])).])).
% 5.10/5.33 fof(c80,plain,(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(((~greatest(X51,X49,X50)|member(X51,X50))&(~greatest(X51,X49,X50)|(~member(X52,X50)|apply(X49,X52,X51))))&(((~member(X55,X54)|member(skolem0009(X53,X54,X55),X54))|greatest(X55,X53,X54))&((~member(X55,X54)|~apply(X53,skolem0009(X53,X54,X55),X55))|greatest(X55,X53,X54))))))))))),inference(distribute,[status(thm)],[c79])).
% 5.10/5.33 cnf(c84,plain,~member(X285,X284)|~apply(X283,skolem0009(X283,X284,X285),X285)|greatest(X285,X283,X284),inference(split_conjunct,[status(thm)],[c80])).
% 5.10/5.33 cnf(reflexivity,axiom,X97=X97,theory(equality)).
% 5.10/5.33 cnf(c2,axiom,X153!=X148|X150!=X149|X152!=X151|~apply(X153,X150,X152)|apply(X148,X149,X151),theory(equality)).
% 5.10/5.33 cnf(c16,negated_conjecture,total_order(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 5.10/5.33 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/sandbox/benchmark/Axioms/SET006+3.ax', total_order)).
% 5.10/5.33 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.10/5.33 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.10/5.33 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.10/5.33 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.10/5.33 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.10/5.33 cnf(c109,plain,~total_order(X104,X105)|order(X104,X105),inference(split_conjunct,[status(thm)],[c108])).
% 5.10/5.33 cnf(c187,plain,order(skolem0001,skolem0002),inference(resolution,[status(thm)],[c109, c16])).
% 5.10/5.33 fof(order,axiom,(![R]:(![E]:(order(R,E)<=>(((![X]:(member(X,E)=>apply(R,X,X)))&(![X]:(![Y]:((member(X,E)&member(Y,E))=>((apply(R,X,Y)&apply(R,Y,X))=>X=Y)))))&(![X]:(![Y]:(![Z]:(((member(X,E)&member(Y,E))&member(Z,E))=>((apply(R,X,Y)&apply(R,Y,Z))=>apply(R,X,Z)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', order)).
% 5.10/5.33 fof(c115,plain,(![R]:(![E]:((~order(R,E)|(((![X]:(~member(X,E)|apply(R,X,X)))&(![X]:(![Y]:((~member(X,E)|~member(Y,E))|((~apply(R,X,Y)|~apply(R,Y,X))|X=Y)))))&(![X]:(![Y]:(![Z]:(((~member(X,E)|~member(Y,E))|~member(Z,E))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z))))))))&((((?[X]:(member(X,E)&~apply(R,X,X)))|(?[X]:(?[Y]:((member(X,E)&member(Y,E))&((apply(R,X,Y)&apply(R,Y,X))&X!=Y)))))|(?[X]:(?[Y]:(?[Z]:(((member(X,E)&member(Y,E))&member(Z,E))&((apply(R,X,Y)&apply(R,Y,Z))&~apply(R,X,Z)))))))|order(R,E))))),inference(fof_nnf,[status(thm)],[order])).
% 5.10/5.33 fof(c116,plain,((![R]:(![E]:(~order(R,E)|(((![X]:(~member(X,E)|apply(R,X,X)))&(![X]:(![Y]:((~member(X,E)|~member(Y,E))|((~apply(R,X,Y)|~apply(R,Y,X))|X=Y)))))&(![X]:(![Y]:(![Z]:(((~member(X,E)|~member(Y,E))|~member(Z,E))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z))))))))))&(![R]:(![E]:((((?[X]:(member(X,E)&~apply(R,X,X)))|(?[X]:(?[Y]:((member(X,E)&member(Y,E))&((apply(R,X,Y)&apply(R,Y,X))&X!=Y)))))|(?[X]:(?[Y]:(?[Z]:(((member(X,E)&member(Y,E))&member(Z,E))&((apply(R,X,Y)&apply(R,Y,Z))&~apply(R,X,Z)))))))|order(R,E))))),inference(shift_quantors,[status(thm)],[c115])).
% 5.10/5.33 fof(c117,plain,((![X81]:(![X82]:(~order(X81,X82)|(((![X83]:(~member(X83,X82)|apply(X81,X83,X83)))&(![X84]:(![X85]:((~member(X84,X82)|~member(X85,X82))|((~apply(X81,X84,X85)|~apply(X81,X85,X84))|X84=X85)))))&(![X86]:(![X87]:(![X88]:(((~member(X86,X82)|~member(X87,X82))|~member(X88,X82))|((~apply(X81,X86,X87)|~apply(X81,X87,X88))|apply(X81,X86,X88))))))))))&(![X89]:(![X90]:((((?[X91]:(member(X91,X90)&~apply(X89,X91,X91)))|(?[X92]:(?[X93]:((member(X92,X90)&member(X93,X90))&((apply(X89,X92,X93)&apply(X89,X93,X92))&X92!=X93)))))|(?[X94]:(?[X95]:(?[X96]:(((member(X94,X90)&member(X95,X90))&member(X96,X90))&((apply(X89,X94,X95)&apply(X89,X95,X96))&~apply(X89,X94,X96)))))))|order(X89,X90))))),inference(variable_rename,[status(thm)],[c116])).
% 5.10/5.33 fof(c119,plain,(![X81]:(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:(![X87]:(![X88]:(![X89]:(![X90]:((~order(X81,X82)|(((~member(X83,X82)|apply(X81,X83,X83))&((~member(X84,X82)|~member(X85,X82))|((~apply(X81,X84,X85)|~apply(X81,X85,X84))|X84=X85)))&(((~member(X86,X82)|~member(X87,X82))|~member(X88,X82))|((~apply(X81,X86,X87)|~apply(X81,X87,X88))|apply(X81,X86,X88)))))&((((member(skolem0014(X89,X90),X90)&~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90)))|((member(skolem0015(X89,X90),X90)&member(skolem0016(X89,X90),X90))&((apply(X89,skolem0015(X89,X90),skolem0016(X89,X90))&apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))&skolem0015(X89,X90)!=skolem0016(X89,X90))))|(((member(skolem0017(X89,X90),X90)&member(skolem0018(X89,X90),X90))&member(skolem0019(X89,X90),X90))&((apply(X89,skolem0017(X89,X90),skolem0018(X89,X90))&apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))&~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))))|order(X89,X90))))))))))))),inference(shift_quantors,[status(thm)],[fof(c118,plain,((![X81]:(![X82]:(~order(X81,X82)|(((![X83]:(~member(X83,X82)|apply(X81,X83,X83)))&(![X84]:(![X85]:((~member(X84,X82)|~member(X85,X82))|((~apply(X81,X84,X85)|~apply(X81,X85,X84))|X84=X85)))))&(![X86]:(![X87]:(![X88]:(((~member(X86,X82)|~member(X87,X82))|~member(X88,X82))|((~apply(X81,X86,X87)|~apply(X81,X87,X88))|apply(X81,X86,X88))))))))))&(![X89]:(![X90]:((((member(skolem0014(X89,X90),X90)&~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90)))|((member(skolem0015(X89,X90),X90)&member(skolem0016(X89,X90),X90))&((apply(X89,skolem0015(X89,X90),skolem0016(X89,X90))&apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))&skolem0015(X89,X90)!=skolem0016(X89,X90))))|(((member(skolem0017(X89,X90),X90)&member(skolem0018(X89,X90),X90))&member(skolem0019(X89,X90),X90))&((apply(X89,skolem0017(X89,X90),skolem0018(X89,X90))&apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))&~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))))|order(X89,X90))))),inference(skolemize,[status(esa)],[c117])).])).
% 5.10/5.33 fof(c120,plain,(![X81]:(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:(![X87]:(![X88]:(![X89]:(![X90]:((((~order(X81,X82)|(~member(X83,X82)|apply(X81,X83,X83)))&(~order(X81,X82)|((~member(X84,X82)|~member(X85,X82))|((~apply(X81,X84,X85)|~apply(X81,X85,X84))|X84=X85))))&(~order(X81,X82)|(((~member(X86,X82)|~member(X87,X82))|~member(X88,X82))|((~apply(X81,X86,X87)|~apply(X81,X87,X88))|apply(X81,X86,X88)))))&(((((((((member(skolem0014(X89,X90),X90)|member(skolem0015(X89,X90),X90))|member(skolem0017(X89,X90),X90))|order(X89,X90))&(((member(skolem0014(X89,X90),X90)|member(skolem0015(X89,X90),X90))|member(skolem0018(X89,X90),X90))|order(X89,X90)))&(((member(skolem0014(X89,X90),X90)|member(skolem0015(X89,X90),X90))|member(skolem0019(X89,X90),X90))|order(X89,X90)))&(((((member(skolem0014(X89,X90),X90)|member(skolem0015(X89,X90),X90))|apply(X89,skolem0017(X89,X90),skolem0018(X89,X90)))|order(X89,X90))&(((member(skolem0014(X89,X90),X90)|member(skolem0015(X89,X90),X90))|apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))&(((member(skolem0014(X89,X90),X90)|member(skolem0015(X89,X90),X90))|~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))|order(X89,X90))))&((((((member(skolem0014(X89,X90),X90)|member(skolem0016(X89,X90),X90))|member(skolem0017(X89,X90),X90))|order(X89,X90))&(((member(skolem0014(X89,X90),X90)|member(skolem0016(X89,X90),X90))|member(skolem0018(X89,X90),X90))|order(X89,X90)))&(((member(skolem0014(X89,X90),X90)|member(skolem0016(X89,X90),X90))|member(skolem0019(X89,X90),X90))|order(X89,X90)))&(((((member(skolem0014(X89,X90),X90)|member(skolem0016(X89,X90),X90))|apply(X89,skolem0017(X89,X90),skolem0018(X89,X90)))|order(X89,X90))&(((member(skolem0014(X89,X90),X90)|member(skolem0016(X89,X90),X90))|apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))&(((member(skolem0014(X89,X90),X90)|member(skolem0016(X89,X90),X90))|~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))))&((((((((member(skolem0014(X89,X90),X90)|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|member(skolem0017(X89,X90),X90))|order(X89,X90))&(((member(skolem0014(X89,X90),X90)|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|member(skolem0018(X89,X90),X90))|order(X89,X90)))&(((member(skolem0014(X89,X90),X90)|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|member(skolem0019(X89,X90),X90))|order(X89,X90)))&(((((member(skolem0014(X89,X90),X90)|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|apply(X89,skolem0017(X89,X90),skolem0018(X89,X90)))|order(X89,X90))&(((member(skolem0014(X89,X90),X90)|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))&(((member(skolem0014(X89,X90),X90)|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))|order(X89,X90))))&((((((member(skolem0014(X89,X90),X90)|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|member(skolem0017(X89,X90),X90))|order(X89,X90))&(((member(skolem0014(X89,X90),X90)|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|member(skolem0018(X89,X90),X90))|order(X89,X90)))&(((member(skolem0014(X89,X90),X90)|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|member(skolem0019(X89,X90),X90))|order(X89,X90)))&(((((member(skolem0014(X89,X90),X90)|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|apply(X89,skolem0017(X89,X90),skolem0018(X89,X90)))|order(X89,X90))&(((member(skolem0014(X89,X90),X90)|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))&(((member(skolem0014(X89,X90),X90)|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))))&((((((member(skolem0014(X89,X90),X90)|skolem0015(X89,X90)!=skolem0016(X89,X90))|member(skolem0017(X89,X90),X90))|order(X89,X90))&(((member(skolem0014(X89,X90),X90)|skolem0015(X89,X90)!=skolem0016(X89,X90))|member(skolem0018(X89,X90),X90))|order(X89,X90)))&(((member(skolem0014(X89,X90),X90)|skolem0015(X89,X90)!=skolem0016(X89,X90))|member(skolem0019(X89,X90),X90))|order(X89,X90)))&(((((member(skolem0014(X89,X90),X90)|skolem0015(X89,X90)!=skolem0016(X89,X90))|apply(X89,skolem0017(X89,X90),skolem0018(X89,X90)))|order(X89,X90))&(((member(skolem0014(X89,X90),X90)|skolem0015(X89,X90)!=skolem0016(X89,X90))|apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))&(((member(skolem0014(X89,X90),X90)|skolem0015(X89,X90)!=skolem0016(X89,X90))|~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))|order(X89,X90))))))&((((((((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0015(X89,X90),X90))|member(skolem0017(X89,X90),X90))|order(X89,X90))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0015(X89,X90),X90))|member(skolem0018(X89,X90),X90))|order(X89,X90)))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0015(X89,X90),X90))|member(skolem0019(X89,X90),X90))|order(X89,X90)))&(((((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0015(X89,X90),X90))|apply(X89,skolem0017(X89,X90),skolem0018(X89,X90)))|order(X89,X90))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0015(X89,X90),X90))|apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0015(X89,X90),X90))|~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))|order(X89,X90))))&((((((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0016(X89,X90),X90))|member(skolem0017(X89,X90),X90))|order(X89,X90))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0016(X89,X90),X90))|member(skolem0018(X89,X90),X90))|order(X89,X90)))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0016(X89,X90),X90))|member(skolem0019(X89,X90),X90))|order(X89,X90)))&(((((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0016(X89,X90),X90))|apply(X89,skolem0017(X89,X90),skolem0018(X89,X90)))|order(X89,X90))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0016(X89,X90),X90))|apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|member(skolem0016(X89,X90),X90))|~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))))&((((((((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|member(skolem0017(X89,X90),X90))|order(X89,X90))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|member(skolem0018(X89,X90),X90))|order(X89,X90)))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|member(skolem0019(X89,X90),X90))|order(X89,X90)))&(((((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|apply(X89,skolem0017(X89,X90),skolem0018(X89,X90)))|order(X89,X90))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0015(X89,X90),skolem0016(X89,X90)))|~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))|order(X89,X90))))&((((((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|member(skolem0017(X89,X90),X90))|order(X89,X90))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|member(skolem0018(X89,X90),X90))|order(X89,X90)))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|member(skolem0019(X89,X90),X90))|order(X89,X90)))&(((((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|apply(X89,skolem0017(X89,X90),skolem0018(X89,X90)))|order(X89,X90))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|apply(X89,skolem0016(X89,X90),skolem0015(X89,X90)))|~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))))&((((((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|skolem0015(X89,X90)!=skolem0016(X89,X90))|member(skolem0017(X89,X90),X90))|order(X89,X90))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|skolem0015(X89,X90)!=skolem0016(X89,X90))|member(skolem0018(X89,X90),X90))|order(X89,X90)))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|skolem0015(X89,X90)!=skolem0016(X89,X90))|member(skolem0019(X89,X90),X90))|order(X89,X90)))&(((((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|skolem0015(X89,X90)!=skolem0016(X89,X90))|apply(X89,skolem0017(X89,X90),skolem0018(X89,X90)))|order(X89,X90))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|skolem0015(X89,X90)!=skolem0016(X89,X90))|apply(X89,skolem0018(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))&(((~apply(X89,skolem0014(X89,X90),skolem0014(X89,X90))|skolem0015(X89,X90)!=skolem0016(X89,X90))|~apply(X89,skolem0017(X89,X90),skolem0019(X89,X90)))|order(X89,X90)))))))))))))))))),inference(distribute,[status(thm)],[c119])).
% 5.10/5.33 cnf(c121,plain,~order(X158,X159)|~member(X157,X159)|apply(X158,X157,X157),inference(split_conjunct,[status(thm)],[c120])).
% 5.10/5.33 cnf(c195,plain,~order(X160,skolem0002)|apply(X160,skolem0003,skolem0003),inference(resolution,[status(thm)],[c121, c189])).
% 5.10/5.33 cnf(c196,plain,apply(skolem0001,skolem0003,skolem0003),inference(resolution,[status(thm)],[c195, c187])).
% 5.10/5.33 cnf(c197,plain,skolem0001!=X336|skolem0003!=X334|skolem0003!=X335|apply(X336,X334,X335),inference(resolution,[status(thm)],[c196, c2])).
% 5.10/5.33 cnf(c341,plain,skolem0001!=X345|skolem0003!=X344|apply(X345,X344,skolem0003),inference(resolution,[status(thm)],[c197, reflexivity])).
% 5.10/5.33 cnf(c83,plain,~member(X241,X240)|member(skolem0009(X239,X240,X241),X240)|greatest(X241,X239,X240),inference(split_conjunct,[status(thm)],[c80])).
% 5.10/5.33 cnf(c222,plain,member(skolem0009(X308,skolem0002,skolem0003),skolem0002)|greatest(skolem0003,X308,skolem0002),inference(resolution,[status(thm)],[c83, c189])).
% 5.10/5.33 cnf(c318,plain,member(skolem0009(skolem0001,skolem0002,skolem0003),skolem0002),inference(resolution,[status(thm)],[c222, c18])).
% 5.10/5.33 cnf(c61,plain,~max(X273,X274,X276)|~member(X275,X276)|~apply(X274,X273,X275)|X273=X275,inference(split_conjunct,[status(thm)],[c59])).
% 5.10/5.33 cnf(c110,plain,~total_order(X396,X397)|~member(X399,X397)|~member(X398,X397)|apply(X396,X399,X398)|apply(X396,X398,X399),inference(split_conjunct,[status(thm)],[c108])).
% 5.10/5.33 cnf(c398,plain,~total_order(X469,skolem0002)|~member(X470,skolem0002)|apply(X469,X470,skolem0003)|apply(X469,skolem0003,X470),inference(resolution,[status(thm)],[c110, c189])).
% 5.10/5.33 cnf(c693,plain,~total_order(X2252,skolem0002)|apply(X2252,skolem0009(skolem0001,skolem0002,skolem0003),skolem0003)|apply(X2252,skolem0003,skolem0009(skolem0001,skolem0002,skolem0003)),inference(resolution,[status(thm)],[c398, c318])).
% 5.10/5.33 cnf(c13605,plain,apply(skolem0001,skolem0009(skolem0001,skolem0002,skolem0003),skolem0003)|apply(skolem0001,skolem0003,skolem0009(skolem0001,skolem0002,skolem0003)),inference(resolution,[status(thm)],[c693, c16])).
% 5.10/5.33 cnf(c13609,plain,apply(skolem0001,skolem0003,skolem0009(skolem0001,skolem0002,skolem0003))|~member(skolem0003,skolem0002)|greatest(skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c13605, c84])).
% 5.10/5.33 cnf(c13618,plain,apply(skolem0001,skolem0003,skolem0009(skolem0001,skolem0002,skolem0003))|greatest(skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c13609, c189])).
% 5.10/5.33 cnf(c13627,plain,apply(skolem0001,skolem0003,skolem0009(skolem0001,skolem0002,skolem0003)),inference(resolution,[status(thm)],[c13618, c18])).
% 5.10/5.33 cnf(c13630,plain,~max(skolem0003,skolem0001,X2298)|~member(skolem0009(skolem0001,skolem0002,skolem0003),X2298)|skolem0003=skolem0009(skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c13627, c61])).
% 5.10/5.33 cnf(c14335,plain,~max(skolem0003,skolem0001,skolem0002)|skolem0003=skolem0009(skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c13630, c318])).
% 5.10/5.33 cnf(c14362,plain,skolem0003=skolem0009(skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c14335, c17])).
% 5.10/5.33 cnf(c14426,plain,skolem0001!=X2313|apply(X2313,skolem0009(skolem0001,skolem0002,skolem0003),skolem0003),inference(resolution,[status(thm)],[c14362, c341])).
% 5.10/5.33 cnf(c15202,plain,apply(skolem0001,skolem0009(skolem0001,skolem0002,skolem0003),skolem0003),inference(resolution,[status(thm)],[c14426, reflexivity])).
% 5.10/5.33 cnf(c15205,plain,~member(skolem0003,skolem0002)|greatest(skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c15202, c84])).
% 5.10/5.33 cnf(c15209,plain,greatest(skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c15205, c189])).
% 5.10/5.33 cnf(c15431,plain,$false,inference(resolution,[status(thm)],[c15209, c18])).
% 5.10/5.33 % SZS output end CNFRefutation
% 5.10/5.33
% 5.10/5.33 % Initial clauses : 123
% 5.10/5.33 % Processed clauses : 664
% 5.10/5.33 % Factors computed : 68
% 5.10/5.33 % Resolvents computed: 15180
% 5.10/5.33 % Tautologies deleted: 6
% 5.10/5.33 % Forward subsumed : 291
% 5.10/5.33 % Backward subsumed : 19
% 5.10/5.33 % -------- CPU Time ---------
% 5.10/5.33 % User time : 4.909 s
% 5.10/5.33 % System time : 0.051 s
% 5.10/5.33 % Total time : 4.960 s
%------------------------------------------------------------------------------