%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL650+1.005 : 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 : n013.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:38 PM UTC 2026
% Result : Theorem 225.65s 29.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL650+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.25/0.50 % Computer : n013.cluster.edu
% 0.25/0.50 % Model : x86_64 x86_64
% 0.25/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.25/0.50 % Memory : 8046.5625MB
% 0.25/0.50 % OS : Linux 6.8.0-71-generic
% 0.25/0.50 % CPULimit : 300
% 0.25/0.50 % WCLimit : 300
% 0.25/0.50 % DateTime : Mon Sep 21 00:45:06 UTC 2026
% 0.25/0.51 % CPUTime :
% 0.28/0.54 % Drodi V4.1.1
% 225.65/29.15 % Refutation found
% 225.65/29.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 225.65/29.15 % SZS output start CNFRefutation for theBenchmark
% 225.65/29.15 fof(f1,conjecture,(
% 225.65/29.15 ~ (? [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)| ( ~ p32(X)& ~ p30(X)& ~ p28(X)& ~ p26(X)& ~ p24(X)& ~ p22(X)& ~ p20(X)& ~ p18(X)& ~ p16(X)& ~ p14(X)& ~ p12(X)& ~ p10(X)& ~ p8(X)& ~ p6(X)& ~ p4(X)& ~ p2(X) ) ) )) )) )) )) )) )) )) )) )) )) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p17(Y) ))| ~ (! [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)| ~ ( ( ~ p15(X)& ~ p1(X) )| ( p1(X)& p15(X) ) ) ) )) )) )) )) )) )) )) )) )) )) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p16(X) ))| ~ (! [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)| ~ ( ( ~ p14(X)& ~ p15(X) )| ( p15(X)& p14(X) ) ) ) )) )) )) )) )) )) )) )) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p15(Y) ))| ~ (! [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)| ~ ( ( ~ p13(X)& ~ p14(X) )| ( p14(X)& p13(X) ) ) ) )) )) )) )) )) )) )) )) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p14(X) ))| ~ (! [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)| ~ ( ( ~ p12(X)& ~ p13(X) )| ( p13(X)& p12(X) ) ) ) )) )) )) )) )) )) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p13(Y) ))| ~ (! [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)| ~ ( ( ~ p11(X)& ~ p12(X) )| ( p12(X)& p11(X) ) ) ) )) )) )) )) )) )) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p12(X) ))| ~ (! [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)| ~ ( ( ~ p10(X)& ~ p11(X) )| ( p11(X)& p10(X) ) ) ) )) )) )) )) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p11(Y) ))| ~ (! [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)| ~ ( ( ~ p9(X)& ~ p10(X) )| ( p10(X)& p9(X) ) ) ) )) )) )) )) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p10(X) ))| ~ (! [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)| ~ ( ( ~ p8(X)& ~ p9(X) )| ( p9(X)& p8(X) ) ) ) )) )) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p9(Y) ))| ~ (! [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)| ~ ( ( ~ p7(X)& ~ p8(X) )| ( p8(X)& p7(X) ) ) ) )) )) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p8(X) ))| ~ (! [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)| ~ ( ( ~ p6(X)& ~ p7(X) )| ( p7(X)& p6(X) ) ) ) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p7(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p5(X)& ~ p6(X) )| ( p6(X)& p5(X) ) ) ) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p6(X) ))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p4(X)& ~ p5(X) )| ( p5(X)& p4(X) ) ) ) )) )) )))| (! [Y] :( ~ r1(X,Y)| p5(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p3(X)& ~ p4(X) )| ( p4(X)& p3(X) ) ) ) )) )))| (! [X] :( ~ r1(Y,X)| p4(X) ))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p2(X)& ~ p3(X) )| ( p3(X)& p2(X) ) ) ) )))| (! [Y] :( ~ r1(X,Y)| p3(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ~ (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p1(X)& ~ p2(X) )| ( p2(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)| ( p16(X)& p15(X)& p14(X)& p13(X)& p12(X)& p11(X)& p10(X)& p9(X)& p8(X)& p7(X)& p6(X)& p5(X)& p4(X)& p3(X)& p2(X)& p1(X) ) ) )) )) )) )) )) )) )) )) )) )) )) )) )) )) )) )) )),
% 225.65/29.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 225.65/29.15 fof(f2,negated_conjecture,(
% 225.65/29.15 ~(~ (? [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)| ( ~ p32(X)& ~ p30(X)& ~ p28(X)& ~ p26(X)& ~ p24(X)& ~ p22(X)& ~ p20(X)& ~ p18(X)& ~ p16(X)& ~ p14(X)& ~ p12(X)& ~ p10(X)& ~ p8(X)& ~ p6(X)& ~ p4(X)& ~ p2(X) ) ) )) )) )) )) )) )) )) )) )) )) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p17(Y) ))| ~ (! [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)| ~ ( ( ~ p15(X)& ~ p1(X) )| ( p1(X)& p15(X) ) ) ) )) )) )) )) )) )) )) )) )) )) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p16(X) ))| ~ (! [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)| ~ ( ( ~ p14(X)& ~ p15(X) )| ( p15(X)& p14(X) ) ) ) )) )) )) )) )) )) )) )) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p15(Y) ))| ~ (! [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)| ~ ( ( ~ p13(X)& ~ p14(X) )| ( p14(X)& p13(X) ) ) ) )) )) )) )) )) )) )) )) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p14(X) ))| ~ (! [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)| ~ ( ( ~ p12(X)& ~ p13(X) )| ( p13(X)& p12(X) ) ) ) )) )) )) )) )) )) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p13(Y) ))| ~ (! [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)| ~ ( ( ~ p11(X)& ~ p12(X) )| ( p12(X)& p11(X) ) ) ) )) )) )) )) )) )) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p12(X) ))| ~ (! [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)| ~ ( ( ~ p10(X)& ~ p11(X) )| ( p11(X)& p10(X) ) ) ) )) )) )) )) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p11(Y) ))| ~ (! [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)| ~ ( ( ~ p9(X)& ~ p10(X) )| ( p10(X)& p9(X) ) ) ) )) )) )) )) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p10(X) ))| ~ (! [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)| ~ ( ( ~ p8(X)& ~ p9(X) )| ( p9(X)& p8(X) ) ) ) )) )) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p9(Y) ))| ~ (! [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)| ~ ( ( ~ p7(X)& ~ p8(X) )| ( p8(X)& p7(X) ) ) ) )) )) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p8(X) ))| ~ (! [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)| ~ ( ( ~ p6(X)& ~ p7(X) )| ( p7(X)& p6(X) ) ) ) )) )) )) )) )))| (! [Y] :( ~ r1(X,Y)| p7(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p5(X)& ~ p6(X) )| ( p6(X)& p5(X) ) ) ) )) )) )) )))| (! [X] :( ~ r1(Y,X)| p6(X) ))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p4(X)& ~ p5(X) )| ( p5(X)& p4(X) ) ) ) )) )) )))| (! [Y] :( ~ r1(X,Y)| p5(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p3(X)& ~ p4(X) )| ( p4(X)& p3(X) ) ) ) )) )))| (! [X] :( ~ r1(Y,X)| p4(X) ))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p2(X)& ~ p3(X) )| ( p3(X)& p2(X) ) ) ) )))| (! [Y] :( ~ r1(X,Y)| p3(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ~ (! [X] :( ~ r1(Y,X)| ~ ( ( ~ p1(X)& ~ p2(X) )| ( p2(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)| ( p16(X)& p15(X)& p14(X)& p13(X)& p12(X)& p11(X)& p10(X)& p9(X)& p8(X)& p7(X)& p6(X)& p5(X)& p4(X)& p3(X)& p2(X)& p1(X) ) ) )) )) )) )) )) )) )) )) )) )) )) )) )) )) )) )) ))),
% 225.65/29.15 inference(negated_conjecture,[status(cth)],[f1])).
% 225.65/29.15 fof(f3,plain,(
% 225.65/29.15 ?[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)&(((((((((((((((p32(X)|p30(X))|p28(X))|p26(X))|p24(X))|p22(X))|p20(X))|p18(X))|p16(X))|p14(X))|p12(X))|p10(X))|p8(X))|p6(X))|p4(X))|p2(X))))))))))))))))))))))))))))))))))&(?[Y]: (r1(X,Y)&~p17(Y))))&(![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)|((p15(X)|p1(X))&(~p1(X)|~p15(X)))))))))))))))))))))))))))))))))&(?[X]: (r1(Y,X)&~p16(X))))&(![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)|((p14(X)|p15(X))&(~p15(X)|~p14(X)))))))))))))))))))))))))))))))&(?[Y]: (r1(X,Y)&~p15(Y))))&(![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)|((p13(X)|p14(X))&(~p14(X)|~p13(X)))))))))))))))))))))))))))))&(?[X]: (r1(Y,X)&~p14(X))))&(![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)|((p12(X)|p13(X))&(~p13(X)|~p12(X)))))))))))))))))))))))))))&(?[Y]: (r1(X,Y)&~p13(Y))))&(![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)|((p11(X)|p12(X))&(~p12(X)|~p11(X)))))))))))))))))))))))))&(?[X]: (r1(Y,X)&~p12(X))))&(![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)|((p10(X)|p11(X))&(~p11(X)|~p10(X)))))))))))))))))))))))&(?[Y]: (r1(X,Y)&~p11(Y))))&(![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)|((p9(X)|p10(X))&(~p10(X)|~p9(X)))))))))))))))))))))&(?[X]: (r1(Y,X)&~p10(X))))&(![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)|((p8(X)|p9(X))&(~p9(X)|~p8(X)))))))))))))))))))&(?[Y]: (r1(X,Y)&~p9(Y))))&(![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)|((p7(X)|p8(X))&(~p8(X)|~p7(X)))))))))))))))))&(?[X]: (r1(Y,X)&~p8(X))))&(![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)|((p6(X)|p7(X))&(~p7(X)|~p6(X)))))))))))))))&(?[Y]: (r1(X,Y)&~p7(Y))))&(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p5(X)|p6(X))&(~p6(X)|~p5(X)))))))))))))&(?[X]: (r1(Y,X)&~p6(X))))&(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p4(X)|p5(X))&(~p5(X)|~p4(X)))))))))))&(?[Y]: (r1(X,Y)&~p5(Y))))&(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p3(X)|p4(X))&(~p4(X)|~p3(X)))))))))&(?[X]: (r1(Y,X)&~p4(X))))&(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p2(X)|p3(X))&(~p3(X)|~p2(X)))))))&(?[Y]: (r1(X,Y)&~p3(Y))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p1(X)|p2(X))&(~p2(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)&(((((((((((((((~p16(X)|~p15(X))|~p14(X))|~p13(X))|~p12(X))|~p11(X))|~p10(X))|~p9(X))|~p8(X))|~p7(X))|~p6(X))|~p5(X))|~p4(X))|~p3(X))|~p2(X))|~p1(X)))))))))))))))))))))))))))))))))))),
% 225.65/29.15 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 225.65/29.15 fof(f4,plain,(
% 225.65/29.15 ((((r1(sK0_skl,sK1_skl)&(r1(sK1_skl,sK2_skl)&(r1(sK2_skl,sK3_skl)&(r1(sK3_skl,sK4_skl)&(r1(sK4_skl,sK5_skl)&(r1(sK5_skl,sK6_skl)&(r1(sK6_skl,sK7_skl)&(r1(sK7_skl,sK8_skl)&(r1(sK8_skl,sK9_skl)&(r1(sK9_skl,sK10_skl)&(r1(sK10_skl,sK11_skl)&(r1(sK11_skl,sK12_skl)&(r1(sK12_skl,sK13_skl)&(r1(sK13_skl,sK14_skl)&(r1(sK14_skl,sK15_skl)&(r1(sK15_skl,sK16_skl)&(((((((((((((((p32(sK16_skl)|p30(sK16_skl))|p28(sK16_skl))|p26(sK16_skl))|p24(sK16_skl))|p22(sK16_skl))|p20(sK16_skl))|p18(sK16_skl))|p16(sK16_skl))|p14(sK16_skl))|p12(sK16_skl))|p10(sK16_skl))|p8(sK16_skl))|p6(sK16_skl))|p4(sK16_skl))|p2(sK16_skl))))))))))))))))))&(r1(sK0_skl,sK17_skl)&~p17(sK17_skl)))&(![Y]: (~r1(sK0_skl,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)|((p15(X)|p1(X))&(~p1(X)|~p15(X)))))))))))))))))))))))))))))))))&(r1(Y,sK18_skl(Y))&~p16(sK18_skl(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)|((p14(X)|p15(X))&(~p15(X)|~p14(X)))))))))))))))))))))))))))))))&(r1(X,sK19_skl(X,Y))&~p15(sK19_skl(X,Y))))&(![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)|((p13(X)|p14(X))&(~p14(X)|~p13(X)))))))))))))))))))))))))))))&(r1(Y,sK20_skl(Y,X,Y))&~p14(sK20_skl(Y,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)|((p12(X)|p13(X))&(~p13(X)|~p12(X)))))))))))))))))))))))))))&(r1(X,sK21_skl(X,Y,X,Y))&~p13(sK21_skl(X,Y,X,Y))))&(![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)|((p11(X)|p12(X))&(~p12(X)|~p11(X)))))))))))))))))))))))))&(r1(Y,sK22_skl(Y,X,Y,X,Y))&~p12(sK22_skl(Y,X,Y,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)|((p10(X)|p11(X))&(~p11(X)|~p10(X)))))))))))))))))))))))&(r1(X,sK23_skl(X,Y,X,Y,X,Y))&~p11(sK23_skl(X,Y,X,Y,X,Y))))&(![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)|((p9(X)|p10(X))&(~p10(X)|~p9(X)))))))))))))))))))))&(r1(Y,sK24_skl(Y,X,Y,X,Y,X,Y))&~p10(sK24_skl(Y,X,Y,X,Y,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)|((p8(X)|p9(X))&(~p9(X)|~p8(X)))))))))))))))))))&(r1(X,sK25_skl(X,Y,X,Y,X,Y,X,Y))&~p9(sK25_skl(X,Y,X,Y,X,Y,X,Y))))&(![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)|((p7(X)|p8(X))&(~p8(X)|~p7(X)))))))))))))))))&(r1(Y,sK26_skl(Y,X,Y,X,Y,X,Y,X,Y))&~p8(sK26_skl(Y,X,Y,X,Y,X,Y,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)|((p6(X)|p7(X))&(~p7(X)|~p6(X)))))))))))))))&(r1(X,sK27_skl(X,Y,X,Y,X,Y,X,Y,X,Y))&~p7(sK27_skl(X,Y,X,Y,X,Y,X,Y,X,Y))))&(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p5(X)|p6(X))&(~p6(X)|~p5(X)))))))))))))&(r1(Y,sK28_skl(Y,X,Y,X,Y,X,Y,X,Y,X,Y))&~p6(sK28_skl(Y,X,Y,X,Y,X,Y,X,Y,X,Y))))&(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p4(X)|p5(X))&(~p5(X)|~p4(X)))))))))))&(r1(X,sK29_skl(X,Y,X,Y,X,Y,X,Y,X,Y,X,Y))&~p5(sK29_skl(X,Y,X,Y,X,Y,X,Y,X,Y,X,Y))))&(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p3(X)|p4(X))&(~p4(X)|~p3(X)))))))))&(r1(Y,sK30_skl(Y,X,Y,X,Y,X,Y,X,Y,X,Y,X,Y))&~p4(sK30_skl(Y,X,Y,X,Y,X,Y,X,Y,X,Y,X,Y))))&(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p2(X)|p3(X))&(~p3(X)|~p2(X)))))))&(r1(X,sK31_skl(X,Y,X,Y,X,Y,X,Y,X,Y,X,Y,X,Y))&~p3(sK31_skl(X,Y,X,Y,X,Y,X,Y,X,Y,X,Y,X,Y))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((p1(X)|p2(X))&(~p2(X)|~p1(X))))))))))))))))))))))))))))))))))))))))))))))))))&(r1(sK0_skl,sK32_skl)&(r1(sK32_skl,sK33_skl)&(r1(sK33_skl,sK34_skl)&(r1(sK34_skl,sK35_skl)&(r1(sK35_skl,sK36_skl)&(r1(sK36_skl,sK37_skl)&(r1(sK37_skl,sK38_skl)&(r1(sK38_skl,sK39_skl)&(r1(sK39_skl,sK40_skl)&(r1(sK40_skl,sK41_skl)&(r1(sK41_skl,sK42_skl)&(r1(sK42_skl,sK43_skl)&(r1(sK43_skl,sK44_skl)&(r1(sK44_skl,sK45_skl)&(r1(sK45_skl,sK46_skl)&(r1(sK46_skl,sK47_skl)&(((((((((((((((~p16(sK47_skl)|~p15(sK47_skl))|~p14(sK47_skl))|~p13(sK47_skl))|~p12(sK47_skl))|~p11(sK47_skl))|~p10(sK47_skl))|~p9(sK47_skl))|~p8(sK47_skl))|~p7(sK47_skl))|~p6(sK47_skl))|~p5(sK47_skl))|~p4(sK47_skl))|~p3(sK47_skl))|~p2(sK47_skl))|~p1(sK47_skl)))))))))))))))))))),
% 225.65/29.15 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,sK34_skl,sK35_skl,sK36_skl,sK37_skl,sK38_skl,sK39_skl,sK40_skl,sK41_skl,sK42_skl,sK43_skl,sK44_skl,sK45_skl,sK46_skl,sK47_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl),skolemize(X,sK2_skl),skolemize(Y,sK3_skl),skolemize(X,sK4_skl),skolemize(Y,sK5_skl),skolemize(X,sK6_skl),skolemize(Y,sK7_skl),skolemize(X,sK8_skl),skolemize(Y,sK9_skl),skolemize(X,sK10_skl),skolemize(Y,sK11_skl),skolemize(X,sK12_skl),skolemize(Y,sK13_skl),skolemize(X,sK14_skl),skolemize(Y,sK15_skl),skolemize(X,sK16_skl),skolemize(Y,sK17_skl),skolemize(X,sK18_skl(Y)),skolemize(Y,sK19_skl(X,Y)),skolemize(X,sK20_skl(Y,X,Y)),skolemize(Y,sK21_skl(X,Y,X,Y)),skolemize(X,sK22_skl(Y,X,Y,X,Y)),skolemize(Y,sK23_skl(X,Y,X,Y,X,Y)),skolemize(X,sK24_skl(Y,X,Y,X,Y,X,Y)),skolemize(Y,sK25_skl(X,Y,X,Y,X,Y,X,Y)),skolemize(X,sK26_skl(Y,X,Y,X,Y,X,Y,X,Y)),skolemize(Y,sK27_skl(X,Y,X,Y,X,Y,X,Y,X,Y)),skolemize(X,sK28_skl(Y,X,Y,X,Y,X,Y,X,Y,X,Y)),skolemize(Y,sK29_skl(X,Y,X,Y,X,Y,X,Y,X,Y,X,Y)),skolemize(X,sK30_skl(Y,X,Y,X,Y,X,Y,X,Y,X,Y,X,Y)),skolemize(Y,sK31_skl(X,Y,X,Y,X,Y,X,Y,X,Y,X,Y,X,Y)),skolemize(Y,sK32_skl),skolemize(X,sK33_skl),skolemize(Y,sK34_skl),skolemize(X,sK35_skl),skolemize(Y,sK36_skl),skolemize(X,sK37_skl),skolemize(Y,sK38_skl),skolemize(X,sK39_skl),skolemize(Y,sK40_skl),skolemize(X,sK41_skl),skolemize(Y,sK42_skl),skolemize(X,sK43_skl),skolemize(Y,sK44_skl),skolemize(X,sK45_skl),skolemize(Y,sK46_skl),skolemize(X,sK47_skl)],[f3])).
% 225.65/29.15 fof(f24,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p15(X15)|p1(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f25,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p1(X15)|~p15(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f28,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p14(X15)|p15(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f29,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p15(X15)|~p14(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f32,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p13(X15)|p14(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f33,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p14(X15)|~p13(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f36,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p12(X15)|p13(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f37,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p13(X15)|~p12(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f40,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p11(X15)|p12(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f41,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p12(X15)|~p11(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f44,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p10(X15)|p11(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f45,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p11(X15)|~p10(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f48,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p9(X15)|p10(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f49,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p10(X15)|~p9(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f52,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p8(X15)|p9(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f53,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p9(X15)|~p8(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f56,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p7(X15)|p8(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f57,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p8(X15)|~p7(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f60,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p6(X15)|p7(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f61,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p7(X15)|~p6(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f64,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p5(X15)|p6(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f65,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p6(X15)|~p5(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f68,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p4(X15)|p5(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f69,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p5(X15)|~p4(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f72,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p3(X15)|p4(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f73,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p4(X15)|~p3(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f76,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p2(X15)|p3(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f77,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p3(X15)|~p2(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f80,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|p1(X15)|p2(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f81,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~p2(X15)|~p1(X15))),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f82,plain,(
% 225.65/29.15 r1(sK0_skl,sK32_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f83,plain,(
% 225.65/29.15 r1(sK32_skl,sK33_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f84,plain,(
% 225.65/29.15 r1(sK33_skl,sK34_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f85,plain,(
% 225.65/29.15 r1(sK34_skl,sK35_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f86,plain,(
% 225.65/29.15 r1(sK35_skl,sK36_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f87,plain,(
% 225.65/29.15 r1(sK36_skl,sK37_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f88,plain,(
% 225.65/29.15 r1(sK37_skl,sK38_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f89,plain,(
% 225.65/29.15 r1(sK38_skl,sK39_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f90,plain,(
% 225.65/29.15 r1(sK39_skl,sK40_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f91,plain,(
% 225.65/29.15 r1(sK40_skl,sK41_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f92,plain,(
% 225.65/29.15 r1(sK41_skl,sK42_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f93,plain,(
% 225.65/29.15 r1(sK42_skl,sK43_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f94,plain,(
% 225.65/29.15 r1(sK43_skl,sK44_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f95,plain,(
% 225.65/29.15 r1(sK44_skl,sK45_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f96,plain,(
% 225.65/29.15 r1(sK45_skl,sK46_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f97,plain,(
% 225.65/29.15 r1(sK46_skl,sK47_skl)),
% 225.65/29.15 inference(cnf_transformation,[status(thm)],[f4])).
% 225.65/29.15 fof(f151,definition,(
% 225.65/29.15 sQ17_spl <=> (p15(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f152,plain,(
% 225.65/29.15 p15(sK47_skl)|~sQ17_spl),
% 225.65/29.15 inference(component_clause,[status(thm)],[f151])).
% 225.65/29.15 fof(f154,definition,(
% 225.65/29.15 sQ18_spl <=> (p14(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f157,definition,(
% 225.65/29.15 sQ19_spl <=> (p13(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f158,plain,(
% 225.65/29.15 p13(sK47_skl)|~sQ19_spl),
% 225.65/29.15 inference(component_clause,[status(thm)],[f157])).
% 225.65/29.15 fof(f160,definition,(
% 225.65/29.15 sQ20_spl <=> (p12(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f163,definition,(
% 225.65/29.15 sQ21_spl <=> (p11(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f164,plain,(
% 225.65/29.15 p11(sK47_skl)|~sQ21_spl),
% 225.65/29.15 inference(component_clause,[status(thm)],[f163])).
% 225.65/29.15 fof(f166,definition,(
% 225.65/29.15 sQ22_spl <=> (p10(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f169,definition,(
% 225.65/29.15 sQ23_spl <=> (p9(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f170,plain,(
% 225.65/29.15 p9(sK47_skl)|~sQ23_spl),
% 225.65/29.15 inference(component_clause,[status(thm)],[f169])).
% 225.65/29.15 fof(f172,definition,(
% 225.65/29.15 sQ24_spl <=> (p8(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f175,definition,(
% 225.65/29.15 sQ25_spl <=> (p7(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f176,plain,(
% 225.65/29.15 p7(sK47_skl)|~sQ25_spl),
% 225.65/29.15 inference(component_clause,[status(thm)],[f175])).
% 225.65/29.15 fof(f178,definition,(
% 225.65/29.15 sQ26_spl <=> (p6(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f181,definition,(
% 225.65/29.15 sQ27_spl <=> (p5(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f182,plain,(
% 225.65/29.15 p5(sK47_skl)|~sQ27_spl),
% 225.65/29.15 inference(component_clause,[status(thm)],[f181])).
% 225.65/29.15 fof(f184,definition,(
% 225.65/29.15 sQ28_spl <=> (p4(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f185,plain,(
% 225.65/29.15 p4(sK47_skl)|~sQ28_spl),
% 225.65/29.15 inference(component_clause,[status(thm)],[f184])).
% 225.65/29.15 fof(f187,definition,(
% 225.65/29.15 sQ29_spl <=> (p3(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f188,plain,(
% 225.65/29.15 p3(sK47_skl)|~sQ29_spl),
% 225.65/29.15 inference(component_clause,[status(thm)],[f187])).
% 225.65/29.15 fof(f190,definition,(
% 225.65/29.15 sQ30_spl <=> (p2(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f193,definition,(
% 225.65/29.15 sQ31_spl <=> (p1(sK47_skl))),
% 225.65/29.15 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 225.65/29.15 fof(f194,plain,(
% 225.65/29.15 p1(sK47_skl)|~sQ31_spl),
% 225.65/29.15 inference(component_clause,[status(thm)],[f193])).
% 225.65/29.15 fof(f358,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p1(X14)|p2(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f80])).
% 225.65/29.15 fof(f359,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p2(X14)|p3(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f76])).
% 225.65/29.15 fof(f360,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p3(X14)|p4(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f72])).
% 225.65/29.15 fof(f361,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p4(X14)|p5(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f68])).
% 225.65/29.15 fof(f362,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p5(X14)|p6(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f64])).
% 225.65/29.15 fof(f363,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p6(X14)|p7(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f60])).
% 225.65/29.15 fof(f364,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p7(X14)|p8(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f56])).
% 225.65/29.15 fof(f365,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p8(X14)|p9(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f52])).
% 225.65/29.15 fof(f366,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p9(X14)|p10(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f48])).
% 225.65/29.15 fof(f367,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p10(X14)|p11(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f44])).
% 225.65/29.15 fof(f368,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p11(X14)|p12(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f40])).
% 225.65/29.15 fof(f369,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p12(X14)|p13(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f36])).
% 225.65/29.15 fof(f370,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p13(X14)|p14(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f32])).
% 225.65/29.15 fof(f371,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p14(X14)|p15(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f28])).
% 225.65/29.15 fof(f372,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK32_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|p15(X14)|p1(X14))),
% 225.65/29.15 inference(resolution,[status(thm)],[f82,f24])).
% 225.65/29.15 fof(f393,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p1(X13)|p2(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f358,f83])).
% 225.65/29.15 fof(f394,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p2(X13)|p3(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f359,f83])).
% 225.65/29.15 fof(f395,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p3(X13)|p4(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f360,f83])).
% 225.65/29.15 fof(f396,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p4(X13)|p5(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f361,f83])).
% 225.65/29.15 fof(f417,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p5(X13)|p6(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f362,f83])).
% 225.65/29.15 fof(f418,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p6(X13)|p7(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f363,f83])).
% 225.65/29.15 fof(f419,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p7(X13)|p8(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f364,f83])).
% 225.65/29.15 fof(f420,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p8(X13)|p9(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f365,f83])).
% 225.65/29.15 fof(f421,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p9(X13)|p10(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f366,f83])).
% 225.65/29.15 fof(f422,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p10(X13)|p11(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f367,f83])).
% 225.65/29.15 fof(f423,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p11(X13)|p12(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f368,f83])).
% 225.65/29.15 fof(f424,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p12(X13)|p13(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f369,f83])).
% 225.65/29.15 fof(f454,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p13(X13)|p14(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f370,f83])).
% 225.65/29.15 fof(f455,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p14(X13)|p15(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f371,f83])).
% 225.65/29.15 fof(f456,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK33_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|p15(X13)|p1(X13))),
% 225.65/29.15 inference(resolution,[status(thm)],[f372,f83])).
% 225.65/29.15 fof(f457,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p1(X12)|p2(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f393,f84])).
% 225.65/29.15 fof(f458,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p2(X12)|p3(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f394,f84])).
% 225.65/29.15 fof(f459,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p3(X12)|p4(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f395,f84])).
% 225.65/29.15 fof(f460,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p4(X12)|p5(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f396,f84])).
% 225.65/29.15 fof(f461,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p5(X12)|p6(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f417,f84])).
% 225.65/29.15 fof(f462,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p6(X12)|p7(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f418,f84])).
% 225.65/29.15 fof(f463,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p7(X12)|p8(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f419,f84])).
% 225.65/29.15 fof(f464,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p8(X12)|p9(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f420,f84])).
% 225.65/29.15 fof(f465,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p9(X12)|p10(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f421,f84])).
% 225.65/29.15 fof(f491,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p10(X12)|p11(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f422,f84])).
% 225.65/29.15 fof(f492,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p11(X12)|p12(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f423,f84])).
% 225.65/29.15 fof(f493,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p12(X12)|p13(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f424,f84])).
% 225.65/29.15 fof(f494,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p13(X12)|p14(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f454,f84])).
% 225.65/29.15 fof(f515,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p14(X12)|p15(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f455,f84])).
% 225.65/29.15 fof(f516,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK34_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|p15(X12)|p1(X12))),
% 225.65/29.15 inference(resolution,[status(thm)],[f456,f84])).
% 225.65/29.15 fof(f518,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p1(X11)|p2(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f457,f85])).
% 225.65/29.15 fof(f519,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p2(X11)|p3(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f458,f85])).
% 225.65/29.15 fof(f520,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p3(X11)|p4(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f459,f85])).
% 225.65/29.15 fof(f521,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p4(X11)|p5(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f460,f85])).
% 225.65/29.15 fof(f522,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p5(X11)|p6(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f461,f85])).
% 225.65/29.15 fof(f552,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p6(X11)|p7(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f462,f85])).
% 225.65/29.15 fof(f553,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p7(X11)|p8(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f463,f85])).
% 225.65/29.15 fof(f554,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p8(X11)|p9(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f464,f85])).
% 225.65/29.15 fof(f555,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p9(X11)|p10(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f465,f85])).
% 225.65/29.15 fof(f556,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p10(X11)|p11(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f491,f85])).
% 225.65/29.15 fof(f557,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p11(X11)|p12(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f492,f85])).
% 225.65/29.15 fof(f558,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p12(X11)|p13(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f493,f85])).
% 225.65/29.15 fof(f559,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p13(X11)|p14(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f494,f85])).
% 225.65/29.15 fof(f560,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p14(X11)|p15(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f515,f85])).
% 225.65/29.15 fof(f561,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK35_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|p15(X11)|p1(X11))),
% 225.65/29.15 inference(resolution,[status(thm)],[f516,f85])).
% 225.65/29.15 fof(f563,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p1(X10)|p2(X10))),
% 225.65/29.15 inference(resolution,[status(thm)],[f518,f86])).
% 225.65/29.15 fof(f636,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p1(X9)|p2(X9))),
% 225.65/29.15 inference(resolution,[status(thm)],[f563,f87])).
% 225.65/29.15 fof(f637,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p1(X8)|p2(X8))),
% 225.65/29.15 inference(resolution,[status(thm)],[f636,f88])).
% 225.65/29.15 fof(f638,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p1(X7)|p2(X7))),
% 225.65/29.15 inference(resolution,[status(thm)],[f637,f89])).
% 225.65/29.15 fof(f639,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p1(X6)|p2(X6))),
% 225.65/29.15 inference(resolution,[status(thm)],[f638,f90])).
% 225.65/29.15 fof(f640,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p1(X5)|p2(X5))),
% 225.65/29.15 inference(resolution,[status(thm)],[f639,f91])).
% 225.65/29.15 fof(f641,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p1(X4)|p2(X4))),
% 225.65/29.15 inference(resolution,[status(thm)],[f640,f92])).
% 225.65/29.15 fof(f642,plain,(
% 225.65/29.15 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p1(X3)|p2(X3))),
% 225.65/29.15 inference(resolution,[status(thm)],[f641,f93])).
% 225.65/29.15 fof(f643,plain,(
% 225.65/29.15 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p1(X2)|p2(X2))),
% 225.65/29.15 inference(resolution,[status(thm)],[f642,f94])).
% 225.65/29.15 fof(f644,plain,(
% 225.65/29.15 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p1(X1)|p2(X1))),
% 225.65/29.15 inference(resolution,[status(thm)],[f643,f95])).
% 225.65/29.15 fof(f645,plain,(
% 225.65/29.15 ![X0]: (~r1(sK46_skl,X0)|p1(X0)|p2(X0))),
% 225.65/29.15 inference(resolution,[status(thm)],[f644,f96])).
% 225.65/29.15 fof(f646,plain,(
% 225.65/29.15 p1(sK47_skl)|p2(sK47_skl)),
% 225.65/29.15 inference(resolution,[status(thm)],[f645,f97])).
% 225.65/29.15 fof(f647,plain,(
% 225.65/29.15 sQ31_spl|sQ30_spl),
% 225.65/29.15 inference(split_clause,[status(thm)],[f646,f193,f190])).
% 225.65/29.15 fof(f648,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p2(X10)|p3(X10))),
% 225.65/29.15 inference(resolution,[status(thm)],[f519,f86])).
% 225.65/29.15 fof(f649,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p2(X9)|p3(X9))),
% 225.65/29.15 inference(resolution,[status(thm)],[f648,f87])).
% 225.65/29.15 fof(f650,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p2(X8)|p3(X8))),
% 225.65/29.15 inference(resolution,[status(thm)],[f649,f88])).
% 225.65/29.15 fof(f651,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p2(X7)|p3(X7))),
% 225.65/29.15 inference(resolution,[status(thm)],[f650,f89])).
% 225.65/29.15 fof(f652,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p2(X6)|p3(X6))),
% 225.65/29.15 inference(resolution,[status(thm)],[f651,f90])).
% 225.65/29.15 fof(f653,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p2(X5)|p3(X5))),
% 225.65/29.15 inference(resolution,[status(thm)],[f652,f91])).
% 225.65/29.15 fof(f654,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p2(X4)|p3(X4))),
% 225.65/29.15 inference(resolution,[status(thm)],[f653,f92])).
% 225.65/29.15 fof(f655,plain,(
% 225.65/29.15 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p2(X3)|p3(X3))),
% 225.65/29.15 inference(resolution,[status(thm)],[f654,f93])).
% 225.65/29.15 fof(f656,plain,(
% 225.65/29.15 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p2(X2)|p3(X2))),
% 225.65/29.15 inference(resolution,[status(thm)],[f655,f94])).
% 225.65/29.15 fof(f657,plain,(
% 225.65/29.15 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p2(X1)|p3(X1))),
% 225.65/29.15 inference(resolution,[status(thm)],[f656,f95])).
% 225.65/29.15 fof(f658,plain,(
% 225.65/29.15 ![X0]: (~r1(sK46_skl,X0)|p2(X0)|p3(X0))),
% 225.65/29.15 inference(resolution,[status(thm)],[f657,f96])).
% 225.65/29.15 fof(f659,plain,(
% 225.65/29.15 p2(sK47_skl)|p3(sK47_skl)),
% 225.65/29.15 inference(resolution,[status(thm)],[f658,f97])).
% 225.65/29.15 fof(f660,plain,(
% 225.65/29.15 sQ30_spl|sQ29_spl),
% 225.65/29.15 inference(split_clause,[status(thm)],[f659,f190,f187])).
% 225.65/29.15 fof(f661,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p3(X10)|p4(X10))),
% 225.65/29.15 inference(resolution,[status(thm)],[f520,f86])).
% 225.65/29.15 fof(f662,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p3(X9)|p4(X9))),
% 225.65/29.15 inference(resolution,[status(thm)],[f661,f87])).
% 225.65/29.15 fof(f663,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p3(X8)|p4(X8))),
% 225.65/29.15 inference(resolution,[status(thm)],[f662,f88])).
% 225.65/29.15 fof(f664,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p3(X7)|p4(X7))),
% 225.65/29.15 inference(resolution,[status(thm)],[f663,f89])).
% 225.65/29.15 fof(f665,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p3(X6)|p4(X6))),
% 225.65/29.15 inference(resolution,[status(thm)],[f664,f90])).
% 225.65/29.15 fof(f666,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p3(X5)|p4(X5))),
% 225.65/29.15 inference(resolution,[status(thm)],[f665,f91])).
% 225.65/29.15 fof(f667,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p3(X4)|p4(X4))),
% 225.65/29.15 inference(resolution,[status(thm)],[f666,f92])).
% 225.65/29.15 fof(f668,plain,(
% 225.65/29.15 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p3(X3)|p4(X3))),
% 225.65/29.15 inference(resolution,[status(thm)],[f667,f93])).
% 225.65/29.15 fof(f669,plain,(
% 225.65/29.15 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p3(X2)|p4(X2))),
% 225.65/29.15 inference(resolution,[status(thm)],[f668,f94])).
% 225.65/29.15 fof(f670,plain,(
% 225.65/29.15 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p3(X1)|p4(X1))),
% 225.65/29.15 inference(resolution,[status(thm)],[f669,f95])).
% 225.65/29.15 fof(f671,plain,(
% 225.65/29.15 ![X0]: (~r1(sK46_skl,X0)|p3(X0)|p4(X0))),
% 225.65/29.15 inference(resolution,[status(thm)],[f670,f96])).
% 225.65/29.15 fof(f672,plain,(
% 225.65/29.15 p3(sK47_skl)|p4(sK47_skl)),
% 225.65/29.15 inference(resolution,[status(thm)],[f671,f97])).
% 225.65/29.15 fof(f673,plain,(
% 225.65/29.15 sQ29_spl|sQ28_spl),
% 225.65/29.15 inference(split_clause,[status(thm)],[f672,f187,f184])).
% 225.65/29.15 fof(f743,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p4(X10)|p5(X10))),
% 225.65/29.15 inference(resolution,[status(thm)],[f521,f86])).
% 225.65/29.15 fof(f744,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p4(X9)|p5(X9))),
% 225.65/29.15 inference(resolution,[status(thm)],[f743,f87])).
% 225.65/29.15 fof(f745,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p4(X8)|p5(X8))),
% 225.65/29.15 inference(resolution,[status(thm)],[f744,f88])).
% 225.65/29.15 fof(f746,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p4(X7)|p5(X7))),
% 225.65/29.15 inference(resolution,[status(thm)],[f745,f89])).
% 225.65/29.15 fof(f747,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p4(X6)|p5(X6))),
% 225.65/29.15 inference(resolution,[status(thm)],[f746,f90])).
% 225.65/29.15 fof(f748,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p4(X5)|p5(X5))),
% 225.65/29.15 inference(resolution,[status(thm)],[f747,f91])).
% 225.65/29.15 fof(f749,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p4(X4)|p5(X4))),
% 225.65/29.15 inference(resolution,[status(thm)],[f748,f92])).
% 225.65/29.15 fof(f750,plain,(
% 225.65/29.15 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p4(X3)|p5(X3))),
% 225.65/29.15 inference(resolution,[status(thm)],[f749,f93])).
% 225.65/29.15 fof(f755,plain,(
% 225.65/29.15 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p4(X2)|p5(X2))),
% 225.65/29.15 inference(resolution,[status(thm)],[f750,f94])).
% 225.65/29.15 fof(f756,plain,(
% 225.65/29.15 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p4(X1)|p5(X1))),
% 225.65/29.15 inference(resolution,[status(thm)],[f755,f95])).
% 225.65/29.15 fof(f757,plain,(
% 225.65/29.15 ![X0]: (~r1(sK46_skl,X0)|p4(X0)|p5(X0))),
% 225.65/29.15 inference(resolution,[status(thm)],[f756,f96])).
% 225.65/29.15 fof(f758,plain,(
% 225.65/29.15 p4(sK47_skl)|p5(sK47_skl)),
% 225.65/29.15 inference(resolution,[status(thm)],[f757,f97])).
% 225.65/29.15 fof(f759,plain,(
% 225.65/29.15 sQ28_spl|sQ27_spl),
% 225.65/29.15 inference(split_clause,[status(thm)],[f758,f184,f181])).
% 225.65/29.15 fof(f760,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p5(X10)|p6(X10))),
% 225.65/29.15 inference(resolution,[status(thm)],[f522,f86])).
% 225.65/29.15 fof(f761,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p5(X9)|p6(X9))),
% 225.65/29.15 inference(resolution,[status(thm)],[f760,f87])).
% 225.65/29.15 fof(f762,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p5(X8)|p6(X8))),
% 225.65/29.15 inference(resolution,[status(thm)],[f761,f88])).
% 225.65/29.15 fof(f763,plain,(
% 225.65/29.15 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p5(X7)|p6(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f762,f89])).
% 225.65/29.17 fof(f764,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p5(X6)|p6(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f763,f90])).
% 225.65/29.17 fof(f765,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p5(X5)|p6(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f764,f91])).
% 225.65/29.17 fof(f766,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p5(X4)|p6(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f765,f92])).
% 225.65/29.17 fof(f767,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p5(X3)|p6(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f766,f93])).
% 225.65/29.17 fof(f768,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p5(X2)|p6(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f767,f94])).
% 225.65/29.17 fof(f769,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p5(X1)|p6(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f768,f95])).
% 225.65/29.17 fof(f770,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p5(X0)|p6(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f769,f96])).
% 225.65/29.17 fof(f771,plain,(
% 225.65/29.17 p5(sK47_skl)|p6(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f770,f97])).
% 225.65/29.17 fof(f772,plain,(
% 225.65/29.17 sQ27_spl|sQ26_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f771,f181,f178])).
% 225.65/29.17 fof(f781,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p6(X10)|p7(X10))),
% 225.65/29.17 inference(resolution,[status(thm)],[f552,f86])).
% 225.65/29.17 fof(f782,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p6(X9)|p7(X9))),
% 225.65/29.17 inference(resolution,[status(thm)],[f781,f87])).
% 225.65/29.17 fof(f783,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p6(X8)|p7(X8))),
% 225.65/29.17 inference(resolution,[status(thm)],[f782,f88])).
% 225.65/29.17 fof(f784,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p6(X7)|p7(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f783,f89])).
% 225.65/29.17 fof(f785,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p6(X6)|p7(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f784,f90])).
% 225.65/29.17 fof(f786,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p6(X5)|p7(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f785,f91])).
% 225.65/29.17 fof(f787,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p6(X4)|p7(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f786,f92])).
% 225.65/29.17 fof(f788,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p6(X3)|p7(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f787,f93])).
% 225.65/29.17 fof(f789,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p6(X2)|p7(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f788,f94])).
% 225.65/29.17 fof(f790,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p6(X1)|p7(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f789,f95])).
% 225.65/29.17 fof(f791,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p6(X0)|p7(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f790,f96])).
% 225.65/29.17 fof(f792,plain,(
% 225.65/29.17 p6(sK47_skl)|p7(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f791,f97])).
% 225.65/29.17 fof(f793,plain,(
% 225.65/29.17 sQ26_spl|sQ25_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f792,f178,f175])).
% 225.65/29.17 fof(f794,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p7(X10)|p8(X10))),
% 225.65/29.17 inference(resolution,[status(thm)],[f553,f86])).
% 225.65/29.17 fof(f795,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p7(X9)|p8(X9))),
% 225.65/29.17 inference(resolution,[status(thm)],[f794,f87])).
% 225.65/29.17 fof(f796,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p7(X8)|p8(X8))),
% 225.65/29.17 inference(resolution,[status(thm)],[f795,f88])).
% 225.65/29.17 fof(f797,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p7(X7)|p8(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f796,f89])).
% 225.65/29.17 fof(f798,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p7(X6)|p8(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f797,f90])).
% 225.65/29.17 fof(f799,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p7(X5)|p8(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f798,f91])).
% 225.65/29.17 fof(f800,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p7(X4)|p8(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f799,f92])).
% 225.65/29.17 fof(f801,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p7(X3)|p8(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f800,f93])).
% 225.65/29.17 fof(f802,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p7(X2)|p8(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f801,f94])).
% 225.65/29.17 fof(f803,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p7(X1)|p8(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f802,f95])).
% 225.65/29.17 fof(f804,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p7(X0)|p8(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f803,f96])).
% 225.65/29.17 fof(f805,plain,(
% 225.65/29.17 p7(sK47_skl)|p8(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f804,f97])).
% 225.65/29.17 fof(f806,plain,(
% 225.65/29.17 sQ25_spl|sQ24_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f805,f175,f172])).
% 225.65/29.17 fof(f816,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p8(sK47_skl)|~sQ25_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f176,f57])).
% 225.65/29.17 fof(f817,definition,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (sQ41_spl <=> (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)))),
% 225.65/29.17 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 225.65/29.17 fof(f818,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~sQ41_spl)),
% 225.65/29.17 inference(component_clause,[status(thm)],[f817])).
% 225.65/29.17 fof(f820,plain,(
% 225.65/29.17 sQ41_spl|~sQ24_spl|~sQ25_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f816,f817,f172,f175])).
% 225.65/29.17 fof(f868,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p8(X10)|p9(X10))),
% 225.65/29.17 inference(resolution,[status(thm)],[f554,f86])).
% 225.65/29.17 fof(f869,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p8(X9)|p9(X9))),
% 225.65/29.17 inference(resolution,[status(thm)],[f868,f87])).
% 225.65/29.17 fof(f870,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p8(X8)|p9(X8))),
% 225.65/29.17 inference(resolution,[status(thm)],[f869,f88])).
% 225.65/29.17 fof(f871,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p8(X7)|p9(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f870,f89])).
% 225.65/29.17 fof(f872,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p8(X6)|p9(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f871,f90])).
% 225.65/29.17 fof(f873,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p8(X5)|p9(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f872,f91])).
% 225.65/29.17 fof(f874,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p8(X4)|p9(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f873,f92])).
% 225.65/29.17 fof(f875,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p8(X3)|p9(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f874,f93])).
% 225.65/29.17 fof(f876,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p8(X2)|p9(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f875,f94])).
% 225.65/29.17 fof(f877,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p8(X1)|p9(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f876,f95])).
% 225.65/29.17 fof(f878,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p8(X0)|p9(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f877,f96])).
% 225.65/29.17 fof(f879,plain,(
% 225.65/29.17 p8(sK47_skl)|p9(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f878,f97])).
% 225.65/29.17 fof(f880,plain,(
% 225.65/29.17 sQ24_spl|sQ23_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f879,f172,f169])).
% 225.65/29.17 fof(f881,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p9(X10)|p10(X10))),
% 225.65/29.17 inference(resolution,[status(thm)],[f555,f86])).
% 225.65/29.17 fof(f882,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p9(X9)|p10(X9))),
% 225.65/29.17 inference(resolution,[status(thm)],[f881,f87])).
% 225.65/29.17 fof(f883,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p9(X8)|p10(X8))),
% 225.65/29.17 inference(resolution,[status(thm)],[f882,f88])).
% 225.65/29.17 fof(f884,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p9(X7)|p10(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f883,f89])).
% 225.65/29.17 fof(f885,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p9(X6)|p10(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f884,f90])).
% 225.65/29.17 fof(f886,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p9(X5)|p10(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f885,f91])).
% 225.65/29.17 fof(f887,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p9(X4)|p10(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f886,f92])).
% 225.65/29.17 fof(f888,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p9(X3)|p10(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f887,f93])).
% 225.65/29.17 fof(f889,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p9(X2)|p10(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f888,f94])).
% 225.65/29.17 fof(f890,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p9(X1)|p10(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f889,f95])).
% 225.65/29.17 fof(f891,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p9(X0)|p10(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f890,f96])).
% 225.65/29.17 fof(f892,plain,(
% 225.65/29.17 p9(sK47_skl)|p10(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f891,f97])).
% 225.65/29.17 fof(f893,plain,(
% 225.65/29.17 sQ23_spl|sQ22_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f892,f169,f166])).
% 225.65/29.17 fof(f894,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p10(X10)|p11(X10))),
% 225.65/29.17 inference(resolution,[status(thm)],[f556,f86])).
% 225.65/29.17 fof(f895,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p10(X9)|p11(X9))),
% 225.65/29.17 inference(resolution,[status(thm)],[f894,f87])).
% 225.65/29.17 fof(f896,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p10(X8)|p11(X8))),
% 225.65/29.17 inference(resolution,[status(thm)],[f895,f88])).
% 225.65/29.17 fof(f897,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p10(X7)|p11(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f896,f89])).
% 225.65/29.17 fof(f898,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p10(X6)|p11(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f897,f90])).
% 225.65/29.17 fof(f899,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p10(X5)|p11(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f898,f91])).
% 225.65/29.17 fof(f900,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p10(X4)|p11(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f899,f92])).
% 225.65/29.17 fof(f901,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p10(X3)|p11(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f900,f93])).
% 225.65/29.17 fof(f902,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p10(X2)|p11(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f901,f94])).
% 225.65/29.17 fof(f903,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p10(X1)|p11(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f902,f95])).
% 225.65/29.17 fof(f904,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p10(X0)|p11(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f903,f96])).
% 225.65/29.17 fof(f905,plain,(
% 225.65/29.17 p10(sK47_skl)|p11(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f904,f97])).
% 225.65/29.17 fof(f906,plain,(
% 225.65/29.17 sQ22_spl|sQ21_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f905,f166,f163])).
% 225.65/29.17 fof(f907,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p11(X10)|p12(X10))),
% 225.65/29.17 inference(resolution,[status(thm)],[f557,f86])).
% 225.65/29.17 fof(f908,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p11(X9)|p12(X9))),
% 225.65/29.17 inference(resolution,[status(thm)],[f907,f87])).
% 225.65/29.17 fof(f909,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p11(X8)|p12(X8))),
% 225.65/29.17 inference(resolution,[status(thm)],[f908,f88])).
% 225.65/29.17 fof(f910,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p11(X7)|p12(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f909,f89])).
% 225.65/29.17 fof(f911,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p11(X6)|p12(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f910,f90])).
% 225.65/29.17 fof(f912,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p11(X5)|p12(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f911,f91])).
% 225.65/29.17 fof(f913,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p11(X4)|p12(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f912,f92])).
% 225.65/29.17 fof(f914,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p11(X3)|p12(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f913,f93])).
% 225.65/29.17 fof(f915,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p11(X2)|p12(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f914,f94])).
% 225.65/29.17 fof(f916,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p11(X1)|p12(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f915,f95])).
% 225.65/29.17 fof(f917,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p11(X0)|p12(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f916,f96])).
% 225.65/29.17 fof(f918,plain,(
% 225.65/29.17 p11(sK47_skl)|p12(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f917,f97])).
% 225.65/29.17 fof(f919,plain,(
% 225.65/29.17 sQ21_spl|sQ20_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f918,f163,f160])).
% 225.65/29.17 fof(f920,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p8(sK47_skl)|~sQ23_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f170,f53])).
% 225.65/29.17 fof(f921,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p10(sK47_skl)|~sQ23_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f170,f49])).
% 225.65/29.17 fof(f922,plain,(
% 225.65/29.17 sQ41_spl|~sQ24_spl|~sQ23_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f920,f817,f172,f169])).
% 225.65/29.17 fof(f923,plain,(
% 225.65/29.17 sQ41_spl|~sQ22_spl|~sQ23_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f921,f817,f166,f169])).
% 225.65/29.17 fof(f927,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p10(sK47_skl)|~sQ21_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f164,f45])).
% 225.65/29.17 fof(f928,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p12(sK47_skl)|~sQ21_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f164,f41])).
% 225.65/29.17 fof(f929,plain,(
% 225.65/29.17 sQ41_spl|~sQ22_spl|~sQ21_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f927,f817,f166,f163])).
% 225.65/29.17 fof(f930,plain,(
% 225.65/29.17 sQ41_spl|~sQ20_spl|~sQ21_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f928,f817,f160,f163])).
% 225.65/29.17 fof(f931,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p6(sK47_skl)|~sQ27_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f182,f65])).
% 225.65/29.17 fof(f932,plain,(
% 225.65/29.17 sQ41_spl|~sQ26_spl|~sQ27_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f931,f817,f178,f181])).
% 225.65/29.17 fof(f933,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p4(sK47_skl)|~sQ27_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f69,f182])).
% 225.65/29.17 fof(f934,plain,(
% 225.65/29.17 sQ41_spl|~sQ28_spl|~sQ27_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f933,f817,f184,f181])).
% 225.65/29.17 fof(f947,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p12(X10)|p13(X10))),
% 225.65/29.17 inference(resolution,[status(thm)],[f558,f86])).
% 225.65/29.17 fof(f948,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p12(X9)|p13(X9))),
% 225.65/29.17 inference(resolution,[status(thm)],[f947,f87])).
% 225.65/29.17 fof(f949,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p12(X8)|p13(X8))),
% 225.65/29.17 inference(resolution,[status(thm)],[f948,f88])).
% 225.65/29.17 fof(f950,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p12(X7)|p13(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f949,f89])).
% 225.65/29.17 fof(f951,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p12(X6)|p13(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f950,f90])).
% 225.65/29.17 fof(f952,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p12(X5)|p13(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f951,f91])).
% 225.65/29.17 fof(f953,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p12(X4)|p13(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f952,f92])).
% 225.65/29.17 fof(f954,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p12(X3)|p13(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f953,f93])).
% 225.65/29.17 fof(f955,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p12(X2)|p13(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f954,f94])).
% 225.65/29.17 fof(f956,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p12(X1)|p13(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f955,f95])).
% 225.65/29.17 fof(f957,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p12(X0)|p13(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f956,f96])).
% 225.65/29.17 fof(f958,plain,(
% 225.65/29.17 p12(sK47_skl)|p13(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f957,f97])).
% 225.65/29.17 fof(f959,plain,(
% 225.65/29.17 sQ20_spl|sQ19_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f958,f160,f157])).
% 225.65/29.17 fof(f960,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p13(X10)|p14(X10))),
% 225.65/29.17 inference(resolution,[status(thm)],[f559,f86])).
% 225.65/29.17 fof(f961,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p13(X9)|p14(X9))),
% 225.65/29.17 inference(resolution,[status(thm)],[f960,f87])).
% 225.65/29.17 fof(f962,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p13(X8)|p14(X8))),
% 225.65/29.17 inference(resolution,[status(thm)],[f961,f88])).
% 225.65/29.17 fof(f963,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p13(X7)|p14(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f962,f89])).
% 225.65/29.17 fof(f964,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p13(X6)|p14(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f963,f90])).
% 225.65/29.17 fof(f965,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p13(X5)|p14(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f964,f91])).
% 225.65/29.17 fof(f966,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p13(X4)|p14(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f965,f92])).
% 225.65/29.17 fof(f967,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p13(X3)|p14(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f966,f93])).
% 225.65/29.17 fof(f968,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p13(X2)|p14(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f967,f94])).
% 225.65/29.17 fof(f969,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p13(X1)|p14(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f968,f95])).
% 225.65/29.17 fof(f970,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p13(X0)|p14(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f969,f96])).
% 225.65/29.17 fof(f971,plain,(
% 225.65/29.17 p13(sK47_skl)|p14(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f970,f97])).
% 225.65/29.17 fof(f972,plain,(
% 225.65/29.17 sQ19_spl|sQ18_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f971,f157,f154])).
% 225.65/29.17 fof(f973,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p14(X10)|p15(X10))),
% 225.65/29.17 inference(resolution,[status(thm)],[f560,f86])).
% 225.65/29.17 fof(f974,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p14(X9)|p15(X9))),
% 225.65/29.17 inference(resolution,[status(thm)],[f973,f87])).
% 225.65/29.17 fof(f975,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p14(X8)|p15(X8))),
% 225.65/29.17 inference(resolution,[status(thm)],[f974,f88])).
% 225.65/29.17 fof(f976,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p14(X7)|p15(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f975,f89])).
% 225.65/29.17 fof(f977,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p14(X6)|p15(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f976,f90])).
% 225.65/29.17 fof(f978,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p14(X5)|p15(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f977,f91])).
% 225.65/29.17 fof(f979,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p14(X4)|p15(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f978,f92])).
% 225.65/29.17 fof(f980,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p14(X3)|p15(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f979,f93])).
% 225.65/29.17 fof(f981,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p14(X2)|p15(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f980,f94])).
% 225.65/29.17 fof(f982,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p14(X1)|p15(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f981,f95])).
% 225.65/29.17 fof(f983,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p14(X0)|p15(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f982,f96])).
% 225.65/29.17 fof(f984,plain,(
% 225.65/29.17 p14(sK47_skl)|p15(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f983,f97])).
% 225.65/29.17 fof(f985,plain,(
% 225.65/29.17 sQ18_spl|sQ17_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f984,f154,f151])).
% 225.65/29.17 fof(f986,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK36_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|p15(X10)|p1(X10))),
% 225.65/29.17 inference(resolution,[status(thm)],[f561,f86])).
% 225.65/29.17 fof(f987,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK37_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|p15(X9)|p1(X9))),
% 225.65/29.17 inference(resolution,[status(thm)],[f986,f87])).
% 225.65/29.17 fof(f988,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK38_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|p15(X8)|p1(X8))),
% 225.65/29.17 inference(resolution,[status(thm)],[f987,f88])).
% 225.65/29.17 fof(f989,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK39_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|p15(X7)|p1(X7))),
% 225.65/29.17 inference(resolution,[status(thm)],[f988,f89])).
% 225.65/29.17 fof(f990,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK40_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|p15(X6)|p1(X6))),
% 225.65/29.17 inference(resolution,[status(thm)],[f989,f90])).
% 225.65/29.17 fof(f991,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK41_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|p15(X5)|p1(X5))),
% 225.65/29.17 inference(resolution,[status(thm)],[f990,f91])).
% 225.65/29.17 fof(f992,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK42_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p15(X4)|p1(X4))),
% 225.65/29.17 inference(resolution,[status(thm)],[f991,f92])).
% 225.65/29.17 fof(f993,plain,(
% 225.65/29.17 ![X0,X1,X2,X3]: (~r1(sK43_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p15(X3)|p1(X3))),
% 225.65/29.17 inference(resolution,[status(thm)],[f992,f93])).
% 225.65/29.17 fof(f994,plain,(
% 225.65/29.17 ![X0,X1,X2]: (~r1(sK44_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p15(X2)|p1(X2))),
% 225.65/29.17 inference(resolution,[status(thm)],[f993,f94])).
% 225.65/29.17 fof(f995,plain,(
% 225.65/29.17 ![X0,X1]: (~r1(sK45_skl,X0)|~r1(X0,X1)|p15(X1)|p1(X1))),
% 225.65/29.17 inference(resolution,[status(thm)],[f994,f95])).
% 225.65/29.17 fof(f996,plain,(
% 225.65/29.17 ![X0]: (~r1(sK46_skl,X0)|p15(X0)|p1(X0))),
% 225.65/29.17 inference(resolution,[status(thm)],[f995,f96])).
% 225.65/29.17 fof(f997,plain,(
% 225.65/29.17 p15(sK47_skl)|p1(sK47_skl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f996,f97])).
% 225.65/29.17 fof(f998,plain,(
% 225.65/29.17 sQ17_spl|sQ31_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f997,f151,f193])).
% 225.65/29.17 fof(f999,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p12(sK47_skl)|~sQ19_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f158,f37])).
% 225.65/29.17 fof(f1000,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p14(sK47_skl)|~sQ19_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f158,f33])).
% 225.65/29.17 fof(f1001,plain,(
% 225.65/29.17 sQ41_spl|~sQ20_spl|~sQ19_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f999,f817,f160,f157])).
% 225.65/29.17 fof(f1002,plain,(
% 225.65/29.17 sQ41_spl|~sQ18_spl|~sQ19_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f1000,f817,f154,f157])).
% 225.65/29.17 fof(f1006,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p14(sK47_skl)|~sQ17_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f152,f29])).
% 225.65/29.17 fof(f1007,plain,(
% 225.65/29.17 sQ41_spl|~sQ18_spl|~sQ17_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f1006,f817,f154,f151])).
% 225.65/29.17 fof(f1012,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p15(sK47_skl)|~sQ31_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f194,f25])).
% 225.65/29.17 fof(f1013,plain,(
% 225.65/29.17 sQ41_spl|~sQ17_spl|~sQ31_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f1012,f817,f151,f193])).
% 225.65/29.17 fof(f1014,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p2(sK47_skl)|~sQ29_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f77,f188])).
% 225.65/29.17 fof(f1015,plain,(
% 225.65/29.17 sQ41_spl|~sQ30_spl|~sQ29_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f1014,f817,f190,f187])).
% 225.65/29.17 fof(f1029,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p2(sK47_skl)|~sQ31_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f81,f194])).
% 225.65/29.17 fof(f1031,plain,(
% 225.65/29.17 sQ41_spl|~sQ30_spl|~sQ31_spl),
% 225.65/29.17 inference(split_clause,[status(thm)],[f1029,f817,f190,f193])).
% 225.65/29.17 fof(f1160,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,sK46_skl)|~sQ41_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f818,f97])).
% 225.65/29.17 fof(f1439,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,sK45_skl)|~sQ41_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f1160,f96])).
% 225.65/29.17 fof(f1646,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,sK44_skl)|~sQ41_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f1439,f95])).
% 225.65/29.17 fof(f1986,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,sK43_skl)|~sQ41_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f1646,f94])).
% 225.65/29.17 fof(f1987,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,sK42_skl)|~sQ41_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f1986,f93])).
% 225.65/29.17 fof(f1991,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,sK41_skl)|~sQ41_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f1987,f92])).
% 225.65/29.17 fof(f1992,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,sK40_skl)|~sQ41_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f1991,f91])).
% 225.65/29.17 fof(f1993,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5,X6]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,sK39_skl)|~sQ41_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f1992,f90])).
% 225.65/29.17 fof(f1994,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4,X5]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,sK38_skl)|~sQ41_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f1993,f89])).
% 225.65/29.17 fof(f1995,plain,(
% 225.65/29.17 ![X0,X1,X2,X3,X4]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,sK37_skl)|~sQ41_spl)),
% 225.65/29.17 inference(resolution,[status(thm)],[f1994,f88])).
% 225.65/29.18 fof(f1996,plain,(
% 225.65/29.18 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,sK36_skl)|~sQ41_spl)),
% 225.65/29.18 inference(resolution,[status(thm)],[f1995,f87])).
% 225.65/29.18 fof(f2003,plain,(
% 225.65/29.18 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,sK35_skl)|~sQ41_spl)),
% 225.65/29.18 inference(resolution,[status(thm)],[f1996,f86])).
% 225.65/29.18 fof(f2004,plain,(
% 225.65/29.18 ![X0,X1]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,sK34_skl)|~sQ41_spl)),
% 225.65/29.18 inference(resolution,[status(thm)],[f2003,f85])).
% 225.65/29.18 fof(f2005,plain,(
% 225.65/29.18 ![X0]: (~r1(sK0_skl,X0)|~r1(X0,sK33_skl)|~sQ41_spl)),
% 225.65/29.18 inference(resolution,[status(thm)],[f2004,f84])).
% 225.65/29.18 fof(f2006,plain,(
% 225.65/29.18 ~r1(sK0_skl,sK32_skl)|~sQ41_spl),
% 225.65/29.18 inference(resolution,[status(thm)],[f2005,f83])).
% 225.65/29.18 fof(f2007,plain,(
% 225.65/29.18 $false|~sQ41_spl),
% 225.65/29.18 inference(forward_subsumption_resolution,[status(thm)],[f2006,f82])).
% 225.65/29.18 fof(f2008,plain,(
% 225.65/29.18 ~sQ41_spl),
% 225.65/29.18 inference(contradiction_clause,[status(thm)],[f2007])).
% 225.65/29.18 fof(f2011,plain,(
% 225.65/29.18 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p6(sK47_skl)|~sQ25_spl)),
% 225.65/29.18 inference(resolution,[status(thm)],[f176,f61])).
% 225.65/29.18 fof(f2013,plain,(
% 225.65/29.18 sQ41_spl|~sQ26_spl|~sQ25_spl),
% 225.65/29.18 inference(split_clause,[status(thm)],[f2011,f817,f178,f175])).
% 225.65/29.18 fof(f2015,plain,(
% 225.65/29.18 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,sK47_skl)|~p3(sK47_skl)|~sQ28_spl)),
% 225.65/29.18 inference(resolution,[status(thm)],[f185,f73])).
% 225.65/29.18 fof(f2016,plain,(
% 225.65/29.18 sQ41_spl|~sQ29_spl|~sQ28_spl),
% 225.65/29.18 inference(split_clause,[status(thm)],[f2015,f817,f187,f184])).
% 225.65/29.18 fof(f2017,plain,(
% 225.65/29.18 $false),
% 225.65/29.18 inference(sat_refutation,[status(thm)],[f647,f660,f673,f759,f772,f793,f806,f820,f880,f893,f906,f919,f922,f923,f929,f930,f932,f934,f959,f972,f985,f998,f1001,f1002,f1007,f1013,f1015,f1031,f2008,f2013,f2016])).
% 225.65/29.18 % SZS output end CNFRefutation for theBenchmark.p
% 225.65/29.18 % Elapsed time: 28.665136 seconds
% 225.65/29.18 % CPU time: 226.194174 seconds
% 225.65/29.18 % Total memory used: 135.881 MB
% 225.65/29.18 % Net memory used: 113.888 MB
%------------------------------------------------------------------------------