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

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n001.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.14s 5.74s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.36  % Computer : n001.cluster.edu
% 0.10/5.36  % Model    : x86_64 x86_64
% 0.10/5.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36  % Memory   : 8046.5625MB
% 0.10/5.36  % OS       : Linux 6.8.0-71-generic
% 0.10/5.36  % CPULimit : 300
% 0.10/5.36  % WCLimit  : 300
% 0.10/5.36  % DateTime : Mon Sep 21 01:04:03 UTC 2026
% 0.10/5.37  % CPUTime  : 
% 0.10/5.39  % Drodi V4.1.1
% 0.14/5.74  % Refutation found
% 0.14/5.74  % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.74  % SZS output start CNFRefutation for theBenchmark
% 0.14/5.74  fof(f1,axiom,(
% 0.14/5.74    (! [X] : r1(X,X) )),
% 0.14/5.74    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.74  fof(f3,conjecture,(
% 0.14/5.74    ~ (? [X] :~ ( (! [Y] :( ~ r1(X,Y)| ~ p60(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)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| $false ))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p59(X)& ~ p58(X) )| ( ~ p59(X)& p58(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p58(Y)& ~ p57(Y) )| ( ~ p58(Y)& p57(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p57(X)& ~ p56(X) )| ( ~ p57(X)& p56(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p56(Y)& ~ p55(Y) )| ( ~ p56(Y)& p55(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p55(X)& ~ p54(X) )| ( ~ p55(X)& p54(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p54(Y)& ~ p53(Y) )| ( ~ p54(Y)& p53(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p53(X)& ~ p52(X) )| ( ~ p53(X)& p52(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p52(Y)& ~ p51(Y) )| ( ~ p52(Y)& p51(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p51(X)& ~ p50(X) )| ( ~ p51(X)& p50(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p50(Y)& ~ p49(Y) )| ( ~ p50(Y)& p49(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p49(X)& ~ p48(X) )| ( ~ p49(X)& p48(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p48(Y)& ~ p47(Y) )| ( ~ p48(Y)& p47(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p47(X)& ~ p46(X) )| ( ~ p47(X)& p46(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p46(Y)& ~ p45(Y) )| ( ~ p46(Y)& p45(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p45(X)& ~ p44(X) )| ( ~ p45(X)& p44(X) ) ) ) )))| ~ (! [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)| p60(Y) ))| (! [Y] :( ~ r1(X,Y)| ( ~ p58(Y)& ~ p59(Y) )| ( p59(Y)& p58(Y) )| ( ~ p57(Y)& ~ p58(Y) )| ( p58(Y)& p57(Y) )| ( ~ p56(Y)& ~ p57(Y) )| ( p57(Y)& p56(Y) )| ( ~ p55(Y)& ~ p56(Y) )| ( p56(Y)& p55(Y) )| ( ~ p54(Y)& ~ p55(Y) )| ( p55(Y)& p54(Y) )| ( ~ p53(Y)& ~ p54(Y) )| ( p54(Y)& p53(Y) )| ( ~ p52(Y)& ~ p53(Y) )| ( p53(Y)& p52(Y) )| ( ~ p51(Y)& ~ p52(Y) )| ( p52(Y)& p51(Y) )| ( ~ p50(Y)& ~ p51(Y) )| ( p51(Y)& p50(Y) )| ( ~ p49(Y)& ~ p50(Y) )| ( p50(Y)& p49(Y) )| ( ~ p48(Y)& ~ p49(Y) )| ( p49(Y)& p48(Y) )| ( ~ p47(Y)& ~ p48(Y) )| ( p48(Y)& p47(Y) )| ( ~ p46(Y)& ~ p47(Y) )| ( p47(Y)& p46(Y) )| ( ~ p45(Y)& ~ p46(Y) )| ( p46(Y)& p45(Y) )| ( ~ p44(Y)& ~ p45(Y) )| ( p45(Y)& p44(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.14/5.74    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.74  fof(f4,negated_conjecture,(
% 0.14/5.74    ~(~ (? [X] :~ ( (! [Y] :( ~ r1(X,Y)| ~ p60(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)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| $false ))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p59(X)& ~ p58(X) )| ( ~ p59(X)& p58(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p58(Y)& ~ p57(Y) )| ( ~ p58(Y)& p57(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p57(X)& ~ p56(X) )| ( ~ p57(X)& p56(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p56(Y)& ~ p55(Y) )| ( ~ p56(Y)& p55(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p55(X)& ~ p54(X) )| ( ~ p55(X)& p54(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p54(Y)& ~ p53(Y) )| ( ~ p54(Y)& p53(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p53(X)& ~ p52(X) )| ( ~ p53(X)& p52(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p52(Y)& ~ p51(Y) )| ( ~ p52(Y)& p51(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p51(X)& ~ p50(X) )| ( ~ p51(X)& p50(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p50(Y)& ~ p49(Y) )| ( ~ p50(Y)& p49(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p49(X)& ~ p48(X) )| ( ~ p49(X)& p48(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p48(Y)& ~ p47(Y) )| ( ~ p48(Y)& p47(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p47(X)& ~ p46(X) )| ( ~ p47(X)& p46(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p46(Y)& ~ p45(Y) )| ( ~ p46(Y)& p45(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p45(X)& ~ p44(X) )| ( ~ p45(X)& p44(X) ) ) ) )))| ~ (! [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)| p60(Y) ))| (! [Y] :( ~ r1(X,Y)| ( ~ p58(Y)& ~ p59(Y) )| ( p59(Y)& p58(Y) )| ( ~ p57(Y)& ~ p58(Y) )| ( p58(Y)& p57(Y) )| ( ~ p56(Y)& ~ p57(Y) )| ( p57(Y)& p56(Y) )| ( ~ p55(Y)& ~ p56(Y) )| ( p56(Y)& p55(Y) )| ( ~ p54(Y)& ~ p55(Y) )| ( p55(Y)& p54(Y) )| ( ~ p53(Y)& ~ p54(Y) )| ( p54(Y)& p53(Y) )| ( ~ p52(Y)& ~ p53(Y) )| ( p53(Y)& p52(Y) )| ( ~ p51(Y)& ~ p52(Y) )| ( p52(Y)& p51(Y) )| ( ~ p50(Y)& ~ p51(Y) )| ( p51(Y)& p50(Y) )| ( ~ p49(Y)& ~ p50(Y) )| ( p50(Y)& p49(Y) )| ( ~ p48(Y)& ~ p49(Y) )| ( p49(Y)& p48(Y) )| ( ~ p47(Y)& ~ p48(Y) )| ( p48(Y)& p47(Y) )| ( ~ p46(Y)& ~ p47(Y) )| ( p47(Y)& p46(Y) )| ( ~ p45(Y)& ~ p46(Y) )| ( p46(Y)& p45(Y) )| ( ~ p44(Y)& ~ p45(Y) )| ( p45(Y)& p44(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.14/5.74    inference(negated_conjecture,[status(cth)],[f3])).
% 0.14/5.74  fof(f5,plain,(
% 0.14/5.74    ![X0]: (r1(X0,X0))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/5.74  fof(f9,plain,(
% 0.14/5.74    ?[X]: ((?[Y]: ((r1(X,Y)&p60(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)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&$true)))&(![X]: (~r1(Y,X)|((~p59(X)|p58(X))&(p59(X)|~p58(X))))))))&(![Y]: (~r1(X,Y)|((~p58(Y)|p57(Y))&(p58(Y)|~p57(Y))))))))&(![X]: (~r1(Y,X)|((~p57(X)|p56(X))&(p57(X)|~p56(X))))))))&(![Y]: (~r1(X,Y)|((~p56(Y)|p55(Y))&(p56(Y)|~p55(Y))))))))&(![X]: (~r1(Y,X)|((~p55(X)|p54(X))&(p55(X)|~p54(X))))))))&(![Y]: (~r1(X,Y)|((~p54(Y)|p53(Y))&(p54(Y)|~p53(Y))))))))&(![X]: (~r1(Y,X)|((~p53(X)|p52(X))&(p53(X)|~p52(X))))))))&(![Y]: (~r1(X,Y)|((~p52(Y)|p51(Y))&(p52(Y)|~p51(Y))))))))&(![X]: (~r1(Y,X)|((~p51(X)|p50(X))&(p51(X)|~p50(X))))))))&(![Y]: (~r1(X,Y)|((~p50(Y)|p49(Y))&(p50(Y)|~p49(Y))))))))&(![X]: (~r1(Y,X)|((~p49(X)|p48(X))&(p49(X)|~p48(X))))))))&(![Y]: (~r1(X,Y)|((~p48(Y)|p47(Y))&(p48(Y)|~p47(Y))))))))&(![X]: (~r1(Y,X)|((~p47(X)|p46(X))&(p47(X)|~p46(X))))))))&(![Y]: (~r1(X,Y)|((~p46(Y)|p45(Y))&(p46(Y)|~p45(Y))))))))&(![X]: (~r1(Y,X)|((~p45(X)|p44(X))&(p45(X)|~p44(X))))))))&(![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)&~p60(Y))))&(?[Y]: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,Y)&(p58(Y)|p59(Y)))&(~p59(Y)|~p58(Y)))&(p57(Y)|p58(Y)))&(~p58(Y)|~p57(Y)))&(p56(Y)|p57(Y)))&(~p57(Y)|~p56(Y)))&(p55(Y)|p56(Y)))&(~p56(Y)|~p55(Y)))&(p54(Y)|p55(Y)))&(~p55(Y)|~p54(Y)))&(p53(Y)|p54(Y)))&(~p54(Y)|~p53(Y)))&(p52(Y)|p53(Y)))&(~p53(Y)|~p52(Y)))&(p51(Y)|p52(Y)))&(~p52(Y)|~p51(Y)))&(p50(Y)|p51(Y)))&(~p51(Y)|~p50(Y)))&(p49(Y)|p50(Y)))&(~p50(Y)|~p49(Y)))&(p48(Y)|p49(Y)))&(~p49(Y)|~p48(Y)))&(p47(Y)|p48(Y)))&(~p48(Y)|~p47(Y)))&(p46(Y)|p47(Y)))&(~p47(Y)|~p46(Y)))&(p45(Y)|p46(Y)))&(~p46(Y)|~p45(Y)))&(p44(Y)|p45(Y)))&(~p45(Y)|~p44(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.14/5.74    inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.14/5.74  fof(f10,plain,(
% 0.14/5.74    ?[X]: ((?[Y]: ((r1(X,Y)&p60(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)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&((?[X]: r1(Y,X))&$true))&(![X]: (~r1(Y,X)|((~p59(X)|p58(X))&(p59(X)|~p58(X))))))))&(![Y]: (~r1(X,Y)|((~p58(Y)|p57(Y))&(p58(Y)|~p57(Y))))))))&(![X]: (~r1(Y,X)|((~p57(X)|p56(X))&(p57(X)|~p56(X))))))))&(![Y]: (~r1(X,Y)|((~p56(Y)|p55(Y))&(p56(Y)|~p55(Y))))))))&(![X]: (~r1(Y,X)|((~p55(X)|p54(X))&(p55(X)|~p54(X))))))))&(![Y]: (~r1(X,Y)|((~p54(Y)|p53(Y))&(p54(Y)|~p53(Y))))))))&(![X]: (~r1(Y,X)|((~p53(X)|p52(X))&(p53(X)|~p52(X))))))))&(![Y]: (~r1(X,Y)|((~p52(Y)|p51(Y))&(p52(Y)|~p51(Y))))))))&(![X]: (~r1(Y,X)|((~p51(X)|p50(X))&(p51(X)|~p50(X))))))))&(![Y]: (~r1(X,Y)|((~p50(Y)|p49(Y))&(p50(Y)|~p49(Y))))))))&(![X]: (~r1(Y,X)|((~p49(X)|p48(X))&(p49(X)|~p48(X))))))))&(![Y]: (~r1(X,Y)|((~p48(Y)|p47(Y))&(p48(Y)|~p47(Y))))))))&(![X]: (~r1(Y,X)|((~p47(X)|p46(X))&(p47(X)|~p46(X))))))))&(![Y]: (~r1(X,Y)|((~p46(Y)|p45(Y))&(p46(Y)|~p45(Y))))))))&(![X]: (~r1(Y,X)|((~p45(X)|p44(X))&(p45(X)|~p44(X))))))))&(![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)&~p60(Y))))&(?[Y]: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,Y)&(p58(Y)|p59(Y)))&(~p59(Y)|~p58(Y)))&(p57(Y)|p58(Y)))&(~p58(Y)|~p57(Y)))&(p56(Y)|p57(Y)))&(~p57(Y)|~p56(Y)))&(p55(Y)|p56(Y)))&(~p56(Y)|~p55(Y)))&(p54(Y)|p55(Y)))&(~p55(Y)|~p54(Y)))&(p53(Y)|p54(Y)))&(~p54(Y)|~p53(Y)))&(p52(Y)|p53(Y)))&(~p53(Y)|~p52(Y)))&(p51(Y)|p52(Y)))&(~p52(Y)|~p51(Y)))&(p50(Y)|p51(Y)))&(~p51(Y)|~p50(Y)))&(p49(Y)|p50(Y)))&(~p50(Y)|~p49(Y)))&(p48(Y)|p49(Y)))&(~p49(Y)|~p48(Y)))&(p47(Y)|p48(Y)))&(~p48(Y)|~p47(Y)))&(p46(Y)|p47(Y)))&(~p47(Y)|~p46(Y)))&(p45(Y)|p46(Y)))&(~p46(Y)|~p45(Y)))&(p44(Y)|p45(Y)))&(~p45(Y)|~p44(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.14/5.74    inference(miniscoping,[status(thm)],[f9])).
% 0.14/5.74  fof(f11,plain,(
% 0.14/5.74    (((r1(sK0_skl,sK1_skl)&p60(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))&((r1(sK46_skl(X),sK47_skl(X))&((r1(sK47_skl(X),sK48_skl(X))&((r1(sK48_skl(X),sK49_skl(X))&((r1(sK49_skl(X),sK50_skl(X))&((r1(sK50_skl(X),sK51_skl(X))&((r1(sK51_skl(X),sK52_skl(X))&((r1(sK52_skl(X),sK53_skl(X))&((r1(sK53_skl(X),sK54_skl(X))&((r1(sK54_skl(X),sK55_skl(X))&((r1(sK55_skl(X),sK56_skl(X))&((r1(sK56_skl(X),sK57_skl(X))&((r1(sK57_skl(X),sK58_skl(X))&((r1(sK58_skl(X),sK59_skl(X))&((r1(sK59_skl(X),sK60_skl(X))&(r1(sK60_skl(X),sK61_skl(X))&$true))&(![X]: (~r1(sK60_skl(X),X)|((~p59(X)|p58(X))&(p59(X)|~p58(X)))))))&(![Y]: (~r1(sK59_skl(X),Y)|((~p58(Y)|p57(Y))&(p58(Y)|~p57(Y)))))))&(![X]: (~r1(sK58_skl(X),X)|((~p57(X)|p56(X))&(p57(X)|~p56(X)))))))&(![Y]: (~r1(sK57_skl(X),Y)|((~p56(Y)|p55(Y))&(p56(Y)|~p55(Y)))))))&(![X]: (~r1(sK56_skl(X),X)|((~p55(X)|p54(X))&(p55(X)|~p54(X)))))))&(![Y]: (~r1(sK55_skl(X),Y)|((~p54(Y)|p53(Y))&(p54(Y)|~p53(Y)))))))&(![X]: (~r1(sK54_skl(X),X)|((~p53(X)|p52(X))&(p53(X)|~p52(X)))))))&(![Y]: (~r1(sK53_skl(X),Y)|((~p52(Y)|p51(Y))&(p52(Y)|~p51(Y)))))))&(![X]: (~r1(sK52_skl(X),X)|((~p51(X)|p50(X))&(p51(X)|~p50(X)))))))&(![Y]: (~r1(sK51_skl(X),Y)|((~p50(Y)|p49(Y))&(p50(Y)|~p49(Y)))))))&(![X]: (~r1(sK50_skl(X),X)|((~p49(X)|p48(X))&(p49(X)|~p48(X)))))))&(![Y]: (~r1(sK49_skl(X),Y)|((~p48(Y)|p47(Y))&(p48(Y)|~p47(Y)))))))&(![X]: (~r1(sK48_skl(X),X)|((~p47(X)|p46(X))&(p47(X)|~p46(X)))))))&(![Y]: (~r1(sK47_skl(X),Y)|((~p46(Y)|p45(Y))&(p46(Y)|~p45(Y)))))))&(![X]: (~r1(sK46_skl(X),X)|((~p45(X)|p44(X))&(p45(X)|~p44(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))))))&(r1(X,sK62_skl(X))&~p60(sK62_skl(X))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,sK63_skl(X))&(p58(sK63_skl(X))|p59(sK63_skl(X))))&(~p59(sK63_skl(X))|~p58(sK63_skl(X))))&(p57(sK63_skl(X))|p58(sK63_skl(X))))&(~p58(sK63_skl(X))|~p57(sK63_skl(X))))&(p56(sK63_skl(X))|p57(sK63_skl(X))))&(~p57(sK63_skl(X))|~p56(sK63_skl(X))))&(p55(sK63_skl(X))|p56(sK63_skl(X))))&(~p56(sK63_skl(X))|~p55(sK63_skl(X))))&(p54(sK63_skl(X))|p55(sK63_skl(X))))&(~p55(sK63_skl(X))|~p54(sK63_skl(X))))&(p53(sK63_skl(X))|p54(sK63_skl(X))))&(~p54(sK63_skl(X))|~p53(sK63_skl(X))))&(p52(sK63_skl(X))|p53(sK63_skl(X))))&(~p53(sK63_skl(X))|~p52(sK63_skl(X))))&(p51(sK63_skl(X))|p52(sK63_skl(X))))&(~p52(sK63_skl(X))|~p51(sK63_skl(X))))&(p50(sK63_skl(X))|p51(sK63_skl(X))))&(~p51(sK63_skl(X))|~p50(sK63_skl(X))))&(p49(sK63_skl(X))|p50(sK63_skl(X))))&(~p50(sK63_skl(X))|~p49(sK63_skl(X))))&(p48(sK63_skl(X))|p49(sK63_skl(X))))&(~p49(sK63_skl(X))|~p48(sK63_skl(X))))&(p47(sK63_skl(X))|p48(sK63_skl(X))))&(~p48(sK63_skl(X))|~p47(sK63_skl(X))))&(p46(sK63_skl(X))|p47(sK63_skl(X))))&(~p47(sK63_skl(X))|~p46(sK63_skl(X))))&(p45(sK63_skl(X))|p46(sK63_skl(X))))&(~p46(sK63_skl(X))|~p45(sK63_skl(X))))&(p44(sK63_skl(X))|p45(sK63_skl(X))))&(~p45(sK63_skl(X))|~p44(sK63_skl(X))))&(p43(sK63_skl(X))|p44(sK63_skl(X))))&(~p44(sK63_skl(X))|~p43(sK63_skl(X))))&(p42(sK63_skl(X))|p43(sK63_skl(X))))&(~p43(sK63_skl(X))|~p42(sK63_skl(X))))&(p41(sK63_skl(X))|p42(sK63_skl(X))))&(~p42(sK63_skl(X))|~p41(sK63_skl(X))))&(p40(sK63_skl(X))|p41(sK63_skl(X))))&(~p41(sK63_skl(X))|~p40(sK63_skl(X))))&(p39(sK63_skl(X))|p40(sK63_skl(X))))&(~p40(sK63_skl(X))|~p39(sK63_skl(X))))&(p38(sK63_skl(X))|p39(sK63_skl(X))))&(~p39(sK63_skl(X))|~p38(sK63_skl(X))))&(p37(sK63_skl(X))|p38(sK63_skl(X))))&(~p38(sK63_skl(X))|~p37(sK63_skl(X))))&(p36(sK63_skl(X))|p37(sK63_skl(X))))&(~p37(sK63_skl(X))|~p36(sK63_skl(X))))&(p35(sK63_skl(X))|p36(sK63_skl(X))))&(~p36(sK63_skl(X))|~p35(sK63_skl(X))))&(p34(sK63_skl(X))|p35(sK63_skl(X))))&(~p35(sK63_skl(X))|~p34(sK63_skl(X))))&(p33(sK63_skl(X))|p34(sK63_skl(X))))&(~p34(sK63_skl(X))|~p33(sK63_skl(X))))&(p32(sK63_skl(X))|p33(sK63_skl(X))))&(~p33(sK63_skl(X))|~p32(sK63_skl(X))))&(p31(sK63_skl(X))|p32(sK63_skl(X))))&(~p32(sK63_skl(X))|~p31(sK63_skl(X))))&(p30(sK63_skl(X))|p31(sK63_skl(X))))&(~p31(sK63_skl(X))|~p30(sK63_skl(X))))&(p29(sK63_skl(X))|p30(sK63_skl(X))))&(~p30(sK63_skl(X))|~p29(sK63_skl(X))))&(p28(sK63_skl(X))|p29(sK63_skl(X))))&(~p29(sK63_skl(X))|~p28(sK63_skl(X))))&(p27(sK63_skl(X))|p28(sK63_skl(X))))&(~p28(sK63_skl(X))|~p27(sK63_skl(X))))&(p26(sK63_skl(X))|p27(sK63_skl(X))))&(~p27(sK63_skl(X))|~p26(sK63_skl(X))))&(p25(sK63_skl(X))|p26(sK63_skl(X))))&(~p26(sK63_skl(X))|~p25(sK63_skl(X))))&(p24(sK63_skl(X))|p25(sK63_skl(X))))&(~p25(sK63_skl(X))|~p24(sK63_skl(X))))&(p23(sK63_skl(X))|p24(sK63_skl(X))))&(~p24(sK63_skl(X))|~p23(sK63_skl(X))))&(p22(sK63_skl(X))|p23(sK63_skl(X))))&(~p23(sK63_skl(X))|~p22(sK63_skl(X))))&(p21(sK63_skl(X))|p22(sK63_skl(X))))&(~p22(sK63_skl(X))|~p21(sK63_skl(X))))&(p20(sK63_skl(X))|p21(sK63_skl(X))))&(~p21(sK63_skl(X))|~p20(sK63_skl(X))))&(p19(sK63_skl(X))|p20(sK63_skl(X))))&(~p20(sK63_skl(X))|~p19(sK63_skl(X))))&(p18(sK63_skl(X))|p19(sK63_skl(X))))&(~p19(sK63_skl(X))|~p18(sK63_skl(X))))&(p17(sK63_skl(X))|p18(sK63_skl(X))))&(~p18(sK63_skl(X))|~p17(sK63_skl(X))))&(p16(sK63_skl(X))|p17(sK63_skl(X))))&(~p17(sK63_skl(X))|~p16(sK63_skl(X))))&(p15(sK63_skl(X))|p16(sK63_skl(X))))&(~p16(sK63_skl(X))|~p15(sK63_skl(X))))&(p14(sK63_skl(X))|p15(sK63_skl(X))))&(~p15(sK63_skl(X))|~p14(sK63_skl(X))))&(p13(sK63_skl(X))|p14(sK63_skl(X))))&(~p14(sK63_skl(X))|~p13(sK63_skl(X))))&(p12(sK63_skl(X))|p13(sK63_skl(X))))&(~p13(sK63_skl(X))|~p12(sK63_skl(X))))&(p11(sK63_skl(X))|p12(sK63_skl(X))))&(~p12(sK63_skl(X))|~p11(sK63_skl(X))))&(p10(sK63_skl(X))|p11(sK63_skl(X))))&(~p11(sK63_skl(X))|~p10(sK63_skl(X))))&(p9(sK63_skl(X))|p10(sK63_skl(X))))&(~p10(sK63_skl(X))|~p9(sK63_skl(X))))&(p8(sK63_skl(X))|p9(sK63_skl(X))))&(~p9(sK63_skl(X))|~p8(sK63_skl(X))))&(p7(sK63_skl(X))|p8(sK63_skl(X))))&(~p8(sK63_skl(X))|~p7(sK63_skl(X))))&(p6(sK63_skl(X))|p7(sK63_skl(X))))&(~p7(sK63_skl(X))|~p6(sK63_skl(X))))&(p5(sK63_skl(X))|p6(sK63_skl(X))))&(~p6(sK63_skl(X))|~p5(sK63_skl(X))))&(p4(sK63_skl(X))|p5(sK63_skl(X))))&(~p5(sK63_skl(X))|~p4(sK63_skl(X))))&(p3(sK63_skl(X))|p4(sK63_skl(X))))&(~p4(sK63_skl(X))|~p3(sK63_skl(X))))&(p2(sK63_skl(X))|p3(sK63_skl(X))))&(~p3(sK63_skl(X))|~p2(sK63_skl(X))))&(p1(sK63_skl(X))|p2(sK63_skl(X))))&(~p2(sK63_skl(X))|~p1(sK63_skl(X)))))))))),
% 0.14/5.74    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,sK49_skl,sK50_skl,sK51_skl,sK52_skl,sK53_skl,sK54_skl,sK55_skl,sK56_skl,sK57_skl,sK58_skl,sK59_skl,sK60_skl,sK61_skl,sK62_skl,sK63_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(X,sK47_skl(X)),skolemize(Y,sK48_skl(X)),skolemize(X,sK49_skl(X)),skolemize(Y,sK50_skl(X)),skolemize(X,sK51_skl(X)),skolemize(Y,sK52_skl(X)),skolemize(X,sK53_skl(X)),skolemize(Y,sK54_skl(X)),skolemize(X,sK55_skl(X)),skolemize(Y,sK56_skl(X)),skolemize(X,sK57_skl(X)),skolemize(Y,sK58_skl(X)),skolemize(X,sK59_skl(X)),skolemize(Y,sK60_skl(X)),skolemize(X,sK61_skl(X)),skolemize(Y,sK62_skl(X)),skolemize(Y,sK63_skl(X))],[f10])).
% 0.14/5.74  fof(f12,plain,(
% 0.14/5.74    ?[X]: ((?[Y]: ((r1(sK0_skl,sK1_skl)&p60(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))&(?[X]: ((r1(sK46_skl(X),sK47_skl(X))&(?[Y]: ((r1(sK47_skl(X),sK48_skl(X))&(?[X]: ((r1(sK48_skl(X),sK49_skl(X))&(?[Y]: ((r1(sK49_skl(X),sK50_skl(X))&(?[X]: ((r1(sK50_skl(X),sK51_skl(X))&(?[Y]: ((r1(sK51_skl(X),sK52_skl(X))&(?[X]: ((r1(sK52_skl(X),sK53_skl(X))&(?[Y]: ((r1(sK53_skl(X),sK54_skl(X))&(?[X]: ((r1(sK54_skl(X),sK55_skl(X))&(?[Y]: ((r1(sK55_skl(X),sK56_skl(X))&(?[X]: ((r1(sK56_skl(X),sK57_skl(X))&(?[Y]: ((r1(sK57_skl(X),sK58_skl(X))&(?[X]: ((r1(sK58_skl(X),sK59_skl(X))&(?[Y]: ((r1(sK59_skl(X),sK60_skl(X))&(?[X]: r1(sK60_skl(X),sK61_skl(X))))&(![X]: (~r1(sK60_skl(X),X)|((~p59(X)|p58(X))&(p59(X)|~p58(X))))))))&(![Y]: (~r1(sK59_skl(X),Y)|((~p58(Y)|p57(Y))&(p58(Y)|~p57(Y))))))))&(![X]: (~r1(sK58_skl(X),X)|((~p57(X)|p56(X))&(p57(X)|~p56(X))))))))&(![Y]: (~r1(sK57_skl(X),Y)|((~p56(Y)|p55(Y))&(p56(Y)|~p55(Y))))))))&(![X]: (~r1(sK56_skl(X),X)|((~p55(X)|p54(X))&(p55(X)|~p54(X))))))))&(![Y]: (~r1(sK55_skl(X),Y)|((~p54(Y)|p53(Y))&(p54(Y)|~p53(Y))))))))&(![X]: (~r1(sK54_skl(X),X)|((~p53(X)|p52(X))&(p53(X)|~p52(X))))))))&(![Y]: (~r1(sK53_skl(X),Y)|((~p52(Y)|p51(Y))&(p52(Y)|~p51(Y))))))))&(![X]: (~r1(sK52_skl(X),X)|((~p51(X)|p50(X))&(p51(X)|~p50(X))))))))&(![Y]: (~r1(sK51_skl(X),Y)|((~p50(Y)|p49(Y))&(p50(Y)|~p49(Y))))))))&(![X]: (~r1(sK50_skl(X),X)|((~p49(X)|p48(X))&(p49(X)|~p48(X))))))))&(![Y]: (~r1(sK49_skl(X),Y)|((~p48(Y)|p47(Y))&(p48(Y)|~p47(Y))))))))&(![X]: (~r1(sK48_skl(X),X)|((~p47(X)|p46(X))&(p47(X)|~p46(X))))))))&(![Y]: (~r1(sK47_skl(X),Y)|((~p46(Y)|p45(Y))&(p46(Y)|~p45(Y))))))))&(![X]: (~r1(sK46_skl(X),X)|((~p45(X)|p44(X))&(p45(X)|~p44(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,sK62_skl(X))&~p60(sK62_skl(X)))))&(?[Y]: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X,sK63_skl(X))&(p58(sK63_skl(X))|p59(sK63_skl(X))))&(~p59(sK63_skl(X))|~p58(sK63_skl(X))))&(p57(sK63_skl(X))|p58(sK63_skl(X))))&(~p58(sK63_skl(X))|~p57(sK63_skl(X))))&(p56(sK63_skl(X))|p57(sK63_skl(X))))&(~p57(sK63_skl(X))|~p56(sK63_skl(X))))&(p55(sK63_skl(X))|p56(sK63_skl(X))))&(~p56(sK63_skl(X))|~p55(sK63_skl(X))))&(p54(sK63_skl(X))|p55(sK63_skl(X))))&(~p55(sK63_skl(X))|~p54(sK63_skl(X))))&(p53(sK63_skl(X))|p54(sK63_skl(X))))&(~p54(sK63_skl(X))|~p53(sK63_skl(X))))&(p52(sK63_skl(X))|p53(sK63_skl(X))))&(~p53(sK63_skl(X))|~p52(sK63_skl(X))))&(p51(sK63_skl(X))|p52(sK63_skl(X))))&(~p52(sK63_skl(X))|~p51(sK63_skl(X))))&(p50(sK63_skl(X))|p51(sK63_skl(X))))&(~p51(sK63_skl(X))|~p50(sK63_skl(X))))&(p49(sK63_skl(X))|p50(sK63_skl(X))))&(~p50(sK63_skl(X))|~p49(sK63_skl(X))))&(p48(sK63_skl(X))|p49(sK63_skl(X))))&(~p49(sK63_skl(X))|~p48(sK63_skl(X))))&(p47(sK63_skl(X))|p48(sK63_skl(X))))&(~p48(sK63_skl(X))|~p47(sK63_skl(X))))&(p46(sK63_skl(X))|p47(sK63_skl(X))))&(~p47(sK63_skl(X))|~p46(sK63_skl(X))))&(p45(sK63_skl(X))|p46(sK63_skl(X))))&(~p46(sK63_skl(X))|~p45(sK63_skl(X))))&(p44(sK63_skl(X))|p45(sK63_skl(X))))&(~p45(sK63_skl(X))|~p44(sK63_skl(X))))&(p43(sK63_skl(X))|p44(sK63_skl(X))))&(~p44(sK63_skl(X))|~p43(sK63_skl(X))))&(p42(sK63_skl(X))|p43(sK63_skl(X))))&(~p43(sK63_skl(X))|~p42(sK63_skl(X))))&(p41(sK63_skl(X))|p42(sK63_skl(X))))&(~p42(sK63_skl(X))|~p41(sK63_skl(X))))&(p40(sK63_skl(X))|p41(sK63_skl(X))))&(~p41(sK63_skl(X))|~p40(sK63_skl(X))))&(p39(sK63_skl(X))|p40(sK63_skl(X))))&(~p40(sK63_skl(X))|~p39(sK63_skl(X))))&(p38(sK63_skl(X))|p39(sK63_skl(X))))&(~p39(sK63_skl(X))|~p38(sK63_skl(X))))&(p37(sK63_skl(X))|p38(sK63_skl(X))))&(~p38(sK63_skl(X))|~p37(sK63_skl(X))))&(p36(sK63_skl(X))|p37(sK63_skl(X))))&(~p37(sK63_skl(X))|~p36(sK63_skl(X))))&(p35(sK63_skl(X))|p36(sK63_skl(X))))&(~p36(sK63_skl(X))|~p35(sK63_skl(X))))&(p34(sK63_skl(X))|p35(sK63_skl(X))))&(~p35(sK63_skl(X))|~p34(sK63_skl(X))))&(p33(sK63_skl(X))|p34(sK63_skl(X))))&(~p34(sK63_skl(X))|~p33(sK63_skl(X))))&(p32(sK63_skl(X))|p33(sK63_skl(X))))&(~p33(sK63_skl(X))|~p32(sK63_skl(X))))&(p31(sK63_skl(X))|p32(sK63_skl(X))))&(~p32(sK63_skl(X))|~p31(sK63_skl(X))))&(p30(sK63_skl(X))|p31(sK63_skl(X))))&(~p31(sK63_skl(X))|~p30(sK63_skl(X))))&(p29(sK63_skl(X))|p30(sK63_skl(X))))&(~p30(sK63_skl(X))|~p29(sK63_skl(X))))&(p28(sK63_skl(X))|p29(sK63_skl(X))))&(~p29(sK63_skl(X))|~p28(sK63_skl(X))))&(p27(sK63_skl(X))|p28(sK63_skl(X))))&(~p28(sK63_skl(X))|~p27(sK63_skl(X))))&(p26(sK63_skl(X))|p27(sK63_skl(X))))&(~p27(sK63_skl(X))|~p26(sK63_skl(X))))&(p25(sK63_skl(X))|p26(sK63_skl(X))))&(~p26(sK63_skl(X))|~p25(sK63_skl(X))))&(p24(sK63_skl(X))|p25(sK63_skl(X))))&(~p25(sK63_skl(X))|~p24(sK63_skl(X))))&(p23(sK63_skl(X))|p24(sK63_skl(X))))&(~p24(sK63_skl(X))|~p23(sK63_skl(X))))&(p22(sK63_skl(X))|p23(sK63_skl(X))))&(~p23(sK63_skl(X))|~p22(sK63_skl(X))))&(p21(sK63_skl(X))|p22(sK63_skl(X))))&(~p22(sK63_skl(X))|~p21(sK63_skl(X))))&(p20(sK63_skl(X))|p21(sK63_skl(X))))&(~p21(sK63_skl(X))|~p20(sK63_skl(X))))&(p19(sK63_skl(X))|p20(sK63_skl(X))))&(~p20(sK63_skl(X))|~p19(sK63_skl(X))))&(p18(sK63_skl(X))|p19(sK63_skl(X))))&(~p19(sK63_skl(X))|~p18(sK63_skl(X))))&(p17(sK63_skl(X))|p18(sK63_skl(X))))&(~p18(sK63_skl(X))|~p17(sK63_skl(X))))&(p16(sK63_skl(X))|p17(sK63_skl(X))))&(~p17(sK63_skl(X))|~p16(sK63_skl(X))))&(p15(sK63_skl(X))|p16(sK63_skl(X))))&(~p16(sK63_skl(X))|~p15(sK63_skl(X))))&(p14(sK63_skl(X))|p15(sK63_skl(X))))&(~p15(sK63_skl(X))|~p14(sK63_skl(X))))&(p13(sK63_skl(X))|p14(sK63_skl(X))))&(~p14(sK63_skl(X))|~p13(sK63_skl(X))))&(p12(sK63_skl(X))|p13(sK63_skl(X))))&(~p13(sK63_skl(X))|~p12(sK63_skl(X))))&(p11(sK63_skl(X))|p12(sK63_skl(X))))&(~p12(sK63_skl(X))|~p11(sK63_skl(X))))&(p10(sK63_skl(X))|p11(sK63_skl(X))))&(~p11(sK63_skl(X))|~p10(sK63_skl(X))))&(p9(sK63_skl(X))|p10(sK63_skl(X))))&(~p10(sK63_skl(X))|~p9(sK63_skl(X))))&(p8(sK63_skl(X))|p9(sK63_skl(X))))&(~p9(sK63_skl(X))|~p8(sK63_skl(X))))&(p7(sK63_skl(X))|p8(sK63_skl(X))))&(~p8(sK63_skl(X))|~p7(sK63_skl(X))))&(p6(sK63_skl(X))|p7(sK63_skl(X))))&(~p7(sK63_skl(X))|~p6(sK63_skl(X))))&(p5(sK63_skl(X))|p6(sK63_skl(X))))&(~p6(sK63_skl(X))|~p5(sK63_skl(X))))&(p4(sK63_skl(X))|p5(sK63_skl(X))))&(~p5(sK63_skl(X))|~p4(sK63_skl(X))))&(p3(sK63_skl(X))|p4(sK63_skl(X))))&(~p4(sK63_skl(X))|~p3(sK63_skl(X))))&(p2(sK63_skl(X))|p3(sK63_skl(X))))&(~p3(sK63_skl(X))|~p2(sK63_skl(X))))&(p1(sK63_skl(X))|p2(sK63_skl(X))))&(~p2(sK63_skl(X))|~p1(sK63_skl(X)))))))))))),
% 0.14/5.74    inference(true_and_false_simplification,[status(thm)],[f11])).
% 0.14/5.74  fof(f18,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|r1(X0,sK4_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f190,plain,(
% 0.14/5.74    ![X0,X1]: (~r1(sK3_skl,X0)|~r1(X0,X1)|~p2(X1)|p1(X1))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f191,plain,(
% 0.14/5.74    ![X0,X1]: (~r1(sK3_skl,X0)|~r1(X0,X1)|p2(X1)|~p1(X1))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f194,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|r1(X0,sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f195,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p58(sK63_skl(X0))|p59(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f196,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p59(sK63_skl(X0))|~p58(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f197,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p57(sK63_skl(X0))|p58(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f198,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p58(sK63_skl(X0))|~p57(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f199,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p56(sK63_skl(X0))|p57(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f200,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p57(sK63_skl(X0))|~p56(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f201,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p55(sK63_skl(X0))|p56(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f203,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p54(sK63_skl(X0))|p55(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f204,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p55(sK63_skl(X0))|~p54(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f205,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p53(sK63_skl(X0))|p54(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f207,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p52(sK63_skl(X0))|p53(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f208,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p53(sK63_skl(X0))|~p52(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f209,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p51(sK63_skl(X0))|p52(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f211,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p50(sK63_skl(X0))|p51(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f212,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p51(sK63_skl(X0))|~p50(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f213,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p49(sK63_skl(X0))|p50(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f215,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p48(sK63_skl(X0))|p49(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f216,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p49(sK63_skl(X0))|~p48(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f217,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p47(sK63_skl(X0))|p48(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f219,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p46(sK63_skl(X0))|p47(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f220,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p47(sK63_skl(X0))|~p46(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f221,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p45(sK63_skl(X0))|p46(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f223,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p44(sK63_skl(X0))|p45(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f224,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p45(sK63_skl(X0))|~p44(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f225,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p43(sK63_skl(X0))|p44(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f227,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p42(sK63_skl(X0))|p43(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f228,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p43(sK63_skl(X0))|~p42(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f229,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p41(sK63_skl(X0))|p42(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f231,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p40(sK63_skl(X0))|p41(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f232,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p41(sK63_skl(X0))|~p40(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f233,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p39(sK63_skl(X0))|p40(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f235,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p38(sK63_skl(X0))|p39(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f236,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p39(sK63_skl(X0))|~p38(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f237,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p37(sK63_skl(X0))|p38(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f239,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p36(sK63_skl(X0))|p37(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f240,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p37(sK63_skl(X0))|~p36(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f241,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p35(sK63_skl(X0))|p36(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f243,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p34(sK63_skl(X0))|p35(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f244,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p35(sK63_skl(X0))|~p34(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f245,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p33(sK63_skl(X0))|p34(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f247,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p32(sK63_skl(X0))|p33(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f248,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p33(sK63_skl(X0))|~p32(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f249,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p31(sK63_skl(X0))|p32(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f251,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p30(sK63_skl(X0))|p31(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f252,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p31(sK63_skl(X0))|~p30(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f253,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p29(sK63_skl(X0))|p30(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f255,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p28(sK63_skl(X0))|p29(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f256,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p29(sK63_skl(X0))|~p28(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f257,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p27(sK63_skl(X0))|p28(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f259,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p26(sK63_skl(X0))|p27(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f260,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p27(sK63_skl(X0))|~p26(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f261,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p25(sK63_skl(X0))|p26(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f263,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p24(sK63_skl(X0))|p25(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f264,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p25(sK63_skl(X0))|~p24(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f265,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p23(sK63_skl(X0))|p24(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f267,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p22(sK63_skl(X0))|p23(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f268,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p23(sK63_skl(X0))|~p22(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f269,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p21(sK63_skl(X0))|p22(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f271,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p20(sK63_skl(X0))|p21(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f272,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p21(sK63_skl(X0))|~p20(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f273,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p19(sK63_skl(X0))|p20(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f275,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p18(sK63_skl(X0))|p19(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f276,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p19(sK63_skl(X0))|~p18(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f277,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p17(sK63_skl(X0))|p18(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f279,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p16(sK63_skl(X0))|p17(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f280,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p17(sK63_skl(X0))|~p16(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f281,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p15(sK63_skl(X0))|p16(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f283,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p14(sK63_skl(X0))|p15(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f284,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p15(sK63_skl(X0))|~p14(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f285,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p13(sK63_skl(X0))|p14(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f287,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p12(sK63_skl(X0))|p13(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f288,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p13(sK63_skl(X0))|~p12(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f289,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p11(sK63_skl(X0))|p12(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f291,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p10(sK63_skl(X0))|p11(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f292,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p11(sK63_skl(X0))|~p10(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f293,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p9(sK63_skl(X0))|p10(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f295,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p8(sK63_skl(X0))|p9(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f296,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|~p9(sK63_skl(X0))|~p8(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f297,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p7(sK63_skl(X0))|p8(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.74  fof(f299,plain,(
% 0.14/5.74    ![X0]: (~r1(sK3_skl,X0)|p6(sK63_skl(X0))|p7(sK63_skl(X0)))),
% 0.14/5.74    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.75  fof(f300,plain,(
% 0.14/5.75    ![X0]: (~r1(sK3_skl,X0)|~p7(sK63_skl(X0))|~p6(sK63_skl(X0)))),
% 0.14/5.75    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.75  fof(f301,plain,(
% 0.14/5.75    ![X0]: (~r1(sK3_skl,X0)|p5(sK63_skl(X0))|p6(sK63_skl(X0)))),
% 0.14/5.75    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.75  fof(f303,plain,(
% 0.14/5.75    ![X0]: (~r1(sK3_skl,X0)|p4(sK63_skl(X0))|p5(sK63_skl(X0)))),
% 0.14/5.75    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.75  fof(f304,plain,(
% 0.14/5.75    ![X0]: (~r1(sK3_skl,X0)|~p5(sK63_skl(X0))|~p4(sK63_skl(X0)))),
% 0.14/5.75    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.75  fof(f305,plain,(
% 0.14/5.75    ![X0]: (~r1(sK3_skl,X0)|p3(sK63_skl(X0))|p4(sK63_skl(X0)))),
% 0.14/5.75    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.75  fof(f307,plain,(
% 0.14/5.75    ![X0]: (~r1(sK3_skl,X0)|p2(sK63_skl(X0))|p3(sK63_skl(X0)))),
% 0.14/5.75    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.75  fof(f308,plain,(
% 0.14/5.75    ![X0]: (~r1(sK3_skl,X0)|~p3(sK63_skl(X0))|~p2(sK63_skl(X0)))),
% 0.14/5.75    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.75  fof(f309,plain,(
% 0.14/5.75    ![X0]: (~r1(sK3_skl,X0)|p1(sK63_skl(X0))|p2(sK63_skl(X0)))),
% 0.14/5.75    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.75  fof(f310,plain,(
% 0.14/5.75    ![X0]: (~r1(sK3_skl,X0)|~p2(sK63_skl(X0))|~p1(sK63_skl(X0)))),
% 0.14/5.75    inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.75  fof(f315,plain,(
% 0.14/5.75    r1(sK3_skl,sK4_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f18,f5])).
% 0.14/5.75  fof(f334,plain,(
% 0.14/5.75    p58(sK63_skl(sK3_skl))|p59(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f195,f5])).
% 0.14/5.75  fof(f342,definition,(
% 0.14/5.75    sQ2_spl <=> (p58(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f343,plain,(
% 0.14/5.75    p58(sK63_skl(sK3_skl))|~sQ2_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f342])).
% 0.14/5.75  fof(f345,definition,(
% 0.14/5.75    sQ3_spl <=> (p59(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f348,plain,(
% 0.14/5.75    sQ2_spl|sQ3_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f334,f342,f345])).
% 0.14/5.75  fof(f350,plain,(
% 0.14/5.75    p57(sK63_skl(sK3_skl))|p58(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f197,f5])).
% 0.14/5.75  fof(f355,definition,(
% 0.14/5.75    sQ5_spl <=> (p57(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f356,plain,(
% 0.14/5.75    p57(sK63_skl(sK3_skl))|~sQ5_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f355])).
% 0.14/5.75  fof(f358,plain,(
% 0.14/5.75    sQ5_spl|sQ2_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f350,f355,f342])).
% 0.14/5.75  fof(f360,plain,(
% 0.14/5.75    p56(sK63_skl(sK3_skl))|p57(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f199,f5])).
% 0.14/5.75  fof(f365,definition,(
% 0.14/5.75    sQ7_spl <=> (p56(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f366,plain,(
% 0.14/5.75    p56(sK63_skl(sK3_skl))|~sQ7_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f365])).
% 0.14/5.75  fof(f368,plain,(
% 0.14/5.75    sQ7_spl|sQ5_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f360,f365,f355])).
% 0.14/5.75  fof(f370,plain,(
% 0.14/5.75    p55(sK63_skl(sK3_skl))|p56(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f201,f5])).
% 0.14/5.75  fof(f375,definition,(
% 0.14/5.75    sQ9_spl <=> (p55(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f378,plain,(
% 0.14/5.75    sQ9_spl|sQ7_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f370,f375,f365])).
% 0.14/5.75  fof(f380,plain,(
% 0.14/5.75    p54(sK63_skl(sK3_skl))|p55(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f203,f5])).
% 0.14/5.75  fof(f385,definition,(
% 0.14/5.75    sQ11_spl <=> (p54(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f386,plain,(
% 0.14/5.75    p54(sK63_skl(sK3_skl))|~sQ11_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f385])).
% 0.14/5.75  fof(f388,plain,(
% 0.14/5.75    sQ11_spl|sQ9_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f380,f385,f375])).
% 0.14/5.75  fof(f390,plain,(
% 0.14/5.75    p53(sK63_skl(sK3_skl))|p54(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f205,f5])).
% 0.14/5.75  fof(f395,definition,(
% 0.14/5.75    sQ13_spl <=> (p53(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f398,plain,(
% 0.14/5.75    sQ13_spl|sQ11_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f390,f395,f385])).
% 0.14/5.75  fof(f400,plain,(
% 0.14/5.75    p52(sK63_skl(sK3_skl))|p53(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f207,f5])).
% 0.14/5.75  fof(f405,definition,(
% 0.14/5.75    sQ15_spl <=> (p52(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f406,plain,(
% 0.14/5.75    p52(sK63_skl(sK3_skl))|~sQ15_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f405])).
% 0.14/5.75  fof(f408,plain,(
% 0.14/5.75    sQ15_spl|sQ13_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f400,f405,f395])).
% 0.14/5.75  fof(f410,plain,(
% 0.14/5.75    p51(sK63_skl(sK3_skl))|p52(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f209,f5])).
% 0.14/5.75  fof(f415,definition,(
% 0.14/5.75    sQ17_spl <=> (p51(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f418,plain,(
% 0.14/5.75    sQ17_spl|sQ15_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f410,f415,f405])).
% 0.14/5.75  fof(f420,plain,(
% 0.14/5.75    p50(sK63_skl(sK3_skl))|p51(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f211,f5])).
% 0.14/5.75  fof(f425,definition,(
% 0.14/5.75    sQ19_spl <=> (p50(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f426,plain,(
% 0.14/5.75    p50(sK63_skl(sK3_skl))|~sQ19_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f425])).
% 0.14/5.75  fof(f428,plain,(
% 0.14/5.75    sQ19_spl|sQ17_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f420,f425,f415])).
% 0.14/5.75  fof(f430,plain,(
% 0.14/5.75    p49(sK63_skl(sK3_skl))|p50(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f213,f5])).
% 0.14/5.75  fof(f435,definition,(
% 0.14/5.75    sQ21_spl <=> (p49(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f438,plain,(
% 0.14/5.75    sQ21_spl|sQ19_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f430,f435,f425])).
% 0.14/5.75  fof(f440,plain,(
% 0.14/5.75    p48(sK63_skl(sK3_skl))|p49(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f215,f5])).
% 0.14/5.75  fof(f445,definition,(
% 0.14/5.75    sQ23_spl <=> (p48(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f446,plain,(
% 0.14/5.75    p48(sK63_skl(sK3_skl))|~sQ23_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f445])).
% 0.14/5.75  fof(f448,plain,(
% 0.14/5.75    sQ23_spl|sQ21_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f440,f445,f435])).
% 0.14/5.75  fof(f450,plain,(
% 0.14/5.75    p47(sK63_skl(sK3_skl))|p48(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f217,f5])).
% 0.14/5.75  fof(f455,definition,(
% 0.14/5.75    sQ25_spl <=> (p47(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f458,plain,(
% 0.14/5.75    sQ25_spl|sQ23_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f450,f455,f445])).
% 0.14/5.75  fof(f460,plain,(
% 0.14/5.75    p46(sK63_skl(sK3_skl))|p47(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f219,f5])).
% 0.14/5.75  fof(f465,definition,(
% 0.14/5.75    sQ27_spl <=> (p46(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f466,plain,(
% 0.14/5.75    p46(sK63_skl(sK3_skl))|~sQ27_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f465])).
% 0.14/5.75  fof(f468,plain,(
% 0.14/5.75    sQ27_spl|sQ25_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f460,f465,f455])).
% 0.14/5.75  fof(f470,plain,(
% 0.14/5.75    p45(sK63_skl(sK3_skl))|p46(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f221,f5])).
% 0.14/5.75  fof(f475,definition,(
% 0.14/5.75    sQ29_spl <=> (p45(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f478,plain,(
% 0.14/5.75    sQ29_spl|sQ27_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f470,f475,f465])).
% 0.14/5.75  fof(f480,plain,(
% 0.14/5.75    p44(sK63_skl(sK3_skl))|p45(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f223,f5])).
% 0.14/5.75  fof(f485,definition,(
% 0.14/5.75    sQ31_spl <=> (p44(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f486,plain,(
% 0.14/5.75    p44(sK63_skl(sK3_skl))|~sQ31_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f485])).
% 0.14/5.75  fof(f488,plain,(
% 0.14/5.75    sQ31_spl|sQ29_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f480,f485,f475])).
% 0.14/5.75  fof(f490,plain,(
% 0.14/5.75    p43(sK63_skl(sK3_skl))|p44(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f225,f5])).
% 0.14/5.75  fof(f495,definition,(
% 0.14/5.75    sQ33_spl <=> (p43(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f498,plain,(
% 0.14/5.75    sQ33_spl|sQ31_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f490,f495,f485])).
% 0.14/5.75  fof(f500,plain,(
% 0.14/5.75    p42(sK63_skl(sK3_skl))|p43(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f227,f5])).
% 0.14/5.75  fof(f505,definition,(
% 0.14/5.75    sQ35_spl <=> (p42(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f506,plain,(
% 0.14/5.75    p42(sK63_skl(sK3_skl))|~sQ35_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f505])).
% 0.14/5.75  fof(f508,plain,(
% 0.14/5.75    sQ35_spl|sQ33_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f500,f505,f495])).
% 0.14/5.75  fof(f510,plain,(
% 0.14/5.75    p41(sK63_skl(sK3_skl))|p42(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f229,f5])).
% 0.14/5.75  fof(f515,definition,(
% 0.14/5.75    sQ37_spl <=> (p41(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f518,plain,(
% 0.14/5.75    sQ37_spl|sQ35_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f510,f515,f505])).
% 0.14/5.75  fof(f520,plain,(
% 0.14/5.75    p40(sK63_skl(sK3_skl))|p41(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f231,f5])).
% 0.14/5.75  fof(f525,definition,(
% 0.14/5.75    sQ39_spl <=> (p40(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f526,plain,(
% 0.14/5.75    p40(sK63_skl(sK3_skl))|~sQ39_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f525])).
% 0.14/5.75  fof(f528,plain,(
% 0.14/5.75    sQ39_spl|sQ37_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f520,f525,f515])).
% 0.14/5.75  fof(f530,plain,(
% 0.14/5.75    p39(sK63_skl(sK3_skl))|p40(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f233,f5])).
% 0.14/5.75  fof(f535,definition,(
% 0.14/5.75    sQ41_spl <=> (p39(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f538,plain,(
% 0.14/5.75    sQ41_spl|sQ39_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f530,f535,f525])).
% 0.14/5.75  fof(f540,plain,(
% 0.14/5.75    p38(sK63_skl(sK3_skl))|p39(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f235,f5])).
% 0.14/5.75  fof(f545,definition,(
% 0.14/5.75    sQ43_spl <=> (p38(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f546,plain,(
% 0.14/5.75    p38(sK63_skl(sK3_skl))|~sQ43_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f545])).
% 0.14/5.75  fof(f548,plain,(
% 0.14/5.75    sQ43_spl|sQ41_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f540,f545,f535])).
% 0.14/5.75  fof(f550,plain,(
% 0.14/5.75    p37(sK63_skl(sK3_skl))|p38(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f237,f5])).
% 0.14/5.75  fof(f555,definition,(
% 0.14/5.75    sQ45_spl <=> (p37(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f558,plain,(
% 0.14/5.75    sQ45_spl|sQ43_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f550,f555,f545])).
% 0.14/5.75  fof(f560,plain,(
% 0.14/5.75    p36(sK63_skl(sK3_skl))|p37(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f239,f5])).
% 0.14/5.75  fof(f565,definition,(
% 0.14/5.75    sQ47_spl <=> (p36(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f566,plain,(
% 0.14/5.75    p36(sK63_skl(sK3_skl))|~sQ47_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f565])).
% 0.14/5.75  fof(f568,plain,(
% 0.14/5.75    sQ47_spl|sQ45_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f560,f565,f555])).
% 0.14/5.75  fof(f570,plain,(
% 0.14/5.75    p35(sK63_skl(sK3_skl))|p36(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f241,f5])).
% 0.14/5.75  fof(f575,definition,(
% 0.14/5.75    sQ49_spl <=> (p35(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f578,plain,(
% 0.14/5.75    sQ49_spl|sQ47_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f570,f575,f565])).
% 0.14/5.75  fof(f580,plain,(
% 0.14/5.75    p34(sK63_skl(sK3_skl))|p35(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f243,f5])).
% 0.14/5.75  fof(f585,definition,(
% 0.14/5.75    sQ51_spl <=> (p34(sK63_skl(sK3_skl)))),
% 0.14/5.75    introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.14/5.75  fof(f586,plain,(
% 0.14/5.75    p34(sK63_skl(sK3_skl))|~sQ51_spl),
% 0.14/5.75    inference(component_clause,[status(thm)],[f585])).
% 0.14/5.75  fof(f588,plain,(
% 0.14/5.75    sQ51_spl|sQ49_spl),
% 0.14/5.75    inference(split_clause,[status(thm)],[f580,f585,f575])).
% 0.14/5.75  fof(f590,plain,(
% 0.14/5.75    p33(sK63_skl(sK3_skl))|p34(sK63_skl(sK3_skl))),
% 0.14/5.75    inference(resolution,[status(thm)],[f245,f5])).
% 0.14/5.76  fof(f595,definition,(
% 0.14/5.76    sQ53_spl <=> (p33(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f598,plain,(
% 0.14/5.76    sQ53_spl|sQ51_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f590,f595,f585])).
% 0.14/5.76  fof(f600,plain,(
% 0.14/5.76    p32(sK63_skl(sK3_skl))|p33(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f247,f5])).
% 0.14/5.76  fof(f605,definition,(
% 0.14/5.76    sQ55_spl <=> (p32(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f606,plain,(
% 0.14/5.76    p32(sK63_skl(sK3_skl))|~sQ55_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f605])).
% 0.14/5.76  fof(f608,plain,(
% 0.14/5.76    sQ55_spl|sQ53_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f600,f605,f595])).
% 0.14/5.76  fof(f610,plain,(
% 0.14/5.76    p31(sK63_skl(sK3_skl))|p32(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f249,f5])).
% 0.14/5.76  fof(f615,definition,(
% 0.14/5.76    sQ57_spl <=> (p31(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f618,plain,(
% 0.14/5.76    sQ57_spl|sQ55_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f610,f615,f605])).
% 0.14/5.76  fof(f620,plain,(
% 0.14/5.76    p30(sK63_skl(sK3_skl))|p31(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f251,f5])).
% 0.14/5.76  fof(f625,definition,(
% 0.14/5.76    sQ59_spl <=> (p30(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f626,plain,(
% 0.14/5.76    p30(sK63_skl(sK3_skl))|~sQ59_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f625])).
% 0.14/5.76  fof(f628,plain,(
% 0.14/5.76    sQ59_spl|sQ57_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f620,f625,f615])).
% 0.14/5.76  fof(f630,plain,(
% 0.14/5.76    p29(sK63_skl(sK3_skl))|p30(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f253,f5])).
% 0.14/5.76  fof(f635,definition,(
% 0.14/5.76    sQ61_spl <=> (p29(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f638,plain,(
% 0.14/5.76    sQ61_spl|sQ59_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f630,f635,f625])).
% 0.14/5.76  fof(f640,plain,(
% 0.14/5.76    p28(sK63_skl(sK3_skl))|p29(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f255,f5])).
% 0.14/5.76  fof(f645,definition,(
% 0.14/5.76    sQ63_spl <=> (p28(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f646,plain,(
% 0.14/5.76    p28(sK63_skl(sK3_skl))|~sQ63_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f645])).
% 0.14/5.76  fof(f648,plain,(
% 0.14/5.76    sQ63_spl|sQ61_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f640,f645,f635])).
% 0.14/5.76  fof(f650,plain,(
% 0.14/5.76    p27(sK63_skl(sK3_skl))|p28(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f257,f5])).
% 0.14/5.76  fof(f655,definition,(
% 0.14/5.76    sQ65_spl <=> (p27(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f658,plain,(
% 0.14/5.76    sQ65_spl|sQ63_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f650,f655,f645])).
% 0.14/5.76  fof(f660,plain,(
% 0.14/5.76    p26(sK63_skl(sK3_skl))|p27(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f259,f5])).
% 0.14/5.76  fof(f665,definition,(
% 0.14/5.76    sQ67_spl <=> (p26(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f666,plain,(
% 0.14/5.76    p26(sK63_skl(sK3_skl))|~sQ67_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f665])).
% 0.14/5.76  fof(f668,plain,(
% 0.14/5.76    sQ67_spl|sQ65_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f660,f665,f655])).
% 0.14/5.76  fof(f670,plain,(
% 0.14/5.76    p25(sK63_skl(sK3_skl))|p26(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f261,f5])).
% 0.14/5.76  fof(f675,definition,(
% 0.14/5.76    sQ69_spl <=> (p25(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f678,plain,(
% 0.14/5.76    sQ69_spl|sQ67_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f670,f675,f665])).
% 0.14/5.76  fof(f680,plain,(
% 0.14/5.76    p24(sK63_skl(sK3_skl))|p25(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f263,f5])).
% 0.14/5.76  fof(f685,definition,(
% 0.14/5.76    sQ71_spl <=> (p24(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f686,plain,(
% 0.14/5.76    p24(sK63_skl(sK3_skl))|~sQ71_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f685])).
% 0.14/5.76  fof(f688,plain,(
% 0.14/5.76    sQ71_spl|sQ69_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f680,f685,f675])).
% 0.14/5.76  fof(f690,plain,(
% 0.14/5.76    p23(sK63_skl(sK3_skl))|p24(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f265,f5])).
% 0.14/5.76  fof(f695,definition,(
% 0.14/5.76    sQ73_spl <=> (p23(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f698,plain,(
% 0.14/5.76    sQ73_spl|sQ71_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f690,f695,f685])).
% 0.14/5.76  fof(f700,plain,(
% 0.14/5.76    p22(sK63_skl(sK3_skl))|p23(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f267,f5])).
% 0.14/5.76  fof(f705,definition,(
% 0.14/5.76    sQ75_spl <=> (p22(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f706,plain,(
% 0.14/5.76    p22(sK63_skl(sK3_skl))|~sQ75_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f705])).
% 0.14/5.76  fof(f708,plain,(
% 0.14/5.76    sQ75_spl|sQ73_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f700,f705,f695])).
% 0.14/5.76  fof(f710,plain,(
% 0.14/5.76    p21(sK63_skl(sK3_skl))|p22(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f269,f5])).
% 0.14/5.76  fof(f715,definition,(
% 0.14/5.76    sQ77_spl <=> (p21(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f718,plain,(
% 0.14/5.76    sQ77_spl|sQ75_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f710,f715,f705])).
% 0.14/5.76  fof(f720,plain,(
% 0.14/5.76    p20(sK63_skl(sK3_skl))|p21(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f271,f5])).
% 0.14/5.76  fof(f725,definition,(
% 0.14/5.76    sQ79_spl <=> (p20(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f726,plain,(
% 0.14/5.76    p20(sK63_skl(sK3_skl))|~sQ79_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f725])).
% 0.14/5.76  fof(f728,plain,(
% 0.14/5.76    sQ79_spl|sQ77_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f720,f725,f715])).
% 0.14/5.76  fof(f730,plain,(
% 0.14/5.76    p19(sK63_skl(sK3_skl))|p20(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f273,f5])).
% 0.14/5.76  fof(f735,definition,(
% 0.14/5.76    sQ81_spl <=> (p19(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f738,plain,(
% 0.14/5.76    sQ81_spl|sQ79_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f730,f735,f725])).
% 0.14/5.76  fof(f740,plain,(
% 0.14/5.76    p18(sK63_skl(sK3_skl))|p19(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f275,f5])).
% 0.14/5.76  fof(f745,definition,(
% 0.14/5.76    sQ83_spl <=> (p18(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f746,plain,(
% 0.14/5.76    p18(sK63_skl(sK3_skl))|~sQ83_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f745])).
% 0.14/5.76  fof(f748,plain,(
% 0.14/5.76    sQ83_spl|sQ81_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f740,f745,f735])).
% 0.14/5.76  fof(f750,plain,(
% 0.14/5.76    p17(sK63_skl(sK3_skl))|p18(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f277,f5])).
% 0.14/5.76  fof(f755,definition,(
% 0.14/5.76    sQ85_spl <=> (p17(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f758,plain,(
% 0.14/5.76    sQ85_spl|sQ83_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f750,f755,f745])).
% 0.14/5.76  fof(f760,plain,(
% 0.14/5.76    p16(sK63_skl(sK3_skl))|p17(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f279,f5])).
% 0.14/5.76  fof(f765,definition,(
% 0.14/5.76    sQ87_spl <=> (p16(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f766,plain,(
% 0.14/5.76    p16(sK63_skl(sK3_skl))|~sQ87_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f765])).
% 0.14/5.76  fof(f768,plain,(
% 0.14/5.76    sQ87_spl|sQ85_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f760,f765,f755])).
% 0.14/5.76  fof(f770,plain,(
% 0.14/5.76    p15(sK63_skl(sK3_skl))|p16(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f281,f5])).
% 0.14/5.76  fof(f775,definition,(
% 0.14/5.76    sQ89_spl <=> (p15(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f778,plain,(
% 0.14/5.76    sQ89_spl|sQ87_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f770,f775,f765])).
% 0.14/5.76  fof(f780,plain,(
% 0.14/5.76    p14(sK63_skl(sK3_skl))|p15(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f283,f5])).
% 0.14/5.76  fof(f785,definition,(
% 0.14/5.76    sQ91_spl <=> (p14(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f786,plain,(
% 0.14/5.76    p14(sK63_skl(sK3_skl))|~sQ91_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f785])).
% 0.14/5.76  fof(f788,plain,(
% 0.14/5.76    sQ91_spl|sQ89_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f780,f785,f775])).
% 0.14/5.76  fof(f790,plain,(
% 0.14/5.76    p13(sK63_skl(sK3_skl))|p14(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f285,f5])).
% 0.14/5.76  fof(f795,definition,(
% 0.14/5.76    sQ93_spl <=> (p13(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f798,plain,(
% 0.14/5.76    sQ93_spl|sQ91_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f790,f795,f785])).
% 0.14/5.76  fof(f800,plain,(
% 0.14/5.76    p12(sK63_skl(sK3_skl))|p13(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f287,f5])).
% 0.14/5.76  fof(f805,definition,(
% 0.14/5.76    sQ95_spl <=> (p12(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f806,plain,(
% 0.14/5.76    p12(sK63_skl(sK3_skl))|~sQ95_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f805])).
% 0.14/5.76  fof(f808,plain,(
% 0.14/5.76    sQ95_spl|sQ93_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f800,f805,f795])).
% 0.14/5.76  fof(f810,plain,(
% 0.14/5.76    p11(sK63_skl(sK3_skl))|p12(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f289,f5])).
% 0.14/5.76  fof(f815,definition,(
% 0.14/5.76    sQ97_spl <=> (p11(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f818,plain,(
% 0.14/5.76    sQ97_spl|sQ95_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f810,f815,f805])).
% 0.14/5.76  fof(f820,plain,(
% 0.14/5.76    p10(sK63_skl(sK3_skl))|p11(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f291,f5])).
% 0.14/5.76  fof(f825,definition,(
% 0.14/5.76    sQ99_spl <=> (p10(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f826,plain,(
% 0.14/5.76    p10(sK63_skl(sK3_skl))|~sQ99_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f825])).
% 0.14/5.76  fof(f828,plain,(
% 0.14/5.76    sQ99_spl|sQ97_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f820,f825,f815])).
% 0.14/5.76  fof(f830,plain,(
% 0.14/5.76    p9(sK63_skl(sK3_skl))|p10(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f293,f5])).
% 0.14/5.76  fof(f835,definition,(
% 0.14/5.76    sQ101_spl <=> (p9(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f838,plain,(
% 0.14/5.76    sQ101_spl|sQ99_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f830,f835,f825])).
% 0.14/5.76  fof(f840,plain,(
% 0.14/5.76    p8(sK63_skl(sK3_skl))|p9(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f295,f5])).
% 0.14/5.76  fof(f845,definition,(
% 0.14/5.76    sQ103_spl <=> (p8(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f846,plain,(
% 0.14/5.76    p8(sK63_skl(sK3_skl))|~sQ103_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f845])).
% 0.14/5.76  fof(f848,plain,(
% 0.14/5.76    sQ103_spl|sQ101_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f840,f845,f835])).
% 0.14/5.76  fof(f850,plain,(
% 0.14/5.76    p7(sK63_skl(sK3_skl))|p8(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f297,f5])).
% 0.14/5.76  fof(f855,definition,(
% 0.14/5.76    sQ105_spl <=> (p7(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f858,plain,(
% 0.14/5.76    sQ105_spl|sQ103_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f850,f855,f845])).
% 0.14/5.76  fof(f860,plain,(
% 0.14/5.76    p6(sK63_skl(sK3_skl))|p7(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f299,f5])).
% 0.14/5.76  fof(f865,definition,(
% 0.14/5.76    sQ107_spl <=> (p6(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f866,plain,(
% 0.14/5.76    p6(sK63_skl(sK3_skl))|~sQ107_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f865])).
% 0.14/5.76  fof(f868,plain,(
% 0.14/5.76    sQ107_spl|sQ105_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f860,f865,f855])).
% 0.14/5.76  fof(f870,plain,(
% 0.14/5.76    p5(sK63_skl(sK3_skl))|p6(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f301,f5])).
% 0.14/5.76  fof(f875,definition,(
% 0.14/5.76    sQ109_spl <=> (p5(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f878,plain,(
% 0.14/5.76    sQ109_spl|sQ107_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f870,f875,f865])).
% 0.14/5.76  fof(f880,plain,(
% 0.14/5.76    p4(sK63_skl(sK3_skl))|p5(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f303,f5])).
% 0.14/5.76  fof(f885,definition,(
% 0.14/5.76    sQ111_spl <=> (p4(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f886,plain,(
% 0.14/5.76    p4(sK63_skl(sK3_skl))|~sQ111_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f885])).
% 0.14/5.76  fof(f888,plain,(
% 0.14/5.76    sQ111_spl|sQ109_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f880,f885,f875])).
% 0.14/5.76  fof(f890,plain,(
% 0.14/5.76    p3(sK63_skl(sK3_skl))|p4(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f305,f5])).
% 0.14/5.76  fof(f895,definition,(
% 0.14/5.76    sQ113_spl <=> (p3(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f898,plain,(
% 0.14/5.76    sQ113_spl|sQ111_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f890,f895,f885])).
% 0.14/5.76  fof(f900,plain,(
% 0.14/5.76    p2(sK63_skl(sK3_skl))|p3(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f307,f5])).
% 0.14/5.76  fof(f905,definition,(
% 0.14/5.76    sQ115_spl <=> (p2(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f906,plain,(
% 0.14/5.76    p2(sK63_skl(sK3_skl))|~sQ115_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f905])).
% 0.14/5.76  fof(f908,plain,(
% 0.14/5.76    sQ115_spl|sQ113_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f900,f905,f895])).
% 0.14/5.76  fof(f910,plain,(
% 0.14/5.76    p1(sK63_skl(sK3_skl))|p2(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f309,f5])).
% 0.14/5.76  fof(f915,definition,(
% 0.14/5.76    sQ117_spl <=> (p1(sK63_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f918,plain,(
% 0.14/5.76    sQ117_spl|sQ115_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f910,f915,f905])).
% 0.14/5.76  fof(f1134,plain,(
% 0.14/5.76    ![X0]: (~r1(sK3_skl,X0)|~p2(X0)|p1(X0))),
% 0.14/5.76    inference(resolution,[status(thm)],[f190,f5])).
% 0.14/5.76  fof(f1136,plain,(
% 0.14/5.76    ![X0]: (~r1(sK3_skl,X0)|p2(X0)|~p1(X0))),
% 0.14/5.76    inference(resolution,[status(thm)],[f191,f5])).
% 0.14/5.76  fof(f1140,plain,(
% 0.14/5.76    r1(sK3_skl,sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f194,f5])).
% 0.14/5.76  fof(f1142,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p59(sK63_skl(sK3_skl))|~sQ2_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f196,f343])).
% 0.14/5.76  fof(f1143,definition,(
% 0.14/5.76    sQ118_spl <=> (r1(sK3_skl,sK4_skl(sK3_skl)))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f1145,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK4_skl(sK3_skl))|sQ118_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f1143])).
% 0.14/5.76  fof(f1147,definition,(
% 0.14/5.76    sQ119_spl <=> (r1(sK3_skl,sK3_skl))),
% 0.14/5.76    introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.14/5.76  fof(f1149,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|sQ119_spl),
% 0.14/5.76    inference(component_clause,[status(thm)],[f1147])).
% 0.14/5.76  fof(f1150,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ3_spl|~sQ2_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1142,f1147,f345,f342])).
% 0.14/5.76  fof(f1151,plain,(
% 0.14/5.76    $false|sQ119_spl),
% 0.14/5.76    inference(forward_subsumption_resolution,[status(thm)],[f1149,f5])).
% 0.14/5.76  fof(f1152,plain,(
% 0.14/5.76    sQ119_spl),
% 0.14/5.76    inference(contradiction_clause,[status(thm)],[f1151])).
% 0.14/5.76  fof(f1153,plain,(
% 0.14/5.76    $false|sQ118_spl),
% 0.14/5.76    inference(forward_subsumption_resolution,[status(thm)],[f1145,f315])).
% 0.14/5.76  fof(f1154,plain,(
% 0.14/5.76    sQ118_spl),
% 0.14/5.76    inference(contradiction_clause,[status(thm)],[f1153])).
% 0.14/5.76  fof(f1156,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p58(sK63_skl(sK3_skl))|~sQ5_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f198,f356])).
% 0.14/5.76  fof(f1158,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ2_spl|~sQ5_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1156,f1147,f342,f355])).
% 0.14/5.76  fof(f1161,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p57(sK63_skl(sK3_skl))|~sQ7_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f200,f366])).
% 0.14/5.76  fof(f1162,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ5_spl|~sQ7_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1161,f1147,f355,f365])).
% 0.14/5.76  fof(f1164,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p55(sK63_skl(sK3_skl))|~sQ11_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f204,f386])).
% 0.14/5.76  fof(f1166,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ9_spl|~sQ11_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1164,f1147,f375,f385])).
% 0.14/5.76  fof(f1168,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p53(sK63_skl(sK3_skl))|~sQ15_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f208,f406])).
% 0.14/5.76  fof(f1170,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ13_spl|~sQ15_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1168,f1147,f395,f405])).
% 0.14/5.76  fof(f1172,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p51(sK63_skl(sK3_skl))|~sQ19_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f212,f426])).
% 0.14/5.76  fof(f1174,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ17_spl|~sQ19_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1172,f1147,f415,f425])).
% 0.14/5.76  fof(f1176,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p49(sK63_skl(sK3_skl))|~sQ23_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f216,f446])).
% 0.14/5.76  fof(f1178,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ21_spl|~sQ23_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1176,f1147,f435,f445])).
% 0.14/5.76  fof(f1180,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p47(sK63_skl(sK3_skl))|~sQ27_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f220,f466])).
% 0.14/5.76  fof(f1182,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ25_spl|~sQ27_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1180,f1147,f455,f465])).
% 0.14/5.76  fof(f1184,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p45(sK63_skl(sK3_skl))|~sQ31_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f224,f486])).
% 0.14/5.76  fof(f1186,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ29_spl|~sQ31_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1184,f1147,f475,f485])).
% 0.14/5.76  fof(f1188,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p43(sK63_skl(sK3_skl))|~sQ35_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f228,f506])).
% 0.14/5.76  fof(f1190,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ33_spl|~sQ35_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1188,f1147,f495,f505])).
% 0.14/5.76  fof(f1192,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p41(sK63_skl(sK3_skl))|~sQ39_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f232,f526])).
% 0.14/5.76  fof(f1194,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ37_spl|~sQ39_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1192,f1147,f515,f525])).
% 0.14/5.76  fof(f1196,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p39(sK63_skl(sK3_skl))|~sQ43_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f236,f546])).
% 0.14/5.76  fof(f1198,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ41_spl|~sQ43_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1196,f1147,f535,f545])).
% 0.14/5.76  fof(f1200,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p37(sK63_skl(sK3_skl))|~sQ47_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f240,f566])).
% 0.14/5.76  fof(f1202,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ45_spl|~sQ47_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1200,f1147,f555,f565])).
% 0.14/5.76  fof(f1204,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p35(sK63_skl(sK3_skl))|~sQ51_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f244,f586])).
% 0.14/5.76  fof(f1206,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ49_spl|~sQ51_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1204,f1147,f575,f585])).
% 0.14/5.76  fof(f1208,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p33(sK63_skl(sK3_skl))|~sQ55_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f248,f606])).
% 0.14/5.76  fof(f1210,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ53_spl|~sQ55_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1208,f1147,f595,f605])).
% 0.14/5.76  fof(f1212,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p31(sK63_skl(sK3_skl))|~sQ59_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f252,f626])).
% 0.14/5.76  fof(f1214,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ57_spl|~sQ59_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1212,f1147,f615,f625])).
% 0.14/5.76  fof(f1215,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p29(sK63_skl(sK3_skl))|~sQ63_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f256,f646])).
% 0.14/5.76  fof(f1216,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ61_spl|~sQ63_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1215,f1147,f635,f645])).
% 0.14/5.76  fof(f1217,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p27(sK63_skl(sK3_skl))|~sQ67_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f260,f666])).
% 0.14/5.76  fof(f1218,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ65_spl|~sQ67_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1217,f1147,f655,f665])).
% 0.14/5.76  fof(f1219,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p25(sK63_skl(sK3_skl))|~sQ71_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f264,f686])).
% 0.14/5.76  fof(f1220,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ69_spl|~sQ71_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1219,f1147,f675,f685])).
% 0.14/5.76  fof(f1221,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p23(sK63_skl(sK3_skl))|~sQ75_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f268,f706])).
% 0.14/5.76  fof(f1222,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ73_spl|~sQ75_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1221,f1147,f695,f705])).
% 0.14/5.76  fof(f1223,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p21(sK63_skl(sK3_skl))|~sQ79_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f272,f726])).
% 0.14/5.76  fof(f1224,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ77_spl|~sQ79_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1223,f1147,f715,f725])).
% 0.14/5.76  fof(f1225,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p19(sK63_skl(sK3_skl))|~sQ83_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f276,f746])).
% 0.14/5.76  fof(f1226,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ81_spl|~sQ83_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1225,f1147,f735,f745])).
% 0.14/5.76  fof(f1227,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p17(sK63_skl(sK3_skl))|~sQ87_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f280,f766])).
% 0.14/5.76  fof(f1228,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ85_spl|~sQ87_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1227,f1147,f755,f765])).
% 0.14/5.76  fof(f1229,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p15(sK63_skl(sK3_skl))|~sQ91_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f284,f786])).
% 0.14/5.76  fof(f1230,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ89_spl|~sQ91_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1229,f1147,f775,f785])).
% 0.14/5.76  fof(f1231,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p13(sK63_skl(sK3_skl))|~sQ95_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f288,f806])).
% 0.14/5.76  fof(f1232,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ93_spl|~sQ95_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1231,f1147,f795,f805])).
% 0.14/5.76  fof(f1233,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p11(sK63_skl(sK3_skl))|~sQ99_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f292,f826])).
% 0.14/5.76  fof(f1234,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ97_spl|~sQ99_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1233,f1147,f815,f825])).
% 0.14/5.76  fof(f1235,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p9(sK63_skl(sK3_skl))|~sQ103_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f296,f846])).
% 0.14/5.76  fof(f1236,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ101_spl|~sQ103_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1235,f1147,f835,f845])).
% 0.14/5.76  fof(f1237,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p7(sK63_skl(sK3_skl))|~sQ107_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f300,f866])).
% 0.14/5.76  fof(f1238,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ105_spl|~sQ107_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1237,f1147,f855,f865])).
% 0.14/5.76  fof(f1239,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p5(sK63_skl(sK3_skl))|~sQ111_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f304,f886])).
% 0.14/5.76  fof(f1240,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ109_spl|~sQ111_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1239,f1147,f875,f885])).
% 0.14/5.76  fof(f1241,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p3(sK63_skl(sK3_skl))|~sQ115_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f308,f906])).
% 0.14/5.76  fof(f1242,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ113_spl|~sQ115_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1241,f1147,f895,f905])).
% 0.14/5.76  fof(f1243,plain,(
% 0.14/5.76    ~r1(sK3_skl,sK3_skl)|~p1(sK63_skl(sK3_skl))|~sQ115_spl),
% 0.14/5.76    inference(resolution,[status(thm)],[f310,f906])).
% 0.14/5.76  fof(f1244,plain,(
% 0.14/5.76    ~sQ119_spl|~sQ117_spl|~sQ115_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f1243,f1147,f915,f905])).
% 0.14/5.76  fof(f2464,plain,(
% 0.14/5.76    p2(sK63_skl(sK3_skl))|~p1(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f1140,f1136])).
% 0.14/5.76  fof(f2465,plain,(
% 0.14/5.76    ~p2(sK63_skl(sK3_skl))|p1(sK63_skl(sK3_skl))),
% 0.14/5.76    inference(resolution,[status(thm)],[f1140,f1134])).
% 0.14/5.76  fof(f2588,plain,(
% 0.14/5.76    sQ115_spl|~sQ117_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f2464,f905,f915])).
% 0.14/5.76  fof(f2589,plain,(
% 0.14/5.76    ~sQ115_spl|sQ117_spl),
% 0.14/5.76    inference(split_clause,[status(thm)],[f2465,f905,f915])).
% 0.14/5.76  fof(f2825,plain,(
% 0.14/5.76    $false),
% 0.14/5.76    inference(sat_refutation,[status(thm)],[f348,f358,f368,f378,f388,f398,f408,f418,f428,f438,f448,f458,f468,f478,f488,f498,f508,f518,f528,f538,f548,f558,f568,f578,f588,f598,f608,f618,f628,f638,f648,f658,f668,f678,f688,f698,f708,f718,f728,f738,f748,f758,f768,f778,f788,f798,f808,f818,f828,f838,f848,f858,f868,f878,f888,f898,f908,f918,f1150,f1152,f1154,f1158,f1162,f1166,f1170,f1174,f1178,f1182,f1186,f1190,f1194,f1198,f1202,f1206,f1210,f1214,f1216,f1218,f1220,f1222,f1224,f1226,f1228,f1230,f1232,f1234,f1236,f1238,f1240,f1242,f1244,f2588,f2589])).
% 0.14/5.76  % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.78  % Elapsed time: 0.397159 seconds
% 0.14/5.78  % CPU time: 2.806292 seconds
% 0.14/5.78  % Total memory used: 50.552 MB
% 0.14/5.78  % Net memory used: 48.837 MB
%------------------------------------------------------------------------------