%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL641+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:47 PM UTC 2026
% Result : CounterSatisfiable 13.26s 13.53s
% Output : Saturation 13.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL641+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.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 6 00:04:05 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.43 (re.compile("\."), Token.FullStop),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.43 (re.compile("\("), Token.OpenPar),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.43 (re.compile("\)"), Token.ClosePar),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.43 (re.compile("\["), Token.OpenSquare),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("~\|"), Token.Nor),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("\|"), Token.Or),
% 0.09/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.43 (re.compile("\?"), Token.Existential),
% 0.09/0.43 /export/starexec/sandbox2/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/sandbox2/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.50 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.22/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.32/0.59 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.59 """
% 13.26/13.53 % Version: 1.5
% 13.26/13.53 % SZS status CounterSatisfiable
% 13.26/13.53 % SZS output start Saturation
% 13.26/13.53 fof(main,conjecture,(~(?[X]:(~((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|((((((((![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|p1(X))))|(~p1(Y))))|(![Y]:((~r1(X,Y))|p1(Y))))|(~p1(X)))|(![Y]:((~r1(X,Y))|(~(![X]:(((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))|(~p1(X))))))))|(~(![Y]:((((~r1(X,Y))|(![X]:((~r1(Y,X))|p1(X))))|(~p1(Y)))|(~(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|p1(X))))|(~p1(Y)))))|(~((![Y]:((~r1(X,Y))|p1(Y)))|(~p1(X)))))))))))&((((![Y]:((~r1(X,Y))|p1(Y)))|p1(X))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|p1(X)))))))|(~(![Y]:(((~r1(X,Y))|p1(Y))|(~(![X]:(((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))|(~p1(X))))))))))&(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))))|(~(![X]:((~r1(Y,X))|p1(X)))))))&((![Y]:((~r1(X,Y))|(![X]:(((~r1(Y,X))|p1(X))|(~(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|p1(X))))|(~p1(Y)))))))))|(~(![Y]:(((~r1(X,Y))|p1(Y))|(~(![X]:(((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))|(~p1(X)))))))))))))))|(~(~(![Y]:((~r1(X,Y))|(![X]:((((~r1(Y,X))|p1(X))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|p1(X)))))))|(~(![Y]:(((~r1(X,Y))|p1(Y))|(~(![X]:(((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))|(~p1(X)))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 13.26/13.53 fof(c0,negated_conjecture,(~(~(?[X]:(~((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|((((((((![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|p1(X))))|(~p1(Y))))|(![Y]:((~r1(X,Y))|p1(Y))))|(~p1(X)))|(![Y]:((~r1(X,Y))|(~(![X]:(((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))|(~p1(X))))))))|(~(![Y]:((((~r1(X,Y))|(![X]:((~r1(Y,X))|p1(X))))|(~p1(Y)))|(~(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|p1(X))))|(~p1(Y)))))|(~((![Y]:((~r1(X,Y))|p1(Y)))|(~p1(X)))))))))))&((((![Y]:((~r1(X,Y))|p1(Y)))|p1(X))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|p1(X)))))))|(~(![Y]:(((~r1(X,Y))|p1(Y))|(~(![X]:(((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))|(~p1(X))))))))))&(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))))|(~(![X]:((~r1(Y,X))|p1(X)))))))&((![Y]:((~r1(X,Y))|(![X]:(((~r1(Y,X))|p1(X))|(~(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|p1(X))))|(~p1(Y)))))))))|(~(![Y]:(((~r1(X,Y))|p1(Y))|(~(![X]:(((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))|(~p1(X)))))))))))))))|(~(~(![Y]:((~r1(X,Y))|(![X]:((((~r1(Y,X))|p1(X))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|p1(X)))))))|(~(![Y]:(((~r1(X,Y))|p1(Y))|(~(![X]:(((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))|(~p1(X))))))))))))))))))),inference(assume_negation,[status(cth)],[main])).
% 13.26/13.53 fof(c1,negated_conjecture,(~(~(?[X]:(~((~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|((((((((![Y]:((~r1(X,Y)|(![X]:(~r1(Y,X)|p1(X))))|~p1(Y)))|(![Y]:(~r1(X,Y)|p1(Y))))|~p1(X))|(![Y]:(~r1(X,Y)|(~(![X]:((~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y))))|~p1(X)))))))|(~(![Y]:(((~r1(X,Y)|(![X]:(~r1(Y,X)|p1(X))))|~p1(Y))|(~(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:(~r1(Y,X)|p1(X))))|~p1(Y))))|(~((![Y]:(~r1(X,Y)|p1(Y)))|~p1(X))))))))))&((((![Y]:(~r1(X,Y)|p1(Y)))|p1(X))|(![Y]:(~r1(X,Y)|(~(![X]:(~r1(Y,X)|p1(X)))))))|(~(![Y]:((~r1(X,Y)|p1(Y))|(~(![X]:((~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y))))|~p1(X)))))))))&(![Y]:((~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y))))))|(~(![X]:(~r1(Y,X)|p1(X)))))))&((![Y]:(~r1(X,Y)|(![X]:((~r1(Y,X)|p1(X))|(~(![Y]:((~r1(X,Y)|(![X]:(~r1(Y,X)|p1(X))))|~p1(Y))))))))|(~(![Y]:((~r1(X,Y)|p1(Y))|(~(![X]:((~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y))))|~p1(X))))))))))))))|(~(~(![Y]:(~r1(X,Y)|(![X]:(((~r1(Y,X)|p1(X))|(![Y]:(~r1(X,Y)|(~(![X]:(~r1(Y,X)|p1(X)))))))|(~(![Y]:((~r1(X,Y)|p1(Y))|(~(![X]:((~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y))))|~p1(X)))))))))))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 13.26/13.53 fof(c2,negated_conjecture,(?[X]:((![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|((((((((![Y]:((~r1(X,Y)|(![X]:(~r1(Y,X)|p1(X))))|~p1(Y)))|(![Y]:(~r1(X,Y)|p1(Y))))|~p1(X))|(![Y]:(~r1(X,Y)|(?[X]:((r1(Y,X)&(?[Y]:(r1(X,Y)&~p1(Y))))&p1(X))))))|(?[Y]:(((r1(X,Y)&(?[X]:(r1(Y,X)&~p1(X))))&p1(Y))&(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:(~r1(Y,X)|p1(X))))|~p1(Y))))|((?[Y]:(r1(X,Y)&~p1(Y)))&p1(X)))))))&((((![Y]:(~r1(X,Y)|p1(Y)))|p1(X))|(![Y]:(~r1(X,Y)|(?[X]:(r1(Y,X)&~p1(X))))))|(?[Y]:((r1(X,Y)&~p1(Y))&(![X]:((~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y))))|~p1(X)))))))&(![Y]:((~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y))))))|(?[X]:(r1(Y,X)&~p1(X))))))&((![Y]:(~r1(X,Y)|(![X]:((~r1(Y,X)|p1(X))|(?[Y]:((r1(X,Y)&(?[X]:(r1(Y,X)&~p1(X))))&p1(Y)))))))|(?[Y]:((r1(X,Y)&~p1(Y))&(![X]:((~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y))))|~p1(X)))))))))))&(?[Y]:(r1(X,Y)&(?[X]:(((r1(Y,X)&~p1(X))&(?[Y]:(r1(X,Y)&(![X]:(~r1(Y,X)|p1(X))))))&(![Y]:((~r1(X,Y)|p1(Y))|(?[X]:((r1(Y,X)&(?[Y]:(r1(X,Y)&~p1(Y))))&p1(X))))))))))),inference(fof_nnf,[status(thm)],[c1])).
% 13.26/13.53 fof(c3,negated_conjecture,(?[X2]:((![X3]:(~r1(X2,X3)|(![X4]:(~r1(X3,X4)|((((((((![X5]:((~r1(X4,X5)|(![X6]:(~r1(X5,X6)|p1(X6))))|~p1(X5)))|(![X7]:(~r1(X4,X7)|p1(X7))))|~p1(X4))|(![X8]:(~r1(X4,X8)|(?[X9]:((r1(X8,X9)&(?[X10]:(r1(X9,X10)&~p1(X10))))&p1(X9))))))|(?[X11]:(((r1(X4,X11)&(?[X12]:(r1(X11,X12)&~p1(X12))))&p1(X11))&(![X13]:((~r1(X11,X13)|(![X14]:((~r1(X13,X14)|(![X15]:(~r1(X14,X15)|p1(X15))))|~p1(X14))))|((?[X16]:(r1(X13,X16)&~p1(X16)))&p1(X13)))))))&((((![X17]:(~r1(X4,X17)|p1(X17)))|p1(X4))|(![X18]:(~r1(X4,X18)|(?[X19]:(r1(X18,X19)&~p1(X19))))))|(?[X20]:((r1(X4,X20)&~p1(X20))&(![X21]:((~r1(X20,X21)|(![X22]:(~r1(X21,X22)|p1(X22))))|~p1(X21)))))))&(![X23]:((~r1(X4,X23)|(![X24]:(~r1(X23,X24)|(![X25]:(~r1(X24,X25)|p1(X25))))))|(?[X26]:(r1(X23,X26)&~p1(X26))))))&((![X27]:(~r1(X4,X27)|(![X28]:((~r1(X27,X28)|p1(X28))|(?[X29]:((r1(X28,X29)&(?[X30]:(r1(X29,X30)&~p1(X30))))&p1(X29)))))))|(?[X31]:((r1(X4,X31)&~p1(X31))&(![X32]:((~r1(X31,X32)|(![X33]:(~r1(X32,X33)|p1(X33))))|~p1(X32)))))))))))&(?[X34]:(r1(X2,X34)&(?[X35]:(((r1(X34,X35)&~p1(X35))&(?[X36]:(r1(X35,X36)&(![X37]:(~r1(X36,X37)|p1(X37))))))&(![X38]:((~r1(X35,X38)|p1(X38))|(?[X39]:((r1(X38,X39)&(?[X40]:(r1(X39,X40)&~p1(X40))))&p1(X39))))))))))),inference(variable_rename,[status(thm)],[c2])).
% 13.26/13.53 fof(c5,negated_conjecture,(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X13]:(![X14]:(![X15]:(![X17]:(![X18]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X27]:(![X28]:(![X32]:(![X33]:(![X37]:(![X38]:((~r1(skolem0001,X3)|(~r1(X3,X4)|(((((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|((r1(X8,skolem0002(X3,X4,X8))&(r1(skolem0002(X3,X4,X8),skolem0003(X3,X4,X8))&~p1(skolem0003(X3,X4,X8))))&p1(skolem0002(X3,X4,X8)))))|(((r1(X4,skolem0004(X3,X4))&(r1(skolem0004(X3,X4),skolem0005(X3,X4))&~p1(skolem0005(X3,X4))))&p1(skolem0004(X3,X4)))&((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|((r1(X13,skolem0006(X3,X4,X13))&~p1(skolem0006(X3,X4,X13)))&p1(X13)))))&((((~r1(X4,X17)|p1(X17))|p1(X4))|(~r1(X4,X18)|(r1(X18,skolem0007(X3,X4,X18))&~p1(skolem0007(X3,X4,X18)))))|((r1(X4,skolem0008(X3,X4))&~p1(skolem0008(X3,X4)))&((~r1(skolem0008(X3,X4),X21)|(~r1(X21,X22)|p1(X22)))|~p1(X21)))))&((~r1(X4,X23)|(~r1(X23,X24)|(~r1(X24,X25)|p1(X25))))|(r1(X23,skolem0009(X3,X4,X23))&~p1(skolem0009(X3,X4,X23)))))&((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|((r1(X28,skolem0010(X3,X4,X27,X28))&(r1(skolem0010(X3,X4,X27,X28),skolem0011(X3,X4,X27,X28))&~p1(skolem0011(X3,X4,X27,X28))))&p1(skolem0010(X3,X4,X27,X28)))))|((r1(X4,skolem0012(X3,X4))&~p1(skolem0012(X3,X4)))&((~r1(skolem0012(X3,X4),X32)|(~r1(X32,X33)|p1(X33)))|~p1(X32)))))))&(r1(skolem0001,skolem0013)&(((r1(skolem0013,skolem0014)&~p1(skolem0014))&(r1(skolem0014,skolem0015)&(~r1(skolem0015,X37)|p1(X37))))&((~r1(skolem0014,X38)|p1(X38))|((r1(X38,skolem0016(X38))&(r1(skolem0016(X38),skolem0017(X38))&~p1(skolem0017(X38))))&p1(skolem0016(X38))))))))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((![X3]:(~r1(skolem0001,X3)|(![X4]:(~r1(X3,X4)|((((((((![X5]:((~r1(X4,X5)|(![X6]:(~r1(X5,X6)|p1(X6))))|~p1(X5)))|(![X7]:(~r1(X4,X7)|p1(X7))))|~p1(X4))|(![X8]:(~r1(X4,X8)|((r1(X8,skolem0002(X3,X4,X8))&(r1(skolem0002(X3,X4,X8),skolem0003(X3,X4,X8))&~p1(skolem0003(X3,X4,X8))))&p1(skolem0002(X3,X4,X8))))))|(((r1(X4,skolem0004(X3,X4))&(r1(skolem0004(X3,X4),skolem0005(X3,X4))&~p1(skolem0005(X3,X4))))&p1(skolem0004(X3,X4)))&(![X13]:((~r1(skolem0004(X3,X4),X13)|(![X14]:((~r1(X13,X14)|(![X15]:(~r1(X14,X15)|p1(X15))))|~p1(X14))))|((r1(X13,skolem0006(X3,X4,X13))&~p1(skolem0006(X3,X4,X13)))&p1(X13))))))&((((![X17]:(~r1(X4,X17)|p1(X17)))|p1(X4))|(![X18]:(~r1(X4,X18)|(r1(X18,skolem0007(X3,X4,X18))&~p1(skolem0007(X3,X4,X18))))))|((r1(X4,skolem0008(X3,X4))&~p1(skolem0008(X3,X4)))&(![X21]:((~r1(skolem0008(X3,X4),X21)|(![X22]:(~r1(X21,X22)|p1(X22))))|~p1(X21))))))&(![X23]:((~r1(X4,X23)|(![X24]:(~r1(X23,X24)|(![X25]:(~r1(X24,X25)|p1(X25))))))|(r1(X23,skolem0009(X3,X4,X23))&~p1(skolem0009(X3,X4,X23))))))&((![X27]:(~r1(X4,X27)|(![X28]:((~r1(X27,X28)|p1(X28))|((r1(X28,skolem0010(X3,X4,X27,X28))&(r1(skolem0010(X3,X4,X27,X28),skolem0011(X3,X4,X27,X28))&~p1(skolem0011(X3,X4,X27,X28))))&p1(skolem0010(X3,X4,X27,X28)))))))|((r1(X4,skolem0012(X3,X4))&~p1(skolem0012(X3,X4)))&(![X32]:((~r1(skolem0012(X3,X4),X32)|(![X33]:(~r1(X32,X33)|p1(X33))))|~p1(X32))))))))))&(r1(skolem0001,skolem0013)&(((r1(skolem0013,skolem0014)&~p1(skolem0014))&(r1(skolem0014,skolem0015)&(![X37]:(~r1(skolem0015,X37)|p1(X37)))))&(![X38]:((~r1(skolem0014,X38)|p1(X38))|((r1(X38,skolem0016(X38))&(r1(skolem0016(X38),skolem0017(X38))&~p1(skolem0017(X38))))&p1(skolem0016(X38)))))))),inference(skolemize,[status(esa)],[c3])).])).
% 13.26/13.53 fof(c6,negated_conjecture,(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X13]:(![X14]:(![X15]:(![X17]:(![X18]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X27]:(![X28]:(![X32]:(![X33]:(![X37]:(![X38]:((((((((((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(X8,skolem0002(X3,X4,X8))))|r1(X4,skolem0004(X3,X4)))))&((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(X8,skolem0002(X3,X4,X8))))|r1(skolem0004(X3,X4),skolem0005(X3,X4)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(X8,skolem0002(X3,X4,X8))))|~p1(skolem0005(X3,X4)))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(X8,skolem0002(X3,X4,X8))))|p1(skolem0004(X3,X4))))))&(((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(X8,skolem0002(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|r1(X13,skolem0006(X3,X4,X13))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(X8,skolem0002(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|~p1(skolem0006(X3,X4,X13)))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(X8,skolem0002(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|p1(X13)))))))&(((((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(skolem0002(X3,X4,X8),skolem0003(X3,X4,X8))))|r1(X4,skolem0004(X3,X4)))))&((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(skolem0002(X3,X4,X8),skolem0003(X3,X4,X8))))|r1(skolem0004(X3,X4),skolem0005(X3,X4)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(skolem0002(X3,X4,X8),skolem0003(X3,X4,X8))))|~p1(skolem0005(X3,X4)))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(skolem0002(X3,X4,X8),skolem0003(X3,X4,X8))))|p1(skolem0004(X3,X4))))))&(((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(skolem0002(X3,X4,X8),skolem0003(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|r1(X13,skolem0006(X3,X4,X13))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(skolem0002(X3,X4,X8),skolem0003(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|~p1(skolem0006(X3,X4,X13)))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|r1(skolem0002(X3,X4,X8),skolem0003(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|p1(X13)))))))&((((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|~p1(skolem0003(X3,X4,X8))))|r1(X4,skolem0004(X3,X4)))))&((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|~p1(skolem0003(X3,X4,X8))))|r1(skolem0004(X3,X4),skolem0005(X3,X4)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|~p1(skolem0003(X3,X4,X8))))|~p1(skolem0005(X3,X4)))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|~p1(skolem0003(X3,X4,X8))))|p1(skolem0004(X3,X4))))))&(((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|~p1(skolem0003(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|r1(X13,skolem0006(X3,X4,X13))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|~p1(skolem0003(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|~p1(skolem0006(X3,X4,X13)))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|~p1(skolem0003(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|p1(X13)))))))))&((((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|p1(skolem0002(X3,X4,X8))))|r1(X4,skolem0004(X3,X4)))))&((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|p1(skolem0002(X3,X4,X8))))|r1(skolem0004(X3,X4),skolem0005(X3,X4)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|p1(skolem0002(X3,X4,X8))))|~p1(skolem0005(X3,X4)))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|p1(skolem0002(X3,X4,X8))))|p1(skolem0004(X3,X4))))))&(((~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|p1(skolem0002(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|r1(X13,skolem0006(X3,X4,X13))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|p1(skolem0002(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|~p1(skolem0006(X3,X4,X13)))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((((~r1(X4,X5)|(~r1(X5,X6)|p1(X6)))|~p1(X5))|(~r1(X4,X7)|p1(X7)))|~p1(X4))|(~r1(X4,X8)|p1(skolem0002(X3,X4,X8))))|((~r1(skolem0004(X3,X4),X13)|((~r1(X13,X14)|(~r1(X14,X15)|p1(X15)))|~p1(X14)))|p1(X13))))))))&((((~r1(skolem0001,X3)|(~r1(X3,X4)|((((~r1(X4,X17)|p1(X17))|p1(X4))|(~r1(X4,X18)|r1(X18,skolem0007(X3,X4,X18))))|r1(X4,skolem0008(X3,X4)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((~r1(X4,X17)|p1(X17))|p1(X4))|(~r1(X4,X18)|r1(X18,skolem0007(X3,X4,X18))))|~p1(skolem0008(X3,X4))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((~r1(X4,X17)|p1(X17))|p1(X4))|(~r1(X4,X18)|r1(X18,skolem0007(X3,X4,X18))))|((~r1(skolem0008(X3,X4),X21)|(~r1(X21,X22)|p1(X22)))|~p1(X21))))))&(((~r1(skolem0001,X3)|(~r1(X3,X4)|((((~r1(X4,X17)|p1(X17))|p1(X4))|(~r1(X4,X18)|~p1(skolem0007(X3,X4,X18))))|r1(X4,skolem0008(X3,X4)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((~r1(X4,X17)|p1(X17))|p1(X4))|(~r1(X4,X18)|~p1(skolem0007(X3,X4,X18))))|~p1(skolem0008(X3,X4))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((((~r1(X4,X17)|p1(X17))|p1(X4))|(~r1(X4,X18)|~p1(skolem0007(X3,X4,X18))))|((~r1(skolem0008(X3,X4),X21)|(~r1(X21,X22)|p1(X22)))|~p1(X21))))))))&((~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X23)|(~r1(X23,X24)|(~r1(X24,X25)|p1(X25))))|r1(X23,skolem0009(X3,X4,X23)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X23)|(~r1(X23,X24)|(~r1(X24,X25)|p1(X25))))|~p1(skolem0009(X3,X4,X23)))))))&(((((~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|r1(X28,skolem0010(X3,X4,X27,X28))))|r1(X4,skolem0012(X3,X4)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|r1(X28,skolem0010(X3,X4,X27,X28))))|~p1(skolem0012(X3,X4))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|r1(X28,skolem0010(X3,X4,X27,X28))))|((~r1(skolem0012(X3,X4),X32)|(~r1(X32,X33)|p1(X33)))|~p1(X32))))))&((((~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|r1(skolem0010(X3,X4,X27,X28),skolem0011(X3,X4,X27,X28))))|r1(X4,skolem0012(X3,X4)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|r1(skolem0010(X3,X4,X27,X28),skolem0011(X3,X4,X27,X28))))|~p1(skolem0012(X3,X4))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|r1(skolem0010(X3,X4,X27,X28),skolem0011(X3,X4,X27,X28))))|((~r1(skolem0012(X3,X4),X32)|(~r1(X32,X33)|p1(X33)))|~p1(X32))))))&(((~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|~p1(skolem0011(X3,X4,X27,X28))))|r1(X4,skolem0012(X3,X4)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|~p1(skolem0011(X3,X4,X27,X28))))|~p1(skolem0012(X3,X4))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|~p1(skolem0011(X3,X4,X27,X28))))|((~r1(skolem0012(X3,X4),X32)|(~r1(X32,X33)|p1(X33)))|~p1(X32))))))))&(((~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|p1(skolem0010(X3,X4,X27,X28))))|r1(X4,skolem0012(X3,X4)))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|p1(skolem0010(X3,X4,X27,X28))))|~p1(skolem0012(X3,X4))))))&(~r1(skolem0001,X3)|(~r1(X3,X4)|((~r1(X4,X27)|((~r1(X27,X28)|p1(X28))|p1(skolem0010(X3,X4,X27,X28))))|((~r1(skolem0012(X3,X4),X32)|(~r1(X32,X33)|p1(X33)))|~p1(X32))))))))&(r1(skolem0001,skolem0013)&(((r1(skolem0013,skolem0014)&~p1(skolem0014))&(r1(skolem0014,skolem0015)&(~r1(skolem0015,X37)|p1(X37))))&((((~r1(skolem0014,X38)|p1(X38))|r1(X38,skolem0016(X38)))&(((~r1(skolem0014,X38)|p1(X38))|r1(skolem0016(X38),skolem0017(X38)))&((~r1(skolem0014,X38)|p1(X38))|~p1(skolem0017(X38)))))&((~r1(skolem0014,X38)|p1(X38))|p1(skolem0016(X38))))))))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 13.26/13.54 cnf(c19,negated_conjecture,~r1(skolem0001,X189)|~r1(X189,X195)|~r1(X195,X192)|~r1(X192,X196)|p1(X196)|~p1(X192)|~r1(X195,X193)|p1(X193)|~p1(X195)|~r1(X195,X197)|r1(skolem0002(X189,X195,X197),skolem0003(X189,X195,X197))|~r1(skolem0004(X189,X195),X190)|~r1(X190,X191)|~r1(X191,X194)|p1(X194)|~p1(X191)|~p1(skolem0006(X189,X195,X190)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c212,plain,~r1(skolem0001,X1293)|~r1(X1293,X1292)|~r1(X1292,skolem0006(X1293,X1292,X1294))|~r1(skolem0006(X1293,X1292,X1294),X1296)|p1(X1296)|~p1(skolem0006(X1293,X1292,X1294))|~r1(X1292,X1290)|p1(X1290)|~p1(X1292)|~r1(X1292,X1297)|r1(skolem0002(X1293,X1292,X1297),skolem0003(X1293,X1292,X1297))|~r1(skolem0004(X1293,X1292),X1294)|~r1(X1294,X1291)|~r1(X1291,X1295)|p1(X1295)|~p1(X1291),inference(factor,[status(thm)],[c19])).
% 13.26/13.54 cnf(c1061,plain,~r1(skolem0001,X3370)|~r1(X3370,X3367)|~r1(X3367,skolem0006(X3370,X3367,X3372))|~r1(skolem0006(X3370,X3367,X3372),X3369)|p1(X3369)|~p1(skolem0006(X3370,X3367,X3372))|~r1(X3367,X3371)|p1(X3371)|~p1(X3367)|~r1(X3367,X3368)|r1(skolem0002(X3370,X3367,X3368),skolem0003(X3370,X3367,X3368))|~r1(skolem0004(X3370,X3367),X3372)|~r1(X3372,skolem0006(X3370,X3367,X3372)),inference(factor,[status(thm)],[c212])).
% 13.26/13.54 cnf(c1820,plain,~r1(skolem0001,X3383)|~r1(X3383,X3385)|~r1(X3385,skolem0006(X3383,X3385,X3385))|~r1(skolem0006(X3383,X3385,X3385),X3382)|p1(X3382)|~p1(skolem0006(X3383,X3385,X3385))|~r1(X3385,X3384)|p1(X3384)|~p1(X3385)|r1(skolem0002(X3383,X3385,skolem0006(X3383,X3385,X3385)),skolem0003(X3383,X3385,skolem0006(X3383,X3385,X3385)))|~r1(skolem0004(X3383,X3385),X3385),inference(factor,[status(thm)],[c1061])).
% 13.26/13.54 cnf(c1818,plain,~r1(skolem0001,X3376)|~r1(X3376,X3374)|~r1(X3374,skolem0006(X3376,X3374,X3374))|~r1(skolem0006(X3376,X3374,X3374),X3375)|p1(X3375)|~p1(skolem0006(X3376,X3374,X3374))|~r1(X3374,X3377)|p1(X3377)|~p1(X3374)|~r1(X3374,X3373)|r1(skolem0002(X3376,X3374,X3373),skolem0003(X3376,X3374,X3373))|~r1(skolem0004(X3376,X3374),X3374),inference(factor,[status(thm)],[c1061])).
% 13.26/13.54 cnf(c27,negated_conjecture,~r1(skolem0001,X294)|~r1(X294,X300)|~r1(X300,X297)|~r1(X297,X301)|p1(X301)|~p1(X297)|~r1(X300,X298)|p1(X298)|~p1(X300)|~r1(X300,X302)|~p1(skolem0003(X294,X300,X302))|~r1(skolem0004(X294,X300),X295)|~r1(X295,X296)|~r1(X296,X299)|p1(X299)|~p1(X296)|p1(X295),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c259,plain,~r1(skolem0001,X1477)|~r1(X1477,X1478)|~r1(X1478,skolem0004(X1477,X1478))|~r1(skolem0004(X1477,X1478),X1479)|p1(X1479)|~p1(skolem0004(X1477,X1478))|~r1(X1478,X1481)|p1(X1481)|~p1(X1478)|~r1(X1478,X1482)|~p1(skolem0003(X1477,X1478,X1482))|~r1(X1479,X1483)|~r1(X1483,X1480)|p1(X1480)|~p1(X1483),inference(factor,[status(thm)],[c27])).
% 13.26/13.54 cnf(c1125,plain,~r1(skolem0001,X3318)|~r1(X3318,X3321)|~r1(X3321,skolem0004(X3318,X3321))|~r1(skolem0004(X3318,X3321),X3317)|p1(X3317)|~p1(skolem0004(X3318,X3321))|~r1(X3321,X3319)|p1(X3319)|~p1(X3321)|~r1(X3321,X3320)|~p1(skolem0003(X3318,X3321,X3320))|~r1(X3317,skolem0003(X3318,X3321,X3320))|~r1(skolem0003(X3318,X3321,X3320),X3316)|p1(X3316),inference(factor,[status(thm)],[c259])).
% 13.26/13.54 cnf(c33,negated_conjecture,~r1(skolem0001,X376)|~r1(X376,X382)|~r1(X382,X379)|~r1(X379,X383)|p1(X383)|~p1(X379)|~r1(X382,X380)|p1(X380)|~p1(X382)|~r1(X382,X384)|p1(skolem0002(X376,X382,X384))|~r1(skolem0004(X376,X382),X377)|~r1(X377,X378)|~r1(X378,X381)|p1(X381)|~p1(X378)|~p1(skolem0006(X376,X382,X377)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c331,plain,~r1(skolem0001,X1814)|~r1(X1814,X1810)|~r1(X1810,skolem0006(X1814,X1810,X1812))|~r1(skolem0006(X1814,X1810,X1812),X1811)|p1(X1811)|~p1(skolem0006(X1814,X1810,X1812))|~r1(X1810,X1813)|p1(X1813)|~p1(X1810)|~r1(X1810,X1815)|p1(skolem0002(X1814,X1810,X1815))|~r1(skolem0004(X1814,X1810),X1812)|~r1(X1812,X1808)|~r1(X1808,X1809)|p1(X1809)|~p1(X1808),inference(factor,[status(thm)],[c33])).
% 13.26/13.54 cnf(c1308,plain,~r1(skolem0001,X3289)|~r1(X3289,X3290)|~r1(X3290,skolem0006(X3289,X3290,X3286))|~r1(skolem0006(X3289,X3290,X3286),X3288)|p1(X3288)|~p1(skolem0006(X3289,X3290,X3286))|~r1(X3290,X3287)|p1(X3287)|~p1(X3290)|~r1(X3290,X3291)|p1(skolem0002(X3289,X3290,X3291))|~r1(skolem0004(X3289,X3290),X3286)|~r1(X3286,skolem0006(X3289,X3290,X3286)),inference(factor,[status(thm)],[c331])).
% 13.26/13.54 cnf(c1816,plain,~r1(skolem0001,X3303)|~r1(X3303,X3304)|~r1(X3304,skolem0006(X3303,X3304,X3304))|~r1(skolem0006(X3303,X3304,X3304),X3301)|p1(X3301)|~p1(skolem0006(X3303,X3304,X3304))|~r1(X3304,X3302)|p1(X3302)|~p1(X3304)|p1(skolem0002(X3303,X3304,skolem0006(X3303,X3304,X3304)))|~r1(skolem0004(X3303,X3304),X3304),inference(factor,[status(thm)],[c1308])).
% 13.26/13.54 cnf(c1814,plain,~r1(skolem0001,X3293)|~r1(X3293,X3296)|~r1(X3296,skolem0006(X3293,X3296,X3296))|~r1(skolem0006(X3293,X3296,X3296),X3294)|p1(X3294)|~p1(skolem0006(X3293,X3296,X3296))|~r1(X3296,X3295)|p1(X3295)|~p1(X3296)|~r1(X3296,X3292)|p1(skolem0002(X3293,X3296,X3292))|~r1(skolem0004(X3293,X3296),X3296),inference(factor,[status(thm)],[c1308])).
% 13.26/13.54 cnf(c26,negated_conjecture,~r1(skolem0001,X280)|~r1(X280,X286)|~r1(X286,X283)|~r1(X283,X287)|p1(X287)|~p1(X283)|~r1(X286,X284)|p1(X284)|~p1(X286)|~r1(X286,X288)|~p1(skolem0003(X280,X286,X288))|~r1(skolem0004(X280,X286),X281)|~r1(X281,X282)|~r1(X282,X285)|p1(X285)|~p1(X282)|~p1(skolem0006(X280,X286,X281)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c251,plain,~r1(skolem0001,X1448)|~r1(X1448,X1446)|~r1(X1446,skolem0006(X1448,X1446,X1452))|~r1(skolem0006(X1448,X1446,X1452),X1445)|p1(X1445)|~p1(skolem0006(X1448,X1446,X1452))|~r1(X1446,X1451)|p1(X1451)|~p1(X1446)|~r1(X1446,X1450)|~p1(skolem0003(X1448,X1446,X1450))|~r1(skolem0004(X1448,X1446),X1452)|~r1(X1452,X1449)|~r1(X1449,X1447)|p1(X1447)|~p1(X1449),inference(factor,[status(thm)],[c26])).
% 13.26/13.54 cnf(c1117,plain,~r1(skolem0001,X3251)|~r1(X3251,X3256)|~r1(X3256,skolem0006(X3251,X3256,X3254))|~r1(skolem0006(X3251,X3256,X3254),X3253)|p1(X3253)|~p1(skolem0006(X3251,X3256,X3254))|~r1(X3256,X3252)|p1(X3252)|~p1(X3256)|~r1(X3256,X3255)|~p1(skolem0003(X3251,X3256,X3255))|~r1(skolem0004(X3251,X3256),X3254)|~r1(X3254,skolem0006(X3251,X3256,X3254)),inference(factor,[status(thm)],[c251])).
% 13.26/13.54 cnf(c1813,plain,~r1(skolem0001,X3269)|~r1(X3269,X3266)|~r1(X3266,skolem0006(X3269,X3266,X3266))|~r1(skolem0006(X3269,X3266,X3266),X3267)|p1(X3267)|~p1(skolem0006(X3269,X3266,X3266))|~r1(X3266,X3268)|p1(X3268)|~p1(X3266)|~p1(skolem0003(X3269,X3266,skolem0006(X3269,X3266,X3266)))|~r1(skolem0004(X3269,X3266),X3266),inference(factor,[status(thm)],[c1117])).
% 13.26/13.54 cnf(c1811,plain,~r1(skolem0001,X3258)|~r1(X3258,X3260)|~r1(X3260,skolem0006(X3258,X3260,X3260))|~r1(skolem0006(X3258,X3260,X3260),X3261)|p1(X3261)|~p1(skolem0006(X3258,X3260,X3260))|~r1(X3260,X3259)|p1(X3259)|~p1(X3260)|~r1(X3260,X3257)|~p1(skolem0003(X3258,X3260,X3257))|~r1(skolem0004(X3258,X3260),X3260),inference(factor,[status(thm)],[c1117])).
% 13.26/13.54 cnf(c12,negated_conjecture,~r1(skolem0001,X106)|~r1(X106,X112)|~r1(X112,X109)|~r1(X109,X113)|p1(X113)|~p1(X109)|~r1(X112,X110)|p1(X110)|~p1(X112)|~r1(X112,X114)|r1(X114,skolem0002(X106,X112,X114))|~r1(skolem0004(X106,X112),X107)|~r1(X107,X108)|~r1(X108,X111)|p1(X111)|~p1(X108)|~p1(skolem0006(X106,X112,X107)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c140,plain,~r1(skolem0001,X829)|~r1(X829,X828)|~r1(X828,skolem0006(X829,X828,X827))|~r1(skolem0006(X829,X828,X827),X822)|p1(X822)|~p1(skolem0006(X829,X828,X827))|~r1(X828,X823)|p1(X823)|~p1(X828)|~r1(X828,X824)|r1(X824,skolem0002(X829,X828,X824))|~r1(skolem0004(X829,X828),X827)|~r1(X827,X825)|~r1(X825,X826)|p1(X826)|~p1(X825),inference(factor,[status(thm)],[c12])).
% 13.26/13.54 cnf(c728,plain,~r1(skolem0001,X2674)|~r1(X2674,X2676)|~r1(X2676,skolem0006(X2674,X2676,X2675))|~r1(skolem0006(X2674,X2676,X2675),X2678)|p1(X2678)|~p1(skolem0006(X2674,X2676,X2675))|~r1(X2676,X2677)|p1(X2677)|~p1(X2676)|~r1(X2676,X2673)|r1(X2673,skolem0002(X2674,X2676,X2673))|~r1(skolem0004(X2674,X2676),X2675)|~r1(X2675,skolem0006(X2674,X2676,X2675)),inference(factor,[status(thm)],[c140])).
% 13.26/13.54 cnf(c1660,plain,~r1(skolem0001,X3212)|~r1(X3212,X3211)|~r1(X3211,skolem0006(X3212,X3211,X3211))|~r1(skolem0006(X3212,X3211,X3211),X3214)|p1(X3214)|~p1(skolem0006(X3212,X3211,X3211))|~r1(X3211,X3213)|p1(X3213)|~p1(X3211)|r1(skolem0006(X3212,X3211,X3211),skolem0002(X3212,X3211,skolem0006(X3212,X3211,X3211)))|~r1(skolem0004(X3212,X3211),X3211),inference(factor,[status(thm)],[c728])).
% 13.26/13.54 cnf(c20,negated_conjecture,~r1(skolem0001,X201)|~r1(X201,X207)|~r1(X207,X204)|~r1(X204,X208)|p1(X208)|~p1(X204)|~r1(X207,X205)|p1(X205)|~p1(X207)|~r1(X207,X209)|r1(skolem0002(X201,X207,X209),skolem0003(X201,X207,X209))|~r1(skolem0004(X201,X207),X202)|~r1(X202,X203)|~r1(X203,X206)|p1(X206)|~p1(X203)|p1(X202),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c214,plain,~r1(skolem0001,X1326)|~r1(X1326,X1320)|~r1(X1320,skolem0004(X1326,X1320))|~r1(skolem0004(X1326,X1320),X1323)|p1(X1323)|~p1(skolem0004(X1326,X1320))|~r1(X1320,X1322)|p1(X1322)|~p1(X1320)|~r1(X1320,X1325)|r1(skolem0002(X1326,X1320,X1325),skolem0003(X1326,X1320,X1325))|~r1(X1323,X1324)|~r1(X1324,X1321)|p1(X1321)|~p1(X1324),inference(factor,[status(thm)],[c20])).
% 13.26/13.54 cnf(c1068,plain,~r1(skolem0001,X3126)|~r1(X3126,X3128)|~r1(X3128,skolem0004(X3126,X3128))|~r1(skolem0004(X3126,X3128),X3127)|p1(X3127)|~p1(skolem0004(X3126,X3128))|~r1(X3128,X3124)|p1(X3124)|~p1(X3128)|~r1(X3128,X3125)|r1(skolem0002(X3126,X3128,X3125),skolem0003(X3126,X3128,X3125))|~r1(X3127,skolem0004(X3126,X3128)),inference(factor,[status(thm)],[c214])).
% 13.26/13.54 cnf(c1658,plain,~r1(skolem0001,X3118)|~r1(X3118,X3117)|~r1(X3117,skolem0006(X3118,X3117,X3117))|~r1(skolem0006(X3118,X3117,X3117),X3116)|p1(X3116)|~p1(skolem0006(X3118,X3117,X3117))|~r1(X3117,X3115)|p1(X3115)|~p1(X3117)|~r1(X3117,X3119)|r1(X3119,skolem0002(X3118,X3117,X3119))|~r1(skolem0004(X3118,X3117),X3117),inference(factor,[status(thm)],[c728])).
% 13.26/13.54 cnf(c34,negated_conjecture,~r1(skolem0001,X392)|~r1(X392,X398)|~r1(X398,X395)|~r1(X395,X399)|p1(X399)|~p1(X395)|~r1(X398,X396)|p1(X396)|~p1(X398)|~r1(X398,X400)|p1(skolem0002(X392,X398,X400))|~r1(skolem0004(X392,X398),X393)|~r1(X393,X394)|~r1(X394,X397)|p1(X397)|~p1(X394)|p1(X393),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c349,plain,~r1(skolem0001,X1853)|~r1(X1853,X1851)|~r1(X1851,skolem0004(X1853,X1851))|~r1(skolem0004(X1853,X1851),X1850)|p1(X1850)|~p1(skolem0004(X1853,X1851))|~r1(X1851,X1848)|p1(X1848)|~p1(X1851)|~r1(X1851,X1847)|p1(skolem0002(X1853,X1851,X1847))|~r1(X1850,X1849)|~r1(X1849,X1852)|p1(X1852)|~p1(X1849),inference(factor,[status(thm)],[c34])).
% 13.26/13.54 cnf(c1328,plain,~r1(skolem0001,X3051)|~r1(X3051,X3053)|~r1(X3053,skolem0004(X3051,X3053))|~r1(skolem0004(X3051,X3053),X3052)|p1(X3052)|~p1(skolem0004(X3051,X3053))|~r1(X3053,X3050)|p1(X3050)|~p1(X3053)|~r1(X3053,X3054)|p1(skolem0002(X3051,X3053,X3054))|~r1(X3052,skolem0004(X3051,X3053)),inference(factor,[status(thm)],[c349])).
% 13.26/13.54 cnf(c55,negated_conjecture,r1(skolem0001,skolem0013),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c15,negated_conjecture,~r1(skolem0001,X147)|~r1(X147,X150)|~r1(X150,X148)|~r1(X148,X151)|p1(X151)|~p1(X148)|~r1(X150,X149)|p1(X149)|~p1(X150)|~r1(X150,X152)|r1(skolem0002(X147,X150,X152),skolem0003(X147,X150,X152))|r1(skolem0004(X147,X150),skolem0005(X147,X150)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c178,plain,~r1(skolem0001,X1082)|~r1(X1082,skolem0001)|~r1(skolem0001,X1081)|~r1(X1081,X1080)|p1(X1080)|~p1(X1081)|~r1(skolem0001,X1079)|p1(X1079)|~p1(skolem0001)|r1(skolem0002(X1082,skolem0001,skolem0013),skolem0003(X1082,skolem0001,skolem0013))|r1(skolem0004(X1082,skolem0001),skolem0005(X1082,skolem0001)),inference(resolution,[status(thm)],[c15, c55])).
% 13.26/13.54 cnf(c938,plain,~r1(skolem0001,X3033)|~r1(X3033,skolem0001)|~r1(skolem0001,X3035)|~r1(X3035,X3034)|p1(X3034)|~p1(X3035)|p1(X3033)|~p1(skolem0001)|r1(skolem0002(X3033,skolem0001,skolem0013),skolem0003(X3033,skolem0001,skolem0013))|r1(skolem0004(X3033,skolem0001),skolem0005(X3033,skolem0001)),inference(factor,[status(thm)],[c178])).
% 13.26/13.54 cnf(c56,negated_conjecture,r1(skolem0013,skolem0014),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c175,plain,~r1(skolem0001,X1053)|~r1(X1053,X1049)|~r1(X1049,X1052)|~r1(X1052,X1050)|p1(X1050)|~p1(X1052)|~r1(X1049,X1051)|p1(X1051)|~p1(X1049)|r1(skolem0002(X1053,X1049,X1051),skolem0003(X1053,X1049,X1051))|r1(skolem0004(X1053,X1049),skolem0005(X1053,X1049)),inference(factor,[status(thm)],[c15])).
% 13.26/13.54 cnf(c913,plain,~r1(skolem0001,X3003)|~r1(X3003,skolem0013)|~r1(skolem0013,X3001)|~r1(X3001,X3002)|p1(X3002)|~p1(X3001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X3003,skolem0013,skolem0014),skolem0003(X3003,skolem0013,skolem0014))|r1(skolem0004(X3003,skolem0013),skolem0005(X3003,skolem0013)),inference(resolution,[status(thm)],[c175, c56])).
% 13.26/13.54 cnf(c1782,plain,~r1(skolem0001,X3029)|~r1(X3029,skolem0013)|~r1(skolem0013,skolem0001)|p1(X3029)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X3029,skolem0013,skolem0014),skolem0003(X3029,skolem0013,skolem0014))|r1(skolem0004(X3029,skolem0013),skolem0005(X3029,skolem0013)),inference(factor,[status(thm)],[c913])).
% 13.26/13.54 cnf(c173,plain,~r1(skolem0001,X1023)|~r1(X1023,X1019)|~r1(X1019,X1022)|~r1(X1022,X1021)|p1(X1021)|~p1(X1022)|~r1(X1019,X1020)|p1(X1020)|~p1(X1019)|r1(skolem0002(X1023,X1019,X1022),skolem0003(X1023,X1019,X1022))|r1(skolem0004(X1023,X1019),skolem0005(X1023,X1019)),inference(factor,[status(thm)],[c15])).
% 13.26/13.54 cnf(c887,plain,~r1(skolem0001,X2985)|~r1(X2985,skolem0013)|~r1(skolem0013,X2983)|~r1(X2983,X2984)|p1(X2984)|~p1(X2983)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2985,skolem0013,X2983),skolem0003(X2985,skolem0013,X2983))|r1(skolem0004(X2985,skolem0013),skolem0005(X2985,skolem0013)),inference(resolution,[status(thm)],[c173, c56])).
% 13.26/13.54 cnf(c1770,plain,~r1(skolem0001,X3026)|~r1(X3026,skolem0013)|~r1(skolem0013,skolem0001)|p1(X3026)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X3026,skolem0013,skolem0001),skolem0003(X3026,skolem0013,skolem0001))|r1(skolem0004(X3026,skolem0013),skolem0005(X3026,skolem0013)),inference(factor,[status(thm)],[c887])).
% 13.26/13.54 cnf(c883,plain,~r1(skolem0001,X2961)|~r1(X2961,skolem0001)|~r1(skolem0001,X2959)|~r1(X2959,X2960)|p1(X2960)|~p1(X2959)|p1(X2961)|~p1(skolem0001)|r1(skolem0002(X2961,skolem0001,X2959),skolem0003(X2961,skolem0001,X2959))|r1(skolem0004(X2961,skolem0001),skolem0005(X2961,skolem0001)),inference(factor,[status(thm)],[c173])).
% 13.26/13.54 cnf(c1767,plain,~r1(skolem0001,X3023)|~r1(X3023,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X3023)|~p1(skolem0001)|r1(skolem0002(X3023,skolem0001,skolem0013),skolem0003(X3023,skolem0001,skolem0013))|r1(skolem0004(X3023,skolem0001),skolem0005(X3023,skolem0001)),inference(resolution,[status(thm)],[c883, c56])).
% 13.26/13.54 cnf(c1795,plain,~r1(skolem0001,X3024)|~r1(X3024,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X3024)|~p1(skolem0001)|r1(skolem0002(X3024,skolem0001,skolem0013),skolem0003(X3024,skolem0001,skolem0013))|r1(skolem0004(X3024,skolem0001),skolem0005(X3024,skolem0001)),inference(resolution,[status(thm)],[c1767, c55])).
% 13.26/13.54 cnf(c914,plain,~r1(skolem0001,X3013)|~r1(X3013,skolem0001)|~r1(skolem0001,X3011)|~r1(X3011,X3012)|p1(X3012)|~p1(X3011)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X3013,skolem0001,skolem0013),skolem0003(X3013,skolem0001,skolem0013))|r1(skolem0004(X3013,skolem0001),skolem0005(X3013,skolem0001)),inference(resolution,[status(thm)],[c175, c55])).
% 13.26/13.54 cnf(c888,plain,~r1(skolem0001,X2991)|~r1(X2991,skolem0001)|~r1(skolem0001,X2989)|~r1(X2989,X2990)|p1(X2990)|~p1(X2989)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2991,skolem0001,X2989),skolem0003(X2991,skolem0001,X2989))|r1(skolem0004(X2991,skolem0001),skolem0005(X2991,skolem0001)),inference(resolution,[status(thm)],[c173, c55])).
% 13.26/13.54 cnf(c171,plain,~r1(skolem0001,X1002)|~r1(X1002,skolem0001)|~r1(skolem0001,X1003)|~r1(X1003,X1001)|p1(X1001)|~p1(X1003)|~r1(skolem0001,X1000)|p1(X1000)|~p1(skolem0001)|r1(skolem0002(X1002,skolem0001,X1002),skolem0003(X1002,skolem0001,X1002))|r1(skolem0004(X1002,skolem0001),skolem0005(X1002,skolem0001)),inference(factor,[status(thm)],[c15])).
% 13.26/13.54 cnf(c858,plain,~r1(skolem0001,X2954)|~r1(X2954,skolem0001)|~r1(skolem0001,X2952)|~r1(X2952,X2953)|p1(X2953)|~p1(X2952)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2954,skolem0001,X2954),skolem0003(X2954,skolem0001,X2954))|r1(skolem0004(X2954,skolem0001),skolem0005(X2954,skolem0001)),inference(resolution,[status(thm)],[c171, c55])).
% 13.26/13.54 cnf(c854,plain,~r1(skolem0001,X2932)|~r1(X2932,skolem0001)|~r1(skolem0001,X2930)|~r1(X2930,X2931)|p1(X2931)|~p1(X2930)|p1(X2932)|~p1(skolem0001)|r1(skolem0002(X2932,skolem0001,X2932),skolem0003(X2932,skolem0001,X2932))|r1(skolem0004(X2932,skolem0001),skolem0005(X2932,skolem0001)),inference(factor,[status(thm)],[c171])).
% 13.26/13.54 cnf(c1752,plain,~r1(skolem0001,X2949)|~r1(X2949,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X2949)|~p1(skolem0001)|r1(skolem0002(X2949,skolem0001,X2949),skolem0003(X2949,skolem0001,X2949))|r1(skolem0004(X2949,skolem0001),skolem0005(X2949,skolem0001)),inference(resolution,[status(thm)],[c854, c56])).
% 13.26/13.54 cnf(c1756,plain,~r1(skolem0001,X2950)|~r1(X2950,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X2950)|~p1(skolem0001)|r1(skolem0002(X2950,skolem0001,X2950),skolem0003(X2950,skolem0001,X2950))|r1(skolem0004(X2950,skolem0001),skolem0005(X2950,skolem0001)),inference(resolution,[status(thm)],[c1752, c55])).
% 13.26/13.54 cnf(c14,negated_conjecture,~r1(skolem0001,X134)|~r1(X134,X137)|~r1(X137,X135)|~r1(X135,X138)|p1(X138)|~p1(X135)|~r1(X137,X136)|p1(X136)|~p1(X137)|~r1(X137,X139)|r1(skolem0002(X134,X137,X139),skolem0003(X134,X137,X139))|r1(X137,skolem0004(X134,X137)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c157,plain,~r1(skolem0001,X950)|~r1(X950,X947)|~r1(X947,X948)|~r1(X948,X949)|p1(X949)|~p1(X948)|~r1(X947,X946)|p1(X946)|~p1(X947)|r1(skolem0002(X950,X947,X946),skolem0003(X950,X947,X946))|r1(X947,skolem0004(X950,X947)),inference(factor,[status(thm)],[c14])).
% 13.26/13.54 cnf(c823,plain,~r1(skolem0001,X2846)|~r1(X2846,skolem0013)|~r1(skolem0013,X2844)|~r1(X2844,X2845)|p1(X2845)|~p1(X2844)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2846,skolem0013,skolem0014),skolem0003(X2846,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X2846,skolem0013)),inference(resolution,[status(thm)],[c157, c56])).
% 13.26/13.54 cnf(c1710,plain,~r1(skolem0001,X2921)|~r1(X2921,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2921)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2921,skolem0013,skolem0014),skolem0003(X2921,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X2921,skolem0013)),inference(factor,[status(thm)],[c823])).
% 13.26/13.54 cnf(c155,plain,~r1(skolem0001,X916)|~r1(X916,X914)|~r1(X914,X913)|~r1(X913,X915)|p1(X915)|~p1(X913)|~r1(X914,X917)|p1(X917)|~p1(X914)|r1(skolem0002(X916,X914,X913),skolem0003(X916,X914,X913))|r1(X914,skolem0004(X916,X914)),inference(factor,[status(thm)],[c14])).
% 13.26/13.54 cnf(c797,plain,~r1(skolem0001,X2826)|~r1(X2826,skolem0013)|~r1(skolem0013,X2824)|~r1(X2824,X2825)|p1(X2825)|~p1(X2824)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2826,skolem0013,X2824),skolem0003(X2826,skolem0013,X2824))|r1(skolem0013,skolem0004(X2826,skolem0013)),inference(resolution,[status(thm)],[c155, c56])).
% 13.26/13.54 cnf(c1695,plain,~r1(skolem0001,X2920)|~r1(X2920,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2920)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2920,skolem0013,skolem0001),skolem0003(X2920,skolem0013,skolem0001))|r1(skolem0013,skolem0004(X2920,skolem0013)),inference(factor,[status(thm)],[c797])).
% 13.26/13.54 cnf(c793,plain,~r1(skolem0001,X2734)|~r1(X2734,skolem0001)|~r1(skolem0001,X2735)|~r1(X2735,X2736)|p1(X2736)|~p1(X2735)|p1(X2734)|~p1(skolem0001)|r1(skolem0002(X2734,skolem0001,X2735),skolem0003(X2734,skolem0001,X2735))|r1(skolem0001,skolem0004(X2734,skolem0001)),inference(factor,[status(thm)],[c155])).
% 13.26/13.54 cnf(c1680,plain,~r1(skolem0001,X2914)|~r1(X2914,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X2914)|~p1(skolem0001)|r1(skolem0002(X2914,skolem0001,skolem0013),skolem0003(X2914,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2914,skolem0001)),inference(resolution,[status(thm)],[c793, c56])).
% 13.26/13.54 cnf(c1747,plain,~r1(skolem0001,X2918)|~r1(X2918,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X2918)|~p1(skolem0001)|r1(skolem0002(X2918,skolem0001,skolem0013),skolem0003(X2918,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2918,skolem0001)),inference(resolution,[status(thm)],[c1680, c55])).
% 13.26/13.54 cnf(c160,plain,~r1(skolem0001,X979)|~r1(X979,skolem0001)|~r1(skolem0001,X977)|~r1(X977,X978)|p1(X978)|~p1(X977)|~r1(skolem0001,X976)|p1(X976)|~p1(skolem0001)|r1(skolem0002(X979,skolem0001,skolem0013),skolem0003(X979,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X979,skolem0001)),inference(resolution,[status(thm)],[c14, c55])).
% 13.26/13.54 cnf(c838,plain,~r1(skolem0001,X2894)|~r1(X2894,skolem0001)|~r1(skolem0001,X2895)|~r1(X2895,X2893)|p1(X2893)|~p1(X2895)|p1(X2894)|~p1(skolem0001)|r1(skolem0002(X2894,skolem0001,skolem0013),skolem0003(X2894,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2894,skolem0001)),inference(factor,[status(thm)],[c160])).
% 13.26/13.54 cnf(c17,negated_conjecture,~r1(skolem0001,X170)|~r1(X170,X173)|~r1(X173,X171)|~r1(X171,X174)|p1(X174)|~p1(X171)|~r1(X173,X172)|p1(X172)|~p1(X173)|~r1(X173,X175)|r1(skolem0002(X170,X173,X175),skolem0003(X170,X173,X175))|p1(skolem0004(X170,X173)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c200,plain,~r1(skolem0001,X1183)|~r1(X1183,X1182)|~r1(X1182,X1181)|~r1(X1181,X1180)|p1(X1180)|~p1(X1181)|~r1(X1182,X1184)|p1(X1184)|~p1(X1182)|r1(skolem0002(X1183,X1182,X1184),skolem0003(X1183,X1182,X1184))|p1(skolem0004(X1183,X1182)),inference(factor,[status(thm)],[c17])).
% 13.26/13.54 cnf(c1018,plain,~r1(skolem0001,X2881)|~r1(X2881,skolem0001)|~r1(skolem0001,X2883)|~r1(X2883,X2882)|p1(X2882)|~p1(X2883)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2881,skolem0001,skolem0013),skolem0003(X2881,skolem0001,skolem0013))|p1(skolem0004(X2881,skolem0001)),inference(resolution,[status(thm)],[c200, c55])).
% 13.26/13.54 cnf(c1017,plain,~r1(skolem0001,X2869)|~r1(X2869,skolem0013)|~r1(skolem0013,X2871)|~r1(X2871,X2870)|p1(X2870)|~p1(X2871)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2869,skolem0013,skolem0014),skolem0003(X2869,skolem0013,skolem0014))|p1(skolem0004(X2869,skolem0013)),inference(resolution,[status(thm)],[c200, c56])).
% 13.26/13.54 cnf(c1728,plain,~r1(skolem0001,X2878)|~r1(X2878,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2878)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2878,skolem0013,skolem0014),skolem0003(X2878,skolem0013,skolem0014))|p1(skolem0004(X2878,skolem0013)),inference(factor,[status(thm)],[c1017])).
% 13.26/13.54 cnf(c941,plain,~r1(skolem0001,X2860)|~r1(X2860,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X2859)|p1(X2859)|~p1(skolem0001)|r1(skolem0002(X2860,skolem0001,skolem0013),skolem0003(X2860,skolem0001,skolem0013))|r1(skolem0004(X2860,skolem0001),skolem0005(X2860,skolem0001)),inference(factor,[status(thm)],[c178])).
% 13.26/13.54 cnf(c1722,plain,~r1(skolem0001,X2864)|~r1(X2864,skolem0001)|~r1(skolem0001,skolem0001)|p1(X2864)|~p1(skolem0001)|r1(skolem0002(X2864,skolem0001,skolem0013),skolem0003(X2864,skolem0001,skolem0013))|r1(skolem0004(X2864,skolem0001),skolem0005(X2864,skolem0001)),inference(factor,[status(thm)],[c941])).
% 13.26/13.54 cnf(c824,plain,~r1(skolem0001,X2854)|~r1(X2854,skolem0001)|~r1(skolem0001,X2852)|~r1(X2852,X2853)|p1(X2853)|~p1(X2852)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2854,skolem0001,skolem0013),skolem0003(X2854,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2854,skolem0001)),inference(resolution,[status(thm)],[c157, c55])).
% 13.26/13.54 cnf(c177,plain,~r1(skolem0001,X1076)|~r1(X1076,skolem0013)|~r1(skolem0013,X1075)|~r1(X1075,X1074)|p1(X1074)|~p1(X1075)|~r1(skolem0013,X1073)|p1(X1073)|~p1(skolem0013)|r1(skolem0002(X1076,skolem0013,skolem0014),skolem0003(X1076,skolem0013,skolem0014))|r1(skolem0004(X1076,skolem0013),skolem0005(X1076,skolem0013)),inference(resolution,[status(thm)],[c15, c56])).
% 13.26/13.54 cnf(c933,plain,~r1(skolem0001,X2842)|~r1(X2842,skolem0013)|~r1(skolem0013,skolem0013)|~r1(skolem0013,X2843)|p1(X2843)|~p1(skolem0013)|r1(skolem0002(X2842,skolem0013,skolem0014),skolem0003(X2842,skolem0013,skolem0014))|r1(skolem0004(X2842,skolem0013),skolem0005(X2842,skolem0013)),inference(factor,[status(thm)],[c177])).
% 13.26/13.54 cnf(c798,plain,~r1(skolem0001,X2834)|~r1(X2834,skolem0001)|~r1(skolem0001,X2832)|~r1(X2832,X2833)|p1(X2833)|~p1(X2832)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2834,skolem0001,X2832),skolem0003(X2834,skolem0001,X2832))|r1(skolem0001,skolem0004(X2834,skolem0001)),inference(resolution,[status(thm)],[c155, c55])).
% 13.26/13.54 cnf(c153,plain,~r1(skolem0001,X891)|~r1(X891,skolem0001)|~r1(skolem0001,X890)|~r1(X890,X892)|p1(X892)|~p1(X890)|~r1(skolem0001,X889)|p1(X889)|~p1(skolem0001)|r1(skolem0002(X891,skolem0001,X891),skolem0003(X891,skolem0001,X891))|r1(skolem0001,skolem0004(X891,skolem0001)),inference(factor,[status(thm)],[c14])).
% 13.26/13.54 cnf(c773,plain,~r1(skolem0001,X2797)|~r1(X2797,skolem0001)|~r1(skolem0001,X2796)|~r1(X2796,X2795)|p1(X2795)|~p1(X2796)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2797,skolem0001,X2797),skolem0003(X2797,skolem0001,X2797))|r1(skolem0001,skolem0004(X2797,skolem0001)),inference(resolution,[status(thm)],[c153, c55])).
% 13.26/13.54 cnf(c203,plain,~r1(skolem0001,X1218)|~r1(X1218,skolem0001)|~r1(skolem0001,X1216)|~r1(X1216,X1215)|p1(X1215)|~p1(X1216)|~r1(skolem0001,X1217)|p1(X1217)|~p1(skolem0001)|r1(skolem0002(X1218,skolem0001,skolem0013),skolem0003(X1218,skolem0001,skolem0013))|p1(skolem0004(X1218,skolem0001)),inference(resolution,[status(thm)],[c17, c55])).
% 13.26/13.54 cnf(c1029,plain,~r1(skolem0001,X2780)|~r1(X2780,skolem0001)|~r1(skolem0001,X2779)|~r1(X2779,X2781)|p1(X2781)|~p1(X2779)|p1(X2780)|~p1(skolem0001)|r1(skolem0002(X2780,skolem0001,skolem0013),skolem0003(X2780,skolem0001,skolem0013))|p1(skolem0004(X2780,skolem0001)),inference(factor,[status(thm)],[c203])).
% 13.26/13.54 cnf(c769,plain,~r1(skolem0001,X2699)|~r1(X2699,skolem0001)|~r1(skolem0001,X2700)|~r1(X2700,X2701)|p1(X2701)|~p1(X2700)|p1(X2699)|~p1(skolem0001)|r1(skolem0002(X2699,skolem0001,X2699),skolem0003(X2699,skolem0001,X2699))|r1(skolem0001,skolem0004(X2699,skolem0001)),inference(factor,[status(thm)],[c153])).
% 13.26/13.54 cnf(c1667,plain,~r1(skolem0001,X2719)|~r1(X2719,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X2719)|~p1(skolem0001)|r1(skolem0002(X2719,skolem0001,X2719),skolem0003(X2719,skolem0001,X2719))|r1(skolem0001,skolem0004(X2719,skolem0001)),inference(resolution,[status(thm)],[c769, c56])).
% 13.26/13.54 cnf(c1675,plain,~r1(skolem0001,X2720)|~r1(X2720,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X2720)|~p1(skolem0001)|r1(skolem0002(X2720,skolem0001,X2720),skolem0003(X2720,skolem0001,X2720))|r1(skolem0001,skolem0004(X2720,skolem0001)),inference(resolution,[status(thm)],[c1667, c55])).
% 13.26/13.54 cnf(c13,negated_conjecture,~r1(skolem0001,X122)|~r1(X122,X128)|~r1(X128,X125)|~r1(X125,X129)|p1(X129)|~p1(X125)|~r1(X128,X126)|p1(X126)|~p1(X128)|~r1(X128,X130)|r1(X130,skolem0002(X122,X128,X130))|~r1(skolem0004(X122,X128),X123)|~r1(X123,X124)|~r1(X124,X127)|p1(X127)|~p1(X124)|p1(X123),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c147,plain,~r1(skolem0001,X850)|~r1(X850,X848)|~r1(X848,skolem0004(X850,X848))|~r1(skolem0004(X850,X848),X854)|p1(X854)|~p1(skolem0004(X850,X848))|~r1(X848,X851)|p1(X851)|~p1(X848)|~r1(X848,X853)|r1(X853,skolem0002(X850,X848,X853))|~r1(X854,X852)|~r1(X852,X849)|p1(X849)|~p1(X852),inference(factor,[status(thm)],[c13])).
% 13.26/13.54 cnf(c745,plain,~r1(skolem0001,X2704)|~r1(X2704,X2706)|~r1(X2706,skolem0004(X2704,X2706))|~r1(skolem0004(X2704,X2706),X2702)|p1(X2702)|~p1(skolem0004(X2704,X2706))|~r1(X2706,X2703)|p1(X2703)|~p1(X2706)|~r1(X2706,X2705)|r1(X2705,skolem0002(X2704,X2706,X2705))|~r1(X2702,skolem0004(X2704,X2706)),inference(factor,[status(thm)],[c147])).
% 13.26/13.54 cnf(c198,plain,~r1(skolem0001,X1161)|~r1(X1161,X1160)|~r1(X1160,X1162)|~r1(X1162,X1158)|p1(X1158)|~p1(X1162)|~r1(X1160,X1159)|p1(X1159)|~p1(X1160)|r1(skolem0002(X1161,X1160,X1162),skolem0003(X1161,X1160,X1162))|p1(skolem0004(X1161,X1160)),inference(factor,[status(thm)],[c17])).
% 13.26/13.54 cnf(c989,plain,~r1(skolem0001,X2603)|~r1(X2603,skolem0013)|~r1(skolem0013,X2604)|~r1(X2604,X2602)|p1(X2602)|~p1(X2604)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2603,skolem0013,X2604),skolem0003(X2603,skolem0013,X2604))|p1(skolem0004(X2603,skolem0013)),inference(resolution,[status(thm)],[c198, c56])).
% 13.26/13.54 cnf(c1631,plain,~r1(skolem0001,X2698)|~r1(X2698,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2698)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2698,skolem0013,skolem0001),skolem0003(X2698,skolem0013,skolem0001))|p1(skolem0004(X2698,skolem0013)),inference(factor,[status(thm)],[c989])).
% 13.26/13.54 cnf(c985,plain,~r1(skolem0001,X2463)|~r1(X2463,skolem0001)|~r1(skolem0001,X2464)|~r1(X2464,X2462)|p1(X2462)|~p1(X2464)|p1(X2463)|~p1(skolem0001)|r1(skolem0002(X2463,skolem0001,X2464),skolem0003(X2463,skolem0001,X2464))|p1(skolem0004(X2463,skolem0001)),inference(factor,[status(thm)],[c198])).
% 13.26/13.54 cnf(c1582,plain,~r1(skolem0001,X2688)|~r1(X2688,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X2688)|~p1(skolem0001)|r1(skolem0002(X2688,skolem0001,skolem0013),skolem0003(X2688,skolem0001,skolem0013))|p1(skolem0004(X2688,skolem0001)),inference(resolution,[status(thm)],[c985, c56])).
% 13.26/13.54 cnf(c1662,plain,~r1(skolem0001,X2689)|~r1(X2689,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X2689)|~p1(skolem0001)|r1(skolem0002(X2689,skolem0001,skolem0013),skolem0003(X2689,skolem0001,skolem0013))|p1(skolem0004(X2689,skolem0001)),inference(resolution,[status(thm)],[c1582, c55])).
% 13.26/13.54 cnf(c8,negated_conjecture,~r1(skolem0001,X51)|~r1(X51,X54)|~r1(X54,X52)|~r1(X52,X55)|p1(X55)|~p1(X52)|~r1(X54,X53)|p1(X53)|~p1(X54)|~r1(X54,X56)|r1(X56,skolem0002(X51,X54,X56))|r1(skolem0004(X51,X54),skolem0005(X51,X54)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c80,plain,~r1(skolem0001,X591)|~r1(X591,X589)|~r1(X589,X588)|~r1(X588,X590)|p1(X590)|~p1(X588)|~r1(X589,X587)|p1(X587)|~p1(X589)|r1(X587,skolem0002(X591,X589,X587))|r1(skolem0004(X591,X589),skolem0005(X591,X589)),inference(factor,[status(thm)],[c8])).
% 13.26/13.54 cnf(c582,plain,~r1(skolem0001,X2439)|~r1(X2439,skolem0013)|~r1(skolem0013,X2441)|~r1(X2441,X2440)|p1(X2440)|~p1(X2441)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(X2439,skolem0013,skolem0014))|r1(skolem0004(X2439,skolem0013),skolem0005(X2439,skolem0013)),inference(resolution,[status(thm)],[c80, c56])).
% 13.26/13.54 cnf(c1564,plain,~r1(skolem0001,X2681)|~r1(X2681,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2681)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(X2681,skolem0013,skolem0014))|r1(skolem0004(X2681,skolem0013),skolem0005(X2681,skolem0013)),inference(factor,[status(thm)],[c582])).
% 13.26/13.54 cnf(c78,plain,~r1(skolem0001,X568)|~r1(X568,X565)|~r1(X565,X564)|~r1(X564,X567)|p1(X567)|~p1(X564)|~r1(X565,X566)|p1(X566)|~p1(X565)|r1(X564,skolem0002(X568,X565,X564))|r1(skolem0004(X568,X565),skolem0005(X568,X565)),inference(factor,[status(thm)],[c8])).
% 13.26/13.54 cnf(c556,plain,~r1(skolem0001,X2417)|~r1(X2417,skolem0013)|~r1(skolem0013,X2415)|~r1(X2415,X2416)|p1(X2416)|~p1(X2415)|p1(skolem0014)|~p1(skolem0013)|r1(X2415,skolem0002(X2417,skolem0013,X2415))|r1(skolem0004(X2417,skolem0013),skolem0005(X2417,skolem0013)),inference(resolution,[status(thm)],[c78, c56])).
% 13.26/13.54 cnf(c1544,plain,~r1(skolem0001,X2680)|~r1(X2680,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2680)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0001,skolem0002(X2680,skolem0013,skolem0001))|r1(skolem0004(X2680,skolem0013),skolem0005(X2680,skolem0013)),inference(factor,[status(thm)],[c556])).
% 13.26/13.54 cnf(c552,plain,~r1(skolem0001,X2383)|~r1(X2383,skolem0001)|~r1(skolem0001,X2385)|~r1(X2385,X2384)|p1(X2384)|~p1(X2385)|p1(X2383)|~p1(skolem0001)|r1(X2385,skolem0002(X2383,skolem0001,X2385))|r1(skolem0004(X2383,skolem0001),skolem0005(X2383,skolem0001)),inference(factor,[status(thm)],[c78])).
% 13.26/13.54 cnf(c1534,plain,~r1(skolem0001,X2671)|~r1(X2671,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X2671)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2671,skolem0001,skolem0013))|r1(skolem0004(X2671,skolem0001),skolem0005(X2671,skolem0001)),inference(resolution,[status(thm)],[c552, c56])).
% 13.26/13.54 cnf(c1656,plain,~r1(skolem0001,X2672)|~r1(X2672,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X2672)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2672,skolem0001,skolem0013))|r1(skolem0004(X2672,skolem0001),skolem0005(X2672,skolem0001)),inference(resolution,[status(thm)],[c1534, c55])).
% 13.26/13.54 cnf(c29,negated_conjecture,~r1(skolem0001,X326)|~r1(X326,X329)|~r1(X329,X327)|~r1(X327,X330)|p1(X330)|~p1(X327)|~r1(X329,X328)|p1(X328)|~p1(X329)|~r1(X329,X331)|p1(skolem0002(X326,X329,X331))|r1(skolem0004(X326,X329),skolem0005(X326,X329)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.54 cnf(c298,plain,~r1(skolem0001,X1624)|~r1(X1624,X1627)|~r1(X1627,X1628)|~r1(X1628,X1626)|p1(X1626)|~p1(X1628)|~r1(X1627,X1625)|p1(X1625)|~p1(X1627)|p1(skolem0002(X1624,X1627,X1625))|r1(skolem0004(X1624,X1627),skolem0005(X1624,X1627)),inference(factor,[status(thm)],[c29])).
% 13.26/13.54 cnf(c1227,plain,~r1(skolem0001,X2643)|~r1(X2643,skolem0001)|~r1(skolem0001,X2644)|~r1(X2644,X2642)|p1(X2642)|~p1(X2644)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X2643,skolem0001,skolem0013))|r1(skolem0004(X2643,skolem0001),skolem0005(X2643,skolem0001)),inference(resolution,[status(thm)],[c298, c55])).
% 13.26/13.54 cnf(c1226,plain,~r1(skolem0001,X2629)|~r1(X2629,skolem0013)|~r1(skolem0013,X2630)|~r1(X2630,X2628)|p1(X2628)|~p1(X2630)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X2629,skolem0013,skolem0014))|r1(skolem0004(X2629,skolem0013),skolem0005(X2629,skolem0013)),inference(resolution,[status(thm)],[c298, c56])).
% 13.26/13.54 cnf(c1643,plain,~r1(skolem0001,X2634)|~r1(X2634,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2634)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X2634,skolem0013,skolem0014))|r1(skolem0004(X2634,skolem0013),skolem0005(X2634,skolem0013)),inference(factor,[status(thm)],[c1226])).
% 13.26/13.54 cnf(c990,plain,~r1(skolem0001,X2609)|~r1(X2609,skolem0001)|~r1(skolem0001,X2610)|~r1(X2610,X2608)|p1(X2608)|~p1(X2610)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2609,skolem0001,X2610),skolem0003(X2609,skolem0001,X2610))|p1(skolem0004(X2609,skolem0001)),inference(resolution,[status(thm)],[c198, c55])).
% 13.26/13.54 cnf(c196,plain,~r1(skolem0001,X1142)|~r1(X1142,skolem0001)|~r1(skolem0001,X1140)|~r1(X1140,X1139)|p1(X1139)|~p1(X1140)|~r1(skolem0001,X1141)|p1(X1141)|~p1(skolem0001)|r1(skolem0002(X1142,skolem0001,X1142),skolem0003(X1142,skolem0001,X1142))|p1(skolem0004(X1142,skolem0001)),inference(factor,[status(thm)],[c17])).
% 13.26/13.54 cnf(c972,plain,~r1(skolem0001,X2583)|~r1(X2583,skolem0001)|~r1(skolem0001,X2582)|~r1(X2582,X2584)|p1(X2584)|~p1(X2582)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2583,skolem0001,X2583),skolem0003(X2583,skolem0001,X2583))|p1(skolem0004(X2583,skolem0001)),inference(resolution,[status(thm)],[c196, c55])).
% 13.26/13.54 cnf(c857,plain,~r1(skolem0001,X2572)|~r1(X2572,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X2573)|p1(X2573)|~p1(skolem0001)|r1(skolem0002(X2572,skolem0001,X2572),skolem0003(X2572,skolem0001,X2572))|r1(skolem0004(X2572,skolem0001),skolem0005(X2572,skolem0001)),inference(factor,[status(thm)],[c171])).
% 13.26/13.54 cnf(c1618,plain,~r1(skolem0001,X2581)|~r1(X2581,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2581,skolem0001,X2581),skolem0003(X2581,skolem0001,X2581))|r1(skolem0004(X2581,skolem0001),skolem0005(X2581,skolem0001)),inference(resolution,[status(thm)],[c857, c55])).
% 13.26/13.54 cnf(c301,plain,~r1(skolem0001,X1658)|~r1(X1658,skolem0001)|~r1(skolem0001,X1657)|~r1(X1657,X1660)|p1(X1660)|~p1(X1657)|~r1(skolem0001,X1659)|p1(X1659)|~p1(skolem0001)|p1(skolem0002(X1658,skolem0001,skolem0013))|r1(skolem0004(X1658,skolem0001),skolem0005(X1658,skolem0001)),inference(resolution,[status(thm)],[c29, c55])).
% 13.26/13.54 cnf(c1238,plain,~r1(skolem0001,X2536)|~r1(X2536,skolem0001)|~r1(skolem0001,X2538)|~r1(X2538,X2537)|p1(X2537)|~p1(X2538)|p1(X2536)|~p1(skolem0001)|p1(skolem0002(X2536,skolem0001,skolem0013))|r1(skolem0004(X2536,skolem0001),skolem0005(X2536,skolem0001)),inference(factor,[status(thm)],[c301])).
% 13.26/13.54 cnf(c296,plain,~r1(skolem0001,X1614)|~r1(X1614,X1617)|~r1(X1617,X1615)|~r1(X1615,X1616)|p1(X1616)|~p1(X1615)|~r1(X1617,X1613)|p1(X1613)|~p1(X1617)|p1(skolem0002(X1614,X1617,X1615))|r1(skolem0004(X1614,X1617),skolem0005(X1614,X1617)),inference(factor,[status(thm)],[c29])).
% 13.26/13.54 cnf(c1214,plain,~r1(skolem0001,X2521)|~r1(X2521,skolem0001)|~r1(skolem0001,X2522)|~r1(X2522,X2520)|p1(X2520)|~p1(X2522)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X2521,skolem0001,X2522))|r1(skolem0004(X2521,skolem0001),skolem0005(X2521,skolem0001)),inference(resolution,[status(thm)],[c296, c55])).
% 13.26/13.54 cnf(c1213,plain,~r1(skolem0001,X2511)|~r1(X2511,skolem0013)|~r1(skolem0013,X2512)|~r1(X2512,X2510)|p1(X2510)|~p1(X2512)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X2511,skolem0013,X2512))|r1(skolem0004(X2511,skolem0013),skolem0005(X2511,skolem0013)),inference(resolution,[status(thm)],[c296, c56])).
% 13.26/13.54 cnf(c1597,plain,~r1(skolem0001,X2519)|~r1(X2519,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2519)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X2519,skolem0013,skolem0001))|r1(skolem0004(X2519,skolem0013),skolem0005(X2519,skolem0013)),inference(factor,[status(thm)],[c1213])).
% 13.26/13.54 cnf(c294,plain,~r1(skolem0001,X1598)|~r1(X1598,skolem0001)|~r1(skolem0001,X1597)|~r1(X1597,X1599)|p1(X1599)|~p1(X1597)|~r1(skolem0001,X1600)|p1(X1600)|~p1(skolem0001)|p1(skolem0002(X1598,skolem0001,X1598))|r1(skolem0004(X1598,skolem0001),skolem0005(X1598,skolem0001)),inference(factor,[status(thm)],[c29])).
% 13.26/13.54 cnf(c1190,plain,~r1(skolem0001,X2493)|~r1(X2493,skolem0001)|~r1(skolem0001,X2494)|~r1(X2494,X2492)|p1(X2492)|~p1(X2494)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X2493,skolem0001,X2493))|r1(skolem0004(X2493,skolem0001),skolem0005(X2493,skolem0001)),inference(resolution,[status(thm)],[c294, c55])).
% 13.26/13.54 cnf(c81,plain,~r1(skolem0001,X597)|~r1(X597,skolem0001)|~r1(skolem0001,X598)|~r1(X598,X596)|p1(X596)|~p1(X598)|~r1(skolem0001,X595)|p1(X595)|~p1(skolem0001)|r1(skolem0013,skolem0002(X597,skolem0001,skolem0013))|r1(skolem0004(X597,skolem0001),skolem0005(X597,skolem0001)),inference(resolution,[status(thm)],[c8, c55])).
% 13.26/13.54 cnf(c585,plain,~r1(skolem0001,X2467)|~r1(X2467,skolem0001)|~r1(skolem0001,X2466)|~r1(X2466,X2468)|p1(X2468)|~p1(X2466)|p1(X2467)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2467,skolem0001,skolem0013))|r1(skolem0004(X2467,skolem0001),skolem0005(X2467,skolem0001)),inference(factor,[status(thm)],[c81])).
% 13.26/13.54 cnf(c968,plain,~r1(skolem0001,X2436)|~r1(X2436,skolem0001)|~r1(skolem0001,X2434)|~r1(X2434,X2435)|p1(X2435)|~p1(X2434)|p1(X2436)|~p1(skolem0001)|r1(skolem0002(X2436,skolem0001,X2436),skolem0003(X2436,skolem0001,X2436))|p1(skolem0004(X2436,skolem0001)),inference(factor,[status(thm)],[c196])).
% 13.26/13.54 cnf(c1561,plain,~r1(skolem0001,X2446)|~r1(X2446,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X2446)|~p1(skolem0001)|r1(skolem0002(X2446,skolem0001,X2446),skolem0003(X2446,skolem0001,X2446))|p1(skolem0004(X2446,skolem0001)),inference(resolution,[status(thm)],[c968, c56])).
% 13.26/13.54 cnf(c1571,plain,~r1(skolem0001,X2450)|~r1(X2450,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X2450)|~p1(skolem0001)|r1(skolem0002(X2450,skolem0001,X2450),skolem0003(X2450,skolem0001,X2450))|p1(skolem0004(X2450,skolem0001)),inference(resolution,[status(thm)],[c1561, c55])).
% 13.26/13.54 cnf(c583,plain,~r1(skolem0001,X2447)|~r1(X2447,skolem0001)|~r1(skolem0001,X2449)|~r1(X2449,X2448)|p1(X2448)|~p1(X2449)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2447,skolem0001,skolem0013))|r1(skolem0004(X2447,skolem0001),skolem0005(X2447,skolem0001)),inference(resolution,[status(thm)],[c80, c55])).
% 13.26/13.54 cnf(c557,plain,~r1(skolem0001,X2423)|~r1(X2423,skolem0001)|~r1(skolem0001,X2421)|~r1(X2421,X2422)|p1(X2422)|~p1(X2421)|p1(skolem0013)|~p1(skolem0001)|r1(X2421,skolem0002(X2423,skolem0001,X2421))|r1(skolem0004(X2423,skolem0001),skolem0005(X2423,skolem0001)),inference(resolution,[status(thm)],[c78, c55])).
% 13.26/13.54 cnf(c841,plain,~r1(skolem0001,X2413)|~r1(X2413,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X2414)|p1(X2414)|~p1(skolem0001)|r1(skolem0002(X2413,skolem0001,skolem0013),skolem0003(X2413,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2413,skolem0001)),inference(factor,[status(thm)],[c160])).
% 13.26/13.54 cnf(c1540,plain,~r1(skolem0001,X2419)|~r1(X2419,skolem0001)|~r1(skolem0001,skolem0001)|p1(X2419)|~p1(skolem0001)|r1(skolem0002(X2419,skolem0001,skolem0013),skolem0003(X2419,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2419,skolem0001)),inference(factor,[status(thm)],[c841])).
% 13.26/13.55 cnf(c159,plain,~r1(skolem0001,X974)|~r1(X974,skolem0013)|~r1(skolem0013,X972)|~r1(X972,X973)|p1(X973)|~p1(X972)|~r1(skolem0013,X971)|p1(X971)|~p1(skolem0013)|r1(skolem0002(X974,skolem0013,skolem0014),skolem0003(X974,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X974,skolem0013)),inference(resolution,[status(thm)],[c14, c56])).
% 13.26/13.55 cnf(c834,plain,~r1(skolem0001,X2407)|~r1(X2407,skolem0013)|~r1(skolem0013,skolem0013)|~r1(skolem0013,X2408)|p1(X2408)|~p1(skolem0013)|r1(skolem0002(X2407,skolem0013,skolem0014),skolem0003(X2407,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X2407,skolem0013)),inference(factor,[status(thm)],[c159])).
% 13.26/13.55 cnf(c76,plain,~r1(skolem0001,X549)|~r1(X549,skolem0001)|~r1(skolem0001,X550)|~r1(X550,X548)|p1(X548)|~p1(X550)|~r1(skolem0001,X551)|p1(X551)|~p1(skolem0001)|r1(X549,skolem0002(X549,skolem0001,X549))|r1(skolem0004(X549,skolem0001),skolem0005(X549,skolem0001)),inference(factor,[status(thm)],[c8])).
% 13.26/13.55 cnf(c532,plain,~r1(skolem0001,X2354)|~r1(X2354,skolem0001)|~r1(skolem0001,X2353)|~r1(X2353,X2352)|p1(X2352)|~p1(X2353)|p1(X2354)|~p1(skolem0001)|r1(X2354,skolem0002(X2354,skolem0001,X2354))|r1(skolem0004(X2354,skolem0001),skolem0005(X2354,skolem0001)),inference(factor,[status(thm)],[c76])).
% 13.26/13.55 cnf(c1516,plain,~r1(skolem0001,X2371)|~r1(X2371,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X2371)|~p1(skolem0001)|r1(X2371,skolem0002(X2371,skolem0001,X2371))|r1(skolem0004(X2371,skolem0001),skolem0005(X2371,skolem0001)),inference(resolution,[status(thm)],[c532, c56])).
% 13.26/13.55 cnf(c1523,plain,~r1(skolem0001,X2376)|~r1(X2376,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X2376)|~p1(skolem0001)|r1(X2376,skolem0002(X2376,skolem0001,X2376))|r1(skolem0004(X2376,skolem0001),skolem0005(X2376,skolem0001)),inference(resolution,[status(thm)],[c1516, c55])).
% 13.26/13.55 cnf(c536,plain,~r1(skolem0001,X2374)|~r1(X2374,skolem0001)|~r1(skolem0001,X2373)|~r1(X2373,X2372)|p1(X2372)|~p1(X2373)|p1(skolem0013)|~p1(skolem0001)|r1(X2374,skolem0002(X2374,skolem0001,X2374))|r1(skolem0004(X2374,skolem0001),skolem0005(X2374,skolem0001)),inference(resolution,[status(thm)],[c76, c55])).
% 13.26/13.55 cnf(c1209,plain,~r1(skolem0001,X2334)|~r1(X2334,skolem0001)|~r1(skolem0001,X2335)|~r1(X2335,X2333)|p1(X2333)|~p1(X2335)|p1(X2334)|~p1(skolem0001)|p1(skolem0002(X2334,skolem0001,X2335))|r1(skolem0004(X2334,skolem0001),skolem0005(X2334,skolem0001)),inference(factor,[status(thm)],[c296])).
% 13.26/13.55 cnf(c1510,plain,~r1(skolem0001,X2368)|~r1(X2368,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X2368)|~p1(skolem0001)|p1(skolem0002(X2368,skolem0001,skolem0013))|r1(skolem0004(X2368,skolem0001),skolem0005(X2368,skolem0001)),inference(resolution,[status(thm)],[c1209, c56])).
% 13.26/13.55 cnf(c1520,plain,~r1(skolem0001,X2369)|~r1(X2369,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X2369)|~p1(skolem0001)|p1(skolem0002(X2369,skolem0001,skolem0013))|r1(skolem0004(X2369,skolem0001),skolem0005(X2369,skolem0001)),inference(resolution,[status(thm)],[c1510, c55])).
% 13.26/13.55 cnf(c174,plain,~r1(skolem0001,X1038)|~r1(X1038,X1035)|~r1(X1035,X1035)|~r1(X1035,X1037)|p1(X1037)|~p1(X1035)|~r1(X1035,X1036)|p1(X1036)|r1(skolem0002(X1038,X1035,X1037),skolem0003(X1038,X1035,X1037))|r1(skolem0004(X1038,X1035),skolem0005(X1038,X1035)),inference(factor,[status(thm)],[c15])).
% 13.26/13.55 cnf(c899,plain,~r1(skolem0001,X1044)|~r1(X1044,X1045)|~r1(X1045,X1045)|~r1(X1045,X1043)|p1(X1043)|~p1(X1045)|r1(skolem0002(X1044,X1045,X1043),skolem0003(X1044,X1045,X1043))|r1(skolem0004(X1044,X1045),skolem0005(X1044,X1045)),inference(factor,[status(thm)],[c174])).
% 13.26/13.55 cnf(c906,plain,~r1(skolem0001,X2287)|~r1(X2287,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2287,skolem0013,skolem0014),skolem0003(X2287,skolem0013,skolem0014))|r1(skolem0004(X2287,skolem0013),skolem0005(X2287,skolem0013)),inference(resolution,[status(thm)],[c899, c56])).
% 13.26/13.55 cnf(c1483,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(skolem0013,skolem0013,skolem0014),skolem0003(skolem0013,skolem0013,skolem0014))|r1(skolem0004(skolem0013,skolem0013),skolem0005(skolem0013,skolem0013)),inference(factor,[status(thm)],[c906])).
% 13.26/13.55 cnf(c1186,plain,~r1(skolem0001,X2316)|~r1(X2316,skolem0001)|~r1(skolem0001,X2315)|~r1(X2315,X2314)|p1(X2314)|~p1(X2315)|p1(X2316)|~p1(skolem0001)|p1(skolem0002(X2316,skolem0001,X2316))|r1(skolem0004(X2316,skolem0001),skolem0005(X2316,skolem0001)),inference(factor,[status(thm)],[c294])).
% 13.26/13.55 cnf(c1501,plain,~r1(skolem0001,X2324)|~r1(X2324,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X2324)|~p1(skolem0001)|p1(skolem0002(X2324,skolem0001,X2324))|r1(skolem0004(X2324,skolem0001),skolem0005(X2324,skolem0001)),inference(resolution,[status(thm)],[c1186, c56])).
% 13.26/13.55 cnf(c1505,plain,~r1(skolem0001,X2328)|~r1(X2328,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X2328)|~p1(skolem0001)|p1(skolem0002(X2328,skolem0001,X2328))|r1(skolem0004(X2328,skolem0001),skolem0005(X2328,skolem0001)),inference(resolution,[status(thm)],[c1501, c55])).
% 13.26/13.55 cnf(c7,negated_conjecture,~r1(skolem0001,X42)|~r1(X42,X45)|~r1(X45,X43)|~r1(X43,X46)|p1(X46)|~p1(X43)|~r1(X45,X44)|p1(X44)|~p1(X45)|~r1(X45,X47)|r1(X47,skolem0002(X42,X45,X47))|r1(X45,skolem0004(X42,X45)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.55 cnf(c68,plain,~r1(skolem0001,X505)|~r1(X505,X504)|~r1(X504,X502)|~r1(X502,X503)|p1(X503)|~p1(X502)|~r1(X504,X506)|p1(X506)|~p1(X504)|r1(X506,skolem0002(X505,X504,X506))|r1(X504,skolem0004(X505,X504)),inference(factor,[status(thm)],[c7])).
% 13.26/13.55 cnf(c507,plain,~r1(skolem0001,X2309)|~r1(X2309,skolem0001)|~r1(skolem0001,X2308)|~r1(X2308,X2307)|p1(X2307)|~p1(X2308)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2309,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2309,skolem0001)),inference(resolution,[status(thm)],[c68, c55])).
% 13.26/13.55 cnf(c506,plain,~r1(skolem0001,X2300)|~r1(X2300,skolem0013)|~r1(skolem0013,X2299)|~r1(X2299,X2298)|p1(X2298)|~p1(X2299)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(X2300,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X2300,skolem0013)),inference(resolution,[status(thm)],[c68, c56])).
% 13.26/13.55 cnf(c1486,plain,~r1(skolem0001,X2304)|~r1(X2304,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2304)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(X2304,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X2304,skolem0013)),inference(factor,[status(thm)],[c506])).
% 13.26/13.55 cnf(c907,plain,~r1(skolem0001,X2288)|~r1(X2288,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2288,skolem0001,skolem0013),skolem0003(X2288,skolem0001,skolem0013))|r1(skolem0004(X2288,skolem0001),skolem0005(X2288,skolem0001)),inference(resolution,[status(thm)],[c899, c55])).
% 13.26/13.55 cnf(c1484,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(skolem0001,skolem0001,skolem0013),skolem0003(skolem0001,skolem0001,skolem0013))|r1(skolem0004(skolem0001,skolem0001),skolem0005(skolem0001,skolem0001)),inference(factor,[status(thm)],[c907])).
% 13.26/13.55 cnf(c886,plain,~r1(skolem0001,X1033)|~r1(X1033,X1032)|~r1(X1032,X1032)|~r1(X1032,X1031)|p1(X1031)|~p1(X1032)|r1(skolem0002(X1033,X1032,X1032),skolem0003(X1033,X1032,X1032))|r1(skolem0004(X1033,X1032),skolem0005(X1033,X1032)),inference(factor,[status(thm)],[c173])).
% 13.26/13.55 cnf(c894,plain,~r1(skolem0001,X2283)|~r1(X2283,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2283,skolem0001,skolem0001),skolem0003(X2283,skolem0001,skolem0001))|r1(skolem0004(X2283,skolem0001),skolem0005(X2283,skolem0001)),inference(resolution,[status(thm)],[c886, c55])).
% 13.26/13.55 cnf(c893,plain,~r1(skolem0001,X2282)|~r1(X2282,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X2282,skolem0013,skolem0013),skolem0003(X2282,skolem0013,skolem0013))|r1(skolem0004(X2282,skolem0013),skolem0005(X2282,skolem0013)),inference(resolution,[status(thm)],[c886, c56])).
% 13.26/13.55 cnf(c172,plain,~r1(skolem0001,X1015)|~r1(X1015,X1015)|~r1(X1015,X1016)|~r1(X1016,X1014)|p1(X1014)|~p1(X1016)|~r1(X1015,X1013)|p1(X1013)|~p1(X1015)|r1(skolem0002(X1015,X1015,X1015),skolem0003(X1015,X1015,X1015))|r1(skolem0004(X1015,X1015),skolem0005(X1015,X1015)),inference(factor,[status(thm)],[c15])).
% 13.26/13.55 cnf(c874,plain,~r1(skolem0001,X1018)|~r1(X1018,X1018)|~r1(X1018,X1017)|p1(X1017)|~p1(X1018)|r1(skolem0002(X1018,X1018,X1018),skolem0003(X1018,X1018,X1018))|r1(skolem0004(X1018,X1018),skolem0005(X1018,X1018)),inference(factor,[status(thm)],[c172])).
% 13.26/13.55 cnf(c880,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(skolem0013,skolem0013,skolem0013),skolem0003(skolem0013,skolem0013,skolem0013))|r1(skolem0004(skolem0013,skolem0013),skolem0005(skolem0013,skolem0013)),inference(resolution,[status(thm)],[c874, c56])).
% 13.26/13.55 cnf(c69,plain,~r1(skolem0001,X511)|~r1(X511,skolem0001)|~r1(skolem0001,X513)|~r1(X513,X512)|p1(X512)|~p1(X513)|~r1(skolem0001,X510)|p1(X510)|~p1(skolem0001)|r1(skolem0013,skolem0002(X511,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X511,skolem0001)),inference(resolution,[status(thm)],[c7, c55])).
% 13.26/13.55 cnf(c509,plain,~r1(skolem0001,X2257)|~r1(X2257,skolem0001)|~r1(skolem0001,X2259)|~r1(X2259,X2258)|p1(X2258)|~p1(X2259)|p1(X2257)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2257,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2257,skolem0001)),inference(factor,[status(thm)],[c69])).
% 13.26/13.55 cnf(c51,negated_conjecture,~r1(skolem0001,X448)|~r1(X448,X453)|~r1(X453,X451)|~r1(X451,X449)|p1(X449)|~p1(skolem0011(X448,X453,X451,X449))|~r1(skolem0012(X448,X453),X450)|~r1(X450,X452)|p1(X452)|~p1(X450),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.55 cnf(c451,plain,~r1(skolem0001,X2252)|~r1(X2252,X2250)|~r1(X2250,X2253)|~r1(X2253,X2251)|p1(X2251)|~p1(skolem0011(X2252,X2250,X2253,X2251))|~r1(skolem0012(X2252,X2250),skolem0011(X2252,X2250,X2253,X2251))|~r1(skolem0011(X2252,X2250,X2253,X2251),X2254)|p1(X2254),inference(factor,[status(thm)],[c51])).
% 13.26/13.55 cnf(c66,plain,~r1(skolem0001,X481)|~r1(X481,X479)|~r1(X479,X482)|~r1(X482,X478)|p1(X478)|~p1(X482)|~r1(X479,X480)|p1(X480)|~p1(X479)|r1(X482,skolem0002(X481,X479,X482))|r1(X479,skolem0004(X481,X479)),inference(factor,[status(thm)],[c7])).
% 13.26/13.55 cnf(c480,plain,~r1(skolem0001,X2084)|~r1(X2084,skolem0013)|~r1(skolem0013,X2082)|~r1(X2082,X2083)|p1(X2083)|~p1(X2082)|p1(skolem0014)|~p1(skolem0013)|r1(X2082,skolem0002(X2084,skolem0013,X2082))|r1(skolem0013,skolem0004(X2084,skolem0013)),inference(resolution,[status(thm)],[c66, c56])).
% 13.26/13.55 cnf(c1409,plain,~r1(skolem0001,X2249)|~r1(X2249,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2249)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0001,skolem0002(X2249,skolem0013,skolem0001))|r1(skolem0013,skolem0004(X2249,skolem0013)),inference(factor,[status(thm)],[c480])).
% 13.26/13.55 cnf(c476,plain,~r1(skolem0001,X1946)|~r1(X1946,skolem0001)|~r1(skolem0001,X1944)|~r1(X1944,X1945)|p1(X1945)|~p1(X1944)|p1(X1946)|~p1(skolem0001)|r1(X1944,skolem0002(X1946,skolem0001,X1944))|r1(skolem0001,skolem0004(X1946,skolem0001)),inference(factor,[status(thm)],[c66])).
% 13.26/13.55 cnf(c1370,plain,~r1(skolem0001,X2244)|~r1(X2244,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X2244)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2244,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2244,skolem0001)),inference(resolution,[status(thm)],[c476, c56])).
% 13.26/13.55 cnf(c1472,plain,~r1(skolem0001,X2245)|~r1(X2245,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X2245)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2245,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2245,skolem0001)),inference(resolution,[status(thm)],[c1370, c55])).
% 13.26/13.55 cnf(c1032,plain,~r1(skolem0001,X2227)|~r1(X2227,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X2228)|p1(X2228)|~p1(skolem0001)|r1(skolem0002(X2227,skolem0001,skolem0013),skolem0003(X2227,skolem0001,skolem0013))|p1(skolem0004(X2227,skolem0001)),inference(factor,[status(thm)],[c203])).
% 13.26/13.55 cnf(c1465,plain,~r1(skolem0001,X2233)|~r1(X2233,skolem0001)|~r1(skolem0001,skolem0001)|p1(X2233)|~p1(skolem0001)|r1(skolem0002(X2233,skolem0001,skolem0013),skolem0003(X2233,skolem0001,skolem0013))|p1(skolem0004(X2233,skolem0001)),inference(factor,[status(thm)],[c1032])).
% 13.26/13.55 cnf(c202,plain,~r1(skolem0001,X1212)|~r1(X1212,skolem0013)|~r1(skolem0013,X1210)|~r1(X1210,X1209)|p1(X1209)|~p1(X1210)|~r1(skolem0013,X1211)|p1(X1211)|~p1(skolem0013)|r1(skolem0002(X1212,skolem0013,skolem0014),skolem0003(X1212,skolem0013,skolem0014))|p1(skolem0004(X1212,skolem0013)),inference(resolution,[status(thm)],[c17, c56])).
% 13.26/13.55 cnf(c1025,plain,~r1(skolem0001,X2223)|~r1(X2223,skolem0013)|~r1(skolem0013,skolem0013)|~r1(skolem0013,X2224)|p1(X2224)|~p1(skolem0013)|r1(skolem0002(X2223,skolem0013,skolem0014),skolem0003(X2223,skolem0013,skolem0014))|p1(skolem0004(X2223,skolem0013)),inference(factor,[status(thm)],[c202])).
% 13.26/13.55 cnf(c28,negated_conjecture,~r1(skolem0001,X310)|~r1(X310,X313)|~r1(X313,X311)|~r1(X311,X314)|p1(X314)|~p1(X311)|~r1(X313,X312)|p1(X312)|~p1(X313)|~r1(X313,X315)|p1(skolem0002(X310,X313,X315))|r1(X313,skolem0004(X310,X313)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.55 cnf(c270,plain,~r1(skolem0001,X1094)|~r1(X1094,X1091)|~r1(X1091,X1093)|~r1(X1093,X1092)|p1(X1092)|~p1(X1093)|~r1(X1091,X1095)|p1(X1095)|~p1(X1091)|p1(skolem0002(X1094,X1091,X1095))|r1(X1091,skolem0004(X1094,X1091)),inference(factor,[status(thm)],[c28])).
% 13.26/13.55 cnf(c948,plain,~r1(skolem0001,X2206)|~r1(X2206,skolem0001)|~r1(skolem0001,X2205)|~r1(X2205,X2207)|p1(X2207)|~p1(X2205)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X2206,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2206,skolem0001)),inference(resolution,[status(thm)],[c270, c55])).
% 13.26/13.55 cnf(c947,plain,~r1(skolem0001,X2189)|~r1(X2189,skolem0013)|~r1(skolem0013,X2188)|~r1(X2188,X2190)|p1(X2190)|~p1(X2188)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X2189,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X2189,skolem0013)),inference(resolution,[status(thm)],[c270, c56])).
% 13.26/13.55 cnf(c1450,plain,~r1(skolem0001,X2198)|~r1(X2198,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2198)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X2198,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X2198,skolem0013)),inference(factor,[status(thm)],[c947])).
% 13.26/13.55 cnf(c890,plain,~r1(skolem0001,X2176)|~r1(X2176,skolem0001)|~r1(skolem0001,skolem0001)|p1(X2176)|~p1(skolem0001)|r1(skolem0002(X2176,skolem0001,skolem0001),skolem0003(X2176,skolem0001,skolem0001))|r1(skolem0004(X2176,skolem0001),skolem0005(X2176,skolem0001)),inference(factor,[status(thm)],[c886])).
% 13.26/13.55 cnf(c772,plain,~r1(skolem0001,X2155)|~r1(X2155,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X2154)|p1(X2154)|~p1(skolem0001)|r1(skolem0002(X2155,skolem0001,X2155),skolem0003(X2155,skolem0001,X2155))|r1(skolem0001,skolem0004(X2155,skolem0001)),inference(factor,[status(thm)],[c153])).
% 13.26/13.55 cnf(c1445,plain,~r1(skolem0001,X2160)|~r1(X2160,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X2160,skolem0001,X2160),skolem0003(X2160,skolem0001,X2160))|r1(skolem0001,skolem0004(X2160,skolem0001)),inference(resolution,[status(thm)],[c772, c55])).
% 13.26/13.55 cnf(c10,negated_conjecture,~r1(skolem0001,X81)|~r1(X81,X84)|~r1(X84,X82)|~r1(X82,X85)|p1(X85)|~p1(X82)|~r1(X84,X83)|p1(X83)|~p1(X84)|~r1(X84,X86)|r1(X86,skolem0002(X81,X84,X86))|p1(skolem0004(X81,X84)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.55 cnf(c113,plain,~r1(skolem0001,X700)|~r1(X700,X697)|~r1(X697,X699)|~r1(X699,X698)|p1(X698)|~p1(X699)|~r1(X697,X701)|p1(X701)|~p1(X697)|r1(X701,skolem0002(X700,X697,X701))|p1(skolem0004(X700,X697)),inference(factor,[status(thm)],[c10])).
% 13.26/13.55 cnf(c675,plain,~r1(skolem0001,X2134)|~r1(X2134,skolem0001)|~r1(skolem0001,X2133)|~r1(X2133,X2132)|p1(X2132)|~p1(X2133)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2134,skolem0001,skolem0013))|p1(skolem0004(X2134,skolem0001)),inference(resolution,[status(thm)],[c113, c55])).
% 13.26/13.55 cnf(c674,plain,~r1(skolem0001,X2121)|~r1(X2121,skolem0013)|~r1(skolem0013,X2120)|~r1(X2120,X2119)|p1(X2119)|~p1(X2120)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(X2121,skolem0013,skolem0014))|p1(skolem0004(X2121,skolem0013)),inference(resolution,[status(thm)],[c113, c56])).
% 13.26/13.55 cnf(c1430,plain,~r1(skolem0001,X2129)|~r1(X2129,skolem0013)|~r1(skolem0013,skolem0001)|p1(X2129)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(X2129,skolem0013,skolem0014))|p1(skolem0004(X2129,skolem0013)),inference(factor,[status(thm)],[c674])).
% 13.26/13.55 cnf(c84,plain,~r1(skolem0001,X629)|~r1(X629,skolem0013)|~r1(skolem0013,X630)|~r1(X630,X628)|p1(X628)|~p1(X630)|~r1(skolem0013,X627)|p1(X627)|~p1(skolem0013)|r1(skolem0014,skolem0002(X629,skolem0013,skolem0014))|r1(skolem0004(X629,skolem0013),skolem0005(X629,skolem0013)),inference(resolution,[status(thm)],[c8, c56])).
% 13.26/13.55 cnf(c610,plain,~r1(skolem0001,X2111)|~r1(X2111,skolem0013)|~r1(skolem0013,skolem0013)|~r1(skolem0013,X2112)|p1(X2112)|~p1(skolem0013)|r1(skolem0014,skolem0002(X2111,skolem0013,skolem0014))|r1(skolem0004(X2111,skolem0013),skolem0005(X2111,skolem0013)),inference(factor,[status(thm)],[c84])).
% 13.26/13.55 cnf(c588,plain,~r1(skolem0001,X2105)|~r1(X2105,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X2106)|p1(X2106)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2105,skolem0001,skolem0013))|r1(skolem0004(X2105,skolem0001),skolem0005(X2105,skolem0001)),inference(factor,[status(thm)],[c81])).
% 13.26/13.55 cnf(c1421,plain,~r1(skolem0001,X2107)|~r1(X2107,skolem0001)|~r1(skolem0001,skolem0001)|p1(X2107)|~p1(skolem0001)|r1(skolem0013,skolem0002(X2107,skolem0001,skolem0013))|r1(skolem0004(X2107,skolem0001),skolem0005(X2107,skolem0001)),inference(factor,[status(thm)],[c588])).
% 13.26/13.55 cnf(c481,plain,~r1(skolem0001,X2091)|~r1(X2091,skolem0001)|~r1(skolem0001,X2089)|~r1(X2089,X2090)|p1(X2090)|~p1(X2089)|p1(skolem0013)|~p1(skolem0001)|r1(X2089,skolem0002(X2091,skolem0001,X2089))|r1(skolem0001,skolem0004(X2091,skolem0001)),inference(resolution,[status(thm)],[c66, c55])).
% 13.26/13.55 cnf(c64,plain,~r1(skolem0001,X465)|~r1(X465,skolem0001)|~r1(skolem0001,X467)|~r1(X467,X466)|p1(X466)|~p1(X467)|~r1(skolem0001,X464)|p1(X464)|~p1(skolem0001)|r1(X465,skolem0002(X465,skolem0001,X465))|r1(skolem0001,skolem0004(X465,skolem0001)),inference(factor,[status(thm)],[c7])).
% 13.26/13.55 cnf(c461,plain,~r1(skolem0001,X2065)|~r1(X2065,skolem0001)|~r1(skolem0001,X2067)|~r1(X2067,X2066)|p1(X2066)|~p1(X2067)|p1(skolem0013)|~p1(skolem0001)|r1(X2065,skolem0002(X2065,skolem0001,X2065))|r1(skolem0001,skolem0004(X2065,skolem0001)),inference(resolution,[status(thm)],[c64, c55])).
% 13.26/13.55 cnf(c273,plain,~r1(skolem0001,X1548)|~r1(X1548,skolem0001)|~r1(skolem0001,X1549)|~r1(X1549,X1546)|p1(X1546)|~p1(X1549)|~r1(skolem0001,X1547)|p1(X1547)|~p1(skolem0001)|p1(skolem0002(X1548,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X1548,skolem0001)),inference(resolution,[status(thm)],[c28, c55])).
% 13.26/13.55 cnf(c1154,plain,~r1(skolem0001,X2030)|~r1(X2030,skolem0001)|~r1(skolem0001,X2029)|~r1(X2029,X2028)|p1(X2028)|~p1(X2029)|p1(X2030)|~p1(skolem0001)|p1(skolem0002(X2030,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X2030,skolem0001)),inference(factor,[status(thm)],[c273])).
% 13.26/13.55 cnf(c266,plain,~r1(skolem0001,X1525)|~r1(X1525,skolem0001)|~r1(skolem0001,X1524)|~r1(X1524,X1522)|p1(X1522)|~p1(X1524)|~r1(skolem0001,X1523)|p1(X1523)|~p1(skolem0001)|p1(skolem0002(X1525,skolem0001,X1525))|r1(skolem0001,skolem0004(X1525,skolem0001)),inference(factor,[status(thm)],[c28])).
% 13.26/13.55 cnf(c1137,plain,~r1(skolem0001,X2008)|~r1(X2008,skolem0001)|~r1(skolem0001,X2009)|~r1(X2009,X2010)|p1(X2010)|~p1(X2009)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X2008,skolem0001,X2008))|r1(skolem0001,skolem0004(X2008,skolem0001)),inference(resolution,[status(thm)],[c266, c55])).
% 13.26/13.55 cnf(c268,plain,~r1(skolem0001,X1060)|~r1(X1060,X1057)|~r1(X1057,X1061)|~r1(X1061,X1058)|p1(X1058)|~p1(X1061)|~r1(X1057,X1059)|p1(X1059)|~p1(X1057)|p1(skolem0002(X1060,X1057,X1061))|r1(X1057,skolem0004(X1060,X1057)),inference(factor,[status(thm)],[c28])).
% 13.26/13.55 cnf(c921,plain,~r1(skolem0001,X1994)|~r1(X1994,skolem0001)|~r1(skolem0001,X1996)|~r1(X1996,X1995)|p1(X1995)|~p1(X1996)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X1994,skolem0001,X1996))|r1(skolem0001,skolem0004(X1994,skolem0001)),inference(resolution,[status(thm)],[c268, c55])).
% 13.26/13.55 cnf(c920,plain,~r1(skolem0001,X1985)|~r1(X1985,skolem0013)|~r1(skolem0013,X1987)|~r1(X1987,X1986)|p1(X1986)|~p1(X1987)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X1985,skolem0013,X1987))|r1(skolem0013,skolem0004(X1985,skolem0013)),inference(resolution,[status(thm)],[c268, c56])).
% 13.26/13.55 cnf(c1379,plain,~r1(skolem0001,X1993)|~r1(X1993,skolem0013)|~r1(skolem0013,skolem0001)|p1(X1993)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X1993,skolem0013,skolem0001))|r1(skolem0013,skolem0004(X1993,skolem0013)),inference(factor,[status(thm)],[c920])).
% 13.26/13.55 cnf(c116,plain,~r1(skolem0001,X736)|~r1(X736,skolem0001)|~r1(skolem0001,X737)|~r1(X737,X738)|p1(X738)|~p1(X737)|~r1(skolem0001,X739)|p1(X739)|~p1(skolem0001)|r1(skolem0013,skolem0002(X736,skolem0001,skolem0013))|p1(skolem0004(X736,skolem0001)),inference(resolution,[status(thm)],[c10, c55])).
% 13.26/13.55 cnf(c684,plain,~r1(skolem0001,X1971)|~r1(X1971,skolem0001)|~r1(skolem0001,X1972)|~r1(X1972,X1973)|p1(X1973)|~p1(X1972)|p1(X1971)|~p1(skolem0001)|r1(skolem0013,skolem0002(X1971,skolem0001,skolem0013))|p1(skolem0004(X1971,skolem0001)),inference(factor,[status(thm)],[c116])).
% 13.26/13.55 cnf(c457,plain,~r1(skolem0001,X1927)|~r1(X1927,skolem0001)|~r1(skolem0001,X1926)|~r1(X1926,X1928)|p1(X1928)|~p1(X1926)|p1(X1927)|~p1(skolem0001)|r1(X1927,skolem0002(X1927,skolem0001,X1927))|r1(skolem0001,skolem0004(X1927,skolem0001)),inference(factor,[status(thm)],[c64])).
% 13.26/13.55 cnf(c1361,plain,~r1(skolem0001,X1934)|~r1(X1934,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X1934)|~p1(skolem0001)|r1(X1934,skolem0002(X1934,skolem0001,X1934))|r1(skolem0001,skolem0004(X1934,skolem0001)),inference(resolution,[status(thm)],[c457, c56])).
% 13.26/13.55 cnf(c1365,plain,~r1(skolem0001,X1935)|~r1(X1935,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X1935)|~p1(skolem0001)|r1(X1935,skolem0002(X1935,skolem0001,X1935))|r1(skolem0001,skolem0004(X1935,skolem0001)),inference(resolution,[status(thm)],[c1361, c55])).
% 13.26/13.55 cnf(c916,plain,~r1(skolem0001,X1837)|~r1(X1837,skolem0001)|~r1(skolem0001,X1835)|~r1(X1835,X1836)|p1(X1836)|~p1(X1835)|p1(X1837)|~p1(skolem0001)|p1(skolem0002(X1837,skolem0001,X1835))|r1(skolem0001,skolem0004(X1837,skolem0001)),inference(factor,[status(thm)],[c268])).
% 13.26/13.55 cnf(c1318,plain,~r1(skolem0001,X1915)|~r1(X1915,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X1915)|~p1(skolem0001)|p1(skolem0002(X1915,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X1915,skolem0001)),inference(resolution,[status(thm)],[c916, c56])).
% 13.26/13.55 cnf(c1356,plain,~r1(skolem0001,X1916)|~r1(X1916,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X1916)|~p1(skolem0001)|p1(skolem0002(X1916,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X1916,skolem0001)),inference(resolution,[status(thm)],[c1318, c55])).
% 13.26/13.55 cnf(c1241,plain,~r1(skolem0001,X1903)|~r1(X1903,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X1902)|p1(X1902)|~p1(skolem0001)|p1(skolem0002(X1903,skolem0001,skolem0013))|r1(skolem0004(X1903,skolem0001),skolem0005(X1903,skolem0001)),inference(factor,[status(thm)],[c301])).
% 13.26/13.55 cnf(c1349,plain,~r1(skolem0001,X1906)|~r1(X1906,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1906)|~p1(skolem0001)|p1(skolem0002(X1906,skolem0001,skolem0013))|r1(skolem0004(X1906,skolem0001),skolem0005(X1906,skolem0001)),inference(factor,[status(thm)],[c1241])).
% 13.26/13.55 cnf(c300,plain,~r1(skolem0001,X1640)|~r1(X1640,skolem0013)|~r1(skolem0013,X1639)|~r1(X1639,X1642)|p1(X1642)|~p1(X1639)|~r1(skolem0013,X1641)|p1(X1641)|~p1(skolem0013)|p1(skolem0002(X1640,skolem0013,skolem0014))|r1(skolem0004(X1640,skolem0013),skolem0005(X1640,skolem0013)),inference(resolution,[status(thm)],[c29, c56])).
% 13.26/13.55 cnf(c1236,plain,~r1(skolem0001,X1898)|~r1(X1898,skolem0013)|~r1(skolem0013,skolem0013)|~r1(skolem0013,X1897)|p1(X1897)|~p1(skolem0013)|p1(skolem0002(X1898,skolem0013,skolem0014))|r1(skolem0004(X1898,skolem0013),skolem0005(X1898,skolem0013)),inference(factor,[status(thm)],[c300])).
% 13.26/13.55 cnf(c111,plain,~r1(skolem0001,X689)|~r1(X689,X685)|~r1(X685,X688)|~r1(X688,X686)|p1(X686)|~p1(X688)|~r1(X685,X687)|p1(X687)|~p1(X685)|r1(X688,skolem0002(X689,X685,X688))|p1(skolem0004(X689,X685)),inference(factor,[status(thm)],[c10])).
% 13.26/13.55 cnf(c659,plain,~r1(skolem0001,X1585)|~r1(X1585,skolem0013)|~r1(skolem0013,X1586)|~r1(X1586,X1584)|p1(X1584)|~p1(X1586)|p1(skolem0014)|~p1(skolem0013)|r1(X1586,skolem0002(X1585,skolem0013,X1586))|p1(skolem0004(X1585,skolem0013)),inference(resolution,[status(thm)],[c111, c56])).
% 13.26/13.55 cnf(c1174,plain,~r1(skolem0001,X1896)|~r1(X1896,skolem0013)|~r1(skolem0013,skolem0001)|p1(X1896)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0001,skolem0002(X1896,skolem0013,skolem0001))|p1(skolem0004(X1896,skolem0013)),inference(factor,[status(thm)],[c659])).
% 13.26/13.55 cnf(c655,plain,~r1(skolem0001,X1413)|~r1(X1413,skolem0001)|~r1(skolem0001,X1414)|~r1(X1414,X1412)|p1(X1412)|~p1(X1414)|p1(X1413)|~p1(skolem0001)|r1(X1414,skolem0002(X1413,skolem0001,X1414))|p1(skolem0004(X1413,skolem0001)),inference(factor,[status(thm)],[c111])).
% 13.26/13.55 cnf(c1101,plain,~r1(skolem0001,X1878)|~r1(X1878,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X1878)|~p1(skolem0001)|r1(skolem0013,skolem0002(X1878,skolem0001,skolem0013))|p1(skolem0004(X1878,skolem0001)),inference(resolution,[status(thm)],[c655, c56])).
% 13.26/13.55 cnf(c1344,plain,~r1(skolem0001,X1880)|~r1(X1880,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X1880)|~p1(skolem0001)|r1(skolem0013,skolem0002(X1880,skolem0001,skolem0013))|p1(skolem0004(X1880,skolem0001)),inference(resolution,[status(thm)],[c1101, c55])).
% 13.26/13.55 cnf(c971,plain,~r1(skolem0001,X1866)|~r1(X1866,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X1867)|p1(X1867)|~p1(skolem0001)|r1(skolem0002(X1866,skolem0001,X1866),skolem0003(X1866,skolem0001,X1866))|p1(skolem0004(X1866,skolem0001)),inference(factor,[status(thm)],[c196])).
% 13.26/13.55 cnf(c1335,plain,~r1(skolem0001,X1877)|~r1(X1877,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X1877,skolem0001,X1877),skolem0003(X1877,skolem0001,X1877))|p1(skolem0004(X1877,skolem0001)),inference(resolution,[status(thm)],[c971, c55])).
% 13.26/13.55 cnf(c351,plain,~r1(skolem0001,X1875)|~r1(X1875,X1872)|~r1(X1872,X1873)|~r1(X1873,X1871)|p1(X1871)|~p1(X1873)|~r1(X1872,X1870)|p1(X1870)|~p1(X1872)|~r1(X1872,X1869)|p1(skolem0002(X1875,X1872,X1869))|~r1(skolem0004(X1875,X1872),X1874)|~r1(X1874,skolem0004(X1875,X1872))|p1(X1874)|~p1(skolem0004(X1875,X1872)),inference(factor,[status(thm)],[c34])).
% 13.26/13.55 cnf(c943,plain,~r1(skolem0001,X1843)|~r1(X1843,skolem0001)|~r1(skolem0001,X1842)|~r1(X1842,X1844)|p1(X1844)|~p1(X1842)|p1(X1843)|~p1(skolem0001)|p1(skolem0002(X1843,skolem0001,X1843))|r1(skolem0001,skolem0004(X1843,skolem0001)),inference(factor,[status(thm)],[c270])).
% 13.26/13.55 cnf(c1324,plain,~r1(skolem0001,X1856)|~r1(X1856,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X1856)|~p1(skolem0001)|p1(skolem0002(X1856,skolem0001,X1856))|r1(skolem0001,skolem0004(X1856,skolem0001)),inference(resolution,[status(thm)],[c943, c56])).
% 13.26/13.55 cnf(c1330,plain,~r1(skolem0001,X1857)|~r1(X1857,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X1857)|~p1(skolem0001)|p1(skolem0002(X1857,skolem0001,X1857))|r1(skolem0001,skolem0004(X1857,skolem0001)),inference(resolution,[status(thm)],[c1324, c55])).
% 13.26/13.55 cnf(c903,plain,~r1(skolem0001,X1832)|~r1(X1832,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1832)|~p1(skolem0001)|r1(skolem0002(X1832,skolem0001,X1832),skolem0003(X1832,skolem0001,X1832))|r1(skolem0004(X1832,skolem0001),skolem0005(X1832,skolem0001)),inference(factor,[status(thm)],[c899])).
% 13.26/13.55 cnf(c332,plain,~r1(skolem0001,X1825)|~r1(X1825,X1821)|~r1(X1821,X1819)|~r1(X1819,X1822)|p1(X1822)|~p1(X1819)|~r1(X1821,X1824)|p1(X1824)|~p1(X1821)|~r1(X1821,X1826)|p1(skolem0002(X1825,X1821,X1826))|~r1(skolem0004(X1825,X1821),X1823)|~r1(X1823,skolem0006(X1825,X1821,X1823))|~r1(skolem0006(X1825,X1821,X1823),X1820)|p1(X1820)|~p1(skolem0006(X1825,X1821,X1823)),inference(factor,[status(thm)],[c33])).
% 13.26/13.55 cnf(c156,plain,~r1(skolem0001,X935)|~r1(X935,X933)|~r1(X933,X933)|~r1(X933,X934)|p1(X934)|~p1(X933)|~r1(X933,X932)|p1(X932)|r1(skolem0002(X935,X933,X934),skolem0003(X935,X933,X934))|r1(X933,skolem0004(X935,X933)),inference(factor,[status(thm)],[c14])).
% 13.26/13.55 cnf(c809,plain,~r1(skolem0001,X940)|~r1(X940,X942)|~r1(X942,X942)|~r1(X942,X941)|p1(X941)|~p1(X942)|r1(skolem0002(X940,X942,X941),skolem0003(X940,X942,X941))|r1(X942,skolem0004(X940,X942)),inference(factor,[status(thm)],[c156])).
% 13.26/13.55 cnf(c817,plain,~r1(skolem0001,X1818)|~r1(X1818,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X1818,skolem0001,skolem0013),skolem0003(X1818,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X1818,skolem0001)),inference(resolution,[status(thm)],[c809, c55])).
% 13.26/13.55 cnf(c1310,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(skolem0001,skolem0001,skolem0013),skolem0003(skolem0001,skolem0001,skolem0013))|r1(skolem0001,skolem0004(skolem0001,skolem0001)),inference(factor,[status(thm)],[c817])).
% 13.26/13.55 cnf(c816,plain,~r1(skolem0001,X1817)|~r1(X1817,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X1817,skolem0013,skolem0014),skolem0003(X1817,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X1817,skolem0013)),inference(resolution,[status(thm)],[c809, c56])).
% 13.26/13.55 cnf(c1309,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(skolem0013,skolem0013,skolem0014),skolem0003(skolem0013,skolem0013,skolem0014))|r1(skolem0013,skolem0004(skolem0013,skolem0013)),inference(factor,[status(thm)],[c816])).
% 13.26/13.55 cnf(c796,plain,~r1(skolem0001,X929)|~r1(X929,X930)|~r1(X930,X930)|~r1(X930,X928)|p1(X928)|~p1(X930)|r1(skolem0002(X929,X930,X930),skolem0003(X929,X930,X930))|r1(X930,skolem0004(X929,X930)),inference(factor,[status(thm)],[c155])).
% 13.26/13.55 cnf(c804,plain,~r1(skolem0001,X1807)|~r1(X1807,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X1807,skolem0001,skolem0001),skolem0003(X1807,skolem0001,skolem0001))|r1(skolem0001,skolem0004(X1807,skolem0001)),inference(resolution,[status(thm)],[c796, c55])).
% 13.26/13.55 cnf(c803,plain,~r1(skolem0001,X1806)|~r1(X1806,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X1806,skolem0013,skolem0013),skolem0003(X1806,skolem0013,skolem0013))|r1(skolem0013,skolem0004(X1806,skolem0013)),inference(resolution,[status(thm)],[c796, c56])).
% 13.26/13.55 cnf(c32,negated_conjecture,~r1(skolem0001,X364)|~r1(X364,X370)|~r1(X370,X367)|~r1(X367,X371)|p1(X371)|~p1(X367)|~r1(X370,X368)|p1(X368)|~p1(X370)|~r1(X370,X372)|p1(skolem0002(X364,X370,X372))|~r1(skolem0004(X364,X370),X365)|~r1(X365,X366)|~r1(X366,X369)|p1(X369)|~p1(X366)|r1(X365,skolem0006(X364,X370,X365)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.55 cnf(c325,plain,~r1(skolem0001,X1785)|~r1(X1785,X1788)|~r1(X1788,X1786)|~r1(X1786,X1783)|p1(X1783)|~p1(X1786)|~r1(X1788,X1784)|p1(X1784)|~p1(X1788)|~r1(X1788,X1789)|p1(skolem0002(X1785,X1788,X1789))|~r1(skolem0004(X1785,X1788),skolem0004(X1785,X1788))|~r1(skolem0004(X1785,X1788),X1787)|p1(X1787)|~p1(skolem0004(X1785,X1788))|r1(skolem0004(X1785,X1788),skolem0006(X1785,X1788,skolem0004(X1785,X1788))),inference(factor,[status(thm)],[c32])).
% 13.26/13.55 cnf(c31,negated_conjecture,~r1(skolem0001,X352)|~r1(X352,X355)|~r1(X355,X353)|~r1(X353,X356)|p1(X356)|~p1(X353)|~r1(X355,X354)|p1(X354)|~p1(X355)|~r1(X355,X357)|p1(skolem0002(X352,X355,X357))|p1(skolem0004(X352,X355)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.55 cnf(c315,plain,~r1(skolem0001,X1742)|~r1(X1742,skolem0001)|~r1(skolem0001,X1740)|~r1(X1740,X1741)|p1(X1741)|~p1(X1740)|~r1(skolem0001,X1739)|p1(X1739)|~p1(skolem0001)|p1(skolem0002(X1742,skolem0001,skolem0013))|p1(skolem0004(X1742,skolem0001)),inference(resolution,[status(thm)],[c31, c55])).
% 13.26/13.55 cnf(c1273,plain,~r1(skolem0001,X1779)|~r1(X1779,skolem0001)|~r1(skolem0001,X1778)|~r1(X1778,X1777)|p1(X1777)|~p1(X1778)|p1(X1779)|~p1(skolem0001)|p1(skolem0002(X1779,skolem0001,skolem0013))|p1(skolem0004(X1779,skolem0001)),inference(factor,[status(thm)],[c315])).
% 13.26/13.55 cnf(c308,plain,~r1(skolem0001,X1711)|~r1(X1711,skolem0001)|~r1(skolem0001,X1710)|~r1(X1710,X1712)|p1(X1712)|~p1(X1710)|~r1(skolem0001,X1709)|p1(X1709)|~p1(skolem0001)|p1(skolem0002(X1711,skolem0001,X1711))|p1(skolem0004(X1711,skolem0001)),inference(factor,[status(thm)],[c31])).
% 13.26/13.55 cnf(c1259,plain,~r1(skolem0001,X1755)|~r1(X1755,skolem0001)|~r1(skolem0001,X1756)|~r1(X1756,X1754)|p1(X1754)|~p1(X1756)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X1755,skolem0001,X1755))|p1(skolem0004(X1755,skolem0001)),inference(resolution,[status(thm)],[c308, c55])).
% 13.26/13.55 cnf(c1276,plain,~r1(skolem0001,X1743)|~r1(X1743,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X1744)|p1(X1744)|~p1(skolem0001)|p1(skolem0002(X1743,skolem0001,skolem0013))|p1(skolem0004(X1743,skolem0001)),inference(factor,[status(thm)],[c315])).
% 13.26/13.55 cnf(c1278,plain,~r1(skolem0001,X1745)|~r1(X1745,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1745)|~p1(skolem0001)|p1(skolem0002(X1745,skolem0001,skolem0013))|p1(skolem0004(X1745,skolem0001)),inference(factor,[status(thm)],[c1276])).
% 13.26/13.55 cnf(c314,plain,~r1(skolem0001,X1733)|~r1(X1733,skolem0013)|~r1(skolem0013,X1731)|~r1(X1731,X1732)|p1(X1732)|~p1(X1731)|~r1(skolem0013,X1730)|p1(X1730)|~p1(skolem0013)|p1(skolem0002(X1733,skolem0013,skolem0014))|p1(skolem0004(X1733,skolem0013)),inference(resolution,[status(thm)],[c31, c56])).
% 13.26/13.55 cnf(c1268,plain,~r1(skolem0001,X1734)|~r1(X1734,skolem0013)|~r1(skolem0013,skolem0013)|~r1(skolem0013,X1735)|p1(X1735)|~p1(skolem0013)|p1(skolem0002(X1734,skolem0013,skolem0014))|p1(skolem0004(X1734,skolem0013)),inference(factor,[status(thm)],[c314])).
% 13.26/13.55 cnf(c1258,plain,~r1(skolem0001,X1714)|~r1(X1714,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X1713)|p1(X1713)|~p1(skolem0001)|p1(skolem0002(X1714,skolem0001,X1714))|p1(skolem0004(X1714,skolem0001)),inference(factor,[status(thm)],[c308])).
% 13.26/13.55 cnf(c1263,plain,~r1(skolem0001,X1717)|~r1(X1717,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X1717,skolem0001,X1717))|p1(skolem0004(X1717,skolem0001)),inference(resolution,[status(thm)],[c1258, c55])).
% 13.26/13.55 cnf(c30,negated_conjecture,~r1(skolem0001,X334)|~r1(X334,X337)|~r1(X337,X335)|~r1(X335,X338)|p1(X338)|~p1(X335)|~r1(X337,X336)|p1(X336)|~p1(X337)|~r1(X337,X339)|p1(skolem0002(X334,X337,X339))|~p1(skolem0005(X334,X337)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.55 cnf(c306,plain,~r1(skolem0001,X1702)|~r1(X1702,X1700)|~r1(X1700,skolem0005(X1702,X1700))|~r1(skolem0005(X1702,X1700),X1703)|p1(X1703)|~p1(skolem0005(X1702,X1700))|~r1(X1700,X1701)|p1(X1701)|~p1(X1700)|~r1(X1700,X1699)|p1(skolem0002(X1702,X1700,X1699)),inference(factor,[status(thm)],[c30])).
% 13.26/13.55 cnf(c312,plain,~r1(skolem0001,X911)|~r1(X911,X912)|~r1(X912,X908)|~r1(X908,X909)|p1(X909)|~p1(X908)|~r1(X912,X910)|p1(X910)|~p1(X912)|p1(skolem0002(X911,X912,X910))|p1(skolem0004(X911,X912)),inference(factor,[status(thm)],[c31])).
% 13.26/13.55 cnf(c791,plain,~r1(skolem0001,X1698)|~r1(X1698,skolem0001)|~r1(skolem0001,X1696)|~r1(X1696,X1697)|p1(X1697)|~p1(X1696)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X1698,skolem0001,skolem0013))|p1(skolem0004(X1698,skolem0001)),inference(resolution,[status(thm)],[c312, c55])).
% 13.26/13.55 cnf(c790,plain,~r1(skolem0001,X1685)|~r1(X1685,skolem0013)|~r1(skolem0013,X1683)|~r1(X1683,X1684)|p1(X1684)|~p1(X1683)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X1685,skolem0013,skolem0014))|p1(skolem0004(X1685,skolem0013)),inference(resolution,[status(thm)],[c312, c56])).
% 13.26/13.55 cnf(c1243,plain,~r1(skolem0001,X1693)|~r1(X1693,skolem0013)|~r1(skolem0013,skolem0001)|p1(X1693)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X1693,skolem0013,skolem0014))|p1(skolem0004(X1693,skolem0013)),inference(factor,[status(thm)],[c790])).
% 13.26/13.55 cnf(c1212,plain,~r1(skolem0001,X1618)|~r1(X1618,X1619)|~r1(X1619,X1619)|~r1(X1619,X1620)|p1(X1620)|~p1(X1619)|p1(skolem0002(X1618,X1619,X1619))|r1(skolem0004(X1618,X1619),skolem0005(X1618,X1619)),inference(factor,[status(thm)],[c296])).
% 13.26/13.55 cnf(c1220,plain,~r1(skolem0001,X1638)|~r1(X1638,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X1638,skolem0001,skolem0001))|r1(skolem0004(X1638,skolem0001),skolem0005(X1638,skolem0001)),inference(resolution,[status(thm)],[c1212, c55])).
% 13.26/13.55 cnf(c1219,plain,~r1(skolem0001,X1637)|~r1(X1637,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X1637,skolem0013,skolem0013))|r1(skolem0004(X1637,skolem0013),skolem0005(X1637,skolem0013)),inference(resolution,[status(thm)],[c1212, c56])).
% 13.26/13.55 cnf(c1216,plain,~r1(skolem0001,X1632)|~r1(X1632,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1632)|~p1(skolem0001)|p1(skolem0002(X1632,skolem0001,skolem0001))|r1(skolem0004(X1632,skolem0001),skolem0005(X1632,skolem0001)),inference(factor,[status(thm)],[c1212])).
% 13.26/13.55 cnf(c295,plain,~r1(skolem0001,X1607)|~r1(X1607,X1607)|~r1(X1607,X1606)|~r1(X1606,X1608)|p1(X1608)|~p1(X1606)|~r1(X1607,X1609)|p1(X1609)|~p1(X1607)|p1(skolem0002(X1607,X1607,X1607))|r1(skolem0004(X1607,X1607),skolem0005(X1607,X1607)),inference(factor,[status(thm)],[c29])).
% 13.26/13.55 cnf(c1200,plain,~r1(skolem0001,X1611)|~r1(X1611,X1611)|~r1(X1611,X1610)|p1(X1610)|~p1(X1611)|p1(skolem0002(X1611,X1611,X1611))|r1(skolem0004(X1611,X1611),skolem0005(X1611,X1611)),inference(factor,[status(thm)],[c295])).
% 13.26/13.55 cnf(c1206,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(skolem0013,skolem0013,skolem0013))|r1(skolem0004(skolem0013,skolem0013),skolem0005(skolem0013,skolem0013)),inference(resolution,[status(thm)],[c1200, c56])).
% 13.26/13.55 cnf(c1189,plain,~r1(skolem0001,X1601)|~r1(X1601,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X1602)|p1(X1602)|~p1(skolem0001)|p1(skolem0002(X1601,skolem0001,X1601))|r1(skolem0004(X1601,skolem0001),skolem0005(X1601,skolem0001)),inference(factor,[status(thm)],[c294])).
% 13.26/13.55 cnf(c1194,plain,~r1(skolem0001,X1605)|~r1(X1605,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X1605,skolem0001,X1605))|r1(skolem0004(X1605,skolem0001),skolem0005(X1605,skolem0001)),inference(resolution,[status(thm)],[c1189, c55])).
% 13.26/13.55 cnf(c1195,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(skolem0001,skolem0001,skolem0001))|r1(skolem0004(skolem0001,skolem0001),skolem0005(skolem0001,skolem0001)),inference(factor,[status(thm)],[c1194])).
% 13.26/13.55 cnf(c660,plain,~r1(skolem0001,X1591)|~r1(X1591,skolem0001)|~r1(skolem0001,X1592)|~r1(X1592,X1590)|p1(X1590)|~p1(X1592)|p1(skolem0013)|~p1(skolem0001)|r1(X1592,skolem0002(X1591,skolem0001,X1592))|p1(skolem0004(X1591,skolem0001)),inference(resolution,[status(thm)],[c111, c55])).
% 13.26/13.55 cnf(c109,plain,~r1(skolem0001,X674)|~r1(X674,skolem0001)|~r1(skolem0001,X672)|~r1(X672,X675)|p1(X675)|~p1(X672)|~r1(skolem0001,X673)|p1(X673)|~p1(skolem0001)|r1(X674,skolem0002(X674,skolem0001,X674))|p1(skolem0004(X674,skolem0001)),inference(factor,[status(thm)],[c10])).
% 13.26/13.55 cnf(c640,plain,~r1(skolem0001,X1569)|~r1(X1569,skolem0001)|~r1(skolem0001,X1571)|~r1(X1571,X1570)|p1(X1570)|~p1(X1571)|p1(skolem0013)|~p1(skolem0001)|r1(X1569,skolem0002(X1569,skolem0001,X1569))|p1(skolem0004(X1569,skolem0001)),inference(resolution,[status(thm)],[c109, c55])).
% 13.26/13.55 cnf(c1157,plain,~r1(skolem0001,X1554)|~r1(X1554,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X1555)|p1(X1555)|~p1(skolem0001)|p1(skolem0002(X1554,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X1554,skolem0001)),inference(factor,[status(thm)],[c273])).
% 13.26/13.55 cnf(c1162,plain,~r1(skolem0001,X1560)|~r1(X1560,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1560)|~p1(skolem0001)|p1(skolem0002(X1560,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X1560,skolem0001)),inference(factor,[status(thm)],[c1157])).
% 13.26/13.55 cnf(c272,plain,~r1(skolem0001,X1541)|~r1(X1541,skolem0013)|~r1(skolem0013,X1542)|~r1(X1542,X1539)|p1(X1539)|~p1(X1542)|~r1(skolem0013,X1540)|p1(X1540)|~p1(skolem0013)|p1(skolem0002(X1541,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X1541,skolem0013)),inference(resolution,[status(thm)],[c28, c56])).
% 13.26/13.55 cnf(c1150,plain,~r1(skolem0001,X1551)|~r1(X1551,skolem0013)|~r1(skolem0013,skolem0013)|~r1(skolem0013,X1550)|p1(X1550)|~p1(skolem0013)|p1(skolem0002(X1551,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X1551,skolem0013)),inference(factor,[status(thm)],[c272])).
% 13.26/13.55 cnf(c535,plain,~r1(skolem0001,X1537)|~r1(X1537,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X1538)|p1(X1538)|~p1(skolem0001)|r1(X1537,skolem0002(X1537,skolem0001,X1537))|r1(skolem0004(X1537,skolem0001),skolem0005(X1537,skolem0001)),inference(factor,[status(thm)],[c76])).
% 13.26/13.55 cnf(c1147,plain,~r1(skolem0001,X1545)|~r1(X1545,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(X1545,skolem0002(X1545,skolem0001,X1545))|r1(skolem0004(X1545,skolem0001),skolem0005(X1545,skolem0001)),inference(resolution,[status(thm)],[c535, c55])).
% 13.26/13.56 cnf(c1136,plain,~r1(skolem0001,X1526)|~r1(X1526,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X1527)|p1(X1527)|~p1(skolem0001)|p1(skolem0002(X1526,skolem0001,X1526))|r1(skolem0001,skolem0004(X1526,skolem0001)),inference(factor,[status(thm)],[c266])).
% 13.26/13.56 cnf(c1141,plain,~r1(skolem0001,X1530)|~r1(X1530,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X1530,skolem0001,X1530))|r1(skolem0001,skolem0004(X1530,skolem0001)),inference(resolution,[status(thm)],[c1136, c55])).
% 13.26/13.56 cnf(c261,plain,~r1(skolem0001,X1510)|~r1(X1510,X1511)|~r1(X1511,X1516)|~r1(X1516,X1512)|p1(X1512)|~p1(X1516)|~r1(X1511,X1514)|p1(X1514)|~p1(X1511)|~r1(X1511,X1515)|~p1(skolem0003(X1510,X1511,X1515))|~r1(skolem0004(X1510,X1511),X1513)|~r1(X1513,skolem0004(X1510,X1511))|p1(X1513)|~p1(skolem0004(X1510,X1511)),inference(factor,[status(thm)],[c27])).
% 13.26/13.56 cnf(c800,plain,~r1(skolem0001,X1491)|~r1(X1491,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1491)|~p1(skolem0001)|r1(skolem0002(X1491,skolem0001,skolem0001),skolem0003(X1491,skolem0001,skolem0001))|r1(skolem0001,skolem0004(X1491,skolem0001)),inference(factor,[status(thm)],[c796])).
% 13.26/13.56 cnf(c154,plain,~r1(skolem0001,X903)|~r1(X903,X903)|~r1(X903,X902)|~r1(X902,X904)|p1(X904)|~p1(X902)|~r1(X903,X901)|p1(X901)|~p1(X903)|r1(skolem0002(X903,X903,X903),skolem0003(X903,X903,X903))|r1(X903,skolem0004(X903,X903)),inference(factor,[status(thm)],[c14])).
% 13.26/13.56 cnf(c777,plain,~r1(skolem0001,X905)|~r1(X905,X905)|~r1(X905,X906)|p1(X906)|~p1(X905)|r1(skolem0002(X905,X905,X905),skolem0003(X905,X905,X905))|r1(X905,skolem0004(X905,X905)),inference(factor,[status(thm)],[c154])).
% 13.26/13.56 cnf(c783,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(skolem0013,skolem0013,skolem0013),skolem0003(skolem0013,skolem0013,skolem0013))|r1(skolem0013,skolem0004(skolem0013,skolem0013)),inference(resolution,[status(thm)],[c777, c56])).
% 13.26/13.56 cnf(c252,plain,~r1(skolem0001,X1463)|~r1(X1463,X1461)|~r1(X1461,X1465)|~r1(X1465,X1460)|p1(X1460)|~p1(X1465)|~r1(X1461,X1466)|p1(X1466)|~p1(X1461)|~r1(X1461,X1464)|~p1(skolem0003(X1463,X1461,X1464))|~r1(skolem0004(X1463,X1461),X1467)|~r1(X1467,skolem0006(X1463,X1461,X1467))|~r1(skolem0006(X1463,X1461,X1467),X1462)|p1(X1462)|~p1(skolem0006(X1463,X1461,X1467)),inference(factor,[status(thm)],[c26])).
% 13.26/13.56 cnf(c310,plain,~r1(skolem0001,X871)|~r1(X871,X872)|~r1(X872,X870)|~r1(X870,X868)|p1(X868)|~p1(X870)|~r1(X872,X869)|p1(X869)|~p1(X872)|p1(skolem0002(X871,X872,X870))|p1(skolem0004(X871,X872)),inference(factor,[status(thm)],[c31])).
% 13.26/13.56 cnf(c751,plain,~r1(skolem0001,X1455)|~r1(X1455,skolem0001)|~r1(skolem0001,X1454)|~r1(X1454,X1453)|p1(X1453)|~p1(X1454)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X1455,skolem0001,X1454))|p1(skolem0004(X1455,skolem0001)),inference(resolution,[status(thm)],[c310, c55])).
% 13.26/13.56 cnf(c750,plain,~r1(skolem0001,X1440)|~r1(X1440,skolem0013)|~r1(skolem0013,X1439)|~r1(X1439,X1438)|p1(X1438)|~p1(X1439)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X1440,skolem0013,X1439))|p1(skolem0004(X1440,skolem0013)),inference(resolution,[status(thm)],[c310, c56])).
% 13.26/13.56 cnf(c1111,plain,~r1(skolem0001,X1444)|~r1(X1444,skolem0013)|~r1(skolem0013,skolem0001)|p1(X1444)|~p1(skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X1444,skolem0013,skolem0001))|p1(skolem0004(X1444,skolem0013)),inference(factor,[status(thm)],[c750])).
% 13.26/13.56 cnf(c25,negated_conjecture,~r1(skolem0001,X268)|~r1(X268,X274)|~r1(X274,X271)|~r1(X271,X275)|p1(X275)|~p1(X271)|~r1(X274,X272)|p1(X272)|~p1(X274)|~r1(X274,X276)|~p1(skolem0003(X268,X274,X276))|~r1(skolem0004(X268,X274),X269)|~r1(X269,X270)|~r1(X270,X273)|p1(X273)|~p1(X270)|r1(X269,skolem0006(X268,X274,X269)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.56 cnf(c246,plain,~r1(skolem0001,X1418)|~r1(X1418,X1422)|~r1(X1422,X1419)|~r1(X1419,X1421)|p1(X1421)|~p1(X1419)|~r1(X1422,X1420)|p1(X1420)|~p1(X1422)|~r1(X1422,X1416)|~p1(skolem0003(X1418,X1422,X1416))|~r1(skolem0004(X1418,X1422),skolem0004(X1418,X1422))|~r1(skolem0004(X1418,X1422),X1417)|p1(X1417)|~p1(skolem0004(X1418,X1422))|r1(skolem0004(X1418,X1422),skolem0006(X1418,X1422,skolem0004(X1418,X1422))),inference(factor,[status(thm)],[c25])).
% 13.26/13.56 cnf(c636,plain,~r1(skolem0001,X1388)|~r1(X1388,skolem0001)|~r1(skolem0001,X1389)|~r1(X1389,X1387)|p1(X1387)|~p1(X1389)|p1(X1388)|~p1(skolem0001)|r1(X1388,skolem0002(X1388,skolem0001,X1388))|p1(skolem0004(X1388,skolem0001)),inference(factor,[status(thm)],[c109])).
% 13.26/13.56 cnf(c1091,plain,~r1(skolem0001,X1399)|~r1(X1399,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X1399)|~p1(skolem0001)|r1(X1399,skolem0002(X1399,skolem0001,X1399))|p1(skolem0004(X1399,skolem0001)),inference(resolution,[status(thm)],[c636, c56])).
% 13.26/13.56 cnf(c1095,plain,~r1(skolem0001,X1400)|~r1(X1400,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X1400)|~p1(skolem0001)|r1(X1400,skolem0002(X1400,skolem0001,X1400))|p1(skolem0004(X1400,skolem0001)),inference(resolution,[status(thm)],[c1091, c55])).
% 13.26/13.56 cnf(c24,negated_conjecture,~r1(skolem0001,X258)|~r1(X258,X261)|~r1(X261,X259)|~r1(X259,X262)|p1(X262)|~p1(X259)|~r1(X261,X260)|p1(X260)|~p1(X261)|~r1(X261,X263)|~p1(skolem0003(X258,X261,X263))|p1(skolem0004(X258,X261)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.56 cnf(c241,plain,~r1(skolem0001,X1394)|~r1(X1394,X1391)|~r1(X1391,skolem0003(X1394,X1391,X1392))|~r1(skolem0003(X1394,X1391,X1392),X1393)|p1(X1393)|~p1(skolem0003(X1394,X1391,X1392))|~r1(X1391,X1395)|p1(X1395)|~p1(X1391)|~r1(X1391,X1392)|p1(skolem0004(X1394,X1391)),inference(factor,[status(thm)],[c24])).
% 13.26/13.56 cnf(c46,negated_conjecture,~r1(skolem0001,X432)|~r1(X432,X433)|~r1(X433,X435)|~r1(X435,X434)|p1(X434)|r1(skolem0010(X432,X433,X435,X434),skolem0011(X432,X433,X435,X434))|r1(X433,skolem0012(X432,X433)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.56 cnf(c434,plain,~r1(skolem0001,X634)|~r1(X634,X633)|~r1(X633,skolem0013)|p1(skolem0014)|r1(skolem0010(X634,X633,skolem0013,skolem0014),skolem0011(X634,X633,skolem0013,skolem0014))|r1(X633,skolem0012(X634,X633)),inference(resolution,[status(thm)],[c46, c56])).
% 13.26/13.56 cnf(c613,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|r1(skolem0010(skolem0013,skolem0013,skolem0013,skolem0014),skolem0011(skolem0013,skolem0013,skolem0013,skolem0014))|r1(skolem0013,skolem0012(skolem0013,skolem0013)),inference(factor,[status(thm)],[c434])).
% 13.26/13.56 cnf(c23,negated_conjecture,~r1(skolem0001,X234)|~r1(X234,X237)|~r1(X237,X235)|~r1(X235,X238)|p1(X238)|~p1(X235)|~r1(X237,X236)|p1(X236)|~p1(X237)|~r1(X237,X239)|~p1(skolem0003(X234,X237,X239))|~p1(skolem0005(X234,X237)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.56 cnf(c225,plain,~r1(skolem0001,X1378)|~r1(X1378,X1375)|~r1(X1375,skolem0003(X1378,X1375,X1377))|~r1(skolem0003(X1378,X1375,X1377),X1376)|p1(X1376)|~p1(skolem0003(X1378,X1375,X1377))|~r1(X1375,X1374)|p1(X1374)|~p1(X1375)|~r1(X1375,X1377)|~p1(skolem0005(X1378,X1375)),inference(factor,[status(thm)],[c23])).
% 13.26/13.56 cnf(c71,plain,~r1(skolem0001,X531)|~r1(X531,skolem0013)|~r1(skolem0013,X533)|~r1(X533,X532)|p1(X532)|~p1(X533)|~r1(skolem0013,X530)|p1(X530)|~p1(skolem0013)|r1(skolem0014,skolem0002(X531,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X531,skolem0013)),inference(resolution,[status(thm)],[c7, c56])).
% 13.26/13.56 cnf(c522,plain,~r1(skolem0001,X1372)|~r1(X1372,skolem0013)|~r1(skolem0013,skolem0013)|~r1(skolem0013,X1373)|p1(X1373)|~p1(skolem0013)|r1(skolem0014,skolem0002(X1372,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X1372,skolem0013)),inference(factor,[status(thm)],[c71])).
% 13.26/13.56 cnf(c22,negated_conjecture,~r1(skolem0001,X222)|~r1(X222,X225)|~r1(X225,X223)|~r1(X223,X226)|p1(X226)|~p1(X223)|~r1(X225,X224)|p1(X224)|~p1(X225)|~r1(X225,X227)|~p1(skolem0003(X222,X225,X227))|r1(skolem0004(X222,X225),skolem0005(X222,X225)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.56 cnf(c223,plain,~r1(skolem0001,X1369)|~r1(X1369,X1367)|~r1(X1367,skolem0003(X1369,X1367,X1365))|~r1(skolem0003(X1369,X1367,X1365),X1366)|p1(X1366)|~p1(skolem0003(X1369,X1367,X1365))|~r1(X1367,X1368)|p1(X1368)|~p1(X1367)|~r1(X1367,X1365)|r1(skolem0004(X1369,X1367),skolem0005(X1369,X1367)),inference(factor,[status(thm)],[c22])).
% 13.26/13.56 cnf(c512,plain,~r1(skolem0001,X1363)|~r1(X1363,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X1362)|p1(X1362)|~p1(skolem0001)|r1(skolem0013,skolem0002(X1363,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X1363,skolem0001)),inference(factor,[status(thm)],[c69])).
% 13.26/13.56 cnf(c1079,plain,~r1(skolem0001,X1364)|~r1(X1364,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1364)|~p1(skolem0001)|r1(skolem0013,skolem0002(X1364,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X1364,skolem0001)),inference(factor,[status(thm)],[c512])).
% 13.26/13.56 cnf(c21,negated_conjecture,~r1(skolem0001,X214)|~r1(X214,X217)|~r1(X217,X215)|~r1(X215,X218)|p1(X218)|~p1(X215)|~r1(X217,X216)|p1(X216)|~p1(X217)|~r1(X217,X219)|~p1(skolem0003(X214,X217,X219))|r1(X217,skolem0004(X214,X217)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.56 cnf(c218,plain,~r1(skolem0001,X1361)|~r1(X1361,X1360)|~r1(X1360,skolem0003(X1361,X1360,X1358))|~r1(skolem0003(X1361,X1360,X1358),X1357)|p1(X1357)|~p1(skolem0003(X1361,X1360,X1358))|~r1(X1360,X1359)|p1(X1359)|~p1(X1360)|~r1(X1360,X1358)|r1(X1360,skolem0004(X1361,X1360)),inference(factor,[status(thm)],[c21])).
% 13.26/13.56 cnf(c430,plain,~r1(skolem0001,X447)|~r1(X447,X446)|~r1(X446,X447)|p1(X446)|r1(skolem0010(X447,X446,X447,X446),skolem0011(X447,X446,X447,X446))|r1(X446,skolem0012(X447,X446)),inference(factor,[status(thm)],[c46])).
% 13.26/13.56 cnf(c448,plain,~r1(skolem0001,skolem0014)|~r1(skolem0014,skolem0013)|p1(skolem0013)|r1(skolem0010(skolem0014,skolem0013,skolem0014,skolem0013),skolem0011(skolem0014,skolem0013,skolem0014,skolem0013))|r1(skolem0013,skolem0012(skolem0014,skolem0013)),inference(resolution,[status(thm)],[c430, c56])).
% 13.26/13.56 cnf(c216,plain,~r1(skolem0001,X1351)|~r1(X1351,X1345)|~r1(X1345,X1349)|~r1(X1349,X1346)|p1(X1346)|~p1(X1349)|~r1(X1345,X1348)|p1(X1348)|~p1(X1345)|~r1(X1345,X1350)|r1(skolem0002(X1351,X1345,X1350),skolem0003(X1351,X1345,X1350))|~r1(skolem0004(X1351,X1345),X1347)|~r1(X1347,skolem0004(X1351,X1345))|p1(X1347)|~p1(skolem0004(X1351,X1345)),inference(factor,[status(thm)],[c20])).
% 13.26/13.56 cnf(c746,plain,~r1(skolem0001,X1249)|~r1(X1249,skolem0001)|~r1(skolem0001,X1251)|~r1(X1251,X1250)|p1(X1250)|~p1(X1251)|p1(X1249)|~p1(skolem0001)|p1(skolem0002(X1249,skolem0001,X1251))|p1(skolem0004(X1249,skolem0001)),inference(factor,[status(thm)],[c310])).
% 13.26/13.56 cnf(c1040,plain,~r1(skolem0001,X1343)|~r1(X1343,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X1343)|~p1(skolem0001)|p1(skolem0002(X1343,skolem0001,skolem0013))|p1(skolem0004(X1343,skolem0001)),inference(resolution,[status(thm)],[c746, c56])).
% 13.26/13.56 cnf(c1072,plain,~r1(skolem0001,X1344)|~r1(X1344,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X1344)|~p1(skolem0001)|p1(skolem0002(X1344,skolem0001,skolem0013))|p1(skolem0004(X1344,skolem0001)),inference(resolution,[status(thm)],[c1040, c55])).
% 13.26/13.56 cnf(c199,plain,~r1(skolem0001,X1173)|~r1(X1173,X1172)|~r1(X1172,X1172)|~r1(X1172,X1170)|p1(X1170)|~p1(X1172)|~r1(X1172,X1171)|p1(X1171)|r1(skolem0002(X1173,X1172,X1170),skolem0003(X1173,X1172,X1170))|p1(skolem0004(X1173,X1172)),inference(factor,[status(thm)],[c17])).
% 13.26/13.56 cnf(c1003,plain,~r1(skolem0001,X1178)|~r1(X1178,X1177)|~r1(X1177,X1177)|~r1(X1177,X1176)|p1(X1176)|~p1(X1177)|r1(skolem0002(X1178,X1177,X1176),skolem0003(X1178,X1177,X1176))|p1(skolem0004(X1178,X1177)),inference(factor,[status(thm)],[c199])).
% 13.26/13.56 cnf(c1011,plain,~r1(skolem0001,X1327)|~r1(X1327,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X1327,skolem0001,skolem0013),skolem0003(X1327,skolem0001,skolem0013))|p1(skolem0004(X1327,skolem0001)),inference(resolution,[status(thm)],[c1003, c55])).
% 13.26/13.56 cnf(c1069,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(skolem0001,skolem0001,skolem0013),skolem0003(skolem0001,skolem0001,skolem0013))|p1(skolem0004(skolem0001,skolem0001)),inference(factor,[status(thm)],[c1011])).
% 13.26/13.56 cnf(c1010,plain,~r1(skolem0001,X1319)|~r1(X1319,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X1319,skolem0013,skolem0014),skolem0003(X1319,skolem0013,skolem0014))|p1(skolem0004(X1319,skolem0013)),inference(resolution,[status(thm)],[c1003, c56])).
% 13.26/13.56 cnf(c1066,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(skolem0013,skolem0013,skolem0014),skolem0003(skolem0013,skolem0013,skolem0014))|p1(skolem0004(skolem0013,skolem0013)),inference(factor,[status(thm)],[c1010])).
% 13.26/13.56 cnf(c988,plain,~r1(skolem0001,X1165)|~r1(X1165,X1163)|~r1(X1163,X1163)|~r1(X1163,X1164)|p1(X1164)|~p1(X1163)|r1(skolem0002(X1165,X1163,X1163),skolem0003(X1165,X1163,X1163))|p1(skolem0004(X1165,X1163)),inference(factor,[status(thm)],[c198])).
% 13.26/13.56 cnf(c996,plain,~r1(skolem0001,X1317)|~r1(X1317,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(X1317,skolem0001,skolem0001),skolem0003(X1317,skolem0001,skolem0001))|p1(skolem0004(X1317,skolem0001)),inference(resolution,[status(thm)],[c988, c55])).
% 13.26/13.56 cnf(c213,plain,~r1(skolem0001,X1312)|~r1(X1312,X1311)|~r1(X1311,X1309)|~r1(X1309,X1315)|p1(X1315)|~p1(X1309)|~r1(X1311,X1310)|p1(X1310)|~p1(X1311)|~r1(X1311,X1316)|r1(skolem0002(X1312,X1311,X1316),skolem0003(X1312,X1311,X1316))|~r1(skolem0004(X1312,X1311),X1313)|~r1(X1313,skolem0006(X1312,X1311,X1313))|~r1(skolem0006(X1312,X1311,X1313),X1314)|p1(X1314)|~p1(skolem0006(X1312,X1311,X1313)),inference(factor,[status(thm)],[c19])).
% 13.26/13.56 cnf(c995,plain,~r1(skolem0001,X1308)|~r1(X1308,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(X1308,skolem0013,skolem0013),skolem0003(X1308,skolem0013,skolem0013))|p1(skolem0004(X1308,skolem0013)),inference(resolution,[status(thm)],[c988, c56])).
% 13.26/13.56 cnf(c786,plain,~r1(skolem0001,X1263)|~r1(X1263,skolem0001)|~r1(skolem0001,X1264)|~r1(X1264,X1265)|p1(X1265)|~p1(X1264)|p1(X1263)|~p1(skolem0001)|p1(skolem0002(X1263,skolem0001,X1263))|p1(skolem0004(X1263,skolem0001)),inference(factor,[status(thm)],[c312])).
% 13.26/13.56 cnf(c1048,plain,~r1(skolem0001,X1277)|~r1(X1277,skolem0001)|~r1(skolem0001,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(X1277)|~p1(skolem0001)|p1(skolem0002(X1277,skolem0001,X1277))|p1(skolem0004(X1277,skolem0001)),inference(resolution,[status(thm)],[c786, c56])).
% 13.26/13.56 cnf(c1054,plain,~r1(skolem0001,X1285)|~r1(X1285,skolem0001)|p1(skolem0014)|~p1(skolem0013)|p1(X1285)|~p1(skolem0001)|p1(skolem0002(X1285,skolem0001,X1285))|p1(skolem0004(X1285,skolem0001)),inference(resolution,[status(thm)],[c1048, c55])).
% 13.26/13.56 cnf(c18,negated_conjecture,~r1(skolem0001,X176)|~r1(X176,X182)|~r1(X182,X179)|~r1(X179,X183)|p1(X183)|~p1(X179)|~r1(X182,X180)|p1(X180)|~p1(X182)|~r1(X182,X184)|r1(skolem0002(X176,X182,X184),skolem0003(X176,X182,X184))|~r1(skolem0004(X176,X182),X177)|~r1(X177,X178)|~r1(X178,X181)|p1(X181)|~p1(X178)|r1(X177,skolem0006(X176,X182,X177)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.56 cnf(c207,plain,~r1(skolem0001,X1271)|~r1(X1271,X1266)|~r1(X1266,X1270)|~r1(X1270,X1272)|p1(X1272)|~p1(X1270)|~r1(X1266,X1267)|p1(X1267)|~p1(X1266)|~r1(X1266,X1269)|r1(skolem0002(X1271,X1266,X1269),skolem0003(X1271,X1266,X1269))|~r1(skolem0004(X1271,X1266),skolem0004(X1271,X1266))|~r1(skolem0004(X1271,X1266),X1268)|p1(X1268)|~p1(skolem0004(X1271,X1266))|r1(skolem0004(X1271,X1266),skolem0006(X1271,X1266,skolem0004(X1271,X1266))),inference(factor,[status(thm)],[c18])).
% 13.26/13.56 cnf(c79,plain,~r1(skolem0001,X577)|~r1(X577,X578)|~r1(X578,X578)|~r1(X578,X576)|p1(X576)|~p1(X578)|~r1(X578,X575)|p1(X575)|r1(X576,skolem0002(X577,X578,X576))|r1(skolem0004(X577,X578),skolem0005(X577,X578)),inference(factor,[status(thm)],[c8])).
% 13.26/13.56 cnf(c568,plain,~r1(skolem0001,X583)|~r1(X583,X581)|~r1(X581,X581)|~r1(X581,X582)|p1(X582)|~p1(X581)|r1(X582,skolem0002(X583,X581,X582))|r1(skolem0004(X583,X581),skolem0005(X583,X581)),inference(factor,[status(thm)],[c79])).
% 13.26/13.56 cnf(c576,plain,~r1(skolem0001,X1220)|~r1(X1220,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0013,skolem0002(X1220,skolem0001,skolem0013))|r1(skolem0004(X1220,skolem0001),skolem0005(X1220,skolem0001)),inference(resolution,[status(thm)],[c568, c55])).
% 13.26/13.56 cnf(c1035,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0013,skolem0002(skolem0001,skolem0001,skolem0013))|r1(skolem0004(skolem0001,skolem0001),skolem0005(skolem0001,skolem0001)),inference(factor,[status(thm)],[c576])).
% 13.26/13.56 cnf(c575,plain,~r1(skolem0001,X1219)|~r1(X1219,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(X1219,skolem0013,skolem0014))|r1(skolem0004(X1219,skolem0013),skolem0005(X1219,skolem0013)),inference(resolution,[status(thm)],[c568, c56])).
% 13.26/13.56 cnf(c1034,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(skolem0013,skolem0013,skolem0014))|r1(skolem0004(skolem0013,skolem0013),skolem0005(skolem0013,skolem0013)),inference(factor,[status(thm)],[c575])).
% 13.26/13.56 cnf(c555,plain,~r1(skolem0001,X571)|~r1(X571,X570)|~r1(X570,X570)|~r1(X570,X569)|p1(X569)|~p1(X570)|r1(X570,skolem0002(X571,X570,X570))|r1(skolem0004(X571,X570),skolem0005(X571,X570)),inference(factor,[status(thm)],[c78])).
% 13.26/13.56 cnf(c563,plain,~r1(skolem0001,X1213)|~r1(X1213,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0001,skolem0002(X1213,skolem0001,skolem0001))|r1(skolem0004(X1213,skolem0001),skolem0005(X1213,skolem0001)),inference(resolution,[status(thm)],[c555, c55])).
% 13.26/13.56 cnf(c562,plain,~r1(skolem0001,X1208)|~r1(X1208,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0013,skolem0002(X1208,skolem0013,skolem0013))|r1(skolem0004(X1208,skolem0013),skolem0005(X1208,skolem0013)),inference(resolution,[status(thm)],[c555, c56])).
% 13.26/13.56 cnf(c1007,plain,~r1(skolem0001,X1193)|~r1(X1193,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1193)|~p1(skolem0001)|r1(skolem0002(X1193,skolem0001,X1193),skolem0003(X1193,skolem0001,X1193))|p1(skolem0004(X1193,skolem0001)),inference(factor,[status(thm)],[c1003])).
% 13.26/13.56 cnf(c992,plain,~r1(skolem0001,X1169)|~r1(X1169,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1169)|~p1(skolem0001)|r1(skolem0002(X1169,skolem0001,skolem0001),skolem0003(X1169,skolem0001,skolem0001))|p1(skolem0004(X1169,skolem0001)),inference(factor,[status(thm)],[c988])).
% 13.26/13.56 cnf(c197,plain,~r1(skolem0001,X1154)|~r1(X1154,X1154)|~r1(X1154,X1152)|~r1(X1152,X1151)|p1(X1151)|~p1(X1152)|~r1(X1154,X1153)|p1(X1153)|~p1(X1154)|r1(skolem0002(X1154,X1154,X1154),skolem0003(X1154,X1154,X1154))|p1(skolem0004(X1154,X1154)),inference(factor,[status(thm)],[c17])).
% 13.26/13.56 cnf(c976,plain,~r1(skolem0001,X1156)|~r1(X1156,X1156)|~r1(X1156,X1155)|p1(X1155)|~p1(X1156)|r1(skolem0002(X1156,X1156,X1156),skolem0003(X1156,X1156,X1156))|p1(skolem0004(X1156,X1156)),inference(factor,[status(thm)],[c197])).
% 13.26/13.56 cnf(c982,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0002(skolem0013,skolem0013,skolem0013),skolem0003(skolem0013,skolem0013,skolem0013))|p1(skolem0004(skolem0013,skolem0013)),inference(resolution,[status(thm)],[c976, c56])).
% 13.26/13.56 cnf(c983,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(skolem0001,skolem0001,skolem0001),skolem0003(skolem0001,skolem0001,skolem0001))|p1(skolem0004(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c976, c55])).
% 13.26/13.56 cnf(c297,plain,~r1(skolem0001,X1112)|~r1(X1112,X1115)|~r1(X1115,X1115)|~r1(X1115,X1114)|p1(X1114)|~p1(X1115)|~r1(X1115,X1113)|p1(X1113)|p1(skolem0002(X1112,X1115,X1114))|r1(skolem0004(X1112,X1115),skolem0005(X1112,X1115)),inference(factor,[status(thm)],[c29])).
% 13.26/13.56 cnf(c953,plain,~r1(skolem0001,X1122)|~r1(X1122,X1124)|~r1(X1124,X1124)|~r1(X1124,X1123)|p1(X1123)|~p1(X1124)|p1(skolem0002(X1122,X1124,X1123))|r1(skolem0004(X1122,X1124),skolem0005(X1122,X1124)),inference(factor,[status(thm)],[c297])).
% 13.26/13.56 cnf(c961,plain,~r1(skolem0001,X1138)|~r1(X1138,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X1138,skolem0001,skolem0013))|r1(skolem0004(X1138,skolem0001),skolem0005(X1138,skolem0001)),inference(resolution,[status(thm)],[c953, c55])).
% 13.26/13.56 cnf(c966,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(skolem0001,skolem0001,skolem0013))|r1(skolem0004(skolem0001,skolem0001),skolem0005(skolem0001,skolem0001)),inference(factor,[status(thm)],[c961])).
% 13.26/13.56 cnf(c960,plain,~r1(skolem0001,X1137)|~r1(X1137,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X1137,skolem0013,skolem0014))|r1(skolem0004(X1137,skolem0013),skolem0005(X1137,skolem0013)),inference(resolution,[status(thm)],[c953, c56])).
% 13.26/13.56 cnf(c965,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(skolem0013,skolem0013,skolem0014))|r1(skolem0004(skolem0013,skolem0013),skolem0005(skolem0013,skolem0013)),inference(factor,[status(thm)],[c960])).
% 13.26/13.56 cnf(c16,negated_conjecture,~r1(skolem0001,X157)|~r1(X157,X160)|~r1(X160,X158)|~r1(X158,X161)|p1(X161)|~p1(X158)|~r1(X160,X159)|p1(X159)|~p1(X160)|~r1(X160,X162)|r1(skolem0002(X157,X160,X162),skolem0003(X157,X160,X162))|~p1(skolem0005(X157,X160)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.56 cnf(c185,plain,~r1(skolem0001,X1132)|~r1(X1132,X1133)|~r1(X1133,skolem0005(X1132,X1133))|~r1(skolem0005(X1132,X1133),X1134)|p1(X1134)|~p1(skolem0005(X1132,X1133))|~r1(X1133,X1135)|p1(X1135)|~p1(X1133)|~r1(X1133,X1136)|r1(skolem0002(X1132,X1133,X1136),skolem0003(X1132,X1133,X1136)),inference(factor,[status(thm)],[c16])).
% 13.26/13.56 cnf(c957,plain,~r1(skolem0001,X1131)|~r1(X1131,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1131)|~p1(skolem0001)|p1(skolem0002(X1131,skolem0001,X1131))|r1(skolem0004(X1131,skolem0001),skolem0005(X1131,skolem0001)),inference(factor,[status(thm)],[c953])).
% 13.26/13.56 cnf(c919,plain,~r1(skolem0001,X1063)|~r1(X1063,X1062)|~r1(X1062,X1062)|~r1(X1062,X1064)|p1(X1064)|~p1(X1062)|p1(skolem0002(X1063,X1062,X1062))|r1(X1062,skolem0004(X1063,X1062)),inference(factor,[status(thm)],[c268])).
% 13.26/13.56 cnf(c927,plain,~r1(skolem0001,X1078)|~r1(X1078,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X1078,skolem0001,skolem0001))|r1(skolem0001,skolem0004(X1078,skolem0001)),inference(resolution,[status(thm)],[c919, c55])).
% 13.26/13.56 cnf(c926,plain,~r1(skolem0001,X1077)|~r1(X1077,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X1077,skolem0013,skolem0013))|r1(skolem0013,skolem0004(X1077,skolem0013)),inference(resolution,[status(thm)],[c919, c56])).
% 13.26/13.56 cnf(c923,plain,~r1(skolem0001,X1072)|~r1(X1072,skolem0001)|~r1(skolem0001,skolem0001)|p1(X1072)|~p1(skolem0001)|p1(skolem0002(X1072,skolem0001,skolem0001))|r1(skolem0001,skolem0004(X1072,skolem0001)),inference(factor,[status(thm)],[c919])).
% 13.26/13.56 cnf(c881,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(skolem0001,skolem0001,skolem0001),skolem0003(skolem0001,skolem0001,skolem0001))|r1(skolem0004(skolem0001,skolem0001),skolem0005(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c874, c55])).
% 13.26/13.56 cnf(c267,plain,~r1(skolem0001,X1009)|~r1(X1009,X1009)|~r1(X1009,X1008)|~r1(X1008,X1006)|p1(X1006)|~p1(X1008)|~r1(X1009,X1007)|p1(X1007)|~p1(X1009)|p1(skolem0002(X1009,X1009,X1009))|r1(X1009,skolem0004(X1009,X1009)),inference(factor,[status(thm)],[c28])).
% 13.26/13.56 cnf(c862,plain,~r1(skolem0001,X1011)|~r1(X1011,X1011)|~r1(X1011,X1010)|p1(X1010)|~p1(X1011)|p1(skolem0002(X1011,X1011,X1011))|r1(X1011,skolem0004(X1011,X1011)),inference(factor,[status(thm)],[c267])).
% 13.26/13.56 cnf(c868,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(skolem0013,skolem0013,skolem0013))|r1(skolem0013,skolem0004(skolem0013,skolem0013)),inference(resolution,[status(thm)],[c862, c56])).
% 13.26/13.56 cnf(c869,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(skolem0001,skolem0001,skolem0001))|r1(skolem0001,skolem0004(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c862, c55])).
% 13.26/13.56 cnf(c813,plain,~r1(skolem0001,X999)|~r1(X999,skolem0001)|~r1(skolem0001,skolem0001)|p1(X999)|~p1(skolem0001)|r1(skolem0002(X999,skolem0001,X999),skolem0003(X999,skolem0001,X999))|r1(skolem0001,skolem0004(X999,skolem0001)),inference(factor,[status(thm)],[c809])).
% 13.26/13.56 cnf(c687,plain,~r1(skolem0001,X991)|~r1(X991,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X990)|p1(X990)|~p1(skolem0001)|r1(skolem0013,skolem0002(X991,skolem0001,skolem0013))|p1(skolem0004(X991,skolem0001)),inference(factor,[status(thm)],[c116])).
% 13.26/13.56 cnf(c846,plain,~r1(skolem0001,X992)|~r1(X992,skolem0001)|~r1(skolem0001,skolem0001)|p1(X992)|~p1(skolem0001)|r1(skolem0013,skolem0002(X992,skolem0001,skolem0013))|p1(skolem0004(X992,skolem0001)),inference(factor,[status(thm)],[c687])).
% 13.26/13.56 cnf(c115,plain,~r1(skolem0001,X715)|~r1(X715,skolem0013)|~r1(skolem0013,X716)|~r1(X716,X717)|p1(X717)|~p1(X716)|~r1(skolem0013,X718)|p1(X718)|~p1(skolem0013)|r1(skolem0014,skolem0002(X715,skolem0013,skolem0014))|p1(skolem0004(X715,skolem0013)),inference(resolution,[status(thm)],[c10, c56])).
% 13.26/13.56 cnf(c682,plain,~r1(skolem0001,X983)|~r1(X983,skolem0013)|~r1(skolem0013,skolem0013)|~r1(skolem0013,X982)|p1(X982)|~p1(skolem0013)|r1(skolem0014,skolem0002(X983,skolem0013,skolem0014))|p1(skolem0004(X983,skolem0013)),inference(factor,[status(thm)],[c115])).
% 13.26/13.56 cnf(c559,plain,~r1(skolem0001,X975)|~r1(X975,skolem0001)|~r1(skolem0001,skolem0001)|p1(X975)|~p1(skolem0001)|r1(skolem0001,skolem0002(X975,skolem0001,skolem0001))|r1(skolem0004(X975,skolem0001),skolem0005(X975,skolem0001)),inference(factor,[status(thm)],[c555])).
% 13.26/13.56 cnf(c77,plain,~r1(skolem0001,X557)|~r1(X557,X557)|~r1(X557,X558)|~r1(X558,X556)|p1(X556)|~p1(X558)|~r1(X557,X559)|p1(X559)|~p1(X557)|r1(X557,skolem0002(X557,X557,X557))|r1(skolem0004(X557,X557),skolem0005(X557,X557)),inference(factor,[status(thm)],[c8])).
% 13.26/13.56 cnf(c543,plain,~r1(skolem0001,X561)|~r1(X561,X561)|~r1(X561,X560)|p1(X560)|~p1(X561)|r1(X561,skolem0002(X561,X561,X561))|r1(skolem0004(X561,X561),skolem0005(X561,X561)),inference(factor,[status(thm)],[c77])).
% 13.26/13.56 cnf(c549,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0013,skolem0002(skolem0013,skolem0013,skolem0013))|r1(skolem0004(skolem0013,skolem0013),skolem0005(skolem0013,skolem0013)),inference(resolution,[status(thm)],[c543, c56])).
% 13.26/13.56 cnf(c460,plain,~r1(skolem0001,X962)|~r1(X962,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X963)|p1(X963)|~p1(skolem0001)|r1(X962,skolem0002(X962,skolem0001,X962))|r1(skolem0001,skolem0004(X962,skolem0001)),inference(factor,[status(thm)],[c64])).
% 13.26/13.56 cnf(c829,plain,~r1(skolem0001,X970)|~r1(X970,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(X970,skolem0002(X970,skolem0001,X970))|r1(skolem0001,skolem0004(X970,skolem0001)),inference(resolution,[status(thm)],[c460, c55])).
% 13.26/13.56 cnf(c784,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0002(skolem0001,skolem0001,skolem0001),skolem0003(skolem0001,skolem0001,skolem0001))|r1(skolem0001,skolem0004(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c777, c55])).
% 13.26/13.56 cnf(c749,plain,~r1(skolem0001,X875)|~r1(X875,X873)|~r1(X873,X873)|~r1(X873,X874)|p1(X874)|~p1(X873)|p1(skolem0002(X875,X873,X873))|p1(skolem0004(X875,X873)),inference(factor,[status(thm)],[c310])).
% 13.26/13.56 cnf(c757,plain,~r1(skolem0001,X888)|~r1(X888,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X888,skolem0001,skolem0001))|p1(skolem0004(X888,skolem0001)),inference(resolution,[status(thm)],[c749, c55])).
% 13.26/13.56 cnf(c756,plain,~r1(skolem0001,X887)|~r1(X887,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X887,skolem0013,skolem0013))|p1(skolem0004(X887,skolem0013)),inference(resolution,[status(thm)],[c749, c56])).
% 13.26/13.56 cnf(c149,plain,~r1(skolem0001,X882)|~r1(X882,X880)|~r1(X880,X883)|~r1(X883,X886)|p1(X886)|~p1(X883)|~r1(X880,X884)|p1(X884)|~p1(X880)|~r1(X880,X885)|r1(X885,skolem0002(X882,X880,X885))|~r1(skolem0004(X882,X880),X881)|~r1(X881,skolem0004(X882,X880))|p1(X881)|~p1(skolem0004(X882,X880)),inference(factor,[status(thm)],[c13])).
% 13.26/13.56 cnf(c753,plain,~r1(skolem0001,X879)|~r1(X879,skolem0001)|~r1(skolem0001,skolem0001)|p1(X879)|~p1(skolem0001)|p1(skolem0002(X879,skolem0001,skolem0001))|p1(skolem0004(X879,skolem0001)),inference(factor,[status(thm)],[c749])).
% 13.26/13.56 cnf(c309,plain,~r1(skolem0001,X843)|~r1(X843,X843)|~r1(X843,X842)|~r1(X842,X844)|p1(X844)|~p1(X842)|~r1(X843,X841)|p1(X841)|~p1(X843)|p1(skolem0002(X843,X843,X843))|p1(skolem0004(X843,X843)),inference(factor,[status(thm)],[c31])).
% 13.26/13.56 cnf(c735,plain,~r1(skolem0001,X846)|~r1(X846,X846)|~r1(X846,X845)|p1(X845)|~p1(X846)|p1(skolem0002(X846,X846,X846))|p1(skolem0004(X846,X846)),inference(factor,[status(thm)],[c309])).
% 13.26/13.56 cnf(c741,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(skolem0013,skolem0013,skolem0013))|p1(skolem0004(skolem0013,skolem0013)),inference(resolution,[status(thm)],[c735, c56])).
% 13.26/13.56 cnf(c742,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(skolem0001,skolem0001,skolem0001))|p1(skolem0004(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c735, c55])).
% 13.26/13.56 cnf(c141,plain,~r1(skolem0001,X840)|~r1(X840,X839)|~r1(X839,X836)|~r1(X836,X833)|p1(X833)|~p1(X836)|~r1(X839,X835)|p1(X835)|~p1(X839)|~r1(X839,X837)|r1(X837,skolem0002(X840,X839,X837))|~r1(skolem0004(X840,X839),X834)|~r1(X834,skolem0006(X840,X839,X834))|~r1(skolem0006(X840,X839,X834),X838)|p1(X838)|~p1(skolem0006(X840,X839,X834)),inference(factor,[status(thm)],[c12])).
% 13.26/13.56 cnf(c639,plain,~r1(skolem0001,X820)|~r1(X820,skolem0001)|~r1(skolem0001,skolem0001)|~r1(skolem0001,X821)|p1(X821)|~p1(skolem0001)|r1(X820,skolem0002(X820,skolem0001,X820))|p1(skolem0004(X820,skolem0001)),inference(factor,[status(thm)],[c109])).
% 13.26/13.56 cnf(c727,plain,~r1(skolem0001,X832)|~r1(X832,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(X832,skolem0002(X832,skolem0001,X832))|p1(skolem0004(X832,skolem0001)),inference(resolution,[status(thm)],[c639, c55])).
% 13.26/13.56 cnf(c572,plain,~r1(skolem0001,X819)|~r1(X819,skolem0001)|~r1(skolem0001,skolem0001)|p1(X819)|~p1(skolem0001)|r1(X819,skolem0002(X819,skolem0001,X819))|r1(skolem0004(X819,skolem0001),skolem0005(X819,skolem0001)),inference(factor,[status(thm)],[c568])).
% 13.26/13.56 cnf(c67,plain,~r1(skolem0001,X490)|~r1(X490,X491)|~r1(X491,X491)|~r1(X491,X492)|p1(X492)|~p1(X491)|~r1(X491,X493)|p1(X493)|r1(X492,skolem0002(X490,X491,X492))|r1(X491,skolem0004(X490,X491)),inference(factor,[status(thm)],[c7])).
% 13.26/13.56 cnf(c492,plain,~r1(skolem0001,X497)|~r1(X497,X496)|~r1(X496,X496)|~r1(X496,X498)|p1(X498)|~p1(X496)|r1(X498,skolem0002(X497,X496,X498))|r1(X496,skolem0004(X497,X496)),inference(factor,[status(thm)],[c67])).
% 13.26/13.56 cnf(c500,plain,~r1(skolem0001,X793)|~r1(X793,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0013,skolem0002(X793,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X793,skolem0001)),inference(resolution,[status(thm)],[c492, c55])).
% 13.26/13.56 cnf(c713,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0013,skolem0002(skolem0001,skolem0001,skolem0013))|r1(skolem0001,skolem0004(skolem0001,skolem0001)),inference(factor,[status(thm)],[c500])).
% 13.26/13.56 cnf(c11,negated_conjecture,~r1(skolem0001,X93)|~r1(X93,X99)|~r1(X99,X96)|~r1(X96,X100)|p1(X100)|~p1(X96)|~r1(X99,X97)|p1(X97)|~p1(X99)|~r1(X99,X101)|r1(X101,skolem0002(X93,X99,X101))|~r1(skolem0004(X93,X99),X94)|~r1(X94,X95)|~r1(X95,X98)|p1(X98)|~p1(X95)|r1(X94,skolem0006(X93,X99,X94)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.56 cnf(c135,plain,~r1(skolem0001,X794)|~r1(X794,X797)|~r1(X797,X798)|~r1(X798,X799)|p1(X799)|~p1(X798)|~r1(X797,X795)|p1(X795)|~p1(X797)|~r1(X797,X796)|r1(X796,skolem0002(X794,X797,X796))|~r1(skolem0004(X794,X797),skolem0004(X794,X797))|~r1(skolem0004(X794,X797),X800)|p1(X800)|~p1(skolem0004(X794,X797))|r1(skolem0004(X794,X797),skolem0006(X794,X797,skolem0004(X794,X797))),inference(factor,[status(thm)],[c11])).
% 13.26/13.56 cnf(c499,plain,~r1(skolem0001,X792)|~r1(X792,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(X792,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X792,skolem0013)),inference(resolution,[status(thm)],[c492, c56])).
% 13.26/13.56 cnf(c712,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(skolem0013,skolem0013,skolem0014))|r1(skolem0013,skolem0004(skolem0013,skolem0013)),inference(factor,[status(thm)],[c499])).
% 13.26/13.56 cnf(c479,plain,~r1(skolem0001,X484)|~r1(X484,X485)|~r1(X485,X485)|~r1(X485,X483)|p1(X483)|~p1(X485)|r1(X485,skolem0002(X484,X485,X485))|r1(X485,skolem0004(X484,X485)),inference(factor,[status(thm)],[c66])).
% 13.26/13.56 cnf(c487,plain,~r1(skolem0001,X783)|~r1(X783,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0001,skolem0002(X783,skolem0001,skolem0001))|r1(skolem0001,skolem0004(X783,skolem0001)),inference(resolution,[status(thm)],[c479, c55])).
% 13.26/13.56 cnf(c486,plain,~r1(skolem0001,X782)|~r1(X782,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0013,skolem0002(X782,skolem0013,skolem0013))|r1(skolem0013,skolem0004(X782,skolem0013)),inference(resolution,[status(thm)],[c479, c56])).
% 13.26/13.56 cnf(c269,plain,~r1(skolem0001,X742)|~r1(X742,X741)|~r1(X741,X741)|~r1(X741,X743)|p1(X743)|~p1(X741)|~r1(X741,X740)|p1(X740)|p1(skolem0002(X742,X741,X743))|r1(X741,skolem0004(X742,X741)),inference(factor,[status(thm)],[c28])).
% 13.26/13.56 cnf(c692,plain,~r1(skolem0001,X747)|~r1(X747,X746)|~r1(X746,X746)|~r1(X746,X748)|p1(X748)|~p1(X746)|p1(skolem0002(X747,X746,X748))|r1(X746,skolem0004(X747,X746)),inference(factor,[status(thm)],[c269])).
% 13.26/13.56 cnf(c700,plain,~r1(skolem0001,X765)|~r1(X765,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X765,skolem0001,skolem0013))|r1(skolem0001,skolem0004(X765,skolem0001)),inference(resolution,[status(thm)],[c692, c55])).
% 13.26/13.56 cnf(c705,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(skolem0001,skolem0001,skolem0013))|r1(skolem0001,skolem0004(skolem0001,skolem0001)),inference(factor,[status(thm)],[c700])).
% 13.26/13.56 cnf(c699,plain,~r1(skolem0001,X760)|~r1(X760,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X760,skolem0013,skolem0014))|r1(skolem0013,skolem0004(X760,skolem0013)),inference(resolution,[status(thm)],[c692, c56])).
% 13.26/13.56 cnf(c704,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(skolem0013,skolem0013,skolem0014))|r1(skolem0013,skolem0004(skolem0013,skolem0013)),inference(factor,[status(thm)],[c699])).
% 13.26/13.56 cnf(c696,plain,~r1(skolem0001,X759)|~r1(X759,skolem0001)|~r1(skolem0001,skolem0001)|p1(X759)|~p1(skolem0001)|p1(skolem0002(X759,skolem0001,X759))|r1(skolem0001,skolem0004(X759,skolem0001)),inference(factor,[status(thm)],[c692])).
% 13.26/13.56 cnf(c658,plain,~r1(skolem0001,X692)|~r1(X692,X691)|~r1(X691,X691)|~r1(X691,X690)|p1(X690)|~p1(X691)|r1(X691,skolem0002(X692,X691,X691))|p1(skolem0004(X692,X691)),inference(factor,[status(thm)],[c111])).
% 13.26/13.56 cnf(c666,plain,~r1(skolem0001,X710)|~r1(X710,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0001,skolem0002(X710,skolem0001,skolem0001))|p1(skolem0004(X710,skolem0001)),inference(resolution,[status(thm)],[c658, c55])).
% 13.26/13.56 cnf(c665,plain,~r1(skolem0001,X705)|~r1(X705,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0013,skolem0002(X705,skolem0013,skolem0013))|p1(skolem0004(X705,skolem0013)),inference(resolution,[status(thm)],[c658, c56])).
% 13.26/13.56 cnf(c662,plain,~r1(skolem0001,X696)|~r1(X696,skolem0001)|~r1(skolem0001,skolem0001)|p1(X696)|~p1(skolem0001)|r1(skolem0001,skolem0002(X696,skolem0001,skolem0001))|p1(skolem0004(X696,skolem0001)),inference(factor,[status(thm)],[c658])).
% 13.26/13.56 cnf(c110,plain,~r1(skolem0001,X680)|~r1(X680,X680)|~r1(X680,X678)|~r1(X678,X681)|p1(X681)|~p1(X678)|~r1(X680,X679)|p1(X679)|~p1(X680)|r1(X680,skolem0002(X680,X680,X680))|p1(skolem0004(X680,X680)),inference(factor,[status(thm)],[c10])).
% 13.26/13.56 cnf(c646,plain,~r1(skolem0001,X682)|~r1(X682,X682)|~r1(X682,X683)|p1(X683)|~p1(X682)|r1(X682,skolem0002(X682,X682,X682))|p1(skolem0004(X682,X682)),inference(factor,[status(thm)],[c110])).
% 13.26/13.56 cnf(c652,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0013,skolem0002(skolem0013,skolem0013,skolem0013))|p1(skolem0004(skolem0013,skolem0013)),inference(resolution,[status(thm)],[c646, c56])).
% 13.26/13.56 cnf(c653,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0001,skolem0002(skolem0001,skolem0001,skolem0001))|p1(skolem0004(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c646, c55])).
% 13.26/13.56 cnf(c112,plain,~r1(skolem0001,X650)|~r1(X650,X652)|~r1(X652,X652)|~r1(X652,X651)|p1(X651)|~p1(X652)|~r1(X652,X649)|p1(X649)|r1(X651,skolem0002(X650,X652,X651))|p1(skolem0004(X650,X652)),inference(factor,[status(thm)],[c10])).
% 13.26/13.56 cnf(c623,plain,~r1(skolem0001,X660)|~r1(X660,X661)|~r1(X661,X661)|~r1(X661,X662)|p1(X662)|~p1(X661)|r1(X662,skolem0002(X660,X661,X662))|p1(skolem0004(X660,X661)),inference(factor,[status(thm)],[c112])).
% 13.26/13.56 cnf(c631,plain,~r1(skolem0001,X676)|~r1(X676,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0013,skolem0002(X676,skolem0001,skolem0013))|p1(skolem0004(X676,skolem0001)),inference(resolution,[status(thm)],[c623, c55])).
% 13.26/13.56 cnf(c641,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0013,skolem0002(skolem0001,skolem0001,skolem0013))|p1(skolem0004(skolem0001,skolem0001)),inference(factor,[status(thm)],[c631])).
% 13.26/13.56 cnf(c630,plain,~r1(skolem0001,X671)|~r1(X671,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(X671,skolem0013,skolem0014))|p1(skolem0004(X671,skolem0013)),inference(resolution,[status(thm)],[c623, c56])).
% 13.26/13.56 cnf(c635,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0014,skolem0002(skolem0013,skolem0013,skolem0014))|p1(skolem0004(skolem0013,skolem0013)),inference(factor,[status(thm)],[c630])).
% 13.26/13.56 cnf(c627,plain,~r1(skolem0001,X666)|~r1(X666,skolem0001)|~r1(skolem0001,skolem0001)|p1(X666)|~p1(skolem0001)|r1(X666,skolem0002(X666,skolem0001,X666))|p1(skolem0004(X666,skolem0001)),inference(factor,[status(thm)],[c623])).
% 13.26/13.56 cnf(c9,negated_conjecture,~r1(skolem0001,X68)|~r1(X68,X71)|~r1(X71,X69)|~r1(X69,X72)|p1(X72)|~p1(X69)|~r1(X71,X70)|p1(X70)|~p1(X71)|~r1(X71,X73)|r1(X73,skolem0002(X68,X71,X73))|~p1(skolem0005(X68,X71)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.56 cnf(c97,plain,~r1(skolem0001,X655)|~r1(X655,X653)|~r1(X653,skolem0005(X655,X653))|~r1(skolem0005(X655,X653),X657)|p1(X657)|~p1(skolem0005(X655,X653))|~r1(X653,X656)|p1(X656)|~p1(X653)|~r1(X653,X654)|r1(X654,skolem0002(X655,X653,X654)),inference(factor,[status(thm)],[c9])).
% 13.26/13.56 cnf(c614,plain,~r1(skolem0001,X648)|~r1(X648,skolem0001)|p1(skolem0014)|r1(skolem0010(X648,skolem0001,skolem0013,skolem0014),skolem0011(X648,skolem0001,skolem0013,skolem0014))|r1(skolem0001,skolem0012(X648,skolem0001)),inference(resolution,[status(thm)],[c434, c55])).
% 13.26/13.56 cnf(c619,plain,~r1(skolem0001,skolem0001)|p1(skolem0014)|r1(skolem0010(skolem0001,skolem0001,skolem0013,skolem0014),skolem0011(skolem0001,skolem0001,skolem0013,skolem0014))|r1(skolem0001,skolem0012(skolem0001,skolem0001)),inference(factor,[status(thm)],[c614])).
% 13.26/13.56 cnf(c483,plain,~r1(skolem0001,X643)|~r1(X643,skolem0001)|~r1(skolem0001,skolem0001)|p1(X643)|~p1(skolem0001)|r1(skolem0001,skolem0002(X643,skolem0001,skolem0001))|r1(skolem0001,skolem0004(X643,skolem0001)),inference(factor,[status(thm)],[c479])).
% 13.26/13.56 cnf(c435,plain,~r1(skolem0001,X640)|~r1(X640,X639)|~r1(X639,skolem0001)|p1(skolem0013)|r1(skolem0010(X640,X639,skolem0001,skolem0013),skolem0011(X640,X639,skolem0001,skolem0013))|r1(X639,skolem0012(X640,X639)),inference(resolution,[status(thm)],[c46, c55])).
% 13.26/13.56 cnf(c615,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0013),skolem0011(skolem0001,skolem0001,skolem0001,skolem0013))|r1(skolem0001,skolem0012(skolem0001,skolem0001)),inference(factor,[status(thm)],[c435])).
% 13.26/13.56 cnf(c311,plain,~r1(skolem0001,X604)|~r1(X604,X601)|~r1(X601,X601)|~r1(X601,X603)|p1(X603)|~p1(X601)|~r1(X601,X602)|p1(X602)|p1(skolem0002(X604,X601,X603))|p1(skolem0004(X604,X601)),inference(factor,[status(thm)],[c31])).
% 13.26/13.57 cnf(c593,plain,~r1(skolem0001,X611)|~r1(X611,X612)|~r1(X612,X612)|~r1(X612,X613)|p1(X613)|~p1(X612)|p1(skolem0002(X611,X612,X613))|p1(skolem0004(X611,X612)),inference(factor,[status(thm)],[c311])).
% 13.26/13.57 cnf(c601,plain,~r1(skolem0001,X626)|~r1(X626,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(X626,skolem0001,skolem0013))|p1(skolem0004(X626,skolem0001)),inference(resolution,[status(thm)],[c593, c55])).
% 13.26/13.57 cnf(c606,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|p1(skolem0002(skolem0001,skolem0001,skolem0013))|p1(skolem0004(skolem0001,skolem0001)),inference(factor,[status(thm)],[c601])).
% 13.26/13.57 cnf(c600,plain,~r1(skolem0001,X625)|~r1(X625,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(X625,skolem0013,skolem0014))|p1(skolem0004(X625,skolem0013)),inference(resolution,[status(thm)],[c593, c56])).
% 13.26/13.57 cnf(c605,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|p1(skolem0002(skolem0013,skolem0013,skolem0014))|p1(skolem0004(skolem0013,skolem0013)),inference(factor,[status(thm)],[c600])).
% 13.26/13.57 cnf(c597,plain,~r1(skolem0001,X617)|~r1(X617,skolem0001)|~r1(skolem0001,skolem0001)|p1(X617)|~p1(skolem0001)|p1(skolem0002(X617,skolem0001,X617))|p1(skolem0004(X617,skolem0001)),inference(factor,[status(thm)],[c593])).
% 13.26/13.57 cnf(c65,plain,~r1(skolem0001,X472)|~r1(X472,X472)|~r1(X472,X474)|~r1(X474,X473)|p1(X473)|~p1(X474)|~r1(X472,X471)|p1(X471)|~p1(X472)|r1(X472,skolem0002(X472,X472,X472))|r1(X472,skolem0004(X472,X472)),inference(factor,[status(thm)],[c7])).
% 13.26/13.57 cnf(c467,plain,~r1(skolem0001,X475)|~r1(X475,X475)|~r1(X475,X476)|p1(X476)|~p1(X475)|r1(X475,skolem0002(X475,X475,X475))|r1(X475,skolem0004(X475,X475)),inference(factor,[status(thm)],[c65])).
% 13.26/13.57 cnf(c473,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|~p1(skolem0013)|r1(skolem0013,skolem0002(skolem0013,skolem0013,skolem0013))|r1(skolem0013,skolem0004(skolem0013,skolem0013)),inference(resolution,[status(thm)],[c467, c56])).
% 13.26/13.57 cnf(c447,plain,~r1(skolem0001,X454)|~r1(X454,X454)|p1(X454)|r1(skolem0010(X454,X454,X454,X454),skolem0011(X454,X454,X454,X454))|r1(X454,skolem0012(X454,X454)),inference(factor,[status(thm)],[c430])).
% 13.26/13.57 cnf(c452,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001),skolem0011(skolem0001,skolem0001,skolem0001,skolem0001))|r1(skolem0001,skolem0012(skolem0001,skolem0001)),inference(factor,[status(thm)],[c447])).
% 13.26/13.57 cnf(c550,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0001,skolem0002(skolem0001,skolem0001,skolem0001))|r1(skolem0004(skolem0001,skolem0001),skolem0005(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c543, c55])).
% 13.26/13.57 cnf(c58,negated_conjecture,r1(skolem0014,skolem0015),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c35,negated_conjecture,~r1(skolem0001,X385)|~r1(X385,X386)|~r1(X386,X387)|p1(X387)|p1(X386)|~r1(X386,X388)|r1(X388,skolem0007(X385,X386,X388))|r1(X386,skolem0008(X385,X386)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c339,plain,~r1(skolem0001,X554)|~r1(X554,skolem0014)|~r1(skolem0014,X555)|p1(X555)|p1(skolem0014)|r1(skolem0015,skolem0007(X554,skolem0014,skolem0015))|r1(skolem0014,skolem0008(X554,skolem0014)),inference(resolution,[status(thm)],[c35, c58])).
% 13.26/13.57 cnf(c538,plain,~r1(skolem0001,skolem0014)|~r1(skolem0014,skolem0014)|p1(skolem0014)|r1(skolem0015,skolem0007(skolem0014,skolem0014,skolem0015))|r1(skolem0014,skolem0008(skolem0014,skolem0014)),inference(factor,[status(thm)],[c339])).
% 13.26/13.57 cnf(c338,plain,~r1(skolem0001,X546)|~r1(X546,skolem0001)|~r1(skolem0001,X547)|p1(X547)|p1(skolem0001)|r1(skolem0013,skolem0007(X546,skolem0001,skolem0013))|r1(skolem0001,skolem0008(X546,skolem0001)),inference(resolution,[status(thm)],[c35, c55])).
% 13.26/13.57 cnf(c529,plain,~r1(skolem0001,X552)|~r1(X552,skolem0001)|p1(X552)|p1(skolem0001)|r1(skolem0013,skolem0007(X552,skolem0001,skolem0013))|r1(skolem0001,skolem0008(X552,skolem0001)),inference(factor,[status(thm)],[c338])).
% 13.26/13.57 cnf(c530,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|r1(skolem0013,skolem0007(skolem0001,skolem0001,skolem0013))|r1(skolem0001,skolem0008(skolem0001,skolem0001)),inference(factor,[status(thm)],[c338])).
% 13.26/13.57 cnf(c337,plain,~r1(skolem0001,X543)|~r1(X543,skolem0013)|~r1(skolem0013,X544)|p1(X544)|p1(skolem0013)|r1(skolem0014,skolem0007(X543,skolem0013,skolem0014))|r1(skolem0013,skolem0008(X543,skolem0013)),inference(resolution,[status(thm)],[c35, c56])).
% 13.26/13.57 cnf(c527,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0013)|r1(skolem0014,skolem0007(skolem0013,skolem0013,skolem0014))|r1(skolem0013,skolem0008(skolem0013,skolem0013)),inference(factor,[status(thm)],[c337])).
% 13.26/13.57 cnf(c496,plain,~r1(skolem0001,X538)|~r1(X538,skolem0001)|~r1(skolem0001,skolem0001)|p1(X538)|~p1(skolem0001)|r1(X538,skolem0002(X538,skolem0001,X538))|r1(skolem0001,skolem0004(X538,skolem0001)),inference(factor,[status(thm)],[c492])).
% 13.26/13.57 cnf(c446,plain,~r1(skolem0001,X534)|~r1(X534,skolem0001)|p1(skolem0001)|r1(skolem0010(X534,skolem0001,X534,skolem0001),skolem0011(X534,skolem0001,X534,skolem0001))|r1(skolem0001,skolem0012(X534,skolem0001)),inference(factor,[status(thm)],[c430])).
% 13.26/13.57 cnf(c429,plain,~r1(skolem0001,X529)|~r1(X529,X528)|~r1(X528,skolem0001)|p1(X529)|r1(skolem0010(X529,X528,skolem0001,X529),skolem0011(X529,X528,skolem0001,X529))|r1(X528,skolem0012(X529,X528)),inference(factor,[status(thm)],[c46])).
% 13.26/13.57 cnf(c333,plain,~r1(skolem0001,X515)|~r1(X515,skolem0001)|~r1(skolem0001,X514)|p1(X514)|p1(skolem0001)|r1(X515,skolem0007(X515,skolem0001,X515))|r1(skolem0001,skolem0008(X515,skolem0001)),inference(factor,[status(thm)],[c35])).
% 13.26/13.57 cnf(c516,plain,~r1(skolem0001,X517)|~r1(X517,skolem0001)|p1(skolem0013)|p1(skolem0001)|r1(X517,skolem0007(X517,skolem0001,X517))|r1(skolem0001,skolem0008(X517,skolem0001)),inference(resolution,[status(thm)],[c333, c55])).
% 13.26/13.57 cnf(c43,negated_conjecture,~r1(skolem0001,X316)|~r1(X316,X317)|~r1(X317,X319)|~r1(X319,X318)|p1(X318)|r1(X318,skolem0010(X316,X317,X319,X318))|r1(X317,skolem0012(X316,X317)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c280,plain,~r1(skolem0001,X359)|~r1(X359,X360)|~r1(X360,skolem0013)|p1(skolem0014)|r1(skolem0014,skolem0010(X359,X360,skolem0013,skolem0014))|r1(X360,skolem0012(X359,X360)),inference(resolution,[status(thm)],[c43, c56])).
% 13.26/13.57 cnf(c319,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|r1(skolem0014,skolem0010(skolem0013,skolem0013,skolem0013,skolem0014))|r1(skolem0013,skolem0012(skolem0013,skolem0013)),inference(factor,[status(thm)],[c280])).
% 13.26/13.57 cnf(c277,plain,~r1(skolem0001,X320)|~r1(X320,X321)|~r1(X321,X320)|p1(X321)|r1(X321,skolem0010(X320,X321,X320,X321))|r1(X321,skolem0012(X320,X321)),inference(factor,[status(thm)],[c43])).
% 13.26/13.57 cnf(c287,plain,~r1(skolem0001,skolem0014)|~r1(skolem0014,skolem0013)|p1(skolem0013)|r1(skolem0013,skolem0010(skolem0014,skolem0013,skolem0014,skolem0013))|r1(skolem0013,skolem0012(skolem0014,skolem0013)),inference(resolution,[status(thm)],[c277, c56])).
% 13.26/13.57 cnf(c474,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|~p1(skolem0001)|r1(skolem0001,skolem0002(skolem0001,skolem0001,skolem0001))|r1(skolem0001,skolem0004(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c467, c55])).
% 13.26/13.57 cnf(c335,plain,~r1(skolem0001,X401)|~r1(X401,X402)|~r1(X402,X403)|p1(X403)|p1(X402)|r1(X403,skolem0007(X401,X402,X403))|r1(X402,skolem0008(X401,X402)),inference(factor,[status(thm)],[c35])).
% 13.26/13.57 cnf(c356,plain,~r1(skolem0001,X469)|~r1(X469,skolem0001)|p1(skolem0013)|p1(skolem0001)|r1(skolem0013,skolem0007(X469,skolem0001,skolem0013))|r1(skolem0001,skolem0008(X469,skolem0001)),inference(resolution,[status(thm)],[c335, c55])).
% 13.26/13.57 cnf(c355,plain,~r1(skolem0001,X468)|~r1(X468,skolem0013)|p1(skolem0014)|p1(skolem0013)|r1(skolem0014,skolem0007(X468,skolem0013,skolem0014))|r1(skolem0013,skolem0008(X468,skolem0013)),inference(resolution,[status(thm)],[c335, c56])).
% 13.26/13.57 cnf(c462,plain,~r1(skolem0001,skolem0001)|p1(skolem0014)|p1(skolem0013)|r1(skolem0014,skolem0007(skolem0001,skolem0013,skolem0014))|r1(skolem0013,skolem0008(skolem0001,skolem0013)),inference(resolution,[status(thm)],[c355, c55])).
% 13.26/13.57 cnf(c52,negated_conjecture,~r1(skolem0001,X252)|~r1(X252,X253)|~r1(X253,X255)|~r1(X255,X254)|p1(X254)|p1(skolem0010(X252,X253,X255,X254))|r1(X253,skolem0012(X252,X253)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c230,plain,~r1(skolem0001,X290)|~r1(X290,X289)|~r1(X289,skolem0013)|p1(skolem0014)|p1(skolem0010(X290,X289,skolem0013,skolem0014))|r1(X289,skolem0012(X290,X289)),inference(resolution,[status(thm)],[c52, c56])).
% 13.26/13.57 cnf(c254,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|p1(skolem0010(skolem0013,skolem0013,skolem0013,skolem0014))|r1(skolem0013,skolem0012(skolem0013,skolem0013)),inference(factor,[status(thm)],[c230])).
% 13.26/13.57 cnf(c54,negated_conjecture,~r1(skolem0001,X458)|~r1(X458,X463)|~r1(X463,X461)|~r1(X461,X459)|p1(X459)|p1(skolem0010(X458,X463,X461,X459))|~r1(skolem0012(X458,X463),X460)|~r1(X460,X462)|p1(X462)|~p1(X460),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c227,plain,~r1(skolem0001,X256)|~r1(X256,X257)|~r1(X257,X256)|p1(X257)|p1(skolem0010(X256,X257,X256,X257))|r1(X257,skolem0012(X256,X257)),inference(factor,[status(thm)],[c52])).
% 13.26/13.57 cnf(c237,plain,~r1(skolem0001,skolem0014)|~r1(skolem0014,skolem0013)|p1(skolem0013)|p1(skolem0010(skolem0014,skolem0013,skolem0014,skolem0013))|r1(skolem0013,skolem0012(skolem0014,skolem0013)),inference(resolution,[status(thm)],[c227, c56])).
% 13.26/13.57 cnf(c431,plain,~r1(skolem0001,X456)|~r1(X456,X455)|~r1(X455,X455)|p1(X455)|r1(skolem0010(X456,X455,X455,X455),skolem0011(X456,X455,X455,X455))|r1(X455,skolem0012(X456,X455)),inference(factor,[status(thm)],[c46])).
% 13.26/13.57 cnf(c62,negated_conjecture,~r1(skolem0014,X48)|p1(X48)|~p1(skolem0017(X48)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c60,negated_conjecture,~r1(skolem0014,X50)|p1(X50)|r1(X50,skolem0016(X50)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c73,plain,p1(skolem0015)|r1(skolem0015,skolem0016(skolem0015)),inference(resolution,[status(thm)],[c60, c58])).
% 13.26/13.57 cnf(c61,negated_conjecture,~r1(skolem0014,X57)|p1(X57)|r1(skolem0016(X57),skolem0017(X57)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c85,plain,p1(skolem0015)|r1(skolem0016(skolem0015),skolem0017(skolem0015)),inference(resolution,[status(thm)],[c61, c58])).
% 13.26/13.57 cnf(c42,negated_conjecture,~r1(skolem0001,X58)|~r1(X58,X62)|~r1(X62,X60)|~r1(X60,X61)|~r1(X61,X59)|p1(X59)|~p1(skolem0009(X58,X62,X60)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c59,negated_conjecture,~r1(skolem0015,X41)|p1(X41),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c41,negated_conjecture,~r1(skolem0001,X63)|~r1(X63,X67)|~r1(X67,X65)|~r1(X65,X66)|~r1(X66,X64)|p1(X64)|r1(X65,skolem0009(X63,X67,X65)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c92,plain,~r1(skolem0001,X413)|~r1(X413,X412)|~r1(X412,X414)|~r1(X414,skolem0016(skolem0015))|p1(skolem0017(skolem0015))|r1(X414,skolem0009(X413,X412,X414))|p1(skolem0015),inference(resolution,[status(thm)],[c41, c85])).
% 13.26/13.57 cnf(c364,plain,~r1(skolem0001,X416)|~r1(X416,X415)|~r1(X415,skolem0015)|p1(skolem0017(skolem0015))|r1(skolem0015,skolem0009(X416,X415,skolem0015))|p1(skolem0015),inference(resolution,[status(thm)],[c92, c73])).
% 13.26/13.57 cnf(c367,plain,~r1(skolem0001,X417)|~r1(X417,skolem0014)|p1(skolem0017(skolem0015))|r1(skolem0015,skolem0009(X417,skolem0014,skolem0015))|p1(skolem0015),inference(resolution,[status(thm)],[c364, c58])).
% 13.26/13.57 cnf(c368,plain,~r1(skolem0001,skolem0013)|p1(skolem0017(skolem0015))|r1(skolem0015,skolem0009(skolem0013,skolem0014,skolem0015))|p1(skolem0015),inference(resolution,[status(thm)],[c367, c56])).
% 13.26/13.57 cnf(c369,plain,p1(skolem0017(skolem0015))|r1(skolem0015,skolem0009(skolem0013,skolem0014,skolem0015))|p1(skolem0015),inference(resolution,[status(thm)],[c368, c55])).
% 13.26/13.57 cnf(c372,plain,p1(skolem0017(skolem0015))|p1(skolem0015)|p1(skolem0009(skolem0013,skolem0014,skolem0015)),inference(resolution,[status(thm)],[c369, c59])).
% 13.26/13.57 cnf(c392,plain,p1(skolem0015)|p1(skolem0009(skolem0013,skolem0014,skolem0015))|~r1(skolem0014,skolem0015),inference(resolution,[status(thm)],[c372, c62])).
% 13.26/13.57 cnf(c394,plain,p1(skolem0015)|p1(skolem0009(skolem0013,skolem0014,skolem0015)),inference(resolution,[status(thm)],[c392, c58])).
% 13.26/13.57 cnf(c395,plain,p1(skolem0015)|~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0014)|~r1(skolem0014,skolem0015)|~r1(skolem0015,X430)|~r1(X430,X431)|p1(X431),inference(resolution,[status(thm)],[c394, c42])).
% 13.26/13.57 cnf(c424,plain,p1(skolem0015)|~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0014)|~r1(skolem0014,skolem0015)|~r1(skolem0015,skolem0016(skolem0015))|p1(skolem0017(skolem0015)),inference(resolution,[status(thm)],[c395, c85])).
% 13.26/13.57 cnf(c438,plain,p1(skolem0015)|~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0014)|~r1(skolem0014,skolem0015)|p1(skolem0017(skolem0015)),inference(resolution,[status(thm)],[c424, c73])).
% 13.26/13.57 cnf(c439,plain,p1(skolem0015)|~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0014)|p1(skolem0017(skolem0015)),inference(resolution,[status(thm)],[c438, c58])).
% 13.26/13.57 cnf(c440,plain,p1(skolem0015)|~r1(skolem0001,skolem0013)|p1(skolem0017(skolem0015)),inference(resolution,[status(thm)],[c439, c56])).
% 13.26/13.57 cnf(c443,plain,p1(skolem0015)|p1(skolem0017(skolem0015)),inference(resolution,[status(thm)],[c440, c55])).
% 13.26/13.57 cnf(c444,plain,p1(skolem0015)|~r1(skolem0014,skolem0015),inference(resolution,[status(thm)],[c443, c62])).
% 13.26/13.57 cnf(c445,plain,p1(skolem0015),inference(resolution,[status(thm)],[c444, c58])).
% 13.26/13.57 cnf(c48,negated_conjecture,~r1(skolem0001,X440)|~r1(X440,X445)|~r1(X445,X443)|~r1(X443,X441)|p1(X441)|r1(skolem0010(X440,X445,X443,X441),skolem0011(X440,X445,X443,X441))|~r1(skolem0012(X440,X445),X442)|~r1(X442,X444)|p1(X444)|~p1(X442),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c47,negated_conjecture,~r1(skolem0001,X436)|~r1(X436,X437)|~r1(X437,X439)|~r1(X439,X438)|p1(X438)|r1(skolem0010(X436,X437,X439,X438),skolem0011(X436,X437,X439,X438))|~p1(skolem0012(X436,X437)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c45,negated_conjecture,~r1(skolem0001,X424)|~r1(X424,X429)|~r1(X429,X427)|~r1(X427,X425)|p1(X425)|r1(X425,skolem0010(X424,X429,X427,X425))|~r1(skolem0012(X424,X429),X426)|~r1(X426,X428)|p1(X428)|~p1(X426),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c40,negated_conjecture,~r1(skolem0001,X418)|~r1(X418,X421)|~r1(X421,X422)|p1(X422)|p1(X421)|~r1(X421,X420)|~p1(skolem0007(X418,X421,X420))|~r1(skolem0008(X418,X421),X419)|~r1(X419,X423)|p1(X423)|~p1(X419),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c37,negated_conjecture,~r1(skolem0001,X406)|~r1(X406,X409)|~r1(X409,X410)|p1(X410)|p1(X409)|~r1(X409,X408)|r1(X408,skolem0007(X406,X409,X408))|~r1(skolem0008(X406,X409),X407)|~r1(X407,X411)|p1(X411)|~p1(X407),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c352,plain,~r1(skolem0001,X405)|~r1(X405,skolem0001)|p1(X405)|p1(skolem0001)|r1(X405,skolem0007(X405,skolem0001,X405))|r1(skolem0001,skolem0008(X405,skolem0001)),inference(factor,[status(thm)],[c335])).
% 13.26/13.57 cnf(c334,plain,~r1(skolem0001,X390)|~r1(X390,X390)|~r1(X390,X389)|p1(X389)|p1(X390)|r1(X390,skolem0007(X390,X390,X390))|r1(X390,skolem0008(X390,X390)),inference(factor,[status(thm)],[c35])).
% 13.26/13.57 cnf(c341,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|r1(skolem0001,skolem0007(skolem0001,skolem0001,skolem0001))|r1(skolem0001,skolem0008(skolem0001,skolem0001)),inference(factor,[status(thm)],[c334])).
% 13.26/13.57 cnf(c342,plain,~r1(skolem0001,X391)|~r1(X391,X391)|p1(X391)|r1(X391,skolem0007(X391,X391,X391))|r1(X391,skolem0008(X391,X391)),inference(factor,[status(thm)],[c334])).
% 13.26/13.57 cnf(c281,plain,~r1(skolem0001,X362)|~r1(X362,X363)|~r1(X363,skolem0001)|p1(skolem0013)|r1(skolem0013,skolem0010(X362,X363,skolem0001,skolem0013))|r1(X363,skolem0012(X362,X363)),inference(resolution,[status(thm)],[c43, c55])).
% 13.26/13.57 cnf(c322,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|r1(skolem0013,skolem0010(skolem0001,skolem0001,skolem0001,skolem0013))|r1(skolem0001,skolem0012(skolem0001,skolem0001)),inference(factor,[status(thm)],[c281])).
% 13.26/13.57 cnf(c320,plain,~r1(skolem0001,X361)|~r1(X361,skolem0001)|p1(skolem0014)|r1(skolem0014,skolem0010(X361,skolem0001,skolem0013,skolem0014))|r1(skolem0001,skolem0012(X361,skolem0001)),inference(resolution,[status(thm)],[c280, c55])).
% 13.26/13.57 cnf(c321,plain,~r1(skolem0001,skolem0001)|p1(skolem0014)|r1(skolem0014,skolem0010(skolem0001,skolem0001,skolem0013,skolem0014))|r1(skolem0001,skolem0012(skolem0001,skolem0001)),inference(factor,[status(thm)],[c320])).
% 13.26/13.57 cnf(c38,negated_conjecture,~r1(skolem0001,X348)|~r1(X348,X349)|~r1(X349,X350)|p1(X350)|p1(X349)|~r1(X349,X351)|~p1(skolem0007(X348,X349,X351))|r1(X349,skolem0008(X348,X349)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c36,negated_conjecture,~r1(skolem0001,X344)|~r1(X344,X345)|~r1(X345,X346)|p1(X346)|p1(X345)|~r1(X345,X347)|r1(X347,skolem0007(X344,X345,X347))|~p1(skolem0008(X344,X345)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c284,plain,~r1(skolem0001,X340)|~r1(X340,skolem0001)|p1(skolem0001)|r1(skolem0001,skolem0010(X340,skolem0001,X340,skolem0001))|r1(skolem0001,skolem0012(X340,skolem0001)),inference(factor,[status(thm)],[c277])).
% 13.26/13.57 cnf(c285,plain,~r1(skolem0001,X322)|~r1(X322,X322)|p1(X322)|r1(X322,skolem0010(X322,X322,X322,X322))|r1(X322,skolem0012(X322,X322)),inference(factor,[status(thm)],[c277])).
% 13.26/13.57 cnf(c291,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|r1(skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001))|r1(skolem0001,skolem0012(skolem0001,skolem0001)),inference(factor,[status(thm)],[c285])).
% 13.26/13.57 cnf(c276,plain,~r1(skolem0001,X333)|~r1(X333,X332)|~r1(X332,skolem0001)|p1(X333)|r1(X333,skolem0010(X333,X332,skolem0001,X333))|r1(X332,skolem0012(X333,X332)),inference(factor,[status(thm)],[c43])).
% 13.26/13.57 cnf(c278,plain,~r1(skolem0001,X323)|~r1(X323,X324)|~r1(X324,X324)|p1(X324)|r1(X324,skolem0010(X323,X324,X324,X324))|r1(X324,skolem0012(X323,X324)),inference(factor,[status(thm)],[c43])).
% 13.26/13.57 cnf(c39,negated_conjecture,~r1(skolem0001,X306)|~r1(X306,X307)|~r1(X307,X308)|p1(X308)|p1(X307)|~r1(X307,X309)|~p1(skolem0007(X306,X307,X309))|~p1(skolem0008(X306,X307)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c231,plain,~r1(skolem0001,X293)|~r1(X293,X292)|~r1(X292,skolem0001)|p1(skolem0013)|p1(skolem0010(X293,X292,skolem0001,skolem0013))|r1(X292,skolem0012(X293,X292)),inference(resolution,[status(thm)],[c52, c55])).
% 13.26/13.57 cnf(c257,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|p1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0013))|r1(skolem0001,skolem0012(skolem0001,skolem0001)),inference(factor,[status(thm)],[c231])).
% 13.26/13.57 cnf(c255,plain,~r1(skolem0001,X291)|~r1(X291,skolem0001)|p1(skolem0014)|p1(skolem0010(X291,skolem0001,skolem0013,skolem0014))|r1(skolem0001,skolem0012(X291,skolem0001)),inference(resolution,[status(thm)],[c230, c55])).
% 13.26/13.57 cnf(c256,plain,~r1(skolem0001,skolem0001)|p1(skolem0014)|p1(skolem0010(skolem0001,skolem0001,skolem0013,skolem0014))|r1(skolem0001,skolem0012(skolem0001,skolem0001)),inference(factor,[status(thm)],[c255])).
% 13.26/13.57 cnf(c234,plain,~r1(skolem0001,X279)|~r1(X279,skolem0001)|p1(skolem0001)|p1(skolem0010(X279,skolem0001,X279,skolem0001))|r1(skolem0001,skolem0012(X279,skolem0001)),inference(factor,[status(thm)],[c227])).
% 13.26/13.57 cnf(c226,plain,~r1(skolem0001,X278)|~r1(X278,X277)|~r1(X277,skolem0001)|p1(X278)|p1(skolem0010(X278,X277,skolem0001,X278))|r1(X277,skolem0012(X278,X277)),inference(factor,[status(thm)],[c52])).
% 13.26/13.57 cnf(c235,plain,~r1(skolem0001,X264)|~r1(X264,X264)|p1(X264)|p1(skolem0010(X264,X264,X264,X264))|r1(X264,skolem0012(X264,X264)),inference(factor,[status(thm)],[c227])).
% 13.26/13.57 cnf(c242,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|p1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001))|r1(skolem0001,skolem0012(skolem0001,skolem0001)),inference(factor,[status(thm)],[c235])).
% 13.26/13.57 cnf(c228,plain,~r1(skolem0001,X265)|~r1(X265,X266)|~r1(X266,X266)|p1(X266)|p1(skolem0010(X265,X266,X266,X266))|r1(X266,skolem0012(X265,X266)),inference(factor,[status(thm)],[c52])).
% 13.26/13.57 cnf(c49,negated_conjecture,~r1(skolem0001,X248)|~r1(X248,X249)|~r1(X249,X251)|~r1(X251,X250)|p1(X250)|~p1(skolem0011(X248,X249,X251,X250))|r1(X249,skolem0012(X248,X249)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c44,negated_conjecture,~r1(skolem0001,X244)|~r1(X244,X245)|~r1(X245,X247)|~r1(X247,X246)|p1(X246)|r1(X246,skolem0010(X244,X245,X247,X246))|~p1(skolem0012(X244,X245)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c53,negated_conjecture,~r1(skolem0001,X240)|~r1(X240,X241)|~r1(X241,X243)|~r1(X243,X242)|p1(X242)|p1(skolem0010(X240,X241,X243,X242))|~p1(skolem0012(X240,X241)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c50,negated_conjecture,~r1(skolem0001,X230)|~r1(X230,X231)|~r1(X231,X233)|~r1(X233,X232)|p1(X232)|~p1(skolem0011(X230,X231,X233,X232))|~p1(skolem0012(X230,X231)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c94,plain,~r1(skolem0001,X154)|~r1(X154,X153)|~r1(X153,X155)|~r1(X155,skolem0001)|p1(skolem0013)|r1(X155,skolem0009(X154,X153,X155)),inference(resolution,[status(thm)],[c41, c55])).
% 13.26/13.57 cnf(c183,plain,~r1(skolem0001,X221)|~r1(X221,skolem0001)|~r1(skolem0001,skolem0001)|p1(skolem0013)|r1(skolem0001,skolem0009(X221,skolem0001,skolem0001)),inference(factor,[status(thm)],[c94])).
% 13.26/13.57 cnf(c181,plain,~r1(skolem0001,skolem0001)|~r1(skolem0001,X220)|~r1(X220,skolem0001)|p1(skolem0013)|r1(skolem0001,skolem0009(skolem0001,X220,skolem0001)),inference(factor,[status(thm)],[c94])).
% 13.26/13.57 cnf(c93,plain,~r1(skolem0001,X142)|~r1(X142,X141)|~r1(X141,X143)|~r1(X143,skolem0013)|p1(skolem0014)|r1(X143,skolem0009(X142,X141,X143)),inference(resolution,[status(thm)],[c41, c56])).
% 13.26/13.57 cnf(c165,plain,~r1(skolem0001,X213)|~r1(X213,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|r1(skolem0013,skolem0009(X213,skolem0013,skolem0013)),inference(factor,[status(thm)],[c93])).
% 13.26/13.57 cnf(c90,plain,~r1(skolem0001,X88)|~r1(X88,X89)|~r1(X89,X87)|~r1(X87,X89)|p1(X87)|r1(X87,skolem0009(X88,X89,X87)),inference(factor,[status(thm)],[c41])).
% 13.26/13.57 cnf(c124,plain,~r1(skolem0001,X199)|~r1(X199,skolem0013)|~r1(skolem0013,skolem0001)|p1(skolem0001)|r1(skolem0001,skolem0009(X199,skolem0013,skolem0001)),inference(resolution,[status(thm)],[c90, c55])).
% 13.26/13.57 cnf(c123,plain,~r1(skolem0001,X198)|~r1(X198,skolem0014)|~r1(skolem0014,skolem0013)|p1(skolem0013)|r1(skolem0013,skolem0009(X198,skolem0014,skolem0013)),inference(resolution,[status(thm)],[c90, c56])).
% 13.26/13.57 cnf(c88,plain,~r1(skolem0001,X132)|~r1(X132,X131)|~r1(X131,X133)|~r1(X133,skolem0001)|p1(X132)|r1(X133,skolem0009(X132,X131,X133)),inference(factor,[status(thm)],[c41])).
% 13.26/13.57 cnf(c152,plain,~r1(skolem0001,X188)|~r1(X188,skolem0001)|~r1(skolem0001,skolem0001)|p1(X188)|r1(skolem0001,skolem0009(X188,skolem0001,skolem0001)),inference(factor,[status(thm)],[c88])).
% 13.26/13.57 cnf(c89,plain,~r1(skolem0001,X76)|~r1(X76,X75)|~r1(X75,X74)|~r1(X74,X76)|p1(X75)|r1(X74,skolem0009(X76,X75,X74)),inference(factor,[status(thm)],[c41])).
% 13.26/13.57 cnf(c102,plain,~r1(skolem0001,skolem0014)|~r1(skolem0014,X185)|~r1(X185,skolem0013)|p1(X185)|r1(skolem0013,skolem0009(skolem0014,X185,skolem0013)),inference(resolution,[status(thm)],[c89, c56])).
% 13.26/13.57 cnf(c209,plain,~r1(skolem0001,skolem0014)|~r1(skolem0014,skolem0001)|p1(skolem0001)|r1(skolem0013,skolem0009(skolem0014,skolem0001,skolem0013)),inference(resolution,[status(thm)],[c102, c55])).
% 13.26/13.57 cnf(c182,plain,~r1(skolem0001,X156)|~r1(X156,skolem0001)|p1(skolem0013)|r1(X156,skolem0009(X156,skolem0001,X156)),inference(factor,[status(thm)],[c94])).
% 13.26/13.57 cnf(c184,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|r1(skolem0001,skolem0009(skolem0001,skolem0001,skolem0001)),inference(factor,[status(thm)],[c182])).
% 13.26/13.57 cnf(c164,plain,~r1(skolem0001,X144)|~r1(X144,skolem0013)|~r1(skolem0013,X144)|p1(skolem0014)|r1(X144,skolem0009(X144,skolem0013,X144)),inference(factor,[status(thm)],[c93])).
% 13.26/13.57 cnf(c167,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0013)|p1(skolem0014)|r1(skolem0013,skolem0009(skolem0013,skolem0013,skolem0013)),inference(factor,[status(thm)],[c164])).
% 13.26/13.57 cnf(c166,plain,~r1(skolem0001,X145)|~r1(X145,X146)|~r1(X146,skolem0001)|p1(skolem0014)|r1(skolem0001,skolem0009(X145,X146,skolem0001)),inference(resolution,[status(thm)],[c93, c55])).
% 13.26/13.57 cnf(c169,plain,~r1(skolem0001,skolem0001)|p1(skolem0014)|r1(skolem0001,skolem0009(skolem0001,skolem0001,skolem0001)),inference(factor,[status(thm)],[c166])).
% 13.26/13.57 cnf(c120,plain,~r1(skolem0001,X90)|~r1(X90,X91)|~r1(X91,X90)|p1(X90)|r1(X90,skolem0009(X90,X91,X90)),inference(factor,[status(thm)],[c90])).
% 13.26/13.57 cnf(c130,plain,~r1(skolem0001,skolem0014)|~r1(skolem0014,skolem0013)|p1(skolem0014)|r1(skolem0014,skolem0009(skolem0014,skolem0013,skolem0014)),inference(resolution,[status(thm)],[c120, c56])).
% 13.26/13.57 cnf(c119,plain,~r1(skolem0001,X121)|~r1(X121,X121)|~r1(X121,skolem0001)|p1(skolem0001)|r1(skolem0001,skolem0009(X121,X121,skolem0001)),inference(factor,[status(thm)],[c90])).
% 13.26/13.57 cnf(c91,plain,~r1(skolem0001,X117)|~r1(X117,X116)|~r1(X116,X115)|~r1(X115,X115)|p1(X115)|r1(X115,skolem0009(X117,X116,X115)),inference(factor,[status(thm)],[c41])).
% 13.26/13.57 cnf(c121,plain,~r1(skolem0001,X104)|~r1(X104,X103)|~r1(X103,X103)|p1(X103)|r1(X103,skolem0009(X104,X103,X103)),inference(factor,[status(thm)],[c90])).
% 13.26/13.57 cnf(c127,plain,~r1(skolem0001,X102)|~r1(X102,skolem0001)|p1(X102)|r1(X102,skolem0009(X102,skolem0001,X102)),inference(factor,[status(thm)],[c120])).
% 13.26/13.57 cnf(c98,plain,~r1(skolem0001,X80)|~r1(X80,X79)|~r1(X79,skolem0001)|p1(X79)|r1(skolem0001,skolem0009(X80,X79,skolem0001)),inference(factor,[status(thm)],[c89])).
% 13.26/13.57 cnf(c99,plain,~r1(skolem0001,X77)|~r1(X77,X77)|p1(X77)|r1(X77,skolem0009(X77,X77,X77)),inference(factor,[status(thm)],[c89])).
% 13.26/13.57 cnf(c106,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|r1(skolem0001,skolem0009(skolem0001,skolem0001,skolem0001)),inference(factor,[status(thm)],[c99])).
% 13.26/13.57 cnf(c63,negated_conjecture,~r1(skolem0014,X49)|p1(X49)|p1(skolem0016(X49)),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 cnf(c57,negated_conjecture,~p1(skolem0014),inference(split_conjunct,[status(thm)],[c6])).
% 13.26/13.57 % SZS output end Saturation
% 13.26/13.57
% 13.26/13.57 % Initial clauses : 57
% 13.26/13.57 % Processed clauses : 587
% 13.26/13.57 % Factors computed : 1087
% 13.26/13.57 % Resolvents computed: 670
% 13.26/13.57 % Tautologies deleted: 654
% 13.26/13.57 % Forward subsumed : 573
% 13.26/13.57 % Backward subsumed : 87
% 13.26/13.57 % -------- CPU Time ---------
% 13.26/13.57 % User time : 13.175 s
% 13.26/13.57 % System time : 0.028 s
% 13.26/13.57 % Total time : 13.203 s
%------------------------------------------------------------------------------