Drodi-SAT---4.1.1.THM-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : LCL686+1.015 : 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 : n026.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu Sep 24 01:10:57 PM UTC 2026

% Result   : Theorem 0.12s 0.42s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35  % Computer : n026.cluster.edu
% 0.08/0.35  % Model    : x86_64 x86_64
% 0.08/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35  % Memory   : 8046.5625MB
% 0.08/0.35  % OS       : Linux 6.8.0-71-generic
% 0.08/0.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Mon Sep 21 01:00:51 UTC 2026
% 0.08/0.35  % CPUTime  : 
% 0.12/0.37  % Drodi V4.1.1
% 0.12/0.42  % Refutation found
% 0.12/0.42  % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.42  % SZS output start CNFRefutation for theBenchmark
% 0.12/0.42  fof(f1,axiom,(
% 0.12/0.42    (! [X] : r1(X,X) )),
% 0.12/0.42    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42  fof(f3,conjecture,(
% 0.12/0.42    ~ (? [X] :~ ( (! [Y] :( ~ r1(X,Y)| ~ p45(Y)| (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| $false ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p44(Y)& ~ p43(Y) )| ( ~ p44(Y)& p43(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p43(X)& ~ p42(X) )| ( ~ p43(X)& p42(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p42(Y)& ~ p41(Y) )| ( ~ p42(Y)& p41(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p41(X)& ~ p40(X) )| ( ~ p41(X)& p40(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p40(Y)& ~ p39(Y) )| ( ~ p40(Y)& p39(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p39(X)& ~ p38(X) )| ( ~ p39(X)& p38(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p38(Y)& ~ p37(Y) )| ( ~ p38(Y)& p37(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p37(X)& ~ p36(X) )| ( ~ p37(X)& p36(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p36(Y)& ~ p35(Y) )| ( ~ p36(Y)& p35(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p35(X)& ~ p34(X) )| ( ~ p35(X)& p34(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p34(Y)& ~ p33(Y) )| ( ~ p34(Y)& p33(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p33(X)& ~ p32(X) )| ( ~ p33(X)& p32(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p32(Y)& ~ p31(Y) )| ( ~ p32(Y)& p31(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p31(X)& ~ p30(X) )| ( ~ p31(X)& p30(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p30(Y)& ~ p29(Y) )| ( ~ p30(Y)& p29(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p29(X)& ~ p28(X) )| ( ~ p29(X)& p28(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p28(Y)& ~ p27(Y) )| ( ~ p28(Y)& p27(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p27(X)& ~ p26(X) )| ( ~ p27(X)& p26(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p26(Y)& ~ p25(Y) )| ( ~ p26(Y)& p25(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p25(X)& ~ p24(X) )| ( ~ p25(X)& p24(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p24(Y)& ~ p23(Y) )| ( ~ p24(Y)& p23(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p23(X)& ~ p22(X) )| ( ~ p23(X)& p22(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p22(Y)& ~ p21(Y) )| ( ~ p22(Y)& p21(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p21(X)& ~ p20(X) )| ( ~ p21(X)& p20(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p20(Y)& ~ p19(Y) )| ( ~ p20(Y)& p19(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p19(X)& ~ p18(X) )| ( ~ p19(X)& p18(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p18(Y)& ~ p17(Y) )| ( ~ p18(Y)& p17(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p17(X)& ~ p16(X) )| ( ~ p17(X)& p16(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p16(Y)& ~ p15(Y) )| ( ~ p16(Y)& p15(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p15(X)& ~ p14(X) )| ( ~ p15(X)& p14(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p14(Y)& ~ p13(Y) )| ( ~ p14(Y)& p13(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p13(X)& ~ p12(X) )| ( ~ p13(X)& p12(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p12(Y)& ~ p11(Y) )| ( ~ p12(Y)& p11(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p11(X)& ~ p10(X) )| ( ~ p11(X)& p10(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p10(Y)& ~ p9(Y) )| ( ~ p10(Y)& p9(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p9(X)& ~ p8(X) )| ( ~ p9(X)& p8(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p8(Y)& ~ p7(Y) )| ( ~ p8(Y)& p7(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p7(X)& ~ p6(X) )| ( ~ p7(X)& p6(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p6(Y)& ~ p5(Y) )| ( ~ p6(Y)& p5(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p5(X)& ~ p4(X) )| ( ~ p5(X)& p4(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p4(Y)& ~ p3(Y) )| ( ~ p4(Y)& p3(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p3(X)& ~ p2(X) )| ( ~ p3(X)& p2(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p2(Y)& ~ p1(Y) )| ( ~ p2(Y)& p1(Y) ) ) ))| (! [Y] :( ~ r1(X,Y)| p45(Y) ))| (! [Y] :( ~ r1(X,Y)| ( ~ p43(Y)& ~ p44(Y) )| ( p44(Y)& p43(Y) )| ( ~ p42(Y)& ~ p43(Y) )| ( p43(Y)& p42(Y) )| ( ~ p41(Y)& ~ p42(Y) )| ( p42(Y)& p41(Y) )| ( ~ p40(Y)& ~ p41(Y) )| ( p41(Y)& p40(Y) )| ( ~ p39(Y)& ~ p40(Y) )| ( p40(Y)& p39(Y) )| ( ~ p38(Y)& ~ p39(Y) )| ( p39(Y)& p38(Y) )| ( ~ p37(Y)& ~ p38(Y) )| ( p38(Y)& p37(Y) )| ( ~ p36(Y)& ~ p37(Y) )| ( p37(Y)& p36(Y) )| ( ~ p35(Y)& ~ p36(Y) )| ( p36(Y)& p35(Y) )| ( ~ p34(Y)& ~ p35(Y) )| ( p35(Y)& p34(Y) )| ( ~ p33(Y)& ~ p34(Y) )| ( p34(Y)& p33(Y) )| ( ~ p32(Y)& ~ p33(Y) )| ( p33(Y)& p32(Y) )| ( ~ p31(Y)& ~ p32(Y) )| ( p32(Y)& p31(Y) )| ( ~ p30(Y)& ~ p31(Y) )| ( p31(Y)& p30(Y) )| ( ~ p29(Y)& ~ p30(Y) )| ( p30(Y)& p29(Y) )| ( ~ p28(Y)& ~ p29(Y) )| ( p29(Y)& p28(Y) )| ( ~ p27(Y)& ~ p28(Y) )| ( p28(Y)& p27(Y) )| ( ~ p26(Y)& ~ p27(Y) )| ( p27(Y)& p26(Y) )| ( ~ p25(Y)& ~ p26(Y) )| ( p26(Y)& p25(Y) )| ( ~ p24(Y)& ~ p25(Y) )| ( p25(Y)& p24(Y) )| ( ~ p23(Y)& ~ p24(Y) )| ( p24(Y)& p23(Y) )| ( ~ p22(Y)& ~ p23(Y) )| ( p23(Y)& p22(Y) )| ( ~ p21(Y)& ~ p22(Y) )| ( p22(Y)& p21(Y) )| ( ~ p20(Y)& ~ p21(Y) )| ( p21(Y)& p20(Y) )| ( ~ p19(Y)& ~ p20(Y) )| ( p20(Y)& p19(Y) )| ( ~ p18(Y)& ~ p19(Y) )| ( p19(Y)& p18(Y) )| ( ~ p17(Y)& ~ p18(Y) )| ( p18(Y)& p17(Y) )| ( ~ p16(Y)& ~ p17(Y) )| ( p17(Y)& p16(Y) )| ( ~ p15(Y)& ~ p16(Y) )| ( p16(Y)& p15(Y) )| ( ~ p14(Y)& ~ p15(Y) )| ( p15(Y)& p14(Y) )| ( ~ p13(Y)& ~ p14(Y) )| ( p14(Y)& p13(Y) )| ( ~ p12(Y)& ~ p13(Y) )| ( p13(Y)& p12(Y) )| ( ~ p11(Y)& ~ p12(Y) )| ( p12(Y)& p11(Y) )| ( ~ p10(Y)& ~ p11(Y) )| ( p11(Y)& p10(Y) )| ( ~ p9(Y)& ~ p10(Y) )| ( p10(Y)& p9(Y) )| ( ~ p8(Y)& ~ p9(Y) )| ( p9(Y)& p8(Y) )| ( ~ p7(Y)& ~ p8(Y) )| ( p8(Y)& p7(Y) )| ( ~ p6(Y)& ~ p7(Y) )| ( p7(Y)& p6(Y) )| ( ~ p5(Y)& ~ p6(Y) )| ( p6(Y)& p5(Y) )| ( ~ p4(Y)& ~ p5(Y) )| ( p5(Y)& p4(Y) )| ( ~ p3(Y)& ~ p4(Y) )| ( p4(Y)& p3(Y) )| ( ~ p2(Y)& ~ p3(Y) )| ( p3(Y)& p2(Y) )| ( ~ p1(Y)& ~ p2(Y) )| ( p2(Y)& p1(Y) ) ) )) ) )) )) )),
% 0.12/0.42    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42  fof(f4,negated_conjecture,(
% 0.12/0.42    ~(~ (? [X] :~ ( (! [Y] :( ~ r1(X,Y)| ~ p45(Y)| (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| $false ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p44(Y)& ~ p43(Y) )| ( ~ p44(Y)& p43(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p43(X)& ~ p42(X) )| ( ~ p43(X)& p42(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p42(Y)& ~ p41(Y) )| ( ~ p42(Y)& p41(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p41(X)& ~ p40(X) )| ( ~ p41(X)& p40(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p40(Y)& ~ p39(Y) )| ( ~ p40(Y)& p39(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p39(X)& ~ p38(X) )| ( ~ p39(X)& p38(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p38(Y)& ~ p37(Y) )| ( ~ p38(Y)& p37(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p37(X)& ~ p36(X) )| ( ~ p37(X)& p36(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p36(Y)& ~ p35(Y) )| ( ~ p36(Y)& p35(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p35(X)& ~ p34(X) )| ( ~ p35(X)& p34(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p34(Y)& ~ p33(Y) )| ( ~ p34(Y)& p33(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p33(X)& ~ p32(X) )| ( ~ p33(X)& p32(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p32(Y)& ~ p31(Y) )| ( ~ p32(Y)& p31(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p31(X)& ~ p30(X) )| ( ~ p31(X)& p30(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p30(Y)& ~ p29(Y) )| ( ~ p30(Y)& p29(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p29(X)& ~ p28(X) )| ( ~ p29(X)& p28(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p28(Y)& ~ p27(Y) )| ( ~ p28(Y)& p27(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p27(X)& ~ p26(X) )| ( ~ p27(X)& p26(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p26(Y)& ~ p25(Y) )| ( ~ p26(Y)& p25(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p25(X)& ~ p24(X) )| ( ~ p25(X)& p24(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p24(Y)& ~ p23(Y) )| ( ~ p24(Y)& p23(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p23(X)& ~ p22(X) )| ( ~ p23(X)& p22(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p22(Y)& ~ p21(Y) )| ( ~ p22(Y)& p21(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p21(X)& ~ p20(X) )| ( ~ p21(X)& p20(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p20(Y)& ~ p19(Y) )| ( ~ p20(Y)& p19(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p19(X)& ~ p18(X) )| ( ~ p19(X)& p18(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p18(Y)& ~ p17(Y) )| ( ~ p18(Y)& p17(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p17(X)& ~ p16(X) )| ( ~ p17(X)& p16(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p16(Y)& ~ p15(Y) )| ( ~ p16(Y)& p15(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p15(X)& ~ p14(X) )| ( ~ p15(X)& p14(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p14(Y)& ~ p13(Y) )| ( ~ p14(Y)& p13(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p13(X)& ~ p12(X) )| ( ~ p13(X)& p12(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p12(Y)& ~ p11(Y) )| ( ~ p12(Y)& p11(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p11(X)& ~ p10(X) )| ( ~ p11(X)& p10(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p10(Y)& ~ p9(Y) )| ( ~ p10(Y)& p9(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p9(X)& ~ p8(X) )| ( ~ p9(X)& p8(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p8(Y)& ~ p7(Y) )| ( ~ p8(Y)& p7(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p7(X)& ~ p6(X) )| ( ~ p7(X)& p6(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p6(Y)& ~ p5(Y) )| ( ~ p6(Y)& p5(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p5(X)& ~ p4(X) )| ( ~ p5(X)& p4(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p4(Y)& ~ p3(Y) )| ( ~ p4(Y)& p3(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p3(X)& ~ p2(X) )| ( ~ p3(X)& p2(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p2(Y)& ~ p1(Y) )| ( ~ p2(Y)& p1(Y) ) ) ))| (! [Y] :( ~ r1(X,Y)| p45(Y) ))| (! [Y] :( ~ r1(X,Y)| ( ~ p43(Y)& ~ p44(Y) )| ( p44(Y)& p43(Y) )| ( ~ p42(Y)& ~ p43(Y) )| ( p43(Y)& p42(Y) )| ( ~ p41(Y)& ~ p42(Y) )| ( p42(Y)& p41(Y) )| ( ~ p40(Y)& ~ p41(Y) )| ( p41(Y)& p40(Y) )| ( ~ p39(Y)& ~ p40(Y) )| ( p40(Y)& p39(Y) )| ( ~ p38(Y)& ~ p39(Y) )| ( p39(Y)& p38(Y) )| ( ~ p37(Y)& ~ p38(Y) )| ( p38(Y)& p37(Y) )| ( ~ p36(Y)& ~ p37(Y) )| ( p37(Y)& p36(Y) )| ( ~ p35(Y)& ~ p36(Y) )| ( p36(Y)& p35(Y) )| ( ~ p34(Y)& ~ p35(Y) )| ( p35(Y)& p34(Y) )| ( ~ p33(Y)& ~ p34(Y) )| ( p34(Y)& p33(Y) )| ( ~ p32(Y)& ~ p33(Y) )| ( p33(Y)& p32(Y) )| ( ~ p31(Y)& ~ p32(Y) )| ( p32(Y)& p31(Y) )| ( ~ p30(Y)& ~ p31(Y) )| ( p31(Y)& p30(Y) )| ( ~ p29(Y)& ~ p30(Y) )| ( p30(Y)& p29(Y) )| ( ~ p28(Y)& ~ p29(Y) )| ( p29(Y)& p28(Y) )| ( ~ p27(Y)& ~ p28(Y) )| ( p28(Y)& p27(Y) )| ( ~ p26(Y)& ~ p27(Y) )| ( p27(Y)& p26(Y) )| ( ~ p25(Y)& ~ p26(Y) )| ( p26(Y)& p25(Y) )| ( ~ p24(Y)& ~ p25(Y) )| ( p25(Y)& p24(Y) )| ( ~ p23(Y)& ~ p24(Y) )| ( p24(Y)& p23(Y) )| ( ~ p22(Y)& ~ p23(Y) )| ( p23(Y)& p22(Y) )| ( ~ p21(Y)& ~ p22(Y) )| ( p22(Y)& p21(Y) )| ( ~ p20(Y)& ~ p21(Y) )| ( p21(Y)& p20(Y) )| ( ~ p19(Y)& ~ p20(Y) )| ( p20(Y)& p19(Y) )| ( ~ p18(Y)& ~ p19(Y) )| ( p19(Y)& p18(Y) )| ( ~ p17(Y)& ~ p18(Y) )| ( p18(Y)& p17(Y) )| ( ~ p16(Y)& ~ p17(Y) )| ( p17(Y)& p16(Y) )| ( ~ p15(Y)& ~ p16(Y) )| ( p16(Y)& p15(Y) )| ( ~ p14(Y)& ~ p15(Y) )| ( p15(Y)& p14(Y) )| ( ~ p13(Y)& ~ p14(Y) )| ( p14(Y)& p13(Y) )| ( ~ p12(Y)& ~ p13(Y) )| ( p13(Y)& p12(Y) )| ( ~ p11(Y)& ~ p12(Y) )| ( p12(Y)& p11(Y) )| ( ~ p10(Y)& ~ p11(Y) )| ( p11(Y)& p10(Y) )| ( ~ p9(Y)& ~ p10(Y) )| ( p10(Y)& p9(Y) )| ( ~ p8(Y)& ~ p9(Y) )| ( p9(Y)& p8(Y) )| ( ~ p7(Y)& ~ p8(Y) )| ( p8(Y)& p7(Y) )| ( ~ p6(Y)& ~ p7(Y) )| ( p7(Y)& p6(Y) )| ( ~ p5(Y)& ~ p6(Y) )| ( p6(Y)& p5(Y) )| ( ~ p4(Y)& ~ p5(Y) )| ( p5(Y)& p4(Y) )| ( ~ p3(Y)& ~ p4(Y) )| ( p4(Y)& p3(Y) )| ( ~ p2(Y)& ~ p3(Y) )| ( p3(Y)& p2(Y) )| ( ~ p1(Y)& ~ p2(Y) )| ( p2(Y)& p1(Y) ) ) )) ) )) )) ))),
% 0.12/0.42    inference(negated_conjecture,[status(cth)],[f3])).
% 0.12/0.42  fof(f5,plain,(
% 0.12/0.42    ![X0]: (r1(X0,X0))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.42  fof(f9,plain,(
% 0.12/0.42    ?[X]: ((?[Y]: ((r1(X,Y)&p45(Y))&(?[X]: (r1(Y,X)&p1(X)))))&(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|((((?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: (r1(X,Y)&$true)))&(![Y]: (~r1(X,Y)|((~p44(Y)|p43(Y))&(p44(Y)|~p43(Y))))))))&(![X]: (~r1(Y,X)|((~p43(X)|p42(X))&(p43(X)|~p42(X))))))))&(![Y]: (~r1(X,Y)|((~p42(Y)|p41(Y))&(p42(Y)|~p41(Y))))))))&(![X]: (~r1(Y,X)|((~p41(X)|p40(X))&(p41(X)|~p40(X))))))))&(![Y]: (~r1(X,Y)|((~p40(Y)|p39(Y))&(p40(Y)|~p39(Y))))))))&(![X]: (~r1(Y,X)|((~p39(X)|p38(X))&(p39(X)|~p38(X))))))))&(![Y]: (~r1(X,Y)|((~p38(Y)|p37(Y))&(p38(Y)|~p37(Y))))))))&(![X]: (~r1(Y,X)|((~p37(X)|p36(X))&(p37(X)|~p36(X))))))))&(![Y]: (~r1(X,Y)|((~p36(Y)|p35(Y))&(p36(Y)|~p35(Y))))))))&(![X]: (~r1(Y,X)|((~p35(X)|p34(X))&(p35(X)|~p34(X))))))))&(![Y]: (~r1(X,Y)|((~p34(Y)|p33(Y))&(p34(Y)|~p33(Y))))))))&(![X]: (~r1(Y,X)|((~p33(X)|p32(X))&(p33(X)|~p32(X))))))))&(![Y]: (~r1(X,Y)|((~p32(Y)|p31(Y))&(p32(Y)|~p31(Y))))))))&(![X]: (~r1(Y,X)|((~p31(X)|p30(X))&(p31(X)|~p30(X))))))))&(![Y]: (~r1(X,Y)|((~p30(Y)|p29(Y))&(p30(Y)|~p29(Y))))))))&(![X]: (~r1(Y,X)|((~p29(X)|p28(X))&(p29(X)|~p28(X))))))))&(![Y]: (~r1(X,Y)|((~p28(Y)|p27(Y))&(p28(Y)|~p27(Y))))))))&(![X]: (~r1(Y,X)|((~p27(X)|p26(X))&(p27(X)|~p26(X))))))))&(![Y]: (~r1(X,Y)|((~p26(Y)|p25(Y))&(p26(Y)|~p25(Y))))))))&(![X]: (~r1(Y,X)|((~p25(X)|p24(X))&(p25(X)|~p24(X))))))))&(![Y]: (~r1(X,Y)|((~p24(Y)|p23(Y))&(p24(Y)|~p23(Y))))))))&(![X]: (~r1(Y,X)|((~p23(X)|p22(X))&(p23(X)|~p22(X))))))))&(![Y]: (~r1(X,Y)|((~p22(Y)|p21(Y))&(p22(Y)|~p21(Y))))))))&(![X]: (~r1(Y,X)|((~p21(X)|p20(X))&(p21(X)|~p20(X))))))))&(![Y]: (~r1(X,Y)|((~p20(Y)|p19(Y))&(p20(Y)|~p19(Y))))))))&(![X]: (~r1(Y,X)|((~p19(X)|p18(X))&(p19(X)|~p18(X))))))))&(![Y]: (~r1(X,Y)|((~p18(Y)|p17(Y))&(p18(Y)|~p17(Y))))))))&(![X]: (~r1(Y,X)|((~p17(X)|p16(X))&(p17(X)|~p16(X))))))))&(![Y]: (~r1(X,Y)|((~p16(Y)|p15(Y))&(p16(Y)|~p15(Y))))))))&(![X]: (~r1(Y,X)|((~p15(X)|p14(X))&(p15(X)|~p14(X))))))))&(![Y]: (~r1(X,Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y))))))))&(![X]: (~r1(Y,X)|((~p13(X)|p12(X))&(p13(X)|~p12(X))))))))&(![Y]: (~r1(X,Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y))))))))&(![X]: (~r1(Y,X)|((~p11(X)|p10(X))&(p11(X)|~p10(X))))))))&(![Y]: (~r1(X,Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y))))))))&(![X]: (~r1(Y,X)|((~p9(X)|p8(X))&(p9(X)|~p8(X))))))))&(![Y]: (~r1(X,Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y))))))))&(![X]: (~r1(Y,X)|((~p7(X)|p6(X))&(p7(X)|~p6(X))))))))&(![Y]: (~r1(X,Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y))))))))&(![X]: (~r1(Y,X)|((~p5(X)|p4(X))&(p5(X)|~p4(X))))))))&(![Y]: (~r1(X,Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y))))))))&(![X]: (~r1(Y,X)|((~p3(X)|p2(X))&(p3(X)|~p2(X)))))))&(![Y]: (~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(?[Y]: (r1(X,Y)&~p45(Y))))&(?[Y]: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,Y)&(p43(Y)|p44(Y)))&(~p44(Y)|~p43(Y)))&(p42(Y)|p43(Y)))&(~p43(Y)|~p42(Y)))&(p41(Y)|p42(Y)))&(~p42(Y)|~p41(Y)))&(p40(Y)|p41(Y)))&(~p41(Y)|~p40(Y)))&(p39(Y)|p40(Y)))&(~p40(Y)|~p39(Y)))&(p38(Y)|p39(Y)))&(~p39(Y)|~p38(Y)))&(p37(Y)|p38(Y)))&(~p38(Y)|~p37(Y)))&(p36(Y)|p37(Y)))&(~p37(Y)|~p36(Y)))&(p35(Y)|p36(Y)))&(~p36(Y)|~p35(Y)))&(p34(Y)|p35(Y)))&(~p35(Y)|~p34(Y)))&(p33(Y)|p34(Y)))&(~p34(Y)|~p33(Y)))&(p32(Y)|p33(Y)))&(~p33(Y)|~p32(Y)))&(p31(Y)|p32(Y)))&(~p32(Y)|~p31(Y)))&(p30(Y)|p31(Y)))&(~p31(Y)|~p30(Y)))&(p29(Y)|p30(Y)))&(~p30(Y)|~p29(Y)))&(p28(Y)|p29(Y)))&(~p29(Y)|~p28(Y)))&(p27(Y)|p28(Y)))&(~p28(Y)|~p27(Y)))&(p26(Y)|p27(Y)))&(~p27(Y)|~p26(Y)))&(p25(Y)|p26(Y)))&(~p26(Y)|~p25(Y)))&(p24(Y)|p25(Y)))&(~p25(Y)|~p24(Y)))&(p23(Y)|p24(Y)))&(~p24(Y)|~p23(Y)))&(p22(Y)|p23(Y)))&(~p23(Y)|~p22(Y)))&(p21(Y)|p22(Y)))&(~p22(Y)|~p21(Y)))&(p20(Y)|p21(Y)))&(~p21(Y)|~p20(Y)))&(p19(Y)|p20(Y)))&(~p20(Y)|~p19(Y)))&(p18(Y)|p19(Y)))&(~p19(Y)|~p18(Y)))&(p17(Y)|p18(Y)))&(~p18(Y)|~p17(Y)))&(p16(Y)|p17(Y)))&(~p17(Y)|~p16(Y)))&(p15(Y)|p16(Y)))&(~p16(Y)|~p15(Y)))&(p14(Y)|p15(Y)))&(~p15(Y)|~p14(Y)))&(p13(Y)|p14(Y)))&(~p14(Y)|~p13(Y)))&(p12(Y)|p13(Y)))&(~p13(Y)|~p12(Y)))&(p11(Y)|p12(Y)))&(~p12(Y)|~p11(Y)))&(p10(Y)|p11(Y)))&(~p11(Y)|~p10(Y)))&(p9(Y)|p10(Y)))&(~p10(Y)|~p9(Y)))&(p8(Y)|p9(Y)))&(~p9(Y)|~p8(Y)))&(p7(Y)|p8(Y)))&(~p8(Y)|~p7(Y)))&(p6(Y)|p7(Y)))&(~p7(Y)|~p6(Y)))&(p5(Y)|p6(Y)))&(~p6(Y)|~p5(Y)))&(p4(Y)|p5(Y)))&(~p5(Y)|~p4(Y)))&(p3(Y)|p4(Y)))&(~p4(Y)|~p3(Y)))&(p2(Y)|p3(Y)))&(~p3(Y)|~p2(Y)))&(p1(Y)|p2(Y)))&(~p2(Y)|~p1(Y))))))))))),
% 0.12/0.42    inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.12/0.42  fof(f10,plain,(
% 0.12/0.42    ?[X]: ((?[Y]: ((r1(X,Y)&p45(Y))&(?[X]: (r1(Y,X)&p1(X)))))&(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|((((?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&((?[Y]: r1(X,Y))&$true))&(![Y]: (~r1(X,Y)|((~p44(Y)|p43(Y))&(p44(Y)|~p43(Y))))))))&(![X]: (~r1(Y,X)|((~p43(X)|p42(X))&(p43(X)|~p42(X))))))))&(![Y]: (~r1(X,Y)|((~p42(Y)|p41(Y))&(p42(Y)|~p41(Y))))))))&(![X]: (~r1(Y,X)|((~p41(X)|p40(X))&(p41(X)|~p40(X))))))))&(![Y]: (~r1(X,Y)|((~p40(Y)|p39(Y))&(p40(Y)|~p39(Y))))))))&(![X]: (~r1(Y,X)|((~p39(X)|p38(X))&(p39(X)|~p38(X))))))))&(![Y]: (~r1(X,Y)|((~p38(Y)|p37(Y))&(p38(Y)|~p37(Y))))))))&(![X]: (~r1(Y,X)|((~p37(X)|p36(X))&(p37(X)|~p36(X))))))))&(![Y]: (~r1(X,Y)|((~p36(Y)|p35(Y))&(p36(Y)|~p35(Y))))))))&(![X]: (~r1(Y,X)|((~p35(X)|p34(X))&(p35(X)|~p34(X))))))))&(![Y]: (~r1(X,Y)|((~p34(Y)|p33(Y))&(p34(Y)|~p33(Y))))))))&(![X]: (~r1(Y,X)|((~p33(X)|p32(X))&(p33(X)|~p32(X))))))))&(![Y]: (~r1(X,Y)|((~p32(Y)|p31(Y))&(p32(Y)|~p31(Y))))))))&(![X]: (~r1(Y,X)|((~p31(X)|p30(X))&(p31(X)|~p30(X))))))))&(![Y]: (~r1(X,Y)|((~p30(Y)|p29(Y))&(p30(Y)|~p29(Y))))))))&(![X]: (~r1(Y,X)|((~p29(X)|p28(X))&(p29(X)|~p28(X))))))))&(![Y]: (~r1(X,Y)|((~p28(Y)|p27(Y))&(p28(Y)|~p27(Y))))))))&(![X]: (~r1(Y,X)|((~p27(X)|p26(X))&(p27(X)|~p26(X))))))))&(![Y]: (~r1(X,Y)|((~p26(Y)|p25(Y))&(p26(Y)|~p25(Y))))))))&(![X]: (~r1(Y,X)|((~p25(X)|p24(X))&(p25(X)|~p24(X))))))))&(![Y]: (~r1(X,Y)|((~p24(Y)|p23(Y))&(p24(Y)|~p23(Y))))))))&(![X]: (~r1(Y,X)|((~p23(X)|p22(X))&(p23(X)|~p22(X))))))))&(![Y]: (~r1(X,Y)|((~p22(Y)|p21(Y))&(p22(Y)|~p21(Y))))))))&(![X]: (~r1(Y,X)|((~p21(X)|p20(X))&(p21(X)|~p20(X))))))))&(![Y]: (~r1(X,Y)|((~p20(Y)|p19(Y))&(p20(Y)|~p19(Y))))))))&(![X]: (~r1(Y,X)|((~p19(X)|p18(X))&(p19(X)|~p18(X))))))))&(![Y]: (~r1(X,Y)|((~p18(Y)|p17(Y))&(p18(Y)|~p17(Y))))))))&(![X]: (~r1(Y,X)|((~p17(X)|p16(X))&(p17(X)|~p16(X))))))))&(![Y]: (~r1(X,Y)|((~p16(Y)|p15(Y))&(p16(Y)|~p15(Y))))))))&(![X]: (~r1(Y,X)|((~p15(X)|p14(X))&(p15(X)|~p14(X))))))))&(![Y]: (~r1(X,Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y))))))))&(![X]: (~r1(Y,X)|((~p13(X)|p12(X))&(p13(X)|~p12(X))))))))&(![Y]: (~r1(X,Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y))))))))&(![X]: (~r1(Y,X)|((~p11(X)|p10(X))&(p11(X)|~p10(X))))))))&(![Y]: (~r1(X,Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y))))))))&(![X]: (~r1(Y,X)|((~p9(X)|p8(X))&(p9(X)|~p8(X))))))))&(![Y]: (~r1(X,Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y))))))))&(![X]: (~r1(Y,X)|((~p7(X)|p6(X))&(p7(X)|~p6(X))))))))&(![Y]: (~r1(X,Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y))))))))&(![X]: (~r1(Y,X)|((~p5(X)|p4(X))&(p5(X)|~p4(X))))))))&(![Y]: (~r1(X,Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y))))))))&(![X]: (~r1(Y,X)|((~p3(X)|p2(X))&(p3(X)|~p2(X)))))))&(![Y]: (~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(?[Y]: (r1(X,Y)&~p45(Y))))&(?[Y]: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,Y)&(p43(Y)|p44(Y)))&(~p44(Y)|~p43(Y)))&(p42(Y)|p43(Y)))&(~p43(Y)|~p42(Y)))&(p41(Y)|p42(Y)))&(~p42(Y)|~p41(Y)))&(p40(Y)|p41(Y)))&(~p41(Y)|~p40(Y)))&(p39(Y)|p40(Y)))&(~p40(Y)|~p39(Y)))&(p38(Y)|p39(Y)))&(~p39(Y)|~p38(Y)))&(p37(Y)|p38(Y)))&(~p38(Y)|~p37(Y)))&(p36(Y)|p37(Y)))&(~p37(Y)|~p36(Y)))&(p35(Y)|p36(Y)))&(~p36(Y)|~p35(Y)))&(p34(Y)|p35(Y)))&(~p35(Y)|~p34(Y)))&(p33(Y)|p34(Y)))&(~p34(Y)|~p33(Y)))&(p32(Y)|p33(Y)))&(~p33(Y)|~p32(Y)))&(p31(Y)|p32(Y)))&(~p32(Y)|~p31(Y)))&(p30(Y)|p31(Y)))&(~p31(Y)|~p30(Y)))&(p29(Y)|p30(Y)))&(~p30(Y)|~p29(Y)))&(p28(Y)|p29(Y)))&(~p29(Y)|~p28(Y)))&(p27(Y)|p28(Y)))&(~p28(Y)|~p27(Y)))&(p26(Y)|p27(Y)))&(~p27(Y)|~p26(Y)))&(p25(Y)|p26(Y)))&(~p26(Y)|~p25(Y)))&(p24(Y)|p25(Y)))&(~p25(Y)|~p24(Y)))&(p23(Y)|p24(Y)))&(~p24(Y)|~p23(Y)))&(p22(Y)|p23(Y)))&(~p23(Y)|~p22(Y)))&(p21(Y)|p22(Y)))&(~p22(Y)|~p21(Y)))&(p20(Y)|p21(Y)))&(~p21(Y)|~p20(Y)))&(p19(Y)|p20(Y)))&(~p20(Y)|~p19(Y)))&(p18(Y)|p19(Y)))&(~p19(Y)|~p18(Y)))&(p17(Y)|p18(Y)))&(~p18(Y)|~p17(Y)))&(p16(Y)|p17(Y)))&(~p17(Y)|~p16(Y)))&(p15(Y)|p16(Y)))&(~p16(Y)|~p15(Y)))&(p14(Y)|p15(Y)))&(~p15(Y)|~p14(Y)))&(p13(Y)|p14(Y)))&(~p14(Y)|~p13(Y)))&(p12(Y)|p13(Y)))&(~p13(Y)|~p12(Y)))&(p11(Y)|p12(Y)))&(~p12(Y)|~p11(Y)))&(p10(Y)|p11(Y)))&(~p11(Y)|~p10(Y)))&(p9(Y)|p10(Y)))&(~p10(Y)|~p9(Y)))&(p8(Y)|p9(Y)))&(~p9(Y)|~p8(Y)))&(p7(Y)|p8(Y)))&(~p8(Y)|~p7(Y)))&(p6(Y)|p7(Y)))&(~p7(Y)|~p6(Y)))&(p5(Y)|p6(Y)))&(~p6(Y)|~p5(Y)))&(p4(Y)|p5(Y)))&(~p5(Y)|~p4(Y)))&(p3(Y)|p4(Y)))&(~p4(Y)|~p3(Y)))&(p2(Y)|p3(Y)))&(~p3(Y)|~p2(Y)))&(p1(Y)|p2(Y)))&(~p2(Y)|~p1(Y))))))))))),
% 0.12/0.42    inference(miniscoping,[status(thm)],[f9])).
% 0.12/0.42  fof(f11,plain,(
% 0.12/0.42    (((r1(sK0_skl,sK1_skl)&p45(sK1_skl))&(r1(sK1_skl,sK2_skl)&p1(sK2_skl)))&(r1(sK0_skl,sK3_skl)&(![X]: (~r1(sK3_skl,X)|(((((r1(X,sK4_skl(X))&((r1(sK4_skl(X),sK5_skl(X))&((r1(sK5_skl(X),sK6_skl(X))&((r1(sK6_skl(X),sK7_skl(X))&((r1(sK7_skl(X),sK8_skl(X))&((r1(sK8_skl(X),sK9_skl(X))&((r1(sK9_skl(X),sK10_skl(X))&((r1(sK10_skl(X),sK11_skl(X))&((r1(sK11_skl(X),sK12_skl(X))&((r1(sK12_skl(X),sK13_skl(X))&((r1(sK13_skl(X),sK14_skl(X))&((r1(sK14_skl(X),sK15_skl(X))&((r1(sK15_skl(X),sK16_skl(X))&((r1(sK16_skl(X),sK17_skl(X))&((r1(sK17_skl(X),sK18_skl(X))&((r1(sK18_skl(X),sK19_skl(X))&((r1(sK19_skl(X),sK20_skl(X))&((r1(sK20_skl(X),sK21_skl(X))&((r1(sK21_skl(X),sK22_skl(X))&((r1(sK22_skl(X),sK23_skl(X))&((r1(sK23_skl(X),sK24_skl(X))&((r1(sK24_skl(X),sK25_skl(X))&((r1(sK25_skl(X),sK26_skl(X))&((r1(sK26_skl(X),sK27_skl(X))&((r1(sK27_skl(X),sK28_skl(X))&((r1(sK28_skl(X),sK29_skl(X))&((r1(sK29_skl(X),sK30_skl(X))&((r1(sK30_skl(X),sK31_skl(X))&((r1(sK31_skl(X),sK32_skl(X))&((r1(sK32_skl(X),sK33_skl(X))&((r1(sK33_skl(X),sK34_skl(X))&((r1(sK34_skl(X),sK35_skl(X))&((r1(sK35_skl(X),sK36_skl(X))&((r1(sK36_skl(X),sK37_skl(X))&((r1(sK37_skl(X),sK38_skl(X))&((r1(sK38_skl(X),sK39_skl(X))&((r1(sK39_skl(X),sK40_skl(X))&((r1(sK40_skl(X),sK41_skl(X))&((r1(sK41_skl(X),sK42_skl(X))&((r1(sK42_skl(X),sK43_skl(X))&((r1(sK43_skl(X),sK44_skl(X))&((r1(sK44_skl(X),sK45_skl(X))&(r1(sK45_skl(X),sK46_skl(X))&$true))&(![Y]: (~r1(sK45_skl(X),Y)|((~p44(Y)|p43(Y))&(p44(Y)|~p43(Y)))))))&(![X]: (~r1(sK44_skl(X),X)|((~p43(X)|p42(X))&(p43(X)|~p42(X)))))))&(![Y]: (~r1(sK43_skl(X),Y)|((~p42(Y)|p41(Y))&(p42(Y)|~p41(Y)))))))&(![X]: (~r1(sK42_skl(X),X)|((~p41(X)|p40(X))&(p41(X)|~p40(X)))))))&(![Y]: (~r1(sK41_skl(X),Y)|((~p40(Y)|p39(Y))&(p40(Y)|~p39(Y)))))))&(![X]: (~r1(sK40_skl(X),X)|((~p39(X)|p38(X))&(p39(X)|~p38(X)))))))&(![Y]: (~r1(sK39_skl(X),Y)|((~p38(Y)|p37(Y))&(p38(Y)|~p37(Y)))))))&(![X]: (~r1(sK38_skl(X),X)|((~p37(X)|p36(X))&(p37(X)|~p36(X)))))))&(![Y]: (~r1(sK37_skl(X),Y)|((~p36(Y)|p35(Y))&(p36(Y)|~p35(Y)))))))&(![X]: (~r1(sK36_skl(X),X)|((~p35(X)|p34(X))&(p35(X)|~p34(X)))))))&(![Y]: (~r1(sK35_skl(X),Y)|((~p34(Y)|p33(Y))&(p34(Y)|~p33(Y)))))))&(![X]: (~r1(sK34_skl(X),X)|((~p33(X)|p32(X))&(p33(X)|~p32(X)))))))&(![Y]: (~r1(sK33_skl(X),Y)|((~p32(Y)|p31(Y))&(p32(Y)|~p31(Y)))))))&(![X]: (~r1(sK32_skl(X),X)|((~p31(X)|p30(X))&(p31(X)|~p30(X)))))))&(![Y]: (~r1(sK31_skl(X),Y)|((~p30(Y)|p29(Y))&(p30(Y)|~p29(Y)))))))&(![X]: (~r1(sK30_skl(X),X)|((~p29(X)|p28(X))&(p29(X)|~p28(X)))))))&(![Y]: (~r1(sK29_skl(X),Y)|((~p28(Y)|p27(Y))&(p28(Y)|~p27(Y)))))))&(![X]: (~r1(sK28_skl(X),X)|((~p27(X)|p26(X))&(p27(X)|~p26(X)))))))&(![Y]: (~r1(sK27_skl(X),Y)|((~p26(Y)|p25(Y))&(p26(Y)|~p25(Y)))))))&(![X]: (~r1(sK26_skl(X),X)|((~p25(X)|p24(X))&(p25(X)|~p24(X)))))))&(![Y]: (~r1(sK25_skl(X),Y)|((~p24(Y)|p23(Y))&(p24(Y)|~p23(Y)))))))&(![X]: (~r1(sK24_skl(X),X)|((~p23(X)|p22(X))&(p23(X)|~p22(X)))))))&(![Y]: (~r1(sK23_skl(X),Y)|((~p22(Y)|p21(Y))&(p22(Y)|~p21(Y)))))))&(![X]: (~r1(sK22_skl(X),X)|((~p21(X)|p20(X))&(p21(X)|~p20(X)))))))&(![Y]: (~r1(sK21_skl(X),Y)|((~p20(Y)|p19(Y))&(p20(Y)|~p19(Y)))))))&(![X]: (~r1(sK20_skl(X),X)|((~p19(X)|p18(X))&(p19(X)|~p18(X)))))))&(![Y]: (~r1(sK19_skl(X),Y)|((~p18(Y)|p17(Y))&(p18(Y)|~p17(Y)))))))&(![X]: (~r1(sK18_skl(X),X)|((~p17(X)|p16(X))&(p17(X)|~p16(X)))))))&(![Y]: (~r1(sK17_skl(X),Y)|((~p16(Y)|p15(Y))&(p16(Y)|~p15(Y)))))))&(![X]: (~r1(sK16_skl(X),X)|((~p15(X)|p14(X))&(p15(X)|~p14(X)))))))&(![Y]: (~r1(sK15_skl(X),Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y)))))))&(![X]: (~r1(sK14_skl(X),X)|((~p13(X)|p12(X))&(p13(X)|~p12(X)))))))&(![Y]: (~r1(sK13_skl(X),Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y)))))))&(![X]: (~r1(sK12_skl(X),X)|((~p11(X)|p10(X))&(p11(X)|~p10(X)))))))&(![Y]: (~r1(sK11_skl(X),Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y)))))))&(![X]: (~r1(sK10_skl(X),X)|((~p9(X)|p8(X))&(p9(X)|~p8(X)))))))&(![Y]: (~r1(sK9_skl(X),Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y)))))))&(![X]: (~r1(sK8_skl(X),X)|((~p7(X)|p6(X))&(p7(X)|~p6(X)))))))&(![Y]: (~r1(sK7_skl(X),Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y)))))))&(![X]: (~r1(sK6_skl(X),X)|((~p5(X)|p4(X))&(p5(X)|~p4(X)))))))&(![Y]: (~r1(sK5_skl(X),Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y)))))))&(![X]: (~r1(sK4_skl(X),X)|((~p3(X)|p2(X))&(p3(X)|~p2(X))))))&(![Y]: (~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(r1(X,sK47_skl(X))&~p45(sK47_skl(X))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,sK48_skl(X))&(p43(sK48_skl(X))|p44(sK48_skl(X))))&(~p44(sK48_skl(X))|~p43(sK48_skl(X))))&(p42(sK48_skl(X))|p43(sK48_skl(X))))&(~p43(sK48_skl(X))|~p42(sK48_skl(X))))&(p41(sK48_skl(X))|p42(sK48_skl(X))))&(~p42(sK48_skl(X))|~p41(sK48_skl(X))))&(p40(sK48_skl(X))|p41(sK48_skl(X))))&(~p41(sK48_skl(X))|~p40(sK48_skl(X))))&(p39(sK48_skl(X))|p40(sK48_skl(X))))&(~p40(sK48_skl(X))|~p39(sK48_skl(X))))&(p38(sK48_skl(X))|p39(sK48_skl(X))))&(~p39(sK48_skl(X))|~p38(sK48_skl(X))))&(p37(sK48_skl(X))|p38(sK48_skl(X))))&(~p38(sK48_skl(X))|~p37(sK48_skl(X))))&(p36(sK48_skl(X))|p37(sK48_skl(X))))&(~p37(sK48_skl(X))|~p36(sK48_skl(X))))&(p35(sK48_skl(X))|p36(sK48_skl(X))))&(~p36(sK48_skl(X))|~p35(sK48_skl(X))))&(p34(sK48_skl(X))|p35(sK48_skl(X))))&(~p35(sK48_skl(X))|~p34(sK48_skl(X))))&(p33(sK48_skl(X))|p34(sK48_skl(X))))&(~p34(sK48_skl(X))|~p33(sK48_skl(X))))&(p32(sK48_skl(X))|p33(sK48_skl(X))))&(~p33(sK48_skl(X))|~p32(sK48_skl(X))))&(p31(sK48_skl(X))|p32(sK48_skl(X))))&(~p32(sK48_skl(X))|~p31(sK48_skl(X))))&(p30(sK48_skl(X))|p31(sK48_skl(X))))&(~p31(sK48_skl(X))|~p30(sK48_skl(X))))&(p29(sK48_skl(X))|p30(sK48_skl(X))))&(~p30(sK48_skl(X))|~p29(sK48_skl(X))))&(p28(sK48_skl(X))|p29(sK48_skl(X))))&(~p29(sK48_skl(X))|~p28(sK48_skl(X))))&(p27(sK48_skl(X))|p28(sK48_skl(X))))&(~p28(sK48_skl(X))|~p27(sK48_skl(X))))&(p26(sK48_skl(X))|p27(sK48_skl(X))))&(~p27(sK48_skl(X))|~p26(sK48_skl(X))))&(p25(sK48_skl(X))|p26(sK48_skl(X))))&(~p26(sK48_skl(X))|~p25(sK48_skl(X))))&(p24(sK48_skl(X))|p25(sK48_skl(X))))&(~p25(sK48_skl(X))|~p24(sK48_skl(X))))&(p23(sK48_skl(X))|p24(sK48_skl(X))))&(~p24(sK48_skl(X))|~p23(sK48_skl(X))))&(p22(sK48_skl(X))|p23(sK48_skl(X))))&(~p23(sK48_skl(X))|~p22(sK48_skl(X))))&(p21(sK48_skl(X))|p22(sK48_skl(X))))&(~p22(sK48_skl(X))|~p21(sK48_skl(X))))&(p20(sK48_skl(X))|p21(sK48_skl(X))))&(~p21(sK48_skl(X))|~p20(sK48_skl(X))))&(p19(sK48_skl(X))|p20(sK48_skl(X))))&(~p20(sK48_skl(X))|~p19(sK48_skl(X))))&(p18(sK48_skl(X))|p19(sK48_skl(X))))&(~p19(sK48_skl(X))|~p18(sK48_skl(X))))&(p17(sK48_skl(X))|p18(sK48_skl(X))))&(~p18(sK48_skl(X))|~p17(sK48_skl(X))))&(p16(sK48_skl(X))|p17(sK48_skl(X))))&(~p17(sK48_skl(X))|~p16(sK48_skl(X))))&(p15(sK48_skl(X))|p16(sK48_skl(X))))&(~p16(sK48_skl(X))|~p15(sK48_skl(X))))&(p14(sK48_skl(X))|p15(sK48_skl(X))))&(~p15(sK48_skl(X))|~p14(sK48_skl(X))))&(p13(sK48_skl(X))|p14(sK48_skl(X))))&(~p14(sK48_skl(X))|~p13(sK48_skl(X))))&(p12(sK48_skl(X))|p13(sK48_skl(X))))&(~p13(sK48_skl(X))|~p12(sK48_skl(X))))&(p11(sK48_skl(X))|p12(sK48_skl(X))))&(~p12(sK48_skl(X))|~p11(sK48_skl(X))))&(p10(sK48_skl(X))|p11(sK48_skl(X))))&(~p11(sK48_skl(X))|~p10(sK48_skl(X))))&(p9(sK48_skl(X))|p10(sK48_skl(X))))&(~p10(sK48_skl(X))|~p9(sK48_skl(X))))&(p8(sK48_skl(X))|p9(sK48_skl(X))))&(~p9(sK48_skl(X))|~p8(sK48_skl(X))))&(p7(sK48_skl(X))|p8(sK48_skl(X))))&(~p8(sK48_skl(X))|~p7(sK48_skl(X))))&(p6(sK48_skl(X))|p7(sK48_skl(X))))&(~p7(sK48_skl(X))|~p6(sK48_skl(X))))&(p5(sK48_skl(X))|p6(sK48_skl(X))))&(~p6(sK48_skl(X))|~p5(sK48_skl(X))))&(p4(sK48_skl(X))|p5(sK48_skl(X))))&(~p5(sK48_skl(X))|~p4(sK48_skl(X))))&(p3(sK48_skl(X))|p4(sK48_skl(X))))&(~p4(sK48_skl(X))|~p3(sK48_skl(X))))&(p2(sK48_skl(X))|p3(sK48_skl(X))))&(~p3(sK48_skl(X))|~p2(sK48_skl(X))))&(p1(sK48_skl(X))|p2(sK48_skl(X))))&(~p2(sK48_skl(X))|~p1(sK48_skl(X)))))))))),
% 0.12/0.42    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,sK48_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl),skolemize(X,sK2_skl),skolemize(Y,sK3_skl),skolemize(Y,sK4_skl(X)),skolemize(X,sK5_skl(X)),skolemize(Y,sK6_skl(X)),skolemize(X,sK7_skl(X)),skolemize(Y,sK8_skl(X)),skolemize(X,sK9_skl(X)),skolemize(Y,sK10_skl(X)),skolemize(X,sK11_skl(X)),skolemize(Y,sK12_skl(X)),skolemize(X,sK13_skl(X)),skolemize(Y,sK14_skl(X)),skolemize(X,sK15_skl(X)),skolemize(Y,sK16_skl(X)),skolemize(X,sK17_skl(X)),skolemize(Y,sK18_skl(X)),skolemize(X,sK19_skl(X)),skolemize(Y,sK20_skl(X)),skolemize(X,sK21_skl(X)),skolemize(Y,sK22_skl(X)),skolemize(X,sK23_skl(X)),skolemize(Y,sK24_skl(X)),skolemize(X,sK25_skl(X)),skolemize(Y,sK26_skl(X)),skolemize(X,sK27_skl(X)),skolemize(Y,sK28_skl(X)),skolemize(X,sK29_skl(X)),skolemize(Y,sK30_skl(X)),skolemize(X,sK31_skl(X)),skolemize(Y,sK32_skl(X)),skolemize(X,sK33_skl(X)),skolemize(Y,sK34_skl(X)),skolemize(X,sK35_skl(X)),skolemize(Y,sK36_skl(X)),skolemize(X,sK37_skl(X)),skolemize(Y,sK38_skl(X)),skolemize(X,sK39_skl(X)),skolemize(Y,sK40_skl(X)),skolemize(X,sK41_skl(X)),skolemize(Y,sK42_skl(X)),skolemize(X,sK43_skl(X)),skolemize(Y,sK44_skl(X)),skolemize(X,sK45_skl(X)),skolemize(Y,sK46_skl(X)),skolemize(Y,sK47_skl(X)),skolemize(Y,sK48_skl(X))],[f10])).
% 0.12/0.42  fof(f12,plain,(
% 0.12/0.42    ?[X]: ((?[Y]: ((r1(sK0_skl,sK1_skl)&p45(sK1_skl))&(?[X]: (r1(sK1_skl,sK2_skl)&p1(sK2_skl)))))&(?[Y]: (r1(sK0_skl,sK3_skl)&(![X]: (~r1(sK3_skl,X)|((((?[Y]: ((r1(X,sK4_skl(X))&(?[X]: ((r1(sK4_skl(X),sK5_skl(X))&(?[Y]: ((r1(sK5_skl(X),sK6_skl(X))&(?[X]: ((r1(sK6_skl(X),sK7_skl(X))&(?[Y]: ((r1(sK7_skl(X),sK8_skl(X))&(?[X]: ((r1(sK8_skl(X),sK9_skl(X))&(?[Y]: ((r1(sK9_skl(X),sK10_skl(X))&(?[X]: ((r1(sK10_skl(X),sK11_skl(X))&(?[Y]: ((r1(sK11_skl(X),sK12_skl(X))&(?[X]: ((r1(sK12_skl(X),sK13_skl(X))&(?[Y]: ((r1(sK13_skl(X),sK14_skl(X))&(?[X]: ((r1(sK14_skl(X),sK15_skl(X))&(?[Y]: ((r1(sK15_skl(X),sK16_skl(X))&(?[X]: ((r1(sK16_skl(X),sK17_skl(X))&(?[Y]: ((r1(sK17_skl(X),sK18_skl(X))&(?[X]: ((r1(sK18_skl(X),sK19_skl(X))&(?[Y]: ((r1(sK19_skl(X),sK20_skl(X))&(?[X]: ((r1(sK20_skl(X),sK21_skl(X))&(?[Y]: ((r1(sK21_skl(X),sK22_skl(X))&(?[X]: ((r1(sK22_skl(X),sK23_skl(X))&(?[Y]: ((r1(sK23_skl(X),sK24_skl(X))&(?[X]: ((r1(sK24_skl(X),sK25_skl(X))&(?[Y]: ((r1(sK25_skl(X),sK26_skl(X))&(?[X]: ((r1(sK26_skl(X),sK27_skl(X))&(?[Y]: ((r1(sK27_skl(X),sK28_skl(X))&(?[X]: ((r1(sK28_skl(X),sK29_skl(X))&(?[Y]: ((r1(sK29_skl(X),sK30_skl(X))&(?[X]: ((r1(sK30_skl(X),sK31_skl(X))&(?[Y]: ((r1(sK31_skl(X),sK32_skl(X))&(?[X]: ((r1(sK32_skl(X),sK33_skl(X))&(?[Y]: ((r1(sK33_skl(X),sK34_skl(X))&(?[X]: ((r1(sK34_skl(X),sK35_skl(X))&(?[Y]: ((r1(sK35_skl(X),sK36_skl(X))&(?[X]: ((r1(sK36_skl(X),sK37_skl(X))&(?[Y]: ((r1(sK37_skl(X),sK38_skl(X))&(?[X]: ((r1(sK38_skl(X),sK39_skl(X))&(?[Y]: ((r1(sK39_skl(X),sK40_skl(X))&(?[X]: ((r1(sK40_skl(X),sK41_skl(X))&(?[Y]: ((r1(sK41_skl(X),sK42_skl(X))&(?[X]: ((r1(sK42_skl(X),sK43_skl(X))&(?[Y]: ((r1(sK43_skl(X),sK44_skl(X))&(?[X]: ((r1(sK44_skl(X),sK45_skl(X))&(?[Y]: r1(sK45_skl(X),sK46_skl(X))))&(![Y]: (~r1(sK45_skl(X),Y)|((~p44(Y)|p43(Y))&(p44(Y)|~p43(Y))))))))&(![X]: (~r1(sK44_skl(X),X)|((~p43(X)|p42(X))&(p43(X)|~p42(X))))))))&(![Y]: (~r1(sK43_skl(X),Y)|((~p42(Y)|p41(Y))&(p42(Y)|~p41(Y))))))))&(![X]: (~r1(sK42_skl(X),X)|((~p41(X)|p40(X))&(p41(X)|~p40(X))))))))&(![Y]: (~r1(sK41_skl(X),Y)|((~p40(Y)|p39(Y))&(p40(Y)|~p39(Y))))))))&(![X]: (~r1(sK40_skl(X),X)|((~p39(X)|p38(X))&(p39(X)|~p38(X))))))))&(![Y]: (~r1(sK39_skl(X),Y)|((~p38(Y)|p37(Y))&(p38(Y)|~p37(Y))))))))&(![X]: (~r1(sK38_skl(X),X)|((~p37(X)|p36(X))&(p37(X)|~p36(X))))))))&(![Y]: (~r1(sK37_skl(X),Y)|((~p36(Y)|p35(Y))&(p36(Y)|~p35(Y))))))))&(![X]: (~r1(sK36_skl(X),X)|((~p35(X)|p34(X))&(p35(X)|~p34(X))))))))&(![Y]: (~r1(sK35_skl(X),Y)|((~p34(Y)|p33(Y))&(p34(Y)|~p33(Y))))))))&(![X]: (~r1(sK34_skl(X),X)|((~p33(X)|p32(X))&(p33(X)|~p32(X))))))))&(![Y]: (~r1(sK33_skl(X),Y)|((~p32(Y)|p31(Y))&(p32(Y)|~p31(Y))))))))&(![X]: (~r1(sK32_skl(X),X)|((~p31(X)|p30(X))&(p31(X)|~p30(X))))))))&(![Y]: (~r1(sK31_skl(X),Y)|((~p30(Y)|p29(Y))&(p30(Y)|~p29(Y))))))))&(![X]: (~r1(sK30_skl(X),X)|((~p29(X)|p28(X))&(p29(X)|~p28(X))))))))&(![Y]: (~r1(sK29_skl(X),Y)|((~p28(Y)|p27(Y))&(p28(Y)|~p27(Y))))))))&(![X]: (~r1(sK28_skl(X),X)|((~p27(X)|p26(X))&(p27(X)|~p26(X))))))))&(![Y]: (~r1(sK27_skl(X),Y)|((~p26(Y)|p25(Y))&(p26(Y)|~p25(Y))))))))&(![X]: (~r1(sK26_skl(X),X)|((~p25(X)|p24(X))&(p25(X)|~p24(X))))))))&(![Y]: (~r1(sK25_skl(X),Y)|((~p24(Y)|p23(Y))&(p24(Y)|~p23(Y))))))))&(![X]: (~r1(sK24_skl(X),X)|((~p23(X)|p22(X))&(p23(X)|~p22(X))))))))&(![Y]: (~r1(sK23_skl(X),Y)|((~p22(Y)|p21(Y))&(p22(Y)|~p21(Y))))))))&(![X]: (~r1(sK22_skl(X),X)|((~p21(X)|p20(X))&(p21(X)|~p20(X))))))))&(![Y]: (~r1(sK21_skl(X),Y)|((~p20(Y)|p19(Y))&(p20(Y)|~p19(Y))))))))&(![X]: (~r1(sK20_skl(X),X)|((~p19(X)|p18(X))&(p19(X)|~p18(X))))))))&(![Y]: (~r1(sK19_skl(X),Y)|((~p18(Y)|p17(Y))&(p18(Y)|~p17(Y))))))))&(![X]: (~r1(sK18_skl(X),X)|((~p17(X)|p16(X))&(p17(X)|~p16(X))))))))&(![Y]: (~r1(sK17_skl(X),Y)|((~p16(Y)|p15(Y))&(p16(Y)|~p15(Y))))))))&(![X]: (~r1(sK16_skl(X),X)|((~p15(X)|p14(X))&(p15(X)|~p14(X))))))))&(![Y]: (~r1(sK15_skl(X),Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y))))))))&(![X]: (~r1(sK14_skl(X),X)|((~p13(X)|p12(X))&(p13(X)|~p12(X))))))))&(![Y]: (~r1(sK13_skl(X),Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y))))))))&(![X]: (~r1(sK12_skl(X),X)|((~p11(X)|p10(X))&(p11(X)|~p10(X))))))))&(![Y]: (~r1(sK11_skl(X),Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y))))))))&(![X]: (~r1(sK10_skl(X),X)|((~p9(X)|p8(X))&(p9(X)|~p8(X))))))))&(![Y]: (~r1(sK9_skl(X),Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y))))))))&(![X]: (~r1(sK8_skl(X),X)|((~p7(X)|p6(X))&(p7(X)|~p6(X))))))))&(![Y]: (~r1(sK7_skl(X),Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y))))))))&(![X]: (~r1(sK6_skl(X),X)|((~p5(X)|p4(X))&(p5(X)|~p4(X))))))))&(![Y]: (~r1(sK5_skl(X),Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y))))))))&(![X]: (~r1(sK4_skl(X),X)|((~p3(X)|p2(X))&(p3(X)|~p2(X)))))))&(![Y]: (~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(?[Y]: (r1(X,sK47_skl(X))&~p45(sK47_skl(X)))))&(?[Y]: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,sK48_skl(X))&(p43(sK48_skl(X))|p44(sK48_skl(X))))&(~p44(sK48_skl(X))|~p43(sK48_skl(X))))&(p42(sK48_skl(X))|p43(sK48_skl(X))))&(~p43(sK48_skl(X))|~p42(sK48_skl(X))))&(p41(sK48_skl(X))|p42(sK48_skl(X))))&(~p42(sK48_skl(X))|~p41(sK48_skl(X))))&(p40(sK48_skl(X))|p41(sK48_skl(X))))&(~p41(sK48_skl(X))|~p40(sK48_skl(X))))&(p39(sK48_skl(X))|p40(sK48_skl(X))))&(~p40(sK48_skl(X))|~p39(sK48_skl(X))))&(p38(sK48_skl(X))|p39(sK48_skl(X))))&(~p39(sK48_skl(X))|~p38(sK48_skl(X))))&(p37(sK48_skl(X))|p38(sK48_skl(X))))&(~p38(sK48_skl(X))|~p37(sK48_skl(X))))&(p36(sK48_skl(X))|p37(sK48_skl(X))))&(~p37(sK48_skl(X))|~p36(sK48_skl(X))))&(p35(sK48_skl(X))|p36(sK48_skl(X))))&(~p36(sK48_skl(X))|~p35(sK48_skl(X))))&(p34(sK48_skl(X))|p35(sK48_skl(X))))&(~p35(sK48_skl(X))|~p34(sK48_skl(X))))&(p33(sK48_skl(X))|p34(sK48_skl(X))))&(~p34(sK48_skl(X))|~p33(sK48_skl(X))))&(p32(sK48_skl(X))|p33(sK48_skl(X))))&(~p33(sK48_skl(X))|~p32(sK48_skl(X))))&(p31(sK48_skl(X))|p32(sK48_skl(X))))&(~p32(sK48_skl(X))|~p31(sK48_skl(X))))&(p30(sK48_skl(X))|p31(sK48_skl(X))))&(~p31(sK48_skl(X))|~p30(sK48_skl(X))))&(p29(sK48_skl(X))|p30(sK48_skl(X))))&(~p30(sK48_skl(X))|~p29(sK48_skl(X))))&(p28(sK48_skl(X))|p29(sK48_skl(X))))&(~p29(sK48_skl(X))|~p28(sK48_skl(X))))&(p27(sK48_skl(X))|p28(sK48_skl(X))))&(~p28(sK48_skl(X))|~p27(sK48_skl(X))))&(p26(sK48_skl(X))|p27(sK48_skl(X))))&(~p27(sK48_skl(X))|~p26(sK48_skl(X))))&(p25(sK48_skl(X))|p26(sK48_skl(X))))&(~p26(sK48_skl(X))|~p25(sK48_skl(X))))&(p24(sK48_skl(X))|p25(sK48_skl(X))))&(~p25(sK48_skl(X))|~p24(sK48_skl(X))))&(p23(sK48_skl(X))|p24(sK48_skl(X))))&(~p24(sK48_skl(X))|~p23(sK48_skl(X))))&(p22(sK48_skl(X))|p23(sK48_skl(X))))&(~p23(sK48_skl(X))|~p22(sK48_skl(X))))&(p21(sK48_skl(X))|p22(sK48_skl(X))))&(~p22(sK48_skl(X))|~p21(sK48_skl(X))))&(p20(sK48_skl(X))|p21(sK48_skl(X))))&(~p21(sK48_skl(X))|~p20(sK48_skl(X))))&(p19(sK48_skl(X))|p20(sK48_skl(X))))&(~p20(sK48_skl(X))|~p19(sK48_skl(X))))&(p18(sK48_skl(X))|p19(sK48_skl(X))))&(~p19(sK48_skl(X))|~p18(sK48_skl(X))))&(p17(sK48_skl(X))|p18(sK48_skl(X))))&(~p18(sK48_skl(X))|~p17(sK48_skl(X))))&(p16(sK48_skl(X))|p17(sK48_skl(X))))&(~p17(sK48_skl(X))|~p16(sK48_skl(X))))&(p15(sK48_skl(X))|p16(sK48_skl(X))))&(~p16(sK48_skl(X))|~p15(sK48_skl(X))))&(p14(sK48_skl(X))|p15(sK48_skl(X))))&(~p15(sK48_skl(X))|~p14(sK48_skl(X))))&(p13(sK48_skl(X))|p14(sK48_skl(X))))&(~p14(sK48_skl(X))|~p13(sK48_skl(X))))&(p12(sK48_skl(X))|p13(sK48_skl(X))))&(~p13(sK48_skl(X))|~p12(sK48_skl(X))))&(p11(sK48_skl(X))|p12(sK48_skl(X))))&(~p12(sK48_skl(X))|~p11(sK48_skl(X))))&(p10(sK48_skl(X))|p11(sK48_skl(X))))&(~p11(sK48_skl(X))|~p10(sK48_skl(X))))&(p9(sK48_skl(X))|p10(sK48_skl(X))))&(~p10(sK48_skl(X))|~p9(sK48_skl(X))))&(p8(sK48_skl(X))|p9(sK48_skl(X))))&(~p9(sK48_skl(X))|~p8(sK48_skl(X))))&(p7(sK48_skl(X))|p8(sK48_skl(X))))&(~p8(sK48_skl(X))|~p7(sK48_skl(X))))&(p6(sK48_skl(X))|p7(sK48_skl(X))))&(~p7(sK48_skl(X))|~p6(sK48_skl(X))))&(p5(sK48_skl(X))|p6(sK48_skl(X))))&(~p6(sK48_skl(X))|~p5(sK48_skl(X))))&(p4(sK48_skl(X))|p5(sK48_skl(X))))&(~p5(sK48_skl(X))|~p4(sK48_skl(X))))&(p3(sK48_skl(X))|p4(sK48_skl(X))))&(~p4(sK48_skl(X))|~p3(sK48_skl(X))))&(p2(sK48_skl(X))|p3(sK48_skl(X))))&(~p3(sK48_skl(X))|~p2(sK48_skl(X))))&(p1(sK48_skl(X))|p2(sK48_skl(X))))&(~p2(sK48_skl(X))|~p1(sK48_skl(X)))))))))))),
% 0.12/0.42    inference(true_and_false_simplification,[status(thm)],[f11])).
% 0.12/0.42  fof(f18,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|r1(X0,sK4_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f145,plain,(
% 0.12/0.42    ![X0,X1]: (~r1(sK3_skl,X0)|~r1(X0,X1)|~p2(X1)|p1(X1))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f146,plain,(
% 0.12/0.42    ![X0,X1]: (~r1(sK3_skl,X0)|~r1(X0,X1)|p2(X1)|~p1(X1))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f149,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|r1(X0,sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f150,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p43(sK48_skl(X0))|p44(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f151,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p44(sK48_skl(X0))|~p43(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f152,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p42(sK48_skl(X0))|p43(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f153,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p43(sK48_skl(X0))|~p42(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f154,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p41(sK48_skl(X0))|p42(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f155,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p42(sK48_skl(X0))|~p41(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f156,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p40(sK48_skl(X0))|p41(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f158,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p39(sK48_skl(X0))|p40(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f159,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p40(sK48_skl(X0))|~p39(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f160,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p38(sK48_skl(X0))|p39(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f162,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p37(sK48_skl(X0))|p38(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f163,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p38(sK48_skl(X0))|~p37(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f164,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p36(sK48_skl(X0))|p37(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f166,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p35(sK48_skl(X0))|p36(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f167,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p36(sK48_skl(X0))|~p35(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f168,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p34(sK48_skl(X0))|p35(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f170,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p33(sK48_skl(X0))|p34(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f171,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p34(sK48_skl(X0))|~p33(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f172,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p32(sK48_skl(X0))|p33(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f174,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p31(sK48_skl(X0))|p32(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f175,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p32(sK48_skl(X0))|~p31(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f176,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p30(sK48_skl(X0))|p31(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f178,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p29(sK48_skl(X0))|p30(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f179,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p30(sK48_skl(X0))|~p29(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f180,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p28(sK48_skl(X0))|p29(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f182,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p27(sK48_skl(X0))|p28(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f183,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p28(sK48_skl(X0))|~p27(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f184,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p26(sK48_skl(X0))|p27(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f186,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p25(sK48_skl(X0))|p26(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f187,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p26(sK48_skl(X0))|~p25(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f188,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p24(sK48_skl(X0))|p25(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f190,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p23(sK48_skl(X0))|p24(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f191,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p24(sK48_skl(X0))|~p23(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f192,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p22(sK48_skl(X0))|p23(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f194,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p21(sK48_skl(X0))|p22(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f195,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p22(sK48_skl(X0))|~p21(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f196,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p20(sK48_skl(X0))|p21(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f198,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p19(sK48_skl(X0))|p20(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f199,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p20(sK48_skl(X0))|~p19(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f200,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p18(sK48_skl(X0))|p19(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f202,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p17(sK48_skl(X0))|p18(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f203,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p18(sK48_skl(X0))|~p17(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f204,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p16(sK48_skl(X0))|p17(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f206,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p15(sK48_skl(X0))|p16(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f207,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p16(sK48_skl(X0))|~p15(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f208,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p14(sK48_skl(X0))|p15(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f210,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p13(sK48_skl(X0))|p14(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f211,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p14(sK48_skl(X0))|~p13(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f212,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p12(sK48_skl(X0))|p13(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f214,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p11(sK48_skl(X0))|p12(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f215,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p12(sK48_skl(X0))|~p11(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f216,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p10(sK48_skl(X0))|p11(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f218,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p9(sK48_skl(X0))|p10(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f219,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p10(sK48_skl(X0))|~p9(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f220,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p8(sK48_skl(X0))|p9(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f222,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p7(sK48_skl(X0))|p8(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f223,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p8(sK48_skl(X0))|~p7(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f224,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p6(sK48_skl(X0))|p7(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f226,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p5(sK48_skl(X0))|p6(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f227,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p6(sK48_skl(X0))|~p5(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f228,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p4(sK48_skl(X0))|p5(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f229,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p5(sK48_skl(X0))|~p4(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f230,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p3(sK48_skl(X0))|p4(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f231,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p4(sK48_skl(X0))|~p3(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f232,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p2(sK48_skl(X0))|p3(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f233,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p3(sK48_skl(X0))|~p2(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f234,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|p1(sK48_skl(X0))|p2(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f235,plain,(
% 0.12/0.42    ![X0]: (~r1(sK3_skl,X0)|~p2(sK48_skl(X0))|~p1(sK48_skl(X0)))),
% 0.12/0.42    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42  fof(f240,plain,(
% 0.12/0.42    r1(sK3_skl,sK4_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f18,f5])).
% 0.12/0.42  fof(f259,plain,(
% 0.12/0.42    p43(sK48_skl(sK3_skl))|p44(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f150,f5])).
% 0.12/0.42  fof(f267,definition,(
% 0.12/0.42    sQ2_spl <=> (p43(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f268,plain,(
% 0.12/0.42    p43(sK48_skl(sK3_skl))|~sQ2_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f267])).
% 0.12/0.42  fof(f270,definition,(
% 0.12/0.42    sQ3_spl <=> (p44(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f273,plain,(
% 0.12/0.42    sQ2_spl|sQ3_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f259,f267,f270])).
% 0.12/0.42  fof(f275,plain,(
% 0.12/0.42    p42(sK48_skl(sK3_skl))|p43(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f152,f5])).
% 0.12/0.42  fof(f280,definition,(
% 0.12/0.42    sQ5_spl <=> (p42(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f281,plain,(
% 0.12/0.42    p42(sK48_skl(sK3_skl))|~sQ5_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f280])).
% 0.12/0.42  fof(f283,plain,(
% 0.12/0.42    sQ5_spl|sQ2_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f275,f280,f267])).
% 0.12/0.42  fof(f285,plain,(
% 0.12/0.42    p41(sK48_skl(sK3_skl))|p42(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f154,f5])).
% 0.12/0.42  fof(f290,definition,(
% 0.12/0.42    sQ7_spl <=> (p41(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f291,plain,(
% 0.12/0.42    p41(sK48_skl(sK3_skl))|~sQ7_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f290])).
% 0.12/0.42  fof(f293,plain,(
% 0.12/0.42    sQ7_spl|sQ5_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f285,f290,f280])).
% 0.12/0.42  fof(f295,plain,(
% 0.12/0.42    p40(sK48_skl(sK3_skl))|p41(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f156,f5])).
% 0.12/0.42  fof(f300,definition,(
% 0.12/0.42    sQ9_spl <=> (p40(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f303,plain,(
% 0.12/0.42    sQ9_spl|sQ7_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f295,f300,f290])).
% 0.12/0.42  fof(f305,plain,(
% 0.12/0.42    p39(sK48_skl(sK3_skl))|p40(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f158,f5])).
% 0.12/0.42  fof(f310,definition,(
% 0.12/0.42    sQ11_spl <=> (p39(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f311,plain,(
% 0.12/0.42    p39(sK48_skl(sK3_skl))|~sQ11_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f310])).
% 0.12/0.42  fof(f313,plain,(
% 0.12/0.42    sQ11_spl|sQ9_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f305,f310,f300])).
% 0.12/0.42  fof(f315,plain,(
% 0.12/0.42    p38(sK48_skl(sK3_skl))|p39(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f160,f5])).
% 0.12/0.42  fof(f320,definition,(
% 0.12/0.42    sQ13_spl <=> (p38(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f323,plain,(
% 0.12/0.42    sQ13_spl|sQ11_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f315,f320,f310])).
% 0.12/0.42  fof(f325,plain,(
% 0.12/0.42    p37(sK48_skl(sK3_skl))|p38(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f162,f5])).
% 0.12/0.42  fof(f330,definition,(
% 0.12/0.42    sQ15_spl <=> (p37(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f331,plain,(
% 0.12/0.42    p37(sK48_skl(sK3_skl))|~sQ15_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f330])).
% 0.12/0.42  fof(f333,plain,(
% 0.12/0.42    sQ15_spl|sQ13_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f325,f330,f320])).
% 0.12/0.42  fof(f335,plain,(
% 0.12/0.42    p36(sK48_skl(sK3_skl))|p37(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f164,f5])).
% 0.12/0.42  fof(f340,definition,(
% 0.12/0.42    sQ17_spl <=> (p36(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f343,plain,(
% 0.12/0.42    sQ17_spl|sQ15_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f335,f340,f330])).
% 0.12/0.42  fof(f345,plain,(
% 0.12/0.42    p35(sK48_skl(sK3_skl))|p36(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f166,f5])).
% 0.12/0.42  fof(f350,definition,(
% 0.12/0.42    sQ19_spl <=> (p35(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f351,plain,(
% 0.12/0.42    p35(sK48_skl(sK3_skl))|~sQ19_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f350])).
% 0.12/0.42  fof(f353,plain,(
% 0.12/0.42    sQ19_spl|sQ17_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f345,f350,f340])).
% 0.12/0.42  fof(f355,plain,(
% 0.12/0.42    p34(sK48_skl(sK3_skl))|p35(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f168,f5])).
% 0.12/0.42  fof(f360,definition,(
% 0.12/0.42    sQ21_spl <=> (p34(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f363,plain,(
% 0.12/0.42    sQ21_spl|sQ19_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f355,f360,f350])).
% 0.12/0.42  fof(f365,plain,(
% 0.12/0.42    p33(sK48_skl(sK3_skl))|p34(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f170,f5])).
% 0.12/0.42  fof(f370,definition,(
% 0.12/0.42    sQ23_spl <=> (p33(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f371,plain,(
% 0.12/0.42    p33(sK48_skl(sK3_skl))|~sQ23_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f370])).
% 0.12/0.42  fof(f373,plain,(
% 0.12/0.42    sQ23_spl|sQ21_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f365,f370,f360])).
% 0.12/0.42  fof(f375,plain,(
% 0.12/0.42    p32(sK48_skl(sK3_skl))|p33(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f172,f5])).
% 0.12/0.42  fof(f380,definition,(
% 0.12/0.42    sQ25_spl <=> (p32(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f383,plain,(
% 0.12/0.42    sQ25_spl|sQ23_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f375,f380,f370])).
% 0.12/0.42  fof(f385,plain,(
% 0.12/0.42    p31(sK48_skl(sK3_skl))|p32(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f174,f5])).
% 0.12/0.42  fof(f390,definition,(
% 0.12/0.42    sQ27_spl <=> (p31(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f391,plain,(
% 0.12/0.42    p31(sK48_skl(sK3_skl))|~sQ27_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f390])).
% 0.12/0.42  fof(f393,plain,(
% 0.12/0.42    sQ27_spl|sQ25_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f385,f390,f380])).
% 0.12/0.42  fof(f395,plain,(
% 0.12/0.42    p30(sK48_skl(sK3_skl))|p31(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f176,f5])).
% 0.12/0.42  fof(f400,definition,(
% 0.12/0.42    sQ29_spl <=> (p30(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f403,plain,(
% 0.12/0.42    sQ29_spl|sQ27_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f395,f400,f390])).
% 0.12/0.42  fof(f405,plain,(
% 0.12/0.42    p29(sK48_skl(sK3_skl))|p30(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f178,f5])).
% 0.12/0.42  fof(f410,definition,(
% 0.12/0.42    sQ31_spl <=> (p29(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f411,plain,(
% 0.12/0.42    p29(sK48_skl(sK3_skl))|~sQ31_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f410])).
% 0.12/0.42  fof(f413,plain,(
% 0.12/0.42    sQ31_spl|sQ29_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f405,f410,f400])).
% 0.12/0.42  fof(f415,plain,(
% 0.12/0.42    p28(sK48_skl(sK3_skl))|p29(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f180,f5])).
% 0.12/0.42  fof(f420,definition,(
% 0.12/0.42    sQ33_spl <=> (p28(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f423,plain,(
% 0.12/0.42    sQ33_spl|sQ31_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f415,f420,f410])).
% 0.12/0.42  fof(f425,plain,(
% 0.12/0.42    p27(sK48_skl(sK3_skl))|p28(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f182,f5])).
% 0.12/0.42  fof(f430,definition,(
% 0.12/0.42    sQ35_spl <=> (p27(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f431,plain,(
% 0.12/0.42    p27(sK48_skl(sK3_skl))|~sQ35_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f430])).
% 0.12/0.42  fof(f433,plain,(
% 0.12/0.42    sQ35_spl|sQ33_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f425,f430,f420])).
% 0.12/0.42  fof(f435,plain,(
% 0.12/0.42    p26(sK48_skl(sK3_skl))|p27(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f184,f5])).
% 0.12/0.42  fof(f440,definition,(
% 0.12/0.42    sQ37_spl <=> (p26(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f443,plain,(
% 0.12/0.42    sQ37_spl|sQ35_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f435,f440,f430])).
% 0.12/0.42  fof(f445,plain,(
% 0.12/0.42    p25(sK48_skl(sK3_skl))|p26(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f186,f5])).
% 0.12/0.42  fof(f450,definition,(
% 0.12/0.42    sQ39_spl <=> (p25(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f451,plain,(
% 0.12/0.42    p25(sK48_skl(sK3_skl))|~sQ39_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f450])).
% 0.12/0.42  fof(f453,plain,(
% 0.12/0.42    sQ39_spl|sQ37_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f445,f450,f440])).
% 0.12/0.42  fof(f455,plain,(
% 0.12/0.42    p24(sK48_skl(sK3_skl))|p25(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f188,f5])).
% 0.12/0.42  fof(f460,definition,(
% 0.12/0.42    sQ41_spl <=> (p24(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f463,plain,(
% 0.12/0.42    sQ41_spl|sQ39_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f455,f460,f450])).
% 0.12/0.42  fof(f465,plain,(
% 0.12/0.42    p23(sK48_skl(sK3_skl))|p24(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f190,f5])).
% 0.12/0.42  fof(f470,definition,(
% 0.12/0.42    sQ43_spl <=> (p23(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f471,plain,(
% 0.12/0.42    p23(sK48_skl(sK3_skl))|~sQ43_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f470])).
% 0.12/0.42  fof(f473,plain,(
% 0.12/0.42    sQ43_spl|sQ41_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f465,f470,f460])).
% 0.12/0.42  fof(f475,plain,(
% 0.12/0.42    p22(sK48_skl(sK3_skl))|p23(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f192,f5])).
% 0.12/0.42  fof(f480,definition,(
% 0.12/0.42    sQ45_spl <=> (p22(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f483,plain,(
% 0.12/0.42    sQ45_spl|sQ43_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f475,f480,f470])).
% 0.12/0.42  fof(f485,plain,(
% 0.12/0.42    p21(sK48_skl(sK3_skl))|p22(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f194,f5])).
% 0.12/0.42  fof(f490,definition,(
% 0.12/0.42    sQ47_spl <=> (p21(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f491,plain,(
% 0.12/0.42    p21(sK48_skl(sK3_skl))|~sQ47_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f490])).
% 0.12/0.42  fof(f493,plain,(
% 0.12/0.42    sQ47_spl|sQ45_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f485,f490,f480])).
% 0.12/0.42  fof(f495,plain,(
% 0.12/0.42    p20(sK48_skl(sK3_skl))|p21(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f196,f5])).
% 0.12/0.42  fof(f500,definition,(
% 0.12/0.42    sQ49_spl <=> (p20(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f503,plain,(
% 0.12/0.42    sQ49_spl|sQ47_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f495,f500,f490])).
% 0.12/0.42  fof(f505,plain,(
% 0.12/0.42    p19(sK48_skl(sK3_skl))|p20(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f198,f5])).
% 0.12/0.42  fof(f510,definition,(
% 0.12/0.42    sQ51_spl <=> (p19(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f511,plain,(
% 0.12/0.42    p19(sK48_skl(sK3_skl))|~sQ51_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f510])).
% 0.12/0.42  fof(f513,plain,(
% 0.12/0.42    sQ51_spl|sQ49_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f505,f510,f500])).
% 0.12/0.42  fof(f515,plain,(
% 0.12/0.42    p18(sK48_skl(sK3_skl))|p19(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f200,f5])).
% 0.12/0.42  fof(f520,definition,(
% 0.12/0.42    sQ53_spl <=> (p18(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f523,plain,(
% 0.12/0.42    sQ53_spl|sQ51_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f515,f520,f510])).
% 0.12/0.42  fof(f525,plain,(
% 0.12/0.42    p17(sK48_skl(sK3_skl))|p18(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f202,f5])).
% 0.12/0.42  fof(f530,definition,(
% 0.12/0.42    sQ55_spl <=> (p17(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f531,plain,(
% 0.12/0.42    p17(sK48_skl(sK3_skl))|~sQ55_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f530])).
% 0.12/0.42  fof(f533,plain,(
% 0.12/0.42    sQ55_spl|sQ53_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f525,f530,f520])).
% 0.12/0.42  fof(f535,plain,(
% 0.12/0.42    p16(sK48_skl(sK3_skl))|p17(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f204,f5])).
% 0.12/0.42  fof(f540,definition,(
% 0.12/0.42    sQ57_spl <=> (p16(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f543,plain,(
% 0.12/0.42    sQ57_spl|sQ55_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f535,f540,f530])).
% 0.12/0.42  fof(f545,plain,(
% 0.12/0.42    p15(sK48_skl(sK3_skl))|p16(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f206,f5])).
% 0.12/0.42  fof(f550,definition,(
% 0.12/0.42    sQ59_spl <=> (p15(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f551,plain,(
% 0.12/0.42    p15(sK48_skl(sK3_skl))|~sQ59_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f550])).
% 0.12/0.42  fof(f553,plain,(
% 0.12/0.42    sQ59_spl|sQ57_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f545,f550,f540])).
% 0.12/0.42  fof(f555,plain,(
% 0.12/0.42    p14(sK48_skl(sK3_skl))|p15(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f208,f5])).
% 0.12/0.42  fof(f560,definition,(
% 0.12/0.42    sQ61_spl <=> (p14(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f563,plain,(
% 0.12/0.42    sQ61_spl|sQ59_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f555,f560,f550])).
% 0.12/0.42  fof(f565,plain,(
% 0.12/0.42    p13(sK48_skl(sK3_skl))|p14(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f210,f5])).
% 0.12/0.42  fof(f570,definition,(
% 0.12/0.42    sQ63_spl <=> (p13(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f571,plain,(
% 0.12/0.42    p13(sK48_skl(sK3_skl))|~sQ63_spl),
% 0.12/0.42    inference(component_clause,[status(thm)],[f570])).
% 0.12/0.42  fof(f573,plain,(
% 0.12/0.42    sQ63_spl|sQ61_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f565,f570,f560])).
% 0.12/0.42  fof(f575,plain,(
% 0.12/0.42    p12(sK48_skl(sK3_skl))|p13(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f212,f5])).
% 0.12/0.42  fof(f580,definition,(
% 0.12/0.42    sQ65_spl <=> (p12(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f583,plain,(
% 0.12/0.42    sQ65_spl|sQ63_spl),
% 0.12/0.42    inference(split_clause,[status(thm)],[f575,f580,f570])).
% 0.12/0.42  fof(f585,plain,(
% 0.12/0.42    p11(sK48_skl(sK3_skl))|p12(sK48_skl(sK3_skl))),
% 0.12/0.42    inference(resolution,[status(thm)],[f214,f5])).
% 0.12/0.42  fof(f590,definition,(
% 0.12/0.42    sQ67_spl <=> (p11(sK48_skl(sK3_skl)))),
% 0.12/0.42    introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.12/0.42  fof(f591,plain,(
% 0.12/0.42    p11(sK48_skl(sK3_skl))|~sQ67_spl),
% 0.12/0.43    inference(component_clause,[status(thm)],[f590])).
% 0.12/0.43  fof(f593,plain,(
% 0.12/0.43    sQ67_spl|sQ65_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f585,f590,f580])).
% 0.12/0.43  fof(f595,plain,(
% 0.12/0.43    p10(sK48_skl(sK3_skl))|p11(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f216,f5])).
% 0.12/0.43  fof(f600,definition,(
% 0.12/0.43    sQ69_spl <=> (p10(sK48_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f603,plain,(
% 0.12/0.43    sQ69_spl|sQ67_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f595,f600,f590])).
% 0.12/0.43  fof(f605,plain,(
% 0.12/0.43    p9(sK48_skl(sK3_skl))|p10(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f218,f5])).
% 0.12/0.43  fof(f610,definition,(
% 0.12/0.43    sQ71_spl <=> (p9(sK48_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f611,plain,(
% 0.12/0.43    p9(sK48_skl(sK3_skl))|~sQ71_spl),
% 0.12/0.43    inference(component_clause,[status(thm)],[f610])).
% 0.12/0.43  fof(f613,plain,(
% 0.12/0.43    sQ71_spl|sQ69_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f605,f610,f600])).
% 0.12/0.43  fof(f615,plain,(
% 0.12/0.43    p8(sK48_skl(sK3_skl))|p9(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f220,f5])).
% 0.12/0.43  fof(f620,definition,(
% 0.12/0.43    sQ73_spl <=> (p8(sK48_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f623,plain,(
% 0.12/0.43    sQ73_spl|sQ71_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f615,f620,f610])).
% 0.12/0.43  fof(f625,plain,(
% 0.12/0.43    p7(sK48_skl(sK3_skl))|p8(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f222,f5])).
% 0.12/0.43  fof(f630,definition,(
% 0.12/0.43    sQ75_spl <=> (p7(sK48_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f631,plain,(
% 0.12/0.43    p7(sK48_skl(sK3_skl))|~sQ75_spl),
% 0.12/0.43    inference(component_clause,[status(thm)],[f630])).
% 0.12/0.43  fof(f633,plain,(
% 0.12/0.43    sQ75_spl|sQ73_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f625,f630,f620])).
% 0.12/0.43  fof(f635,plain,(
% 0.12/0.43    p6(sK48_skl(sK3_skl))|p7(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f224,f5])).
% 0.12/0.43  fof(f640,definition,(
% 0.12/0.43    sQ77_spl <=> (p6(sK48_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f643,plain,(
% 0.12/0.43    sQ77_spl|sQ75_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f635,f640,f630])).
% 0.12/0.43  fof(f645,plain,(
% 0.12/0.43    p5(sK48_skl(sK3_skl))|p6(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f226,f5])).
% 0.12/0.43  fof(f650,definition,(
% 0.12/0.43    sQ79_spl <=> (p5(sK48_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f651,plain,(
% 0.12/0.43    p5(sK48_skl(sK3_skl))|~sQ79_spl),
% 0.12/0.43    inference(component_clause,[status(thm)],[f650])).
% 0.12/0.43  fof(f653,plain,(
% 0.12/0.43    sQ79_spl|sQ77_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f645,f650,f640])).
% 0.12/0.43  fof(f655,plain,(
% 0.12/0.43    p4(sK48_skl(sK3_skl))|p5(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f228,f5])).
% 0.12/0.43  fof(f660,definition,(
% 0.12/0.43    sQ81_spl <=> (p4(sK48_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f661,plain,(
% 0.12/0.43    p4(sK48_skl(sK3_skl))|~sQ81_spl),
% 0.12/0.43    inference(component_clause,[status(thm)],[f660])).
% 0.12/0.43  fof(f663,plain,(
% 0.12/0.43    sQ81_spl|sQ79_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f655,f660,f650])).
% 0.12/0.43  fof(f665,plain,(
% 0.12/0.43    p3(sK48_skl(sK3_skl))|p4(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f230,f5])).
% 0.12/0.43  fof(f670,definition,(
% 0.12/0.43    sQ83_spl <=> (p3(sK48_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f671,plain,(
% 0.12/0.43    p3(sK48_skl(sK3_skl))|~sQ83_spl),
% 0.12/0.43    inference(component_clause,[status(thm)],[f670])).
% 0.12/0.43  fof(f673,plain,(
% 0.12/0.43    sQ83_spl|sQ81_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f665,f670,f660])).
% 0.12/0.43  fof(f675,plain,(
% 0.12/0.43    p2(sK48_skl(sK3_skl))|p3(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f232,f5])).
% 0.12/0.43  fof(f680,definition,(
% 0.12/0.43    sQ85_spl <=> (p2(sK48_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f681,plain,(
% 0.12/0.43    p2(sK48_skl(sK3_skl))|~sQ85_spl),
% 0.12/0.43    inference(component_clause,[status(thm)],[f680])).
% 0.12/0.43  fof(f683,plain,(
% 0.12/0.43    sQ85_spl|sQ83_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f675,f680,f670])).
% 0.12/0.43  fof(f685,plain,(
% 0.12/0.43    p1(sK48_skl(sK3_skl))|p2(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f234,f5])).
% 0.12/0.43  fof(f690,definition,(
% 0.12/0.43    sQ87_spl <=> (p1(sK48_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f693,plain,(
% 0.12/0.43    sQ87_spl|sQ85_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f685,f690,f680])).
% 0.12/0.43  fof(f849,plain,(
% 0.12/0.43    ![X0]: (~r1(sK3_skl,X0)|~p2(X0)|p1(X0))),
% 0.12/0.43    inference(resolution,[status(thm)],[f145,f5])).
% 0.12/0.43  fof(f851,plain,(
% 0.12/0.43    ![X0]: (~r1(sK3_skl,X0)|p2(X0)|~p1(X0))),
% 0.12/0.43    inference(resolution,[status(thm)],[f146,f5])).
% 0.12/0.43  fof(f855,plain,(
% 0.12/0.43    r1(sK3_skl,sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f149,f5])).
% 0.12/0.43  fof(f857,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p44(sK48_skl(sK3_skl))|~sQ2_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f151,f268])).
% 0.12/0.43  fof(f858,definition,(
% 0.12/0.43    sQ88_spl <=> (r1(sK3_skl,sK4_skl(sK3_skl)))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f860,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK4_skl(sK3_skl))|sQ88_spl),
% 0.12/0.43    inference(component_clause,[status(thm)],[f858])).
% 0.12/0.43  fof(f862,definition,(
% 0.12/0.43    sQ89_spl <=> (r1(sK3_skl,sK3_skl))),
% 0.12/0.43    introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.12/0.43  fof(f864,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|sQ89_spl),
% 0.12/0.43    inference(component_clause,[status(thm)],[f862])).
% 0.12/0.43  fof(f865,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ3_spl|~sQ2_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f857,f862,f270,f267])).
% 0.12/0.43  fof(f866,plain,(
% 0.12/0.43    $false|sQ89_spl),
% 0.12/0.43    inference(forward_subsumption_resolution,[status(thm)],[f864,f5])).
% 0.12/0.43  fof(f867,plain,(
% 0.12/0.43    sQ89_spl),
% 0.12/0.43    inference(contradiction_clause,[status(thm)],[f866])).
% 0.12/0.43  fof(f868,plain,(
% 0.12/0.43    $false|sQ88_spl),
% 0.12/0.43    inference(forward_subsumption_resolution,[status(thm)],[f860,f240])).
% 0.12/0.43  fof(f869,plain,(
% 0.12/0.43    sQ88_spl),
% 0.12/0.43    inference(contradiction_clause,[status(thm)],[f868])).
% 0.12/0.43  fof(f871,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p43(sK48_skl(sK3_skl))|~sQ5_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f153,f281])).
% 0.12/0.43  fof(f873,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ2_spl|~sQ5_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f871,f862,f267,f280])).
% 0.12/0.43  fof(f875,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p40(sK48_skl(sK3_skl))|~sQ11_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f159,f311])).
% 0.12/0.43  fof(f877,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ9_spl|~sQ11_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f875,f862,f300,f310])).
% 0.12/0.43  fof(f879,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p38(sK48_skl(sK3_skl))|~sQ15_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f163,f331])).
% 0.12/0.43  fof(f881,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ13_spl|~sQ15_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f879,f862,f320,f330])).
% 0.12/0.43  fof(f883,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p36(sK48_skl(sK3_skl))|~sQ19_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f167,f351])).
% 0.12/0.43  fof(f885,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ17_spl|~sQ19_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f883,f862,f340,f350])).
% 0.12/0.43  fof(f887,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p34(sK48_skl(sK3_skl))|~sQ23_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f171,f371])).
% 0.12/0.43  fof(f889,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ21_spl|~sQ23_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f887,f862,f360,f370])).
% 0.12/0.43  fof(f891,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p32(sK48_skl(sK3_skl))|~sQ27_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f175,f391])).
% 0.12/0.43  fof(f893,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ25_spl|~sQ27_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f891,f862,f380,f390])).
% 0.12/0.43  fof(f895,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p30(sK48_skl(sK3_skl))|~sQ31_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f179,f411])).
% 0.12/0.43  fof(f897,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ29_spl|~sQ31_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f895,f862,f400,f410])).
% 0.12/0.43  fof(f899,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p28(sK48_skl(sK3_skl))|~sQ35_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f183,f431])).
% 0.12/0.43  fof(f901,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ33_spl|~sQ35_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f899,f862,f420,f430])).
% 0.12/0.43  fof(f903,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p26(sK48_skl(sK3_skl))|~sQ39_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f187,f451])).
% 0.12/0.43  fof(f905,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ37_spl|~sQ39_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f903,f862,f440,f450])).
% 0.12/0.43  fof(f907,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p24(sK48_skl(sK3_skl))|~sQ43_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f191,f471])).
% 0.12/0.43  fof(f909,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ41_spl|~sQ43_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f907,f862,f460,f470])).
% 0.12/0.43  fof(f910,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p42(sK48_skl(sK3_skl))|~sQ7_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f291,f155])).
% 0.12/0.43  fof(f911,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ5_spl|~sQ7_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f910,f862,f280,f290])).
% 0.12/0.43  fof(f913,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p22(sK48_skl(sK3_skl))|~sQ47_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f195,f491])).
% 0.12/0.43  fof(f915,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ45_spl|~sQ47_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f913,f862,f480,f490])).
% 0.12/0.43  fof(f916,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p20(sK48_skl(sK3_skl))|~sQ51_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f199,f511])).
% 0.12/0.43  fof(f917,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ49_spl|~sQ51_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f916,f862,f500,f510])).
% 0.12/0.43  fof(f918,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p18(sK48_skl(sK3_skl))|~sQ55_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f203,f531])).
% 0.12/0.43  fof(f919,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ53_spl|~sQ55_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f918,f862,f520,f530])).
% 0.12/0.43  fof(f922,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p16(sK48_skl(sK3_skl))|~sQ59_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f207,f551])).
% 0.12/0.43  fof(f923,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ57_spl|~sQ59_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f922,f862,f540,f550])).
% 0.12/0.43  fof(f924,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p14(sK48_skl(sK3_skl))|~sQ63_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f211,f571])).
% 0.12/0.43  fof(f925,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ61_spl|~sQ63_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f924,f862,f560,f570])).
% 0.12/0.43  fof(f926,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p12(sK48_skl(sK3_skl))|~sQ67_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f215,f591])).
% 0.12/0.43  fof(f927,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ65_spl|~sQ67_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f926,f862,f580,f590])).
% 0.12/0.43  fof(f928,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p10(sK48_skl(sK3_skl))|~sQ71_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f219,f611])).
% 0.12/0.43  fof(f929,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ69_spl|~sQ71_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f928,f862,f600,f610])).
% 0.12/0.43  fof(f930,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p8(sK48_skl(sK3_skl))|~sQ75_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f223,f631])).
% 0.12/0.43  fof(f931,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ73_spl|~sQ75_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f930,f862,f620,f630])).
% 0.12/0.43  fof(f932,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p6(sK48_skl(sK3_skl))|~sQ79_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f227,f651])).
% 0.12/0.43  fof(f933,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ77_spl|~sQ79_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f932,f862,f640,f650])).
% 0.12/0.43  fof(f934,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p4(sK48_skl(sK3_skl))|~sQ83_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f231,f671])).
% 0.12/0.43  fof(f935,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ81_spl|~sQ83_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f934,f862,f660,f670])).
% 0.12/0.43  fof(f936,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p3(sK48_skl(sK3_skl))|~sQ85_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f233,f681])).
% 0.12/0.43  fof(f937,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ83_spl|~sQ85_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f936,f862,f670,f680])).
% 0.12/0.43  fof(f1832,plain,(
% 0.12/0.43    p2(sK48_skl(sK3_skl))|~p1(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f855,f851])).
% 0.12/0.43  fof(f1833,plain,(
% 0.12/0.43    ~p2(sK48_skl(sK3_skl))|p1(sK48_skl(sK3_skl))),
% 0.12/0.43    inference(resolution,[status(thm)],[f855,f849])).
% 0.12/0.43  fof(f1926,plain,(
% 0.12/0.43    sQ85_spl|~sQ87_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f1832,f680,f690])).
% 0.12/0.43  fof(f1927,plain,(
% 0.12/0.43    ~sQ85_spl|sQ87_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f1833,f680,f690])).
% 0.12/0.43  fof(f2103,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p5(sK48_skl(sK3_skl))|~sQ81_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f661,f229])).
% 0.12/0.43  fof(f2104,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ79_spl|~sQ81_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f2103,f862,f650,f660])).
% 0.12/0.43  fof(f2105,plain,(
% 0.12/0.43    ~r1(sK3_skl,sK3_skl)|~p1(sK48_skl(sK3_skl))|~sQ85_spl),
% 0.12/0.43    inference(resolution,[status(thm)],[f681,f235])).
% 0.12/0.43  fof(f2107,plain,(
% 0.12/0.43    ~sQ89_spl|~sQ87_spl|~sQ85_spl),
% 0.12/0.43    inference(split_clause,[status(thm)],[f2105,f862,f690,f680])).
% 0.12/0.43  fof(f2109,plain,(
% 0.12/0.43    $false),
% 0.12/0.43    inference(sat_refutation,[status(thm)],[f273,f283,f293,f303,f313,f323,f333,f343,f353,f363,f373,f383,f393,f403,f413,f423,f433,f443,f453,f463,f473,f483,f493,f503,f513,f523,f533,f543,f553,f563,f573,f583,f593,f603,f613,f623,f633,f643,f653,f663,f673,f683,f693,f865,f867,f869,f873,f877,f881,f885,f889,f893,f897,f901,f905,f909,f911,f915,f917,f919,f923,f925,f927,f929,f931,f933,f935,f937,f1926,f1927,f2104,f2107])).
% 0.12/0.43  % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.45  % Elapsed time: 0.090932 seconds
% 0.12/0.45  % CPU time: 0.394011 seconds
% 0.12/0.45  % Total memory used: 29.310 MB
% 0.12/0.45  % Net memory used: 29.053 MB
%------------------------------------------------------------------------------