%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:59:00 PM UTC 2026
% Result : Theorem 0.57s 0.80s
% Output : CNFRefutation 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.33 % Computer : n002.cluster.edu
% 0.09/0.33 % Model : x86_64 x86_64
% 0.09/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.33 % Memory : 8046.5625MB
% 0.09/0.33 % OS : Linux 6.8.0-71-generic
% 0.09/0.33 % CPULimit : 300
% 0.09/0.33 % WCLimit : 300
% 0.09/0.33 % DateTime : Sat Sep 5 02:08:35 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.12/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.40 (re.compile("\."), Token.FullStop),
% 0.12/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.40 (re.compile("\("), Token.OpenPar),
% 0.12/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.40 (re.compile("\)"), Token.ClosePar),
% 0.12/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.40 (re.compile("\["), Token.OpenSquare),
% 0.12/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.40 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.40 (re.compile("~\|"), Token.Nor),
% 0.12/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.40 (re.compile("\|"), Token.Or),
% 0.12/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.40 (re.compile("\?"), Token.Existential),
% 0.12/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.40 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.40 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.40 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.47 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.47 """
% 0.22/0.47 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.47 """
% 0.33/0.56 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.56 """
% 0.57/0.80 % Version: 1.5
% 0.57/0.80 % SZS status Theorem
% 0.57/0.80 % SZS output start CNFRefutation
% 0.57/0.80 fof(main,conjecture,(~(?[X]:(~((~(![Y]:((~r1(X,Y))|p3(Y))))|(~(((![Y]:((~r1(X,Y))|(((((((((((((((((((~(![X]:((~r1(Y,X))|(~(((~p6(X))&(~p106(X)))&p105(X))))))&(~(![X]:((~r1(Y,X))|(~((p6(X)&(~p106(X)))&p105(X)))))))|(~((~p105(Y))&p104(Y))))&(((~(![X]:((~r1(Y,X))|(~(((~p5(X))&(~p105(X)))&p104(X))))))&(~(![X]:((~r1(Y,X))|(~((p5(X)&(~p105(X)))&p104(X)))))))|(~((~p104(Y))&p103(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p4(X))&(~p104(X)))&p103(X))))))&(~(![X]:((~r1(Y,X))|(~((p4(X)&(~p104(X)))&p103(X)))))))|(~((~p103(Y))&p102(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p3(X))&(~p103(X)))&p102(X))))))&(~(![X]:((~r1(Y,X))|(~((p3(X)&(~p103(X)))&p102(X)))))))|(~((~p102(Y))&p101(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p2(X))&(~p102(X)))&p101(X))))))&(~(![X]:((~r1(Y,X))|(~((p2(X)&(~p102(X)))&p101(X)))))))|(~((~p101(Y))&p100(Y)))))&((((![X]:(((~r1(Y,X))|(~p6(X)))|(~p105(X))))|p6(Y))&((![X]:(((~r1(Y,X))|p6(X))|(~p105(X))))|(~p6(Y))))|(~p105(Y))))&((((![X]:(((~r1(Y,X))|(~p5(X)))|(~p104(X))))|p5(Y))&((![X]:(((~r1(Y,X))|p5(X))|(~p104(X))))|(~p5(Y))))|(~p104(Y))))&((((![X]:(((~r1(Y,X))|(~p4(X)))|(~p103(X))))|p4(Y))&((![X]:(((~r1(Y,X))|p4(X))|(~p103(X))))|(~p4(Y))))|(~p103(Y))))&((((![X]:(((~r1(Y,X))|(~p3(X)))|(~p102(X))))|p3(Y))&((![X]:(((~r1(Y,X))|p3(X))|(~p102(X))))|(~p3(Y))))|(~p102(Y))))&((((![X]:(((~r1(Y,X))|(~p2(X)))|(~p101(X))))|p2(Y))&((![X]:(((~r1(Y,X))|p2(X))|(~p101(X))))|(~p2(Y))))|(~p101(Y))))&((((![X]:(((~r1(Y,X))|(~p1(X)))|(~p100(X))))|p1(Y))&((![X]:(((~r1(Y,X))|p1(X))|(~p100(X))))|(~p1(Y))))|(~p100(Y))))&(p105(Y)|(~p106(Y))))&(p104(Y)|(~p105(Y))))&(p103(Y)|(~p104(Y))))&(p102(Y)|(~p103(Y))))&(p101(Y)|(~p102(Y))))&(p100(Y)|(~p101(Y))))))&(~p101(X)))&p100(X))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 0.57/0.80 fof(c0,negated_conjecture,(~(~(?[X]:(~((~(![Y]:((~r1(X,Y))|p3(Y))))|(~(((![Y]:((~r1(X,Y))|(((((((((((((((((((~(![X]:((~r1(Y,X))|(~(((~p6(X))&(~p106(X)))&p105(X))))))&(~(![X]:((~r1(Y,X))|(~((p6(X)&(~p106(X)))&p105(X)))))))|(~((~p105(Y))&p104(Y))))&(((~(![X]:((~r1(Y,X))|(~(((~p5(X))&(~p105(X)))&p104(X))))))&(~(![X]:((~r1(Y,X))|(~((p5(X)&(~p105(X)))&p104(X)))))))|(~((~p104(Y))&p103(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p4(X))&(~p104(X)))&p103(X))))))&(~(![X]:((~r1(Y,X))|(~((p4(X)&(~p104(X)))&p103(X)))))))|(~((~p103(Y))&p102(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p3(X))&(~p103(X)))&p102(X))))))&(~(![X]:((~r1(Y,X))|(~((p3(X)&(~p103(X)))&p102(X)))))))|(~((~p102(Y))&p101(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p2(X))&(~p102(X)))&p101(X))))))&(~(![X]:((~r1(Y,X))|(~((p2(X)&(~p102(X)))&p101(X)))))))|(~((~p101(Y))&p100(Y)))))&((((![X]:(((~r1(Y,X))|(~p6(X)))|(~p105(X))))|p6(Y))&((![X]:(((~r1(Y,X))|p6(X))|(~p105(X))))|(~p6(Y))))|(~p105(Y))))&((((![X]:(((~r1(Y,X))|(~p5(X)))|(~p104(X))))|p5(Y))&((![X]:(((~r1(Y,X))|p5(X))|(~p104(X))))|(~p5(Y))))|(~p104(Y))))&((((![X]:(((~r1(Y,X))|(~p4(X)))|(~p103(X))))|p4(Y))&((![X]:(((~r1(Y,X))|p4(X))|(~p103(X))))|(~p4(Y))))|(~p103(Y))))&((((![X]:(((~r1(Y,X))|(~p3(X)))|(~p102(X))))|p3(Y))&((![X]:(((~r1(Y,X))|p3(X))|(~p102(X))))|(~p3(Y))))|(~p102(Y))))&((((![X]:(((~r1(Y,X))|(~p2(X)))|(~p101(X))))|p2(Y))&((![X]:(((~r1(Y,X))|p2(X))|(~p101(X))))|(~p2(Y))))|(~p101(Y))))&((((![X]:(((~r1(Y,X))|(~p1(X)))|(~p100(X))))|p1(Y))&((![X]:(((~r1(Y,X))|p1(X))|(~p100(X))))|(~p1(Y))))|(~p100(Y))))&(p105(Y)|(~p106(Y))))&(p104(Y)|(~p105(Y))))&(p103(Y)|(~p104(Y))))&(p102(Y)|(~p103(Y))))&(p101(Y)|(~p102(Y))))&(p100(Y)|(~p101(Y))))))&(~p101(X)))&p100(X)))))))),inference(assume_negation,[status(cth)],[main])).
% 0.57/0.80 fof(c1,negated_conjecture,(~(~(?[X]:(~((~(![Y]:(~r1(X,Y)|p3(Y))))|(~(((![Y]:(~r1(X,Y)|(((((((((((((((((((~(![X]:(~r1(Y,X)|(~((~p6(X)&~p106(X))&p105(X))))))&(~(![X]:(~r1(Y,X)|(~((p6(X)&~p106(X))&p105(X)))))))|(~(~p105(Y)&p104(Y))))&(((~(![X]:(~r1(Y,X)|(~((~p5(X)&~p105(X))&p104(X))))))&(~(![X]:(~r1(Y,X)|(~((p5(X)&~p105(X))&p104(X)))))))|(~(~p104(Y)&p103(Y)))))&(((~(![X]:(~r1(Y,X)|(~((~p4(X)&~p104(X))&p103(X))))))&(~(![X]:(~r1(Y,X)|(~((p4(X)&~p104(X))&p103(X)))))))|(~(~p103(Y)&p102(Y)))))&(((~(![X]:(~r1(Y,X)|(~((~p3(X)&~p103(X))&p102(X))))))&(~(![X]:(~r1(Y,X)|(~((p3(X)&~p103(X))&p102(X)))))))|(~(~p102(Y)&p101(Y)))))&(((~(![X]:(~r1(Y,X)|(~((~p2(X)&~p102(X))&p101(X))))))&(~(![X]:(~r1(Y,X)|(~((p2(X)&~p102(X))&p101(X)))))))|(~(~p101(Y)&p100(Y)))))&((((![X]:((~r1(Y,X)|~p6(X))|~p105(X)))|p6(Y))&((![X]:((~r1(Y,X)|p6(X))|~p105(X)))|~p6(Y)))|~p105(Y)))&((((![X]:((~r1(Y,X)|~p5(X))|~p104(X)))|p5(Y))&((![X]:((~r1(Y,X)|p5(X))|~p104(X)))|~p5(Y)))|~p104(Y)))&((((![X]:((~r1(Y,X)|~p4(X))|~p103(X)))|p4(Y))&((![X]:((~r1(Y,X)|p4(X))|~p103(X)))|~p4(Y)))|~p103(Y)))&((((![X]:((~r1(Y,X)|~p3(X))|~p102(X)))|p3(Y))&((![X]:((~r1(Y,X)|p3(X))|~p102(X)))|~p3(Y)))|~p102(Y)))&((((![X]:((~r1(Y,X)|~p2(X))|~p101(X)))|p2(Y))&((![X]:((~r1(Y,X)|p2(X))|~p101(X)))|~p2(Y)))|~p101(Y)))&((((![X]:((~r1(Y,X)|~p1(X))|~p100(X)))|p1(Y))&((![X]:((~r1(Y,X)|p1(X))|~p100(X)))|~p1(Y)))|~p100(Y)))&(p105(Y)|~p106(Y)))&(p104(Y)|~p105(Y)))&(p103(Y)|~p104(Y)))&(p102(Y)|~p103(Y)))&(p101(Y)|~p102(Y)))&(p100(Y)|~p101(Y)))))&~p101(X))&p100(X)))))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.57/0.80 fof(c2,negated_conjecture,(?[X]:((![Y]:(~r1(X,Y)|p3(Y)))&(((![Y]:(~r1(X,Y)|(((((((((((((((((((?[X]:(r1(Y,X)&((~p6(X)&~p106(X))&p105(X))))&(?[X]:(r1(Y,X)&((p6(X)&~p106(X))&p105(X)))))|(p105(Y)|~p104(Y)))&(((?[X]:(r1(Y,X)&((~p5(X)&~p105(X))&p104(X))))&(?[X]:(r1(Y,X)&((p5(X)&~p105(X))&p104(X)))))|(p104(Y)|~p103(Y))))&(((?[X]:(r1(Y,X)&((~p4(X)&~p104(X))&p103(X))))&(?[X]:(r1(Y,X)&((p4(X)&~p104(X))&p103(X)))))|(p103(Y)|~p102(Y))))&(((?[X]:(r1(Y,X)&((~p3(X)&~p103(X))&p102(X))))&(?[X]:(r1(Y,X)&((p3(X)&~p103(X))&p102(X)))))|(p102(Y)|~p101(Y))))&(((?[X]:(r1(Y,X)&((~p2(X)&~p102(X))&p101(X))))&(?[X]:(r1(Y,X)&((p2(X)&~p102(X))&p101(X)))))|(p101(Y)|~p100(Y))))&((((![X]:((~r1(Y,X)|~p6(X))|~p105(X)))|p6(Y))&((![X]:((~r1(Y,X)|p6(X))|~p105(X)))|~p6(Y)))|~p105(Y)))&((((![X]:((~r1(Y,X)|~p5(X))|~p104(X)))|p5(Y))&((![X]:((~r1(Y,X)|p5(X))|~p104(X)))|~p5(Y)))|~p104(Y)))&((((![X]:((~r1(Y,X)|~p4(X))|~p103(X)))|p4(Y))&((![X]:((~r1(Y,X)|p4(X))|~p103(X)))|~p4(Y)))|~p103(Y)))&((((![X]:((~r1(Y,X)|~p3(X))|~p102(X)))|p3(Y))&((![X]:((~r1(Y,X)|p3(X))|~p102(X)))|~p3(Y)))|~p102(Y)))&((((![X]:((~r1(Y,X)|~p2(X))|~p101(X)))|p2(Y))&((![X]:((~r1(Y,X)|p2(X))|~p101(X)))|~p2(Y)))|~p101(Y)))&((((![X]:((~r1(Y,X)|~p1(X))|~p100(X)))|p1(Y))&((![X]:((~r1(Y,X)|p1(X))|~p100(X)))|~p1(Y)))|~p100(Y)))&(p105(Y)|~p106(Y)))&(p104(Y)|~p105(Y)))&(p103(Y)|~p104(Y)))&(p102(Y)|~p103(Y)))&(p101(Y)|~p102(Y)))&(p100(Y)|~p101(Y)))))&~p101(X))&p100(X)))),inference(fof_nnf,[status(thm)],[c1])).
% 0.57/0.81 fof(c3,negated_conjecture,(?[X2]:((![X3]:(~r1(X2,X3)|p3(X3)))&(((![X4]:(~r1(X2,X4)|(((((((((((((((((((?[X5]:(r1(X4,X5)&((~p6(X5)&~p106(X5))&p105(X5))))&(?[X6]:(r1(X4,X6)&((p6(X6)&~p106(X6))&p105(X6)))))|(p105(X4)|~p104(X4)))&(((?[X7]:(r1(X4,X7)&((~p5(X7)&~p105(X7))&p104(X7))))&(?[X8]:(r1(X4,X8)&((p5(X8)&~p105(X8))&p104(X8)))))|(p104(X4)|~p103(X4))))&(((?[X9]:(r1(X4,X9)&((~p4(X9)&~p104(X9))&p103(X9))))&(?[X10]:(r1(X4,X10)&((p4(X10)&~p104(X10))&p103(X10)))))|(p103(X4)|~p102(X4))))&(((?[X11]:(r1(X4,X11)&((~p3(X11)&~p103(X11))&p102(X11))))&(?[X12]:(r1(X4,X12)&((p3(X12)&~p103(X12))&p102(X12)))))|(p102(X4)|~p101(X4))))&(((?[X13]:(r1(X4,X13)&((~p2(X13)&~p102(X13))&p101(X13))))&(?[X14]:(r1(X4,X14)&((p2(X14)&~p102(X14))&p101(X14)))))|(p101(X4)|~p100(X4))))&((((![X15]:((~r1(X4,X15)|~p6(X15))|~p105(X15)))|p6(X4))&((![X16]:((~r1(X4,X16)|p6(X16))|~p105(X16)))|~p6(X4)))|~p105(X4)))&((((![X17]:((~r1(X4,X17)|~p5(X17))|~p104(X17)))|p5(X4))&((![X18]:((~r1(X4,X18)|p5(X18))|~p104(X18)))|~p5(X4)))|~p104(X4)))&((((![X19]:((~r1(X4,X19)|~p4(X19))|~p103(X19)))|p4(X4))&((![X20]:((~r1(X4,X20)|p4(X20))|~p103(X20)))|~p4(X4)))|~p103(X4)))&((((![X21]:((~r1(X4,X21)|~p3(X21))|~p102(X21)))|p3(X4))&((![X22]:((~r1(X4,X22)|p3(X22))|~p102(X22)))|~p3(X4)))|~p102(X4)))&((((![X23]:((~r1(X4,X23)|~p2(X23))|~p101(X23)))|p2(X4))&((![X24]:((~r1(X4,X24)|p2(X24))|~p101(X24)))|~p2(X4)))|~p101(X4)))&((((![X25]:((~r1(X4,X25)|~p1(X25))|~p100(X25)))|p1(X4))&((![X26]:((~r1(X4,X26)|p1(X26))|~p100(X26)))|~p1(X4)))|~p100(X4)))&(p105(X4)|~p106(X4)))&(p104(X4)|~p105(X4)))&(p103(X4)|~p104(X4)))&(p102(X4)|~p103(X4)))&(p101(X4)|~p102(X4)))&(p100(X4)|~p101(X4)))))&~p101(X2))&p100(X2)))),inference(variable_rename,[status(thm)],[c2])).
% 0.57/0.81 fof(c5,negated_conjecture,(![X3]:(![X4]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:((~r1(skolem0001,X3)|p3(X3))&(((~r1(skolem0001,X4)|(((((((((((((((((((r1(X4,skolem0002(X4))&((~p6(skolem0002(X4))&~p106(skolem0002(X4)))&p105(skolem0002(X4))))&(r1(X4,skolem0003(X4))&((p6(skolem0003(X4))&~p106(skolem0003(X4)))&p105(skolem0003(X4)))))|(p105(X4)|~p104(X4)))&(((r1(X4,skolem0004(X4))&((~p5(skolem0004(X4))&~p105(skolem0004(X4)))&p104(skolem0004(X4))))&(r1(X4,skolem0005(X4))&((p5(skolem0005(X4))&~p105(skolem0005(X4)))&p104(skolem0005(X4)))))|(p104(X4)|~p103(X4))))&(((r1(X4,skolem0006(X4))&((~p4(skolem0006(X4))&~p104(skolem0006(X4)))&p103(skolem0006(X4))))&(r1(X4,skolem0007(X4))&((p4(skolem0007(X4))&~p104(skolem0007(X4)))&p103(skolem0007(X4)))))|(p103(X4)|~p102(X4))))&(((r1(X4,skolem0008(X4))&((~p3(skolem0008(X4))&~p103(skolem0008(X4)))&p102(skolem0008(X4))))&(r1(X4,skolem0009(X4))&((p3(skolem0009(X4))&~p103(skolem0009(X4)))&p102(skolem0009(X4)))))|(p102(X4)|~p101(X4))))&(((r1(X4,skolem0010(X4))&((~p2(skolem0010(X4))&~p102(skolem0010(X4)))&p101(skolem0010(X4))))&(r1(X4,skolem0011(X4))&((p2(skolem0011(X4))&~p102(skolem0011(X4)))&p101(skolem0011(X4)))))|(p101(X4)|~p100(X4))))&(((((~r1(X4,X15)|~p6(X15))|~p105(X15))|p6(X4))&(((~r1(X4,X16)|p6(X16))|~p105(X16))|~p6(X4)))|~p105(X4)))&(((((~r1(X4,X17)|~p5(X17))|~p104(X17))|p5(X4))&(((~r1(X4,X18)|p5(X18))|~p104(X18))|~p5(X4)))|~p104(X4)))&(((((~r1(X4,X19)|~p4(X19))|~p103(X19))|p4(X4))&(((~r1(X4,X20)|p4(X20))|~p103(X20))|~p4(X4)))|~p103(X4)))&(((((~r1(X4,X21)|~p3(X21))|~p102(X21))|p3(X4))&(((~r1(X4,X22)|p3(X22))|~p102(X22))|~p3(X4)))|~p102(X4)))&(((((~r1(X4,X23)|~p2(X23))|~p101(X23))|p2(X4))&(((~r1(X4,X24)|p2(X24))|~p101(X24))|~p2(X4)))|~p101(X4)))&(((((~r1(X4,X25)|~p1(X25))|~p100(X25))|p1(X4))&(((~r1(X4,X26)|p1(X26))|~p100(X26))|~p1(X4)))|~p100(X4)))&(p105(X4)|~p106(X4)))&(p104(X4)|~p105(X4)))&(p103(X4)|~p104(X4)))&(p102(X4)|~p103(X4)))&(p101(X4)|~p102(X4)))&(p100(X4)|~p101(X4))))&~p101(skolem0001))&p100(skolem0001))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((![X3]:(~r1(skolem0001,X3)|p3(X3)))&(((![X4]:(~r1(skolem0001,X4)|(((((((((((((((((((r1(X4,skolem0002(X4))&((~p6(skolem0002(X4))&~p106(skolem0002(X4)))&p105(skolem0002(X4))))&(r1(X4,skolem0003(X4))&((p6(skolem0003(X4))&~p106(skolem0003(X4)))&p105(skolem0003(X4)))))|(p105(X4)|~p104(X4)))&(((r1(X4,skolem0004(X4))&((~p5(skolem0004(X4))&~p105(skolem0004(X4)))&p104(skolem0004(X4))))&(r1(X4,skolem0005(X4))&((p5(skolem0005(X4))&~p105(skolem0005(X4)))&p104(skolem0005(X4)))))|(p104(X4)|~p103(X4))))&(((r1(X4,skolem0006(X4))&((~p4(skolem0006(X4))&~p104(skolem0006(X4)))&p103(skolem0006(X4))))&(r1(X4,skolem0007(X4))&((p4(skolem0007(X4))&~p104(skolem0007(X4)))&p103(skolem0007(X4)))))|(p103(X4)|~p102(X4))))&(((r1(X4,skolem0008(X4))&((~p3(skolem0008(X4))&~p103(skolem0008(X4)))&p102(skolem0008(X4))))&(r1(X4,skolem0009(X4))&((p3(skolem0009(X4))&~p103(skolem0009(X4)))&p102(skolem0009(X4)))))|(p102(X4)|~p101(X4))))&(((r1(X4,skolem0010(X4))&((~p2(skolem0010(X4))&~p102(skolem0010(X4)))&p101(skolem0010(X4))))&(r1(X4,skolem0011(X4))&((p2(skolem0011(X4))&~p102(skolem0011(X4)))&p101(skolem0011(X4)))))|(p101(X4)|~p100(X4))))&((((![X15]:((~r1(X4,X15)|~p6(X15))|~p105(X15)))|p6(X4))&((![X16]:((~r1(X4,X16)|p6(X16))|~p105(X16)))|~p6(X4)))|~p105(X4)))&((((![X17]:((~r1(X4,X17)|~p5(X17))|~p104(X17)))|p5(X4))&((![X18]:((~r1(X4,X18)|p5(X18))|~p104(X18)))|~p5(X4)))|~p104(X4)))&((((![X19]:((~r1(X4,X19)|~p4(X19))|~p103(X19)))|p4(X4))&((![X20]:((~r1(X4,X20)|p4(X20))|~p103(X20)))|~p4(X4)))|~p103(X4)))&((((![X21]:((~r1(X4,X21)|~p3(X21))|~p102(X21)))|p3(X4))&((![X22]:((~r1(X4,X22)|p3(X22))|~p102(X22)))|~p3(X4)))|~p102(X4)))&((((![X23]:((~r1(X4,X23)|~p2(X23))|~p101(X23)))|p2(X4))&((![X24]:((~r1(X4,X24)|p2(X24))|~p101(X24)))|~p2(X4)))|~p101(X4)))&((((![X25]:((~r1(X4,X25)|~p1(X25))|~p100(X25)))|p1(X4))&((![X26]:((~r1(X4,X26)|p1(X26))|~p100(X26)))|~p1(X4)))|~p100(X4)))&(p105(X4)|~p106(X4)))&(p104(X4)|~p105(X4)))&(p103(X4)|~p104(X4)))&(p102(X4)|~p103(X4)))&(p101(X4)|~p102(X4)))&(p100(X4)|~p101(X4)))))&~p101(skolem0001))&p100(skolem0001))),inference(skolemize,[status(esa)],[c3])).])).
% 0.57/0.81 fof(c6,negated_conjecture,(![X3]:(![X4]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:((~r1(skolem0001,X3)|p3(X3))&(((((((((((((((((((((~r1(skolem0001,X4)|(r1(X4,skolem0002(X4))|(p105(X4)|~p104(X4))))&(((~r1(skolem0001,X4)|(~p6(skolem0002(X4))|(p105(X4)|~p104(X4))))&(~r1(skolem0001,X4)|(~p106(skolem0002(X4))|(p105(X4)|~p104(X4)))))&(~r1(skolem0001,X4)|(p105(skolem0002(X4))|(p105(X4)|~p104(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0003(X4))|(p105(X4)|~p104(X4))))&(((~r1(skolem0001,X4)|(p6(skolem0003(X4))|(p105(X4)|~p104(X4))))&(~r1(skolem0001,X4)|(~p106(skolem0003(X4))|(p105(X4)|~p104(X4)))))&(~r1(skolem0001,X4)|(p105(skolem0003(X4))|(p105(X4)|~p104(X4)))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0004(X4))|(p104(X4)|~p103(X4))))&(((~r1(skolem0001,X4)|(~p5(skolem0004(X4))|(p104(X4)|~p103(X4))))&(~r1(skolem0001,X4)|(~p105(skolem0004(X4))|(p104(X4)|~p103(X4)))))&(~r1(skolem0001,X4)|(p104(skolem0004(X4))|(p104(X4)|~p103(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0005(X4))|(p104(X4)|~p103(X4))))&(((~r1(skolem0001,X4)|(p5(skolem0005(X4))|(p104(X4)|~p103(X4))))&(~r1(skolem0001,X4)|(~p105(skolem0005(X4))|(p104(X4)|~p103(X4)))))&(~r1(skolem0001,X4)|(p104(skolem0005(X4))|(p104(X4)|~p103(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0006(X4))|(p103(X4)|~p102(X4))))&(((~r1(skolem0001,X4)|(~p4(skolem0006(X4))|(p103(X4)|~p102(X4))))&(~r1(skolem0001,X4)|(~p104(skolem0006(X4))|(p103(X4)|~p102(X4)))))&(~r1(skolem0001,X4)|(p103(skolem0006(X4))|(p103(X4)|~p102(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0007(X4))|(p103(X4)|~p102(X4))))&(((~r1(skolem0001,X4)|(p4(skolem0007(X4))|(p103(X4)|~p102(X4))))&(~r1(skolem0001,X4)|(~p104(skolem0007(X4))|(p103(X4)|~p102(X4)))))&(~r1(skolem0001,X4)|(p103(skolem0007(X4))|(p103(X4)|~p102(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0008(X4))|(p102(X4)|~p101(X4))))&(((~r1(skolem0001,X4)|(~p3(skolem0008(X4))|(p102(X4)|~p101(X4))))&(~r1(skolem0001,X4)|(~p103(skolem0008(X4))|(p102(X4)|~p101(X4)))))&(~r1(skolem0001,X4)|(p102(skolem0008(X4))|(p102(X4)|~p101(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0009(X4))|(p102(X4)|~p101(X4))))&(((~r1(skolem0001,X4)|(p3(skolem0009(X4))|(p102(X4)|~p101(X4))))&(~r1(skolem0001,X4)|(~p103(skolem0009(X4))|(p102(X4)|~p101(X4)))))&(~r1(skolem0001,X4)|(p102(skolem0009(X4))|(p102(X4)|~p101(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0010(X4))|(p101(X4)|~p100(X4))))&(((~r1(skolem0001,X4)|(~p2(skolem0010(X4))|(p101(X4)|~p100(X4))))&(~r1(skolem0001,X4)|(~p102(skolem0010(X4))|(p101(X4)|~p100(X4)))))&(~r1(skolem0001,X4)|(p101(skolem0010(X4))|(p101(X4)|~p100(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0011(X4))|(p101(X4)|~p100(X4))))&(((~r1(skolem0001,X4)|(p2(skolem0011(X4))|(p101(X4)|~p100(X4))))&(~r1(skolem0001,X4)|(~p102(skolem0011(X4))|(p101(X4)|~p100(X4)))))&(~r1(skolem0001,X4)|(p101(skolem0011(X4))|(p101(X4)|~p100(X4))))))))&((~r1(skolem0001,X4)|((((~r1(X4,X15)|~p6(X15))|~p105(X15))|p6(X4))|~p105(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X16)|p6(X16))|~p105(X16))|~p6(X4))|~p105(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X17)|~p5(X17))|~p104(X17))|p5(X4))|~p104(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X18)|p5(X18))|~p104(X18))|~p5(X4))|~p104(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X19)|~p4(X19))|~p103(X19))|p4(X4))|~p103(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X20)|p4(X20))|~p103(X20))|~p4(X4))|~p103(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X21)|~p3(X21))|~p102(X21))|p3(X4))|~p102(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X22)|p3(X22))|~p102(X22))|~p3(X4))|~p102(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X23)|~p2(X23))|~p101(X23))|p2(X4))|~p101(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X24)|p2(X24))|~p101(X24))|~p2(X4))|~p101(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X25)|~p1(X25))|~p100(X25))|p1(X4))|~p100(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X26)|p1(X26))|~p100(X26))|~p1(X4))|~p100(X4)))))&(~r1(skolem0001,X4)|(p105(X4)|~p106(X4))))&(~r1(skolem0001,X4)|(p104(X4)|~p105(X4))))&(~r1(skolem0001,X4)|(p103(X4)|~p104(X4))))&(~r1(skolem0001,X4)|(p102(X4)|~p103(X4))))&(~r1(skolem0001,X4)|(p101(X4)|~p102(X4))))&(~r1(skolem0001,X4)|(p100(X4)|~p101(X4))))&~p101(skolem0001))&p100(skolem0001))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 0.57/0.81 cnf(c66,negated_conjecture,~p101(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.57/0.81 cnf(c67,negated_conjecture,p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.57/0.81 fof(reflexivity,axiom,(![X]:r1(X,X)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 0.57/0.81 fof(c71,plain,(![X30]:r1(X30,X30)),inference(variable_rename,[status(thm)],[reflexivity])).
% 0.57/0.81 cnf(c72,plain,r1(X31,X31),inference(split_conjunct,[status(thm)],[c71])).
% 0.57/0.81 cnf(c42,negated_conjecture,~r1(skolem0001,X77)|~p102(skolem0010(X77))|p101(X77)|~p100(X77),inference(split_conjunct,[status(thm)],[c6])).
% 0.57/0.81 cnf(c43,negated_conjecture,~r1(skolem0001,X79)|p101(skolem0010(X79))|p101(X79)|~p100(X79),inference(split_conjunct,[status(thm)],[c6])).
% 0.57/0.81 cnf(c102,plain,p101(skolem0010(skolem0001))|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c43, c72])).
% 0.57/0.81 cnf(c103,plain,p101(skolem0010(skolem0001))|p101(skolem0001),inference(resolution,[status(thm)],[c102, c67])).
% 0.57/0.81 cnf(c104,plain,p101(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c103, c66])).
% 0.57/0.81 cnf(c40,negated_conjecture,~r1(skolem0001,X81)|r1(X81,skolem0010(X81))|p101(X81)|~p100(X81),inference(split_conjunct,[status(thm)],[c6])).
% 0.57/0.81 cnf(c106,plain,r1(skolem0001,skolem0010(skolem0001))|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c40, c72])).
% 0.57/0.81 cnf(c117,plain,r1(skolem0001,skolem0010(skolem0001))|p101(skolem0001),inference(resolution,[status(thm)],[c106, c67])).
% 0.57/0.81 cnf(c153,plain,r1(skolem0001,skolem0010(skolem0001)),inference(resolution,[status(thm)],[c117, c66])).
% 0.57/0.81 cnf(c33,negated_conjecture,~r1(skolem0001,X68)|~p3(skolem0008(X68))|p102(X68)|~p101(X68),inference(split_conjunct,[status(thm)],[c6])).
% 0.57/0.81 cnf(c7,negated_conjecture,~r1(skolem0001,X32)|p3(X32),inference(split_conjunct,[status(thm)],[c6])).
% 0.57/0.81 fof(transitivity,axiom,(![X]:(![Y]:(![Z]:((r1(X,Y)&r1(Y,Z))=>r1(X,Z))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', transitivity)).
% 0.57/0.81 fof(c68,plain,(![X]:(![Y]:(![Z]:((~r1(X,Y)|~r1(Y,Z))|r1(X,Z))))),inference(fof_nnf,[status(thm)],[transitivity])).
% 0.57/0.81 fof(c69,plain,(![X27]:(![X28]:(![X29]:((~r1(X27,X28)|~r1(X28,X29))|r1(X27,X29))))),inference(variable_rename,[status(thm)],[c68])).
% 0.57/0.81 cnf(c70,plain,~r1(X42,X44)|~r1(X44,X43)|r1(X42,X43),inference(split_conjunct,[status(thm)],[c69])).
% 0.57/0.81 cnf(c32,negated_conjecture,~r1(skolem0001,X73)|r1(X73,skolem0008(X73))|p102(X73)|~p101(X73),inference(split_conjunct,[status(thm)],[c6])).
% 0.57/0.81 cnf(c118,plain,p101(skolem0001)|r1(skolem0010(skolem0001),skolem0008(skolem0010(skolem0001)))|p102(skolem0010(skolem0001))|~p101(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c117, c32])).
% 0.57/0.81 cnf(c306,plain,p101(skolem0001)|r1(skolem0010(skolem0001),skolem0008(skolem0010(skolem0001)))|p102(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c118, c104])).
% 0.57/0.81 cnf(c338,plain,r1(skolem0010(skolem0001),skolem0008(skolem0010(skolem0001)))|p102(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c306, c66])).
% 0.57/0.81 cnf(c364,plain,p102(skolem0010(skolem0001))|~r1(X124,skolem0010(skolem0001))|r1(X124,skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c338, c70])).
% 0.57/0.81 cnf(c426,plain,p102(skolem0010(skolem0001))|r1(skolem0001,skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c364, c153])).
% 0.57/0.81 cnf(c458,plain,p102(skolem0010(skolem0001))|p3(skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c426, c7])).
% 0.57/0.81 cnf(c481,plain,p102(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|~p101(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c458, c33])).
% 0.57/0.81 cnf(c483,plain,p102(skolem0010(skolem0001))|~p101(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c481, c153])).
% 0.57/0.81 cnf(c484,plain,p102(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c483, c104])).
% 0.57/0.81 cnf(c486,plain,~r1(skolem0001,skolem0001)|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c484, c42])).
% 0.57/0.81 cnf(c490,plain,p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c486, c72])).
% 0.57/0.81 cnf(c491,plain,p101(skolem0001),inference(resolution,[status(thm)],[c490, c67])).
% 0.57/0.81 cnf(c492,plain,$false,inference(resolution,[status(thm)],[c491, c66])).
% 0.57/0.81 % SZS output end CNFRefutation
% 0.57/0.81
% 0.57/0.81 % Initial clauses : 63
% 0.57/0.81 % Processed clauses : 190
% 0.57/0.81 % Factors computed : 12
% 0.57/0.81 % Resolvents computed: 408
% 0.57/0.81 % Tautologies deleted: 24
% 0.57/0.81 % Forward subsumed : 65
% 0.57/0.81 % Backward subsumed : 64
% 0.57/0.81 % -------- CPU Time ---------
% 0.57/0.81 % User time : 0.441 s
% 0.57/0.81 % System time : 0.028 s
% 0.57/0.81 % Total time : 0.469 s
%------------------------------------------------------------------------------