%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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 10.34s 10.62s
% Output : CNFRefutation 10.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n027.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 : Fri Sep 4 19:18:57 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.42 (re.compile("\."), Token.FullStop),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.42 (re.compile("\("), Token.OpenPar),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.42 (re.compile("\)"), Token.ClosePar),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.42 (re.compile("\["), Token.OpenSquare),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.42 (re.compile("~\|"), Token.Nor),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.42 (re.compile("\|"), Token.Or),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.42 (re.compile("\?"), Token.Existential),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.42 (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.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.33/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.58 """
% 10.34/10.62 % Version: 1.5
% 10.34/10.62 % SZS status Theorem
% 10.34/10.62 % SZS output start CNFRefutation
% 10.34/10.62 fof(reflexivity,axiom,(![X]:r1(X,X)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 10.34/10.62 fof(c233,plain,(![X98]:r1(X98,X98)),inference(variable_rename,[status(thm)],[reflexivity])).
% 10.34/10.62 cnf(c234,plain,r1(X99,X99),inference(split_conjunct,[status(thm)],[c233])).
% 10.34/10.62 fof(main,conjecture,(~(?[X]:(~((![Y]:(((~r1(X,Y))|(~p45(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))|(![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))|$false)))|(~(![Y]:((~r1(X,Y))|(~((p44(Y)&(~p43(Y)))|((~p44(Y))&p43(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p43(X)&(~p42(X)))|((~p43(X))&p42(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p42(Y)&(~p41(Y)))|((~p42(Y))&p41(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p41(X)&(~p40(X)))|((~p41(X))&p40(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p40(Y)&(~p39(Y)))|((~p40(Y))&p39(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p39(X)&(~p38(X)))|((~p39(X))&p38(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p38(Y)&(~p37(Y)))|((~p38(Y))&p37(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p37(X)&(~p36(X)))|((~p37(X))&p36(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p36(Y)&(~p35(Y)))|((~p36(Y))&p35(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p35(X)&(~p34(X)))|((~p35(X))&p34(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p34(Y)&(~p33(Y)))|((~p34(Y))&p33(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p33(X)&(~p32(X)))|((~p33(X))&p32(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p32(Y)&(~p31(Y)))|((~p32(Y))&p31(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p31(X)&(~p30(X)))|((~p31(X))&p30(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p30(Y)&(~p29(Y)))|((~p30(Y))&p29(Y))))))))))|(~(![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))|p45(Y))))|(![Y]:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~r1(X,Y))|((~p43(Y))&(~p44(Y))))|(p44(Y)&p43(Y)))|((~p42(Y))&(~p43(Y))))|(p43(Y)&p42(Y)))|((~p41(Y))&(~p42(Y))))|(p42(Y)&p41(Y)))|((~p40(Y))&(~p41(Y))))|(p41(Y)&p40(Y)))|((~p39(Y))&(~p40(Y))))|(p40(Y)&p39(Y)))|((~p38(Y))&(~p39(Y))))|(p39(Y)&p38(Y)))|((~p37(Y))&(~p38(Y))))|(p38(Y)&p37(Y)))|((~p36(Y))&(~p37(Y))))|(p37(Y)&p36(Y)))|((~p35(Y))&(~p36(Y))))|(p36(Y)&p35(Y)))|((~p34(Y))&(~p35(Y))))|(p35(Y)&p34(Y)))|((~p33(Y))&(~p34(Y))))|(p34(Y)&p33(Y)))|((~p32(Y))&(~p33(Y))))|(p33(Y)&p32(Y)))|((~p31(Y))&(~p32(Y))))|(p32(Y)&p31(Y)))|((~p30(Y))&(~p31(Y))))|(p31(Y)&p30(Y)))|((~p29(Y))&(~p30(Y))))|(p30(Y)&p29(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)).
% 10.34/10.62 fof(c0,negated_conjecture,(~(~(?[X]:(~((![Y]:(((~r1(X,Y))|(~p45(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))|(![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))|$false)))|(~(![Y]:((~r1(X,Y))|(~((p44(Y)&(~p43(Y)))|((~p44(Y))&p43(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p43(X)&(~p42(X)))|((~p43(X))&p42(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p42(Y)&(~p41(Y)))|((~p42(Y))&p41(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p41(X)&(~p40(X)))|((~p41(X))&p40(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p40(Y)&(~p39(Y)))|((~p40(Y))&p39(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p39(X)&(~p38(X)))|((~p39(X))&p38(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p38(Y)&(~p37(Y)))|((~p38(Y))&p37(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p37(X)&(~p36(X)))|((~p37(X))&p36(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p36(Y)&(~p35(Y)))|((~p36(Y))&p35(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p35(X)&(~p34(X)))|((~p35(X))&p34(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p34(Y)&(~p33(Y)))|((~p34(Y))&p33(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p33(X)&(~p32(X)))|((~p33(X))&p32(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p32(Y)&(~p31(Y)))|((~p32(Y))&p31(Y))))))))))|(~(![X]:((~r1(Y,X))|(~((p31(X)&(~p30(X)))|((~p31(X))&p30(X))))))))))|(~(![Y]:((~r1(X,Y))|(~((p30(Y)&(~p29(Y)))|((~p30(Y))&p29(Y))))))))))|(~(![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))|p45(Y))))|(![Y]:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~r1(X,Y))|((~p43(Y))&(~p44(Y))))|(p44(Y)&p43(Y)))|((~p42(Y))&(~p43(Y))))|(p43(Y)&p42(Y)))|((~p41(Y))&(~p42(Y))))|(p42(Y)&p41(Y)))|((~p40(Y))&(~p41(Y))))|(p41(Y)&p40(Y)))|((~p39(Y))&(~p40(Y))))|(p40(Y)&p39(Y)))|((~p38(Y))&(~p39(Y))))|(p39(Y)&p38(Y)))|((~p37(Y))&(~p38(Y))))|(p38(Y)&p37(Y)))|((~p36(Y))&(~p37(Y))))|(p37(Y)&p36(Y)))|((~p35(Y))&(~p36(Y))))|(p36(Y)&p35(Y)))|((~p34(Y))&(~p35(Y))))|(p35(Y)&p34(Y)))|((~p33(Y))&(~p34(Y))))|(p34(Y)&p33(Y)))|((~p32(Y))&(~p33(Y))))|(p33(Y)&p32(Y)))|((~p31(Y))&(~p32(Y))))|(p32(Y)&p31(Y)))|((~p30(Y))&(~p31(Y))))|(p31(Y)&p30(Y)))|((~p29(Y))&(~p30(Y))))|(p30(Y)&p29(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])).
% 10.34/10.63 fof(c1,negated_conjecture,(~(~(?[X]:(~((![Y]:((~r1(X,Y)|~p45(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)|(![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)))|(~(![Y]:(~r1(X,Y)|(~((p44(Y)&~p43(Y))|(~p44(Y)&p43(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p43(X)&~p42(X))|(~p43(X)&p42(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p42(Y)&~p41(Y))|(~p42(Y)&p41(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p41(X)&~p40(X))|(~p41(X)&p40(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p40(Y)&~p39(Y))|(~p40(Y)&p39(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p39(X)&~p38(X))|(~p39(X)&p38(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p38(Y)&~p37(Y))|(~p38(Y)&p37(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p37(X)&~p36(X))|(~p37(X)&p36(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p36(Y)&~p35(Y))|(~p36(Y)&p35(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p35(X)&~p34(X))|(~p35(X)&p34(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p34(Y)&~p33(Y))|(~p34(Y)&p33(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p33(X)&~p32(X))|(~p33(X)&p32(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p32(Y)&~p31(Y))|(~p32(Y)&p31(Y))))))))))|(~(![X]:(~r1(Y,X)|(~((p31(X)&~p30(X))|(~p31(X)&p30(X))))))))))|(~(![Y]:(~r1(X,Y)|(~((p30(Y)&~p29(Y))|(~p30(Y)&p29(Y))))))))))|(~(![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)|p45(Y))))|(![Y]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~r1(X,Y)|(~p43(Y)&~p44(Y)))|(p44(Y)&p43(Y)))|(~p42(Y)&~p43(Y)))|(p43(Y)&p42(Y)))|(~p41(Y)&~p42(Y)))|(p42(Y)&p41(Y)))|(~p40(Y)&~p41(Y)))|(p41(Y)&p40(Y)))|(~p39(Y)&~p40(Y)))|(p40(Y)&p39(Y)))|(~p38(Y)&~p39(Y)))|(p39(Y)&p38(Y)))|(~p37(Y)&~p38(Y)))|(p38(Y)&p37(Y)))|(~p36(Y)&~p37(Y)))|(p37(Y)&p36(Y)))|(~p35(Y)&~p36(Y)))|(p36(Y)&p35(Y)))|(~p34(Y)&~p35(Y)))|(p35(Y)&p34(Y)))|(~p33(Y)&~p34(Y)))|(p34(Y)&p33(Y)))|(~p32(Y)&~p33(Y)))|(p33(Y)&p32(Y)))|(~p31(Y)&~p32(Y)))|(p32(Y)&p31(Y)))|(~p30(Y)&~p31(Y)))|(p31(Y)&p30(Y)))|(~p29(Y)&~p30(Y)))|(p30(Y)&p29(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])).
% 10.34/10.63 fof(c2,negated_conjecture,(?[X]:((?[Y]:((r1(X,Y)&p45(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)&(?[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)))&(![Y]:(~r1(X,Y)|((~p44(Y)|p43(Y))&(p44(Y)|~p43(Y))))))))&(![X]:(~r1(Y,X)|((~p43(X)|p42(X))&(p43(X)|~p42(X))))))))&(![Y]:(~r1(X,Y)|((~p42(Y)|p41(Y))&(p42(Y)|~p41(Y))))))))&(![X]:(~r1(Y,X)|((~p41(X)|p40(X))&(p41(X)|~p40(X))))))))&(![Y]:(~r1(X,Y)|((~p40(Y)|p39(Y))&(p40(Y)|~p39(Y))))))))&(![X]:(~r1(Y,X)|((~p39(X)|p38(X))&(p39(X)|~p38(X))))))))&(![Y]:(~r1(X,Y)|((~p38(Y)|p37(Y))&(p38(Y)|~p37(Y))))))))&(![X]:(~r1(Y,X)|((~p37(X)|p36(X))&(p37(X)|~p36(X))))))))&(![Y]:(~r1(X,Y)|((~p36(Y)|p35(Y))&(p36(Y)|~p35(Y))))))))&(![X]:(~r1(Y,X)|((~p35(X)|p34(X))&(p35(X)|~p34(X))))))))&(![Y]:(~r1(X,Y)|((~p34(Y)|p33(Y))&(p34(Y)|~p33(Y))))))))&(![X]:(~r1(Y,X)|((~p33(X)|p32(X))&(p33(X)|~p32(X))))))))&(![Y]:(~r1(X,Y)|((~p32(Y)|p31(Y))&(p32(Y)|~p31(Y))))))))&(![X]:(~r1(Y,X)|((~p31(X)|p30(X))&(p31(X)|~p30(X))))))))&(![Y]:(~r1(X,Y)|((~p30(Y)|p29(Y))&(p30(Y)|~p29(Y))))))))&(![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)&~p45(Y))))&(?[Y]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,Y)&(p43(Y)|p44(Y)))&(~p44(Y)|~p43(Y)))&(p42(Y)|p43(Y)))&(~p43(Y)|~p42(Y)))&(p41(Y)|p42(Y)))&(~p42(Y)|~p41(Y)))&(p40(Y)|p41(Y)))&(~p41(Y)|~p40(Y)))&(p39(Y)|p40(Y)))&(~p40(Y)|~p39(Y)))&(p38(Y)|p39(Y)))&(~p39(Y)|~p38(Y)))&(p37(Y)|p38(Y)))&(~p38(Y)|~p37(Y)))&(p36(Y)|p37(Y)))&(~p37(Y)|~p36(Y)))&(p35(Y)|p36(Y)))&(~p36(Y)|~p35(Y)))&(p34(Y)|p35(Y)))&(~p35(Y)|~p34(Y)))&(p33(Y)|p34(Y)))&(~p34(Y)|~p33(Y)))&(p32(Y)|p33(Y)))&(~p33(Y)|~p32(Y)))&(p31(Y)|p32(Y)))&(~p32(Y)|~p31(Y)))&(p30(Y)|p31(Y)))&(~p31(Y)|~p30(Y)))&(p29(Y)|p30(Y)))&(~p30(Y)|~p29(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])).
% 10.34/10.64 fof(c3,negated_conjecture,(?[X2]:((?[X3]:((r1(X2,X3)&p45(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(X34,X35)&(?[X36]:((r1(X35,X36)&(?[X37]:((r1(X36,X37)&(?[X38]:((r1(X37,X38)&(?[X39]:((r1(X38,X39)&(?[X40]:((r1(X39,X40)&(?[X41]:((r1(X40,X41)&(?[X42]:((r1(X41,X42)&(?[X43]:((r1(X42,X43)&(?[X44]:((r1(X43,X44)&(?[X45]:((r1(X44,X45)&(?[X46]:((r1(X45,X46)&(?[X47]:((r1(X46,X47)&(?[X48]:((r1(X47,X48)&(?[X49]:r1(X48,X49)))&(![X50]:(~r1(X48,X50)|((~p44(X50)|p43(X50))&(p44(X50)|~p43(X50))))))))&(![X51]:(~r1(X47,X51)|((~p43(X51)|p42(X51))&(p43(X51)|~p42(X51))))))))&(![X52]:(~r1(X46,X52)|((~p42(X52)|p41(X52))&(p42(X52)|~p41(X52))))))))&(![X53]:(~r1(X45,X53)|((~p41(X53)|p40(X53))&(p41(X53)|~p40(X53))))))))&(![X54]:(~r1(X44,X54)|((~p40(X54)|p39(X54))&(p40(X54)|~p39(X54))))))))&(![X55]:(~r1(X43,X55)|((~p39(X55)|p38(X55))&(p39(X55)|~p38(X55))))))))&(![X56]:(~r1(X42,X56)|((~p38(X56)|p37(X56))&(p38(X56)|~p37(X56))))))))&(![X57]:(~r1(X41,X57)|((~p37(X57)|p36(X57))&(p37(X57)|~p36(X57))))))))&(![X58]:(~r1(X40,X58)|((~p36(X58)|p35(X58))&(p36(X58)|~p35(X58))))))))&(![X59]:(~r1(X39,X59)|((~p35(X59)|p34(X59))&(p35(X59)|~p34(X59))))))))&(![X60]:(~r1(X38,X60)|((~p34(X60)|p33(X60))&(p34(X60)|~p33(X60))))))))&(![X61]:(~r1(X37,X61)|((~p33(X61)|p32(X61))&(p33(X61)|~p32(X61))))))))&(![X62]:(~r1(X36,X62)|((~p32(X62)|p31(X62))&(p32(X62)|~p31(X62))))))))&(![X63]:(~r1(X35,X63)|((~p31(X63)|p30(X63))&(p31(X63)|~p30(X63))))))))&(![X64]:(~r1(X34,X64)|((~p30(X64)|p29(X64))&(p30(X64)|~p29(X64))))))))&(![X65]:(~r1(X33,X65)|((~p29(X65)|p28(X65))&(p29(X65)|~p28(X65))))))))&(![X66]:(~r1(X32,X66)|((~p28(X66)|p27(X66))&(p28(X66)|~p27(X66))))))))&(![X67]:(~r1(X31,X67)|((~p27(X67)|p26(X67))&(p27(X67)|~p26(X67))))))))&(![X68]:(~r1(X30,X68)|((~p26(X68)|p25(X68))&(p26(X68)|~p25(X68))))))))&(![X69]:(~r1(X29,X69)|((~p25(X69)|p24(X69))&(p25(X69)|~p24(X69))))))))&(![X70]:(~r1(X28,X70)|((~p24(X70)|p23(X70))&(p24(X70)|~p23(X70))))))))&(![X71]:(~r1(X27,X71)|((~p23(X71)|p22(X71))&(p23(X71)|~p22(X71))))))))&(![X72]:(~r1(X26,X72)|((~p22(X72)|p21(X72))&(p22(X72)|~p21(X72))))))))&(![X73]:(~r1(X25,X73)|((~p21(X73)|p20(X73))&(p21(X73)|~p20(X73))))))))&(![X74]:(~r1(X24,X74)|((~p20(X74)|p19(X74))&(p20(X74)|~p19(X74))))))))&(![X75]:(~r1(X23,X75)|((~p19(X75)|p18(X75))&(p19(X75)|~p18(X75))))))))&(![X76]:(~r1(X22,X76)|((~p18(X76)|p17(X76))&(p18(X76)|~p17(X76))))))))&(![X77]:(~r1(X21,X77)|((~p17(X77)|p16(X77))&(p17(X77)|~p16(X77))))))))&(![X78]:(~r1(X20,X78)|((~p16(X78)|p15(X78))&(p16(X78)|~p15(X78))))))))&(![X79]:(~r1(X19,X79)|((~p15(X79)|p14(X79))&(p15(X79)|~p14(X79))))))))&(![X80]:(~r1(X18,X80)|((~p14(X80)|p13(X80))&(p14(X80)|~p13(X80))))))))&(![X81]:(~r1(X17,X81)|((~p13(X81)|p12(X81))&(p13(X81)|~p12(X81))))))))&(![X82]:(~r1(X16,X82)|((~p12(X82)|p11(X82))&(p12(X82)|~p11(X82))))))))&(![X83]:(~r1(X15,X83)|((~p11(X83)|p10(X83))&(p11(X83)|~p10(X83))))))))&(![X84]:(~r1(X14,X84)|((~p10(X84)|p9(X84))&(p10(X84)|~p9(X84))))))))&(![X85]:(~r1(X13,X85)|((~p9(X85)|p8(X85))&(p9(X85)|~p8(X85))))))))&(![X86]:(~r1(X12,X86)|((~p8(X86)|p7(X86))&(p8(X86)|~p7(X86))))))))&(![X87]:(~r1(X11,X87)|((~p7(X87)|p6(X87))&(p7(X87)|~p6(X87))))))))&(![X88]:(~r1(X10,X88)|((~p6(X88)|p5(X88))&(p6(X88)|~p5(X88))))))))&(![X89]:(~r1(X9,X89)|((~p5(X89)|p4(X89))&(p5(X89)|~p4(X89))))))))&(![X90]:(~r1(X8,X90)|((~p4(X90)|p3(X90))&(p4(X90)|~p3(X90))))))))&(![X91]:(~r1(X7,X91)|((~p3(X91)|p2(X91))&(p3(X91)|~p2(X91)))))))&(![X92]:(~r1(X6,X92)|((~p2(X92)|p1(X92))&(p2(X92)|~p1(X92))))))&(?[X93]:(r1(X6,X93)&~p45(X93))))&(?[X94]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X6,X94)&(p43(X94)|p44(X94)))&(~p44(X94)|~p43(X94)))&(p42(X94)|p43(X94)))&(~p43(X94)|~p42(X94)))&(p41(X94)|p42(X94)))&(~p42(X94)|~p41(X94)))&(p40(X94)|p41(X94)))&(~p41(X94)|~p40(X94)))&(p39(X94)|p40(X94)))&(~p40(X94)|~p39(X94)))&(p38(X94)|p39(X94)))&(~p39(X94)|~p38(X94)))&(p37(X94)|p38(X94)))&(~p38(X94)|~p37(X94)))&(p36(X94)|p37(X94)))&(~p37(X94)|~p36(X94)))&(p35(X94)|p36(X94)))&(~p36(X94)|~p35(X94)))&(p34(X94)|p35(X94)))&(~p35(X94)|~p34(X94)))&(p33(X94)|p34(X94)))&(~p34(X94)|~p33(X94)))&(p32(X94)|p33(X94)))&(~p33(X94)|~p32(X94)))&(p31(X94)|p32(X94)))&(~p32(X94)|~p31(X94)))&(p30(X94)|p31(X94)))&(~p31(X94)|~p30(X94)))&(p29(X94)|p30(X94)))&(~p30(X94)|~p29(X94)))&(p28(X94)|p29(X94)))&(~p29(X94)|~p28(X94)))&(p27(X94)|p28(X94)))&(~p28(X94)|~p27(X94)))&(p26(X94)|p27(X94)))&(~p27(X94)|~p26(X94)))&(p25(X94)|p26(X94)))&(~p26(X94)|~p25(X94)))&(p24(X94)|p25(X94)))&(~p25(X94)|~p24(X94)))&(p23(X94)|p24(X94)))&(~p24(X94)|~p23(X94)))&(p22(X94)|p23(X94)))&(~p23(X94)|~p22(X94)))&(p21(X94)|p22(X94)))&(~p22(X94)|~p21(X94)))&(p20(X94)|p21(X94)))&(~p21(X94)|~p20(X94)))&(p19(X94)|p20(X94)))&(~p20(X94)|~p19(X94)))&(p18(X94)|p19(X94)))&(~p19(X94)|~p18(X94)))&(p17(X94)|p18(X94)))&(~p18(X94)|~p17(X94)))&(p16(X94)|p17(X94)))&(~p17(X94)|~p16(X94)))&(p15(X94)|p16(X94)))&(~p16(X94)|~p15(X94)))&(p14(X94)|p15(X94)))&(~p15(X94)|~p14(X94)))&(p13(X94)|p14(X94)))&(~p14(X94)|~p13(X94)))&(p12(X94)|p13(X94)))&(~p13(X94)|~p12(X94)))&(p11(X94)|p12(X94)))&(~p12(X94)|~p11(X94)))&(p10(X94)|p11(X94)))&(~p11(X94)|~p10(X94)))&(p9(X94)|p10(X94)))&(~p10(X94)|~p9(X94)))&(p8(X94)|p9(X94)))&(~p9(X94)|~p8(X94)))&(p7(X94)|p8(X94)))&(~p8(X94)|~p7(X94)))&(p6(X94)|p7(X94)))&(~p7(X94)|~p6(X94)))&(p5(X94)|p6(X94)))&(~p6(X94)|~p5(X94)))&(p4(X94)|p5(X94)))&(~p5(X94)|~p4(X94)))&(p3(X94)|p4(X94)))&(~p4(X94)|~p3(X94)))&(p2(X94)|p3(X94)))&(~p3(X94)|~p2(X94)))&(p1(X94)|p2(X94)))&(~p2(X94)|~p1(X94))))))))))),inference(variable_rename,[status(thm)],[c2])).
% 10.34/10.64 fof(c5,negated_conjecture,(![X6]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:(![X66]:(![X67]:(![X68]:(![X69]:(![X70]:(![X71]:(![X72]:(![X73]:(![X74]:(![X75]:(![X76]:(![X77]:(![X78]:(![X79]:(![X80]:(![X81]:(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:(![X87]:(![X88]:(![X89]:(![X90]:(![X91]:(![X92]:(((r1(skolem0001,skolem0002)&p45(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(skolem0032(X6),skolem0033(X6))&((r1(skolem0033(X6),skolem0034(X6))&((r1(skolem0034(X6),skolem0035(X6))&((r1(skolem0035(X6),skolem0036(X6))&((r1(skolem0036(X6),skolem0037(X6))&((r1(skolem0037(X6),skolem0038(X6))&((r1(skolem0038(X6),skolem0039(X6))&((r1(skolem0039(X6),skolem0040(X6))&((r1(skolem0040(X6),skolem0041(X6))&((r1(skolem0041(X6),skolem0042(X6))&((r1(skolem0042(X6),skolem0043(X6))&((r1(skolem0043(X6),skolem0044(X6))&((r1(skolem0044(X6),skolem0045(X6))&((r1(skolem0045(X6),skolem0046(X6))&r1(skolem0046(X6),skolem0047(X6)))&(~r1(skolem0046(X6),X50)|((~p44(X50)|p43(X50))&(p44(X50)|~p43(X50))))))&(~r1(skolem0045(X6),X51)|((~p43(X51)|p42(X51))&(p43(X51)|~p42(X51))))))&(~r1(skolem0044(X6),X52)|((~p42(X52)|p41(X52))&(p42(X52)|~p41(X52))))))&(~r1(skolem0043(X6),X53)|((~p41(X53)|p40(X53))&(p41(X53)|~p40(X53))))))&(~r1(skolem0042(X6),X54)|((~p40(X54)|p39(X54))&(p40(X54)|~p39(X54))))))&(~r1(skolem0041(X6),X55)|((~p39(X55)|p38(X55))&(p39(X55)|~p38(X55))))))&(~r1(skolem0040(X6),X56)|((~p38(X56)|p37(X56))&(p38(X56)|~p37(X56))))))&(~r1(skolem0039(X6),X57)|((~p37(X57)|p36(X57))&(p37(X57)|~p36(X57))))))&(~r1(skolem0038(X6),X58)|((~p36(X58)|p35(X58))&(p36(X58)|~p35(X58))))))&(~r1(skolem0037(X6),X59)|((~p35(X59)|p34(X59))&(p35(X59)|~p34(X59))))))&(~r1(skolem0036(X6),X60)|((~p34(X60)|p33(X60))&(p34(X60)|~p33(X60))))))&(~r1(skolem0035(X6),X61)|((~p33(X61)|p32(X61))&(p33(X61)|~p32(X61))))))&(~r1(skolem0034(X6),X62)|((~p32(X62)|p31(X62))&(p32(X62)|~p31(X62))))))&(~r1(skolem0033(X6),X63)|((~p31(X63)|p30(X63))&(p31(X63)|~p30(X63))))))&(~r1(skolem0032(X6),X64)|((~p30(X64)|p29(X64))&(p30(X64)|~p29(X64))))))&(~r1(skolem0031(X6),X65)|((~p29(X65)|p28(X65))&(p29(X65)|~p28(X65))))))&(~r1(skolem0030(X6),X66)|((~p28(X66)|p27(X66))&(p28(X66)|~p27(X66))))))&(~r1(skolem0029(X6),X67)|((~p27(X67)|p26(X67))&(p27(X67)|~p26(X67))))))&(~r1(skolem0028(X6),X68)|((~p26(X68)|p25(X68))&(p26(X68)|~p25(X68))))))&(~r1(skolem0027(X6),X69)|((~p25(X69)|p24(X69))&(p25(X69)|~p24(X69))))))&(~r1(skolem0026(X6),X70)|((~p24(X70)|p23(X70))&(p24(X70)|~p23(X70))))))&(~r1(skolem0025(X6),X71)|((~p23(X71)|p22(X71))&(p23(X71)|~p22(X71))))))&(~r1(skolem0024(X6),X72)|((~p22(X72)|p21(X72))&(p22(X72)|~p21(X72))))))&(~r1(skolem0023(X6),X73)|((~p21(X73)|p20(X73))&(p21(X73)|~p20(X73))))))&(~r1(skolem0022(X6),X74)|((~p20(X74)|p19(X74))&(p20(X74)|~p19(X74))))))&(~r1(skolem0021(X6),X75)|((~p19(X75)|p18(X75))&(p19(X75)|~p18(X75))))))&(~r1(skolem0020(X6),X76)|((~p18(X76)|p17(X76))&(p18(X76)|~p17(X76))))))&(~r1(skolem0019(X6),X77)|((~p17(X77)|p16(X77))&(p17(X77)|~p16(X77))))))&(~r1(skolem0018(X6),X78)|((~p16(X78)|p15(X78))&(p16(X78)|~p15(X78))))))&(~r1(skolem0017(X6),X79)|((~p15(X79)|p14(X79))&(p15(X79)|~p14(X79))))))&(~r1(skolem0016(X6),X80)|((~p14(X80)|p13(X80))&(p14(X80)|~p13(X80))))))&(~r1(skolem0015(X6),X81)|((~p13(X81)|p12(X81))&(p13(X81)|~p12(X81))))))&(~r1(skolem0014(X6),X82)|((~p12(X82)|p11(X82))&(p12(X82)|~p11(X82))))))&(~r1(skolem0013(X6),X83)|((~p11(X83)|p10(X83))&(p11(X83)|~p10(X83))))))&(~r1(skolem0012(X6),X84)|((~p10(X84)|p9(X84))&(p10(X84)|~p9(X84))))))&(~r1(skolem0011(X6),X85)|((~p9(X85)|p8(X85))&(p9(X85)|~p8(X85))))))&(~r1(skolem0010(X6),X86)|((~p8(X86)|p7(X86))&(p8(X86)|~p7(X86))))))&(~r1(skolem0009(X6),X87)|((~p7(X87)|p6(X87))&(p7(X87)|~p6(X87))))))&(~r1(skolem0008(X6),X88)|((~p6(X88)|p5(X88))&(p6(X88)|~p5(X88))))))&(~r1(skolem0007(X6),X89)|((~p5(X89)|p4(X89))&(p5(X89)|~p4(X89))))))&(~r1(skolem0006(X6),X90)|((~p4(X90)|p3(X90))&(p4(X90)|~p3(X90))))))&(~r1(skolem0005(X6),X91)|((~p3(X91)|p2(X91))&(p3(X91)|~p2(X91)))))&(~r1(X6,X92)|((~p2(X92)|p1(X92))&(p2(X92)|~p1(X92)))))&(r1(X6,skolem0048(X6))&~p45(skolem0048(X6))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X6,skolem0049(X6))&(p43(skolem0049(X6))|p44(skolem0049(X6))))&(~p44(skolem0049(X6))|~p43(skolem0049(X6))))&(p42(skolem0049(X6))|p43(skolem0049(X6))))&(~p43(skolem0049(X6))|~p42(skolem0049(X6))))&(p41(skolem0049(X6))|p42(skolem0049(X6))))&(~p42(skolem0049(X6))|~p41(skolem0049(X6))))&(p40(skolem0049(X6))|p41(skolem0049(X6))))&(~p41(skolem0049(X6))|~p40(skolem0049(X6))))&(p39(skolem0049(X6))|p40(skolem0049(X6))))&(~p40(skolem0049(X6))|~p39(skolem0049(X6))))&(p38(skolem0049(X6))|p39(skolem0049(X6))))&(~p39(skolem0049(X6))|~p38(skolem0049(X6))))&(p37(skolem0049(X6))|p38(skolem0049(X6))))&(~p38(skolem0049(X6))|~p37(skolem0049(X6))))&(p36(skolem0049(X6))|p37(skolem0049(X6))))&(~p37(skolem0049(X6))|~p36(skolem0049(X6))))&(p35(skolem0049(X6))|p36(skolem0049(X6))))&(~p36(skolem0049(X6))|~p35(skolem0049(X6))))&(p34(skolem0049(X6))|p35(skolem0049(X6))))&(~p35(skolem0049(X6))|~p34(skolem0049(X6))))&(p33(skolem0049(X6))|p34(skolem0049(X6))))&(~p34(skolem0049(X6))|~p33(skolem0049(X6))))&(p32(skolem0049(X6))|p33(skolem0049(X6))))&(~p33(skolem0049(X6))|~p32(skolem0049(X6))))&(p31(skolem0049(X6))|p32(skolem0049(X6))))&(~p32(skolem0049(X6))|~p31(skolem0049(X6))))&(p30(skolem0049(X6))|p31(skolem0049(X6))))&(~p31(skolem0049(X6))|~p30(skolem0049(X6))))&(p29(skolem0049(X6))|p30(skolem0049(X6))))&(~p30(skolem0049(X6))|~p29(skolem0049(X6))))&(p28(skolem0049(X6))|p29(skolem0049(X6))))&(~p29(skolem0049(X6))|~p28(skolem0049(X6))))&(p27(skolem0049(X6))|p28(skolem0049(X6))))&(~p28(skolem0049(X6))|~p27(skolem0049(X6))))&(p26(skolem0049(X6))|p27(skolem0049(X6))))&(~p27(skolem0049(X6))|~p26(skolem0049(X6))))&(p25(skolem0049(X6))|p26(skolem0049(X6))))&(~p26(skolem0049(X6))|~p25(skolem0049(X6))))&(p24(skolem0049(X6))|p25(skolem0049(X6))))&(~p25(skolem0049(X6))|~p24(skolem0049(X6))))&(p23(skolem0049(X6))|p24(skolem0049(X6))))&(~p24(skolem0049(X6))|~p23(skolem0049(X6))))&(p22(skolem0049(X6))|p23(skolem0049(X6))))&(~p23(skolem0049(X6))|~p22(skolem0049(X6))))&(p21(skolem0049(X6))|p22(skolem0049(X6))))&(~p22(skolem0049(X6))|~p21(skolem0049(X6))))&(p20(skolem0049(X6))|p21(skolem0049(X6))))&(~p21(skolem0049(X6))|~p20(skolem0049(X6))))&(p19(skolem0049(X6))|p20(skolem0049(X6))))&(~p20(skolem0049(X6))|~p19(skolem0049(X6))))&(p18(skolem0049(X6))|p19(skolem0049(X6))))&(~p19(skolem0049(X6))|~p18(skolem0049(X6))))&(p17(skolem0049(X6))|p18(skolem0049(X6))))&(~p18(skolem0049(X6))|~p17(skolem0049(X6))))&(p16(skolem0049(X6))|p17(skolem0049(X6))))&(~p17(skolem0049(X6))|~p16(skolem0049(X6))))&(p15(skolem0049(X6))|p16(skolem0049(X6))))&(~p16(skolem0049(X6))|~p15(skolem0049(X6))))&(p14(skolem0049(X6))|p15(skolem0049(X6))))&(~p15(skolem0049(X6))|~p14(skolem0049(X6))))&(p13(skolem0049(X6))|p14(skolem0049(X6))))&(~p14(skolem0049(X6))|~p13(skolem0049(X6))))&(p12(skolem0049(X6))|p13(skolem0049(X6))))&(~p13(skolem0049(X6))|~p12(skolem0049(X6))))&(p11(skolem0049(X6))|p12(skolem0049(X6))))&(~p12(skolem0049(X6))|~p11(skolem0049(X6))))&(p10(skolem0049(X6))|p11(skolem0049(X6))))&(~p11(skolem0049(X6))|~p10(skolem0049(X6))))&(p9(skolem0049(X6))|p10(skolem0049(X6))))&(~p10(skolem0049(X6))|~p9(skolem0049(X6))))&(p8(skolem0049(X6))|p9(skolem0049(X6))))&(~p9(skolem0049(X6))|~p8(skolem0049(X6))))&(p7(skolem0049(X6))|p8(skolem0049(X6))))&(~p8(skolem0049(X6))|~p7(skolem0049(X6))))&(p6(skolem0049(X6))|p7(skolem0049(X6))))&(~p7(skolem0049(X6))|~p6(skolem0049(X6))))&(p5(skolem0049(X6))|p6(skolem0049(X6))))&(~p6(skolem0049(X6))|~p5(skolem0049(X6))))&(p4(skolem0049(X6))|p5(skolem0049(X6))))&(~p5(skolem0049(X6))|~p4(skolem0049(X6))))&(p3(skolem0049(X6))|p4(skolem0049(X6))))&(~p4(skolem0049(X6))|~p3(skolem0049(X6))))&(p2(skolem0049(X6))|p3(skolem0049(X6))))&(~p3(skolem0049(X6))|~p2(skolem0049(X6))))&(p1(skolem0049(X6))|p2(skolem0049(X6))))&(~p2(skolem0049(X6))|~p1(skolem0049(X6)))))))))))))))))))))))))))))))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,(((r1(skolem0001,skolem0002)&p45(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))&((r1(skolem0032(X6),skolem0033(X6))&((r1(skolem0033(X6),skolem0034(X6))&((r1(skolem0034(X6),skolem0035(X6))&((r1(skolem0035(X6),skolem0036(X6))&((r1(skolem0036(X6),skolem0037(X6))&((r1(skolem0037(X6),skolem0038(X6))&((r1(skolem0038(X6),skolem0039(X6))&((r1(skolem0039(X6),skolem0040(X6))&((r1(skolem0040(X6),skolem0041(X6))&((r1(skolem0041(X6),skolem0042(X6))&((r1(skolem0042(X6),skolem0043(X6))&((r1(skolem0043(X6),skolem0044(X6))&((r1(skolem0044(X6),skolem0045(X6))&((r1(skolem0045(X6),skolem0046(X6))&r1(skolem0046(X6),skolem0047(X6)))&(![X50]:(~r1(skolem0046(X6),X50)|((~p44(X50)|p43(X50))&(p44(X50)|~p43(X50)))))))&(![X51]:(~r1(skolem0045(X6),X51)|((~p43(X51)|p42(X51))&(p43(X51)|~p42(X51)))))))&(![X52]:(~r1(skolem0044(X6),X52)|((~p42(X52)|p41(X52))&(p42(X52)|~p41(X52)))))))&(![X53]:(~r1(skolem0043(X6),X53)|((~p41(X53)|p40(X53))&(p41(X53)|~p40(X53)))))))&(![X54]:(~r1(skolem0042(X6),X54)|((~p40(X54)|p39(X54))&(p40(X54)|~p39(X54)))))))&(![X55]:(~r1(skolem0041(X6),X55)|((~p39(X55)|p38(X55))&(p39(X55)|~p38(X55)))))))&(![X56]:(~r1(skolem0040(X6),X56)|((~p38(X56)|p37(X56))&(p38(X56)|~p37(X56)))))))&(![X57]:(~r1(skolem0039(X6),X57)|((~p37(X57)|p36(X57))&(p37(X57)|~p36(X57)))))))&(![X58]:(~r1(skolem0038(X6),X58)|((~p36(X58)|p35(X58))&(p36(X58)|~p35(X58)))))))&(![X59]:(~r1(skolem0037(X6),X59)|((~p35(X59)|p34(X59))&(p35(X59)|~p34(X59)))))))&(![X60]:(~r1(skolem0036(X6),X60)|((~p34(X60)|p33(X60))&(p34(X60)|~p33(X60)))))))&(![X61]:(~r1(skolem0035(X6),X61)|((~p33(X61)|p32(X61))&(p33(X61)|~p32(X61)))))))&(![X62]:(~r1(skolem0034(X6),X62)|((~p32(X62)|p31(X62))&(p32(X62)|~p31(X62)))))))&(![X63]:(~r1(skolem0033(X6),X63)|((~p31(X63)|p30(X63))&(p31(X63)|~p30(X63)))))))&(![X64]:(~r1(skolem0032(X6),X64)|((~p30(X64)|p29(X64))&(p30(X64)|~p29(X64)))))))&(![X65]:(~r1(skolem0031(X6),X65)|((~p29(X65)|p28(X65))&(p29(X65)|~p28(X65)))))))&(![X66]:(~r1(skolem0030(X6),X66)|((~p28(X66)|p27(X66))&(p28(X66)|~p27(X66)))))))&(![X67]:(~r1(skolem0029(X6),X67)|((~p27(X67)|p26(X67))&(p27(X67)|~p26(X67)))))))&(![X68]:(~r1(skolem0028(X6),X68)|((~p26(X68)|p25(X68))&(p26(X68)|~p25(X68)))))))&(![X69]:(~r1(skolem0027(X6),X69)|((~p25(X69)|p24(X69))&(p25(X69)|~p24(X69)))))))&(![X70]:(~r1(skolem0026(X6),X70)|((~p24(X70)|p23(X70))&(p24(X70)|~p23(X70)))))))&(![X71]:(~r1(skolem0025(X6),X71)|((~p23(X71)|p22(X71))&(p23(X71)|~p22(X71)))))))&(![X72]:(~r1(skolem0024(X6),X72)|((~p22(X72)|p21(X72))&(p22(X72)|~p21(X72)))))))&(![X73]:(~r1(skolem0023(X6),X73)|((~p21(X73)|p20(X73))&(p21(X73)|~p20(X73)))))))&(![X74]:(~r1(skolem0022(X6),X74)|((~p20(X74)|p19(X74))&(p20(X74)|~p19(X74)))))))&(![X75]:(~r1(skolem0021(X6),X75)|((~p19(X75)|p18(X75))&(p19(X75)|~p18(X75)))))))&(![X76]:(~r1(skolem0020(X6),X76)|((~p18(X76)|p17(X76))&(p18(X76)|~p17(X76)))))))&(![X77]:(~r1(skolem0019(X6),X77)|((~p17(X77)|p16(X77))&(p17(X77)|~p16(X77)))))))&(![X78]:(~r1(skolem0018(X6),X78)|((~p16(X78)|p15(X78))&(p16(X78)|~p15(X78)))))))&(![X79]:(~r1(skolem0017(X6),X79)|((~p15(X79)|p14(X79))&(p15(X79)|~p14(X79)))))))&(![X80]:(~r1(skolem0016(X6),X80)|((~p14(X80)|p13(X80))&(p14(X80)|~p13(X80)))))))&(![X81]:(~r1(skolem0015(X6),X81)|((~p13(X81)|p12(X81))&(p13(X81)|~p12(X81)))))))&(![X82]:(~r1(skolem0014(X6),X82)|((~p12(X82)|p11(X82))&(p12(X82)|~p11(X82)))))))&(![X83]:(~r1(skolem0013(X6),X83)|((~p11(X83)|p10(X83))&(p11(X83)|~p10(X83)))))))&(![X84]:(~r1(skolem0012(X6),X84)|((~p10(X84)|p9(X84))&(p10(X84)|~p9(X84)))))))&(![X85]:(~r1(skolem0011(X6),X85)|((~p9(X85)|p8(X85))&(p9(X85)|~p8(X85)))))))&(![X86]:(~r1(skolem0010(X6),X86)|((~p8(X86)|p7(X86))&(p8(X86)|~p7(X86)))))))&(![X87]:(~r1(skolem0009(X6),X87)|((~p7(X87)|p6(X87))&(p7(X87)|~p6(X87)))))))&(![X88]:(~r1(skolem0008(X6),X88)|((~p6(X88)|p5(X88))&(p6(X88)|~p5(X88)))))))&(![X89]:(~r1(skolem0007(X6),X89)|((~p5(X89)|p4(X89))&(p5(X89)|~p4(X89)))))))&(![X90]:(~r1(skolem0006(X6),X90)|((~p4(X90)|p3(X90))&(p4(X90)|~p3(X90)))))))&(![X91]:(~r1(skolem0005(X6),X91)|((~p3(X91)|p2(X91))&(p3(X91)|~p2(X91))))))&(![X92]:(~r1(X6,X92)|((~p2(X92)|p1(X92))&(p2(X92)|~p1(X92))))))&(r1(X6,skolem0048(X6))&~p45(skolem0048(X6))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X6,skolem0049(X6))&(p43(skolem0049(X6))|p44(skolem0049(X6))))&(~p44(skolem0049(X6))|~p43(skolem0049(X6))))&(p42(skolem0049(X6))|p43(skolem0049(X6))))&(~p43(skolem0049(X6))|~p42(skolem0049(X6))))&(p41(skolem0049(X6))|p42(skolem0049(X6))))&(~p42(skolem0049(X6))|~p41(skolem0049(X6))))&(p40(skolem0049(X6))|p41(skolem0049(X6))))&(~p41(skolem0049(X6))|~p40(skolem0049(X6))))&(p39(skolem0049(X6))|p40(skolem0049(X6))))&(~p40(skolem0049(X6))|~p39(skolem0049(X6))))&(p38(skolem0049(X6))|p39(skolem0049(X6))))&(~p39(skolem0049(X6))|~p38(skolem0049(X6))))&(p37(skolem0049(X6))|p38(skolem0049(X6))))&(~p38(skolem0049(X6))|~p37(skolem0049(X6))))&(p36(skolem0049(X6))|p37(skolem0049(X6))))&(~p37(skolem0049(X6))|~p36(skolem0049(X6))))&(p35(skolem0049(X6))|p36(skolem0049(X6))))&(~p36(skolem0049(X6))|~p35(skolem0049(X6))))&(p34(skolem0049(X6))|p35(skolem0049(X6))))&(~p35(skolem0049(X6))|~p34(skolem0049(X6))))&(p33(skolem0049(X6))|p34(skolem0049(X6))))&(~p34(skolem0049(X6))|~p33(skolem0049(X6))))&(p32(skolem0049(X6))|p33(skolem0049(X6))))&(~p33(skolem0049(X6))|~p32(skolem0049(X6))))&(p31(skolem0049(X6))|p32(skolem0049(X6))))&(~p32(skolem0049(X6))|~p31(skolem0049(X6))))&(p30(skolem0049(X6))|p31(skolem0049(X6))))&(~p31(skolem0049(X6))|~p30(skolem0049(X6))))&(p29(skolem0049(X6))|p30(skolem0049(X6))))&(~p30(skolem0049(X6))|~p29(skolem0049(X6))))&(p28(skolem0049(X6))|p29(skolem0049(X6))))&(~p29(skolem0049(X6))|~p28(skolem0049(X6))))&(p27(skolem0049(X6))|p28(skolem0049(X6))))&(~p28(skolem0049(X6))|~p27(skolem0049(X6))))&(p26(skolem0049(X6))|p27(skolem0049(X6))))&(~p27(skolem0049(X6))|~p26(skolem0049(X6))))&(p25(skolem0049(X6))|p26(skolem0049(X6))))&(~p26(skolem0049(X6))|~p25(skolem0049(X6))))&(p24(skolem0049(X6))|p25(skolem0049(X6))))&(~p25(skolem0049(X6))|~p24(skolem0049(X6))))&(p23(skolem0049(X6))|p24(skolem0049(X6))))&(~p24(skolem0049(X6))|~p23(skolem0049(X6))))&(p22(skolem0049(X6))|p23(skolem0049(X6))))&(~p23(skolem0049(X6))|~p22(skolem0049(X6))))&(p21(skolem0049(X6))|p22(skolem0049(X6))))&(~p22(skolem0049(X6))|~p21(skolem0049(X6))))&(p20(skolem0049(X6))|p21(skolem0049(X6))))&(~p21(skolem0049(X6))|~p20(skolem0049(X6))))&(p19(skolem0049(X6))|p20(skolem0049(X6))))&(~p20(skolem0049(X6))|~p19(skolem0049(X6))))&(p18(skolem0049(X6))|p19(skolem0049(X6))))&(~p19(skolem0049(X6))|~p18(skolem0049(X6))))&(p17(skolem0049(X6))|p18(skolem0049(X6))))&(~p18(skolem0049(X6))|~p17(skolem0049(X6))))&(p16(skolem0049(X6))|p17(skolem0049(X6))))&(~p17(skolem0049(X6))|~p16(skolem0049(X6))))&(p15(skolem0049(X6))|p16(skolem0049(X6))))&(~p16(skolem0049(X6))|~p15(skolem0049(X6))))&(p14(skolem0049(X6))|p15(skolem0049(X6))))&(~p15(skolem0049(X6))|~p14(skolem0049(X6))))&(p13(skolem0049(X6))|p14(skolem0049(X6))))&(~p14(skolem0049(X6))|~p13(skolem0049(X6))))&(p12(skolem0049(X6))|p13(skolem0049(X6))))&(~p13(skolem0049(X6))|~p12(skolem0049(X6))))&(p11(skolem0049(X6))|p12(skolem0049(X6))))&(~p12(skolem0049(X6))|~p11(skolem0049(X6))))&(p10(skolem0049(X6))|p11(skolem0049(X6))))&(~p11(skolem0049(X6))|~p10(skolem0049(X6))))&(p9(skolem0049(X6))|p10(skolem0049(X6))))&(~p10(skolem0049(X6))|~p9(skolem0049(X6))))&(p8(skolem0049(X6))|p9(skolem0049(X6))))&(~p9(skolem0049(X6))|~p8(skolem0049(X6))))&(p7(skolem0049(X6))|p8(skolem0049(X6))))&(~p8(skolem0049(X6))|~p7(skolem0049(X6))))&(p6(skolem0049(X6))|p7(skolem0049(X6))))&(~p7(skolem0049(X6))|~p6(skolem0049(X6))))&(p5(skolem0049(X6))|p6(skolem0049(X6))))&(~p6(skolem0049(X6))|~p5(skolem0049(X6))))&(p4(skolem0049(X6))|p5(skolem0049(X6))))&(~p5(skolem0049(X6))|~p4(skolem0049(X6))))&(p3(skolem0049(X6))|p4(skolem0049(X6))))&(~p4(skolem0049(X6))|~p3(skolem0049(X6))))&(p2(skolem0049(X6))|p3(skolem0049(X6))))&(~p3(skolem0049(X6))|~p2(skolem0049(X6))))&(p1(skolem0049(X6))|p2(skolem0049(X6))))&(~p2(skolem0049(X6))|~p1(skolem0049(X6))))))))),inference(skolemize,[status(esa)],[c3])).])).
% 10.34/10.65 fof(c6,negated_conjecture,(![X6]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:(![X66]:(![X67]:(![X68]:(![X69]:(![X70]:(![X71]:(![X72]:(![X73]:(![X74]:(![X75]:(![X76]:(![X77]:(![X78]:(![X79]:(![X80]:(![X81]:(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:(![X87]:(![X88]:(![X89]:(![X90]:(![X91]:(![X92]:(((r1(skolem0001,skolem0002)&p45(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(skolem0032(X6),skolem0033(X6)))&(((~r1(skolem0004,X6)|r1(skolem0033(X6),skolem0034(X6)))&(((~r1(skolem0004,X6)|r1(skolem0034(X6),skolem0035(X6)))&(((~r1(skolem0004,X6)|r1(skolem0035(X6),skolem0036(X6)))&(((~r1(skolem0004,X6)|r1(skolem0036(X6),skolem0037(X6)))&(((~r1(skolem0004,X6)|r1(skolem0037(X6),skolem0038(X6)))&(((~r1(skolem0004,X6)|r1(skolem0038(X6),skolem0039(X6)))&(((~r1(skolem0004,X6)|r1(skolem0039(X6),skolem0040(X6)))&(((~r1(skolem0004,X6)|r1(skolem0040(X6),skolem0041(X6)))&(((~r1(skolem0004,X6)|r1(skolem0041(X6),skolem0042(X6)))&(((~r1(skolem0004,X6)|r1(skolem0042(X6),skolem0043(X6)))&(((~r1(skolem0004,X6)|r1(skolem0043(X6),skolem0044(X6)))&(((~r1(skolem0004,X6)|r1(skolem0044(X6),skolem0045(X6)))&(((~r1(skolem0004,X6)|r1(skolem0045(X6),skolem0046(X6)))&(~r1(skolem0004,X6)|r1(skolem0046(X6),skolem0047(X6))))&((~r1(skolem0004,X6)|(~r1(skolem0046(X6),X50)|(~p44(X50)|p43(X50))))&(~r1(skolem0004,X6)|(~r1(skolem0046(X6),X50)|(p44(X50)|~p43(X50)))))))&((~r1(skolem0004,X6)|(~r1(skolem0045(X6),X51)|(~p43(X51)|p42(X51))))&(~r1(skolem0004,X6)|(~r1(skolem0045(X6),X51)|(p43(X51)|~p42(X51)))))))&((~r1(skolem0004,X6)|(~r1(skolem0044(X6),X52)|(~p42(X52)|p41(X52))))&(~r1(skolem0004,X6)|(~r1(skolem0044(X6),X52)|(p42(X52)|~p41(X52)))))))&((~r1(skolem0004,X6)|(~r1(skolem0043(X6),X53)|(~p41(X53)|p40(X53))))&(~r1(skolem0004,X6)|(~r1(skolem0043(X6),X53)|(p41(X53)|~p40(X53)))))))&((~r1(skolem0004,X6)|(~r1(skolem0042(X6),X54)|(~p40(X54)|p39(X54))))&(~r1(skolem0004,X6)|(~r1(skolem0042(X6),X54)|(p40(X54)|~p39(X54)))))))&((~r1(skolem0004,X6)|(~r1(skolem0041(X6),X55)|(~p39(X55)|p38(X55))))&(~r1(skolem0004,X6)|(~r1(skolem0041(X6),X55)|(p39(X55)|~p38(X55)))))))&((~r1(skolem0004,X6)|(~r1(skolem0040(X6),X56)|(~p38(X56)|p37(X56))))&(~r1(skolem0004,X6)|(~r1(skolem0040(X6),X56)|(p38(X56)|~p37(X56)))))))&((~r1(skolem0004,X6)|(~r1(skolem0039(X6),X57)|(~p37(X57)|p36(X57))))&(~r1(skolem0004,X6)|(~r1(skolem0039(X6),X57)|(p37(X57)|~p36(X57)))))))&((~r1(skolem0004,X6)|(~r1(skolem0038(X6),X58)|(~p36(X58)|p35(X58))))&(~r1(skolem0004,X6)|(~r1(skolem0038(X6),X58)|(p36(X58)|~p35(X58)))))))&((~r1(skolem0004,X6)|(~r1(skolem0037(X6),X59)|(~p35(X59)|p34(X59))))&(~r1(skolem0004,X6)|(~r1(skolem0037(X6),X59)|(p35(X59)|~p34(X59)))))))&((~r1(skolem0004,X6)|(~r1(skolem0036(X6),X60)|(~p34(X60)|p33(X60))))&(~r1(skolem0004,X6)|(~r1(skolem0036(X6),X60)|(p34(X60)|~p33(X60)))))))&((~r1(skolem0004,X6)|(~r1(skolem0035(X6),X61)|(~p33(X61)|p32(X61))))&(~r1(skolem0004,X6)|(~r1(skolem0035(X6),X61)|(p33(X61)|~p32(X61)))))))&((~r1(skolem0004,X6)|(~r1(skolem0034(X6),X62)|(~p32(X62)|p31(X62))))&(~r1(skolem0004,X6)|(~r1(skolem0034(X6),X62)|(p32(X62)|~p31(X62)))))))&((~r1(skolem0004,X6)|(~r1(skolem0033(X6),X63)|(~p31(X63)|p30(X63))))&(~r1(skolem0004,X6)|(~r1(skolem0033(X6),X63)|(p31(X63)|~p30(X63)))))))&((~r1(skolem0004,X6)|(~r1(skolem0032(X6),X64)|(~p30(X64)|p29(X64))))&(~r1(skolem0004,X6)|(~r1(skolem0032(X6),X64)|(p30(X64)|~p29(X64)))))))&((~r1(skolem0004,X6)|(~r1(skolem0031(X6),X65)|(~p29(X65)|p28(X65))))&(~r1(skolem0004,X6)|(~r1(skolem0031(X6),X65)|(p29(X65)|~p28(X65)))))))&((~r1(skolem0004,X6)|(~r1(skolem0030(X6),X66)|(~p28(X66)|p27(X66))))&(~r1(skolem0004,X6)|(~r1(skolem0030(X6),X66)|(p28(X66)|~p27(X66)))))))&((~r1(skolem0004,X6)|(~r1(skolem0029(X6),X67)|(~p27(X67)|p26(X67))))&(~r1(skolem0004,X6)|(~r1(skolem0029(X6),X67)|(p27(X67)|~p26(X67)))))))&((~r1(skolem0004,X6)|(~r1(skolem0028(X6),X68)|(~p26(X68)|p25(X68))))&(~r1(skolem0004,X6)|(~r1(skolem0028(X6),X68)|(p26(X68)|~p25(X68)))))))&((~r1(skolem0004,X6)|(~r1(skolem0027(X6),X69)|(~p25(X69)|p24(X69))))&(~r1(skolem0004,X6)|(~r1(skolem0027(X6),X69)|(p25(X69)|~p24(X69)))))))&((~r1(skolem0004,X6)|(~r1(skolem0026(X6),X70)|(~p24(X70)|p23(X70))))&(~r1(skolem0004,X6)|(~r1(skolem0026(X6),X70)|(p24(X70)|~p23(X70)))))))&((~r1(skolem0004,X6)|(~r1(skolem0025(X6),X71)|(~p23(X71)|p22(X71))))&(~r1(skolem0004,X6)|(~r1(skolem0025(X6),X71)|(p23(X71)|~p22(X71)))))))&((~r1(skolem0004,X6)|(~r1(skolem0024(X6),X72)|(~p22(X72)|p21(X72))))&(~r1(skolem0004,X6)|(~r1(skolem0024(X6),X72)|(p22(X72)|~p21(X72)))))))&((~r1(skolem0004,X6)|(~r1(skolem0023(X6),X73)|(~p21(X73)|p20(X73))))&(~r1(skolem0004,X6)|(~r1(skolem0023(X6),X73)|(p21(X73)|~p20(X73)))))))&((~r1(skolem0004,X6)|(~r1(skolem0022(X6),X74)|(~p20(X74)|p19(X74))))&(~r1(skolem0004,X6)|(~r1(skolem0022(X6),X74)|(p20(X74)|~p19(X74)))))))&((~r1(skolem0004,X6)|(~r1(skolem0021(X6),X75)|(~p19(X75)|p18(X75))))&(~r1(skolem0004,X6)|(~r1(skolem0021(X6),X75)|(p19(X75)|~p18(X75)))))))&((~r1(skolem0004,X6)|(~r1(skolem0020(X6),X76)|(~p18(X76)|p17(X76))))&(~r1(skolem0004,X6)|(~r1(skolem0020(X6),X76)|(p18(X76)|~p17(X76)))))))&((~r1(skolem0004,X6)|(~r1(skolem0019(X6),X77)|(~p17(X77)|p16(X77))))&(~r1(skolem0004,X6)|(~r1(skolem0019(X6),X77)|(p17(X77)|~p16(X77)))))))&((~r1(skolem0004,X6)|(~r1(skolem0018(X6),X78)|(~p16(X78)|p15(X78))))&(~r1(skolem0004,X6)|(~r1(skolem0018(X6),X78)|(p16(X78)|~p15(X78)))))))&((~r1(skolem0004,X6)|(~r1(skolem0017(X6),X79)|(~p15(X79)|p14(X79))))&(~r1(skolem0004,X6)|(~r1(skolem0017(X6),X79)|(p15(X79)|~p14(X79)))))))&((~r1(skolem0004,X6)|(~r1(skolem0016(X6),X80)|(~p14(X80)|p13(X80))))&(~r1(skolem0004,X6)|(~r1(skolem0016(X6),X80)|(p14(X80)|~p13(X80)))))))&((~r1(skolem0004,X6)|(~r1(skolem0015(X6),X81)|(~p13(X81)|p12(X81))))&(~r1(skolem0004,X6)|(~r1(skolem0015(X6),X81)|(p13(X81)|~p12(X81)))))))&((~r1(skolem0004,X6)|(~r1(skolem0014(X6),X82)|(~p12(X82)|p11(X82))))&(~r1(skolem0004,X6)|(~r1(skolem0014(X6),X82)|(p12(X82)|~p11(X82)))))))&((~r1(skolem0004,X6)|(~r1(skolem0013(X6),X83)|(~p11(X83)|p10(X83))))&(~r1(skolem0004,X6)|(~r1(skolem0013(X6),X83)|(p11(X83)|~p10(X83)))))))&((~r1(skolem0004,X6)|(~r1(skolem0012(X6),X84)|(~p10(X84)|p9(X84))))&(~r1(skolem0004,X6)|(~r1(skolem0012(X6),X84)|(p10(X84)|~p9(X84)))))))&((~r1(skolem0004,X6)|(~r1(skolem0011(X6),X85)|(~p9(X85)|p8(X85))))&(~r1(skolem0004,X6)|(~r1(skolem0011(X6),X85)|(p9(X85)|~p8(X85)))))))&((~r1(skolem0004,X6)|(~r1(skolem0010(X6),X86)|(~p8(X86)|p7(X86))))&(~r1(skolem0004,X6)|(~r1(skolem0010(X6),X86)|(p8(X86)|~p7(X86)))))))&((~r1(skolem0004,X6)|(~r1(skolem0009(X6),X87)|(~p7(X87)|p6(X87))))&(~r1(skolem0004,X6)|(~r1(skolem0009(X6),X87)|(p7(X87)|~p6(X87)))))))&((~r1(skolem0004,X6)|(~r1(skolem0008(X6),X88)|(~p6(X88)|p5(X88))))&(~r1(skolem0004,X6)|(~r1(skolem0008(X6),X88)|(p6(X88)|~p5(X88)))))))&((~r1(skolem0004,X6)|(~r1(skolem0007(X6),X89)|(~p5(X89)|p4(X89))))&(~r1(skolem0004,X6)|(~r1(skolem0007(X6),X89)|(p5(X89)|~p4(X89)))))))&((~r1(skolem0004,X6)|(~r1(skolem0006(X6),X90)|(~p4(X90)|p3(X90))))&(~r1(skolem0004,X6)|(~r1(skolem0006(X6),X90)|(p4(X90)|~p3(X90)))))))&((~r1(skolem0004,X6)|(~r1(skolem0005(X6),X91)|(~p3(X91)|p2(X91))))&(~r1(skolem0004,X6)|(~r1(skolem0005(X6),X91)|(p3(X91)|~p2(X91))))))&((~r1(skolem0004,X6)|(~r1(X6,X92)|(~p2(X92)|p1(X92))))&(~r1(skolem0004,X6)|(~r1(X6,X92)|(p2(X92)|~p1(X92))))))&((~r1(skolem0004,X6)|r1(X6,skolem0048(X6)))&(~r1(skolem0004,X6)|~p45(skolem0048(X6)))))&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~r1(skolem0004,X6)|r1(X6,skolem0049(X6)))&(~r1(skolem0004,X6)|(p43(skolem0049(X6))|p44(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p44(skolem0049(X6))|~p43(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p42(skolem0049(X6))|p43(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p43(skolem0049(X6))|~p42(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p41(skolem0049(X6))|p42(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p42(skolem0049(X6))|~p41(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p40(skolem0049(X6))|p41(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p41(skolem0049(X6))|~p40(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p39(skolem0049(X6))|p40(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p40(skolem0049(X6))|~p39(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p38(skolem0049(X6))|p39(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p39(skolem0049(X6))|~p38(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p37(skolem0049(X6))|p38(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p38(skolem0049(X6))|~p37(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p36(skolem0049(X6))|p37(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p37(skolem0049(X6))|~p36(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p35(skolem0049(X6))|p36(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p36(skolem0049(X6))|~p35(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p34(skolem0049(X6))|p35(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p35(skolem0049(X6))|~p34(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p33(skolem0049(X6))|p34(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p34(skolem0049(X6))|~p33(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p32(skolem0049(X6))|p33(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p33(skolem0049(X6))|~p32(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p31(skolem0049(X6))|p32(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p32(skolem0049(X6))|~p31(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p30(skolem0049(X6))|p31(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p31(skolem0049(X6))|~p30(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p29(skolem0049(X6))|p30(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p30(skolem0049(X6))|~p29(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p28(skolem0049(X6))|p29(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p29(skolem0049(X6))|~p28(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p27(skolem0049(X6))|p28(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p28(skolem0049(X6))|~p27(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p26(skolem0049(X6))|p27(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p27(skolem0049(X6))|~p26(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p25(skolem0049(X6))|p26(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p26(skolem0049(X6))|~p25(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p24(skolem0049(X6))|p25(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p25(skolem0049(X6))|~p24(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p23(skolem0049(X6))|p24(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p24(skolem0049(X6))|~p23(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p22(skolem0049(X6))|p23(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p23(skolem0049(X6))|~p22(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p21(skolem0049(X6))|p22(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p22(skolem0049(X6))|~p21(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p20(skolem0049(X6))|p21(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p21(skolem0049(X6))|~p20(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p19(skolem0049(X6))|p20(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p20(skolem0049(X6))|~p19(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p18(skolem0049(X6))|p19(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p19(skolem0049(X6))|~p18(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p17(skolem0049(X6))|p18(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p18(skolem0049(X6))|~p17(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p16(skolem0049(X6))|p17(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p17(skolem0049(X6))|~p16(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p15(skolem0049(X6))|p16(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p16(skolem0049(X6))|~p15(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p14(skolem0049(X6))|p15(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p15(skolem0049(X6))|~p14(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p13(skolem0049(X6))|p14(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p14(skolem0049(X6))|~p13(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p12(skolem0049(X6))|p13(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p13(skolem0049(X6))|~p12(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p11(skolem0049(X6))|p12(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p12(skolem0049(X6))|~p11(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p10(skolem0049(X6))|p11(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p11(skolem0049(X6))|~p10(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p9(skolem0049(X6))|p10(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p10(skolem0049(X6))|~p9(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p8(skolem0049(X6))|p9(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p9(skolem0049(X6))|~p8(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p7(skolem0049(X6))|p8(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p8(skolem0049(X6))|~p7(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p6(skolem0049(X6))|p7(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p7(skolem0049(X6))|~p6(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p5(skolem0049(X6))|p6(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p6(skolem0049(X6))|~p5(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p4(skolem0049(X6))|p5(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p5(skolem0049(X6))|~p4(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p3(skolem0049(X6))|p4(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p4(skolem0049(X6))|~p3(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p2(skolem0049(X6))|p3(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p3(skolem0049(X6))|~p2(skolem0049(X6)))))&(~r1(skolem0004,X6)|(p1(skolem0049(X6))|p2(skolem0049(X6)))))&(~r1(skolem0004,X6)|(~p2(skolem0049(X6))|~p1(skolem0049(X6)))))))))))))))))))))))))))))))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 10.34/10.65 cnf(c143,negated_conjecture,~r1(skolem0004,X104)|r1(X104,skolem0049(X104)),inference(split_conjunct,[status(thm)],[c6])).
% 10.34/10.65 cnf(c244,plain,r1(skolem0004,skolem0049(skolem0004)),inference(resolution,[status(thm)],[c143, c234])).
% 10.34/10.65 cnf(c140,negated_conjecture,~r1(skolem0004,X388)|~r1(X388,X387)|p2(X387)|~p1(X387),inference(split_conjunct,[status(thm)],[c6])).
% 10.34/10.65 cnf(c3133,plain,~r1(skolem0004,X389)|p2(X389)|~p1(X389),inference(resolution,[status(thm)],[c140, c234])).
% 10.34/10.65 cnf(c3309,plain,p2(skolem0049(skolem0004))|~p1(skolem0049(skolem0004)),inference(resolution,[status(thm)],[c3133, c244])).
% 10.34/10.65 cnf(c228,negated_conjecture,~r1(skolem0004,X500)|p1(skolem0049(X500))|p2(skolem0049(X500)),inference(split_conjunct,[status(thm)],[c6])).
% 10.34/10.65 cnf(c6695,plain,p1(skolem0049(skolem0004))|p2(skolem0049(skolem0004)),inference(resolution,[status(thm)],[c228, c234])).
% 10.34/10.65 cnf(c6726,plain,p2(skolem0049(skolem0004)),inference(resolution,[status(thm)],[c6695, c3309])).
% 10.34/10.65 cnf(c229,negated_conjecture,~r1(skolem0004,X502)|~p2(skolem0049(X502))|~p1(skolem0049(X502)),inference(split_conjunct,[status(thm)],[c6])).
% 10.34/10.65 cnf(c139,negated_conjecture,~r1(skolem0004,X385)|~r1(X385,X384)|~p2(X384)|p1(X384),inference(split_conjunct,[status(thm)],[c6])).
% 10.34/10.65 cnf(c2750,plain,~r1(skolem0004,X386)|~p2(X386)|p1(X386),inference(resolution,[status(thm)],[c139, c234])).
% 10.34/10.65 cnf(c2926,plain,~p2(skolem0049(skolem0004))|p1(skolem0049(skolem0004)),inference(resolution,[status(thm)],[c2750, c244])).
% 10.34/10.65 cnf(c6729,plain,p1(skolem0049(skolem0004)),inference(resolution,[status(thm)],[c6695, c2926])).
% 10.34/10.65 cnf(c6735,plain,~r1(skolem0004,skolem0004)|~p2(skolem0049(skolem0004)),inference(resolution,[status(thm)],[c6729, c229])).
% 10.34/10.65 cnf(c6932,plain,~r1(skolem0004,skolem0004),inference(resolution,[status(thm)],[c6735, c6726])).
% 10.34/10.65 cnf(c6936,plain,$false,inference(resolution,[status(thm)],[c6932, c234])).
% 10.34/10.65 % SZS output end CNFRefutation
% 10.34/10.65
% 10.34/10.65 % Initial clauses : 225
% 10.34/10.65 % Processed clauses : 1060
% 10.34/10.65 % Factors computed : 3
% 10.34/10.65 % Resolvents computed: 6699
% 10.34/10.65 % Tautologies deleted: 2
% 10.34/10.65 % Forward subsumed : 121
% 10.34/10.65 % Backward subsumed : 6
% 10.34/10.65 % -------- CPU Time ---------
% 10.34/10.65 % User time : 10.110 s
% 10.34/10.65 % System time : 0.174 s
% 10.34/10.65 % Total time : 10.284 s
%------------------------------------------------------------------------------