%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 : Thu Sep 24 01:10:57 PM UTC 2026
% Result : Theorem 0.17s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n018.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 00:59:43 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 0.17/0.50 % Refutation found
% 0.17/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.50 fof(f1,axiom,(
% 0.17/0.50 (! [X] : r1(X,X) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f3,conjecture,(
% 0.17/0.50 ~ (? [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) ) ) )) ) )) )) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f4,negated_conjecture,(
% 0.17/0.50 ~(~ (? [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) ) ) )) ) )) )) ))),
% 0.17/0.50 inference(negated_conjecture,[status(cth)],[f3])).
% 0.17/0.50 fof(f5,plain,(
% 0.17/0.50 ![X0]: (r1(X0,X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f1])).
% 0.17/0.50 fof(f9,plain,(
% 0.17/0.50 ?[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)&$true)))&(![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))))))))))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.17/0.50 fof(f10,plain,(
% 0.17/0.50 ?[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))&$true))&(![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))))))))))),
% 0.17/0.50 inference(miniscoping,[status(thm)],[f9])).
% 0.17/0.50 fof(f11,plain,(
% 0.17/0.50 (((r1(sK0_skl,sK1_skl)&p30(sK1_skl))&(r1(sK1_skl,sK2_skl)&p1(sK2_skl)))&(r1(sK0_skl,sK3_skl)&(![X]: (~r1(sK3_skl,X)|(((((r1(X,sK4_skl(X))&((r1(sK4_skl(X),sK5_skl(X))&((r1(sK5_skl(X),sK6_skl(X))&((r1(sK6_skl(X),sK7_skl(X))&((r1(sK7_skl(X),sK8_skl(X))&((r1(sK8_skl(X),sK9_skl(X))&((r1(sK9_skl(X),sK10_skl(X))&((r1(sK10_skl(X),sK11_skl(X))&((r1(sK11_skl(X),sK12_skl(X))&((r1(sK12_skl(X),sK13_skl(X))&((r1(sK13_skl(X),sK14_skl(X))&((r1(sK14_skl(X),sK15_skl(X))&((r1(sK15_skl(X),sK16_skl(X))&((r1(sK16_skl(X),sK17_skl(X))&((r1(sK17_skl(X),sK18_skl(X))&((r1(sK18_skl(X),sK19_skl(X))&((r1(sK19_skl(X),sK20_skl(X))&((r1(sK20_skl(X),sK21_skl(X))&((r1(sK21_skl(X),sK22_skl(X))&((r1(sK22_skl(X),sK23_skl(X))&((r1(sK23_skl(X),sK24_skl(X))&((r1(sK24_skl(X),sK25_skl(X))&((r1(sK25_skl(X),sK26_skl(X))&((r1(sK26_skl(X),sK27_skl(X))&((r1(sK27_skl(X),sK28_skl(X))&((r1(sK28_skl(X),sK29_skl(X))&((r1(sK29_skl(X),sK30_skl(X))&(r1(sK30_skl(X),sK31_skl(X))&$true))&(![X]: (~r1(sK30_skl(X),X)|((~p29(X)|p28(X))&(p29(X)|~p28(X)))))))&(![Y]: (~r1(sK29_skl(X),Y)|((~p28(Y)|p27(Y))&(p28(Y)|~p27(Y)))))))&(![X]: (~r1(sK28_skl(X),X)|((~p27(X)|p26(X))&(p27(X)|~p26(X)))))))&(![Y]: (~r1(sK27_skl(X),Y)|((~p26(Y)|p25(Y))&(p26(Y)|~p25(Y)))))))&(![X]: (~r1(sK26_skl(X),X)|((~p25(X)|p24(X))&(p25(X)|~p24(X)))))))&(![Y]: (~r1(sK25_skl(X),Y)|((~p24(Y)|p23(Y))&(p24(Y)|~p23(Y)))))))&(![X]: (~r1(sK24_skl(X),X)|((~p23(X)|p22(X))&(p23(X)|~p22(X)))))))&(![Y]: (~r1(sK23_skl(X),Y)|((~p22(Y)|p21(Y))&(p22(Y)|~p21(Y)))))))&(![X]: (~r1(sK22_skl(X),X)|((~p21(X)|p20(X))&(p21(X)|~p20(X)))))))&(![Y]: (~r1(sK21_skl(X),Y)|((~p20(Y)|p19(Y))&(p20(Y)|~p19(Y)))))))&(![X]: (~r1(sK20_skl(X),X)|((~p19(X)|p18(X))&(p19(X)|~p18(X)))))))&(![Y]: (~r1(sK19_skl(X),Y)|((~p18(Y)|p17(Y))&(p18(Y)|~p17(Y)))))))&(![X]: (~r1(sK18_skl(X),X)|((~p17(X)|p16(X))&(p17(X)|~p16(X)))))))&(![Y]: (~r1(sK17_skl(X),Y)|((~p16(Y)|p15(Y))&(p16(Y)|~p15(Y)))))))&(![X]: (~r1(sK16_skl(X),X)|((~p15(X)|p14(X))&(p15(X)|~p14(X)))))))&(![Y]: (~r1(sK15_skl(X),Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y)))))))&(![X]: (~r1(sK14_skl(X),X)|((~p13(X)|p12(X))&(p13(X)|~p12(X)))))))&(![Y]: (~r1(sK13_skl(X),Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y)))))))&(![X]: (~r1(sK12_skl(X),X)|((~p11(X)|p10(X))&(p11(X)|~p10(X)))))))&(![Y]: (~r1(sK11_skl(X),Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y)))))))&(![X]: (~r1(sK10_skl(X),X)|((~p9(X)|p8(X))&(p9(X)|~p8(X)))))))&(![Y]: (~r1(sK9_skl(X),Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y)))))))&(![X]: (~r1(sK8_skl(X),X)|((~p7(X)|p6(X))&(p7(X)|~p6(X)))))))&(![Y]: (~r1(sK7_skl(X),Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y)))))))&(![X]: (~r1(sK6_skl(X),X)|((~p5(X)|p4(X))&(p5(X)|~p4(X)))))))&(![Y]: (~r1(sK5_skl(X),Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y)))))))&(![X]: (~r1(sK4_skl(X),X)|((~p3(X)|p2(X))&(p3(X)|~p2(X))))))&(![Y]: (~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(r1(X,sK32_skl(X))&~p30(sK32_skl(X))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,sK33_skl(X))&(p28(sK33_skl(X))|p29(sK33_skl(X))))&(~p29(sK33_skl(X))|~p28(sK33_skl(X))))&(p27(sK33_skl(X))|p28(sK33_skl(X))))&(~p28(sK33_skl(X))|~p27(sK33_skl(X))))&(p26(sK33_skl(X))|p27(sK33_skl(X))))&(~p27(sK33_skl(X))|~p26(sK33_skl(X))))&(p25(sK33_skl(X))|p26(sK33_skl(X))))&(~p26(sK33_skl(X))|~p25(sK33_skl(X))))&(p24(sK33_skl(X))|p25(sK33_skl(X))))&(~p25(sK33_skl(X))|~p24(sK33_skl(X))))&(p23(sK33_skl(X))|p24(sK33_skl(X))))&(~p24(sK33_skl(X))|~p23(sK33_skl(X))))&(p22(sK33_skl(X))|p23(sK33_skl(X))))&(~p23(sK33_skl(X))|~p22(sK33_skl(X))))&(p21(sK33_skl(X))|p22(sK33_skl(X))))&(~p22(sK33_skl(X))|~p21(sK33_skl(X))))&(p20(sK33_skl(X))|p21(sK33_skl(X))))&(~p21(sK33_skl(X))|~p20(sK33_skl(X))))&(p19(sK33_skl(X))|p20(sK33_skl(X))))&(~p20(sK33_skl(X))|~p19(sK33_skl(X))))&(p18(sK33_skl(X))|p19(sK33_skl(X))))&(~p19(sK33_skl(X))|~p18(sK33_skl(X))))&(p17(sK33_skl(X))|p18(sK33_skl(X))))&(~p18(sK33_skl(X))|~p17(sK33_skl(X))))&(p16(sK33_skl(X))|p17(sK33_skl(X))))&(~p17(sK33_skl(X))|~p16(sK33_skl(X))))&(p15(sK33_skl(X))|p16(sK33_skl(X))))&(~p16(sK33_skl(X))|~p15(sK33_skl(X))))&(p14(sK33_skl(X))|p15(sK33_skl(X))))&(~p15(sK33_skl(X))|~p14(sK33_skl(X))))&(p13(sK33_skl(X))|p14(sK33_skl(X))))&(~p14(sK33_skl(X))|~p13(sK33_skl(X))))&(p12(sK33_skl(X))|p13(sK33_skl(X))))&(~p13(sK33_skl(X))|~p12(sK33_skl(X))))&(p11(sK33_skl(X))|p12(sK33_skl(X))))&(~p12(sK33_skl(X))|~p11(sK33_skl(X))))&(p10(sK33_skl(X))|p11(sK33_skl(X))))&(~p11(sK33_skl(X))|~p10(sK33_skl(X))))&(p9(sK33_skl(X))|p10(sK33_skl(X))))&(~p10(sK33_skl(X))|~p9(sK33_skl(X))))&(p8(sK33_skl(X))|p9(sK33_skl(X))))&(~p9(sK33_skl(X))|~p8(sK33_skl(X))))&(p7(sK33_skl(X))|p8(sK33_skl(X))))&(~p8(sK33_skl(X))|~p7(sK33_skl(X))))&(p6(sK33_skl(X))|p7(sK33_skl(X))))&(~p7(sK33_skl(X))|~p6(sK33_skl(X))))&(p5(sK33_skl(X))|p6(sK33_skl(X))))&(~p6(sK33_skl(X))|~p5(sK33_skl(X))))&(p4(sK33_skl(X))|p5(sK33_skl(X))))&(~p5(sK33_skl(X))|~p4(sK33_skl(X))))&(p3(sK33_skl(X))|p4(sK33_skl(X))))&(~p4(sK33_skl(X))|~p3(sK33_skl(X))))&(p2(sK33_skl(X))|p3(sK33_skl(X))))&(~p3(sK33_skl(X))|~p2(sK33_skl(X))))&(p1(sK33_skl(X))|p2(sK33_skl(X))))&(~p2(sK33_skl(X))|~p1(sK33_skl(X)))))))))),
% 0.17/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl,sK31_skl,sK32_skl,sK33_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl),skolemize(X,sK2_skl),skolemize(Y,sK3_skl),skolemize(Y,sK4_skl(X)),skolemize(X,sK5_skl(X)),skolemize(Y,sK6_skl(X)),skolemize(X,sK7_skl(X)),skolemize(Y,sK8_skl(X)),skolemize(X,sK9_skl(X)),skolemize(Y,sK10_skl(X)),skolemize(X,sK11_skl(X)),skolemize(Y,sK12_skl(X)),skolemize(X,sK13_skl(X)),skolemize(Y,sK14_skl(X)),skolemize(X,sK15_skl(X)),skolemize(Y,sK16_skl(X)),skolemize(X,sK17_skl(X)),skolemize(Y,sK18_skl(X)),skolemize(X,sK19_skl(X)),skolemize(Y,sK20_skl(X)),skolemize(X,sK21_skl(X)),skolemize(Y,sK22_skl(X)),skolemize(X,sK23_skl(X)),skolemize(Y,sK24_skl(X)),skolemize(X,sK25_skl(X)),skolemize(Y,sK26_skl(X)),skolemize(X,sK27_skl(X)),skolemize(Y,sK28_skl(X)),skolemize(X,sK29_skl(X)),skolemize(Y,sK30_skl(X)),skolemize(X,sK31_skl(X)),skolemize(Y,sK32_skl(X)),skolemize(Y,sK33_skl(X))],[f10])).
% 0.17/0.50 fof(f12,plain,(
% 0.17/0.50 ?[X]: ((?[Y]: ((r1(sK0_skl,sK1_skl)&p30(sK1_skl))&(?[X]: (r1(sK1_skl,sK2_skl)&p1(sK2_skl)))))&(?[Y]: (r1(sK0_skl,sK3_skl)&(![X]: (~r1(sK3_skl,X)|((((?[Y]: ((r1(X,sK4_skl(X))&(?[X]: ((r1(sK4_skl(X),sK5_skl(X))&(?[Y]: ((r1(sK5_skl(X),sK6_skl(X))&(?[X]: ((r1(sK6_skl(X),sK7_skl(X))&(?[Y]: ((r1(sK7_skl(X),sK8_skl(X))&(?[X]: ((r1(sK8_skl(X),sK9_skl(X))&(?[Y]: ((r1(sK9_skl(X),sK10_skl(X))&(?[X]: ((r1(sK10_skl(X),sK11_skl(X))&(?[Y]: ((r1(sK11_skl(X),sK12_skl(X))&(?[X]: ((r1(sK12_skl(X),sK13_skl(X))&(?[Y]: ((r1(sK13_skl(X),sK14_skl(X))&(?[X]: ((r1(sK14_skl(X),sK15_skl(X))&(?[Y]: ((r1(sK15_skl(X),sK16_skl(X))&(?[X]: ((r1(sK16_skl(X),sK17_skl(X))&(?[Y]: ((r1(sK17_skl(X),sK18_skl(X))&(?[X]: ((r1(sK18_skl(X),sK19_skl(X))&(?[Y]: ((r1(sK19_skl(X),sK20_skl(X))&(?[X]: ((r1(sK20_skl(X),sK21_skl(X))&(?[Y]: ((r1(sK21_skl(X),sK22_skl(X))&(?[X]: ((r1(sK22_skl(X),sK23_skl(X))&(?[Y]: ((r1(sK23_skl(X),sK24_skl(X))&(?[X]: ((r1(sK24_skl(X),sK25_skl(X))&(?[Y]: ((r1(sK25_skl(X),sK26_skl(X))&(?[X]: ((r1(sK26_skl(X),sK27_skl(X))&(?[Y]: ((r1(sK27_skl(X),sK28_skl(X))&(?[X]: ((r1(sK28_skl(X),sK29_skl(X))&(?[Y]: ((r1(sK29_skl(X),sK30_skl(X))&(?[X]: r1(sK30_skl(X),sK31_skl(X))))&(![X]: (~r1(sK30_skl(X),X)|((~p29(X)|p28(X))&(p29(X)|~p28(X))))))))&(![Y]: (~r1(sK29_skl(X),Y)|((~p28(Y)|p27(Y))&(p28(Y)|~p27(Y))))))))&(![X]: (~r1(sK28_skl(X),X)|((~p27(X)|p26(X))&(p27(X)|~p26(X))))))))&(![Y]: (~r1(sK27_skl(X),Y)|((~p26(Y)|p25(Y))&(p26(Y)|~p25(Y))))))))&(![X]: (~r1(sK26_skl(X),X)|((~p25(X)|p24(X))&(p25(X)|~p24(X))))))))&(![Y]: (~r1(sK25_skl(X),Y)|((~p24(Y)|p23(Y))&(p24(Y)|~p23(Y))))))))&(![X]: (~r1(sK24_skl(X),X)|((~p23(X)|p22(X))&(p23(X)|~p22(X))))))))&(![Y]: (~r1(sK23_skl(X),Y)|((~p22(Y)|p21(Y))&(p22(Y)|~p21(Y))))))))&(![X]: (~r1(sK22_skl(X),X)|((~p21(X)|p20(X))&(p21(X)|~p20(X))))))))&(![Y]: (~r1(sK21_skl(X),Y)|((~p20(Y)|p19(Y))&(p20(Y)|~p19(Y))))))))&(![X]: (~r1(sK20_skl(X),X)|((~p19(X)|p18(X))&(p19(X)|~p18(X))))))))&(![Y]: (~r1(sK19_skl(X),Y)|((~p18(Y)|p17(Y))&(p18(Y)|~p17(Y))))))))&(![X]: (~r1(sK18_skl(X),X)|((~p17(X)|p16(X))&(p17(X)|~p16(X))))))))&(![Y]: (~r1(sK17_skl(X),Y)|((~p16(Y)|p15(Y))&(p16(Y)|~p15(Y))))))))&(![X]: (~r1(sK16_skl(X),X)|((~p15(X)|p14(X))&(p15(X)|~p14(X))))))))&(![Y]: (~r1(sK15_skl(X),Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y))))))))&(![X]: (~r1(sK14_skl(X),X)|((~p13(X)|p12(X))&(p13(X)|~p12(X))))))))&(![Y]: (~r1(sK13_skl(X),Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y))))))))&(![X]: (~r1(sK12_skl(X),X)|((~p11(X)|p10(X))&(p11(X)|~p10(X))))))))&(![Y]: (~r1(sK11_skl(X),Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y))))))))&(![X]: (~r1(sK10_skl(X),X)|((~p9(X)|p8(X))&(p9(X)|~p8(X))))))))&(![Y]: (~r1(sK9_skl(X),Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y))))))))&(![X]: (~r1(sK8_skl(X),X)|((~p7(X)|p6(X))&(p7(X)|~p6(X))))))))&(![Y]: (~r1(sK7_skl(X),Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y))))))))&(![X]: (~r1(sK6_skl(X),X)|((~p5(X)|p4(X))&(p5(X)|~p4(X))))))))&(![Y]: (~r1(sK5_skl(X),Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y))))))))&(![X]: (~r1(sK4_skl(X),X)|((~p3(X)|p2(X))&(p3(X)|~p2(X)))))))&(![Y]: (~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(?[Y]: (r1(X,sK32_skl(X))&~p30(sK32_skl(X)))))&(?[Y]: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,sK33_skl(X))&(p28(sK33_skl(X))|p29(sK33_skl(X))))&(~p29(sK33_skl(X))|~p28(sK33_skl(X))))&(p27(sK33_skl(X))|p28(sK33_skl(X))))&(~p28(sK33_skl(X))|~p27(sK33_skl(X))))&(p26(sK33_skl(X))|p27(sK33_skl(X))))&(~p27(sK33_skl(X))|~p26(sK33_skl(X))))&(p25(sK33_skl(X))|p26(sK33_skl(X))))&(~p26(sK33_skl(X))|~p25(sK33_skl(X))))&(p24(sK33_skl(X))|p25(sK33_skl(X))))&(~p25(sK33_skl(X))|~p24(sK33_skl(X))))&(p23(sK33_skl(X))|p24(sK33_skl(X))))&(~p24(sK33_skl(X))|~p23(sK33_skl(X))))&(p22(sK33_skl(X))|p23(sK33_skl(X))))&(~p23(sK33_skl(X))|~p22(sK33_skl(X))))&(p21(sK33_skl(X))|p22(sK33_skl(X))))&(~p22(sK33_skl(X))|~p21(sK33_skl(X))))&(p20(sK33_skl(X))|p21(sK33_skl(X))))&(~p21(sK33_skl(X))|~p20(sK33_skl(X))))&(p19(sK33_skl(X))|p20(sK33_skl(X))))&(~p20(sK33_skl(X))|~p19(sK33_skl(X))))&(p18(sK33_skl(X))|p19(sK33_skl(X))))&(~p19(sK33_skl(X))|~p18(sK33_skl(X))))&(p17(sK33_skl(X))|p18(sK33_skl(X))))&(~p18(sK33_skl(X))|~p17(sK33_skl(X))))&(p16(sK33_skl(X))|p17(sK33_skl(X))))&(~p17(sK33_skl(X))|~p16(sK33_skl(X))))&(p15(sK33_skl(X))|p16(sK33_skl(X))))&(~p16(sK33_skl(X))|~p15(sK33_skl(X))))&(p14(sK33_skl(X))|p15(sK33_skl(X))))&(~p15(sK33_skl(X))|~p14(sK33_skl(X))))&(p13(sK33_skl(X))|p14(sK33_skl(X))))&(~p14(sK33_skl(X))|~p13(sK33_skl(X))))&(p12(sK33_skl(X))|p13(sK33_skl(X))))&(~p13(sK33_skl(X))|~p12(sK33_skl(X))))&(p11(sK33_skl(X))|p12(sK33_skl(X))))&(~p12(sK33_skl(X))|~p11(sK33_skl(X))))&(p10(sK33_skl(X))|p11(sK33_skl(X))))&(~p11(sK33_skl(X))|~p10(sK33_skl(X))))&(p9(sK33_skl(X))|p10(sK33_skl(X))))&(~p10(sK33_skl(X))|~p9(sK33_skl(X))))&(p8(sK33_skl(X))|p9(sK33_skl(X))))&(~p9(sK33_skl(X))|~p8(sK33_skl(X))))&(p7(sK33_skl(X))|p8(sK33_skl(X))))&(~p8(sK33_skl(X))|~p7(sK33_skl(X))))&(p6(sK33_skl(X))|p7(sK33_skl(X))))&(~p7(sK33_skl(X))|~p6(sK33_skl(X))))&(p5(sK33_skl(X))|p6(sK33_skl(X))))&(~p6(sK33_skl(X))|~p5(sK33_skl(X))))&(p4(sK33_skl(X))|p5(sK33_skl(X))))&(~p5(sK33_skl(X))|~p4(sK33_skl(X))))&(p3(sK33_skl(X))|p4(sK33_skl(X))))&(~p4(sK33_skl(X))|~p3(sK33_skl(X))))&(p2(sK33_skl(X))|p3(sK33_skl(X))))&(~p3(sK33_skl(X))|~p2(sK33_skl(X))))&(p1(sK33_skl(X))|p2(sK33_skl(X))))&(~p2(sK33_skl(X))|~p1(sK33_skl(X)))))))))))),
% 0.17/0.50 inference(true_and_false_simplification,[status(thm)],[f11])).
% 0.17/0.50 fof(f18,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|r1(X0,sK4_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f100,plain,(
% 0.17/0.50 ![X0,X1]: (~r1(sK3_skl,X0)|~r1(X0,X1)|~p2(X1)|p1(X1))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f101,plain,(
% 0.17/0.50 ![X0,X1]: (~r1(sK3_skl,X0)|~r1(X0,X1)|p2(X1)|~p1(X1))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f104,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|r1(X0,sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f105,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p28(sK33_skl(X0))|p29(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f106,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p29(sK33_skl(X0))|~p28(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f107,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p27(sK33_skl(X0))|p28(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f108,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p28(sK33_skl(X0))|~p27(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f109,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p26(sK33_skl(X0))|p27(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f110,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p27(sK33_skl(X0))|~p26(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f111,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p25(sK33_skl(X0))|p26(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f113,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p24(sK33_skl(X0))|p25(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f114,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p25(sK33_skl(X0))|~p24(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f115,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p23(sK33_skl(X0))|p24(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f117,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p22(sK33_skl(X0))|p23(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f118,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p23(sK33_skl(X0))|~p22(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f119,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p21(sK33_skl(X0))|p22(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f121,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p20(sK33_skl(X0))|p21(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f122,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p21(sK33_skl(X0))|~p20(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f123,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p19(sK33_skl(X0))|p20(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f125,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p18(sK33_skl(X0))|p19(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f126,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p19(sK33_skl(X0))|~p18(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f127,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p17(sK33_skl(X0))|p18(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f129,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p16(sK33_skl(X0))|p17(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f130,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p17(sK33_skl(X0))|~p16(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f131,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p15(sK33_skl(X0))|p16(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f133,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p14(sK33_skl(X0))|p15(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f134,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p15(sK33_skl(X0))|~p14(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f135,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p13(sK33_skl(X0))|p14(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f137,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p12(sK33_skl(X0))|p13(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f138,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p13(sK33_skl(X0))|~p12(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f139,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p11(sK33_skl(X0))|p12(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f141,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p10(sK33_skl(X0))|p11(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f142,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p11(sK33_skl(X0))|~p10(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f143,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p9(sK33_skl(X0))|p10(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f145,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p8(sK33_skl(X0))|p9(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f146,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p9(sK33_skl(X0))|~p8(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f147,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p7(sK33_skl(X0))|p8(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f149,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p6(sK33_skl(X0))|p7(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f150,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p7(sK33_skl(X0))|~p6(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f151,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p5(sK33_skl(X0))|p6(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f153,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p4(sK33_skl(X0))|p5(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f154,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p5(sK33_skl(X0))|~p4(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f155,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p3(sK33_skl(X0))|p4(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f157,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p2(sK33_skl(X0))|p3(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f158,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p3(sK33_skl(X0))|~p2(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f159,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p1(sK33_skl(X0))|p2(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f160,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p2(sK33_skl(X0))|~p1(sK33_skl(X0)))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.50 fof(f165,plain,(
% 0.17/0.50 r1(sK3_skl,sK4_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f18,f5])).
% 0.17/0.50 fof(f184,plain,(
% 0.17/0.50 p28(sK33_skl(sK3_skl))|p29(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f105,f5])).
% 0.17/0.50 fof(f192,definition,(
% 0.17/0.50 sQ2_spl <=> (p28(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f193,plain,(
% 0.17/0.50 p28(sK33_skl(sK3_skl))|~sQ2_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f192])).
% 0.17/0.50 fof(f195,definition,(
% 0.17/0.50 sQ3_spl <=> (p29(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f198,plain,(
% 0.17/0.50 sQ2_spl|sQ3_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f184,f192,f195])).
% 0.17/0.50 fof(f200,plain,(
% 0.17/0.50 p27(sK33_skl(sK3_skl))|p28(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f107,f5])).
% 0.17/0.50 fof(f205,definition,(
% 0.17/0.50 sQ5_spl <=> (p27(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f206,plain,(
% 0.17/0.50 p27(sK33_skl(sK3_skl))|~sQ5_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f205])).
% 0.17/0.50 fof(f208,plain,(
% 0.17/0.50 sQ5_spl|sQ2_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f200,f205,f192])).
% 0.17/0.50 fof(f210,plain,(
% 0.17/0.50 p26(sK33_skl(sK3_skl))|p27(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f109,f5])).
% 0.17/0.50 fof(f215,definition,(
% 0.17/0.50 sQ7_spl <=> (p26(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f216,plain,(
% 0.17/0.50 p26(sK33_skl(sK3_skl))|~sQ7_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f215])).
% 0.17/0.50 fof(f218,plain,(
% 0.17/0.50 sQ7_spl|sQ5_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f210,f215,f205])).
% 0.17/0.50 fof(f220,plain,(
% 0.17/0.50 p25(sK33_skl(sK3_skl))|p26(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f111,f5])).
% 0.17/0.50 fof(f225,definition,(
% 0.17/0.50 sQ9_spl <=> (p25(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f228,plain,(
% 0.17/0.50 sQ9_spl|sQ7_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f220,f225,f215])).
% 0.17/0.50 fof(f230,plain,(
% 0.17/0.50 p24(sK33_skl(sK3_skl))|p25(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f113,f5])).
% 0.17/0.50 fof(f235,definition,(
% 0.17/0.50 sQ11_spl <=> (p24(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f236,plain,(
% 0.17/0.50 p24(sK33_skl(sK3_skl))|~sQ11_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f235])).
% 0.17/0.50 fof(f238,plain,(
% 0.17/0.50 sQ11_spl|sQ9_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f230,f235,f225])).
% 0.17/0.50 fof(f240,plain,(
% 0.17/0.50 p23(sK33_skl(sK3_skl))|p24(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f115,f5])).
% 0.17/0.50 fof(f245,definition,(
% 0.17/0.50 sQ13_spl <=> (p23(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f248,plain,(
% 0.17/0.50 sQ13_spl|sQ11_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f240,f245,f235])).
% 0.17/0.50 fof(f250,plain,(
% 0.17/0.50 p22(sK33_skl(sK3_skl))|p23(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f117,f5])).
% 0.17/0.50 fof(f255,definition,(
% 0.17/0.50 sQ15_spl <=> (p22(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f256,plain,(
% 0.17/0.50 p22(sK33_skl(sK3_skl))|~sQ15_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f255])).
% 0.17/0.50 fof(f258,plain,(
% 0.17/0.50 sQ15_spl|sQ13_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f250,f255,f245])).
% 0.17/0.50 fof(f260,plain,(
% 0.17/0.50 p21(sK33_skl(sK3_skl))|p22(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f119,f5])).
% 0.17/0.50 fof(f265,definition,(
% 0.17/0.50 sQ17_spl <=> (p21(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f268,plain,(
% 0.17/0.50 sQ17_spl|sQ15_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f260,f265,f255])).
% 0.17/0.50 fof(f270,plain,(
% 0.17/0.50 p20(sK33_skl(sK3_skl))|p21(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f121,f5])).
% 0.17/0.50 fof(f275,definition,(
% 0.17/0.50 sQ19_spl <=> (p20(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f276,plain,(
% 0.17/0.50 p20(sK33_skl(sK3_skl))|~sQ19_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f275])).
% 0.17/0.50 fof(f278,plain,(
% 0.17/0.50 sQ19_spl|sQ17_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f270,f275,f265])).
% 0.17/0.50 fof(f280,plain,(
% 0.17/0.50 p19(sK33_skl(sK3_skl))|p20(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f123,f5])).
% 0.17/0.50 fof(f285,definition,(
% 0.17/0.50 sQ21_spl <=> (p19(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f288,plain,(
% 0.17/0.50 sQ21_spl|sQ19_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f280,f285,f275])).
% 0.17/0.50 fof(f290,plain,(
% 0.17/0.50 p18(sK33_skl(sK3_skl))|p19(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f125,f5])).
% 0.17/0.50 fof(f295,definition,(
% 0.17/0.50 sQ23_spl <=> (p18(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f296,plain,(
% 0.17/0.50 p18(sK33_skl(sK3_skl))|~sQ23_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f295])).
% 0.17/0.50 fof(f298,plain,(
% 0.17/0.50 sQ23_spl|sQ21_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f290,f295,f285])).
% 0.17/0.50 fof(f300,plain,(
% 0.17/0.50 p17(sK33_skl(sK3_skl))|p18(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f127,f5])).
% 0.17/0.50 fof(f305,definition,(
% 0.17/0.50 sQ25_spl <=> (p17(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f308,plain,(
% 0.17/0.50 sQ25_spl|sQ23_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f300,f305,f295])).
% 0.17/0.50 fof(f310,plain,(
% 0.17/0.50 p16(sK33_skl(sK3_skl))|p17(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f129,f5])).
% 0.17/0.50 fof(f315,definition,(
% 0.17/0.50 sQ27_spl <=> (p16(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f316,plain,(
% 0.17/0.50 p16(sK33_skl(sK3_skl))|~sQ27_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f315])).
% 0.17/0.50 fof(f318,plain,(
% 0.17/0.50 sQ27_spl|sQ25_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f310,f315,f305])).
% 0.17/0.50 fof(f320,plain,(
% 0.17/0.50 p15(sK33_skl(sK3_skl))|p16(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f131,f5])).
% 0.17/0.50 fof(f325,definition,(
% 0.17/0.50 sQ29_spl <=> (p15(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f328,plain,(
% 0.17/0.50 sQ29_spl|sQ27_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f320,f325,f315])).
% 0.17/0.50 fof(f330,plain,(
% 0.17/0.50 p14(sK33_skl(sK3_skl))|p15(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f133,f5])).
% 0.17/0.50 fof(f335,definition,(
% 0.17/0.50 sQ31_spl <=> (p14(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f336,plain,(
% 0.17/0.50 p14(sK33_skl(sK3_skl))|~sQ31_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f335])).
% 0.17/0.50 fof(f338,plain,(
% 0.17/0.50 sQ31_spl|sQ29_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f330,f335,f325])).
% 0.17/0.50 fof(f340,plain,(
% 0.17/0.50 p13(sK33_skl(sK3_skl))|p14(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f135,f5])).
% 0.17/0.50 fof(f345,definition,(
% 0.17/0.50 sQ33_spl <=> (p13(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f348,plain,(
% 0.17/0.50 sQ33_spl|sQ31_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f340,f345,f335])).
% 0.17/0.50 fof(f350,plain,(
% 0.17/0.50 p12(sK33_skl(sK3_skl))|p13(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f137,f5])).
% 0.17/0.50 fof(f355,definition,(
% 0.17/0.50 sQ35_spl <=> (p12(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f356,plain,(
% 0.17/0.50 p12(sK33_skl(sK3_skl))|~sQ35_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f355])).
% 0.17/0.50 fof(f358,plain,(
% 0.17/0.50 sQ35_spl|sQ33_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f350,f355,f345])).
% 0.17/0.50 fof(f360,plain,(
% 0.17/0.50 p11(sK33_skl(sK3_skl))|p12(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f139,f5])).
% 0.17/0.50 fof(f365,definition,(
% 0.17/0.50 sQ37_spl <=> (p11(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f368,plain,(
% 0.17/0.50 sQ37_spl|sQ35_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f360,f365,f355])).
% 0.17/0.50 fof(f370,plain,(
% 0.17/0.50 p10(sK33_skl(sK3_skl))|p11(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f141,f5])).
% 0.17/0.50 fof(f375,definition,(
% 0.17/0.50 sQ39_spl <=> (p10(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f376,plain,(
% 0.17/0.50 p10(sK33_skl(sK3_skl))|~sQ39_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f375])).
% 0.17/0.50 fof(f378,plain,(
% 0.17/0.50 sQ39_spl|sQ37_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f370,f375,f365])).
% 0.17/0.50 fof(f380,plain,(
% 0.17/0.50 p9(sK33_skl(sK3_skl))|p10(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f143,f5])).
% 0.17/0.50 fof(f385,definition,(
% 0.17/0.50 sQ41_spl <=> (p9(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f388,plain,(
% 0.17/0.50 sQ41_spl|sQ39_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f380,f385,f375])).
% 0.17/0.50 fof(f390,plain,(
% 0.17/0.50 p8(sK33_skl(sK3_skl))|p9(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f145,f5])).
% 0.17/0.50 fof(f395,definition,(
% 0.17/0.50 sQ43_spl <=> (p8(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f396,plain,(
% 0.17/0.50 p8(sK33_skl(sK3_skl))|~sQ43_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f395])).
% 0.17/0.50 fof(f398,plain,(
% 0.17/0.50 sQ43_spl|sQ41_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f390,f395,f385])).
% 0.17/0.50 fof(f400,plain,(
% 0.17/0.50 p7(sK33_skl(sK3_skl))|p8(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f147,f5])).
% 0.17/0.50 fof(f405,definition,(
% 0.17/0.50 sQ45_spl <=> (p7(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f408,plain,(
% 0.17/0.50 sQ45_spl|sQ43_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f400,f405,f395])).
% 0.17/0.50 fof(f410,plain,(
% 0.17/0.50 p6(sK33_skl(sK3_skl))|p7(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f149,f5])).
% 0.17/0.50 fof(f415,definition,(
% 0.17/0.50 sQ47_spl <=> (p6(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f416,plain,(
% 0.17/0.50 p6(sK33_skl(sK3_skl))|~sQ47_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f415])).
% 0.17/0.50 fof(f418,plain,(
% 0.17/0.50 sQ47_spl|sQ45_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f410,f415,f405])).
% 0.17/0.50 fof(f420,plain,(
% 0.17/0.50 p5(sK33_skl(sK3_skl))|p6(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f151,f5])).
% 0.17/0.50 fof(f425,definition,(
% 0.17/0.50 sQ49_spl <=> (p5(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f428,plain,(
% 0.17/0.50 sQ49_spl|sQ47_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f420,f425,f415])).
% 0.17/0.50 fof(f430,plain,(
% 0.17/0.50 p4(sK33_skl(sK3_skl))|p5(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f153,f5])).
% 0.17/0.50 fof(f435,definition,(
% 0.17/0.50 sQ51_spl <=> (p4(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f436,plain,(
% 0.17/0.50 p4(sK33_skl(sK3_skl))|~sQ51_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f435])).
% 0.17/0.50 fof(f438,plain,(
% 0.17/0.50 sQ51_spl|sQ49_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f430,f435,f425])).
% 0.17/0.50 fof(f440,plain,(
% 0.17/0.50 p3(sK33_skl(sK3_skl))|p4(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f155,f5])).
% 0.17/0.50 fof(f445,definition,(
% 0.17/0.50 sQ53_spl <=> (p3(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f448,plain,(
% 0.17/0.50 sQ53_spl|sQ51_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f440,f445,f435])).
% 0.17/0.50 fof(f450,plain,(
% 0.17/0.50 p2(sK33_skl(sK3_skl))|p3(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f157,f5])).
% 0.17/0.50 fof(f455,definition,(
% 0.17/0.50 sQ55_spl <=> (p2(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f456,plain,(
% 0.17/0.50 p2(sK33_skl(sK3_skl))|~sQ55_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f455])).
% 0.17/0.50 fof(f458,plain,(
% 0.17/0.50 sQ55_spl|sQ53_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f450,f455,f445])).
% 0.17/0.50 fof(f460,plain,(
% 0.17/0.50 p1(sK33_skl(sK3_skl))|p2(sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f159,f5])).
% 0.17/0.50 fof(f465,definition,(
% 0.17/0.50 sQ57_spl <=> (p1(sK33_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f468,plain,(
% 0.17/0.50 sQ57_spl|sQ55_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f460,f465,f455])).
% 0.17/0.50 fof(f564,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|~p2(X0)|p1(X0))),
% 0.17/0.50 inference(resolution,[status(thm)],[f100,f5])).
% 0.17/0.50 fof(f566,plain,(
% 0.17/0.50 ![X0]: (~r1(sK3_skl,X0)|p2(X0)|~p1(X0))),
% 0.17/0.50 inference(resolution,[status(thm)],[f101,f5])).
% 0.17/0.50 fof(f570,plain,(
% 0.17/0.50 r1(sK3_skl,sK33_skl(sK3_skl))),
% 0.17/0.50 inference(resolution,[status(thm)],[f104,f5])).
% 0.17/0.50 fof(f572,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|~p29(sK33_skl(sK3_skl))|~sQ2_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f106,f193])).
% 0.17/0.50 fof(f573,definition,(
% 0.17/0.50 sQ58_spl <=> (r1(sK3_skl,sK4_skl(sK3_skl)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f575,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK4_skl(sK3_skl))|sQ58_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f573])).
% 0.17/0.50 fof(f577,definition,(
% 0.17/0.50 sQ59_spl <=> (r1(sK3_skl,sK3_skl))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f579,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|sQ59_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f577])).
% 0.17/0.50 fof(f580,plain,(
% 0.17/0.50 ~sQ59_spl|~sQ3_spl|~sQ2_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f572,f577,f195,f192])).
% 0.17/0.50 fof(f581,plain,(
% 0.17/0.50 $false|sQ59_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f579,f5])).
% 0.17/0.50 fof(f582,plain,(
% 0.17/0.50 sQ59_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f581])).
% 0.17/0.50 fof(f583,plain,(
% 0.17/0.50 $false|sQ58_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f575,f165])).
% 0.17/0.50 fof(f584,plain,(
% 0.17/0.50 sQ58_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f583])).
% 0.17/0.50 fof(f586,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|~p28(sK33_skl(sK3_skl))|~sQ5_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f108,f206])).
% 0.17/0.50 fof(f588,plain,(
% 0.17/0.50 ~sQ59_spl|~sQ2_spl|~sQ5_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f586,f577,f192,f205])).
% 0.17/0.50 fof(f590,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|~p25(sK33_skl(sK3_skl))|~sQ11_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f114,f236])).
% 0.17/0.50 fof(f592,plain,(
% 0.17/0.50 ~sQ59_spl|~sQ9_spl|~sQ11_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f590,f577,f225,f235])).
% 0.17/0.50 fof(f594,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|~p23(sK33_skl(sK3_skl))|~sQ15_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f118,f256])).
% 0.17/0.50 fof(f596,plain,(
% 0.17/0.50 ~sQ59_spl|~sQ13_spl|~sQ15_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f594,f577,f245,f255])).
% 0.17/0.50 fof(f598,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|~p21(sK33_skl(sK3_skl))|~sQ19_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f122,f276])).
% 0.17/0.50 fof(f600,plain,(
% 0.17/0.50 ~sQ59_spl|~sQ17_spl|~sQ19_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f598,f577,f265,f275])).
% 0.17/0.50 fof(f602,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|~p19(sK33_skl(sK3_skl))|~sQ23_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f126,f296])).
% 0.17/0.50 fof(f604,plain,(
% 0.17/0.50 ~sQ59_spl|~sQ21_spl|~sQ23_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f602,f577,f285,f295])).
% 0.17/0.50 fof(f606,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|~p17(sK33_skl(sK3_skl))|~sQ27_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f130,f316])).
% 0.17/0.50 fof(f608,plain,(
% 0.17/0.50 ~sQ59_spl|~sQ25_spl|~sQ27_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f606,f577,f305,f315])).
% 0.17/0.50 fof(f609,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|~p27(sK33_skl(sK3_skl))|~sQ7_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f216,f110])).
% 0.17/0.50 fof(f610,plain,(
% 0.17/0.50 ~sQ59_spl|~sQ5_spl|~sQ7_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f609,f577,f205,f215])).
% 0.17/0.50 fof(f612,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|~p15(sK33_skl(sK3_skl))|~sQ31_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f134,f336])).
% 0.17/0.50 fof(f614,plain,(
% 0.17/0.50 ~sQ59_spl|~sQ29_spl|~sQ31_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f612,f577,f325,f335])).
% 0.17/0.50 fof(f615,plain,(
% 0.17/0.50 ~r1(sK3_skl,sK3_skl)|~p13(sK33_skl(sK3_skl))|~sQ35_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f138,f356])).
% 0.17/0.50 fof(f616,plain,(
% 0.17/0.51 ~sQ59_spl|~sQ33_spl|~sQ35_spl),
% 0.17/0.51 inference(split_clause,[status(thm)],[f615,f577,f345,f355])).
% 0.17/0.51 fof(f617,plain,(
% 0.17/0.51 ~r1(sK3_skl,sK3_skl)|~p11(sK33_skl(sK3_skl))|~sQ39_spl),
% 0.17/0.51 inference(resolution,[status(thm)],[f142,f376])).
% 0.17/0.51 fof(f618,plain,(
% 0.17/0.51 ~sQ59_spl|~sQ37_spl|~sQ39_spl),
% 0.17/0.51 inference(split_clause,[status(thm)],[f617,f577,f365,f375])).
% 0.17/0.51 fof(f621,plain,(
% 0.17/0.51 ~r1(sK3_skl,sK3_skl)|~p9(sK33_skl(sK3_skl))|~sQ43_spl),
% 0.17/0.51 inference(resolution,[status(thm)],[f146,f396])).
% 0.17/0.51 fof(f622,plain,(
% 0.17/0.51 ~sQ59_spl|~sQ41_spl|~sQ43_spl),
% 0.17/0.51 inference(split_clause,[status(thm)],[f621,f577,f385,f395])).
% 0.17/0.51 fof(f623,plain,(
% 0.17/0.51 ~r1(sK3_skl,sK3_skl)|~p7(sK33_skl(sK3_skl))|~sQ47_spl),
% 0.17/0.51 inference(resolution,[status(thm)],[f150,f416])).
% 0.17/0.51 fof(f624,plain,(
% 0.17/0.51 ~sQ59_spl|~sQ45_spl|~sQ47_spl),
% 0.17/0.51 inference(split_clause,[status(thm)],[f623,f577,f405,f415])).
% 0.17/0.51 fof(f625,plain,(
% 0.17/0.51 ~r1(sK3_skl,sK3_skl)|~p5(sK33_skl(sK3_skl))|~sQ51_spl),
% 0.17/0.51 inference(resolution,[status(thm)],[f154,f436])).
% 0.17/0.51 fof(f626,plain,(
% 0.17/0.51 ~sQ59_spl|~sQ49_spl|~sQ51_spl),
% 0.17/0.51 inference(split_clause,[status(thm)],[f625,f577,f425,f435])).
% 0.17/0.51 fof(f627,plain,(
% 0.17/0.51 ~r1(sK3_skl,sK3_skl)|~p3(sK33_skl(sK3_skl))|~sQ55_spl),
% 0.17/0.51 inference(resolution,[status(thm)],[f158,f456])).
% 0.17/0.51 fof(f628,plain,(
% 0.17/0.51 ~sQ59_spl|~sQ53_spl|~sQ55_spl),
% 0.17/0.51 inference(split_clause,[status(thm)],[f627,f577,f445,f455])).
% 0.17/0.51 fof(f629,plain,(
% 0.17/0.51 ~r1(sK3_skl,sK3_skl)|~p1(sK33_skl(sK3_skl))|~sQ55_spl),
% 0.17/0.51 inference(resolution,[status(thm)],[f160,f456])).
% 0.17/0.51 fof(f630,plain,(
% 0.17/0.51 ~sQ59_spl|~sQ57_spl|~sQ55_spl),
% 0.17/0.51 inference(split_clause,[status(thm)],[f629,f577,f465,f455])).
% 0.17/0.51 fof(f1245,plain,(
% 0.17/0.51 p2(sK33_skl(sK3_skl))|~p1(sK33_skl(sK3_skl))),
% 0.17/0.51 inference(resolution,[status(thm)],[f570,f566])).
% 0.17/0.51 fof(f1246,plain,(
% 0.17/0.51 ~p2(sK33_skl(sK3_skl))|p1(sK33_skl(sK3_skl))),
% 0.17/0.51 inference(resolution,[status(thm)],[f570,f564])).
% 0.17/0.51 fof(f1309,plain,(
% 0.17/0.51 sQ55_spl|~sQ57_spl),
% 0.17/0.51 inference(split_clause,[status(thm)],[f1245,f455,f465])).
% 0.17/0.51 fof(f1310,plain,(
% 0.17/0.51 ~sQ55_spl|sQ57_spl),
% 0.17/0.51 inference(split_clause,[status(thm)],[f1246,f455,f465])).
% 0.17/0.51 fof(f1426,plain,(
% 0.17/0.51 $false),
% 0.17/0.51 inference(sat_refutation,[status(thm)],[f198,f208,f218,f228,f238,f248,f258,f268,f278,f288,f298,f308,f318,f328,f338,f348,f358,f368,f378,f388,f398,f408,f418,f428,f438,f448,f458,f468,f580,f582,f584,f588,f592,f596,f600,f604,f608,f610,f614,f616,f618,f622,f624,f626,f628,f630,f1309,f1310])).
% 0.17/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.54 % Elapsed time: 0.105724 seconds
% 0.17/0.54 % CPU time: 0.356507 seconds
% 0.17/0.54 % Total memory used: 15.792 MB
% 0.17/0.54 % Net memory used: 15.663 MB
%------------------------------------------------------------------------------