%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL639+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:58:46 PM UTC 2026
% Result : CounterSatisfiable 0.67s 0.99s
% Output : Saturation 0.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL639+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 : n007.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.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 02:39:24 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.42 (re.compile("\."), Token.FullStop),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.42 (re.compile("\("), Token.OpenPar),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.42 (re.compile("\)"), Token.ClosePar),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.42 (re.compile("\["), Token.OpenSquare),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.42 (re.compile("~\|"), Token.Nor),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.42 (re.compile("\|"), Token.Or),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.43 (re.compile("\?"), Token.Existential),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.50 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.31/0.59 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.59 """
% 0.67/0.99 % Version: 1.5
% 0.67/0.99 % SZS status CounterSatisfiable
% 0.67/0.99 % SZS output start Saturation
% 0.67/0.99 fof(main,conjecture,(~(?[X]:(~(((((((~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(~((~p1(Y))&(![X]:((~r1(Y,X))|p1(X))))))))))&(![X]:(((~r1(Y,X))|p1(X))|(~(![Y]:((~r1(X,Y))|p1(Y)))))))))))|(~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(~((~p1(Y))&(~(![X]:((~r1(Y,X))|(~p1(X))))))))))))&(![X]:(((~r1(Y,X))|p1(X))|(![Y]:((~r1(X,Y))|(~p1(Y))))))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|(~p1(X))))&(![X]:((~r1(Y,X))|p1(X)))))))))|(~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|(~p1(X))))))))))&(![X]:((~r1(Y,X))|(~(![Y]:((~r1(X,Y))|(~p1(Y)))))))))))))|(~(![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))|$false)))))))|(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(![Y]:((~r1(X,Y))|p1(Y)))))))|(![X]:((~r1(Y,X))|p1(X))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 0.67/0.99 fof(c0,negated_conjecture,(~(~(?[X]:(~(((((((~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(~((~p1(Y))&(![X]:((~r1(Y,X))|p1(X))))))))))&(![X]:(((~r1(Y,X))|p1(X))|(~(![Y]:((~r1(X,Y))|p1(Y)))))))))))|(~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(~((~p1(Y))&(~(![X]:((~r1(Y,X))|(~p1(X))))))))))))&(![X]:(((~r1(Y,X))|p1(X))|(![Y]:((~r1(X,Y))|(~p1(Y))))))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|(~p1(X))))&(![X]:((~r1(Y,X))|p1(X)))))))))|(~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|(~p1(X))))))))))&(![X]:((~r1(Y,X))|(~(![Y]:((~r1(X,Y))|(~p1(Y)))))))))))))|(~(![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))|$false)))))))|(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(![Y]:((~r1(X,Y))|p1(Y)))))))|(![X]:((~r1(Y,X))|p1(X)))))))))),inference(assume_negation,[status(cth)],[main])).
% 0.67/0.99 fof(c1,negated_conjecture,(~(~(?[X]:(~(((((((~(![Y]:(~r1(X,Y)|(~((~(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(~(~p1(Y)&(![X]:(~r1(Y,X)|p1(X))))))))))&(![X]:((~r1(Y,X)|p1(X))|(~(![Y]:(~r1(X,Y)|p1(Y)))))))))))|(~(![Y]:(~r1(X,Y)|(~((~(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(~(~p1(Y)&(~(![X]:(~r1(Y,X)|~p1(X)))))))))))&(![X]:((~r1(Y,X)|p1(X))|(![Y]:(~r1(X,Y)|~p1(Y)))))))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|~p1(X)))&(![X]:(~r1(Y,X)|p1(X)))))))))|(~(![Y]:(~r1(X,Y)|(~((~(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(~(![X]:(~r1(Y,X)|~p1(X)))))))))&(![X]:(~r1(Y,X)|(~(![Y]:(~r1(X,Y)|~p1(Y))))))))))))|(~(![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)))))))|(![Y]:((~r1(X,Y)|(![X]:(~r1(Y,X)|(~(![Y]:(~r1(X,Y)|p1(Y)))))))|(![X]:(~r1(Y,X)|p1(X)))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.67/0.99 fof(c2,negated_conjecture,(?[X]:(((((((![Y]:(~r1(X,Y)|((![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(p1(Y)|(?[X]:(r1(Y,X)&~p1(X))))))))|(?[X]:((r1(Y,X)&~p1(X))&(![Y]:(~r1(X,Y)|p1(Y))))))))&(![Y]:(~r1(X,Y)|((![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(p1(Y)|(![X]:(~r1(Y,X)|~p1(X))))))))|(?[X]:((r1(Y,X)&~p1(X))&(?[Y]:(r1(X,Y)&p1(Y)))))))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&p1(X)))|(?[X]:(r1(Y,X)&~p1(X)))))))&(![Y]:(~r1(X,Y)|((![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(?[X]:(r1(Y,X)&p1(X)))))))|(?[X]:(r1(Y,X)&(![Y]:(~r1(X,Y)|~p1(Y)))))))))&(![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)))))&(?[Y]:((r1(X,Y)&(?[X]:(r1(Y,X)&(![Y]:(~r1(X,Y)|p1(Y))))))&(?[X]:(r1(Y,X)&~p1(X))))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.67/0.99 fof(c3,negated_conjecture,(?[X2]:(((((((![X3]:(~r1(X2,X3)|((![X4]:(~r1(X3,X4)|(![X5]:(~r1(X4,X5)|(p1(X5)|(?[X6]:(r1(X5,X6)&~p1(X6))))))))|(?[X7]:((r1(X3,X7)&~p1(X7))&(![X8]:(~r1(X7,X8)|p1(X8))))))))&(![X9]:(~r1(X2,X9)|((![X10]:(~r1(X9,X10)|(![X11]:(~r1(X10,X11)|(p1(X11)|(![X12]:(~r1(X11,X12)|~p1(X12))))))))|(?[X13]:((r1(X9,X13)&~p1(X13))&(?[X14]:(r1(X13,X14)&p1(X14)))))))))&(![X15]:(~r1(X2,X15)|((?[X16]:(r1(X15,X16)&p1(X16)))|(?[X17]:(r1(X15,X17)&~p1(X17)))))))&(![X18]:(~r1(X2,X18)|((![X19]:(~r1(X18,X19)|(![X20]:(~r1(X19,X20)|(?[X21]:(r1(X20,X21)&p1(X21)))))))|(?[X22]:(r1(X18,X22)&(![X23]:(~r1(X22,X23)|~p1(X23)))))))))&(![X24]:(~r1(X2,X24)|((![X25]:(~r1(X24,X25)|(![X26]:(~r1(X25,X26)|p1(X26)))))|(?[X27]:(r1(X24,X27)&~p1(X27)))))))&(![X28]:(~r1(X2,X28)|(?[X29]:r1(X28,X29)))))&(?[X30]:((r1(X2,X30)&(?[X31]:(r1(X30,X31)&(![X32]:(~r1(X31,X32)|p1(X32))))))&(?[X33]:(r1(X30,X33)&~p1(X33))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.67/0.99 fof(c5,negated_conjecture,(![X3]:(![X4]:(![X5]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X15]:(![X18]:(![X19]:(![X20]:(![X23]:(![X24]:(![X25]:(![X26]:(![X28]:(![X32]:(((((((~r1(skolem0001,X3)|((~r1(X3,X4)|(~r1(X4,X5)|(p1(X5)|(r1(X5,skolem0002(X3,X4,X5))&~p1(skolem0002(X3,X4,X5))))))|((r1(X3,skolem0003(X3))&~p1(skolem0003(X3)))&(~r1(skolem0003(X3),X8)|p1(X8)))))&(~r1(skolem0001,X9)|((~r1(X9,X10)|(~r1(X10,X11)|(p1(X11)|(~r1(X11,X12)|~p1(X12)))))|((r1(X9,skolem0004(X9))&~p1(skolem0004(X9)))&(r1(skolem0004(X9),skolem0005(X9))&p1(skolem0005(X9)))))))&(~r1(skolem0001,X15)|((r1(X15,skolem0006(X15))&p1(skolem0006(X15)))|(r1(X15,skolem0007(X15))&~p1(skolem0007(X15))))))&(~r1(skolem0001,X18)|((~r1(X18,X19)|(~r1(X19,X20)|(r1(X20,skolem0008(X18,X19,X20))&p1(skolem0008(X18,X19,X20)))))|(r1(X18,skolem0009(X18))&(~r1(skolem0009(X18),X23)|~p1(X23))))))&(~r1(skolem0001,X24)|((~r1(X24,X25)|(~r1(X25,X26)|p1(X26)))|(r1(X24,skolem0010(X24))&~p1(skolem0010(X24))))))&(~r1(skolem0001,X28)|r1(X28,skolem0011(X28))))&((r1(skolem0001,skolem0012)&(r1(skolem0012,skolem0013)&(~r1(skolem0013,X32)|p1(X32))))&(r1(skolem0012,skolem0014)&~p1(skolem0014)))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,(((((((![X3]:(~r1(skolem0001,X3)|((![X4]:(~r1(X3,X4)|(![X5]:(~r1(X4,X5)|(p1(X5)|(r1(X5,skolem0002(X3,X4,X5))&~p1(skolem0002(X3,X4,X5))))))))|((r1(X3,skolem0003(X3))&~p1(skolem0003(X3)))&(![X8]:(~r1(skolem0003(X3),X8)|p1(X8)))))))&(![X9]:(~r1(skolem0001,X9)|((![X10]:(~r1(X9,X10)|(![X11]:(~r1(X10,X11)|(p1(X11)|(![X12]:(~r1(X11,X12)|~p1(X12))))))))|((r1(X9,skolem0004(X9))&~p1(skolem0004(X9)))&(r1(skolem0004(X9),skolem0005(X9))&p1(skolem0005(X9))))))))&(![X15]:(~r1(skolem0001,X15)|((r1(X15,skolem0006(X15))&p1(skolem0006(X15)))|(r1(X15,skolem0007(X15))&~p1(skolem0007(X15)))))))&(![X18]:(~r1(skolem0001,X18)|((![X19]:(~r1(X18,X19)|(![X20]:(~r1(X19,X20)|(r1(X20,skolem0008(X18,X19,X20))&p1(skolem0008(X18,X19,X20)))))))|(r1(X18,skolem0009(X18))&(![X23]:(~r1(skolem0009(X18),X23)|~p1(X23))))))))&(![X24]:(~r1(skolem0001,X24)|((![X25]:(~r1(X24,X25)|(![X26]:(~r1(X25,X26)|p1(X26)))))|(r1(X24,skolem0010(X24))&~p1(skolem0010(X24)))))))&(![X28]:(~r1(skolem0001,X28)|r1(X28,skolem0011(X28)))))&((r1(skolem0001,skolem0012)&(r1(skolem0012,skolem0013)&(![X32]:(~r1(skolem0013,X32)|p1(X32)))))&(r1(skolem0012,skolem0014)&~p1(skolem0014)))),inference(skolemize,[status(esa)],[c3])).])).
% 0.67/0.99 fof(c6,negated_conjecture,(![X3]:(![X4]:(![X5]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X15]:(![X18]:(![X19]:(![X20]:(![X23]:(![X24]:(![X25]:(![X26]:(![X28]:(![X32]:((((((((((~r1(skolem0001,X3)|((~r1(X3,X4)|(~r1(X4,X5)|(p1(X5)|r1(X5,skolem0002(X3,X4,X5)))))|r1(X3,skolem0003(X3))))&(~r1(skolem0001,X3)|((~r1(X3,X4)|(~r1(X4,X5)|(p1(X5)|r1(X5,skolem0002(X3,X4,X5)))))|~p1(skolem0003(X3)))))&(~r1(skolem0001,X3)|((~r1(X3,X4)|(~r1(X4,X5)|(p1(X5)|r1(X5,skolem0002(X3,X4,X5)))))|(~r1(skolem0003(X3),X8)|p1(X8)))))&(((~r1(skolem0001,X3)|((~r1(X3,X4)|(~r1(X4,X5)|(p1(X5)|~p1(skolem0002(X3,X4,X5)))))|r1(X3,skolem0003(X3))))&(~r1(skolem0001,X3)|((~r1(X3,X4)|(~r1(X4,X5)|(p1(X5)|~p1(skolem0002(X3,X4,X5)))))|~p1(skolem0003(X3)))))&(~r1(skolem0001,X3)|((~r1(X3,X4)|(~r1(X4,X5)|(p1(X5)|~p1(skolem0002(X3,X4,X5)))))|(~r1(skolem0003(X3),X8)|p1(X8))))))&(((~r1(skolem0001,X9)|((~r1(X9,X10)|(~r1(X10,X11)|(p1(X11)|(~r1(X11,X12)|~p1(X12)))))|r1(X9,skolem0004(X9))))&(~r1(skolem0001,X9)|((~r1(X9,X10)|(~r1(X10,X11)|(p1(X11)|(~r1(X11,X12)|~p1(X12)))))|~p1(skolem0004(X9)))))&((~r1(skolem0001,X9)|((~r1(X9,X10)|(~r1(X10,X11)|(p1(X11)|(~r1(X11,X12)|~p1(X12)))))|r1(skolem0004(X9),skolem0005(X9))))&(~r1(skolem0001,X9)|((~r1(X9,X10)|(~r1(X10,X11)|(p1(X11)|(~r1(X11,X12)|~p1(X12)))))|p1(skolem0005(X9)))))))&(((~r1(skolem0001,X15)|(r1(X15,skolem0006(X15))|r1(X15,skolem0007(X15))))&(~r1(skolem0001,X15)|(r1(X15,skolem0006(X15))|~p1(skolem0007(X15)))))&((~r1(skolem0001,X15)|(p1(skolem0006(X15))|r1(X15,skolem0007(X15))))&(~r1(skolem0001,X15)|(p1(skolem0006(X15))|~p1(skolem0007(X15)))))))&(((~r1(skolem0001,X18)|((~r1(X18,X19)|(~r1(X19,X20)|r1(X20,skolem0008(X18,X19,X20))))|r1(X18,skolem0009(X18))))&(~r1(skolem0001,X18)|((~r1(X18,X19)|(~r1(X19,X20)|r1(X20,skolem0008(X18,X19,X20))))|(~r1(skolem0009(X18),X23)|~p1(X23)))))&((~r1(skolem0001,X18)|((~r1(X18,X19)|(~r1(X19,X20)|p1(skolem0008(X18,X19,X20))))|r1(X18,skolem0009(X18))))&(~r1(skolem0001,X18)|((~r1(X18,X19)|(~r1(X19,X20)|p1(skolem0008(X18,X19,X20))))|(~r1(skolem0009(X18),X23)|~p1(X23)))))))&((~r1(skolem0001,X24)|((~r1(X24,X25)|(~r1(X25,X26)|p1(X26)))|r1(X24,skolem0010(X24))))&(~r1(skolem0001,X24)|((~r1(X24,X25)|(~r1(X25,X26)|p1(X26)))|~p1(skolem0010(X24))))))&(~r1(skolem0001,X28)|r1(X28,skolem0011(X28))))&((r1(skolem0001,skolem0012)&(r1(skolem0012,skolem0013)&(~r1(skolem0013,X32)|p1(X32))))&(r1(skolem0012,skolem0014)&~p1(skolem0014)))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 0.67/0.99 cnf(c28,negated_conjecture,r1(skolem0001,skolem0012),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/0.99 cnf(c17,negated_conjecture,~r1(skolem0001,X45)|r1(X45,skolem0006(X45))|r1(X45,skolem0007(X45)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/0.99 cnf(c42,plain,r1(skolem0012,skolem0006(skolem0012))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c17, c28])).
% 0.67/0.99 cnf(c15,negated_conjecture,~r1(skolem0001,X100)|~r1(X100,X98)|~r1(X98,X101)|p1(X101)|~r1(X101,X99)|~p1(X99)|r1(skolem0004(X100),skolem0005(X100)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/0.99 cnf(c107,plain,~r1(skolem0001,X137)|~r1(X137,X136)|~r1(X136,X137)|p1(X137)|~p1(X136)|r1(skolem0004(X137),skolem0005(X137)),inference(factor,[status(thm)],[c15])).
% 0.67/0.99 cnf(c155,plain,~r1(skolem0001,skolem0007(skolem0012))|~r1(skolem0007(skolem0012),skolem0012)|p1(skolem0007(skolem0012))|~p1(skolem0012)|r1(skolem0004(skolem0007(skolem0012)),skolem0005(skolem0007(skolem0012)))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c107, c42])).
% 0.67/0.99 cnf(c19,negated_conjecture,~r1(skolem0001,X41)|p1(skolem0006(X41))|r1(X41,skolem0007(X41)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/0.99 cnf(c40,plain,p1(skolem0006(skolem0012))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c19, c28])).
% 0.67/0.99 cnf(c158,plain,~r1(skolem0001,skolem0007(skolem0012))|~r1(skolem0007(skolem0012),skolem0012)|p1(skolem0007(skolem0012))|~p1(skolem0012)|r1(skolem0004(skolem0007(skolem0012)),skolem0005(skolem0007(skolem0012)))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c107, c40])).
% 0.67/0.99 cnf(c7,negated_conjecture,~r1(skolem0001,X35)|~r1(X35,X36)|~r1(X36,X37)|p1(X37)|r1(X37,skolem0002(X35,X36,X37))|r1(X35,skolem0003(X35)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/0.99 cnf(c44,plain,r1(skolem0012,skolem0006(skolem0012))|~r1(skolem0001,X162)|~r1(X162,skolem0012)|p1(skolem0007(skolem0012))|r1(skolem0007(skolem0012),skolem0002(X162,skolem0012,skolem0007(skolem0012)))|r1(X162,skolem0003(X162)),inference(resolution,[status(thm)],[c42, c7])).
% 0.67/0.99 cnf(c179,plain,r1(skolem0012,skolem0006(skolem0012))|~r1(skolem0001,skolem0001)|p1(skolem0007(skolem0012))|r1(skolem0007(skolem0012),skolem0002(skolem0001,skolem0012,skolem0007(skolem0012)))|r1(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c44, c28])).
% 0.67/0.99 cnf(c41,plain,p1(skolem0006(skolem0012))|~r1(skolem0001,X155)|~r1(X155,skolem0012)|p1(skolem0007(skolem0012))|r1(skolem0007(skolem0012),skolem0002(X155,skolem0012,skolem0007(skolem0012)))|r1(X155,skolem0003(X155)),inference(resolution,[status(thm)],[c40, c7])).
% 0.67/0.99 cnf(c174,plain,p1(skolem0006(skolem0012))|~r1(skolem0001,skolem0001)|p1(skolem0007(skolem0012))|r1(skolem0007(skolem0012),skolem0002(skolem0001,skolem0012,skolem0007(skolem0012)))|r1(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c41, c28])).
% 0.67/0.99 cnf(c27,negated_conjecture,~r1(skolem0001,X38)|r1(X38,skolem0011(X38)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/0.99 cnf(c38,plain,r1(skolem0012,skolem0011(skolem0012)),inference(resolution,[status(thm)],[c27, c28])).
% 0.67/0.99 cnf(c154,plain,~r1(skolem0001,skolem0011(skolem0012))|~r1(skolem0011(skolem0012),skolem0012)|p1(skolem0011(skolem0012))|~p1(skolem0012)|r1(skolem0004(skolem0011(skolem0012)),skolem0005(skolem0011(skolem0012))),inference(resolution,[status(thm)],[c107, c38])).
% 0.67/0.99 cnf(c16,negated_conjecture,~r1(skolem0001,X107)|~r1(X107,X105)|~r1(X105,X108)|p1(X108)|~r1(X108,X106)|~p1(X106)|p1(skolem0005(X107)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/0.99 cnf(c120,plain,~r1(skolem0001,X109)|~r1(X109,X110)|~r1(X110,X109)|p1(X109)|~p1(X110)|p1(skolem0005(X109)),inference(factor,[status(thm)],[c16])).
% 0.67/0.99 cnf(c135,plain,~r1(skolem0001,skolem0007(skolem0012))|~r1(skolem0007(skolem0012),skolem0012)|p1(skolem0007(skolem0012))|~p1(skolem0012)|p1(skolem0005(skolem0007(skolem0012)))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c120, c40])).
% 0.67/0.99 cnf(c115,plain,~r1(skolem0001,X217)|~r1(X217,X216)|~r1(X216,skolem0012)|p1(skolem0012)|~p1(skolem0006(skolem0012))|r1(skolem0004(X217),skolem0005(X217))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c15, c42])).
% 0.67/0.99 cnf(c206,plain,~r1(skolem0001,X219)|~r1(X219,X218)|~r1(X218,skolem0012)|p1(skolem0012)|r1(skolem0004(X219),skolem0005(X219))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c115, c40])).
% 0.67/0.99 cnf(c208,plain,~r1(skolem0001,skolem0012)|~r1(skolem0012,skolem0012)|p1(skolem0012)|r1(skolem0004(skolem0012),skolem0005(skolem0012))|r1(skolem0012,skolem0007(skolem0012)),inference(factor,[status(thm)],[c206])).
% 0.67/0.99 cnf(c209,plain,~r1(skolem0001,X220)|~r1(X220,skolem0001)|p1(skolem0012)|r1(skolem0004(X220),skolem0005(X220))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c206, c28])).
% 0.67/0.99 cnf(c210,plain,~r1(skolem0001,skolem0001)|p1(skolem0012)|r1(skolem0004(skolem0001),skolem0005(skolem0001))|r1(skolem0012,skolem0007(skolem0012)),inference(factor,[status(thm)],[c209])).
% 0.67/0.99 cnf(c132,plain,~r1(skolem0001,skolem0007(skolem0012))|~r1(skolem0007(skolem0012),skolem0012)|p1(skolem0007(skolem0012))|~p1(skolem0012)|p1(skolem0005(skolem0007(skolem0012)))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c120, c42])).
% 0.67/0.99 cnf(c110,plain,~r1(skolem0001,X215)|~r1(X215,X214)|~r1(X214,skolem0012)|p1(skolem0012)|~p1(skolem0007(skolem0012))|r1(skolem0004(X215),skolem0005(X215))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c15, c42])).
% 0.67/0.99 cnf(c21,negated_conjecture,~r1(skolem0001,X96)|~r1(X96,X95)|~r1(X95,X97)|r1(X97,skolem0008(X96,X95,X97))|r1(X96,skolem0009(X96)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c105,plain,~r1(skolem0001,X213)|~r1(X213,skolem0012)|r1(skolem0006(skolem0012),skolem0008(X213,skolem0012,skolem0006(skolem0012)))|r1(X213,skolem0009(X213))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c21, c42])).
% 0.67/1.00 cnf(c205,plain,~r1(skolem0001,skolem0001)|r1(skolem0006(skolem0012),skolem0008(skolem0001,skolem0012,skolem0006(skolem0012)))|r1(skolem0001,skolem0009(skolem0001))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c105, c28])).
% 0.67/1.00 cnf(c100,plain,~r1(skolem0001,X212)|~r1(X212,skolem0012)|r1(skolem0007(skolem0012),skolem0008(X212,skolem0012,skolem0007(skolem0012)))|r1(X212,skolem0009(X212))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c21, c42])).
% 0.67/1.00 cnf(c204,plain,~r1(skolem0001,skolem0001)|r1(skolem0007(skolem0012),skolem0008(skolem0001,skolem0012,skolem0007(skolem0012)))|r1(skolem0001,skolem0009(skolem0001))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c100, c28])).
% 0.67/1.00 cnf(c113,plain,~r1(skolem0001,X211)|~r1(X211,X210)|~r1(X210,skolem0012)|p1(skolem0012)|~p1(skolem0007(skolem0012))|r1(skolem0004(X211),skolem0005(X211))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c15, c40])).
% 0.67/1.00 cnf(c128,plain,~r1(skolem0001,X206)|~r1(X206,X205)|~r1(X205,skolem0012)|p1(skolem0012)|~p1(skolem0006(skolem0012))|p1(skolem0005(X206))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c16, c42])).
% 0.67/1.00 cnf(c199,plain,~r1(skolem0001,X208)|~r1(X208,X207)|~r1(X207,skolem0012)|p1(skolem0012)|p1(skolem0005(X208))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c128, c40])).
% 0.67/1.00 cnf(c201,plain,~r1(skolem0001,skolem0012)|~r1(skolem0012,skolem0012)|p1(skolem0012)|p1(skolem0005(skolem0012))|r1(skolem0012,skolem0007(skolem0012)),inference(factor,[status(thm)],[c199])).
% 0.67/1.00 cnf(c13,negated_conjecture,~r1(skolem0001,X81)|~r1(X81,X79)|~r1(X79,X82)|p1(X82)|~r1(X82,X80)|~p1(X80)|r1(X81,skolem0004(X81)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c75,plain,~r1(skolem0001,X85)|~r1(X85,X84)|~r1(X84,X85)|p1(X85)|~p1(X84)|r1(X85,skolem0004(X85)),inference(factor,[status(thm)],[c13])).
% 0.67/1.00 cnf(c91,plain,~r1(skolem0001,skolem0007(skolem0012))|~r1(skolem0007(skolem0012),skolem0012)|p1(skolem0007(skolem0012))|~p1(skolem0012)|r1(skolem0007(skolem0012),skolem0004(skolem0007(skolem0012)))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c75, c40])).
% 0.67/1.00 cnf(c202,plain,~r1(skolem0001,X209)|~r1(X209,skolem0001)|p1(skolem0012)|p1(skolem0005(X209))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c199, c28])).
% 0.67/1.00 cnf(c203,plain,~r1(skolem0001,skolem0001)|p1(skolem0012)|p1(skolem0005(skolem0001))|r1(skolem0012,skolem0007(skolem0012)),inference(factor,[status(thm)],[c202])).
% 0.67/1.00 cnf(c123,plain,~r1(skolem0001,X204)|~r1(X204,X203)|~r1(X203,skolem0012)|p1(skolem0012)|~p1(skolem0007(skolem0012))|p1(skolem0005(X204))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c16, c42])).
% 0.67/1.00 cnf(c88,plain,~r1(skolem0001,skolem0007(skolem0012))|~r1(skolem0007(skolem0012),skolem0012)|p1(skolem0007(skolem0012))|~p1(skolem0012)|r1(skolem0007(skolem0012),skolem0004(skolem0007(skolem0012)))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c75, c42])).
% 0.67/1.00 cnf(c103,plain,~r1(skolem0001,X202)|~r1(X202,skolem0012)|r1(skolem0007(skolem0012),skolem0008(X202,skolem0012,skolem0007(skolem0012)))|r1(X202,skolem0009(X202))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c21, c40])).
% 0.67/1.00 cnf(c198,plain,~r1(skolem0001,skolem0001)|r1(skolem0007(skolem0012),skolem0008(skolem0001,skolem0012,skolem0007(skolem0012)))|r1(skolem0001,skolem0009(skolem0001))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c103, c28])).
% 0.67/1.00 cnf(c39,plain,~r1(skolem0001,X151)|~r1(X151,skolem0012)|p1(skolem0011(skolem0012))|r1(skolem0011(skolem0012),skolem0002(X151,skolem0012,skolem0011(skolem0012)))|r1(X151,skolem0003(X151)),inference(resolution,[status(thm)],[c38, c7])).
% 0.67/1.00 cnf(c170,plain,~r1(skolem0001,skolem0001)|p1(skolem0011(skolem0012))|r1(skolem0011(skolem0012),skolem0002(skolem0001,skolem0012,skolem0011(skolem0012)))|r1(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c39, c28])).
% 0.67/1.00 cnf(c126,plain,~r1(skolem0001,X201)|~r1(X201,X200)|~r1(X200,skolem0012)|p1(skolem0012)|~p1(skolem0007(skolem0012))|p1(skolem0005(X201))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c16, c40])).
% 0.67/1.00 cnf(c23,negated_conjecture,~r1(skolem0001,X69)|~r1(X69,X68)|~r1(X68,X70)|p1(skolem0008(X69,X68,X70))|r1(X69,skolem0009(X69)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c69,plain,~r1(skolem0001,X187)|~r1(X187,skolem0012)|p1(skolem0008(X187,skolem0012,skolem0006(skolem0012)))|r1(X187,skolem0009(X187))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c23, c42])).
% 0.67/1.00 cnf(c191,plain,~r1(skolem0001,skolem0001)|p1(skolem0008(skolem0001,skolem0012,skolem0006(skolem0012)))|r1(skolem0001,skolem0009(skolem0001))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c69, c28])).
% 0.67/1.00 cnf(c87,plain,~r1(skolem0001,skolem0011(skolem0012))|~r1(skolem0011(skolem0012),skolem0012)|p1(skolem0011(skolem0012))|~p1(skolem0012)|r1(skolem0011(skolem0012),skolem0004(skolem0011(skolem0012))),inference(resolution,[status(thm)],[c75, c38])).
% 0.67/1.00 cnf(c83,plain,~r1(skolem0001,X196)|~r1(X196,X195)|~r1(X195,skolem0012)|p1(skolem0012)|~p1(skolem0006(skolem0012))|r1(X196,skolem0004(X196))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c13, c42])).
% 0.67/1.00 cnf(c193,plain,~r1(skolem0001,X197)|~r1(X197,X198)|~r1(X198,skolem0012)|p1(skolem0012)|r1(X197,skolem0004(X197))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c83, c40])).
% 0.67/1.00 cnf(c195,plain,~r1(skolem0001,skolem0012)|~r1(skolem0012,skolem0012)|p1(skolem0012)|r1(skolem0012,skolem0004(skolem0012))|r1(skolem0012,skolem0007(skolem0012)),inference(factor,[status(thm)],[c193])).
% 0.67/1.00 cnf(c196,plain,~r1(skolem0001,X199)|~r1(X199,skolem0001)|p1(skolem0012)|r1(X199,skolem0004(X199))|r1(skolem0012,skolem0007(skolem0012)),inference(resolution,[status(thm)],[c193, c28])).
% 0.67/1.00 cnf(c197,plain,~r1(skolem0001,skolem0001)|p1(skolem0012)|r1(skolem0001,skolem0004(skolem0001))|r1(skolem0012,skolem0007(skolem0012)),inference(factor,[status(thm)],[c196])).
% 0.67/1.00 cnf(c64,plain,~r1(skolem0001,X174)|~r1(X174,skolem0012)|p1(skolem0008(X174,skolem0012,skolem0007(skolem0012)))|r1(X174,skolem0009(X174))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c23, c42])).
% 0.67/1.00 cnf(c183,plain,~r1(skolem0001,skolem0001)|p1(skolem0008(skolem0001,skolem0012,skolem0007(skolem0012)))|r1(skolem0001,skolem0009(skolem0001))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c64, c28])).
% 0.67/1.00 cnf(c131,plain,~r1(skolem0001,skolem0011(skolem0012))|~r1(skolem0011(skolem0012),skolem0012)|p1(skolem0011(skolem0012))|~p1(skolem0012)|p1(skolem0005(skolem0011(skolem0012))),inference(resolution,[status(thm)],[c120, c38])).
% 0.67/1.00 cnf(c67,plain,~r1(skolem0001,X179)|~r1(X179,skolem0012)|p1(skolem0008(X179,skolem0012,skolem0007(skolem0012)))|r1(X179,skolem0009(X179))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c23, c40])).
% 0.67/1.00 cnf(c186,plain,~r1(skolem0001,skolem0001)|p1(skolem0008(skolem0001,skolem0012,skolem0007(skolem0012)))|r1(skolem0001,skolem0009(skolem0001))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c67, c28])).
% 0.67/1.00 cnf(c109,plain,~r1(skolem0001,X194)|~r1(X194,X193)|~r1(X193,skolem0012)|p1(skolem0012)|~p1(skolem0011(skolem0012))|r1(skolem0004(X194),skolem0005(X194)),inference(resolution,[status(thm)],[c15, c38])).
% 0.67/1.00 cnf(c99,plain,~r1(skolem0001,X190)|~r1(X190,skolem0012)|r1(skolem0011(skolem0012),skolem0008(X190,skolem0012,skolem0011(skolem0012)))|r1(X190,skolem0009(X190)),inference(resolution,[status(thm)],[c21, c38])).
% 0.67/1.00 cnf(c192,plain,~r1(skolem0001,skolem0001)|r1(skolem0011(skolem0012),skolem0008(skolem0001,skolem0012,skolem0011(skolem0012)))|r1(skolem0001,skolem0009(skolem0001)),inference(resolution,[status(thm)],[c99, c28])).
% 0.67/1.00 cnf(c81,plain,~r1(skolem0001,X192)|~r1(X192,X191)|~r1(X191,skolem0012)|p1(skolem0012)|~p1(skolem0007(skolem0012))|r1(X192,skolem0004(X192))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c13, c40])).
% 0.67/1.00 cnf(c29,negated_conjecture,r1(skolem0012,skolem0013),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c114,plain,~r1(skolem0001,X183)|~r1(X183,X182)|~r1(X182,skolem0012)|p1(skolem0012)|~p1(skolem0013)|r1(skolem0004(X183),skolem0005(X183)),inference(resolution,[status(thm)],[c15, c29])).
% 0.67/1.00 cnf(c188,plain,~r1(skolem0001,skolem0012)|~r1(skolem0012,skolem0012)|p1(skolem0012)|~p1(skolem0013)|r1(skolem0004(skolem0012),skolem0005(skolem0012)),inference(factor,[status(thm)],[c114])).
% 0.67/1.00 cnf(c37,plain,~r1(skolem0001,X145)|~r1(X145,skolem0012)|p1(skolem0013)|r1(skolem0013,skolem0002(X145,skolem0012,skolem0013))|r1(X145,skolem0003(X145)),inference(resolution,[status(thm)],[c7, c29])).
% 0.67/1.00 cnf(c165,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|r1(skolem0013,skolem0002(skolem0001,skolem0012,skolem0013))|r1(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c37, c28])).
% 0.67/1.00 cnf(c36,plain,~r1(skolem0001,X139)|~r1(X139,skolem0001)|p1(skolem0012)|r1(skolem0012,skolem0002(X139,skolem0001,skolem0012))|r1(X139,skolem0003(X139)),inference(resolution,[status(thm)],[c7, c28])).
% 0.67/1.00 cnf(c161,plain,~r1(skolem0001,skolem0001)|p1(skolem0012)|r1(skolem0012,skolem0002(skolem0001,skolem0001,skolem0012))|r1(skolem0001,skolem0003(skolem0001)),inference(factor,[status(thm)],[c36])).
% 0.67/1.00 cnf(c78,plain,~r1(skolem0001,X189)|~r1(X189,X188)|~r1(X188,skolem0012)|p1(skolem0012)|~p1(skolem0007(skolem0012))|r1(X189,skolem0004(X189))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c13, c42])).
% 0.67/1.00 cnf(c159,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0012)|p1(skolem0013)|~p1(skolem0012)|r1(skolem0004(skolem0013),skolem0005(skolem0013)),inference(resolution,[status(thm)],[c107, c29])).
% 0.67/1.00 cnf(c31,negated_conjecture,r1(skolem0012,skolem0014),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c157,plain,~r1(skolem0001,skolem0014)|~r1(skolem0014,skolem0012)|p1(skolem0014)|~p1(skolem0012)|r1(skolem0004(skolem0014),skolem0005(skolem0014)),inference(resolution,[status(thm)],[c107, c31])).
% 0.67/1.00 cnf(c35,plain,~r1(skolem0001,X134)|~r1(X134,skolem0012)|p1(skolem0014)|r1(skolem0014,skolem0002(X134,skolem0012,skolem0014))|r1(X134,skolem0003(X134)),inference(resolution,[status(thm)],[c7, c31])).
% 0.67/1.00 cnf(c150,plain,~r1(skolem0001,skolem0001)|p1(skolem0014)|r1(skolem0014,skolem0002(skolem0001,skolem0012,skolem0014))|r1(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c35, c28])).
% 0.67/1.00 cnf(c22,negated_conjecture,~r1(skolem0001,X116)|~r1(X116,X115)|~r1(X115,X118)|r1(X118,skolem0008(X116,X115,X118))|~r1(skolem0009(X116),X117)|~p1(X117),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c139,plain,~r1(skolem0001,X185)|~r1(X185,skolem0009(X185))|~r1(skolem0009(X185),X186)|r1(X186,skolem0008(X185,skolem0009(X185),X186))|~p1(X186),inference(factor,[status(thm)],[c22])).
% 0.67/1.00 cnf(c189,plain,~r1(skolem0001,X184)|~r1(X184,skolem0001)|p1(skolem0012)|~p1(skolem0013)|r1(skolem0004(X184),skolem0005(X184)),inference(resolution,[status(thm)],[c114, c28])).
% 0.67/1.00 cnf(c190,plain,~r1(skolem0001,skolem0001)|p1(skolem0012)|~p1(skolem0013)|r1(skolem0004(skolem0001),skolem0005(skolem0001)),inference(factor,[status(thm)],[c189])).
% 0.67/1.00 cnf(c111,plain,~r1(skolem0001,X178)|~r1(X178,X177)|~r1(X177,skolem0001)|p1(skolem0001)|~p1(skolem0012)|r1(skolem0004(X178),skolem0005(X178)),inference(resolution,[status(thm)],[c15, c28])).
% 0.67/1.00 cnf(c184,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|~p1(skolem0012)|r1(skolem0004(skolem0001),skolem0005(skolem0001)),inference(factor,[status(thm)],[c111])).
% 0.67/1.00 cnf(c34,plain,~r1(skolem0001,X94)|~r1(X94,X94)|p1(X94)|r1(X94,skolem0002(X94,X94,X94))|r1(X94,skolem0003(X94)),inference(factor,[status(thm)],[c7])).
% 0.67/1.00 cnf(c96,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|r1(skolem0001,skolem0002(skolem0001,skolem0001,skolem0001))|r1(skolem0001,skolem0003(skolem0001)),inference(factor,[status(thm)],[c34])).
% 0.67/1.00 cnf(c77,plain,~r1(skolem0001,X176)|~r1(X176,X175)|~r1(X175,skolem0012)|p1(skolem0012)|~p1(skolem0011(skolem0012))|r1(X176,skolem0004(X176)),inference(resolution,[status(thm)],[c13, c38])).
% 0.67/1.00 cnf(c9,negated_conjecture,~r1(skolem0001,X52)|~r1(X52,X53)|~r1(X53,X55)|p1(X55)|r1(X55,skolem0002(X52,X53,X55))|~r1(skolem0003(X52),X54)|p1(X54),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c54,plain,~r1(skolem0001,X172)|~r1(X172,skolem0003(X172))|~r1(skolem0003(X172),X173)|p1(X173)|r1(X173,skolem0002(X172,skolem0003(X172),X173)),inference(factor,[status(thm)],[c9])).
% 0.67/1.00 cnf(c24,negated_conjecture,~r1(skolem0001,X122)|~r1(X122,X121)|~r1(X121,X124)|p1(skolem0008(X122,X121,X124))|~r1(skolem0009(X122),X123)|~p1(X123),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c142,plain,~r1(skolem0001,X168)|~r1(X168,skolem0009(X168))|~r1(skolem0009(X168),X169)|p1(skolem0008(X168,skolem0009(X168),X169))|~p1(X169),inference(factor,[status(thm)],[c24])).
% 0.67/1.00 cnf(c25,negated_conjecture,~r1(skolem0001,X50)|~r1(X50,X49)|~r1(X49,X51)|p1(X51)|r1(X50,skolem0010(X50)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c48,plain,~r1(skolem0001,X167)|~r1(X167,skolem0012)|p1(skolem0007(skolem0012))|r1(X167,skolem0010(X167))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c25, c42])).
% 0.67/1.00 cnf(c182,plain,~r1(skolem0001,skolem0001)|p1(skolem0007(skolem0012))|r1(skolem0001,skolem0010(skolem0001))|r1(skolem0012,skolem0006(skolem0012)),inference(resolution,[status(thm)],[c48, c28])).
% 0.67/1.00 cnf(c122,plain,~r1(skolem0001,X166)|~r1(X166,X165)|~r1(X165,skolem0012)|p1(skolem0012)|~p1(skolem0011(skolem0012))|p1(skolem0005(X166)),inference(resolution,[status(thm)],[c16, c38])).
% 0.67/1.00 cnf(c106,plain,~r1(skolem0001,X163)|~r1(X163,X164)|~r1(X164,skolem0001)|p1(skolem0001)|~p1(X163)|r1(skolem0004(X163),skolem0005(X163)),inference(factor,[status(thm)],[c15])).
% 0.67/1.00 cnf(c82,plain,~r1(skolem0001,X159)|~r1(X159,X158)|~r1(X158,skolem0012)|p1(skolem0012)|~p1(skolem0013)|r1(X159,skolem0004(X159)),inference(resolution,[status(thm)],[c13, c29])).
% 0.67/1.00 cnf(c176,plain,~r1(skolem0001,skolem0012)|~r1(skolem0012,skolem0012)|p1(skolem0012)|~p1(skolem0013)|r1(skolem0012,skolem0004(skolem0012)),inference(factor,[status(thm)],[c82])).
% 0.67/1.00 cnf(c92,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0012)|p1(skolem0013)|~p1(skolem0012)|r1(skolem0013,skolem0004(skolem0013)),inference(resolution,[status(thm)],[c75, c29])).
% 0.67/1.00 cnf(c90,plain,~r1(skolem0001,skolem0014)|~r1(skolem0014,skolem0012)|p1(skolem0014)|~p1(skolem0012)|r1(skolem0014,skolem0004(skolem0014)),inference(resolution,[status(thm)],[c75, c31])).
% 0.67/1.00 cnf(c177,plain,~r1(skolem0001,X160)|~r1(X160,skolem0001)|p1(skolem0012)|~p1(skolem0013)|r1(X160,skolem0004(X160)),inference(resolution,[status(thm)],[c82, c28])).
% 0.67/1.00 cnf(c178,plain,~r1(skolem0001,skolem0001)|p1(skolem0012)|~p1(skolem0013)|r1(skolem0001,skolem0004(skolem0001)),inference(factor,[status(thm)],[c177])).
% 0.67/1.00 cnf(c79,plain,~r1(skolem0001,X154)|~r1(X154,X153)|~r1(X153,skolem0001)|p1(skolem0001)|~p1(skolem0012)|r1(X154,skolem0004(X154)),inference(resolution,[status(thm)],[c13, c28])).
% 0.67/1.00 cnf(c172,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|~p1(skolem0012)|r1(skolem0001,skolem0004(skolem0001)),inference(factor,[status(thm)],[c79])).
% 0.67/1.00 cnf(c51,plain,~r1(skolem0001,X152)|~r1(X152,skolem0012)|p1(skolem0007(skolem0012))|r1(X152,skolem0010(X152))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c25, c40])).
% 0.67/1.00 cnf(c171,plain,~r1(skolem0001,skolem0001)|p1(skolem0007(skolem0012))|r1(skolem0001,skolem0010(skolem0001))|p1(skolem0006(skolem0012)),inference(resolution,[status(thm)],[c51, c28])).
% 0.67/1.00 cnf(c127,plain,~r1(skolem0001,X149)|~r1(X149,X148)|~r1(X148,skolem0012)|p1(skolem0012)|~p1(skolem0013)|p1(skolem0005(X149)),inference(resolution,[status(thm)],[c16, c29])).
% 0.67/1.00 cnf(c167,plain,~r1(skolem0001,skolem0012)|~r1(skolem0012,skolem0012)|p1(skolem0012)|~p1(skolem0013)|p1(skolem0005(skolem0012)),inference(factor,[status(thm)],[c127])).
% 0.67/1.00 cnf(c168,plain,~r1(skolem0001,X150)|~r1(X150,skolem0001)|p1(skolem0012)|~p1(skolem0013)|p1(skolem0005(X150)),inference(resolution,[status(thm)],[c127, c28])).
% 0.67/1.00 cnf(c169,plain,~r1(skolem0001,skolem0001)|p1(skolem0012)|~p1(skolem0013)|p1(skolem0005(skolem0001)),inference(factor,[status(thm)],[c168])).
% 0.67/1.00 cnf(c124,plain,~r1(skolem0001,X144)|~r1(X144,X143)|~r1(X143,skolem0001)|p1(skolem0001)|~p1(skolem0012)|p1(skolem0005(X144)),inference(resolution,[status(thm)],[c16, c28])).
% 0.67/1.00 cnf(c163,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|~p1(skolem0012)|p1(skolem0005(skolem0001)),inference(factor,[status(thm)],[c124])).
% 0.67/1.00 cnf(c152,plain,~r1(skolem0001,X140)|~r1(X140,skolem0001)|p1(X140)|~p1(skolem0001)|r1(skolem0004(X140),skolem0005(X140)),inference(factor,[status(thm)],[c107])).
% 0.67/1.00 cnf(c104,plain,~r1(skolem0001,X135)|~r1(X135,skolem0012)|r1(skolem0013,skolem0008(X135,skolem0012,skolem0013))|r1(X135,skolem0009(X135)),inference(resolution,[status(thm)],[c21, c29])).
% 0.67/1.00 cnf(c151,plain,~r1(skolem0001,skolem0001)|r1(skolem0013,skolem0008(skolem0001,skolem0012,skolem0013))|r1(skolem0001,skolem0009(skolem0001)),inference(resolution,[status(thm)],[c104, c28])).
% 0.67/1.00 cnf(c102,plain,~r1(skolem0001,X133)|~r1(X133,skolem0012)|r1(skolem0014,skolem0008(X133,skolem0012,skolem0014))|r1(X133,skolem0009(X133)),inference(resolution,[status(thm)],[c21, c31])).
% 0.67/1.00 cnf(c149,plain,~r1(skolem0001,skolem0001)|r1(skolem0014,skolem0008(skolem0001,skolem0012,skolem0014))|r1(skolem0001,skolem0009(skolem0001)),inference(resolution,[status(thm)],[c102, c28])).
% 0.67/1.00 cnf(c101,plain,~r1(skolem0001,X132)|~r1(X132,skolem0001)|r1(skolem0012,skolem0008(X132,skolem0001,skolem0012))|r1(X132,skolem0009(X132)),inference(resolution,[status(thm)],[c21, c28])).
% 0.67/1.00 cnf(c148,plain,~r1(skolem0001,skolem0001)|r1(skolem0012,skolem0008(skolem0001,skolem0001,skolem0012))|r1(skolem0001,skolem0009(skolem0001)),inference(factor,[status(thm)],[c101])).
% 0.67/1.00 cnf(c14,negated_conjecture,~r1(skolem0001,X89)|~r1(X89,X87)|~r1(X87,X90)|p1(X90)|~r1(X90,X88)|~p1(X88)|~p1(skolem0004(X89)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c94,plain,~r1(skolem0001,X130)|~r1(X130,X129)|~r1(X129,X128)|p1(X128)|~r1(X128,skolem0004(X130))|~p1(skolem0004(X130)),inference(factor,[status(thm)],[c14])).
% 0.67/1.00 cnf(c146,plain,~r1(skolem0001,X131)|~r1(X131,skolem0004(X131))|~r1(skolem0004(X131),X131)|p1(X131)|~p1(skolem0004(X131)),inference(factor,[status(thm)],[c94])).
% 0.67/1.00 cnf(c33,plain,~r1(skolem0001,X127)|~r1(X127,skolem0001)|p1(X127)|r1(X127,skolem0002(X127,skolem0001,X127))|r1(X127,skolem0003(X127)),inference(factor,[status(thm)],[c7])).
% 0.67/1.00 cnf(c74,plain,~r1(skolem0001,X125)|~r1(X125,X126)|~r1(X126,skolem0001)|p1(skolem0001)|~p1(X125)|r1(X125,skolem0004(X125)),inference(factor,[status(thm)],[c13])).
% 0.67/1.00 cnf(c136,plain,~r1(skolem0001,skolem0013)|~r1(skolem0013,skolem0012)|p1(skolem0013)|~p1(skolem0012)|p1(skolem0005(skolem0013)),inference(resolution,[status(thm)],[c120, c29])).
% 0.67/1.00 cnf(c134,plain,~r1(skolem0001,skolem0014)|~r1(skolem0014,skolem0012)|p1(skolem0014)|~p1(skolem0012)|p1(skolem0005(skolem0014)),inference(resolution,[status(thm)],[c120, c31])).
% 0.67/1.00 cnf(c119,plain,~r1(skolem0001,X119)|~r1(X119,X120)|~r1(X120,skolem0001)|p1(skolem0001)|~p1(X119)|p1(skolem0005(X119)),inference(factor,[status(thm)],[c16])).
% 0.67/1.00 cnf(c63,plain,~r1(skolem0001,X104)|~r1(X104,skolem0012)|p1(skolem0008(X104,skolem0012,skolem0011(skolem0012)))|r1(X104,skolem0009(X104)),inference(resolution,[status(thm)],[c23, c38])).
% 0.67/1.00 cnf(c118,plain,~r1(skolem0001,skolem0001)|p1(skolem0008(skolem0001,skolem0012,skolem0011(skolem0012)))|r1(skolem0001,skolem0009(skolem0001)),inference(resolution,[status(thm)],[c63, c28])).
% 0.67/1.00 cnf(c129,plain,~r1(skolem0001,X112)|~r1(X112,skolem0001)|p1(X112)|~p1(skolem0001)|p1(skolem0005(X112)),inference(factor,[status(thm)],[c120])).
% 0.67/1.00 cnf(c98,plain,~r1(skolem0001,X102)|~r1(X102,X102)|r1(X102,skolem0008(X102,X102,X102))|r1(X102,skolem0009(X102)),inference(factor,[status(thm)],[c21])).
% 0.67/1.00 cnf(c116,plain,~r1(skolem0001,skolem0001)|r1(skolem0001,skolem0008(skolem0001,skolem0001,skolem0001))|r1(skolem0001,skolem0009(skolem0001)),inference(factor,[status(thm)],[c98])).
% 0.67/1.00 cnf(c97,plain,~r1(skolem0001,X103)|~r1(X103,skolem0001)|r1(X103,skolem0008(X103,skolem0001,X103))|r1(X103,skolem0009(X103)),inference(factor,[status(thm)],[c21])).
% 0.67/1.00 cnf(c85,plain,~r1(skolem0001,X91)|~r1(X91,skolem0001)|p1(X91)|~p1(skolem0001)|r1(X91,skolem0004(X91)),inference(factor,[status(thm)],[c75])).
% 0.67/1.00 cnf(c68,plain,~r1(skolem0001,X83)|~r1(X83,skolem0012)|p1(skolem0008(X83,skolem0012,skolem0013))|r1(X83,skolem0009(X83)),inference(resolution,[status(thm)],[c23, c29])).
% 0.67/1.00 cnf(c84,plain,~r1(skolem0001,skolem0001)|p1(skolem0008(skolem0001,skolem0012,skolem0013))|r1(skolem0001,skolem0009(skolem0001)),inference(resolution,[status(thm)],[c68, c28])).
% 0.67/1.00 cnf(c66,plain,~r1(skolem0001,X78)|~r1(X78,skolem0012)|p1(skolem0008(X78,skolem0012,skolem0014))|r1(X78,skolem0009(X78)),inference(resolution,[status(thm)],[c23, c31])).
% 0.67/1.00 cnf(c73,plain,~r1(skolem0001,skolem0001)|p1(skolem0008(skolem0001,skolem0012,skolem0014))|r1(skolem0001,skolem0009(skolem0001)),inference(resolution,[status(thm)],[c66, c28])).
% 0.67/1.00 cnf(c65,plain,~r1(skolem0001,X77)|~r1(X77,skolem0001)|p1(skolem0008(X77,skolem0001,skolem0012))|r1(X77,skolem0009(X77)),inference(resolution,[status(thm)],[c23, c28])).
% 0.67/1.00 cnf(c72,plain,~r1(skolem0001,skolem0001)|p1(skolem0008(skolem0001,skolem0001,skolem0012))|r1(skolem0001,skolem0009(skolem0001)),inference(factor,[status(thm)],[c65])).
% 0.67/1.00 cnf(c62,plain,~r1(skolem0001,X71)|~r1(X71,X71)|p1(skolem0008(X71,X71,X71))|r1(X71,skolem0009(X71)),inference(factor,[status(thm)],[c23])).
% 0.67/1.00 cnf(c70,plain,~r1(skolem0001,skolem0001)|p1(skolem0008(skolem0001,skolem0001,skolem0001))|r1(skolem0001,skolem0009(skolem0001)),inference(factor,[status(thm)],[c62])).
% 0.67/1.00 cnf(c12,negated_conjecture,~r1(skolem0001,X73)|~r1(X73,X74)|~r1(X74,X76)|p1(X76)|~p1(skolem0002(X73,X74,X76))|~r1(skolem0003(X73),X75)|p1(X75),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c61,plain,~r1(skolem0001,X72)|~r1(X72,skolem0001)|p1(skolem0008(X72,skolem0001,X72))|r1(X72,skolem0009(X72)),inference(factor,[status(thm)],[c23])).
% 0.67/1.00 cnf(c47,plain,~r1(skolem0001,X67)|~r1(X67,skolem0012)|p1(skolem0011(skolem0012))|r1(X67,skolem0010(X67)),inference(resolution,[status(thm)],[c25, c38])).
% 0.67/1.00 cnf(c60,plain,~r1(skolem0001,skolem0001)|p1(skolem0011(skolem0012))|r1(skolem0001,skolem0010(skolem0001)),inference(resolution,[status(thm)],[c47, c28])).
% 0.67/1.00 cnf(c11,negated_conjecture,~r1(skolem0001,X64)|~r1(X64,X65)|~r1(X65,X66)|p1(X66)|~p1(skolem0002(X64,X65,X66))|~p1(skolem0003(X64)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c52,plain,~r1(skolem0001,X63)|~r1(X63,skolem0012)|p1(skolem0013)|r1(X63,skolem0010(X63)),inference(resolution,[status(thm)],[c25, c29])).
% 0.67/1.00 cnf(c59,plain,~r1(skolem0001,skolem0001)|p1(skolem0013)|r1(skolem0001,skolem0010(skolem0001)),inference(resolution,[status(thm)],[c52, c28])).
% 0.67/1.00 cnf(c50,plain,~r1(skolem0001,X62)|~r1(X62,skolem0012)|p1(skolem0014)|r1(X62,skolem0010(X62)),inference(resolution,[status(thm)],[c25, c31])).
% 0.67/1.00 cnf(c58,plain,~r1(skolem0001,skolem0001)|p1(skolem0014)|r1(skolem0001,skolem0010(skolem0001)),inference(resolution,[status(thm)],[c50, c28])).
% 0.67/1.00 cnf(c49,plain,~r1(skolem0001,X58)|~r1(X58,skolem0001)|p1(skolem0012)|r1(X58,skolem0010(X58)),inference(resolution,[status(thm)],[c25, c28])).
% 0.67/1.00 cnf(c57,plain,~r1(skolem0001,skolem0001)|p1(skolem0012)|r1(skolem0001,skolem0010(skolem0001)),inference(factor,[status(thm)],[c49])).
% 0.67/1.00 cnf(c10,negated_conjecture,~r1(skolem0001,X59)|~r1(X59,X60)|~r1(X60,X61)|p1(X61)|~p1(skolem0002(X59,X60,X61))|r1(X59,skolem0003(X59)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c45,plain,~r1(skolem0001,X57)|~r1(X57,skolem0001)|p1(X57)|r1(X57,skolem0010(X57)),inference(factor,[status(thm)],[c25])).
% 0.67/1.00 cnf(c46,plain,~r1(skolem0001,X56)|~r1(X56,X56)|p1(X56)|r1(X56,skolem0010(X56)),inference(factor,[status(thm)],[c25])).
% 0.67/1.00 cnf(c55,plain,~r1(skolem0001,skolem0001)|p1(skolem0001)|r1(skolem0001,skolem0010(skolem0001)),inference(factor,[status(thm)],[c46])).
% 0.67/1.00 cnf(c26,negated_conjecture,~r1(skolem0001,X47)|~r1(X47,X46)|~r1(X46,X48)|p1(X48)|~p1(skolem0010(X47)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c8,negated_conjecture,~r1(skolem0001,X42)|~r1(X42,X43)|~r1(X43,X44)|p1(X44)|r1(X44,skolem0002(X42,X43,X44))|~p1(skolem0003(X42)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c18,negated_conjecture,~r1(skolem0001,X40)|r1(X40,skolem0006(X40))|~p1(skolem0007(X40)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c20,negated_conjecture,~r1(skolem0001,X39)|p1(skolem0006(X39))|~p1(skolem0007(X39)),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c30,negated_conjecture,~r1(skolem0013,X34)|p1(X34),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 cnf(c32,negated_conjecture,~p1(skolem0014),inference(split_conjunct,[status(thm)],[c6])).
% 0.67/1.00 % SZS output end Saturation
% 0.67/1.00
% 0.67/1.00 % Initial clauses : 26
% 0.67/1.00 % Processed clauses : 164
% 0.67/1.00 % Factors computed : 74
% 0.67/1.00 % Resolvents computed: 104
% 0.67/1.00 % Tautologies deleted: 16
% 0.67/1.00 % Forward subsumed : 24
% 0.67/1.00 % Backward subsumed : 3
% 0.67/1.00 % -------- CPU Time ---------
% 0.67/1.00 % User time : 0.614 s
% 0.67/1.00 % System time : 0.022 s
% 0.67/1.00 % Total time : 0.636 s
%------------------------------------------------------------------------------