%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL647+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:50 PM UTC 2026
% Result : CounterSatisfiable 0.66s 0.97s
% Output : Saturation 0.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL647+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.37 % Computer : n007.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sat Sep 5 13:21:54 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.15/0.44 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.15/0.44 (re.compile("\."), Token.FullStop),
% 0.15/0.44 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.15/0.44 (re.compile("\("), Token.OpenPar),
% 0.15/0.44 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.15/0.44 (re.compile("\)"), Token.ClosePar),
% 0.15/0.44 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.15/0.44 (re.compile("\["), Token.OpenSquare),
% 0.15/0.44 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.15/0.44 (re.compile("\]"), Token.CloseSquare),
% 0.15/0.44 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.44 (re.compile("~\|"), Token.Nor),
% 0.15/0.44 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.44 (re.compile("\|"), Token.Or),
% 0.15/0.44 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.15/0.44 (re.compile("\?"), Token.Existential),
% 0.15/0.44 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.15/0.44 (re.compile("\s+"), Token.WhiteSpace),
% 0.15/0.44 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.15/0.44 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.50 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.22/0.51 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.51 """
% 0.31/0.60 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.60 """
% 0.66/0.97 % Version: 1.5
% 0.66/0.97 % SZS status CounterSatisfiable
% 0.66/0.97 % SZS output start Saturation
% 0.66/0.97 fof(main,conjecture,(~(?[X]:(~((((((((((((((((((((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p6(X))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p5(X)))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p4(X)))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p2(X)))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p6(X)))&(~p6(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p6(X)))&(~p4(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p4(X)))&(~p6(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p4(X)))&(~p4(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p2(X)))&(~p6(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p2(X)))&(~p4(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p3(X)))&(~p5(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p1(X)))&(~p5(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p3(X)))&(~p3(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p1(X)))&(~p3(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p3(X)))&(~p1(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p1(X)))&(~p1(Y))))))))|(![Y]:((~r1(X,Y))|p5(Y))))|(![Y]:((~r1(X,Y))|p3(Y))))|(![Y]:((~r1(X,Y))|p2(Y))))|(![Y]:((~r1(X,Y))|p1(Y))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 0.66/0.97 fof(c0,negated_conjecture,(~(~(?[X]:(~((((((((((((((((((((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p6(X))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p5(X)))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p4(X)))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p2(X)))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p6(X)))&(~p6(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p6(X)))&(~p4(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p4(X)))&(~p6(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p4(X)))&(~p4(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p2(X)))&(~p6(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p2(X)))&(~p4(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p3(X)))&(~p5(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p1(X)))&(~p5(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p3(X)))&(~p3(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p1(X)))&(~p3(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p3(X)))&(~p1(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p1(X)))&(~p1(Y))))))))|(![Y]:((~r1(X,Y))|p5(Y))))|(![Y]:((~r1(X,Y))|p3(Y))))|(![Y]:((~r1(X,Y))|p2(Y))))|(![Y]:((~r1(X,Y))|p1(Y)))))))),inference(assume_negation,[status(cth)],[main])).
% 0.66/0.97 fof(c1,negated_conjecture,(~(~(?[X]:(~((((((((((((((((((((~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p6(X))))))|(~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p5(X)))))))|(~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p4(X)))))))|(~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p2(X)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p6(X)))&~p6(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p6(X)))&~p4(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p4(X)))&~p6(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p4(X)))&~p4(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p2(X)))&~p6(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p2(X)))&~p4(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p3(X)))&~p5(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p1(X)))&~p5(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p3(X)))&~p3(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p1(X)))&~p3(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p3(X)))&~p1(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p1(X)))&~p1(Y)))))))|(![Y]:(~r1(X,Y)|p5(Y))))|(![Y]:(~r1(X,Y)|p3(Y))))|(![Y]:(~r1(X,Y)|p2(Y))))|(![Y]:(~r1(X,Y)|p1(Y)))))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.66/0.97 fof(c2,negated_conjecture,(?[X]:((((((((((((((((((((![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p6(X)))))&(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p5(X))))))&(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p4(X))))))&(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p2(X))))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p6(X)))|p6(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p6(X)))|p4(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p4(X)))|p6(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p4(X)))|p4(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p2(X)))|p6(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p2(X)))|p4(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p3(X)))|p5(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p1(X)))|p5(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p3(X)))|p3(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p1(X)))|p3(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p3(X)))|p1(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p1(X)))|p1(Y)))))&(?[Y]:(r1(X,Y)&~p5(Y))))&(?[Y]:(r1(X,Y)&~p3(Y))))&(?[Y]:(r1(X,Y)&~p2(Y))))&(?[Y]:(r1(X,Y)&~p1(Y))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.66/0.97 fof(c3,negated_conjecture,(?[X2]:((((((((((((((((((((![X3]:(~r1(X2,X3)|(![X4]:(~r1(X3,X4)|p6(X4)))))&(![X5]:(~r1(X2,X5)|(![X6]:(~r1(X5,X6)|p5(X6))))))&(![X7]:(~r1(X2,X7)|(![X8]:(~r1(X7,X8)|p4(X8))))))&(![X9]:(~r1(X2,X9)|(![X10]:(~r1(X9,X10)|p2(X10))))))&(![X11]:(~r1(X2,X11)|((?[X12]:(r1(X11,X12)&~p6(X12)))|p6(X11)))))&(![X13]:(~r1(X2,X13)|((?[X14]:(r1(X13,X14)&~p6(X14)))|p4(X13)))))&(![X15]:(~r1(X2,X15)|((?[X16]:(r1(X15,X16)&~p4(X16)))|p6(X15)))))&(![X17]:(~r1(X2,X17)|((?[X18]:(r1(X17,X18)&~p4(X18)))|p4(X17)))))&(![X19]:(~r1(X2,X19)|((?[X20]:(r1(X19,X20)&~p2(X20)))|p6(X19)))))&(![X21]:(~r1(X2,X21)|((?[X22]:(r1(X21,X22)&~p2(X22)))|p4(X21)))))&(![X23]:(~r1(X2,X23)|((?[X24]:(r1(X23,X24)&~p3(X24)))|p5(X23)))))&(![X25]:(~r1(X2,X25)|((?[X26]:(r1(X25,X26)&~p1(X26)))|p5(X25)))))&(![X27]:(~r1(X2,X27)|((?[X28]:(r1(X27,X28)&~p3(X28)))|p3(X27)))))&(![X29]:(~r1(X2,X29)|((?[X30]:(r1(X29,X30)&~p1(X30)))|p3(X29)))))&(![X31]:(~r1(X2,X31)|((?[X32]:(r1(X31,X32)&~p3(X32)))|p1(X31)))))&(![X33]:(~r1(X2,X33)|((?[X34]:(r1(X33,X34)&~p1(X34)))|p1(X33)))))&(?[X35]:(r1(X2,X35)&~p5(X35))))&(?[X36]:(r1(X2,X36)&~p3(X36))))&(?[X37]:(r1(X2,X37)&~p2(X37))))&(?[X38]:(r1(X2,X38)&~p1(X38))))),inference(variable_rename,[status(thm)],[c2])).
% 0.66/0.97 fof(c5,negated_conjecture,(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X13]:(![X15]:(![X17]:(![X19]:(![X21]:(![X23]:(![X25]:(![X27]:(![X29]:(![X31]:(![X33]:((((((((((((((((((((~r1(skolem0001,X3)|(~r1(X3,X4)|p6(X4)))&(~r1(skolem0001,X5)|(~r1(X5,X6)|p5(X6))))&(~r1(skolem0001,X7)|(~r1(X7,X8)|p4(X8))))&(~r1(skolem0001,X9)|(~r1(X9,X10)|p2(X10))))&(~r1(skolem0001,X11)|((r1(X11,skolem0002(X11))&~p6(skolem0002(X11)))|p6(X11))))&(~r1(skolem0001,X13)|((r1(X13,skolem0003(X13))&~p6(skolem0003(X13)))|p4(X13))))&(~r1(skolem0001,X15)|((r1(X15,skolem0004(X15))&~p4(skolem0004(X15)))|p6(X15))))&(~r1(skolem0001,X17)|((r1(X17,skolem0005(X17))&~p4(skolem0005(X17)))|p4(X17))))&(~r1(skolem0001,X19)|((r1(X19,skolem0006(X19))&~p2(skolem0006(X19)))|p6(X19))))&(~r1(skolem0001,X21)|((r1(X21,skolem0007(X21))&~p2(skolem0007(X21)))|p4(X21))))&(~r1(skolem0001,X23)|((r1(X23,skolem0008(X23))&~p3(skolem0008(X23)))|p5(X23))))&(~r1(skolem0001,X25)|((r1(X25,skolem0009(X25))&~p1(skolem0009(X25)))|p5(X25))))&(~r1(skolem0001,X27)|((r1(X27,skolem0010(X27))&~p3(skolem0010(X27)))|p3(X27))))&(~r1(skolem0001,X29)|((r1(X29,skolem0011(X29))&~p1(skolem0011(X29)))|p3(X29))))&(~r1(skolem0001,X31)|((r1(X31,skolem0012(X31))&~p3(skolem0012(X31)))|p1(X31))))&(~r1(skolem0001,X33)|((r1(X33,skolem0013(X33))&~p1(skolem0013(X33)))|p1(X33))))&(r1(skolem0001,skolem0014)&~p5(skolem0014)))&(r1(skolem0001,skolem0015)&~p3(skolem0015)))&(r1(skolem0001,skolem0016)&~p2(skolem0016)))&(r1(skolem0001,skolem0017)&~p1(skolem0017))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((((((((((((((((((((![X3]:(~r1(skolem0001,X3)|(![X4]:(~r1(X3,X4)|p6(X4)))))&(![X5]:(~r1(skolem0001,X5)|(![X6]:(~r1(X5,X6)|p5(X6))))))&(![X7]:(~r1(skolem0001,X7)|(![X8]:(~r1(X7,X8)|p4(X8))))))&(![X9]:(~r1(skolem0001,X9)|(![X10]:(~r1(X9,X10)|p2(X10))))))&(![X11]:(~r1(skolem0001,X11)|((r1(X11,skolem0002(X11))&~p6(skolem0002(X11)))|p6(X11)))))&(![X13]:(~r1(skolem0001,X13)|((r1(X13,skolem0003(X13))&~p6(skolem0003(X13)))|p4(X13)))))&(![X15]:(~r1(skolem0001,X15)|((r1(X15,skolem0004(X15))&~p4(skolem0004(X15)))|p6(X15)))))&(![X17]:(~r1(skolem0001,X17)|((r1(X17,skolem0005(X17))&~p4(skolem0005(X17)))|p4(X17)))))&(![X19]:(~r1(skolem0001,X19)|((r1(X19,skolem0006(X19))&~p2(skolem0006(X19)))|p6(X19)))))&(![X21]:(~r1(skolem0001,X21)|((r1(X21,skolem0007(X21))&~p2(skolem0007(X21)))|p4(X21)))))&(![X23]:(~r1(skolem0001,X23)|((r1(X23,skolem0008(X23))&~p3(skolem0008(X23)))|p5(X23)))))&(![X25]:(~r1(skolem0001,X25)|((r1(X25,skolem0009(X25))&~p1(skolem0009(X25)))|p5(X25)))))&(![X27]:(~r1(skolem0001,X27)|((r1(X27,skolem0010(X27))&~p3(skolem0010(X27)))|p3(X27)))))&(![X29]:(~r1(skolem0001,X29)|((r1(X29,skolem0011(X29))&~p1(skolem0011(X29)))|p3(X29)))))&(![X31]:(~r1(skolem0001,X31)|((r1(X31,skolem0012(X31))&~p3(skolem0012(X31)))|p1(X31)))))&(![X33]:(~r1(skolem0001,X33)|((r1(X33,skolem0013(X33))&~p1(skolem0013(X33)))|p1(X33)))))&(r1(skolem0001,skolem0014)&~p5(skolem0014)))&(r1(skolem0001,skolem0015)&~p3(skolem0015)))&(r1(skolem0001,skolem0016)&~p2(skolem0016)))&(r1(skolem0001,skolem0017)&~p1(skolem0017))),inference(skolemize,[status(esa)],[c3])).])).
% 0.66/0.97 fof(c6,negated_conjecture,(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X13]:(![X15]:(![X17]:(![X19]:(![X21]:(![X23]:(![X25]:(![X27]:(![X29]:(![X31]:(![X33]:((((((((((((((((((((~r1(skolem0001,X3)|(~r1(X3,X4)|p6(X4)))&(~r1(skolem0001,X5)|(~r1(X5,X6)|p5(X6))))&(~r1(skolem0001,X7)|(~r1(X7,X8)|p4(X8))))&(~r1(skolem0001,X9)|(~r1(X9,X10)|p2(X10))))&((~r1(skolem0001,X11)|(r1(X11,skolem0002(X11))|p6(X11)))&(~r1(skolem0001,X11)|(~p6(skolem0002(X11))|p6(X11)))))&((~r1(skolem0001,X13)|(r1(X13,skolem0003(X13))|p4(X13)))&(~r1(skolem0001,X13)|(~p6(skolem0003(X13))|p4(X13)))))&((~r1(skolem0001,X15)|(r1(X15,skolem0004(X15))|p6(X15)))&(~r1(skolem0001,X15)|(~p4(skolem0004(X15))|p6(X15)))))&((~r1(skolem0001,X17)|(r1(X17,skolem0005(X17))|p4(X17)))&(~r1(skolem0001,X17)|(~p4(skolem0005(X17))|p4(X17)))))&((~r1(skolem0001,X19)|(r1(X19,skolem0006(X19))|p6(X19)))&(~r1(skolem0001,X19)|(~p2(skolem0006(X19))|p6(X19)))))&((~r1(skolem0001,X21)|(r1(X21,skolem0007(X21))|p4(X21)))&(~r1(skolem0001,X21)|(~p2(skolem0007(X21))|p4(X21)))))&((~r1(skolem0001,X23)|(r1(X23,skolem0008(X23))|p5(X23)))&(~r1(skolem0001,X23)|(~p3(skolem0008(X23))|p5(X23)))))&((~r1(skolem0001,X25)|(r1(X25,skolem0009(X25))|p5(X25)))&(~r1(skolem0001,X25)|(~p1(skolem0009(X25))|p5(X25)))))&((~r1(skolem0001,X27)|(r1(X27,skolem0010(X27))|p3(X27)))&(~r1(skolem0001,X27)|(~p3(skolem0010(X27))|p3(X27)))))&((~r1(skolem0001,X29)|(r1(X29,skolem0011(X29))|p3(X29)))&(~r1(skolem0001,X29)|(~p1(skolem0011(X29))|p3(X29)))))&((~r1(skolem0001,X31)|(r1(X31,skolem0012(X31))|p1(X31)))&(~r1(skolem0001,X31)|(~p3(skolem0012(X31))|p1(X31)))))&((~r1(skolem0001,X33)|(r1(X33,skolem0013(X33))|p1(X33)))&(~r1(skolem0001,X33)|(~p1(skolem0013(X33))|p1(X33)))))&(r1(skolem0001,skolem0014)&~p5(skolem0014)))&(r1(skolem0001,skolem0015)&~p3(skolem0015)))&(r1(skolem0001,skolem0016)&~p2(skolem0016)))&(r1(skolem0001,skolem0017)&~p1(skolem0017))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 0.66/0.97 cnf(c35,negated_conjecture,r1(skolem0001,skolem0014),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c9,negated_conjecture,~r1(skolem0001,X43)|~r1(X43,X44)|p4(X44),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c33,negated_conjecture,~r1(skolem0001,X69)|r1(X69,skolem0013(X69))|p1(X69),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c298,plain,r1(skolem0014,skolem0013(skolem0014))|p1(skolem0014),inference(resolution,[status(thm)],[c33, c35])).
% 0.66/0.97 cnf(c354,plain,p1(skolem0014)|~r1(skolem0001,skolem0014)|p4(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c298, c9])).
% 0.66/0.97 cnf(c470,plain,p1(skolem0014)|p4(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c354, c35])).
% 0.66/0.97 cnf(c7,negated_conjecture,~r1(skolem0001,X40)|~r1(X40,X39)|p6(X39),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c353,plain,p1(skolem0014)|~r1(skolem0001,skolem0014)|p6(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c298, c7])).
% 0.66/0.97 cnf(c469,plain,p1(skolem0014)|p6(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c353, c35])).
% 0.66/0.97 cnf(c10,negated_conjecture,~r1(skolem0001,X45)|~r1(X45,X46)|p2(X46),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c352,plain,p1(skolem0014)|~r1(skolem0001,skolem0014)|p2(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c298, c10])).
% 0.66/0.97 cnf(c468,plain,p1(skolem0014)|p2(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c352, c35])).
% 0.66/0.97 cnf(c8,negated_conjecture,~r1(skolem0001,X41)|~r1(X41,X42)|p5(X42),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c351,plain,p1(skolem0014)|~r1(skolem0001,skolem0014)|p5(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c298, c8])).
% 0.66/0.97 cnf(c467,plain,p1(skolem0014)|p5(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c351, c35])).
% 0.66/0.97 cnf(c37,negated_conjecture,r1(skolem0001,skolem0015),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c297,plain,r1(skolem0015,skolem0013(skolem0015))|p1(skolem0015),inference(resolution,[status(thm)],[c33, c37])).
% 0.66/0.97 cnf(c350,plain,p1(skolem0015)|~r1(skolem0001,skolem0015)|p4(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c297, c9])).
% 0.66/0.97 cnf(c466,plain,p1(skolem0015)|p4(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c350, c37])).
% 0.66/0.97 cnf(c349,plain,p1(skolem0015)|~r1(skolem0001,skolem0015)|p6(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c297, c7])).
% 0.66/0.97 cnf(c465,plain,p1(skolem0015)|p6(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c349, c37])).
% 0.66/0.97 cnf(c348,plain,p1(skolem0015)|~r1(skolem0001,skolem0015)|p2(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c297, c10])).
% 0.66/0.97 cnf(c464,plain,p1(skolem0015)|p2(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c348, c37])).
% 0.66/0.97 cnf(c347,plain,p1(skolem0015)|~r1(skolem0001,skolem0015)|p5(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c297, c8])).
% 0.66/0.97 cnf(c463,plain,p1(skolem0015)|p5(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c347, c37])).
% 0.66/0.97 cnf(c39,negated_conjecture,r1(skolem0001,skolem0016),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c296,plain,r1(skolem0016,skolem0013(skolem0016))|p1(skolem0016),inference(resolution,[status(thm)],[c33, c39])).
% 0.66/0.97 cnf(c345,plain,p1(skolem0016)|~r1(skolem0001,skolem0016)|p4(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c296, c9])).
% 0.66/0.97 cnf(c462,plain,p1(skolem0016)|p4(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c345, c39])).
% 0.66/0.97 cnf(c344,plain,p1(skolem0016)|~r1(skolem0001,skolem0016)|p6(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c296, c7])).
% 0.66/0.97 cnf(c461,plain,p1(skolem0016)|p6(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c344, c39])).
% 0.66/0.97 cnf(c343,plain,p1(skolem0016)|~r1(skolem0001,skolem0016)|p2(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c296, c10])).
% 0.66/0.97 cnf(c460,plain,p1(skolem0016)|p2(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c343, c39])).
% 0.66/0.97 cnf(c342,plain,p1(skolem0016)|~r1(skolem0001,skolem0016)|p5(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c296, c8])).
% 0.66/0.97 cnf(c459,plain,p1(skolem0016)|p5(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c342, c39])).
% 0.66/0.97 cnf(c31,negated_conjecture,~r1(skolem0001,X67)|r1(X67,skolem0012(X67))|p1(X67),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c277,plain,r1(skolem0014,skolem0012(skolem0014))|p1(skolem0014),inference(resolution,[status(thm)],[c31, c35])).
% 0.66/0.97 cnf(c324,plain,p1(skolem0014)|~r1(skolem0001,skolem0014)|p4(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c277, c9])).
% 0.66/0.97 cnf(c458,plain,p1(skolem0014)|p4(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c324, c35])).
% 0.66/0.97 cnf(c323,plain,p1(skolem0014)|~r1(skolem0001,skolem0014)|p6(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c277, c7])).
% 0.66/0.97 cnf(c457,plain,p1(skolem0014)|p6(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c323, c35])).
% 0.66/0.97 cnf(c322,plain,p1(skolem0014)|~r1(skolem0001,skolem0014)|p2(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c277, c10])).
% 0.66/0.97 cnf(c456,plain,p1(skolem0014)|p2(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c322, c35])).
% 0.66/0.97 cnf(c321,plain,p1(skolem0014)|~r1(skolem0001,skolem0014)|p5(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c277, c8])).
% 0.66/0.97 cnf(c455,plain,p1(skolem0014)|p5(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c321, c35])).
% 0.66/0.97 cnf(c276,plain,r1(skolem0015,skolem0012(skolem0015))|p1(skolem0015),inference(resolution,[status(thm)],[c31, c37])).
% 0.66/0.97 cnf(c320,plain,p1(skolem0015)|~r1(skolem0001,skolem0015)|p4(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c276, c9])).
% 0.66/0.97 cnf(c454,plain,p1(skolem0015)|p4(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c320, c37])).
% 0.66/0.97 cnf(c319,plain,p1(skolem0015)|~r1(skolem0001,skolem0015)|p6(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c276, c7])).
% 0.66/0.97 cnf(c453,plain,p1(skolem0015)|p6(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c319, c37])).
% 0.66/0.97 cnf(c318,plain,p1(skolem0015)|~r1(skolem0001,skolem0015)|p2(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c276, c10])).
% 0.66/0.97 cnf(c452,plain,p1(skolem0015)|p2(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c318, c37])).
% 0.66/0.97 cnf(c317,plain,p1(skolem0015)|~r1(skolem0001,skolem0015)|p5(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c276, c8])).
% 0.66/0.97 cnf(c451,plain,p1(skolem0015)|p5(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c317, c37])).
% 0.66/0.97 cnf(c275,plain,r1(skolem0016,skolem0012(skolem0016))|p1(skolem0016),inference(resolution,[status(thm)],[c31, c39])).
% 0.66/0.97 cnf(c316,plain,p1(skolem0016)|~r1(skolem0001,skolem0016)|p4(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c275, c9])).
% 0.66/0.97 cnf(c450,plain,p1(skolem0016)|p4(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c316, c39])).
% 0.66/0.97 cnf(c315,plain,p1(skolem0016)|~r1(skolem0001,skolem0016)|p6(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c275, c7])).
% 0.66/0.97 cnf(c449,plain,p1(skolem0016)|p6(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c315, c39])).
% 0.66/0.97 cnf(c314,plain,p1(skolem0016)|~r1(skolem0001,skolem0016)|p2(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c275, c10])).
% 0.66/0.97 cnf(c448,plain,p1(skolem0016)|p2(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c314, c39])).
% 0.66/0.97 cnf(c313,plain,p1(skolem0016)|~r1(skolem0001,skolem0016)|p5(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c275, c8])).
% 0.66/0.97 cnf(c447,plain,p1(skolem0016)|p5(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c313, c39])).
% 0.66/0.97 cnf(c29,negated_conjecture,~r1(skolem0001,X65)|r1(X65,skolem0011(X65))|p3(X65),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c231,plain,r1(skolem0014,skolem0011(skolem0014))|p3(skolem0014),inference(resolution,[status(thm)],[c29, c35])).
% 0.66/0.97 cnf(c290,plain,p3(skolem0014)|~r1(skolem0001,skolem0014)|p4(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c231, c9])).
% 0.66/0.97 cnf(c446,plain,p3(skolem0014)|p4(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c290, c35])).
% 0.66/0.97 cnf(c289,plain,p3(skolem0014)|~r1(skolem0001,skolem0014)|p6(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c231, c7])).
% 0.66/0.97 cnf(c445,plain,p3(skolem0014)|p6(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c289, c35])).
% 0.66/0.97 cnf(c288,plain,p3(skolem0014)|~r1(skolem0001,skolem0014)|p2(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c231, c10])).
% 0.66/0.97 cnf(c444,plain,p3(skolem0014)|p2(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c288, c35])).
% 0.66/0.97 cnf(c287,plain,p3(skolem0014)|~r1(skolem0001,skolem0014)|p5(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c231, c8])).
% 0.66/0.97 cnf(c443,plain,p3(skolem0014)|p5(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c287, c35])).
% 0.66/0.97 cnf(c229,plain,r1(skolem0016,skolem0011(skolem0016))|p3(skolem0016),inference(resolution,[status(thm)],[c29, c39])).
% 0.66/0.97 cnf(c273,plain,p3(skolem0016)|~r1(skolem0001,skolem0016)|p4(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c229, c9])).
% 0.66/0.97 cnf(c442,plain,p3(skolem0016)|p4(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c273, c39])).
% 0.66/0.97 cnf(c272,plain,p3(skolem0016)|~r1(skolem0001,skolem0016)|p6(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c229, c7])).
% 0.66/0.97 cnf(c441,plain,p3(skolem0016)|p6(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c272, c39])).
% 0.66/0.97 cnf(c271,plain,p3(skolem0016)|~r1(skolem0001,skolem0016)|p2(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c229, c10])).
% 0.66/0.97 cnf(c440,plain,p3(skolem0016)|p2(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c271, c39])).
% 0.66/0.97 cnf(c270,plain,p3(skolem0016)|~r1(skolem0001,skolem0016)|p5(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c229, c8])).
% 0.66/0.97 cnf(c439,plain,p3(skolem0016)|p5(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c270, c39])).
% 0.66/0.97 cnf(c41,negated_conjecture,r1(skolem0001,skolem0017),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c228,plain,r1(skolem0017,skolem0011(skolem0017))|p3(skolem0017),inference(resolution,[status(thm)],[c29, c41])).
% 0.66/0.97 cnf(c269,plain,p3(skolem0017)|~r1(skolem0001,skolem0017)|p4(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c228, c9])).
% 0.66/0.97 cnf(c438,plain,p3(skolem0017)|p4(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c269, c41])).
% 0.66/0.97 cnf(c268,plain,p3(skolem0017)|~r1(skolem0001,skolem0017)|p6(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c228, c7])).
% 0.66/0.97 cnf(c437,plain,p3(skolem0017)|p6(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c268, c41])).
% 0.66/0.97 cnf(c267,plain,p3(skolem0017)|~r1(skolem0001,skolem0017)|p2(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c228, c10])).
% 0.66/0.97 cnf(c436,plain,p3(skolem0017)|p2(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c267, c41])).
% 0.66/0.97 cnf(c266,plain,p3(skolem0017)|~r1(skolem0001,skolem0017)|p5(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c228, c8])).
% 0.66/0.97 cnf(c435,plain,p3(skolem0017)|p5(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c266, c41])).
% 0.66/0.97 cnf(c27,negated_conjecture,~r1(skolem0001,X64)|r1(X64,skolem0010(X64))|p3(X64),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c218,plain,r1(skolem0014,skolem0010(skolem0014))|p3(skolem0014),inference(resolution,[status(thm)],[c27, c35])).
% 0.66/0.97 cnf(c265,plain,p3(skolem0014)|~r1(skolem0001,skolem0014)|p4(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c218, c9])).
% 0.66/0.97 cnf(c434,plain,p3(skolem0014)|p4(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c265, c35])).
% 0.66/0.97 cnf(c264,plain,p3(skolem0014)|~r1(skolem0001,skolem0014)|p6(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c218, c7])).
% 0.66/0.97 cnf(c433,plain,p3(skolem0014)|p6(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c264, c35])).
% 0.66/0.97 cnf(c263,plain,p3(skolem0014)|~r1(skolem0001,skolem0014)|p2(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c218, c10])).
% 0.66/0.97 cnf(c432,plain,p3(skolem0014)|p2(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c263, c35])).
% 0.66/0.97 cnf(c262,plain,p3(skolem0014)|~r1(skolem0001,skolem0014)|p5(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c218, c8])).
% 0.66/0.97 cnf(c431,plain,p3(skolem0014)|p5(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c262, c35])).
% 0.66/0.97 cnf(c216,plain,r1(skolem0016,skolem0010(skolem0016))|p3(skolem0016),inference(resolution,[status(thm)],[c27, c39])).
% 0.66/0.97 cnf(c252,plain,p3(skolem0016)|~r1(skolem0001,skolem0016)|p4(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c216, c9])).
% 0.66/0.97 cnf(c430,plain,p3(skolem0016)|p4(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c252, c39])).
% 0.66/0.97 cnf(c251,plain,p3(skolem0016)|~r1(skolem0001,skolem0016)|p6(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c216, c7])).
% 0.66/0.97 cnf(c429,plain,p3(skolem0016)|p6(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c251, c39])).
% 0.66/0.97 cnf(c250,plain,p3(skolem0016)|~r1(skolem0001,skolem0016)|p2(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c216, c10])).
% 0.66/0.97 cnf(c428,plain,p3(skolem0016)|p2(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c250, c39])).
% 0.66/0.97 cnf(c249,plain,p3(skolem0016)|~r1(skolem0001,skolem0016)|p5(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c216, c8])).
% 0.66/0.97 cnf(c427,plain,p3(skolem0016)|p5(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c249, c39])).
% 0.66/0.97 cnf(c215,plain,r1(skolem0017,skolem0010(skolem0017))|p3(skolem0017),inference(resolution,[status(thm)],[c27, c41])).
% 0.66/0.97 cnf(c248,plain,p3(skolem0017)|~r1(skolem0001,skolem0017)|p4(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c215, c9])).
% 0.66/0.97 cnf(c426,plain,p3(skolem0017)|p4(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c248, c41])).
% 0.66/0.97 cnf(c247,plain,p3(skolem0017)|~r1(skolem0001,skolem0017)|p6(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c215, c7])).
% 0.66/0.97 cnf(c425,plain,p3(skolem0017)|p6(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c247, c41])).
% 0.66/0.97 cnf(c246,plain,p3(skolem0017)|~r1(skolem0001,skolem0017)|p2(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c215, c10])).
% 0.66/0.97 cnf(c424,plain,p3(skolem0017)|p2(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c246, c41])).
% 0.66/0.97 cnf(c245,plain,p3(skolem0017)|~r1(skolem0001,skolem0017)|p5(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c215, c8])).
% 0.66/0.97 cnf(c423,plain,p3(skolem0017)|p5(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c245, c41])).
% 0.66/0.97 cnf(c25,negated_conjecture,~r1(skolem0001,X63)|r1(X63,skolem0009(X63))|p5(X63),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c210,plain,r1(skolem0015,skolem0009(skolem0015))|p5(skolem0015),inference(resolution,[status(thm)],[c25, c37])).
% 0.66/0.97 cnf(c235,plain,p5(skolem0015)|~r1(skolem0001,skolem0015)|p4(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c210, c9])).
% 0.66/0.97 cnf(c422,plain,p5(skolem0015)|p4(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c235, c37])).
% 0.66/0.97 cnf(c234,plain,p5(skolem0015)|~r1(skolem0001,skolem0015)|p6(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c210, c7])).
% 0.66/0.97 cnf(c421,plain,p5(skolem0015)|p6(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c234, c37])).
% 0.66/0.97 cnf(c233,plain,p5(skolem0015)|~r1(skolem0001,skolem0015)|p2(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c210, c10])).
% 0.66/0.97 cnf(c420,plain,p5(skolem0015)|p2(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c233, c37])).
% 0.66/0.97 cnf(c232,plain,p5(skolem0015)|~r1(skolem0001,skolem0015)|p5(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c210, c8])).
% 0.66/0.97 cnf(c419,plain,p5(skolem0015)|p5(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c232, c37])).
% 0.66/0.97 cnf(c209,plain,r1(skolem0016,skolem0009(skolem0016))|p5(skolem0016),inference(resolution,[status(thm)],[c25, c39])).
% 0.66/0.97 cnf(c227,plain,p5(skolem0016)|~r1(skolem0001,skolem0016)|p4(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c209, c9])).
% 0.66/0.97 cnf(c418,plain,p5(skolem0016)|p4(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c227, c39])).
% 0.66/0.97 cnf(c226,plain,p5(skolem0016)|~r1(skolem0001,skolem0016)|p6(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c209, c7])).
% 0.66/0.97 cnf(c417,plain,p5(skolem0016)|p6(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c226, c39])).
% 0.66/0.97 cnf(c225,plain,p5(skolem0016)|~r1(skolem0001,skolem0016)|p2(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c209, c10])).
% 0.66/0.97 cnf(c416,plain,p5(skolem0016)|p2(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c225, c39])).
% 0.66/0.97 cnf(c224,plain,p5(skolem0016)|~r1(skolem0001,skolem0016)|p5(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c209, c8])).
% 0.66/0.97 cnf(c415,plain,p5(skolem0016)|p5(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c224, c39])).
% 0.66/0.97 cnf(c208,plain,r1(skolem0017,skolem0009(skolem0017))|p5(skolem0017),inference(resolution,[status(thm)],[c25, c41])).
% 0.66/0.97 cnf(c223,plain,p5(skolem0017)|~r1(skolem0001,skolem0017)|p4(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c208, c9])).
% 0.66/0.97 cnf(c414,plain,p5(skolem0017)|p4(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c223, c41])).
% 0.66/0.97 cnf(c222,plain,p5(skolem0017)|~r1(skolem0001,skolem0017)|p6(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c208, c7])).
% 0.66/0.97 cnf(c413,plain,p5(skolem0017)|p6(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c222, c41])).
% 0.66/0.97 cnf(c221,plain,p5(skolem0017)|~r1(skolem0001,skolem0017)|p2(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c208, c10])).
% 0.66/0.97 cnf(c412,plain,p5(skolem0017)|p2(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c221, c41])).
% 0.66/0.97 cnf(c220,plain,p5(skolem0017)|~r1(skolem0001,skolem0017)|p5(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c208, c8])).
% 0.66/0.97 cnf(c411,plain,p5(skolem0017)|p5(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c220, c41])).
% 0.66/0.97 cnf(c23,negated_conjecture,~r1(skolem0001,X62)|r1(X62,skolem0008(X62))|p5(X62),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c185,plain,r1(skolem0015,skolem0008(skolem0015))|p5(skolem0015),inference(resolution,[status(thm)],[c23, c37])).
% 0.66/0.97 cnf(c198,plain,p5(skolem0015)|~r1(skolem0001,skolem0015)|p4(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c185, c9])).
% 0.66/0.97 cnf(c410,plain,p5(skolem0015)|p4(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c198, c37])).
% 0.66/0.97 cnf(c197,plain,p5(skolem0015)|~r1(skolem0001,skolem0015)|p6(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c185, c7])).
% 0.66/0.97 cnf(c409,plain,p5(skolem0015)|p6(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c197, c37])).
% 0.66/0.97 cnf(c196,plain,p5(skolem0015)|~r1(skolem0001,skolem0015)|p2(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c185, c10])).
% 0.66/0.97 cnf(c408,plain,p5(skolem0015)|p2(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c196, c37])).
% 0.66/0.97 cnf(c195,plain,p5(skolem0015)|~r1(skolem0001,skolem0015)|p5(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c185, c8])).
% 0.66/0.97 cnf(c407,plain,p5(skolem0015)|p5(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c195, c37])).
% 0.66/0.97 cnf(c184,plain,r1(skolem0016,skolem0008(skolem0016))|p5(skolem0016),inference(resolution,[status(thm)],[c23, c39])).
% 0.66/0.97 cnf(c194,plain,p5(skolem0016)|~r1(skolem0001,skolem0016)|p4(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c184, c9])).
% 0.66/0.97 cnf(c406,plain,p5(skolem0016)|p4(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c194, c39])).
% 0.66/0.97 cnf(c193,plain,p5(skolem0016)|~r1(skolem0001,skolem0016)|p6(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c184, c7])).
% 0.66/0.97 cnf(c405,plain,p5(skolem0016)|p6(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c193, c39])).
% 0.66/0.97 cnf(c192,plain,p5(skolem0016)|~r1(skolem0001,skolem0016)|p2(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c184, c10])).
% 0.66/0.97 cnf(c404,plain,p5(skolem0016)|p2(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c192, c39])).
% 0.66/0.97 cnf(c191,plain,p5(skolem0016)|~r1(skolem0001,skolem0016)|p5(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c184, c8])).
% 0.66/0.97 cnf(c403,plain,p5(skolem0016)|p5(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c191, c39])).
% 0.66/0.97 cnf(c183,plain,r1(skolem0017,skolem0008(skolem0017))|p5(skolem0017),inference(resolution,[status(thm)],[c23, c41])).
% 0.66/0.97 cnf(c190,plain,p5(skolem0017)|~r1(skolem0001,skolem0017)|p4(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c183, c9])).
% 0.66/0.97 cnf(c402,plain,p5(skolem0017)|p4(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c190, c41])).
% 0.66/0.97 cnf(c189,plain,p5(skolem0017)|~r1(skolem0001,skolem0017)|p6(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c183, c7])).
% 0.66/0.97 cnf(c401,plain,p5(skolem0017)|p6(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c189, c41])).
% 0.66/0.97 cnf(c188,plain,p5(skolem0017)|~r1(skolem0001,skolem0017)|p2(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c183, c10])).
% 0.66/0.97 cnf(c400,plain,p5(skolem0017)|p2(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c188, c41])).
% 0.66/0.97 cnf(c187,plain,p5(skolem0017)|~r1(skolem0001,skolem0017)|p5(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c183, c8])).
% 0.66/0.97 cnf(c399,plain,p5(skolem0017)|p5(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c187, c41])).
% 0.66/0.97 cnf(c14,negated_conjecture,~r1(skolem0001,X49)|~p6(skolem0003(X49))|p4(X49),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c13,negated_conjecture,~r1(skolem0001,X52)|r1(X52,skolem0003(X52))|p4(X52),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c86,plain,r1(skolem0015,skolem0003(skolem0015))|p4(skolem0015),inference(resolution,[status(thm)],[c13, c37])).
% 0.66/0.97 cnf(c101,plain,p4(skolem0015)|~r1(skolem0001,skolem0015)|p6(skolem0003(skolem0015)),inference(resolution,[status(thm)],[c86, c7])).
% 0.66/0.97 cnf(c396,plain,p4(skolem0015)|p6(skolem0003(skolem0015)),inference(resolution,[status(thm)],[c101, c37])).
% 0.66/0.97 cnf(c397,plain,p4(skolem0015)|~r1(skolem0001,skolem0015),inference(resolution,[status(thm)],[c396, c14])).
% 0.66/0.97 cnf(c398,plain,p4(skolem0015),inference(resolution,[status(thm)],[c397, c37])).
% 0.66/0.97 cnf(c85,plain,r1(skolem0014,skolem0003(skolem0014))|p4(skolem0014),inference(resolution,[status(thm)],[c13, c35])).
% 0.66/0.97 cnf(c97,plain,p4(skolem0014)|~r1(skolem0001,skolem0014)|p6(skolem0003(skolem0014)),inference(resolution,[status(thm)],[c85, c7])).
% 0.66/0.97 cnf(c391,plain,p4(skolem0014)|p6(skolem0003(skolem0014)),inference(resolution,[status(thm)],[c97, c35])).
% 0.66/0.97 cnf(c392,plain,p4(skolem0014)|~r1(skolem0001,skolem0014),inference(resolution,[status(thm)],[c391, c14])).
% 0.66/0.97 cnf(c393,plain,p4(skolem0014),inference(resolution,[status(thm)],[c392, c35])).
% 0.66/0.97 cnf(c84,plain,r1(skolem0016,skolem0003(skolem0016))|p4(skolem0016),inference(resolution,[status(thm)],[c13, c39])).
% 0.66/0.97 cnf(c93,plain,p4(skolem0016)|~r1(skolem0001,skolem0016)|p6(skolem0003(skolem0016)),inference(resolution,[status(thm)],[c84, c7])).
% 0.66/0.97 cnf(c385,plain,p4(skolem0016)|p6(skolem0003(skolem0016)),inference(resolution,[status(thm)],[c93, c39])).
% 0.66/0.97 cnf(c387,plain,p4(skolem0016)|~r1(skolem0001,skolem0016),inference(resolution,[status(thm)],[c385, c14])).
% 0.66/0.97 cnf(c388,plain,p4(skolem0016),inference(resolution,[status(thm)],[c387, c39])).
% 0.66/0.97 cnf(c83,plain,r1(skolem0017,skolem0003(skolem0017))|p4(skolem0017),inference(resolution,[status(thm)],[c13, c41])).
% 0.66/0.97 cnf(c89,plain,p4(skolem0017)|~r1(skolem0001,skolem0017)|p6(skolem0003(skolem0017)),inference(resolution,[status(thm)],[c83, c7])).
% 0.66/0.97 cnf(c380,plain,p4(skolem0017)|p6(skolem0003(skolem0017)),inference(resolution,[status(thm)],[c89, c41])).
% 0.66/0.97 cnf(c381,plain,p4(skolem0017)|~r1(skolem0001,skolem0017),inference(resolution,[status(thm)],[c380, c14])).
% 0.66/0.97 cnf(c382,plain,p4(skolem0017),inference(resolution,[status(thm)],[c381, c41])).
% 0.66/0.97 cnf(c12,negated_conjecture,~r1(skolem0001,X48)|~p6(skolem0002(X48))|p6(X48),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c11,negated_conjecture,~r1(skolem0001,X47)|r1(X47,skolem0002(X47))|p6(X47),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c66,plain,r1(skolem0017,skolem0002(skolem0017))|p6(skolem0017),inference(resolution,[status(thm)],[c11, c41])).
% 0.66/0.97 cnf(c81,plain,p6(skolem0017)|~r1(skolem0001,skolem0017)|p6(skolem0002(skolem0017)),inference(resolution,[status(thm)],[c66, c7])).
% 0.66/0.97 cnf(c374,plain,p6(skolem0017)|p6(skolem0002(skolem0017)),inference(resolution,[status(thm)],[c81, c41])).
% 0.66/0.97 cnf(c375,plain,p6(skolem0017)|~r1(skolem0001,skolem0017),inference(resolution,[status(thm)],[c374, c12])).
% 0.66/0.97 cnf(c377,plain,p6(skolem0017),inference(resolution,[status(thm)],[c375, c41])).
% 0.66/0.97 cnf(c65,plain,r1(skolem0014,skolem0002(skolem0014))|p6(skolem0014),inference(resolution,[status(thm)],[c11, c35])).
% 0.66/0.97 cnf(c77,plain,p6(skolem0014)|~r1(skolem0001,skolem0014)|p6(skolem0002(skolem0014)),inference(resolution,[status(thm)],[c65, c7])).
% 0.66/0.97 cnf(c369,plain,p6(skolem0014)|p6(skolem0002(skolem0014)),inference(resolution,[status(thm)],[c77, c35])).
% 0.66/0.97 cnf(c370,plain,p6(skolem0014)|~r1(skolem0001,skolem0014),inference(resolution,[status(thm)],[c369, c12])).
% 0.66/0.97 cnf(c371,plain,p6(skolem0014),inference(resolution,[status(thm)],[c370, c35])).
% 0.66/0.97 cnf(c42,negated_conjecture,~p1(skolem0017),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c295,plain,r1(skolem0017,skolem0013(skolem0017))|p1(skolem0017),inference(resolution,[status(thm)],[c33, c41])).
% 0.66/0.97 cnf(c337,plain,r1(skolem0017,skolem0013(skolem0017)),inference(resolution,[status(thm)],[c295, c42])).
% 0.66/0.97 cnf(c341,plain,~r1(skolem0001,skolem0017)|p4(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c337, c9])).
% 0.66/0.97 cnf(c367,plain,p4(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c341, c41])).
% 0.66/0.97 cnf(c340,plain,~r1(skolem0001,skolem0017)|p6(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c337, c7])).
% 0.66/0.97 cnf(c365,plain,p6(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c340, c41])).
% 0.66/0.97 cnf(c339,plain,~r1(skolem0001,skolem0017)|p2(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c337, c10])).
% 0.66/0.97 cnf(c364,plain,p2(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c339, c41])).
% 0.66/0.97 cnf(c338,plain,~r1(skolem0001,skolem0017)|p5(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c337, c8])).
% 0.66/0.97 cnf(c363,plain,p5(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c338, c41])).
% 0.66/0.97 cnf(c274,plain,r1(skolem0017,skolem0012(skolem0017))|p1(skolem0017),inference(resolution,[status(thm)],[c31, c41])).
% 0.66/0.97 cnf(c307,plain,r1(skolem0017,skolem0012(skolem0017)),inference(resolution,[status(thm)],[c274, c42])).
% 0.66/0.97 cnf(c312,plain,~r1(skolem0001,skolem0017)|p4(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c307, c9])).
% 0.66/0.97 cnf(c362,plain,p4(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c312, c41])).
% 0.66/0.97 cnf(c64,plain,r1(skolem0016,skolem0002(skolem0016))|p6(skolem0016),inference(resolution,[status(thm)],[c11, c39])).
% 0.66/0.97 cnf(c73,plain,p6(skolem0016)|~r1(skolem0001,skolem0016)|p6(skolem0002(skolem0016)),inference(resolution,[status(thm)],[c64, c7])).
% 0.66/0.97 cnf(c359,plain,p6(skolem0016)|p6(skolem0002(skolem0016)),inference(resolution,[status(thm)],[c73, c39])).
% 0.66/0.97 cnf(c360,plain,p6(skolem0016)|~r1(skolem0001,skolem0016),inference(resolution,[status(thm)],[c359, c12])).
% 0.66/0.97 cnf(c361,plain,p6(skolem0016),inference(resolution,[status(thm)],[c360, c39])).
% 0.66/0.97 cnf(c311,plain,~r1(skolem0001,skolem0017)|p6(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c307, c7])).
% 0.66/0.97 cnf(c358,plain,p6(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c311, c41])).
% 0.66/0.97 cnf(c310,plain,~r1(skolem0001,skolem0017)|p2(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c307, c10])).
% 0.66/0.97 cnf(c357,plain,p2(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c310, c41])).
% 0.66/0.97 cnf(c309,plain,~r1(skolem0001,skolem0017)|p5(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c307, c8])).
% 0.66/0.97 cnf(c355,plain,p5(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c309, c41])).
% 0.66/0.97 cnf(c38,negated_conjecture,~p3(skolem0015),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c230,plain,r1(skolem0015,skolem0011(skolem0015))|p3(skolem0015),inference(resolution,[status(thm)],[c29, c37])).
% 0.66/0.97 cnf(c282,plain,r1(skolem0015,skolem0011(skolem0015)),inference(resolution,[status(thm)],[c230, c38])).
% 0.66/0.97 cnf(c286,plain,~r1(skolem0001,skolem0015)|p4(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c282, c9])).
% 0.66/0.97 cnf(c332,plain,p4(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c286, c37])).
% 0.66/0.97 cnf(c285,plain,~r1(skolem0001,skolem0015)|p6(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c282, c7])).
% 0.66/0.97 cnf(c331,plain,p6(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c285, c37])).
% 0.66/0.97 cnf(c63,plain,r1(skolem0015,skolem0002(skolem0015))|p6(skolem0015),inference(resolution,[status(thm)],[c11, c37])).
% 0.66/0.97 cnf(c69,plain,p6(skolem0015)|~r1(skolem0001,skolem0015)|p6(skolem0002(skolem0015)),inference(resolution,[status(thm)],[c63, c7])).
% 0.66/0.97 cnf(c328,plain,p6(skolem0015)|p6(skolem0002(skolem0015)),inference(resolution,[status(thm)],[c69, c37])).
% 0.66/0.97 cnf(c329,plain,p6(skolem0015)|~r1(skolem0001,skolem0015),inference(resolution,[status(thm)],[c328, c12])).
% 0.66/0.97 cnf(c330,plain,p6(skolem0015),inference(resolution,[status(thm)],[c329, c37])).
% 0.66/0.97 cnf(c284,plain,~r1(skolem0001,skolem0015)|p2(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c282, c10])).
% 0.66/0.97 cnf(c327,plain,p2(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c284, c37])).
% 0.66/0.97 cnf(c283,plain,~r1(skolem0001,skolem0015)|p5(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c282, c8])).
% 0.66/0.97 cnf(c326,plain,p5(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c283, c37])).
% 0.66/0.97 cnf(c217,plain,r1(skolem0015,skolem0010(skolem0015))|p3(skolem0015),inference(resolution,[status(thm)],[c27, c37])).
% 0.66/0.97 cnf(c257,plain,r1(skolem0015,skolem0010(skolem0015)),inference(resolution,[status(thm)],[c217, c38])).
% 0.66/0.97 cnf(c261,plain,~r1(skolem0001,skolem0015)|p4(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c257, c9])).
% 0.66/0.97 cnf(c302,plain,p4(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c261, c37])).
% 0.66/0.97 cnf(c260,plain,~r1(skolem0001,skolem0015)|p6(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c257, c7])).
% 0.66/0.97 cnf(c301,plain,p6(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c260, c37])).
% 0.66/0.97 cnf(c34,negated_conjecture,~r1(skolem0001,X70)|~p1(skolem0013(X70))|p1(X70),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c259,plain,~r1(skolem0001,skolem0015)|p2(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c257, c10])).
% 0.66/0.97 cnf(c300,plain,p2(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c259, c37])).
% 0.66/0.97 cnf(c258,plain,~r1(skolem0001,skolem0015)|p5(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c257, c8])).
% 0.66/0.97 cnf(c299,plain,p5(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c258, c37])).
% 0.66/0.97 cnf(c36,negated_conjecture,~p5(skolem0014),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c211,plain,r1(skolem0014,skolem0009(skolem0014))|p5(skolem0014),inference(resolution,[status(thm)],[c25, c35])).
% 0.66/0.97 cnf(c240,plain,r1(skolem0014,skolem0009(skolem0014)),inference(resolution,[status(thm)],[c211, c36])).
% 0.66/0.97 cnf(c244,plain,~r1(skolem0001,skolem0014)|p4(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c240, c9])).
% 0.66/0.97 cnf(c294,plain,p4(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c244, c35])).
% 0.66/0.97 cnf(c243,plain,~r1(skolem0001,skolem0014)|p6(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c240, c7])).
% 0.66/0.97 cnf(c293,plain,p6(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c243, c35])).
% 0.66/0.97 cnf(c242,plain,~r1(skolem0001,skolem0014)|p2(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c240, c10])).
% 0.66/0.97 cnf(c292,plain,p2(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c242, c35])).
% 0.66/0.97 cnf(c32,negated_conjecture,~r1(skolem0001,X68)|~p3(skolem0012(X68))|p1(X68),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c241,plain,~r1(skolem0001,skolem0014)|p5(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c240, c8])).
% 0.66/0.97 cnf(c291,plain,p5(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c241, c35])).
% 0.66/0.97 cnf(c30,negated_conjecture,~r1(skolem0001,X66)|~p1(skolem0011(X66))|p3(X66),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c186,plain,r1(skolem0014,skolem0008(skolem0014))|p5(skolem0014),inference(resolution,[status(thm)],[c23, c35])).
% 0.66/0.97 cnf(c203,plain,r1(skolem0014,skolem0008(skolem0014)),inference(resolution,[status(thm)],[c186, c36])).
% 0.66/0.97 cnf(c207,plain,~r1(skolem0001,skolem0014)|p4(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c203, c9])).
% 0.66/0.97 cnf(c219,plain,p4(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c207, c35])).
% 0.66/0.97 cnf(c206,plain,~r1(skolem0001,skolem0014)|p6(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c203, c7])).
% 0.66/0.97 cnf(c214,plain,p6(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c206, c35])).
% 0.66/0.97 cnf(c205,plain,~r1(skolem0001,skolem0014)|p2(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c203, c10])).
% 0.66/0.97 cnf(c213,plain,p2(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c205, c35])).
% 0.66/0.97 cnf(c204,plain,~r1(skolem0001,skolem0014)|p5(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c203, c8])).
% 0.66/0.97 cnf(c212,plain,p5(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c204, c35])).
% 0.66/0.97 cnf(c28,negated_conjecture,~r1(skolem0001,X61)|~p3(skolem0010(X61))|p3(X61),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c21,negated_conjecture,~r1(skolem0001,X60)|r1(X60,skolem0007(X60))|p4(X60),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c26,negated_conjecture,~r1(skolem0001,X59)|~p1(skolem0009(X59))|p5(X59),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c19,negated_conjecture,~r1(skolem0001,X58)|r1(X58,skolem0006(X58))|p6(X58),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c24,negated_conjecture,~r1(skolem0001,X57)|~p3(skolem0008(X57))|p5(X57),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c17,negated_conjecture,~r1(skolem0001,X56)|r1(X56,skolem0005(X56))|p4(X56),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c22,negated_conjecture,~r1(skolem0001,X55)|~p2(skolem0007(X55))|p4(X55),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c15,negated_conjecture,~r1(skolem0001,X54)|r1(X54,skolem0004(X54))|p6(X54),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c20,negated_conjecture,~r1(skolem0001,X53)|~p2(skolem0006(X53))|p6(X53),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c18,negated_conjecture,~r1(skolem0001,X51)|~p4(skolem0005(X51))|p4(X51),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c16,negated_conjecture,~r1(skolem0001,X50)|~p4(skolem0004(X50))|p6(X50),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 cnf(c62,plain,~r1(skolem0001,skolem0001)|p2(skolem0017),inference(resolution,[status(thm)],[c10, c41])).
% 0.66/0.97 cnf(c61,plain,~r1(skolem0001,skolem0001)|p2(skolem0014),inference(resolution,[status(thm)],[c10, c35])).
% 0.66/0.97 cnf(c60,plain,~r1(skolem0001,skolem0001)|p2(skolem0016),inference(resolution,[status(thm)],[c10, c39])).
% 0.66/0.97 cnf(c59,plain,~r1(skolem0001,skolem0001)|p2(skolem0015),inference(resolution,[status(thm)],[c10, c37])).
% 0.66/0.97 cnf(c58,plain,~r1(skolem0001,skolem0001)|p2(skolem0001),inference(factor,[status(thm)],[c10])).
% 0.66/0.97 cnf(c53,plain,~r1(skolem0001,skolem0001)|p4(skolem0001),inference(factor,[status(thm)],[c9])).
% 0.66/0.97 cnf(c52,plain,~r1(skolem0001,skolem0001)|p5(skolem0017),inference(resolution,[status(thm)],[c8, c41])).
% 0.66/0.97 cnf(c51,plain,~r1(skolem0001,skolem0001)|p5(skolem0014),inference(resolution,[status(thm)],[c8, c35])).
% 0.66/0.97 cnf(c50,plain,~r1(skolem0001,skolem0001)|p5(skolem0016),inference(resolution,[status(thm)],[c8, c39])).
% 0.66/0.97 cnf(c49,plain,~r1(skolem0001,skolem0001)|p5(skolem0015),inference(resolution,[status(thm)],[c8, c37])).
% 0.66/0.97 cnf(c48,plain,~r1(skolem0001,skolem0001)|p5(skolem0001),inference(factor,[status(thm)],[c8])).
% 0.66/0.97 cnf(c43,plain,~r1(skolem0001,skolem0001)|p6(skolem0001),inference(factor,[status(thm)],[c7])).
% 0.66/0.97 cnf(c40,negated_conjecture,~p2(skolem0016),inference(split_conjunct,[status(thm)],[c6])).
% 0.66/0.97 % SZS output end Saturation
% 0.66/0.97
% 0.66/0.97 % Initial clauses : 36
% 0.66/0.97 % Processed clauses : 369
% 0.66/0.97 % Factors computed : 4
% 0.66/0.97 % Resolvents computed: 424
% 0.66/0.97 % Tautologies deleted: 0
% 0.66/0.97 % Forward subsumed : 95
% 0.66/0.97 % Backward subsumed : 193
% 0.66/0.97 % -------- CPU Time ---------
% 0.66/0.97 % User time : 0.565 s
% 0.66/0.97 % System time : 0.031 s
% 0.66/0.97 % Total time : 0.596 s
%------------------------------------------------------------------------------