%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:59:05 PM UTC 2026
% Result : Theorem 5.05s 5.30s
% Output : CNFRefutation 5.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 16:24:50 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.42 (re.compile("\."), Token.FullStop),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.42 (re.compile("\("), Token.OpenPar),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.42 (re.compile("\)"), Token.ClosePar),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.43 (re.compile("\["), Token.OpenSquare),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("~\|"), Token.Nor),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("\|"), Token.Or),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.43 (re.compile("\?"), Token.Existential),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.50 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.32/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 5.05/5.30 % Version: 1.5
% 5.05/5.30 % SZS status Theorem
% 5.05/5.30 % SZS output start CNFRefutation
% 5.05/5.30 fof(reflexivity,axiom,(![X]:r1(X,X)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 5.05/5.30 fof(c158,plain,(![X68]:r1(X68,X68)),inference(variable_rename,[status(thm)],[reflexivity])).
% 5.05/5.30 cnf(c159,plain,r1(X69,X69),inference(split_conjunct,[status(thm)],[c158])).
% 5.05/5.30 fof(main,conjecture,(~(?[X]:(~((![Y]:(((~r1(X,Y))|(~p30(Y)))|(![X]:((~r1(Y,X))|(~p1(X))))))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|(~((((![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|$false)))|(~(![X]:((~r1(Y,X))|(~((p29(X)&(~p28(X)))|((~p29(X))&p28(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p28(Y)&(~p27(Y)))|((~p28(Y))&p27(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p27(X)&(~p26(X)))|((~p27(X))&p26(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p26(Y)&(~p25(Y)))|((~p26(Y))&p25(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p25(X)&(~p24(X)))|((~p25(X))&p24(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p24(Y)&(~p23(Y)))|((~p24(Y))&p23(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p23(X)&(~p22(X)))|((~p23(X))&p22(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p22(Y)&(~p21(Y)))|((~p22(Y))&p21(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p21(X)&(~p20(X)))|((~p21(X))&p20(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p20(Y)&(~p19(Y)))|((~p20(Y))&p19(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p19(X)&(~p18(X)))|((~p19(X))&p18(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p18(Y)&(~p17(Y)))|((~p18(Y))&p17(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p17(X)&(~p16(X)))|((~p17(X))&p16(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p16(Y)&(~p15(Y)))|((~p16(Y))&p15(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p15(X)&(~p14(X)))|((~p15(X))&p14(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p14(Y)&(~p13(Y)))|((~p14(Y))&p13(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p13(X)&(~p12(X)))|((~p13(X))&p12(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p12(Y)&(~p11(Y)))|((~p12(Y))&p11(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p11(X)&(~p10(X)))|((~p11(X))&p10(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p10(Y)&(~p9(Y)))|((~p10(Y))&p9(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p9(X)&(~p8(X)))|((~p9(X))&p8(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p8(Y)&(~p7(Y)))|((~p8(Y))&p7(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p7(X)&(~p6(X)))|((~p7(X))&p6(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p6(Y)&(~p5(Y)))|((~p6(Y))&p5(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p5(X)&(~p4(X)))|((~p5(X))&p4(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p4(Y)&(~p3(Y)))|((~p4(Y))&p3(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p3(X)&(~p2(X)))|((~p3(X))&p2(X)))))))))|(~(![Y]:((~r1(X,Y))|(~((p2(Y)&(~p1(Y)))|((~p2(Y))&p1(Y))))))))|(![Y]:((~r1(X,Y))|p30(Y))))|(![Y]:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((~r1(X,Y))|((~p28(Y))&(~p29(Y))))|(p29(Y)&p28(Y)))|((~p27(Y))&(~p28(Y))))|(p28(Y)&p27(Y)))|((~p26(Y))&(~p27(Y))))|(p27(Y)&p26(Y)))|((~p25(Y))&(~p26(Y))))|(p26(Y)&p25(Y)))|((~p24(Y))&(~p25(Y))))|(p25(Y)&p24(Y)))|((~p23(Y))&(~p24(Y))))|(p24(Y)&p23(Y)))|((~p22(Y))&(~p23(Y))))|(p23(Y)&p22(Y)))|((~p21(Y))&(~p22(Y))))|(p22(Y)&p21(Y)))|((~p20(Y))&(~p21(Y))))|(p21(Y)&p20(Y)))|((~p19(Y))&(~p20(Y))))|(p20(Y)&p19(Y)))|((~p18(Y))&(~p19(Y))))|(p19(Y)&p18(Y)))|((~p17(Y))&(~p18(Y))))|(p18(Y)&p17(Y)))|((~p16(Y))&(~p17(Y))))|(p17(Y)&p16(Y)))|((~p15(Y))&(~p16(Y))))|(p16(Y)&p15(Y)))|((~p14(Y))&(~p15(Y))))|(p15(Y)&p14(Y)))|((~p13(Y))&(~p14(Y))))|(p14(Y)&p13(Y)))|((~p12(Y))&(~p13(Y))))|(p13(Y)&p12(Y)))|((~p11(Y))&(~p12(Y))))|(p12(Y)&p11(Y)))|((~p10(Y))&(~p11(Y))))|(p11(Y)&p10(Y)))|((~p9(Y))&(~p10(Y))))|(p10(Y)&p9(Y)))|((~p8(Y))&(~p9(Y))))|(p9(Y)&p8(Y)))|((~p7(Y))&(~p8(Y))))|(p8(Y)&p7(Y)))|((~p6(Y))&(~p7(Y))))|(p7(Y)&p6(Y)))|((~p5(Y))&(~p6(Y))))|(p6(Y)&p5(Y)))|((~p4(Y))&(~p5(Y))))|(p5(Y)&p4(Y)))|((~p3(Y))&(~p4(Y))))|(p4(Y)&p3(Y)))|((~p2(Y))&(~p3(Y))))|(p3(Y)&p2(Y)))|((~p1(Y))&(~p2(Y))))|(p2(Y)&p1(Y))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 5.05/5.30 fof(c0,negated_conjecture,(~(~(?[X]:(~((![Y]:(((~r1(X,Y))|(~p30(Y)))|(![X]:((~r1(Y,X))|(~p1(X))))))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|(~((((![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:(((~r1(Y,X))|(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|$false)))|(~(![X]:((~r1(Y,X))|(~((p29(X)&(~p28(X)))|((~p29(X))&p28(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p28(Y)&(~p27(Y)))|((~p28(Y))&p27(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p27(X)&(~p26(X)))|((~p27(X))&p26(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p26(Y)&(~p25(Y)))|((~p26(Y))&p25(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p25(X)&(~p24(X)))|((~p25(X))&p24(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p24(Y)&(~p23(Y)))|((~p24(Y))&p23(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p23(X)&(~p22(X)))|((~p23(X))&p22(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p22(Y)&(~p21(Y)))|((~p22(Y))&p21(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p21(X)&(~p20(X)))|((~p21(X))&p20(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p20(Y)&(~p19(Y)))|((~p20(Y))&p19(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p19(X)&(~p18(X)))|((~p19(X))&p18(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p18(Y)&(~p17(Y)))|((~p18(Y))&p17(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p17(X)&(~p16(X)))|((~p17(X))&p16(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p16(Y)&(~p15(Y)))|((~p16(Y))&p15(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p15(X)&(~p14(X)))|((~p15(X))&p14(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p14(Y)&(~p13(Y)))|((~p14(Y))&p13(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p13(X)&(~p12(X)))|((~p13(X))&p12(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p12(Y)&(~p11(Y)))|((~p12(Y))&p11(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p11(X)&(~p10(X)))|((~p11(X))&p10(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p10(Y)&(~p9(Y)))|((~p10(Y))&p9(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p9(X)&(~p8(X)))|((~p9(X))&p8(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p8(Y)&(~p7(Y)))|((~p8(Y))&p7(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p7(X)&(~p6(X)))|((~p7(X))&p6(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p6(Y)&(~p5(Y)))|((~p6(Y))&p5(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p5(X)&(~p4(X)))|((~p5(X))&p4(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p4(Y)&(~p3(Y)))|((~p4(Y))&p3(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p3(X)&(~p2(X)))|((~p3(X))&p2(X)))))))))|(~(![Y]:((~r1(X,Y))|(~((p2(Y)&(~p1(Y)))|((~p2(Y))&p1(Y))))))))|(![Y]:((~r1(X,Y))|p30(Y))))|(![Y]:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((~r1(X,Y))|((~p28(Y))&(~p29(Y))))|(p29(Y)&p28(Y)))|((~p27(Y))&(~p28(Y))))|(p28(Y)&p27(Y)))|((~p26(Y))&(~p27(Y))))|(p27(Y)&p26(Y)))|((~p25(Y))&(~p26(Y))))|(p26(Y)&p25(Y)))|((~p24(Y))&(~p25(Y))))|(p25(Y)&p24(Y)))|((~p23(Y))&(~p24(Y))))|(p24(Y)&p23(Y)))|((~p22(Y))&(~p23(Y))))|(p23(Y)&p22(Y)))|((~p21(Y))&(~p22(Y))))|(p22(Y)&p21(Y)))|((~p20(Y))&(~p21(Y))))|(p21(Y)&p20(Y)))|((~p19(Y))&(~p20(Y))))|(p20(Y)&p19(Y)))|((~p18(Y))&(~p19(Y))))|(p19(Y)&p18(Y)))|((~p17(Y))&(~p18(Y))))|(p18(Y)&p17(Y)))|((~p16(Y))&(~p17(Y))))|(p17(Y)&p16(Y)))|((~p15(Y))&(~p16(Y))))|(p16(Y)&p15(Y)))|((~p14(Y))&(~p15(Y))))|(p15(Y)&p14(Y)))|((~p13(Y))&(~p14(Y))))|(p14(Y)&p13(Y)))|((~p12(Y))&(~p13(Y))))|(p13(Y)&p12(Y)))|((~p11(Y))&(~p12(Y))))|(p12(Y)&p11(Y)))|((~p10(Y))&(~p11(Y))))|(p11(Y)&p10(Y)))|((~p9(Y))&(~p10(Y))))|(p10(Y)&p9(Y)))|((~p8(Y))&(~p9(Y))))|(p9(Y)&p8(Y)))|((~p7(Y))&(~p8(Y))))|(p8(Y)&p7(Y)))|((~p6(Y))&(~p7(Y))))|(p7(Y)&p6(Y)))|((~p5(Y))&(~p6(Y))))|(p6(Y)&p5(Y)))|((~p4(Y))&(~p5(Y))))|(p5(Y)&p4(Y)))|((~p3(Y))&(~p4(Y))))|(p4(Y)&p3(Y)))|((~p2(Y))&(~p3(Y))))|(p3(Y)&p2(Y)))|((~p1(Y))&(~p2(Y))))|(p2(Y)&p1(Y)))))))))))))))),inference(assume_negation,[status(cth)],[main])).
% 5.05/5.31 fof(c1,negated_conjecture,(~(~(?[X]:(~((![Y]:((~r1(X,Y)|~p30(Y))|(![X]:(~r1(Y,X)|~p1(X)))))|(![Y]:(~r1(X,Y)|(~(![X]:(~r1(Y,X)|(~((((![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:((~r1(Y,X)|(![Y]:((~r1(X,Y)|(![X]:~r1(Y,X)))|(~(![X]:(~r1(Y,X)|(~((p29(X)&~p28(X))|(~p29(X)&p28(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p28(Y)&~p27(Y))|(~p28(Y)&p27(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p27(X)&~p26(X))|(~p27(X)&p26(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p26(Y)&~p25(Y))|(~p26(Y)&p25(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p25(X)&~p24(X))|(~p25(X)&p24(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p24(Y)&~p23(Y))|(~p24(Y)&p23(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p23(X)&~p22(X))|(~p23(X)&p22(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p22(Y)&~p21(Y))|(~p22(Y)&p21(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p21(X)&~p20(X))|(~p21(X)&p20(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p20(Y)&~p19(Y))|(~p20(Y)&p19(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p19(X)&~p18(X))|(~p19(X)&p18(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p18(Y)&~p17(Y))|(~p18(Y)&p17(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p17(X)&~p16(X))|(~p17(X)&p16(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p16(Y)&~p15(Y))|(~p16(Y)&p15(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p15(X)&~p14(X))|(~p15(X)&p14(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p14(Y)&~p13(Y))|(~p14(Y)&p13(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p13(X)&~p12(X))|(~p13(X)&p12(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p12(Y)&~p11(Y))|(~p12(Y)&p11(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p11(X)&~p10(X))|(~p11(X)&p10(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p10(Y)&~p9(Y))|(~p10(Y)&p9(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p9(X)&~p8(X))|(~p9(X)&p8(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p8(Y)&~p7(Y))|(~p8(Y)&p7(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p7(X)&~p6(X))|(~p7(X)&p6(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p6(Y)&~p5(Y))|(~p6(Y)&p5(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p5(X)&~p4(X))|(~p5(X)&p4(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p4(Y)&~p3(Y))|(~p4(Y)&p3(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p3(X)&~p2(X))|(~p3(X)&p2(X)))))))))|(~(![Y]:(~r1(X,Y)|(~((p2(Y)&~p1(Y))|(~p2(Y)&p1(Y))))))))|(![Y]:(~r1(X,Y)|p30(Y))))|(![Y]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((~r1(X,Y)|(~p28(Y)&~p29(Y)))|(p29(Y)&p28(Y)))|(~p27(Y)&~p28(Y)))|(p28(Y)&p27(Y)))|(~p26(Y)&~p27(Y)))|(p27(Y)&p26(Y)))|(~p25(Y)&~p26(Y)))|(p26(Y)&p25(Y)))|(~p24(Y)&~p25(Y)))|(p25(Y)&p24(Y)))|(~p23(Y)&~p24(Y)))|(p24(Y)&p23(Y)))|(~p22(Y)&~p23(Y)))|(p23(Y)&p22(Y)))|(~p21(Y)&~p22(Y)))|(p22(Y)&p21(Y)))|(~p20(Y)&~p21(Y)))|(p21(Y)&p20(Y)))|(~p19(Y)&~p20(Y)))|(p20(Y)&p19(Y)))|(~p18(Y)&~p19(Y)))|(p19(Y)&p18(Y)))|(~p17(Y)&~p18(Y)))|(p18(Y)&p17(Y)))|(~p16(Y)&~p17(Y)))|(p17(Y)&p16(Y)))|(~p15(Y)&~p16(Y)))|(p16(Y)&p15(Y)))|(~p14(Y)&~p15(Y)))|(p15(Y)&p14(Y)))|(~p13(Y)&~p14(Y)))|(p14(Y)&p13(Y)))|(~p12(Y)&~p13(Y)))|(p13(Y)&p12(Y)))|(~p11(Y)&~p12(Y)))|(p12(Y)&p11(Y)))|(~p10(Y)&~p11(Y)))|(p11(Y)&p10(Y)))|(~p9(Y)&~p10(Y)))|(p10(Y)&p9(Y)))|(~p8(Y)&~p9(Y)))|(p9(Y)&p8(Y)))|(~p7(Y)&~p8(Y)))|(p8(Y)&p7(Y)))|(~p6(Y)&~p7(Y)))|(p7(Y)&p6(Y)))|(~p5(Y)&~p6(Y)))|(p6(Y)&p5(Y)))|(~p4(Y)&~p5(Y)))|(p5(Y)&p4(Y)))|(~p3(Y)&~p4(Y)))|(p4(Y)&p3(Y)))|(~p2(Y)&~p3(Y)))|(p3(Y)&p2(Y)))|(~p1(Y)&~p2(Y)))|(p2(Y)&p1(Y)))))))))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 5.05/5.31 fof(c2,negated_conjecture,(?[X]:((?[Y]:((r1(X,Y)&p30(Y))&(?[X]:(r1(Y,X)&p1(X)))))&(?[Y]:(r1(X,Y)&(![X]:(~r1(Y,X)|((((?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:((r1(Y,X)&(?[Y]:((r1(X,Y)&(?[X]:r1(Y,X)))&(![X]:(~r1(Y,X)|((~p29(X)|p28(X))&(p29(X)|~p28(X))))))))&(![Y]:(~r1(X,Y)|((~p28(Y)|p27(Y))&(p28(Y)|~p27(Y))))))))&(![X]:(~r1(Y,X)|((~p27(X)|p26(X))&(p27(X)|~p26(X))))))))&(![Y]:(~r1(X,Y)|((~p26(Y)|p25(Y))&(p26(Y)|~p25(Y))))))))&(![X]:(~r1(Y,X)|((~p25(X)|p24(X))&(p25(X)|~p24(X))))))))&(![Y]:(~r1(X,Y)|((~p24(Y)|p23(Y))&(p24(Y)|~p23(Y))))))))&(![X]:(~r1(Y,X)|((~p23(X)|p22(X))&(p23(X)|~p22(X))))))))&(![Y]:(~r1(X,Y)|((~p22(Y)|p21(Y))&(p22(Y)|~p21(Y))))))))&(![X]:(~r1(Y,X)|((~p21(X)|p20(X))&(p21(X)|~p20(X))))))))&(![Y]:(~r1(X,Y)|((~p20(Y)|p19(Y))&(p20(Y)|~p19(Y))))))))&(![X]:(~r1(Y,X)|((~p19(X)|p18(X))&(p19(X)|~p18(X))))))))&(![Y]:(~r1(X,Y)|((~p18(Y)|p17(Y))&(p18(Y)|~p17(Y))))))))&(![X]:(~r1(Y,X)|((~p17(X)|p16(X))&(p17(X)|~p16(X))))))))&(![Y]:(~r1(X,Y)|((~p16(Y)|p15(Y))&(p16(Y)|~p15(Y))))))))&(![X]:(~r1(Y,X)|((~p15(X)|p14(X))&(p15(X)|~p14(X))))))))&(![Y]:(~r1(X,Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y))))))))&(![X]:(~r1(Y,X)|((~p13(X)|p12(X))&(p13(X)|~p12(X))))))))&(![Y]:(~r1(X,Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y))))))))&(![X]:(~r1(Y,X)|((~p11(X)|p10(X))&(p11(X)|~p10(X))))))))&(![Y]:(~r1(X,Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y))))))))&(![X]:(~r1(Y,X)|((~p9(X)|p8(X))&(p9(X)|~p8(X))))))))&(![Y]:(~r1(X,Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y))))))))&(![X]:(~r1(Y,X)|((~p7(X)|p6(X))&(p7(X)|~p6(X))))))))&(![Y]:(~r1(X,Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y))))))))&(![X]:(~r1(Y,X)|((~p5(X)|p4(X))&(p5(X)|~p4(X))))))))&(![Y]:(~r1(X,Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y))))))))&(![X]:(~r1(Y,X)|((~p3(X)|p2(X))&(p3(X)|~p2(X)))))))&(![Y]:(~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(?[Y]:(r1(X,Y)&~p30(Y))))&(?[Y]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,Y)&(p28(Y)|p29(Y)))&(~p29(Y)|~p28(Y)))&(p27(Y)|p28(Y)))&(~p28(Y)|~p27(Y)))&(p26(Y)|p27(Y)))&(~p27(Y)|~p26(Y)))&(p25(Y)|p26(Y)))&(~p26(Y)|~p25(Y)))&(p24(Y)|p25(Y)))&(~p25(Y)|~p24(Y)))&(p23(Y)|p24(Y)))&(~p24(Y)|~p23(Y)))&(p22(Y)|p23(Y)))&(~p23(Y)|~p22(Y)))&(p21(Y)|p22(Y)))&(~p22(Y)|~p21(Y)))&(p20(Y)|p21(Y)))&(~p21(Y)|~p20(Y)))&(p19(Y)|p20(Y)))&(~p20(Y)|~p19(Y)))&(p18(Y)|p19(Y)))&(~p19(Y)|~p18(Y)))&(p17(Y)|p18(Y)))&(~p18(Y)|~p17(Y)))&(p16(Y)|p17(Y)))&(~p17(Y)|~p16(Y)))&(p15(Y)|p16(Y)))&(~p16(Y)|~p15(Y)))&(p14(Y)|p15(Y)))&(~p15(Y)|~p14(Y)))&(p13(Y)|p14(Y)))&(~p14(Y)|~p13(Y)))&(p12(Y)|p13(Y)))&(~p13(Y)|~p12(Y)))&(p11(Y)|p12(Y)))&(~p12(Y)|~p11(Y)))&(p10(Y)|p11(Y)))&(~p11(Y)|~p10(Y)))&(p9(Y)|p10(Y)))&(~p10(Y)|~p9(Y)))&(p8(Y)|p9(Y)))&(~p9(Y)|~p8(Y)))&(p7(Y)|p8(Y)))&(~p8(Y)|~p7(Y)))&(p6(Y)|p7(Y)))&(~p7(Y)|~p6(Y)))&(p5(Y)|p6(Y)))&(~p6(Y)|~p5(Y)))&(p4(Y)|p5(Y)))&(~p5(Y)|~p4(Y)))&(p3(Y)|p4(Y)))&(~p4(Y)|~p3(Y)))&(p2(Y)|p3(Y)))&(~p3(Y)|~p2(Y)))&(p1(Y)|p2(Y)))&(~p2(Y)|~p1(Y))))))))))),inference(fof_nnf,[status(thm)],[c1])).
% 5.05/5.31 fof(c3,negated_conjecture,(?[X2]:((?[X3]:((r1(X2,X3)&p30(X3))&(?[X4]:(r1(X3,X4)&p1(X4)))))&(?[X5]:(r1(X2,X5)&(![X6]:(~r1(X5,X6)|((((?[X7]:((r1(X6,X7)&(?[X8]:((r1(X7,X8)&(?[X9]:((r1(X8,X9)&(?[X10]:((r1(X9,X10)&(?[X11]:((r1(X10,X11)&(?[X12]:((r1(X11,X12)&(?[X13]:((r1(X12,X13)&(?[X14]:((r1(X13,X14)&(?[X15]:((r1(X14,X15)&(?[X16]:((r1(X15,X16)&(?[X17]:((r1(X16,X17)&(?[X18]:((r1(X17,X18)&(?[X19]:((r1(X18,X19)&(?[X20]:((r1(X19,X20)&(?[X21]:((r1(X20,X21)&(?[X22]:((r1(X21,X22)&(?[X23]:((r1(X22,X23)&(?[X24]:((r1(X23,X24)&(?[X25]:((r1(X24,X25)&(?[X26]:((r1(X25,X26)&(?[X27]:((r1(X26,X27)&(?[X28]:((r1(X27,X28)&(?[X29]:((r1(X28,X29)&(?[X30]:((r1(X29,X30)&(?[X31]:((r1(X30,X31)&(?[X32]:((r1(X31,X32)&(?[X33]:((r1(X32,X33)&(?[X34]:r1(X33,X34)))&(![X35]:(~r1(X33,X35)|((~p29(X35)|p28(X35))&(p29(X35)|~p28(X35))))))))&(![X36]:(~r1(X32,X36)|((~p28(X36)|p27(X36))&(p28(X36)|~p27(X36))))))))&(![X37]:(~r1(X31,X37)|((~p27(X37)|p26(X37))&(p27(X37)|~p26(X37))))))))&(![X38]:(~r1(X30,X38)|((~p26(X38)|p25(X38))&(p26(X38)|~p25(X38))))))))&(![X39]:(~r1(X29,X39)|((~p25(X39)|p24(X39))&(p25(X39)|~p24(X39))))))))&(![X40]:(~r1(X28,X40)|((~p24(X40)|p23(X40))&(p24(X40)|~p23(X40))))))))&(![X41]:(~r1(X27,X41)|((~p23(X41)|p22(X41))&(p23(X41)|~p22(X41))))))))&(![X42]:(~r1(X26,X42)|((~p22(X42)|p21(X42))&(p22(X42)|~p21(X42))))))))&(![X43]:(~r1(X25,X43)|((~p21(X43)|p20(X43))&(p21(X43)|~p20(X43))))))))&(![X44]:(~r1(X24,X44)|((~p20(X44)|p19(X44))&(p20(X44)|~p19(X44))))))))&(![X45]:(~r1(X23,X45)|((~p19(X45)|p18(X45))&(p19(X45)|~p18(X45))))))))&(![X46]:(~r1(X22,X46)|((~p18(X46)|p17(X46))&(p18(X46)|~p17(X46))))))))&(![X47]:(~r1(X21,X47)|((~p17(X47)|p16(X47))&(p17(X47)|~p16(X47))))))))&(![X48]:(~r1(X20,X48)|((~p16(X48)|p15(X48))&(p16(X48)|~p15(X48))))))))&(![X49]:(~r1(X19,X49)|((~p15(X49)|p14(X49))&(p15(X49)|~p14(X49))))))))&(![X50]:(~r1(X18,X50)|((~p14(X50)|p13(X50))&(p14(X50)|~p13(X50))))))))&(![X51]:(~r1(X17,X51)|((~p13(X51)|p12(X51))&(p13(X51)|~p12(X51))))))))&(![X52]:(~r1(X16,X52)|((~p12(X52)|p11(X52))&(p12(X52)|~p11(X52))))))))&(![X53]:(~r1(X15,X53)|((~p11(X53)|p10(X53))&(p11(X53)|~p10(X53))))))))&(![X54]:(~r1(X14,X54)|((~p10(X54)|p9(X54))&(p10(X54)|~p9(X54))))))))&(![X55]:(~r1(X13,X55)|((~p9(X55)|p8(X55))&(p9(X55)|~p8(X55))))))))&(![X56]:(~r1(X12,X56)|((~p8(X56)|p7(X56))&(p8(X56)|~p7(X56))))))))&(![X57]:(~r1(X11,X57)|((~p7(X57)|p6(X57))&(p7(X57)|~p6(X57))))))))&(![X58]:(~r1(X10,X58)|((~p6(X58)|p5(X58))&(p6(X58)|~p5(X58))))))))&(![X59]:(~r1(X9,X59)|((~p5(X59)|p4(X59))&(p5(X59)|~p4(X59))))))))&(![X60]:(~r1(X8,X60)|((~p4(X60)|p3(X60))&(p4(X60)|~p3(X60))))))))&(![X61]:(~r1(X7,X61)|((~p3(X61)|p2(X61))&(p3(X61)|~p2(X61)))))))&(![X62]:(~r1(X6,X62)|((~p2(X62)|p1(X62))&(p2(X62)|~p1(X62))))))&(?[X63]:(r1(X6,X63)&~p30(X63))))&(?[X64]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X6,X64)&(p28(X64)|p29(X64)))&(~p29(X64)|~p28(X64)))&(p27(X64)|p28(X64)))&(~p28(X64)|~p27(X64)))&(p26(X64)|p27(X64)))&(~p27(X64)|~p26(X64)))&(p25(X64)|p26(X64)))&(~p26(X64)|~p25(X64)))&(p24(X64)|p25(X64)))&(~p25(X64)|~p24(X64)))&(p23(X64)|p24(X64)))&(~p24(X64)|~p23(X64)))&(p22(X64)|p23(X64)))&(~p23(X64)|~p22(X64)))&(p21(X64)|p22(X64)))&(~p22(X64)|~p21(X64)))&(p20(X64)|p21(X64)))&(~p21(X64)|~p20(X64)))&(p19(X64)|p20(X64)))&(~p20(X64)|~p19(X64)))&(p18(X64)|p19(X64)))&(~p19(X64)|~p18(X64)))&(p17(X64)|p18(X64)))&(~p18(X64)|~p17(X64)))&(p16(X64)|p17(X64)))&(~p17(X64)|~p16(X64)))&(p15(X64)|p16(X64)))&(~p16(X64)|~p15(X64)))&(p14(X64)|p15(X64)))&(~p15(X64)|~p14(X64)))&(p13(X64)|p14(X64)))&(~p14(X64)|~p13(X64)))&(p12(X64)|p13(X64)))&(~p13(X64)|~p12(X64)))&(p11(X64)|p12(X64)))&(~p12(X64)|~p11(X64)))&(p10(X64)|p11(X64)))&(~p11(X64)|~p10(X64)))&(p9(X64)|p10(X64)))&(~p10(X64)|~p9(X64)))&(p8(X64)|p9(X64)))&(~p9(X64)|~p8(X64)))&(p7(X64)|p8(X64)))&(~p8(X64)|~p7(X64)))&(p6(X64)|p7(X64)))&(~p7(X64)|~p6(X64)))&(p5(X64)|p6(X64)))&(~p6(X64)|~p5(X64)))&(p4(X64)|p5(X64)))&(~p5(X64)|~p4(X64)))&(p3(X64)|p4(X64)))&(~p4(X64)|~p3(X64)))&(p2(X64)|p3(X64)))&(~p3(X64)|~p2(X64)))&(p1(X64)|p2(X64)))&(~p2(X64)|~p1(X64))))))))))),inference(variable_rename,[status(thm)],[c2])).
% 5.05/5.31 fof(c5,negated_conjecture,(![X6]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(![X62]:(((r1(skolem0001,skolem0002)&p30(skolem0002))&(r1(skolem0002,skolem0003)&p1(skolem0003)))&(r1(skolem0001,skolem0004)&(~r1(skolem0004,X6)|(((((r1(X6,skolem0005(X6))&((r1(skolem0005(X6),skolem0006(X6))&((r1(skolem0006(X6),skolem0007(X6))&((r1(skolem0007(X6),skolem0008(X6))&((r1(skolem0008(X6),skolem0009(X6))&((r1(skolem0009(X6),skolem0010(X6))&((r1(skolem0010(X6),skolem0011(X6))&((r1(skolem0011(X6),skolem0012(X6))&((r1(skolem0012(X6),skolem0013(X6))&((r1(skolem0013(X6),skolem0014(X6))&((r1(skolem0014(X6),skolem0015(X6))&((r1(skolem0015(X6),skolem0016(X6))&((r1(skolem0016(X6),skolem0017(X6))&((r1(skolem0017(X6),skolem0018(X6))&((r1(skolem0018(X6),skolem0019(X6))&((r1(skolem0019(X6),skolem0020(X6))&((r1(skolem0020(X6),skolem0021(X6))&((r1(skolem0021(X6),skolem0022(X6))&((r1(skolem0022(X6),skolem0023(X6))&((r1(skolem0023(X6),skolem0024(X6))&((r1(skolem0024(X6),skolem0025(X6))&((r1(skolem0025(X6),skolem0026(X6))&((r1(skolem0026(X6),skolem0027(X6))&((r1(skolem0027(X6),skolem0028(X6))&((r1(skolem0028(X6),skolem0029(X6))&((r1(skolem0029(X6),skolem0030(X6))&((r1(skolem0030(X6),skolem0031(X6))&r1(skolem0031(X6),skolem0032(X6)))&(~r1(skolem0031(X6),X35)|((~p29(X35)|p28(X35))&(p29(X35)|~p28(X35))))))&(~r1(skolem0030(X6),X36)|((~p28(X36)|p27(X36))&(p28(X36)|~p27(X36))))))&(~r1(skolem0029(X6),X37)|((~p27(X37)|p26(X37))&(p27(X37)|~p26(X37))))))&(~r1(skolem0028(X6),X38)|((~p26(X38)|p25(X38))&(p26(X38)|~p25(X38))))))&(~r1(skolem0027(X6),X39)|((~p25(X39)|p24(X39))&(p25(X39)|~p24(X39))))))&(~r1(skolem0026(X6),X40)|((~p24(X40)|p23(X40))&(p24(X40)|~p23(X40))))))&(~r1(skolem0025(X6),X41)|((~p23(X41)|p22(X41))&(p23(X41)|~p22(X41))))))&(~r1(skolem0024(X6),X42)|((~p22(X42)|p21(X42))&(p22(X42)|~p21(X42))))))&(~r1(skolem0023(X6),X43)|((~p21(X43)|p20(X43))&(p21(X43)|~p20(X43))))))&(~r1(skolem0022(X6),X44)|((~p20(X44)|p19(X44))&(p20(X44)|~p19(X44))))))&(~r1(skolem0021(X6),X45)|((~p19(X45)|p18(X45))&(p19(X45)|~p18(X45))))))&(~r1(skolem0020(X6),X46)|((~p18(X46)|p17(X46))&(p18(X46)|~p17(X46))))))&(~r1(skolem0019(X6),X47)|((~p17(X47)|p16(X47))&(p17(X47)|~p16(X47))))))&(~r1(skolem0018(X6),X48)|((~p16(X48)|p15(X48))&(p16(X48)|~p15(X48))))))&(~r1(skolem0017(X6),X49)|((~p15(X49)|p14(X49))&(p15(X49)|~p14(X49))))))&(~r1(skolem0016(X6),X50)|((~p14(X50)|p13(X50))&(p14(X50)|~p13(X50))))))&(~r1(skolem0015(X6),X51)|((~p13(X51)|p12(X51))&(p13(X51)|~p12(X51))))))&(~r1(skolem0014(X6),X52)|((~p12(X52)|p11(X52))&(p12(X52)|~p11(X52))))))&(~r1(skolem0013(X6),X53)|((~p11(X53)|p10(X53))&(p11(X53)|~p10(X53))))))&(~r1(skolem0012(X6),X54)|((~p10(X54)|p9(X54))&(p10(X54)|~p9(X54))))))&(~r1(skolem0011(X6),X55)|((~p9(X55)|p8(X55))&(p9(X55)|~p8(X55))))))&(~r1(skolem0010(X6),X56)|((~p8(X56)|p7(X56))&(p8(X56)|~p7(X56))))))&(~r1(skolem0009(X6),X57)|((~p7(X57)|p6(X57))&(p7(X57)|~p6(X57))))))&(~r1(skolem0008(X6),X58)|((~p6(X58)|p5(X58))&(p6(X58)|~p5(X58))))))&(~r1(skolem0007(X6),X59)|((~p5(X59)|p4(X59))&(p5(X59)|~p4(X59))))))&(~r1(skolem0006(X6),X60)|((~p4(X60)|p3(X60))&(p4(X60)|~p3(X60))))))&(~r1(skolem0005(X6),X61)|((~p3(X61)|p2(X61))&(p3(X61)|~p2(X61)))))&(~r1(X6,X62)|((~p2(X62)|p1(X62))&(p2(X62)|~p1(X62)))))&(r1(X6,skolem0033(X6))&~p30(skolem0033(X6))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X6,skolem0034(X6))&(p28(skolem0034(X6))|p29(skolem0034(X6))))&(~p29(skolem0034(X6))|~p28(skolem0034(X6))))&(p27(skolem0034(X6))|p28(skolem0034(X6))))&(~p28(skolem0034(X6))|~p27(skolem0034(X6))))&(p26(skolem0034(X6))|p27(skolem0034(X6))))&(~p27(skolem0034(X6))|~p26(skolem0034(X6))))&(p25(skolem0034(X6))|p26(skolem0034(X6))))&(~p26(skolem0034(X6))|~p25(skolem0034(X6))))&(p24(skolem0034(X6))|p25(skolem0034(X6))))&(~p25(skolem0034(X6))|~p24(skolem0034(X6))))&(p23(skolem0034(X6))|p24(skolem0034(X6))))&(~p24(skolem0034(X6))|~p23(skolem0034(X6))))&(p22(skolem0034(X6))|p23(skolem0034(X6))))&(~p23(skolem0034(X6))|~p22(skolem0034(X6))))&(p21(skolem0034(X6))|p22(skolem0034(X6))))&(~p22(skolem0034(X6))|~p21(skolem0034(X6))))&(p20(skolem0034(X6))|p21(skolem0034(X6))))&(~p21(skolem0034(X6))|~p20(skolem0034(X6))))&(p19(skolem0034(X6))|p20(skolem0034(X6))))&(~p20(skolem0034(X6))|~p19(skolem0034(X6))))&(p18(skolem0034(X6))|p19(skolem0034(X6))))&(~p19(skolem0034(X6))|~p18(skolem0034(X6))))&(p17(skolem0034(X6))|p18(skolem0034(X6))))&(~p18(skolem0034(X6))|~p17(skolem0034(X6))))&(p16(skolem0034(X6))|p17(skolem0034(X6))))&(~p17(skolem0034(X6))|~p16(skolem0034(X6))))&(p15(skolem0034(X6))|p16(skolem0034(X6))))&(~p16(skolem0034(X6))|~p15(skolem0034(X6))))&(p14(skolem0034(X6))|p15(skolem0034(X6))))&(~p15(skolem0034(X6))|~p14(skolem0034(X6))))&(p13(skolem0034(X6))|p14(skolem0034(X6))))&(~p14(skolem0034(X6))|~p13(skolem0034(X6))))&(p12(skolem0034(X6))|p13(skolem0034(X6))))&(~p13(skolem0034(X6))|~p12(skolem0034(X6))))&(p11(skolem0034(X6))|p12(skolem0034(X6))))&(~p12(skolem0034(X6))|~p11(skolem0034(X6))))&(p10(skolem0034(X6))|p11(skolem0034(X6))))&(~p11(skolem0034(X6))|~p10(skolem0034(X6))))&(p9(skolem0034(X6))|p10(skolem0034(X6))))&(~p10(skolem0034(X6))|~p9(skolem0034(X6))))&(p8(skolem0034(X6))|p9(skolem0034(X6))))&(~p9(skolem0034(X6))|~p8(skolem0034(X6))))&(p7(skolem0034(X6))|p8(skolem0034(X6))))&(~p8(skolem0034(X6))|~p7(skolem0034(X6))))&(p6(skolem0034(X6))|p7(skolem0034(X6))))&(~p7(skolem0034(X6))|~p6(skolem0034(X6))))&(p5(skolem0034(X6))|p6(skolem0034(X6))))&(~p6(skolem0034(X6))|~p5(skolem0034(X6))))&(p4(skolem0034(X6))|p5(skolem0034(X6))))&(~p5(skolem0034(X6))|~p4(skolem0034(X6))))&(p3(skolem0034(X6))|p4(skolem0034(X6))))&(~p4(skolem0034(X6))|~p3(skolem0034(X6))))&(p2(skolem0034(X6))|p3(skolem0034(X6))))&(~p3(skolem0034(X6))|~p2(skolem0034(X6))))&(p1(skolem0034(X6))|p2(skolem0034(X6))))&(~p2(skolem0034(X6))|~p1(skolem0034(X6))))))))))))))))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,(((r1(skolem0001,skolem0002)&p30(skolem0002))&(r1(skolem0002,skolem0003)&p1(skolem0003)))&(r1(skolem0001,skolem0004)&(![X6]:(~r1(skolem0004,X6)|(((((r1(X6,skolem0005(X6))&((r1(skolem0005(X6),skolem0006(X6))&((r1(skolem0006(X6),skolem0007(X6))&((r1(skolem0007(X6),skolem0008(X6))&((r1(skolem0008(X6),skolem0009(X6))&((r1(skolem0009(X6),skolem0010(X6))&((r1(skolem0010(X6),skolem0011(X6))&((r1(skolem0011(X6),skolem0012(X6))&((r1(skolem0012(X6),skolem0013(X6))&((r1(skolem0013(X6),skolem0014(X6))&((r1(skolem0014(X6),skolem0015(X6))&((r1(skolem0015(X6),skolem0016(X6))&((r1(skolem0016(X6),skolem0017(X6))&((r1(skolem0017(X6),skolem0018(X6))&((r1(skolem0018(X6),skolem0019(X6))&((r1(skolem0019(X6),skolem0020(X6))&((r1(skolem0020(X6),skolem0021(X6))&((r1(skolem0021(X6),skolem0022(X6))&((r1(skolem0022(X6),skolem0023(X6))&((r1(skolem0023(X6),skolem0024(X6))&((r1(skolem0024(X6),skolem0025(X6))&((r1(skolem0025(X6),skolem0026(X6))&((r1(skolem0026(X6),skolem0027(X6))&((r1(skolem0027(X6),skolem0028(X6))&((r1(skolem0028(X6),skolem0029(X6))&((r1(skolem0029(X6),skolem0030(X6))&((r1(skolem0030(X6),skolem0031(X6))&r1(skolem0031(X6),skolem0032(X6)))&(![X35]:(~r1(skolem0031(X6),X35)|((~p29(X35)|p28(X35))&(p29(X35)|~p28(X35)))))))&(![X36]:(~r1(skolem0030(X6),X36)|((~p28(X36)|p27(X36))&(p28(X36)|~p27(X36)))))))&(![X37]:(~r1(skolem0029(X6),X37)|((~p27(X37)|p26(X37))&(p27(X37)|~p26(X37)))))))&(![X38]:(~r1(skolem0028(X6),X38)|((~p26(X38)|p25(X38))&(p26(X38)|~p25(X38)))))))&(![X39]:(~r1(skolem0027(X6),X39)|((~p25(X39)|p24(X39))&(p25(X39)|~p24(X39)))))))&(![X40]:(~r1(skolem0026(X6),X40)|((~p24(X40)|p23(X40))&(p24(X40)|~p23(X40)))))))&(![X41]:(~r1(skolem0025(X6),X41)|((~p23(X41)|p22(X41))&(p23(X41)|~p22(X41)))))))&(![X42]:(~r1(skolem0024(X6),X42)|((~p22(X42)|p21(X42))&(p22(X42)|~p21(X42)))))))&(![X43]:(~r1(skolem0023(X6),X43)|((~p21(X43)|p20(X43))&(p21(X43)|~p20(X43)))))))&(![X44]:(~r1(skolem0022(X6),X44)|((~p20(X44)|p19(X44))&(p20(X44)|~p19(X44)))))))&(![X45]:(~r1(skolem0021(X6),X45)|((~p19(X45)|p18(X45))&(p19(X45)|~p18(X45)))))))&(![X46]:(~r1(skolem0020(X6),X46)|((~p18(X46)|p17(X46))&(p18(X46)|~p17(X46)))))))&(![X47]:(~r1(skolem0019(X6),X47)|((~p17(X47)|p16(X47))&(p17(X47)|~p16(X47)))))))&(![X48]:(~r1(skolem0018(X6),X48)|((~p16(X48)|p15(X48))&(p16(X48)|~p15(X48)))))))&(![X49]:(~r1(skolem0017(X6),X49)|((~p15(X49)|p14(X49))&(p15(X49)|~p14(X49)))))))&(![X50]:(~r1(skolem0016(X6),X50)|((~p14(X50)|p13(X50))&(p14(X50)|~p13(X50)))))))&(![X51]:(~r1(skolem0015(X6),X51)|((~p13(X51)|p12(X51))&(p13(X51)|~p12(X51)))))))&(![X52]:(~r1(skolem0014(X6),X52)|((~p12(X52)|p11(X52))&(p12(X52)|~p11(X52)))))))&(![X53]:(~r1(skolem0013(X6),X53)|((~p11(X53)|p10(X53))&(p11(X53)|~p10(X53)))))))&(![X54]:(~r1(skolem0012(X6),X54)|((~p10(X54)|p9(X54))&(p10(X54)|~p9(X54)))))))&(![X55]:(~r1(skolem0011(X6),X55)|((~p9(X55)|p8(X55))&(p9(X55)|~p8(X55)))))))&(![X56]:(~r1(skolem0010(X6),X56)|((~p8(X56)|p7(X56))&(p8(X56)|~p7(X56)))))))&(![X57]:(~r1(skolem0009(X6),X57)|((~p7(X57)|p6(X57))&(p7(X57)|~p6(X57)))))))&(![X58]:(~r1(skolem0008(X6),X58)|((~p6(X58)|p5(X58))&(p6(X58)|~p5(X58)))))))&(![X59]:(~r1(skolem0007(X6),X59)|((~p5(X59)|p4(X59))&(p5(X59)|~p4(X59)))))))&(![X60]:(~r1(skolem0006(X6),X60)|((~p4(X60)|p3(X60))&(p4(X60)|~p3(X60)))))))&(![X61]:(~r1(skolem0005(X6),X61)|((~p3(X61)|p2(X61))&(p3(X61)|~p2(X61))))))&(![X62]:(~r1(X6,X62)|((~p2(X62)|p1(X62))&(p2(X62)|~p1(X62))))))&(r1(X6,skolem0033(X6))&~p30(skolem0033(X6))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X6,skolem0034(X6))&(p28(skolem0034(X6))|p29(skolem0034(X6))))&(~p29(skolem0034(X6))|~p28(skolem0034(X6))))&(p27(skolem0034(X6))|p28(skolem0034(X6))))&(~p28(skolem0034(X6))|~p27(skolem0034(X6))))&(p26(skolem0034(X6))|p27(skolem0034(X6))))&(~p27(skolem0034(X6))|~p26(skolem0034(X6))))&(p25(skolem0034(X6))|p26(skolem0034(X6))))&(~p26(skolem0034(X6))|~p25(skolem0034(X6))))&(p24(skolem0034(X6))|p25(skolem0034(X6))))&(~p25(skolem0034(X6))|~p24(skolem0034(X6))))&(p23(skolem0034(X6))|p24(skolem0034(X6))))&(~p24(skolem0034(X6))|~p23(skolem0034(X6))))&(p22(skolem0034(X6))|p23(skolem0034(X6))))&(~p23(skolem0034(X6))|~p22(skolem0034(X6))))&(p21(skolem0034(X6))|p22(skolem0034(X6))))&(~p22(skolem0034(X6))|~p21(skolem0034(X6))))&(p20(skolem0034(X6))|p21(skolem0034(X6))))&(~p21(skolem0034(X6))|~p20(skolem0034(X6))))&(p19(skolem0034(X6))|p20(skolem0034(X6))))&(~p20(skolem0034(X6))|~p19(skolem0034(X6))))&(p18(skolem0034(X6))|p19(skolem0034(X6))))&(~p19(skolem0034(X6))|~p18(skolem0034(X6))))&(p17(skolem0034(X6))|p18(skolem0034(X6))))&(~p18(skolem0034(X6))|~p17(skolem0034(X6))))&(p16(skolem0034(X6))|p17(skolem0034(X6))))&(~p17(skolem0034(X6))|~p16(skolem0034(X6))))&(p15(skolem0034(X6))|p16(skolem0034(X6))))&(~p16(skolem0034(X6))|~p15(skolem0034(X6))))&(p14(skolem0034(X6))|p15(skolem0034(X6))))&(~p15(skolem0034(X6))|~p14(skolem0034(X6))))&(p13(skolem0034(X6))|p14(skolem0034(X6))))&(~p14(skolem0034(X6))|~p13(skolem0034(X6))))&(p12(skolem0034(X6))|p13(skolem0034(X6))))&(~p13(skolem0034(X6))|~p12(skolem0034(X6))))&(p11(skolem0034(X6))|p12(skolem0034(X6))))&(~p12(skolem0034(X6))|~p11(skolem0034(X6))))&(p10(skolem0034(X6))|p11(skolem0034(X6))))&(~p11(skolem0034(X6))|~p10(skolem0034(X6))))&(p9(skolem0034(X6))|p10(skolem0034(X6))))&(~p10(skolem0034(X6))|~p9(skolem0034(X6))))&(p8(skolem0034(X6))|p9(skolem0034(X6))))&(~p9(skolem0034(X6))|~p8(skolem0034(X6))))&(p7(skolem0034(X6))|p8(skolem0034(X6))))&(~p8(skolem0034(X6))|~p7(skolem0034(X6))))&(p6(skolem0034(X6))|p7(skolem0034(X6))))&(~p7(skolem0034(X6))|~p6(skolem0034(X6))))&(p5(skolem0034(X6))|p6(skolem0034(X6))))&(~p6(skolem0034(X6))|~p5(skolem0034(X6))))&(p4(skolem0034(X6))|p5(skolem0034(X6))))&(~p5(skolem0034(X6))|~p4(skolem0034(X6))))&(p3(skolem0034(X6))|p4(skolem0034(X6))))&(~p4(skolem0034(X6))|~p3(skolem0034(X6))))&(p2(skolem0034(X6))|p3(skolem0034(X6))))&(~p3(skolem0034(X6))|~p2(skolem0034(X6))))&(p1(skolem0034(X6))|p2(skolem0034(X6))))&(~p2(skolem0034(X6))|~p1(skolem0034(X6))))))))),inference(skolemize,[status(esa)],[c3])).])).
% 5.05/5.32 fof(c6,negated_conjecture,(![X6]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(![X62]:(((r1(skolem0001,skolem0002)&p30(skolem0002))&(r1(skolem0002,skolem0003)&p1(skolem0003)))&(r1(skolem0001,skolem0004)&((((((~r1(skolem0004,X6)|r1(X6,skolem0005(X6)))&(((~r1(skolem0004,X6)|r1(skolem0005(X6),skolem0006(X6)))&(((~r1(skolem0004,X6)|r1(skolem0006(X6),skolem0007(X6)))&(((~r1(skolem0004,X6)|r1(skolem0007(X6),skolem0008(X6)))&(((~r1(skolem0004,X6)|r1(skolem0008(X6),skolem0009(X6)))&(((~r1(skolem0004,X6)|r1(skolem0009(X6),skolem0010(X6)))&(((~r1(skolem0004,X6)|r1(skolem0010(X6),skolem0011(X6)))&(((~r1(skolem0004,X6)|r1(skolem0011(X6),skolem0012(X6)))&(((~r1(skolem0004,X6)|r1(skolem0012(X6),skolem0013(X6)))&(((~r1(skolem0004,X6)|r1(skolem0013(X6),skolem0014(X6)))&(((~r1(skolem0004,X6)|r1(skolem0014(X6),skolem0015(X6)))&(((~r1(skolem0004,X6)|r1(skolem0015(X6),skolem0016(X6)))&(((~r1(skolem0004,X6)|r1(skolem0016(X6),skolem0017(X6)))&(((~r1(skolem0004,X6)|r1(skolem0017(X6),skolem0018(X6)))&(((~r1(skolem0004,X6)|r1(skolem0018(X6),skolem0019(X6)))&(((~r1(skolem0004,X6)|r1(skolem0019(X6),skolem0020(X6)))&(((~r1(skolem0004,X6)|r1(skolem0020(X6),skolem0021(X6)))&(((~r1(skolem0004,X6)|r1(skolem0021(X6),skolem0022(X6)))&(((~r1(skolem0004,X6)|r1(skolem0022(X6),skolem0023(X6)))&(((~r1(skolem0004,X6)|r1(skolem0023(X6),skolem0024(X6)))&(((~r1(skolem0004,X6)|r1(skolem0024(X6),skolem0025(X6)))&(((~r1(skolem0004,X6)|r1(skolem0025(X6),skolem0026(X6)))&(((~r1(skolem0004,X6)|r1(skolem0026(X6),skolem0027(X6)))&(((~r1(skolem0004,X6)|r1(skolem0027(X6),skolem0028(X6)))&(((~r1(skolem0004,X6)|r1(skolem0028(X6),skolem0029(X6)))&(((~r1(skolem0004,X6)|r1(skolem0029(X6),skolem0030(X6)))&(((~r1(skolem0004,X6)|r1(skolem0030(X6),skolem0031(X6)))&(~r1(skolem0004,X6)|r1(skolem0031(X6),skolem0032(X6))))&((~r1(skolem0004,X6)|(~r1(skolem0031(X6),X35)|(~p29(X35)|p28(X35))))&(~r1(skolem0004,X6)|(~r1(skolem0031(X6),X35)|(p29(X35)|~p28(X35)))))))&((~r1(skolem0004,X6)|(~r1(skolem0030(X6),X36)|(~p28(X36)|p27(X36))))&(~r1(skolem0004,X6)|(~r1(skolem0030(X6),X36)|(p28(X36)|~p27(X36)))))))&((~r1(skolem0004,X6)|(~r1(skolem0029(X6),X37)|(~p27(X37)|p26(X37))))&(~r1(skolem0004,X6)|(~r1(skolem0029(X6),X37)|(p27(X37)|~p26(X37)))))))&((~r1(skolem0004,X6)|(~r1(skolem0028(X6),X38)|(~p26(X38)|p25(X38))))&(~r1(skolem0004,X6)|(~r1(skolem0028(X6),X38)|(p26(X38)|~p25(X38)))))))&((~r1(skolem0004,X6)|(~r1(skolem0027(X6),X39)|(~p25(X39)|p24(X39))))&(~r1(skolem0004,X6)|(~r1(skolem0027(X6),X39)|(p25(X39)|~p24(X39)))))))&((~r1(skolem0004,X6)|(~r1(skolem0026(X6),X40)|(~p24(X40)|p23(X40))))&(~r1(skolem0004,X6)|(~r1(skolem0026(X6),X40)|(p24(X40)|~p23(X40)))))))&((~r1(skolem0004,X6)|(~r1(skolem0025(X6),X41)|(~p23(X41)|p22(X41))))&(~r1(skolem0004,X6)|(~r1(skolem0025(X6),X41)|(p23(X41)|~p22(X41)))))))&((~r1(skolem0004,X6)|(~r1(skolem0024(X6),X42)|(~p22(X42)|p21(X42))))&(~r1(skolem0004,X6)|(~r1(skolem0024(X6),X42)|(p22(X42)|~p21(X42)))))))&((~r1(skolem0004,X6)|(~r1(skolem0023(X6),X43)|(~p21(X43)|p20(X43))))&(~r1(skolem0004,X6)|(~r1(skolem0023(X6),X43)|(p21(X43)|~p20(X43)))))))&((~r1(skolem0004,X6)|(~r1(skolem0022(X6),X44)|(~p20(X44)|p19(X44))))&(~r1(skolem0004,X6)|(~r1(skolem0022(X6),X44)|(p20(X44)|~p19(X44)))))))&((~r1(skolem0004,X6)|(~r1(skolem0021(X6),X45)|(~p19(X45)|p18(X45))))&(~r1(skolem0004,X6)|(~r1(skolem0021(X6),X45)|(p19(X45)|~p18(X45)))))))&((~r1(skolem0004,X6)|(~r1(skolem0020(X6),X46)|(~p18(X46)|p17(X46))))&(~r1(skolem0004,X6)|(~r1(skolem0020(X6),X46)|(p18(X46)|~p17(X46)))))))&((~r1(skolem0004,X6)|(~r1(skolem0019(X6),X47)|(~p17(X47)|p16(X47))))&(~r1(skolem0004,X6)|(~r1(skolem0019(X6),X47)|(p17(X47)|~p16(X47)))))))&((~r1(skolem0004,X6)|(~r1(skolem0018(X6),X48)|(~p16(X48)|p15(X48))))&(~r1(skolem0004,X6)|(~r1(skolem0018(X6),X48)|(p16(X48)|~p15(X48)))))))&((~r1(skolem0004,X6)|(~r1(skolem0017(X6),X49)|(~p15(X49)|p14(X49))))&(~r1(skolem0004,X6)|(~r1(skolem0017(X6),X49)|(p15(X49)|~p14(X49)))))))&((~r1(skolem0004,X6)|(~r1(skolem0016(X6),X50)|(~p14(X50)|p13(X50))))&(~r1(skolem0004,X6)|(~r1(skolem0016(X6),X50)|(p14(X50)|~p13(X50)))))))&((~r1(skolem0004,X6)|(~r1(skolem0015(X6),X51)|(~p13(X51)|p12(X51))))&(~r1(skolem0004,X6)|(~r1(skolem0015(X6),X51)|(p13(X51)|~p12(X51)))))))&((~r1(skolem0004,X6)|(~r1(skolem0014(X6),X52)|(~p12(X52)|p11(X52))))&(~r1(skolem0004,X6)|(~r1(skolem0014(X6),X52)|(p12(X52)|~p11(X52)))))))&((~r1(skolem0004,X6)|(~r1(skolem0013(X6),X53)|(~p11(X53)|p10(X53))))&(~r1(skolem0004,X6)|(~r1(skolem0013(X6),X53)|(p11(X53)|~p10(X53)))))))&((~r1(skolem0004,X6)|(~r1(skolem0012(X6),X54)|(~p10(X54)|p9(X54))))&(~r1(skolem0004,X6)|(~r1(skolem0012(X6),X54)|(p10(X54)|~p9(X54)))))))&((~r1(skolem0004,X6)|(~r1(skolem0011(X6),X55)|(~p9(X55)|p8(X55))))&(~r1(skolem0004,X6)|(~r1(skolem0011(X6),X55)|(p9(X55)|~p8(X55)))))))&((~r1(skolem0004,X6)|(~r1(skolem0010(X6),X56)|(~p8(X56)|p7(X56))))&(~r1(skolem0004,X6)|(~r1(skolem0010(X6),X56)|(p8(X56)|~p7(X56)))))))&((~r1(skolem0004,X6)|(~r1(skolem0009(X6),X57)|(~p7(X57)|p6(X57))))&(~r1(skolem0004,X6)|(~r1(skolem0009(X6),X57)|(p7(X57)|~p6(X57)))))))&((~r1(skolem0004,X6)|(~r1(skolem0008(X6),X58)|(~p6(X58)|p5(X58))))&(~r1(skolem0004,X6)|(~r1(skolem0008(X6),X58)|(p6(X58)|~p5(X58)))))))&((~r1(skolem0004,X6)|(~r1(skolem0007(X6),X59)|(~p5(X59)|p4(X59))))&(~r1(skolem0004,X6)|(~r1(skolem0007(X6),X59)|(p5(X59)|~p4(X59)))))))&((~r1(skolem0004,X6)|(~r1(skolem0006(X6),X60)|(~p4(X60)|p3(X60))))&(~r1(skolem0004,X6)|(~r1(skolem0006(X6),X60)|(p4(X60)|~p3(X60)))))))&((~r1(skolem0004,X6)|(~r1(skolem0005(X6),X61)|(~p3(X61)|p2(X61))))&(~r1(skolem0004,X6)|(~r1(skolem0005(X6),X61)|(p3(X61)|~p2(X61))))))&((~r1(skolem0004,X6)|(~r1(X6,X62)|(~p2(X62)|p1(X62))))&(~r1(skolem0004,X6)|(~r1(X6,X62)|(p2(X62)|~p1(X62))))))&((~r1(skolem0004,X6)|r1(X6,skolem0033(X6)))&(~r1(skolem0004,X6)|~p30(skolem0033(X6)))))&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((~r1(skolem0004,X6)|r1(X6,skolem0034(X6)))&(~r1(skolem0004,X6)|(p28(skolem0034(X6))|p29(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p29(skolem0034(X6))|~p28(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p27(skolem0034(X6))|p28(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p28(skolem0034(X6))|~p27(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p26(skolem0034(X6))|p27(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p27(skolem0034(X6))|~p26(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p25(skolem0034(X6))|p26(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p26(skolem0034(X6))|~p25(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p24(skolem0034(X6))|p25(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p25(skolem0034(X6))|~p24(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p23(skolem0034(X6))|p24(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p24(skolem0034(X6))|~p23(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p22(skolem0034(X6))|p23(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p23(skolem0034(X6))|~p22(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p21(skolem0034(X6))|p22(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p22(skolem0034(X6))|~p21(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p20(skolem0034(X6))|p21(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p21(skolem0034(X6))|~p20(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p19(skolem0034(X6))|p20(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p20(skolem0034(X6))|~p19(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p18(skolem0034(X6))|p19(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p19(skolem0034(X6))|~p18(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p17(skolem0034(X6))|p18(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p18(skolem0034(X6))|~p17(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p16(skolem0034(X6))|p17(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p17(skolem0034(X6))|~p16(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p15(skolem0034(X6))|p16(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p16(skolem0034(X6))|~p15(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p14(skolem0034(X6))|p15(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p15(skolem0034(X6))|~p14(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p13(skolem0034(X6))|p14(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p14(skolem0034(X6))|~p13(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p12(skolem0034(X6))|p13(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p13(skolem0034(X6))|~p12(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p11(skolem0034(X6))|p12(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p12(skolem0034(X6))|~p11(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p10(skolem0034(X6))|p11(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p11(skolem0034(X6))|~p10(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p9(skolem0034(X6))|p10(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p10(skolem0034(X6))|~p9(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p8(skolem0034(X6))|p9(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p9(skolem0034(X6))|~p8(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p7(skolem0034(X6))|p8(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p8(skolem0034(X6))|~p7(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p6(skolem0034(X6))|p7(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p7(skolem0034(X6))|~p6(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p5(skolem0034(X6))|p6(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p6(skolem0034(X6))|~p5(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p4(skolem0034(X6))|p5(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p5(skolem0034(X6))|~p4(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p3(skolem0034(X6))|p4(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p4(skolem0034(X6))|~p3(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p2(skolem0034(X6))|p3(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p3(skolem0034(X6))|~p2(skolem0034(X6)))))&(~r1(skolem0004,X6)|(p1(skolem0034(X6))|p2(skolem0034(X6)))))&(~r1(skolem0004,X6)|(~p2(skolem0034(X6))|~p1(skolem0034(X6))))))))))))))))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 5.05/5.32 cnf(c98,negated_conjecture,~r1(skolem0004,X74)|r1(X74,skolem0034(X74)),inference(split_conjunct,[status(thm)],[c6])).
% 5.05/5.32 cnf(c170,plain,r1(skolem0004,skolem0034(skolem0004)),inference(resolution,[status(thm)],[c98, c159])).
% 5.05/5.32 cnf(c95,negated_conjecture,~r1(skolem0004,X267)|~r1(X267,X268)|p2(X268)|~p1(X268),inference(split_conjunct,[status(thm)],[c6])).
% 5.05/5.32 cnf(c1962,plain,~r1(skolem0004,X269)|p2(X269)|~p1(X269),inference(resolution,[status(thm)],[c95, c159])).
% 5.05/5.32 cnf(c1989,plain,p2(skolem0034(skolem0004))|~p1(skolem0034(skolem0004)),inference(resolution,[status(thm)],[c1962, c170])).
% 5.05/5.32 cnf(c153,negated_conjecture,~r1(skolem0004,X343)|p1(skolem0034(X343))|p2(skolem0034(X343)),inference(split_conjunct,[status(thm)],[c6])).
% 5.05/5.32 cnf(c3858,plain,p1(skolem0034(skolem0004))|p2(skolem0034(skolem0004)),inference(resolution,[status(thm)],[c153, c159])).
% 5.05/5.32 cnf(c4045,plain,p2(skolem0034(skolem0004)),inference(resolution,[status(thm)],[c3858, c1989])).
% 5.05/5.32 cnf(c154,negated_conjecture,~r1(skolem0004,X345)|~p2(skolem0034(X345))|~p1(skolem0034(X345)),inference(split_conjunct,[status(thm)],[c6])).
% 5.05/5.32 cnf(c94,negated_conjecture,~r1(skolem0004,X264)|~r1(X264,X265)|~p2(X265)|p1(X265),inference(split_conjunct,[status(thm)],[c6])).
% 5.05/5.32 cnf(c1714,plain,~r1(skolem0004,X266)|~p2(X266)|p1(X266),inference(resolution,[status(thm)],[c94, c159])).
% 5.05/5.32 cnf(c1741,plain,~p2(skolem0034(skolem0004))|p1(skolem0034(skolem0004)),inference(resolution,[status(thm)],[c1714, c170])).
% 5.05/5.32 cnf(c4046,plain,p1(skolem0034(skolem0004)),inference(resolution,[status(thm)],[c3858, c1741])).
% 5.05/5.32 cnf(c4050,plain,~r1(skolem0004,skolem0004)|~p2(skolem0034(skolem0004)),inference(resolution,[status(thm)],[c4046, c154])).
% 5.05/5.32 cnf(c4190,plain,~r1(skolem0004,skolem0004),inference(resolution,[status(thm)],[c4050, c4045])).
% 5.05/5.32 cnf(c4194,plain,$false,inference(resolution,[status(thm)],[c4190, c159])).
% 5.05/5.32 % SZS output end CNFRefutation
% 5.05/5.32
% 5.05/5.32 % Initial clauses : 150
% 5.05/5.32 % Processed clauses : 709
% 5.05/5.32 % Factors computed : 3
% 5.05/5.32 % Resolvents computed: 4032
% 5.05/5.32 % Tautologies deleted: 2
% 5.05/5.32 % Forward subsumed : 94
% 5.05/5.32 % Backward subsumed : 6
% 5.05/5.32 % -------- CPU Time ---------
% 5.05/5.32 % User time : 4.827 s
% 5.05/5.32 % System time : 0.119 s
% 5.05/5.32 % Total time : 4.945 s
%------------------------------------------------------------------------------