%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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 30.96s 31.28s
% Output : CNFRefutation 30.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.34 % Computer : n028.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Sat Sep 5 21:14:15 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.41 (re.compile("\."), Token.FullStop),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.41 (re.compile("\("), Token.OpenPar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.41 (re.compile("\)"), Token.ClosePar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.41 (re.compile("\["), Token.OpenSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.22/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.32/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.57 """
% 30.96/31.28 % Version: 1.5
% 30.96/31.28 % SZS status Theorem
% 30.96/31.28 % SZS output start CNFRefutation
% 30.96/31.28 fof(main,conjecture,(~(?[X]:(~((~(![Y]:((~r1(X,Y))|p5(Y))))|(~(((![Y]:((~r1(X,Y))|((((((((((((((((((((((((((((((((((~(![X]:((~r1(Y,X))|(~(((~p11(X))&(~p111(X)))&p110(X))))))&(~(![X]:((~r1(Y,X))|(~((p11(X)&(~p111(X)))&p110(X)))))))|(~((~p110(Y))&p109(Y))))&(((~(![X]:((~r1(Y,X))|(~(((~p10(X))&(~p110(X)))&p109(X))))))&(~(![X]:((~r1(Y,X))|(~((p10(X)&(~p110(X)))&p109(X)))))))|(~((~p109(Y))&p108(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p9(X))&(~p109(X)))&p108(X))))))&(~(![X]:((~r1(Y,X))|(~((p9(X)&(~p109(X)))&p108(X)))))))|(~((~p108(Y))&p107(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p8(X))&(~p108(X)))&p107(X))))))&(~(![X]:((~r1(Y,X))|(~((p8(X)&(~p108(X)))&p107(X)))))))|(~((~p107(Y))&p106(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p7(X))&(~p107(X)))&p106(X))))))&(~(![X]:((~r1(Y,X))|(~((p7(X)&(~p107(X)))&p106(X)))))))|(~((~p106(Y))&p105(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))|(~p11(X)))|(~p110(X))))|p11(Y))&((![X]:(((~r1(Y,X))|p11(X))|(~p110(X))))|(~p11(Y))))|(~p110(Y))))&((((![X]:(((~r1(Y,X))|(~p10(X)))|(~p109(X))))|p10(Y))&((![X]:(((~r1(Y,X))|p10(X))|(~p109(X))))|(~p10(Y))))|(~p109(Y))))&((((![X]:(((~r1(Y,X))|(~p9(X)))|(~p108(X))))|p9(Y))&((![X]:(((~r1(Y,X))|p9(X))|(~p108(X))))|(~p9(Y))))|(~p108(Y))))&((((![X]:(((~r1(Y,X))|(~p8(X)))|(~p107(X))))|p8(Y))&((![X]:(((~r1(Y,X))|p8(X))|(~p107(X))))|(~p8(Y))))|(~p107(Y))))&((((![X]:(((~r1(Y,X))|(~p7(X)))|(~p106(X))))|p7(Y))&((![X]:(((~r1(Y,X))|p7(X))|(~p106(X))))|(~p7(Y))))|(~p106(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))))&(p110(Y)|(~p111(Y))))&(p109(Y)|(~p110(Y))))&(p108(Y)|(~p109(Y))))&(p107(Y)|(~p108(Y))))&(p106(Y)|(~p107(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)).
% 30.96/31.28 fof(c0,negated_conjecture,(~(~(?[X]:(~((~(![Y]:((~r1(X,Y))|p5(Y))))|(~(((![Y]:((~r1(X,Y))|((((((((((((((((((((((((((((((((((~(![X]:((~r1(Y,X))|(~(((~p11(X))&(~p111(X)))&p110(X))))))&(~(![X]:((~r1(Y,X))|(~((p11(X)&(~p111(X)))&p110(X)))))))|(~((~p110(Y))&p109(Y))))&(((~(![X]:((~r1(Y,X))|(~(((~p10(X))&(~p110(X)))&p109(X))))))&(~(![X]:((~r1(Y,X))|(~((p10(X)&(~p110(X)))&p109(X)))))))|(~((~p109(Y))&p108(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p9(X))&(~p109(X)))&p108(X))))))&(~(![X]:((~r1(Y,X))|(~((p9(X)&(~p109(X)))&p108(X)))))))|(~((~p108(Y))&p107(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p8(X))&(~p108(X)))&p107(X))))))&(~(![X]:((~r1(Y,X))|(~((p8(X)&(~p108(X)))&p107(X)))))))|(~((~p107(Y))&p106(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p7(X))&(~p107(X)))&p106(X))))))&(~(![X]:((~r1(Y,X))|(~((p7(X)&(~p107(X)))&p106(X)))))))|(~((~p106(Y))&p105(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))|(~p11(X)))|(~p110(X))))|p11(Y))&((![X]:(((~r1(Y,X))|p11(X))|(~p110(X))))|(~p11(Y))))|(~p110(Y))))&((((![X]:(((~r1(Y,X))|(~p10(X)))|(~p109(X))))|p10(Y))&((![X]:(((~r1(Y,X))|p10(X))|(~p109(X))))|(~p10(Y))))|(~p109(Y))))&((((![X]:(((~r1(Y,X))|(~p9(X)))|(~p108(X))))|p9(Y))&((![X]:(((~r1(Y,X))|p9(X))|(~p108(X))))|(~p9(Y))))|(~p108(Y))))&((((![X]:(((~r1(Y,X))|(~p8(X)))|(~p107(X))))|p8(Y))&((![X]:(((~r1(Y,X))|p8(X))|(~p107(X))))|(~p8(Y))))|(~p107(Y))))&((((![X]:(((~r1(Y,X))|(~p7(X)))|(~p106(X))))|p7(Y))&((![X]:(((~r1(Y,X))|p7(X))|(~p106(X))))|(~p7(Y))))|(~p106(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))))&(p110(Y)|(~p111(Y))))&(p109(Y)|(~p110(Y))))&(p108(Y)|(~p109(Y))))&(p107(Y)|(~p108(Y))))&(p106(Y)|(~p107(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])).
% 30.96/31.28 fof(c1,negated_conjecture,(~(~(?[X]:(~((~(![Y]:(~r1(X,Y)|p5(Y))))|(~(((![Y]:(~r1(X,Y)|((((((((((((((((((((((((((((((((((~(![X]:(~r1(Y,X)|(~((~p11(X)&~p111(X))&p110(X))))))&(~(![X]:(~r1(Y,X)|(~((p11(X)&~p111(X))&p110(X)))))))|(~(~p110(Y)&p109(Y))))&(((~(![X]:(~r1(Y,X)|(~((~p10(X)&~p110(X))&p109(X))))))&(~(![X]:(~r1(Y,X)|(~((p10(X)&~p110(X))&p109(X)))))))|(~(~p109(Y)&p108(Y)))))&(((~(![X]:(~r1(Y,X)|(~((~p9(X)&~p109(X))&p108(X))))))&(~(![X]:(~r1(Y,X)|(~((p9(X)&~p109(X))&p108(X)))))))|(~(~p108(Y)&p107(Y)))))&(((~(![X]:(~r1(Y,X)|(~((~p8(X)&~p108(X))&p107(X))))))&(~(![X]:(~r1(Y,X)|(~((p8(X)&~p108(X))&p107(X)))))))|(~(~p107(Y)&p106(Y)))))&(((~(![X]:(~r1(Y,X)|(~((~p7(X)&~p107(X))&p106(X))))))&(~(![X]:(~r1(Y,X)|(~((p7(X)&~p107(X))&p106(X)))))))|(~(~p106(Y)&p105(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)|~p11(X))|~p110(X)))|p11(Y))&((![X]:((~r1(Y,X)|p11(X))|~p110(X)))|~p11(Y)))|~p110(Y)))&((((![X]:((~r1(Y,X)|~p10(X))|~p109(X)))|p10(Y))&((![X]:((~r1(Y,X)|p10(X))|~p109(X)))|~p10(Y)))|~p109(Y)))&((((![X]:((~r1(Y,X)|~p9(X))|~p108(X)))|p9(Y))&((![X]:((~r1(Y,X)|p9(X))|~p108(X)))|~p9(Y)))|~p108(Y)))&((((![X]:((~r1(Y,X)|~p8(X))|~p107(X)))|p8(Y))&((![X]:((~r1(Y,X)|p8(X))|~p107(X)))|~p8(Y)))|~p107(Y)))&((((![X]:((~r1(Y,X)|~p7(X))|~p106(X)))|p7(Y))&((![X]:((~r1(Y,X)|p7(X))|~p106(X)))|~p7(Y)))|~p106(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)))&(p110(Y)|~p111(Y)))&(p109(Y)|~p110(Y)))&(p108(Y)|~p109(Y)))&(p107(Y)|~p108(Y)))&(p106(Y)|~p107(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])).
% 30.96/31.28 fof(c2,negated_conjecture,(?[X]:((![Y]:(~r1(X,Y)|p5(Y)))&(((![Y]:(~r1(X,Y)|((((((((((((((((((((((((((((((((((?[X]:(r1(Y,X)&((~p11(X)&~p111(X))&p110(X))))&(?[X]:(r1(Y,X)&((p11(X)&~p111(X))&p110(X)))))|(p110(Y)|~p109(Y)))&(((?[X]:(r1(Y,X)&((~p10(X)&~p110(X))&p109(X))))&(?[X]:(r1(Y,X)&((p10(X)&~p110(X))&p109(X)))))|(p109(Y)|~p108(Y))))&(((?[X]:(r1(Y,X)&((~p9(X)&~p109(X))&p108(X))))&(?[X]:(r1(Y,X)&((p9(X)&~p109(X))&p108(X)))))|(p108(Y)|~p107(Y))))&(((?[X]:(r1(Y,X)&((~p8(X)&~p108(X))&p107(X))))&(?[X]:(r1(Y,X)&((p8(X)&~p108(X))&p107(X)))))|(p107(Y)|~p106(Y))))&(((?[X]:(r1(Y,X)&((~p7(X)&~p107(X))&p106(X))))&(?[X]:(r1(Y,X)&((p7(X)&~p107(X))&p106(X)))))|(p106(Y)|~p105(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)|~p11(X))|~p110(X)))|p11(Y))&((![X]:((~r1(Y,X)|p11(X))|~p110(X)))|~p11(Y)))|~p110(Y)))&((((![X]:((~r1(Y,X)|~p10(X))|~p109(X)))|p10(Y))&((![X]:((~r1(Y,X)|p10(X))|~p109(X)))|~p10(Y)))|~p109(Y)))&((((![X]:((~r1(Y,X)|~p9(X))|~p108(X)))|p9(Y))&((![X]:((~r1(Y,X)|p9(X))|~p108(X)))|~p9(Y)))|~p108(Y)))&((((![X]:((~r1(Y,X)|~p8(X))|~p107(X)))|p8(Y))&((![X]:((~r1(Y,X)|p8(X))|~p107(X)))|~p8(Y)))|~p107(Y)))&((((![X]:((~r1(Y,X)|~p7(X))|~p106(X)))|p7(Y))&((![X]:((~r1(Y,X)|p7(X))|~p106(X)))|~p7(Y)))|~p106(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)))&(p110(Y)|~p111(Y)))&(p109(Y)|~p110(Y)))&(p108(Y)|~p109(Y)))&(p107(Y)|~p108(Y)))&(p106(Y)|~p107(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])).
% 30.96/31.29 fof(c3,negated_conjecture,(?[X2]:((![X3]:(~r1(X2,X3)|p5(X3)))&(((![X4]:(~r1(X2,X4)|((((((((((((((((((((((((((((((((((?[X5]:(r1(X4,X5)&((~p11(X5)&~p111(X5))&p110(X5))))&(?[X6]:(r1(X4,X6)&((p11(X6)&~p111(X6))&p110(X6)))))|(p110(X4)|~p109(X4)))&(((?[X7]:(r1(X4,X7)&((~p10(X7)&~p110(X7))&p109(X7))))&(?[X8]:(r1(X4,X8)&((p10(X8)&~p110(X8))&p109(X8)))))|(p109(X4)|~p108(X4))))&(((?[X9]:(r1(X4,X9)&((~p9(X9)&~p109(X9))&p108(X9))))&(?[X10]:(r1(X4,X10)&((p9(X10)&~p109(X10))&p108(X10)))))|(p108(X4)|~p107(X4))))&(((?[X11]:(r1(X4,X11)&((~p8(X11)&~p108(X11))&p107(X11))))&(?[X12]:(r1(X4,X12)&((p8(X12)&~p108(X12))&p107(X12)))))|(p107(X4)|~p106(X4))))&(((?[X13]:(r1(X4,X13)&((~p7(X13)&~p107(X13))&p106(X13))))&(?[X14]:(r1(X4,X14)&((p7(X14)&~p107(X14))&p106(X14)))))|(p106(X4)|~p105(X4))))&(((?[X15]:(r1(X4,X15)&((~p6(X15)&~p106(X15))&p105(X15))))&(?[X16]:(r1(X4,X16)&((p6(X16)&~p106(X16))&p105(X16)))))|(p105(X4)|~p104(X4))))&(((?[X17]:(r1(X4,X17)&((~p5(X17)&~p105(X17))&p104(X17))))&(?[X18]:(r1(X4,X18)&((p5(X18)&~p105(X18))&p104(X18)))))|(p104(X4)|~p103(X4))))&(((?[X19]:(r1(X4,X19)&((~p4(X19)&~p104(X19))&p103(X19))))&(?[X20]:(r1(X4,X20)&((p4(X20)&~p104(X20))&p103(X20)))))|(p103(X4)|~p102(X4))))&(((?[X21]:(r1(X4,X21)&((~p3(X21)&~p103(X21))&p102(X21))))&(?[X22]:(r1(X4,X22)&((p3(X22)&~p103(X22))&p102(X22)))))|(p102(X4)|~p101(X4))))&(((?[X23]:(r1(X4,X23)&((~p2(X23)&~p102(X23))&p101(X23))))&(?[X24]:(r1(X4,X24)&((p2(X24)&~p102(X24))&p101(X24)))))|(p101(X4)|~p100(X4))))&((((![X25]:((~r1(X4,X25)|~p11(X25))|~p110(X25)))|p11(X4))&((![X26]:((~r1(X4,X26)|p11(X26))|~p110(X26)))|~p11(X4)))|~p110(X4)))&((((![X27]:((~r1(X4,X27)|~p10(X27))|~p109(X27)))|p10(X4))&((![X28]:((~r1(X4,X28)|p10(X28))|~p109(X28)))|~p10(X4)))|~p109(X4)))&((((![X29]:((~r1(X4,X29)|~p9(X29))|~p108(X29)))|p9(X4))&((![X30]:((~r1(X4,X30)|p9(X30))|~p108(X30)))|~p9(X4)))|~p108(X4)))&((((![X31]:((~r1(X4,X31)|~p8(X31))|~p107(X31)))|p8(X4))&((![X32]:((~r1(X4,X32)|p8(X32))|~p107(X32)))|~p8(X4)))|~p107(X4)))&((((![X33]:((~r1(X4,X33)|~p7(X33))|~p106(X33)))|p7(X4))&((![X34]:((~r1(X4,X34)|p7(X34))|~p106(X34)))|~p7(X4)))|~p106(X4)))&((((![X35]:((~r1(X4,X35)|~p6(X35))|~p105(X35)))|p6(X4))&((![X36]:((~r1(X4,X36)|p6(X36))|~p105(X36)))|~p6(X4)))|~p105(X4)))&((((![X37]:((~r1(X4,X37)|~p5(X37))|~p104(X37)))|p5(X4))&((![X38]:((~r1(X4,X38)|p5(X38))|~p104(X38)))|~p5(X4)))|~p104(X4)))&((((![X39]:((~r1(X4,X39)|~p4(X39))|~p103(X39)))|p4(X4))&((![X40]:((~r1(X4,X40)|p4(X40))|~p103(X40)))|~p4(X4)))|~p103(X4)))&((((![X41]:((~r1(X4,X41)|~p3(X41))|~p102(X41)))|p3(X4))&((![X42]:((~r1(X4,X42)|p3(X42))|~p102(X42)))|~p3(X4)))|~p102(X4)))&((((![X43]:((~r1(X4,X43)|~p2(X43))|~p101(X43)))|p2(X4))&((![X44]:((~r1(X4,X44)|p2(X44))|~p101(X44)))|~p2(X4)))|~p101(X4)))&((((![X45]:((~r1(X4,X45)|~p1(X45))|~p100(X45)))|p1(X4))&((![X46]:((~r1(X4,X46)|p1(X46))|~p100(X46)))|~p1(X4)))|~p100(X4)))&(p110(X4)|~p111(X4)))&(p109(X4)|~p110(X4)))&(p108(X4)|~p109(X4)))&(p107(X4)|~p108(X4)))&(p106(X4)|~p107(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])).
% 30.96/31.29 fof(c5,negated_conjecture,(![X3]:(![X4]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:((~r1(skolem0001,X3)|p5(X3))&(((~r1(skolem0001,X4)|((((((((((((((((((((((((((((((((((r1(X4,skolem0002(X4))&((~p11(skolem0002(X4))&~p111(skolem0002(X4)))&p110(skolem0002(X4))))&(r1(X4,skolem0003(X4))&((p11(skolem0003(X4))&~p111(skolem0003(X4)))&p110(skolem0003(X4)))))|(p110(X4)|~p109(X4)))&(((r1(X4,skolem0004(X4))&((~p10(skolem0004(X4))&~p110(skolem0004(X4)))&p109(skolem0004(X4))))&(r1(X4,skolem0005(X4))&((p10(skolem0005(X4))&~p110(skolem0005(X4)))&p109(skolem0005(X4)))))|(p109(X4)|~p108(X4))))&(((r1(X4,skolem0006(X4))&((~p9(skolem0006(X4))&~p109(skolem0006(X4)))&p108(skolem0006(X4))))&(r1(X4,skolem0007(X4))&((p9(skolem0007(X4))&~p109(skolem0007(X4)))&p108(skolem0007(X4)))))|(p108(X4)|~p107(X4))))&(((r1(X4,skolem0008(X4))&((~p8(skolem0008(X4))&~p108(skolem0008(X4)))&p107(skolem0008(X4))))&(r1(X4,skolem0009(X4))&((p8(skolem0009(X4))&~p108(skolem0009(X4)))&p107(skolem0009(X4)))))|(p107(X4)|~p106(X4))))&(((r1(X4,skolem0010(X4))&((~p7(skolem0010(X4))&~p107(skolem0010(X4)))&p106(skolem0010(X4))))&(r1(X4,skolem0011(X4))&((p7(skolem0011(X4))&~p107(skolem0011(X4)))&p106(skolem0011(X4)))))|(p106(X4)|~p105(X4))))&(((r1(X4,skolem0012(X4))&((~p6(skolem0012(X4))&~p106(skolem0012(X4)))&p105(skolem0012(X4))))&(r1(X4,skolem0013(X4))&((p6(skolem0013(X4))&~p106(skolem0013(X4)))&p105(skolem0013(X4)))))|(p105(X4)|~p104(X4))))&(((r1(X4,skolem0014(X4))&((~p5(skolem0014(X4))&~p105(skolem0014(X4)))&p104(skolem0014(X4))))&(r1(X4,skolem0015(X4))&((p5(skolem0015(X4))&~p105(skolem0015(X4)))&p104(skolem0015(X4)))))|(p104(X4)|~p103(X4))))&(((r1(X4,skolem0016(X4))&((~p4(skolem0016(X4))&~p104(skolem0016(X4)))&p103(skolem0016(X4))))&(r1(X4,skolem0017(X4))&((p4(skolem0017(X4))&~p104(skolem0017(X4)))&p103(skolem0017(X4)))))|(p103(X4)|~p102(X4))))&(((r1(X4,skolem0018(X4))&((~p3(skolem0018(X4))&~p103(skolem0018(X4)))&p102(skolem0018(X4))))&(r1(X4,skolem0019(X4))&((p3(skolem0019(X4))&~p103(skolem0019(X4)))&p102(skolem0019(X4)))))|(p102(X4)|~p101(X4))))&(((r1(X4,skolem0020(X4))&((~p2(skolem0020(X4))&~p102(skolem0020(X4)))&p101(skolem0020(X4))))&(r1(X4,skolem0021(X4))&((p2(skolem0021(X4))&~p102(skolem0021(X4)))&p101(skolem0021(X4)))))|(p101(X4)|~p100(X4))))&(((((~r1(X4,X25)|~p11(X25))|~p110(X25))|p11(X4))&(((~r1(X4,X26)|p11(X26))|~p110(X26))|~p11(X4)))|~p110(X4)))&(((((~r1(X4,X27)|~p10(X27))|~p109(X27))|p10(X4))&(((~r1(X4,X28)|p10(X28))|~p109(X28))|~p10(X4)))|~p109(X4)))&(((((~r1(X4,X29)|~p9(X29))|~p108(X29))|p9(X4))&(((~r1(X4,X30)|p9(X30))|~p108(X30))|~p9(X4)))|~p108(X4)))&(((((~r1(X4,X31)|~p8(X31))|~p107(X31))|p8(X4))&(((~r1(X4,X32)|p8(X32))|~p107(X32))|~p8(X4)))|~p107(X4)))&(((((~r1(X4,X33)|~p7(X33))|~p106(X33))|p7(X4))&(((~r1(X4,X34)|p7(X34))|~p106(X34))|~p7(X4)))|~p106(X4)))&(((((~r1(X4,X35)|~p6(X35))|~p105(X35))|p6(X4))&(((~r1(X4,X36)|p6(X36))|~p105(X36))|~p6(X4)))|~p105(X4)))&(((((~r1(X4,X37)|~p5(X37))|~p104(X37))|p5(X4))&(((~r1(X4,X38)|p5(X38))|~p104(X38))|~p5(X4)))|~p104(X4)))&(((((~r1(X4,X39)|~p4(X39))|~p103(X39))|p4(X4))&(((~r1(X4,X40)|p4(X40))|~p103(X40))|~p4(X4)))|~p103(X4)))&(((((~r1(X4,X41)|~p3(X41))|~p102(X41))|p3(X4))&(((~r1(X4,X42)|p3(X42))|~p102(X42))|~p3(X4)))|~p102(X4)))&(((((~r1(X4,X43)|~p2(X43))|~p101(X43))|p2(X4))&(((~r1(X4,X44)|p2(X44))|~p101(X44))|~p2(X4)))|~p101(X4)))&(((((~r1(X4,X45)|~p1(X45))|~p100(X45))|p1(X4))&(((~r1(X4,X46)|p1(X46))|~p100(X46))|~p1(X4)))|~p100(X4)))&(p110(X4)|~p111(X4)))&(p109(X4)|~p110(X4)))&(p108(X4)|~p109(X4)))&(p107(X4)|~p108(X4)))&(p106(X4)|~p107(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)|p5(X3)))&(((![X4]:(~r1(skolem0001,X4)|((((((((((((((((((((((((((((((((((r1(X4,skolem0002(X4))&((~p11(skolem0002(X4))&~p111(skolem0002(X4)))&p110(skolem0002(X4))))&(r1(X4,skolem0003(X4))&((p11(skolem0003(X4))&~p111(skolem0003(X4)))&p110(skolem0003(X4)))))|(p110(X4)|~p109(X4)))&(((r1(X4,skolem0004(X4))&((~p10(skolem0004(X4))&~p110(skolem0004(X4)))&p109(skolem0004(X4))))&(r1(X4,skolem0005(X4))&((p10(skolem0005(X4))&~p110(skolem0005(X4)))&p109(skolem0005(X4)))))|(p109(X4)|~p108(X4))))&(((r1(X4,skolem0006(X4))&((~p9(skolem0006(X4))&~p109(skolem0006(X4)))&p108(skolem0006(X4))))&(r1(X4,skolem0007(X4))&((p9(skolem0007(X4))&~p109(skolem0007(X4)))&p108(skolem0007(X4)))))|(p108(X4)|~p107(X4))))&(((r1(X4,skolem0008(X4))&((~p8(skolem0008(X4))&~p108(skolem0008(X4)))&p107(skolem0008(X4))))&(r1(X4,skolem0009(X4))&((p8(skolem0009(X4))&~p108(skolem0009(X4)))&p107(skolem0009(X4)))))|(p107(X4)|~p106(X4))))&(((r1(X4,skolem0010(X4))&((~p7(skolem0010(X4))&~p107(skolem0010(X4)))&p106(skolem0010(X4))))&(r1(X4,skolem0011(X4))&((p7(skolem0011(X4))&~p107(skolem0011(X4)))&p106(skolem0011(X4)))))|(p106(X4)|~p105(X4))))&(((r1(X4,skolem0012(X4))&((~p6(skolem0012(X4))&~p106(skolem0012(X4)))&p105(skolem0012(X4))))&(r1(X4,skolem0013(X4))&((p6(skolem0013(X4))&~p106(skolem0013(X4)))&p105(skolem0013(X4)))))|(p105(X4)|~p104(X4))))&(((r1(X4,skolem0014(X4))&((~p5(skolem0014(X4))&~p105(skolem0014(X4)))&p104(skolem0014(X4))))&(r1(X4,skolem0015(X4))&((p5(skolem0015(X4))&~p105(skolem0015(X4)))&p104(skolem0015(X4)))))|(p104(X4)|~p103(X4))))&(((r1(X4,skolem0016(X4))&((~p4(skolem0016(X4))&~p104(skolem0016(X4)))&p103(skolem0016(X4))))&(r1(X4,skolem0017(X4))&((p4(skolem0017(X4))&~p104(skolem0017(X4)))&p103(skolem0017(X4)))))|(p103(X4)|~p102(X4))))&(((r1(X4,skolem0018(X4))&((~p3(skolem0018(X4))&~p103(skolem0018(X4)))&p102(skolem0018(X4))))&(r1(X4,skolem0019(X4))&((p3(skolem0019(X4))&~p103(skolem0019(X4)))&p102(skolem0019(X4)))))|(p102(X4)|~p101(X4))))&(((r1(X4,skolem0020(X4))&((~p2(skolem0020(X4))&~p102(skolem0020(X4)))&p101(skolem0020(X4))))&(r1(X4,skolem0021(X4))&((p2(skolem0021(X4))&~p102(skolem0021(X4)))&p101(skolem0021(X4)))))|(p101(X4)|~p100(X4))))&((((![X25]:((~r1(X4,X25)|~p11(X25))|~p110(X25)))|p11(X4))&((![X26]:((~r1(X4,X26)|p11(X26))|~p110(X26)))|~p11(X4)))|~p110(X4)))&((((![X27]:((~r1(X4,X27)|~p10(X27))|~p109(X27)))|p10(X4))&((![X28]:((~r1(X4,X28)|p10(X28))|~p109(X28)))|~p10(X4)))|~p109(X4)))&((((![X29]:((~r1(X4,X29)|~p9(X29))|~p108(X29)))|p9(X4))&((![X30]:((~r1(X4,X30)|p9(X30))|~p108(X30)))|~p9(X4)))|~p108(X4)))&((((![X31]:((~r1(X4,X31)|~p8(X31))|~p107(X31)))|p8(X4))&((![X32]:((~r1(X4,X32)|p8(X32))|~p107(X32)))|~p8(X4)))|~p107(X4)))&((((![X33]:((~r1(X4,X33)|~p7(X33))|~p106(X33)))|p7(X4))&((![X34]:((~r1(X4,X34)|p7(X34))|~p106(X34)))|~p7(X4)))|~p106(X4)))&((((![X35]:((~r1(X4,X35)|~p6(X35))|~p105(X35)))|p6(X4))&((![X36]:((~r1(X4,X36)|p6(X36))|~p105(X36)))|~p6(X4)))|~p105(X4)))&((((![X37]:((~r1(X4,X37)|~p5(X37))|~p104(X37)))|p5(X4))&((![X38]:((~r1(X4,X38)|p5(X38))|~p104(X38)))|~p5(X4)))|~p104(X4)))&((((![X39]:((~r1(X4,X39)|~p4(X39))|~p103(X39)))|p4(X4))&((![X40]:((~r1(X4,X40)|p4(X40))|~p103(X40)))|~p4(X4)))|~p103(X4)))&((((![X41]:((~r1(X4,X41)|~p3(X41))|~p102(X41)))|p3(X4))&((![X42]:((~r1(X4,X42)|p3(X42))|~p102(X42)))|~p3(X4)))|~p102(X4)))&((((![X43]:((~r1(X4,X43)|~p2(X43))|~p101(X43)))|p2(X4))&((![X44]:((~r1(X4,X44)|p2(X44))|~p101(X44)))|~p2(X4)))|~p101(X4)))&((((![X45]:((~r1(X4,X45)|~p1(X45))|~p100(X45)))|p1(X4))&((![X46]:((~r1(X4,X46)|p1(X46))|~p100(X46)))|~p1(X4)))|~p100(X4)))&(p110(X4)|~p111(X4)))&(p109(X4)|~p110(X4)))&(p108(X4)|~p109(X4)))&(p107(X4)|~p108(X4)))&(p106(X4)|~p107(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])).])).
% 30.96/31.29 fof(c6,negated_conjecture,(![X3]:(![X4]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:((~r1(skolem0001,X3)|p5(X3))&((((((((((((((((((((((((((((((((((((~r1(skolem0001,X4)|(r1(X4,skolem0002(X4))|(p110(X4)|~p109(X4))))&(((~r1(skolem0001,X4)|(~p11(skolem0002(X4))|(p110(X4)|~p109(X4))))&(~r1(skolem0001,X4)|(~p111(skolem0002(X4))|(p110(X4)|~p109(X4)))))&(~r1(skolem0001,X4)|(p110(skolem0002(X4))|(p110(X4)|~p109(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0003(X4))|(p110(X4)|~p109(X4))))&(((~r1(skolem0001,X4)|(p11(skolem0003(X4))|(p110(X4)|~p109(X4))))&(~r1(skolem0001,X4)|(~p111(skolem0003(X4))|(p110(X4)|~p109(X4)))))&(~r1(skolem0001,X4)|(p110(skolem0003(X4))|(p110(X4)|~p109(X4)))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0004(X4))|(p109(X4)|~p108(X4))))&(((~r1(skolem0001,X4)|(~p10(skolem0004(X4))|(p109(X4)|~p108(X4))))&(~r1(skolem0001,X4)|(~p110(skolem0004(X4))|(p109(X4)|~p108(X4)))))&(~r1(skolem0001,X4)|(p109(skolem0004(X4))|(p109(X4)|~p108(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0005(X4))|(p109(X4)|~p108(X4))))&(((~r1(skolem0001,X4)|(p10(skolem0005(X4))|(p109(X4)|~p108(X4))))&(~r1(skolem0001,X4)|(~p110(skolem0005(X4))|(p109(X4)|~p108(X4)))))&(~r1(skolem0001,X4)|(p109(skolem0005(X4))|(p109(X4)|~p108(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0006(X4))|(p108(X4)|~p107(X4))))&(((~r1(skolem0001,X4)|(~p9(skolem0006(X4))|(p108(X4)|~p107(X4))))&(~r1(skolem0001,X4)|(~p109(skolem0006(X4))|(p108(X4)|~p107(X4)))))&(~r1(skolem0001,X4)|(p108(skolem0006(X4))|(p108(X4)|~p107(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0007(X4))|(p108(X4)|~p107(X4))))&(((~r1(skolem0001,X4)|(p9(skolem0007(X4))|(p108(X4)|~p107(X4))))&(~r1(skolem0001,X4)|(~p109(skolem0007(X4))|(p108(X4)|~p107(X4)))))&(~r1(skolem0001,X4)|(p108(skolem0007(X4))|(p108(X4)|~p107(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0008(X4))|(p107(X4)|~p106(X4))))&(((~r1(skolem0001,X4)|(~p8(skolem0008(X4))|(p107(X4)|~p106(X4))))&(~r1(skolem0001,X4)|(~p108(skolem0008(X4))|(p107(X4)|~p106(X4)))))&(~r1(skolem0001,X4)|(p107(skolem0008(X4))|(p107(X4)|~p106(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0009(X4))|(p107(X4)|~p106(X4))))&(((~r1(skolem0001,X4)|(p8(skolem0009(X4))|(p107(X4)|~p106(X4))))&(~r1(skolem0001,X4)|(~p108(skolem0009(X4))|(p107(X4)|~p106(X4)))))&(~r1(skolem0001,X4)|(p107(skolem0009(X4))|(p107(X4)|~p106(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0010(X4))|(p106(X4)|~p105(X4))))&(((~r1(skolem0001,X4)|(~p7(skolem0010(X4))|(p106(X4)|~p105(X4))))&(~r1(skolem0001,X4)|(~p107(skolem0010(X4))|(p106(X4)|~p105(X4)))))&(~r1(skolem0001,X4)|(p106(skolem0010(X4))|(p106(X4)|~p105(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0011(X4))|(p106(X4)|~p105(X4))))&(((~r1(skolem0001,X4)|(p7(skolem0011(X4))|(p106(X4)|~p105(X4))))&(~r1(skolem0001,X4)|(~p107(skolem0011(X4))|(p106(X4)|~p105(X4)))))&(~r1(skolem0001,X4)|(p106(skolem0011(X4))|(p106(X4)|~p105(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0012(X4))|(p105(X4)|~p104(X4))))&(((~r1(skolem0001,X4)|(~p6(skolem0012(X4))|(p105(X4)|~p104(X4))))&(~r1(skolem0001,X4)|(~p106(skolem0012(X4))|(p105(X4)|~p104(X4)))))&(~r1(skolem0001,X4)|(p105(skolem0012(X4))|(p105(X4)|~p104(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0013(X4))|(p105(X4)|~p104(X4))))&(((~r1(skolem0001,X4)|(p6(skolem0013(X4))|(p105(X4)|~p104(X4))))&(~r1(skolem0001,X4)|(~p106(skolem0013(X4))|(p105(X4)|~p104(X4)))))&(~r1(skolem0001,X4)|(p105(skolem0013(X4))|(p105(X4)|~p104(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0014(X4))|(p104(X4)|~p103(X4))))&(((~r1(skolem0001,X4)|(~p5(skolem0014(X4))|(p104(X4)|~p103(X4))))&(~r1(skolem0001,X4)|(~p105(skolem0014(X4))|(p104(X4)|~p103(X4)))))&(~r1(skolem0001,X4)|(p104(skolem0014(X4))|(p104(X4)|~p103(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0015(X4))|(p104(X4)|~p103(X4))))&(((~r1(skolem0001,X4)|(p5(skolem0015(X4))|(p104(X4)|~p103(X4))))&(~r1(skolem0001,X4)|(~p105(skolem0015(X4))|(p104(X4)|~p103(X4)))))&(~r1(skolem0001,X4)|(p104(skolem0015(X4))|(p104(X4)|~p103(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0016(X4))|(p103(X4)|~p102(X4))))&(((~r1(skolem0001,X4)|(~p4(skolem0016(X4))|(p103(X4)|~p102(X4))))&(~r1(skolem0001,X4)|(~p104(skolem0016(X4))|(p103(X4)|~p102(X4)))))&(~r1(skolem0001,X4)|(p103(skolem0016(X4))|(p103(X4)|~p102(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0017(X4))|(p103(X4)|~p102(X4))))&(((~r1(skolem0001,X4)|(p4(skolem0017(X4))|(p103(X4)|~p102(X4))))&(~r1(skolem0001,X4)|(~p104(skolem0017(X4))|(p103(X4)|~p102(X4)))))&(~r1(skolem0001,X4)|(p103(skolem0017(X4))|(p103(X4)|~p102(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0018(X4))|(p102(X4)|~p101(X4))))&(((~r1(skolem0001,X4)|(~p3(skolem0018(X4))|(p102(X4)|~p101(X4))))&(~r1(skolem0001,X4)|(~p103(skolem0018(X4))|(p102(X4)|~p101(X4)))))&(~r1(skolem0001,X4)|(p102(skolem0018(X4))|(p102(X4)|~p101(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0019(X4))|(p102(X4)|~p101(X4))))&(((~r1(skolem0001,X4)|(p3(skolem0019(X4))|(p102(X4)|~p101(X4))))&(~r1(skolem0001,X4)|(~p103(skolem0019(X4))|(p102(X4)|~p101(X4)))))&(~r1(skolem0001,X4)|(p102(skolem0019(X4))|(p102(X4)|~p101(X4))))))))&(((~r1(skolem0001,X4)|(r1(X4,skolem0020(X4))|(p101(X4)|~p100(X4))))&(((~r1(skolem0001,X4)|(~p2(skolem0020(X4))|(p101(X4)|~p100(X4))))&(~r1(skolem0001,X4)|(~p102(skolem0020(X4))|(p101(X4)|~p100(X4)))))&(~r1(skolem0001,X4)|(p101(skolem0020(X4))|(p101(X4)|~p100(X4))))))&((~r1(skolem0001,X4)|(r1(X4,skolem0021(X4))|(p101(X4)|~p100(X4))))&(((~r1(skolem0001,X4)|(p2(skolem0021(X4))|(p101(X4)|~p100(X4))))&(~r1(skolem0001,X4)|(~p102(skolem0021(X4))|(p101(X4)|~p100(X4)))))&(~r1(skolem0001,X4)|(p101(skolem0021(X4))|(p101(X4)|~p100(X4))))))))&((~r1(skolem0001,X4)|((((~r1(X4,X25)|~p11(X25))|~p110(X25))|p11(X4))|~p110(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X26)|p11(X26))|~p110(X26))|~p11(X4))|~p110(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X27)|~p10(X27))|~p109(X27))|p10(X4))|~p109(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X28)|p10(X28))|~p109(X28))|~p10(X4))|~p109(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X29)|~p9(X29))|~p108(X29))|p9(X4))|~p108(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X30)|p9(X30))|~p108(X30))|~p9(X4))|~p108(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X31)|~p8(X31))|~p107(X31))|p8(X4))|~p107(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X32)|p8(X32))|~p107(X32))|~p8(X4))|~p107(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X33)|~p7(X33))|~p106(X33))|p7(X4))|~p106(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X34)|p7(X34))|~p106(X34))|~p7(X4))|~p106(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X35)|~p6(X35))|~p105(X35))|p6(X4))|~p105(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X36)|p6(X36))|~p105(X36))|~p6(X4))|~p105(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X37)|~p5(X37))|~p104(X37))|p5(X4))|~p104(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X38)|p5(X38))|~p104(X38))|~p5(X4))|~p104(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X39)|~p4(X39))|~p103(X39))|p4(X4))|~p103(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X40)|p4(X40))|~p103(X40))|~p4(X4))|~p103(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X41)|~p3(X41))|~p102(X41))|p3(X4))|~p102(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X42)|p3(X42))|~p102(X42))|~p3(X4))|~p102(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X43)|~p2(X43))|~p101(X43))|p2(X4))|~p101(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X44)|p2(X44))|~p101(X44))|~p2(X4))|~p101(X4)))))&((~r1(skolem0001,X4)|((((~r1(X4,X45)|~p1(X45))|~p100(X45))|p1(X4))|~p100(X4)))&(~r1(skolem0001,X4)|((((~r1(X4,X46)|p1(X46))|~p100(X46))|~p1(X4))|~p100(X4)))))&(~r1(skolem0001,X4)|(p110(X4)|~p111(X4))))&(~r1(skolem0001,X4)|(p109(X4)|~p110(X4))))&(~r1(skolem0001,X4)|(p108(X4)|~p109(X4))))&(~r1(skolem0001,X4)|(p107(X4)|~p108(X4))))&(~r1(skolem0001,X4)|(p106(X4)|~p107(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])).
% 30.96/31.29 cnf(c121,negated_conjecture,~p101(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c122,negated_conjecture,p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 fof(reflexivity,axiom,(![X]:r1(X,X)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 30.96/31.29 fof(c126,plain,(![X50]:r1(X50,X50)),inference(variable_rename,[status(thm)],[reflexivity])).
% 30.96/31.29 cnf(c127,plain,r1(X51,X51),inference(split_conjunct,[status(thm)],[c126])).
% 30.96/31.29 cnf(c82,negated_conjecture,~r1(skolem0001,X142)|~p102(skolem0020(X142))|p101(X142)|~p100(X142),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c83,negated_conjecture,~r1(skolem0001,X143)|p101(skolem0020(X143))|p101(X143)|~p100(X143),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c186,plain,p101(skolem0020(skolem0001))|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c83, c127])).
% 30.96/31.29 cnf(c188,plain,p101(skolem0020(skolem0001))|p101(skolem0001),inference(resolution,[status(thm)],[c186, c122])).
% 30.96/31.29 cnf(c189,plain,p101(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c188, c121])).
% 30.96/31.29 cnf(c80,negated_conjecture,~r1(skolem0001,X146)|r1(X146,skolem0020(X146))|p101(X146)|~p100(X146),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c192,plain,r1(skolem0001,skolem0020(skolem0001))|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c80, c127])).
% 30.96/31.29 cnf(c206,plain,r1(skolem0001,skolem0020(skolem0001))|p101(skolem0001),inference(resolution,[status(thm)],[c192, c122])).
% 30.96/31.29 cnf(c277,plain,r1(skolem0001,skolem0020(skolem0001)),inference(resolution,[status(thm)],[c206, c121])).
% 30.96/31.29 cnf(c74,negated_conjecture,~r1(skolem0001,X134)|~p103(skolem0018(X134))|p102(X134)|~p101(X134),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c75,negated_conjecture,~r1(skolem0001,X136)|p102(skolem0018(X136))|p102(X136)|~p101(X136),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c309,plain,p102(skolem0018(skolem0020(skolem0001)))|p102(skolem0020(skolem0001))|~p101(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c277, c75])).
% 30.96/31.29 cnf(c563,plain,p102(skolem0018(skolem0020(skolem0001)))|p102(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c309, c189])).
% 30.96/31.29 cnf(c564,plain,p102(skolem0018(skolem0020(skolem0001)))|~r1(skolem0001,skolem0001)|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c563, c82])).
% 30.96/31.29 cnf(c593,plain,p102(skolem0018(skolem0020(skolem0001)))|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c564, c127])).
% 30.96/31.29 cnf(c594,plain,p102(skolem0018(skolem0020(skolem0001)))|p101(skolem0001),inference(resolution,[status(thm)],[c593, c122])).
% 30.96/31.29 cnf(c595,plain,p102(skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c594, c121])).
% 30.96/31.29 fof(transitivity,axiom,(![X]:(![Y]:(![Z]:((r1(X,Y)&r1(Y,Z))=>r1(X,Z))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', transitivity)).
% 30.96/31.29 fof(c123,plain,(![X]:(![Y]:(![Z]:((~r1(X,Y)|~r1(Y,Z))|r1(X,Z))))),inference(fof_nnf,[status(thm)],[transitivity])).
% 30.96/31.29 fof(c124,plain,(![X47]:(![X48]:(![X49]:((~r1(X47,X48)|~r1(X48,X49))|r1(X47,X49))))),inference(variable_rename,[status(thm)],[c123])).
% 30.96/31.29 cnf(c125,plain,~r1(X71,X70)|~r1(X70,X69)|r1(X71,X69),inference(split_conjunct,[status(thm)],[c124])).
% 30.96/31.29 cnf(c72,negated_conjecture,~r1(skolem0001,X139)|r1(X139,skolem0018(X139))|p102(X139)|~p101(X139),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c236,plain,p101(skolem0001)|r1(skolem0020(skolem0001),skolem0018(skolem0020(skolem0001)))|p102(skolem0020(skolem0001))|~p101(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c206, c72])).
% 30.96/31.29 cnf(c605,plain,p101(skolem0001)|r1(skolem0020(skolem0001),skolem0018(skolem0020(skolem0001)))|p102(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c236, c189])).
% 30.96/31.29 cnf(c606,plain,r1(skolem0020(skolem0001),skolem0018(skolem0020(skolem0001)))|p102(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c605, c121])).
% 30.96/31.29 cnf(c634,plain,p102(skolem0020(skolem0001))|~r1(X219,skolem0020(skolem0001))|r1(X219,skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c606, c125])).
% 30.96/31.29 cnf(c659,plain,p102(skolem0020(skolem0001))|r1(skolem0001,skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c634, c277])).
% 30.96/31.29 cnf(c661,plain,r1(skolem0001,skolem0018(skolem0020(skolem0001)))|~r1(skolem0001,skolem0001)|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c659, c82])).
% 30.96/31.29 cnf(c1318,plain,r1(skolem0001,skolem0018(skolem0020(skolem0001)))|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c661, c127])).
% 30.96/31.29 cnf(c1319,plain,r1(skolem0001,skolem0018(skolem0020(skolem0001)))|p101(skolem0001),inference(resolution,[status(thm)],[c1318, c122])).
% 30.96/31.29 cnf(c1404,plain,r1(skolem0001,skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c1319, c121])).
% 30.96/31.29 cnf(c70,negated_conjecture,~r1(skolem0001,X131)|~p104(skolem0017(X131))|p103(X131)|~p102(X131),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c71,negated_conjecture,~r1(skolem0001,X132)|p103(skolem0017(X132))|p103(X132)|~p102(X132),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c1480,plain,p103(skolem0017(skolem0018(skolem0020(skolem0001))))|p103(skolem0018(skolem0020(skolem0001)))|~p102(skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c1404, c71])).
% 30.96/31.29 cnf(c2711,plain,p103(skolem0017(skolem0018(skolem0020(skolem0001))))|p103(skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c1480, c595])).
% 30.96/31.29 cnf(c2715,plain,p103(skolem0017(skolem0018(skolem0020(skolem0001))))|~r1(skolem0001,skolem0020(skolem0001))|p102(skolem0020(skolem0001))|~p101(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c2711, c74])).
% 30.96/31.29 cnf(c3045,plain,p103(skolem0017(skolem0018(skolem0020(skolem0001))))|p102(skolem0020(skolem0001))|~p101(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c2715, c277])).
% 30.96/31.29 cnf(c3046,plain,p103(skolem0017(skolem0018(skolem0020(skolem0001))))|p102(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c3045, c189])).
% 30.96/31.29 cnf(c3052,plain,p103(skolem0017(skolem0018(skolem0020(skolem0001))))|~r1(skolem0001,skolem0001)|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c3046, c82])).
% 30.96/31.29 cnf(c3071,plain,p103(skolem0017(skolem0018(skolem0020(skolem0001))))|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c3052, c127])).
% 30.96/31.29 cnf(c3072,plain,p103(skolem0017(skolem0018(skolem0020(skolem0001))))|p101(skolem0001),inference(resolution,[status(thm)],[c3071, c122])).
% 30.96/31.29 cnf(c3073,plain,p103(skolem0017(skolem0018(skolem0020(skolem0001)))),inference(resolution,[status(thm)],[c3072, c121])).
% 30.96/31.29 cnf(c68,negated_conjecture,~r1(skolem0001,X135)|r1(X135,skolem0017(X135))|p103(X135)|~p102(X135),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c1448,plain,r1(skolem0018(skolem0020(skolem0001)),skolem0017(skolem0018(skolem0020(skolem0001))))|p103(skolem0018(skolem0020(skolem0001)))|~p102(skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c1404, c68])).
% 30.96/31.29 cnf(c3444,plain,r1(skolem0018(skolem0020(skolem0001)),skolem0017(skolem0018(skolem0020(skolem0001))))|p103(skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c1448, c595])).
% 30.96/31.29 cnf(c3446,plain,p103(skolem0018(skolem0020(skolem0001)))|~r1(X253,skolem0018(skolem0020(skolem0001)))|r1(X253,skolem0017(skolem0018(skolem0020(skolem0001)))),inference(resolution,[status(thm)],[c3444, c125])).
% 30.96/31.29 cnf(c3477,plain,p103(skolem0018(skolem0020(skolem0001)))|r1(skolem0001,skolem0017(skolem0018(skolem0020(skolem0001)))),inference(resolution,[status(thm)],[c3446, c1404])).
% 30.96/31.29 cnf(c3484,plain,r1(skolem0001,skolem0017(skolem0018(skolem0020(skolem0001))))|~r1(skolem0001,skolem0020(skolem0001))|p102(skolem0020(skolem0001))|~p101(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c3477, c74])).
% 30.96/31.29 cnf(c8847,plain,r1(skolem0001,skolem0017(skolem0018(skolem0020(skolem0001))))|p102(skolem0020(skolem0001))|~p101(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c3484, c277])).
% 30.96/31.29 cnf(c8848,plain,r1(skolem0001,skolem0017(skolem0018(skolem0020(skolem0001))))|p102(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c8847, c189])).
% 30.96/31.29 cnf(c8938,plain,r1(skolem0001,skolem0017(skolem0018(skolem0020(skolem0001))))|~r1(skolem0001,skolem0001)|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c8848, c82])).
% 30.96/31.29 cnf(c9125,plain,r1(skolem0001,skolem0017(skolem0018(skolem0020(skolem0001))))|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c8938, c127])).
% 30.96/31.29 cnf(c9126,plain,r1(skolem0001,skolem0017(skolem0018(skolem0020(skolem0001))))|p101(skolem0001),inference(resolution,[status(thm)],[c9125, c122])).
% 30.96/31.29 cnf(c9211,plain,r1(skolem0001,skolem0017(skolem0018(skolem0020(skolem0001)))),inference(resolution,[status(thm)],[c9126, c121])).
% 30.96/31.29 cnf(c57,negated_conjecture,~r1(skolem0001,X118)|~p5(skolem0014(X118))|p104(X118)|~p103(X118),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c7,negated_conjecture,~r1(skolem0001,X52)|p5(X52),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c56,negated_conjecture,~r1(skolem0001,X122)|r1(X122,skolem0014(X122))|p104(X122)|~p103(X122),inference(split_conjunct,[status(thm)],[c6])).
% 30.96/31.29 cnf(c9212,plain,r1(skolem0017(skolem0018(skolem0020(skolem0001))),skolem0014(skolem0017(skolem0018(skolem0020(skolem0001)))))|p104(skolem0017(skolem0018(skolem0020(skolem0001))))|~p103(skolem0017(skolem0018(skolem0020(skolem0001)))),inference(resolution,[status(thm)],[c9211, c56])).
% 30.96/31.29 cnf(c18944,plain,r1(skolem0017(skolem0018(skolem0020(skolem0001))),skolem0014(skolem0017(skolem0018(skolem0020(skolem0001)))))|p104(skolem0017(skolem0018(skolem0020(skolem0001)))),inference(resolution,[status(thm)],[c9212, c3073])).
% 30.96/31.29 cnf(c18946,plain,p104(skolem0017(skolem0018(skolem0020(skolem0001))))|~r1(X493,skolem0017(skolem0018(skolem0020(skolem0001))))|r1(X493,skolem0014(skolem0017(skolem0018(skolem0020(skolem0001))))),inference(resolution,[status(thm)],[c18944, c125])).
% 30.96/31.29 cnf(c18981,plain,p104(skolem0017(skolem0018(skolem0020(skolem0001))))|r1(skolem0001,skolem0014(skolem0017(skolem0018(skolem0020(skolem0001))))),inference(resolution,[status(thm)],[c18946, c9211])).
% 30.96/31.29 cnf(c19066,plain,p104(skolem0017(skolem0018(skolem0020(skolem0001))))|p5(skolem0014(skolem0017(skolem0018(skolem0020(skolem0001))))),inference(resolution,[status(thm)],[c18981, c7])).
% 30.96/31.29 cnf(c19092,plain,p104(skolem0017(skolem0018(skolem0020(skolem0001))))|~r1(skolem0001,skolem0017(skolem0018(skolem0020(skolem0001))))|~p103(skolem0017(skolem0018(skolem0020(skolem0001)))),inference(resolution,[status(thm)],[c19066, c57])).
% 30.96/31.29 cnf(c19164,plain,p104(skolem0017(skolem0018(skolem0020(skolem0001))))|~p103(skolem0017(skolem0018(skolem0020(skolem0001)))),inference(resolution,[status(thm)],[c19092, c9211])).
% 30.96/31.29 cnf(c19165,plain,p104(skolem0017(skolem0018(skolem0020(skolem0001)))),inference(resolution,[status(thm)],[c19164, c3073])).
% 30.96/31.29 cnf(c19168,plain,~r1(skolem0001,skolem0018(skolem0020(skolem0001)))|p103(skolem0018(skolem0020(skolem0001)))|~p102(skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c19165, c70])).
% 30.96/31.29 cnf(c19229,plain,p103(skolem0018(skolem0020(skolem0001)))|~p102(skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c19168, c1404])).
% 30.96/31.29 cnf(c19230,plain,p103(skolem0018(skolem0020(skolem0001))),inference(resolution,[status(thm)],[c19229, c595])).
% 30.96/31.29 cnf(c19238,plain,~r1(skolem0001,skolem0020(skolem0001))|p102(skolem0020(skolem0001))|~p101(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c19230, c74])).
% 30.96/31.29 cnf(c19255,plain,p102(skolem0020(skolem0001))|~p101(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c19238, c277])).
% 30.96/31.29 cnf(c19256,plain,p102(skolem0020(skolem0001)),inference(resolution,[status(thm)],[c19255, c189])).
% 30.96/31.29 cnf(c19264,plain,~r1(skolem0001,skolem0001)|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c19256, c82])).
% 30.96/31.29 cnf(c19285,plain,p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c19264, c127])).
% 30.96/31.29 cnf(c19286,plain,p101(skolem0001),inference(resolution,[status(thm)],[c19285, c122])).
% 30.96/31.29 cnf(c19287,plain,$false,inference(resolution,[status(thm)],[c19286, c121])).
% 30.96/31.29 % SZS output end CNFRefutation
% 30.96/31.29
% 30.96/31.29 % Initial clauses : 118
% 30.96/31.29 % Processed clauses : 3518
% 30.96/31.29 % Factors computed : 22
% 30.96/31.29 % Resolvents computed: 19138
% 30.96/31.29 % Tautologies deleted: 100
% 30.96/31.29 % Forward subsumed : 6712
% 30.96/31.29 % Backward subsumed : 2428
% 30.96/31.29 % -------- CPU Time ---------
% 30.96/31.29 % User time : 30.850 s
% 30.96/31.29 % System time : 0.094 s
% 30.96/31.29 % Total time : 30.944 s
%------------------------------------------------------------------------------