%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET789+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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:05 EDT 2024
% Result : Theorem 19.55s 19.77s
% Output : Refutation 19.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SET789+4 : TPTP v8.1.2. Released v3.2.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n020.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 19:29:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 19.55/19.77 % Version: 1.5
% 19.55/19.77 % SZS status Theorem
% 19.55/19.77 % SZS output start CNFRefutation
% 19.55/19.77 fof(thIV1,conjecture,(![R]:(![E]:(![M]:((order(R,E)&greatest(M,R,E))=>(![X]:(greatest(X,R,E)=>M=X)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thIV1)).
% 19.55/19.77 fof(c12,negated_conjecture,(~(![R]:(![E]:(![M]:((order(R,E)&greatest(M,R,E))=>(![X]:(greatest(X,R,E)=>M=X))))))),inference(assume_negation,[status(cth)],[thIV1])).
% 19.55/19.77 fof(c13,negated_conjecture,(?[R]:(?[E]:(?[M]:((order(R,E)&greatest(M,R,E))&(?[X]:(greatest(X,R,E)&M!=X)))))),inference(fof_nnf,[status(thm)],[c12])).
% 19.55/19.77 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((order(X2,X3)&greatest(X4,X2,X3))&(?[X5]:(greatest(X5,X2,X3)&X4!=X5)))))),inference(variable_rename,[status(thm)],[c13])).
% 19.55/19.77 fof(c15,negated_conjecture,((order(skolem0001,skolem0002)&greatest(skolem0003,skolem0001,skolem0002))&(greatest(skolem0004,skolem0001,skolem0002)&skolem0003!=skolem0004)),inference(skolemize,[status(esa)],[c14])).
% 19.55/19.77 cnf(c19,negated_conjecture,skolem0003!=skolem0004,inference(split_conjunct,[status(thm)],[c15])).
% 19.55/19.77 cnf(symmetry,axiom,X99!=X100|X100=X99,theory(equality)).
% 19.55/19.77 cnf(c16,negated_conjecture,order(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 19.55/19.77 cnf(c18,negated_conjecture,greatest(skolem0004,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 19.55/19.77 fof(greatest,axiom,(![R]:(![E]:(![M]:(greatest(M,R,E)<=>(member(M,E)&(![X]:(member(X,E)=>apply(R,X,M)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+3.ax', greatest)).
% 19.55/19.77 fof(c76,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])).
% 19.55/19.77 fof(c77,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)],[c76])).
% 19.55/19.77 fof(c78,plain,((![X50]:(![X51]:(![X52]:(~greatest(X52,X50,X51)|(member(X52,X51)&(![X53]:(~member(X53,X51)|apply(X50,X53,X52))))))))&(![X54]:(![X55]:(![X56]:((~member(X56,X55)|(?[X57]:(member(X57,X55)&~apply(X54,X57,X56))))|greatest(X56,X54,X55)))))),inference(variable_rename,[status(thm)],[c77])).
% 19.55/19.77 fof(c80,plain,(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(![X56]:((~greatest(X52,X50,X51)|(member(X52,X51)&(~member(X53,X51)|apply(X50,X53,X52))))&((~member(X56,X55)|(member(skolem0010(X54,X55,X56),X55)&~apply(X54,skolem0010(X54,X55,X56),X56)))|greatest(X56,X54,X55)))))))))),inference(shift_quantors,[status(thm)],[fof(c79,plain,((![X50]:(![X51]:(![X52]:(~greatest(X52,X50,X51)|(member(X52,X51)&(![X53]:(~member(X53,X51)|apply(X50,X53,X52))))))))&(![X54]:(![X55]:(![X56]:((~member(X56,X55)|(member(skolem0010(X54,X55,X56),X55)&~apply(X54,skolem0010(X54,X55,X56),X56)))|greatest(X56,X54,X55)))))),inference(skolemize,[status(esa)],[c78])).])).
% 19.55/19.77 fof(c81,plain,(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(![X56]:(((~greatest(X52,X50,X51)|member(X52,X51))&(~greatest(X52,X50,X51)|(~member(X53,X51)|apply(X50,X53,X52))))&(((~member(X56,X55)|member(skolem0010(X54,X55,X56),X55))|greatest(X56,X54,X55))&((~member(X56,X55)|~apply(X54,skolem0010(X54,X55,X56),X56))|greatest(X56,X54,X55))))))))))),inference(distribute,[status(thm)],[c80])).
% 19.55/19.77 cnf(c82,plain,~greatest(X125,X123,X124)|member(X125,X124),inference(split_conjunct,[status(thm)],[c81])).
% 19.55/19.77 cnf(c189,plain,member(skolem0004,skolem0002),inference(resolution,[status(thm)],[c82, c18])).
% 19.55/19.77 cnf(c17,negated_conjecture,greatest(skolem0003,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 19.55/19.77 cnf(c190,plain,member(skolem0003,skolem0002),inference(resolution,[status(thm)],[c82, c17])).
% 19.55/19.77 cnf(c83,plain,~greatest(X173,X171,X172)|~member(X174,X172)|apply(X171,X174,X173),inference(split_conjunct,[status(thm)],[c81])).
% 19.55/19.77 cnf(c204,plain,~member(X182,skolem0002)|apply(skolem0001,X182,skolem0003),inference(resolution,[status(thm)],[c83, c17])).
% 19.55/19.77 cnf(c211,plain,apply(skolem0001,skolem0004,skolem0003),inference(resolution,[status(thm)],[c204, c189])).
% 19.55/19.77 cnf(c203,plain,~member(X175,skolem0002)|apply(skolem0001,X175,skolem0004),inference(resolution,[status(thm)],[c83, c18])).
% 19.55/19.77 cnf(c208,plain,apply(skolem0001,skolem0003,skolem0004),inference(resolution,[status(thm)],[c203, c190])).
% 19.55/19.77 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/sandbox2/benchmark/Axioms/SET006+3.ax', order)).
% 19.55/19.77 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))))))))&((((?[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])).
% 19.55/19.77 fof(c117,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)],[c116])).
% 19.55/19.77 fof(c118,plain,((![X82]:(![X83]:(~order(X82,X83)|(((![X84]:(~member(X84,X83)|apply(X82,X84,X84)))&(![X85]:(![X86]:((~member(X85,X83)|~member(X86,X83))|((~apply(X82,X85,X86)|~apply(X82,X86,X85))|X85=X86)))))&(![X87]:(![X88]:(![X89]:(((~member(X87,X83)|~member(X88,X83))|~member(X89,X83))|((~apply(X82,X87,X88)|~apply(X82,X88,X89))|apply(X82,X87,X89))))))))))&(![X90]:(![X91]:((((?[X92]:(member(X92,X91)&~apply(X90,X92,X92)))|(?[X93]:(?[X94]:((member(X93,X91)&member(X94,X91))&((apply(X90,X93,X94)&apply(X90,X94,X93))&X93!=X94)))))|(?[X95]:(?[X96]:(?[X97]:(((member(X95,X91)&member(X96,X91))&member(X97,X91))&((apply(X90,X95,X96)&apply(X90,X96,X97))&~apply(X90,X95,X97)))))))|order(X90,X91))))),inference(variable_rename,[status(thm)],[c117])).
% 19.55/19.77 fof(c120,plain,(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:(![X87]:(![X88]:(![X89]:(![X90]:(![X91]:((~order(X82,X83)|(((~member(X84,X83)|apply(X82,X84,X84))&((~member(X85,X83)|~member(X86,X83))|((~apply(X82,X85,X86)|~apply(X82,X86,X85))|X85=X86)))&(((~member(X87,X83)|~member(X88,X83))|~member(X89,X83))|((~apply(X82,X87,X88)|~apply(X82,X88,X89))|apply(X82,X87,X89)))))&((((member(skolem0015(X90,X91),X91)&~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91)))|((member(skolem0016(X90,X91),X91)&member(skolem0017(X90,X91),X91))&((apply(X90,skolem0016(X90,X91),skolem0017(X90,X91))&apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))&skolem0016(X90,X91)!=skolem0017(X90,X91))))|(((member(skolem0018(X90,X91),X91)&member(skolem0019(X90,X91),X91))&member(skolem0020(X90,X91),X91))&((apply(X90,skolem0018(X90,X91),skolem0019(X90,X91))&apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))&~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))))|order(X90,X91))))))))))))),inference(shift_quantors,[status(thm)],[fof(c119,plain,((![X82]:(![X83]:(~order(X82,X83)|(((![X84]:(~member(X84,X83)|apply(X82,X84,X84)))&(![X85]:(![X86]:((~member(X85,X83)|~member(X86,X83))|((~apply(X82,X85,X86)|~apply(X82,X86,X85))|X85=X86)))))&(![X87]:(![X88]:(![X89]:(((~member(X87,X83)|~member(X88,X83))|~member(X89,X83))|((~apply(X82,X87,X88)|~apply(X82,X88,X89))|apply(X82,X87,X89))))))))))&(![X90]:(![X91]:((((member(skolem0015(X90,X91),X91)&~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91)))|((member(skolem0016(X90,X91),X91)&member(skolem0017(X90,X91),X91))&((apply(X90,skolem0016(X90,X91),skolem0017(X90,X91))&apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))&skolem0016(X90,X91)!=skolem0017(X90,X91))))|(((member(skolem0018(X90,X91),X91)&member(skolem0019(X90,X91),X91))&member(skolem0020(X90,X91),X91))&((apply(X90,skolem0018(X90,X91),skolem0019(X90,X91))&apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))&~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))))|order(X90,X91))))),inference(skolemize,[status(esa)],[c118])).])).
% 19.55/19.77 fof(c121,plain,(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:(![X87]:(![X88]:(![X89]:(![X90]:(![X91]:((((~order(X82,X83)|(~member(X84,X83)|apply(X82,X84,X84)))&(~order(X82,X83)|((~member(X85,X83)|~member(X86,X83))|((~apply(X82,X85,X86)|~apply(X82,X86,X85))|X85=X86))))&(~order(X82,X83)|(((~member(X87,X83)|~member(X88,X83))|~member(X89,X83))|((~apply(X82,X87,X88)|~apply(X82,X88,X89))|apply(X82,X87,X89)))))&(((((((((member(skolem0015(X90,X91),X91)|member(skolem0016(X90,X91),X91))|member(skolem0018(X90,X91),X91))|order(X90,X91))&(((member(skolem0015(X90,X91),X91)|member(skolem0016(X90,X91),X91))|member(skolem0019(X90,X91),X91))|order(X90,X91)))&(((member(skolem0015(X90,X91),X91)|member(skolem0016(X90,X91),X91))|member(skolem0020(X90,X91),X91))|order(X90,X91)))&(((((member(skolem0015(X90,X91),X91)|member(skolem0016(X90,X91),X91))|apply(X90,skolem0018(X90,X91),skolem0019(X90,X91)))|order(X90,X91))&(((member(skolem0015(X90,X91),X91)|member(skolem0016(X90,X91),X91))|apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))&(((member(skolem0015(X90,X91),X91)|member(skolem0016(X90,X91),X91))|~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))|order(X90,X91))))&((((((member(skolem0015(X90,X91),X91)|member(skolem0017(X90,X91),X91))|member(skolem0018(X90,X91),X91))|order(X90,X91))&(((member(skolem0015(X90,X91),X91)|member(skolem0017(X90,X91),X91))|member(skolem0019(X90,X91),X91))|order(X90,X91)))&(((member(skolem0015(X90,X91),X91)|member(skolem0017(X90,X91),X91))|member(skolem0020(X90,X91),X91))|order(X90,X91)))&(((((member(skolem0015(X90,X91),X91)|member(skolem0017(X90,X91),X91))|apply(X90,skolem0018(X90,X91),skolem0019(X90,X91)))|order(X90,X91))&(((member(skolem0015(X90,X91),X91)|member(skolem0017(X90,X91),X91))|apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))&(((member(skolem0015(X90,X91),X91)|member(skolem0017(X90,X91),X91))|~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))))&((((((((member(skolem0015(X90,X91),X91)|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|member(skolem0018(X90,X91),X91))|order(X90,X91))&(((member(skolem0015(X90,X91),X91)|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|member(skolem0019(X90,X91),X91))|order(X90,X91)))&(((member(skolem0015(X90,X91),X91)|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|member(skolem0020(X90,X91),X91))|order(X90,X91)))&(((((member(skolem0015(X90,X91),X91)|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|apply(X90,skolem0018(X90,X91),skolem0019(X90,X91)))|order(X90,X91))&(((member(skolem0015(X90,X91),X91)|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))&(((member(skolem0015(X90,X91),X91)|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))|order(X90,X91))))&((((((member(skolem0015(X90,X91),X91)|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|member(skolem0018(X90,X91),X91))|order(X90,X91))&(((member(skolem0015(X90,X91),X91)|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|member(skolem0019(X90,X91),X91))|order(X90,X91)))&(((member(skolem0015(X90,X91),X91)|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|member(skolem0020(X90,X91),X91))|order(X90,X91)))&(((((member(skolem0015(X90,X91),X91)|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|apply(X90,skolem0018(X90,X91),skolem0019(X90,X91)))|order(X90,X91))&(((member(skolem0015(X90,X91),X91)|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))&(((member(skolem0015(X90,X91),X91)|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))))&((((((member(skolem0015(X90,X91),X91)|skolem0016(X90,X91)!=skolem0017(X90,X91))|member(skolem0018(X90,X91),X91))|order(X90,X91))&(((member(skolem0015(X90,X91),X91)|skolem0016(X90,X91)!=skolem0017(X90,X91))|member(skolem0019(X90,X91),X91))|order(X90,X91)))&(((member(skolem0015(X90,X91),X91)|skolem0016(X90,X91)!=skolem0017(X90,X91))|member(skolem0020(X90,X91),X91))|order(X90,X91)))&(((((member(skolem0015(X90,X91),X91)|skolem0016(X90,X91)!=skolem0017(X90,X91))|apply(X90,skolem0018(X90,X91),skolem0019(X90,X91)))|order(X90,X91))&(((member(skolem0015(X90,X91),X91)|skolem0016(X90,X91)!=skolem0017(X90,X91))|apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))&(((member(skolem0015(X90,X91),X91)|skolem0016(X90,X91)!=skolem0017(X90,X91))|~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))|order(X90,X91))))))&((((((((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0016(X90,X91),X91))|member(skolem0018(X90,X91),X91))|order(X90,X91))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0016(X90,X91),X91))|member(skolem0019(X90,X91),X91))|order(X90,X91)))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0016(X90,X91),X91))|member(skolem0020(X90,X91),X91))|order(X90,X91)))&(((((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0016(X90,X91),X91))|apply(X90,skolem0018(X90,X91),skolem0019(X90,X91)))|order(X90,X91))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0016(X90,X91),X91))|apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0016(X90,X91),X91))|~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))|order(X90,X91))))&((((((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0017(X90,X91),X91))|member(skolem0018(X90,X91),X91))|order(X90,X91))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0017(X90,X91),X91))|member(skolem0019(X90,X91),X91))|order(X90,X91)))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0017(X90,X91),X91))|member(skolem0020(X90,X91),X91))|order(X90,X91)))&(((((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0017(X90,X91),X91))|apply(X90,skolem0018(X90,X91),skolem0019(X90,X91)))|order(X90,X91))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0017(X90,X91),X91))|apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|member(skolem0017(X90,X91),X91))|~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))))&((((((((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|member(skolem0018(X90,X91),X91))|order(X90,X91))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|member(skolem0019(X90,X91),X91))|order(X90,X91)))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|member(skolem0020(X90,X91),X91))|order(X90,X91)))&(((((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|apply(X90,skolem0018(X90,X91),skolem0019(X90,X91)))|order(X90,X91))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0016(X90,X91),skolem0017(X90,X91)))|~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))|order(X90,X91))))&((((((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|member(skolem0018(X90,X91),X91))|order(X90,X91))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|member(skolem0019(X90,X91),X91))|order(X90,X91)))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|member(skolem0020(X90,X91),X91))|order(X90,X91)))&(((((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|apply(X90,skolem0018(X90,X91),skolem0019(X90,X91)))|order(X90,X91))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|apply(X90,skolem0017(X90,X91),skolem0016(X90,X91)))|~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))))&((((((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|skolem0016(X90,X91)!=skolem0017(X90,X91))|member(skolem0018(X90,X91),X91))|order(X90,X91))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|skolem0016(X90,X91)!=skolem0017(X90,X91))|member(skolem0019(X90,X91),X91))|order(X90,X91)))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|skolem0016(X90,X91)!=skolem0017(X90,X91))|member(skolem0020(X90,X91),X91))|order(X90,X91)))&(((((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|skolem0016(X90,X91)!=skolem0017(X90,X91))|apply(X90,skolem0018(X90,X91),skolem0019(X90,X91)))|order(X90,X91))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|skolem0016(X90,X91)!=skolem0017(X90,X91))|apply(X90,skolem0019(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))&(((~apply(X90,skolem0015(X90,X91),skolem0015(X90,X91))|skolem0016(X90,X91)!=skolem0017(X90,X91))|~apply(X90,skolem0018(X90,X91),skolem0020(X90,X91)))|order(X90,X91)))))))))))))))))),inference(distribute,[status(thm)],[c120])).
% 19.55/19.77 cnf(c123,plain,~order(X408,X407)|~member(X409,X407)|~member(X410,X407)|~apply(X408,X409,X410)|~apply(X408,X410,X409)|X409=X410,inference(split_conjunct,[status(thm)],[c121])).
% 19.55/19.77 cnf(c688,plain,~order(skolem0001,X3881)|~member(skolem0004,X3881)|~member(skolem0003,X3881)|~apply(skolem0001,skolem0004,skolem0003)|skolem0004=skolem0003,inference(resolution,[status(thm)],[c123, c208])).
% 19.55/19.77 cnf(c34410,plain,~order(skolem0001,X3882)|~member(skolem0004,X3882)|~member(skolem0003,X3882)|skolem0004=skolem0003,inference(resolution,[status(thm)],[c688, c211])).
% 19.55/19.77 cnf(c34427,plain,~order(skolem0001,skolem0002)|~member(skolem0004,skolem0002)|skolem0004=skolem0003,inference(resolution,[status(thm)],[c34410, c190])).
% 19.55/19.77 cnf(c34428,plain,~order(skolem0001,skolem0002)|skolem0004=skolem0003,inference(resolution,[status(thm)],[c34427, c189])).
% 19.55/19.77 cnf(c34439,plain,skolem0004=skolem0003,inference(resolution,[status(thm)],[c34428, c16])).
% 19.55/19.77 cnf(c34502,plain,skolem0003=skolem0004,inference(resolution,[status(thm)],[c34439, symmetry])).
% 19.55/19.77 cnf(c34666,plain,$false,inference(resolution,[status(thm)],[c34502, c19])).
% 19.55/19.77 % SZS output end CNFRefutation
% 19.55/19.77
% 19.55/19.77 % Initial clauses : 124
% 19.55/19.77 % Processed clauses : 1287
% 19.55/19.77 % Factors computed : 122
% 19.55/19.77 % Resolvents computed: 34460
% 19.55/19.77 % Tautologies deleted: 5
% 19.55/19.77 % Forward subsumed : 779
% 19.55/19.77 % Backward subsumed : 45
% 19.55/19.77 % -------- CPU Time ---------
% 19.55/19.77 % User time : 19.313 s
% 19.55/19.77 % System time : 0.095 s
% 19.55/19.77 % Total time : 19.408 s
%------------------------------------------------------------------------------