%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL665+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n031.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:57 PM UTC 2026
% Result : CounterSatisfiable 1.66s 1.92s
% Output : Saturation 1.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL665+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n031.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 03:06:09 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.41 (re.compile("\."), Token.FullStop),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.41 (re.compile("\("), Token.OpenPar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.41 (re.compile("\)"), Token.ClosePar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.41 (re.compile("\["), Token.OpenSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.21/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.32/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.57 """
% 1.66/1.92 % Version: 1.5
% 1.66/1.92 % SZS status CounterSatisfiable
% 1.66/1.92 % SZS output start Saturation
% 1.66/1.92 fof(reflexivity,axiom,(![X]:r1(X,X)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 1.66/1.92 fof(c43,plain,(![X39]:r1(X39,X39)),inference(variable_rename,[status(thm)],[reflexivity])).
% 1.66/1.92 cnf(c44,plain,r1(X40,X40),inference(split_conjunct,[status(thm)],[c43])).
% 1.66/1.92 fof(main,conjecture,(~(?[X]:(~((((((((((((((((((((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p26(X))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p25(X)))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p24(X)))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p22(X)))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p26(X)))&(~p16(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p26(X)))&(~p14(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p24(X)))&(~p16(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p24(X)))&(~p14(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p22(X)))&(~p16(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p22(X)))&(~p14(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p23(X)))&(~p15(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p21(X)))&(~p15(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p23(X)))&(~p13(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p21(X)))&(~p13(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p23(X)))&(~p11(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p21(X)))&(~p11(Y))))))))|(![Y]:((~r1(X,Y))|p15(Y))))|(![Y]:((~r1(X,Y))|p13(Y))))|(![Y]:((~r1(X,Y))|p12(Y))))|(![Y]:((~r1(X,Y))|p11(Y))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 1.66/1.92 fof(c0,negated_conjecture,(~(~(?[X]:(~((((((((((((((((((((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p26(X))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p25(X)))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p24(X)))))))|(~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p22(X)))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p26(X)))&(~p16(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p26(X)))&(~p14(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p24(X)))&(~p16(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p24(X)))&(~p14(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p22(X)))&(~p16(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p22(X)))&(~p14(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p23(X)))&(~p15(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p21(X)))&(~p15(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p23(X)))&(~p13(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p21(X)))&(~p13(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p23(X)))&(~p11(Y))))))))|(~(![Y]:((~r1(X,Y))|(~((![X]:((~r1(Y,X))|p21(X)))&(~p11(Y))))))))|(![Y]:((~r1(X,Y))|p15(Y))))|(![Y]:((~r1(X,Y))|p13(Y))))|(![Y]:((~r1(X,Y))|p12(Y))))|(![Y]:((~r1(X,Y))|p11(Y)))))))),inference(assume_negation,[status(cth)],[main])).
% 1.66/1.92 fof(c1,negated_conjecture,(~(~(?[X]:(~((((((((((((((((((((~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p26(X))))))|(~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p25(X)))))))|(~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p24(X)))))))|(~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p22(X)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p26(X)))&~p16(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p26(X)))&~p14(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p24(X)))&~p16(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p24(X)))&~p14(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p22(X)))&~p16(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p22(X)))&~p14(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p23(X)))&~p15(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p21(X)))&~p15(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p23(X)))&~p13(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p21(X)))&~p13(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p23(X)))&~p11(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((![X]:(~r1(Y,X)|p21(X)))&~p11(Y)))))))|(![Y]:(~r1(X,Y)|p15(Y))))|(![Y]:(~r1(X,Y)|p13(Y))))|(![Y]:(~r1(X,Y)|p12(Y))))|(![Y]:(~r1(X,Y)|p11(Y)))))))),inference(fof_simplification,[status(thm)],[c0])).
% 1.66/1.92 fof(c2,negated_conjecture,(?[X]:((((((((((((((((((((![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p26(X)))))&(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p25(X))))))&(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p24(X))))))&(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p22(X))))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p26(X)))|p16(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p26(X)))|p14(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p24(X)))|p16(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p24(X)))|p14(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p22(X)))|p16(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p22(X)))|p14(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p23(X)))|p15(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p21(X)))|p15(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p23(X)))|p13(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p21(X)))|p13(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p23(X)))|p11(Y)))))&(![Y]:(~r1(X,Y)|((?[X]:(r1(Y,X)&~p21(X)))|p11(Y)))))&(?[Y]:(r1(X,Y)&~p15(Y))))&(?[Y]:(r1(X,Y)&~p13(Y))))&(?[Y]:(r1(X,Y)&~p12(Y))))&(?[Y]:(r1(X,Y)&~p11(Y))))),inference(fof_nnf,[status(thm)],[c1])).
% 1.66/1.92 fof(c3,negated_conjecture,(?[X2]:((((((((((((((((((((![X3]:(~r1(X2,X3)|(![X4]:(~r1(X3,X4)|p26(X4)))))&(![X5]:(~r1(X2,X5)|(![X6]:(~r1(X5,X6)|p25(X6))))))&(![X7]:(~r1(X2,X7)|(![X8]:(~r1(X7,X8)|p24(X8))))))&(![X9]:(~r1(X2,X9)|(![X10]:(~r1(X9,X10)|p22(X10))))))&(![X11]:(~r1(X2,X11)|((?[X12]:(r1(X11,X12)&~p26(X12)))|p16(X11)))))&(![X13]:(~r1(X2,X13)|((?[X14]:(r1(X13,X14)&~p26(X14)))|p14(X13)))))&(![X15]:(~r1(X2,X15)|((?[X16]:(r1(X15,X16)&~p24(X16)))|p16(X15)))))&(![X17]:(~r1(X2,X17)|((?[X18]:(r1(X17,X18)&~p24(X18)))|p14(X17)))))&(![X19]:(~r1(X2,X19)|((?[X20]:(r1(X19,X20)&~p22(X20)))|p16(X19)))))&(![X21]:(~r1(X2,X21)|((?[X22]:(r1(X21,X22)&~p22(X22)))|p14(X21)))))&(![X23]:(~r1(X2,X23)|((?[X24]:(r1(X23,X24)&~p23(X24)))|p15(X23)))))&(![X25]:(~r1(X2,X25)|((?[X26]:(r1(X25,X26)&~p21(X26)))|p15(X25)))))&(![X27]:(~r1(X2,X27)|((?[X28]:(r1(X27,X28)&~p23(X28)))|p13(X27)))))&(![X29]:(~r1(X2,X29)|((?[X30]:(r1(X29,X30)&~p21(X30)))|p13(X29)))))&(![X31]:(~r1(X2,X31)|((?[X32]:(r1(X31,X32)&~p23(X32)))|p11(X31)))))&(![X33]:(~r1(X2,X33)|((?[X34]:(r1(X33,X34)&~p21(X34)))|p11(X33)))))&(?[X35]:(r1(X2,X35)&~p15(X35))))&(?[X36]:(r1(X2,X36)&~p13(X36))))&(?[X37]:(r1(X2,X37)&~p12(X37))))&(?[X38]:(r1(X2,X38)&~p11(X38))))),inference(variable_rename,[status(thm)],[c2])).
% 1.66/1.92 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)|p26(X4)))&(~r1(skolem0001,X5)|(~r1(X5,X6)|p25(X6))))&(~r1(skolem0001,X7)|(~r1(X7,X8)|p24(X8))))&(~r1(skolem0001,X9)|(~r1(X9,X10)|p22(X10))))&(~r1(skolem0001,X11)|((r1(X11,skolem0002(X11))&~p26(skolem0002(X11)))|p16(X11))))&(~r1(skolem0001,X13)|((r1(X13,skolem0003(X13))&~p26(skolem0003(X13)))|p14(X13))))&(~r1(skolem0001,X15)|((r1(X15,skolem0004(X15))&~p24(skolem0004(X15)))|p16(X15))))&(~r1(skolem0001,X17)|((r1(X17,skolem0005(X17))&~p24(skolem0005(X17)))|p14(X17))))&(~r1(skolem0001,X19)|((r1(X19,skolem0006(X19))&~p22(skolem0006(X19)))|p16(X19))))&(~r1(skolem0001,X21)|((r1(X21,skolem0007(X21))&~p22(skolem0007(X21)))|p14(X21))))&(~r1(skolem0001,X23)|((r1(X23,skolem0008(X23))&~p23(skolem0008(X23)))|p15(X23))))&(~r1(skolem0001,X25)|((r1(X25,skolem0009(X25))&~p21(skolem0009(X25)))|p15(X25))))&(~r1(skolem0001,X27)|((r1(X27,skolem0010(X27))&~p23(skolem0010(X27)))|p13(X27))))&(~r1(skolem0001,X29)|((r1(X29,skolem0011(X29))&~p21(skolem0011(X29)))|p13(X29))))&(~r1(skolem0001,X31)|((r1(X31,skolem0012(X31))&~p23(skolem0012(X31)))|p11(X31))))&(~r1(skolem0001,X33)|((r1(X33,skolem0013(X33))&~p21(skolem0013(X33)))|p11(X33))))&(r1(skolem0001,skolem0014)&~p15(skolem0014)))&(r1(skolem0001,skolem0015)&~p13(skolem0015)))&(r1(skolem0001,skolem0016)&~p12(skolem0016)))&(r1(skolem0001,skolem0017)&~p11(skolem0017))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((((((((((((((((((((![X3]:(~r1(skolem0001,X3)|(![X4]:(~r1(X3,X4)|p26(X4)))))&(![X5]:(~r1(skolem0001,X5)|(![X6]:(~r1(X5,X6)|p25(X6))))))&(![X7]:(~r1(skolem0001,X7)|(![X8]:(~r1(X7,X8)|p24(X8))))))&(![X9]:(~r1(skolem0001,X9)|(![X10]:(~r1(X9,X10)|p22(X10))))))&(![X11]:(~r1(skolem0001,X11)|((r1(X11,skolem0002(X11))&~p26(skolem0002(X11)))|p16(X11)))))&(![X13]:(~r1(skolem0001,X13)|((r1(X13,skolem0003(X13))&~p26(skolem0003(X13)))|p14(X13)))))&(![X15]:(~r1(skolem0001,X15)|((r1(X15,skolem0004(X15))&~p24(skolem0004(X15)))|p16(X15)))))&(![X17]:(~r1(skolem0001,X17)|((r1(X17,skolem0005(X17))&~p24(skolem0005(X17)))|p14(X17)))))&(![X19]:(~r1(skolem0001,X19)|((r1(X19,skolem0006(X19))&~p22(skolem0006(X19)))|p16(X19)))))&(![X21]:(~r1(skolem0001,X21)|((r1(X21,skolem0007(X21))&~p22(skolem0007(X21)))|p14(X21)))))&(![X23]:(~r1(skolem0001,X23)|((r1(X23,skolem0008(X23))&~p23(skolem0008(X23)))|p15(X23)))))&(![X25]:(~r1(skolem0001,X25)|((r1(X25,skolem0009(X25))&~p21(skolem0009(X25)))|p15(X25)))))&(![X27]:(~r1(skolem0001,X27)|((r1(X27,skolem0010(X27))&~p23(skolem0010(X27)))|p13(X27)))))&(![X29]:(~r1(skolem0001,X29)|((r1(X29,skolem0011(X29))&~p21(skolem0011(X29)))|p13(X29)))))&(![X31]:(~r1(skolem0001,X31)|((r1(X31,skolem0012(X31))&~p23(skolem0012(X31)))|p11(X31)))))&(![X33]:(~r1(skolem0001,X33)|((r1(X33,skolem0013(X33))&~p21(skolem0013(X33)))|p11(X33)))))&(r1(skolem0001,skolem0014)&~p15(skolem0014)))&(r1(skolem0001,skolem0015)&~p13(skolem0015)))&(r1(skolem0001,skolem0016)&~p12(skolem0016)))&(r1(skolem0001,skolem0017)&~p11(skolem0017))),inference(skolemize,[status(esa)],[c3])).])).
% 1.66/1.92 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)|p26(X4)))&(~r1(skolem0001,X5)|(~r1(X5,X6)|p25(X6))))&(~r1(skolem0001,X7)|(~r1(X7,X8)|p24(X8))))&(~r1(skolem0001,X9)|(~r1(X9,X10)|p22(X10))))&((~r1(skolem0001,X11)|(r1(X11,skolem0002(X11))|p16(X11)))&(~r1(skolem0001,X11)|(~p26(skolem0002(X11))|p16(X11)))))&((~r1(skolem0001,X13)|(r1(X13,skolem0003(X13))|p14(X13)))&(~r1(skolem0001,X13)|(~p26(skolem0003(X13))|p14(X13)))))&((~r1(skolem0001,X15)|(r1(X15,skolem0004(X15))|p16(X15)))&(~r1(skolem0001,X15)|(~p24(skolem0004(X15))|p16(X15)))))&((~r1(skolem0001,X17)|(r1(X17,skolem0005(X17))|p14(X17)))&(~r1(skolem0001,X17)|(~p24(skolem0005(X17))|p14(X17)))))&((~r1(skolem0001,X19)|(r1(X19,skolem0006(X19))|p16(X19)))&(~r1(skolem0001,X19)|(~p22(skolem0006(X19))|p16(X19)))))&((~r1(skolem0001,X21)|(r1(X21,skolem0007(X21))|p14(X21)))&(~r1(skolem0001,X21)|(~p22(skolem0007(X21))|p14(X21)))))&((~r1(skolem0001,X23)|(r1(X23,skolem0008(X23))|p15(X23)))&(~r1(skolem0001,X23)|(~p23(skolem0008(X23))|p15(X23)))))&((~r1(skolem0001,X25)|(r1(X25,skolem0009(X25))|p15(X25)))&(~r1(skolem0001,X25)|(~p21(skolem0009(X25))|p15(X25)))))&((~r1(skolem0001,X27)|(r1(X27,skolem0010(X27))|p13(X27)))&(~r1(skolem0001,X27)|(~p23(skolem0010(X27))|p13(X27)))))&((~r1(skolem0001,X29)|(r1(X29,skolem0011(X29))|p13(X29)))&(~r1(skolem0001,X29)|(~p21(skolem0011(X29))|p13(X29)))))&((~r1(skolem0001,X31)|(r1(X31,skolem0012(X31))|p11(X31)))&(~r1(skolem0001,X31)|(~p23(skolem0012(X31))|p11(X31)))))&((~r1(skolem0001,X33)|(r1(X33,skolem0013(X33))|p11(X33)))&(~r1(skolem0001,X33)|(~p21(skolem0013(X33))|p11(X33)))))&(r1(skolem0001,skolem0014)&~p15(skolem0014)))&(r1(skolem0001,skolem0015)&~p13(skolem0015)))&(r1(skolem0001,skolem0016)&~p12(skolem0016)))&(r1(skolem0001,skolem0017)&~p11(skolem0017))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 1.66/1.92 cnf(c33,negated_conjecture,~r1(skolem0001,X75)|r1(X75,skolem0013(X75))|p11(X75),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c397,plain,r1(skolem0001,skolem0013(skolem0001))|p11(skolem0001),inference(resolution,[status(thm)],[c33, c44])).
% 1.66/1.92 cnf(c10,negated_conjecture,~r1(skolem0001,X49)|~r1(X49,X50)|p22(X50),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c523,plain,p11(skolem0001)|r1(skolem0013(skolem0001),skolem0013(skolem0013(skolem0001)))|p11(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c33])).
% 1.66/1.92 cnf(c945,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p22(skolem0013(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c523, c10])).
% 1.66/1.92 cnf(c1153,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|p22(skolem0013(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c945, c397])).
% 1.66/1.92 cnf(c7,negated_conjecture,~r1(skolem0001,X41)|~r1(X41,X42)|p26(X42),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c944,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p26(skolem0013(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c523, c7])).
% 1.66/1.92 cnf(c1152,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|p26(skolem0013(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c944, c397])).
% 1.66/1.92 cnf(c9,negated_conjecture,~r1(skolem0001,X46)|~r1(X46,X47)|p24(X47),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c943,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p24(skolem0013(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c523, c9])).
% 1.66/1.92 cnf(c1151,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|p24(skolem0013(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c943, c397])).
% 1.66/1.92 cnf(c8,negated_conjecture,~r1(skolem0001,X44)|~r1(X44,X45)|p25(X45),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c942,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p25(skolem0013(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c523, c8])).
% 1.66/1.92 cnf(c1150,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|p25(skolem0013(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c942, c397])).
% 1.66/1.92 cnf(c29,negated_conjecture,~r1(skolem0001,X71)|r1(X71,skolem0011(X71))|p13(X71),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c518,plain,p11(skolem0001)|r1(skolem0013(skolem0001),skolem0011(skolem0013(skolem0001)))|p13(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c29])).
% 1.66/1.92 cnf(c929,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p22(skolem0011(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c518, c10])).
% 1.66/1.92 cnf(c1149,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|p22(skolem0011(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c929, c397])).
% 1.66/1.92 cnf(c928,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p26(skolem0011(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c518, c7])).
% 1.66/1.92 cnf(c1148,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|p26(skolem0011(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c928, c397])).
% 1.66/1.92 cnf(c927,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p24(skolem0011(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c518, c9])).
% 1.66/1.92 cnf(c1147,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|p24(skolem0011(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c927, c397])).
% 1.66/1.92 cnf(c926,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p25(skolem0011(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c518, c8])).
% 1.66/1.92 cnf(c1146,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|p25(skolem0011(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c926, c397])).
% 1.66/1.92 cnf(c27,negated_conjecture,~r1(skolem0001,X69)|r1(X69,skolem0010(X69))|p13(X69),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c517,plain,p11(skolem0001)|r1(skolem0013(skolem0001),skolem0010(skolem0013(skolem0001)))|p13(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c27])).
% 1.66/1.92 cnf(c925,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p22(skolem0010(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c517, c10])).
% 1.66/1.92 cnf(c1145,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|p22(skolem0010(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c925, c397])).
% 1.66/1.92 cnf(c924,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p26(skolem0010(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c517, c7])).
% 1.66/1.92 cnf(c1144,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|p26(skolem0010(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c924, c397])).
% 1.66/1.92 cnf(c923,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p24(skolem0010(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c517, c9])).
% 1.66/1.92 cnf(c1143,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|p24(skolem0010(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c923, c397])).
% 1.66/1.92 cnf(c922,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p25(skolem0010(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c517, c8])).
% 1.66/1.92 cnf(c1142,plain,p11(skolem0001)|p13(skolem0013(skolem0001))|p25(skolem0010(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c922, c397])).
% 1.66/1.92 cnf(c25,negated_conjecture,~r1(skolem0001,X67)|r1(X67,skolem0009(X67))|p15(X67),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c512,plain,p11(skolem0001)|r1(skolem0013(skolem0001),skolem0009(skolem0013(skolem0001)))|p15(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c25])).
% 1.66/1.92 cnf(c917,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p22(skolem0009(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c512, c10])).
% 1.66/1.92 cnf(c1141,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|p22(skolem0009(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c917, c397])).
% 1.66/1.92 cnf(c916,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p26(skolem0009(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c512, c7])).
% 1.66/1.92 cnf(c1140,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|p26(skolem0009(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c916, c397])).
% 1.66/1.92 cnf(c915,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p24(skolem0009(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c512, c9])).
% 1.66/1.92 cnf(c1139,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|p24(skolem0009(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c915, c397])).
% 1.66/1.92 cnf(c914,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p25(skolem0009(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c512, c8])).
% 1.66/1.92 cnf(c1138,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|p25(skolem0009(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c914, c397])).
% 1.66/1.92 cnf(c16,negated_conjecture,~r1(skolem0001,X58)|~p24(skolem0004(X58))|p16(X58),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c15,negated_conjecture,~r1(skolem0001,X57)|r1(X57,skolem0004(X57))|p16(X57),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c511,plain,p11(skolem0001)|r1(skolem0013(skolem0001),skolem0004(skolem0013(skolem0001)))|p16(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c15])).
% 1.66/1.92 cnf(c911,plain,p11(skolem0001)|p16(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p24(skolem0004(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c511, c9])).
% 1.66/1.92 cnf(c1135,plain,p11(skolem0001)|p16(skolem0013(skolem0001))|p24(skolem0004(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c911, c397])).
% 1.66/1.92 cnf(c1136,plain,p11(skolem0001)|p16(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001)),inference(resolution,[status(thm)],[c1135, c16])).
% 1.66/1.92 cnf(c1137,plain,p11(skolem0001)|p16(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c1136, c397])).
% 1.66/1.92 cnf(c22,negated_conjecture,~r1(skolem0001,X64)|~p22(skolem0007(X64))|p14(X64),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c21,negated_conjecture,~r1(skolem0001,X63)|r1(X63,skolem0007(X63))|p14(X63),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c510,plain,p11(skolem0001)|r1(skolem0013(skolem0001),skolem0007(skolem0013(skolem0001)))|p14(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c21])).
% 1.66/1.92 cnf(c909,plain,p11(skolem0001)|p14(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p22(skolem0007(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c510, c10])).
% 1.66/1.92 cnf(c1131,plain,p11(skolem0001)|p14(skolem0013(skolem0001))|p22(skolem0007(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c909, c397])).
% 1.66/1.92 cnf(c1132,plain,p11(skolem0001)|p14(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001)),inference(resolution,[status(thm)],[c1131, c22])).
% 1.66/1.92 cnf(c1133,plain,p11(skolem0001)|p14(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c1132, c397])).
% 1.66/1.92 cnf(c23,negated_conjecture,~r1(skolem0001,X65)|r1(X65,skolem0008(X65))|p15(X65),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c508,plain,p11(skolem0001)|r1(skolem0013(skolem0001),skolem0008(skolem0013(skolem0001)))|p15(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c23])).
% 1.66/1.92 cnf(c905,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p22(skolem0008(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c508, c10])).
% 1.66/1.92 cnf(c1127,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|p22(skolem0008(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c905, c397])).
% 1.66/1.92 cnf(c904,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p26(skolem0008(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c508, c7])).
% 1.66/1.92 cnf(c1126,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|p26(skolem0008(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c904, c397])).
% 1.66/1.92 cnf(c903,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p24(skolem0008(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c508, c9])).
% 1.66/1.92 cnf(c1125,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|p24(skolem0008(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c903, c397])).
% 1.66/1.92 cnf(c902,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p25(skolem0008(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c508, c8])).
% 1.66/1.92 cnf(c1124,plain,p11(skolem0001)|p15(skolem0013(skolem0001))|p25(skolem0008(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c902, c397])).
% 1.66/1.92 cnf(c31,negated_conjecture,~r1(skolem0001,X73)|r1(X73,skolem0012(X73))|p11(X73),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.92 cnf(c506,plain,p11(skolem0001)|r1(skolem0013(skolem0001),skolem0012(skolem0013(skolem0001)))|p11(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c31])).
% 1.66/1.92 cnf(c901,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p22(skolem0012(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c506, c10])).
% 1.66/1.92 cnf(c1123,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|p22(skolem0012(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c901, c397])).
% 1.66/1.92 cnf(c900,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p26(skolem0012(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c506, c7])).
% 1.66/1.92 cnf(c1122,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|p26(skolem0012(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c900, c397])).
% 1.66/1.92 cnf(c899,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p24(skolem0012(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c506, c9])).
% 1.66/1.92 cnf(c1121,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|p24(skolem0012(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c899, c397])).
% 1.66/1.92 cnf(c898,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|~r1(skolem0001,skolem0013(skolem0001))|p25(skolem0012(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c506, c8])).
% 1.66/1.92 cnf(c1120,plain,p11(skolem0001)|p11(skolem0013(skolem0001))|p25(skolem0012(skolem0013(skolem0001))),inference(resolution,[status(thm)],[c898, c397])).
% 1.66/1.92 cnf(c371,plain,r1(skolem0001,skolem0012(skolem0001))|p11(skolem0001),inference(resolution,[status(thm)],[c31, c44])).
% 1.66/1.92 cnf(c469,plain,p11(skolem0001)|r1(skolem0012(skolem0001),skolem0013(skolem0012(skolem0001)))|p11(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c33])).
% 1.66/1.92 cnf(c897,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p22(skolem0013(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c469, c10])).
% 1.66/1.92 cnf(c1119,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|p22(skolem0013(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c897, c371])).
% 1.66/1.92 cnf(c896,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p26(skolem0013(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c469, c7])).
% 1.66/1.92 cnf(c1118,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|p26(skolem0013(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c896, c371])).
% 1.66/1.92 cnf(c895,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p24(skolem0013(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c469, c9])).
% 1.66/1.92 cnf(c1117,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|p24(skolem0013(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c895, c371])).
% 1.66/1.92 cnf(c894,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p25(skolem0013(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c469, c8])).
% 1.66/1.92 cnf(c1116,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|p25(skolem0013(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c894, c371])).
% 1.66/1.92 cnf(c464,plain,p11(skolem0001)|r1(skolem0012(skolem0001),skolem0011(skolem0012(skolem0001)))|p13(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c29])).
% 1.66/1.92 cnf(c881,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p22(skolem0011(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c464, c10])).
% 1.66/1.92 cnf(c1115,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|p22(skolem0011(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c881, c371])).
% 1.66/1.92 cnf(c880,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p26(skolem0011(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c464, c7])).
% 1.66/1.92 cnf(c1114,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|p26(skolem0011(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c880, c371])).
% 1.66/1.92 cnf(c879,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p24(skolem0011(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c464, c9])).
% 1.66/1.92 cnf(c1113,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|p24(skolem0011(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c879, c371])).
% 1.66/1.92 cnf(c878,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p25(skolem0011(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c464, c8])).
% 1.66/1.92 cnf(c1112,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|p25(skolem0011(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c878, c371])).
% 1.66/1.92 cnf(c463,plain,p11(skolem0001)|r1(skolem0012(skolem0001),skolem0010(skolem0012(skolem0001)))|p13(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c27])).
% 1.66/1.92 cnf(c877,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p22(skolem0010(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c463, c10])).
% 1.66/1.92 cnf(c1111,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|p22(skolem0010(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c877, c371])).
% 1.66/1.92 cnf(c876,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p26(skolem0010(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c463, c7])).
% 1.66/1.92 cnf(c1110,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|p26(skolem0010(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c876, c371])).
% 1.66/1.92 cnf(c875,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p24(skolem0010(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c463, c9])).
% 1.66/1.92 cnf(c1109,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|p24(skolem0010(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c875, c371])).
% 1.66/1.92 cnf(c874,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p25(skolem0010(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c463, c8])).
% 1.66/1.92 cnf(c1108,plain,p11(skolem0001)|p13(skolem0012(skolem0001))|p25(skolem0010(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c874, c371])).
% 1.66/1.92 cnf(c458,plain,p11(skolem0001)|r1(skolem0012(skolem0001),skolem0009(skolem0012(skolem0001)))|p15(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c25])).
% 1.66/1.92 cnf(c869,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p22(skolem0009(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c458, c10])).
% 1.66/1.92 cnf(c1107,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|p22(skolem0009(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c869, c371])).
% 1.66/1.92 cnf(c868,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p26(skolem0009(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c458, c7])).
% 1.66/1.92 cnf(c1106,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|p26(skolem0009(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c868, c371])).
% 1.66/1.92 cnf(c867,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p24(skolem0009(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c458, c9])).
% 1.66/1.92 cnf(c1105,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|p24(skolem0009(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c867, c371])).
% 1.66/1.92 cnf(c866,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p25(skolem0009(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c458, c8])).
% 1.66/1.92 cnf(c1104,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|p25(skolem0009(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c866, c371])).
% 1.66/1.92 cnf(c457,plain,p11(skolem0001)|r1(skolem0012(skolem0001),skolem0004(skolem0012(skolem0001)))|p16(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c15])).
% 1.66/1.92 cnf(c863,plain,p11(skolem0001)|p16(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p24(skolem0004(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c457, c9])).
% 1.66/1.92 cnf(c1101,plain,p11(skolem0001)|p16(skolem0012(skolem0001))|p24(skolem0004(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c863, c371])).
% 1.66/1.92 cnf(c1102,plain,p11(skolem0001)|p16(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001)),inference(resolution,[status(thm)],[c1101, c16])).
% 1.66/1.92 cnf(c1103,plain,p11(skolem0001)|p16(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c1102, c371])).
% 1.66/1.92 cnf(c456,plain,p11(skolem0001)|r1(skolem0012(skolem0001),skolem0007(skolem0012(skolem0001)))|p14(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c21])).
% 1.66/1.92 cnf(c861,plain,p11(skolem0001)|p14(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p22(skolem0007(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c456, c10])).
% 1.66/1.92 cnf(c1097,plain,p11(skolem0001)|p14(skolem0012(skolem0001))|p22(skolem0007(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c861, c371])).
% 1.66/1.92 cnf(c1098,plain,p11(skolem0001)|p14(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001)),inference(resolution,[status(thm)],[c1097, c22])).
% 1.66/1.92 cnf(c1099,plain,p11(skolem0001)|p14(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c1098, c371])).
% 1.66/1.92 cnf(c454,plain,p11(skolem0001)|r1(skolem0012(skolem0001),skolem0008(skolem0012(skolem0001)))|p15(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c23])).
% 1.66/1.92 cnf(c857,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p22(skolem0008(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c454, c10])).
% 1.66/1.92 cnf(c1093,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|p22(skolem0008(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c857, c371])).
% 1.66/1.92 cnf(c856,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p26(skolem0008(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c454, c7])).
% 1.66/1.92 cnf(c1092,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|p26(skolem0008(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c856, c371])).
% 1.66/1.92 cnf(c855,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p24(skolem0008(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c454, c9])).
% 1.66/1.92 cnf(c1091,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|p24(skolem0008(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c855, c371])).
% 1.66/1.92 cnf(c854,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p25(skolem0008(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c454, c8])).
% 1.66/1.92 cnf(c1090,plain,p11(skolem0001)|p15(skolem0012(skolem0001))|p25(skolem0008(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c854, c371])).
% 1.66/1.92 cnf(c452,plain,p11(skolem0001)|r1(skolem0012(skolem0001),skolem0012(skolem0012(skolem0001)))|p11(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c31])).
% 1.66/1.92 cnf(c853,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p22(skolem0012(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c452, c10])).
% 1.66/1.92 cnf(c1089,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|p22(skolem0012(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c853, c371])).
% 1.66/1.92 cnf(c852,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p26(skolem0012(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c452, c7])).
% 1.66/1.92 cnf(c1088,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|p26(skolem0012(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c852, c371])).
% 1.66/1.92 cnf(c851,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p24(skolem0012(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c452, c9])).
% 1.66/1.92 cnf(c1087,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|p24(skolem0012(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c851, c371])).
% 1.66/1.92 cnf(c850,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|~r1(skolem0001,skolem0012(skolem0001))|p25(skolem0012(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c452, c8])).
% 1.66/1.92 cnf(c1086,plain,p11(skolem0001)|p11(skolem0012(skolem0001))|p25(skolem0012(skolem0012(skolem0001))),inference(resolution,[status(thm)],[c850, c371])).
% 1.66/1.92 cnf(c338,plain,r1(skolem0001,skolem0011(skolem0001))|p13(skolem0001),inference(resolution,[status(thm)],[c29, c44])).
% 1.66/1.92 cnf(c426,plain,p13(skolem0001)|r1(skolem0011(skolem0001),skolem0013(skolem0011(skolem0001)))|p11(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c33])).
% 1.66/1.92 cnf(c849,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p22(skolem0013(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c426, c10])).
% 1.66/1.92 cnf(c1085,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|p22(skolem0013(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c849, c338])).
% 1.66/1.92 cnf(c848,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p26(skolem0013(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c426, c7])).
% 1.66/1.92 cnf(c1084,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|p26(skolem0013(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c848, c338])).
% 1.66/1.92 cnf(c847,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p24(skolem0013(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c426, c9])).
% 1.66/1.92 cnf(c1083,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|p24(skolem0013(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c847, c338])).
% 1.66/1.92 cnf(c846,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p25(skolem0013(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c426, c8])).
% 1.66/1.92 cnf(c1082,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|p25(skolem0013(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c846, c338])).
% 1.66/1.92 cnf(c421,plain,p13(skolem0001)|r1(skolem0011(skolem0001),skolem0011(skolem0011(skolem0001)))|p13(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c29])).
% 1.66/1.92 cnf(c833,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p22(skolem0011(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c421, c10])).
% 1.66/1.92 cnf(c1081,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|p22(skolem0011(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c833, c338])).
% 1.66/1.92 cnf(c832,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p26(skolem0011(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c421, c7])).
% 1.66/1.92 cnf(c1080,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|p26(skolem0011(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c832, c338])).
% 1.66/1.92 cnf(c831,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p24(skolem0011(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c421, c9])).
% 1.66/1.92 cnf(c1079,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|p24(skolem0011(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c831, c338])).
% 1.66/1.92 cnf(c830,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p25(skolem0011(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c421, c8])).
% 1.66/1.92 cnf(c1078,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|p25(skolem0011(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c830, c338])).
% 1.66/1.92 cnf(c420,plain,p13(skolem0001)|r1(skolem0011(skolem0001),skolem0010(skolem0011(skolem0001)))|p13(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c27])).
% 1.66/1.92 cnf(c829,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p22(skolem0010(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c420, c10])).
% 1.66/1.92 cnf(c1077,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|p22(skolem0010(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c829, c338])).
% 1.66/1.92 cnf(c828,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p26(skolem0010(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c420, c7])).
% 1.66/1.92 cnf(c1076,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|p26(skolem0010(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c828, c338])).
% 1.66/1.92 cnf(c827,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p24(skolem0010(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c420, c9])).
% 1.66/1.92 cnf(c1075,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|p24(skolem0010(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c827, c338])).
% 1.66/1.92 cnf(c826,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p25(skolem0010(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c420, c8])).
% 1.66/1.92 cnf(c1074,plain,p13(skolem0001)|p13(skolem0011(skolem0001))|p25(skolem0010(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c826, c338])).
% 1.66/1.92 cnf(c415,plain,p13(skolem0001)|r1(skolem0011(skolem0001),skolem0009(skolem0011(skolem0001)))|p15(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c25])).
% 1.66/1.92 cnf(c821,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p22(skolem0009(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c415, c10])).
% 1.66/1.92 cnf(c1073,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|p22(skolem0009(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c821, c338])).
% 1.66/1.92 cnf(c820,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p26(skolem0009(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c415, c7])).
% 1.66/1.92 cnf(c1072,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|p26(skolem0009(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c820, c338])).
% 1.66/1.92 cnf(c819,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p24(skolem0009(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c415, c9])).
% 1.66/1.92 cnf(c1071,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|p24(skolem0009(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c819, c338])).
% 1.66/1.92 cnf(c818,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p25(skolem0009(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c415, c8])).
% 1.66/1.92 cnf(c1070,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|p25(skolem0009(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c818, c338])).
% 1.66/1.92 cnf(c414,plain,p13(skolem0001)|r1(skolem0011(skolem0001),skolem0004(skolem0011(skolem0001)))|p16(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c15])).
% 1.66/1.92 cnf(c815,plain,p13(skolem0001)|p16(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p24(skolem0004(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c414, c9])).
% 1.66/1.92 cnf(c1066,plain,p13(skolem0001)|p16(skolem0011(skolem0001))|p24(skolem0004(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c815, c338])).
% 1.66/1.92 cnf(c1067,plain,p13(skolem0001)|p16(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001)),inference(resolution,[status(thm)],[c1066, c16])).
% 1.66/1.92 cnf(c1069,plain,p13(skolem0001)|p16(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c1067, c338])).
% 1.66/1.92 cnf(c413,plain,p13(skolem0001)|r1(skolem0011(skolem0001),skolem0007(skolem0011(skolem0001)))|p14(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c21])).
% 1.66/1.92 cnf(c813,plain,p13(skolem0001)|p14(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p22(skolem0007(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c413, c10])).
% 1.66/1.92 cnf(c1062,plain,p13(skolem0001)|p14(skolem0011(skolem0001))|p22(skolem0007(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c813, c338])).
% 1.66/1.92 cnf(c1063,plain,p13(skolem0001)|p14(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001)),inference(resolution,[status(thm)],[c1062, c22])).
% 1.66/1.92 cnf(c1065,plain,p13(skolem0001)|p14(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c1063, c338])).
% 1.66/1.92 cnf(c411,plain,p13(skolem0001)|r1(skolem0011(skolem0001),skolem0008(skolem0011(skolem0001)))|p15(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c23])).
% 1.66/1.92 cnf(c809,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p22(skolem0008(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c411, c10])).
% 1.66/1.92 cnf(c1058,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|p22(skolem0008(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c809, c338])).
% 1.66/1.92 cnf(c808,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p26(skolem0008(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c411, c7])).
% 1.66/1.92 cnf(c1057,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|p26(skolem0008(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c808, c338])).
% 1.66/1.92 cnf(c807,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p24(skolem0008(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c411, c9])).
% 1.66/1.92 cnf(c1056,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|p24(skolem0008(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c807, c338])).
% 1.66/1.92 cnf(c806,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p25(skolem0008(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c411, c8])).
% 1.66/1.92 cnf(c1055,plain,p13(skolem0001)|p15(skolem0011(skolem0001))|p25(skolem0008(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c806, c338])).
% 1.66/1.92 cnf(c409,plain,p13(skolem0001)|r1(skolem0011(skolem0001),skolem0012(skolem0011(skolem0001)))|p11(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c31])).
% 1.66/1.92 cnf(c804,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p22(skolem0012(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c409, c10])).
% 1.66/1.92 cnf(c1054,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|p22(skolem0012(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c804, c338])).
% 1.66/1.92 cnf(c803,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p26(skolem0012(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c409, c7])).
% 1.66/1.92 cnf(c1053,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|p26(skolem0012(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c803, c338])).
% 1.66/1.92 cnf(c802,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p24(skolem0012(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c409, c9])).
% 1.66/1.92 cnf(c1052,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|p24(skolem0012(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c802, c338])).
% 1.66/1.92 cnf(c801,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|~r1(skolem0001,skolem0011(skolem0001))|p25(skolem0012(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c409, c8])).
% 1.66/1.92 cnf(c1051,plain,p13(skolem0001)|p11(skolem0011(skolem0001))|p25(skolem0012(skolem0011(skolem0001))),inference(resolution,[status(thm)],[c801, c338])).
% 1.66/1.92 cnf(c293,plain,r1(skolem0001,skolem0010(skolem0001))|p13(skolem0001),inference(resolution,[status(thm)],[c27, c44])).
% 1.66/1.92 cnf(c400,plain,r1(skolem0010(skolem0001),skolem0013(skolem0010(skolem0001)))|p11(skolem0010(skolem0001))|p13(skolem0001),inference(resolution,[status(thm)],[c33, c293])).
% 1.66/1.92 cnf(c797,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|~r1(skolem0001,skolem0010(skolem0001))|p22(skolem0013(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c400, c10])).
% 1.66/1.92 cnf(c1050,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|p22(skolem0013(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c797, c293])).
% 1.66/1.92 cnf(c796,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|~r1(skolem0001,skolem0010(skolem0001))|p26(skolem0013(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c400, c7])).
% 1.66/1.92 cnf(c1049,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|p26(skolem0013(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c796, c293])).
% 1.66/1.92 cnf(c795,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|~r1(skolem0001,skolem0010(skolem0001))|p24(skolem0013(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c400, c9])).
% 1.66/1.93 cnf(c1048,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|p24(skolem0013(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c795, c293])).
% 1.66/1.93 cnf(c794,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|~r1(skolem0001,skolem0010(skolem0001))|p25(skolem0013(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c400, c8])).
% 1.66/1.93 cnf(c1047,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|p25(skolem0013(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c794, c293])).
% 1.66/1.93 cnf(c250,plain,r1(skolem0001,skolem0009(skolem0001))|p15(skolem0001),inference(resolution,[status(thm)],[c25, c44])).
% 1.66/1.93 cnf(c396,plain,r1(skolem0009(skolem0001),skolem0013(skolem0009(skolem0001)))|p11(skolem0009(skolem0001))|p15(skolem0001),inference(resolution,[status(thm)],[c33, c250])).
% 1.66/1.93 cnf(c791,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p22(skolem0013(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c396, c10])).
% 1.66/1.93 cnf(c1046,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|p22(skolem0013(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c791, c250])).
% 1.66/1.93 cnf(c790,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p26(skolem0013(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c396, c7])).
% 1.66/1.93 cnf(c1045,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|p26(skolem0013(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c790, c250])).
% 1.66/1.93 cnf(c789,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p24(skolem0013(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c396, c9])).
% 1.66/1.93 cnf(c1044,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|p24(skolem0013(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c789, c250])).
% 1.66/1.93 cnf(c788,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p25(skolem0013(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c396, c8])).
% 1.66/1.93 cnf(c1043,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|p25(skolem0013(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c788, c250])).
% 1.66/1.93 cnf(c213,plain,r1(skolem0001,skolem0008(skolem0001))|p15(skolem0001),inference(resolution,[status(thm)],[c23, c44])).
% 1.66/1.93 cnf(c395,plain,r1(skolem0008(skolem0001),skolem0013(skolem0008(skolem0001)))|p11(skolem0008(skolem0001))|p15(skolem0001),inference(resolution,[status(thm)],[c33, c213])).
% 1.66/1.93 cnf(c785,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p22(skolem0013(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c395, c10])).
% 1.66/1.93 cnf(c1042,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|p22(skolem0013(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c785, c213])).
% 1.66/1.93 cnf(c784,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p26(skolem0013(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c395, c7])).
% 1.66/1.93 cnf(c1041,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|p26(skolem0013(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c784, c213])).
% 1.66/1.93 cnf(c783,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p24(skolem0013(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c395, c9])).
% 1.66/1.93 cnf(c1040,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|p24(skolem0013(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c783, c213])).
% 1.66/1.93 cnf(c782,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p25(skolem0013(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c395, c8])).
% 1.66/1.93 cnf(c1039,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|p25(skolem0013(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c782, c213])).
% 1.66/1.93 cnf(c374,plain,r1(skolem0010(skolem0001),skolem0012(skolem0010(skolem0001)))|p11(skolem0010(skolem0001))|p13(skolem0001),inference(resolution,[status(thm)],[c31, c293])).
% 1.66/1.93 cnf(c781,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|~r1(skolem0001,skolem0010(skolem0001))|p22(skolem0012(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c374, c10])).
% 1.66/1.93 cnf(c1038,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|p22(skolem0012(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c781, c293])).
% 1.66/1.93 cnf(c780,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|~r1(skolem0001,skolem0010(skolem0001))|p26(skolem0012(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c374, c7])).
% 1.66/1.93 cnf(c1037,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|p26(skolem0012(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c780, c293])).
% 1.66/1.93 cnf(c779,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|~r1(skolem0001,skolem0010(skolem0001))|p24(skolem0012(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c374, c9])).
% 1.66/1.93 cnf(c1036,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|p24(skolem0012(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c779, c293])).
% 1.66/1.93 cnf(c778,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|~r1(skolem0001,skolem0010(skolem0001))|p25(skolem0012(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c374, c8])).
% 1.66/1.93 cnf(c1035,plain,p11(skolem0010(skolem0001))|p13(skolem0001)|p25(skolem0012(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c778, c293])).
% 1.66/1.93 cnf(c370,plain,r1(skolem0009(skolem0001),skolem0012(skolem0009(skolem0001)))|p11(skolem0009(skolem0001))|p15(skolem0001),inference(resolution,[status(thm)],[c31, c250])).
% 1.66/1.93 cnf(c775,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p22(skolem0012(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c370, c10])).
% 1.66/1.93 cnf(c1034,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|p22(skolem0012(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c775, c250])).
% 1.66/1.93 cnf(c774,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p26(skolem0012(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c370, c7])).
% 1.66/1.93 cnf(c1033,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|p26(skolem0012(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c774, c250])).
% 1.66/1.93 cnf(c773,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p24(skolem0012(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c370, c9])).
% 1.66/1.93 cnf(c1032,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|p24(skolem0012(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c773, c250])).
% 1.66/1.93 cnf(c772,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p25(skolem0012(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c370, c8])).
% 1.66/1.93 cnf(c1031,plain,p11(skolem0009(skolem0001))|p15(skolem0001)|p25(skolem0012(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c772, c250])).
% 1.66/1.93 cnf(c369,plain,r1(skolem0008(skolem0001),skolem0012(skolem0008(skolem0001)))|p11(skolem0008(skolem0001))|p15(skolem0001),inference(resolution,[status(thm)],[c31, c213])).
% 1.66/1.93 cnf(c769,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p22(skolem0012(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c369, c10])).
% 1.66/1.93 cnf(c1030,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|p22(skolem0012(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c769, c213])).
% 1.66/1.93 cnf(c768,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p26(skolem0012(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c369, c7])).
% 1.66/1.93 cnf(c1029,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|p26(skolem0012(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c768, c213])).
% 1.66/1.93 cnf(c767,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p24(skolem0012(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c369, c9])).
% 1.66/1.93 cnf(c1028,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|p24(skolem0012(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c767, c213])).
% 1.66/1.93 cnf(c766,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p25(skolem0012(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c369, c8])).
% 1.66/1.93 cnf(c1027,plain,p11(skolem0008(skolem0001))|p15(skolem0001)|p25(skolem0012(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c766, c213])).
% 1.66/1.93 cnf(c361,plain,p13(skolem0001)|r1(skolem0010(skolem0001),skolem0011(skolem0010(skolem0001)))|p13(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c293, c29])).
% 1.66/1.93 cnf(c745,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p22(skolem0011(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c361, c10])).
% 1.66/1.93 cnf(c1026,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|p22(skolem0011(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c745, c293])).
% 1.66/1.93 cnf(c744,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p26(skolem0011(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c361, c7])).
% 1.66/1.93 cnf(c1025,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|p26(skolem0011(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c744, c293])).
% 1.66/1.93 cnf(c743,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p24(skolem0011(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c361, c9])).
% 1.66/1.93 cnf(c1024,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|p24(skolem0011(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c743, c293])).
% 1.66/1.93 cnf(c742,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p25(skolem0011(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c361, c8])).
% 1.66/1.93 cnf(c1023,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|p25(skolem0011(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c742, c293])).
% 1.66/1.93 cnf(c360,plain,p13(skolem0001)|r1(skolem0010(skolem0001),skolem0010(skolem0010(skolem0001)))|p13(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c293, c27])).
% 1.66/1.93 cnf(c740,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p22(skolem0010(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c360, c10])).
% 1.66/1.93 cnf(c1022,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|p22(skolem0010(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c740, c293])).
% 1.66/1.93 cnf(c739,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p26(skolem0010(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c360, c7])).
% 1.66/1.93 cnf(c1021,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|p26(skolem0010(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c739, c293])).
% 1.66/1.93 cnf(c738,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p24(skolem0010(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c360, c9])).
% 1.66/1.93 cnf(c1020,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|p24(skolem0010(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c738, c293])).
% 1.66/1.93 cnf(c737,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p25(skolem0010(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c360, c8])).
% 1.66/1.93 cnf(c1019,plain,p13(skolem0001)|p13(skolem0010(skolem0001))|p25(skolem0010(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c737, c293])).
% 1.66/1.93 cnf(c355,plain,p13(skolem0001)|r1(skolem0010(skolem0001),skolem0009(skolem0010(skolem0001)))|p15(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c293, c25])).
% 1.66/1.93 cnf(c727,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p22(skolem0009(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c355, c10])).
% 1.66/1.93 cnf(c1018,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|p22(skolem0009(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c727, c293])).
% 1.66/1.93 cnf(c726,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p26(skolem0009(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c355, c7])).
% 1.66/1.93 cnf(c1017,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|p26(skolem0009(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c726, c293])).
% 1.66/1.93 cnf(c725,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p24(skolem0009(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c355, c9])).
% 1.66/1.93 cnf(c1016,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|p24(skolem0009(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c725, c293])).
% 1.66/1.93 cnf(c724,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p25(skolem0009(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c355, c8])).
% 1.66/1.93 cnf(c1015,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|p25(skolem0009(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c724, c293])).
% 1.66/1.93 cnf(c354,plain,p13(skolem0001)|r1(skolem0010(skolem0001),skolem0004(skolem0010(skolem0001)))|p16(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c293, c15])).
% 1.66/1.93 cnf(c719,plain,p13(skolem0001)|p16(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p24(skolem0004(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c354, c9])).
% 1.66/1.93 cnf(c1012,plain,p13(skolem0001)|p16(skolem0010(skolem0001))|p24(skolem0004(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c719, c293])).
% 1.66/1.93 cnf(c1013,plain,p13(skolem0001)|p16(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001)),inference(resolution,[status(thm)],[c1012, c16])).
% 1.66/1.93 cnf(c1014,plain,p13(skolem0001)|p16(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c1013, c293])).
% 1.66/1.93 cnf(c353,plain,p13(skolem0001)|r1(skolem0010(skolem0001),skolem0007(skolem0010(skolem0001)))|p14(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c293, c21])).
% 1.66/1.93 cnf(c716,plain,p13(skolem0001)|p14(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p22(skolem0007(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c353, c10])).
% 1.66/1.93 cnf(c1008,plain,p13(skolem0001)|p14(skolem0010(skolem0001))|p22(skolem0007(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c716, c293])).
% 1.66/1.93 cnf(c1009,plain,p13(skolem0001)|p14(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001)),inference(resolution,[status(thm)],[c1008, c22])).
% 1.66/1.93 cnf(c1010,plain,p13(skolem0001)|p14(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c1009, c293])).
% 1.66/1.93 cnf(c351,plain,p13(skolem0001)|r1(skolem0010(skolem0001),skolem0008(skolem0010(skolem0001)))|p15(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c293, c23])).
% 1.66/1.93 cnf(c710,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p22(skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c351, c10])).
% 1.66/1.93 cnf(c1004,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|p22(skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c710, c293])).
% 1.66/1.93 cnf(c709,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p26(skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c351, c7])).
% 1.66/1.93 cnf(c1003,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|p26(skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c709, c293])).
% 1.66/1.93 cnf(c708,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p24(skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c351, c9])).
% 1.66/1.93 cnf(c1002,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|p24(skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c708, c293])).
% 1.66/1.93 cnf(c707,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|~r1(skolem0001,skolem0010(skolem0001))|p25(skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c351, c8])).
% 1.66/1.93 cnf(c1001,plain,p13(skolem0001)|p15(skolem0010(skolem0001))|p25(skolem0008(skolem0010(skolem0001))),inference(resolution,[status(thm)],[c707, c293])).
% 1.66/1.93 cnf(c337,plain,r1(skolem0009(skolem0001),skolem0011(skolem0009(skolem0001)))|p13(skolem0009(skolem0001))|p15(skolem0001),inference(resolution,[status(thm)],[c29, c250])).
% 1.66/1.93 cnf(c705,plain,p13(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p22(skolem0011(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c337, c10])).
% 1.66/1.93 cnf(c1000,plain,p13(skolem0009(skolem0001))|p15(skolem0001)|p22(skolem0011(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c705, c250])).
% 1.66/1.93 cnf(c704,plain,p13(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p26(skolem0011(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c337, c7])).
% 1.66/1.93 cnf(c999,plain,p13(skolem0009(skolem0001))|p15(skolem0001)|p26(skolem0011(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c704, c250])).
% 1.66/1.93 cnf(c703,plain,p13(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p24(skolem0011(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c337, c9])).
% 1.66/1.93 cnf(c998,plain,p13(skolem0009(skolem0001))|p15(skolem0001)|p24(skolem0011(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c703, c250])).
% 1.66/1.93 cnf(c702,plain,p13(skolem0009(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0009(skolem0001))|p25(skolem0011(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c337, c8])).
% 1.66/1.93 cnf(c997,plain,p13(skolem0009(skolem0001))|p15(skolem0001)|p25(skolem0011(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c702, c250])).
% 1.66/1.93 cnf(c336,plain,r1(skolem0008(skolem0001),skolem0011(skolem0008(skolem0001)))|p13(skolem0008(skolem0001))|p15(skolem0001),inference(resolution,[status(thm)],[c29, c213])).
% 1.66/1.93 cnf(c699,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p22(skolem0011(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c336, c10])).
% 1.66/1.93 cnf(c996,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|p22(skolem0011(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c699, c213])).
% 1.66/1.93 cnf(c698,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p26(skolem0011(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c336, c7])).
% 1.66/1.93 cnf(c995,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|p26(skolem0011(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c698, c213])).
% 1.66/1.93 cnf(c697,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p24(skolem0011(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c336, c9])).
% 1.66/1.93 cnf(c994,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|p24(skolem0011(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c697, c213])).
% 1.66/1.93 cnf(c696,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p25(skolem0011(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c336, c8])).
% 1.66/1.93 cnf(c993,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|p25(skolem0011(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c696, c213])).
% 1.66/1.93 cnf(c311,plain,p15(skolem0001)|r1(skolem0009(skolem0001),skolem0007(skolem0009(skolem0001)))|p14(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c250, c21])).
% 1.66/1.93 cnf(c669,plain,p15(skolem0001)|p14(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p22(skolem0007(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c311, c10])).
% 1.66/1.93 cnf(c990,plain,p15(skolem0001)|p14(skolem0009(skolem0001))|p22(skolem0007(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c669, c250])).
% 1.66/1.93 cnf(c991,plain,p15(skolem0001)|p14(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001)),inference(resolution,[status(thm)],[c990, c22])).
% 1.66/1.93 cnf(c992,plain,p15(skolem0001)|p14(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c991, c250])).
% 1.66/1.93 cnf(c12,negated_conjecture,~r1(skolem0001,X54)|~p26(skolem0002(X54))|p16(X54),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.93 cnf(c11,negated_conjecture,~r1(skolem0001,X52)|r1(X52,skolem0002(X52))|p16(X52),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.93 cnf(c307,plain,p15(skolem0001)|r1(skolem0009(skolem0001),skolem0002(skolem0009(skolem0001)))|p16(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c250, c11])).
% 1.66/1.93 cnf(c663,plain,p15(skolem0001)|p16(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p26(skolem0002(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c307, c7])).
% 1.66/1.93 cnf(c984,plain,p15(skolem0001)|p16(skolem0009(skolem0001))|p26(skolem0002(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c663, c250])).
% 1.66/1.93 cnf(c985,plain,p15(skolem0001)|p16(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001)),inference(resolution,[status(thm)],[c984, c12])).
% 1.66/1.93 cnf(c986,plain,p15(skolem0001)|p16(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c985, c250])).
% 1.66/1.93 cnf(c305,plain,p15(skolem0001)|r1(skolem0009(skolem0001),skolem0008(skolem0009(skolem0001)))|p15(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c250, c23])).
% 1.66/1.93 cnf(c657,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p22(skolem0008(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c305, c10])).
% 1.66/1.93 cnf(c981,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|p22(skolem0008(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c657, c250])).
% 1.66/1.93 cnf(c656,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p26(skolem0008(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c305, c7])).
% 1.66/1.93 cnf(c980,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|p26(skolem0008(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c656, c250])).
% 1.66/1.93 cnf(c655,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p24(skolem0008(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c305, c9])).
% 1.66/1.93 cnf(c979,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|p24(skolem0008(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c655, c250])).
% 1.66/1.93 cnf(c654,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p25(skolem0008(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c305, c8])).
% 1.66/1.93 cnf(c978,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|p25(skolem0008(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c654, c250])).
% 1.66/1.93 cnf(c303,plain,p15(skolem0001)|r1(skolem0009(skolem0001),skolem0009(skolem0009(skolem0001)))|p15(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c250, c25])).
% 1.66/1.93 cnf(c653,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p22(skolem0009(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c303, c10])).
% 1.66/1.93 cnf(c977,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|p22(skolem0009(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c653, c250])).
% 1.66/1.93 cnf(c652,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p26(skolem0009(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c303, c7])).
% 1.66/1.93 cnf(c976,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|p26(skolem0009(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c652, c250])).
% 1.66/1.93 cnf(c651,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p24(skolem0009(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c303, c9])).
% 1.66/1.93 cnf(c975,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|p24(skolem0009(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c651, c250])).
% 1.66/1.93 cnf(c650,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p25(skolem0009(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c303, c8])).
% 1.66/1.93 cnf(c974,plain,p15(skolem0001)|p15(skolem0009(skolem0001))|p25(skolem0009(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c650, c250])).
% 1.66/1.93 cnf(c302,plain,p15(skolem0001)|r1(skolem0009(skolem0001),skolem0010(skolem0009(skolem0001)))|p13(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c250, c27])).
% 1.66/1.93 cnf(c646,plain,p15(skolem0001)|p13(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p22(skolem0010(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c302, c10])).
% 1.66/1.93 cnf(c973,plain,p15(skolem0001)|p13(skolem0009(skolem0001))|p22(skolem0010(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c646, c250])).
% 1.66/1.93 cnf(c645,plain,p15(skolem0001)|p13(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p26(skolem0010(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c302, c7])).
% 1.66/1.93 cnf(c972,plain,p15(skolem0001)|p13(skolem0009(skolem0001))|p26(skolem0010(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c645, c250])).
% 1.66/1.93 cnf(c644,plain,p15(skolem0001)|p13(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p24(skolem0010(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c302, c9])).
% 1.66/1.93 cnf(c971,plain,p15(skolem0001)|p13(skolem0009(skolem0001))|p24(skolem0010(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c644, c250])).
% 1.66/1.93 cnf(c643,plain,p15(skolem0001)|p13(skolem0009(skolem0001))|~r1(skolem0001,skolem0009(skolem0001))|p25(skolem0010(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c302, c8])).
% 1.66/1.93 cnf(c970,plain,p15(skolem0001)|p13(skolem0009(skolem0001))|p25(skolem0010(skolem0009(skolem0001))),inference(resolution,[status(thm)],[c643, c250])).
% 1.66/1.93 cnf(c292,plain,r1(skolem0008(skolem0001),skolem0010(skolem0008(skolem0001)))|p13(skolem0008(skolem0001))|p15(skolem0001),inference(resolution,[status(thm)],[c27, c213])).
% 1.66/1.93 cnf(c640,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p22(skolem0010(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c292, c10])).
% 1.66/1.93 cnf(c969,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|p22(skolem0010(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c640, c213])).
% 1.66/1.93 cnf(c639,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p26(skolem0010(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c292, c7])).
% 1.66/1.93 cnf(c968,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|p26(skolem0010(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c639, c213])).
% 1.66/1.93 cnf(c638,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p24(skolem0010(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c292, c9])).
% 1.66/1.93 cnf(c967,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|p24(skolem0010(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c638, c213])).
% 1.66/1.93 cnf(c637,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|~r1(skolem0001,skolem0008(skolem0001))|p25(skolem0010(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c292, c8])).
% 1.66/1.93 cnf(c966,plain,p13(skolem0008(skolem0001))|p15(skolem0001)|p25(skolem0010(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c637, c213])).
% 1.66/1.93 cnf(c267,plain,p15(skolem0001)|r1(skolem0008(skolem0001),skolem0007(skolem0008(skolem0001)))|p14(skolem0008(skolem0001)),inference(resolution,[status(thm)],[c213, c21])).
% 1.66/1.93 cnf(c611,plain,p15(skolem0001)|p14(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001))|p22(skolem0007(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c267, c10])).
% 1.66/1.93 cnf(c963,plain,p15(skolem0001)|p14(skolem0008(skolem0001))|p22(skolem0007(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c611, c213])).
% 1.66/1.93 cnf(c964,plain,p15(skolem0001)|p14(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001)),inference(resolution,[status(thm)],[c963, c22])).
% 1.66/1.93 cnf(c965,plain,p15(skolem0001)|p14(skolem0008(skolem0001)),inference(resolution,[status(thm)],[c964, c213])).
% 1.66/1.93 cnf(c263,plain,p15(skolem0001)|r1(skolem0008(skolem0001),skolem0002(skolem0008(skolem0001)))|p16(skolem0008(skolem0001)),inference(resolution,[status(thm)],[c213, c11])).
% 1.66/1.93 cnf(c604,plain,p15(skolem0001)|p16(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001))|p26(skolem0002(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c263, c7])).
% 1.66/1.93 cnf(c956,plain,p15(skolem0001)|p16(skolem0008(skolem0001))|p26(skolem0002(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c604, c213])).
% 1.66/1.93 cnf(c958,plain,p15(skolem0001)|p16(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001)),inference(resolution,[status(thm)],[c956, c12])).
% 1.66/1.93 cnf(c959,plain,p15(skolem0001)|p16(skolem0008(skolem0001)),inference(resolution,[status(thm)],[c958, c213])).
% 1.66/1.93 cnf(c261,plain,p15(skolem0001)|r1(skolem0008(skolem0001),skolem0008(skolem0008(skolem0001)))|p15(skolem0008(skolem0001)),inference(resolution,[status(thm)],[c213, c23])).
% 1.66/1.93 cnf(c598,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001))|p22(skolem0008(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c261, c10])).
% 1.66/1.93 cnf(c953,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|p22(skolem0008(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c598, c213])).
% 1.66/1.93 cnf(c597,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001))|p26(skolem0008(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c261, c7])).
% 1.66/1.93 cnf(c952,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|p26(skolem0008(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c597, c213])).
% 1.66/1.93 cnf(c596,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001))|p24(skolem0008(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c261, c9])).
% 1.66/1.93 cnf(c951,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|p24(skolem0008(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c596, c213])).
% 1.66/1.93 cnf(c595,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001))|p25(skolem0008(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c261, c8])).
% 1.66/1.93 cnf(c950,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|p25(skolem0008(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c595, c213])).
% 1.66/1.93 cnf(c259,plain,p15(skolem0001)|r1(skolem0008(skolem0001),skolem0009(skolem0008(skolem0001)))|p15(skolem0008(skolem0001)),inference(resolution,[status(thm)],[c213, c25])).
% 1.66/1.93 cnf(c593,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001))|p22(skolem0009(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c259, c10])).
% 1.66/1.93 cnf(c949,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|p22(skolem0009(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c593, c213])).
% 1.66/1.93 cnf(c592,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001))|p26(skolem0009(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c259, c7])).
% 1.66/1.93 cnf(c948,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|p26(skolem0009(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c592, c213])).
% 1.66/1.93 cnf(c591,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001))|p24(skolem0009(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c259, c9])).
% 1.66/1.93 cnf(c947,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|p24(skolem0009(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c591, c213])).
% 1.66/1.93 cnf(c590,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|~r1(skolem0001,skolem0008(skolem0001))|p25(skolem0009(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c259, c8])).
% 1.66/1.93 cnf(c946,plain,p15(skolem0001)|p15(skolem0008(skolem0001))|p25(skolem0009(skolem0008(skolem0001))),inference(resolution,[status(thm)],[c590, c213])).
% 1.66/1.93 cnf(c35,negated_conjecture,r1(skolem0001,skolem0014),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.93 cnf(c401,plain,r1(skolem0014,skolem0013(skolem0014))|p11(skolem0014),inference(resolution,[status(thm)],[c33, c35])).
% 1.66/1.93 cnf(c544,plain,p11(skolem0014)|~r1(skolem0001,skolem0014)|p22(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c401, c10])).
% 1.66/1.93 cnf(c805,plain,p11(skolem0014)|p22(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c544, c35])).
% 1.66/1.93 cnf(c543,plain,p11(skolem0014)|~r1(skolem0001,skolem0014)|p26(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c401, c7])).
% 1.66/1.93 cnf(c800,plain,p11(skolem0014)|p26(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c543, c35])).
% 1.66/1.93 cnf(c542,plain,p11(skolem0014)|~r1(skolem0001,skolem0014)|p24(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c401, c9])).
% 1.66/1.93 cnf(c799,plain,p11(skolem0014)|p24(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c542, c35])).
% 1.66/1.93 cnf(c541,plain,p11(skolem0014)|~r1(skolem0001,skolem0014)|p25(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c401, c8])).
% 1.66/1.93 cnf(c798,plain,p11(skolem0014)|p25(skolem0013(skolem0014)),inference(resolution,[status(thm)],[c541, c35])).
% 1.66/1.93 cnf(c37,negated_conjecture,r1(skolem0001,skolem0015),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.93 cnf(c399,plain,r1(skolem0015,skolem0013(skolem0015))|p11(skolem0015),inference(resolution,[status(thm)],[c33, c37])).
% 1.66/1.93 cnf(c539,plain,p11(skolem0015)|~r1(skolem0001,skolem0015)|p22(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c399, c10])).
% 1.66/1.93 cnf(c793,plain,p11(skolem0015)|p22(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c539, c37])).
% 1.66/1.93 cnf(c538,plain,p11(skolem0015)|~r1(skolem0001,skolem0015)|p26(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c399, c7])).
% 1.66/1.93 cnf(c792,plain,p11(skolem0015)|p26(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c538, c37])).
% 1.66/1.93 cnf(c537,plain,p11(skolem0015)|~r1(skolem0001,skolem0015)|p24(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c399, c9])).
% 1.66/1.93 cnf(c787,plain,p11(skolem0015)|p24(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c537, c37])).
% 1.66/1.93 cnf(c536,plain,p11(skolem0015)|~r1(skolem0001,skolem0015)|p25(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c399, c8])).
% 1.66/1.93 cnf(c786,plain,p11(skolem0015)|p25(skolem0013(skolem0015)),inference(resolution,[status(thm)],[c536, c37])).
% 1.66/1.93 cnf(c39,negated_conjecture,r1(skolem0001,skolem0016),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.93 cnf(c394,plain,r1(skolem0016,skolem0013(skolem0016))|p11(skolem0016),inference(resolution,[status(thm)],[c33, c39])).
% 1.66/1.93 cnf(c505,plain,p11(skolem0016)|~r1(skolem0001,skolem0016)|p22(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c394, c10])).
% 1.66/1.93 cnf(c777,plain,p11(skolem0016)|p22(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c505, c39])).
% 1.66/1.93 cnf(c504,plain,p11(skolem0016)|~r1(skolem0001,skolem0016)|p26(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c394, c7])).
% 1.66/1.93 cnf(c776,plain,p11(skolem0016)|p26(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c504, c39])).
% 1.66/1.93 cnf(c503,plain,p11(skolem0016)|~r1(skolem0001,skolem0016)|p24(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c394, c9])).
% 1.66/1.93 cnf(c771,plain,p11(skolem0016)|p24(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c503, c39])).
% 1.66/1.93 cnf(c502,plain,p11(skolem0016)|~r1(skolem0001,skolem0016)|p25(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c394, c8])).
% 1.66/1.93 cnf(c770,plain,p11(skolem0016)|p25(skolem0013(skolem0016)),inference(resolution,[status(thm)],[c502, c39])).
% 1.66/1.93 cnf(c375,plain,r1(skolem0014,skolem0012(skolem0014))|p11(skolem0014),inference(resolution,[status(thm)],[c31, c35])).
% 1.66/1.93 cnf(c493,plain,p11(skolem0014)|~r1(skolem0001,skolem0014)|p22(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c375, c10])).
% 1.66/1.93 cnf(c765,plain,p11(skolem0014)|p22(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c493, c35])).
% 1.66/1.93 cnf(c492,plain,p11(skolem0014)|~r1(skolem0001,skolem0014)|p26(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c375, c7])).
% 1.66/1.93 cnf(c764,plain,p11(skolem0014)|p26(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c492, c35])).
% 1.66/1.93 cnf(c491,plain,p11(skolem0014)|~r1(skolem0001,skolem0014)|p24(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c375, c9])).
% 1.66/1.93 cnf(c763,plain,p11(skolem0014)|p24(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c491, c35])).
% 1.66/1.93 cnf(c490,plain,p11(skolem0014)|~r1(skolem0001,skolem0014)|p25(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c375, c8])).
% 1.66/1.93 cnf(c758,plain,p11(skolem0014)|p25(skolem0012(skolem0014)),inference(resolution,[status(thm)],[c490, c35])).
% 1.66/1.93 cnf(c373,plain,r1(skolem0015,skolem0012(skolem0015))|p11(skolem0015),inference(resolution,[status(thm)],[c31, c37])).
% 1.66/1.93 cnf(c489,plain,p11(skolem0015)|~r1(skolem0001,skolem0015)|p22(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c373, c10])).
% 1.66/1.93 cnf(c757,plain,p11(skolem0015)|p22(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c489, c37])).
% 1.66/1.93 cnf(c488,plain,p11(skolem0015)|~r1(skolem0001,skolem0015)|p26(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c373, c7])).
% 1.66/1.93 cnf(c752,plain,p11(skolem0015)|p26(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c488, c37])).
% 1.66/1.93 cnf(c487,plain,p11(skolem0015)|~r1(skolem0001,skolem0015)|p24(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c373, c9])).
% 1.66/1.93 cnf(c751,plain,p11(skolem0015)|p24(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c487, c37])).
% 1.66/1.93 cnf(c486,plain,p11(skolem0015)|~r1(skolem0001,skolem0015)|p25(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c373, c8])).
% 1.66/1.93 cnf(c750,plain,p11(skolem0015)|p25(skolem0012(skolem0015)),inference(resolution,[status(thm)],[c486, c37])).
% 1.66/1.93 cnf(c368,plain,r1(skolem0016,skolem0012(skolem0016))|p11(skolem0016),inference(resolution,[status(thm)],[c31, c39])).
% 1.66/1.93 cnf(c451,plain,p11(skolem0016)|~r1(skolem0001,skolem0016)|p22(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c368, c10])).
% 1.66/1.93 cnf(c741,plain,p11(skolem0016)|p22(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c451, c39])).
% 1.66/1.93 cnf(c450,plain,p11(skolem0016)|~r1(skolem0001,skolem0016)|p26(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c368, c7])).
% 1.66/1.93 cnf(c736,plain,p11(skolem0016)|p26(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c450, c39])).
% 1.66/1.93 cnf(c449,plain,p11(skolem0016)|~r1(skolem0001,skolem0016)|p24(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c368, c9])).
% 1.66/1.93 cnf(c735,plain,p11(skolem0016)|p24(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c449, c39])).
% 1.66/1.93 cnf(c448,plain,p11(skolem0016)|~r1(skolem0001,skolem0016)|p25(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c368, c8])).
% 1.66/1.93 cnf(c730,plain,p11(skolem0016)|p25(skolem0012(skolem0016)),inference(resolution,[status(thm)],[c448, c39])).
% 1.66/1.93 cnf(c341,plain,r1(skolem0014,skolem0011(skolem0014))|p13(skolem0014),inference(resolution,[status(thm)],[c29, c35])).
% 1.66/1.93 cnf(c447,plain,p13(skolem0014)|~r1(skolem0001,skolem0014)|p22(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c341, c10])).
% 1.66/1.93 cnf(c729,plain,p13(skolem0014)|p22(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c447, c35])).
% 1.66/1.93 cnf(c446,plain,p13(skolem0014)|~r1(skolem0001,skolem0014)|p26(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c341, c7])).
% 1.66/1.93 cnf(c728,plain,p13(skolem0014)|p26(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c446, c35])).
% 1.66/1.93 cnf(c445,plain,p13(skolem0014)|~r1(skolem0001,skolem0014)|p24(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c341, c9])).
% 1.66/1.93 cnf(c723,plain,p13(skolem0014)|p24(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c445, c35])).
% 1.66/1.93 cnf(c444,plain,p13(skolem0014)|~r1(skolem0001,skolem0014)|p25(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c341, c8])).
% 1.66/1.93 cnf(c722,plain,p13(skolem0014)|p25(skolem0011(skolem0014)),inference(resolution,[status(thm)],[c444, c35])).
% 1.66/1.93 cnf(c41,negated_conjecture,r1(skolem0001,skolem0017),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.93 cnf(c339,plain,r1(skolem0017,skolem0011(skolem0017))|p13(skolem0017),inference(resolution,[status(thm)],[c29, c41])).
% 1.66/1.93 cnf(c433,plain,p13(skolem0017)|~r1(skolem0001,skolem0017)|p22(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c339, c10])).
% 1.66/1.93 cnf(c717,plain,p13(skolem0017)|p22(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c433, c41])).
% 1.66/1.93 cnf(c432,plain,p13(skolem0017)|~r1(skolem0001,skolem0017)|p26(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c339, c7])).
% 1.66/1.93 cnf(c712,plain,p13(skolem0017)|p26(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c432, c41])).
% 1.66/1.93 cnf(c431,plain,p13(skolem0017)|~r1(skolem0001,skolem0017)|p24(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c339, c9])).
% 1.66/1.93 cnf(c711,plain,p13(skolem0017)|p24(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c431, c41])).
% 1.66/1.93 cnf(c430,plain,p13(skolem0017)|~r1(skolem0001,skolem0017)|p25(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c339, c8])).
% 1.66/1.93 cnf(c706,plain,p13(skolem0017)|p25(skolem0011(skolem0017)),inference(resolution,[status(thm)],[c430, c41])).
% 1.66/1.93 cnf(c335,plain,r1(skolem0016,skolem0011(skolem0016))|p13(skolem0016),inference(resolution,[status(thm)],[c29, c39])).
% 1.66/1.93 cnf(c408,plain,p13(skolem0016)|~r1(skolem0001,skolem0016)|p22(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c335, c10])).
% 1.66/1.93 cnf(c701,plain,p13(skolem0016)|p22(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c408, c39])).
% 1.66/1.93 cnf(c407,plain,p13(skolem0016)|~r1(skolem0001,skolem0016)|p26(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c335, c7])).
% 1.66/1.93 cnf(c700,plain,p13(skolem0016)|p26(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c407, c39])).
% 1.66/1.93 cnf(c406,plain,p13(skolem0016)|~r1(skolem0001,skolem0016)|p24(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c335, c9])).
% 1.66/1.93 cnf(c695,plain,p13(skolem0016)|p24(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c406, c39])).
% 1.66/1.93 cnf(c405,plain,p13(skolem0016)|~r1(skolem0001,skolem0016)|p25(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c335, c8])).
% 1.66/1.93 cnf(c694,plain,p13(skolem0016)|p25(skolem0011(skolem0016)),inference(resolution,[status(thm)],[c405, c39])).
% 1.66/1.93 cnf(c296,plain,r1(skolem0014,skolem0010(skolem0014))|p13(skolem0014),inference(resolution,[status(thm)],[c27, c35])).
% 1.66/1.93 cnf(c392,plain,p13(skolem0014)|~r1(skolem0001,skolem0014)|p22(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c296, c10])).
% 1.66/1.93 cnf(c693,plain,p13(skolem0014)|p22(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c392, c35])).
% 1.66/1.93 cnf(c391,plain,p13(skolem0014)|~r1(skolem0001,skolem0014)|p26(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c296, c7])).
% 1.66/1.93 cnf(c688,plain,p13(skolem0014)|p26(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c391, c35])).
% 1.66/1.93 cnf(c390,plain,p13(skolem0014)|~r1(skolem0001,skolem0014)|p24(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c296, c9])).
% 1.66/1.93 cnf(c687,plain,p13(skolem0014)|p24(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c390, c35])).
% 1.66/1.93 cnf(c389,plain,p13(skolem0014)|~r1(skolem0001,skolem0014)|p25(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c296, c8])).
% 1.66/1.93 cnf(c682,plain,p13(skolem0014)|p25(skolem0010(skolem0014)),inference(resolution,[status(thm)],[c389, c35])).
% 1.66/1.93 cnf(c294,plain,r1(skolem0017,skolem0010(skolem0017))|p13(skolem0017),inference(resolution,[status(thm)],[c27, c41])).
% 1.66/1.93 cnf(c379,plain,p13(skolem0017)|~r1(skolem0001,skolem0017)|p22(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c294, c10])).
% 1.66/1.93 cnf(c677,plain,p13(skolem0017)|p22(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c379, c41])).
% 1.66/1.93 cnf(c378,plain,p13(skolem0017)|~r1(skolem0001,skolem0017)|p26(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c294, c7])).
% 1.66/1.93 cnf(c676,plain,p13(skolem0017)|p26(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c378, c41])).
% 1.66/1.93 cnf(c377,plain,p13(skolem0017)|~r1(skolem0001,skolem0017)|p24(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c294, c9])).
% 1.66/1.93 cnf(c671,plain,p13(skolem0017)|p24(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c377, c41])).
% 1.66/1.93 cnf(c376,plain,p13(skolem0017)|~r1(skolem0001,skolem0017)|p25(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c294, c8])).
% 1.66/1.93 cnf(c670,plain,p13(skolem0017)|p25(skolem0010(skolem0017)),inference(resolution,[status(thm)],[c376, c41])).
% 1.66/1.93 cnf(c291,plain,r1(skolem0016,skolem0010(skolem0016))|p13(skolem0016),inference(resolution,[status(thm)],[c27, c39])).
% 1.66/1.93 cnf(c349,plain,p13(skolem0016)|~r1(skolem0001,skolem0016)|p22(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c291, c10])).
% 1.66/1.93 cnf(c665,plain,p13(skolem0016)|p22(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c349, c39])).
% 1.66/1.93 cnf(c348,plain,p13(skolem0016)|~r1(skolem0001,skolem0016)|p26(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c291, c7])).
% 1.66/1.93 cnf(c660,plain,p13(skolem0016)|p26(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c348, c39])).
% 1.66/1.93 cnf(c347,plain,p13(skolem0016)|~r1(skolem0001,skolem0016)|p24(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c291, c9])).
% 1.66/1.93 cnf(c659,plain,p13(skolem0016)|p24(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c347, c39])).
% 1.66/1.93 cnf(c346,plain,p13(skolem0016)|~r1(skolem0001,skolem0016)|p25(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c291, c8])).
% 1.66/1.93 cnf(c658,plain,p13(skolem0016)|p25(skolem0010(skolem0016)),inference(resolution,[status(thm)],[c346, c39])).
% 1.66/1.93 cnf(c252,plain,r1(skolem0015,skolem0009(skolem0015))|p15(skolem0015),inference(resolution,[status(thm)],[c25, c37])).
% 1.66/1.93 cnf(c325,plain,p15(skolem0015)|~r1(skolem0001,skolem0015)|p22(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c252, c10])).
% 1.66/1.93 cnf(c649,plain,p15(skolem0015)|p22(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c325, c37])).
% 1.66/1.93 cnf(c324,plain,p15(skolem0015)|~r1(skolem0001,skolem0015)|p26(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c252, c7])).
% 1.66/1.93 cnf(c648,plain,p15(skolem0015)|p26(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c324, c37])).
% 1.66/1.93 cnf(c323,plain,p15(skolem0015)|~r1(skolem0001,skolem0015)|p24(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c252, c9])).
% 1.66/1.93 cnf(c647,plain,p15(skolem0015)|p24(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c323, c37])).
% 1.66/1.93 cnf(c322,plain,p15(skolem0015)|~r1(skolem0001,skolem0015)|p25(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c252, c8])).
% 1.66/1.93 cnf(c642,plain,p15(skolem0015)|p25(skolem0009(skolem0015)),inference(resolution,[status(thm)],[c322, c37])).
% 1.66/1.93 cnf(c251,plain,r1(skolem0017,skolem0009(skolem0017))|p15(skolem0017),inference(resolution,[status(thm)],[c25, c41])).
% 1.66/1.93 cnf(c321,plain,p15(skolem0017)|~r1(skolem0001,skolem0017)|p22(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c251, c10])).
% 1.66/1.93 cnf(c641,plain,p15(skolem0017)|p22(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c321, c41])).
% 1.66/1.93 cnf(c320,plain,p15(skolem0017)|~r1(skolem0001,skolem0017)|p26(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c251, c7])).
% 1.66/1.93 cnf(c636,plain,p15(skolem0017)|p26(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c320, c41])).
% 1.66/1.93 cnf(c319,plain,p15(skolem0017)|~r1(skolem0001,skolem0017)|p24(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c251, c9])).
% 1.66/1.93 cnf(c635,plain,p15(skolem0017)|p24(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c319, c41])).
% 1.66/1.93 cnf(c318,plain,p15(skolem0017)|~r1(skolem0001,skolem0017)|p25(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c251, c8])).
% 1.66/1.93 cnf(c634,plain,p15(skolem0017)|p25(skolem0009(skolem0017)),inference(resolution,[status(thm)],[c318, c41])).
% 1.66/1.93 cnf(c249,plain,r1(skolem0016,skolem0009(skolem0016))|p15(skolem0016),inference(resolution,[status(thm)],[c25, c39])).
% 1.66/1.93 cnf(c300,plain,p15(skolem0016)|~r1(skolem0001,skolem0016)|p22(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c249, c10])).
% 1.66/1.93 cnf(c625,plain,p15(skolem0016)|p22(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c300, c39])).
% 1.66/1.94 cnf(c299,plain,p15(skolem0016)|~r1(skolem0001,skolem0016)|p26(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c249, c7])).
% 1.66/1.94 cnf(c624,plain,p15(skolem0016)|p26(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c299, c39])).
% 1.66/1.94 cnf(c298,plain,p15(skolem0016)|~r1(skolem0001,skolem0016)|p24(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c249, c9])).
% 1.66/1.94 cnf(c623,plain,p15(skolem0016)|p24(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c298, c39])).
% 1.66/1.94 cnf(c297,plain,p15(skolem0016)|~r1(skolem0001,skolem0016)|p25(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c249, c8])).
% 1.66/1.94 cnf(c618,plain,p15(skolem0016)|p25(skolem0009(skolem0016)),inference(resolution,[status(thm)],[c297, c39])).
% 1.66/1.94 cnf(c215,plain,r1(skolem0015,skolem0008(skolem0015))|p15(skolem0015),inference(resolution,[status(thm)],[c23, c37])).
% 1.66/1.94 cnf(c281,plain,p15(skolem0015)|~r1(skolem0001,skolem0015)|p22(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c215, c10])).
% 1.66/1.94 cnf(c613,plain,p15(skolem0015)|p22(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c281, c37])).
% 1.66/1.94 cnf(c280,plain,p15(skolem0015)|~r1(skolem0001,skolem0015)|p26(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c215, c7])).
% 1.66/1.94 cnf(c612,plain,p15(skolem0015)|p26(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c280, c37])).
% 1.66/1.94 cnf(c279,plain,p15(skolem0015)|~r1(skolem0001,skolem0015)|p24(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c215, c9])).
% 1.66/1.94 cnf(c607,plain,p15(skolem0015)|p24(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c279, c37])).
% 1.66/1.94 cnf(c278,plain,p15(skolem0015)|~r1(skolem0001,skolem0015)|p25(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c215, c8])).
% 1.66/1.94 cnf(c606,plain,p15(skolem0015)|p25(skolem0008(skolem0015)),inference(resolution,[status(thm)],[c278, c37])).
% 1.66/1.94 cnf(c214,plain,r1(skolem0017,skolem0008(skolem0017))|p15(skolem0017),inference(resolution,[status(thm)],[c23, c41])).
% 1.66/1.94 cnf(c277,plain,p15(skolem0017)|~r1(skolem0001,skolem0017)|p22(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c214, c10])).
% 1.66/1.94 cnf(c601,plain,p15(skolem0017)|p22(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c277, c41])).
% 1.66/1.94 cnf(c276,plain,p15(skolem0017)|~r1(skolem0001,skolem0017)|p26(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c214, c7])).
% 1.66/1.94 cnf(c600,plain,p15(skolem0017)|p26(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c276, c41])).
% 1.66/1.94 cnf(c275,plain,p15(skolem0017)|~r1(skolem0001,skolem0017)|p24(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c214, c9])).
% 1.66/1.94 cnf(c599,plain,p15(skolem0017)|p24(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c275, c41])).
% 1.66/1.94 cnf(c274,plain,p15(skolem0017)|~r1(skolem0001,skolem0017)|p25(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c214, c8])).
% 1.66/1.94 cnf(c594,plain,p15(skolem0017)|p25(skolem0008(skolem0017)),inference(resolution,[status(thm)],[c274, c41])).
% 1.66/1.94 cnf(c212,plain,r1(skolem0016,skolem0008(skolem0016))|p15(skolem0016),inference(resolution,[status(thm)],[c23, c39])).
% 1.66/1.94 cnf(c257,plain,p15(skolem0016)|~r1(skolem0001,skolem0016)|p22(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c212, c10])).
% 1.66/1.94 cnf(c589,plain,p15(skolem0016)|p22(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c257, c39])).
% 1.66/1.94 cnf(c256,plain,p15(skolem0016)|~r1(skolem0001,skolem0016)|p26(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c212, c7])).
% 1.66/1.94 cnf(c588,plain,p15(skolem0016)|p26(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c256, c39])).
% 1.66/1.94 cnf(c255,plain,p15(skolem0016)|~r1(skolem0001,skolem0016)|p24(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c212, c9])).
% 1.66/1.94 cnf(c587,plain,p15(skolem0016)|p24(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c255, c39])).
% 1.66/1.94 cnf(c254,plain,p15(skolem0016)|~r1(skolem0001,skolem0016)|p25(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c212, c8])).
% 1.66/1.94 cnf(c586,plain,p15(skolem0016)|p25(skolem0008(skolem0016)),inference(resolution,[status(thm)],[c254, c39])).
% 1.66/1.94 cnf(c14,negated_conjecture,~r1(skolem0001,X56)|~p26(skolem0003(X56))|p14(X56),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c13,negated_conjecture,~r1(skolem0001,X55)|r1(X55,skolem0003(X55))|p14(X55),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c97,plain,r1(skolem0014,skolem0003(skolem0014))|p14(skolem0014),inference(resolution,[status(thm)],[c13, c35])).
% 1.66/1.94 cnf(c158,plain,p14(skolem0014)|~r1(skolem0001,skolem0014)|p26(skolem0003(skolem0014)),inference(resolution,[status(thm)],[c97, c7])).
% 1.66/1.94 cnf(c583,plain,p14(skolem0014)|p26(skolem0003(skolem0014)),inference(resolution,[status(thm)],[c158, c35])).
% 1.66/1.94 cnf(c584,plain,p14(skolem0014)|~r1(skolem0001,skolem0014),inference(resolution,[status(thm)],[c583, c14])).
% 1.66/1.94 cnf(c585,plain,p14(skolem0014),inference(resolution,[status(thm)],[c584, c35])).
% 1.66/1.94 cnf(c96,plain,r1(skolem0016,skolem0003(skolem0016))|p14(skolem0016),inference(resolution,[status(thm)],[c13, c39])).
% 1.66/1.94 cnf(c154,plain,p14(skolem0016)|~r1(skolem0001,skolem0016)|p26(skolem0003(skolem0016)),inference(resolution,[status(thm)],[c96, c7])).
% 1.66/1.94 cnf(c577,plain,p14(skolem0016)|p26(skolem0003(skolem0016)),inference(resolution,[status(thm)],[c154, c39])).
% 1.66/1.94 cnf(c579,plain,p14(skolem0016)|~r1(skolem0001,skolem0016),inference(resolution,[status(thm)],[c577, c14])).
% 1.66/1.94 cnf(c580,plain,p14(skolem0016),inference(resolution,[status(thm)],[c579, c39])).
% 1.66/1.94 cnf(c95,plain,r1(skolem0017,skolem0003(skolem0017))|p14(skolem0017),inference(resolution,[status(thm)],[c13, c41])).
% 1.66/1.94 cnf(c150,plain,p14(skolem0017)|~r1(skolem0001,skolem0017)|p26(skolem0003(skolem0017)),inference(resolution,[status(thm)],[c95, c7])).
% 1.66/1.94 cnf(c572,plain,p14(skolem0017)|p26(skolem0003(skolem0017)),inference(resolution,[status(thm)],[c150, c41])).
% 1.66/1.94 cnf(c573,plain,p14(skolem0017)|~r1(skolem0001,skolem0017),inference(resolution,[status(thm)],[c572, c14])).
% 1.66/1.94 cnf(c574,plain,p14(skolem0017),inference(resolution,[status(thm)],[c573, c41])).
% 1.66/1.94 cnf(c94,plain,r1(skolem0015,skolem0003(skolem0015))|p14(skolem0015),inference(resolution,[status(thm)],[c13, c37])).
% 1.66/1.94 cnf(c141,plain,p14(skolem0015)|~r1(skolem0001,skolem0015)|p26(skolem0003(skolem0015)),inference(resolution,[status(thm)],[c94, c7])).
% 1.66/1.94 cnf(c567,plain,p14(skolem0015)|p26(skolem0003(skolem0015)),inference(resolution,[status(thm)],[c141, c37])).
% 1.66/1.94 cnf(c568,plain,p14(skolem0015)|~r1(skolem0001,skolem0015),inference(resolution,[status(thm)],[c567, c14])).
% 1.66/1.94 cnf(c569,plain,p14(skolem0015),inference(resolution,[status(thm)],[c568, c37])).
% 1.66/1.94 cnf(c42,negated_conjecture,~p11(skolem0017),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c398,plain,r1(skolem0017,skolem0013(skolem0017))|p11(skolem0017),inference(resolution,[status(thm)],[c33, c41])).
% 1.66/1.94 cnf(c531,plain,r1(skolem0017,skolem0013(skolem0017)),inference(resolution,[status(thm)],[c398, c42])).
% 1.66/1.94 cnf(c535,plain,~r1(skolem0001,skolem0017)|p22(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c531, c10])).
% 1.66/1.94 cnf(c564,plain,p22(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c535, c41])).
% 1.66/1.94 cnf(c534,plain,~r1(skolem0001,skolem0017)|p26(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c531, c7])).
% 1.66/1.94 cnf(c563,plain,p26(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c534, c41])).
% 1.66/1.94 cnf(c533,plain,~r1(skolem0001,skolem0017)|p24(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c531, c9])).
% 1.66/1.94 cnf(c562,plain,p24(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c533, c41])).
% 1.66/1.94 cnf(c87,plain,r1(skolem0014,skolem0002(skolem0014))|p16(skolem0014),inference(resolution,[status(thm)],[c11, c35])).
% 1.66/1.94 cnf(c123,plain,p16(skolem0014)|~r1(skolem0001,skolem0014)|p26(skolem0002(skolem0014)),inference(resolution,[status(thm)],[c87, c7])).
% 1.66/1.94 cnf(c559,plain,p16(skolem0014)|p26(skolem0002(skolem0014)),inference(resolution,[status(thm)],[c123, c35])).
% 1.66/1.94 cnf(c560,plain,p16(skolem0014)|~r1(skolem0001,skolem0014),inference(resolution,[status(thm)],[c559, c12])).
% 1.66/1.94 cnf(c561,plain,p16(skolem0014),inference(resolution,[status(thm)],[c560, c35])).
% 1.66/1.94 cnf(c532,plain,~r1(skolem0001,skolem0017)|p25(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c531, c8])).
% 1.66/1.94 cnf(c558,plain,p25(skolem0013(skolem0017)),inference(resolution,[status(thm)],[c532, c41])).
% 1.66/1.94 cnf(c372,plain,r1(skolem0017,skolem0012(skolem0017))|p11(skolem0017),inference(resolution,[status(thm)],[c31, c41])).
% 1.66/1.94 cnf(c480,plain,r1(skolem0017,skolem0012(skolem0017)),inference(resolution,[status(thm)],[c372, c42])).
% 1.66/1.94 cnf(c484,plain,~r1(skolem0001,skolem0017)|p22(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c480, c10])).
% 1.66/1.94 cnf(c557,plain,p22(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c484, c41])).
% 1.66/1.94 cnf(c483,plain,~r1(skolem0001,skolem0017)|p26(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c480, c7])).
% 1.66/1.94 cnf(c555,plain,p26(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c483, c41])).
% 1.66/1.94 cnf(c482,plain,~r1(skolem0001,skolem0017)|p24(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c480, c9])).
% 1.66/1.94 cnf(c554,plain,p24(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c482, c41])).
% 1.66/1.94 cnf(c481,plain,~r1(skolem0001,skolem0017)|p25(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c480, c8])).
% 1.66/1.94 cnf(c552,plain,p25(skolem0012(skolem0017)),inference(resolution,[status(thm)],[c481, c41])).
% 1.66/1.94 cnf(c38,negated_conjecture,~p13(skolem0015),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c340,plain,r1(skolem0015,skolem0011(skolem0015))|p13(skolem0015),inference(resolution,[status(thm)],[c29, c37])).
% 1.66/1.94 cnf(c438,plain,r1(skolem0015,skolem0011(skolem0015)),inference(resolution,[status(thm)],[c340, c38])).
% 1.66/1.94 cnf(c443,plain,~r1(skolem0001,skolem0015)|p22(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c438, c10])).
% 1.66/1.94 cnf(c551,plain,p22(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c443, c37])).
% 1.66/1.94 cnf(c442,plain,~r1(skolem0001,skolem0015)|p26(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c438, c7])).
% 1.66/1.94 cnf(c550,plain,p26(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c442, c37])).
% 1.66/1.94 cnf(c86,plain,r1(skolem0016,skolem0002(skolem0016))|p16(skolem0016),inference(resolution,[status(thm)],[c11, c39])).
% 1.66/1.94 cnf(c119,plain,p16(skolem0016)|~r1(skolem0001,skolem0016)|p26(skolem0002(skolem0016)),inference(resolution,[status(thm)],[c86, c7])).
% 1.66/1.94 cnf(c547,plain,p16(skolem0016)|p26(skolem0002(skolem0016)),inference(resolution,[status(thm)],[c119, c39])).
% 1.66/1.94 cnf(c548,plain,p16(skolem0016)|~r1(skolem0001,skolem0016),inference(resolution,[status(thm)],[c547, c12])).
% 1.66/1.94 cnf(c549,plain,p16(skolem0016),inference(resolution,[status(thm)],[c548, c39])).
% 1.66/1.94 cnf(c441,plain,~r1(skolem0001,skolem0015)|p24(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c438, c9])).
% 1.66/1.94 cnf(c546,plain,p24(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c441, c37])).
% 1.66/1.94 cnf(c440,plain,~r1(skolem0001,skolem0015)|p25(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c438, c8])).
% 1.66/1.94 cnf(c545,plain,p25(skolem0011(skolem0015)),inference(resolution,[status(thm)],[c440, c37])).
% 1.66/1.94 cnf(c61,plain,~r1(skolem0001,X48)|p25(X48),inference(resolution,[status(thm)],[c8, c44])).
% 1.66/1.94 cnf(c524,plain,p11(skolem0001)|p25(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c61])).
% 1.66/1.94 cnf(c78,plain,~r1(skolem0001,X53)|p22(X53),inference(resolution,[status(thm)],[c10, c44])).
% 1.66/1.94 cnf(c522,plain,p11(skolem0001)|p22(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c78])).
% 1.66/1.94 cnf(c46,plain,~r1(skolem0001,X43)|p26(X43),inference(resolution,[status(thm)],[c7, c44])).
% 1.66/1.94 cnf(c516,plain,p11(skolem0001)|p26(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c46])).
% 1.66/1.94 cnf(c67,plain,~r1(skolem0001,X51)|p24(X51),inference(resolution,[status(thm)],[c9, c44])).
% 1.66/1.94 cnf(c507,plain,p11(skolem0001)|p24(skolem0013(skolem0001)),inference(resolution,[status(thm)],[c397, c67])).
% 1.66/1.94 cnf(c295,plain,r1(skolem0015,skolem0010(skolem0015))|p13(skolem0015),inference(resolution,[status(thm)],[c27, c37])).
% 1.66/1.94 cnf(c384,plain,r1(skolem0015,skolem0010(skolem0015)),inference(resolution,[status(thm)],[c295, c38])).
% 1.66/1.94 cnf(c388,plain,~r1(skolem0001,skolem0015)|p22(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c384, c10])).
% 1.66/1.94 cnf(c501,plain,p22(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c388, c37])).
% 1.66/1.94 cnf(c85,plain,r1(skolem0017,skolem0002(skolem0017))|p16(skolem0017),inference(resolution,[status(thm)],[c11, c41])).
% 1.66/1.94 cnf(c110,plain,p16(skolem0017)|~r1(skolem0001,skolem0017)|p26(skolem0002(skolem0017)),inference(resolution,[status(thm)],[c85, c7])).
% 1.66/1.94 cnf(c498,plain,p16(skolem0017)|p26(skolem0002(skolem0017)),inference(resolution,[status(thm)],[c110, c41])).
% 1.66/1.94 cnf(c499,plain,p16(skolem0017)|~r1(skolem0001,skolem0017),inference(resolution,[status(thm)],[c498, c12])).
% 1.66/1.94 cnf(c500,plain,p16(skolem0017),inference(resolution,[status(thm)],[c499, c41])).
% 1.66/1.94 cnf(c387,plain,~r1(skolem0001,skolem0015)|p26(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c384, c7])).
% 1.66/1.94 cnf(c497,plain,p26(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c387, c37])).
% 1.66/1.94 cnf(c386,plain,~r1(skolem0001,skolem0015)|p24(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c384, c9])).
% 1.66/1.94 cnf(c496,plain,p24(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c386, c37])).
% 1.66/1.94 cnf(c385,plain,~r1(skolem0001,skolem0015)|p25(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c384, c8])).
% 1.66/1.94 cnf(c494,plain,p25(skolem0010(skolem0015)),inference(resolution,[status(thm)],[c385, c37])).
% 1.66/1.94 cnf(c84,plain,r1(skolem0015,skolem0002(skolem0015))|p16(skolem0015),inference(resolution,[status(thm)],[c11, c37])).
% 1.66/1.94 cnf(c106,plain,p16(skolem0015)|~r1(skolem0001,skolem0015)|p26(skolem0002(skolem0015)),inference(resolution,[status(thm)],[c84, c7])).
% 1.66/1.94 cnf(c472,plain,p16(skolem0015)|p26(skolem0002(skolem0015)),inference(resolution,[status(thm)],[c106, c37])).
% 1.66/1.94 cnf(c473,plain,p16(skolem0015)|~r1(skolem0001,skolem0015),inference(resolution,[status(thm)],[c472, c12])).
% 1.66/1.94 cnf(c475,plain,p16(skolem0015),inference(resolution,[status(thm)],[c473, c37])).
% 1.66/1.94 cnf(c470,plain,p11(skolem0001)|p25(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c61])).
% 1.66/1.94 cnf(c468,plain,p11(skolem0001)|p22(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c78])).
% 1.66/1.94 cnf(c462,plain,p11(skolem0001)|p26(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c46])).
% 1.66/1.94 cnf(c453,plain,p11(skolem0001)|p24(skolem0012(skolem0001)),inference(resolution,[status(thm)],[c371, c67])).
% 1.66/1.94 cnf(c427,plain,p13(skolem0001)|p25(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c61])).
% 1.66/1.94 cnf(c425,plain,p13(skolem0001)|p22(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c78])).
% 1.66/1.94 cnf(c419,plain,p13(skolem0001)|p26(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c46])).
% 1.66/1.94 cnf(c410,plain,p13(skolem0001)|p24(skolem0011(skolem0001)),inference(resolution,[status(thm)],[c338, c67])).
% 1.66/1.94 cnf(c36,negated_conjecture,~p15(skolem0014),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c253,plain,r1(skolem0014,skolem0009(skolem0014))|p15(skolem0014),inference(resolution,[status(thm)],[c25, c35])).
% 1.66/1.94 cnf(c330,plain,r1(skolem0014,skolem0009(skolem0014)),inference(resolution,[status(thm)],[c253, c36])).
% 1.66/1.94 cnf(c334,plain,~r1(skolem0001,skolem0014)|p22(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c330, c10])).
% 1.66/1.94 cnf(c404,plain,p22(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c334, c35])).
% 1.66/1.94 cnf(c34,negated_conjecture,~r1(skolem0001,X76)|~p21(skolem0013(X76))|p11(X76),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c333,plain,~r1(skolem0001,skolem0014)|p26(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c330, c7])).
% 1.66/1.94 cnf(c403,plain,p26(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c333, c35])).
% 1.66/1.94 cnf(c332,plain,~r1(skolem0001,skolem0014)|p24(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c330, c9])).
% 1.66/1.94 cnf(c402,plain,p24(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c332, c35])).
% 1.66/1.94 cnf(c331,plain,~r1(skolem0001,skolem0014)|p25(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c330, c8])).
% 1.66/1.94 cnf(c393,plain,p25(skolem0009(skolem0014)),inference(resolution,[status(thm)],[c331, c35])).
% 1.66/1.94 cnf(c32,negated_conjecture,~r1(skolem0001,X74)|~p23(skolem0012(X74))|p11(X74),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c366,plain,p13(skolem0001)|p25(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c293, c61])).
% 1.66/1.94 cnf(c365,plain,p13(skolem0001)|p22(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c293, c78])).
% 1.66/1.94 cnf(c359,plain,p13(skolem0001)|p26(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c293, c46])).
% 1.66/1.94 cnf(c350,plain,p13(skolem0001)|p24(skolem0010(skolem0001)),inference(resolution,[status(thm)],[c293, c67])).
% 1.66/1.94 cnf(c216,plain,r1(skolem0014,skolem0008(skolem0014))|p15(skolem0014),inference(resolution,[status(thm)],[c23, c35])).
% 1.66/1.94 cnf(c286,plain,r1(skolem0014,skolem0008(skolem0014)),inference(resolution,[status(thm)],[c216, c36])).
% 1.66/1.94 cnf(c290,plain,~r1(skolem0001,skolem0014)|p22(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c286, c10])).
% 1.66/1.94 cnf(c345,plain,p22(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c290, c35])).
% 1.66/1.94 cnf(c289,plain,~r1(skolem0001,skolem0014)|p26(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c286, c7])).
% 1.66/1.94 cnf(c344,plain,p26(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c289, c35])).
% 1.66/1.94 cnf(c30,negated_conjecture,~r1(skolem0001,X72)|~p21(skolem0011(X72))|p13(X72),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c288,plain,~r1(skolem0001,skolem0014)|p24(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c286, c9])).
% 1.66/1.94 cnf(c343,plain,p24(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c288, c35])).
% 1.66/1.94 cnf(c287,plain,~r1(skolem0001,skolem0014)|p25(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c286, c8])).
% 1.66/1.94 cnf(c342,plain,p25(skolem0008(skolem0014)),inference(resolution,[status(thm)],[c287, c35])).
% 1.66/1.94 cnf(c313,plain,p15(skolem0001)|p26(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c250, c46])).
% 1.66/1.94 cnf(c28,negated_conjecture,~r1(skolem0001,X70)|~p23(skolem0010(X70))|p13(X70),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c310,plain,p15(skolem0001)|p25(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c250, c61])).
% 1.66/1.94 cnf(c304,plain,p15(skolem0001)|p22(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c250, c78])).
% 1.66/1.94 cnf(c301,plain,p15(skolem0001)|p24(skolem0009(skolem0001)),inference(resolution,[status(thm)],[c250, c67])).
% 1.66/1.94 cnf(c269,plain,p15(skolem0001)|p26(skolem0008(skolem0001)),inference(resolution,[status(thm)],[c213, c46])).
% 1.66/1.94 cnf(c26,negated_conjecture,~r1(skolem0001,X68)|~p21(skolem0009(X68))|p15(X68),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c266,plain,p15(skolem0001)|p25(skolem0008(skolem0001)),inference(resolution,[status(thm)],[c213, c61])).
% 1.66/1.94 cnf(c260,plain,p15(skolem0001)|p22(skolem0008(skolem0001)),inference(resolution,[status(thm)],[c213, c78])).
% 1.66/1.94 cnf(c258,plain,p15(skolem0001)|p24(skolem0008(skolem0001)),inference(resolution,[status(thm)],[c213, c67])).
% 1.66/1.94 cnf(c24,negated_conjecture,~r1(skolem0001,X66)|~p23(skolem0008(X66))|p15(X66),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c98,plain,r1(skolem0001,skolem0003(skolem0001))|p14(skolem0001),inference(resolution,[status(thm)],[c13, c44])).
% 1.66/1.94 cnf(c168,plain,p14(skolem0001)|p26(skolem0003(skolem0001)),inference(resolution,[status(thm)],[c98, c46])).
% 1.66/1.94 cnf(c173,plain,p14(skolem0001)|~r1(skolem0001,skolem0001),inference(resolution,[status(thm)],[c168, c14])).
% 1.66/1.94 cnf(c174,plain,p14(skolem0001),inference(resolution,[status(thm)],[c173, c44])).
% 1.66/1.94 cnf(c20,negated_conjecture,~r1(skolem0001,X62)|~p22(skolem0006(X62))|p16(X62),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c19,negated_conjecture,~r1(skolem0001,X61)|r1(X61,skolem0006(X61))|p16(X61),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c88,plain,r1(skolem0001,skolem0002(skolem0001))|p16(skolem0001),inference(resolution,[status(thm)],[c11, c44])).
% 1.66/1.94 cnf(c132,plain,p16(skolem0001)|p26(skolem0002(skolem0001)),inference(resolution,[status(thm)],[c88, c46])).
% 1.66/1.94 cnf(c137,plain,p16(skolem0001)|~r1(skolem0001,skolem0001),inference(resolution,[status(thm)],[c132, c12])).
% 1.66/1.94 cnf(c138,plain,p16(skolem0001),inference(resolution,[status(thm)],[c137, c44])).
% 1.66/1.94 cnf(c18,negated_conjecture,~r1(skolem0001,X60)|~p24(skolem0005(X60))|p14(X60),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c17,negated_conjecture,~r1(skolem0001,X59)|r1(X59,skolem0005(X59))|p14(X59),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 cnf(c93,plain,p22(skolem0001),inference(resolution,[status(thm)],[c78, c44])).
% 1.66/1.94 cnf(c92,plain,p22(skolem0014),inference(resolution,[status(thm)],[c78, c35])).
% 1.66/1.94 cnf(c91,plain,p22(skolem0016),inference(resolution,[status(thm)],[c78, c39])).
% 1.66/1.94 cnf(c90,plain,p22(skolem0017),inference(resolution,[status(thm)],[c78, c41])).
% 1.66/1.94 cnf(c89,plain,p22(skolem0015),inference(resolution,[status(thm)],[c78, c37])).
% 1.66/1.94 cnf(c83,plain,p24(skolem0001),inference(resolution,[status(thm)],[c67, c44])).
% 1.66/1.94 cnf(c82,plain,p24(skolem0014),inference(resolution,[status(thm)],[c67, c35])).
% 1.66/1.94 cnf(c81,plain,p24(skolem0016),inference(resolution,[status(thm)],[c67, c39])).
% 1.66/1.94 cnf(c80,plain,p24(skolem0017),inference(resolution,[status(thm)],[c67, c41])).
% 1.66/1.94 cnf(c79,plain,p24(skolem0015),inference(resolution,[status(thm)],[c67, c37])).
% 1.66/1.94 cnf(c72,plain,p25(skolem0001),inference(resolution,[status(thm)],[c61, c44])).
% 1.66/1.94 cnf(c71,plain,p25(skolem0014),inference(resolution,[status(thm)],[c61, c35])).
% 1.66/1.94 cnf(c70,plain,p25(skolem0016),inference(resolution,[status(thm)],[c61, c39])).
% 1.66/1.94 cnf(c69,plain,p25(skolem0017),inference(resolution,[status(thm)],[c61, c41])).
% 1.66/1.94 cnf(c68,plain,p25(skolem0015),inference(resolution,[status(thm)],[c61, c37])).
% 1.66/1.94 cnf(c55,plain,p26(skolem0001),inference(resolution,[status(thm)],[c46, c44])).
% 1.66/1.94 cnf(c54,plain,p26(skolem0014),inference(resolution,[status(thm)],[c46, c35])).
% 1.66/1.94 cnf(c53,plain,p26(skolem0016),inference(resolution,[status(thm)],[c46, c39])).
% 1.66/1.94 cnf(c52,plain,p26(skolem0017),inference(resolution,[status(thm)],[c46, c41])).
% 1.66/1.94 cnf(c51,plain,p26(skolem0015),inference(resolution,[status(thm)],[c46, c37])).
% 1.66/1.94 cnf(c40,negated_conjecture,~p12(skolem0016),inference(split_conjunct,[status(thm)],[c6])).
% 1.66/1.94 % SZS output end Saturation
% 1.66/1.94
% 1.66/1.94 % Initial clauses : 37
% 1.66/1.94 % Processed clauses : 881
% 1.66/1.94 % Factors computed : 4
% 1.66/1.94 % Resolvents computed: 1105
% 1.66/1.94 % Tautologies deleted: 0
% 1.66/1.94 % Forward subsumed : 265
% 1.66/1.94 % Backward subsumed : 468
% 1.66/1.94 % -------- CPU Time ---------
% 1.66/1.94 % User time : 1.556 s
% 1.66/1.94 % System time : 0.034 s
% 1.66/1.94 % Total time : 1.590 s
%------------------------------------------------------------------------------