%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL664+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : 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:43 PM UTC 2026
% Result : Theorem 138.10s 22.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL664+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/5.37 % Computer : n001.cluster.edu
% 0.08/5.37 % Model : x86_64 x86_64
% 0.08/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.37 % Memory : 8046.5625MB
% 0.08/5.37 % OS : Linux 6.8.0-71-generic
% 0.08/5.37 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Mon Sep 21 00:56:04 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.08/5.39 % Drodi V4.1.1
% 138.10/22.91 % Refutation found
% 138.10/22.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 138.10/22.91 % SZS output start CNFRefutation for theBenchmark
% 138.10/22.91 fof(f2,conjecture,(
% 138.10/22.91 ~ (? [X] :~ ( ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p56(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p54(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p54(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p52(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p56(Y) ))& ~ p46(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p56(Y) ))& ~ p44(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p56(Y) ))& ~ p42(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p54(Y) ))& ~ p46(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p54(Y) ))& ~ p44(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p54(Y) ))& ~ p42(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p52(Y) ))& ~ p46(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p52(Y) ))& ~ p44(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p52(Y) ))& ~ p42(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p46(X) ))& ~ p36(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p46(X) ))& ~ p32(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p55(Y) ))& ~ p45(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p53(Y) ))& ~ p45(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p51(Y) ))& ~ p45(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p44(X) ))& ~ p36(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p44(X) ))& ~ p32(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p55(Y) ))& ~ p43(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p53(Y) ))& ~ p43(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p51(Y) ))& ~ p43(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p42(X) ))& ~ p36(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p42(X) ))& ~ p32(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p55(Y) ))& ~ p41(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p54(Y) ))& ~ p41(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p53(Y) ))& ~ p41(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p51(Y) ))& ~ p41(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p36(Y) ))& ~ p26(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p36(Y) ))& ~ p24(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p36(Y) ))& ~ p22(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p45(X) ))& ~ p35(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p43(X) ))& ~ p35(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p34(Y) ))& ~ p26(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p34(Y) ))& ~ p24(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p34(Y) ))& ~ p22(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p41(X) ))& ~ p34(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p45(X) ))& ~ p33(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p43(X) ))& ~ p33(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p32(Y) ))& ~ p26(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p32(Y) ))& ~ p24(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p32(Y) ))& ~ p22(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p45(X) ))& ~ p31(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p43(X) ))& ~ p31(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p26(X) ))& ~ p16(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p26(X) ))& ~ p14(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p35(Y) ))& ~ p25(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p33(Y) ))& ~ p25(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p31(Y) ))& ~ p25(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p24(X) ))& ~ p16(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p24(X) ))& ~ p14(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p35(Y) ))& ~ p23(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p33(Y) ))& ~ p23(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p31(Y) ))& ~ p23(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p22(X) ))& ~ p16(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p22(X) ))& ~ p14(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p35(Y) ))& ~ p21(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p34(Y) ))& ~ p21(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p33(Y) ))& ~ p21(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p31(Y) ))& ~ p21(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p25(X) ))& ~ p15(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p23(X) ))& ~ p15(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p25(X) ))& ~ p13(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p23(X) ))& ~ p13(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p21(X) ))& ~ p12(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p25(X) ))& ~ p11(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p23(X) ))& ~ p11(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p15(Y) ))| (! [Y] :( ~ r1(X,Y)| p13(Y) ))| (! [Y] :( ~ r1(X,Y)| p12(Y) ))| (! [Y] :( ~ r1(X,Y)| p11(Y) ) )) )),
% 138.94/22.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.94/22.92 fof(f3,negated_conjecture,(
% 138.94/22.92 ~(~ (? [X] :~ ( ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p56(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p54(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p54(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p52(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p56(Y) ))& ~ p46(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p56(Y) ))& ~ p44(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p56(Y) ))& ~ p42(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p54(Y) ))& ~ p46(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p54(Y) ))& ~ p44(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p54(Y) ))& ~ p42(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p52(Y) ))& ~ p46(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p52(Y) ))& ~ p44(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p52(Y) ))& ~ p42(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p46(X) ))& ~ p36(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p46(X) ))& ~ p32(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p55(Y) ))& ~ p45(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p53(Y) ))& ~ p45(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p51(Y) ))& ~ p45(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p44(X) ))& ~ p36(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p44(X) ))& ~ p32(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p55(Y) ))& ~ p43(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p53(Y) ))& ~ p43(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p51(Y) ))& ~ p43(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p42(X) ))& ~ p36(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p42(X) ))& ~ p32(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p55(Y) ))& ~ p41(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p54(Y) ))& ~ p41(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p53(Y) ))& ~ p41(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p51(Y) ))& ~ p41(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p36(Y) ))& ~ p26(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p36(Y) ))& ~ p24(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p36(Y) ))& ~ p22(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p45(X) ))& ~ p35(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p43(X) ))& ~ p35(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p34(Y) ))& ~ p26(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p34(Y) ))& ~ p24(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p34(Y) ))& ~ p22(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p41(X) ))& ~ p34(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p45(X) ))& ~ p33(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p43(X) ))& ~ p33(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p32(Y) ))& ~ p26(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p32(Y) ))& ~ p24(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p32(Y) ))& ~ p22(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p45(X) ))& ~ p31(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p43(X) ))& ~ p31(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p26(X) ))& ~ p16(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p26(X) ))& ~ p14(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p35(Y) ))& ~ p25(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p33(Y) ))& ~ p25(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p31(Y) ))& ~ p25(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p24(X) ))& ~ p16(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p24(X) ))& ~ p14(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p35(Y) ))& ~ p23(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p33(Y) ))& ~ p23(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p31(Y) ))& ~ p23(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p22(X) ))& ~ p16(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p22(X) ))& ~ p14(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p35(Y) ))& ~ p21(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p34(Y) ))& ~ p21(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p33(Y) ))& ~ p21(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p31(Y) ))& ~ p21(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p25(X) ))& ~ p15(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p23(X) ))& ~ p15(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p25(X) ))& ~ p13(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p23(X) ))& ~ p13(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p21(X) ))& ~ p12(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p25(X) ))& ~ p11(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p23(X) ))& ~ p11(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p15(Y) ))| (! [Y] :( ~ r1(X,Y)| p13(Y) ))| (! [Y] :( ~ r1(X,Y)| p12(Y) ))| (! [Y] :( ~ r1(X,Y)| p11(Y) ) )) ))),
% 138.94/22.92 inference(negated_conjecture,[status(cth)],[f2])).
% 138.94/22.92 fof(f5,plain,(
% 138.94/22.92 ?[X]: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p56(Y)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p54(Y))))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p54(Y))))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p52(Y))))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p56(Y)))|p46(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p56(Y)))|p44(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p56(Y)))|p42(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p54(Y)))|p46(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p54(Y)))|p44(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p54(Y)))|p42(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p52(Y)))|p46(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p52(Y)))|p44(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p52(Y)))|p42(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p46(X)))|p36(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p46(X)))|p32(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p55(Y)))|p45(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p53(Y)))|p45(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p51(Y)))|p45(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p44(X)))|p36(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p44(X)))|p32(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p55(Y)))|p43(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p53(Y)))|p43(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p51(Y)))|p43(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p42(X)))|p36(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p42(X)))|p32(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p55(Y)))|p41(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p54(Y)))|p41(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p53(Y)))|p41(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p51(Y)))|p41(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p36(Y)))|p26(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p36(Y)))|p24(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p36(Y)))|p22(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p45(X)))|p35(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p43(X)))|p35(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p34(Y)))|p26(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p34(Y)))|p24(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p34(Y)))|p22(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p41(X)))|p34(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p45(X)))|p33(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p43(X)))|p33(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p32(Y)))|p26(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p32(Y)))|p24(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p32(Y)))|p22(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p45(X)))|p31(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p43(X)))|p31(Y)))))))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p26(X)))|p16(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p26(X)))|p14(Y)))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p35(Y)))|p25(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p33(Y)))|p25(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p31(Y)))|p25(X)))))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p24(X)))|p16(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p24(X)))|p14(Y)))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p35(Y)))|p23(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p33(Y)))|p23(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p31(Y)))|p23(X)))))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p22(X)))|p16(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p22(X)))|p14(Y)))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p35(Y)))|p21(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p34(Y)))|p21(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p33(Y)))|p21(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p31(Y)))|p21(X)))))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p25(X)))|p15(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p23(X)))|p15(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p25(X)))|p13(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p23(X)))|p13(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p21(X)))|p12(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p25(X)))|p11(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p23(X)))|p11(Y)))))&(?[Y]: (r1(X,Y)&~p15(Y))))&(?[Y]: (r1(X,Y)&~p13(Y))))&(?[Y]: (r1(X,Y)&~p12(Y))))&(?[Y]: (r1(X,Y)&~p11(Y))))),
% 138.94/22.92 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 138.94/22.92 fof(f6,plain,(
% 138.94/22.92 ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p56(Y)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p54(Y))))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p54(Y))))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p52(Y))))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK1_skl(X,Y,X,Y))&~p56(sK1_skl(X,Y,X,Y)))|p46(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK2_skl(X,Y,X,Y))&~p56(sK2_skl(X,Y,X,Y)))|p44(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK3_skl(X,Y,X,Y))&~p56(sK3_skl(X,Y,X,Y)))|p42(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK4_skl(X,Y,X,Y))&~p54(sK4_skl(X,Y,X,Y)))|p46(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK5_skl(X,Y,X,Y))&~p54(sK5_skl(X,Y,X,Y)))|p44(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK6_skl(X,Y,X,Y))&~p54(sK6_skl(X,Y,X,Y)))|p42(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK7_skl(X,Y,X,Y))&~p52(sK7_skl(X,Y,X,Y)))|p46(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK8_skl(X,Y,X,Y))&~p52(sK8_skl(X,Y,X,Y)))|p44(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK9_skl(X,Y,X,Y))&~p52(sK9_skl(X,Y,X,Y)))|p42(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK10_skl(Y,X,Y))&~p46(sK10_skl(Y,X,Y)))|p36(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK11_skl(Y,X,Y))&~p46(sK11_skl(Y,X,Y)))|p32(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK12_skl(X,Y,X,Y))&~p55(sK12_skl(X,Y,X,Y)))|p45(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK13_skl(X,Y,X,Y))&~p53(sK13_skl(X,Y,X,Y)))|p45(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK14_skl(X,Y,X,Y))&~p51(sK14_skl(X,Y,X,Y)))|p45(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK15_skl(Y,X,Y))&~p44(sK15_skl(Y,X,Y)))|p36(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK16_skl(Y,X,Y))&~p44(sK16_skl(Y,X,Y)))|p32(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK17_skl(X,Y,X,Y))&~p55(sK17_skl(X,Y,X,Y)))|p43(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK18_skl(X,Y,X,Y))&~p53(sK18_skl(X,Y,X,Y)))|p43(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK19_skl(X,Y,X,Y))&~p51(sK19_skl(X,Y,X,Y)))|p43(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK20_skl(Y,X,Y))&~p42(sK20_skl(Y,X,Y)))|p36(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK21_skl(Y,X,Y))&~p42(sK21_skl(Y,X,Y)))|p32(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK22_skl(X,Y,X,Y))&~p55(sK22_skl(X,Y,X,Y)))|p41(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK23_skl(X,Y,X,Y))&~p54(sK23_skl(X,Y,X,Y)))|p41(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK24_skl(X,Y,X,Y))&~p53(sK24_skl(X,Y,X,Y)))|p41(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((r1(X,sK25_skl(X,Y,X,Y))&~p51(sK25_skl(X,Y,X,Y)))|p41(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK26_skl(X,Y))&~p36(sK26_skl(X,Y)))|p26(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK27_skl(X,Y))&~p36(sK27_skl(X,Y)))|p24(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK28_skl(X,Y))&~p36(sK28_skl(X,Y)))|p22(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK29_skl(Y,X,Y))&~p45(sK29_skl(Y,X,Y)))|p35(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK30_skl(Y,X,Y))&~p43(sK30_skl(Y,X,Y)))|p35(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK31_skl(X,Y))&~p34(sK31_skl(X,Y)))|p26(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK32_skl(X,Y))&~p34(sK32_skl(X,Y)))|p24(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK33_skl(X,Y))&~p34(sK33_skl(X,Y)))|p22(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK34_skl(Y,X,Y))&~p41(sK34_skl(Y,X,Y)))|p34(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK35_skl(Y,X,Y))&~p45(sK35_skl(Y,X,Y)))|p33(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK36_skl(Y,X,Y))&~p43(sK36_skl(Y,X,Y)))|p33(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK37_skl(X,Y))&~p32(sK37_skl(X,Y)))|p26(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK38_skl(X,Y))&~p32(sK38_skl(X,Y)))|p24(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK39_skl(X,Y))&~p32(sK39_skl(X,Y)))|p22(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK40_skl(Y,X,Y))&~p45(sK40_skl(Y,X,Y)))|p31(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK41_skl(Y,X,Y))&~p43(sK41_skl(Y,X,Y)))|p31(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK42_skl(Y))&~p26(sK42_skl(Y)))|p16(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK43_skl(Y))&~p26(sK43_skl(Y)))|p14(Y)))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK44_skl(X,Y))&~p35(sK44_skl(X,Y)))|p25(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK45_skl(X,Y))&~p33(sK45_skl(X,Y)))|p25(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK46_skl(X,Y))&~p31(sK46_skl(X,Y)))|p25(X)))))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK47_skl(Y))&~p24(sK47_skl(Y)))|p16(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK48_skl(Y))&~p24(sK48_skl(Y)))|p14(Y)))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK49_skl(X,Y))&~p35(sK49_skl(X,Y)))|p23(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK50_skl(X,Y))&~p33(sK50_skl(X,Y)))|p23(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK51_skl(X,Y))&~p31(sK51_skl(X,Y)))|p23(X)))))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK52_skl(Y))&~p22(sK52_skl(Y)))|p16(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK53_skl(Y))&~p22(sK53_skl(Y)))|p14(Y)))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK54_skl(X,Y))&~p35(sK54_skl(X,Y)))|p21(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK55_skl(X,Y))&~p34(sK55_skl(X,Y)))|p21(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK56_skl(X,Y))&~p33(sK56_skl(X,Y)))|p21(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK57_skl(X,Y))&~p31(sK57_skl(X,Y)))|p21(X)))))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK58_skl(Y))&~p25(sK58_skl(Y)))|p15(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK59_skl(Y))&~p23(sK59_skl(Y)))|p15(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK60_skl(Y))&~p25(sK60_skl(Y)))|p13(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK61_skl(Y))&~p23(sK61_skl(Y)))|p13(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK62_skl(Y))&~p21(sK62_skl(Y)))|p12(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK63_skl(Y))&~p25(sK63_skl(Y)))|p11(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK64_skl(Y))&~p23(sK64_skl(Y)))|p11(Y)))))&(r1(sK0_skl,sK65_skl)&~p15(sK65_skl)))&(r1(sK0_skl,sK66_skl)&~p13(sK66_skl)))&(r1(sK0_skl,sK67_skl)&~p12(sK67_skl)))&(r1(sK0_skl,sK68_skl)&~p11(sK68_skl)))),
% 138.94/22.92 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,sK64_skl,sK65_skl,sK66_skl,sK67_skl,sK68_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl(X,Y,X,Y)),skolemize(Y,sK2_skl(X,Y,X,Y)),skolemize(Y,sK3_skl(X,Y,X,Y)),skolemize(Y,sK4_skl(X,Y,X,Y)),skolemize(Y,sK5_skl(X,Y,X,Y)),skolemize(Y,sK6_skl(X,Y,X,Y)),skolemize(Y,sK7_skl(X,Y,X,Y)),skolemize(Y,sK8_skl(X,Y,X,Y)),skolemize(Y,sK9_skl(X,Y,X,Y)),skolemize(X,sK10_skl(Y,X,Y)),skolemize(X,sK11_skl(Y,X,Y)),skolemize(Y,sK12_skl(X,Y,X,Y)),skolemize(Y,sK13_skl(X,Y,X,Y)),skolemize(Y,sK14_skl(X,Y,X,Y)),skolemize(X,sK15_skl(Y,X,Y)),skolemize(X,sK16_skl(Y,X,Y)),skolemize(Y,sK17_skl(X,Y,X,Y)),skolemize(Y,sK18_skl(X,Y,X,Y)),skolemize(Y,sK19_skl(X,Y,X,Y)),skolemize(X,sK20_skl(Y,X,Y)),skolemize(X,sK21_skl(Y,X,Y)),skolemize(Y,sK22_skl(X,Y,X,Y)),skolemize(Y,sK23_skl(X,Y,X,Y)),skolemize(Y,sK24_skl(X,Y,X,Y)),skolemize(Y,sK25_skl(X,Y,X,Y)),skolemize(Y,sK26_skl(X,Y)),skolemize(Y,sK27_skl(X,Y)),skolemize(Y,sK28_skl(X,Y)),skolemize(X,sK29_skl(Y,X,Y)),skolemize(X,sK30_skl(Y,X,Y)),skolemize(Y,sK31_skl(X,Y)),skolemize(Y,sK32_skl(X,Y)),skolemize(Y,sK33_skl(X,Y)),skolemize(X,sK34_skl(Y,X,Y)),skolemize(X,sK35_skl(Y,X,Y)),skolemize(X,sK36_skl(Y,X,Y)),skolemize(Y,sK37_skl(X,Y)),skolemize(Y,sK38_skl(X,Y)),skolemize(Y,sK39_skl(X,Y)),skolemize(X,sK40_skl(Y,X,Y)),skolemize(X,sK41_skl(Y,X,Y)),skolemize(X,sK42_skl(Y)),skolemize(X,sK43_skl(Y)),skolemize(Y,sK44_skl(X,Y)),skolemize(Y,sK45_skl(X,Y)),skolemize(Y,sK46_skl(X,Y)),skolemize(X,sK47_skl(Y)),skolemize(X,sK48_skl(Y)),skolemize(Y,sK49_skl(X,Y)),skolemize(Y,sK50_skl(X,Y)),skolemize(Y,sK51_skl(X,Y)),skolemize(X,sK52_skl(Y)),skolemize(X,sK53_skl(Y)),skolemize(Y,sK54_skl(X,Y)),skolemize(Y,sK55_skl(X,Y)),skolemize(Y,sK56_skl(X,Y)),skolemize(Y,sK57_skl(X,Y)),skolemize(X,sK58_skl(Y)),skolemize(X,sK59_skl(Y)),skolemize(X,sK60_skl(Y)),skolemize(X,sK61_skl(Y)),skolemize(X,sK62_skl(Y)),skolemize(X,sK63_skl(Y)),skolemize(X,sK64_skl(Y)),skolemize(Y,sK65_skl),skolemize(Y,sK66_skl),skolemize(Y,sK67_skl),skolemize(Y,sK68_skl)],[f5])).
% 138.94/22.92 fof(f8,plain,(
% 138.94/22.92 ![X0,X1,X2,X3,X4]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p54(X4))),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f55,plain,(
% 138.94/22.92 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|r1(X3,sK23_skl(X3,X2,X1,X0))|p41(X3))),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f56,plain,(
% 138.94/22.92 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~p54(sK23_skl(X3,X2,X1,X0))|p41(X3))),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f77,plain,(
% 138.94/22.92 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|r1(X2,sK34_skl(X2,X1,X0))|p34(X2))),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f78,plain,(
% 138.94/22.92 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~p41(sK34_skl(X2,X1,X0))|p34(X2))),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f119,plain,(
% 138.94/22.92 ![X0,X1]: (~r1(sK0_skl,X0)|~r1(X0,X1)|r1(X1,sK55_skl(X1,X0))|p21(X1))),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f120,plain,(
% 138.94/22.92 ![X0,X1]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~p34(sK55_skl(X1,X0))|p21(X1))),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f133,plain,(
% 138.94/22.92 ![X0]: (~r1(sK0_skl,X0)|r1(X0,sK62_skl(X0))|p12(X0))),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f134,plain,(
% 138.94/22.92 ![X0]: (~r1(sK0_skl,X0)|~p21(sK62_skl(X0))|p12(X0))),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f143,plain,(
% 138.94/22.92 r1(sK0_skl,sK67_skl)),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f144,plain,(
% 138.94/22.92 ~p12(sK67_skl)),
% 138.94/22.92 inference(cnf_transformation,[status(thm)],[f6])).
% 138.94/22.92 fof(f153,plain,(
% 138.94/22.92 ![X0,X1,X2,X3]: (~r1(sK67_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p54(X3))),
% 138.94/22.92 inference(resolution,[status(thm)],[f143,f8])).
% 138.94/22.92 fof(f522,plain,(
% 138.94/22.92 r1(sK67_skl,sK62_skl(sK67_skl))|p12(sK67_skl)),
% 138.94/22.92 inference(resolution,[status(thm)],[f133,f143])).
% 138.94/22.92 fof(f533,definition,(
% 138.94/22.92 sQ77_spl <=> (r1(sK67_skl,sK62_skl(sK67_skl)))),
% 138.94/22.92 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 138.94/22.92 fof(f534,plain,(
% 138.94/22.92 r1(sK67_skl,sK62_skl(sK67_skl))|~sQ77_spl),
% 138.94/22.92 inference(component_clause,[status(thm)],[f533])).
% 138.94/22.92 fof(f536,definition,(
% 138.94/22.92 sQ78_spl <=> (p12(sK67_skl))),
% 138.94/22.92 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 138.94/22.92 fof(f537,plain,(
% 138.94/22.92 p12(sK67_skl)|~sQ78_spl),
% 138.94/22.92 inference(component_clause,[status(thm)],[f536])).
% 138.94/22.92 fof(f539,plain,(
% 138.94/22.92 sQ77_spl|sQ78_spl),
% 138.94/22.92 inference(split_clause,[status(thm)],[f522,f533,f536])).
% 138.94/22.92 fof(f1039,plain,(
% 138.94/22.92 ![X0,X1,X2]: (~r1(sK67_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|r1(X2,sK23_skl(X2,X1,X0,sK67_skl))|p41(X2))),
% 138.94/22.92 inference(resolution,[status(thm)],[f55,f143])).
% 138.94/22.92 fof(f1144,plain,(
% 138.94/22.92 ![X0,X1]: (~r1(sK67_skl,X0)|~r1(X0,X1)|r1(X1,sK34_skl(X1,X0,sK67_skl))|p34(X1))),
% 138.94/22.92 inference(resolution,[status(thm)],[f77,f143])).
% 138.94/22.92 fof(f1564,plain,(
% 138.94/22.92 ![X0]: (~r1(sK67_skl,X0)|r1(X0,sK55_skl(X0,sK67_skl))|p21(X0))),
% 138.94/22.92 inference(resolution,[status(thm)],[f119,f143])).
% 138.94/22.92 fof(f5032,plain,(
% 138.94/22.92 ~p21(sK62_skl(sK67_skl))|p12(sK67_skl)),
% 138.94/22.92 inference(resolution,[status(thm)],[f134,f143])).
% 138.94/22.92 fof(f5040,definition,(
% 138.94/22.92 sQ869_spl <=> (p21(sK62_skl(sK67_skl)))),
% 138.94/22.92 introduced(definition,[new_symbols(definition,[sQ869_spl])],[split_symbol_definition])).
% 138.94/22.92 fof(f5043,plain,(
% 138.94/22.92 ~sQ869_spl|sQ78_spl),
% 138.94/22.92 inference(split_clause,[status(thm)],[f5032,f5040,f536])).
% 138.94/22.92 fof(f5056,plain,(
% 138.94/22.92 $false|~sQ78_spl),
% 138.94/22.92 inference(forward_subsumption_resolution,[status(thm)],[f537,f144])).
% 138.94/22.92 fof(f5057,plain,(
% 138.94/22.92 ~sQ78_spl),
% 138.94/22.92 inference(contradiction_clause,[status(thm)],[f5056])).
% 138.94/22.92 fof(f9670,plain,(
% 138.94/22.92 ![X0,X1,X2]: (~r1(sK62_skl(sK67_skl),X0)|~r1(X0,X1)|~r1(X1,X2)|p54(X2)|~sQ77_spl)),
% 138.94/22.92 inference(resolution,[status(thm)],[f534,f153])).
% 138.94/22.92 fof(f9777,plain,(
% 138.94/22.92 ![X0,X1]: (~r1(sK62_skl(sK67_skl),X0)|~r1(X0,X1)|r1(X1,sK23_skl(X1,X0,sK62_skl(sK67_skl),sK67_skl))|p41(X1)|~sQ77_spl)),
% 138.94/22.92 inference(resolution,[status(thm)],[f534,f1039])).
% 138.94/22.92 fof(f9783,plain,(
% 138.94/22.92 ![X0]: (~r1(sK62_skl(sK67_skl),X0)|r1(X0,sK34_skl(X0,sK62_skl(sK67_skl),sK67_skl))|p34(X0)|~sQ77_spl)),
% 138.94/22.92 inference(resolution,[status(thm)],[f534,f1144])).
% 138.94/22.92 fof(f9821,plain,(
% 138.94/22.92 r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl))|p21(sK62_skl(sK67_skl))|~sQ77_spl),
% 138.94/22.92 inference(resolution,[status(thm)],[f534,f1564])).
% 138.94/22.92 fof(f10217,definition,(
% 138.94/22.92 sQ1823_spl <=> (r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl)))),
% 138.94/22.92 introduced(definition,[new_symbols(definition,[sQ1823_spl])],[split_symbol_definition])).
% 138.94/22.92 fof(f10218,plain,(
% 138.94/22.92 r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl))|~sQ1823_spl),
% 138.94/22.92 inference(component_clause,[status(thm)],[f10217])).
% 138.94/22.92 fof(f10220,plain,(
% 138.94/22.92 sQ1823_spl|sQ869_spl|~sQ77_spl),
% 138.94/22.92 inference(split_clause,[status(thm)],[f9821,f10217,f5040,f533])).
% 138.94/22.92 fof(f22192,plain,(
% 138.94/22.92 ![X0,X1]: (~r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),X0)|~r1(X0,X1)|p54(X1)|~sQ1823_spl|~sQ77_spl)),
% 138.94/22.92 inference(resolution,[status(thm)],[f10218,f9670])).
% 138.94/22.92 fof(f22268,plain,(
% 138.94/22.92 ![X0]: (~r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),X0)|r1(X0,sK23_skl(X0,sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|p41(X0)|~sQ1823_spl|~sQ77_spl)),
% 138.94/22.92 inference(resolution,[status(thm)],[f10218,f9777])).
% 138.94/22.92 fof(f22279,plain,(
% 138.94/22.92 r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|p34(sK55_skl(sK62_skl(sK67_skl),sK67_skl))|~sQ1823_spl|~sQ77_spl),
% 138.94/22.92 inference(resolution,[status(thm)],[f10218,f9783])).
% 138.94/22.92 fof(f22571,definition,(
% 138.94/22.92 sQ4274_spl <=> (r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl)))),
% 138.94/22.92 introduced(definition,[new_symbols(definition,[sQ4274_spl])],[split_symbol_definition])).
% 138.94/22.92 fof(f22572,plain,(
% 138.94/22.92 r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|~sQ4274_spl),
% 138.94/22.92 inference(component_clause,[status(thm)],[f22571])).
% 138.94/22.92 fof(f22574,definition,(
% 138.94/22.92 sQ4275_spl <=> (p34(sK55_skl(sK62_skl(sK67_skl),sK67_skl)))),
% 138.94/22.92 introduced(definition,[new_symbols(definition,[sQ4275_spl])],[split_symbol_definition])).
% 138.94/22.92 fof(f22575,plain,(
% 138.94/22.92 p34(sK55_skl(sK62_skl(sK67_skl),sK67_skl))|~sQ4275_spl),
% 138.94/22.92 inference(component_clause,[status(thm)],[f22574])).
% 138.94/22.92 fof(f22577,plain,(
% 138.94/22.92 sQ4274_spl|sQ4275_spl|~sQ1823_spl|~sQ77_spl),
% 138.94/22.92 inference(split_clause,[status(thm)],[f22279,f22571,f22574,f10217,f533])).
% 138.94/22.92 fof(f26398,definition,(
% 138.94/22.92 sQ4989_spl <=> (r1(sK0_skl,sK67_skl))),
% 138.94/22.92 introduced(definition,[new_symbols(definition,[sQ4989_spl])],[split_symbol_definition])).
% 138.94/22.92 fof(f26400,plain,(
% 138.94/22.92 ~r1(sK0_skl,sK67_skl)|sQ4989_spl),
% 138.94/22.92 inference(component_clause,[status(thm)],[f26398])).
% 138.94/22.92 fof(f26402,plain,(
% 138.94/22.92 $false|sQ4989_spl),
% 138.94/22.92 inference(forward_subsumption_resolution,[status(thm)],[f26400,f143])).
% 138.94/22.92 fof(f26403,plain,(
% 138.94/22.92 sQ4989_spl),
% 138.94/22.92 inference(contradiction_clause,[status(thm)],[f26402])).
% 138.94/22.92 fof(f28504,plain,(
% 138.94/22.92 ![X0]: (~r1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),X0)|p54(X0)|~sQ4274_spl|~sQ1823_spl|~sQ77_spl)),
% 138.94/22.92 inference(resolution,[status(thm)],[f22572,f22192])).
% 138.94/22.92 fof(f28507,plain,(
% 138.94/22.92 r1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|p41(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|~sQ4274_spl|~sQ1823_spl|~sQ77_spl),
% 138.94/22.92 inference(resolution,[status(thm)],[f22572,f22268])).
% 138.94/22.92 fof(f28527,definition,(
% 138.94/22.92 sQ5417_spl <=> (p41(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl)))),
% 138.94/22.92 introduced(definition,[new_symbols(definition,[sQ5417_spl])],[split_symbol_definition])).
% 138.94/22.92 fof(f28528,plain,(
% 138.94/22.92 p41(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|~sQ5417_spl),
% 138.94/22.92 inference(component_clause,[status(thm)],[f28527])).
% 138.94/22.92 fof(f28535,definition,(
% 138.94/22.92 sQ5419_spl <=> (r1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl)))),
% 138.94/22.92 introduced(definition,[new_symbols(definition,[sQ5419_spl])],[split_symbol_definition])).
% 138.94/22.92 fof(f28536,plain,(
% 138.94/22.92 r1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|~sQ5419_spl),
% 138.94/22.92 inference(component_clause,[status(thm)],[f28535])).
% 138.94/22.92 fof(f28538,plain,(
% 138.94/22.92 sQ5419_spl|sQ5417_spl|~sQ4274_spl|~sQ1823_spl|~sQ77_spl),
% 138.94/22.92 inference(split_clause,[status(thm)],[f28507,f28535,f28527,f22571,f10217,f533])).
% 138.94/22.98 fof(f32869,plain,(
% 138.94/22.98 ~r1(sK0_skl,sK67_skl)|~r1(sK67_skl,sK62_skl(sK67_skl))|~r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl))|p34(sK55_skl(sK62_skl(sK67_skl),sK67_skl))|~sQ5417_spl),
% 138.94/22.98 inference(resolution,[status(thm)],[f28528,f78])).
% 138.94/22.98 fof(f32870,plain,(
% 138.94/22.98 ~sQ4989_spl|~sQ77_spl|~sQ1823_spl|sQ4275_spl|~sQ5417_spl),
% 138.94/22.98 inference(split_clause,[status(thm)],[f32869,f26398,f533,f10217,f22574,f28527])).
% 138.94/22.98 fof(f32871,plain,(
% 138.94/22.98 ~r1(sK0_skl,sK67_skl)|~r1(sK67_skl,sK62_skl(sK67_skl))|p21(sK62_skl(sK67_skl))|~sQ4275_spl),
% 138.94/22.98 inference(resolution,[status(thm)],[f22575,f120])).
% 138.94/22.98 fof(f32872,plain,(
% 138.94/22.98 ~sQ4989_spl|~sQ77_spl|sQ869_spl|~sQ4275_spl),
% 138.94/22.98 inference(split_clause,[status(thm)],[f32871,f26398,f533,f5040,f22574])).
% 138.94/22.98 fof(f33137,plain,(
% 138.94/22.98 p54(sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|~sQ5419_spl|~sQ4274_spl|~sQ1823_spl|~sQ77_spl),
% 138.94/22.98 inference(resolution,[status(thm)],[f28536,f28504])).
% 138.94/22.98 fof(f33431,plain,(
% 138.94/22.98 ~r1(sK0_skl,sK67_skl)|~r1(sK67_skl,sK62_skl(sK67_skl))|~r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl))|~r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|p41(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|~sQ5419_spl|~sQ4274_spl|~sQ1823_spl|~sQ77_spl),
% 138.94/22.98 inference(resolution,[status(thm)],[f33137,f56])).
% 138.94/22.98 fof(f33432,plain,(
% 138.94/22.98 ~sQ4989_spl|~sQ77_spl|~sQ1823_spl|~sQ4274_spl|sQ5417_spl|~sQ5419_spl),
% 138.94/22.98 inference(split_clause,[status(thm)],[f33431,f26398,f533,f10217,f22571,f28527,f28535])).
% 138.94/22.98 fof(f33433,plain,(
% 138.94/22.98 $false),
% 138.94/22.98 inference(sat_refutation,[status(thm)],[f539,f5043,f5057,f10220,f22577,f26403,f28538,f32870,f32872,f33432])).
% 138.94/22.98 % SZS output end CNFRefutation for theBenchmark.p
% 17.52/23.02 % Elapsed time: 17.631611 seconds
% 17.52/23.02 % CPU time: 139.754716 seconds
% 17.52/23.02 % Total memory used: 495.778 MB
% 17.52/23.02 % Net memory used: 484.987 MB
%------------------------------------------------------------------------------