%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL644+1.010 : 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 : n012.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:28 PM UTC 2026
% Result : Theorem 0.09s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL644+1.010 : 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.09/0.36 % Computer : n012.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 00:44:07 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.39 % Refutation found
% 0.09/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.39 fof(f1,conjecture,(
% 0.09/0.39 ~ (? [X] :~ ( ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p11(Y)& (! [X] :( ~ r1(Y,X)| p11(X) ) ))| p10(Y) ))| (! [Y] :( ~ r1(X,Y)| p11(Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ))& p10(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p11(X)& (! [Y] :( ~ r1(X,Y)| p11(Y) ) ))| p10(X) ))| p11(Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ))& p10(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p11(Y)& (! [X] :( ~ r1(Y,X)| p11(X) ) ))| p10(Y)| (! [X] :( ~ r1(Y,X)| p11(X)| ~ ( p10(X)& (! [Y] :( ~ r1(X,Y)| p10(Y) ))& p10(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p11(Y)& (! [X] :( ~ r1(Y,X)| p11(X) ) ))| p10(Y)| p11(Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ))& p10(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ) ))| p9(Y) ))| (! [Y] :( ~ r1(X,Y)| p10(Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ))& p9(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p10(X)& (! [Y] :( ~ r1(X,Y)| p10(Y) ) ))| p9(X) ))| p10(Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ))& p9(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ) ))| p9(Y)| (! [X] :( ~ r1(Y,X)| p10(X)| ~ ( p9(X)& (! [Y] :( ~ r1(X,Y)| p9(Y) ))& p9(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ) ))| p9(Y)| p10(Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ))& p9(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ) ))| p8(Y) ))| (! [Y] :( ~ r1(X,Y)| p9(Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ))& p8(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p9(X)& (! [Y] :( ~ r1(X,Y)| p9(Y) ) ))| p8(X) ))| p9(Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ))& p8(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ) ))| p8(Y)| (! [X] :( ~ r1(Y,X)| p9(X)| ~ ( p8(X)& (! [Y] :( ~ r1(X,Y)| p8(Y) ))& p8(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ) ))| p8(Y)| p9(Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ))& p8(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ) ))| p7(Y) ))| (! [Y] :( ~ r1(X,Y)| p8(Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ))& p7(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p8(X)& (! [Y] :( ~ r1(X,Y)| p8(Y) ) ))| p7(X) ))| p8(Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ))& p7(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ) ))| p7(Y)| (! [X] :( ~ r1(Y,X)| p8(X)| ~ ( p7(X)& (! [Y] :( ~ r1(X,Y)| p7(Y) ))& p7(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ) ))| p7(Y)| p8(Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ))& p7(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ) ))| p6(Y) ))| (! [Y] :( ~ r1(X,Y)| p7(Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ))& p6(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p7(X)& (! [Y] :( ~ r1(X,Y)| p7(Y) ) ))| p6(X) ))| p7(Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ))& p6(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ) ))| p6(Y)| (! [X] :( ~ r1(Y,X)| p7(X)| ~ ( p6(X)& (! [Y] :( ~ r1(X,Y)| p6(Y) ))& p6(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ) ))| p6(Y)| p7(Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ))& p6(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y) ))| (! [Y] :( ~ r1(X,Y)| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p6(X)& (! [Y] :( ~ r1(X,Y)| p6(Y) ) ))| p5(X) ))| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y)| (! [X] :( ~ r1(Y,X)| p6(X)| ~ ( p5(X)& (! [Y] :( ~ r1(X,Y)| p5(Y) ))& p5(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y)| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y) ))| (! [Y] :( ~ r1(X,Y)| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p5(X)& (! [Y] :( ~ r1(X,Y)| p5(Y) ) ))| p4(X) ))| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y)| (! [X] :( ~ r1(Y,X)| p5(X)| ~ ( p4(X)& (! [Y] :( ~ r1(X,Y)| p4(Y) ))& p4(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y)| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ) )) )| (! [Y] :( ~ r1(X,Y)| p10(Y)| ~ ( (! [X] :( ~ r1(Y,X)| p10(X) ))& p10(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p10(Y)| ~ ( (! [X] :( ~ r1(Y,X)| p10(X) ))& p10(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y) ))| (! [Y] :( ~ r1(X,Y)| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p4(X)& (! [Y] :( ~ r1(X,Y)| p4(Y) ) ))| p3(X) ))| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y)| (! [X] :( ~ r1(Y,X)| p4(X)| ~ ( p3(X)& (! [Y] :( ~ r1(X,Y)| p3(Y) ))& p3(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y)| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p3(X)& (! [Y] :( ~ r1(X,Y)| p3(Y) ) ))| p2(X) ))| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y)| (! [X] :( ~ r1(Y,X)| p3(X)| ~ ( p2(X)& (! [Y] :( ~ r1(X,Y)| p2(Y) ))& p2(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y)| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y) ))| (! [Y] :( ~ r1(X,Y)| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p2(X)& (! [Y] :( ~ r1(X,Y)| p2(Y) ) ))| p1(X) ))| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y)| (! [X] :( ~ r1(Y,X)| p2(X)| ~ ( p1(X)& (! [Y] :( ~ r1(X,Y)| p1(Y) ))& p1(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y)| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ) )) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f2,negated_conjecture,(
% 0.09/0.39 ~(~ (? [X] :~ ( ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p11(Y)& (! [X] :( ~ r1(Y,X)| p11(X) ) ))| p10(Y) ))| (! [Y] :( ~ r1(X,Y)| p11(Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ))& p10(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p11(X)& (! [Y] :( ~ r1(X,Y)| p11(Y) ) ))| p10(X) ))| p11(Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ))& p10(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p11(Y)& (! [X] :( ~ r1(Y,X)| p11(X) ) ))| p10(Y)| (! [X] :( ~ r1(Y,X)| p11(X)| ~ ( p10(X)& (! [Y] :( ~ r1(X,Y)| p10(Y) ))& p10(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p11(Y)& (! [X] :( ~ r1(Y,X)| p11(X) ) ))| p10(Y)| p11(Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ))& p10(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ) ))| p9(Y) ))| (! [Y] :( ~ r1(X,Y)| p10(Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ))& p9(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p10(X)& (! [Y] :( ~ r1(X,Y)| p10(Y) ) ))| p9(X) ))| p10(Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ))& p9(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ) ))| p9(Y)| (! [X] :( ~ r1(Y,X)| p10(X)| ~ ( p9(X)& (! [Y] :( ~ r1(X,Y)| p9(Y) ))& p9(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p10(Y)& (! [X] :( ~ r1(Y,X)| p10(X) ) ))| p9(Y)| p10(Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ))& p9(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ) ))| p8(Y) ))| (! [Y] :( ~ r1(X,Y)| p9(Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ))& p8(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p9(X)& (! [Y] :( ~ r1(X,Y)| p9(Y) ) ))| p8(X) ))| p9(Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ))& p8(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ) ))| p8(Y)| (! [X] :( ~ r1(Y,X)| p9(X)| ~ ( p8(X)& (! [Y] :( ~ r1(X,Y)| p8(Y) ))& p8(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p9(Y)& (! [X] :( ~ r1(Y,X)| p9(X) ) ))| p8(Y)| p9(Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ))& p8(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ) ))| p7(Y) ))| (! [Y] :( ~ r1(X,Y)| p8(Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ))& p7(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p8(X)& (! [Y] :( ~ r1(X,Y)| p8(Y) ) ))| p7(X) ))| p8(Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ))& p7(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ) ))| p7(Y)| (! [X] :( ~ r1(Y,X)| p8(X)| ~ ( p7(X)& (! [Y] :( ~ r1(X,Y)| p7(Y) ))& p7(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p8(Y)& (! [X] :( ~ r1(Y,X)| p8(X) ) ))| p7(Y)| p8(Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ))& p7(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ) ))| p6(Y) ))| (! [Y] :( ~ r1(X,Y)| p7(Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ))& p6(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p7(X)& (! [Y] :( ~ r1(X,Y)| p7(Y) ) ))| p6(X) ))| p7(Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ))& p6(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ) ))| p6(Y)| (! [X] :( ~ r1(Y,X)| p7(X)| ~ ( p6(X)& (! [Y] :( ~ r1(X,Y)| p6(Y) ))& p6(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p7(Y)& (! [X] :( ~ r1(Y,X)| p7(X) ) ))| p6(Y)| p7(Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ))& p6(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y) ))| (! [Y] :( ~ r1(X,Y)| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p6(X)& (! [Y] :( ~ r1(X,Y)| p6(Y) ) ))| p5(X) ))| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y)| (! [X] :( ~ r1(Y,X)| p6(X)| ~ ( p5(X)& (! [Y] :( ~ r1(X,Y)| p5(Y) ))& p5(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y)| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y) ))| (! [Y] :( ~ r1(X,Y)| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p5(X)& (! [Y] :( ~ r1(X,Y)| p5(Y) ) ))| p4(X) ))| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y)| (! [X] :( ~ r1(Y,X)| p5(X)| ~ ( p4(X)& (! [Y] :( ~ r1(X,Y)| p4(Y) ))& p4(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y)| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ) )) )| (! [Y] :( ~ r1(X,Y)| p10(Y)| ~ ( (! [X] :( ~ r1(Y,X)| p10(X) ))& p10(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p10(Y)| ~ ( (! [X] :( ~ r1(Y,X)| p10(X) ))& p10(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y) ))| (! [Y] :( ~ r1(X,Y)| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p4(X)& (! [Y] :( ~ r1(X,Y)| p4(Y) ) ))| p3(X) ))| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y)| (! [X] :( ~ r1(Y,X)| p4(X)| ~ ( p3(X)& (! [Y] :( ~ r1(X,Y)| p3(Y) ))& p3(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y)| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p3(X)& (! [Y] :( ~ r1(X,Y)| p3(Y) ) ))| p2(X) ))| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y)| (! [X] :( ~ r1(Y,X)| p3(X)| ~ ( p2(X)& (! [Y] :( ~ r1(X,Y)| p2(Y) ))& p2(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y)| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y) ))| (! [Y] :( ~ r1(X,Y)| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p2(X)& (! [Y] :( ~ r1(X,Y)| p2(Y) ) ))| p1(X) ))| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y)| (! [X] :( ~ r1(Y,X)| p2(X)| ~ ( p1(X)& (! [Y] :( ~ r1(X,Y)| p1(Y) ))& p1(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y)| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ) )) ) ) ))),
% 0.09/0.39 inference(negated_conjecture,[status(cth)],[f1])).
% 0.09/0.39 fof(f3,plain,(
% 0.09/0.39 ?[X]: ((((((((((((((![Y]: ((~r1(X,Y)|(~p11(Y)|(?[X]: (r1(Y,X)&~p11(X)))))|p10(Y)))|(![Y]: ((~r1(X,Y)|p11(Y))|((~p10(Y)|(?[X]: (r1(Y,X)&~p10(X))))|~p10(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p11(X)&(![Y]: (~r1(X,Y)|p11(Y)))))&~p10(X))))&~p11(Y))&((p10(Y)&(![X]: (~r1(Y,X)|p10(X))))&p10(Y))))|(?[Y]: (((r1(X,Y)&(p11(Y)&(![X]: (~r1(Y,X)|p11(X)))))&~p10(Y))&(?[X]: ((r1(Y,X)&~p11(X))&((p10(X)&(![Y]: (~r1(X,Y)|p10(Y))))&p10(X)))))))|(?[Y]: ((((r1(X,Y)&(p11(Y)&(![X]: (~r1(Y,X)|p11(X)))))&~p10(Y))&~p11(Y))&((p10(Y)&(![X]: (~r1(Y,X)|p10(X))))&p10(Y))))))&(((![Y]: ((~r1(X,Y)|(~p10(Y)|(?[X]: (r1(Y,X)&~p10(X)))))|p9(Y)))|(![Y]: ((~r1(X,Y)|p10(Y))|((~p9(Y)|(?[X]: (r1(Y,X)&~p9(X))))|~p9(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p10(X)&(![Y]: (~r1(X,Y)|p10(Y)))))&~p9(X))))&~p10(Y))&((p9(Y)&(![X]: (~r1(Y,X)|p9(X))))&p9(Y))))|(?[Y]: (((r1(X,Y)&(p10(Y)&(![X]: (~r1(Y,X)|p10(X)))))&~p9(Y))&(?[X]: ((r1(Y,X)&~p10(X))&((p9(X)&(![Y]: (~r1(X,Y)|p9(Y))))&p9(X)))))))|(?[Y]: ((((r1(X,Y)&(p10(Y)&(![X]: (~r1(Y,X)|p10(X)))))&~p9(Y))&~p10(Y))&((p9(Y)&(![X]: (~r1(Y,X)|p9(X))))&p9(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p9(Y)|(?[X]: (r1(Y,X)&~p9(X)))))|p8(Y)))|(![Y]: ((~r1(X,Y)|p9(Y))|((~p8(Y)|(?[X]: (r1(Y,X)&~p8(X))))|~p8(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p9(X)&(![Y]: (~r1(X,Y)|p9(Y)))))&~p8(X))))&~p9(Y))&((p8(Y)&(![X]: (~r1(Y,X)|p8(X))))&p8(Y))))|(?[Y]: (((r1(X,Y)&(p9(Y)&(![X]: (~r1(Y,X)|p9(X)))))&~p8(Y))&(?[X]: ((r1(Y,X)&~p9(X))&((p8(X)&(![Y]: (~r1(X,Y)|p8(Y))))&p8(X)))))))|(?[Y]: ((((r1(X,Y)&(p9(Y)&(![X]: (~r1(Y,X)|p9(X)))))&~p8(Y))&~p9(Y))&((p8(Y)&(![X]: (~r1(Y,X)|p8(X))))&p8(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p8(Y)|(?[X]: (r1(Y,X)&~p8(X)))))|p7(Y)))|(![Y]: ((~r1(X,Y)|p8(Y))|((~p7(Y)|(?[X]: (r1(Y,X)&~p7(X))))|~p7(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p8(X)&(![Y]: (~r1(X,Y)|p8(Y)))))&~p7(X))))&~p8(Y))&((p7(Y)&(![X]: (~r1(Y,X)|p7(X))))&p7(Y))))|(?[Y]: (((r1(X,Y)&(p8(Y)&(![X]: (~r1(Y,X)|p8(X)))))&~p7(Y))&(?[X]: ((r1(Y,X)&~p8(X))&((p7(X)&(![Y]: (~r1(X,Y)|p7(Y))))&p7(X)))))))|(?[Y]: ((((r1(X,Y)&(p8(Y)&(![X]: (~r1(Y,X)|p8(X)))))&~p7(Y))&~p8(Y))&((p7(Y)&(![X]: (~r1(Y,X)|p7(X))))&p7(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p7(Y)|(?[X]: (r1(Y,X)&~p7(X)))))|p6(Y)))|(![Y]: ((~r1(X,Y)|p7(Y))|((~p6(Y)|(?[X]: (r1(Y,X)&~p6(X))))|~p6(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p7(X)&(![Y]: (~r1(X,Y)|p7(Y)))))&~p6(X))))&~p7(Y))&((p6(Y)&(![X]: (~r1(Y,X)|p6(X))))&p6(Y))))|(?[Y]: (((r1(X,Y)&(p7(Y)&(![X]: (~r1(Y,X)|p7(X)))))&~p6(Y))&(?[X]: ((r1(Y,X)&~p7(X))&((p6(X)&(![Y]: (~r1(X,Y)|p6(Y))))&p6(X)))))))|(?[Y]: ((((r1(X,Y)&(p7(Y)&(![X]: (~r1(Y,X)|p7(X)))))&~p6(Y))&~p7(Y))&((p6(Y)&(![X]: (~r1(Y,X)|p6(X))))&p6(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p6(Y)|(?[X]: (r1(Y,X)&~p6(X)))))|p5(Y)))|(![Y]: ((~r1(X,Y)|p6(Y))|((~p5(Y)|(?[X]: (r1(Y,X)&~p5(X))))|~p5(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p6(X)&(![Y]: (~r1(X,Y)|p6(Y)))))&~p5(X))))&~p6(Y))&((p5(Y)&(![X]: (~r1(Y,X)|p5(X))))&p5(Y))))|(?[Y]: (((r1(X,Y)&(p6(Y)&(![X]: (~r1(Y,X)|p6(X)))))&~p5(Y))&(?[X]: ((r1(Y,X)&~p6(X))&((p5(X)&(![Y]: (~r1(X,Y)|p5(Y))))&p5(X)))))))|(?[Y]: ((((r1(X,Y)&(p6(Y)&(![X]: (~r1(Y,X)|p6(X)))))&~p5(Y))&~p6(Y))&((p5(Y)&(![X]: (~r1(Y,X)|p5(X))))&p5(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p5(Y)|(?[X]: (r1(Y,X)&~p5(X)))))|p4(Y)))|(![Y]: ((~r1(X,Y)|p5(Y))|((~p4(Y)|(?[X]: (r1(Y,X)&~p4(X))))|~p4(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p5(X)&(![Y]: (~r1(X,Y)|p5(Y)))))&~p4(X))))&~p5(Y))&((p4(Y)&(![X]: (~r1(Y,X)|p4(X))))&p4(Y))))|(?[Y]: (((r1(X,Y)&(p5(Y)&(![X]: (~r1(Y,X)|p5(X)))))&~p4(Y))&(?[X]: ((r1(Y,X)&~p5(X))&((p4(X)&(![Y]: (~r1(X,Y)|p4(Y))))&p4(X)))))))|(?[Y]: ((((r1(X,Y)&(p5(Y)&(![X]: (~r1(Y,X)|p5(X)))))&~p4(Y))&~p5(Y))&((p4(Y)&(![X]: (~r1(Y,X)|p4(X))))&p4(Y)))))))&(?[Y]: ((r1(X,Y)&~p10(Y))&((![X]: (~r1(Y,X)|p10(X)))&p10(Y)))))&(?[Y]: ((r1(X,Y)&~p10(Y))&((![X]: (~r1(Y,X)|p10(X)))&p10(Y)))))&(((![Y]: ((~r1(X,Y)|(~p4(Y)|(?[X]: (r1(Y,X)&~p4(X)))))|p3(Y)))|(![Y]: ((~r1(X,Y)|p4(Y))|((~p3(Y)|(?[X]: (r1(Y,X)&~p3(X))))|~p3(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p4(X)&(![Y]: (~r1(X,Y)|p4(Y)))))&~p3(X))))&~p4(Y))&((p3(Y)&(![X]: (~r1(Y,X)|p3(X))))&p3(Y))))|(?[Y]: (((r1(X,Y)&(p4(Y)&(![X]: (~r1(Y,X)|p4(X)))))&~p3(Y))&(?[X]: ((r1(Y,X)&~p4(X))&((p3(X)&(![Y]: (~r1(X,Y)|p3(Y))))&p3(X)))))))|(?[Y]: ((((r1(X,Y)&(p4(Y)&(![X]: (~r1(Y,X)|p4(X)))))&~p3(Y))&~p4(Y))&((p3(Y)&(![X]: (~r1(Y,X)|p3(X))))&p3(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p3(Y)|(?[X]: (r1(Y,X)&~p3(X)))))|p2(Y)))|(![Y]: ((~r1(X,Y)|p3(Y))|((~p2(Y)|(?[X]: (r1(Y,X)&~p2(X))))|~p2(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p3(X)&(![Y]: (~r1(X,Y)|p3(Y)))))&~p2(X))))&~p3(Y))&((p2(Y)&(![X]: (~r1(Y,X)|p2(X))))&p2(Y))))|(?[Y]: (((r1(X,Y)&(p3(Y)&(![X]: (~r1(Y,X)|p3(X)))))&~p2(Y))&(?[X]: ((r1(Y,X)&~p3(X))&((p2(X)&(![Y]: (~r1(X,Y)|p2(Y))))&p2(X)))))))|(?[Y]: ((((r1(X,Y)&(p3(Y)&(![X]: (~r1(Y,X)|p3(X)))))&~p2(Y))&~p3(Y))&((p2(Y)&(![X]: (~r1(Y,X)|p2(X))))&p2(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p2(Y)|(?[X]: (r1(Y,X)&~p2(X)))))|p1(Y)))|(![Y]: ((~r1(X,Y)|p2(Y))|((~p1(Y)|(?[X]: (r1(Y,X)&~p1(X))))|~p1(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p2(X)&(![Y]: (~r1(X,Y)|p2(Y)))))&~p1(X))))&~p2(Y))&((p1(Y)&(![X]: (~r1(Y,X)|p1(X))))&p1(Y))))|(?[Y]: (((r1(X,Y)&(p2(Y)&(![X]: (~r1(Y,X)|p2(X)))))&~p1(Y))&(?[X]: ((r1(Y,X)&~p2(X))&((p1(X)&(![Y]: (~r1(X,Y)|p1(Y))))&p1(X)))))))|(?[Y]: ((((r1(X,Y)&(p2(Y)&(![X]: (~r1(Y,X)|p2(X)))))&~p1(Y))&~p2(Y))&((p1(Y)&(![X]: (~r1(Y,X)|p1(X))))&p1(Y)))))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.09/0.39 fof(f4,definition,(
% 0.09/0.39 ![Y,X]: (sP0_prd(X,Y)<=>(r1(Y,X)&~p11(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.09/0.39 fof(f5,definition,(
% 0.09/0.39 ![Y,X]: (sP1_prd(X,Y)<=>(r1(Y,X)&~p10(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.09/0.39 fof(f6,definition,(
% 0.09/0.39 ![X]: (sP2_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p11(X)&(![Y]: (~r1(X,Y)|p11(Y)))))&~p10(X))))&~p11(Y))&((p10(Y)&(![X]: (~r1(Y,X)|p10(X))))&p10(Y))))|(?[Y]: (((r1(X,Y)&(p11(Y)&(![X]: (~r1(Y,X)|p11(X)))))&~p10(Y))&(?[X]: ((r1(Y,X)&~p11(X))&((p10(X)&(![Y]: (~r1(X,Y)|p10(Y))))&p10(X))))))))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.09/0.39 fof(f7,definition,(
% 0.09/0.39 ![Y,X]: (sP3_prd(X,Y)<=>(r1(Y,X)&~p10(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.09/0.39 fof(f8,definition,(
% 0.09/0.39 ![Y,X]: (sP4_prd(X,Y)<=>(r1(Y,X)&~p9(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.09/0.39 fof(f9,definition,(
% 0.09/0.39 ![X]: (sP5_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p10(X)&(![Y]: (~r1(X,Y)|p10(Y)))))&~p9(X))))&~p10(Y))&((p9(Y)&(![X]: (~r1(Y,X)|p9(X))))&p9(Y))))|(?[Y]: (((r1(X,Y)&(p10(Y)&(![X]: (~r1(Y,X)|p10(X)))))&~p9(Y))&(?[X]: ((r1(Y,X)&~p10(X))&((p9(X)&(![Y]: (~r1(X,Y)|p9(Y))))&p9(X))))))))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.09/0.39 fof(f10,definition,(
% 0.09/0.39 ![Y,X]: (sP6_prd(X,Y)<=>(r1(Y,X)&~p9(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.09/0.39 fof(f11,definition,(
% 0.09/0.39 ![Y,X]: (sP7_prd(X,Y)<=>(r1(Y,X)&~p8(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.09/0.39 fof(f12,definition,(
% 0.09/0.39 ![X]: (sP8_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p9(X)&(![Y]: (~r1(X,Y)|p9(Y)))))&~p8(X))))&~p9(Y))&((p8(Y)&(![X]: (~r1(Y,X)|p8(X))))&p8(Y))))|(?[Y]: (((r1(X,Y)&(p9(Y)&(![X]: (~r1(Y,X)|p9(X)))))&~p8(Y))&(?[X]: ((r1(Y,X)&~p9(X))&((p8(X)&(![Y]: (~r1(X,Y)|p8(Y))))&p8(X))))))))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.09/0.39 fof(f13,definition,(
% 0.09/0.39 ![Y,X]: (sP9_prd(X,Y)<=>(r1(Y,X)&~p8(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.09/0.39 fof(f14,definition,(
% 0.09/0.39 ![Y,X]: (sP10_prd(X,Y)<=>(r1(Y,X)&~p7(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.09/0.39 fof(f15,definition,(
% 0.09/0.39 ![X]: (sP11_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p8(X)&(![Y]: (~r1(X,Y)|p8(Y)))))&~p7(X))))&~p8(Y))&((p7(Y)&(![X]: (~r1(Y,X)|p7(X))))&p7(Y))))|(?[Y]: (((r1(X,Y)&(p8(Y)&(![X]: (~r1(Y,X)|p8(X)))))&~p7(Y))&(?[X]: ((r1(Y,X)&~p8(X))&((p7(X)&(![Y]: (~r1(X,Y)|p7(Y))))&p7(X))))))))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.09/0.39 fof(f16,definition,(
% 0.09/0.39 ![Y,X]: (sP12_prd(X,Y)<=>(r1(Y,X)&~p7(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.09/0.39 fof(f17,definition,(
% 0.09/0.39 ![Y,X]: (sP13_prd(X,Y)<=>(r1(Y,X)&~p6(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.09/0.39 fof(f18,definition,(
% 0.09/0.39 ![X]: (sP14_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p7(X)&(![Y]: (~r1(X,Y)|p7(Y)))))&~p6(X))))&~p7(Y))&((p6(Y)&(![X]: (~r1(Y,X)|p6(X))))&p6(Y))))|(?[Y]: (((r1(X,Y)&(p7(Y)&(![X]: (~r1(Y,X)|p7(X)))))&~p6(Y))&(?[X]: ((r1(Y,X)&~p7(X))&((p6(X)&(![Y]: (~r1(X,Y)|p6(Y))))&p6(X))))))))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 0.09/0.39 fof(f19,definition,(
% 0.09/0.39 ![Y,X]: (sP15_prd(X,Y)<=>(r1(Y,X)&~p6(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 0.09/0.39 fof(f20,definition,(
% 0.09/0.39 ![Y,X]: (sP16_prd(X,Y)<=>(r1(Y,X)&~p5(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP16_prd])],[])).
% 0.09/0.39 fof(f21,definition,(
% 0.09/0.39 ![X]: (sP17_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p6(X)&(![Y]: (~r1(X,Y)|p6(Y)))))&~p5(X))))&~p6(Y))&((p5(Y)&(![X]: (~r1(Y,X)|p5(X))))&p5(Y))))|(?[Y]: (((r1(X,Y)&(p6(Y)&(![X]: (~r1(Y,X)|p6(X)))))&~p5(Y))&(?[X]: ((r1(Y,X)&~p6(X))&((p5(X)&(![Y]: (~r1(X,Y)|p5(Y))))&p5(X))))))))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP17_prd])],[])).
% 0.09/0.39 fof(f22,definition,(
% 0.09/0.39 ![Y,X]: (sP18_prd(X,Y)<=>(r1(Y,X)&~p5(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP18_prd])],[])).
% 0.09/0.39 fof(f23,definition,(
% 0.09/0.39 ![Y,X]: (sP19_prd(X,Y)<=>(r1(Y,X)&~p4(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP19_prd])],[])).
% 0.09/0.39 fof(f24,definition,(
% 0.09/0.39 ![X]: (sP20_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p5(X)&(![Y]: (~r1(X,Y)|p5(Y)))))&~p4(X))))&~p5(Y))&((p4(Y)&(![X]: (~r1(Y,X)|p4(X))))&p4(Y))))|(?[Y]: (((r1(X,Y)&(p5(Y)&(![X]: (~r1(Y,X)|p5(X)))))&~p4(Y))&(?[X]: ((r1(Y,X)&~p5(X))&((p4(X)&(![Y]: (~r1(X,Y)|p4(Y))))&p4(X))))))))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP20_prd])],[])).
% 0.09/0.39 fof(f25,definition,(
% 0.09/0.39 ![Y,X]: (sP21_prd(X,Y)<=>(r1(Y,X)&~p4(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP21_prd])],[])).
% 0.09/0.39 fof(f26,definition,(
% 0.09/0.39 ![Y,X]: (sP22_prd(X,Y)<=>(r1(Y,X)&~p3(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP22_prd])],[])).
% 0.09/0.39 fof(f27,definition,(
% 0.09/0.39 ![X]: (sP23_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p4(X)&(![Y]: (~r1(X,Y)|p4(Y)))))&~p3(X))))&~p4(Y))&((p3(Y)&(![X]: (~r1(Y,X)|p3(X))))&p3(Y))))|(?[Y]: (((r1(X,Y)&(p4(Y)&(![X]: (~r1(Y,X)|p4(X)))))&~p3(Y))&(?[X]: ((r1(Y,X)&~p4(X))&((p3(X)&(![Y]: (~r1(X,Y)|p3(Y))))&p3(X))))))))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP23_prd])],[])).
% 0.09/0.39 fof(f28,definition,(
% 0.09/0.39 ![Y,X]: (sP24_prd(X,Y)<=>(r1(Y,X)&~p3(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP24_prd])],[])).
% 0.09/0.39 fof(f29,definition,(
% 0.09/0.39 ![Y,X]: (sP25_prd(X,Y)<=>(r1(Y,X)&~p2(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP25_prd])],[])).
% 0.09/0.39 fof(f30,definition,(
% 0.09/0.39 ![X]: (sP26_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p3(X)&(![Y]: (~r1(X,Y)|p3(Y)))))&~p2(X))))&~p3(Y))&((p2(Y)&(![X]: (~r1(Y,X)|p2(X))))&p2(Y))))|(?[Y]: (((r1(X,Y)&(p3(Y)&(![X]: (~r1(Y,X)|p3(X)))))&~p2(Y))&(?[X]: ((r1(Y,X)&~p3(X))&((p2(X)&(![Y]: (~r1(X,Y)|p2(Y))))&p2(X))))))))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP26_prd])],[])).
% 0.09/0.39 fof(f31,definition,(
% 0.09/0.39 ![Y,X]: (sP27_prd(X,Y)<=>(r1(Y,X)&~p2(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP27_prd])],[])).
% 0.09/0.39 fof(f32,definition,(
% 0.09/0.39 ![Y,X]: (sP28_prd(X,Y)<=>(r1(Y,X)&~p1(X)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP28_prd])],[])).
% 0.09/0.39 fof(f33,definition,(
% 0.09/0.39 ![X]: (sP29_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p2(X)&(![Y]: (~r1(X,Y)|p2(Y)))))&~p1(X))))&~p2(Y))&((p1(Y)&(![X]: (~r1(Y,X)|p1(X))))&p1(Y))))|(?[Y]: (((r1(X,Y)&(p2(Y)&(![X]: (~r1(Y,X)|p2(X)))))&~p1(Y))&(?[X]: ((r1(Y,X)&~p2(X))&((p1(X)&(![Y]: (~r1(X,Y)|p1(Y))))&p1(X))))))))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP29_prd])],[])).
% 0.09/0.39 fof(f34,plain,(
% 0.09/0.39 ?[X]: ((((((((((((((![Y]: ((~r1(X,Y)|(~p11(Y)|(?[X]: sP0_prd(X,Y))))|p10(Y)))|(![Y]: ((~r1(X,Y)|p11(Y))|((~p10(Y)|(?[X]: sP1_prd(X,Y)))|~p10(Y)))))|(sP2_prd(X)|(?[Y]: ((((r1(X,Y)&(p11(Y)&(![X]: (~r1(Y,X)|p11(X)))))&~p10(Y))&~p11(Y))&((p10(Y)&(![X]: (~r1(Y,X)|p10(X))))&p10(Y))))))&(((![Y]: ((~r1(X,Y)|(~p10(Y)|(?[X]: sP3_prd(X,Y))))|p9(Y)))|(![Y]: ((~r1(X,Y)|p10(Y))|((~p9(Y)|(?[X]: sP4_prd(X,Y)))|~p9(Y)))))|(sP5_prd(X)|(?[Y]: ((((r1(X,Y)&(p10(Y)&(![X]: (~r1(Y,X)|p10(X)))))&~p9(Y))&~p10(Y))&((p9(Y)&(![X]: (~r1(Y,X)|p9(X))))&p9(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p9(Y)|(?[X]: sP6_prd(X,Y))))|p8(Y)))|(![Y]: ((~r1(X,Y)|p9(Y))|((~p8(Y)|(?[X]: sP7_prd(X,Y)))|~p8(Y)))))|(sP8_prd(X)|(?[Y]: ((((r1(X,Y)&(p9(Y)&(![X]: (~r1(Y,X)|p9(X)))))&~p8(Y))&~p9(Y))&((p8(Y)&(![X]: (~r1(Y,X)|p8(X))))&p8(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p8(Y)|(?[X]: sP9_prd(X,Y))))|p7(Y)))|(![Y]: ((~r1(X,Y)|p8(Y))|((~p7(Y)|(?[X]: sP10_prd(X,Y)))|~p7(Y)))))|(sP11_prd(X)|(?[Y]: ((((r1(X,Y)&(p8(Y)&(![X]: (~r1(Y,X)|p8(X)))))&~p7(Y))&~p8(Y))&((p7(Y)&(![X]: (~r1(Y,X)|p7(X))))&p7(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p7(Y)|(?[X]: sP12_prd(X,Y))))|p6(Y)))|(![Y]: ((~r1(X,Y)|p7(Y))|((~p6(Y)|(?[X]: sP13_prd(X,Y)))|~p6(Y)))))|(sP14_prd(X)|(?[Y]: ((((r1(X,Y)&(p7(Y)&(![X]: (~r1(Y,X)|p7(X)))))&~p6(Y))&~p7(Y))&((p6(Y)&(![X]: (~r1(Y,X)|p6(X))))&p6(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p6(Y)|(?[X]: sP15_prd(X,Y))))|p5(Y)))|(![Y]: ((~r1(X,Y)|p6(Y))|((~p5(Y)|(?[X]: sP16_prd(X,Y)))|~p5(Y)))))|(sP17_prd(X)|(?[Y]: ((((r1(X,Y)&(p6(Y)&(![X]: (~r1(Y,X)|p6(X)))))&~p5(Y))&~p6(Y))&((p5(Y)&(![X]: (~r1(Y,X)|p5(X))))&p5(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p5(Y)|(?[X]: sP18_prd(X,Y))))|p4(Y)))|(![Y]: ((~r1(X,Y)|p5(Y))|((~p4(Y)|(?[X]: sP19_prd(X,Y)))|~p4(Y)))))|(sP20_prd(X)|(?[Y]: ((((r1(X,Y)&(p5(Y)&(![X]: (~r1(Y,X)|p5(X)))))&~p4(Y))&~p5(Y))&((p4(Y)&(![X]: (~r1(Y,X)|p4(X))))&p4(Y)))))))&(?[Y]: ((r1(X,Y)&~p10(Y))&((![X]: (~r1(Y,X)|p10(X)))&p10(Y)))))&(?[Y]: ((r1(X,Y)&~p10(Y))&((![X]: (~r1(Y,X)|p10(X)))&p10(Y)))))&(((![Y]: ((~r1(X,Y)|(~p4(Y)|(?[X]: sP21_prd(X,Y))))|p3(Y)))|(![Y]: ((~r1(X,Y)|p4(Y))|((~p3(Y)|(?[X]: sP22_prd(X,Y)))|~p3(Y)))))|(sP23_prd(X)|(?[Y]: ((((r1(X,Y)&(p4(Y)&(![X]: (~r1(Y,X)|p4(X)))))&~p3(Y))&~p4(Y))&((p3(Y)&(![X]: (~r1(Y,X)|p3(X))))&p3(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p3(Y)|(?[X]: sP24_prd(X,Y))))|p2(Y)))|(![Y]: ((~r1(X,Y)|p3(Y))|((~p2(Y)|(?[X]: sP25_prd(X,Y)))|~p2(Y)))))|(sP26_prd(X)|(?[Y]: ((((r1(X,Y)&(p3(Y)&(![X]: (~r1(Y,X)|p3(X)))))&~p2(Y))&~p3(Y))&((p2(Y)&(![X]: (~r1(Y,X)|p2(X))))&p2(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p2(Y)|(?[X]: sP27_prd(X,Y))))|p1(Y)))|(![Y]: ((~r1(X,Y)|p2(Y))|((~p1(Y)|(?[X]: sP28_prd(X,Y)))|~p1(Y)))))|(sP29_prd(X)|(?[Y]: ((((r1(X,Y)&(p2(Y)&(![X]: (~r1(Y,X)|p2(X)))))&~p1(Y))&~p2(Y))&((p1(Y)&(![X]: (~r1(Y,X)|p1(X))))&p1(Y)))))))),
% 0.09/0.39 inference(formula_renaming,[status(thm)],[f3,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7,f6,f5,f4])).
% 0.09/0.39 fof(f35,plain,(
% 0.09/0.39 ((((((((((((((![Y]: ((~r1(sK0_skl,Y)|(~p11(Y)|sP0_prd(sK1_skl(Y),Y)))|p10(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p11(Y))|((~p10(Y)|sP1_prd(sK2_skl(Y),Y))|~p10(Y)))))|(sP2_prd(sK0_skl)|((((r1(sK0_skl,sK3_skl)&(p11(sK3_skl)&(![X]: (~r1(sK3_skl,X)|p11(X)))))&~p10(sK3_skl))&~p11(sK3_skl))&((p10(sK3_skl)&(![X]: (~r1(sK3_skl,X)|p10(X))))&p10(sK3_skl)))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p10(Y)|sP3_prd(sK4_skl(Y),Y)))|p9(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p10(Y))|((~p9(Y)|sP4_prd(sK5_skl(Y),Y))|~p9(Y)))))|(sP5_prd(sK0_skl)|((((r1(sK0_skl,sK6_skl)&(p10(sK6_skl)&(![X]: (~r1(sK6_skl,X)|p10(X)))))&~p9(sK6_skl))&~p10(sK6_skl))&((p9(sK6_skl)&(![X]: (~r1(sK6_skl,X)|p9(X))))&p9(sK6_skl))))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p9(Y)|sP6_prd(sK7_skl(Y),Y)))|p8(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p9(Y))|((~p8(Y)|sP7_prd(sK8_skl(Y),Y))|~p8(Y)))))|(sP8_prd(sK0_skl)|((((r1(sK0_skl,sK9_skl)&(p9(sK9_skl)&(![X]: (~r1(sK9_skl,X)|p9(X)))))&~p8(sK9_skl))&~p9(sK9_skl))&((p8(sK9_skl)&(![X]: (~r1(sK9_skl,X)|p8(X))))&p8(sK9_skl))))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p8(Y)|sP9_prd(sK10_skl(Y),Y)))|p7(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p8(Y))|((~p7(Y)|sP10_prd(sK11_skl(Y),Y))|~p7(Y)))))|(sP11_prd(sK0_skl)|((((r1(sK0_skl,sK12_skl)&(p8(sK12_skl)&(![X]: (~r1(sK12_skl,X)|p8(X)))))&~p7(sK12_skl))&~p8(sK12_skl))&((p7(sK12_skl)&(![X]: (~r1(sK12_skl,X)|p7(X))))&p7(sK12_skl))))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p7(Y)|sP12_prd(sK13_skl(Y),Y)))|p6(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p7(Y))|((~p6(Y)|sP13_prd(sK14_skl(Y),Y))|~p6(Y)))))|(sP14_prd(sK0_skl)|((((r1(sK0_skl,sK15_skl)&(p7(sK15_skl)&(![X]: (~r1(sK15_skl,X)|p7(X)))))&~p6(sK15_skl))&~p7(sK15_skl))&((p6(sK15_skl)&(![X]: (~r1(sK15_skl,X)|p6(X))))&p6(sK15_skl))))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p6(Y)|sP15_prd(sK16_skl(Y),Y)))|p5(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p6(Y))|((~p5(Y)|sP16_prd(sK17_skl(Y),Y))|~p5(Y)))))|(sP17_prd(sK0_skl)|((((r1(sK0_skl,sK18_skl)&(p6(sK18_skl)&(![X]: (~r1(sK18_skl,X)|p6(X)))))&~p5(sK18_skl))&~p6(sK18_skl))&((p5(sK18_skl)&(![X]: (~r1(sK18_skl,X)|p5(X))))&p5(sK18_skl))))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p5(Y)|sP18_prd(sK19_skl(Y),Y)))|p4(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p5(Y))|((~p4(Y)|sP19_prd(sK20_skl(Y),Y))|~p4(Y)))))|(sP20_prd(sK0_skl)|((((r1(sK0_skl,sK21_skl)&(p5(sK21_skl)&(![X]: (~r1(sK21_skl,X)|p5(X)))))&~p4(sK21_skl))&~p5(sK21_skl))&((p4(sK21_skl)&(![X]: (~r1(sK21_skl,X)|p4(X))))&p4(sK21_skl))))))&((r1(sK0_skl,sK22_skl)&~p10(sK22_skl))&((![X]: (~r1(sK22_skl,X)|p10(X)))&p10(sK22_skl))))&((r1(sK0_skl,sK23_skl)&~p10(sK23_skl))&((![X]: (~r1(sK23_skl,X)|p10(X)))&p10(sK23_skl))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p4(Y)|sP21_prd(sK24_skl(Y),Y)))|p3(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p4(Y))|((~p3(Y)|sP22_prd(sK25_skl(Y),Y))|~p3(Y)))))|(sP23_prd(sK0_skl)|((((r1(sK0_skl,sK26_skl)&(p4(sK26_skl)&(![X]: (~r1(sK26_skl,X)|p4(X)))))&~p3(sK26_skl))&~p4(sK26_skl))&((p3(sK26_skl)&(![X]: (~r1(sK26_skl,X)|p3(X))))&p3(sK26_skl))))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p3(Y)|sP24_prd(sK27_skl(Y),Y)))|p2(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p3(Y))|((~p2(Y)|sP25_prd(sK28_skl(Y),Y))|~p2(Y)))))|(sP26_prd(sK0_skl)|((((r1(sK0_skl,sK29_skl)&(p3(sK29_skl)&(![X]: (~r1(sK29_skl,X)|p3(X)))))&~p2(sK29_skl))&~p3(sK29_skl))&((p2(sK29_skl)&(![X]: (~r1(sK29_skl,X)|p2(X))))&p2(sK29_skl))))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p2(Y)|sP27_prd(sK30_skl(Y),Y)))|p1(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p2(Y))|((~p1(Y)|sP28_prd(sK31_skl(Y),Y))|~p1(Y)))))|(sP29_prd(sK0_skl)|((((r1(sK0_skl,sK32_skl)&(p2(sK32_skl)&(![X]: (~r1(sK32_skl,X)|p2(X)))))&~p1(sK32_skl))&~p2(sK32_skl))&((p1(sK32_skl)&(![X]: (~r1(sK32_skl,X)|p1(X))))&p1(sK32_skl))))))),
% 0.09/0.39 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]),skolemize(X,sK0_skl),skolemize(X,sK1_skl(Y)),skolemize(X,sK2_skl(Y)),skolemize(Y,sK3_skl),skolemize(X,sK4_skl(Y)),skolemize(X,sK5_skl(Y)),skolemize(Y,sK6_skl),skolemize(X,sK7_skl(Y)),skolemize(X,sK8_skl(Y)),skolemize(Y,sK9_skl),skolemize(X,sK10_skl(Y)),skolemize(X,sK11_skl(Y)),skolemize(Y,sK12_skl),skolemize(X,sK13_skl(Y)),skolemize(X,sK14_skl(Y)),skolemize(Y,sK15_skl),skolemize(X,sK16_skl(Y)),skolemize(X,sK17_skl(Y)),skolemize(Y,sK18_skl),skolemize(X,sK19_skl(Y)),skolemize(X,sK20_skl(Y)),skolemize(Y,sK21_skl),skolemize(Y,sK22_skl),skolemize(Y,sK23_skl),skolemize(X,sK24_skl(Y)),skolemize(X,sK25_skl(Y)),skolemize(Y,sK26_skl),skolemize(X,sK27_skl(Y)),skolemize(X,sK28_skl(Y)),skolemize(Y,sK29_skl),skolemize(X,sK30_skl(Y)),skolemize(X,sK31_skl(Y)),skolemize(Y,sK32_skl)],[f34])).
% 0.09/0.39 fof(f93,plain,(
% 0.09/0.39 ~p10(sK22_skl)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f35])).
% 0.09/0.39 fof(f95,plain,(
% 0.09/0.39 p10(sK22_skl)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f35])).
% 0.09/0.39 fof(f983,plain,(
% 0.09/0.39 $false),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f95,f93])).
% 0.09/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.42 % Elapsed time: 0.049690 seconds
% 0.09/0.42 % CPU time: 0.042929 seconds
% 0.09/0.42 % Total memory used: 2.349 MB
% 0.09/0.42 % Net memory used: 2.319 MB
%------------------------------------------------------------------------------