%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL637+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:58:46 PM UTC 2026
% Result : CounterSatisfiable 0.39s 0.66s
% Output : Saturation 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL637+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.37 % Computer : n014.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 5 01:18:12 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.43 (re.compile("\."), Token.FullStop),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.43 (re.compile("\("), Token.OpenPar),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.43 (re.compile("\)"), Token.ClosePar),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.43 (re.compile("\["), Token.OpenSquare),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("~\|"), Token.Nor),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("\|"), Token.Or),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.43 (re.compile("\?"), Token.Existential),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.50 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.32/0.59 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.59 """
% 0.39/0.66 % Version: 1.5
% 0.39/0.66 % SZS status CounterSatisfiable
% 0.39/0.66 % SZS output start Saturation
% 0.39/0.66 fof(main,conjecture,(~(?[X]:((((((((![Y]:((~r1(X,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))|(~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))))&(p101(Y)|(~p102(Y))))&(p100(Y)|(~p101(Y))))))&(((~(![Y]:((~r1(X,Y))|(~(((~p2(Y))&(~p102(Y)))&p101(Y))))))&(~(![Y]:((~r1(X,Y))|(~((p2(Y)&(~p102(Y)))&p101(Y)))))))|(~((~p101(X))&p100(X)))))&((((![Y]:(((~r1(X,Y))|(~p2(Y)))|(~p101(Y))))|p2(X))&((![Y]:(((~r1(X,Y))|p2(Y))|(~p101(Y))))|(~p2(X))))|(~p101(X))))&((((![Y]:(((~r1(X,Y))|(~p1(Y)))|(~p100(Y))))|p1(X))&((![Y]:(((~r1(X,Y))|p1(Y))|(~p100(Y))))|(~p1(X))))|(~p100(X))))&(p101(X)|(~p102(X))))&(p100(X)|(~p101(X))))&(~p101(X)))&p100(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 0.39/0.66 fof(c0,negated_conjecture,(~(~(?[X]:((((((((![Y]:((~r1(X,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))|(~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))))&(p101(Y)|(~p102(Y))))&(p100(Y)|(~p101(Y))))))&(((~(![Y]:((~r1(X,Y))|(~(((~p2(Y))&(~p102(Y)))&p101(Y))))))&(~(![Y]:((~r1(X,Y))|(~((p2(Y)&(~p102(Y)))&p101(Y)))))))|(~((~p101(X))&p100(X)))))&((((![Y]:(((~r1(X,Y))|(~p2(Y)))|(~p101(Y))))|p2(X))&((![Y]:(((~r1(X,Y))|p2(Y))|(~p101(Y))))|(~p2(X))))|(~p101(X))))&((((![Y]:(((~r1(X,Y))|(~p1(Y)))|(~p100(Y))))|p1(X))&((![Y]:(((~r1(X,Y))|p1(Y))|(~p100(Y))))|(~p1(X))))|(~p100(X))))&(p101(X)|(~p102(X))))&(p100(X)|(~p101(X))))&(~p101(X)))&p100(X))))),inference(assume_negation,[status(cth)],[main])).
% 0.39/0.66 fof(c1,negated_conjecture,(~(~(?[X]:((((((((![Y]:(~r1(X,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)|~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)))&(p101(Y)|~p102(Y)))&(p100(Y)|~p101(Y)))))&(((~(![Y]:(~r1(X,Y)|(~((~p2(Y)&~p102(Y))&p101(Y))))))&(~(![Y]:(~r1(X,Y)|(~((p2(Y)&~p102(Y))&p101(Y)))))))|(~(~p101(X)&p100(X)))))&((((![Y]:((~r1(X,Y)|~p2(Y))|~p101(Y)))|p2(X))&((![Y]:((~r1(X,Y)|p2(Y))|~p101(Y)))|~p2(X)))|~p101(X)))&((((![Y]:((~r1(X,Y)|~p1(Y))|~p100(Y)))|p1(X))&((![Y]:((~r1(X,Y)|p1(Y))|~p100(Y)))|~p1(X)))|~p100(X)))&(p101(X)|~p102(X)))&(p100(X)|~p101(X)))&~p101(X))&p100(X))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.39/0.66 fof(c2,negated_conjecture,(?[X]:((((((((![Y]:(~r1(X,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)|~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)))&(p101(Y)|~p102(Y)))&(p100(Y)|~p101(Y)))))&(((?[Y]:(r1(X,Y)&((~p2(Y)&~p102(Y))&p101(Y))))&(?[Y]:(r1(X,Y)&((p2(Y)&~p102(Y))&p101(Y)))))|(p101(X)|~p100(X))))&((((![Y]:((~r1(X,Y)|~p2(Y))|~p101(Y)))|p2(X))&((![Y]:((~r1(X,Y)|p2(Y))|~p101(Y)))|~p2(X)))|~p101(X)))&((((![Y]:((~r1(X,Y)|~p1(Y))|~p100(Y)))|p1(X))&((![Y]:((~r1(X,Y)|p1(Y))|~p100(Y)))|~p1(X)))|~p100(X)))&(p101(X)|~p102(X)))&(p100(X)|~p101(X)))&~p101(X))&p100(X))),inference(fof_nnf,[status(thm)],[c1])).
% 0.39/0.66 fof(c3,negated_conjecture,(?[X2]:((((((((![X3]:(~r1(X2,X3)|(((((((?[X4]:(r1(X3,X4)&((~p2(X4)&~p102(X4))&p101(X4))))&(?[X5]:(r1(X3,X5)&((p2(X5)&~p102(X5))&p101(X5)))))|(p101(X3)|~p100(X3)))&((((![X6]:((~r1(X3,X6)|~p2(X6))|~p101(X6)))|p2(X3))&((![X7]:((~r1(X3,X7)|p2(X7))|~p101(X7)))|~p2(X3)))|~p101(X3)))&((((![X8]:((~r1(X3,X8)|~p1(X8))|~p100(X8)))|p1(X3))&((![X9]:((~r1(X3,X9)|p1(X9))|~p100(X9)))|~p1(X3)))|~p100(X3)))&(p101(X3)|~p102(X3)))&(p100(X3)|~p101(X3)))))&(((?[X10]:(r1(X2,X10)&((~p2(X10)&~p102(X10))&p101(X10))))&(?[X11]:(r1(X2,X11)&((p2(X11)&~p102(X11))&p101(X11)))))|(p101(X2)|~p100(X2))))&((((![X12]:((~r1(X2,X12)|~p2(X12))|~p101(X12)))|p2(X2))&((![X13]:((~r1(X2,X13)|p2(X13))|~p101(X13)))|~p2(X2)))|~p101(X2)))&((((![X14]:((~r1(X2,X14)|~p1(X14))|~p100(X14)))|p1(X2))&((![X15]:((~r1(X2,X15)|p1(X15))|~p100(X15)))|~p1(X2)))|~p100(X2)))&(p101(X2)|~p102(X2)))&(p100(X2)|~p101(X2)))&~p101(X2))&p100(X2))),inference(variable_rename,[status(thm)],[c2])).
% 0.39/0.66 fof(c5,negated_conjecture,(![X3]:(![X6]:(![X7]:(![X8]:(![X9]:(![X12]:(![X13]:(![X14]:(![X15]:((((((((~r1(skolem0001,X3)|(((((((r1(X3,skolem0002(X3))&((~p2(skolem0002(X3))&~p102(skolem0002(X3)))&p101(skolem0002(X3))))&(r1(X3,skolem0003(X3))&((p2(skolem0003(X3))&~p102(skolem0003(X3)))&p101(skolem0003(X3)))))|(p101(X3)|~p100(X3)))&(((((~r1(X3,X6)|~p2(X6))|~p101(X6))|p2(X3))&(((~r1(X3,X7)|p2(X7))|~p101(X7))|~p2(X3)))|~p101(X3)))&(((((~r1(X3,X8)|~p1(X8))|~p100(X8))|p1(X3))&(((~r1(X3,X9)|p1(X9))|~p100(X9))|~p1(X3)))|~p100(X3)))&(p101(X3)|~p102(X3)))&(p100(X3)|~p101(X3))))&(((r1(skolem0001,skolem0004)&((~p2(skolem0004)&~p102(skolem0004))&p101(skolem0004)))&(r1(skolem0001,skolem0005)&((p2(skolem0005)&~p102(skolem0005))&p101(skolem0005))))|(p101(skolem0001)|~p100(skolem0001))))&(((((~r1(skolem0001,X12)|~p2(X12))|~p101(X12))|p2(skolem0001))&(((~r1(skolem0001,X13)|p2(X13))|~p101(X13))|~p2(skolem0001)))|~p101(skolem0001)))&(((((~r1(skolem0001,X14)|~p1(X14))|~p100(X14))|p1(skolem0001))&(((~r1(skolem0001,X15)|p1(X15))|~p100(X15))|~p1(skolem0001)))|~p100(skolem0001)))&(p101(skolem0001)|~p102(skolem0001)))&(p100(skolem0001)|~p101(skolem0001)))&~p101(skolem0001))&p100(skolem0001))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((((((((![X3]:(~r1(skolem0001,X3)|(((((((r1(X3,skolem0002(X3))&((~p2(skolem0002(X3))&~p102(skolem0002(X3)))&p101(skolem0002(X3))))&(r1(X3,skolem0003(X3))&((p2(skolem0003(X3))&~p102(skolem0003(X3)))&p101(skolem0003(X3)))))|(p101(X3)|~p100(X3)))&((((![X6]:((~r1(X3,X6)|~p2(X6))|~p101(X6)))|p2(X3))&((![X7]:((~r1(X3,X7)|p2(X7))|~p101(X7)))|~p2(X3)))|~p101(X3)))&((((![X8]:((~r1(X3,X8)|~p1(X8))|~p100(X8)))|p1(X3))&((![X9]:((~r1(X3,X9)|p1(X9))|~p100(X9)))|~p1(X3)))|~p100(X3)))&(p101(X3)|~p102(X3)))&(p100(X3)|~p101(X3)))))&(((r1(skolem0001,skolem0004)&((~p2(skolem0004)&~p102(skolem0004))&p101(skolem0004)))&(r1(skolem0001,skolem0005)&((p2(skolem0005)&~p102(skolem0005))&p101(skolem0005))))|(p101(skolem0001)|~p100(skolem0001))))&((((![X12]:((~r1(skolem0001,X12)|~p2(X12))|~p101(X12)))|p2(skolem0001))&((![X13]:((~r1(skolem0001,X13)|p2(X13))|~p101(X13)))|~p2(skolem0001)))|~p101(skolem0001)))&((((![X14]:((~r1(skolem0001,X14)|~p1(X14))|~p100(X14)))|p1(skolem0001))&((![X15]:((~r1(skolem0001,X15)|p1(X15))|~p100(X15)))|~p1(skolem0001)))|~p100(skolem0001)))&(p101(skolem0001)|~p102(skolem0001)))&(p100(skolem0001)|~p101(skolem0001)))&~p101(skolem0001))&p100(skolem0001)),inference(skolemize,[status(esa)],[c3])).])).
% 0.39/0.66 fof(c6,negated_conjecture,(![X3]:(![X6]:(![X7]:(![X8]:(![X9]:(![X12]:(![X13]:(![X14]:(![X15]:((((((((((((((~r1(skolem0001,X3)|(r1(X3,skolem0002(X3))|(p101(X3)|~p100(X3))))&(((~r1(skolem0001,X3)|(~p2(skolem0002(X3))|(p101(X3)|~p100(X3))))&(~r1(skolem0001,X3)|(~p102(skolem0002(X3))|(p101(X3)|~p100(X3)))))&(~r1(skolem0001,X3)|(p101(skolem0002(X3))|(p101(X3)|~p100(X3))))))&((~r1(skolem0001,X3)|(r1(X3,skolem0003(X3))|(p101(X3)|~p100(X3))))&(((~r1(skolem0001,X3)|(p2(skolem0003(X3))|(p101(X3)|~p100(X3))))&(~r1(skolem0001,X3)|(~p102(skolem0003(X3))|(p101(X3)|~p100(X3)))))&(~r1(skolem0001,X3)|(p101(skolem0003(X3))|(p101(X3)|~p100(X3)))))))&((~r1(skolem0001,X3)|((((~r1(X3,X6)|~p2(X6))|~p101(X6))|p2(X3))|~p101(X3)))&(~r1(skolem0001,X3)|((((~r1(X3,X7)|p2(X7))|~p101(X7))|~p2(X3))|~p101(X3)))))&((~r1(skolem0001,X3)|((((~r1(X3,X8)|~p1(X8))|~p100(X8))|p1(X3))|~p100(X3)))&(~r1(skolem0001,X3)|((((~r1(X3,X9)|p1(X9))|~p100(X9))|~p1(X3))|~p100(X3)))))&(~r1(skolem0001,X3)|(p101(X3)|~p102(X3))))&(~r1(skolem0001,X3)|(p100(X3)|~p101(X3))))&(((r1(skolem0001,skolem0004)|(p101(skolem0001)|~p100(skolem0001)))&(((~p2(skolem0004)|(p101(skolem0001)|~p100(skolem0001)))&(~p102(skolem0004)|(p101(skolem0001)|~p100(skolem0001))))&(p101(skolem0004)|(p101(skolem0001)|~p100(skolem0001)))))&((r1(skolem0001,skolem0005)|(p101(skolem0001)|~p100(skolem0001)))&(((p2(skolem0005)|(p101(skolem0001)|~p100(skolem0001)))&(~p102(skolem0005)|(p101(skolem0001)|~p100(skolem0001))))&(p101(skolem0005)|(p101(skolem0001)|~p100(skolem0001)))))))&(((((~r1(skolem0001,X12)|~p2(X12))|~p101(X12))|p2(skolem0001))|~p101(skolem0001))&((((~r1(skolem0001,X13)|p2(X13))|~p101(X13))|~p2(skolem0001))|~p101(skolem0001))))&(((((~r1(skolem0001,X14)|~p1(X14))|~p100(X14))|p1(skolem0001))|~p100(skolem0001))&((((~r1(skolem0001,X15)|p1(X15))|~p100(X15))|~p1(skolem0001))|~p100(skolem0001))))&(p101(skolem0001)|~p102(skolem0001)))&(p100(skolem0001)|~p101(skolem0001)))&~p101(skolem0001))&p100(skolem0001))))))))))),inference(distribute,[status(thm)],[c5])).
% 0.39/0.66 cnf(c36,negated_conjecture,p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c35,negated_conjecture,~p101(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c25,negated_conjecture,r1(skolem0001,skolem0005)|p101(skolem0001)|~p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c58,plain,r1(skolem0001,skolem0005)|p101(skolem0001),inference(resolution,[status(thm)],[c25, c36])).
% 0.39/0.66 cnf(c66,plain,r1(skolem0001,skolem0005),inference(resolution,[status(thm)],[c58, c35])).
% 0.39/0.66 cnf(c32,negated_conjecture,~r1(skolem0001,X37)|p1(X37)|~p100(X37)|~p1(skolem0001)|~p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c95,plain,p1(skolem0005)|~p100(skolem0005)|~p1(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c32, c66])).
% 0.39/0.66 cnf(c97,plain,p1(skolem0005)|~p100(skolem0005)|~p1(skolem0001),inference(resolution,[status(thm)],[c95, c36])).
% 0.39/0.66 cnf(c21,negated_conjecture,r1(skolem0001,skolem0004)|p101(skolem0001)|~p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c46,plain,r1(skolem0001,skolem0004)|p101(skolem0001),inference(resolution,[status(thm)],[c21, c36])).
% 0.39/0.66 cnf(c51,plain,r1(skolem0001,skolem0004),inference(resolution,[status(thm)],[c46, c35])).
% 0.39/0.66 cnf(c94,plain,p1(skolem0004)|~p100(skolem0004)|~p1(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c32, c51])).
% 0.39/0.66 cnf(c96,plain,p1(skolem0004)|~p100(skolem0004)|~p1(skolem0001),inference(resolution,[status(thm)],[c94, c36])).
% 0.39/0.66 cnf(c28,negated_conjecture,p101(skolem0005)|p101(skolem0001)|~p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c44,plain,p101(skolem0005)|p101(skolem0001),inference(resolution,[status(thm)],[c28, c36])).
% 0.39/0.66 cnf(c45,plain,p101(skolem0005),inference(resolution,[status(thm)],[c44, c35])).
% 0.39/0.66 cnf(c20,negated_conjecture,~r1(skolem0001,X18)|p100(X18)|~p101(X18),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c67,plain,p100(skolem0005)|~p101(skolem0005),inference(resolution,[status(thm)],[c66, c20])).
% 0.39/0.66 cnf(c73,plain,p100(skolem0005),inference(resolution,[status(thm)],[c67, c45])).
% 0.39/0.66 cnf(c31,negated_conjecture,~r1(skolem0001,X32)|~p1(X32)|~p100(X32)|p1(skolem0001)|~p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c83,plain,~p1(skolem0005)|~p100(skolem0005)|p1(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c31, c66])).
% 0.39/0.66 cnf(c89,plain,~p1(skolem0005)|~p100(skolem0005)|p1(skolem0001),inference(resolution,[status(thm)],[c83, c36])).
% 0.39/0.66 cnf(c90,plain,~p1(skolem0005)|p1(skolem0001),inference(resolution,[status(thm)],[c89, c73])).
% 0.39/0.66 cnf(c18,negated_conjecture,~r1(skolem0001,X35)|~r1(X35,X36)|p1(X36)|~p100(X36)|~p1(X35)|~p100(X35),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c24,negated_conjecture,p101(skolem0004)|p101(skolem0001)|~p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c39,plain,p101(skolem0004)|p101(skolem0001),inference(resolution,[status(thm)],[c24, c36])).
% 0.39/0.66 cnf(c40,plain,p101(skolem0004),inference(resolution,[status(thm)],[c39, c35])).
% 0.39/0.66 cnf(c53,plain,p100(skolem0004)|~p101(skolem0004),inference(resolution,[status(thm)],[c51, c20])).
% 0.39/0.66 cnf(c56,plain,p100(skolem0004),inference(resolution,[status(thm)],[c53, c40])).
% 0.39/0.66 cnf(c82,plain,~p1(skolem0004)|~p100(skolem0004)|p1(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c31, c51])).
% 0.39/0.66 cnf(c87,plain,~p1(skolem0004)|~p100(skolem0004)|p1(skolem0001),inference(resolution,[status(thm)],[c82, c36])).
% 0.39/0.66 cnf(c88,plain,~p1(skolem0004)|p1(skolem0001),inference(resolution,[status(thm)],[c87, c56])).
% 0.39/0.66 cnf(c17,negated_conjecture,~r1(skolem0001,X33)|~r1(X33,X34)|~p1(X34)|~p100(X34)|p1(X33)|~p100(X33),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c16,negated_conjecture,~r1(skolem0001,X28)|~r1(X28,X29)|p2(X29)|~p101(X29)|~p2(X28)|~p101(X28),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c15,negated_conjecture,~r1(skolem0001,X27)|~r1(X27,X26)|~p2(X26)|~p101(X26)|p2(X27)|~p101(X27),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c14,negated_conjecture,~r1(skolem0001,X25)|p101(skolem0003(X25))|p101(X25)|~p100(X25),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c13,negated_conjecture,~r1(skolem0001,X24)|~p102(skolem0003(X24))|p101(X24)|~p100(X24),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c12,negated_conjecture,~r1(skolem0001,X23)|p2(skolem0003(X23))|p101(X23)|~p100(X23),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c11,negated_conjecture,~r1(skolem0001,X22)|r1(X22,skolem0003(X22))|p101(X22)|~p100(X22),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c10,negated_conjecture,~r1(skolem0001,X21)|p101(skolem0002(X21))|p101(X21)|~p100(X21),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c27,negated_conjecture,~p102(skolem0005)|p101(skolem0001)|~p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c43,plain,~p102(skolem0005)|p101(skolem0001),inference(resolution,[status(thm)],[c27, c36])).
% 0.39/0.66 cnf(c26,negated_conjecture,p2(skolem0005)|p101(skolem0001)|~p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c41,plain,p2(skolem0005)|p101(skolem0001),inference(resolution,[status(thm)],[c26, c36])).
% 0.39/0.66 cnf(c42,plain,p2(skolem0005),inference(resolution,[status(thm)],[c41, c35])).
% 0.39/0.66 cnf(c9,negated_conjecture,~r1(skolem0001,X20)|~p102(skolem0002(X20))|p101(X20)|~p100(X20),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c8,negated_conjecture,~r1(skolem0001,X19)|~p2(skolem0002(X19))|p101(X19)|~p100(X19),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c23,negated_conjecture,~p102(skolem0004)|p101(skolem0001)|~p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c38,plain,~p102(skolem0004)|p101(skolem0001),inference(resolution,[status(thm)],[c23, c36])).
% 0.39/0.66 cnf(c22,negated_conjecture,~p2(skolem0004)|p101(skolem0001)|~p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c37,plain,~p2(skolem0004)|p101(skolem0001),inference(resolution,[status(thm)],[c22, c36])).
% 0.39/0.66 cnf(c7,negated_conjecture,~r1(skolem0001,X17)|r1(X17,skolem0002(X17))|p101(X17)|~p100(X17),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c19,negated_conjecture,~r1(skolem0001,X16)|p101(X16)|~p102(X16),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 cnf(c33,negated_conjecture,p101(skolem0001)|~p102(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.66 % SZS output end Saturation
% 0.39/0.66
% 0.39/0.66 % Initial clauses : 30
% 0.39/0.66 % Processed clauses : 54
% 0.39/0.66 % Factors computed : 4
% 0.39/0.66 % Resolvents computed: 57
% 0.39/0.66 % Tautologies deleted: 4
% 0.39/0.66 % Forward subsumed : 33
% 0.39/0.66 % Backward subsumed : 21
% 0.39/0.66 % -------- CPU Time ---------
% 0.39/0.66 % User time : 0.260 s
% 0.39/0.66 % System time : 0.028 s
% 0.39/0.66 % Total time : 0.288 s
%------------------------------------------------------------------------------